foundry_evm_symbolic/
runtime.rs

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

foundry_evm_symbolic/
runtime.rs
