Add ptr mod val to binop

formalsec · Jan 25, 2024 · 39a387e · 39a387e
1 parent b03bf56
commit 39a387e
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/lib/expr.ml b/lib/expr.ml
@@ -159,6 +159,10 @@ let rec simplify_binop ty (op : binop) e1 e2 =
     | Sub ->
       let new_offset = simplify_binop offset.ty Sub offset e2 in
       Ptr (base, new_offset @: offset.ty)
+    | Rem ->
+      let rhs = Val (Value.Num (Num.I32 base)) @: ty in
+      let addr = (simplify_binop ty Add rhs offset) @: ty in
+      simplify_binop ty Rem addr e2
     | _ -> Binop (op, e1, e2) )
   | _, Ptr (base, offset) -> (
     match op with

diff --git a/test/regression/test_cvtop.ml b/test/regression/test_cvtop.ml
@@ -1,9 +1,16 @@
 open Encoding
 open Ty
+open Encoding.Expr
 
 let f32 f = Num.F32 (Int32.bits_of_float f)
 let f64 f = Num.F64 (Int64.bits_of_float f)
 
+let () =
+  let ptr = Ptr (8390670l, Expr.Bitv.I32.v 2l) @: Ty_bitv S32 in
+  let rem = Binop (Rem, ptr, Expr.Bitv.I32.v 1l) @: Ty_bitv S32 in
+  let result = Expr.simplify rem in
+  assert(result.e = Val (Num (I32 0l)))
+
 let () =
   let cvtop = Eval_numeric.eval_cvtop in
   assert (cvtop (Ty_bitv S32) TruncSF32 (f32 8.5) = I32 8l);