From 2f15adece76fa06e819c745e64fe12585283ba71 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Fri, 24 Apr 2026 18:52:00 +0000 Subject: [PATCH 1/3] Extend pool-based quantifier instantiation to axioms; add diagnostic flags QI / axioms: Axioms with {:pool ...} or {:add_to_pool ...} annotations now participate in pool-based quantifier instantiation. Previously only assume/assert commands fed the pool machinery, so axiom quantifiers with pool hints silently did nothing. Lifted-lambda definition axioms stay on the BindLambdaFunction path to avoid double-instantiation. Per-impl gating adds PoolHintChecker.HasPoolAxioms so QI is skipped cleanly when an impl has no sources and no non-lambda pool axioms. /poolTrace: Per-impl trace emitted as each implementation runs: pool contents (pretty-printed via VCExprPrinter), per-quantifier instantiation counts (keyed by qid), and the count of candidates dropped by pool-type mismatch. Writes are serialized against parallel-split races via a static lock on Options.OutputWriter. /poolSummary: One-shot audit emitted at verification start: axiom counts (total / pool-bearing / lambda-definition / plain); quantifier counts (total / pool-bearing / polymorphic / plain); per-pool producer/consumer locations with (!! no producers) / (!! no consumers) warnings for orphans. Plain axioms and quantifiers are listed exhaustively so users can grep/sort them when deciding where to add pool hints. Walks program.Axioms unioned with program.Functions.DefinitionAxioms. /jsonOutput:: Structured per-implementation verification results via System.Text.Json (no new dependencies). Filename "-" routes through Options.OutputWriter for library-embedding friendliness. Outcome lowercased to match XML. Handles AssertCounterexample, CallCounterexample (precondition violations), and ReturnCounterexample (postcondition violations) with correct location and message for each. Tests: Test/inst/axiom.bpl -- pool instantiation via axioms Test/inst/poolTrace.bpl -- /poolTrace golden output Test/inst/poolSummary.bpl -- /poolSummary golden output Test/commandline/jsonOutput.bpl -- /jsonOutput schema check Full lit suite: 55 pre-existing failures, unchanged by this work. NUnit: 85 pass. Co-Authored-By: Claude Opus 4.7 (1M context) --- Source/BoogieDriver/BoogieDriver.cs | 5 + Source/Core/CoreOptions.cs | 3 + Source/Core/JsonSink.cs | 104 +++++++++ Source/ExecutionEngine/CommandLineOptions.cs | 48 +++- Source/ExecutionEngine/ExecutionEngine.cs | 7 + .../ImplementationRunResult.cs | 48 ++++ .../VCExpr/QuantifierInstantiationEngine.cs | 187 ++++++++++++++- Source/VCGeneration/PoolSummary.cs | 220 ++++++++++++++++++ Source/VCGeneration/Splits/Split.cs | 2 +- Test/commandline/jsonOutput.bpl | 17 ++ Test/commandline/jsonOutput.bpl.expect | 39 ++++ Test/inst/axiom.bpl | 42 ++++ Test/inst/axiom.bpl.expect | 2 + Test/inst/poolSummary.bpl | 13 ++ Test/inst/poolSummary.bpl.expect | 10 + Test/inst/poolTrace.bpl | 10 + Test/inst/poolTrace.bpl.expect | 5 + 17 files changed, 755 insertions(+), 7 deletions(-) create mode 100644 Source/Core/JsonSink.cs create mode 100644 Source/VCGeneration/PoolSummary.cs create mode 100644 Test/commandline/jsonOutput.bpl create mode 100644 Test/commandline/jsonOutput.bpl.expect create mode 100644 Test/inst/axiom.bpl create mode 100644 Test/inst/axiom.bpl.expect create mode 100644 Test/inst/poolSummary.bpl create mode 100644 Test/inst/poolSummary.bpl.expect create mode 100644 Test/inst/poolTrace.bpl create mode 100644 Test/inst/poolTrace.bpl.expect diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index b80be0ec6..2f08269af 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -78,6 +78,11 @@ public static int Main(string[] args) options.XmlSink.Close(); } + if (options.JsonSink != null) + { + options.JsonSink.Close(); + } + if (options.Wait) { Console.WriteLine("Press Enter to exit."); diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index 075ed432d..0bad48e1f 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -109,6 +109,9 @@ public enum VerbosityLevel double VcsPathJoinMult { get; } bool VerifySeparately { get; } bool KeepQuantifier { get; } + bool PoolTrace { get; } + bool PoolSummary { get; } + JsonSink JsonSink { get; } public enum ProverWarnings { diff --git a/Source/Core/JsonSink.cs b/Source/Core/JsonSink.cs new file mode 100644 index 000000000..5caa75ef7 --- /dev/null +++ b/Source/Core/JsonSink.cs @@ -0,0 +1,104 @@ +using System; +using System.IO; +using System.Text.Json; +using System.Text.Json.Nodes; + +namespace Microsoft.Boogie +{ + // /jsonOutput: — writes one structured JSON document per Boogie run, + // with per-implementation verification results. Designed for tooling / AI + // consumers that want a stable machine-readable surface. + // + // Schema (v1): + // { + // "boogieVersion": "3.x.x", + // "commandLine": "...", + // "implementations": [ + // { + // "name": "Foo", + // "location": { "file": "...", "line": 12, "column": 5 }, + // "outcome": "Correct" | "Errors" | "TimedOut" | ..., + // "durationMs": 1234.5, + // "resourceCount": 1000, + // "errors": [ + // { "message": "...", "location": { "file": ..., "line": ..., "column": ... } } + // ] + // } + // ] + // } + public sealed class JsonSink + { + private readonly string filename; // "-" means options.OutputWriter + private readonly CoreOptions options; + private readonly JsonObject root = new(); + private readonly JsonArray implementations = new(); + private readonly object gate = new(); + + public JsonSink(CoreOptions options, string filename) + { + this.filename = filename; + this.options = options; + root["boogieVersion"] = options.VersionNumber; + root["commandLine"] = Environment.CommandLine; + root["implementations"] = implementations; + } + + public readonly struct ErrorRecord + { + public readonly string Message; + public readonly IToken Tok; + public ErrorRecord(string message, IToken tok) { Message = message; Tok = tok; } + } + + public void WriteImplementationResult(string name, IToken tok, string outcome, + double durationMs, int resourceCount, System.Collections.Generic.IEnumerable errors) + { + var obj = new JsonObject + { + ["name"] = name, + ["location"] = LocationOf(tok), + ["outcome"] = outcome, + ["durationMs"] = durationMs, + ["resourceCount"] = resourceCount + }; + var errorArr = new JsonArray(); + foreach (var e in errors) + { + errorArr.Add(new JsonObject + { + ["message"] = e.Message, + ["location"] = LocationOf(e.Tok) + }); + } + obj["errors"] = errorArr; + lock (gate) + { + implementations.Add(obj); + } + } + + public void Close() + { + var json = root.ToJsonString(new JsonSerializerOptions { WriteIndented = true }); + if (filename == "-") + { + options.OutputWriter.WriteLine(json); + options.OutputWriter.Flush(); + } + else + { + File.WriteAllText(filename, json); + } + } + + private static JsonObject LocationOf(IToken tok) + { + return new JsonObject + { + ["file"] = tok?.filename ?? "", + ["line"] = tok?.line ?? 0, + ["column"] = tok?.col ?? 0 + }; + } + } +} diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index e60113793..16f9017f4 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -210,6 +210,8 @@ public bool PrintWithUniqueASTIds { private string XmlSinkFilename { get; set; } [Peer] public XmlSink XmlSink { get; set; } + public JsonSink JsonSink { get; set; } + private string JsonSinkFilename { get; set; } public bool Wait { get; set; } public bool Trace => Verbosity == CoreOptions.VerbosityLevel.Trace; @@ -559,6 +561,16 @@ public bool KeepQuantifier { set => keepQuantifier = value; } + public bool PoolTrace { + get => poolTrace; + set => poolTrace = value; + } + + public bool PoolSummary { + get => poolSummary; + set => poolSummary = value; + } + public HashSet Libraries { get; set; } = new HashSet(); // Note that procsToCheck stores all patterns

supplied with /proc:

@@ -609,6 +621,8 @@ void ObjectInvariant5() private bool normalizeNames; private bool normalizeDeclarationOrder = true; private bool keepQuantifier = false; + private bool poolTrace = false; + private bool poolSummary = false; public List Cho { get; set; } = new(); @@ -701,6 +715,14 @@ protected override bool ParseOption(string name, CommandLineParseState ps) return true; + case "jsonOutput": + if (ps.ConfirmArgumentCount(1)) + { + JsonSinkFilename = args[ps.i]; + } + + return true; + case "printPruned": case "printSplit": if (ps.ConfirmArgumentCount(1)) @@ -1390,7 +1412,9 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) || ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) || ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) || - ps.CheckBooleanFlag("keepQuantifier", x => keepQuantifier = x) + ps.CheckBooleanFlag("keepQuantifier", x => keepQuantifier = x) || + ps.CheckBooleanFlag("poolTrace", x => poolTrace = x) || + ps.CheckBooleanFlag("poolSummary", x => poolSummary = x) ) { // one of the boolean flags matched @@ -1422,6 +1446,11 @@ public override void ApplyDefaultOptions() XmlSink = new XmlSink(this, XmlSinkFilename); } + if (JsonSinkFilename != null) + { + JsonSink = new JsonSink(this, JsonSinkFilename); + } + if (printErrorModelFile != null) { ModelWriter = new StreamWriter(printErrorModelFile, false); } @@ -2019,6 +2048,23 @@ not covered by a proof. If pool-based quantifier instantiation creates instances of a quantifier then keep the quantifier along with the instances. By default, the quantifier is dropped if any instances are created. + /poolTrace + Emit diagnostics about pool-based quantifier instantiation as each + implementation is verified: which pool received which values, how + many instances each factorized quantifier produced, and which + candidate instances were dropped due to pool-type mismatches. + Useful for debugging why a {:pool ...} annotation did not fire. + /poolSummary + At the start of verification, print a summary: count of axioms + (total, pool-bearing, lambda-definition, plain); count of + quantifiers (total, pool-bearing, polymorphic); and the pool names + referenced in the program, with their producer/consumer locations. + Useful for auditing pool annotations across a program. + /jsonOutput: + Write a structured JSON document summarising the verification run: + per-implementation outcome, duration, resource count, and errors + with source locations. Use '-' as the filename to write to stdout. + Intended for programmatic / AI consumers. ---- Verification-condition splitting -------------------------------------- diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index d0dfc7f70..77cc210b1 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -590,6 +590,12 @@ public async Task InferAndVerify( action(Options, processedProgram); } + if (Options.PoolSummary) + { + PoolSummary.Emit(processedProgram.Program, Options.OutputWriter); + Options.OutputWriter.Flush(); + } + if (!Options.Verify) { return PipelineOutcome.Done; @@ -767,6 +773,7 @@ private async Task VerifyEachImplementation(TextWriter outputWr await Task.WhenAll(tasks); foreach (var task in tasks) { task.Result.ProcessXml(this); + task.Result.ProcessJson(this); } } catch(TaskCanceledException) { outcome = PipelineOutcome.Cancelled; diff --git a/Source/ExecutionEngine/ImplementationRunResult.cs b/Source/ExecutionEngine/ImplementationRunResult.cs index bd9c89cfe..c07147cd8 100644 --- a/Source/ExecutionEngine/ImplementationRunResult.cs +++ b/Source/ExecutionEngine/ImplementationRunResult.cs @@ -68,6 +68,54 @@ public String GetOutput(OutputPrinter printer, return result.ToString(); } + public void ProcessJson(ExecutionEngine engine) { + var sink = engine.Options.JsonSink; + if (sink == null) { return; } + var errors = Errors.Select(ExtractError); + sink.WriteImplementationResult( + implementation.VerboseName, + implementation.tok, + VcOutcome.ToString().ToLowerInvariant(), + Elapsed.TotalMilliseconds, + ResourceCount, + errors); + } + + private JsonSink.ErrorRecord ExtractError(Counterexample cex) { + // Each Counterexample subtype reports a different failure shape. + IToken tok; + string msg; + switch (cex) { + case CallCounterexample call: + // Precondition violation at a call site. + tok = call.FailingCall.tok; + msg = call.FailingRequires.ErrorMessage + ?? call.FailingRequires.Description?.FailureDescription + ?? "a precondition could not be proved"; + break; + case ReturnCounterexample ret: + // Postcondition violation at a return site. + tok = ret.FailingReturn.tok; + msg = ret.FailingEnsures.ErrorMessage + ?? ret.FailingEnsures.Description?.FailureDescription + ?? "a postcondition could not be proved"; + break; + case AssertCounterexample asrt: + tok = asrt.FailingAssert.tok; + msg = asrt.FailingAssert.ErrorMessage + ?? asrt.FailingAssert.Description?.FailureDescription + ?? "this assertion could not be proved"; + break; + default: + tok = cex.FailingAssert?.tok ?? implementation.tok; + msg = cex.FailingAssert?.ErrorMessage + ?? cex.FailingAssert?.Description?.FailureDescription + ?? "verification failed"; + break; + } + return new JsonSink.ErrorRecord(msg, tok); + } + public void ProcessXml(ExecutionEngine engine) { if (engine.Options.XmlSink == null) { return; diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index eb67c8024..2d7857920 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -53,14 +53,22 @@ public QuantifierInstantiationInfo(Dictionary> boundV private Boogie2VCExprTranslator exprTranslator; internal static ConcurrentDictionary> labelToTypes = new(); // pool name may map to multiple types - public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr) + // /poolTrace instrumentation — populated only when Options.PoolTrace is true. + private Dictionary traceInstantiationCount; + private Dictionary traceTypeMismatchCount; + // Guards writes to Options.OutputWriter so parallel splits don't interleave + // multi-line traces. Writers themselves aren't guaranteed thread-safe. + private static readonly object poolTraceWriteLock = new(); + + public static VCExpr Instantiate(Program program, Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr) { - if (!InstantiationSourceChecker.HasInstantiationSources(impl)) + if (!InstantiationSourceChecker.HasInstantiationSources(impl) && + !PoolHintChecker.HasPoolAxioms(program)) { return vcExpr; } var qiEngine = new QuantifierInstantiationEngine(vcExprGen, exprTranslator); - return qiEngine.Execute(impl, vcExpr); + return qiEngine.Execute(program, impl, vcExpr); } private QuantifierInstantiationEngine(VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator) @@ -77,8 +85,12 @@ private QuantifierInstantiationEngine(VCExpressionGenerator vcExprGen, Boogie2VC this.skolemConstantNamePrefix = "skolemConstant"; this.vcExprGen = vcExprGen; this.exprTranslator = exprTranslator; + this.traceInstantiationCount = new Dictionary(); + this.traceTypeMismatchCount = new Dictionary(); } + private bool PoolTraceEnabled => exprTranslator.GenerationOptions.Options.PoolTrace; + public static void SubstituteIncarnationInInstantiationSources(Cmd cmd, Substitution incarnationSubst) { var attrCmd = cmd as ICarriesAttributes; @@ -242,12 +254,47 @@ private static void AddDictionary(Dictionary>> @from, D }); } - private VCExpr Execute(Implementation impl, VCExpr vcExpr) + private VCExpr Execute(Program program, Implementation impl, VCExpr vcExpr) { impl.Blocks.ForEach(block => block.Cmds.OfType().ForEach(predicateCmd => { AddDictionary(FindInstantiationSources(predicateCmd, exprTranslator), labelToInstances); })); + // Pool-bearing axioms contribute to the implementation's pool the same way + // top-level assumes do: their add_to_pool sources feed labelToInstances, + // and their expressions are threaded into the VC as an antecedent so their + // pool-annotated quantifiers get factorized and instantiated by the fixpoint + // loop below. The axioms remain in the prover context via ctx.AddAxiom; the + // antecedent just materializes ground instances as hints. + // + // Definition axioms of lifted lambdas are skipped: BindLambdaFunction and + // InstantiateLambdaDefinition already instantiate them against actual call + // sites, and pool-expanding them here would double-process and bloat the VC. + var lambdaDefinitionAxioms = program.Functions + .Where(f => f.OriginalLambdaExprAsString != null) + .SelectMany(f => f.DefinitionAxioms) + .ToHashSet(); + var axiomAntecedents = new List(); + foreach (var axiom in program.Axioms) + { + if (lambdaDefinitionAxioms.Contains(axiom)) + { + continue; + } + if (!PoolHintChecker.AxiomCarriesPoolHints(axiom)) + { + continue; + } + AddDictionary(FindInstantiationSources(axiom, exprTranslator), labelToInstances); + axiomAntecedents.Add(exprTranslator.Translate(axiom.Expr)); + } + if (axiomAntecedents.Count > 0) + { + var axiomConj = axiomAntecedents.Count == 1 + ? axiomAntecedents[0] + : vcExprGen.NAry(VCExpressionGenerator.AndOp, axiomAntecedents); + vcExpr = vcExprGen.Implies(axiomConj, vcExpr); + } vcExpr = Skolemizer.Skolemize(this, Polarity.Negative, vcExpr); while (labelToInstances.Count > 0 || lambdaToInstances.Count > 0) { @@ -316,6 +363,10 @@ private VCExpr Execute(Implementation impl, VCExpr vcExpr) } } + if (PoolTraceEnabled) + { + EmitPoolTrace(impl); + } var lambdaAxioms = vcExprGen.NAry(VCExpressionGenerator.AndOp, lambdaDefinition.Values .SelectMany(quantifierExpr => quantifierInstantiationInfo[quantifierExpr].instances.Values.ToList()).ToList()); @@ -424,6 +475,10 @@ private void InstantiateQuantifierAtInstance(VCExprQuantifier quantifierExpr, Li { if (!quantifierExpr.BoundVars[i].Type.Equals(instance[i].Type)) { + if (PoolTraceEnabled) + { + traceTypeMismatchCount[quantifierExpr] = traceTypeMismatchCount.GetValueOrDefault(quantifierExpr) + 1; + } return; } } @@ -437,6 +492,47 @@ private void InstantiateQuantifierAtInstance(VCExprQuantifier quantifierExpr, Li quantifierInstantiationInfo.instances[new List(instance)] = Skolemizer.Skolemize(this, quantifierExpr.Quan == Quantifier.ALL ? Polarity.Positive : Polarity.Negative, instantiation); + if (PoolTraceEnabled) + { + traceInstantiationCount[quantifierExpr] = traceInstantiationCount.GetValueOrDefault(quantifierExpr) + 1; + } + } + + private static string PrettyPrint(VCExpr e) + { + var sw = new System.IO.StringWriter(); + new VCExprPrinter(PrintOptions.Default).Print(e, sw); + return sw.ToString(); + } + + private void EmitPoolTrace(Implementation impl) + { + var sb = new System.Text.StringBuilder(); + sb.AppendLine($"[poolTrace] impl {impl.Name}"); + var poolNames = accLabelToInstances.Keys.Concat(labelToInstances.Keys).Distinct().OrderBy(x => x); + foreach (var pool in poolNames) + { + var vals = new HashSet(); + if (accLabelToInstances.TryGetValue(pool, out var acc)) { vals.UnionWith(acc); } + if (labelToInstances.TryGetValue(pool, out var pending)) { vals.UnionWith(pending); } + sb.AppendLine($"[poolTrace] pool \"{pool}\" ({vals.Count} value(s)): {string.Join(", ", vals.Select(PrettyPrint))}"); + } + foreach (var kv in quantifierInstantiationInfo) + { + var q = kv.Key; + var qid = q.Info.qid ?? ""; + var count = traceInstantiationCount.GetValueOrDefault(q); + var drops = traceTypeMismatchCount.GetValueOrDefault(q); + var labels = string.Join(",", kv.Value.relevantLabels.OrderBy(x => x)); + var tail = drops > 0 ? $" ({drops} dropped by type mismatch)" : ""; + sb.AppendLine($"[poolTrace] qid={qid} pool={{{labels}}} instances={count}{tail}"); + } + var writer = exprTranslator.GenerationOptions.Options.OutputWriter; + lock (poolTraceWriteLock) + { + writer.Write(sb.ToString()); + writer.Flush(); + } } } @@ -851,7 +947,7 @@ private InstantiationSourceChecker() { this.hasInstances = false; } - + public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { FindInstantiationSources(node); @@ -864,4 +960,85 @@ public override List VisitCmdSeq(List cmdSeq) return base.VisitCmdSeq(cmdSeq); } } + + public class PoolHintChecker : ReadOnlyVisitor + { + // Recognizes axioms that interact with pool-based instantiation: either the + // axiom (or any embedded quantifier) carries {:add_to_pool ...}, or a + // quantifier's bound var carries {:pool ...}. Unlike InstantiationSourceChecker, + // this does not require the pool type to be pre-registered — an axiom can be + // the sole consumer of a pool seeded by impl commands. + private bool found; + + public static bool AxiomCarriesPoolHints(Axiom axiom) + { + var checker = new PoolHintChecker(); + checker.VisitAxiom(axiom); + return checker.found; + } + + // Gate for running QI solely on axiom pool hints. Lifted-lambda definition + // axioms are excluded here: they are handled specially by BindLambdaFunction + // and should not force QI to run when the implementation has no pool sources. + public static bool HasPoolAxioms(Program program) + { + var lambdaDefinitionAxioms = program.Functions + .Where(f => f.OriginalLambdaExprAsString != null) + .SelectMany(f => f.DefinitionAxioms) + .ToHashSet(); + foreach (var axiom in program.Axioms) + { + if (lambdaDefinitionAxioms.Contains(axiom)) + { + continue; + } + if (AxiomCarriesPoolHints(axiom)) + { + return true; + } + } + return false; + } + + private static bool HasAttribute(ICarriesAttributes o, string key) + { + for (var iter = o.Attributes; iter != null; iter = iter.Next) + { + if (iter.Key == key) + { + return true; + } + } + return false; + } + + public override Axiom VisitAxiom(Axiom node) + { + if (HasAttribute(node, "add_to_pool")) + { + found = true; + } + return found ? node : base.VisitAxiom(node); + } + + public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) + { + if (HasAttribute(node, "add_to_pool")) + { + found = true; + } + if (!found) + { + foreach (var dummy in node.Dummies) + { + if (HasAttribute(dummy, "pool")) + { + found = true; + break; + } + } + } + return found ? node : base.VisitQuantifierExpr(node); + } + } } diff --git a/Source/VCGeneration/PoolSummary.cs b/Source/VCGeneration/PoolSummary.cs new file mode 100644 index 000000000..1fb2ea0f3 --- /dev/null +++ b/Source/VCGeneration/PoolSummary.cs @@ -0,0 +1,220 @@ +using System.Collections.Generic; +using System.IO; +using System.Linq; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie +{ + // Implements the /poolSummary option. Walks a program's axioms and quantifier + // expressions, classifies them by pool / polymorphism / lambda-definition, and + // emits a short report so users can audit pool annotations across a program at + // a glance. + public static class PoolSummary + { + public static void Emit(Program program, TextWriter writer) + { + var lambdaAxioms = program.Functions + .Where(f => f.OriginalLambdaExprAsString != null) + .SelectMany(f => f.DefinitionAxioms) + .ToHashSet(); + + int axiomTotal = 0, axiomPool = 0, axiomLambda = 0, axiomPlain = 0; + var poolAxiomLocations = new List(); + var plainAxiomLocations = new List(); + var poolProducers = new Dictionary>(); + var poolConsumers = new Dictionary>(); + + void AddTo(Dictionary> dict, string pool, string loc) + { + if (!dict.TryGetValue(pool, out var list)) + { + dict[pool] = list = new List(); + } + list.Add(loc); + } + + // program.Axioms only returns top-level Axiom declarations; function-level + // DefinitionAxioms are attached via Function.DefinitionAxiom(s) and may not + // always be moved to top level, so walk both and dedupe by reference. + var allAxioms = new HashSet(program.Axioms); + foreach (var f in program.Functions) + { + foreach (var a in f.DefinitionAxioms) { allAxioms.Add(a); } + } + foreach (var axiom in allAxioms) + { + axiomTotal++; + if (lambdaAxioms.Contains(axiom)) + { + axiomLambda++; + continue; // lambda-defn axioms get their pool hints reported via quantifiers below + } + var carriesPool = PoolHintChecker.AxiomCarriesPoolHints(axiom); + if (carriesPool) + { + axiomPool++; + poolAxiomLocations.Add(TokLoc(axiom.tok)); + CollectAxiomAttrPools(axiom, poolProducers); + } + else + { + axiomPlain++; + plainAxiomLocations.Add(TokLoc(axiom.tok)); + } + } + + // Commands also contribute {:add_to_pool} producers. + foreach (var impl in program.Implementations) + { + foreach (var block in impl.Blocks) + { + foreach (var cmd in block.Cmds.OfType()) + { + for (var kv = cmd.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "add_to_pool" && kv.Params.Count > 0 && kv.Params[0] is string poolName) + { + AddTo(poolProducers, poolName, TokLoc(cmd.tok)); + } + } + } + } + } + + var collector = new QuantifierCollectorVisitor(); + collector.VisitProgram(program); + + int qTotal = collector.quantifiers.Count; + int qPlain = 0; + var poolQuantifiers = new List(); + var polyQuantifiers = new List(); + var plainQuantifiers = new List(); + foreach (var q in collector.quantifiers) + { + var hasPool = false; + foreach (var dummy in q.Dummies) + { + var labels = QuantifierInstantiationEngine.FindInstantiationHints(dummy); + foreach (var label in labels) + { + AddTo(poolConsumers, label, TokLoc(q.tok)); + hasPool = true; + } + } + for (var kv = q.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "add_to_pool" && kv.Params.Count > 0 && kv.Params[0] is string poolName) + { + AddTo(poolProducers, poolName, TokLoc(q.tok)); + hasPool = true; + } + } + var isPoly = q.TypeParameters.Count > 0; + if (hasPool) { poolQuantifiers.Add(TokLoc(q.tok)); } + if (isPoly) { polyQuantifiers.Add(TokLoc(q.tok)); } + if (!hasPool && !isPoly) + { + qPlain++; + plainQuantifiers.Add(TokLoc(q.tok)); + } + } + int qPool = poolQuantifiers.Count; + int qPoly = polyQuantifiers.Count; + + writer.WriteLine($"[poolSummary] axioms: {axiomTotal} total ({axiomPool} pool-bearing, {axiomLambda} lambda-definition, {axiomPlain} plain)"); + if (poolAxiomLocations.Count > 0) + { + writer.WriteLine($"[poolSummary] pool axioms at: {FormatLocs(poolAxiomLocations)}"); + } + if (plainAxiomLocations.Count > 0) + { + writer.WriteLine($"[poolSummary] plain axioms at: {FormatLocsAll(plainAxiomLocations)}"); + } + writer.WriteLine($"[poolSummary] quantifiers: {qTotal} total ({qPool} pool-bearing, {qPoly} polymorphic, {qPlain} plain)"); + if (poolQuantifiers.Count > 0) + { + writer.WriteLine($"[poolSummary] pool-bearing quantifiers at: {FormatLocs(poolQuantifiers)}"); + } + if (polyQuantifiers.Count > 0) + { + writer.WriteLine($"[poolSummary] polymorphic quantifiers at: {FormatLocs(polyQuantifiers)}"); + } + if (plainQuantifiers.Count > 0) + { + writer.WriteLine($"[poolSummary] plain quantifiers at: {FormatLocsAll(plainQuantifiers)}"); + } + + var allPools = poolProducers.Keys.Concat(poolConsumers.Keys).Distinct().OrderBy(x => x).ToList(); + if (allPools.Count > 0) + { + writer.WriteLine($"[poolSummary] pools referenced: {allPools.Count}"); + foreach (var pool in allPools) + { + var producers = poolProducers.TryGetValue(pool, out var ps) ? ps : new List(); + var consumers = poolConsumers.TryGetValue(pool, out var cs) ? cs : new List(); + var warn = ""; + if (producers.Count == 0) { warn = " (!! no producers)"; } + else if (consumers.Count == 0) { warn = " (!! no consumers)"; } + writer.WriteLine($"[poolSummary] \"{pool}\": producers={{{FormatLocs(producers)}}} consumers={{{FormatLocs(consumers)}}}{warn}"); + } + } + } + + private static string TokLoc(IToken tok) + { + var file = tok.filename; + if (string.IsNullOrEmpty(file) || file == "" || tok.line == 0) + { + return ""; + } + var slash = file.LastIndexOfAny(new[] { '/', '\\' }); + if (slash >= 0) { file = file.Substring(slash + 1); } + return $"{file}:{tok.line}"; + } + + private const int MaxLocsShown = 5; + + private static string FormatLocs(List locs) + { + var distinct = locs.Distinct().OrderBy(x => x).ToList(); + if (distinct.Count <= MaxLocsShown) + { + return string.Join(",", distinct); + } + var head = distinct.Take(MaxLocsShown); + return $"{string.Join(",", head)},... and {distinct.Count - MaxLocsShown} more"; + } + + // Plain axioms/quantifiers are listed exhaustively (no cap, no aggregation) + // so users can pipe the output to grep / sort and target pool hints precisely. + private static string FormatLocsAll(List locs) + { + return string.Join(",", locs.Distinct().OrderBy(x => x)); + } + + private static void CollectAxiomAttrPools(Axiom axiom, Dictionary> producers) + { + for (var kv = axiom.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "add_to_pool" && kv.Params.Count > 0 && kv.Params[0] is string poolName) + { + if (!producers.TryGetValue(poolName, out var list)) + { + producers[poolName] = list = new List(); + } + list.Add(TokLoc(axiom.tok)); + } + } + } + + private class QuantifierCollectorVisitor : ReadOnlyVisitor + { + public readonly List quantifiers = new(); + public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) + { + quantifiers.Add(node); + return base.VisitQuantifierExpr(node); + } + } + } +} diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs index f75628554..3035d704b 100644 --- a/Source/VCGeneration/Splits/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -961,7 +961,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa vc = parent.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, checker.TheoremProver.Context); Contract.Assert(vc != null); - vc = QuantifierInstantiationEngine.Instantiate(Implementation, exprGen, bet, vc); + vc = QuantifierInstantiationEngine.Instantiate(parent.program, Implementation, exprGen, bet, vc); VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); diff --git a/Test/commandline/jsonOutput.bpl b/Test/commandline/jsonOutput.bpl new file mode 100644 index 000000000..c889e14e8 --- /dev/null +++ b/Test/commandline/jsonOutput.bpl @@ -0,0 +1,17 @@ +// Writes JSON to a file, strips non-deterministic fields (durationMs, resourceCount, +// boogieVersion, commandLine) and the runtime-dependent file path, then diffs. +// RUN: %parallel-boogie "%s" /jsonOutput:"%t.json" > "%t.stdout" +// RUN: sed -e 's/"durationMs": [0-9.]*/"durationMs": _/g' -e 's/"resourceCount": [0-9]*/"resourceCount": _/g' -e 's/"boogieVersion": "[^"]*"/"boogieVersion": "_"/g' -e 's/"commandLine": "[^"]*"/"commandLine": "_"/g' "%t.json" > "%t.normalized.json" +// RUN: %diff "%s.expect" "%t.normalized.json" + +procedure Foo(x: int) returns (y: int) + ensures y >= x; +{ + y := x; +} + +procedure Bar(x: int) returns (y: int) + ensures y > x; +{ + y := x; +} diff --git a/Test/commandline/jsonOutput.bpl.expect b/Test/commandline/jsonOutput.bpl.expect new file mode 100644 index 000000000..cafeaf426 --- /dev/null +++ b/Test/commandline/jsonOutput.bpl.expect @@ -0,0 +1,39 @@ +{ + "boogieVersion": "_", + "commandLine": "_", + "implementations": [ + { + "name": "Foo", + "location": { + "file": "jsonOutput.bpl", + "line": 7, + "column": 11 + }, + "outcome": "correct", + "durationMs": _, + "resourceCount": _, + "errors": [] + }, + { + "name": "Bar", + "location": { + "file": "jsonOutput.bpl", + "line": 13, + "column": 11 + }, + "outcome": "errors", + "durationMs": _, + "resourceCount": _, + "errors": [ + { + "message": "this is the postcondition that could not be proved", + "location": { + "file": "jsonOutput.bpl", + "line": 17, + "column": 1 + } + } + ] + } + ] +} \ No newline at end of file diff --git a/Test/inst/axiom.bpl b/Test/inst/axiom.bpl new file mode 100644 index 000000000..f057925e4 --- /dev/null +++ b/Test/inst/axiom.bpl @@ -0,0 +1,42 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// Regression: pool-based quantifier instantiation must consider axioms too, +// not only assume/assert commands inside implementations. + +function F(int): bool; +function G(int, int): bool; + +axiom (forall {:pool "L"} x: int :: F(x - 1)); + +procedure A0() +{ + assert {:add_to_pool "L", 1} F(0); +} + +procedure A1() +{ + assert (forall y: int :: {:add_to_pool "L", y + 1} F(y)); +} + +axiom (forall {:pool "M0"} x0: int, {:pool "M1"} x1: int :: G(x0 - 1, x1 - 1)); + +procedure B0() +{ + assert {:add_to_pool "M0", 1} {:add_to_pool "M1", 1} G(0, 0); +} + +procedure B1() +{ + assert (forall y0, y1: int :: {:add_to_pool "M0", y0 + 1} {:add_to_pool "M1", y1 + 1} G(y0, y1)); +} + +// add_to_pool carried on the axiom itself also works. +function H(int): bool; + +axiom {:add_to_pool "K", 5} (forall {:pool "K"} x: int :: H(x)); + +procedure C0() +{ + assert H(5); +} diff --git a/Test/inst/axiom.bpl.expect b/Test/inst/axiom.bpl.expect new file mode 100644 index 000000000..3e6d423af --- /dev/null +++ b/Test/inst/axiom.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/inst/poolSummary.bpl b/Test/inst/poolSummary.bpl new file mode 100644 index 000000000..41453c2ba --- /dev/null +++ b/Test/inst/poolSummary.bpl @@ -0,0 +1,13 @@ +// RUN: %parallel-boogie "%s" /poolSummary > "%t" 2>&1 +// RUN: %diff "%s.expect" "%t" + +function F(int): bool; +function Unused(int): bool; + +axiom (forall {:pool "L"} x: int :: F(x - 1)); +axiom Unused(0); + +procedure A() +{ + assert {:add_to_pool "L", 1} {:add_to_pool "Orphan", 99} F(0); +} diff --git a/Test/inst/poolSummary.bpl.expect b/Test/inst/poolSummary.bpl.expect new file mode 100644 index 000000000..701fd0429 --- /dev/null +++ b/Test/inst/poolSummary.bpl.expect @@ -0,0 +1,10 @@ +[poolSummary] axioms: 2 total (1 pool-bearing, 0 lambda-definition, 1 plain) +[poolSummary] pool axioms at: poolSummary.bpl:7 +[poolSummary] plain axioms at: poolSummary.bpl:8 +[poolSummary] quantifiers: 1 total (1 pool-bearing, 0 polymorphic, 0 plain) +[poolSummary] pool-bearing quantifiers at: poolSummary.bpl:7 +[poolSummary] pools referenced: 2 +[poolSummary] "L": producers={poolSummary.bpl:12} consumers={poolSummary.bpl:7} +[poolSummary] "Orphan": producers={poolSummary.bpl:12} consumers={} (!! no consumers) + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/inst/poolTrace.bpl b/Test/inst/poolTrace.bpl new file mode 100644 index 000000000..bd9ceede0 --- /dev/null +++ b/Test/inst/poolTrace.bpl @@ -0,0 +1,10 @@ +// RUN: %parallel-boogie "%s" /poolTrace > "%t" 2>&1 +// RUN: %diff "%s.expect" "%t" + +function F(int): bool; + +procedure A() +{ + assume (forall {:pool "L"} x: int :: F(x - 1)); + assert {:add_to_pool "L", 1} F(0); +} diff --git a/Test/inst/poolTrace.bpl.expect b/Test/inst/poolTrace.bpl.expect new file mode 100644 index 000000000..a08f3f3d7 --- /dev/null +++ b/Test/inst/poolTrace.bpl.expect @@ -0,0 +1,5 @@ +[poolTrace] impl A +[poolTrace] pool "L" (1 value(s)): 1 +[poolTrace] qid=poolTracebpl.8:32 pool={L} instances=1 + +Boogie program verifier finished with 1 verified, 0 errors From 0768daba855186e561719ce99da55ea90a0ee94f Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Fri, 24 Apr 2026 19:29:28 +0000 Subject: [PATCH 2/3] QI axiom-antecedent path must respect pruning / hide-reveal MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The prior patch walked program.Axioms, but Checker.Setup only calls ctx.AddAxiom on split.PrunedDeclarations. When a user has a hideable axiom and hides it (via `hide *;` / `hide F;`), pruning removes it from the prover context. The axiom-antecedent path, however, still translated the axiom's expression and fed pool-based ground instances into the VC, smuggling the hidden axiom back in. This is mathematically sound (the axiom is still a true statement of the user's theory) but defeats `{:hideable}` / `reveal` as a sanity- check mechanism — the user asks "is this assertion provable WITHOUT axiom F?" and the old code silently answered "yes" by using F anyway. Fix: thread the pruned axiom list (same set Checker.Setup uses) from Split.cs through Instantiate and into Execute / HasPoolAxioms. Lambda- definition axioms are still filtered via program.Functions to keep that classification independent of what any particular split prunes. Test/inst/axiomPoolHidden.bpl: hideable axiom with a pool hint; hide * procedure expects failure, revealed procedure expects success. Verified against the pre-fix baseline that both procedures previously verified (proving the bug was real) and that post-fix only the revealed one does. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../VCExpr/QuantifierInstantiationEngine.cs | 25 +++++++++++------ Source/VCGeneration/Splits/Split.cs | 2 +- Test/inst/axiomPoolHidden.bpl | 27 +++++++++++++++++++ Test/inst/axiomPoolHidden.bpl.expect | 3 +++ 4 files changed, 48 insertions(+), 9 deletions(-) create mode 100644 Test/inst/axiomPoolHidden.bpl create mode 100644 Test/inst/axiomPoolHidden.bpl.expect diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index 2d7857920..7a1cf65f7 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -60,15 +60,22 @@ public QuantifierInstantiationInfo(Dictionary> boundV // multi-line traces. Writers themselves aren't guaranteed thread-safe. private static readonly object poolTraceWriteLock = new(); - public static VCExpr Instantiate(Program program, Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr) - { + public static VCExpr Instantiate(Program program, IEnumerable availableAxioms, Implementation impl, + VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr) + { + // availableAxioms is what the current split (post-pruning, post-hide) + // actually exposes to the prover. The axiom-antecedent path must use the + // same set — otherwise a {:hide}-annotated or pruned axiom would be + // smuggled into the VC antecedent via pool instantiation while absent + // from the prover context, defeating hide/reveal and /prune. + var axioms = availableAxioms.ToList(); if (!InstantiationSourceChecker.HasInstantiationSources(impl) && - !PoolHintChecker.HasPoolAxioms(program)) + !PoolHintChecker.HasPoolAxioms(program, axioms)) { return vcExpr; } var qiEngine = new QuantifierInstantiationEngine(vcExprGen, exprTranslator); - return qiEngine.Execute(program, impl, vcExpr); + return qiEngine.Execute(program, axioms, impl, vcExpr); } private QuantifierInstantiationEngine(VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator) @@ -254,7 +261,7 @@ private static void AddDictionary(Dictionary>> @from, D }); } - private VCExpr Execute(Program program, Implementation impl, VCExpr vcExpr) + private VCExpr Execute(Program program, IReadOnlyCollection availableAxioms, Implementation impl, VCExpr vcExpr) { impl.Blocks.ForEach(block => block.Cmds.OfType().ForEach(predicateCmd => { @@ -275,7 +282,7 @@ private VCExpr Execute(Program program, Implementation impl, VCExpr vcExpr) .SelectMany(f => f.DefinitionAxioms) .ToHashSet(); var axiomAntecedents = new List(); - foreach (var axiom in program.Axioms) + foreach (var axiom in availableAxioms) { if (lambdaDefinitionAxioms.Contains(axiom)) { @@ -980,13 +987,15 @@ public static bool AxiomCarriesPoolHints(Axiom axiom) // Gate for running QI solely on axiom pool hints. Lifted-lambda definition // axioms are excluded here: they are handled specially by BindLambdaFunction // and should not force QI to run when the implementation has no pool sources. - public static bool HasPoolAxioms(Program program) + // availableAxioms must be the post-pruning list exposed to the current split + // so this gate matches the axiom set the engine will actually process. + public static bool HasPoolAxioms(Program program, IEnumerable availableAxioms) { var lambdaDefinitionAxioms = program.Functions .Where(f => f.OriginalLambdaExprAsString != null) .SelectMany(f => f.DefinitionAxioms) .ToHashSet(); - foreach (var axiom in program.Axioms) + foreach (var axiom in availableAxioms) { if (lambdaDefinitionAxioms.Contains(axiom)) { diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs index 3035d704b..07015abb8 100644 --- a/Source/VCGeneration/Splits/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -961,7 +961,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa vc = parent.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, checker.TheoremProver.Context); Contract.Assert(vc != null); - vc = QuantifierInstantiationEngine.Instantiate(parent.program, Implementation, exprGen, bet, vc); + vc = QuantifierInstantiationEngine.Instantiate(parent.program, PrunedDeclarations.OfType(), Implementation, exprGen, bet, vc); VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); diff --git a/Test/inst/axiomPoolHidden.bpl b/Test/inst/axiomPoolHidden.bpl new file mode 100644 index 000000000..17b2a6031 --- /dev/null +++ b/Test/inst/axiomPoolHidden.bpl @@ -0,0 +1,27 @@ +// RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// +// Regression: with /prune, a hideable axiom that is hidden must NOT be +// smuggled into the VC via pool-based quantifier instantiation. Previously +// the axiom-antecedent path walked all of program.Axioms, ignoring +// PrunedDeclarations, so hidden axioms' ground instances ended up in the +// antecedent even though the axiom itself was absent from the prover +// context. The fix routes the axiom-antecedent path through the same +// pruned list Checker.Setup uses. + +function F(int): bool uses { + hideable axiom (forall {:pool "L"} x: int :: F(x - 1)); +} + +procedure HiddenAxiom() +{ + hide *; + // With the axiom hidden, pool-based instantiation must not smuggle it in. + assert {:add_to_pool "L", 1} F(0); // should fail +} + +procedure RevealedAxiom() +{ + // Default (not hidden). Pool value 1 + axiom :pool "L" consumer ⇒ F(0). + assert {:add_to_pool "L", 1} F(0); +} diff --git a/Test/inst/axiomPoolHidden.bpl.expect b/Test/inst/axiomPoolHidden.bpl.expect new file mode 100644 index 000000000..272959384 --- /dev/null +++ b/Test/inst/axiomPoolHidden.bpl.expect @@ -0,0 +1,3 @@ +axiomPoolHidden.bpl(20,3): Error: this assertion could not be proved + +Boogie program verifier finished with 1 verified, 1 error From b95cde67bff5287df56ed7f86d71fa749739b9d6 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Fri, 24 Apr 2026 19:55:06 +0000 Subject: [PATCH 3/3] Make /keepQuantifier symmetric for pool-bearing axioms Before: pool-based instantiation of an assume-antecedent forall replaced the quantifier with its ground instances when /keepQuantifier=false, but the same flag applied to a pool-bearing axiom only affected what went into the VC antecedent -- the axiom was *also* unconditionally installed into the prover context via ctx.AddAxiom, so the full forall survived and could still fire via E-matching. /keepQuantifier therefore meant different things for assumes vs. axioms. Fix: in Checker.Setup, a pool-bearing non-lambda-definition axiom is skipped from ctx.AddAxiom when /keepQuantifier=false. The axiom then lives only as its pool-instantiated ground forms in the VC antecedent, matching the assume path. With /keepQuantifier=true the axiom goes into the prover context as before. Users who want both pool hints *and* E-matching on the same axiom should use /keepQuantifier (or split the axiom -- one annotated version for the pool, one plain for E-matching). This is a (behavior-changing) trade-off made explicit: marking an axiom {:pool ...} is now a positive decision to drive instantiation through pools, not a freebie on top of E-matching. Test/inst/axiomPoolKeepQuantifier.bpl: impl that needs the axiom via E-matching (no pool source). Expected to fail by default and succeed under /keepQuantifier, demonstrating the symmetric semantics. Help text for /keepQuantifier updated to document the axiom side. Co-Authored-By: Claude Opus 4.7 (1M context) --- Source/ExecutionEngine/CommandLineOptions.cs | 4 +++ Source/VCGeneration/Checker.cs | 20 +++++++++++++- Test/inst/axiomPoolKeepQuantifier.bpl | 27 +++++++++++++++++++ .../axiomPoolKeepQuantifier.bpl.expect.off | 5 ++++ .../axiomPoolKeepQuantifier.bpl.expect.on | 2 ++ 5 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 Test/inst/axiomPoolKeepQuantifier.bpl create mode 100644 Test/inst/axiomPoolKeepQuantifier.bpl.expect.off create mode 100644 Test/inst/axiomPoolKeepQuantifier.bpl.expect.on diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 16f9017f4..9f4b58007 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -2048,6 +2048,10 @@ not covered by a proof. If pool-based quantifier instantiation creates instances of a quantifier then keep the quantifier along with the instances. By default, the quantifier is dropped if any instances are created. + For pool-bearing axioms (non-lambda-definition), the same rule applies + symmetrically: by default the axiom is dropped from the prover context and + survives only as its pool-instantiated ground forms in the VC antecedent; + with /keepQuantifier the axiom is kept in the prover context as usual. /poolTrace Emit diagnostics about pool-based quantifier instantiation as each implementation is verified: which pool received which values, how diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 363f22183..0bbd55d79 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -169,6 +169,22 @@ private void Setup(Program program, ProverContext ctx, Split split) { var declarations = split.PrunedDeclarations; var reorderedDeclarations = GetReorderedDeclarations(declarations, SolverOptions.RandomSeed); + // Pool-bearing axioms (non-lambda-definition) are handled entirely by + // QuantifierInstantiationEngine when /keepQuantifier=false: the engine + // adds pool-instantiated ground forms to the VC antecedent and, per the + // /keepQuantifier contract, the original quantifier is dropped. If we + // also added the axiom here, the forall would still reach the solver + // via ctx.AddAxiom regardless of the flag, defeating /keepQuantifier + // asymmetrically between axioms and assumes. With /keepQuantifier=true + // we keep the axiom in the context as usual, matching the assume path. + var lambdaDefinitionAxioms = program.Functions + .Where(f => f.OriginalLambdaExprAsString != null) + .SelectMany(f => f.DefinitionAxioms) + .ToHashSet(); + bool SkipAxiomForPoolQI(Axiom axiom) => + !Options.KeepQuantifier + && !lambdaDefinitionAxioms.Contains(axiom) + && PoolHintChecker.AxiomCarriesPoolHints(axiom); foreach (var declaration in reorderedDeclarations) { Contract.Assert(declaration != null); if (declaration is TypeCtorDecl typeDecl) @@ -185,7 +201,9 @@ private void Setup(Program program, ProverContext ctx, Split split) } else if (declaration is Axiom axiomDecl) { - ctx.AddAxiom(axiomDecl, null); + if (!SkipAxiomForPoolQI(axiomDecl)) { + ctx.AddAxiom(axiomDecl, null); + } } else if (declaration is GlobalVariable glVarDecl) { diff --git a/Test/inst/axiomPoolKeepQuantifier.bpl b/Test/inst/axiomPoolKeepQuantifier.bpl new file mode 100644 index 000000000..d70719606 --- /dev/null +++ b/Test/inst/axiomPoolKeepQuantifier.bpl @@ -0,0 +1,27 @@ +// /keepQuantifier is symmetric between assume-antecedent and axiom quantifiers: +// with /keepQuantifier=false (default), the pool-bearing axiom is dropped from +// the prover context and survives only as its pool-instantiated ground forms in +// the VC antecedent; E-matching on the axiom no longer fires. With +// /keepQuantifier=true, the axiom stays in the prover context as usual. +// +// Test construction: an impl that needs the axiom via E-matching (no pool +// source) must fail by default and succeed with /keepQuantifier. +// +// RUN: %parallel-boogie "%s" > "%t.off" 2>&1 +// RUN: %parallel-boogie "%s" /keepQuantifier > "%t.on" 2>&1 +// RUN: %diff "%s.expect.off" "%t.off" +// RUN: %diff "%s.expect.on" "%t.on" + +function P(int): bool; +function Q(int): bool; + +axiom (forall {:pool "L"} x: int :: {P(x)} P(x) ==> Q(x)); + +procedure NeedsEMatching() +{ + assume P(41); + // With /keepQuantifier=false the axiom is out of the prover context and + // pool "L" has no source feeding value 41, so Q(41) cannot be derived. + // With /keepQuantifier=true the axiom stays, E-matches P(41), yields Q(41). + assert Q(41); +} diff --git a/Test/inst/axiomPoolKeepQuantifier.bpl.expect.off b/Test/inst/axiomPoolKeepQuantifier.bpl.expect.off new file mode 100644 index 000000000..c835a782e --- /dev/null +++ b/Test/inst/axiomPoolKeepQuantifier.bpl.expect.off @@ -0,0 +1,5 @@ +axiomPoolKeepQuantifier.bpl(26,3): Error: this assertion could not be proved +Execution trace: + axiomPoolKeepQuantifier.bpl(22,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/inst/axiomPoolKeepQuantifier.bpl.expect.on b/Test/inst/axiomPoolKeepQuantifier.bpl.expect.on new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/inst/axiomPoolKeepQuantifier.bpl.expect.on @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors