diff --git a/sidekick.opam b/sidekick.opam index 03a6a890..c9da08f3 100644 --- a/sidekick.opam +++ b/sidekick.opam @@ -15,6 +15,7 @@ depends: [ "containers" { >= "3.0" & < "4.0" } "iter" { >= "1.0" & < "2.0" } "ocaml" { >= "4.04" } + "zarith" { with-test } "alcotest" {with-test} "odoc" {with-doc} ] diff --git a/src/lra/tests/dune b/src/lra/tests/dune index 5661451c..df4bd73d 100644 --- a/src/lra/tests/dune +++ b/src/lra/tests/dune @@ -1,25 +1,15 @@ -(executable - (name run_tests) - (modules run_tests test_simplex2) - (libraries containers sidekick.arith-lra - sidekick.zarith zarith iter alcotest qcheck) - (flags :standard -warn-error -a+8 -color always)) -(alias - (name runtest) - (locks /test) - (package sidekick) - (action - (progn - (run ./run_tests.exe alcotest) ; run regressions first - (run ./run_tests.exe qcheck --verbose)))) +(library + (name sidekick_test_simplex2) + (libraries zarith sidekick.arith-lra sidekick.util sidekick.zarith + qcheck alcotest)) (rule - (targets test_simplex2.ml) + (targets sidekick_test_simplex2.ml) (enabled_if (>= %{ocaml_version} 4.08.0)) (action (copy test_simplex2.real.ml %{targets}))) (rule - (targets test_simplex2.ml) + (targets sidekick_test_simplex2.ml) (enabled_if (< %{ocaml_version} 4.08.0)) (action (with-stdout-to %{targets} (echo "let props=[];; let tests=\"simplex2\",[]")))) diff --git a/src/mini-cc/tests/dune b/src/mini-cc/tests/dune index 988a0170..4b0fe303 100644 --- a/src/mini-cc/tests/dune +++ b/src/mini-cc/tests/dune @@ -1,7 +1,4 @@ -(tests - (names tests) - (libraries sidekick.mini-cc sidekick-base alcotest) - (package sidekick-base) - (flags :standard -warn-error -a+8 -safe-string -color always) - (locks /test) - (modes native)) +(library + (name sidekick_test_minicc) + (libraries sidekick.mini-cc sidekick-base alcotest) + (flags :standard -warn-error -a+8)) diff --git a/src/mini-cc/tests/tests.ml b/src/mini-cc/tests/sidekick_test_minicc.ml similarity index 98% rename from src/mini-cc/tests/tests.ml rename to src/mini-cc/tests/sidekick_test_minicc.ml index 291d0d58..8671d1a1 100644 --- a/src/mini-cc/tests/tests.ml +++ b/src/mini-cc/tests/sidekick_test_minicc.ml @@ -40,7 +40,7 @@ module Setup() = struct let p t1 = app_l fun_p [t1] end -let l = ref [] +let l : unit Alcotest.test_case list ref = ref [] let mk_test name f = l := (name, `Quick, f) :: !l @@ -165,5 +165,4 @@ let () = mk_test "test_reg_1" @@ fun () -> A.(check bool) "is-unsat" (CC.check_sat cc) false; () -(* run alcotest *) -let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l] +let tests = "mini-cc", List.rev !l diff --git a/src/tests/dune b/src/tests/dune new file mode 100644 index 00000000..11edd0e1 --- /dev/null +++ b/src/tests/dune @@ -0,0 +1,16 @@ + +(executable + (name run_tests) + (modules run_tests) + (libraries containers alcotest qcheck sidekick.util + sidekick_test_simplex2 sidekick_test_util sidekick_test_minicc) + (flags :standard -warn-error -a+8 -color always)) + +(alias + (name runtest) + (locks /test) + (package sidekick) + (action + (progn + (run ./run_tests.exe alcotest) ; run regressions first + (run ./run_tests.exe qcheck --verbose)))) diff --git a/src/lra/tests/run_tests.ml b/src/tests/run_tests.ml similarity index 66% rename from src/lra/tests/run_tests.ml rename to src/tests/run_tests.ml index 2fd6a4f3..22ab6559 100644 --- a/src/lra/tests/run_tests.ml +++ b/src/tests/run_tests.ml @@ -1,11 +1,15 @@ -let tests : unit Alcotest.test list = [ - Test_simplex2.tests; -] +let tests : unit Alcotest.test list = + List.flatten @@ [ + [Sidekick_test_simplex2.tests]; + [Sidekick_test_minicc.tests]; + Sidekick_test_util.tests; + ] let props = List.flatten - [ Test_simplex2.props; + [ Sidekick_test_simplex2.props; + Sidekick_test_util.props; ] let () = diff --git a/src/util/Bitvec.ml b/src/util/Bitvec.ml new file mode 100644 index 00000000..ab861ea7 --- /dev/null +++ b/src/util/Bitvec.ml @@ -0,0 +1,59 @@ + +module I32Vec = Vec +type i32vec = int Vec.t + +type t = { + mutable chunks: bytes; (* TODO: use a in32vec with bigarray *) +} + +let create () : t = { + chunks = Bytes.make 32 '\x00'; +} + +let n_bits_ = 8 +let i2c = Char.chr +let c2i = Char.code + +(* from index to offset in bytes *) +let[@inline] idx_bytes_ (i:int) : int = i lsr 3 + +(* from index to offset in a single char *) +let mask_ = 0b111 + +(* number of bytes *) +let[@inline] len_ (self:t) : int = Bytes.length self.chunks + +let[@inline never] resize_ self idx : unit = + let new_size = + min Sys.max_string_length + (max (idx+2) (let l = len_ self in l + 10 + l / 2)) + in + let new_chunks = Bytes.make new_size (i2c 0) in + Bytes.blit self.chunks 0 new_chunks 0 (len_ self); + self.chunks <- new_chunks; + assert (len_ self > idx) + +let[@inline] ensure_size self i = + let idx = idx_bytes_ i in + if idx >= len_ self then ( + resize_ self idx + ) + +let[@inline] get self i : bool = + let idx = idx_bytes_ i in + let c = c2i (Bytes.get self.chunks idx) in + (c land (1 lsl (i land mask_))) <> 0 + +let set self i b : unit = + let idx = idx_bytes_ i in + let c = c2i (Bytes.get self.chunks idx) in + let c = + if b + then c lor (1 lsl (i land mask_)) + else c land (lnot (1 lsl (i land mask_))) + in + Bytes.set self.chunks idx (i2c c) + +let clear_all self = + Bytes.fill self.chunks 0 (len_ self) '\x00' + diff --git a/src/util/Bitvec.mli b/src/util/Bitvec.mli new file mode 100644 index 00000000..fc65d8f1 --- /dev/null +++ b/src/util/Bitvec.mli @@ -0,0 +1,15 @@ + +(** Bitvector *) + +type t + +val create : unit -> t + +val ensure_size : t -> int -> unit +(** [ensure_size bv i] ensures that [i] is a valid index in [bv] *) + +val get : t -> int -> bool + +val set : t -> int -> bool -> unit + +val clear_all : t -> unit diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index 09b56058..e1de8bfd 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -4,6 +4,7 @@ module Fmt = CCFormat module Util = Util module Vec = Vec +module Bitvec = Bitvec module Log = Log module Backtrack_stack = Backtrack_stack module Backtrackable_tbl = Backtrackable_tbl diff --git a/src/util/tests/dune b/src/util/tests/dune new file mode 100644 index 00000000..94e4a21a --- /dev/null +++ b/src/util/tests/dune @@ -0,0 +1,5 @@ + +(library + (name sidekick_test_util) + (flags :standard -warn-error -a+8 -open Sidekick_util) + (libraries qcheck alcotest sidekick.util)) diff --git a/src/util/tests/sidekick_test_util.ml b/src/util/tests/sidekick_test_util.ml new file mode 100644 index 00000000..963f09a6 --- /dev/null +++ b/src/util/tests/sidekick_test_util.ml @@ -0,0 +1,5 @@ + +let tests = [Test_bitvec.tests] + +let props = [ +] diff --git a/src/util/tests/test_bitvec.ml b/src/util/tests/test_bitvec.ml new file mode 100644 index 00000000..2a5d7ce6 --- /dev/null +++ b/src/util/tests/test_bitvec.ml @@ -0,0 +1,30 @@ + +module A = Alcotest + +let spf = Printf.sprintf +let msgline line = spf "test at line %d" line +let alco_mk name f = name, `Quick, f + +module BV = Bitvec + +let t1 = alco_mk "mkgetset" @@ fun () -> + let bv = BV.create() in + BV.ensure_size bv 200; + A.(check bool) (msgline __LINE__) false (BV.get bv 0); + A.(check bool) (msgline __LINE__) false (BV.get bv 1); + for i=30 to 150 do + A.(check bool) (msgline __LINE__) false (BV.get bv i); + done; + + BV.set bv 25 true; + BV.set bv 1 true; + BV.set bv 127 true; + BV.set bv 126 true; + BV.set bv 126 false; + + for i=0 to 150 do + A.(check bool) (msgline __LINE__) (i=1||i=25||i=127) (BV.get bv i); + done; + () + +let tests = "bitvec", [t1]