From c39e7243facb967c4df5060c9b34cc18f43fb3f4 Mon Sep 17 00:00:00 2001 From: felixL-K Date: Wed, 14 May 2025 17:52:58 +0200 Subject: [PATCH 01/10] adding atomic simplifications --- src/smtml/expr.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 46828482..8d3fbae6 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -358,6 +358,12 @@ 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, _, _ when equal hte2 (make (Val (Str ""))) -> + make (Val True) + | Ty.Binop.String_prefix, _, _ when equal hte2 (make (Val (Str ""))) -> + make (Val True) + | Ty.Binop.String_suffix, _, _ when equal hte2 (make (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 @@ -381,9 +387,18 @@ let rec binop ty op hte1 hte2 = hte1 | (Add | Or), _, Val (Bitv bv) when Bitvector.eqz bv -> hte1 | (And | Mul), _, Val (Bitv bv) when Bitvector.eqz bv -> hte2 + | And, Val True, _ -> hte2 + | And, _, Val True -> hte1 + | And, Val False, _ | And, _, Val False -> make (Val False) + | 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 @@ -417,6 +432,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 From a2379837afbd50ee5d2f68928306f3adf9d92f7c Mon Sep 17 00:00:00 2001 From: felixL-K Date: Fri, 16 May 2025 14:22:58 +0200 Subject: [PATCH 02/10] adding convertion simplifications --- src/smtml/expr.ml | 9 +++++++-- test/integration/test_solver.ml | 4 ++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 8d3fbae6..2f92b0f2 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -325,8 +325,7 @@ let normalize_eq_or_ne op (ty', e1, e2) = let negate_relop (hte : t) : t = let e = match view hte with - | Relop (ty, Eq, e1, e2) -> normalize_eq_or_ne Ne (ty, e1, e2) - | Relop (ty, Ne, e1, e2) -> normalize_eq_or_ne Eq (ty, e1, e2) + | Relop (ty, ((Eq | Ne) as op), e1, e2) -> normalize_eq_or_ne op (ty, e1, e2) | Relop (ty, Lt, e1, e2) -> Relop (ty, Le, e2, e1) | Relop (ty, LtU, e1, e2) -> Relop (ty, LeU, e2, e1) | Relop (ty, Le, e1, e2) -> Relop (ty, Lt, e2, e1) @@ -517,6 +516,12 @@ 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 32, Reinterpret_int, e1) -> e1 + | Reinterpret_float, Cvtop (Ty_fp 64, Reinterpret_int, e1) -> e1 + | Reinterpret_int, Cvtop (Ty_int, Reinterpret_float, e1) -> e1 + | Reinterpret_int, Cvtop (Ty_bitv 32, Reinterpret_float, e1) -> e1 + | Reinterpret_int, Cvtop (Ty_bitv 64, Reinterpret_float, e1) -> e1 | _ -> raw_cvtop ty op hte let raw_naryop ty op es = make (Naryop (ty, op, es)) [@@inline] diff --git a/test/integration/test_solver.ml b/test/integration/test_solver.ml index 48aa1915..1028ae19 100644 --- a/test/integration/test_solver.ml +++ b/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 From 39dc3b45cbb7f11668c755af6968cf932c7e0770 Mon Sep 17 00:00:00 2001 From: felixL-K Date: Fri, 16 May 2025 17:08:36 +0200 Subject: [PATCH 03/10] simplification of conversions --- src/smtml/expr.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 2f92b0f2..98911335 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -522,6 +522,20 @@ let cvtop ty op hte = | Reinterpret_int, Cvtop (Ty_int, Reinterpret_float, e1) -> e1 | Reinterpret_int, Cvtop (Ty_bitv 32, Reinterpret_float, e1) -> e1 | Reinterpret_int, Cvtop (Ty_bitv 64, Reinterpret_float, e1) -> e1 + | ToString, Cvtop (_, OfString, e1) -> e1 + | OfString, Cvtop (_, ToString, e1) -> e1 + | ToBool, Cvtop (_, OfBool, e1) -> e1 + | OfBool, Cvtop (_, ToBool, e1) -> e1 + | PromoteF32, Cvtop (_, DemoteF64, e1) -> e1 + | DemoteF64, Cvtop (_, PromoteF32, e1) -> e1 + | Reinterpret_int, Cvtop (_, Reinterpret_float, e1) -> e1 + | Reinterpret_float, Cvtop (_, Reinterpret_int, 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] From 744721f401dda89294a187f2f0aa77129a9329c4 Mon Sep 17 00:00:00 2001 From: felixL-K Date: Thu, 22 May 2025 15:10:29 +0200 Subject: [PATCH 04/10] adding reviews changes --- src/smtml/expr.ml | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 98911335..ad5477d1 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -357,12 +357,9 @@ 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, _, _ when equal hte2 (make (Val (Str ""))) -> - make (Val True) - | Ty.Binop.String_prefix, _, _ when equal hte2 (make (Val (Str ""))) -> - make (Val True) - | Ty.Binop.String_suffix, _, _ when equal hte2 (make (Val (Str ""))) -> - make (Val True) + | Ty.Binop.String_contains, _, Val (Str "") -> make (Val True) + | Ty.Binop.String_prefix, _, Val (Str "") -> make (Val True) + | 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 @@ -517,19 +514,15 @@ let 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 32, Reinterpret_int, e1) -> e1 - | Reinterpret_float, Cvtop (Ty_fp 64, 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 32, Reinterpret_float, e1) -> e1 - | Reinterpret_int, Cvtop (Ty_bitv 64, 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 - | OfString, Cvtop (_, ToString, e1) -> e1 | ToBool, Cvtop (_, OfBool, e1) -> e1 - | OfBool, Cvtop (_, ToBool, e1) -> e1 - | PromoteF32, Cvtop (_, DemoteF64, e1) -> e1 - | DemoteF64, Cvtop (_, PromoteF32, e1) -> e1 - | Reinterpret_int, Cvtop (_, Reinterpret_float, e1) -> e1 - | Reinterpret_float, Cvtop (_, Reinterpret_int, e1) -> e1 | Zero_extend 0, _ -> hte | Sign_extend 0, _ -> hte | String_from_code, Cvtop (_, String_to_code, e1) -> e1 From 91d5160acd9cc3078c10a233026f82fb1485a435 Mon Sep 17 00:00:00 2001 From: felixL-K Date: Fri, 23 May 2025 11:38:12 +0200 Subject: [PATCH 05/10] adding unit test for simplification --- src/smtml/expr.ml | 12 +++++++++--- test/unit/test_expr.ml | 22 ++++++++++++++++++++++ 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index ad5477d1..b9002972 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -357,9 +357,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, _, Val (Str "") -> make (Val True) - | Ty.Binop.String_prefix, _, Val (Str "") -> make (Val True) - | Ty.Binop.String_suffix, _, Val (Str "") -> make (Val True) + | ( ( 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 @@ -382,6 +384,10 @@ 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 diff --git a/test/unit/test_expr.ml b/test/unit/test_expr.ml index 74478bb7..6e987ffa 100644 --- a/test/unit/test_expr.ml +++ b/test/unit/test_expr.ml @@ -619,10 +619,32 @@ 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_simplify_normalize = + [ "test_simplify_reinterpret_int" >:: test_simplify_reinterpret_int ] + let test_simplify = [ "test_simplify_assoc" >:: test_simplify_assoc ; "test_simplify_extract" >::: test_simplify_extract ; "test_simplify_concat" >::: test_simplify_concat + ; "test_simplify_normalize" >::: test_simplify_normalize ] let test_suite = From 9a1197fe982d59afc0757407c174bcc484fe7a3f Mon Sep 17 00:00:00 2001 From: felixL-K Date: Mon, 26 May 2025 13:59:36 +0200 Subject: [PATCH 06/10] adding unit tests for normalization --- src/smtml/expr.ml | 4 +- test/unit/test_expr.ml | 152 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 154 insertions(+), 2 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index b9002972..3e45c021 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -325,7 +325,8 @@ let normalize_eq_or_ne op (ty', e1, e2) = let negate_relop (hte : t) : t = let e = match view hte with - | Relop (ty, ((Eq | Ne) as op), e1, e2) -> normalize_eq_or_ne op (ty, e1, e2) + | Relop (ty, Eq, e1, e2) -> normalize_eq_or_ne Ne (ty, e1, e2) + | Relop (ty, Ne, e1, e2) -> normalize_eq_or_ne Eq (ty, e1, e2) | Relop (ty, Lt, e1, e2) -> Relop (ty, Le, e2, e1) | Relop (ty, LtU, e1, e2) -> Relop (ty, LeU, e2, e1) | Relop (ty, Le, e1, e2) -> Relop (ty, Lt, e2, e1) @@ -468,6 +469,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) diff --git a/test/unit/test_expr.ml b/test/unit/test_expr.ml index 6e987ffa..e40df53d 100644 --- a/test/unit/test_expr.ml +++ b/test/unit/test_expr.ml @@ -637,8 +637,158 @@ let test_simplify_reinterpret_int _ = 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_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 From f2f40929fd648e9b6b9820d40602a1aa2211241b Mon Sep 17 00:00:00 2001 From: felixL-K Date: Tue, 27 May 2025 09:58:41 +0200 Subject: [PATCH 07/10] adding reviews of zapashcanon and filipe --- src/smtml/expr.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 3e45c021..293efefa 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -385,14 +385,15 @@ 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 + | 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, _ | And, _, Val False -> make (Val False) + | 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 From 1e41a765e6d1211d1cbf9e77d884024d570a2a00 Mon Sep 17 00:00:00 2001 From: felixL-K Date: Tue, 15 Jul 2025 14:55:20 +0200 Subject: [PATCH 08/10] resolving conversations --- src/smtml/expr.ml | 4 ++-- test/unit/test_expr.ml | 9 --------- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index ce303560..034f016a 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -392,6 +392,8 @@ let rec binop ty op hte1 hte2 = | Add, Val (Real -0.), _ -> hte2 | Add, _, Val (Num (F32 -0l)) -> hte1 | Add, Val (Num (F32 -0l)), _ -> hte2 + | Add, _, Val (Num (F64 -0L)) -> hte1 + | Add, Val (Num (F64 -0L)), _ -> hte2 | (And | Mul), _, Val (Bitv bv) when Bitvector.eqz bv -> hte2 | And, Val True, _ -> hte2 | And, _, Val True -> hte1 @@ -539,8 +541,6 @@ let cvtop ty op 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] diff --git a/test/unit/test_expr.ml b/test/unit/test_expr.ml index 3a5d79b1..cf812690 100644 --- a/test/unit/test_expr.ml +++ b/test/unit/test_expr.ml @@ -772,14 +772,6 @@ let test_string_to_code_from_code _ = 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 @@ -797,7 +789,6 @@ let test_simplify_normalize = ; "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 = From 113690478171c2b77c8537aad1bc17e6c7b1eae6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?F=C3=A9lix=20LOYAU-KAHN?= Date: Tue, 15 Jul 2025 15:02:30 +0200 Subject: [PATCH 09/10] Update src/smtml/expr.ml Co-authored-by: Hichem R. A. --- src/smtml/expr.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 034f016a..62c65d9e 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -399,7 +399,8 @@ let rec binop ty op hte1 hte2 = | And, _, Val True -> hte1 | And, Val False, _ -> hte1 | And, _, Val False -> hte2 - | Or, Val True, _ | Or, _, Val True -> make (Val True) + | Or, Val True, _ -> hte1 + | Or, _, Val True -> hte2 | Or, Val False, _ -> hte2 | Or, _, Val False -> hte1 | Add, Binop (ty, Add, x, { node = Val v1; _ }), Val v2 -> From bda797887da261a77623a4b87fc18174ae7583dd Mon Sep 17 00:00:00 2001 From: felixL-K Date: Tue, 15 Jul 2025 15:38:07 +0200 Subject: [PATCH 10/10] removed duplicates, And with cst --- src/smtml/expr.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml index 62c65d9e..d99234f8 100644 --- a/src/smtml/expr.ml +++ b/src/smtml/expr.ml @@ -406,9 +406,6 @@ let rec binop ty op hte1 hte2 = | 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