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 1 commit
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
12 changes: 9 additions & 3 deletions src/smtml/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
22 changes: 22 additions & 0 deletions test/unit/test_expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down