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    /// Returns staged solver portfolio diagnostics collected by this executor.
116    pub fn portfolio_diagnostics(&self) -> Option<PortfolioDiagnostics> {
117        self.solver.portfolio_diagnostics().cloned()
118    }
119
120    /// Defers verbose solver diagnostics until the caller explicitly takes them.
121    pub fn capture_diagnostics(&mut self) {
122        self.solver.capture_diagnostics();
123    }
124
125    /// Returns and clears deferred verbose solver diagnostics.
126    pub fn take_diagnostics(&mut self) -> Option<String> {
127        self.solver.take_diagnostics()
128    }
129
130    /// Registers a callback invoked after each solver query for live progress rendering.
131    pub fn set_query_observer(&mut self, observer: impl Fn(usize) + Send + Sync + 'static) {
132        self.solver.set_query_observer(Some(Box::new(observer)));
133    }
134
135    /// Executes one function symbolically against an already-deployed test contract.
136    ///
137    /// The input executor supplies the deployed bytecode, storage backend, caller, and
138    /// target address established by the normal forge test setup flow. This method
139    /// does not mutate the concrete executor and does not replay failures itself; when
140    /// it returns [`SymbolicRunResult::Counterexample`], callers should replay the
141    /// returned arguments through the concrete executor before reporting the failure.
142    ///
143    /// Unsupported opcodes, unsupported ABI types, missing solver support, and resource
144    /// limit exhaustion are reported as [`SymbolicRunResult::Incomplete`].
145    ///
146    /// Ordinary Solidity `require` reverts prune the current path. Assertion failures,
147    /// forge-std assertion reverts, and DSTest failure signals are reported as
148    /// counterexample candidates when the failing path is satisfiable.
149    pub fn run<FEN: FoundryEvmNetwork>(
150        &mut self,
151        input: SymbolicRunInput<'_, FEN>,
152    ) -> SymbolicRunResult {
153        self.execute_run(input, None)
154    }
155
156    /// Searches for concrete inputs that complete after reaching a requested branch outcome.
157    ///
158    /// Unlike [`Self::run`], this retains replay candidates independently of the proof result, so a
159    /// later unsupported path or resource limit does not discard an input found on an earlier
160    /// completed path. The caller must concretely replay every candidate before using it.
161    pub fn search_branch_target<FEN: FoundryEvmNetwork>(
162        &mut self,
163        input: SymbolicRunInput<'_, FEN>,
164    ) -> SymbolicBranchTargetSearchResult {
165        let mut candidates = Vec::new();
166        if input.branch_target.is_none() {
167            return SymbolicBranchTargetSearchResult {
168                candidates,
169                execution: SymbolicRunResult::Incomplete {
170                    kind: SymbolicStopReason::Error,
171                    reason: "branch target search requires a branch target".to_string(),
172                    stats: SymbolicStats::default(),
173                },
174            };
175        }
176
177        let execution = self.execute_run(input, Some(&mut candidates));
178        if let SymbolicRunResult::Counterexample { args, calldata, .. } = &execution {
179            candidates.insert(
180                0,
181                SymbolicConcreteInput { args: args.clone(), calldata: calldata.clone() },
182            );
183        }
184        SymbolicBranchTargetSearchResult { candidates, execution }
185    }
186
187    fn execute_run<FEN: FoundryEvmNetwork>(
188        &mut self,
189        input: SymbolicRunInput<'_, FEN>,
190        mut branch_candidates: Option<&mut Vec<SymbolicConcreteInput>>,
191    ) -> SymbolicRunResult {
192        self.reset_run_state(false);
193        self.solver.clear_context_caches();
194        self.cx = SymCx::new();
195        if let Err(err) = self.solver.check_available() {
196            return SymbolicRunResult::Incomplete {
197                kind: err.stop_reason(),
198                reason: err.to_string(),
199                stats: SymbolicStats::default(),
200            };
201        }
202
203        let mut completed_paths = 0;
204        let first =
205            match self.run_inner(&input, branch_candidates.as_deref_mut(), &mut completed_paths) {
206                Ok(result) => result,
207                Err(err) => {
208                    return SymbolicRunResult::Incomplete {
209                        kind: err.stop_reason(),
210                        reason: err.to_string(),
211                        stats: self.stats_with_paths(completed_paths),
212                    };
213                }
214            };
215
216        // Preserve the cheap-path priority of the first pass. Only a deterministic stateless
217        // proof retries after nested hard arithmetic was its remaining limitation.
218        let retry_nested_deferred = branch_candidates.is_none()
219            && self.stateless_retry_safe
220            && matches!(self.deferred_incomplete, Some(DeferredIncomplete::HardArithmetic))
221            && matches!(
222                &first,
223                SymbolicRunResult::Incomplete {
224                    kind: SymbolicStopReason::RevertAll | SymbolicStopReason::Timeout,
225                    ..
226                }
227            );
228        if !retry_nested_deferred {
229            return first;
230        }
231
232        if let Err(err) = self.check_timeout() {
233            return SymbolicRunResult::Incomplete {
234                kind: err.stop_reason(),
235                reason: err.to_string(),
236                stats: self.stats_with_paths(completed_paths),
237            };
238        }
239
240        self.deferred_incomplete = None;
241        self.nested_deferred_mode = DeferredPathMode::Yield;
242        let prioritized = match self.run_inner(&input, None, &mut completed_paths) {
243            Ok(result) => result,
244            Err(err) => {
245                return SymbolicRunResult::Incomplete {
246                    kind: err.stop_reason(),
247                    reason: err.to_string(),
248                    stats: self.stats_with_paths(completed_paths),
249                };
250            }
251        };
252        let drain_nested_deferred = self.stateless_retry_safe
253            && matches!(self.deferred_incomplete, Some(DeferredIncomplete::HardArithmetic))
254            && matches!(
255                &prioritized,
256                SymbolicRunResult::Incomplete {
257                    kind: SymbolicStopReason::RevertAll | SymbolicStopReason::Timeout,
258                    ..
259                }
260            );
261        if !drain_nested_deferred {
262            return prioritized;
263        }
264
265        if let Err(err) = self.check_timeout() {
266            return SymbolicRunResult::Incomplete {
267                kind: err.stop_reason(),
268                reason: err.to_string(),
269                stats: self.stats_with_paths(completed_paths),
270            };
271        }
272
273        self.deferred_incomplete = None;
274        self.nested_deferred_mode = DeferredPathMode::Drain;
275        match self.run_inner(&input, None, &mut completed_paths) {
276            Ok(result) => result,
277            Err(err) => SymbolicRunResult::Incomplete {
278                kind: err.stop_reason(),
279                reason: err.to_string(),
280                stats: self.stats_with_paths(completed_paths),
281            },
282        }
283    }
284
285    /// Returns corpus seed indexes that can be modeled by at least one symbolic calldata variant.
286    pub fn modeled_corpus_seed_indexes(
287        config: &SymbolicConfig,
288        function: &Function,
289        corpus_seeds: &[SymbolicConcreteInput],
290    ) -> Result<Vec<usize>, SymbolicError> {
291        let mut cx = SymCx::new();
292        let variants = SymbolicCalldata::variants(function, config, &mut cx)?;
293        let mut modeled = vec![false; corpus_seeds.len()];
294        for calldata in &variants {
295            for (idx, seed) in corpus_seeds.iter().enumerate() {
296                if !modeled[idx] && calldata.seed_model(&mut cx, seed).is_some() {
297                    modeled[idx] = true;
298                }
299            }
300        }
301        Ok(modeled
302            .into_iter()
303            .enumerate()
304            .filter_map(|(idx, modeled)| modeled.then_some(idx))
305            .collect())
306    }
307
308    /// Executes a bounded symbolic invariant call sequence.
309    ///
310    /// Each sequence step chooses from the concrete target functions and senders supplied by
311    /// Foundry's invariant target discovery. Arguments are generated through the same symbolic ABI
312    /// model used by stateless symbolic tests, and the symbolic world state is preserved between
313    /// steps. Returned counterexamples must still be replayed by the caller before reporting.
314    ///
315    /// The configured invariant depth limits the number of target calls explored before the
316    /// invariant is checked. A depth of zero checks only the invariant against setup state.
317    pub fn run_invariant<FEN: FoundryEvmNetwork>(
318        &mut self,
319        input: SymbolicInvariantRunInput<'_, FEN>,
320    ) -> SymbolicInvariantRunResult {
321        self.reset_run_state(true);
322        self.solver.clear_context_caches();
323        self.cx = SymCx::new();
324        if let Err(err) = self.solver.check_available() {
325            return SymbolicInvariantRunResult::Incomplete {
326                kind: err.stop_reason(),
327                reason: err.to_string(),
328                stats: SymbolicStats::default(),
329            };
330        }
331
332        match self.run_invariant_inner(input) {
333            Ok(result) => result,
334            Err(err) => SymbolicInvariantRunResult::Incomplete {
335                kind: err.stop_reason(),
336                reason: err.to_string(),
337                stats: self.solver.stats(),
338            },
339        }
340    }
341
342    /// Searches for invariant-breaking inputs after one symbolic handler call.
343    ///
344    /// This is a best-effort candidate search from a concrete state. Returned candidates are
345    /// unconfirmed until the caller replays them concretely, and an empty result does not prove
346    /// any invariant.
347    pub fn search_invariant_candidates<FEN: FoundryEvmNetwork>(
348        &mut self,
349        input: SymbolicInvariantCandidateInput<'_, FEN>,
350    ) -> SymbolicInvariantCandidateSearchResult {
351        self.reset_run_state(true);
352        self.solver.clear_context_caches();
353        self.cx = SymCx::new();
354        if let Err(error) = self.solver.check_available() {
355            return SymbolicInvariantCandidateSearchResult {
356                candidates: Vec::new(),
357                limitation: Some(error.into()),
358            };
359        }
360
361        let mut candidates = Vec::new();
362        let mut limitation = None;
363        if let Err(error) =
364            self.search_invariant_candidates_inner(&input, &mut candidates, &mut limitation)
365        {
366            limitation.get_or_insert_with(|| error.into());
367        }
368        // Deferred hard-arithmetic branches are now sent to SMT before candidate search finishes.
369        // Only branches that nested execution could not escalate remain incomplete.
370        if limitation.is_none()
371            && let Some((kind, reason)) = self.deferred_incomplete()
372        {
373            limitation = Some(SymbolicInvariantSearchLimitation { kind, reason });
374        }
375
376        SymbolicInvariantCandidateSearchResult { candidates, limitation }
377    }
378
379    pub(super) fn run_inner<FEN: FoundryEvmNetwork>(
380        &mut self,
381        input: &SymbolicRunInput<'_, FEN>,
382        mut branch_candidates: Option<&mut Vec<SymbolicConcreteInput>>,
383        completed_paths: &mut usize,
384    ) -> Result<SymbolicRunResult, SymbolicError> {
385        let account = input
386            .executor
387            .backend()
388            .basic_ref(input.target)
389            .map_err(|err| SymbolicError::Backend(err.to_string()))?
390            .ok_or(SymbolicError::MissingAccount(input.target))?;
391        let bytecode = account.code.ok_or(SymbolicError::MissingCode(input.target))?;
392        let code = SymCode::from_bytecode(&mut self.cx, &bytecode);
393        let mut roots = Vec::new();
394        for calldata in SymbolicCalldata::variants(input.function, &self.config, &mut self.cx)? {
395            let corpus_seed_models = input
396                .corpus_seeds
397                .iter()
398                .filter_map(|seed| calldata.seed_model(&mut self.cx, seed).map(Arc::new))
399                .collect();
400            let mut root = PathState::new(
401                &mut self.cx,
402                input.target,
403                input.sender,
404                input.value,
405                calldata,
406                input.ffi_enabled,
407            );
408            root.set_corpus_seed_models(corpus_seed_models);
409            root.set_branch_target(input.branch_target);
410            root.apply_executor_env(&mut self.cx, input.executor);
411            root.world.set_storage_layout(self.config.storage_layout);
412            root.world.clear_transaction_scoped_state();
413            roots.push(root);
414        }
415        order_roots_by_corpus_seed_count(&mut roots, self.config.exploration_order);
416        let mut worklist = roots.into_iter().collect::<VecDeque<_>>();
417        let mut deferred_worklist = VecDeque::new();
418        let mut reverted_paths = 0usize;
419        let mut normal_paths = 0usize;
420        let mut success_input = None;
421        let path_limit = self.config.path_width() as usize;
422        let depth_limit = self.config.execution_depth() as usize;
423
424        while let Some(next) = self.pop_next_feasible_path(
425            &mut worklist,
426            &mut deferred_worklist,
427            DeferredPathMode::Drain,
428        )? {
429            let mut state = next.state;
430            if *completed_paths >= path_limit {
431                debug!(
432                    completed_paths = *completed_paths,
433                    path_limit, "symbolic path limit reached"
434                );
435                return Ok(SymbolicRunResult::Incomplete {
436                    kind: SymbolicStopReason::Stuck,
437                    reason: format!("symbolic path limit exceeded ({path_limit})"),
438                    stats: self.stats_with_paths(*completed_paths),
439                });
440            }
441            if std::mem::take(&mut state.pending_storage_hook_revert) {
442                self.collect_branch_candidate(
443                    branch_candidates.as_deref_mut(),
444                    input.function,
445                    &state,
446                )?;
447                *completed_paths += 1;
448                reverted_paths += 1;
449                continue;
450            }
451            let _path_span = trace_span!(
452                "symbolic_path",
453                completed_paths = *completed_paths,
454                worklist_size = worklist.len()
455            )
456            .entered();
457            trace!(
458                completed_paths = *completed_paths,
459                worklist_size = worklist.len(),
460                "exploring symbolic path"
461            );
462
463            loop {
464                self.check_timeout()?;
465                if state.depth >= depth_limit {
466                    debug!(depth = state.depth, depth_limit, "symbolic depth limit reached");
467                    return Ok(SymbolicRunResult::Incomplete {
468                        kind: SymbolicStopReason::Stuck,
469                        reason: format!("symbolic depth limit exceeded ({depth_limit})"),
470                        stats: self.stats_with_paths(*completed_paths),
471                    });
472                }
473                state.depth += 1;
474
475                let Some(op) = code.opcode(&mut self.cx, state.pc)? else {
476                    if !state.expectations_satisfied() {
477                        let Some((args, calldata_bytes)) = self
478                            .materialize_stateless_counterexample_if_branch_target_satisfied(
479                                state.root_calldata.as_ref().ok_or_else(|| {
480                                    SymbolicError::Unsupported("missing root symbolic calldata")
481                                })?,
482                                input.function,
483                                &state,
484                            )?
485                        else {
486                            *completed_paths += 1;
487                            break;
488                        };
489                        return Ok(SymbolicRunResult::Counterexample {
490                            args,
491                            calldata: calldata_bytes,
492                            stats: self.stats_with_paths(*completed_paths + 1),
493                        });
494                    }
495                    let candidate = self.collect_branch_candidate(
496                        branch_candidates.as_deref_mut(),
497                        input.function,
498                        &state,
499                    )?;
500                    if input.collect_success_input
501                        && state.satisfies_branch_target()
502                        && state.can_materialize_seed()
503                        && success_input.as_ref().is_none_or(|(depth, _)| state.depth > *depth)
504                    {
505                        let input = match candidate {
506                            Some(input) => input,
507                            None => self.materialize_stateless_input(
508                                state.root_calldata.as_ref().ok_or_else(|| {
509                                    SymbolicError::Unsupported("missing root symbolic calldata")
510                                })?,
511                                input.function,
512                                &state,
513                            )?,
514                        };
515                        success_input = Some((state.depth, input));
516                    }
517                    *completed_paths += 1;
518                    break;
519                };
520
521                let _step_span = trace_span!("symbolic_step", pc = state.pc, op).entered();
522                match self.step(
523                    input.executor,
524                    &code,
525                    code.jump_table(),
526                    &mut state,
527                    &mut worklist,
528                    completed_paths,
529                    op,
530                )? {
531                    StepOutcome::Continue => {}
532                    StepOutcome::Halt => {
533                        if !state.expectations_satisfied() {
534                            let Some((args, calldata_bytes)) = self
535                                .materialize_stateless_counterexample_if_branch_target_satisfied(
536                                    state.root_calldata.as_ref().ok_or_else(|| {
537                                        SymbolicError::Unsupported("missing root symbolic calldata")
538                                    })?,
539                                    input.function,
540                                    &state,
541                                )?
542                            else {
543                                *completed_paths += 1;
544                                break;
545                            };
546                            return Ok(SymbolicRunResult::Counterexample {
547                                args,
548                                calldata: calldata_bytes,
549                                stats: self.stats_with_paths(*completed_paths + 1),
550                            });
551                        }
552                        let candidate = self.collect_branch_candidate(
553                            branch_candidates.as_deref_mut(),
554                            input.function,
555                            &state,
556                        )?;
557                        if input.collect_success_input
558                            && state.satisfies_branch_target()
559                            && state.can_materialize_seed()
560                            && success_input.as_ref().is_none_or(|(depth, _)| state.depth > *depth)
561                        {
562                            let input = match candidate {
563                                Some(input) => input,
564                                None => self.materialize_stateless_input(
565                                    state.root_calldata.as_ref().ok_or_else(|| {
566                                        SymbolicError::Unsupported("missing root symbolic calldata")
567                                    })?,
568                                    input.function,
569                                    &state,
570                                )?,
571                            };
572                            success_input = Some((state.depth, input));
573                        }
574                        *completed_paths += 1;
575                        normal_paths += 1;
576                        break;
577                    }
578                    StepOutcome::Revert => {
579                        self.collect_branch_candidate(
580                            branch_candidates.as_deref_mut(),
581                            input.function,
582                            &state,
583                        )?;
584                        *completed_paths += 1;
585                        reverted_paths += 1;
586                        break;
587                    }
588                    StepOutcome::AssumeRejected => break,
589                    StepOutcome::Forked => break,
590                    StepOutcome::ExceptionalHalt | StepOutcome::Failure => {
591                        let Some((args, calldata_bytes)) = self
592                            .materialize_stateless_counterexample_if_branch_target_satisfied(
593                                state.root_calldata.as_ref().ok_or_else(|| {
594                                    SymbolicError::Unsupported("missing root symbolic calldata")
595                                })?,
596                                input.function,
597                                &state,
598                            )?
599                        else {
600                            *completed_paths += 1;
601                            break;
602                        };
603                        return Ok(SymbolicRunResult::Counterexample {
604                            args,
605                            calldata: calldata_bytes,
606                            stats: self.stats_with_paths(*completed_paths + 1),
607                        });
608                    }
609                }
610            }
611        }
612
613        if normal_paths == 0 && reverted_paths > 0 {
614            debug!(completed_paths = *completed_paths, "all symbolic paths reverted");
615            return Ok(SymbolicRunResult::Incomplete {
616                kind: SymbolicStopReason::RevertAll,
617                reason: "all symbolic paths reverted".to_string(),
618                stats: self.stats_with_paths(*completed_paths),
619            });
620        }
621
622        if let Some((kind, reason)) = self.deferred_incomplete() {
623            return Ok(SymbolicRunResult::Incomplete {
624                kind,
625                reason,
626                stats: self.stats_with_paths(*completed_paths),
627            });
628        }
629
630        debug!(completed_paths = *completed_paths, "symbolic execution safe");
631        Ok(SymbolicRunResult::Safe {
632            stats: self.stats_with_paths(*completed_paths),
633            success_input: success_input.map(|(_, input)| input),
634        })
635    }
636
637    fn collect_branch_candidate(
638        &mut self,
639        candidates: Option<&mut Vec<SymbolicConcreteInput>>,
640        function: &Function,
641        state: &PathState,
642    ) -> Result<Option<SymbolicConcreteInput>, SymbolicError> {
643        let Some(candidates) = candidates else {
644            return Ok(None);
645        };
646        if !state.satisfies_branch_target() || !state.can_materialize_seed() {
647            return Ok(None);
648        }
649
650        let input = self.materialize_stateless_input(
651            state
652                .root_calldata
653                .as_ref()
654                .ok_or(SymbolicError::Unsupported("missing root symbolic calldata"))?,
655            function,
656            state,
657        )?;
658        candidates.push(input.clone());
659        Ok(Some(input))
660    }
661
662    fn materialize_stateless_counterexample_if_branch_target_satisfied(
663        &mut self,
664        calldata: &SymbolicCalldata,
665        function: &Function,
666        state: &PathState,
667    ) -> Result<Option<(Vec<DynSolValue>, Bytes)>, SymbolicError> {
668        if !state.satisfies_branch_target() {
669            return Ok(None);
670        }
671        self.materialize_stateless_counterexample(calldata, function, state).map(Some)
672    }
673
674    pub(super) fn materialize_stateless_counterexample(
675        &mut self,
676        calldata: &SymbolicCalldata,
677        function: &Function,
678        state: &PathState,
679    ) -> Result<(Vec<DynSolValue>, Bytes), SymbolicError> {
680        debug!(
681            constraint_count = state.constraints.len(),
682            "materializing counterexample from solver model"
683        );
684        self.materialize_stateless_input(calldata, function, state)
685            .map(|input| (input.args, input.calldata))
686    }
687
688    /// Runs the `materialize_stateless_input` symbolic executor helper.
689    pub(super) fn materialize_stateless_input(
690        &mut self,
691        calldata: &SymbolicCalldata,
692        function: &Function,
693        state: &PathState,
694    ) -> Result<SymbolicConcreteInput, SymbolicError> {
695        let replayable_storage = state.world.replay_storage_symbols();
696        let model = self.solver.model_with_replayable_storage(
697            &mut self.cx,
698            &state.constraints,
699            &replayable_storage,
700        )?;
701        let args = calldata.model_to_args(&mut self.cx, &model)?;
702        let calldata_bytes = Bytes::from(function.abi_encode_input(&args)?);
703        Ok(SymbolicConcreteInput { args, calldata: calldata_bytes })
704    }
705
706    pub(super) fn run_invariant_inner<FEN: FoundryEvmNetwork>(
707        &mut self,
708        input: SymbolicInvariantRunInput<'_, FEN>,
709    ) -> Result<SymbolicInvariantRunResult, SymbolicError> {
710        if input.targets.is_empty() {
711            return Err(SymbolicError::Unsupported("symbolic invariant has no targets"));
712        }
713
714        let mut senders =
715            if input.senders.is_empty() { vec![input.sender] } else { input.senders.clone() };
716        senders.retain(|sender| !input.excluded_senders.contains(sender));
717        if senders.is_empty() {
718            return Err(SymbolicError::Unsupported("symbolic invariant senders are excluded"));
719        }
720        let after_invariant_for = |steps_len: usize| {
721            (steps_len == input.depth).then_some(input.after_invariant).flatten()
722        };
723        let mut completed_paths = 0usize;
724        let mut initial_state = PathState::empty(
725            &mut self.cx,
726            input.invariant_address,
727            input.sender,
728            input.ffi_enabled,
729        );
730        initial_state.apply_executor_env(&mut self.cx, input.executor);
731        initial_state.world.set_storage_layout(self.config.storage_layout);
732        let initial = SequencePath { state: initial_state, steps: Vec::new() };
733
734        if symbolic_invariant_should_check(0, input.depth, input.check_interval) {
735            for outcome in self.execute_invariant_check(
736                input.executor,
737                initial.state.clone(),
738                input.invariant_address,
739                input.sender,
740                input.invariant,
741                after_invariant_for(0),
742                &mut completed_paths,
743            )? {
744                if outcome.failed {
745                    let (sequence, storage) =
746                        self.materialize_sequence(&initial.steps, &outcome.state)?;
747                    return Ok(SymbolicInvariantRunResult::Counterexample {
748                        kind: SymbolicInvariantCounterexampleKind::Predicate,
749                        sequence,
750                        storage,
751                        stats: self.stats_with_paths(completed_paths),
752                    });
753                }
754            }
755        }
756
757        let path_limit = self.config.path_width() as usize;
758        let mut frontier = vec![initial];
759        for depth in 0..input.depth {
760            self.check_timeout()?;
761            let mut next_frontier = Vec::new();
762            for sequence in frontier {
763                self.check_timeout()?;
764                for (target_idx, target) in input.targets.iter().enumerate() {
765                    for (sender_idx, sender) in senders.iter().copied().enumerate() {
766                        self.check_timeout()?;
767                        let prefix = format!("sequence_{depth}_{target_idx}_{sender_idx}");
768                        let calldatas = SymbolicCalldata::variants_with_prefix(
769                            &target.function,
770                            &self.config,
771                            &mut self.cx,
772                            &prefix,
773                        )?;
774                        for calldata in calldatas {
775                            let step = SequenceStepTemplate {
776                                sender,
777                                address: target.address,
778                                contract_name: target.contract_name.clone(),
779                                function: target.function.clone(),
780                                calldata,
781                            };
782                            let calldata = step.calldata.call_data(&mut self.cx);
783                            let constraints = step.calldata.constraints().to_vec();
784                            let mut call = self.prepare_sequence_call(
785                                input.executor,
786                                sequence.state.clone(),
787                                target.address,
788                                sender,
789                                &target.function,
790                                calldata,
791                                constraints,
792                            )?;
793
794                            while let Some(outcome) = self.execute_sequence_call_next(
795                                input.executor,
796                                &mut call,
797                                &mut completed_paths,
798                            )? {
799                                let mut steps = sequence.steps.clone();
800                                steps.push(step.clone());
801
802                                match outcome.status {
803                                    CallStatus::Failure => {
804                                        let (sequence, storage) =
805                                            self.materialize_sequence(&steps, &outcome.state)?;
806                                        return Ok(SymbolicInvariantRunResult::Counterexample {
807                                            kind: SymbolicInvariantCounterexampleKind::Handler,
808                                            sequence,
809                                            storage,
810                                            stats: self.stats_with_paths(completed_paths),
811                                        });
812                                    }
813                                    CallStatus::Revert | CallStatus::ExceptionalHalt => {
814                                        if input.fail_on_revert {
815                                            let (sequence, storage) =
816                                                self.materialize_sequence(&steps, &outcome.state)?;
817                                            return Ok(
818                                                SymbolicInvariantRunResult::Counterexample {
819                                                    kind: SymbolicInvariantCounterexampleKind::Predicate,
820                                                    sequence,
821                                                    storage,
822                                                    stats: self.stats_with_paths(completed_paths),
823                                                },
824                                            );
825                                        }
826                                        // A reverted top-level call cannot change persistent
827                                        // state, but it still consumes one invariant sequence
828                                        // step. Preserve the pre-call world together with the
829                                        // reverted branch constraints so end-only and periodic
830                                        // invariant checks observe the same call schedule as the
831                                        // concrete campaign.
832                                        let mut reverted_state = sequence.state.clone();
833                                        reverted_state
834                                            .take_reverted_top_level_effects(outcome.state);
835                                        if symbolic_invariant_should_check(
836                                            steps.len(),
837                                            input.depth,
838                                            input.check_interval,
839                                        ) {
840                                            for mut invariant_outcome in self
841                                                .execute_invariant_check(
842                                                    input.executor,
843                                                    reverted_state.clone(),
844                                                    input.invariant_address,
845                                                    input.sender,
846                                                    input.invariant,
847                                                    after_invariant_for(steps.len()),
848                                                    &mut completed_paths,
849                                                )?
850                                            {
851                                                if invariant_outcome.failed {
852                                                    let (sequence, storage) = self
853                                                        .materialize_sequence(
854                                                            &steps,
855                                                            &invariant_outcome.state,
856                                                        )?;
857                                                    return Ok(
858                                                        SymbolicInvariantRunResult::Counterexample {
859                                                            kind: SymbolicInvariantCounterexampleKind::Predicate,
860                                                            sequence,
861                                                            storage,
862                                                            stats: self
863                                                                .stats_with_paths(completed_paths),
864                                                        },
865                                                    );
866                                                }
867                                                let mut state = reverted_state.clone();
868                                                state.take_noncommitting_check_state(
869                                                    &mut invariant_outcome.state,
870                                                );
871                                                next_frontier.push(SequencePath {
872                                                    state,
873                                                    steps: steps.clone(),
874                                                });
875                                            }
876                                        } else {
877                                            next_frontier.push(SequencePath {
878                                                state: reverted_state,
879                                                steps: steps.clone(),
880                                            });
881                                        }
882                                    }
883                                    CallStatus::Success => {
884                                        if symbolic_invariant_should_check(
885                                            steps.len(),
886                                            input.depth,
887                                            input.check_interval,
888                                        ) {
889                                            for mut invariant_outcome in self
890                                                .execute_invariant_check(
891                                                    input.executor,
892                                                    outcome.state.clone(),
893                                                    input.invariant_address,
894                                                    input.sender,
895                                                    input.invariant,
896                                                    after_invariant_for(steps.len()),
897                                                    &mut completed_paths,
898                                                )?
899                                            {
900                                                if invariant_outcome.failed {
901                                                    let (sequence, storage) = self
902                                                        .materialize_sequence(
903                                                            &steps,
904                                                            &invariant_outcome.state,
905                                                        )?;
906                                                    return Ok(
907                                                        SymbolicInvariantRunResult::Counterexample {
908                                                            kind: SymbolicInvariantCounterexampleKind::Predicate,
909                                                            sequence,
910                                                            storage,
911                                                            stats: self
912                                                                .stats_with_paths(completed_paths),
913                                                        },
914                                                    );
915                                                }
916                                                let mut state = outcome.state.clone();
917                                                state.take_noncommitting_check_state(
918                                                    &mut invariant_outcome.state,
919                                                );
920                                                next_frontier.push(SequencePath {
921                                                    state,
922                                                    steps: steps.clone(),
923                                                });
924                                            }
925                                        } else {
926                                            next_frontier.push(SequencePath {
927                                                state: outcome.state,
928                                                steps: steps.clone(),
929                                            });
930                                        }
931                                    }
932                                }
933
934                                if completed_paths >= path_limit {
935                                    return Ok(SymbolicInvariantRunResult::Incomplete {
936                                        kind: SymbolicStopReason::Stuck,
937                                        reason: format!(
938                                            "symbolic path limit exceeded ({path_limit})"
939                                        ),
940                                        stats: self.stats_with_paths(completed_paths),
941                                    });
942                                }
943                            }
944                        }
945                    }
946                }
947            }
948
949            if next_frontier.is_empty() {
950                break;
951            }
952            frontier = next_frontier;
953        }
954
955        if let Some((kind, reason)) = self.deferred_incomplete() {
956            return Ok(SymbolicInvariantRunResult::Incomplete {
957                kind,
958                reason,
959                stats: self.stats_with_paths(completed_paths),
960            });
961        }
962
963        Ok(SymbolicInvariantRunResult::Safe(self.stats_with_paths(completed_paths)))
964    }
965
966    pub(super) fn stats_with_paths(&self, paths: usize) -> SymbolicStats {
967        let mut stats = self.solver.stats();
968        stats.paths = paths;
969        stats
970    }
971}
972
973fn order_roots_by_corpus_seed_count(roots: &mut [PathState], order: SymbolicExplorationOrder) {
974    let Some((first, rest)) = roots.split_first() else {
975        return;
976    };
977    if rest.iter().all(|root| root.corpus_seed_model_count() == first.corpus_seed_model_count()) {
978        return;
979    }
980
981    match order {
982        SymbolicExplorationOrder::Bfs => {
983            roots.sort_by_key(|root| Reverse(root.corpus_seed_model_count()));
984        }
985        SymbolicExplorationOrder::Dfs => {
986            roots.sort_by_key(PathState::corpus_seed_model_count);
987        }
988    }
989}
990
991const fn symbolic_invariant_should_check(
992    sequence_len: usize,
993    depth: usize,
994    check_interval: u32,
995) -> bool {
996    sequence_len == depth
997        || (check_interval != 0
998            && sequence_len != 0
999            && sequence_len.is_multiple_of(check_interval as usize))
1000}
1001
1002#[cfg(test)]
1003mod tests {
1004    use super::*;
1005
1006    #[test]
1007    fn stateless_runs_only_start_wall_clock_deadline_for_deferred_solver_phase() {
1008        let mut executor =
1009            SymbolicExecutor::new(SymbolicConfig { timeout: Some(1), ..Default::default() });
1010
1011        executor.reset_run_state(false);
1012        assert!(executor.deadline.is_none());
1013
1014        executor.reset_run_state(true);
1015        assert!(executor.deadline.is_some());
1016    }
1017
1018    #[test]
1019    fn hard_arithmetic_never_masks_a_specific_incomplete_reason() {
1020        let mut executor = SymbolicExecutor::new(SymbolicConfig::default());
1021
1022        executor.defer_hard_arithmetic();
1023        executor.defer_solver_unknown();
1024        assert_eq!(executor.deferred_incomplete, Some(DeferredIncomplete::SolverUnknown));
1025
1026        executor.reset_run_state(false);
1027        executor.defer_hard_arithmetic();
1028        executor.defer_incomplete("unsupported after hard arithmetic");
1029        assert_eq!(
1030            executor.deferred_incomplete,
1031            Some(DeferredIncomplete::Unsupported("unsupported after hard arithmetic"))
1032        );
1033
1034        executor.reset_run_state(false);
1035        executor.defer_solver_unknown();
1036        executor.defer_hard_arithmetic();
1037        assert_eq!(executor.deferred_incomplete, Some(DeferredIncomplete::SolverUnknown));
1038    }
1039}
foundry_evm_symbolic/executor/run.rs

foundry_evm_symbolic/executor/
run.rs
