Allow to properly use symbolic execution in property mode

lib/Echidna/Config.hs

@@ -111,6 +111,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "symExecMaxIters"    ..!= defaultSymExecMaxIters
         <*> v ..:? "symExecAskSMTIters" ..!= defaultSymExecAskSMTIters
         <*> v ..:? "symExecMaxExplore"  ..!= defaultSymExecMaxExplore
+        <*> v ..:? "symExecSeqSamples"   ..!= defaultSymExecSeqSamples
         where
         smtSolver = v ..:? "symExecSMTSolver" >>= \case
           Just ("z3" :: String)  -> pure Z3

lib/Echidna/SymExec/Common.hs

@@ -16,7 +16,7 @@ import Data.Set qualified as Set
 import Data.Text qualified as T
 import Optics.Core ((.~), (%), (%~))
 
-import EVM (loadContract, resetState, symbolify)
+import EVM (initialContract, loadContract, resetState, symbolify)
 import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..))
 import EVM.Effects (TTY, ReadConfig)
 import EVM.Expr qualified
@@ -25,7 +25,7 @@ import EVM.Format (formatPartialDetailed)
 import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..))
 import EVM.Solvers (SolverGroup)
 import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
-import EVM.Types (Addr, VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
+import EVM.Types (Addr, Contract(..), VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
 import qualified EVM.Types (VM(..))
 
 import Echidna.Test (isFoundryMode)
@@ -83,7 +83,8 @@ extractErrors = mapMaybe (\case
   _ -> Nothing)
 
 suitableForSymExec :: Method -> Bool
-suitableForSymExec m = not $ null m.inputs
+suitableForSymExec m =
+  not (null m.inputs)
   && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs)
   && not (T.isInfixOf "_no_symexec" m.name)
 
@@ -166,8 +167,14 @@ getUnknownLogs = mapMaybe (\case
 
 exploreMethod :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
   Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
+exploreMethod = exploreMethodWith Nothing
 
-exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
+-- | Like 'exploreMethod' but accepts a custom postcondition. When 'Nothing',
+-- uses the default assertion-checking postcondition.
+exploreMethodWith :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
+  Maybe Postcondition -> Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
+
+exploreMethodWith customPost method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
   calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
   let
     cd = fst calldataSym
@@ -190,7 +197,98 @@ exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers r
   -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
   -- Doing so might mess up concolic execution.
   let foundry = isFoundryMode conf.solConf.testMode
-  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1] foundry) Nothing
+  let postcondition = case customPost of
+        Just p  -> p
+        Nothing -> checkAssertions [0x1] foundry
+  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' postcondition Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
   --liftIO $ mapM_ print partials
   return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) partials)
+
+-- | Convert a symbolic contract expression (from a Success leaf) to a
+-- concrete Contract value suitable for use in a VM's env.contracts map.
+fromEContract :: Expr EContract -> Contract
+fromEContract (C code storage tStorage balance nonce) =
+  initialContract code
+    & #storage .~ storage
+    & #tStorage .~ tStorage
+    & #balance .~ balance
+    & #nonce .~ nonce
+fromEContract _ = error "fromEContract: unexpected non-C expression"
+
+-- | Two-phase symbolic execution.
+--
+-- Phase 1: Symbolically execute a state-changing method with a trivially-true
+-- postcondition (no solver calls). This collects all reachable Success leaves,
+-- each containing symbolic contract states and path constraints.
+--
+-- Phase 2: For each Success leaf and each target method, reconstruct a VM
+-- with the symbolic contract states, execute the target, and check the given
+-- postcondition. The solver finds concrete values for phase 1's symbolic
+-- variables (calldata, caller, etc.) that cause a violation.
+exploreMethodTwoPhase :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
+  Postcondition -> Expr EAddr -> (Method -> m ()) -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
+
+exploreMethodTwoPhase phase2Post phase2Caller logTarget method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
+  -- Phase 1: Execute state-changing method symbolically
+  calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+  let
+    cd = fst calldataSym
+    fetcher = Fetch.oracle solvers (Just session) rpcInfo
+    dst = conf.solConf.contractAddr
+  vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
+  let
+    vm' = vmReset & execState (loadContract (LitAddr dst))
+                  & #tx % #isCreate .~ False
+                  & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else 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)
+
+  -- Phase 1: PBool True postcondition → no solver calls, all Success paths return Qed
+  (phase1Models, phase1Partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (\_ _ -> PBool True) Nothing
+
+  -- Extract Success leaves with their path constraints and symbolic contract states
+  let successLeaves = [(props, contracts) | (_, Success props _ _ contracts) <- phase1Models]
+
+  -- Phase 2: For each Success leaf, check each target method
+  allResults <- concat <$> mapM (checkLeaf fetcher dst vm cd) successLeaves
+
+  let allPartialLogs = map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) phase1Partials
+  return (allResults, allPartialLogs)
+
+  where
+
+  -- | Phase 2 for a single Success leaf: check all target methods
+  checkLeaf fetcher dst vm0 cd (leafConstraints, leafContracts) = do
+    let convertedContracts = Map.map fromEContract leafContracts
+    concat <$> mapM (checkTarget fetcher dst vm0 cd convertedContracts leafConstraints) targetMethods
+
+  -- | Phase 2 for a single (leaf, target) pair
+  checkTarget fetcher dst vm0 cd convertedContracts leafConstraints targetMethod = do
+    logTarget targetMethod
+    vmReset2 <- liftIO $ snd <$> runStateT (fromEVM resetState) vm0
+    let
+      targetCd = ConcreteBuf (selector targetMethod.methodSignature)
+      -- Replace contracts with phase 1's symbolic state, keeping originals as fallback
+      vm2 = vmReset2 & #env % #contracts %~ Map.union convertedContracts
+                     & execState (loadContract (LitAddr dst))
+                     & #tx % #isCreate .~ False
+                     & #state % #callvalue .~ Lit 0
+                     & #state % #caller .~ phase2Caller
+                     & #state % #calldata .~ targetCd
+      -- Carry over phase 1's path constraints so the solver must satisfy both phases
+      -- Reset exploration state so phase 2 gets fresh budget
+      vm2' = symbolify vm2
+          & #constraints .~ leafConstraints
+          & #iterations .~ mempty
+          & #pathsVisited .~ mempty
+          & #exploreDepth .~ 0
+
+    (phase2Models, _) <- verifyInputsWithHandler solvers veriOpts fetcher vm2' phase2Post Nothing
+    let results2 = filter (\(r, _) -> not (isQed r)) phase2Models & map fst
+    return $ map (modelToTx dst vm0.block.timestamp vm0.block.number method conf.solConf.sender defaultSender cd) results2

lib/Echidna/SymExec/Exploration.hs

@@ -8,7 +8,7 @@ import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO)
-import Control.Monad.State.Strict (MonadState)
+import Control.Monad.State.Strict (MonadState, gets)
 import Data.List.NonEmpty (fromList)
 import Data.Map qualified as Map
 import Data.Maybe (fromJust)
@@ -20,19 +20,22 @@ import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
 import EVM.Fetch (RpcInfo(..))
 import EVM.Solidity (SolcContract(..), Method(..))
 import EVM.Solvers (defMemLimit, withSolvers)
-import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..))
-import EVM.Types (VMType(..))
+import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), Postcondition)
+import EVM.Types (VMType(..), EType(..), Expr(..))
 import qualified EVM.Types (VM(..))
 
-import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, rpcFetcher, TxOrError(..), PartialsLogs)
-import Echidna.Types.Campaign (CampaignConf(..), WorkerState)
+import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs)
+import Echidna.SymExec.Property (checkPropertyReturn)
+import Echidna.Test (isFoundryMode)
+import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..))
 import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..))
+import Echidna.Types.Test (TestConf(..))
 import Echidna.Types.Random (rElem)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..))
-import Echidna.Types.Worker (WorkerEvent(..))
+import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..))
 import Echidna.Types.World (World(..))
-import Echidna.Worker (pushWorkerEvent)
+import Echidna.Worker (pushWorkerEvent, pushCampaignEvent)
 
 -- | Uses symbolic execution to find transactions which would increase coverage.
 -- Spawns a new thread; returns its thread ID as the first return value.
@@ -102,7 +105,7 @@ exploreContract contract method vm = do
   let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
   let runtimeEnv = defaultEnv { config = hevmConfig }
   session <- asks (.fetchSession)
-  pushWorkerEvent $ SymExecLog ("Exploring " <> (show method.name))
+  pushWorkerEvent $ SymExecLog ("Exploring " <> unpack method.methodSignature)
   liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
     threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
       -- For now, we will be exploring a single method at a time.
@@ -116,3 +119,58 @@ exploreContract contract method vm = do
 
   threadId <- liftIO $ takeMVar threadIdChan
   pure (threadId, resultChan)
+
+-- | Two-phase exploration for assertion mode (symbolic caller).
+exploreContractTwoPhase :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContractTwoPhase contract method targetMethods vm baseLabel = do
+  conf <- asks (.cfg)
+  let isFoundry = isFoundryMode conf.solConf.testMode
+  exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) (SymAddr "caller") contract method targetMethods vm baseLabel
+
+-- | Two-phase exploration for property mode (concrete test sender).
+exploreContractTwoPhaseProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContractTwoPhaseProperty contract method targetMethods vm baseLabel = do
+  conf <- asks (.cfg)
+  let dst = conf.solConf.contractAddr
+      propertySender = LitAddr (conf.testConf.testSender dst)
+  exploreContractTwoPhaseWith checkPropertyReturn propertySender contract method targetMethods vm baseLabel
+
+-- | Two-phase exploration parameterized by postcondition and phase 2 caller.
+exploreContractTwoPhaseWith :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => Postcondition -> Expr EAddr -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContractTwoPhaseWith postcondition phase2Caller contract method targetMethods vm baseLabel = do
+  env <- ask
+  wid <- gets (.workerId)
+  let conf = env.cfg
+  dappInfo <- asks (.dapp)
+  let
+    timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = Just conf.campaignConf.symExecMaxIters
+    maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore)
+    askSmtIters = conf.campaignConf.symExecAskSMTIters
+    rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock))
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- liftIO newEmptyMVar
+  doneChan <- liftIO newEmptyMVar
+  resultChan <- liftIO newEmptyMVar
+  let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
+  let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased }
+  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False }
+  let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo }
+  let runtimeEnv = defaultEnv { config = hevmConfig }
+  session <- asks (.fetchSession)
+  let methodSig = unpack method.methodSignature
+      logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Two-phase " <> baseLabel <> ": " <> methodSig <> " -> " <> unpack target.methodSignature)))
+  liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
+    threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
+      res <- exploreMethodTwoPhase postcondition phase2Caller logTarget method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session
+      liftIO $ putMVar resultChan res
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- liftIO $ takeMVar threadIdChan
+  pure (threadId, resultChan)