Improve nonlinear reasoning (#14)

a16z · Feb 1, 2023 · 05a2b44 · 05a2b44
1 parent 0c7f39e
commit 05a2b44
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 2 deletions.
diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
@@ -224,7 +224,10 @@ def run(
     # print result
     print(f"{passfail} {funsig} (paths: {normal}/{len(exs)}, time: {end - start:0.2f}s, bounds: [{', '.join(dyn_param_size)}])")
     for model, idx, ex in models:
-        print(color_warn('Counterexample: ' + str(model)))
+        if model:
+            print(color_warn('Counterexample: ' + str(model)))
+        else:
+            print(color_warn('Counterexample: unknown'))
         if args.verbose >= 1:
             print(f'# {idx+1} / {len(exs)}')
             print(ex)
@@ -261,6 +264,15 @@ def gen_model(args: argparse.Namespace, models: List, idx: int, ex: Exec):
         sol2.from_string(ex.solver.sexpr())
         res = sol2.check()
         if res == sat: model = sol2.model()
+    if res == sat and not is_valid_model(model):
+        query = ex.solver.sexpr()
+        query += '(assert (forall ((x (_ BitVec 256)) (y (_ BitVec 256))) (bvule (evm_div x y) x)))'
+    #   query += '(assert (forall ((x (_ BitVec 256)) (y (_ BitVec 256))) (implies (and (not (= x (_ bv0 256))) (not (= y (_ bv0 256))) (= (evm_div (bvmul x y) x) y)) (= (evm_div (bvmul x y) y) x))))'
+        sol3 = Solver(ctx=Context())
+        sol3.set(timeout=args.solver_timeout_assertion)
+        sol3.from_string(query)
+        res = sol3.check()
+        if res == sat: model = sol3.model()
     if res == unknown and args.solver_subprocess:
         fname = f'/tmp/{uuid.uuid4().hex}.smt2'
         if args.verbose >= 4: print(f'z3 -smt2 {fname}')
@@ -274,10 +286,20 @@ def gen_model(args: argparse.Namespace, models: List, idx: int, ex: Exec):
     if res == unsat:
         return
     if res == sat:
-        models.append((model, idx, ex))
+        if is_valid_model(model):
+            models.append((model, idx, ex))
+        else:
+            models.append((None, idx, ex))
     else:
         models.append((None, idx, ex))
 
+def is_valid_model(model) -> bool:
+    for decl in model:
+        inter = model[decl]
+        if str(decl).startswith('evm_'):
+            return False
+    return True
+
 def main() -> int:
     #
     # z3 global options

diff --git a/tests/test/Counter.t.sol b/tests/test/Counter.t.sol
@@ -90,6 +90,30 @@ contract CounterTest is Counter {
         assert(cnt == oldCnt + bytes(s).length + bytes(r).length);
     }
 
+    function testDiv1(uint x, uint y) public pure {
+        if (y > 0) {
+            assert(x / y <= x);
+        }
+    }
+
+    function testDiv2(uint x, uint y) public pure {
+        if (y > 0) {
+            assert(x / y == x / y);
+        }
+    }
+
+    function testMulDiv(uint x, uint y) public pure {
+        unchecked {
+            if (x > 0 && y > 0) {
+                uint z = x * y;
+                if (z / x == y) {
+                    assert(z / x == y);
+                  //assert(z / y == x); // smt failed to solve
+                }
+            }
+        }
+    }
+
     function testFail() public pure {
         require(false);
         // deadcode