foundry_bench/
symbolic.rs

1//! Formal symbolic benchmark suite definitions and result parsing.
2
3use crate::results::SymbolicBenchmarkSummary;
4use eyre::{Result, WrapErr};
5use serde::Serialize;
6use serde_json::Value;
7use std::{
8    fs,
9    path::{Path, PathBuf},
10};
11
12const FARCASTER_PATH: &str = "test/FarcasterNativeSymbolic.t.sol";
13const FARCASTER_TEST: &str = include_str!("../fixtures/symbolic/FarcasterNativeSymbolic.t.sol");
14const PREFIX: &str =
15    "FOUNDRY_DYNAMIC_TEST_LINKING=false FOUNDRY_LINT_LINT_ON_BUILD=false FOUNDRY_ISOLATE=false";
16const SOLADY_MATCH: &str = "check_(SaturatingAddEquivalence|SaturatingMulEquivalence|HasDuplicateHashmapCapacityTrickEquivalence|IsPermit2AndValueIsNotInfinityTrickEquivalence|IsNotUint256MaxTrickEquivalence|DelayRestriction|OperationStateDifferentialTrick|CarryBoundsTrick|SafeCastInt256ToIntTrickEquivalence|P256Normalized|AuxPackEquivalence|EcrecoverTrickEquivalence|EcrecoverLoopTrick)";
17
18#[derive(Clone, Copy, Debug, Serialize)]
19#[serde(rename_all = "snake_case")]
20pub enum Fixture {
21    Solady,
22    Angstrom,
23    Farcaster,
24    Generic,
25}
26
27impl Fixture {
28    pub const fn identify(org: &str, repo: &str) -> Self {
29        if org.eq_ignore_ascii_case("vectorized") && repo.eq_ignore_ascii_case("solady") {
30            Self::Solady
31        } else if org.eq_ignore_ascii_case("sorellalabs") && repo.eq_ignore_ascii_case("angstrom") {
32            Self::Angstrom
33        } else if org.eq_ignore_ascii_case("farcasterxyz") && repo.eq_ignore_ascii_case("contracts")
34        {
35            Self::Farcaster
36        } else {
37            Self::Generic
38        }
39    }
40
41    pub fn build_command(self) -> String {
42        format!(
43            "{PREFIX} {}",
44            match self {
45                Self::Angstrom => "forge build --root contracts",
46                _ => "forge build",
47            }
48        )
49    }
50
51    pub fn test_command(self) -> String {
52        match self {
53            Self::Solady => {
54                format!("{PREFIX} forge test --symbolic --json --match-test '{SOLADY_MATCH}'")
55            }
56            Self::Angstrom => format!(
57                "{PREFIX} forge test --root contracts --symbolic --json --symbolic-timeout 5 --match-path test/libraries/X128MathLib.t.sol --match-test check_matchesSolady_fullMulX128"
58            ),
59            Self::Farcaster => format!(
60                "{PREFIX} forge test --symbolic --json --symbolic-timeout 5 --match-path '{FARCASTER_PATH}' --match-test 'check_'"
61            ),
62            Self::Generic => format!("{PREFIX} forge test --symbolic --json"),
63        }
64    }
65}
66
67/// Error-safe installation of the Farcaster benchmark overlay.
68pub struct Overlay {
69    path: Option<PathBuf>,
70}
71
72impl Overlay {
73    pub fn install(root: &Path, fixture: Fixture) -> Result<Self> {
74        if !matches!(fixture, Fixture::Farcaster) {
75            return Ok(Self { path: None });
76        }
77        let path = root.join(FARCASTER_PATH);
78        if path.exists() {
79            eyre::bail!("refusing to overwrite existing {}", path.display());
80        }
81        if let Err(write_err) = fs::write(&path, FARCASTER_TEST) {
82            if let Err(cleanup_err) = fs::remove_file(&path)
83                && cleanup_err.kind() != std::io::ErrorKind::NotFound
84            {
85                eyre::bail!(
86                    "failed to install Farcaster symbolic fixture: {write_err}; failed to remove partially written {}: {cleanup_err}",
87                    path.display()
88                );
89            }
90            return Err(write_err).wrap_err("failed to install Farcaster symbolic fixture");
91        }
92        Ok(Self { path: Some(path) })
93    }
94
95    pub fn finish(mut self) -> Result<()> {
96        self.cleanup()
97    }
98
99    fn cleanup(&mut self) -> Result<()> {
100        if let Some(path) = &self.path {
101            fs::remove_file(path).wrap_err_with(|| {
102                format!("failed to remove symbolic fixture {}", path.display())
103            })?;
104            self.path = None;
105        }
106        Ok(())
107    }
108}
109
110impl Drop for Overlay {
111    fn drop(&mut self) {
112        let _ = self.cleanup();
113    }
114}
115
116#[derive(Clone, Debug, Default, Serialize)]
117pub struct Metrics {
118    pub paths: u64,
119    pub solver_queries: u64,
120    pub smt_queries: u64,
121    pub sat_queries: u64,
122    pub model_queries: u64,
123    pub sat_cache_hits: u64,
124    pub model_cache_hits: u64,
125    pub heuristic_witnesses: u64,
126    pub solver_time_ms: u64,
127    pub smt_input_bytes: Option<u64>,
128    pub smt_max_query_bytes: Option<u64>,
129    pub smt_build_time_ms: Option<u64>,
130    pub smt_max_query_time_ms: Option<u64>,
131    #[serde(skip)]
132    smt_input_bytes_compat: u64,
133    #[serde(skip)]
134    smt_max_query_bytes_compat: u64,
135    #[serde(skip)]
136    smt_build_time_ms_compat: u64,
137    #[serde(skip)]
138    smt_max_query_time_ms_compat: u64,
139}
140
141#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)]
142#[serde(rename_all = "snake_case")]
143pub enum OutcomeStatus {
144    Passed,
145    Failed,
146    Incomplete,
147}
148
149#[derive(Clone, Debug, PartialEq, Eq, Serialize)]
150pub struct TestOutcome {
151    pub suite: String,
152    pub signature: String,
153    pub status: OutcomeStatus,
154}
155
156impl TestOutcome {
157    fn identity(&self) -> String {
158        format!("{}::{}", self.suite, self.signature)
159    }
160}
161
162#[derive(Clone, Debug, Serialize)]
163pub struct ParsedRun {
164    pub outcomes: Vec<TestOutcome>,
165    pub passed: usize,
166    pub failed: usize,
167    pub incomplete: usize,
168    pub metrics: Metrics,
169}
170
171#[derive(Clone, Debug, Serialize)]
172pub struct Sample {
173    pub wall_time_seconds: f64,
174    pub exit_code: i32,
175    #[serde(flatten)]
176    pub run: ParsedRun,
177}
178
179#[derive(Clone, Debug, Serialize)]
180pub struct Sidecar {
181    pub schema: &'static str,
182    pub schema_version: u32,
183    pub fixture: FixtureMetadata,
184    pub samples: Vec<Sample>,
185}
186
187#[derive(Clone, Debug, Serialize)]
188pub struct FixtureMetadata {
189    pub name: Fixture,
190    pub repository: String,
191    pub revision: String,
192    pub build_command: String,
193    pub test_command: String,
194}
195
196impl Sidecar {
197    pub fn new(
198        fixture: Fixture,
199        repository: &str,
200        revision: &str,
201        build_command: &str,
202        test_command: &str,
203        samples: Vec<Sample>,
204    ) -> Self {
205        Self {
206            schema: "foundry:symbolic-benchmark@v1",
207            schema_version: 1,
208            fixture: FixtureMetadata {
209                name: fixture,
210                repository: repository.to_string(),
211                revision: revision.to_string(),
212                build_command: build_command.to_string(),
213                test_command: test_command.to_string(),
214            },
215            samples,
216        }
217    }
218}
219
220pub fn parse(stdout: &[u8]) -> Result<ParsedRun> {
221    let json: Value =
222        serde_json::from_slice(stdout).wrap_err("invalid forge test --json output")?;
223    let suites = json.as_object().ok_or_else(|| eyre::eyre!("expected JSON object"))?;
224    let stable = suites
225        .values()
226        .filter_map(|s| s.get("test_results").and_then(Value::as_object))
227        .flat_map(|r| r.values())
228        .any(|r| r.get("symbolic").is_some());
229    let mut run = ParsedRun {
230        outcomes: Vec::new(),
231        passed: 0,
232        failed: 0,
233        incomplete: 0,
234        metrics: Metrics::default(),
235    };
236    for (suite_name, suite) in suites {
237        let Some(results) = suite.get("test_results").and_then(Value::as_object) else { continue };
238        for (identity, result) in results {
239            let (stats, status) = if stable {
240                let Some(symbolic) = result.get("symbolic") else { continue };
241                if symbolic.get("schema_version").and_then(Value::as_u64) != Some(1) {
242                    eyre::bail!("unknown or missing symbolic schema_version");
243                }
244                let status = symbolic
245                    .get("status")
246                    .and_then(Value::as_str)
247                    .ok_or_else(|| eyre::eyre!("missing symbolic.status"))?;
248                let status = match status {
249                    "pass" => OutcomeStatus::Passed,
250                    "fail_counterexample" => OutcomeStatus::Failed,
251                    "incomplete" => OutcomeStatus::Incomplete,
252                    _ => {
253                        eyre::bail!("unknown symbolic.status {status}");
254                    }
255                };
256                let stats = symbolic
257                    .pointer("/solver/stats")
258                    .filter(|stats| stats.is_object())
259                    .ok_or_else(|| eyre::eyre!("missing or invalid symbolic.solver.stats"))?;
260                (stats, status)
261            } else {
262                let Some(stats) = result.pointer("/kind/Symbolic") else { continue };
263                let status = result.get("status").and_then(Value::as_str).unwrap_or_default();
264                let reason = result.get("reason").and_then(Value::as_str).unwrap_or_default();
265                let status = if status == "Success" {
266                    OutcomeStatus::Passed
267                } else if reason.contains("incomplete symbolic execution") {
268                    OutcomeStatus::Incomplete
269                } else {
270                    OutcomeStatus::Failed
271                };
272                (stats, status)
273            };
274            run.outcomes.push(TestOutcome {
275                suite: suite_name.clone(),
276                signature: identity.clone(),
277                status,
278            });
279            add_metrics(&mut run.metrics, stats, stable, run.outcomes.len() == 1)?;
280        }
281    }
282    if run.outcomes.is_empty() {
283        eyre::bail!("forge symbolic benchmark produced no symbolic test results");
284    }
285    run.outcomes.sort_by_key(TestOutcome::identity);
286    run.passed =
287        run.outcomes.iter().filter(|outcome| outcome.status == OutcomeStatus::Passed).count();
288    run.failed =
289        run.outcomes.iter().filter(|outcome| outcome.status == OutcomeStatus::Failed).count();
290    run.incomplete =
291        run.outcomes.iter().filter(|outcome| outcome.status == OutcomeStatus::Incomplete).count();
292    Ok(run)
293}
294
295fn add_metrics(out: &mut Metrics, stats: &Value, stable: bool, first: bool) -> Result<()> {
296    macro_rules! add {
297        ($field:ident) => {
298            out.$field += required(stats, stringify!($field), stable)?;
299        };
300    }
301    add!(paths);
302    add!(solver_queries);
303    add!(smt_queries);
304    add!(sat_queries);
305    add!(model_queries);
306    add!(sat_cache_hits);
307    add!(model_cache_hits);
308    add!(heuristic_witnesses);
309    add!(solver_time_ms);
310    optional_add(
311        &mut out.smt_input_bytes,
312        &mut out.smt_input_bytes_compat,
313        stats,
314        "smt_input_bytes",
315        first,
316    )?;
317    optional_add(
318        &mut out.smt_build_time_ms,
319        &mut out.smt_build_time_ms_compat,
320        stats,
321        "smt_build_time_ms",
322        first,
323    )?;
324    optional_max(
325        &mut out.smt_max_query_bytes,
326        &mut out.smt_max_query_bytes_compat,
327        stats,
328        "smt_max_query_bytes",
329        first,
330    )?;
331    optional_max(
332        &mut out.smt_max_query_time_ms,
333        &mut out.smt_max_query_time_ms_compat,
334        stats,
335        "smt_max_query_time_ms",
336        first,
337    )?;
338    Ok(())
339}
340
341fn required(v: &Value, key: &str, strict: bool) -> Result<u64> {
342    match v.get(key) {
343        Some(v) => v.as_u64().ok_or_else(|| eyre::eyre!("invalid metric {key}")),
344        None if strict => Err(eyre::eyre!("missing metric {key}")),
345        None => Ok(0),
346    }
347}
348
349fn optional_add(
350    out: &mut Option<u64>,
351    compatibility: &mut u64,
352    v: &Value,
353    key: &str,
354    first: bool,
355) -> Result<()> {
356    let value = v
357        .get(key)
358        .map(|n| n.as_u64().ok_or_else(|| eyre::eyre!("invalid metric {key}")))
359        .transpose()?;
360    *compatibility += value.unwrap_or_default();
361    *out = if first { value } else { (*out).zip(value).map(|(old, value)| old + value) };
362    Ok(())
363}
364
365fn optional_max(
366    out: &mut Option<u64>,
367    compatibility: &mut u64,
368    v: &Value,
369    key: &str,
370    first: bool,
371) -> Result<()> {
372    let value = v
373        .get(key)
374        .map(|n| n.as_u64().ok_or_else(|| eyre::eyre!("invalid metric {key}")))
375        .transpose()?;
376    *compatibility = (*compatibility).max(value.unwrap_or_default());
377    *out = if first { value } else { (*out).zip(value).map(|(old, value)| old.max(value)) };
378    Ok(())
379}
380
381pub const fn compatibility(run: &ParsedRun) -> SymbolicBenchmarkSummary {
382    let m = &run.metrics;
383    SymbolicBenchmarkSummary {
384        tests: run.outcomes.len(),
385        passed: run.passed,
386        failed: run.failed,
387        incomplete: run.incomplete,
388        paths: m.paths,
389        solver_queries: m.solver_queries,
390        smt_queries: m.smt_queries,
391        sat_queries: m.sat_queries,
392        model_queries: m.model_queries,
393        sat_cache_hits: m.sat_cache_hits,
394        model_cache_hits: m.model_cache_hits,
395        heuristic_witnesses: m.heuristic_witnesses,
396        solver_time_ms: m.solver_time_ms,
397        smt_input_bytes: m.smt_input_bytes_compat,
398        smt_max_query_bytes: m.smt_max_query_bytes_compat,
399        smt_build_time_ms: m.smt_build_time_ms_compat,
400        smt_max_query_time_ms: m.smt_max_query_time_ms_compat,
401    }
402}
403
404#[cfg(test)]
405mod tests {
406    use super::*;
407
408    fn stable(status: &str, schema: u64) -> Vec<u8> {
409        serde_json::to_vec(&serde_json::json!({"test/FarcasterNativeSymbolic.t.sol:FarcasterNativeSymbolicTest":{"test_results":{
410            "check_migrateOnlyMigrator(uint24,address,address,address,uint40)":{"symbolic":{"schema_version":schema,"status":status,"bounds":{},"solver":{"name":"z3","command":null,"portfolio":[],"stats":{"paths":1,"solver_queries":2,"smt_queries":3,"sat_queries":4,"model_queries":5,"sat_cache_hits":6,"model_cache_hits":7,"heuristic_witnesses":8,"solver_time_ms":9,"smt_input_bytes":10,"smt_max_query_bytes":11,"smt_build_time_ms":12,"smt_max_query_time_ms":13}}}},
411            "check_setMigratorOnlyOwner(uint24,address,address,address,address)":{"symbolic":{"schema_version":schema,"status":"incomplete","bounds":{},"solver":{"name":"z3","command":null,"portfolio":[],"stats":{"paths":10,"solver_queries":20,"smt_queries":30,"sat_queries":40,"model_queries":50,"sat_cache_hits":60,"model_cache_hits":70,"heuristic_witnesses":80,"solver_time_ms":90}}}}
412        }}})).unwrap()
413    }
414
415    #[test]
416    fn stable_parser_validates_statuses_and_missing_optional_metrics() {
417        let run = parse(&stable("pass", 1)).unwrap();
418        assert_eq!((run.passed, run.failed, run.incomplete), (1, 0, 1));
419        assert_eq!(run.metrics.paths, 11);
420        assert_eq!(run.metrics.solver_time_ms, 99);
421        assert_eq!(run.metrics.smt_max_query_bytes, None);
422        assert_eq!(run.metrics.smt_input_bytes, None);
423        assert_eq!(run.metrics.smt_build_time_ms, None);
424        assert_eq!(run.metrics.smt_max_query_time_ms, None);
425        assert_eq!(
426            run.outcomes[0].suite,
427            "test/FarcasterNativeSymbolic.t.sol:FarcasterNativeSymbolicTest"
428        );
429        let compatibility = compatibility(&run);
430        assert_eq!(compatibility.tests, 2);
431        assert_eq!(compatibility.smt_input_bytes, 10);
432    }
433
434    #[test]
435    fn rejects_unknown_stable_schema() {
436        assert!(parse(&stable("pass", 2)).is_err());
437    }
438
439    #[test]
440    fn aggregates_optional_metrics_only_when_every_test_reports_them() {
441        let first = serde_json::json!({
442            "paths": 1, "solver_queries": 1, "smt_queries": 1, "sat_queries": 1,
443            "model_queries": 1, "sat_cache_hits": 1, "model_cache_hits": 1,
444            "heuristic_witnesses": 1, "solver_time_ms": 1, "smt_input_bytes": 10,
445            "smt_max_query_bytes": 8, "smt_build_time_ms": 2, "smt_max_query_time_ms": 4
446        });
447        let second = serde_json::json!({
448            "paths": 1, "solver_queries": 1, "smt_queries": 1, "sat_queries": 1,
449            "model_queries": 1, "sat_cache_hits": 1, "model_cache_hits": 1,
450            "heuristic_witnesses": 1, "solver_time_ms": 1, "smt_input_bytes": 20,
451            "smt_max_query_bytes": 7, "smt_build_time_ms": 3, "smt_max_query_time_ms": 9
452        });
453        let mut metrics = Metrics::default();
454        add_metrics(&mut metrics, &first, true, true).unwrap();
455        add_metrics(&mut metrics, &second, true, false).unwrap();
456        assert_eq!(metrics.smt_input_bytes, Some(30));
457        assert_eq!(metrics.smt_build_time_ms, Some(5));
458        assert_eq!(metrics.smt_max_query_bytes, Some(8));
459        assert_eq!(metrics.smt_max_query_time_ms, Some(9));
460    }
461
462    #[test]
463    fn parses_whole_output_legacy_results() {
464        let stats = serde_json::json!({"paths": 1, "solver_queries": 2});
465        let stdout = serde_json::to_vec(&serde_json::json!({"test/FarcasterNativeSymbolic.t.sol:FarcasterNativeSymbolicTest":{"test_results":{
466            "check_migrateOnlyMigrator(uint24,address,address,address,uint40)":{
467                "kind":{"Symbolic":stats},"status":"Success"
468            },
469            "check_setMigratorOnlyOwner(uint24,address,address,address,address)":{
470                "kind":{"Symbolic":stats},"status":"Failure",
471                "reason":"incomplete symbolic execution (Timeout)"
472            }
473        }}}))
474        .unwrap();
475        let run = parse(&stdout).unwrap();
476        assert_eq!((run.passed, run.failed, run.incomplete), (1, 0, 1));
477        assert_eq!(run.metrics.paths, 2);
478    }
479
480    #[test]
481    fn unknown_repository_uses_generic_symbolic_command() {
482        let fixture = Fixture::identify("example", "contracts");
483        assert!(matches!(fixture, Fixture::Generic));
484        assert_eq!(fixture.test_command(), format!("{PREFIX} forge test --symbolic --json"));
485    }
486
487    #[test]
488    fn metrics_serialize_the_complete_v1_counter_set() {
489        let value = serde_json::to_value(Metrics::default()).unwrap();
490        let keys = value
491            .as_object()
492            .unwrap()
493            .keys()
494            .map(String::as_str)
495            .collect::<std::collections::BTreeSet<_>>();
496        assert_eq!(
497            keys,
498            std::collections::BTreeSet::from([
499                "heuristic_witnesses",
500                "model_cache_hits",
501                "model_queries",
502                "paths",
503                "sat_cache_hits",
504                "sat_queries",
505                "smt_build_time_ms",
506                "smt_input_bytes",
507                "smt_max_query_bytes",
508                "smt_max_query_time_ms",
509                "smt_queries",
510                "solver_queries",
511                "solver_time_ms",
512            ])
513        );
514    }
515
516    #[test]
517    fn sidecar_retains_samples_and_revision() {
518        let first = parse(&stable("pass", 1)).unwrap();
519        let second = parse(&stable("fail_counterexample", 1)).unwrap();
520        let samples = [first, second]
521            .into_iter()
522            .map(|run| Sample { wall_time_seconds: 1.0, exit_code: 0, run })
523            .collect();
524        let sidecar = Sidecar::new(
525            Fixture::Farcaster,
526            "farcasterxyz/contracts",
527            "test-revision",
528            "forge build",
529            "forge test --symbolic --json",
530            samples,
531        );
532        assert_eq!(sidecar.fixture.revision, "test-revision");
533        assert_eq!(sidecar.samples.len(), 2);
534    }
535
536    #[test]
537    fn overlay_is_explicitly_removed_and_existing_file_is_preserved() {
538        let dir = tempfile::tempdir().unwrap();
539        fs::create_dir(dir.path().join("test")).unwrap();
540        let path = dir.path().join(FARCASTER_PATH);
541        let overlay = Overlay::install(dir.path(), Fixture::Farcaster).unwrap();
542        assert_eq!(fs::read_to_string(&path).unwrap(), FARCASTER_TEST);
543        overlay.finish().unwrap();
544        assert!(!path.exists());
545        fs::write(&path, "unexpected").unwrap();
546        assert!(Overlay::install(dir.path(), Fixture::Farcaster).is_err());
547        assert_eq!(fs::read_to_string(path).unwrap(), "unexpected");
548    }
549}
foundry_bench/symbolic.rs

foundry_bench/
symbolic.rs
