foundry_evm_symbolic/
lib.rs

1//! Foundry's symbolic EVM executor.
2
3#![cfg_attr(not(test), 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, 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::{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, 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};
33#[cfg(test)]
34use std::collections::BTreeMap;
35use std::{
36    collections::VecDeque,
37    fmt::{self, Write as _},
38    io::Write,
39    ops::{ControlFlow, Deref, DerefMut},
40    path::{Path, PathBuf},
41    process::{Command, Stdio},
42    sync::{
43        Arc,
44        atomic::{AtomicBool, Ordering},
45        mpsc,
46    },
47    thread,
48    time::{Duration, Instant, SystemTime, UNIX_EPOCH},
49};
50use thiserror::Error;
51use tracing::{debug, trace, trace_span, warn};
52
53mod consts;
54pub use consts::BUILTIN_SYMBOLIC_SOLVERS;
55pub(crate) use consts::*;
56
57mod abi;
58mod executor;
59mod runtime;
60
61pub use runtime::{PortfolioDiagnostics, SymbolicBranchTarget, SymbolicError, SymbolicRunInput};
62
63/// Returns whether `solver` is one of Foundry's semantic symbolic solver names.
64pub fn symbolic_solver_is_builtin(solver: &str) -> bool {
65    BUILTIN_SYMBOLIC_SOLVERS.contains(&solver)
66}
67
68/// Returns a warning when a configured symbolic solver portfolio has unavailable entries.
69pub fn symbolic_solver_portfolio_availability_warning(config: &SymbolicConfig) -> Option<String> {
70    runtime::solver_portfolio_availability_warning(config)
71}
72
73#[derive(Clone, Copy, Debug, PartialEq, Eq)]
74enum SymbolicVmCheatcode {
75    CreateAddress,
76    CreateBool,
77    CreateBytes,
78    CreateBytesSized,
79    CreateBytesFixed(usize),
80    CreateCalldata,
81    CreateInt,
82    CreateIntBits(usize),
83    CreateString,
84    CreateStringSized,
85    CreateUint,
86    CreateUintBits(usize),
87    EnableSymbolicStorage,
88    SnapshotStorage,
89    SnapshotState,
90}
91
92impl SymbolicVmCheatcode {
93    fn from_selector(selector: [u8; 4]) -> Option<Self> {
94        match selector {
95            SymbolicVm::createAddressCall::SELECTOR => Some(Self::CreateAddress),
96            SymbolicVm::createBoolCall::SELECTOR => Some(Self::CreateBool),
97            SymbolicVm::createBytes_0Call::SELECTOR => Some(Self::CreateBytes),
98            SymbolicVm::createBytes_1Call::SELECTOR => Some(Self::CreateBytesSized),
99            SymbolicVm::createCalldataCall::SELECTOR => Some(Self::CreateCalldata),
100            SymbolicVm::createIntCall::SELECTOR => Some(Self::CreateInt),
101            SymbolicVm::createString_0Call::SELECTOR => Some(Self::CreateString),
102            SymbolicVm::createString_1Call::SELECTOR => Some(Self::CreateStringSized),
103            SymbolicVm::createUintCall::SELECTOR => Some(Self::CreateUint),
104            SymbolicVm::enableSymbolicStorageCall::SELECTOR
105            | Vm::setArbitraryStorage_0Call::SELECTOR => Some(Self::EnableSymbolicStorage),
106            SymbolicVm::snapshotStorageCall::SELECTOR => Some(Self::SnapshotStorage),
107            Vm::snapshotStateCall::SELECTOR => Some(Self::SnapshotState),
108            _ => {
109                for &(bits, candidate) in symbolic_create_uint_selectors() {
110                    if selector == candidate {
111                        return Some(Self::CreateUintBits(bits));
112                    }
113                }
114                for &(bits, candidate) in symbolic_create_int_selectors() {
115                    if selector == candidate {
116                        return Some(Self::CreateIntBits(bits));
117                    }
118                }
119                for &(bytes, candidate) in symbolic_create_bytes_selectors() {
120                    if selector == candidate {
121                        return Some(Self::CreateBytesFixed(bytes));
122                    }
123                }
124                None
125            }
126        }
127    }
128
129    const fn min_input_words(self) -> usize {
130        match self {
131            Self::CreateUint
132            | Self::CreateInt
133            | Self::CreateBytesSized
134            | Self::CreateStringSized
135            | Self::EnableSymbolicStorage
136            | Self::SnapshotStorage => 1,
137            Self::CreateAddress
138            | Self::CreateBool
139            | Self::CreateBytes
140            | Self::CreateBytesFixed(_)
141            | Self::CreateCalldata
142            | Self::CreateIntBits(_)
143            | Self::CreateString
144            | Self::CreateUintBits(_)
145            | Self::SnapshotState => 0,
146        }
147    }
148}
149
150fn symbolic_create_uint_selectors() -> &'static [(usize, [u8; 4]); 32] {
151    static SELECTORS: [(usize, [u8; 4]); 32] = [
152        (8, SymbolicVm::createUint8Call::SELECTOR),
153        (16, SymbolicVm::createUint16Call::SELECTOR),
154        (24, SymbolicVm::createUint24Call::SELECTOR),
155        (32, SymbolicVm::createUint32Call::SELECTOR),
156        (40, SymbolicVm::createUint40Call::SELECTOR),
157        (48, SymbolicVm::createUint48Call::SELECTOR),
158        (56, SymbolicVm::createUint56Call::SELECTOR),
159        (64, SymbolicVm::createUint64Call::SELECTOR),
160        (72, SymbolicVm::createUint72Call::SELECTOR),
161        (80, SymbolicVm::createUint80Call::SELECTOR),
162        (88, SymbolicVm::createUint88Call::SELECTOR),
163        (96, SymbolicVm::createUint96Call::SELECTOR),
164        (104, SymbolicVm::createUint104Call::SELECTOR),
165        (112, SymbolicVm::createUint112Call::SELECTOR),
166        (120, SymbolicVm::createUint120Call::SELECTOR),
167        (128, SymbolicVm::createUint128Call::SELECTOR),
168        (136, SymbolicVm::createUint136Call::SELECTOR),
169        (144, SymbolicVm::createUint144Call::SELECTOR),
170        (152, SymbolicVm::createUint152Call::SELECTOR),
171        (160, SymbolicVm::createUint160Call::SELECTOR),
172        (168, SymbolicVm::createUint168Call::SELECTOR),
173        (176, SymbolicVm::createUint176Call::SELECTOR),
174        (184, SymbolicVm::createUint184Call::SELECTOR),
175        (192, SymbolicVm::createUint192Call::SELECTOR),
176        (200, SymbolicVm::createUint200Call::SELECTOR),
177        (208, SymbolicVm::createUint208Call::SELECTOR),
178        (216, SymbolicVm::createUint216Call::SELECTOR),
179        (224, SymbolicVm::createUint224Call::SELECTOR),
180        (232, SymbolicVm::createUint232Call::SELECTOR),
181        (240, SymbolicVm::createUint240Call::SELECTOR),
182        (248, SymbolicVm::createUint248Call::SELECTOR),
183        (256, SymbolicVm::createUint256Call::SELECTOR),
184    ];
185    &SELECTORS
186}
187
188fn symbolic_create_int_selectors() -> &'static [(usize, [u8; 4]); 32] {
189    static SELECTORS: [(usize, [u8; 4]); 32] = [
190        (8, SymbolicVm::createInt8Call::SELECTOR),
191        (16, SymbolicVm::createInt16Call::SELECTOR),
192        (24, SymbolicVm::createInt24Call::SELECTOR),
193        (32, SymbolicVm::createInt32Call::SELECTOR),
194        (40, SymbolicVm::createInt40Call::SELECTOR),
195        (48, SymbolicVm::createInt48Call::SELECTOR),
196        (56, SymbolicVm::createInt56Call::SELECTOR),
197        (64, SymbolicVm::createInt64Call::SELECTOR),
198        (72, SymbolicVm::createInt72Call::SELECTOR),
199        (80, SymbolicVm::createInt80Call::SELECTOR),
200        (88, SymbolicVm::createInt88Call::SELECTOR),
201        (96, SymbolicVm::createInt96Call::SELECTOR),
202        (104, SymbolicVm::createInt104Call::SELECTOR),
203        (112, SymbolicVm::createInt112Call::SELECTOR),
204        (120, SymbolicVm::createInt120Call::SELECTOR),
205        (128, SymbolicVm::createInt128Call::SELECTOR),
206        (136, SymbolicVm::createInt136Call::SELECTOR),
207        (144, SymbolicVm::createInt144Call::SELECTOR),
208        (152, SymbolicVm::createInt152Call::SELECTOR),
209        (160, SymbolicVm::createInt160Call::SELECTOR),
210        (168, SymbolicVm::createInt168Call::SELECTOR),
211        (176, SymbolicVm::createInt176Call::SELECTOR),
212        (184, SymbolicVm::createInt184Call::SELECTOR),
213        (192, SymbolicVm::createInt192Call::SELECTOR),
214        (200, SymbolicVm::createInt200Call::SELECTOR),
215        (208, SymbolicVm::createInt208Call::SELECTOR),
216        (216, SymbolicVm::createInt216Call::SELECTOR),
217        (224, SymbolicVm::createInt224Call::SELECTOR),
218        (232, SymbolicVm::createInt232Call::SELECTOR),
219        (240, SymbolicVm::createInt240Call::SELECTOR),
220        (248, SymbolicVm::createInt248Call::SELECTOR),
221        (256, SymbolicVm::createInt256Call::SELECTOR),
222    ];
223    &SELECTORS
224}
225
226fn symbolic_create_bytes_selectors() -> &'static [(usize, [u8; 4]); 32] {
227    static SELECTORS: [(usize, [u8; 4]); 32] = [
228        (1, SymbolicVm::createBytes1Call::SELECTOR),
229        (2, SymbolicVm::createBytes2Call::SELECTOR),
230        (3, SymbolicVm::createBytes3Call::SELECTOR),
231        (4, SymbolicVm::createBytes4Call::SELECTOR),
232        (5, SymbolicVm::createBytes5Call::SELECTOR),
233        (6, SymbolicVm::createBytes6Call::SELECTOR),
234        (7, SymbolicVm::createBytes7Call::SELECTOR),
235        (8, SymbolicVm::createBytes8Call::SELECTOR),
236        (9, SymbolicVm::createBytes9Call::SELECTOR),
237        (10, SymbolicVm::createBytes10Call::SELECTOR),
238        (11, SymbolicVm::createBytes11Call::SELECTOR),
239        (12, SymbolicVm::createBytes12Call::SELECTOR),
240        (13, SymbolicVm::createBytes13Call::SELECTOR),
241        (14, SymbolicVm::createBytes14Call::SELECTOR),
242        (15, SymbolicVm::createBytes15Call::SELECTOR),
243        (16, SymbolicVm::createBytes16Call::SELECTOR),
244        (17, SymbolicVm::createBytes17Call::SELECTOR),
245        (18, SymbolicVm::createBytes18Call::SELECTOR),
246        (19, SymbolicVm::createBytes19Call::SELECTOR),
247        (20, SymbolicVm::createBytes20Call::SELECTOR),
248        (21, SymbolicVm::createBytes21Call::SELECTOR),
249        (22, SymbolicVm::createBytes22Call::SELECTOR),
250        (23, SymbolicVm::createBytes23Call::SELECTOR),
251        (24, SymbolicVm::createBytes24Call::SELECTOR),
252        (25, SymbolicVm::createBytes25Call::SELECTOR),
253        (26, SymbolicVm::createBytes26Call::SELECTOR),
254        (27, SymbolicVm::createBytes27Call::SELECTOR),
255        (28, SymbolicVm::createBytes28Call::SELECTOR),
256        (29, SymbolicVm::createBytes29Call::SELECTOR),
257        (30, SymbolicVm::createBytes30Call::SELECTOR),
258        (31, SymbolicVm::createBytes31Call::SELECTOR),
259        (32, SymbolicVm::createBytes32Call::SELECTOR),
260    ];
261    &SELECTORS
262}
263
264/// Outcome of a symbolic test execution.
265///
266/// The forge runner treats `Safe` as a passing symbolic test, `Counterexample` as a
267/// candidate failure that must be replayed concretely, and `Incomplete` as a failing
268/// test because the symbolic engine could not prove the property with the supported
269/// semantics and configured resource limits.
270#[derive(Clone, Debug)]
271pub enum SymbolicRunResult {
272    /// All explored paths completed without a feasible failure.
273    Safe {
274        /// Execution counters collected during the run.
275        stats: SymbolicStats,
276        /// One concrete successful input, when requested by the caller.
277        success_input: Option<SymbolicConcreteInput>,
278    },
279    /// A feasible failure was found.
280    Counterexample {
281        /// ABI-typed argument values extracted from the solver model.
282        args: Vec<DynSolValue>,
283        /// ABI-encoded calldata for the failing invocation.
284        calldata: Bytes,
285        /// Execution counters collected before the counterexample was returned.
286        stats: SymbolicStats,
287    },
288    /// Execution was intentionally stopped because V1 semantics were insufficient.
289    Incomplete {
290        /// Category describing why symbolic execution stopped before proving the test.
291        kind: SymbolicStopReason,
292        /// Human-readable explanation of the unsupported construct or exhausted limit.
293        reason: String,
294        /// Execution counters collected before execution stopped.
295        stats: SymbolicStats,
296    },
297}
298
299/// One concrete symbolic input materialized from a solver model.
300#[derive(Clone, Debug)]
301pub struct SymbolicConcreteInput {
302    /// ABI-typed argument values extracted from the solver model.
303    pub args: Vec<DynSolValue>,
304    /// ABI-encoded calldata for replay.
305    pub calldata: Bytes,
306}
307
308/// A concrete invariant target selected from Foundry's invariant discovery.
309#[derive(Clone, Debug)]
310pub struct SymbolicInvariantTarget {
311    /// Address that receives the sequence call.
312    pub address: Address,
313    /// Human-readable contract identifier used in counterexample rendering.
314    pub contract_name: Option<String>,
315    /// ABI function invoked with symbolic arguments.
316    pub function: Function,
317}
318
319/// Input for bounded symbolic invariant execution.
320pub struct SymbolicInvariantRunInput<'a, FEN: FoundryEvmNetwork> {
321    /// Concrete Foundry executor used as the source of deployed bytecode and backend state.
322    pub executor: &'a Executor<FEN>,
323    /// Address of the deployed invariant test contract.
324    pub invariant_address: Address,
325    /// Default sender used when invariant targeting does not configure senders.
326    pub sender: Address,
327    /// Invariant function checked after each symbolic sequence step.
328    pub invariant: &'a Function,
329    /// Optional `afterInvariant` hook to execute after a passing invariant check.
330    pub after_invariant: Option<&'a Function>,
331    /// Concrete target/selector set discovered by Foundry invariant targeting.
332    pub targets: Vec<SymbolicInvariantTarget>,
333    /// Concrete sender set discovered by Foundry invariant targeting.
334    pub senders: Vec<Address>,
335    /// Sender addresses excluded by Foundry invariant targeting.
336    pub excluded_senders: Vec<Address>,
337    /// Maximum number of sequence calls to execute.
338    pub depth: usize,
339    /// Concrete invariant check interval. `0` means only check at sequence end.
340    pub check_interval: u32,
341    /// Whether ordinary target-call reverts should be reported as failures.
342    pub fail_on_revert: bool,
343    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
344    pub ffi_enabled: bool,
345}
346
347/// One concrete storage value required to replay a symbolic invariant candidate.
348#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
349pub struct SymbolicStorageAssignment {
350    /// Account whose storage slot should be initialized.
351    pub address: Address,
352    /// Concrete storage slot.
353    pub slot: U256,
354    /// Concrete value extracted from the solver model.
355    pub value: U256,
356}
357
358/// Outcome of bounded symbolic invariant execution.
359#[derive(Clone, Debug)]
360pub enum SymbolicInvariantRunResult {
361    /// No feasible invariant failure was found within the configured sequence depth.
362    Safe(SymbolicStats),
363    /// A feasible invariant or handler failure was found.
364    Counterexample {
365        /// Which part of the invariant run produced the failure.
366        kind: SymbolicInvariantCounterexampleKind,
367        /// Concrete sequence extracted from the solver model.
368        sequence: Vec<SymbolicInvariantStep>,
369        /// Concrete setup-storage values needed for replay.
370        storage: Vec<SymbolicStorageAssignment>,
371        /// Execution counters collected before the counterexample was returned.
372        stats: SymbolicStats,
373    },
374    /// Execution stopped before proving the invariant.
375    Incomplete {
376        /// Category describing why symbolic execution stopped.
377        kind: SymbolicStopReason,
378        /// Human-readable explanation of the unsupported construct or exhausted limit.
379        reason: String,
380        /// Execution counters collected before execution stopped.
381        stats: SymbolicStats,
382    },
383}
384
385/// Part of a symbolic invariant run that produced a replayable counterexample.
386#[derive(Clone, Copy, Debug, PartialEq, Eq)]
387pub enum SymbolicInvariantCounterexampleKind {
388    /// An `invariant_*` or `afterInvariant` check failed.
389    Predicate,
390    /// A fuzzed target/handler call failed with an assertion.
391    Handler,
392}
393
394/// One concrete step in a symbolic invariant counterexample sequence.
395#[derive(Clone, Debug)]
396pub struct SymbolicInvariantStep {
397    /// Sender used for the call.
398    pub sender: Address,
399    /// Target address called by the sequence step.
400    pub address: Address,
401    /// Human-readable contract identifier, when known.
402    pub contract_name: Option<String>,
403    /// ABI function name.
404    pub function_name: String,
405    /// ABI function signature.
406    pub signature: String,
407    /// ABI-typed arguments extracted from the solver model.
408    pub args: Vec<DynSolValue>,
409    /// ABI-encoded calldata for replay.
410    pub calldata: Bytes,
411}
412
413/// High-level reason a symbolic run stopped without a proof or replayed counterexample.
414#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
415pub enum SymbolicStopReason {
416    /// The executor reached a supported-but-incomplete semantic boundary.
417    Stuck,
418    /// Every explored execution path ended in an ordinary revert.
419    RevertAll,
420    /// The solver timed out or returned `unknown`.
421    Timeout,
422    /// An internal engine, backend, or solver process error occurred.
423    Error,
424}
425
426/// Symbolic execution counters.
427#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
428pub struct SymbolicStats {
429    /// Number of explored symbolic paths.
430    pub paths: usize,
431    /// Number of normalized solver queries issued during the run.
432    pub solver_queries: usize,
433    /// Number of queries sent to the SMT backend after local fast paths.
434    #[serde(default)]
435    pub smt_queries: usize,
436    /// Number of satisfiability checks requested by the executor.
437    #[serde(default)]
438    pub sat_queries: usize,
439    /// Number of concrete model requests requested by the executor.
440    #[serde(default)]
441    pub model_queries: usize,
442    /// Number of satisfiability checks served from the normalized cache.
443    #[serde(default)]
444    pub sat_cache_hits: usize,
445    /// Number of model requests served from the normalized model cache.
446    #[serde(default)]
447    pub model_cache_hits: usize,
448    /// Number of satisfiable witnesses produced by local hard-arithmetic search.
449    #[serde(default)]
450    pub heuristic_witnesses: usize,
451    /// Wall-clock time spent waiting on backend solver subprocesses, in milliseconds.
452    #[serde(default)]
453    pub solver_time_ms: u64,
454    /// Total SMT-LIB input bytes sent to backend solver subprocesses.
455    #[serde(default)]
456    pub smt_input_bytes: u64,
457    /// Largest single SMT-LIB query input sent to a backend solver subprocess, in bytes.
458    #[serde(default)]
459    pub smt_max_query_bytes: u64,
460    /// Wall-clock time spent building SMT-LIB query strings, in milliseconds.
461    #[serde(default)]
462    pub smt_build_time_ms: u64,
463    /// Longest single backend solver subprocess query, in milliseconds.
464    #[serde(default)]
465    pub smt_max_query_time_ms: u64,
466}
467
468/// SMT-LIB-backed symbolic executor.
469///
470/// This executor is intentionally separate from the concrete revm executor used by
471/// Foundry. It consumes bytecode and state from an existing [`Executor`], explores
472/// symbolic branches, and returns either a proof result, a counterexample candidate,
473/// or an incomplete result.
474pub struct SymbolicExecutor {
475    config: SymbolicConfig,
476    cx: runtime::SymCx,
477    solver: Box<dyn runtime::SymbolicSolver>,
478    deferred_incomplete: Option<DeferredIncomplete>,
479    deadline: Option<Instant>,
480}
481
482#[derive(Clone, Copy, Debug)]
483enum DeferredIncomplete {
484    Unsupported(&'static str),
485    SolverUnknown,
486}
487
488#[cfg(test)]
489mod tests;
foundry_evm_symbolic/lib.rs

foundry_evm_symbolic/
lib.rs
