foundry_evm_symbolic/
lib.rs

1//! Foundry's symbolic EVM executor.
2
3#![warn(unused_crate_dependencies)]
4
5use alloy_dyn_abi::{DynSolType, DynSolValue, JsonAbiExt};
6use alloy_json_abi::Function;
7use alloy_primitives::{
8    Address, B256, Bytes, I256, Keccak256, U256, hex, keccak256,
9    map::{HashMap, HashSet, IndexSet},
10};
11use alloy_signer::SignerSync;
12use alloy_signer_local::{
13    PrivateKeySigner,
14    coins_bip39::{English, Wordlist},
15};
16use alloy_sol_types::SolCall;
17use base64::prelude::*;
18use foundry_cheatcodes_spec::{SymbolicVm, Vm};
19use foundry_config::{SymbolicConfig, SymbolicExplorationOrder, SymbolicStorageLayout};
20use foundry_evm::{
21    constants::{CALLER, CHEATCODE_ADDRESS, DEFAULT_CREATE2_DEPLOYER, HARDHAT_CONSOLE_ADDRESS},
22    core::{backend::DatabaseExt, evm::FoundryEvmNetwork},
23    executors::Executor,
24    revm::{
25        bytecode::{Bytecode, JumpTable, eip7702::EIP7702_BYTECODE_LEN, opcode},
26        context::{Block, Cfg, Transaction},
27        database::DatabaseRef,
28        precompile::{PrecompileSpecId, Precompiles, kzg_point_evaluation},
29        primitives::hardfork::SpecId,
30    },
31};
32use serde::{Deserialize, Serialize};
33use std::{
34    collections::VecDeque,
35    fmt::{self, Write as _},
36    io::Write,
37    ops::{ControlFlow, Deref, DerefMut},
38    path::{Path, PathBuf},
39    process::{Command, Stdio},
40    sync::{
41        Arc,
42        atomic::{AtomicBool, Ordering},
43        mpsc,
44    },
45    thread,
46    time::{Duration, Instant, SystemTime, UNIX_EPOCH},
47};
48use thiserror::Error;
49use tracing::{debug, trace, trace_span, warn};
50
51mod abi;
52mod consts;
53mod executor;
54mod runtime;
55
56pub(crate) use consts::*;
57pub use runtime::{ExecutorView, SymbolicBranchTarget, SymbolicError, SymbolicRunInput};
58
59#[derive(Clone, Copy, Debug, PartialEq, Eq)]
60enum SymbolicVmCheatcode {
61    CreateAddress,
62    CreateBool,
63    CreateBytes,
64    CreateBytesSized,
65    CreateBytesFixed(usize),
66    CreateCalldata,
67    CreateInt,
68    CreateIntBits(usize),
69    CreateString,
70    CreateStringSized,
71    CreateUint,
72    CreateUintBits(usize),
73    EnableSymbolicStorage,
74    SnapshotStorage,
75    SnapshotState,
76}
77
78impl SymbolicVmCheatcode {
79    fn from_selector(selector: [u8; 4]) -> Option<Self> {
80        match selector {
81            SymbolicVm::createAddressCall::SELECTOR => Some(Self::CreateAddress),
82            SymbolicVm::createBoolCall::SELECTOR => Some(Self::CreateBool),
83            SymbolicVm::createBytes_0Call::SELECTOR => Some(Self::CreateBytes),
84            SymbolicVm::createBytes_1Call::SELECTOR => Some(Self::CreateBytesSized),
85            SymbolicVm::createCalldataCall::SELECTOR => Some(Self::CreateCalldata),
86            SymbolicVm::createIntCall::SELECTOR => Some(Self::CreateInt),
87            SymbolicVm::createString_0Call::SELECTOR => Some(Self::CreateString),
88            SymbolicVm::createString_1Call::SELECTOR => Some(Self::CreateStringSized),
89            SymbolicVm::createUintCall::SELECTOR => Some(Self::CreateUint),
90            SymbolicVm::enableSymbolicStorageCall::SELECTOR
91            | Vm::setArbitraryStorage_0Call::SELECTOR => Some(Self::EnableSymbolicStorage),
92            SymbolicVm::snapshotStorageCall::SELECTOR => Some(Self::SnapshotStorage),
93            Vm::snapshotStateCall::SELECTOR => Some(Self::SnapshotState),
94            _ => {
95                let name = SymbolicVm::SymbolicVmCalls::name_by_selector(selector)?;
96                if let Some(bits) = name.strip_prefix("createUint") {
97                    bits.parse().ok().map(Self::CreateUintBits)
98                } else if let Some(bits) = name.strip_prefix("createInt") {
99                    bits.parse().ok().map(Self::CreateIntBits)
100                } else if let Some(bytes) = name.strip_prefix("createBytes") {
101                    bytes.parse().ok().map(Self::CreateBytesFixed)
102                } else {
103                    None
104                }
105            }
106        }
107    }
108
109    const fn min_input_words(self) -> usize {
110        match self {
111            Self::CreateUint
112            | Self::CreateInt
113            | Self::CreateBytesSized
114            | Self::CreateStringSized
115            | Self::EnableSymbolicStorage
116            | Self::SnapshotStorage => 1,
117            Self::CreateAddress
118            | Self::CreateBool
119            | Self::CreateBytes
120            | Self::CreateBytesFixed(_)
121            | Self::CreateCalldata
122            | Self::CreateIntBits(_)
123            | Self::CreateString
124            | Self::CreateUintBits(_)
125            | Self::SnapshotState => 0,
126        }
127    }
128}
129
130/// Outcome of a symbolic test execution.
131///
132/// The forge runner treats `Safe` as a passing symbolic test, `Counterexample` as a
133/// candidate failure that must be replayed concretely, and `Incomplete` as a failing
134/// test because the symbolic engine could not prove the property with the supported
135/// semantics and configured resource limits.
136#[derive(Clone, Debug)]
137pub enum SymbolicRunResult {
138    /// All explored paths completed without a feasible failure.
139    Safe {
140        /// Execution counters collected during the run.
141        stats: SymbolicStats,
142        /// One concrete successful input, when requested by the caller.
143        success_input: Option<SymbolicConcreteInput>,
144    },
145    /// A feasible failure was found.
146    Counterexample {
147        /// ABI-typed argument values extracted from the solver model.
148        args: Vec<DynSolValue>,
149        /// ABI-encoded calldata for the failing invocation.
150        calldata: Bytes,
151        /// Execution counters collected before the counterexample was returned.
152        stats: SymbolicStats,
153    },
154    /// Execution was intentionally stopped because V1 semantics were insufficient.
155    Incomplete {
156        /// Category describing why symbolic execution stopped before proving the test.
157        kind: SymbolicStopReason,
158        /// Human-readable explanation of the unsupported construct or exhausted limit.
159        reason: String,
160        /// Execution counters collected before execution stopped.
161        stats: SymbolicStats,
162    },
163}
164
165/// One concrete symbolic input materialized from a solver model.
166#[derive(Clone, Debug)]
167pub struct SymbolicConcreteInput {
168    /// ABI-typed argument values extracted from the solver model.
169    pub args: Vec<DynSolValue>,
170    /// ABI-encoded calldata for replay.
171    pub calldata: Bytes,
172}
173
174/// Result of best-effort symbolic exploration toward one branch target.
175#[derive(Debug)]
176pub struct SymbolicBranchTargetSearchResult {
177    /// Concrete inputs whose completed root path reached the requested branch outcome.
178    pub candidates: Vec<SymbolicConcreteInput>,
179    /// Underlying execution result, retained so callers can report incomplete exploration.
180    pub execution: SymbolicRunResult,
181}
182
183/// A concrete invariant target selected from Foundry's invariant discovery.
184#[derive(Clone, Debug)]
185pub struct SymbolicInvariantTarget {
186    /// Address that receives the sequence call.
187    pub address: Address,
188    /// Human-readable contract identifier used in counterexample rendering.
189    pub contract_name: Option<String>,
190    /// ABI function invoked with symbolic arguments.
191    pub function: Function,
192}
193
194/// Input for best-effort invariant candidate search after one symbolic handler call.
195pub struct SymbolicInvariantCandidateInput<'a> {
196    /// Read-only view of the concrete Foundry executor containing the replayed invariant frontier
197    /// prefix.
198    pub executor: ExecutorView<'a>,
199    /// Address of the deployed invariant test contract.
200    pub invariant_address: Address,
201    /// Invariant functions checked independently after the handler call.
202    pub invariants: &'a [&'a Function],
203    /// Optional campaign hook checked from the unchanged post-handler state.
204    pub after_invariant: Option<&'a Function>,
205    /// Concrete handler target selected from the captured frontier.
206    pub target: &'a SymbolicInvariantTarget,
207    /// Sender of the captured handler call.
208    pub handler_sender: Address,
209    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
210    pub ffi_enabled: bool,
211}
212
213/// One unconfirmed symbolic input produced by invariant candidate search.
214#[derive(Clone, Debug)]
215pub struct SymbolicInvariantCandidate {
216    /// Index within [`SymbolicInvariantCandidateInput::invariants`] predicted to fail.
217    pub invariant_idx: usize,
218    /// Concrete handler call extracted from the solver model.
219    pub step: SymbolicInvariantStep,
220    /// Concrete setup-storage values needed to replay the candidate.
221    pub storage: Vec<SymbolicStorageAssignment>,
222}
223
224/// An execution or solver limitation encountered during best-effort candidate search.
225#[derive(Clone, Debug, PartialEq, Eq)]
226pub struct SymbolicInvariantSearchLimitation {
227    /// Category describing why part of the search could not complete.
228    pub kind: SymbolicStopReason,
229    /// Human-readable description of the limitation.
230    pub reason: String,
231}
232
233impl From<SymbolicError> for SymbolicInvariantSearchLimitation {
234    fn from(error: SymbolicError) -> Self {
235        Self { kind: error.stop_reason(), reason: error.to_string() }
236    }
237}
238
239/// Result of best-effort invariant candidate search after one symbolic handler call.
240#[derive(Clone, Debug)]
241pub struct SymbolicInvariantCandidateSearchResult {
242    /// Unconfirmed candidates that must be replayed concretely by the caller.
243    pub candidates: Vec<SymbolicInvariantCandidate>,
244    /// First encountered search limitation, unless a later error exhausts the search.
245    /// `None` is not a proof of safety.
246    pub limitation: Option<SymbolicInvariantSearchLimitation>,
247}
248
249/// Input for bounded symbolic invariant execution.
250pub struct SymbolicInvariantRunInput<'a> {
251    /// Read-only view of the concrete Foundry executor used as the source of deployed bytecode and
252    /// backend state.
253    pub executor: ExecutorView<'a>,
254    /// Address of the deployed invariant test contract.
255    pub invariant_address: Address,
256    /// Default sender used when invariant targeting does not configure senders.
257    pub sender: Address,
258    /// Invariant function checked after each symbolic sequence step.
259    pub invariant: &'a Function,
260    /// Optional `afterInvariant` hook to execute after a passing invariant check.
261    pub after_invariant: Option<&'a Function>,
262    /// Concrete target/selector set discovered by Foundry invariant targeting.
263    pub targets: Vec<SymbolicInvariantTarget>,
264    /// Concrete sender set discovered by Foundry invariant targeting.
265    pub senders: Vec<Address>,
266    /// Sender addresses excluded by Foundry invariant targeting.
267    pub excluded_senders: Vec<Address>,
268    /// Maximum number of sequence calls to execute.
269    pub depth: usize,
270    /// Concrete invariant check interval. `0` means only check at sequence end.
271    pub check_interval: u32,
272    /// Whether ordinary target-call reverts should be reported as failures.
273    pub fail_on_revert: bool,
274    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
275    pub ffi_enabled: bool,
276}
277
278/// One concrete storage value required to replay a symbolic invariant candidate.
279#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
280pub struct SymbolicStorageAssignment {
281    /// Account whose storage slot should be initialized.
282    pub address: Address,
283    /// Concrete storage slot.
284    pub slot: U256,
285    /// Concrete value extracted from the solver model.
286    pub value: U256,
287}
288
289/// Outcome of bounded symbolic invariant execution.
290#[derive(Clone, Debug)]
291pub enum SymbolicInvariantRunResult {
292    /// No feasible invariant failure was found within the configured sequence depth.
293    Safe(SymbolicStats),
294    /// A feasible invariant or handler failure was found.
295    Counterexample {
296        /// Which part of the invariant run produced the failure.
297        kind: SymbolicInvariantCounterexampleKind,
298        /// Concrete sequence extracted from the solver model.
299        sequence: Vec<SymbolicInvariantStep>,
300        /// Concrete setup-storage values needed for replay.
301        storage: Vec<SymbolicStorageAssignment>,
302        /// Execution counters collected before the counterexample was returned.
303        stats: SymbolicStats,
304    },
305    /// Execution stopped before proving the invariant.
306    Incomplete {
307        /// Category describing why symbolic execution stopped.
308        kind: SymbolicStopReason,
309        /// Human-readable explanation of the unsupported construct or exhausted limit.
310        reason: String,
311        /// Execution counters collected before execution stopped.
312        stats: SymbolicStats,
313    },
314}
315
316/// Part of a symbolic invariant run that produced a replayable counterexample.
317#[derive(Clone, Copy, Debug, PartialEq, Eq)]
318pub enum SymbolicInvariantCounterexampleKind {
319    /// An `invariant_*` or `afterInvariant` check failed.
320    Predicate,
321    /// A fuzzed target/handler call failed with an assertion.
322    Handler,
323}
324
325/// One concrete step in a symbolic invariant counterexample sequence.
326#[derive(Clone, Debug)]
327pub struct SymbolicInvariantStep {
328    /// Sender used for the call.
329    pub sender: Address,
330    /// Target address called by the sequence step.
331    pub address: Address,
332    /// Human-readable contract identifier, when known.
333    pub contract_name: Option<String>,
334    /// ABI function name.
335    pub function_name: String,
336    /// ABI function signature.
337    pub signature: String,
338    /// ABI-typed arguments extracted from the solver model.
339    pub args: Vec<DynSolValue>,
340    /// ABI-encoded calldata for replay.
341    pub calldata: Bytes,
342}
343
344/// High-level reason a symbolic run stopped without a proof or replayed counterexample.
345#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
346pub enum SymbolicStopReason {
347    /// The executor reached a supported-but-incomplete semantic boundary.
348    Stuck,
349    /// Every explored execution path ended in an ordinary revert.
350    RevertAll,
351    /// The solver timed out or returned `unknown`.
352    Timeout,
353    /// An internal engine, backend, or solver process error occurred.
354    Error,
355}
356
357/// Symbolic execution counters.
358#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
359pub struct SymbolicStats {
360    /// Number of explored symbolic paths.
361    pub paths: usize,
362    /// Number of normalized solver queries issued during the run.
363    pub solver_queries: usize,
364    /// Number of queries sent to the SMT backend after local fast paths.
365    #[serde(default)]
366    pub smt_queries: usize,
367    /// Number of satisfiability checks requested by the executor.
368    #[serde(default)]
369    pub sat_queries: usize,
370    /// Number of concrete model requests requested by the executor.
371    #[serde(default)]
372    pub model_queries: usize,
373    /// Number of satisfiability checks served from the normalized cache.
374    #[serde(default)]
375    pub sat_cache_hits: usize,
376    /// Number of model requests served from the normalized model cache.
377    #[serde(default)]
378    pub model_cache_hits: usize,
379    /// Number of satisfiable witnesses produced by local hard-arithmetic search.
380    #[serde(default)]
381    pub heuristic_witnesses: usize,
382    /// Wall-clock time spent waiting on backend solver subprocesses, in milliseconds.
383    #[serde(default)]
384    pub solver_time_ms: u64,
385    /// Total SMT-LIB input bytes sent to backend solver subprocesses.
386    #[serde(default)]
387    pub smt_input_bytes: u64,
388    /// Largest single SMT-LIB query input sent to a backend solver subprocess, in bytes.
389    #[serde(default)]
390    pub smt_max_query_bytes: u64,
391    /// Wall-clock time spent building SMT-LIB query strings, in milliseconds.
392    #[serde(default)]
393    pub smt_build_time_ms: u64,
394    /// Longest single backend solver subprocess query, in milliseconds.
395    #[serde(default)]
396    pub smt_max_query_time_ms: u64,
397}
398
399/// SMT-LIB-backed symbolic executor.
400///
401/// This executor is intentionally separate from the concrete revm executor used by
402/// Foundry. It consumes bytecode and state from an existing [`Executor`], explores
403/// symbolic branches, and returns either a proof result, a counterexample candidate,
404/// or an incomplete result.
405pub struct SymbolicExecutor {
406    config: SymbolicConfig,
407    cx: runtime::SymCx,
408    solver: runtime::SmtLibSubprocessSolver,
409    deferred_incomplete: Option<DeferredIncomplete>,
410    deadline: Option<Instant>,
411    nested_deferred_mode: DeferredPathMode,
412    stateless_retry_safe: bool,
413}
414
415#[derive(Clone, Copy, Debug, PartialEq, Eq)]
416enum DeferredPathMode {
417    Skip,
418    Yield,
419    Drain,
420}
421
422#[derive(Clone, Copy, Debug, PartialEq, Eq)]
423enum DeferredIncomplete {
424    Unsupported(&'static str),
425    SolverUnknown,
426    HardArithmetic,
427}
foundry_evm_symbolic/lib.rs

foundry_evm_symbolic/
lib.rs
