From 27590d753b6de825165f763c172d6e436ccb4b46 Mon Sep 17 00:00:00 2001 From: Zain Aamer Date: Fri, 16 Aug 2024 13:41:10 -0400 Subject: [PATCH] [CN] Add OUnit testing for pure term evaluation --- backend/cn/dune | 2 +- backend/cn/tests/dune | 25 ++++ backend/cn/tests/eval.ml | 260 ++++++++++++++++++++++++++++++++++ backend/cn/tests/main.ml | 3 + backend/cn/tests/testUtils.ml | 6 + cn.opam | 3 + 6 files changed, 298 insertions(+), 1 deletion(-) create mode 100644 backend/cn/tests/dune create mode 100644 backend/cn/tests/eval.ml create mode 100644 backend/cn/tests/main.ml create mode 100644 backend/cn/tests/testUtils.ml diff --git a/backend/cn/dune b/backend/cn/dune index 3a6b3e885..a6986ae87 100644 --- a/backend/cn/dune +++ b/backend/cn/dune @@ -1 +1 @@ -(dirs lib bin) +(dirs lib bin tests) diff --git a/backend/cn/tests/dune b/backend/cn/tests/dune new file mode 100644 index 000000000..a6ca06ed5 --- /dev/null +++ b/backend/cn/tests/dune @@ -0,0 +1,25 @@ +(include_subdirs qualified) + +(executable + (name main) + (public_name cn_tests) + (package cn) + (modes exe) + (flags + (:standard -w -37 -open Monomorphic.Int)) + (libraries + cerb_backend + cerb_frontend + cerb_util + cn + mem_concrete + menhirLib + monomorphic + ocamlgraph + ounit2 + result + qcheck + qcheck-ounit + str + unix + z3)) diff --git a/backend/cn/tests/eval.ml b/backend/cn/tests/eval.ml new file mode 100644 index 000000000..e87bb0579 --- /dev/null +++ b/backend/cn/tests/eval.ml @@ -0,0 +1,260 @@ +module BT = Cn.BaseTypes +module IT = Cn.IndexTerms +module LC = Cn.LogicalConstraints +open Cn +open Eval +open OUnit2 + +let test_tuple = + TestUtils.test_name __FUNCTION__ + >:: fun _ -> + let here = Locations.other __FUNCTION__ in + let bt = BT.Datatype (Sym.fresh_named "bt") in + let it_res = IT.num_lit_ (Z.of_int 21) BT.Integer here in + let it_tuple = IT.tuple_ [ IT.sym_ (Sym.fresh (), bt, here); it_res ] here in + let it_nth = IT.nthTuple_ ~item_bt:BT.Integer (1, it_tuple) here in + let printer r = match r with Ok it -> Pp.plain (IT.pp it) | Error err -> err in + assert_equal + ~printer + ~cmp:(Result.equal ~ok:IT.equal ~error:(fun _ _ -> false)) + ~msg:"Lazy evaluation did not step" + (Ok it_res) + (eval ~mode:Lazy it_nth); + assert_bool + "Strict evaluation did not get stuck on free variables" + (eval ~mode:Strict it_nth |> Result.is_error) + + +let test_struct = + TestUtils.test_name __FUNCTION__ + >:: fun _ -> + let here = Locations.other __FUNCTION__ in + let bt = BT.Datatype (Sym.fresh_named "bt") in + let mem_id = Id.id "member" in + let it_res = IT.num_lit_ (Z.of_int 21) BT.Integer here in + let it_struct = + IT.struct_ + ( Sym.fresh (), + [ (Id.id "filler", IT.sym_ (Sym.fresh (), bt, here)); (mem_id, it_res) ] ) + here + in + let it_member = IT.member_ ~member_bt:BT.Integer (it_struct, mem_id) here in + let printer r = match r with Ok it -> Pp.plain (IT.pp it) | Error err -> err in + assert_equal + ~printer + ~cmp:(Result.equal ~ok:IT.equal ~error:(fun _ _ -> false)) + ~msg:"Lazy evaluation did not step" + (Ok it_res) + (eval ~mode:Lazy it_member); + assert_bool + "Strict evaluation did not get stuck on free variables" + (eval ~mode:Strict it_member |> Result.is_error) + + +let test_record = + TestUtils.test_name __FUNCTION__ + >:: fun _ -> + let here = Locations.other __FUNCTION__ in + let bt = BT.Datatype (Sym.fresh_named "bt") in + let mem_id = Id.id "member" in + let it_res = IT.num_lit_ (Z.of_int 21) BT.Integer here in + let it_record = + IT.record_ + [ (Id.id "filler", IT.sym_ (Sym.fresh (), bt, here)); (mem_id, it_res) ] + here + in + let it_member = IT.recordMember_ ~member_bt:BT.Integer (it_record, mem_id) here in + let printer r = match r with Ok it -> Pp.plain (IT.pp it) | Error err -> err in + assert_equal + ~printer + ~cmp:(Result.equal ~ok:IT.equal ~error:(fun _ _ -> false)) + ~msg:"Lazy evaluation did not step" + (Ok it_res) + (eval ~mode:Lazy it_member); + assert_bool + "Strict evaluation did not get stuck on free variables" + (eval ~mode:Strict it_member |> Result.is_error) + + +let test_constructor = + TestUtils.test_name __FUNCTION__ + >:: fun _ -> + let here = Locations.other __FUNCTION__ in + let constr_sym = Sym.fresh_named "constr" in + let member = Id.id "abc" in + let bt = BT.Datatype (Sym.fresh_named "bt") in + let it_constr = + IT.IT + (Constructor (constr_sym, [ (member, IT.sym_ (Sym.fresh (), bt, here)) ]), bt, here) + in + let it_match = + IT.IT + ( Match + ( it_constr, + [ ( Pat + ( PConstructor (constr_sym, [ (member, Pat (PWild, bt, here)) ]), + bt, + here ), + IT.bool_ true here ) + ] ), + BT.Bool, + here ) + in + let printer r = match r with Ok it -> Pp.plain (IT.pp it) | Error err -> err in + assert_equal + ~printer + ~cmp:(Result.equal ~ok:IT.equal ~error:(fun _ _ -> false)) + ~msg:"Lazy evaluation did not step" + (Ok (IT.bool_ true here)) + (eval ~mode:Lazy it_match); + assert_bool + "Strict evaluation did not get stuck on free variables" + (eval ~mode:Strict it_match |> Result.is_error) + + +let test_apply_rename = + TestUtils.test_name __FUNCTION__ + >:: fun _ -> + let here = Locations.other __FUNCTION__ in + let x_sym = Sym.fresh_named "x" in + let y_sym = Sym.fresh_named "y" in + let y_sym' = Sym.fresh_named "y" in + let it mode = + IT.let_ + ( (x_sym, IT.sym_ (y_sym, BT.Integer, here)), + IT.let_ + ( (y_sym', IT.num_lit_ (Z.of_int 10) BT.Integer here), + IT.add_ + (IT.sym_ (x_sym, BT.Integer, here), IT.sym_ (y_sym', BT.Integer, here)) + here ) + here ) + here + |> partial_eval ~mode + |> IT.subst (IT.make_subst [ (y_sym, IT.num_lit_ (Z.of_int 20) BT.Integer here) ]) + |> eval ~mode + in + let printer r = match r with Ok it -> Pp.plain (IT.pp it) | Error err -> err in + assert_equal + ~printer + ~msg:"Strict evalution failed" + (Ok (IT.num_lit_ (Z.of_int 30) BT.Integer here)) + (it Strict); + assert_equal + ~printer + ~msg:"Lazy evalution failed" + (Ok (IT.num_lit_ (Z.of_int 30) BT.Integer here)) + (it Lazy) + + +let test_unops = + QCheck_ounit.to_ounit2_test + @@ + let here = Locations.other __FUNCTION__ in + let gen_it = + let open QCheck.Gen in + oneofl [ 8; 16; 32; 64 ] + >>= fun bits -> + (fun rng -> Z.random_bits ~rng bits) + >>= fun n -> + oneofl BT.[ Signed; Unsigned ] + >>= fun sgn -> + let bt = BT.Bits (sgn, bits) in + let n = BT.normalise_to_range_bt bt n in + oneofl + (let ops = + IT.[ BW_CLZ_NoSMT; BW_CTZ_NoSMT; BW_FFS_NoSMT; BW_FLS_NoSMT; BW_Compl ] + in + if BT.equal_sign sgn Signed then IT.Negate :: ops else ops) + >>= fun unop -> return (IT.arith_unop unop (IT.num_lit_ n bt here) here) + in + let print (it : IT.t) : string = + let open Pp in + plain + (IT.pp it + ^^ space + ^^ equals + ^^ space + ^^ + match eval it with + | Ok it -> precede (string "Ok") (parens (IT.pp it)) + | Error msg -> precede (string "Error") (parens (string msg))) + in + let shrink (it : IT.t) : IT.t QCheck.Iter.t = + match it with + | IT (Unop (op, it'), Bits (sgn, sz), loc) -> + let n = Option.get (IT.get_num_z it') in + let open QCheck.Iter in + if Z.equal n Z.zero then + empty + else ( + let to_64, of_64 = + match sgn with + | Signed -> (Z.to_int64, Z.of_int64) + | Unsigned -> (Z.to_int64_unsigned, Z.of_int64_unsigned) + in + n + |> to_64 + |> QCheck.Shrink.int64 + >|= fun n -> + IT.arith_unop + op + (IT.num_lit_ (of_64 n) (Bits (sgn, sz)) loc) + (Locations.other __FUNCTION__)) + | _ -> failwith "unreachable" + in + let arb_it = QCheck.make ~print ~shrink gen_it in + QCheck.Test.make ~name:(TestUtils.test_name __FUNCTION__) arb_it (fun it -> + let it_result = Result.get_ok (eval it) in + let lc_equal = LC.T (IT.eq_ (it, it_result) here) in + let global = { Global.empty with datatype_order = Some [] } in + let solver = Solver.make global in + match + Solver.provable + ~loc:here + ~solver + ~global + ~assumptions:Context.LCSet.empty + ~simp_ctxt:(Simplify.default global) + lc_equal + with + | `True -> true + | `False -> false) + + +let test_partial_eval_arith = + TestUtils.test_name __FUNCTION__ + >:: fun _ -> + let here = Locations.other __FUNCTION__ in + let num_lit n = IT.num_lit_ n BT.Integer here in + let x = Z.random_bits 1000 in + let y = Z.random_bits 1000 in + let z = Z.random_bits 1000 in + let w = Z.random_bits 1000 in + let it_sym = IT.sym_ (Sym.fresh (), BT.Integer, here) in + let it_math = + let open IT in + (((num_lit x %+ num_lit y) here %- num_lit z) here %* num_lit w) here + in + let it = IT.mul_no_smt_ (it_sym, it_math) here in + assert_equal + ~cmp:IT.equal + ~printer:(fun it -> Pp.plain @@ IT.pp it) + (IT.mul_no_smt_ + ( it_sym, + num_lit + (let open Z in + (x + y - z) * w) ) + here) + (partial_eval it) + + +let tests = + TestUtils.test_suite_name __FILE__ + >::: [ test_tuple; + test_struct; + test_record; + test_constructor; + test_apply_rename; + test_partial_eval_arith; + test_unops + ] diff --git a/backend/cn/tests/main.ml b/backend/cn/tests/main.ml new file mode 100644 index 000000000..97de1febe --- /dev/null +++ b/backend/cn/tests/main.ml @@ -0,0 +1,3 @@ +open OUnit2 + +let () = run_test_tt_main ("CN" >::: [ Eval.tests ]) diff --git a/backend/cn/tests/testUtils.ml b/backend/cn/tests/testUtils.ml new file mode 100644 index 000000000..cc3c6c559 --- /dev/null +++ b/backend/cn/tests/testUtils.ml @@ -0,0 +1,6 @@ +let test_name fun_name = + fun_name |> String.split_on_char '.' |> Cn.List.last |> Option.get + + +let test_suite_name filename = + filename |> Filename.basename |> Filename.chop_extension |> String.capitalize_ascii diff --git a/cn.opam b/cn.opam index b5b38d126..70b458837 100644 --- a/cn.opam +++ b/cn.opam @@ -10,6 +10,9 @@ depends: [ "z3" {>= "4.8.14"} "cmdliner" "ocamlgraph" + "ounit2" + "qcheck" + "qcheck-ounit" ] build: [ ["dune" "subst"] {pinned}