foundry_evm_symbolic/executor/
mod.rs1use super::{abi::*, runtime::*, *};
2
3mod calls;
4mod cheatcodes;
5mod constraints;
6mod create;
7mod invariant;
8mod opcodes;
9mod run;
10
11#[derive(Debug)]
12struct CallOutcome {
13 status: CallStatus,
14 state: PathState,
15}
16
17#[derive(Clone, Copy, Debug, PartialEq, Eq)]
18enum CallStatus {
19 Success,
20 Revert,
21 ExceptionalHalt,
22 Failure,
23}
24
25enum JoinedCallOutcome {
26 Rejected,
27 ExpectedRevert { parent: PathState, child: PathState },
28 Success { parent: PathState, child: PathState },
29 Revert { parent: PathState, child: PathState },
30 ExceptionalHalt(PathState),
31 Failure(PathState),
32}
33
34#[derive(Clone, Copy)]
35enum CallPathKind {
36 External,
37 Sequence,
38}
39
40enum CallPathOpcode {
41 Execute(u8),
42 Halt,
43 Discard,
44}
45
46pub(super) struct FeasiblePath {
47 state: PathState,
48 from_deferred: bool,
49}
50
51#[derive(Debug)]
52struct SequencePath {
53 state: PathState,
54 steps: Vec<SequenceStepTemplate>,
55}
56
57#[derive(Debug)]
58struct SequenceCall {
59 code: SymCode,
60 worklist: VecDeque<PathState>,
61 deferred_worklist: VecDeque<PathState>,
62}
63
64#[derive(Clone, Debug)]
65struct SequenceStepTemplate {
66 sender: Address,
67 address: Address,
68 contract_name: Option<String>,
69 function: Function,
70 calldata: SymbolicCalldata,
71}
72
73#[derive(Debug)]
74struct InvariantCheckOutcome {
75 failed: bool,
76 state: PathState,
77}
78
79impl SymbolicExecutor {
80 pub(super) fn pop_next_path(&self, paths: &mut VecDeque<PathState>) -> Option<PathState> {
81 match self.config.exploration_order {
82 SymbolicExplorationOrder::Bfs => paths.pop_front(),
83 SymbolicExplorationOrder::Dfs => paths.pop_back(),
84 }
85 }
86
87 pub(super) fn pop_next_feasible_path(
88 &mut self,
89 paths: &mut VecDeque<PathState>,
90 deferred_paths: &mut VecDeque<PathState>,
91 deferred_mode: DeferredPathMode,
92 ) -> Result<Option<FeasiblePath>, SymbolicError> {
93 loop {
94 while let Some(mut state) = self.pop_next_path(paths) {
95 if state.take_deferred_feasibility_check() {
96 let replayable_storage = state.world.replay_storage_symbols();
97 match self.solver.branch_feasibility_with_replayable_storage(
98 &mut self.cx,
99 &state.constraints,
100 &replayable_storage,
101 ) {
102 Ok(BranchFeasibility::Sat) => {}
103 Ok(BranchFeasibility::Unsat) => continue,
104 Ok(BranchFeasibility::NeedsSolver) => {
105 if matches!(deferred_mode, DeferredPathMode::Skip) {
106 self.defer_hard_arithmetic();
107 continue;
108 }
109 trace!("queued hard arithmetic branch for deferred SMT solving");
110 deferred_paths.push_back(state);
111 continue;
112 }
113 Err(SymbolicError::SolverUnknown) => {
114 self.defer_solver_unknown();
115 continue;
116 }
117 Err(err) => return Err(err),
118 }
119 }
120 return Ok(Some(FeasiblePath { state, from_deferred: false }));
121 }
122
123 let Some(state) = self.pop_next_path(deferred_paths) else {
124 return Ok(None);
125 };
126 if self.deadline.is_none() {
127 self.deadline = self
128 .config
129 .timeout
130 .filter(|seconds| *seconds > 0)
131 .map(|seconds| Instant::now() + Duration::from_secs(seconds.into()));
132 }
133 self.check_timeout()?;
134 trace!("escalating deferred hard arithmetic branch to SMT solver");
135 match self.is_sat_with_state(&state, &state.constraints) {
136 Ok(true) => return Ok(Some(FeasiblePath { state, from_deferred: true })),
137 Ok(false) => {}
138 Err(SymbolicError::SolverUnknown) => self.defer_solver_unknown(),
139 Err(err) => return Err(err),
140 }
141 }
142 }
143
144 fn join_call_outcome(
145 &mut self,
146 state: &PathState,
147 mut outcome: CallOutcome,
148 reverter: Address,
149 ) -> Result<JoinedCallOutcome, SymbolicError> {
150 let mut parent = state.clone();
151 parent.take_call_outcome_state(&mut outcome.state);
152
153 if let Some(assumption) = parent.assume_no_revert_next_call.take()
154 && matches!(outcome.status, CallStatus::Revert)
155 && self.assume_no_revert_rejects(
156 &mut parent,
157 &assumption,
158 reverter,
159 &outcome.state.frame.return_data,
160 )?
161 {
162 return Ok(JoinedCallOutcome::Rejected);
163 }
164
165 if let Some(mut expected) = parent.expected_revert.clone() {
166 match outcome.status {
167 CallStatus::Success => return Ok(JoinedCallOutcome::Failure(parent)),
168 CallStatus::Revert | CallStatus::ExceptionalHalt | CallStatus::Failure => {
169 if !self.expected_revert_matches(
170 &mut parent,
171 &expected,
172 reverter,
173 &outcome.state.frame.return_data,
174 )? {
175 return Ok(JoinedCallOutcome::Failure(parent));
176 }
177 if expected.consume_one() {
178 parent.expected_revert = None;
179 } else {
180 parent.expected_revert = Some(expected);
181 }
182 return Ok(JoinedCallOutcome::ExpectedRevert { parent, child: outcome.state });
183 }
184 }
185 }
186
187 Ok(match outcome.status {
188 CallStatus::Success => JoinedCallOutcome::Success { parent, child: outcome.state },
189 CallStatus::Revert => JoinedCallOutcome::Revert { parent, child: outcome.state },
190 CallStatus::ExceptionalHalt => JoinedCallOutcome::ExceptionalHalt(parent),
191 CallStatus::Failure => JoinedCallOutcome::Failure(parent),
192 })
193 }
194
195 fn resume_parent_paths(
196 &self,
197 state: &mut PathState,
198 worklist: &mut VecDeque<PathState>,
199 mut parents: VecDeque<PathState>,
200 ) -> StepOutcome {
201 let Some(first) = self.pop_next_path(&mut parents) else {
202 return StepOutcome::AssumeRejected;
203 };
204 *state = first;
205 worklist.extend(parents);
206 StepOutcome::Continue
207 }
208
209 fn execute_call_path_batch<FEN: FoundryEvmNetwork>(
210 &mut self,
211 executor: &Executor<FEN>,
212 code: &SymCode,
213 worklist: &mut VecDeque<PathState>,
214 deferred_worklist: &mut VecDeque<PathState>,
215 completed_paths: &mut usize,
216 kind: CallPathKind,
217 ) -> Result<Vec<CallOutcome>, SymbolicError> {
218 let mut outcomes = Vec::new();
219 let mut outcomes_before_deferred = None;
220 let path_limit = self.config.path_width() as usize;
221 let depth_limit = self.config.execution_depth() as usize;
222
223 loop {
224 if matches!(kind, CallPathKind::Sequence) && !outcomes.is_empty() {
227 break;
228 }
229 if matches!(kind, CallPathKind::External)
230 && matches!(self.nested_deferred_mode, DeferredPathMode::Yield)
231 && outcomes_before_deferred.is_some_and(|count| outcomes.len() > count)
232 {
233 if !worklist.is_empty() || !deferred_worklist.is_empty() {
234 self.defer_hard_arithmetic();
235 }
236 break;
237 }
238 let deferred_mode = match kind {
239 CallPathKind::Sequence => DeferredPathMode::Drain,
240 CallPathKind::External => self.nested_deferred_mode,
241 };
242 let Some(next) =
243 self.pop_next_feasible_path(worklist, deferred_worklist, deferred_mode)?
244 else {
245 break;
246 };
247 if next.from_deferred
248 && matches!(kind, CallPathKind::External)
249 && matches!(deferred_mode, DeferredPathMode::Yield)
250 {
251 outcomes_before_deferred = Some(outcomes.len());
252 }
253 let mut state = next.state;
254 if *completed_paths >= path_limit {
255 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
256 }
257 if std::mem::take(&mut state.pending_storage_hook_revert) {
258 *completed_paths += 1;
259 outcomes.push(CallOutcome { status: CallStatus::Revert, state });
260 continue;
261 }
262 let _path_span = matches!(kind, CallPathKind::Sequence).then(|| {
263 trace_span!("symbolic_path", completed_paths, worklist_size = worklist.len())
264 .entered()
265 });
266 if matches!(kind, CallPathKind::Sequence) {
267 trace!(completed_paths, worklist_size = worklist.len(), "exploring symbolic path");
268 }
269
270 loop {
271 self.check_timeout()?;
272 if state.depth >= depth_limit {
273 return Err(SymbolicError::Unsupported("symbolic depth limit exceeded"));
274 }
275 state.depth += 1;
276
277 let op = match kind {
278 CallPathKind::Sequence => match code.opcode(&mut self.cx, state.pc)? {
279 Some(op) => CallPathOpcode::Execute(op),
280 None => CallPathOpcode::Halt,
281 },
282 CallPathKind::External => match code.guarded_opcode(&mut self.cx, state.pc)? {
283 GuardedOpcode::End => CallPathOpcode::Halt,
284 GuardedOpcode::Concrete(op) => CallPathOpcode::Execute(op),
285 GuardedOpcode::SymbolicSize { condition, opcode } => {
286 let mut in_bounds_constraints = state.constraints.clone();
287 in_bounds_constraints.push(condition.clone());
288 let in_bounds_sat =
289 self.is_sat_with_state(&state, &in_bounds_constraints)?;
290
291 let mut out_of_bounds_constraints = state.constraints.clone();
292 out_of_bounds_constraints.push(condition.not(&mut self.cx));
293 if self.is_sat_with_state(&state, &out_of_bounds_constraints)? {
294 if *completed_paths >= path_limit {
295 return Err(SymbolicError::Unsupported(
296 "symbolic path limit exceeded",
297 ));
298 }
299 let mut halted = state.clone();
300 halted.constraints = out_of_bounds_constraints;
301 *completed_paths += 1;
302 let status = self.successful_call_status(kind, &halted);
303 outcomes.push(CallOutcome { status, state: halted });
304 }
305
306 if in_bounds_sat {
307 state.constraints = in_bounds_constraints;
308 CallPathOpcode::Execute(opcode)
309 } else {
310 CallPathOpcode::Discard
311 }
312 }
313 },
314 };
315 let op = match op {
316 CallPathOpcode::Execute(op) => op,
317 CallPathOpcode::Halt => {
318 if *completed_paths >= path_limit {
319 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
320 }
321 *completed_paths += 1;
322 let status = self.successful_call_status(kind, &state);
323 outcomes.push(CallOutcome { status, state });
324 break;
325 }
326 CallPathOpcode::Discard => break,
327 };
328
329 let _step_span = matches!(kind, CallPathKind::Sequence)
330 .then(|| trace_span!("symbolic_step", pc = state.pc, op).entered());
331 match self.step(
332 executor,
333 code,
334 code.jump_table(),
335 &mut state,
336 &mut *worklist,
337 completed_paths,
338 op,
339 )? {
340 StepOutcome::Continue => {}
341 StepOutcome::Halt => {
342 if *completed_paths >= path_limit {
343 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
344 }
345 *completed_paths += 1;
346 let status = self.successful_call_status(kind, &state);
347 outcomes.push(CallOutcome { status, state });
348 break;
349 }
350 StepOutcome::Revert => {
351 if *completed_paths >= path_limit {
352 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
353 }
354 *completed_paths += 1;
355 outcomes.push(CallOutcome { status: CallStatus::Revert, state });
356 break;
357 }
358 StepOutcome::ExceptionalHalt => {
359 if *completed_paths >= path_limit {
360 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
361 }
362 *completed_paths += 1;
363 outcomes.push(CallOutcome { status: CallStatus::ExceptionalHalt, state });
364 break;
365 }
366 StepOutcome::Failure => {
367 if *completed_paths >= path_limit {
368 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
369 }
370 *completed_paths += 1;
371 outcomes.push(CallOutcome { status: CallStatus::Failure, state });
372 break;
373 }
374 StepOutcome::AssumeRejected | StepOutcome::Forked => break,
375 }
376 }
377 }
378
379 Ok(outcomes)
380 }
381
382 fn successful_call_status(&self, kind: CallPathKind, state: &PathState) -> CallStatus {
383 if matches!(kind, CallPathKind::External) || state.expectations_satisfied() {
384 CallStatus::Success
385 } else {
386 CallStatus::Failure
387 }
388 }
389}