In order to combine PRECONDS + Expr we need to use the SMT solver

[msooseth]

This is potential future work.

It turns out we could do better in determining branching statically. Currently, in SymExec.hs we have:

          PleaseAskSMT cond _ continue -> do
            case cond of
              -- is the condition concrete?
              Lit c ->

Where _ is the set of path conditions, and cond has been simplified (after https://github.com/ethereum/hevm/pull/329 is merged). However, if e.g. the preconditions say a=b and the cond is a==b then of course we should have this evaluate to TRUE. Unfortunately, we don't do that, mostly because our simplifier is not capable of catching some things. For example,

ghci> Expr.simplify (Expr.and (Expr.eq (Var "a") (Lit 1)) (Expr.eq (Var "a") (Lit 0)))
And (Eq (Lit 0x1) (Var "a")) (Eq (Lit 0x0) (Var "a"))

which is clearly FALSE, since a is both 0 and 1. So, we can't just do e.g. a fold' (Expr.and) (Lit 1) (cond:pathConds).

In other words, we need a more sophisticated constant folding system and then we can do better static path condition checking.

[msooseth]

As discussed, while #358 does folding of the preconditions, it will NOT do the heavy-lifting of figuring out whether the path conditions contradict the Expr. For that, we'd need a SMT call.

[msooseth]

This just came up a little bit. This test:

+     , test "mulmod-speed" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function proveFun(uint8 a, uint8 b, uint8 c) external pure {
+                require(a < 4);
+                require(b < 4);
+                require(c < 4);
+                uint16 r1;
+                uint16 r2;
+                uint16 g2;
+                assembly {
+                  r1 := mul(a,b)
+                  r2 := mod(r1, c)
+                  g2 := mulmod (a, b, c)
+                }
+                assert (r2 == g2);
+              }
+             }
+            |]
+        let sig = Sig "proveFun(uint8,uint8,uint8)" [AbiIntType 8, AbiUIntType 8, AbiUIntType 8]
+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+        putStrLnM "Mulmod is fast"

Is very slow, 25s, to run. When one looks at the Props:

;(PLEq
;  (Var "arg3")
;  255
;)
;(PLEq
;  (Var "arg2")
;  255
;)
;(PLEq
;  (Var "arg1")
;  255
;)
;(PNeg
;  (PEq
;    (And
;      65535
;      (Mod
;        (Mul
;          (Var "arg1")
;          (Var "arg2")
;        )
;        (Var "arg3")
;      )
;    )
;    (And
;      65535
;      (MulMod
;        (Var "arg1")
;        (Var "arg2")
;        (Var "arg3")
;      )
;    )
;  )
;)

It looks okay. However, MulMod is accounts for things going over 256b, and so the SMT looks like this:

(assert (bvule arg3 (_ bv255 256)))
(assert (bvule arg2 (_ bv255 256)))
(assert (bvule arg1 (_ bv255 256)))
; (assert (not (= (bvand (_ bv65535 256) (ite (= arg3 (_ bv0 256)) (_ bv0 256) (bvurem (bvmul arg1 arg2) arg3))) (bvand (_ bv65535 256) ((_ extract 255 0) (ite (= arg3 (_ bv0 256)) (_ bv0 512) (bvurem (bvmul (concat (_ bv0 256) arg1) (concat (_ bv0 256) arg2))(concat (_ bv0 256) arg3))))))))

Notice the extension to 512b to make sure things stay within bounds. This is the proper way to encode MulMod in case its arguments could be large. However, that's unnecessary here, since arg1..3 are all <255, so the extension to 512b is useless. However, it makes things a LOT slower. Without the extension:

(assert (not (= (bvand (_ bv65535 256) (ite (= arg3 (_ bv0 256)) (_ bv0 256) (bvurem (bvmul arg1 arg2) arg3))) (bvand (_ bv65535 256) ((_ extract 255 0) (ite (= arg3 (_ bv0 256)) (_ bv0 512) (bvurem (bvmul (concat (_ bv0 256) arg1) (concat (_ bv0 256) arg2))(concat (_ bv0 256) arg3))))))))

The generated SMT query runs in <1s.

We could either query the solver to make sure we don't need to extend to 512b, or we can add type annotations to variables, and generate simpler SMT queries. The type annotation can be constructed & destructed as part of generating the SMT query, i.e. it could be ephemeral and may not need to be saved to Expr.