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, opcode},
26        context::{Block, Cfg, Transaction},
27        database::DatabaseRef,
28        precompile::{blake2, bn254, hash, identity, kzg_point_evaluation, modexp, secp256k1},
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::{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, FEN: FoundryEvmNetwork> {
196    /// Concrete Foundry executor containing the replayed invariant frontier prefix.
197    pub executor: &'a Executor<FEN>,
198    /// Address of the deployed invariant test contract.
199    pub invariant_address: Address,
200    /// Invariant functions checked independently after the handler call.
201    pub invariants: &'a [&'a Function],
202    /// Optional campaign hook checked from the unchanged post-handler state.
203    pub after_invariant: Option<&'a Function>,
204    /// Concrete handler target selected from the captured frontier.
205    pub target: &'a SymbolicInvariantTarget,
206    /// Sender of the captured handler call.
207    pub handler_sender: Address,
208    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
209    pub ffi_enabled: bool,
210}
211
212/// One unconfirmed symbolic input produced by invariant candidate search.
213#[derive(Clone, Debug)]
214pub struct SymbolicInvariantCandidate {
215    /// Index within [`SymbolicInvariantCandidateInput::invariants`] predicted to fail.
216    pub invariant_idx: usize,
217    /// Concrete handler call extracted from the solver model.
218    pub step: SymbolicInvariantStep,
219    /// Concrete setup-storage values needed to replay the candidate.
220    pub storage: Vec<SymbolicStorageAssignment>,
221}
222
223/// An execution or solver limitation encountered during best-effort candidate search.
224#[derive(Clone, Debug, PartialEq, Eq)]
225pub struct SymbolicInvariantSearchLimitation {
226    /// Category describing why part of the search could not complete.
227    pub kind: SymbolicStopReason,
228    /// Human-readable description of the limitation.
229    pub reason: String,
230}
231
232impl From<SymbolicError> for SymbolicInvariantSearchLimitation {
233    fn from(error: SymbolicError) -> Self {
234        Self { kind: error.stop_reason(), reason: error.to_string() }
235    }
236}
237
238/// Result of best-effort invariant candidate search after one symbolic handler call.
239#[derive(Clone, Debug)]
240pub struct SymbolicInvariantCandidateSearchResult {
241    /// Unconfirmed candidates that must be replayed concretely by the caller.
242    pub candidates: Vec<SymbolicInvariantCandidate>,
243    /// First encountered search limitation, unless a later error exhausts the search.
244    /// `None` is not a proof of safety.
245    pub limitation: Option<SymbolicInvariantSearchLimitation>,
246}
247
248/// Input for bounded symbolic invariant execution.
249pub struct SymbolicInvariantRunInput<'a, FEN: FoundryEvmNetwork> {
250    /// Concrete Foundry executor used as the source of deployed bytecode and backend state.
251    pub executor: &'a Executor<FEN>,
252    /// Address of the deployed invariant test contract.
253    pub invariant_address: Address,
254    /// Default sender used when invariant targeting does not configure senders.
255    pub sender: Address,
256    /// Invariant function checked after each symbolic sequence step.
257    pub invariant: &'a Function,
258    /// Optional `afterInvariant` hook to execute after a passing invariant check.
259    pub after_invariant: Option<&'a Function>,
260    /// Concrete target/selector set discovered by Foundry invariant targeting.
261    pub targets: Vec<SymbolicInvariantTarget>,
262    /// Concrete sender set discovered by Foundry invariant targeting.
263    pub senders: Vec<Address>,
264    /// Sender addresses excluded by Foundry invariant targeting.
265    pub excluded_senders: Vec<Address>,
266    /// Maximum number of sequence calls to execute.
267    pub depth: usize,
268    /// Concrete invariant check interval. `0` means only check at sequence end.
269    pub check_interval: u32,
270    /// Whether ordinary target-call reverts should be reported as failures.
271    pub fail_on_revert: bool,
272    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
273    pub ffi_enabled: bool,
274}
275
276/// One concrete storage value required to replay a symbolic invariant candidate.
277#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
278pub struct SymbolicStorageAssignment {
279    /// Account whose storage slot should be initialized.
280    pub address: Address,
281    /// Concrete storage slot.
282    pub slot: U256,
283    /// Concrete value extracted from the solver model.
284    pub value: U256,
285}
286
287/// Outcome of bounded symbolic invariant execution.
288#[derive(Clone, Debug)]
289pub enum SymbolicInvariantRunResult {
290    /// No feasible invariant failure was found within the configured sequence depth.
291    Safe(SymbolicStats),
292    /// A feasible invariant or handler failure was found.
293    Counterexample {
294        /// Which part of the invariant run produced the failure.
295        kind: SymbolicInvariantCounterexampleKind,
296        /// Concrete sequence extracted from the solver model.
297        sequence: Vec<SymbolicInvariantStep>,
298        /// Concrete setup-storage values needed for replay.
299        storage: Vec<SymbolicStorageAssignment>,
300        /// Execution counters collected before the counterexample was returned.
301        stats: SymbolicStats,
302    },
303    /// Execution stopped before proving the invariant.
304    Incomplete {
305        /// Category describing why symbolic execution stopped.
306        kind: SymbolicStopReason,
307        /// Human-readable explanation of the unsupported construct or exhausted limit.
308        reason: String,
309        /// Execution counters collected before execution stopped.
310        stats: SymbolicStats,
311    },
312}
313
314/// Part of a symbolic invariant run that produced a replayable counterexample.
315#[derive(Clone, Copy, Debug, PartialEq, Eq)]
316pub enum SymbolicInvariantCounterexampleKind {
317    /// An `invariant_*` or `afterInvariant` check failed.
318    Predicate,
319    /// A fuzzed target/handler call failed with an assertion.
320    Handler,
321}
322
323/// One concrete step in a symbolic invariant counterexample sequence.
324#[derive(Clone, Debug)]
325pub struct SymbolicInvariantStep {
326    /// Sender used for the call.
327    pub sender: Address,
328    /// Target address called by the sequence step.
329    pub address: Address,
330    /// Human-readable contract identifier, when known.
331    pub contract_name: Option<String>,
332    /// ABI function name.
333    pub function_name: String,
334    /// ABI function signature.
335    pub signature: String,
336    /// ABI-typed arguments extracted from the solver model.
337    pub args: Vec<DynSolValue>,
338    /// ABI-encoded calldata for replay.
339    pub calldata: Bytes,
340}
341
342/// High-level reason a symbolic run stopped without a proof or replayed counterexample.
343#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
344pub enum SymbolicStopReason {
345    /// The executor reached a supported-but-incomplete semantic boundary.
346    Stuck,
347    /// Every explored execution path ended in an ordinary revert.
348    RevertAll,
349    /// The solver timed out or returned `unknown`.
350    Timeout,
351    /// An internal engine, backend, or solver process error occurred.
352    Error,
353}
354
355/// Symbolic execution counters.
356#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
357pub struct SymbolicStats {
358    /// Number of explored symbolic paths.
359    pub paths: usize,
360    /// Number of normalized solver queries issued during the run.
361    pub solver_queries: usize,
362    /// Number of queries sent to the SMT backend after local fast paths.
363    #[serde(default)]
364    pub smt_queries: usize,
365    /// Number of satisfiability checks requested by the executor.
366    #[serde(default)]
367    pub sat_queries: usize,
368    /// Number of concrete model requests requested by the executor.
369    #[serde(default)]
370    pub model_queries: usize,
371    /// Number of satisfiability checks served from the normalized cache.
372    #[serde(default)]
373    pub sat_cache_hits: usize,
374    /// Number of model requests served from the normalized model cache.
375    #[serde(default)]
376    pub model_cache_hits: usize,
377    /// Number of satisfiable witnesses produced by local hard-arithmetic search.
378    #[serde(default)]
379    pub heuristic_witnesses: usize,
380    /// Wall-clock time spent waiting on backend solver subprocesses, in milliseconds.
381    #[serde(default)]
382    pub solver_time_ms: u64,
383    /// Total SMT-LIB input bytes sent to backend solver subprocesses.
384    #[serde(default)]
385    pub smt_input_bytes: u64,
386    /// Largest single SMT-LIB query input sent to a backend solver subprocess, in bytes.
387    #[serde(default)]
388    pub smt_max_query_bytes: u64,
389    /// Wall-clock time spent building SMT-LIB query strings, in milliseconds.
390    #[serde(default)]
391    pub smt_build_time_ms: u64,
392    /// Longest single backend solver subprocess query, in milliseconds.
393    #[serde(default)]
394    pub smt_max_query_time_ms: u64,
395}
396
397/// SMT-LIB-backed symbolic executor.
398///
399/// This executor is intentionally separate from the concrete revm executor used by
400/// Foundry. It consumes bytecode and state from an existing [`Executor`], explores
401/// symbolic branches, and returns either a proof result, a counterexample candidate,
402/// or an incomplete result.
403pub struct SymbolicExecutor {
404    config: SymbolicConfig,
405    cx: runtime::SymCx,
406    solver: runtime::SmtLibSubprocessSolver,
407    deferred_incomplete: Option<DeferredIncomplete>,
408    deadline: Option<Instant>,
409    nested_deferred_mode: DeferredPathMode,
410    stateless_retry_safe: bool,
411}
412
413#[derive(Clone, Copy, Debug, PartialEq, Eq)]
414enum DeferredPathMode {
415    Skip,
416    Yield,
417    Drain,
418}
419
420#[derive(Clone, Copy, Debug, PartialEq, Eq)]
421enum DeferredIncomplete {
422    Unsupported(&'static str),
423    SolverUnknown,
424    HardArithmetic,
425}
foundry_evm_symbolic/lib.rs

foundry_evm_symbolic/
lib.rs
