foundry_evm_symbolic/
runtime.rs1use 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#[derive(Clone, Copy, Debug, PartialEq, Eq)]
31pub struct SymbolicBranchTarget {
32 address: Address,
34 pc: usize,
36 opcode: u8,
38 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 pub executor: &'a Executor<FEN>,
59 pub target: Address,
61 pub sender: Address,
63 pub function: &'a Function,
65 pub value: U256,
67 pub ffi_enabled: bool,
69 pub collect_success_input: bool,
71 pub corpus_seeds: Vec<SymbolicConcreteInput>,
73 pub branch_target: Option<SymbolicBranchTarget>,
75}
76
77#[derive(Debug, Error)]
83pub enum SymbolicError {
84 #[error("missing account {0}")]
86 MissingAccount(Address),
87 #[error("missing code for account {0}")]
89 MissingCode(Address),
90 #[error("backend error: {0}")]
92 Backend(String),
93 #[error("unsupported ABI type for symbolic execution: {0}")]
95 UnsupportedAbi(String),
96 #[error("symbolic calldata variant limit exceeded ({0})")]
98 CalldataVariantLimit(usize),
99 #[error("unsupported symbolic execution feature: {0}")]
101 Unsupported(&'static str),
102 #[error("unsupported opcode 0x{0:02x}")]
104 UnsupportedOpcode(u8),
105 #[error("invalid bytecode: {0}")]
107 InvalidBytecode(&'static str),
108 #[error("invalid jump destination {0}")]
110 InvalidJump(usize),
111 #[error("stack underflow")]
113 StackUnderflow,
114 #[error("stack overflow")]
116 StackOverflow,
117 #[error("solver error: {0}")]
119 Solver(String),
120 #[error("solver returned unknown")]
122 SolverUnknown,
123 #[error("symbolic execution timeout exceeded ({0}s)")]
125 Timeout(u32),
126 #[error("symbolic solver query limit exceeded ({0})")]
128 SolverQueryLimit(usize),
129 #[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}