diff --git a/bin/dune b/bin/dune index 26d20101..15504bb4 100644 --- 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 new file mode 100644 index 00000000..98f9ce63 --- /dev/null +++ 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 "] +authors: [ + "João Pereira " + "Filipe Marques " + "Hichem Rami Ait El Hara " + "Léo Andrès " + "Arthur Carcano " + "Pierre Chambart " + "José Fragoso Santos " +] +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 index 89ad5c2f..12433262 100644 --- 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")) + zartih)) + (package (name smtml) (synopsis "An SMT solver frontend for OCaml") diff --git a/src/bisect.exclude b/src/bisect.exclude index 154c460e..1ab5cd59 100644 --- 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 new file mode 100644 index 00000000..952550aa --- /dev/null +++ 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 new file mode 100644 index 00000000..2a892494 --- /dev/null +++ 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 new file mode 100644 index 00000000..c45bf4d5 --- /dev/null +++ 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 b/src/smtml/altergo_mappings.default.ml similarity index 100% rename from src/altergo_mappings.default.ml rename to src/smtml/altergo_mappings.default.ml diff --git a/src/ast.ml b/src/smtml/ast.ml similarity index 100% rename from src/ast.ml rename to src/smtml/ast.ml diff --git a/src/ast.mli b/src/smtml/ast.mli similarity index 100% rename from src/ast.mli rename to src/smtml/ast.mli diff --git a/src/axioms.ml b/src/smtml/axioms.ml similarity index 100% rename from src/axioms.ml rename to src/smtml/axioms.ml diff --git a/src/binder.ml b/src/smtml/binder.ml similarity index 100% rename from src/binder.ml rename to src/smtml/binder.ml diff --git a/src/bitwuzla_mappings.default.ml b/src/smtml/bitwuzla_mappings.default.ml similarity index 100% rename from src/bitwuzla_mappings.default.ml rename to src/smtml/bitwuzla_mappings.default.ml diff --git a/src/bitwuzla_mappings.mli b/src/smtml/bitwuzla_mappings.mli similarity index 100% rename from src/bitwuzla_mappings.mli rename to src/smtml/bitwuzla_mappings.mli diff --git a/src/cache.ml b/src/smtml/cache.ml similarity index 100% rename from src/cache.ml rename to src/smtml/cache.ml diff --git a/src/cache.mli b/src/smtml/cache.mli similarity index 100% rename from src/cache.mli rename to src/smtml/cache.mli diff --git a/src/cache_intf.ml b/src/smtml/cache_intf.ml similarity index 100% rename from src/cache_intf.ml rename to src/smtml/cache_intf.ml diff --git a/src/colibri2_mappings.default.ml b/src/smtml/colibri2_mappings.default.ml similarity index 100% rename from src/colibri2_mappings.default.ml rename to src/smtml/colibri2_mappings.default.ml diff --git a/src/colibri2_mappings.mli b/src/smtml/colibri2_mappings.mli similarity index 100% rename from src/colibri2_mappings.mli rename to src/smtml/colibri2_mappings.mli diff --git a/src/compile.ml b/src/smtml/compile.ml similarity index 100% rename from src/compile.ml rename to src/smtml/compile.ml diff --git a/src/constructors_intf.ml b/src/smtml/constructors_intf.ml similarity index 100% rename from src/constructors_intf.ml rename to src/smtml/constructors_intf.ml diff --git a/src/cvc5_mappings.default.ml b/src/smtml/cvc5_mappings.default.ml similarity index 100% rename from src/cvc5_mappings.default.ml rename to src/smtml/cvc5_mappings.default.ml diff --git a/src/cvc5_mappings.mli b/src/smtml/cvc5_mappings.mli similarity index 100% rename from src/cvc5_mappings.mli rename to src/smtml/cvc5_mappings.mli diff --git a/src/dolmenexpr_to_expr.ml b/src/smtml/dolmenexpr_to_expr.ml similarity index 100% rename from src/dolmenexpr_to_expr.ml rename to src/smtml/dolmenexpr_to_expr.ml diff --git a/src/dolmenexpr_to_expr.mli b/src/smtml/dolmenexpr_to_expr.mli similarity index 100% rename from src/dolmenexpr_to_expr.mli rename to src/smtml/dolmenexpr_to_expr.mli diff --git a/src/dune b/src/smtml/dune similarity index 96% rename from src/dune rename to src/smtml/dune index 205bd2ed..272f0829 100644 --- a/src/dune +++ b/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 b/src/smtml/eval.ml similarity index 100% rename from src/eval.ml rename to src/smtml/eval.ml diff --git a/src/eval.mli b/src/smtml/eval.mli similarity index 100% rename from src/eval.mli rename to src/smtml/eval.mli diff --git a/src/expr.ml b/src/smtml/expr.ml similarity index 99% rename from src/expr.ml rename to src/smtml/expr.ml index aed78879..373e81ac 100644 --- a/src/expr.ml +++ b/src/smtml/expr.ml @@ -498,7 +498,9 @@ 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 } -> + (* FIXME: *) + 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 b/src/smtml/expr.mli similarity index 100% rename from src/expr.mli rename to src/smtml/expr.mli diff --git a/src/interpret.ml b/src/smtml/interpret.ml similarity index 100% rename from src/interpret.ml rename to src/smtml/interpret.ml diff --git a/src/interpret.mli b/src/smtml/interpret.mli similarity index 100% rename from src/interpret.mli rename to src/smtml/interpret.mli diff --git a/src/interpret_intf.ml b/src/smtml/interpret_intf.ml similarity index 100% rename from src/interpret_intf.ml rename to src/smtml/interpret_intf.ml diff --git a/src/lexer.mll b/src/smtml/lexer.mll similarity index 100% rename from src/lexer.mll rename to src/smtml/lexer.mll diff --git a/src/log.ml b/src/smtml/log.ml similarity index 100% rename from src/log.ml rename to src/smtml/log.ml diff --git a/src/logic.ml b/src/smtml/logic.ml similarity index 100% rename from src/logic.ml rename to src/smtml/logic.ml diff --git a/src/mappings.ml b/src/smtml/mappings.ml similarity index 100% rename from src/mappings.ml rename to src/smtml/mappings.ml diff --git a/src/mappings.nop.ml b/src/smtml/mappings.nop.ml similarity index 100% rename from src/mappings.nop.ml rename to src/smtml/mappings.nop.ml diff --git a/src/mappings_intf.ml b/src/smtml/mappings_intf.ml similarity index 100% rename from src/mappings_intf.ml rename to src/smtml/mappings_intf.ml diff --git a/src/model.ml b/src/smtml/model.ml similarity index 100% rename from src/model.ml rename to src/smtml/model.ml diff --git a/src/model.mli b/src/smtml/model.mli similarity index 100% rename from src/model.mli rename to src/smtml/model.mli diff --git a/src/num.ml b/src/smtml/num.ml similarity index 100% rename from src/num.ml rename to src/smtml/num.ml diff --git a/src/num.mli b/src/smtml/num.mli similarity index 100% rename from src/num.mli rename to src/smtml/num.mli diff --git a/src/op_intf.ml b/src/smtml/op_intf.ml similarity index 100% rename from src/op_intf.ml rename to src/smtml/op_intf.ml diff --git a/src/optimizer.ml b/src/smtml/optimizer.ml similarity index 100% rename from src/optimizer.ml rename to src/smtml/optimizer.ml diff --git a/src/optimizer.mli b/src/smtml/optimizer.mli similarity index 100% rename from src/optimizer.mli rename to src/smtml/optimizer.mli diff --git a/src/optimizer_intf.ml b/src/smtml/optimizer_intf.ml similarity index 100% rename from src/optimizer_intf.ml rename to src/smtml/optimizer_intf.ml diff --git a/src/params.ml b/src/smtml/params.ml similarity index 100% rename from src/params.ml rename to src/smtml/params.ml diff --git a/src/params.mli b/src/smtml/params.mli similarity index 100% rename from src/params.mli rename to src/smtml/params.mli diff --git a/src/parse.ml b/src/smtml/parse.ml similarity index 100% rename from src/parse.ml rename to src/smtml/parse.ml diff --git a/src/parse.mli b/src/smtml/parse.mli similarity index 100% rename from src/parse.mli rename to src/smtml/parse.mli diff --git a/src/parser.mly b/src/smtml/parser.mly similarity index 100% rename from src/parser.mly rename to src/smtml/parser.mly diff --git a/src/rewrite.ml b/src/smtml/rewrite.ml similarity index 100% rename from src/rewrite.ml rename to src/smtml/rewrite.ml diff --git a/src/smtlib.ml b/src/smtml/smtlib.ml similarity index 100% rename from src/smtlib.ml rename to src/smtml/smtlib.ml diff --git a/src/altergo_mappings.mli b/src/smtml/smtmlaltergo_mappings.mli similarity index 100% rename from src/altergo_mappings.mli rename to src/smtml/smtmlaltergo_mappings.mli diff --git a/src/solver.ml b/src/smtml/solver.ml similarity index 100% rename from src/solver.ml rename to src/smtml/solver.ml diff --git a/src/solver.mli b/src/smtml/solver.mli similarity index 100% rename from src/solver.mli rename to src/smtml/solver.mli diff --git a/src/solver_dispatcher.ml b/src/smtml/solver_dispatcher.ml similarity index 100% rename from src/solver_dispatcher.ml rename to src/smtml/solver_dispatcher.ml diff --git a/src/solver_dispatcher.mli b/src/smtml/solver_dispatcher.mli similarity index 100% rename from src/solver_dispatcher.mli rename to src/smtml/solver_dispatcher.mli diff --git a/src/solver_intf.ml b/src/smtml/solver_intf.ml similarity index 100% rename from src/solver_intf.ml rename to src/smtml/solver_intf.ml diff --git a/src/solver_mode.ml b/src/smtml/solver_mode.ml similarity index 100% rename from src/solver_mode.ml rename to src/smtml/solver_mode.ml diff --git a/src/solver_mode.mli b/src/smtml/solver_mode.mli similarity index 100% rename from src/solver_mode.mli rename to src/smtml/solver_mode.mli diff --git a/src/solver_type.ml b/src/smtml/solver_type.ml similarity index 100% rename from src/solver_type.ml rename to src/smtml/solver_type.ml diff --git a/src/solver_type.mli b/src/smtml/solver_type.mli similarity index 100% rename from src/solver_type.mli rename to src/smtml/solver_type.mli diff --git a/src/statistics.ml b/src/smtml/statistics.ml similarity index 100% rename from src/statistics.ml rename to src/smtml/statistics.ml diff --git a/src/statistics.mli b/src/smtml/statistics.mli similarity index 100% rename from src/statistics.mli rename to src/smtml/statistics.mli diff --git a/src/symbol.ml b/src/smtml/symbol.ml similarity index 100% rename from src/symbol.ml rename to src/smtml/symbol.ml diff --git a/src/symbol.mli b/src/smtml/symbol.mli similarity index 100% rename from src/symbol.mli rename to src/smtml/symbol.mli diff --git a/src/ty.ml b/src/smtml/ty.ml similarity index 100% rename from src/ty.ml rename to src/smtml/ty.ml diff --git a/src/ty.mli b/src/smtml/ty.mli similarity index 100% rename from src/ty.mli rename to src/smtml/ty.mli diff --git a/src/utils.ml b/src/smtml/utils.ml similarity index 100% rename from src/utils.ml rename to src/smtml/utils.ml diff --git a/src/value.ml b/src/smtml/value.ml similarity index 100% rename from src/value.ml rename to src/smtml/value.ml diff --git a/src/value.mli b/src/smtml/value.mli similarity index 100% rename from src/value.mli rename to src/smtml/value.mli diff --git a/src/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml similarity index 100% rename from src/z3_mappings.default.ml rename to src/smtml/z3_mappings.default.ml diff --git a/src/z3_mappings.mli b/src/smtml/z3_mappings.mli similarity index 100% rename from src/z3_mappings.mli rename to src/smtml/z3_mappings.mli diff --git a/src/smtml_prelude/dune b/src/smtml_prelude/dune new file mode 100644 index 00000000..00464e21 --- /dev/null +++ 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 b/src/smtml_prelude/smtml_prelude.ml similarity index 100% rename from src/smtml_prelude.ml rename to src/smtml_prelude/smtml_prelude.ml