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

foundry_config/
symbolic.rs
