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    /// Solver executable to invoke.
36    pub solver: String,
37    /// Exact solver command to invoke. When set, this overrides `solver`.
38    #[serde(default, skip_serializing_if = "Option::is_none")]
39    pub solver_command: Option<String>,
40    /// Solver names or exact commands to race in parallel. Ignored when `solver_command` is set.
41    #[serde(default, skip_serializing_if = "Vec::is_empty")]
42    pub solver_portfolio: Vec<String>,
43    /// Optional timeout in seconds for solver-backed symbolic execution.
44    pub timeout: Option<u32>,
45    /// Halmos-compatible loop bound accepted by config and annotations.
46    #[serde(default, rename = "loop", skip_serializing_if = "Option::is_none")]
47    pub loop_bound: Option<u32>,
48    /// Halmos-compatible execution depth alias. When set, this overrides `max_depth`.
49    #[serde(default, skip_serializing_if = "Option::is_none")]
50    pub depth: Option<u32>,
51    /// Halmos-compatible path width alias. When set, this overrides `max_paths`.
52    #[serde(default, skip_serializing_if = "Option::is_none")]
53    pub width: Option<u32>,
54    /// Maximum number of opcodes to execute along a path.
55    pub max_depth: u32,
56    /// Maximum number of symbolic paths to explore.
57    pub max_paths: u32,
58    /// Maximum number of calls in a bounded symbolic invariant sequence.
59    pub invariant_depth: u32,
60    /// Order used to select the next pending symbolic path.
61    #[serde(default)]
62    pub exploration_order: SymbolicExplorationOrder,
63    /// Maximum number of solver queries.
64    pub max_solver_queries: u32,
65    /// Default bounded length for dynamic ABI inputs.
66    pub default_dynamic_length: u32,
67    /// Maximum permitted bounded length for a dynamic ABI input.
68    pub max_dynamic_length: u32,
69    /// Per-dynamic-leaf bounded lengths, applied in ABI traversal order.
70    pub array_lengths: Vec<u32>,
71    /// Per-symbolic-input bounded lengths keyed by ABI argument name or generated symbolic name.
72    #[serde(default, skip_serializing_if = "BTreeMap::is_empty")]
73    pub dynamic_lengths: BTreeMap<String, Vec<u32>>,
74    /// Default bounded lengths for dynamic ABI arrays without an explicit length.
75    #[serde(default, skip_serializing_if = "Vec::is_empty")]
76    pub default_array_lengths: Vec<u32>,
77    /// Default bounded lengths for ABI `bytes` and `string` values without an explicit length.
78    #[serde(default, skip_serializing_if = "Vec::is_empty")]
79    pub default_bytes_lengths: Vec<u32>,
80    /// Maximum symbolic calldata size in bytes.
81    pub max_calldata_bytes: u32,
82    /// Whether symbolic call targets may be expanded over known deployed contracts.
83    pub symbolic_call_targets: bool,
84    /// Whether to dump SMT-LIB queries before invoking the configured solver.
85    pub dump_smt: bool,
86    /// Storage modelling mode used for symbolic storage reads.
87    pub storage_layout: SymbolicStorageLayout,
88}
89
90impl Default for SymbolicConfig {
91    fn default() -> Self {
92        Self {
93            enabled: false,
94            solver: "z3".to_string(),
95            solver_command: None,
96            solver_portfolio: Vec::new(),
97            timeout: Some(30),
98            loop_bound: None,
99            depth: None,
100            width: None,
101            max_depth: 10_000,
102            max_paths: 1_024,
103            invariant_depth: 10,
104            exploration_order: SymbolicExplorationOrder::default(),
105            max_solver_queries: 10_000,
106            default_dynamic_length: 2,
107            max_dynamic_length: 256,
108            array_lengths: Vec::new(),
109            dynamic_lengths: BTreeMap::new(),
110            default_array_lengths: Vec::new(),
111            default_bytes_lengths: Vec::new(),
112            max_calldata_bytes: 4_096,
113            symbolic_call_targets: false,
114            dump_smt: false,
115            storage_layout: SymbolicStorageLayout::Solidity,
116        }
117    }
118}
119
120impl SymbolicConfig {
121    /// Returns the effective per-path opcode depth limit used by the symbolic executor.
122    ///
123    /// The Halmos-compatible `depth` alias takes precedence over `max_depth` so inline
124    /// compatibility annotations and native Foundry config resolve to one internal limit.
125    pub fn execution_depth(&self) -> u32 {
126        self.depth.unwrap_or(self.max_depth)
127    }
128
129    /// Returns the effective symbolic path width limit used by the symbolic executor.
130    ///
131    /// The Halmos-compatible `width` alias takes precedence over `max_paths` so both
132    /// configuration spellings feed the same path exploration budget.
133    pub fn path_width(&self) -> u32 {
134        self.width.unwrap_or(self.max_paths)
135    }
136}
137
138#[cfg(test)]
139mod tests {
140    use super::*;
141
142    #[test]
143    fn missing_exploration_order_defaults_to_bfs() {
144        let value = serde_json::json!({
145            "enabled": false,
146            "solver": "z3",
147            "timeout": 30,
148            "max_depth": 10000,
149            "max_paths": 1024,
150            "invariant_depth": 10,
151            "max_solver_queries": 10000,
152            "default_dynamic_length": 2,
153            "max_dynamic_length": 256,
154            "array_lengths": [],
155            "max_calldata_bytes": 4096,
156            "symbolic_call_targets": false,
157            "dump_smt": false,
158            "storage_layout": "solidity"
159        });
160
161        let config: SymbolicConfig = serde_json::from_value(value).unwrap();
162
163        assert_eq!(config.exploration_order, SymbolicExplorationOrder::Bfs);
164    }
165}
foundry_config/symbolic.rs

foundry_config/
symbolic.rs
