Merge pull request #783 from ethereum/concretization-addmod-mulmod

Adding a number of serious improvements to dispatched SMT2 query

Author: msooseth

CHANGELOG.md

@@ -61,6 +61,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   via masking
 - More rewrite rules for (PLT (Lit 0) _) and (PEq (Lit 1) _)
 - Simplification can now be turned off from the cli via --no-simplify
+- When doing Keccak concretization, and simplification is enabled,
+  we do both until fixedpoint
+- When gathering Keccak axioms, we simplify the bytestring that
+  the keccak is applied to
+- More rewrite rules for MulMod, AddMod, SHL, SHR, SLT, and SignExtend
+- PLEq is now concretized in case it can be computed
+- More SignExtend test cases
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM/Expr.hs

@@ -40,6 +40,12 @@ import EVM.Types
 maxLit :: W256
 maxLit = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
 
+maxLitSigned :: W256
+maxLitSigned = 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+
+minLitSigned :: W256
+minLitSigned = 0x1000000000000000000000000000000000000000000000000000000000000000
+
 -- ** Stack Ops ** ---------------------------------------------------------------------------------
 
 
@@ -103,14 +109,12 @@ smod = op2 SMod (\x y ->
 
 addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
 addmod = op3 AddMod (\x y z ->
-  if z == 0
-  then 0
+  if z == 0 then 0
   else fromIntegral $ (into @Word512 x + into y) `Prelude.mod` into z)
 
 mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
 mulmod = op3 MulMod (\x y z ->
-  if z == 0
-  then 0
+  if z == 0 then 0
   else fromIntegral $ (into @Word512 x * into y) `Prelude.mod` into z)
 
 exp :: Expr EWord -> Expr EWord -> Expr EWord
@@ -203,13 +207,20 @@ sar = op2 SAR (\x y ->
 
 peq :: (Typeable a) => Expr a -> Expr a -> Prop
 peq (Lit x) (Lit y) = PBool (x == y)
+peq (LitAddr x) (LitAddr y) = PBool (x == y)
 peq (LitByte x) (LitByte y) = PBool (x == y)
 peq (ConcreteBuf x) (ConcreteBuf y) = PBool (x == y)
 peq a b
   | a == b = PBool True
   | otherwise = let args = sort [a, b]
      in PEq (args !! 0) (args !! 1)
 
+pleq :: Expr EWord -> Expr EWord -> Prop
+pleq (Lit a) (Lit b) = PBool (a <= b)
+pleq a b
+  | a == b = PBool True
+  | otherwise = PLEq a b
+
 -- ** Bufs ** --------------------------------------------------------------------------------------
 
 
@@ -1057,21 +1068,9 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
 
     go (IndexWord a b) = indexWord a b
 
-    -- LT
-    go (EVM.Types.LT (Lit a) (Lit b))
-      | a < b = Lit 1
-      | otherwise = Lit 0
-    go (EVM.Types.LT _ (Lit 0)) = Lit 0
-    go (EVM.Types.LT a (Lit 1)) = iszero a
-    go (EVM.Types.LT (Lit 0) a) = iszero (Eq (Lit 0) a)
 
-    -- normalize all comparisons in terms of LT
-    go (EVM.Types.GT a b) = lt b a
-    go (EVM.Types.GEq a b) = leq b a
-    go (EVM.Types.LEq a b) = iszero (lt b a)
-    go (SLT a@(Lit _) b@(Lit _)) = slt a b
-    go (SGT a b) = SLT b a
     go (SEx a (SEx a2 b)) | a == a2  = sex a b
+    go (SEx _ (Lit 0)) = Lit 0
     go (SEx a b) = sex a b
 
     -- IsZero
@@ -1106,14 +1105,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     -- literal addresses
     go (WAddr (LitAddr a)) = Lit $ into a
 
-    -- simple div/mod/add/sub
-    go (Div o1@(Lit _)  o2@(Lit _)) = EVM.Expr.div  o1 o2
-    go (SDiv o1@(Lit _) o2@(Lit _)) = EVM.Expr.sdiv o1 o2
-    go (Mod o1@(Lit _)  o2@(Lit _)) = EVM.Expr.mod  o1 o2
-    go (SMod o1@(Lit _) o2@(Lit _)) = EVM.Expr.smod o1 o2
-    go (Add o1@(Lit _)  o2@(Lit _)) = EVM.Expr.add  o1 o2
-    go (Sub o1@(Lit _)  o2@(Lit _)) = EVM.Expr.sub  o1 o2
-
     -- Mod
     go (Mod _ (Lit 0)) = Lit 0
     go (SMod _ (Lit 0)) = Lit 0
@@ -1122,6 +1113,18 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     go (Mod (Lit 0) _) = Lit 0
     go (SMod (Lit 0) _) = Lit 0
 
+    -- MulMod
+    go (MulMod (Lit 0) _ _) = Lit 0
+    go (MulMod _ (Lit 0) _) = Lit 0
+    go (MulMod _ _ (Lit 0)) = Lit 0
+    go (MulMod a b c) = mulmod a b c
+
+    -- AddMod
+    go (AddMod (Lit 0) a b) = Mod a b
+    go (AddMod a (Lit 0) b) = Mod a b
+    go (AddMod _ _ (Lit 0)) = Lit 0
+    go (AddMod a b c) = addmod a b c
+
     -- Triple And (must be before 3-way sort below)
     go (And (Lit a) (And (Lit b) c)) = And (EVM.Expr.and (Lit a) (Lit b)) c
 
@@ -1207,9 +1210,11 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     -- SHL / SHR by 0
     go (SHL a v)
       | a == (Lit 0) = v
+      | v == (Lit 0) = v
       | otherwise = shl a v
     go (SHR a v)
       | a == (Lit 0) = v
+      | v == (Lit 0) = v
       | otherwise = shr a v
 
     -- Bitwise AND & OR. These MUST preserve bitwise equivalence
@@ -1286,6 +1291,29 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
            then Lit 0
            else o
 
+    -- normalize all comparisons in terms of (S)LT
+    go (EVM.Types.GT a b) = lt b a
+    go (EVM.Types.GEq a b) = leq b a
+    go (EVM.Types.LEq a b) = iszero (lt b a)
+    go (SGT a b) = slt b a
+
+    -- LT
+    go (EVM.Types.LT _ (Lit 0)) = Lit 0
+    go (EVM.Types.LT a (Lit 1)) = iszero a
+    go (EVM.Types.LT (Lit 0) a) = iszero (Eq (Lit 0) a)
+    go (EVM.Types.LT a b) = lt a b
+
+    -- SLT
+    go (SLT _ (Lit a)) | a == minLitSigned = Lit 0
+    go (SLT (Lit a) _) | a == maxLitSigned = Lit 0
+    go (SLT a b) = slt a b
+
+    -- simple div/mod/add/sub
+    go (Div  o1 o2) = EVM.Expr.div  o1 o2
+    go (SDiv o1 o2) = EVM.Expr.sdiv o1 o2
+    go (Mod  o1 o2) = EVM.Expr.mod  o1 o2
+    go (SMod o1 o2) = EVM.Expr.smod o1 o2
+
     go a = a
 
 
@@ -1330,6 +1358,7 @@ simplifyProp prop =
     go (PLEq (Sub a b) c) | a == c = PLEq b a
     go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)
     go (PLT (Lit 0) (Eq a b)) = peq a b
+    go (PLEq a b) = pleq a b
 
     -- when it's PLT but comparison on the RHS then it's just (PEq 1 RHS)
     go (PLT (Lit 0) (a@LT {})) = peq (Lit 1) a
@@ -1338,6 +1367,7 @@ simplifyProp prop =
     go (PLT (Lit 0) (a@GT {})) = peq (Lit 1) a
     go (PLT (Lit 0) (a@GEq {})) = peq (Lit 1) a
     go (PLT (Lit 0) (a@SGT {})) = peq (Lit 1) a
+    go (POr (PLEq a1 (Lit b)) (PLEq (Lit c) a2)) | a1 == a2 && c == b+1 = PBool True
 
     -- negations
     go (PNeg (PBool b)) = PBool (Prelude.not b)
@@ -1348,6 +1378,7 @@ simplifyProp prop =
     go (PNeg (PLEq a b)) = PGT a b
     go (PNeg (PAnd a b)) = POr (PNeg a) (PNeg b)
     go (PNeg (POr a b)) = PAnd (PNeg a) (PNeg b)
+    go (PNeg (PEq (Lit 1) (IsZero b))) = PEq (Lit 0) (IsZero b)
 
     -- Empty buf
     go (PEq (Lit 0) (BufLength k)) = peq k (ConcreteBuf "")
@@ -1739,6 +1770,10 @@ concKeccakSimpExpr orig = untilFixpoint (simplifyNoLitToKeccak . (mapExpr concKe
 concKeccakProps :: [Prop] -> [Prop]
 concKeccakProps orig = untilFixpoint (map (mapProp concKeccakOnePass)) orig
 
+-- As above, but also simplify, to fixedpoint
+concKeccakSimpProps :: [Prop] -> [Prop]
+concKeccakSimpProps orig = untilFixpoint (simplifyProps . map (mapProp concKeccakOnePass)) orig
+
 -- Simplifies in case the input to the Keccak is of specific array/map format and
 --            can be simplified into a concrete value
 -- Turns (Keccak ConcreteBuf) into a Lit

src/EVM/Fuzz.hs

@@ -27,7 +27,7 @@ import Test.QuickCheck.Random (mkQCGen)
 tryCexFuzz :: [Prop] -> Integer -> (Maybe (SMT.SMTCex))
 tryCexFuzz prePs tries = unGen (testVals tries) (mkQCGen 0) 1337
   where
-    ps = Expr.simplifyProps $ Expr.concKeccakProps prePs
+    ps = Expr.concKeccakSimpProps prePs
     vars = extractVars ps
     bufs = extractBufs ps
     stores = extractStorage ps
@@ -39,7 +39,7 @@ tryCexFuzz prePs tries = unGen (testVals tries) (mkQCGen 0) 1337
       storeVals <- getStores stores
       let
         ret = filterCorrectKeccak $ map (substituteEWord varvals . substituteBuf bufVals . substituteStores storeVals) ps
-        retSimp = Expr.simplifyProps $ Expr.concKeccakProps ret
+        retSimp = Expr.concKeccakSimpProps ret
       if null retSimp then pure $ Just (SMT.SMTCex {
                                     vars = varvals
                                     , addrs = mempty

src/EVM/Keccak.hs

@@ -63,10 +63,10 @@ keccakAssumptions :: [Prop] -> [Expr Buf] -> [Expr Storage] -> [Prop]
 keccakAssumptions ps bufs stores = injectivity <> minValue <> minDiffOfPairs
   where
     (_, st) = runState (findKeccakPropsExprs ps bufs stores) initState
-
-    keccakPairs = uniquePairs (Set.toList st.keccakExprs)
+    ks = Set.toList $ Set.map concretizeKeccakParam st.keccakExprs
+    keccakPairs = uniquePairs ks
     injectivity = map injProp keccakPairs
-    minValue = map minProp (Set.toList st.keccakExprs)
+    minValue = map minProp ks
     minDiffOfPairs = map minDistance keccakPairs
      where
       minDistance :: (Expr EWord, Expr EWord) -> Prop
@@ -76,12 +76,16 @@ keccakAssumptions ps bufs stores = injectivity <> minValue <> minDiffOfPairs
           req2 = (PGEq (Sub kb ka) (Lit 256))
       minDistance _ = internalError "expected Keccak expression"
 
+concretizeKeccakParam :: Expr EWord -> Expr EWord
+concretizeKeccakParam (Keccak buf) = Keccak (concKeccakSimpExpr buf)
+concretizeKeccakParam _ = internalError "Cannot happen"
+
 compute :: forall a. Expr a -> Set Prop
 compute = \case
   e@(Keccak buf) -> do
     let b = simplify buf
     case keccak b of
-      lit@(Lit _) -> Set.singleton (PEq lit e)
+      lit@(Lit _) -> Set.singleton (PEq lit (concretizeKeccakParam e))
       _ -> Set.empty
   _ -> Set.empty
 

src/EVM/SMT.hs

@@ -92,6 +92,7 @@ collapse model = case toBuf model of
 getVar :: SMTCex -> TS.Text -> W256
 getVar cex name = fromJust $ Map.lookup (Var name) cex.vars
 
+-- Props are ONLY for pretty printing the query Props
 data SMT2 = SMT2 [Builder] CexVars [Prop]
   deriving (Eq, Show)
 
@@ -132,11 +133,13 @@ declareIntermediates bufs stores = do
 smt2Line :: Builder -> SMT2
 smt2Line txt = SMT2 [txt] mempty mempty
 
-assertProps :: Config -> [Prop] -> Err SMT2
 -- simplify to rewrite sload/sstore combos
--- notice: it is VERY important not to concretize, because Keccak assumptions
---         will be generated by assertPropsNoSimp, and that needs unconcretized Props
-assertProps conf ps = assertPropsNoSimp (decompose . Expr.simplifyProps $ ps)
+-- notice: it is VERY important not to concretize early, because Keccak assumptions
+--         need unconcretized Props
+assertProps :: Config -> [Prop] -> Err SMT2
+assertProps conf ps =
+  if not conf.simp then assertPropsHelper False ps
+  else assertPropsHelper True (decompose . Expr.simplifyProps $ ps)
   where
     decompose :: [Prop] -> [Prop]
     decompose props = if conf.decomposeStorage && safeExprs && safeProps
@@ -147,11 +150,12 @@ assertProps conf ps = assertPropsNoSimp (decompose . Expr.simplifyProps $ ps)
         safeExprs = all (isJust . mapPropM_ Expr.safeToDecompose) props
         safeProps = all Expr.safeToDecomposeProp props
 
+
 -- Note: we need a version that does NOT call simplify,
 -- because we make use of it to verify the correctness of our simplification
 -- passes through property-based testing.
-assertPropsNoSimp :: [Prop] -> Err SMT2
-assertPropsNoSimp psPreConc = do
+assertPropsHelper :: Bool -> [Prop]  -> Err SMT2
+assertPropsHelper simp psPreConc = do
  encs <- mapM propToSMT psElim
  intermediates <- declareIntermediates bufs stores
  readAssumes' <- readAssumes
@@ -177,12 +181,10 @@ assertPropsNoSimp psPreConc = do
   <> readAssumes'
   <> gasOrder
   <> smt2Line ""
-  <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty
-  <> SMT2 mempty mempty { storeReads = storageReads } mempty
-  <> SMT2 mempty mempty psPreConc
+  <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) (cexInfo storageReads) ps
 
   where
-    ps = Expr.concKeccakProps psPreConc
+    ps = if simp then Expr.concKeccakSimpProps psPreConc else Expr.concKeccakProps psPreConc
     (psElim, bufs, stores) = eliminateProps ps
 
     -- Props storing info that need declaration(s)
@@ -219,6 +221,10 @@ assertPropsNoSimp psPreConc = do
       assumps <- mapM assertSMT $ assertReads psElim bufs stores
       pure $ smt2Line "; read assumptions" <> SMT2 assumps mempty mempty
 
+    cexInfo :: Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord)) -> CexVars
+    cexInfo a = mempty { storeReads = a }
+
+
 referencedAbstractStores :: TraversableTerm a => a -> Set Builder
 referencedAbstractStores term = foldTerm go mempty term
   where

src/EVM/Solvers.hs

@@ -106,7 +106,7 @@ checkSatWithProps sg props = do
   let psSimp = if conf.simp then simplifyProps props else props
   if psSimp == [PBool False] then pure (Qed, Right mempty)
   else do
-    let smt2 = if conf.simp then assertProps conf psSimp else assertPropsNoSimp psSimp
+    let smt2 = assertProps conf psSimp
     if isLeft smt2 then
       let err = getError smt2 in pure (Error err, Left err)
     else do
@@ -126,9 +126,9 @@ checkSatWithProps sg props = do
         readChan resChan
 
 writeSMT2File :: SMT2 -> String -> IO ()
-writeSMT2File smt2 postfix =
+writeSMT2File smt2 postfix = do
     let content = formatSMT2 smt2 <> "\n\n(check-sat)"
-    in T.writeFile ("query-" <> postfix <> ".smt2") content
+    T.writeFile ("query-" <> postfix <> ".smt2") content
 
 withSolvers :: App m => Solver -> Natural -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
 withSolvers solver count threads timeout cont = do

src/EVM/SymExec.hs

@@ -400,7 +400,7 @@ interpret fetcher iterConf vm =
                     -- ask the smt solver about the loop condition
                     performQuery
                   _ -> do
-                    let simpProps = Expr.simplifyProps $ Expr.concKeccakProps ((cond ./= Lit 0):preconds)
+                    let simpProps = Expr.concKeccakSimpProps ((cond ./= Lit 0):preconds)
                     (r, vm') <- case simpProps of
                       [PBool False] -> liftIO $ stToIO $ runStateT (continue (Case False)) vm
                       [] -> liftIO $ stToIO $ runStateT (continue (Case True)) vm

test/test.hs

@@ -4467,6 +4467,17 @@ tests = testGroup "hevm"
         assertEqualM "Must be 3-length" 3 (length simp2)
     -- we run these without the simplifier inside `checkSatWithProps`, so
     -- we can test the SMT solver's ability to handle sign extension
+    , test "sign-extend-conc-1" $ do
+      let p = Expr.sex (Lit 0) (Lit 0xff)
+      assertEqualM "stuff" p (Expr.simplify (Sub (Lit 0) (Lit 1)))
+      let p2 = Expr.sex (Lit 30) (Lit 0xff)
+      assertEqualM "stuff" p2 (Lit 0xff)
+      let p3 = Expr.sex (Lit 1) (Lit 0xff)
+      assertEqualM "stuff" p3 (Lit 0xff)
+      let p4 = Expr.sex (Lit 0) (Lit 0x1)
+      assertEqualM "stuff" p4 (Lit 0x1)
+      let p5 = Expr.sex (Lit 0) (Lit 0x0)
+      assertEqualM "stuff" p5 (Lit 0x0)
     , testNoSimplify "sign-extend-1" $ do
         let p = (PEq (Lit 1) (SLT (Lit 1774544) (SEx (Lit 2) (Lit 1774567))))
         let simp = Expr.simplifyProps [p]