From 22915094e3c2d0d01bcdeb907da2b54f787ad814 Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Thu, 21 May 2026 12:39:15 +0100 Subject: [PATCH] feat(symbolic): show query progress Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp --- crates/evm/symbolic/src/executor.rs | 5 +++ crates/evm/symbolic/src/runtime/solver.rs | 24 ++++++++++++-- crates/forge/src/progress.rs | 39 +++++++++++++++++++++++ crates/forge/src/runner.rs | 28 +++++++++++++++- 4 files changed, 93 insertions(+), 3 deletions(-) diff --git a/crates/evm/symbolic/src/executor.rs b/crates/evm/symbolic/src/executor.rs index 706b9d16ea983..1274d95e10074 100644 --- a/crates/evm/symbolic/src/executor.rs +++ b/crates/evm/symbolic/src/executor.rs @@ -28,6 +28,11 @@ impl SymbolicExecutor { self.solver.take_diagnostics() } + /// Registers a callback invoked after each solver query for live progress rendering. + pub fn set_query_observer(&mut self, observer: impl Fn(usize) + Send + Sync + 'static) { + self.solver.set_query_observer(Some(Box::new(observer))); + } + /// Executes one function symbolically against an already-deployed test contract. /// /// The input executor supplies the deployed bytecode, storage backend, caller, and diff --git a/crates/evm/symbolic/src/runtime/solver.rs b/crates/evm/symbolic/src/runtime/solver.rs index 5e4be89a10361..741279fd60700 100644 --- a/crates/evm/symbolic/src/runtime/solver.rs +++ b/crates/evm/symbolic/src/runtime/solver.rs @@ -47,6 +47,8 @@ impl fmt::Display for SolverOutcome { } } +pub(crate) type QueryObserver = Box; + /// Minimal solver backend interface used by the symbolic executor. /// /// Implementations are responsible for translating accumulated symbolic constraints @@ -57,6 +59,9 @@ pub(crate) trait SymbolicSolver { /// Returns solver counters collected by this backend. fn stats(&self) -> SymbolicStats; + /// Registers a callback invoked after each logical solver query is reserved. + fn set_query_observer(&mut self, observer: Option); + /// Returns aggregate staged-portfolio diagnostics collected by this backend. fn portfolio_diagnostics(&self) -> Option<&PortfolioDiagnostics>; @@ -115,6 +120,7 @@ pub(crate) struct SmtLibSubprocessSolver { pub(crate) timeout: Option, pub(crate) max_queries: usize, pub(crate) queries: usize, + query_observer: Option, pub(crate) dump_smt: bool, portfolio_diagnostics: PortfolioDiagnostics, captured_diagnostics: Option, @@ -133,6 +139,7 @@ impl SmtLibSubprocessSolver { timeout, max_queries, queries: 0, + query_observer: None, dump_smt, portfolio_diagnostics: PortfolioDiagnostics::default(), captured_diagnostics: None, @@ -156,6 +163,11 @@ impl SymbolicSolver for SmtLibSubprocessSolver { SymbolicStats { paths: 0, solver_queries: self.queries } } + /// Registers a live query observer for progress rendering. + fn set_query_observer(&mut self, observer: Option) { + self.query_observer = observer; + } + /// Returns staged-portfolio diagnostics collected by this solver. fn portfolio_diagnostics(&self) -> Option<&PortfolioDiagnostics> { (!self.portfolio_diagnostics.is_empty()).then_some(&self.portfolio_diagnostics) @@ -194,7 +206,7 @@ impl SymbolicSolver for SmtLibSubprocessSolver { /// Returns whether `is_sat` holds. fn is_sat(&mut self, constraints: &[BoolExpr]) -> Result { self.reserve_query()?; - self.queries += 1; + self.record_query(); if constraints_prefer_fallback_first(constraints) && fallback_single_var_model(constraints).is_some() { @@ -214,7 +226,7 @@ impl SymbolicSolver for SmtLibSubprocessSolver { /// Implements the `model` solver helper. fn model(&mut self, constraints: &[BoolExpr]) -> Result, SymbolicError> { self.reserve_query()?; - self.queries += 1; + self.record_query(); if constraints_prefer_fallback_first(constraints) && let Some(model) = fallback_single_var_model(constraints) { @@ -255,6 +267,14 @@ impl SmtLibSubprocessSolver { Ok(()) } + /// Records one logical solver query and notifies the live observer, if any. + fn record_query(&mut self) { + self.queries += 1; + if let Some(observer) = &self.query_observer { + observer(self.queries); + } + } + /// Implements the `query` solver helper. pub(crate) fn query( &mut self, diff --git a/crates/forge/src/progress.rs b/crates/forge/src/progress.rs index e8a5d7e049682..4f10862ce5e71 100644 --- a/crates/forge/src/progress.rs +++ b/crates/forge/src/progress.rs @@ -90,6 +90,31 @@ impl TestsProgressState { } } + /// Creates progress entry for symbolic tests. + pub fn start_symbolic_progress( + &mut self, + suite_name: &str, + test_name: &str, + max_queries: u32, + ) -> Option { + if let Some(suite_progress) = self.suites_progress.get(suite_name) { + let symbolic_progress = + self.multi.insert_after(suite_progress, ProgressBar::new(max_queries as u64)); + symbolic_progress.set_style( + indicatif::ProgressStyle::with_template( + " ↪ {prefix:.bold.dim}: [{pos}/{len}] SMT queries {msg}", + ) + .unwrap() + .tick_chars("⠁⠂⠄⡀⢀⠠⠐⠈ "), + ); + symbolic_progress.set_prefix(test_name.to_owned()); + symbolic_progress.enable_steady_tick(Duration::from_millis(100)); + Some(symbolic_progress) + } else { + None + } + } + /// Removes overall test progress. pub fn clear(&mut self) { self.multi.clear().unwrap(); @@ -122,3 +147,17 @@ pub fn start_fuzz_progress( None } } + +/// Helper function for creating symbolic test progress bar. +pub fn start_symbolic_progress( + tests_progress: Option<&TestsProgress>, + suite_name: &str, + test_name: &str, + max_queries: u32, +) -> Option { + if let Some(progress) = tests_progress { + progress.inner.lock().start_symbolic_progress(suite_name, test_name, max_queries) + } else { + None + } +} diff --git a/crates/forge/src/runner.rs b/crates/forge/src/runner.rs index 69a0bb6b621c8..b64d7fa4bc70e 100644 --- a/crates/forge/src/runner.rs +++ b/crates/forge/src/runner.rs @@ -5,7 +5,7 @@ use crate::{ coverage::HitMaps, fuzz::{BaseCounterExample, FuzzTestResult}, multi_runner::{TestContract, TestRunnerConfig}, - progress::{TestsProgress, start_fuzz_progress}, + progress::{TestsProgress, start_fuzz_progress, start_symbolic_progress}, result::{InvariantFailure, SuiteResult, TestResult, TestSetup}, }; use alloy_dyn_abi::{DynSolValue, JsonAbiExt}; @@ -749,6 +749,16 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> { if self.should_defer_symbolic_diagnostics() { symbolic.capture_diagnostics(); } + let progress = start_symbolic_progress( + self.cr.progress, + self.cr.name, + &func.name, + self.config.symbolic.max_solver_queries, + ); + if let Some(progress) = progress.as_ref() { + let progress = progress.clone(); + symbolic.set_query_observer(move |queries| progress.set_position(queries as u64)); + } let result = symbolic.run(SymbolicRunInput { executor: self.executor.as_ref(), target: self.address, @@ -757,6 +767,9 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> { value: U256::ZERO, ffi_enabled: self.config.ffi, }); + if let Some(progress) = progress { + progress.finish_and_clear(); + } let portfolio_diagnostics = symbolic.portfolio_diagnostics(); let symbolic_diagnostics = symbolic.take_diagnostics(); @@ -901,6 +914,16 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> { if self.should_defer_symbolic_diagnostics() { symbolic.capture_diagnostics(); } + let progress = start_symbolic_progress( + self.cr.progress, + self.cr.name, + &func.name, + self.config.symbolic.max_solver_queries, + ); + if let Some(progress) = progress.as_ref() { + let progress = progress.clone(); + symbolic.set_query_observer(move |queries| progress.set_position(queries as u64)); + } let result = symbolic.run_invariant(SymbolicInvariantRunInput { executor: self.executor.as_ref(), invariant_address: self.address, @@ -913,6 +936,9 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> { fail_on_revert, ffi_enabled: self.config.ffi, }); + if let Some(progress) = progress { + progress.finish_and_clear(); + } let portfolio_diagnostics = symbolic.portfolio_diagnostics(); let symbolic_diagnostics = symbolic.take_diagnostics();