foundry_evm_symbolic/
runtime.rs

1use super::{abi::*, *};
2
3mod address;
4mod calldata;
5mod cheatcodes;
6mod control;
7mod evm;
8mod expressions;
9mod memory;
10mod precompiles;
11mod solver;
12mod state;
13
14pub(crate) use address::*;
15pub(crate) use calldata::*;
16pub(crate) use cheatcodes::*;
17pub(crate) use control::*;
18pub(crate) use evm::*;
19pub(crate) use expressions::*;
20pub(crate) use memory::*;
21pub(crate) use precompiles::*;
22pub use solver::PortfolioDiagnostics;
23pub(crate) use solver::{
24    SmtLibSubprocessSolver, SymbolicSolver, solver_portfolio_availability_warning,
25};
26#[cfg(test)]
27pub(crate) use solver::{
28    SolverCommand, SolverConfigError, SolverOutcome, SolverRunSummary, expr_contains_hard_arith,
29    fallback_single_var_model, hard_arith_fallback_model, named_solver_command,
30    normalize_bool_for_solver, normalize_constraints_for_solver, normalize_expr_for_solver,
31    parse_model, product_monotonic_unsat, solver_commands_for_config, split_solver_command,
32    validate_solver_model_output,
33};
34pub(crate) use state::*;
35
36pub struct SymbolicRunInput<'a, FEN: FoundryEvmNetwork> {
37    /// Concrete Foundry executor used as the source of deployed bytecode and backend state.
38    pub executor: &'a Executor<FEN>,
39    /// Address of the deployed test contract whose runtime bytecode will be explored.
40    pub target: Address,
41    /// Sender used for symbolic execution environment opcodes such as `CALLER` and `ORIGIN`.
42    pub sender: Address,
43    /// ABI function to invoke symbolically.
44    pub function: &'a Function,
45    /// Call value exposed to the symbolic execution through `CALLVALUE`.
46    pub value: U256,
47    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
48    pub ffi_enabled: bool,
49}
50
51/// Error returned by the internal symbolic executor.
52///
53/// Public callers normally receive these errors as [`SymbolicRunResult::Incomplete`]
54/// through [`SymbolicExecutor::run`]. The enum is public so integration code and tests
55/// can inspect exact failure causes when using lower-level helpers in this crate.
56#[derive(Debug, Error)]
57pub enum SymbolicError {
58    /// The target account was not present in the executor backend.
59    #[error("missing account {0}")]
60    MissingAccount(Address),
61    /// The target account had no runtime bytecode.
62    #[error("missing code for account {0}")]
63    MissingCode(Address),
64    /// The concrete backend returned an error while reading account state.
65    #[error("backend error: {0}")]
66    Backend(String),
67    /// The function ABI contains a type that is not supported by the V1 symbolic calldata model.
68    #[error("unsupported ABI type for symbolic execution: {0}")]
69    UnsupportedAbi(String),
70    /// Symbolic calldata variant expansion exceeded the configured path-width budget.
71    #[error("symbolic calldata variant limit exceeded ({0})")]
72    CalldataVariantLimit(usize),
73    /// Symbolic execution reached a feature that is not implemented yet.
74    #[error("unsupported symbolic execution feature: {0}")]
75    Unsupported(&'static str),
76    /// Symbolic execution reached an opcode that is not implemented yet.
77    #[error("unsupported opcode 0x{0:02x}")]
78    UnsupportedOpcode(u8),
79    /// Runtime bytecode was malformed in a way that prevents symbolic execution.
80    #[error("invalid bytecode: {0}")]
81    InvalidBytecode(&'static str),
82    /// A jump targeted a byte offset that is not a valid `JUMPDEST`.
83    #[error("invalid jump destination {0}")]
84    InvalidJump(usize),
85    /// The symbolic stack was popped without enough values.
86    #[error("stack underflow")]
87    StackUnderflow,
88    /// The symbolic stack exceeded the EVM stack limit.
89    #[error("stack overflow")]
90    StackOverflow,
91    /// The solver process failed, timed out, or returned an unexpected response.
92    #[error("solver error: {0}")]
93    Solver(String),
94    /// The solver returned `unknown`.
95    #[error("solver returned unknown")]
96    SolverUnknown,
97    /// The configured maximum number of solver queries was reached.
98    #[error("symbolic solver query limit exceeded ({0})")]
99    SolverQueryLimit(usize),
100    /// ABI encoding failed while constructing a concrete counterexample call.
101    #[error(transparent)]
102    Abi(#[from] alloy_dyn_abi::Error),
103}
104
105impl SymbolicError {
106    /// Implements the `stop_reason` symbolic runtime helper.
107    pub(super) const fn stop_reason(&self) -> SymbolicStopReason {
108        match self {
109            Self::Unsupported(_)
110            | Self::CalldataVariantLimit(_)
111            | Self::UnsupportedOpcode(_)
112            | Self::SolverQueryLimit(_) => SymbolicStopReason::Stuck,
113            Self::SolverUnknown => SymbolicStopReason::Timeout,
114            Self::Solver(_)
115            | Self::MissingAccount(_)
116            | Self::MissingCode(_)
117            | Self::Backend(_)
118            | Self::UnsupportedAbi(_)
119            | Self::InvalidBytecode(_)
120            | Self::InvalidJump(_)
121            | Self::StackUnderflow
122            | Self::StackOverflow
123            | Self::Abi(_) => SymbolicStopReason::Error,
124        }
125    }
126}
127
128impl fmt::Display for SymbolicRunResult {
129    /// Implements the `fmt` symbolic runtime helper.
130    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
131        match self {
132            Self::Safe(stats) => write!(f, "safe after {} paths", stats.paths),
133            Self::Counterexample { stats, .. } => {
134                write!(f, "counterexample after {} paths", stats.paths)
135            }
136            Self::Incomplete { kind, reason, .. } => {
137                write!(f, "incomplete symbolic execution ({kind:?}): {reason}")
138            }
139        }
140    }
141}
foundry_evm_symbolic/runtime.rs

foundry_evm_symbolic/
runtime.rs
