Add bitvector library (wip)

formalsec · Feb 12, 2025 · 8e1c6e0 · 8e1c6e0
1 parent 8393d76
commit 8e1c6e0
Show file tree

Hide file tree

Showing 77 changed files with 81 additions and 10 deletions.
diff --git a/bin/dune b/bin/dune
@@ -1,4 +1,5 @@
 (executable
+ (package smtml)
  (name main)
  (public_name smtml)
  (libraries cmdliner smtml)

diff --git a/bitvector.opam b/bitvector.opam
@@ -0,0 +1,39 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Another Arbitrary-Width Bitvectors using the Zarith Library"
+description: "Arbitrary-Width Bitvectors using the Zarith Library"
+maintainer: ["Filipe Marques <[email protected]>"]
+authors: [
+  "João Pereira <[email protected]>"
+  "Filipe Marques <[email protected]>"
+  "Hichem Rami Ait El Hara <[email protected]>"
+  "Léo Andrès <[email protected]>"
+  "Arthur Carcano <[email protected]>"
+  "Pierre Chambart <[email protected]>"
+  "José Fragoso Santos <[email protected]>"
+]
+license: "MIT"
+homepage: "https://github.com/formalsec/smtml"
+doc: "https://formalsec.github.io/smtml/smtml/index.html"
+bug-reports: "https://github.com/formalsec/smtml/issues"
+depends: [
+  "dune" {>= "3.10"}
+  "ocaml" {>= "4.14.0"}
+  "zartih"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/formalsec/smtml.git"
diff --git a/dune-project b/dune-project
@@ -26,6 +26,15 @@
 
 (license "MIT")
 
+(package
+ (name bitvector)
+ (synopsis "Another Arbitrary-Width Bitvectors using the Zarith Library")
+ (description "Arbitrary-Width Bitvectors using the Zarith Library")
+ (depends
+  (ocaml
+   (>= "4.14.0"))
+  zarith))
+
 (package
  (name smtml)
  (synopsis "An SMT solver frontend for OCaml")

diff --git a/src/bisect.exclude b/src/bisect.exclude
@@ -1,3 +1,3 @@
-file "src/colibri2_mappings.ml"
-file "src/bitwuzla_mappings.ml"
-file "src/cvc5_mappings.ml"
+file "src/smtml/colibri2_mappings.ml"
+file "src/smtml/bitwuzla_mappings.ml"
+file "src/smtml/cvc5_mappings.ml"
diff --git a/src/bitvector/bitv.ml b/src/bitvector/bitv.ml
@@ -0,0 +1,10 @@
+type t =
+  { value : Z.t
+  ; width : int
+  }
+
+let make v m = { value = v; width = m }
+
+let view { value; _ } = value
+
+let numbits { width; _ } = width
diff --git a/src/bitvector/bitv.mli b/src/bitvector/bitv.mli
@@ -0,0 +1,7 @@
+type t
+
+val make : Z.t -> int -> t
+
+val view : t -> Z.t
+
+val numbits : t -> int
diff --git a/src/bitvector/dune b/src/bitvector/dune
@@ -0,0 +1,5 @@
+(library
+ (name bitvector)
+ (public_name bitvector)
+ (modules bitv)
+ (libraries zarith))
diff --git a/src/altergo_mappings.default.ml → src/smtml/altergo_mappings.default.ml b/src/altergo_mappings.default.ml → src/smtml/altergo_mappings.default.ml
diff --git a/src/ast.ml → src/smtml/ast.ml b/src/ast.ml → src/smtml/ast.ml
diff --git a/src/ast.mli → src/smtml/ast.mli b/src/ast.mli → src/smtml/ast.mli
diff --git a/src/axioms.ml → src/smtml/axioms.ml b/src/axioms.ml → src/smtml/axioms.ml
diff --git a/src/binder.ml → src/smtml/binder.ml b/src/binder.ml → src/smtml/binder.ml
diff --git a/src/bitwuzla_mappings.default.ml → src/smtml/bitwuzla_mappings.default.ml b/src/bitwuzla_mappings.default.ml → src/smtml/bitwuzla_mappings.default.ml
diff --git a/src/bitwuzla_mappings.mli → src/smtml/bitwuzla_mappings.mli b/src/bitwuzla_mappings.mli → src/smtml/bitwuzla_mappings.mli
diff --git a/src/cache.ml → src/smtml/cache.ml b/src/cache.ml → src/smtml/cache.ml
diff --git a/src/cache.mli → src/smtml/cache.mli b/src/cache.mli → src/smtml/cache.mli
diff --git a/src/cache_intf.ml → src/smtml/cache_intf.ml b/src/cache_intf.ml → src/smtml/cache_intf.ml
diff --git a/src/colibri2_mappings.default.ml → src/smtml/colibri2_mappings.default.ml b/src/colibri2_mappings.default.ml → src/smtml/colibri2_mappings.default.ml
diff --git a/src/colibri2_mappings.mli → src/smtml/colibri2_mappings.mli b/src/colibri2_mappings.mli → src/smtml/colibri2_mappings.mli
diff --git a/src/compile.ml → src/smtml/compile.ml b/src/compile.ml → src/smtml/compile.ml
diff --git a/src/constructors_intf.ml → src/smtml/constructors_intf.ml b/src/constructors_intf.ml → src/smtml/constructors_intf.ml
diff --git a/src/cvc5_mappings.default.ml → src/smtml/cvc5_mappings.default.ml b/src/cvc5_mappings.default.ml → src/smtml/cvc5_mappings.default.ml
diff --git a/src/cvc5_mappings.mli → src/smtml/cvc5_mappings.mli b/src/cvc5_mappings.mli → src/smtml/cvc5_mappings.mli
diff --git a/src/dolmenexpr_to_expr.ml → src/smtml/dolmenexpr_to_expr.ml b/src/dolmenexpr_to_expr.ml → src/smtml/dolmenexpr_to_expr.ml
diff --git a/src/dolmenexpr_to_expr.mli → src/smtml/dolmenexpr_to_expr.mli b/src/dolmenexpr_to_expr.mli → src/smtml/dolmenexpr_to_expr.mli
diff --git a/src/dune → src/smtml/dune b/src/dune → src/smtml/dune
@@ -1,9 +1,3 @@
-(library
- (name smtml_prelude)
- (public_name smtml.prelude)
- (modules smtml_prelude)
- (libraries prelude))
-
 (ocamllex
  (modules lexer))
 

diff --git a/src/eval.ml → src/smtml/eval.ml b/src/eval.ml → src/smtml/eval.ml
diff --git a/src/eval.mli → src/smtml/eval.mli b/src/eval.mli → src/smtml/eval.mli
diff --git a/src/expr.ml → src/smtml/expr.ml b/src/expr.ml → src/smtml/expr.ml
@@ -498,7 +498,8 @@ let concat (msb : t) (lsb : t) : t =
 let rec simplify_expr ?(rm_extract = true) (hte : t) : t =
   match view hte with
   | Val _ | Symbol _ -> hte
-  | Ptr { base; offset } -> ptr base (simplify_expr offset)
+  | Ptr { base; offset } ->
+      binop (Ty_bitv 32) Add (value (Num (I32 base))) offset
   | List es -> make @@ List (List.map simplify_expr es)
   | App (x, es) -> make @@ App (x, List.map simplify_expr es)
   | Unop (ty, op, e) ->

diff --git a/src/expr.mli → src/smtml/expr.mli b/src/expr.mli → src/smtml/expr.mli
diff --git a/src/interpret.ml → src/smtml/interpret.ml b/src/interpret.ml → src/smtml/interpret.ml
diff --git a/src/interpret.mli → src/smtml/interpret.mli b/src/interpret.mli → src/smtml/interpret.mli
diff --git a/src/interpret_intf.ml → src/smtml/interpret_intf.ml b/src/interpret_intf.ml → src/smtml/interpret_intf.ml
diff --git a/src/lexer.mll → src/smtml/lexer.mll b/src/lexer.mll → src/smtml/lexer.mll
diff --git a/src/log.ml → src/smtml/log.ml b/src/log.ml → src/smtml/log.ml
diff --git a/src/logic.ml → src/smtml/logic.ml b/src/logic.ml → src/smtml/logic.ml
diff --git a/src/mappings.ml → src/smtml/mappings.ml b/src/mappings.ml → src/smtml/mappings.ml
diff --git a/src/mappings.nop.ml → src/smtml/mappings.nop.ml b/src/mappings.nop.ml → src/smtml/mappings.nop.ml
diff --git a/src/mappings_intf.ml → src/smtml/mappings_intf.ml b/src/mappings_intf.ml → src/smtml/mappings_intf.ml
diff --git a/src/model.ml → src/smtml/model.ml b/src/model.ml → src/smtml/model.ml
diff --git a/src/model.mli → src/smtml/model.mli b/src/model.mli → src/smtml/model.mli
diff --git a/src/num.ml → src/smtml/num.ml b/src/num.ml → src/smtml/num.ml
diff --git a/src/num.mli → src/smtml/num.mli b/src/num.mli → src/smtml/num.mli
diff --git a/src/op_intf.ml → src/smtml/op_intf.ml b/src/op_intf.ml → src/smtml/op_intf.ml
diff --git a/src/optimizer.ml → src/smtml/optimizer.ml b/src/optimizer.ml → src/smtml/optimizer.ml
diff --git a/src/optimizer.mli → src/smtml/optimizer.mli b/src/optimizer.mli → src/smtml/optimizer.mli
diff --git a/src/optimizer_intf.ml → src/smtml/optimizer_intf.ml b/src/optimizer_intf.ml → src/smtml/optimizer_intf.ml
diff --git a/src/params.ml → src/smtml/params.ml b/src/params.ml → src/smtml/params.ml
diff --git a/src/params.mli → src/smtml/params.mli b/src/params.mli → src/smtml/params.mli
diff --git a/src/parse.ml → src/smtml/parse.ml b/src/parse.ml → src/smtml/parse.ml
diff --git a/src/parse.mli → src/smtml/parse.mli b/src/parse.mli → src/smtml/parse.mli
diff --git a/src/parser.mly → src/smtml/parser.mly b/src/parser.mly → src/smtml/parser.mly
diff --git a/src/rewrite.ml → src/smtml/rewrite.ml b/src/rewrite.ml → src/smtml/rewrite.ml
diff --git a/src/smtlib.ml → src/smtml/smtlib.ml b/src/smtlib.ml → src/smtml/smtlib.ml
diff --git a/src/altergo_mappings.mli → src/smtml/smtmlaltergo_mappings.mli b/src/altergo_mappings.mli → src/smtml/smtmlaltergo_mappings.mli
diff --git a/src/solver.ml → src/smtml/solver.ml b/src/solver.ml → src/smtml/solver.ml
diff --git a/src/solver.mli → src/smtml/solver.mli b/src/solver.mli → src/smtml/solver.mli
diff --git a/src/solver_dispatcher.ml → src/smtml/solver_dispatcher.ml b/src/solver_dispatcher.ml → src/smtml/solver_dispatcher.ml
diff --git a/src/solver_dispatcher.mli → src/smtml/solver_dispatcher.mli b/src/solver_dispatcher.mli → src/smtml/solver_dispatcher.mli
diff --git a/src/solver_intf.ml → src/smtml/solver_intf.ml b/src/solver_intf.ml → src/smtml/solver_intf.ml
diff --git a/src/solver_mode.ml → src/smtml/solver_mode.ml b/src/solver_mode.ml → src/smtml/solver_mode.ml
diff --git a/src/solver_mode.mli → src/smtml/solver_mode.mli b/src/solver_mode.mli → src/smtml/solver_mode.mli
diff --git a/src/solver_type.ml → src/smtml/solver_type.ml b/src/solver_type.ml → src/smtml/solver_type.ml
diff --git a/src/solver_type.mli → src/smtml/solver_type.mli b/src/solver_type.mli → src/smtml/solver_type.mli
diff --git a/src/statistics.ml → src/smtml/statistics.ml b/src/statistics.ml → src/smtml/statistics.ml
diff --git a/src/statistics.mli → src/smtml/statistics.mli b/src/statistics.mli → src/smtml/statistics.mli
diff --git a/src/symbol.ml → src/smtml/symbol.ml b/src/symbol.ml → src/smtml/symbol.ml
diff --git a/src/symbol.mli → src/smtml/symbol.mli b/src/symbol.mli → src/smtml/symbol.mli
diff --git a/src/ty.ml → src/smtml/ty.ml b/src/ty.ml → src/smtml/ty.ml
diff --git a/src/ty.mli → src/smtml/ty.mli b/src/ty.mli → src/smtml/ty.mli
diff --git a/src/utils.ml → src/smtml/utils.ml b/src/utils.ml → src/smtml/utils.ml
diff --git a/src/value.ml → src/smtml/value.ml b/src/value.ml → src/smtml/value.ml
diff --git a/src/value.mli → src/smtml/value.mli b/src/value.mli → src/smtml/value.mli
diff --git a/src/z3_mappings.default.ml → src/smtml/z3_mappings.default.ml b/src/z3_mappings.default.ml → src/smtml/z3_mappings.default.ml
diff --git a/src/z3_mappings.mli → src/smtml/z3_mappings.mli b/src/z3_mappings.mli → src/smtml/z3_mappings.mli
diff --git a/src/smtml_prelude/dune b/src/smtml_prelude/dune
@@ -0,0 +1,5 @@
+(library
+ (name smtml_prelude)
+ (public_name smtml.prelude)
+ (modules smtml_prelude)
+ (libraries prelude))
diff --git a/src/smtml_prelude.ml → src/smtml_prelude/smtml_prelude.ml b/src/smtml_prelude.ml → src/smtml_prelude/smtml_prelude.ml