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::{Address, B256, Bytes, I256, U256, U512, hex, keccak256};
8use alloy_signer::SignerSync;
9use alloy_signer_local::{
10    PrivateKeySigner,
11    coins_bip39::{English, Wordlist},
12};
13use base64::prelude::*;
14use foundry_config::{
15    SymbolicConfig, SymbolicExplorationOrder, SymbolicStorageLayout, split_quoted_args,
16};
17use foundry_evm::{
18    constants::{CHEATCODE_ADDRESS, DEFAULT_CREATE2_DEPLOYER, HARDHAT_CONSOLE_ADDRESS},
19    core::{backend::DatabaseExt, evm::FoundryEvmNetwork},
20    executors::Executor,
21    revm::{
22        bytecode::opcode,
23        context::{Block, Transaction},
24        database::DatabaseRef,
25        precompile::{blake2, bn254, hash, identity, modexp, secp256k1},
26        primitives::hardfork::SpecId,
27    },
28};
29use serde::{Deserialize, Serialize};
30use std::{
31    collections::{BTreeMap, BTreeSet, VecDeque},
32    fmt::{self, Write as _},
33    io::{Read, Write},
34    ops::{Deref, DerefMut},
35    path::{Path, PathBuf},
36    process::{Command, Stdio},
37    sync::{
38        Arc,
39        atomic::{AtomicBool, Ordering},
40        mpsc,
41    },
42    thread,
43    time::{Duration, Instant, SystemTime, UNIX_EPOCH},
44};
45use thiserror::Error;
46use tracing::{debug, trace, trace_span, warn};
47
48macro_rules! selector {
49    ($signature:literal) => {{
50        let hash = keccak256($signature);
51        [hash[0], hash[1], hash[2], hash[3]]
52    }};
53}
54
55mod consts;
56pub use consts::BUILTIN_SYMBOLIC_SOLVERS;
57pub(crate) use consts::*;
58
59mod abi;
60mod executor;
61mod runtime;
62
63pub use runtime::{PortfolioDiagnostics, SymbolicError, SymbolicRunInput};
64
65/// Returns whether `solver` is one of Foundry's semantic symbolic solver names.
66pub fn symbolic_solver_is_builtin(solver: &str) -> bool {
67    BUILTIN_SYMBOLIC_SOLVERS.contains(&solver)
68}
69
70/// Returns a warning when a configured symbolic solver portfolio has unavailable entries.
71pub fn symbolic_solver_portfolio_availability_warning(config: &SymbolicConfig) -> Option<String> {
72    runtime::solver_portfolio_availability_warning(config)
73}
74
75/// Returns the `selector_for` symbolic public API helper result.
76fn selector_for(signature: &str) -> [u8; 4] {
77    let hash = keccak256(signature);
78    [hash[0], hash[1], hash[2], hash[3]]
79}
80
81/// Outcome of a symbolic test execution.
82///
83/// The forge runner treats `Safe` as a passing symbolic test, `Counterexample` as a
84/// candidate failure that must be replayed concretely, and `Incomplete` as a failing
85/// test because the symbolic engine could not prove the property with the supported
86/// semantics and configured resource limits.
87#[derive(Clone, Debug)]
88pub enum SymbolicRunResult {
89    /// All explored paths completed without a feasible failure.
90    Safe(SymbolicStats),
91    /// A feasible failure was found.
92    Counterexample {
93        /// ABI-typed argument values extracted from the solver model.
94        args: Vec<DynSolValue>,
95        /// ABI-encoded calldata for the failing invocation.
96        calldata: Bytes,
97        /// Execution counters collected before the counterexample was returned.
98        stats: SymbolicStats,
99    },
100    /// Execution was intentionally stopped because V1 semantics were insufficient.
101    Incomplete {
102        /// Category describing why symbolic execution stopped before proving the test.
103        kind: SymbolicStopReason,
104        /// Human-readable explanation of the unsupported construct or exhausted limit.
105        reason: String,
106        /// Execution counters collected before execution stopped.
107        stats: SymbolicStats,
108    },
109}
110
111/// A concrete invariant target selected from Foundry's invariant discovery.
112#[derive(Clone, Debug)]
113pub struct SymbolicInvariantTarget {
114    /// Address that receives the sequence call.
115    pub address: Address,
116    /// Human-readable contract identifier used in counterexample rendering.
117    pub contract_name: Option<String>,
118    /// ABI function invoked with symbolic arguments.
119    pub function: Function,
120}
121
122/// Input for bounded symbolic invariant execution.
123pub struct SymbolicInvariantRunInput<'a, FEN: FoundryEvmNetwork> {
124    /// Concrete Foundry executor used as the source of deployed bytecode and backend state.
125    pub executor: &'a Executor<FEN>,
126    /// Address of the deployed invariant test contract.
127    pub invariant_address: Address,
128    /// Default sender used when invariant targeting does not configure senders.
129    pub sender: Address,
130    /// Invariant function checked after each symbolic sequence step.
131    pub invariant: &'a Function,
132    /// Optional `afterInvariant` hook to execute after a passing invariant check.
133    pub after_invariant: Option<&'a Function>,
134    /// Concrete target/selector set discovered by Foundry invariant targeting.
135    pub targets: Vec<SymbolicInvariantTarget>,
136    /// Concrete sender set discovered by Foundry invariant targeting.
137    pub senders: Vec<Address>,
138    /// Maximum number of sequence calls to execute.
139    pub depth: usize,
140    /// Whether ordinary target-call reverts should be reported as failures.
141    pub fail_on_revert: bool,
142    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
143    pub ffi_enabled: bool,
144}
145
146/// Outcome of bounded symbolic invariant execution.
147#[derive(Clone, Debug)]
148pub enum SymbolicInvariantRunResult {
149    /// No feasible invariant failure was found within the configured sequence depth.
150    Safe(SymbolicStats),
151    /// A feasible invariant or handler failure was found.
152    Counterexample {
153        /// Concrete sequence extracted from the solver model.
154        sequence: Vec<SymbolicInvariantStep>,
155        /// Execution counters collected before the counterexample was returned.
156        stats: SymbolicStats,
157    },
158    /// Execution stopped before proving the invariant.
159    Incomplete {
160        /// Category describing why symbolic execution stopped.
161        kind: SymbolicStopReason,
162        /// Human-readable explanation of the unsupported construct or exhausted limit.
163        reason: String,
164        /// Execution counters collected before execution stopped.
165        stats: SymbolicStats,
166    },
167}
168
169/// One concrete step in a symbolic invariant counterexample sequence.
170#[derive(Clone, Debug)]
171pub struct SymbolicInvariantStep {
172    /// Sender used for the call.
173    pub sender: Address,
174    /// Target address called by the sequence step.
175    pub address: Address,
176    /// Human-readable contract identifier, when known.
177    pub contract_name: Option<String>,
178    /// ABI function name.
179    pub function_name: String,
180    /// ABI function signature.
181    pub signature: String,
182    /// ABI-typed arguments extracted from the solver model.
183    pub args: Vec<DynSolValue>,
184    /// ABI-encoded calldata for replay.
185    pub calldata: Bytes,
186}
187
188/// High-level reason a symbolic run stopped without a proof or replayed counterexample.
189#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
190pub enum SymbolicStopReason {
191    /// The executor reached a supported-but-incomplete semantic boundary.
192    Stuck,
193    /// Every explored execution path ended in an ordinary revert.
194    RevertAll,
195    /// The solver timed out or returned `unknown`.
196    Timeout,
197    /// An internal engine, backend, or solver process error occurred.
198    Error,
199}
200
201/// Symbolic execution counters.
202#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
203pub struct SymbolicStats {
204    /// Number of explored symbolic paths.
205    pub paths: usize,
206    /// Number of normalized solver queries issued during the run.
207    pub solver_queries: usize,
208    /// Number of queries sent to the SMT backend after local fast paths.
209    #[serde(default)]
210    pub smt_queries: usize,
211    /// Number of satisfiability checks requested by the executor.
212    #[serde(default)]
213    pub sat_queries: usize,
214    /// Number of concrete model requests requested by the executor.
215    #[serde(default)]
216    pub model_queries: usize,
217    /// Number of satisfiability checks served from the normalized cache.
218    #[serde(default)]
219    pub sat_cache_hits: usize,
220    /// Number of model requests served from the normalized model cache.
221    #[serde(default)]
222    pub model_cache_hits: usize,
223    /// Number of satisfiable witnesses produced by local hard-arithmetic search.
224    #[serde(default)]
225    pub heuristic_witnesses: usize,
226    /// Wall-clock time spent waiting on backend solver subprocesses, in milliseconds.
227    #[serde(default)]
228    pub solver_time_ms: u64,
229}
230
231/// SMT-LIB-backed symbolic executor.
232///
233/// This executor is intentionally separate from the concrete revm executor used by
234/// Foundry. It consumes bytecode and state from an existing [`Executor`], explores
235/// symbolic branches, and returns either a proof result, a counterexample candidate,
236/// or an incomplete result.
237pub struct SymbolicExecutor {
238    config: SymbolicConfig,
239    solver: Box<dyn runtime::SymbolicSolver>,
240}
241
242#[cfg(test)]
243mod tests;
foundry_evm_symbolic/lib.rs

foundry_evm_symbolic/
lib.rs
