Keccak improvements

src/EVM.hs

@@ -667,7 +667,7 @@ exec1 = do
                 else do
                   let
                     original =
-                      case Expr.concKeccakSimpExpr True $ SLoad x this.origStorage of
+                      case Expr.concKeccakSimpExpr $ SLoad x this.origStorage of
                         Lit v -> v
                         _ -> 0
                     storage_cost =
@@ -1260,7 +1260,7 @@ branch cond continue = do
   query $ PleaseAskSMT cond pathconds (choosePath loc)
   where
     condSimp = Expr.simplify cond
-    condSimpConc = Expr.concKeccakSimpExpr True condSimp
+    condSimpConc = Expr.concKeccakSimpExpr condSimp
     choosePath :: CodeLocation -> BranchCondition -> EVM s ()
     choosePath loc (Case v) = do
       assign #result Nothing
@@ -1304,11 +1304,14 @@ accessStorage
   -> (Expr EWord -> EVM s ())
   -> EVM s ()
 accessStorage addr slot continue = do
-  let slotConc = Expr.concKeccakSimpExpr True slot
+  let slotConc = Expr.concKeccakSimpExpr slot
   use (#env % #contracts % at addr) >>= \case
     Just c ->
       -- Try first without concretization. Then if we get a Just, with concretization
-      -- if both give a Just, should we `continue`
+      -- if both give a Just, should we `continue`.
+      -- --> This is because readStorage can do smart rewrites, but only in case
+      --     the expression is of a particular format, which can be destroyed by simplification.
+      --     However, without concretization, it may not find things that are actually in the storage
       case readStorage slot c.storage of
         Just x -> case readStorage slotConc c.storage of
           Just _ -> continue x

src/EVM/Expr.hs

@@ -1350,35 +1350,20 @@ constFoldProp ps = oneRun ps (ConstState mempty True)
         PBool False -> put $ ConstState {canBeSat=False, values=mempty}
         _ -> pure ()
 
--- Concretize Keccak Expressions until fixed-point.
--- Can either simplify before, or not
-concKeccakSimpExpr :: Bool -> Expr a -> Expr a
-concKeccakSimpExpr simp orig = final
-  where
-    simplified = if simp then simplify orig else orig
-    conc = mapExpr concKeccakSimpOnePass simplified
-    final = if conc == orig then conc
-                            else concKeccakSimpExpr simp conc
-
-concKeccakSimps :: Bool -> [Prop] -> [Prop]
-concKeccakSimps simp orig = final
-  where
-    conc = simplifyProps $ map (concKeccakSimp simp) orig
-    final = if conc == orig then conc
-                            else concKeccakSimps simp conc
-
-concKeccakSimp :: Bool -> Prop -> Prop
-concKeccakSimp simp orig = final
-  where
-    simplified = if simp then simplifyProp orig else orig
-    conc = mapProp concKeccakSimpOnePass simplified
-    final = if conc == orig then conc
-                            else concKeccakSimp simp conc
-
-concKeccakSimpOnePass :: Expr a -> Expr a
-concKeccakSimpOnePass (Keccak (ConcreteBuf bs)) = Lit (keccak' bs)
-concKeccakSimpOnePass orig@(Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) orig2@(WriteWord (Lit 0) _ (ConcreteBuf bs)) (ConcreteBuf ""))) =
+-- Concretize & simplify Keccak expressions until fixed-point.
+concKeccakSimpExpr :: Expr a -> Expr a
+concKeccakSimpExpr orig = untilFixpoint ((mapExpr concKeccakOnePass) . simplify) orig
+
+concKeccakProps :: [Prop] -> [Prop]
+concKeccakProps orig = simplifyProps $ untilFixpoint (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
+concKeccakOnePass :: Expr a -> Expr a
+concKeccakOnePass (Keccak (ConcreteBuf bs)) = Lit (keccak' bs)
+concKeccakOnePass orig@(Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) orig2@(WriteWord (Lit 0) _ (ConcreteBuf bs)) (ConcreteBuf ""))) =
   case (BS.length bs, (copySlice (Lit 0) (Lit 0) (Lit 64) (simplify orig2) (ConcreteBuf ""))) of
     (64, ConcreteBuf a) -> Lit (keccak' a)
     _ -> orig
-concKeccakSimpOnePass x = x
+concKeccakOnePass x = x

src/EVM/Format.hs

@@ -314,7 +314,7 @@ showTrace dapp env trace =
       let calltype = if target == context
                      then "call "
                      else "delegatecall "
-          hash' = fromJust $ maybeLitWord hash
+          hash' = fromJust $ maybeLitWord $ Expr.concKeccakSimpExpr hash
       in case preview (ix hash' % _2) dapp.solcByHash of
         Nothing ->
           calltype

src/EVM/SMT.hs

@@ -204,10 +204,12 @@ smt2Line :: Builder -> SMT2
 smt2Line txt = SMT2 [txt] mempty mempty mempty
 
 assertProps :: Config -> [Prop] -> SMT2
--- first simplify to rewrite sload/sstore combos, then concretize&simplify
-assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps)
+-- 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 conf $ Expr.simplifyProps ps
 
--- Note: we need a version that does NOT call simplify or simplifyProps,
+-- 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 :: Config -> [Prop] -> SMT2
@@ -239,7 +241,7 @@ assertPropsNoSimp config psPreConc =
   <> SMT2 mempty mempty mempty psPreConc
 
   where
-    ps = Expr.concKeccakSimps False psPreConc
+    ps = Expr.concKeccakProps psPreConc
     (psElim, bufs, stores) = eliminateProps ps
     (psElimAbst, abst@(AbstState abstExprToInt _)) = if config.abstRefineArith || config.abstRefineMem
       then abstractAwayProps config psElim

src/EVM/SymExec.hs

@@ -276,10 +276,9 @@ interpret fetcher maxIter askSmtIters heuristic vm =
         case q of
           PleaseAskSMT cond preconds continue -> do
             let
-              simpCond = Expr.concKeccakSimpExpr True cond
               -- no concretiziation here, or we may lose information
               simpProps = Expr.simplifyProps ((cond ./= Lit 0):preconds)
-            case simpCond of
+            case Expr.concKeccakSimpExpr cond of
               -- is the condition concrete?
               Lit c ->
                 -- have we reached max iterations, are we inside a loop?
@@ -836,7 +835,7 @@ formatCex cd sig m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $
     -- callvalue check inserted by solidity in contracts that don't have any
     -- payable functions).
     cd' = case sig of
-      Nothing -> prettyBuf . (Expr.concKeccakSimpExpr True) . defaultSymbolicValues $ subModel m cd
+      Nothing -> prettyBuf . Expr.concKeccakSimpExpr . defaultSymbolicValues $ subModel m cd
       Just (Sig n ts) -> prettyCalldata m cd n ts
 
     storeCex :: [Text]

src/EVM/Types.hs

@@ -1311,6 +1311,10 @@ paddedShowHex w n = pad ++ str
      str = showHex n ""
      pad = replicate (w - length str) '0'
 
+untilFixpoint :: Eq a => (a -> a) -> a -> a
+untilFixpoint f a = if f a == a
+                    then a
+                    else untilFixpoint f (f a)
 
 -- Optics ------------------------------------------------------------------------------------------