foundry_config/
symbolic.rs

1//! Configuration for symbolic testing.
2
3use serde::{Deserialize, Serialize};
4use std::collections::BTreeMap;
5
6/// Storage modelling mode for symbolic tests.
7#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
8#[serde(rename_all = "snake_case")]
9pub enum SymbolicStorageLayout {
10    /// Model Solidity storage layout precisely where the symbolic executor knows the layout shape.
11    #[default]
12    Solidity,
13    /// Treat every storage read as potentially arbitrary symbolic storage.
14    Generic,
15    /// Treat unwritten symbolic storage reads as zero.
16    ZeroInit,
17}
18
19/// Pending symbolic path exploration order.
20#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
21#[serde(rename_all = "snake_case")]
22pub enum SymbolicExplorationOrder {
23    /// Explore pending paths in first-in, first-out order.
24    #[default]
25    Bfs,
26    /// Explore pending paths in last-in, first-out order.
27    Dfs,
28}
29
30/// Configuration for symbolic testing.
31#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
32pub struct SymbolicConfig {
33    /// Whether symbolic tests are enabled.
34    pub enabled: bool,
35    /// Whether fuzz tests should be symbolically concretized into fuzz corpus seeds.
36    pub seed_corpus: bool,
37    /// Whether fuzz corpus seeds should guide symbolic fuzz-test exploration.
38    pub use_fuzz_corpus: bool,
39    /// Maximum number of fuzz corpus seeds to import for one symbolic run.
40    pub corpus_seed_limit: usize,
41    /// Whether fuzz branch frontiers should guide targeted symbolic fuzz-test seeding.
42    pub use_fuzz_frontiers: bool,
43    /// Maximum number of fuzz branch frontiers to try for one symbolic run.
44    pub frontier_limit: usize,
45    /// Fuzz branch frontier artifact IDs to import. Empty imports by artifact order.
46    #[serde(default, skip_serializing_if = "Vec::is_empty")]
47    pub frontier_ids: Vec<u64>,
48    /// Fuzz branch frontier comparison program counters to import. Empty imports any PC.
49    #[serde(default, skip_serializing_if = "Vec::is_empty")]
50    pub frontier_pcs: Vec<usize>,
51    /// Fuzz branch frontier calldata selectors to import. Empty imports any selector.
52    #[serde(default, skip_serializing_if = "Vec::is_empty")]
53    pub frontier_selectors: Vec<String>,
54    /// Solver executable to invoke.
55    pub solver: String,
56    /// Exact solver command to invoke. When set, this overrides `solver`.
57    #[serde(default, skip_serializing_if = "Option::is_none")]
58    pub solver_command: Option<String>,
59    /// Solver names or exact commands to race in parallel. Ignored when `solver_command` is set.
60    #[serde(default, skip_serializing_if = "Vec::is_empty")]
61    pub solver_portfolio: Vec<String>,
62    /// Optional SMT solver timeout in seconds. Also bounds wall-clock symbolic invariant
63    /// exploration before falling back to invariant fuzzing.
64    pub timeout: Option<u32>,
65    /// Halmos-compatible loop bound accepted by config and annotations.
66    #[serde(default, rename = "loop", skip_serializing_if = "Option::is_none")]
67    pub loop_bound: Option<u32>,
68    /// Halmos-compatible execution depth alias. When set, this overrides `max_depth`.
69    #[serde(default, skip_serializing_if = "Option::is_none")]
70    pub depth: Option<u32>,
71    /// Halmos-compatible path width alias. When set, this overrides `max_paths`.
72    #[serde(default, skip_serializing_if = "Option::is_none")]
73    pub width: Option<u32>,
74    /// Maximum number of opcodes to execute along a path.
75    pub max_depth: u32,
76    /// Maximum number of symbolic paths to explore.
77    pub max_paths: u32,
78    /// Maximum number of calls in a bounded symbolic invariant sequence.
79    pub invariant_depth: u32,
80    /// Order used to select the next pending symbolic path.
81    #[serde(default)]
82    pub exploration_order: SymbolicExplorationOrder,
83    /// Maximum number of solver queries.
84    pub max_solver_queries: u32,
85    /// Default bounded length for dynamic ABI inputs.
86    pub default_dynamic_length: u32,
87    /// Maximum permitted bounded length for a dynamic ABI input.
88    pub max_dynamic_length: u32,
89    /// Per-dynamic-leaf bounded lengths, applied in ABI traversal order.
90    pub array_lengths: Vec<u32>,
91    /// Per-symbolic-input bounded lengths keyed by ABI argument name or generated symbolic name.
92    #[serde(default, skip_serializing_if = "BTreeMap::is_empty")]
93    pub dynamic_lengths: BTreeMap<String, Vec<u32>>,
94    /// Default bounded lengths for dynamic ABI arrays without an explicit length.
95    #[serde(default, skip_serializing_if = "Vec::is_empty")]
96    pub default_array_lengths: Vec<u32>,
97    /// Default bounded lengths for ABI `bytes` and `string` values without an explicit length.
98    #[serde(default, skip_serializing_if = "Vec::is_empty")]
99    pub default_bytes_lengths: Vec<u32>,
100    /// Maximum symbolic calldata size in bytes.
101    pub max_calldata_bytes: u32,
102    /// Whether symbolic call targets may be expanded over known deployed contracts.
103    pub symbolic_call_targets: bool,
104    /// Whether to dump SMT-LIB queries before invoking the configured solver.
105    pub dump_smt: bool,
106    /// Storage modelling mode used for symbolic storage reads.
107    pub storage_layout: SymbolicStorageLayout,
108}
109
110impl Default for SymbolicConfig {
111    fn default() -> Self {
112        Self {
113            enabled: false,
114            seed_corpus: false,
115            use_fuzz_corpus: false,
116            corpus_seed_limit: 32,
117            use_fuzz_frontiers: false,
118            frontier_limit: 256,
119            frontier_ids: Vec::new(),
120            frontier_pcs: Vec::new(),
121            frontier_selectors: Vec::new(),
122            solver: "z3".to_string(),
123            solver_command: None,
124            solver_portfolio: Vec::new(),
125            timeout: Some(30),
126            loop_bound: None,
127            depth: None,
128            width: None,
129            max_depth: 10_000,
130            max_paths: 1_024,
131            invariant_depth: 10,
132            exploration_order: SymbolicExplorationOrder::default(),
133            max_solver_queries: 10_000,
134            default_dynamic_length: 2,
135            max_dynamic_length: 256,
136            array_lengths: Vec::new(),
137            dynamic_lengths: BTreeMap::new(),
138            default_array_lengths: Vec::new(),
139            default_bytes_lengths: Vec::new(),
140            max_calldata_bytes: 4_096,
141            symbolic_call_targets: false,
142            dump_smt: false,
143            storage_layout: SymbolicStorageLayout::Solidity,
144        }
145    }
146}
147
148impl SymbolicConfig {
149    /// Returns the effective per-path opcode depth limit used by the symbolic executor.
150    ///
151    /// The Halmos-compatible `depth` alias takes precedence over `max_depth` so inline
152    /// compatibility annotations and native Foundry config resolve to one internal limit.
153    pub fn execution_depth(&self) -> u32 {
154        self.depth.unwrap_or(self.max_depth)
155    }
156
157    /// Returns the effective symbolic path width limit used by the symbolic executor.
158    ///
159    /// The Halmos-compatible `width` alias takes precedence over `max_paths` so both
160    /// configuration spellings feed the same path exploration budget.
161    pub fn path_width(&self) -> u32 {
162        self.width.unwrap_or(self.max_paths)
163    }
164}
165
166#[cfg(test)]
167mod tests {
168    use super::*;
169
170    #[test]
171    fn missing_exploration_order_defaults_to_bfs() {
172        let value = serde_json::json!({
173            "enabled": false,
174            "seed_corpus": false,
175            "use_fuzz_corpus": false,
176            "corpus_seed_limit": 32,
177            "use_fuzz_frontiers": false,
178            "frontier_limit": 256,
179            "frontier_ids": [],
180            "frontier_pcs": [],
181            "frontier_selectors": [],
182            "solver": "z3",
183            "timeout": 30,
184            "max_depth": 10000,
185            "max_paths": 1024,
186            "invariant_depth": 10,
187            "max_solver_queries": 10000,
188            "default_dynamic_length": 2,
189            "max_dynamic_length": 256,
190            "array_lengths": [],
191            "max_calldata_bytes": 4096,
192            "symbolic_call_targets": false,
193            "dump_smt": false,
194            "storage_layout": "solidity"
195        });
196
197        let config: SymbolicConfig = serde_json::from_value(value).unwrap();
198
199        assert_eq!(config.exploration_order, SymbolicExplorationOrder::Bfs);
200    }
201}
foundry_config/symbolic.rs

foundry_config/
symbolic.rs
