Normalize and simplify

src/smtml/expr.ml

@@ -361,6 +361,11 @@ let raw_binop ty op hte1 hte2 = make (Binop (ty, op, hte1, hte2)) [@@inline]
 let rec binop ty op hte1 hte2 =
   match (op, view hte1, view hte2) with
   | Ty.Binop.(String_in_re | Regexp_range), _, _ -> raw_binop ty op hte1 hte2
+  | ( ( Ty.Binop.String_contains | Ty.Binop.String_prefix
+      | Ty.Binop.String_suffix )
+    , _
+    , Val (Str "") ) ->
+    make (Val True)
   | op, Val v1, Val v2 -> value (Eval.binop ty op v1 v2)
   | Sub, Ptr { base = b1; offset = os1 }, Ptr { base = b2; offset = os2 } ->
     if Int32.equal b1 b2 then binop ty Sub os1 os2
@@ -383,10 +388,24 @@ let rec binop ty op hte1 hte2 =
     when Bitvector.eqz bv ->
     hte1
   | (Add | Or), _, Val (Bitv bv) when Bitvector.eqz bv -> hte1
+  | Add, _, Val (Real -0.) -> hte1
+  | Add, Val (Real -0.), _ -> hte2
+  | Add, _, Val (Num (F32 -0l)) -> hte1
+  | Add, Val (Num (F32 -0l)), _ -> hte2
   | (And | Mul), _, Val (Bitv bv) when Bitvector.eqz bv -> hte2
+  | And, Val True, _ -> hte2
+  | And, _, Val True -> hte1
+  | And, Val False, _ -> hte1
+  | And, _, Val False -> hte2
+  | Or, Val True, _ | Or, _, Val True -> make (Val True)
+  | Or, Val False, _ -> hte2
+  | Or, _, Val False -> hte1
   | Add, Binop (ty, Add, x, { node = Val v1; _ }), Val v2 ->
     let v = value (Eval.binop ty Add v1 v2) in
     raw_binop ty Add x v
+  | And, Binop (ty, And, x, { node = Val v1; _ }), Val v2 ->
+    let v = value (Eval.binop ty And v1 v2) in
+    raw_binop ty And x v
   | Sub, Binop (ty, Sub, x, { node = Val v1; _ }), Val v2 ->
     let v = value (Eval.binop ty Add v1 v2) in
     raw_binop ty Sub x v
@@ -420,6 +439,7 @@ let triop ty op e1 e2 e3 =
   match (op, view e1, view e2, view e3) with
   | Ty.Triop.Ite, Val True, _, _ -> e2
   | Ite, Val False, _, _ -> e3
+  | Ite, _, _, _ when equal e2 e3 -> e2
   | op, Val v1, Val v2, Val v3 -> value (Eval.triop ty op v1 v2 v3)
   | Ite, _, Triop (_, Ite, c2, r1, r2), Triop (_, Ite, _, _, _) ->
     let else_ = raw_triop ty Ite e1 r2 e3 in
@@ -453,6 +473,7 @@ let rec relop ty op hte1 hte2 =
     raw_unop Ty_bool Not (raw_unop (Ty_fp prec1) Is_nan hte1)
   | Eq, Ptr { base = b1; offset = os1 }, Ptr { base = b2; offset = os2 } ->
     if Int32.equal b1 b2 then relop Ty_bool Eq os1 os2 else value False
+  (* | Eq, _, _ -> make (normalize_eq_or_ne Eq (ty,hte1,hte2)) *)
   | Ne, Ptr { base = b1; offset = os1 }, Ptr { base = b2; offset = os2 } ->
     if Int32.equal b1 b2 then relop Ty_bool Ne os1 os2 else value True
   | ( (LtU | LeU)
@@ -504,6 +525,22 @@ let cvtop ty op hte =
   | Ty.Cvtop.String_to_re, _ -> raw_cvtop ty op hte
   | _, Val v -> value (Eval.cvtop ty op v)
   | String_to_float, Cvtop (Ty_real, ToString, real) -> real
+  | Reinterpret_float, Cvtop (Ty_real, Reinterpret_int, e1) -> e1
+  | Reinterpret_float, Cvtop (Ty_fp n, Reinterpret_int, e) ->
+    assert (match ty with Ty_bitv m -> n = m | _ -> false);
+    e
+  | Reinterpret_int, Cvtop (Ty_int, Reinterpret_float, e1) -> e1
+  | Reinterpret_int, Cvtop (Ty_bitv m, Reinterpret_float, e) ->
+    assert (match ty with Ty_fp n -> n = m | _ -> false);
+    e
+  | ToString, Cvtop (_, OfString, e1) -> e1
+  | ToBool, Cvtop (_, OfBool, e1) -> e1
+  | Zero_extend 0, _ -> hte
+  | Sign_extend 0, _ -> hte
+  | String_from_code, Cvtop (_, String_to_code, e1) -> e1
+  | String_to_code, Cvtop (_, String_from_code, e1) -> e1
+  | String_to_int, Cvtop (_, String_from_int, e1) -> e1
+  | String_from_int, Cvtop (_, String_to_int, e1) -> e1
   | _ -> raw_cvtop ty op hte
 
 let raw_naryop ty op es = make (Naryop (ty, op, es)) [@@inline]

test/integration/test_solver.ml

@@ -221,9 +221,9 @@ module Make (M : Mappings_intf.S_with_fresh) = struct
       ];
     assert_sat ~f:"test_copysign64" (Solver.check solver [])
 
-  let test_to_ieee_bv solver_modulde =
+  let test_to_ieee_bv solver_module =
     let open Infix in
-    let module Solver = (val solver_modulde : Solver_intf.S) in
+    let module Solver = (val solver_module : Solver_intf.S) in
     let solver =
       Solver.create ~params:(Params.default ()) ~logic:Logic.QF_UFBV ()
     in

test/unit/test_expr.ml

@@ -629,11 +629,183 @@ let test_simplify_concat =
   ; "test_simplify_concat_i32_symbol" >:: test_simplify_concat_i32_symbol
   ]
 
+let test_simplify_reinterpret_int _ =
+  let open Infix in
+  let sym_0 = symbol "symbol_0" (Ty_fp 32) in
+  let lhs =
+    Expr.binop (Ty_fp 32) Add
+      (Expr.cvtop (Ty_fp 32) Reinterpret_int
+         (Expr.cvtop (Ty_bitv 32) Reinterpret_float sym_0) )
+      (float32 0.)
+  in
+  let sym_1 = symbol "symbol_1" (Ty_fp 32) in
+  let rhs =
+    Expr.cvtop (Ty_fp 32) Reinterpret_int
+      (Expr.cvtop (Ty_bitv 32) Reinterpret_float sym_1)
+  in
+  let result = Expr.binop (Ty_fp 32) Add lhs rhs in
+  let expected = Expr.binop (Ty_fp 32) Add sym_0 sym_1 in
+  check result expected
+
+let test_relop_eq_normalize_bitv _ =
+  let open Infix in
+  let x = symbol "x" (Ty_bitv 32) in
+  let y = symbol "y" (Ty_bitv 32) in
+  let expected =
+    Expr.relop (Ty_bitv 32) Ne
+      (Expr.binop (Ty_bitv 32) Sub x y)
+      (Expr.value (Bitv (Bitvector.make Z.zero 32)))
+  in
+  let result = Expr.unop (Ty_bitv 32) Not (Expr.relop (Ty_bitv 32) Eq x y) in
+  check result expected
+
+let test_relop_eq_normalize_int _ =
+  let open Infix in
+  let x = symbol "x" Ty_int in
+  let y = symbol "y" Ty_int in
+  let expected =
+    Expr.relop Ty_int Ne (Expr.binop Ty_int Sub x y) (Expr.value (Int 0))
+  in
+  let result = Expr.unop Ty_int Not (Expr.relop Ty_int Eq x y) in
+  check result expected
+
+let test_relop_eq_normalize_real _ =
+  let open Infix in
+  let x = symbol "x" Ty_real in
+  let y = symbol "y" Ty_real in
+  let expected =
+    Expr.relop Ty_real Ne (Expr.binop Ty_real Sub x y) (Expr.value (Real 0.))
+  in
+  let result = Expr.unop Ty_real Not (Expr.relop Ty_real Eq x y) in
+  check result expected
+
+let test_str_contains_empty_rhs _ =
+  let open Infix in
+  let str s = Expr.value (Str s) in
+  let s = symbol "x" Ty_str in
+  let e = Expr.binop Ty_bool String_contains s (str "") in
+  let expected = Expr.value True in
+  check e expected
+
+let test_str_prefix_empty_rhs _ =
+  let open Infix in
+  let str s = Expr.value (Str s) in
+  let s = symbol "x" Ty_str in
+  let e = Expr.binop Ty_bool String_prefix s (str "") in
+  let expected = Expr.value True in
+  check e expected
+
+let test_str_suffix_empty_rhs _ =
+  let open Infix in
+  let str s = Expr.value (Str s) in
+  let s = symbol "x" Ty_str in
+  let e = Expr.binop Ty_bool String_suffix s (str "") in
+  let expected = Expr.value True in
+  check e expected
+
+let test_and_true_rhs _ =
+  let open Infix in
+  let symbol_i name = symbol name Ty_int in
+  let s = symbol_i "x" in
+  let e = Expr.binop Ty_bool And s (Expr.value True) in
+  check e s
+
+let test_and_false_lhs _ =
+  let open Infix in
+  let symbol_i name = symbol name Ty_int in
+  let s = symbol_i "x" in
+  let e = Expr.binop Ty_bool And (Expr.value False) s in
+  check e (Expr.value False)
+
+let test_or_true_rhs _ =
+  let open Infix in
+  let symbol_i name = symbol name Ty_int in
+  let s = symbol_i "x" in
+  let e = Expr.binop Ty_bool Or s (Expr.value True) in
+  check e (Expr.value True)
+
+let test_or_false_rhs _ =
+  let open Infix in
+  let symbol_i name = symbol name Ty_int in
+  let s = symbol_i "x" in
+  let e = Expr.binop Ty_bool Or s (Expr.value False) in
+  check e s
+
+let test_and_fold_constants _ =
+  let open Infix in
+  let x = symbol "x" Ty_int in
+  let v1 = Expr.value (Int 3) in
+  let v2 = Expr.value (Int 6) in
+  let and_const = Expr.binop Ty_int And x (Expr.binop Ty_int And v1 v2) in
+  match (v1.node, v2.node) with
+  | Val v1, Val v2 ->
+    let folded = Expr.value (Eval.binop Ty_int And v1 v2) in
+    let expected = Expr.binop Ty_int And x folded in
+    check and_const expected
+  | _ -> assert false
+
+let test_ite_same_branches _ =
+  let open Infix in
+  let symbol_i name = symbol name Ty_int in
+  let c = symbol_i "cond" in
+  let x = symbol_i "x" in
+  let e = Expr.triop Ty_int Ite c x x in
+  check e x
+
+let test_to_string_of_string _ =
+  let open Infix in
+  let s = symbol "s" Ty_str in
+  let e = Expr.cvtop Ty_str ToString (Expr.cvtop Ty_str OfString s) in
+  check e s
+
+let test_zero_extend_0 _ =
+  let open Infix in
+  let x = symbol "x" (Ty_bitv 32) in
+  let e = Expr.cvtop (Ty_bitv 32) (Zero_extend 0) x in
+  check e x
+
+let test_string_to_code_from_code _ =
+  let open Infix in
+  let s = symbol "s" Ty_str in
+  let e =
+    Expr.cvtop Ty_int String_to_code (Expr.cvtop Ty_str String_from_code s)
+  in
+  check e s
+
+let test_string_to_int_from_int _ =
+  let open Infix in
+  let s = symbol "s" Ty_str in
+  let e =
+    Expr.cvtop Ty_int String_to_int (Expr.cvtop Ty_str String_from_int s)
+  in
+  check e s
+
+let test_simplify_normalize =
+  [ "test_simplify_reinterpret_int" >:: test_simplify_reinterpret_int
+  ; "test_relop_eq_normalize_bitv" >:: test_relop_eq_normalize_bitv
+  ; "test_relop_eq_normalize_int" >:: test_relop_eq_normalize_int
+  ; "test_relop_eq_normalize_real" >:: test_relop_eq_normalize_real
+  ; "test_str_contains_empty_rhs" >:: test_str_contains_empty_rhs
+  ; "test_str_prefix_empty_rhs" >:: test_str_prefix_empty_rhs
+  ; "test_str_suffix_empty_rhs" >:: test_str_suffix_empty_rhs
+  ; "test_and_true_rhs" >:: test_and_true_rhs
+  ; "test_and_false_lhs" >:: test_and_false_lhs
+  ; "test_or_true_rhs" >:: test_or_true_rhs
+  ; "test_or_false_rhs" >:: test_or_false_rhs
+  ; "test_and_fold_constants" >:: test_and_fold_constants
+  ; "test_ite_same_branches" >:: test_ite_same_branches
+  ; "test_to_string_of_string" >:: test_to_string_of_string
+  ; "test_zero_extend_0" >:: test_zero_extend_0
+  ; "test_string_to_code_from_code" >:: test_string_to_code_from_code
+  ; "test_string_to_int_from_int" >:: test_string_to_int_from_int
+  ]
+
 let test_simplify =
   [ "test_simplify_assoc" >:: test_simplify_assoc
   ; "test_fp_nan_not_geffects" >:: test_fp_nan_not_geffects
   ; "test_simplify_extract" >::: test_simplify_extract
   ; "test_simplify_concat" >::: test_simplify_concat
+  ; "test_simplify_normalize" >::: test_simplify_normalize
   ]
 
 let test_suite =