|
| 1 | +{-# LANGUAGE DataKinds #-} |
| 2 | +{-# LANGUAGE ScopedTypeVariables #-} |
| 3 | + |
| 4 | +-- | State merging for symbolic execution |
| 5 | +-- |
| 6 | +-- This module provides functions for merging execution paths during symbolic |
| 7 | +-- execution. Instead of forking on every JUMPI, we can speculatively execute |
| 8 | +-- both paths and merge them using ITE (If-Then-Else) expressions when: |
| 9 | +-- |
| 10 | +-- 1. Both paths converge to the same PC (forward jump pattern) |
| 11 | +-- 2. Neither path has side effects (storage, memory, logs unchanged) |
| 12 | +-- 3. Both paths have the same stack depth |
| 13 | +-- |
| 14 | +-- This reduces path explosion from 2^N to linear in many common patterns. |
| 15 | + |
| 16 | +module EVM.Merge |
| 17 | + ( tryMergeForwardJump |
| 18 | + ) where |
| 19 | + |
| 20 | +import Control.Monad (when) |
| 21 | +import Control.Monad.State.Strict (get, put) |
| 22 | +import Debug.Trace (traceM) |
| 23 | +import Optics.Core |
| 24 | +import Optics.State |
| 25 | + |
| 26 | +import EVM.Effects (Config(..)) |
| 27 | +import EVM.Expr qualified as Expr |
| 28 | +import EVM.Types |
| 29 | + |
| 30 | +-- | Execute instructions speculatively until target PC is reached or |
| 31 | +-- we hit budget limit/SMT query/RPC call/revert/error. |
| 32 | +speculateLoopOuter |
| 33 | + :: Config |
| 34 | + -> EVM Symbolic () -- ^ Single-step executor |
| 35 | + -> Int -- ^ Target PC |
| 36 | + -> EVM Symbolic (Maybe (VM Symbolic)) |
| 37 | +speculateLoopOuter conf exec1Step targetPC = do |
| 38 | + -- Initialize merge state for this speculation |
| 39 | + let budget = conf.mergeMaxBudget |
| 40 | + modifying #mergeState $ \ms -> ms { msActive = True , msRemainingBudget = budget } |
| 41 | + res <- speculateLoop conf exec1Step targetPC |
| 42 | + -- Reset merge state |
| 43 | + assign #mergeState defaultMergeState |
| 44 | + pure res |
| 45 | + |
| 46 | +-- | Inner loop for speculative execution with budget tracking |
| 47 | +speculateLoop |
| 48 | + :: Config |
| 49 | + -> EVM Symbolic () -- ^ Single-step executor |
| 50 | + -> Int -- ^ Target PC |
| 51 | + -> EVM Symbolic (Maybe (VM Symbolic)) |
| 52 | +speculateLoop conf exec1Step targetPC = do |
| 53 | + ms <- use #mergeState |
| 54 | + if ms.msRemainingBudget <= 0 |
| 55 | + then pure Nothing -- Budget exhausted |
| 56 | + else do |
| 57 | + pc <- use (#state % #pc) |
| 58 | + result <- use #result |
| 59 | + case result of |
| 60 | + Just _ -> pure Nothing -- Hit RPC call/revert/SMT query/etc. |
| 61 | + Nothing |
| 62 | + | pc == targetPC -> Just <$> get -- Reached target |
| 63 | + | otherwise -> do |
| 64 | + -- Decrement budget and execute one instruction |
| 65 | + modifying #mergeState $ \s -> s { msRemainingBudget = subtract 1 s.msRemainingBudget } |
| 66 | + exec1Step |
| 67 | + speculateLoop conf exec1Step targetPC |
| 68 | + |
| 69 | +-- | Try to merge a forward jump (skip block pattern) for Symbolic execution |
| 70 | +-- Returns True if merge succeeded, False if we should fall back to forking |
| 71 | +-- SOUNDNESS: Both paths (jump and fall-through) must converge to the same PC, |
| 72 | +-- have the same stack depth, and have no side effects. Only then can we merge. |
| 73 | +tryMergeForwardJump |
| 74 | + :: Config |
| 75 | + -> EVM Symbolic () -- ^ Single-step executor |
| 76 | + -> Int -- ^ Current PC |
| 77 | + -> Int -- ^ Jump target PC |
| 78 | + -> Expr EWord -- ^ Branch condition |
| 79 | + -> [Expr EWord] -- ^ Stack after popping JUMPI args |
| 80 | + -> EVM Symbolic Bool |
| 81 | +tryMergeForwardJump conf exec1Step currentPC jumpTarget cond stackAfterPop = do |
| 82 | + -- Only handle forward jumps (skip block pattern) |
| 83 | + if jumpTarget <= currentPC |
| 84 | + then pure False -- Not a forward jump |
| 85 | + else do |
| 86 | + vm0 <- get |
| 87 | + |
| 88 | + -- Skip merge if memory is mutable (ConcreteMemory) |
| 89 | + case vm0.state.memory of |
| 90 | + ConcreteMemory _ -> pure False |
| 91 | + SymbolicMemory _ -> do |
| 92 | + -- True branch (jump taken): Just sets PC to target, no execution needed |
| 93 | + let trueStack = stackAfterPop -- Stack after popping JUMPI args |
| 94 | + |
| 95 | + -- False branch (fall through): Execute until we reach jump target |
| 96 | + assign' (#state % #stack) stackAfterPop |
| 97 | + modifying' (#state % #pc) (+ 1) -- Move past JUMPI |
| 98 | + maybeVmFalse <- speculateLoopOuter conf exec1Step jumpTarget |
| 99 | + |
| 100 | + case maybeVmFalse of |
| 101 | + Nothing -> put vm0 >> pure False -- can't merge: EVM error, SMT/RPC query, over-budget |
| 102 | + Just vmFalse -> do |
| 103 | + let falseStack = vmFalse.state.stack |
| 104 | + soundnessOK = checkNoSideEffects vm0 vmFalse |
| 105 | + |
| 106 | + -- Check merge conditions: same stack depth AND no side effects |
| 107 | + if length trueStack == length falseStack && soundnessOK |
| 108 | + then do |
| 109 | + -- Merge stacks using ITE expressions, simplifying to prevent growth |
| 110 | + let condSimp = Expr.simplify cond |
| 111 | + mergeExpr t f = Expr.simplify $ ITE condSimp t f |
| 112 | + mergedStack = zipWith mergeExpr trueStack falseStack |
| 113 | + -- Use vm0 as base and update only PC and stack |
| 114 | + when conf.debug $ traceM $ |
| 115 | + "Merged forward jump to PC: " <> show jumpTarget <> " from PC: " <> show currentPC |
| 116 | + put vm0 |
| 117 | + assign (#state % #pc) jumpTarget |
| 118 | + assign (#state % #stack) mergedStack |
| 119 | + assign #result Nothing |
| 120 | + assign (#mergeState % #msActive) False |
| 121 | + pure True |
| 122 | + else put vm0 >> pure False -- can't merge: stack depth or state differs |
| 123 | + |
| 124 | +-- | Check that execution had no side effects (storage, memory, logs, etc.) |
| 125 | +checkNoSideEffects :: VM Symbolic -> VM Symbolic -> Bool |
| 126 | +checkNoSideEffects vm0 vmAfter = |
| 127 | + let memoryUnchanged = case (vm0.state.memory, vmAfter.state.memory) of |
| 128 | + (SymbolicMemory m1, SymbolicMemory m2) -> m1 == m2 |
| 129 | + _ -> False |
| 130 | + memorySizeUnchanged = vm0.state.memorySize == vmAfter.state.memorySize |
| 131 | + returndataUnchanged = vm0.state.returndata == vmAfter.state.returndata |
| 132 | + storageUnchanged = vm0.env.contracts == vmAfter.env.contracts |
| 133 | + logsUnchanged = vm0.logs == vmAfter.logs |
| 134 | + constraintsUnchanged = vm0.constraints == vmAfter.constraints |
| 135 | + keccakUnchanged = vm0.keccakPreImgs == vmAfter.keccakPreImgs |
| 136 | + freshVarUnchanged = vm0.freshVar == vmAfter.freshVar |
| 137 | + framesUnchanged = length vm0.frames == length vmAfter.frames |
| 138 | + subStateUnchanged = vm0.tx.subState == vmAfter.tx.subState |
| 139 | + in memoryUnchanged && memorySizeUnchanged && returndataUnchanged |
| 140 | + && storageUnchanged && logsUnchanged && constraintsUnchanged |
| 141 | + && keccakUnchanged && freshVarUnchanged |
| 142 | + && framesUnchanged && subStateUnchanged |
0 commit comments