From 47fc75ce508f156f921d5b334600c6752acefc55 Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Wed, 20 May 2026 12:35:15 +0100 Subject: [PATCH 1/5] chore(symbolic): share builtin solver registry Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp --- crates/evm/symbolic/src/lib.rs | 9 +++++++++ crates/evm/symbolic/src/tests.rs | 8 ++++++++ crates/forge/src/runner.rs | 9 +++------ 3 files changed, 20 insertions(+), 6 deletions(-) diff --git a/crates/evm/symbolic/src/lib.rs b/crates/evm/symbolic/src/lib.rs index 58cd0a530508f..55adf5ab572c1 100644 --- a/crates/evm/symbolic/src/lib.rs +++ b/crates/evm/symbolic/src/lib.rs @@ -57,10 +57,19 @@ mod runtime; pub use runtime::{SymbolicError, SymbolicRunInput}; +/// Symbolic solver names with built-in command-line mappings. +pub const BUILTIN_SYMBOLIC_SOLVERS: &[&str] = + &["z3", "yices", "cvc5", "cvc5-int", "bitwuzla", "bitwuzla-abs"]; + const DEFAULT_DERIVATION_PATH_PREFIX: &str = "m/44'/60'/0'/0/"; const MAX_REMEMBER_KEYS: u32 = 64; const SYMBOLIC_VM_COMPAT_ADDRESS: Address = address!("0xF3993A62377BCd56AE39D773740A5390411E8BC9"); +/// Returns whether `solver` is one of Foundry's semantic symbolic solver names. +pub fn symbolic_solver_is_builtin(solver: &str) -> bool { + BUILTIN_SYMBOLIC_SOLVERS.contains(&solver) +} + /// Returns the `selector_for` symbolic public API helper result. fn selector_for(signature: &str) -> [u8; 4] { let hash = keccak256(signature); diff --git a/crates/evm/symbolic/src/tests.rs b/crates/evm/symbolic/src/tests.rs index 3ae6d44e21937..8899eaf49a779 100644 --- a/crates/evm/symbolic/src/tests.rs +++ b/crates/evm/symbolic/src/tests.rs @@ -1881,6 +1881,14 @@ fn query_limit_is_enforced_before_spawning_solver() { #[test] /// Regression coverage for `known_solver_names_resolve_to_smtlib_commands`. fn known_solver_names_resolve_to_smtlib_commands() { + for solver in BUILTIN_SYMBOLIC_SOLVERS { + assert!(symbolic_solver_is_builtin(solver)); + named_solver_command(solver).unwrap(); + } + assert!(!symbolic_solver_is_builtin("yices-2.7.0")); + assert!(!symbolic_solver_is_builtin("cvc5-1.3.4")); + assert!(!symbolic_solver_is_builtin("bitwuzla-0.9.0")); + let commands = solver_commands_for_config(&SymbolicConfig { solver: "yices".to_string(), ..Default::default() diff --git a/crates/forge/src/runner.rs b/crates/forge/src/runner.rs index 3f756e44832e6..910388dd33b5c 100644 --- a/crates/forge/src/runner.rs +++ b/crates/forge/src/runner.rs @@ -37,7 +37,7 @@ use foundry_evm::{ }; use foundry_evm_symbolic::{ SymbolicExecutor, SymbolicInvariantRunInput, SymbolicInvariantRunResult, SymbolicInvariantStep, - SymbolicInvariantTarget, SymbolicRunInput, SymbolicRunResult, + SymbolicInvariantTarget, SymbolicRunInput, SymbolicRunResult, symbolic_solver_is_builtin, }; use itertools::Itertools; use proptest::test_runner::{RngAlgorithm, TestError, TestRng, TestRunner}; @@ -62,9 +62,6 @@ use tracing::Span; /// `address(uint160(uint256(keccak256("foundry library deployer"))))` pub const LIBRARY_DEPLOYER: Address = address!("0x1F95D37F27EA0dEA9C252FC09D5A6eaA97647353"); -const BUILTIN_SYMBOLIC_SOLVERS: &[&str] = - &["z3", "yices", "cvc5", "cvc5-int", "bitwuzla", "bitwuzla-abs"]; - pub(crate) fn is_symbolic_entrypoint(func: &Function) -> bool { func.name.starts_with("check") || func.name.starts_with("prove") } @@ -575,10 +572,10 @@ fn symbolic_solver_config_executes_custom_program(symbolic: &SymbolicConfig) -> let entry = entry.trim(); !entry.is_empty() && (entry.chars().any(|ch| ch.is_whitespace() || matches!(ch, '"' | '\'' | '\\')) - || !BUILTIN_SYMBOLIC_SOLVERS.contains(&entry)) + || !symbolic_solver_is_builtin(entry)) }); } - !BUILTIN_SYMBOLIC_SOLVERS.contains(&symbolic.solver.trim()) + !symbolic_solver_is_builtin(symbolic.solver.trim()) } /// Executes a single test function, returning a [`TestResult`]. From b53d94cd58f4a15d6922527db3deaf52714f9198 Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Wed, 20 May 2026 13:00:07 +0100 Subject: [PATCH 2/5] feat(symbolic): report portfolio solver outcomes Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp --- crates/evm/symbolic/README.md | 3 +- crates/evm/symbolic/src/runtime/solver.rs | 145 ++++++++++++++++++++-- 2 files changed, 136 insertions(+), 12 deletions(-) diff --git a/crates/evm/symbolic/README.md b/crates/evm/symbolic/README.md index 17549ab5a1423..36b23119368e2 100644 --- a/crates/evm/symbolic/README.md +++ b/crates/evm/symbolic/README.md @@ -225,7 +225,8 @@ whitespace, quotes, or backslashes are split into argv parts like For latency-sensitive local runs, start with a small portfolio such as `["yices", "z3"]`. Broader portfolios can help on solver-diverse workloads but use more CPU and can be slower when one fast solver already handles most -queries. +queries. `--symbolic-dump-smt` also prints per-query portfolio outcomes so solver +mixes can be compared without changing execution semantics. Security note: `symbolic.solver_command`, custom `symbolic.solver` values, and custom or command-like `symbolic.solver_portfolio` entries execute local programs diff --git a/crates/evm/symbolic/src/runtime/solver.rs b/crates/evm/symbolic/src/runtime/solver.rs index 2b24302332224..088022358643d 100644 --- a/crates/evm/symbolic/src/runtime/solver.rs +++ b/crates/evm/symbolic/src/runtime/solver.rs @@ -201,7 +201,13 @@ impl SmtLibSubprocessSolver { let _ = writeln!(stderr, "--- symbolic SMT query {} ---\n{smt}", self.queries); } - run_solver_commands(commands, &smt, self.timeout, model.then_some(constraints)) + run_solver_commands( + commands, + &smt, + self.timeout, + model.then_some(constraints), + self.dump_smt, + ) } } @@ -289,12 +295,45 @@ enum SolverProcessOutcome { Error(String), } +#[derive(Debug)] +struct SolverProcessResult { + display: String, + elapsed: Duration, + outcome: SolverProcessOutcome, +} + +#[derive(Debug)] +struct SolverRunSummary { + display: String, + elapsed: Duration, + outcome: &'static str, + detail: Option, + winner: bool, +} + +impl SolverRunSummary { + fn new(display: String, elapsed: Duration, outcome: &'static str) -> Self { + Self { display, elapsed, outcome, detail: None, winner: false } + } + + fn with_detail(mut self, detail: impl Into) -> Self { + self.detail = Some(detail.into()); + self + } + + const fn winner(mut self) -> Self { + self.winner = true; + self + } +} + /// Runs one or more solver commands and returns the first decisive SMT-LIB response. fn run_solver_commands( commands: &[SolverCommand], smt: &str, timeout: Option, model_constraints: Option<&[BoolExpr]>, + dump_diagnostics: bool, ) -> Result { if commands.is_empty() { return Err(SymbolicError::Solver("symbolic solver portfolio is empty".to_string())); @@ -317,8 +356,13 @@ fn run_solver_commands( let tx = tx.clone(); let cancel = Arc::clone(&cancel); scope.spawn(move || { + let start = Instant::now(); let outcome = run_solver_process(&command, smt, timeout, &cancel); - let _ = tx.send((command.display, outcome)); + let _ = tx.send(SolverProcessResult { + display: command.display, + elapsed: start.elapsed(), + outcome, + }); }); } drop(tx); @@ -328,40 +372,73 @@ fn run_solver_commands( let mut saw_invalid_sat_model = false; let mut errors = Vec::new(); let mut decisive = None; - while let Ok((display, outcome)) = rx.recv() { + let mut summaries = Vec::new(); + while let Ok(result) = rx.recv() { + let SolverProcessResult { display, elapsed, outcome } = result; match outcome { SolverProcessOutcome::Output(output) if solver_output_is_sat(&output) => { if let Some(constraints) = model_constraints && let Err(err) = validate_solver_model_output(&output, constraints) { + summaries.push( + SolverRunSummary::new(display.clone(), elapsed, "sat-invalid") + .with_detail(err.to_string()), + ); saw_invalid_sat_model = true; errors.push(format!("{display}: {err}")); continue; } + summaries.push(SolverRunSummary::new(display, elapsed, "sat-valid").winner()); decisive = Some(output); cancel.store(true, Ordering::SeqCst); break; } SolverProcessOutcome::Output(output) if solver_output_is_unsat(&output) => { + summaries.push(SolverRunSummary::new(display, elapsed, "unsat")); saw_unsat = true; } SolverProcessOutcome::Output(output) if solver_output_is_unknown(&output) => { + summaries.push(SolverRunSummary::new(display, elapsed, "unknown")); saw_unknown = true; } SolverProcessOutcome::Output(output) => { - errors.push(format!( - "{display}: unexpected solver response `{}`", - first_solver_line(&output) - )); + let first_line = first_solver_line(&output).to_string(); + summaries.push( + SolverRunSummary::new(display.clone(), elapsed, "unexpected") + .with_detail(first_line.clone()), + ); + errors.push(format!("{display}: unexpected solver response `{}`", first_line)); + } + SolverProcessOutcome::Unknown => { + summaries.push(SolverRunSummary::new(display, elapsed, "timeout-or-unknown")); + saw_unknown = true; + } + SolverProcessOutcome::Cancelled => { + summaries.push(SolverRunSummary::new(display, elapsed, "cancelled")); + } + SolverProcessOutcome::Error(err) => { + summaries.push( + SolverRunSummary::new(display.clone(), elapsed, "error") + .with_detail(err.clone()), + ); + errors.push(format!("{display}: {err}")); } - SolverProcessOutcome::Unknown => saw_unknown = true, - SolverProcessOutcome::Cancelled => {} - SolverProcessOutcome::Error(err) => errors.push(format!("{display}: {err}")), } } if decisive.is_some() { - while rx.recv().is_ok() {} + while let Ok(result) = rx.recv() { + let SolverProcessResult { display, elapsed, outcome } = result; + summaries.push(summary_for_cancelled_solver_result(display, elapsed, outcome)); + } + } else if saw_unsat { + if let Some(summary) = summaries.iter_mut().find(|summary| summary.outcome == "unsat") { + summary.winner = true; + } + } + + if dump_diagnostics { + dump_solver_portfolio_summaries(&summaries); } if let Some(output) = decisive { @@ -378,6 +455,52 @@ fn run_solver_commands( }) } +fn summary_for_cancelled_solver_result( + display: String, + elapsed: Duration, + outcome: SolverProcessOutcome, +) -> SolverRunSummary { + match outcome { + SolverProcessOutcome::Output(output) if solver_output_is_sat(&output) => { + SolverRunSummary::new(display, elapsed, "sat-after-winner") + } + SolverProcessOutcome::Output(output) if solver_output_is_unsat(&output) => { + SolverRunSummary::new(display, elapsed, "unsat-after-winner") + } + SolverProcessOutcome::Output(output) if solver_output_is_unknown(&output) => { + SolverRunSummary::new(display, elapsed, "unknown-after-winner") + } + SolverProcessOutcome::Output(output) => { + SolverRunSummary::new(display, elapsed, "unexpected") + .with_detail(first_solver_line(&output).to_string()) + } + SolverProcessOutcome::Unknown => { + SolverRunSummary::new(display, elapsed, "timeout-or-unknown") + } + SolverProcessOutcome::Cancelled => SolverRunSummary::new(display, elapsed, "cancelled"), + SolverProcessOutcome::Error(err) => { + SolverRunSummary::new(display, elapsed, "error").with_detail(err) + } + } +} + +fn dump_solver_portfolio_summaries(summaries: &[SolverRunSummary]) { + let mut stderr = std::io::stderr().lock(); + let _ = writeln!(stderr, "--- symbolic solver portfolio outcomes ---"); + for summary in summaries { + let marker = if summary.winner { " winner" } else { "" }; + let _ = write!( + stderr, + "{}: {} in {:.3?}{}", + summary.display, summary.outcome, summary.elapsed, marker + ); + if let Some(detail) = summary.detail.as_deref().filter(|detail| !detail.is_empty()) { + let _ = write!(stderr, " ({detail})"); + } + let _ = writeln!(stderr); + } +} + /// Runs one solver process to completion, timeout, or cooperative cancellation. fn run_solver_process( command: &SolverCommand, From 948eff1ce7a58f296ff075cc743aeb86de73e4cf Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Wed, 20 May 2026 13:09:28 +0100 Subject: [PATCH 3/5] feat(symbolic): warn on degraded solver portfolios Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp --- crates/evm/symbolic/README.md | 2 ++ crates/evm/symbolic/src/lib.rs | 5 +++ crates/evm/symbolic/src/runtime/solver.rs | 40 +++++++++++++++++++++++ crates/evm/symbolic/src/tests.rs | 23 +++++++++++++ crates/forge/src/runner.rs | 23 ++++++++++++- 5 files changed, 92 insertions(+), 1 deletion(-) diff --git a/crates/evm/symbolic/README.md b/crates/evm/symbolic/README.md index 36b23119368e2..d36b80ef8afef 100644 --- a/crates/evm/symbolic/README.md +++ b/crates/evm/symbolic/README.md @@ -227,6 +227,8 @@ For latency-sensitive local runs, start with a small portfolio such as use more CPU and can be slower when one fast solver already handles most queries. `--symbolic-dump-smt` also prints per-query portfolio outcomes so solver mixes can be compared without changing execution semantics. +Forge warns when a configured portfolio is degraded because one or more solver +entries are not available, but it still uses the entries that can be invoked. Security note: `symbolic.solver_command`, custom `symbolic.solver` values, and custom or command-like `symbolic.solver_portfolio` entries execute local programs diff --git a/crates/evm/symbolic/src/lib.rs b/crates/evm/symbolic/src/lib.rs index 55adf5ab572c1..2c2f00b7d2f9b 100644 --- a/crates/evm/symbolic/src/lib.rs +++ b/crates/evm/symbolic/src/lib.rs @@ -70,6 +70,11 @@ pub fn symbolic_solver_is_builtin(solver: &str) -> bool { BUILTIN_SYMBOLIC_SOLVERS.contains(&solver) } +/// Returns a warning when a configured symbolic solver portfolio has unavailable entries. +pub fn symbolic_solver_portfolio_availability_warning(config: &SymbolicConfig) -> Option { + runtime::solver_portfolio_availability_warning(config) +} + /// Returns the `selector_for` symbolic public API helper result. fn selector_for(signature: &str) -> [u8; 4] { let hash = keccak256(signature); diff --git a/crates/evm/symbolic/src/runtime/solver.rs b/crates/evm/symbolic/src/runtime/solver.rs index 088022358643d..c8d6d03c63c6c 100644 --- a/crates/evm/symbolic/src/runtime/solver.rs +++ b/crates/evm/symbolic/src/runtime/solver.rs @@ -232,6 +232,37 @@ pub(crate) fn solver_commands_for_config( Ok(vec![named_solver_command(&config.solver)?]) } +/// Returns a warning when a configured portfolio will run with unavailable solver entries. +pub(crate) fn solver_portfolio_availability_warning(config: &SymbolicConfig) -> Option { + if config.solver_command.as_deref().is_some_and(|command| !command.trim().is_empty()) + || config.solver_portfolio.iter().all(|entry| entry.trim().is_empty()) + { + return None; + } + + let commands = solver_commands_for_config(config).ok()?; + let unavailable = commands + .iter() + .filter_map(|command| { + solver_command_availability_error(command) + .map(|err| format!("`{}` ({err})", command.display)) + }) + .collect::>(); + if unavailable.is_empty() { + return None; + } + + let suffix = if unavailable.len() == commands.len() { + "No configured portfolio entries are currently available." + } else { + "Available portfolio entries will still be used." + }; + Some(format!( + "Symbolic solver portfolio is degraded; unavailable entries: {}. {suffix}", + unavailable.join("; ") + )) +} + /// Returns the default command for a known solver name. pub(crate) fn named_solver_command(solver: &str) -> Result { let (parts, smt_timeout) = match solver { @@ -287,6 +318,15 @@ pub(crate) fn split_solver_command(command: &str) -> Result, String> Ok(parts) } +fn solver_command_availability_error(command: &SolverCommand) -> Option { + let output = match Command::new(&command.program).arg("--version").output() { + Ok(output) => output, + Err(err) => return Some(format!("failed to execute `{}`: {err}", command.program)), + }; + (!output.status.success()) + .then(|| format!("`{}` is not a usable SMT solver executable", command.program)) +} + #[derive(Debug)] enum SolverProcessOutcome { Output(String), diff --git a/crates/evm/symbolic/src/tests.rs b/crates/evm/symbolic/src/tests.rs index 8899eaf49a779..30bbd1164a156 100644 --- a/crates/evm/symbolic/src/tests.rs +++ b/crates/evm/symbolic/src/tests.rs @@ -1990,6 +1990,29 @@ fn solver_portfolio_resolves_parallel_commands() { assert!(!commands[2].smt_timeout); } +#[test] +/// Regression coverage for `solver_portfolio_availability_warning_reports_missing_entries`. +fn solver_portfolio_availability_warning_reports_missing_entries() { + let warning = symbolic_solver_portfolio_availability_warning(&SymbolicConfig { + solver_portfolio: vec!["foundry-missing-symbolic-solver".to_string()], + ..Default::default() + }) + .unwrap(); + + assert!(warning.contains("Symbolic solver portfolio is degraded")); + assert!(warning.contains("foundry-missing-symbolic-solver")); + assert!(warning.contains("No configured portfolio entries are currently available")); + + assert!( + symbolic_solver_portfolio_availability_warning(&SymbolicConfig { + solver_portfolio: vec!["foundry-missing-symbolic-solver".to_string()], + solver_command: Some("custom-solver".to_string()), + ..Default::default() + }) + .is_none() + ); +} + #[cfg(unix)] #[test] /// Regression coverage for `portfolio_sat_beats_early_unsat`. diff --git a/crates/forge/src/runner.rs b/crates/forge/src/runner.rs index 910388dd33b5c..e1d054f602879 100644 --- a/crates/forge/src/runner.rs +++ b/crates/forge/src/runner.rs @@ -38,6 +38,7 @@ use foundry_evm::{ use foundry_evm_symbolic::{ SymbolicExecutor, SymbolicInvariantRunInput, SymbolicInvariantRunResult, SymbolicInvariantStep, SymbolicInvariantTarget, SymbolicRunInput, SymbolicRunResult, symbolic_solver_is_builtin, + symbolic_solver_portfolio_availability_warning, }; use itertools::Itertools; use proptest::test_runner::{RngAlgorithm, TestError, TestRng, TestRunner}; @@ -46,7 +47,7 @@ use serde::{Deserialize, Serialize}; use std::{ borrow::Cow, cmp::min, - collections::BTreeMap, + collections::{BTreeMap, BTreeSet}, ops::Deref, path::{Path, PathBuf}, sync::Arc, @@ -453,6 +454,7 @@ impl<'a, FEN: FoundryEvmNetwork> ContractRunner<'a, FEN> { if let Some(warning) = self.symbolic_solver_command_warning(&functions) { warnings.push(warning); } + warnings.extend(self.symbolic_solver_portfolio_availability_warnings(&functions)); let identified_contracts = has_invariants.then(|| { load_contracts(setup.traces.iter().map(|(_, t)| &t.arena), &self.mcr.known_contracts) @@ -561,6 +563,25 @@ impl<'a, FEN: FoundryEvmNetwork> ContractRunner<'a, FEN> { Some(self.config.symbolic.clone()) } } + + fn symbolic_solver_portfolio_availability_warnings( + &self, + functions: &[&Function], + ) -> Vec { + if !self.config.symbolic.enabled { + return Vec::new(); + } + + functions + .iter() + .copied() + .filter(|func| is_symbolic_entrypoint(func) || func.is_invariant_test()) + .filter_map(|func| self.effective_symbolic_config(func)) + .filter_map(|symbolic| symbolic_solver_portfolio_availability_warning(&symbolic)) + .collect::>() + .into_iter() + .collect() + } } fn symbolic_solver_config_executes_custom_program(symbolic: &SymbolicConfig) -> bool { From 5f270cf24601c1cd5d7a526c4a320ff1f9df886d Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Wed, 20 May 2026 14:47:29 +0100 Subject: [PATCH 4/5] chore(symbolic): fix portfolio diagnostics clippy Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp --- crates/evm/symbolic/src/runtime/solver.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/crates/evm/symbolic/src/runtime/solver.rs b/crates/evm/symbolic/src/runtime/solver.rs index c8d6d03c63c6c..187aa07ac5f86 100644 --- a/crates/evm/symbolic/src/runtime/solver.rs +++ b/crates/evm/symbolic/src/runtime/solver.rs @@ -352,7 +352,7 @@ struct SolverRunSummary { } impl SolverRunSummary { - fn new(display: String, elapsed: Duration, outcome: &'static str) -> Self { + const fn new(display: String, elapsed: Duration, outcome: &'static str) -> Self { Self { display, elapsed, outcome, detail: None, winner: false } } @@ -447,7 +447,7 @@ fn run_solver_commands( SolverRunSummary::new(display.clone(), elapsed, "unexpected") .with_detail(first_line.clone()), ); - errors.push(format!("{display}: unexpected solver response `{}`", first_line)); + errors.push(format!("{display}: unexpected solver response `{first_line}`")); } SolverProcessOutcome::Unknown => { summaries.push(SolverRunSummary::new(display, elapsed, "timeout-or-unknown")); @@ -471,10 +471,10 @@ fn run_solver_commands( let SolverProcessResult { display, elapsed, outcome } = result; summaries.push(summary_for_cancelled_solver_result(display, elapsed, outcome)); } - } else if saw_unsat { - if let Some(summary) = summaries.iter_mut().find(|summary| summary.outcome == "unsat") { - summary.winner = true; - } + } else if saw_unsat + && let Some(summary) = summaries.iter_mut().find(|summary| summary.outcome == "unsat") + { + summary.winner = true; } if dump_diagnostics { From a7faa2ab864accc6523d8eb5e252b68a36232e62 Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Wed, 20 May 2026 15:32:09 +0100 Subject: [PATCH 5/5] docs(symbolic): document solver portfolio helpers --- crates/evm/symbolic/src/runtime/solver.rs | 6 ++++++ crates/forge/src/runner.rs | 1 + 2 files changed, 7 insertions(+) diff --git a/crates/evm/symbolic/src/runtime/solver.rs b/crates/evm/symbolic/src/runtime/solver.rs index 187aa07ac5f86..2a49d75dc4332 100644 --- a/crates/evm/symbolic/src/runtime/solver.rs +++ b/crates/evm/symbolic/src/runtime/solver.rs @@ -318,6 +318,7 @@ pub(crate) fn split_solver_command(command: &str) -> Result, String> Ok(parts) } +/// Returns why `command` is not currently executable as an SMT solver. fn solver_command_availability_error(command: &SolverCommand) -> Option { let output = match Command::new(&command.program).arg("--version").output() { Ok(output) => output, @@ -352,15 +353,18 @@ struct SolverRunSummary { } impl SolverRunSummary { + /// Builds a portfolio run summary with no detail or winner marker. const fn new(display: String, elapsed: Duration, outcome: &'static str) -> Self { Self { display, elapsed, outcome, detail: None, winner: false } } + /// Attaches an additional diagnostic detail string to this summary. fn with_detail(mut self, detail: impl Into) -> Self { self.detail = Some(detail.into()); self } + /// Marks this solver run as the portfolio result winner. const fn winner(mut self) -> Self { self.winner = true; self @@ -495,6 +499,7 @@ fn run_solver_commands( }) } +/// Summarizes a solver result received after a portfolio winner was chosen. fn summary_for_cancelled_solver_result( display: String, elapsed: Duration, @@ -524,6 +529,7 @@ fn summary_for_cancelled_solver_result( } } +/// Writes solver portfolio outcome diagnostics to stderr. fn dump_solver_portfolio_summaries(summaries: &[SolverRunSummary]) { let mut stderr = std::io::stderr().lock(); let _ = writeln!(stderr, "--- symbolic solver portfolio outcomes ---"); diff --git a/crates/forge/src/runner.rs b/crates/forge/src/runner.rs index e1d054f602879..86945c9d510f0 100644 --- a/crates/forge/src/runner.rs +++ b/crates/forge/src/runner.rs @@ -564,6 +564,7 @@ impl<'a, FEN: FoundryEvmNetwork> ContractRunner<'a, FEN> { } } + /// Returns unique availability warnings for symbolic solver portfolios used by this suite. fn symbolic_solver_portfolio_availability_warnings( &self, functions: &[&Function],