fix: smt encoding for evm semantics of {div,sdiv,mod,smod}-by-zero

a16z · Apr 9, 2024 · fd27d64 · fd27d64
1 parent f868681
commit fd27d64
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 14 deletions.
diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
@@ -1091,16 +1091,13 @@ def is_unknown(result: CheckSatResult, model: Model) -> bool:
 
 
 def refine(query: str) -> str:
-    # replace uninterpreted abstraction with actual symbols for assertion solving
-    # TODO: replace `(evm_bvudiv x y)` with `(ite (= y (_ bv0 256)) (_ bv0 256) (bvudiv x y))`
-    #       as bvudiv is undefined when y = 0; also similarly for evm_bvurem
-    query = re.sub(r"(\(\s*)evm_(bv[a-z]+)(_[0-9]+)?\b", r"\1\2", query)
-    # remove the uninterpreted function symbols
-    # TODO: this will be no longer needed once is_model_valid is properly implemented
+    # replace `(evm_bvudiv x y)` with `(ite (= y (_ bv0 256)) (_ bv0 256) (bvudiv x y))`
+    # similarly for bvurem, bvsdiv, and bvsrem
+    # NOTE: (bvudiv x (_ bv0 N)) is *defined* to (bvneg (_ bv1 N)); while (div x 0) is undefined
     return re.sub(
-        r"\(\s*declare-fun\s+evm_(bv[a-z]+)(_[0-9]+)?\b",
-        r"(declare-fun dummy_\1\2",
-        query,
+        r"\(declare-fun evm_(bv[a-z]+)_([0-9]+) \(\(_ BitVec \2\) \(_ BitVec \2\)\) \(_ BitVec \2\)\)",
+        r"(define-fun evm_\1_\2 ((x (_ BitVec \2)) (y (_ BitVec \2))) (_ BitVec \2) (ite (= y (_ bv0 \2)) (_ bv0 \2) (\1 x y)))",
+        query
     )
 
 

diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -60,15 +60,16 @@
 f_origin = Function("origin", BitVecSort160)
 
 # uninterpreted arithmetic
-f_div = Function("evm_bvudiv", BitVecSort256, BitVecSort256, BitVecSort256)
+# NOTE: do not introduce new symbols starting `evm_bv`; see __main__.refine()
+f_div = Function("evm_bvudiv_256", BitVecSort256, BitVecSort256, BitVecSort256)
 f_mod = {
-    256: Function("evm_bvurem", BitVecSort256, BitVecSort256, BitVecSort256),
+    256: Function("evm_bvurem_256", BitVecSort256, BitVecSort256, BitVecSort256),
     264: Function("evm_bvurem_264", BitVecSort264, BitVecSort264, BitVecSort264),
     512: Function("evm_bvurem_512", BitVecSort512, BitVecSort512, BitVecSort512),
 }
-f_sdiv = Function("evm_bvsdiv", BitVecSort256, BitVecSort256, BitVecSort256)
-f_smod = Function("evm_bvsrem", BitVecSort256, BitVecSort256, BitVecSort256)
-f_exp = Function("evm_exp", BitVecSort256, BitVecSort256, BitVecSort256)
+f_sdiv = Function("evm_bvsdiv_256", BitVecSort256, BitVecSort256, BitVecSort256)
+f_smod = Function("evm_bvsrem_256", BitVecSort256, BitVecSort256, BitVecSort256)
+f_exp = Function("evm_exp_256", BitVecSort256, BitVecSort256, BitVecSort256)
 
 magic_address: int = 0xAAAA0000