Skip to main content

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