foundry_evm_symbolic/executor/
run.rs

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

foundry_evm_symbolic/executor/
run.rs
