From b7b1e010cc50385de75c33e26c67d94ad3fd2d6e Mon Sep 17 00:00:00 2001 From: Andrii Date: Fri, 24 Apr 2026 20:17:47 +0300 Subject: [PATCH] Fix three unrelated prover-side failure modes in split/parallel verification This addresses three independent bugs that surface under sui-prover's -vcsSplitOnEveryAssert + -vcsMaxKeepGoingSplits + -vcsCores>1 configuration on large, heavily-inlined Move specs (e.g. cetus clmm_math::*): 1. BlockRewriter.ComputeNewBlocks: rebuild Predecessors after DeleteBlocksNotLeadingToAssertions + BlockCoalescer.CoalesceInPlace (Source/VCGeneration/Splits/BlockRewriter.cs). ShallowClone leaves Predecessors empty, and both transformations rewrite gotos without touching the downstream Predecessors lists -- so the returned newBlocks reach Split.CountAssertions with empty predecessor lists. CountAssertions then reads next.Predecessors.Count as 0 for a block N that actually has multiple real predecessors, incorrectly merges N (setting N.bigBlock = false), and later finds another big block Q still referencing N in its virtualSuccessors. That trips the invariant at Split.cs:354 with "non-big N accessed from Q" and a Cce.UnreachableException that kills the whole verification. Mirrors the predecessor rebuild BlockTransformations.Optimize already performs after the same two steps. 2. SMTLibProcess.Send: make each SMT command atomic with respect to concurrent writers (Source/Provers/SMTLib/SMTLibProcess.cs). The asyncLock (SemaphoreSlim) only serializes the high-level async operations (SendRequest / PingPong / SendRequestsAndCloseInput); a large number of call sites invoke Send directly (SendThisVC during VC setup, Reset, RunTimeoutDiagnostics) without holding it. With -vcsCores>1 + keep-going splits, these paths can race against another checker's in-flight ping, and because StreamWriter.WriteLine may chunk the string and Flush is a separate call, bytes from two commands interleave on Z3's stdin. Z3 then reports diagnostics like unknown constant $IsValid'$(get-info :name)\n -- the ping request literally spliced into the middle of a declare-fun identifier, followed by a cascade of unknown-constant, invalid-let-declaration, invalid-pop, and ControlFlow-already-declared errors as Z3 loses sync. Add a writerLock that guards the WriteLine + Flush pair so each command reaches Z3 as a single contiguous byte stream. 3. Pipe-death normalization across Send + ExecutionEngine (Source/Provers/SMTLib/SMTLibProcess.cs, Source/ExecutionEngine/ExecutionEngine.cs). When the solver process exits mid-verification (crash, OOM, hard timeout kill), Send's WriteLine/Flush throw ObjectDisposedException or IOException raw. Checker.Check's generic `catch (Exception e)` wraps them as UnexpectedProverOutputException(e.ToString()), and ExecutionEngine reports Advisory: SKIPPED because of internal error: unexpected prover output: System.ObjectDisposedException: ... with VcOutcome.Inconclusive. Convert those into the existing ProverDiedException in Send (already thrown from PingPong when Z3 returns null, so both code paths now speak the same language), and in ExecutionEngine.VerifyImplementationWithLargeThread replace the `catch (ProverDiedException) { throw; }` -- which today bubbles to VerifyEachImplementation and aborts the whole multi-spec run with "Fatal Error: ProverException" -- with a per-spec handler that emits a clean advisory and sets VcOutcome.SolverException, matching the sibling IOException branch. Also: add .foxy/sessions to .gitignore. Tested: - dotnet build Source/Boogie.sln -c Release: 0 warnings, 0 errors (-warnaserror). - dotnet test Source/Boogie.sln: 281/281 pass (CoreTests 58, ExecutionEngineTests 27, BaseTypesTests 196). - lit Test/: 635 pass, 2 XFAIL; 6 remaining failures are pre-existing and environmental (cvc5 binary missing, Z3-version-specific model output). Verified they fail identically with these changes reverted. - End-to-end on cetus_clmm_specs: clmm_math::get_delta_down_from_output_spec and clmm_math::get_liquidity_by_amount_spec now verify cleanly where they previously crashed with Cce.UnreachableException and ObjectDisposedException respectively. Co-Authored-By: Claude Opus 4.7 --- .gitignore | 1 + Source/ExecutionEngine/ExecutionEngine.cs | 12 +++++- Source/Provers/SMTLib/SMTLibProcess.cs | 42 ++++++++++++++++++++- Source/VCGeneration/Splits/BlockRewriter.cs | 12 +++++- 4 files changed, 62 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index 31c75878f..3024cdf22 100644 --- a/.gitignore +++ b/.gitignore @@ -42,3 +42,4 @@ Source/*.userprefs # Rider files .idea/ +.foxy/sessions diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index d3868530d..d0dfc7f70 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1020,9 +1020,17 @@ private Task VerifyImplementationWithLargeThread(Proces verificationResult.Errors = null; verificationResult.VcOutcome = VcOutcome.Inconclusive; } - catch (ProverDiedException) + catch (ProverDiedException e) { - throw; + // Z3 (or whichever SMT solver) exited mid-verification -- crash, OOM, + // hard timeout kill, a malformed earlier command, etc. Surface it as a + // per-spec solver exception instead of propagating (which would abort + // the entire multi-spec run at VerifyEachImplementation). + Options.Printer.AdvisoryWriteLine(traceWriter, + "Advisory: {0} SKIPPED because the prover died: {1}", + impl.VerboseName, e.Message); + verificationResult.Errors = null; + verificationResult.VcOutcome = VcOutcome.SolverException; } catch (UnexpectedProverOutputException upo) { diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index f0669f471..9b9fd6438 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -18,6 +18,16 @@ public class SMTLibProcess : SMTLibSolver { private readonly AsyncQueue solverOutput = new(); // Used to synchronise between requests into this class. private readonly SemaphoreSlim asyncLock = new(1); + // Guards the underlying stdin pipe so that a whole SMT command (WriteLine + Flush) + // is written atomically. asyncLock only serializes the high-level async operations + // (SendRequest / PingPong / SendRequestsAndCloseInput); plenty of call sites invoke + // Send directly while some *other* thread is holding asyncLock (e.g. a sync + // SendThisVC during VC setup concurrent with a ping from another checker under + // -vcsCores>1 + keep-going splits). Without this monitor the writer's chunked + // WriteLine + separate Flush can interleave, splicing one command's bytes into + // another -- which Z3 reports as "(get-info :name)" appearing inside a + // declare-fun identifier, "invalid let declaration", etc. + private readonly object writerLock = new(); private TextWriter toProver; private readonly int smtProcessId; private static int smtProcessIdSeq = 0; @@ -133,8 +143,36 @@ public override void Send(string cmd) Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log); } - toProver.WriteLine(cmd); - toProver.Flush(); + // If the solver process has already exited (crash, OOM, killed on timeout, + // etc.), its stdin pipe is closed; WriteLine/Flush throw ObjectDisposedException + // or IOException. Normalize those into ProverDiedException so upstream handlers + // can surface a clean per-spec SolverException instead of a noisy + // "unexpected prover output" advisory with a System.ObjectDisposedException + // stack trace as the message. + var writer = toProver; + if (writer == null) + { + throw new ProverDiedException(); + } + + // Hold writerLock across BOTH the WriteLine and the Flush so a single SMT + // command is written to Z3's stdin as a single contiguous byte stream. + try + { + lock (writerLock) + { + writer.WriteLine(cmd); + writer.Flush(); + } + } + catch (ObjectDisposedException) + { + throw new ProverDiedException(); + } + catch (IOException) + { + throw new ProverDiedException(); + } } public override async Task SendRequest(string request, CancellationToken cancellationToken = default) { diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs index 856e28c9c..d66c6bf68 100644 --- a/Source/VCGeneration/Splits/BlockRewriter.cs +++ b/Source/VCGeneration/Splits/BlockRewriter.cs @@ -169,8 +169,18 @@ public List ComputeNewBlocks( newBlocks.Reverse(); BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); - + BlockCoalescer.CoalesceInPlace(newBlocks); + + // ShallowClone leaves Predecessors empty, and DeleteBlocksNotLeadingToAssertions + // / BlockCoalescer.CoalesceInPlace rewrite gotos without updating downstream + // Predecessors lists. Rebuild them so callers (notably Split.CountAssertions, + // which uses Predecessors.Count to decide block coalescing) see the final CFG. + foreach (var block in newBlocks) { + block.Predecessors.Clear(); + } + Implementation.ComputePredecessorsForBlocks(newBlocks); + return newBlocks; }