Skip to content

Normalize and simplify #348

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 14 commits into
base: main
Choose a base branch
from
Draft

Normalize and simplify #348

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
c39e724
adding atomic simplifications
felixL-K May 14, 2025
a237983
adding convertion simplifications
felixL-K May 16, 2025
39dc3b4
simplification of conversions
felixL-K May 16, 2025
557a54d
Merge branch 'formalsec:main' into normalize
felixL-K May 19, 2025
598d4ca
Merge branch 'formalsec:main' into normalize
felixL-K May 22, 2025
744721f
adding reviews changes
felixL-K May 22, 2025
91d5160
adding unit test for simplification
felixL-K May 23, 2025
9a1197f
adding unit tests for normalization
felixL-K May 26, 2025
f2f4092
adding reviews of zapashcanon and filipe
felixL-K May 27, 2025
8bee159
Merge branch 'formalsec:main' into normalize
felixL-K Jun 18, 2025
1e41a76
resolving conversations
felixL-K Jul 15, 2025
1136904
Update src/smtml/expr.ml
felixL-K Jul 15, 2025
bda7978
removed duplicates, And with cst
felixL-K Jul 15, 2025
13e8356
resolved synk conflicts
felixL-K Jul 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 37 additions & 2 deletions src/smtml/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -358,6 +357,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
Expand All @@ -381,9 +386,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
Expand Down Expand Up @@ -417,6 +431,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
Expand Down Expand Up @@ -501,6 +516,26 @@ 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
| 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]
Expand Down
4 changes: 2 additions & 2 deletions test/integration/test_solver.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading