[CN] Make eval more accurate to solver

backend/cn/lib/eval.ml

@@ -2,7 +2,7 @@ module BT = BaseTypes
 module IT = IndexTerms
 
 let check_bits_bt (sgn1, sz1) (sgn2, sz2) here : (unit, string) result =
-  if Stdlib.( = ) sgn1 sgn2 then
+  if not @@ BT.equal_sign sgn1 sgn2 then
     Result.error ("Mismatched signs at " ^ Locations.simple_location here)
   else if sz1 <> sz2 then
     Result.error ("Mismatched sizes at " ^ Locations.simple_location here)
@@ -13,14 +13,7 @@ let check_bits_bt (sgn1, sz1) (sgn2, sz2) here : (unit, string) result =
 let handle_bounds (sgn, sz) (n : Z.t) : (Z.t, string) result =
   let min, max = BT.bits_range (sgn, sz) in
   match sgn with
-  | Unsigned ->
-    Ok
-      (if Z.gt n max then
-         Z.rem n (Z.add max Z.one)
-       else if Z.lt n Z.zero then
-         Z.add n max
-       else
-         n)
+  | Unsigned -> Ok (BT.normalise_to_range (sgn, sz) n)
   | Signed ->
     if Z.lt n min then
       Error "signed underflow"
@@ -50,13 +43,7 @@ let eval_num_binop
   | IT (Const (Bits ((sgn1, sz1), n1)), _, _), IT (Const (Bits ((sgn2, sz2), n2)), _, _)
     ->
     let@ () = check_bits_bt (sgn1, sz1) (sgn2, sz2) here in
-    (match sgn1 with
-     | Unsigned ->
-       let@ res = handle_bounds (sgn1, sz1) (f n1 n2) in
-       return @@ IT.num_lit_ res bt here
-     | Signed ->
-       let@ res = handle_bounds (sgn1, sz1) (f n1 n2) in
-       return @@ IT.num_lit_ res bt here)
+    return @@ IT.num_lit_ (BT.normalise_to_range (sgn1, sz1) (f n1 n2)) bt here
   | _ -> return @@ IT.arith_binop op (it1, it2) here
 
 
@@ -90,7 +77,31 @@ let eval_term_generic
      | IT (Const (Bits ((Unsigned, _), _)), _, _) ->
        Result.error ("Can't negate unsigned integer at " ^ Locations.simple_location here)
      | _ -> return @@ negate it' here)
-  | Unop (BW_CLZ_NoSMT, _) -> failwith "todo: BW_CLZ_NoSMT"
+  | Unop (BW_CLZ_NoSMT, it') ->
+    let@ it' = eval_aux it' in
+    (match it' with
+     | IT (Const (Bits ((sgn, bits), n)), bt, _) ->
+       let open Int64 in
+       let reverse_bits (n : Z.t) : Z.t =
+         let rec aux (bits : int) (n : int64) (acc : int64) : int64 =
+           if bits = 0 then
+             acc
+           else (
+             let shift =
+               match sgn with Signed -> shift_right_logical | Unsigned -> shift_right
+             in
+             let acc = logor (shift_left acc 1) (logand n (of_int 1)) in
+             aux (bits - 1) (shift n 1) acc)
+         in
+         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
+         of_64 (aux bits (to_64 n) (of_int 0))
+       in
+       return @@ arith_unop BW_CTZ_NoSMT (num_lit_ (reverse_bits n) bt here) here
+     | _ -> return @@ arith_unop BW_CLZ_NoSMT it' here)
   | Unop (BW_CTZ_NoSMT, it') ->
     let@ it' = eval_aux it' in
     (match it' with
@@ -109,7 +120,16 @@ let eval_term_generic
          let@ it' = return @@ arith_unop BW_CTZ_NoSMT it' here in
          eval_aux (add_ (it', num_lit_ Z.one bt here) here)
      | _ -> return @@ arith_unop BW_FFS_NoSMT it' here)
-  | Unop (BW_FLS_NoSMT, _) -> failwith "todo: BW_FLS_NoSMT"
+  | Unop (BW_FLS_NoSMT, it') ->
+    let@ it' = eval_aux it' in
+    (match it' with
+     | IT (Const (Bits ((_, sz), n)), bt, _) ->
+       if Z.equal n Z.zero then
+         return @@ int_lit_ 0 bt here
+       else (
+         let it' = arith_unop BW_CLZ_NoSMT it' here in
+         eval_aux (sub_ (int_lit_ sz bt here, it') here))
+     | _ -> return @@ arith_unop BW_FLS_NoSMT it' here)
   | Unop (BW_Compl, it') ->
     let@ it' = eval_aux it' in
     (match it' with

backend/cn/tests/dune

@@ -18,6 +18,8 @@
   ocamlgraph
   ounit2
   result
+  qcheck
+  qcheck-ounit
   str
   unix
   z3))

backend/cn/tests/eval.ml

@@ -1,5 +1,6 @@
 module BT = Cn.BaseTypes
 module IT = Cn.IndexTerms
+module LC = Cn.LogicalConstraints
 open Cn
 open Eval
 open OUnit2
@@ -145,6 +146,69 @@ let test_apply_rename =
     (it Lazy)
 
 
+let test_ctz_ffs =
+  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 IT.[ BW_CLZ_NoSMT; BW_CTZ_NoSMT; BW_FFS_NoSMT; BW_FLS_NoSMT ]
+    >>= fun unop ->
+    return (IT.arith_unop unop (IT.num_lit_ n (Bits (Unsigned, bits)) 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'), bt, 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
+        n
+        |> Z.to_int64_unsigned
+        |> QCheck.Shrink.int64
+        >|= fun n ->
+        IT.arith_unop
+          op
+          (IT.num_lit_ (Z.of_int64_unsigned n) bt 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 _ ->
@@ -179,5 +243,6 @@ let tests =
          test_record;
          test_constructor;
          test_apply_rename;
-         test_partial_eval_arith
+         test_partial_eval_arith;
+         test_ctz_ffs
        ]

cn.opam

@@ -11,6 +11,8 @@ depends: [
   "cmdliner"
   "ocamlgraph"
   "ounit2"
+  "qcheck"
+  "qcheck-ounit"
 ]
 build: [
   ["dune" "subst"] {pinned}