Merge pull request #1441 from gustavo-grieco/dev-sym-exec-fixes

Symbolic execution fixes to make sure no counter example is missed

Author: elopez

flake.nix

@@ -54,8 +54,8 @@
           (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "ethereum";
             repo = "hevm";
-            rev = "9982c580ed19b88ebab9744d29d940fd2f0bd8c6";
-            sha256 = "sha256-B60aJo9EfIaTWuJaN06Wl1Br+rstzUAYGFBE5rX72Fs=";
+            rev = "87fe0eec5abb69c0b54c097784dfd8712a36de70";
+            sha256 = "sha256-cgfrP+K5NoXvVPRN6XRnTkdOIJztc/4wrto9nQ/9tnY=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck

lib/Echidna.hs

@@ -15,7 +15,6 @@ import System.FilePath ((</>))
 import EVM (cheatCode)
 import EVM.ABI (AbiValue(AbiAddress))
 import EVM.Dapp (dappInfo)
-import EVM.Fetch qualified
 import EVM.Solidity (BuildOutput(..), Contracts(Contracts), Method(..), Mutability(..), SolcContract(..))
 import EVM.Types hiding (Env)
 
@@ -111,7 +110,7 @@ loadInitialCorpus env = do
 mkEnv :: EConfig -> BuildOutput -> [EchidnaTest] -> World -> Maybe SlitherInfo -> IO Env
 mkEnv cfg buildOutput tests world slitherInfo = do
   codehashMap <- newIORef mempty
-  chainId <- maybe (pure Nothing) EVM.Fetch.fetchChainIdFrom cfg.rpcUrl
+  chainId <- maybe (pure Nothing) Onchain.fetchChainIdFrom (Just cfg.rpcUrl)
   eventQueue <- newChan
   coverageRefInit <- newIORef mempty
   coverageRefRuntime <- newIORef mempty

lib/Echidna/Campaign.hs

@@ -294,27 +294,26 @@ runSymWorker callback vm dict workerId _ name = do
 
     modify' (\ws -> ws { runningThreads = [] })
     lift callback
+    -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event
+    newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs
     let methodSignature = unpack method.methodSignature
-    if not (null partials) || not (null errors) then do
+    unless newCoverage ( do
+      unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong."
+      updateTests $ \test -> do
+        if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
+              pure $ Just $ test { Test.state = Unsolvable }
+        else
+          pure $ Just test
+      pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction."))
+
+    when (not (null partials) || not (null errors)) $ do
       unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors
       unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials
       updateTests $ \test -> do
-          if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
-              pure $ Just $ test { Test.state = Passed }
-          else
-            pure $ Just test
-    else do
-      -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event
-      newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs
-
-      unless newCoverage ( do
-        unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong."
-        updateTests $ \test -> do
-          if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
-                pure $ Just $ test { Test.state = Unsolvable }
-          else
-            pure $ Just test
-        pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction."))
+        if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
+          pure $ Just $ test {Test.state = Passed}
+        else
+          pure $ Just test
 
 -- | Run a fuzzing campaign given an initial universe state, some tests, and an
 -- optional dictionary to generate calls with. Return the 'Campaign' state once

lib/Echidna/Onchain.hs

@@ -3,9 +3,8 @@
 module Echidna.Onchain where
 
 import Control.Exception (catch)
-import Data.Aeson (ToJSON, FromJSON, ToJSONKey(toJSONKey))
+import Data.Aeson (ToJSON, FromJSON)
 import Data.Aeson qualified as JSON
-import Data.Aeson.Types (toJSONKeyText)
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.ByteString.UTF8 qualified as UTF8
@@ -25,9 +24,11 @@ import Optics (view)
 import System.Directory (createDirectoryIfMissing, doesFileExist)
 import System.Environment (lookupEnv)
 import System.FilePath ((</>))
+import Network.Wreq.Session qualified as Session
 import Text.Read (readMaybe)
 
 import EVM (initialContract, bytecode)
+import EVM.Effects (defaultConfig)
 import EVM.Fetch qualified
 import EVM.Solidity (SourceCache(..), SolcContract (..))
 import EVM.Types hiding (Env)
@@ -57,16 +58,16 @@ etherscanApiKey = do
 
 -- TODO: temporary solution, handle errors gracefully
 safeFetchContractFrom :: EVM.Fetch.BlockNumber -> Text -> Addr -> IO (Maybe Contract)
-safeFetchContractFrom rpcBlock rpcUrl addr =
+safeFetchContractFrom rpcBlock rpcUrl addr = do
   catch
-    (EVM.Fetch.fetchContractFrom rpcBlock rpcUrl addr)
+    (EVM.Fetch.fetchContractFrom defaultConfig rpcBlock rpcUrl addr)
     (\(_ :: HttpException) -> pure $ Just emptyAccount)
 
 -- TODO: temporary solution, handle errors gracefully
 safeFetchSlotFrom :: EVM.Fetch.BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
 safeFetchSlotFrom rpcBlock rpcUrl addr slot =
   catch
-    (EVM.Fetch.fetchSlotFrom rpcBlock rpcUrl addr slot)
+    (EVM.Fetch.fetchSlotFrom defaultConfig rpcBlock rpcUrl addr slot)
     (\(_ :: HttpException) -> pure $ Just 0)
 
 data FetchedContractData = FetchedContractData
@@ -76,9 +77,6 @@ data FetchedContractData = FetchedContractData
   }
   deriving (Generic, ToJSON, FromJSON, Show)
 
-instance ToJSONKey W256 where
-  toJSONKey = toJSONKeyText (Text.pack . show)
-
 fromFetchedContractData :: FetchedContractData -> Contract
 fromFetchedContractData contractData =
   (initialContract (RuntimeCode (ConcreteRuntimeCode contractData.runtimeCode)))
@@ -211,3 +209,12 @@ saveCoverageReport env runId = do
                                 [solcContract]
                 Nothing -> pure ()
             Nothing -> pure ()
+
+fetchChainIdFrom :: Maybe Text -> IO (Maybe W256)
+fetchChainIdFrom (Just url) = do
+  sess <- Session.newAPISession
+  EVM.Fetch.fetchQuery
+    EVM.Fetch.Latest -- this shouldn't matter
+    (EVM.Fetch.fetchWithSession url sess)
+    EVM.Fetch.QueryChainId
+fetchChainIdFrom Nothing = pure Nothing

lib/Echidna/SymExec/Common.hs

@@ -1,27 +1,26 @@
 module Echidna.SymExec.Common where
 
 import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO)
-import Data.ByteString.Lazy qualified as BS
 import Data.Function ((&))
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text qualified as T
-import Data.Vector (toList, fromList)
 import GHC.IORef (IORef, readIORef)
 import Optics.Core ((.~), (%), (%~))
-import EVM.ABI (abiKind, AbiKind(Dynamic), AbiValue(..), AbiType(..), Sig(..), decodeAbiValue)
+import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..))
 import EVM.Fetch qualified as Fetch
-import EVM (loadContract, resetState, forceLit)
+import EVM (loadContract, resetState, symbolify)
 import EVM.Effects (TTY, ReadConfig)
-import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData(..))
 import EVM.Solvers (SolverGroup)
-import EVM.SymExec (abstractVM, mkCalldata, verifyInputs, VeriOpts(..), checkAssertions)
-import EVM.Types (Addr, Frame(..), FrameState(..), VMType(..), EType(..), Expr(..), word256Bytes, Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), Query(..))
-import qualified EVM.Types (VM(..), Env(..))
-import EVM.Format (formatPartial)
-import Control.Monad.ST (stToIO, RealWorld)
+import EVM.SymExec (mkCalldata, verifyInputs, VeriOpts(..), checkAssertions, subModel, defaultSymbolicValues)
+import EVM.Expr qualified
+import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), Query(..), forceLit)
+import qualified EVM.Types (VM(..))
+import EVM.Format (formatPartialDetailed)
+import Control.Monad.ST (RealWorld)
 import Control.Monad.State.Strict (execState, runStateT)
 
 import Echidna.Types (fromEVM)
@@ -50,31 +49,6 @@ suitableForSymExec m = not $ null m.inputs
   && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs) 
   && not (T.isInfixOf "_no_symexec" m.name)
 
--- | Sets result to Nothing, and sets gas to ()
-vmMakeSymbolic :: W256 -> W256 -> EVM.Types.VM Concrete s -> EVM.Types.VM Symbolic s
-vmMakeSymbolic maxTimestampDiff maxNumberDiff vm
-  = EVM.Types.VM
-  { result         = Nothing
-  , state          = frameStateMakeSymbolic vm.state
-  , frames         = map frameMakeSymbolic vm.frames
-  , env            = vm.env
-  , block          = blockMakeSymbolic vm.block
-  , tx             = vm.tx
-  , logs           = vm.logs
-  , traces         = vm.traces
-  , cache          = vm.cache
-  , burned         = ()
-  , iterations     = vm.iterations
-  , constraints    = addBlockConstraints maxTimestampDiff maxNumberDiff vm.block vm.constraints
-  , config         = vm.config
-  , forks          = vm.forks
-  , currentFork    = vm.currentFork
-  , labels         = vm.labels
-  , osEnv          = vm.osEnv
-  , freshVar       = vm.freshVar
-  , exploreDepth   = 0
-  , keccakPreImgs  = vm.keccakPreImgs
-  }
 
 blockMakeSymbolic :: Block -> Block
 blockMakeSymbolic b
@@ -93,72 +67,21 @@ addBlockConstraints maxTimestampDiff maxNumberDiff block cs =
 senderConstraints :: Set Addr -> [Prop]
 senderConstraints as = [foldr (\a b -> POr b (PEq (SymAddr "caller") (LitAddr a))) (PBool False) $ Set.toList as]
 
-frameStateMakeSymbolic :: FrameState Concrete s -> FrameState Symbolic s
-frameStateMakeSymbolic fs
-  = FrameState
-  { contract     = fs.contract
-  , codeContract = fs.codeContract
-  , code         = fs.code
-  , pc           = fs.pc
-  , stack        = fs.stack
-  , memory       = fs.memory
-  , memorySize   = fs.memorySize
-  , calldata     = fs.calldata
-  , callvalue    = fs.callvalue
-  , caller       = fs.caller
-  , gas          = ()
-  , returndata   = fs.returndata
-  , static       = fs.static
-  , overrideCaller = fs.overrideCaller
-  , resetCaller  = fs.resetCaller
-  }
-
-frameMakeSymbolic :: Frame Concrete s -> Frame Symbolic s
-frameMakeSymbolic fr = Frame { context = fr.context, state = frameStateMakeSymbolic fr.state }
-
--- | Convert a n-bit unsigned integer to a n-bit signed integer.
-uintToInt :: W256 -> Integer
-uintToInt w = fromIntegral (w - 2 ^ (256 :: Int))
-
-modelToTx :: Addr -> Expr EWord -> Expr EWord -> Method -> Set Addr -> Addr -> ProofResult SMTCex String -> TxOrError
-modelToTx dst oldTimestamp oldNumber method senders fallbackSender result =
+modelToTx :: Addr -> Expr EWord -> Expr EWord -> Method -> Set Addr -> Addr -> Expr Buf -> ProofResult SMTCex String -> TxOrError
+modelToTx dst oldTimestamp oldNumber method senders fallbackSender calldata result =
   case result of
     Cex cex ->
       let
-        args = zipWith grabArg (snd <$> method.inputs) ["arg" <> T.pack (show n) | n <- [1..] :: [Int]]
-
-        grabArg t
-          = case t of
-              AbiUIntType _ -> grabNormalArg t
-              AbiIntType _ -> grabNormalArgInt t
-              AbiBoolType -> grabNormalArg t
-              AbiBytesType _ -> grabNormalArg t
-              AbiAddressType -> grabAddressArg
-              AbiArrayType n mt -> grabArrayArg n mt
-              AbiTupleType mt -> grabTupleArg mt
-              _ -> error "Unexpected ABI type in `modelToTx`"
-
-        grabNormalArg argType name
-          = case Map.lookup (Var name) cex.vars of
-              Just w ->
-                decodeAbiValue argType (BS.fromStrict (word256Bytes w))
-              Nothing -> -- put a placeholder
-                decodeAbiValue argType (BS.repeat 0)
-
-        grabNormalArgInt argType name
-          = case Map.lookup (Var name) cex.vars of
-              Just w ->
-                case argType of
-                  AbiIntType n -> AbiInt n (fromIntegral (uintToInt w))
-                  _ -> error "Expected AbiIntType"
-              Nothing -> -- put a placeholder
-                decodeAbiValue argType (BS.repeat 0)
-
-        grabAddressArg name = AbiAddress $ fromMaybe 0 $ Map.lookup (SymAddr name) cex.addrs
-
-        grabArrayArg nElem memberType name = AbiArray nElem memberType $ fromList [grabArg memberType $ name <> "-a-" <> T.pack (show n) | n <- [0..nElem - 1] :: [Int]]
-
-        grabTupleArg memberTypes name = AbiTuple $ fromList [grabArg t $ name <> "-t-" <> T.pack (show n) | (n, t) <- zip ([0..] :: [Int]) (toList memberTypes)]
+        cd = defaultSymbolicValues $ subModel cex calldata
+        types = snd <$> method.inputs
+        argdata = case cd of
+          Right cd' -> Right $ EVM.Expr.drop 4 (EVM.Expr.simplify cd')
+          Left e -> Left e
+        args = case argdata of
+          Right argdata' -> case decodeBuf types argdata' of
+            CAbi v -> v
+            _ -> []
+          Left _ -> []
 
         src_ = fromMaybe 0 $ Map.lookup (SymAddr "caller") cex.addrs
         src = if Set.member src_ senders then src_ else fallbackSender
@@ -222,28 +145,32 @@ getUnknownLogs = mapMaybe (\case
   _ -> Nothing)
 
 exploreMethod :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
-  Method -> SolcContract -> EVM.Types.VM Concrete RealWorld -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> IORef ContractCache -> IORef SlotCache -> m ([TxOrError], PartialsLogs)
+  Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete RealWorld -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> IORef ContractCache -> IORef SlotCache -> m ([TxOrError], PartialsLogs)
 
-exploreMethod method contract vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef = do
-  --liftIO $ putStrLn ("Exploring: " ++ T.unpack method.methodSignature)
-  --pushWorkerEvent undefined
-  calldataSym@(cd, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef = do
+  calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+  let
+    cd = fst calldataSym
   let
     fetcher = cachedOracle contractCacheRef slotCacheRef solvers rpcInfo
     dst = conf.solConf.contractAddr
-    vmSym = abstractVM calldataSym contract.runtimeCode Nothing False
-  vmSym' <- liftIO $ stToIO vmSym
   vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
-  let vm' = vmReset & execState (loadContract (LitAddr dst))
-                    & vmMakeSymbolic conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay
-                    & #constraints %~ (++ constraints ++ (senderConstraints conf.solConf.sender))
-                    & #state % #callvalue .~ TxValue
-                    & #state % #caller .~ SymAddr "caller"
-                    & #state % #calldata .~ cd
-                    & #env % #contracts .~ (Map.union vmSym'.env.contracts vm.env.contracts)
+  let
+    vm' = vmReset & execState (loadContract (LitAddr dst))
+                  & #tx % #isCreate .~ False
+                  & #state % #callvalue .~ TxValue
+                  & #state % #caller .~ SymAddr "caller"
+                  & #state % #calldata .~ cd
+
+    vm'' = symbolify vm'
+        & #block %~ blockMakeSymbolic
+        & #constraints %~ (addBlockConstraints conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay vm'.block)
+        & #constraints %~ (++ constraints ++ senderConstraints conf.solConf.sender)
+
   -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
   -- Doing so might mess up concolic execution.
-  (_, models, partials) <- verifyInputs solvers veriOpts fetcher vm' (Just $ checkAssertions [0x1])
+  (_, models, partials) <- verifyInputs solvers veriOpts fetcher vm'' (Just $ checkAssertions [0x1])
   let results = map fst models
+  let warnData = Just $ WarningData contract sources vm' 
   --liftIO $ mapM_ TIO.putStrLn partials
-  return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender) results, map (formatPartial . fst) partials)
+  return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) partials)