Merge pull request #199 from ethereum/bump-hevm

Bump hevm

Author: zoep

flake.lock

@@ -222,7 +222,7 @@ decompile' :: FilePath -> Text -> Solvers.Solver -> Maybe Integer -> Bool -> IO
 decompile' solFile' cid solver' timeout debug' = do
   let config = if debug' then debugActConfig else defaultActConfig
   cores <- fmap fromIntegral getNumProcessors
-  json <- solc Solidity =<< TIO.readFile solFile'
+  json <- flip (solc Solidity) False =<< TIO.readFile solFile'
   let (Contracts contracts, _, _) = fromJust $ readStdJSON json
   case Map.lookup ("hevm.sol:" <> cid) contracts of
     Nothing -> do
@@ -274,7 +274,7 @@ hevm actspec sol' code' initcode' solver' timeout debug' = do
 
 bytecodes :: Text -> Text -> IO (BS.ByteString, BS.ByteString)
 bytecodes cid src = do
-  json <- solc Solidity src
+  json <- solc Solidity src False
   let (Contracts sol', _, _) = fromJust $ readStdJSON json
   let err = error $ "Cannot find Solidity contract " <> Text.unpack cid
   pure ((fromMaybe err . Map.lookup ("hevm.sol" <> ":" <> cid) $ sol').creationCode,

src/Act/CLI.hs

@@ -46,8 +46,8 @@ import EVM.Solidity hiding (SlotType(..))
 import EVM.Solidity qualified as EVM (SlotType(..))
 import EVM.Types qualified as EVM
 import EVM.Types ((.<=), (.>=), (.==))
-import EVM.Solvers (SolverGroup, checkSat, CheckSatResult(..))
-import EVM.SymExec hiding (EquivResult)
+import EVM.Solvers (SolverGroup, checkSat)
+import EVM.SymExec
 import EVM.Expr qualified as Expr
 import EVM.Traversals (mapExprM)
 import GHC.IO hiding (liftIO)
@@ -111,7 +111,7 @@ summarize solvers contract = do
       let fragments = fmap (uncurry symAbiArg) contract.constructorInputs
           args = combineFragments' fragments 0 (EVM.ConcreteBuf "")
       initVM <- liftIO $ stToIO $ abstractVM (fst args, []) contract.creationCode Nothing True
-      expr <- Expr.simplify <$> interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr
+      expr <- Expr.simplify <$> interpret (Fetch.oracle solvers Nothing) iterConfig initVM runExpr
       let branches = flattenExpr expr
       if any isPartial branches
       then pure . Left $ "partially explored branches in creation code:\n" <> T.unlines (fmap formatExpr (filter isPartial branches))
@@ -126,7 +126,7 @@ summarize solvers contract = do
                      . (flip combineFragments) (EVM.AbstractBuf "txdata")
                      $ fmap (uncurry symAbiArg) method.inputs
         prestate <- liftIO $ stToIO $ abstractVM (fst calldata, []) contract.runtimeCode Nothing False
-        expr <- Expr.simplify <$> interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased prestate runExpr
+        expr <- Expr.simplify <$> interpret (Fetch.oracle solvers Nothing) iterConfig prestate runExpr
         let branches = flattenExpr expr
         if any isPartial branches
         then pure . Left $ "partially explored branches in runtime code:\n" <> T.unlines (fmap formatExpr (filter isPartial branches))
@@ -168,8 +168,8 @@ makeIntSafe solvers expr = evalStateT (mapExprM go expr) mempty
                , fromMaybe (EVM.PBool True) (Map.lookup r s)
                , EVM.PNeg safe
                ]
-      liftIO (checkSat solvers (assertProps defaultActConfig ps)) >>= \case
-        Unsat -> do
+      liftIO (checkSat solvers Nothing (assertProps defaultActConfig ps)) >>= \case
+        EVM.Qed -> do
           put $ Map.insert full safe s
           pure full
         _ -> pure $ EVM.Mod full (EVM.Lit MAX_UINT)

src/Act/Decompile.hs

@@ -49,9 +49,8 @@ import EVM.ABI (Sig(..))
 import qualified EVM hiding (bytecode)
 import qualified EVM.Types as EVM hiding (FrameState(..))
 import EVM.Expr hiding (op2, inRange, div, xor, readStorage)
-import EVM.SymExec hiding (EquivResult, isPartial, reachable)
-import qualified EVM.SymExec as SymExec (EquivResult, ProofResult(..))
-import EVM.SMT (SMTCex(..), assertProps)
+import EVM.SymExec hiding (isPartial, reachable)
+import EVM.SMT (assertProps)
 import EVM.Solvers
 import EVM.Effects
 import EVM.Format as Format
@@ -73,7 +72,7 @@ type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract, Id)
 -- when we encounter a constructor call.
 type CodeMap = M.Map Id (Contract, BS.ByteString, BS.ByteString)
 
-type EquivResult = ProofResult () (T.Text, SMTCex) T.Text T.Text
+type EquivResult = EVM.ProofResult (String, EVM.SMTCex) String
 
 initAddr :: EVM.Expr EVM.EAddr
 initAddr = EVM.SymAddr "entrypoint"
@@ -677,14 +676,14 @@ checkOp (Create _ _ _) = error "Internal error: invalid in range expression"
 -- | Wrapper for the equivalenceCheck function of hevm
 checkEquiv :: App m => SolverGroup -> [EVM.Expr EVM.End] -> [EVM.Expr EVM.End] -> m [EquivResult]
 checkEquiv solvers l1 l2 = do
-  (res, _) <- equivalenceCheck' solvers l1 l2 False
-  pure $ fmap toEquivRes res
+  EqIssues res _ <- equivalenceCheck' solvers l1 l2 False
+  pure $ fmap (toEquivRes . fst) res
   where
-    toEquivRes :: SymExec.EquivResult -> EquivResult
-    toEquivRes (Cex cex) = Cex ("\x1b[1mThe following input results in different behaviours\x1b[m", cex)
-    toEquivRes (Qed a) = Qed a
-    toEquivRes (SymExec.Unknown ()) = SymExec.Unknown ""
-    toEquivRes (SymExec.Error b) = SymExec.Error (T.pack b)
+    toEquivRes :: EVM.EquivResult -> EquivResult
+    toEquivRes (EVM.Cex cex) = EVM.Cex ("\x1b[1mThe following input results in different behaviours\x1b[m", cex)
+    toEquivRes EVM.Qed = EVM.Qed
+    toEquivRes (EVM.Unknown s) = EVM.Unknown s
+    toEquivRes (EVM.Error b) = EVM.Error b
 
 
 -- | Create the initial contract state before analysing a contract
@@ -738,7 +737,7 @@ getInitContractState solvers iface pointers preconds cmap = do
     checkQueries :: App m => [EVM.Prop] -> m (Error String ())
     checkQueries queries = do
       conf <- readConfig
-      res <- liftIO $ checkSat solvers (assertProps conf queries)
+      res <- liftIO $ checkSat solvers Nothing (assertProps conf queries)
       checkResult (makeCalldata iface) Nothing [toVRes msg res]
 
     makeSymAddr n = EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show n))
@@ -955,15 +954,15 @@ checkInputSpaces solvers l1 l2 = do
   let queries = fmap (assertProps conf) [ [ EVM.PNeg (EVM.por p1), EVM.por p2 ]
                                         , [ EVM.por p1, EVM.PNeg (EVM.por p2) ] ]
 
-  results <- liftIO $ mapConcurrently (checkSat solvers) queries
+  results <- liftIO $ mapConcurrently (checkSat solvers Nothing) queries
   let results' = case results of
                    [r1, r2] -> [ toVRes "\x1b[1mThe following inputs are accepted by Act but not EVM\x1b[m" r1
                                , toVRes "\x1b[1mThe following inputs are accepted by EVM but not Act\x1b[m" r2 ]
                    _ -> error "Internal error: impossible"
 
-  case all isQed results' of
-    True -> pure [Qed ()]
-    False -> pure $ filter (/= Qed ()) results'
+  case all EVM.isQed results' of
+    True -> pure [EVM.Qed]
+    False -> pure $ filter (/= EVM.Qed) results'
 
 
 
@@ -978,7 +977,7 @@ checkAbi solver contract cmap = do
   evmBehvs <- getRuntimeBranches solver hevmstorage (txdata, []) 0 -- TODO what freshAddr goes here?
   conf <- readConfig
   let queries =  fmap (assertProps conf) $ filter (/= []) $ fmap (checkBehv selectorProps) evmBehvs
-  res <- liftIO $ mapConcurrently (checkSat solver) queries
+  res <- liftIO $ mapConcurrently (checkSat solver Nothing) queries
   checkResult (txdata, []) Nothing (fmap (toVRes msg) res)
 
   where
@@ -1034,19 +1033,19 @@ assertSelector txdata sig =
 
 -- * Utils
 
-toVRes :: T.Text -> CheckSatResult -> EquivResult
+toVRes :: String -> EVM.SMTResult -> EquivResult
 toVRes msg res = case res of
-  Sat cex -> Cex (msg, cex)
-  EVM.Solvers.Unknown e -> SymExec.Unknown (T.pack e)
-  Unsat -> Qed ()
-  EVM.Solvers.Error e -> SymExec.Error (T.pack e)
+  EVM.Cex cex -> EVM.Cex (msg, cex)
+  EVM.Unknown e -> EVM.Unknown e
+  EVM.Qed -> EVM.Qed
+  EVM.Error e -> EVM.Error e
 
 
 checkResult :: App m => Calldata -> Maybe Sig -> [EquivResult] -> m (Error String ())
 checkResult calldata sig res =
-  case any isCex res of
+  case any EVM.isCex res of
     False ->
-      case any isUnknown res || any isError res of
+      case any EVM.isUnknown res || any EVM.isError res of
         True -> do
           showMsg "\x1b[41mNo discrepancies found but timeouts or solver errors were encountered. \x1b[m"
           pure $ Failure $ NE.singleton (nowhere, "Failure: Cannot prove equivalence.")
@@ -1055,7 +1054,7 @@ checkResult calldata sig res =
           pure $ Success ()
     True -> do
       let cexs = mapMaybe getCex res
-      showMsg $ T.unpack . T.unlines $ [ "\x1b[41mNot equivalent.\x1b[m", "" , "-----", ""] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (\(msg, cex) -> msg <> "\n" <> formatCex (fst calldata) sig cex) cexs)
+      showMsg $ T.unpack . T.unlines $ [ "\x1b[41mNot equivalent.\x1b[m", "" , "-----", ""] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (\(msg, cex) -> T.pack msg <> "\n" <> formatCex (fst calldata) sig cex) cexs)
       pure $ Failure $ NE.singleton (nowhere, "Failure: Cannot prove equivalence.")
 
 -- | Pretty prints a list of hevm behaviours for debugging purposes

src/Act/HEVM.hs

@@ -26,7 +26,7 @@ import Act.Syntax.Untyped (makeIface)
 import qualified EVM.Types as EVM
 import EVM.Types (VM(..))
 import EVM.Expr hiding (op2, inRange)
-import EVM.SymExec hiding (EquivResult, isPartial, abstractVM, loadSymVM)
+import EVM.SymExec hiding (isPartial, abstractVM, loadSymVM)
 import EVM.Solvers
 import qualified EVM.Format as Format
 import qualified EVM.Fetch as Fetch
@@ -53,12 +53,15 @@ defaultActConfig = Config
   , numCexFuzz = 0
   , onlyCexFuzz = False
   , decomposeStorage = False
-  , maxBranch = 100
   , promiseNoReent = False
   , maxBufSize = 64
+  , maxWidth = 100
+  , maxDepth = Nothing
   , verb = 0
+  , simp = True
   }
 
+
 debugActConfig :: Config
 debugActConfig = defaultActConfig { dumpQueries = True, dumpExprs = True, dumpEndStates = True, debug = True }
 
@@ -107,11 +110,19 @@ checkPartial nodes =
      showMsg ""
      showMsg . T.unpack . T.unlines . fmap (Format.indent 2 . ("- " <>)) . fmap Format.formatPartial . nubOrd $ (getPartials nodes)
 
+
+iterConfig :: IterConfig
+iterConfig = IterConfig
+  { maxIter = Nothing
+  , askSmtIters = 1
+  , loopHeuristic = StackBased
+  }
+
 -- | decompiles the given EVM bytecode into a list of Expr branches
 getRuntimeBranches :: App m => SolverGroup -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> Int -> m [EVM.Expr EVM.End]
 getRuntimeBranches solvers contracts calldata fresh = do
   prestate <- liftIO $ stToIO $ abstractVM contracts calldata fresh
-  expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased prestate runExpr
+  expr <- interpret (Fetch.oracle solvers Nothing) iterConfig prestate runExpr
   let simpl = simplify expr
   let nodes = flattenExpr simpl
   checkPartial nodes
@@ -122,7 +133,7 @@ getRuntimeBranches solvers contracts calldata fresh = do
 getInitcodeBranches :: App m => SolverGroup -> BS.ByteString -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> [EVM.Prop] -> Int -> m [EVM.Expr EVM.End]
 getInitcodeBranches solvers initcode contracts calldata precond fresh = do
   initVM <- liftIO $ stToIO $ abstractInitVM initcode contracts calldata precond fresh
-  expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr
+  expr <- interpret (Fetch.oracle solvers Nothing) iterConfig initVM runExpr
   let simpl = simplify expr
   let nodes = flattenExpr simpl
   checkPartial nodes
@@ -170,7 +181,7 @@ loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create fresh =
      , origin = EVM.SymAddr "origin"
      , gas = ()
      , gaslimit = 0xffffffffffffffff
-     , number = 0
+     , number = EVM.Lit 0
      , timestamp = EVM.Lit 0
      , coinbase = EVM.SymAddr "coinbase"
      , prevRandao = 42069

src/Act/HEVM_utils.hs

@@ -106,7 +106,7 @@ decompilerTests = testGroup "decompiler"
 
 checkDecompilation :: Text -> Text -> Assertion
 checkDecompilation contract src = do
-  json <- solc Solidity src
+  json <- solc Solidity src False
   let (Contracts sol, _, _) = fromJust $ readStdJSON json
   let c = fromJust $ Map.lookup ("hevm.sol:" <> contract) sol
   runEnv (Env defaultActConfig) (Solvers.withSolvers CVC5 1 1 (Just 100000000) (decompile c)) >>= \case