foundry_evm_symbolic/
runtime.rs

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

foundry_evm_symbolic/
runtime.rs
