foundry_evm_symbolic/executor/
run.rs

1use super::*;
2use std::cmp::Reverse;
3
4impl SymbolicExecutor {
5    /// Creates a symbolic executor from Foundry's symbolic configuration.
6    ///
7    /// The configured solver command is not executed here. Solver availability is
8    /// checked by [`Self::run`] so construction remains cheap and side-effect free.
9    ///
10    /// The executor owns an isolated solver backend and symbolic world overlay. Create
11    /// a fresh executor when a caller needs independent solver query accounting.
12    pub fn new(config: SymbolicConfig) -> Self {
13        let solver = SmtLibSubprocessSolver::from_config(&config);
14        Self {
15            config,
16            cx: SymCx::new(),
17            solver,
18            deferred_incomplete: None,
19            deadline: None,
20            nested_deferred_mode: DeferredPathMode::Skip,
21            stateless_retry_safe: true,
22        }
23    }
24
25    fn reset_run_state(&mut self, use_wall_clock_deadline: bool) {
26        self.deferred_incomplete = None;
27        self.nested_deferred_mode = DeferredPathMode::Skip;
28        self.stateless_retry_safe = true;
29        self.deadline = if use_wall_clock_deadline {
30            self.config
31                .timeout
32                .filter(|seconds| *seconds > 0)
33                .map(|seconds| Instant::now() + Duration::from_secs(seconds.into()))
34        } else {
35            None
36        };
37    }
38
39    pub(super) fn check_timeout(&self) -> Result<(), SymbolicError> {
40        if let Some(deadline) = self.deadline
41            && Instant::now() >= deadline
42        {
43            return Err(SymbolicError::Timeout(self.config.timeout.unwrap_or_default()));
44        }
45        Ok(())
46    }
47
48    /// Defers an incomplete result until all counterexample-producing modeled paths are explored.
49    pub(super) fn defer_incomplete(&mut self, reason: &'static str) {
50        if self
51            .deferred_incomplete
52            .is_none_or(|reason| reason == DeferredIncomplete::HardArithmetic)
53        {
54            self.deferred_incomplete = Some(DeferredIncomplete::Unsupported(reason));
55        }
56    }
57
58    /// Defers a solver-unknown result while continuing with decidable sibling paths.
59    pub(super) fn defer_solver_unknown(&mut self) {
60        if self
61            .deferred_incomplete
62            .is_none_or(|reason| reason == DeferredIncomplete::HardArithmetic)
63        {
64            self.deferred_incomplete = Some(DeferredIncomplete::SolverUnknown);
65        }
66    }
67
68    /// Defers an incomplete result for a hard-arithmetic branch skipped by nested execution.
69    pub(super) fn defer_hard_arithmetic(&mut self) {
70        self.deferred_incomplete.get_or_insert(DeferredIncomplete::HardArithmetic);
71    }
72
73    pub(super) fn is_sat_with_state(
74        &mut self,
75        state: &PathState,
76        constraints: &[SymBoolExpr],
77    ) -> Result<bool, SymbolicError> {
78        let replayable_storage = state.world.replay_storage_symbols();
79        self.solver.is_sat_with_replayable_storage(&mut self.cx, constraints, &replayable_storage)
80    }
81
82    /// Checks branch feasibility, recording solver-unknown as an incomplete proof path.
83    pub(super) fn branch_is_sat_or_defer(
84        &mut self,
85        state: &PathState,
86        constraints: &[SymBoolExpr],
87    ) -> Result<bool, SymbolicError> {
88        match self.is_sat_with_state(state, constraints) {
89            Ok(feasible) => Ok(feasible),
90            Err(SymbolicError::SolverUnknown) => {
91                self.defer_solver_unknown();
92                Ok(false)
93            }
94            Err(err) => Err(err),
95        }
96    }
97
98    /// Returns any deferred incomplete reason.
99    fn deferred_incomplete(&self) -> Option<(SymbolicStopReason, String)> {
100        match self.deferred_incomplete? {
101            DeferredIncomplete::Unsupported(reason) => Some((
102                SymbolicStopReason::Stuck,
103                format!("unsupported symbolic execution feature: {reason}"),
104            )),
105            DeferredIncomplete::SolverUnknown => {
106                Some((SymbolicStopReason::Timeout, "solver returned unknown".to_string()))
107            }
108            DeferredIncomplete::HardArithmetic => Some((
109                SymbolicStopReason::Timeout,
110                "nested hard arithmetic branch requires deferred SMT solving".to_string(),
111            )),
112        }
113    }
114
115    /// Executes one function symbolically against an already-deployed test contract.
116    ///
117    /// The input executor supplies the deployed bytecode, storage backend, caller, and
118    /// target address established by the normal forge test setup flow. This method
119    /// does not mutate the concrete executor and does not replay failures itself; when
120    /// it returns [`SymbolicRunResult::Counterexample`], callers should replay the
121    /// returned arguments through the concrete executor before reporting the failure.
122    ///
123    /// Unsupported opcodes, unsupported ABI types, missing solver support, and resource
124    /// limit exhaustion are reported as [`SymbolicRunResult::Incomplete`].
125    ///
126    /// Ordinary Solidity `require` reverts prune the current path. Assertion failures,
127    /// forge-std assertion reverts, and DSTest failure signals are reported as
128    /// counterexample candidates when the failing path is satisfiable.
129    pub fn run<FEN: FoundryEvmNetwork>(
130        &mut self,
131        input: SymbolicRunInput<'_, FEN>,
132    ) -> SymbolicRunResult {
133        self.execute_run(input, None)
134    }
135
136    /// Searches for concrete inputs that complete after reaching a requested branch outcome.
137    ///
138    /// Unlike [`Self::run`], this retains replay candidates independently of the proof result, so a
139    /// later unsupported path or resource limit does not discard an input found on an earlier
140    /// completed path. The caller must concretely replay every candidate before using it.
141    pub fn search_branch_target<FEN: FoundryEvmNetwork>(
142        &mut self,
143        input: SymbolicRunInput<'_, FEN>,
144    ) -> SymbolicBranchTargetSearchResult {
145        let mut candidates = Vec::new();
146        if input.branch_target.is_none() {
147            return SymbolicBranchTargetSearchResult {
148                candidates,
149                execution: SymbolicRunResult::Incomplete {
150                    kind: SymbolicStopReason::Error,
151                    reason: "branch target search requires a branch target".to_string(),
152                    stats: SymbolicStats::default(),
153                },
154            };
155        }
156
157        let execution = self.execute_run(input, Some(&mut candidates));
158        if let SymbolicRunResult::Counterexample { args, calldata, .. } = &execution {
159            candidates.insert(
160                0,
161                SymbolicConcreteInput { args: args.clone(), calldata: calldata.clone() },
162            );
163        }
164        SymbolicBranchTargetSearchResult { candidates, execution }
165    }
166
167    fn execute_run<FEN: FoundryEvmNetwork>(
168        &mut self,
169        input: SymbolicRunInput<'_, FEN>,
170        mut branch_candidates: Option<&mut Vec<SymbolicConcreteInput>>,
171    ) -> SymbolicRunResult {
172        self.reset_run_state(false);
173        self.solver.clear_context_caches();
174        self.cx = SymCx::new();
175        if let Err(err) = self.solver.check_available() {
176            return SymbolicRunResult::Incomplete {
177                kind: err.stop_reason(),
178                reason: err.to_string(),
179                stats: SymbolicStats::default(),
180            };
181        }
182
183        let mut completed_paths = 0;
184        let first =
185            match self.run_inner(&input, branch_candidates.as_deref_mut(), &mut completed_paths) {
186                Ok(result) => result,
187                Err(err) => {
188                    return SymbolicRunResult::Incomplete {
189                        kind: err.stop_reason(),
190                        reason: err.to_string(),
191                        stats: self.stats_with_paths(completed_paths),
192                    };
193                }
194            };
195
196        // Preserve the cheap-path priority of the first pass. Only a deterministic stateless
197        // proof retries after nested hard arithmetic was its remaining limitation.
198        let retry_nested_deferred = branch_candidates.is_none()
199            && self.stateless_retry_safe
200            && matches!(self.deferred_incomplete, Some(DeferredIncomplete::HardArithmetic))
201            && matches!(
202                &first,
203                SymbolicRunResult::Incomplete {
204                    kind: SymbolicStopReason::RevertAll | SymbolicStopReason::Timeout,
205                    ..
206                }
207            );
208        if !retry_nested_deferred {
209            return first;
210        }
211
212        if let Err(err) = self.check_timeout() {
213            return SymbolicRunResult::Incomplete {
214                kind: err.stop_reason(),
215                reason: err.to_string(),
216                stats: self.stats_with_paths(completed_paths),
217            };
218        }
219
220        self.deferred_incomplete = None;
221        self.nested_deferred_mode = DeferredPathMode::Yield;
222        let prioritized = match self.run_inner(&input, None, &mut completed_paths) {
223            Ok(result) => result,
224            Err(err) => {
225                return SymbolicRunResult::Incomplete {
226                    kind: err.stop_reason(),
227                    reason: err.to_string(),
228                    stats: self.stats_with_paths(completed_paths),
229                };
230            }
231        };
232        let drain_nested_deferred = self.stateless_retry_safe
233            && matches!(self.deferred_incomplete, Some(DeferredIncomplete::HardArithmetic))
234            && matches!(
235                &prioritized,
236                SymbolicRunResult::Incomplete {
237                    kind: SymbolicStopReason::RevertAll | SymbolicStopReason::Timeout,
238                    ..
239                }
240            );
241        if !drain_nested_deferred {
242            return prioritized;
243        }
244
245        if let Err(err) = self.check_timeout() {
246            return SymbolicRunResult::Incomplete {
247                kind: err.stop_reason(),
248                reason: err.to_string(),
249                stats: self.stats_with_paths(completed_paths),
250            };
251        }
252
253        self.deferred_incomplete = None;
254        self.nested_deferred_mode = DeferredPathMode::Drain;
255        match self.run_inner(&input, None, &mut completed_paths) {
256            Ok(result) => result,
257            Err(err) => SymbolicRunResult::Incomplete {
258                kind: err.stop_reason(),
259                reason: err.to_string(),
260                stats: self.stats_with_paths(completed_paths),
261            },
262        }
263    }
264
265    /// Returns corpus seed indexes that can be modeled by at least one symbolic calldata variant.
266    pub fn modeled_corpus_seed_indexes(
267        config: &SymbolicConfig,
268        function: &Function,
269        corpus_seeds: &[SymbolicConcreteInput],
270    ) -> Result<Vec<usize>, SymbolicError> {
271        let mut cx = SymCx::new();
272        let variants = SymbolicCalldata::variants(function, config, &mut cx)?;
273        let mut modeled = vec![false; corpus_seeds.len()];
274        for calldata in &variants {
275            for (idx, seed) in corpus_seeds.iter().enumerate() {
276                if !modeled[idx] && calldata.seed_model(&mut cx, seed).is_some() {
277                    modeled[idx] = true;
278                }
279            }
280        }
281        Ok(modeled
282            .into_iter()
283            .enumerate()
284            .filter_map(|(idx, modeled)| modeled.then_some(idx))
285            .collect())
286    }
287
288    /// Executes a bounded symbolic invariant call sequence.
289    ///
290    /// Each sequence step chooses from the concrete target functions and senders supplied by
291    /// Foundry's invariant target discovery. Arguments are generated through the same symbolic ABI
292    /// model used by stateless symbolic tests, and the symbolic world state is preserved between
293    /// steps. Returned counterexamples must still be replayed by the caller before reporting.
294    ///
295    /// The configured invariant depth limits the number of target calls explored before the
296    /// invariant is checked. A depth of zero checks only the invariant against setup state.
297    pub fn run_invariant<FEN: FoundryEvmNetwork>(
298        &mut self,
299        input: SymbolicInvariantRunInput<'_, FEN>,
300    ) -> SymbolicInvariantRunResult {
301        self.reset_run_state(true);
302        self.solver.clear_context_caches();
303        self.cx = SymCx::new();
304        if let Err(err) = self.solver.check_available() {
305            return SymbolicInvariantRunResult::Incomplete {
306                kind: err.stop_reason(),
307                reason: err.to_string(),
308                stats: SymbolicStats::default(),
309            };
310        }
311
312        match self.run_invariant_inner(input) {
313            Ok(result) => result,
314            Err(err) => SymbolicInvariantRunResult::Incomplete {
315                kind: err.stop_reason(),
316                reason: err.to_string(),
317                stats: self.solver.stats(),
318            },
319        }
320    }
321
322    /// Searches for invariant-breaking inputs after one symbolic handler call.
323    ///
324    /// This is a best-effort candidate search from a concrete state. Returned candidates are
325    /// unconfirmed until the caller replays them concretely, and an empty result does not prove
326    /// any invariant.
327    pub fn search_invariant_candidates<FEN: FoundryEvmNetwork>(
328        &mut self,
329        input: SymbolicInvariantCandidateInput<'_, FEN>,
330    ) -> SymbolicInvariantCandidateSearchResult {
331        self.reset_run_state(true);
332        self.solver.clear_context_caches();
333        self.cx = SymCx::new();
334        if let Err(error) = self.solver.check_available() {
335            return SymbolicInvariantCandidateSearchResult {
336                candidates: Vec::new(),
337                limitation: Some(error.into()),
338            };
339        }
340
341        let mut candidates = Vec::new();
342        let mut limitation = None;
343        if let Err(error) =
344            self.search_invariant_candidates_inner(&input, &mut candidates, &mut limitation)
345        {
346            limitation = Some(error.into());
347        }
348        // Deferred hard-arithmetic branches are now sent to SMT before candidate search finishes.
349        // Only branches that nested execution could not escalate remain incomplete.
350        if limitation.is_none()
351            && let Some((kind, reason)) = self.deferred_incomplete()
352        {
353            limitation = Some(SymbolicInvariantSearchLimitation { kind, reason });
354        }
355
356        SymbolicInvariantCandidateSearchResult { candidates, limitation }
357    }
358
359    pub(super) fn run_inner<FEN: FoundryEvmNetwork>(
360        &mut self,
361        input: &SymbolicRunInput<'_, FEN>,
362        mut branch_candidates: Option<&mut Vec<SymbolicConcreteInput>>,
363        completed_paths: &mut usize,
364    ) -> Result<SymbolicRunResult, SymbolicError> {
365        let account = input
366            .executor
367            .backend()
368            .basic_ref(input.target)
369            .map_err(|err| SymbolicError::Backend(err.to_string()))?
370            .ok_or(SymbolicError::MissingAccount(input.target))?;
371        let bytecode = account.code.ok_or(SymbolicError::MissingCode(input.target))?;
372        let code = SymCode::from_bytecode(&mut self.cx, &bytecode);
373        let mut roots = Vec::new();
374        for calldata in SymbolicCalldata::variants(input.function, &self.config, &mut self.cx)? {
375            let corpus_seed_models = input
376                .corpus_seeds
377                .iter()
378                .filter_map(|seed| calldata.seed_model(&mut self.cx, seed).map(Arc::new))
379                .collect();
380            let mut root = PathState::new(
381                &mut self.cx,
382                input.target,
383                input.sender,
384                input.value,
385                calldata,
386                input.ffi_enabled,
387            );
388            root.set_corpus_seed_models(corpus_seed_models);
389            root.set_branch_target(input.branch_target);
390            root.apply_executor_env(&mut self.cx, input.executor);
391            root.world.set_storage_layout(self.config.storage_layout);
392            root.world.clear_transaction_scoped_state();
393            roots.push(root);
394        }
395        order_roots_by_corpus_seed_count(&mut roots, self.config.exploration_order);
396        let mut worklist = roots.into_iter().collect::<VecDeque<_>>();
397        let mut deferred_worklist = VecDeque::new();
398        let mut reverted_paths = 0usize;
399        let mut normal_paths = 0usize;
400        let mut success_input = None;
401        let path_limit = self.config.path_width() as usize;
402        let depth_limit = self.config.execution_depth() as usize;
403
404        while let Some(next) = self.pop_next_feasible_path(
405            &mut worklist,
406            &mut deferred_worklist,
407            DeferredPathMode::Drain,
408        )? {
409            let mut state = next.state;
410            if *completed_paths >= path_limit {
411                debug!(
412                    completed_paths = *completed_paths,
413                    path_limit, "symbolic path limit reached"
414                );
415                return Ok(SymbolicRunResult::Incomplete {
416                    kind: SymbolicStopReason::Stuck,
417                    reason: format!("symbolic path limit exceeded ({path_limit})"),
418                    stats: self.stats_with_paths(*completed_paths),
419                });
420            }
421            if std::mem::take(&mut state.pending_storage_hook_revert) {
422                self.collect_branch_candidate(
423                    branch_candidates.as_deref_mut(),
424                    input.function,
425                    &state,
426                )?;
427                *completed_paths += 1;
428                reverted_paths += 1;
429                continue;
430            }
431            let _path_span = trace_span!(
432                "symbolic_path",
433                completed_paths = *completed_paths,
434                worklist_size = worklist.len()
435            )
436            .entered();
437            trace!(
438                completed_paths = *completed_paths,
439                worklist_size = worklist.len(),
440                "exploring symbolic path"
441            );
442
443            loop {
444                self.check_timeout()?;
445                if state.depth >= depth_limit {
446                    debug!(depth = state.depth, depth_limit, "symbolic depth limit reached");
447                    return Ok(SymbolicRunResult::Incomplete {
448                        kind: SymbolicStopReason::Stuck,
449                        reason: format!("symbolic depth limit exceeded ({depth_limit})"),
450                        stats: self.stats_with_paths(*completed_paths),
451                    });
452                }
453                state.depth += 1;
454
455                let outcome = match code.opcode(&mut self.cx, state.pc)? {
456                    Some(op) => {
457                        let _step_span = trace_span!("symbolic_step", pc = state.pc, op).entered();
458                        self.step(
459                            input.executor,
460                            &code,
461                            code.jump_table(),
462                            &mut state,
463                            &mut worklist,
464                            completed_paths,
465                            op,
466                        )?
467                    }
468                    None => StepOutcome::Halt,
469                };
470                match outcome {
471                    StepOutcome::Continue => {}
472                    StepOutcome::AssumeRejected | StepOutcome::Forked => break,
473                    StepOutcome::Revert => {
474                        self.collect_branch_candidate(
475                            branch_candidates.as_deref_mut(),
476                            input.function,
477                            &state,
478                        )?;
479                        *completed_paths += 1;
480                        reverted_paths += 1;
481                        break;
482                    }
483                    StepOutcome::Halt if state.expectations_satisfied() => {
484                        let candidate = self.collect_branch_candidate(
485                            branch_candidates.as_deref_mut(),
486                            input.function,
487                            &state,
488                        )?;
489                        if input.collect_success_input
490                            && state.satisfies_branch_target()
491                            && state.can_materialize_seed()
492                            && success_input.as_ref().is_none_or(|(depth, _)| state.depth > *depth)
493                        {
494                            let input = match candidate {
495                                Some(input) => input,
496                                None => self.materialize_root_input(input.function, &state)?,
497                            };
498                            success_input = Some((state.depth, input));
499                        }
500                        *completed_paths += 1;
501                        normal_paths += 1;
502                        break;
503                    }
504                    StepOutcome::Halt | StepOutcome::ExceptionalHalt | StepOutcome::Failure => {
505                        if !state.satisfies_branch_target() {
506                            *completed_paths += 1;
507                            break;
508                        }
509                        debug!(
510                            constraint_count = state.constraints.len(),
511                            "materializing counterexample from solver model"
512                        );
513                        let SymbolicConcreteInput { args, calldata } =
514                            self.materialize_root_input(input.function, &state)?;
515                        return Ok(SymbolicRunResult::Counterexample {
516                            args,
517                            calldata,
518                            stats: self.stats_with_paths(*completed_paths + 1),
519                        });
520                    }
521                }
522            }
523        }
524
525        if normal_paths == 0 && reverted_paths > 0 {
526            debug!(completed_paths = *completed_paths, "all symbolic paths reverted");
527            return Ok(SymbolicRunResult::Incomplete {
528                kind: SymbolicStopReason::RevertAll,
529                reason: "all symbolic paths reverted".to_string(),
530                stats: self.stats_with_paths(*completed_paths),
531            });
532        }
533
534        if let Some((kind, reason)) = self.deferred_incomplete() {
535            return Ok(SymbolicRunResult::Incomplete {
536                kind,
537                reason,
538                stats: self.stats_with_paths(*completed_paths),
539            });
540        }
541
542        if normal_paths == 0 {
543            return Ok(SymbolicRunResult::Incomplete {
544                kind: SymbolicStopReason::Stuck,
545                reason: "no successful symbolic paths".to_string(),
546                stats: self.stats_with_paths(*completed_paths),
547            });
548        }
549
550        debug!(completed_paths = *completed_paths, "symbolic execution safe");
551        Ok(SymbolicRunResult::Safe {
552            stats: self.stats_with_paths(*completed_paths),
553            success_input: success_input.map(|(_, input)| input),
554        })
555    }
556
557    fn collect_branch_candidate(
558        &mut self,
559        candidates: Option<&mut Vec<SymbolicConcreteInput>>,
560        function: &Function,
561        state: &PathState,
562    ) -> Result<Option<SymbolicConcreteInput>, SymbolicError> {
563        let Some(candidates) = candidates else {
564            return Ok(None);
565        };
566        if !state.satisfies_branch_target() || !state.can_materialize_seed() {
567            return Ok(None);
568        }
569
570        let input = self.materialize_root_input(function, state)?;
571        candidates.push(input.clone());
572        Ok(Some(input))
573    }
574
575    /// Materializes the root call input for `state` from a solver model.
576    fn materialize_root_input(
577        &mut self,
578        function: &Function,
579        state: &PathState,
580    ) -> Result<SymbolicConcreteInput, SymbolicError> {
581        let calldata = state
582            .root_calldata
583            .as_ref()
584            .ok_or(SymbolicError::Unsupported("missing root symbolic calldata"))?;
585        let replayable_storage = state.world.replay_storage_symbols();
586        let model = self.solver.model_with_replayable_storage(
587            &mut self.cx,
588            &state.constraints,
589            &replayable_storage,
590        )?;
591        let args = calldata.model_to_args(&mut self.cx, &model)?;
592        let calldata_bytes = Bytes::from(function.abi_encode_input(&args)?);
593        Ok(SymbolicConcreteInput { args, calldata: calldata_bytes })
594    }
595
596    pub(super) fn run_invariant_inner<FEN: FoundryEvmNetwork>(
597        &mut self,
598        input: SymbolicInvariantRunInput<'_, FEN>,
599    ) -> Result<SymbolicInvariantRunResult, SymbolicError> {
600        if input.targets.is_empty() {
601            return Err(SymbolicError::Unsupported("symbolic invariant has no targets"));
602        }
603
604        let mut senders =
605            if input.senders.is_empty() { vec![input.sender] } else { input.senders.clone() };
606        senders.retain(|sender| !input.excluded_senders.contains(sender));
607        if senders.is_empty() {
608            return Err(SymbolicError::Unsupported("symbolic invariant senders are excluded"));
609        }
610        let after_invariant_for = |steps_len: usize| {
611            (steps_len == input.depth).then_some(input.after_invariant).flatten()
612        };
613        let mut completed_paths = 0usize;
614        let mut initial_state = PathState::empty(
615            &mut self.cx,
616            input.invariant_address,
617            input.sender,
618            input.ffi_enabled,
619        );
620        initial_state.apply_executor_env(&mut self.cx, input.executor);
621        initial_state.world.set_storage_layout(self.config.storage_layout);
622        let initial = SequencePath { state: initial_state, steps: Vec::new() };
623
624        if symbolic_invariant_should_check(0, input.depth, input.check_interval) {
625            for outcome in self.execute_invariant_check(
626                input.executor,
627                initial.state.clone(),
628                input.invariant_address,
629                input.sender,
630                input.invariant,
631                after_invariant_for(0),
632                &mut completed_paths,
633            )? {
634                if outcome.failed {
635                    let (sequence, storage) =
636                        self.materialize_sequence(&initial.steps, &outcome.state)?;
637                    return Ok(SymbolicInvariantRunResult::Counterexample {
638                        kind: SymbolicInvariantCounterexampleKind::Predicate,
639                        sequence,
640                        storage,
641                        stats: self.stats_with_paths(completed_paths),
642                    });
643                }
644            }
645        }
646
647        let path_limit = self.config.path_width() as usize;
648        let mut frontier = vec![initial];
649        for depth in 0..input.depth {
650            self.check_timeout()?;
651            let mut next_frontier = Vec::new();
652            for sequence in frontier {
653                self.check_timeout()?;
654                for (target_idx, target) in input.targets.iter().enumerate() {
655                    for (sender_idx, sender) in senders.iter().copied().enumerate() {
656                        self.check_timeout()?;
657                        let prefix = format!("sequence_{depth}_{target_idx}_{sender_idx}");
658                        let calldatas = SymbolicCalldata::variants_with_prefix(
659                            &target.function,
660                            &self.config,
661                            &mut self.cx,
662                            &prefix,
663                        )?;
664                        for calldata in calldatas {
665                            let step = SequenceStepTemplate {
666                                sender,
667                                address: target.address,
668                                contract_name: target.contract_name.clone(),
669                                function: target.function.clone(),
670                                calldata,
671                            };
672                            let calldata = step.calldata.call_data(&mut self.cx);
673                            let constraints = step.calldata.constraints().to_vec();
674                            let mut call = self.prepare_sequence_call(
675                                input.executor,
676                                sequence.state.clone(),
677                                target.address,
678                                sender,
679                                &target.function,
680                                calldata,
681                                constraints,
682                            )?;
683
684                            while let Some(outcome) = self.execute_sequence_call_next(
685                                input.executor,
686                                &mut call,
687                                &mut completed_paths,
688                            )? {
689                                let mut steps = sequence.steps.clone();
690                                steps.push(step.clone());
691
692                                let post_state = match outcome.status {
693                                    CallStatus::Failure => {
694                                        let (sequence, storage) =
695                                            self.materialize_sequence(&steps, &outcome.state)?;
696                                        return Ok(SymbolicInvariantRunResult::Counterexample {
697                                            kind: SymbolicInvariantCounterexampleKind::Handler,
698                                            sequence,
699                                            storage,
700                                            stats: self.stats_with_paths(completed_paths),
701                                        });
702                                    }
703                                    CallStatus::Revert | CallStatus::ExceptionalHalt => {
704                                        if input.fail_on_revert {
705                                            let (sequence, storage) =
706                                                self.materialize_sequence(&steps, &outcome.state)?;
707                                            return Ok(
708                                                SymbolicInvariantRunResult::Counterexample {
709                                                    kind: SymbolicInvariantCounterexampleKind::Predicate,
710                                                    sequence,
711                                                    storage,
712                                                    stats: self.stats_with_paths(completed_paths),
713                                                },
714                                            );
715                                        }
716                                        // A reverted top-level call cannot change persistent
717                                        // state, but it still consumes one invariant sequence
718                                        // step. Preserve the pre-call world together with the
719                                        // reverted branch constraints so end-only and periodic
720                                        // invariant checks observe the same call schedule as the
721                                        // concrete campaign.
722                                        let mut reverted_state = sequence.state.clone();
723                                        reverted_state
724                                            .take_reverted_top_level_effects(outcome.state);
725                                        reverted_state
726                                    }
727                                    CallStatus::Success => outcome.state,
728                                };
729                                if symbolic_invariant_should_check(
730                                    steps.len(),
731                                    input.depth,
732                                    input.check_interval,
733                                ) {
734                                    for mut invariant_outcome in self.execute_invariant_check(
735                                        input.executor,
736                                        post_state.clone(),
737                                        input.invariant_address,
738                                        input.sender,
739                                        input.invariant,
740                                        after_invariant_for(steps.len()),
741                                        &mut completed_paths,
742                                    )? {
743                                        if invariant_outcome.failed {
744                                            let (sequence, storage) = self.materialize_sequence(
745                                                &steps,
746                                                &invariant_outcome.state,
747                                            )?;
748                                            return Ok(SymbolicInvariantRunResult::Counterexample {
749                                                kind: SymbolicInvariantCounterexampleKind::Predicate,
750                                                sequence,
751                                                storage,
752                                                stats: self.stats_with_paths(completed_paths),
753                                            });
754                                        }
755                                        let mut state = post_state.clone();
756                                        state.take_noncommitting_check_state(
757                                            &mut invariant_outcome.state,
758                                        );
759                                        next_frontier
760                                            .push(SequencePath { state, steps: steps.clone() });
761                                    }
762                                } else {
763                                    next_frontier.push(SequencePath { state: post_state, steps });
764                                }
765
766                                if completed_paths >= path_limit {
767                                    return Ok(SymbolicInvariantRunResult::Incomplete {
768                                        kind: SymbolicStopReason::Stuck,
769                                        reason: format!(
770                                            "symbolic path limit exceeded ({path_limit})"
771                                        ),
772                                        stats: self.stats_with_paths(completed_paths),
773                                    });
774                                }
775                            }
776                        }
777                    }
778                }
779            }
780
781            if next_frontier.is_empty() {
782                break;
783            }
784            frontier = next_frontier;
785        }
786
787        if let Some((kind, reason)) = self.deferred_incomplete() {
788            return Ok(SymbolicInvariantRunResult::Incomplete {
789                kind,
790                reason,
791                stats: self.stats_with_paths(completed_paths),
792            });
793        }
794
795        Ok(SymbolicInvariantRunResult::Safe(self.stats_with_paths(completed_paths)))
796    }
797
798    pub(super) fn stats_with_paths(&self, paths: usize) -> SymbolicStats {
799        let mut stats = self.solver.stats();
800        stats.paths = paths;
801        stats
802    }
803}
804
805fn order_roots_by_corpus_seed_count(roots: &mut [PathState], order: SymbolicExplorationOrder) {
806    let Some((first, rest)) = roots.split_first() else {
807        return;
808    };
809    if rest.iter().all(|root| root.corpus_seed_model_count() == first.corpus_seed_model_count()) {
810        return;
811    }
812
813    match order {
814        SymbolicExplorationOrder::Bfs => {
815            roots.sort_by_key(|root| Reverse(root.corpus_seed_model_count()));
816        }
817        SymbolicExplorationOrder::Dfs => {
818            roots.sort_by_key(PathState::corpus_seed_model_count);
819        }
820    }
821}
822
823const fn symbolic_invariant_should_check(
824    sequence_len: usize,
825    depth: usize,
826    check_interval: u32,
827) -> bool {
828    sequence_len == depth
829        || (check_interval != 0
830            && sequence_len != 0
831            && sequence_len.is_multiple_of(check_interval as usize))
832}
foundry_evm_symbolic/executor/run.rs

foundry_evm_symbolic/executor/
run.rs
