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
+199 −3
Draft

Normalize and simplify #348

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
25 changes: 9 additions & 16 deletions src/smtml/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down