Simplify subtractions with ptr

formalsec · Aug 27, 2024 · 3b3371f · 3b3371f
1 parent a210546
commit 3b3371f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/expr.ml b/src/expr.ml
@@ -288,6 +288,8 @@ let rec binop ty (op : binop) (hte1 : t) (hte2 : t) : t =
     binop ty Rem addr hte2
   | Add, _, Ptr { base; offset } ->
     ptr base (binop (Ty_bitv 32) Add offset hte1)
+  | Sub, _, Ptr { base; offset } ->
+    binop ty Sub hte1 (binop (Ty_bitv 32) Add (value (Num (I32 base))) offset)
   | (Add | Or), Val (Num (I32 0l)), _ -> hte2
   | (And | Div | DivU | Mul | Rem | RemU), Val (Num (I32 0l)), _ -> hte1
   | (Add | Or), _, Val (Num (I32 0l)) -> hte1