From 155032d1786979d92fbf0a4b52d815ea4ea312fc Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Thu, 22 Oct 2026 03:31:52 -0400 Subject: [PATCH] perf(klee): pin the nondet values only when they will be formatted Under KLEE the nondet log was concretised at the end of every path, one solver query plus one assume per value, though it is written only on a violation (and the JSON report only without a mode). Map2Check 9.0 pins the values only on the violating path. On loop-acceleration/array_3-2 (1024 nondet reads) KLEE completed 1 path in its first phase where the 9.0 C runtime completed 263, and the target 9.0 finds in every run (3/3, ~185 s) was never found (0/3). Pinning only when the log or the report will be formatted: found in 2/2 runs (254 s, 113 s). --- rust/src/nondet/klee.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/rust/src/nondet/klee.rs b/rust/src/nondet/klee.rs index c177a83..20c0975 100644 --- a/rust/src/nondet/klee.rs +++ b/rust/src/nondet/klee.rs @@ -383,8 +383,17 @@ pub(crate) const KLEE_LOG_MAX_ROWS: usize = 1024; /// memory records, which a symbolic size or index reaches) by a concrete /// value of the current path. Called right before the witness logs or the /// JSON report are written (`output::prepare_for_output`). +/// +/// The nondet values are pinned only when something will format them: the +/// nondet log, which is written on a violation, and the JSON report, which is +/// printed when no analysis mode is set. Map2Check 9.0 pins them only on the +/// violating path too (`nondet_generate_aux_witness_files`). Pinning on every +/// path that ends normally costs a solver query per value per path: on +/// loop-acceleration/array_3-2 (1024 reads) KLEE completed 1 path where the +/// 9.0 C runtime completed 263, and lost a target 9.0 finds every time. pub(crate) fn concretize(state: &mut AnalysisState) { - if state.nondets.len() <= KLEE_LOG_MAX_ROWS { + let formatted = !state.result.ok || crate::state::config().mode.is_none(); + if formatted && state.nondets.len() <= KLEE_LOG_MAX_ROWS { for entry in &mut state.nondets { entry.value = concrete_value(&entry.value); }