Merge pull request #358 from ethereum/mates-simpl-pc2

Constant folding during path checking

CHANGELOG.md

@@ -49,6 +49,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Improved Prop simplification
 - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases
 - Better simplification of Eq IR elements
+- Run a toplevel constant folding reasoning system on branch conditions
 
 ## API Changes
 

src/EVM/Expr.hs

@@ -21,6 +21,7 @@ import Data.Vector.Storable.ByteString
 import Data.Word (Word8, Word32)
 import Witch (unsafeInto, into, tryFrom)
 import Data.Containers.ListUtils (nubOrd)
+import Control.Monad.State
 
 import Optics.Core
 
@@ -843,18 +844,18 @@ simplify e = if (mapExpr go e == e)
 
 
 simplifyProps :: [Prop] -> [Prop]
-simplifyProps = remRedundantProps . map evalProp . flattenProps
+simplifyProps ps = if canBeSat then simplified else [PBool False]
+  where
+    simplified = remRedundantProps . map evalProp . flattenProps $ ps
+    canBeSat = constFoldProp simplified
 
 -- | Evaluate the provided proposition down to its most concrete result
 evalProp :: Prop -> Prop
 evalProp prop =
-  let new = mapProp' go prop
+  let new = mapProp' go (simpInnerExpr prop)
   in if (new == prop) then prop else evalProp new
   where
     go :: Prop -> Prop
-    -- rewrite everything as LEq or LT
-    go (PGEq a b) = PLEq b a
-    go (PGT a b) = PLT b a
 
     -- LT/LEq comparisions
     go (PLT  (Var _) (Lit 0)) = PBool False
@@ -892,6 +893,22 @@ evalProp prop =
       | l == r = PBool True
       | otherwise = o
     go p = p
+    -- Applies `simplify` to the inner part of a Prop, e.g.
+    -- (PEq (Add (Lit 1) (Lit 2)) (Var "a")) becomes
+    -- (PEq (Lit 3) (Var "a")
+    simpInnerExpr :: Prop -> Prop
+    -- rewrite everything as LEq or LT
+    simpInnerExpr (PGEq a b) = simpInnerExpr (PLEq b a)
+    simpInnerExpr (PGT a b) = simpInnerExpr (PLT b a)
+    -- simplifies the inner expression
+    simpInnerExpr (PEq a b) = PEq (simplify a) (simplify b)
+    simpInnerExpr (PLT a b) = PLT (simplify a) (simplify b)
+    simpInnerExpr (PLEq a b) = PLEq (simplify a) (simplify b)
+    simpInnerExpr (PNeg a) = PNeg (simpInnerExpr a)
+    simpInnerExpr (PAnd a b) = PAnd (simpInnerExpr a) (simpInnerExpr b)
+    simpInnerExpr (POr a b) = POr (simpInnerExpr a) (simpInnerExpr b)
+    simpInnerExpr (PImpl a b) = PImpl (simpInnerExpr a) (simpInnerExpr b)
+    simpInnerExpr orig@(PBool _) = orig
 
 -- Makes [PAnd a b] into [a,b]
 flattenProps :: [Prop] -> [Prop]
@@ -1122,3 +1139,41 @@ containsNode p = getAny . foldExpr go (Any False)
 inRange :: Int -> Expr EWord -> Prop
 inRange sz e = PAnd (PGEq e (Lit 0)) (PLEq e (Lit $ 2 ^ sz - 1))
 
+
+data ConstState = ConstState
+  { values :: Map.Map (Expr EWord) W256
+  , canBeSat :: Bool
+  }
+  deriving (Show)
+
+-- | Folds constants
+constFoldProp :: [Prop] -> Bool
+constFoldProp ps = oneRun ps (ConstState mempty True)
+  where
+    oneRun ps2 startState = (execState (mapM (go . evalProp) ps2) startState).canBeSat
+    go :: Prop -> State ConstState ()
+    go x = case x of
+        PEq (Lit l) a -> do
+          s <- get
+          case Map.lookup a s.values of
+            Just l2 -> case l==l2 of
+                True -> pure ()
+                False -> put ConstState {canBeSat=False, values=mempty}
+            Nothing -> do
+              let vs' = Map.insert a l s.values
+              put $ s{values=vs'}
+        PEq a b@(Lit _) -> go (PEq b a)
+        PAnd a b -> do
+          go a
+          go b
+        POr a b -> do
+          s <- get
+          let
+            v1 = oneRun [a] s
+            v2 = oneRun [b] s
+          when (Prelude.not v1) $ go b
+          when (Prelude.not v2) $ go a
+          s2 <- get
+          put $ s{canBeSat=(s2.canBeSat && (v1 || v2))}
+        PBool False -> put $ ConstState {canBeSat=False, values=mempty}
+        _ -> pure ()

src/EVM/SMT.hs

@@ -155,7 +155,6 @@ declareIntermediates bufs stores =
     encodeStore n expr =
       SMT2 ["(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"] mempty mempty
 
-
 data AbstState = AbstState
   { words :: Map (Expr EWord) Int
   , count :: Int
@@ -194,7 +193,13 @@ smt2Line :: Builder -> SMT2
 smt2Line txt = SMT2 [txt] mempty mempty
 
 assertProps :: AbstRefineConfig -> [Prop] -> SMT2
-assertProps abstRefineConfig ps =
+assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps)
+
+-- Note: we need a version that does NOT call simplify or simplifyProps,
+-- because we make use of it to verify the correctness of our simplification
+-- passes through property-based testing.
+assertPropsNoSimp :: AbstRefineConfig -> [Prop] -> SMT2
+assertPropsNoSimp abstRefineConfig ps =
   let encs = map propToSMT psElimAbst
       abstSMT = map propToSMT abstProps
       intermediates = declareIntermediates bufs stores in

src/EVM/SymExec.hs

@@ -282,8 +282,11 @@ interpret fetcher maxIter askSmtIters heuristic vm =
               interpret fetcher maxIter askSmtIters heuristic vm' (k r)
 
         case q of
-          PleaseAskSMT cond _ continue -> do
-            case cond of
+          PleaseAskSMT cond preconds continue -> do
+            let
+              simpCond = Expr.simplify cond
+              simpProps = Expr.simplifyProps ((simpCond ./= Lit 0):preconds)
+            case simpCond of
               -- is the condition concrete?
               Lit c ->
                 -- have we reached max iterations, are we inside a loop?
@@ -311,11 +314,13 @@ interpret fetcher maxIter askSmtIters heuristic vm =
                   (Just True, True, _) ->
                     -- ask the smt solver about the loop condition
                     performQuery
-                  -- otherwise just try both branches and don't ask the solver
                   _ -> do
-                    (r, vm') <- stToIO $ runStateT (continue EVM.Types.Unknown) vm
+                    (r, vm') <- case simpProps of
+                      -- if we can statically determine unsatisfiability then we skip exploring the jump
+                      [PBool False] -> stToIO $ runStateT (continue (Case False)) vm
+                      -- otherwise we explore both branches
+                      _ -> stToIO $ runStateT (continue EVM.Types.Unknown) vm
                     interpret fetcher maxIter askSmtIters heuristic vm' (k r)
-
           _ -> performQuery
 
       Stepper.EVM m -> do

test/test.hs

@@ -226,9 +226,11 @@ tests = testGroup "hevm"
             let asBuf = Expr.fromList asList
             checkEquiv asBuf input
     , testProperty "evalProp-equivalence-lit" $ \(LitProp p) -> ioProperty $ do
-        let simplified = Expr.evalProp p
-        assertBool "must evaluate down to a literal bool" (isPBool simplified)
-        checkEquivProp simplified p
+        let simplified = Expr.simplifyProps [p]
+        case simplified of
+          [] -> checkEquivProp (PBool True) p
+          [val@(PBool _)] -> checkEquivProp val p
+          _ -> assertFailure "must evaluate down to a literal bool"
     , testProperty "evalProp-equivalence-sym" $ \(p) -> ioProperty $ do
         let simplified = Expr.evalProp p
         checkEquivProp simplified p
@@ -239,6 +241,67 @@ tests = testGroup "hevm"
         let simplified = pand (Expr.simplifyProps [p])
         checkEquivProp simplified p
     ]
+  , testGroup "simpProp-concrete-tests" [
+      testCase "simpProp-concrete-trues" $ do
+        let
+          t = [PBool True, PBool True]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [] simplified
+    , testCase "simpProp-concrete-false1" $ do
+        let
+          t = [PBool True, PBool False]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+    , testCase "simpProp-concrete-false2" $ do
+        let
+          t = [PBool False, PBool False]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+    , testCase "simpProp-concrete-or-1" $ do
+        let
+          -- a = 5 && (a=4 || a=3)  -> False
+          t = [PEq (Lit 5) (Var "a"), POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 3))]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+    , ignoreTest $ testCase "simpProp-concrete-or-2" $ do
+        let
+          -- Currently does not work, because we don't do simplification inside
+          --   POr/PAnd using canBeSat
+          -- a = 5 && (a=4 || a=5)  -> a=5
+          t = [PEq (Lit 5) (Var "a"), POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 5))]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [] simplified
+    , testCase "simpProp-concrete-and-1" $ do
+        let
+          -- a = 5 && (a=4 && a=3)  -> False
+          t = [PEq (Lit 5) (Var "a"), PAnd (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 3))]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+    , testCase "simpProp-concrete-or-of-or" $ do
+        let
+          -- a = 5 && ((a=4 || a=6) || a=3)  -> False
+          t = [PEq (Lit 5) (Var "a"), POr (POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 6))) (PEq (Var "a") (Lit 3))]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+    , testCase "simpProp-concrete-or-eq-rem" $ do
+        let
+          -- a = 5 && ((a=4 || a=6) || a=3)  -> False
+          t = [PEq (Lit 5) (Var "a"), POr (POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 6))) (PEq (Var "a") (Lit 3))]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+    , testCase "simpProp-inner-expr-simp" $ do
+        let
+          -- 5+1 = 6
+          t = [PEq (Add (Lit 5) (Lit 1)) (Var "a")]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PEq (Lit 6) (Var "a")] simplified
+    , testCase "simpProp-inner-expr-simp-with-canBeSat" $ do
+        let
+          -- 5+1 = 6, 6 != 7
+          t = [PAnd (PEq (Add (Lit 5) (Lit 1)) (Var "a")) (PEq (Var "a") (Lit 7))]
+          simplified = Expr.simplifyProps t
+        assertEqual "Must be equal" [PBool False] simplified
+  ]
   , testGroup "MemoryTests"
     [ testCase "read-write-same-byte"  $ assertEqual ""
         (LitByte 0x12)
@@ -2804,7 +2867,7 @@ checkEquivBase mkprop l r = withSolvers Z3 1 (Just 1) $ \solvers -> do
        putStrLn "skip"
        pure True
      else do
-       let smt = assertProps abstRefineDefault [mkprop l r]
+       let smt = assertPropsNoSimp abstRefineDefault [mkprop l r]
        res <- checkSat solvers smt
        print res
        pure $ case res of