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

foundry_evm_symbolic/
runtime.rs
