From 49d5d23ddc63f9763d3d8cc0da6774ee8711efa3 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 9 May 2023 16:15:53 -0700 Subject: [PATCH 01/27] Recognize {:id ...} attributes on assignments This allows assignments to be treated as "necessary assumptions" --- Source/Core/AST/Absy.cs | 8 ++++++++ Source/VCGeneration/ConditionGeneration.cs | 6 +++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 8305d8fb6..48d164d15 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -280,6 +280,14 @@ public List FindLayers() } return layers.Distinct().OrderBy(l => l).ToList(); } + + public static void CopyAttribute(ICarriesAttributes src, string attr, ICarriesAttributes dest) + { + var attrArgs = QKeyValue.FindAttribute(src.Attributes, kv => kv.Key == attr); + if (attrArgs is not null) { + dest.Attributes = new QKeyValue(attrArgs.tok, attrArgs.Key, attrArgs.Params, dest.Attributes); + } + } } [ContractClassFor(typeof(Absy))] diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index bb4b554aa..6036e6f21 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1381,7 +1381,11 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing assumption = Expr.And(assumption, assumptions[i]); } - passiveCmds.Add(new AssumeCmd(c.tok, assumption)); + var assumeCmd = new AssumeCmd(c.tok, assumption); + // Copy any {:id ...} from the assignment to the assumption, so + // we can track it as a "necessary assumption". + ICarriesAttributes.CopyAttribute(assign, "id", assumeCmd); + passiveCmds.Add(assumeCmd); } if (currentImplementation != null From 0ac082462cbc1cb79235298313617b9c30355d80 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 10 May 2023 13:34:35 -0700 Subject: [PATCH 02/27] Recognize {:id ...} on requires clauses Allows them to be tracked in unseat cores. --- Source/VCGeneration/ConditionGeneration.cs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6036e6f21..e6d73f10f 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -253,7 +253,10 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu { Contract.Assert(req != null); Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); - Cmd c = new AssumeCmd(req.tok, e); + AssumeCmd c = new AssumeCmd(req.tok, e); + // Copy any {:id ...} from the precondition to the assumption, so + // we can track it as a "necessary assumption". + ICarriesAttributes.CopyAttribute(req, "id", c); c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) From 32398ee165e88f21429f51619409d25ea7a7a38e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 10 May 2023 13:51:31 -0700 Subject: [PATCH 03/27] Recognize {:id ...} on loop invariants MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Allows them to be tracked in unseat cores. Add a suffix to distinguish between the assumption and the assertion implied by an invariant, since we’ll be tracking assertions, too, in a later step. --- Source/Core/AST/Absy.cs | 8 ++++++++ Source/VCGeneration/VCGen.cs | 6 +++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 48d164d15..e7db849e1 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -288,6 +288,14 @@ public static void CopyAttribute(ICarriesAttributes src, string attr, ICarriesAt dest.Attributes = new QKeyValue(attrArgs.tok, attrArgs.Key, attrArgs.Params, dest.Attributes); } } + + public static void CopyStringAttributeWithSuffix(IToken tok, ICarriesAttributes src, string attr, string suffix, ICarriesAttributes dest) + { + var arg = QKeyValue.FindStringAttribute(src.Attributes, attr); + if (arg is not null) { + dest.Attributes = new QKeyValue(tok, attr, new List( ){arg + suffix}, dest.Attributes); + } + } } [ContractClassFor(typeof(Absy))] diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index e1833ea8d..a31c3322b 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -751,7 +751,11 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary Date: Wed, 10 May 2023 13:52:29 -0700 Subject: [PATCH 04/27] Add a field to VCResult to track unsat cores --- Source/VCGeneration/Split.cs | 19 ++++++++++--------- Source/VCGeneration/VCResult.cs | 1 + 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 6ede06f00..54b4ac55f 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1274,15 +1274,16 @@ public int GetHashCode(List obj) var resourceCount = await checker.GetProverResourceCount(); var result = new VCResult( - SplitIndex + 1, - iteration, - checker.ProverStart, - outcome, - checker.ProverRunTime, - checker.Options.ErrorLimit, - Counterexamples, - Asserts, - resourceCount); + vcNum: SplitIndex + 1, + iteration: iteration, + startTime: checker.ProverStart, + outcome: outcome, + runTime: checker.ProverRunTime, + maxCounterExamples: checker.Options.ErrorLimit, + counterExamples: Counterexamples, + asserts: Asserts, + core: new HashSet(), + resourceCount: resourceCount); callback.OnVCResult(result); if (options.VcsDumpSplits) diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VCResult.cs index 9e75668bb..0d7e5101e 100644 --- a/Source/VCGeneration/VCResult.cs +++ b/Source/VCGeneration/VCResult.cs @@ -24,6 +24,7 @@ public record VCResult int maxCounterExamples, List counterExamples, List asserts, + ISet core, int resourceCount ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, From e94523044e116ea2c1a754dc22b14c0f413a90cb Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 15 May 2023 08:35:59 -0700 Subject: [PATCH 05/27] Basic support for labeled assertions --- Source/Core/AST/AbsyCmd.cs | 2 ++ Source/ExecutionEngine/ExecutionEngine.csproj | 1 + Source/Provers/SMTLib/SMTLibLineariser.cs | 2 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 6 ++++-- Source/VCExpr/VCExpressionGenerator.cs | 1 + Source/VCGeneration/VCGen.cs | 2 ++ Source/VCGeneration/Wlp.cs | 7 +++++++ 7 files changed, 18 insertions(+), 3 deletions(-) diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 0c88c4cc4..23713303f 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -4003,6 +4003,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(e != null); Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition); AssumeCmd assume = new AssumeCmd(this.tok, copy); + // TODO: fix the case where a given postcondition appears at multiple call sites + //ICarriesAttributes.CopyAttribute(e, "id", assume); #region stratified inlining support diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index 968bdab33..897f68d9b 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -21,6 +21,7 @@ + diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 6f2aedf36..567b536cd 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -398,7 +398,7 @@ public bool Visit(VCExprNAry node, LineariserOptions options) return true; } - if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) + if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp)) { var exprVar = node[0] as VCExprVar; NamedAssumes.Add(exprVar); diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index dd22da918..57b4cc509 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -212,7 +212,7 @@ public override bool Visit(VCExprNAry node, bool arg) AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp) node.Op).Weight)); } - else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) + else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp)) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); @@ -270,7 +270,9 @@ public override bool Visit(VCExprVar node, bool arg) RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || + if (!(printedName.StartsWith("assume$$") || + printedName.StartsWith("assert$$") || + printedName.StartsWith("soft$$") || printedName.StartsWith("try$$"))) { AddDeclaration(decl); diff --git a/Source/VCExpr/VCExpressionGenerator.cs b/Source/VCExpr/VCExpressionGenerator.cs index cf898fa38..9ebe816ef 100644 --- a/Source/VCExpr/VCExpressionGenerator.cs +++ b/Source/VCExpr/VCExpressionGenerator.cs @@ -445,6 +445,7 @@ int AndSize(VCExpr e) public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool); public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool); public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool); + public static readonly VCExprOp NamedAssertOp = new VCExprCustomOp("named_assert##dummy", 2, Type.Bool); public VCExprOp BoogieFunctionOp(Function func) { diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index a31c3322b..7cd96021d 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -57,6 +57,7 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a throw new cce.UnreachableException(); // unexpected case } + // TODO: track id here, too? return new AssumeCmd(assrt.tok, expr); } @@ -730,6 +731,7 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary Date: Wed, 31 May 2023 14:48:50 -0700 Subject: [PATCH 06/27] Fix concurrency bug accidentally discovered --- Source/VCExpr/QuantifierInstantiationEngine.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index 3d83909a6..f0afc70fd 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; @@ -50,7 +51,7 @@ public QuantifierInstantiationInfo(Dictionary> boundV private string skolemConstantNamePrefix; internal VCExpressionGenerator vcExprGen; private Boogie2VCExprTranslator exprTranslator; - internal static Dictionary labelToType = new(); + internal static ConcurrentDictionary labelToType = new(); public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr) { From a97032b48dea50d4cabc36ad70a132d5eaf3d803 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 31 May 2023 14:54:37 -0700 Subject: [PATCH 07/27] Mostly complete verification coverage tracking --- Source/Core/AST/AbsyCmd.cs | 20 ++++++++- Source/Core/AST/Program.cs | 2 +- Source/ExecutionEngine/CommandLineOptions.cs | 11 ++++- Source/ExecutionEngine/ExecutionEngine.cs | 7 ++- Source/Provers/SMTLib/ProverInterface.cs | 2 +- .../SMTLib/SMTLibInteractiveTheoremProver.cs | 8 ++-- Source/Provers/SMTLib/SMTLibOptions.cs | 1 + Source/Provers/SMTLib/TypeDeclCollector.cs | 2 +- Source/VCGeneration/ConditionGeneration.cs | 21 ++++++--- Source/VCGeneration/Split.cs | 6 ++- Source/VCGeneration/VCGen.cs | 44 +++++++++++++------ Source/VCGeneration/VCResult.cs | 2 +- Source/VCGeneration/Wlp.cs | 7 ++- 13 files changed, 95 insertions(+), 38 deletions(-) diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 23713303f..b988b1f18 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -3720,6 +3720,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Dictionary substMapBound = new Dictionary(); List /*!*/ tempVars = new List(); + string idAttr = QKeyValue.FindStringAttribute(Attributes, "id"); // proc P(ins) returns (outs) // requires Pre @@ -3838,6 +3839,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) AssertCmd /*!*/ a = new AssertRequiresCmd(this, reqCopy); Contract.Assert(a != null); + if (Attributes != null) { // Inherit attributes of call. @@ -3846,6 +3848,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options) a.Attributes = attrCopy; } + // Do this after copying the attributes so it doesn't get overwritten + if (idAttr is not null) { + ICarriesAttributes.CopyStringAttributeWithSuffix(tok, req, "id", $"${idAttr}$requires", a); + } + a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; newBlockBody.Add(a); } @@ -3857,6 +3864,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options) AssumeCmd /*!*/ a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition)); Contract.Assert(a != null); + // These probably won't have IDs, but copy if they do. + if (idAttr is not null) { + ICarriesAttributes.CopyStringAttributeWithSuffix(tok, req, "id", $"${idAttr}$requires_assumed", a); + } + newBlockBody.Add(a); } } @@ -4003,8 +4015,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(e != null); Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition); AssumeCmd assume = new AssumeCmd(this.tok, copy); - // TODO: fix the case where a given postcondition appears at multiple call sites - //ICarriesAttributes.CopyAttribute(e, "id", assume); + if (idAttr is not null) { + ICarriesAttributes.CopyStringAttributeWithSuffix(tok, e, "id", $"${idAttr}$ensures", assume); + } #region stratified inlining support @@ -4038,6 +4051,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options) cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i])); Contract.Assert(cout_exp != null); AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp); + if (idAttr is not null) { + Attributes = new QKeyValue(param_i.tok, "id", new List(){ $"{idAttr}$out{i}" }, Attributes); + } newBlockBody.Add(assign); } } diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 10ba93b29..7ac5728ee 100644 --- a/Source/Core/AST/Program.cs +++ b/Source/Core/AST/Program.cs @@ -395,7 +395,7 @@ public List /*!*/ GlobalVariables } } - public readonly ISet NecessaryAssumes = new HashSet(); + public readonly ISet AllCoveredElements = new HashSet(); public IEnumerable Blocks() { diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 9faefcd79..115894494 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -201,7 +201,9 @@ public bool NormalizeDeclarationOrder public bool ImmediatelyAcceptCommands => StratifiedInlining > 0 || ContractInfer; - public bool ProduceUnsatCores => PrintNecessaryAssumes || EnableUnSatCoreExtract == 1 || + public bool ProduceUnsatCores => PrintNecessaryAssumes || + PrintVerificationCoverage || + EnableUnSatCoreExtract == 1 || ContractInfer && (UseUnsatCoreForContractInfer || ExplainHoudini); public bool BatchModeSolver { get; set; } @@ -285,6 +287,11 @@ public bool PrintNecessaryAssumes { set => printNecessaryAssumes = value; } + public bool PrintVerificationCoverage { + get => printVerificationCoverage; + set => printVerificationCoverage = value; + } + public int InlineDepth { get; set; } = -1; public bool UseProverEvaluate { @@ -545,6 +552,7 @@ void ObjectInvariant5() private bool houdiniUseCrossDependencies = false; private bool useUnsatCoreForContractInfer = false; private bool printNecessaryAssumes = false; + private bool printVerificationCoverage = false; private bool useProverEvaluate; private bool trustMoverTypes = false; private bool trustNoninterference = false; @@ -1298,6 +1306,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("useUnsatCoreForContractInfer", x => useUnsatCoreForContractInfer = x) || ps.CheckBooleanFlag("printAssignment", x => PrintAssignment = x) || ps.CheckBooleanFlag("printNecessaryAssumes", x => printNecessaryAssumes = x) || + ps.CheckBooleanFlag("printVerificationCoverage", x => printVerificationCoverage = x) || ps.CheckBooleanFlag("useProverEvaluate", x => useProverEvaluate = x) || ps.CheckBooleanFlag("deterministicExtractLoops", x => DeterministicExtractLoops = x) || ps.CheckBooleanFlag("verifySeparately", x => VerifySeparately = x) || diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index b11cc968e..50fd595ee 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -673,8 +673,11 @@ private async Task VerifyEachImplementation(TextWriter output, CleanupRequest(requestId); } - if (Options.PrintNecessaryAssumes && processedProgram.Program.NecessaryAssumes.Any()) { - Options.OutputWriter.WriteLine("Necessary assume command(s): {0}", string.Join(", ", processedProgram.Program.NecessaryAssumes.OrderBy(s => s))); + if (Options.PrintNecessaryAssumes && processedProgram.Program.AllCoveredElements.Any()) { + Options.OutputWriter.WriteLine("Necessary assume command(s): {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); + } + if (Options.PrintVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { + Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); } cce.NonNull(Options.TheProverFactory).Close(); diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index fb028650f..fa6ba0c2b 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -112,7 +112,7 @@ protected ErrorHandler(SMTLibOptions options) this.options = options; } - public virtual void AddNecessaryAssume(string id) + public virtual void AddCoveredElement(string id) { throw new System.NotImplementedException(); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index d4fe00fad..fd1c007eb 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -223,18 +223,18 @@ public async Task CheckSat(CancellationToken cancellationToken, if (resp.Name != "") { usedNamedAssumes.Add(resp.Name); - if (libOptions.PrintNecessaryAssumes) + if (libOptions.PrintNecessaryAssumes || libOptions.PrintVerificationCoverage) { - reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + reporter.AddCoveredElement(resp.Name.Substring("aux$$assume$$".Length)); } } foreach (var arg in resp.Arguments) { usedNamedAssumes.Add(arg.Name); - if (libOptions.PrintNecessaryAssumes) + if (libOptions.PrintNecessaryAssumes || libOptions.PrintVerificationCoverage) { - reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + reporter.AddCoveredElement(arg.Name.Substring("aux$$assume$$".Length)); } } } diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs index c479e4532..81c487216 100644 --- a/Source/Provers/SMTLib/SMTLibOptions.cs +++ b/Source/Provers/SMTLib/SMTLibOptions.cs @@ -15,6 +15,7 @@ public interface SMTLibOptions : CoreOptions bool ImmediatelyAcceptCommands { get; } bool RunningBoogieFromCommandLine { get; } bool PrintNecessaryAssumes { get; } + bool PrintVerificationCoverage { get; } string ProverPreamble { get; } bool TraceDiagnosticsOnTimeout { get; } uint TimeLimitPerAssertionInPercent { get; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 57b4cc509..a6c41ee7f 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -216,7 +216,7 @@ public override bool Visit(VCExprNAry node, bool arg) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); - if (options.PrintNecessaryAssumes) + if (options.PrintNecessaryAssumes || options.PrintVerificationCoverage) { AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index e6d73f10f..094b6abdf 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -254,9 +254,11 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu Contract.Assert(req != null); Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); AssumeCmd c = new AssumeCmd(req.tok, e); - // Copy any {:id ...} from the precondition to the assumption, so - // we can track it as a "necessary assumption". - ICarriesAttributes.CopyAttribute(req, "id", c); + if (options.PrintVerificationCoverage) { + // Copy any {:id ...} from the precondition to the assumption, so + // we can track it as a "necessary assumption". + ICarriesAttributes.CopyAttribute(req, "id", c); + } c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) @@ -319,6 +321,11 @@ protected static void InjectPostConditions(VCGenOptions options, ImplementationR ensCopy.Condition = e; AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; + if (options.PrintVerificationCoverage) { + // Copy any {:id ...} from the precondition to the assumption, so + // we can track it as a "necessary assumption". + ICarriesAttributes.CopyAttribute(ens, "id", c); + } unifiedExitBlock.Cmds.Add(c); if (debugWriter != null) { @@ -1385,9 +1392,11 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing } var assumeCmd = new AssumeCmd(c.tok, assumption); - // Copy any {:id ...} from the assignment to the assumption, so - // we can track it as a "necessary assumption". - ICarriesAttributes.CopyAttribute(assign, "id", assumeCmd); + if (Options.PrintVerificationCoverage) { + // Copy any {:id ...} from the assignment to the assumption, so + // we can track it as a "necessary assumption". + ICarriesAttributes.CopyAttribute(assign, "id", assumeCmd); + } passiveCmds.Add(assumeCmd); } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 54b4ac55f..ccac566e4 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1271,6 +1271,10 @@ public int GetHashCode(List obj) run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, checker.ProverRunTime.TotalSeconds, outcome); } + if (options.Trace && options.PrintVerificationCoverage) { + run.OutputWriter.WriteLine("Covered elements: {0}", + string.Join(", ", reporter.CurrentCoveredElements.OrderBy(s => s))); + } var resourceCount = await checker.GetProverResourceCount(); var result = new VCResult( @@ -1282,7 +1286,7 @@ public int GetHashCode(List obj) maxCounterExamples: checker.Options.ErrorLimit, counterExamples: Counterexamples, asserts: Asserts, - core: new HashSet(), + coveredElements: reporter.CurrentCoveredElements, resourceCount: resourceCount); callback.OnVCResult(result); diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 7cd96021d..1f5148524 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -57,8 +57,11 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a throw new cce.UnreachableException(); // unexpected case } - // TODO: track id here, too? - return new AssumeCmd(assrt.tok, expr); + var assume = new AssumeCmd(assrt.tok, expr); + if (options.PrintVerificationCoverage) { + ICarriesAttributes.CopyAttribute(assrt, "id", assume); + } + return assume; } #region Soundness smoke tester @@ -459,14 +462,12 @@ void ObjectInvariant() Program program; - public IEnumerable NecessaryAssumes - { - get { return program.NecessaryAssumes; } - } + public HashSet CurrentCoveredElements { get; } - public override void AddNecessaryAssume(string id) + public override void AddCoveredElement(string id) { - program.NecessaryAssumes.Add(id); + program.AllCoveredElements.Add(id); + CurrentCoveredElements.Add(id); } public ErrorReporter(VCGenOptions options, @@ -496,6 +497,7 @@ public ErrorReporter(VCGenOptions options, this.program = program; this.split = split; this.options = options; + this.CurrentCoveredElements = new(); } public override void OnModel(IList labels /*!*/ /*!*/, Model model, @@ -730,8 +732,13 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary counterExamples, List asserts, - ISet core, + IEnumerable coveredElements, int resourceCount ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 7efc78af9..f2a6fcea2 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -110,10 +110,9 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (aid != null) + if (aid != null && ctxt.Options.PrintVerificationCoverage) { - var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); - var v = gen.Variable((isTry ? "try$$" : "assert$$") + aid, Microsoft.Boogie.Type.Bool); + var v = gen.Variable($"assert$${aid}", Microsoft.Boogie.Type.Bool); C = gen.Function(VCExpressionGenerator.NamedAssertOp, v, gen.AndSimp(v, C)); } @@ -205,7 +204,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (aid != null) + if (aid != null && (ctxt.Options.PrintVerificationCoverage || ctxt.Options.PrintNecessaryAssumes)) { var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool); From 5919289a2d4691ae4ef12f80942724d66a15ce26 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 31 May 2023 17:05:39 -0700 Subject: [PATCH 08/27] Add initial test for verification coverage --- Test/coverage/verificationCoverage.bpl | 106 ++++++++++++++++++ .../verificationCoverage.bpl.expect.coverage | 3 + .../verificationCoverage.bpl.expect.plain | 2 + 3 files changed, 111 insertions(+) create mode 100644 Test/coverage/verificationCoverage.bpl create mode 100644 Test/coverage/verificationCoverage.bpl.expect.coverage create mode 100644 Test/coverage/verificationCoverage.bpl.expect.plain diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl new file mode 100644 index 000000000..86378cf27 --- /dev/null +++ b/Test/coverage/verificationCoverage.bpl @@ -0,0 +1,106 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect.plain" "%t" +// RUN: %boogie -printVerificationCoverage "%s" > "%t" +// RUN: %diff "%s.expect.coverage" "%t" + +procedure testRequiresAssign(n: int) + requires {:id "r0"} n > 0; // covered + requires {:id "r_not_1"} n < 10; // not covered +{ + var x: int; + x := {:id "a0"} n + 1; // covered + assert {:id "assert_a0"} x == n + 1; // covered + x := {:id "a_not_1"} 0; // not covered + assert {:id "assert_r0"} n > 0; // covered +} + +procedure sum(n: int) returns (s: int) + requires {:id "spre1"} n >= 0; // covered + ensures {:id "spost"} s == (n * (n + 1)) div 2; // covered +{ + var i: int; + var foo: int; + + i := 0; + s := 0; + foo := 27; + while (i < n) + invariant {:id "sinv1"} 0 <= i && i <= n; // covered: established, maintained, assumed + invariant {:id "sinv2"} s == (i * (i + 1)) div 2; // covered: established, maintained, assumed + invariant {:id "sinv_not_1"} n >= 0; // covered: established, maintained, NOT assumed + { + i := i + 1; + s := s + i; + foo := {:id "update_foo"} foo * 2; // not covered + } +} + +procedure contradictoryAssume(n: int) +{ + assume {:id "cont_assume_1"} n > 0; // covered + assume {:id "cont_assume_2"} n < 0; // covered + assume {:id "unreach_assume_1"} n == 5; // not covered + assert {:id "unreach_assert_1"} n < 10; // not covered +} + +// NB: an explicit `requires false` leads to _nothing_ being covered +procedure falseRequires(n: int) + requires {:id "false_req"} n != n; // covered +{ + assert {:id "false_assert"} false; // not covered +} + +procedure contradictoryRequires(n: int) + requires {:id "cont_req_1"} n > 0; // covered + requires {:id "cont_req_2"} n < 0; // covered +{ + assume {:id "n_eq_5"} n == 5; // not covered + assert {:id "n_lt_10"} n > 10; // not covered +} + +procedure assumeFalse() { + assume {:id "assumeFalse"} false; // covered + assert {:id "assertSimple"} 1 + 1 == 2; // not covered +} + +procedure testEnsuresCallee(n: int) returns (r: int) + requires {:id "ter0"} n > 0; // covered + ensures {:id "tee0"} r > n; // covered by this procedure and caller + ensures {:id "tee1"} r > 0; // covered when proving this procedure, not from caller +{ + r := n + 1; +} + +procedure testEnsuresCaller(n: int) returns (r: int) + requires {:id "ter1"} n > 0; // covered + ensures {:id "tee_not_1"} r > n; // covered +{ + var x: int; + var y: int; + call {:id "call1"} x := testEnsuresCallee(n+1); // covered + call {:id "call2"} y := testEnsuresCallee(n+1); // covered + r := x + y; // covered +} + +procedure obviouslyUnconstrainedCode(x: int) returns (a: int, b: int) + requires {:id "x_gt_10"} x > 10; // covered + requires {:id "x_lt_100"} x < 100; // not covered + ensures {:id "a_gt_10"} a > 10; // covered +{ + a := {:id "constrained"} x + 1; // covered: constrained by ensures clause + b := {:id "not_constrained"} x - 1; // not covered: not constrained by ensures clause +} + + +procedure contradictoryEnsuresClause(x: int) returns (r: int); + requires {:id "xpos_abs"} x > 1; // covered (established by caller) + ensures {:id "cont_ens_abs"} r > x && r < 0; // covered (used by caller proof) + +// Call function that has contradictory ensures clauses. +procedure callContradictoryFunction(x: int) returns (r: int) + requires {:id "xpos_caller"} x > 1; // covered + ensures {:id "caller_ensures"} r < 0; // not covered +{ + call {:id "call_cont"} r := contradictoryEnsuresClause(x); + r := {:id "unreachable_assignment"} r - 1; // not covered +} diff --git a/Test/coverage/verificationCoverage.bpl.expect.coverage b/Test/coverage/verificationCoverage.bpl.expect.coverage new file mode 100644 index 000000000..8ad14013c --- /dev/null +++ b/Test/coverage/verificationCoverage.bpl.expect.coverage @@ -0,0 +1,3 @@ +Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller + +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/coverage/verificationCoverage.bpl.expect.plain b/Test/coverage/verificationCoverage.bpl.expect.plain new file mode 100644 index 000000000..12041afe1 --- /dev/null +++ b/Test/coverage/verificationCoverage.bpl.expect.plain @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 10 verified, 0 errors From 8ad7c1674a1cfb8b20266ca68b0594c117a941c4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 1 Jun 2023 09:14:37 -0700 Subject: [PATCH 09/27] Tweak RUN commands for verification coverage test --- Test/coverage/verificationCoverage.bpl | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index 86378cf27..d3cf4fa53 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect.plain" "%t" -// RUN: %boogie -printVerificationCoverage "%s" > "%t" -// RUN: %diff "%s.expect.coverage" "%t" +// RUN: %boogie "%s" > "%t.plain" +// RUN: %diff "%s.expect.plain" "%t.plain" +// RUN: %boogie -printVerificationCoverage "%s" > "%t.coverage" +// RUN: %diff "%s.expect.coverage" "%t.coverage" procedure testRequiresAssign(n: int) requires {:id "r0"} n > 0; // covered From e95aab580f831ea9f605250fa4bb7ca4138f73ff Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 1 Jun 2023 10:01:22 -0700 Subject: [PATCH 10/27] Verification coverage unsupported in batch mode --- Test/coverage/verificationCoverage.bpl | 1 + 1 file changed, 1 insertion(+) diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index d3cf4fa53..fddcf22ea 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -2,6 +2,7 @@ // RUN: %diff "%s.expect.plain" "%t.plain" // RUN: %boogie -printVerificationCoverage "%s" > "%t.coverage" // RUN: %diff "%s.expect.coverage" "%t.coverage" +// UNSUPPORTED: batch_mode procedure testRequiresAssign(n: int) requires {:id "r0"} n > 0; // covered From 3ce42444ad37494e068eebc4f5c9f93b7e501478 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 1 Jun 2023 10:44:01 -0700 Subject: [PATCH 11/27] Attempt to make timeouts test more robust --- Test/test2/Timeouts0.bpl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index 7ca86452a..fcec988b0 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -6,7 +6,7 @@ // UNSUPPORTED: batch_mode // CHECK-L: (set-option :timeout 4000) // CHECK-L: (set-option :timeout 8000) -// CHECK-L: (set-option :timeout 2000) +// CHECK-L: (set-option :timeout 1000) procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1); requires 0 < len; @@ -68,7 +68,7 @@ procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int); requires 0 < len; ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j); -implementation {:timeLimit 2} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int) +implementation {:timeLimit 1} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int) { var i : int; From 950080b2699ad6c8765339a480fe84554a89cbe2 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 1 Jun 2023 10:57:22 -0700 Subject: [PATCH 12/27] Another try for more deterministic timeout testing --- Test/test2/Timeouts0.bpl | 30 ------------------------------ Test/test2/Timeouts0.bpl.expect | 17 +++++++---------- 2 files changed, 7 insertions(+), 40 deletions(-) diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index fcec988b0..733cc119e 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -6,7 +6,6 @@ // UNSUPPORTED: batch_mode // CHECK-L: (set-option :timeout 4000) // CHECK-L: (set-option :timeout 8000) -// CHECK-L: (set-option :timeout 1000) procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1); requires 0 < len; @@ -61,32 +60,3 @@ implementation {:timeLimit 8} TestTimeouts1(in: [int]int, len: int) returns (out i := i + 1; } } - - -procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int); - requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1); - requires 0 < len; - ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j); - -implementation {:timeLimit 1} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int) -{ - var i : int; - - i := 0; - out[i] := 0; - while (i < len) - invariant 0 <= i && i <= len; - invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1); - { - out[i + 1] := out[i] + 1; - i := i + 1; - } - - i := 0; - while (i < len) - invariant 0 <= i && i <= len; - invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]); - { - i := i + 1; - } -} diff --git a/Test/test2/Timeouts0.bpl.expect b/Test/test2/Timeouts0.bpl.expect index bb09751e0..0b8a02314 100644 --- a/Test/test2/Timeouts0.bpl.expect +++ b/Test/test2/Timeouts0.bpl.expect @@ -1,11 +1,8 @@ -Timeouts0.bpl(28,5): Error: a postcondition could not be proved on this return path -Timeouts0.bpl(13,3): Related location: this is the postcondition that could not be proved -Timeouts0.bpl(30,7): Error: this invariant could not be proved to be maintained by the loop -Timeouts0.bpl(57,5): Error: a postcondition could not be proved on this return path -Timeouts0.bpl(40,3): Related location: this is the postcondition that could not be proved -Timeouts0.bpl(59,7): Error: this invariant could not be proved to be maintained by the loop -Timeouts0.bpl(86,5): Error: a postcondition could not be proved on this return path -Timeouts0.bpl(69,3): Related location: this is the postcondition that could not be proved -Timeouts0.bpl(88,7): Error: this invariant could not be proved to be maintained by the loop +Timeouts0.bpl(27,5): Error: a postcondition could not be proved on this return path +Timeouts0.bpl(12,3): Related location: this is the postcondition that could not be proved +Timeouts0.bpl(29,7): Error: this invariant could not be proved to be maintained by the loop +Timeouts0.bpl(56,5): Error: a postcondition could not be proved on this return path +Timeouts0.bpl(39,3): Related location: this is the postcondition that could not be proved +Timeouts0.bpl(58,7): Error: this invariant could not be proved to be maintained by the loop -Boogie program verifier finished with 0 verified, 6 errors +Boogie program verifier finished with 0 verified, 4 errors From 7b6679b30aaac8e0049d839a214709a469570527 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 1 Jun 2023 11:18:42 -0700 Subject: [PATCH 13/27] Tiny tweaks to coverage tests --- Test/coverage/verificationCoverage.bpl | 8 ++++---- Test/coverage/verificationCoverage.bpl.expect.coverage | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index fddcf22ea..064a946f8 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -78,9 +78,9 @@ procedure testEnsuresCaller(n: int) returns (r: int) { var x: int; var y: int; - call {:id "call1"} x := testEnsuresCallee(n+1); // covered - call {:id "call2"} y := testEnsuresCallee(n+1); // covered - r := x + y; // covered + call {:id "call1"} x := testEnsuresCallee(n+1); // requires and ensures covered + call {:id "call2"} y := testEnsuresCallee(n+1); // requires and ensures covered + r := {:id "xy_sum"} x + y; // covered } procedure obviouslyUnconstrainedCode(x: int) returns (a: int, b: int) @@ -102,6 +102,6 @@ procedure callContradictoryFunction(x: int) returns (r: int) requires {:id "xpos_caller"} x > 1; // covered ensures {:id "caller_ensures"} r < 0; // not covered { - call {:id "call_cont"} r := contradictoryEnsuresClause(x); + call {:id "call_cont"} r := contradictoryEnsuresClause(x); // requires and ensures covered r := {:id "unreachable_assignment"} r - 1; // not covered } diff --git a/Test/coverage/verificationCoverage.bpl.expect.coverage b/Test/coverage/verificationCoverage.bpl.expect.coverage index 8ad14013c..9d7da48a0 100644 --- a/Test/coverage/verificationCoverage.bpl.expect.coverage +++ b/Test/coverage/verificationCoverage.bpl.expect.coverage @@ -1,3 +1,3 @@ -Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller +Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum Boogie program verifier finished with 10 verified, 0 errors From 20e06a0f7efd3b5e09de02d5d68f8df750ab0e56 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 2 Jun 2023 09:43:57 -0700 Subject: [PATCH 14/27] Rename variables --- Source/VCGeneration/Wlp.cs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index f2a6fcea2..416cb26e6 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -109,10 +109,10 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) } VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); - var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (aid != null && ctxt.Options.PrintVerificationCoverage) + var assertId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); + if (assertId != null && ctxt.Options.PrintVerificationCoverage) { - var v = gen.Variable($"assert$${aid}", Microsoft.Boogie.Type.Bool); + var v = gen.Variable($"assert$${assertId}", Microsoft.Boogie.Type.Bool); C = gen.Function(VCExpressionGenerator.NamedAssertOp, v, gen.AndSimp(v, C)); } @@ -203,19 +203,19 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); - var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (aid != null && (ctxt.Options.PrintVerificationCoverage || ctxt.Options.PrintNecessaryAssumes)) + var assumeId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); + if (assumeId != null && (ctxt.Options.PrintVerificationCoverage || ctxt.Options.PrintNecessaryAssumes)) { var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); - var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool); + var v = gen.Variable((isTry ? "try$$" : "assume$$") + assumeId, Microsoft.Boogie.Type.Bool); expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); } var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0); - if ((soft || 0 < softWeight) && aid != null) + if ((soft || 0 < softWeight) && assumeId != null) { - var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool); + var v = gen.Variable("soft$$" + assumeId, Microsoft.Boogie.Type.Bool); expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr)); } From abcae74925a9daaa69eac6e18e847aff6cac014e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 2 Jun 2023 09:44:58 -0700 Subject: [PATCH 15/27] Adjust how IDs (and other attributes) are tracked --- Source/Core/AST/Absy.cs | 38 +++++++++++--------- Source/Core/AST/AbsyCmd.cs | 21 +++++------ Source/Core/AST/AbsyType.cs | 2 +- Source/Core/Monomorphization.cs | 2 +- Source/ExecutionEngine/VerificationResult.cs | 2 +- Source/Provers/SMTLib/SMTLibLineariser.cs | 4 +-- Source/VCGeneration/ConditionGeneration.cs | 6 ++-- Source/VCGeneration/VCGen.cs | 8 ++--- 8 files changed, 44 insertions(+), 39 deletions(-) diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index e7db849e1..f817c5c0d 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -281,19 +281,30 @@ public List FindLayers() return layers.Distinct().OrderBy(l => l).ToList(); } - public static void CopyAttribute(ICarriesAttributes src, string attr, ICarriesAttributes dest) + // Look for {:name string} in list of attributes. + public string FindStringAttribute(string name) + { + return QKeyValue.FindStringAttribute(Attributes, name); + } + + public void AddStringAttribute(IToken tok, string name, string parameter) + { + Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); + } + + public void CopyIdFrom(IToken tok, ICarriesAttributes src) { - var attrArgs = QKeyValue.FindAttribute(src.Attributes, kv => kv.Key == attr); - if (attrArgs is not null) { - dest.Attributes = new QKeyValue(attrArgs.tok, attrArgs.Key, attrArgs.Params, dest.Attributes); + var id = src.FindStringAttribute("id"); + if (id is not null) { + AddStringAttribute(tok, "id", id); } } - public static void CopyStringAttributeWithSuffix(IToken tok, ICarriesAttributes src, string attr, string suffix, ICarriesAttributes dest) + public void CopyIdWithSuffixFrom(IToken tok, ICarriesAttributes src, string suffix) { - var arg = QKeyValue.FindStringAttribute(src.Attributes, attr); - if (arg is not null) { - dest.Attributes = new QKeyValue(tok, attr, new List( ){arg + suffix}, dest.Attributes); + var id = src.FindStringAttribute("id"); + if (id is not null) { + AddStringAttribute(tok, "id", id + suffix); } } } @@ -426,13 +437,6 @@ public Expr FindExprAttribute(string name) return res; } - // Look for {:name string} in list of attributes. - public string FindStringAttribute(string name) - { - Contract.Requires(name != null); - return QKeyValue.FindStringAttribute(this.Attributes, name); - } - // Look for {:name N} in list of attributes. Return false if attribute // 'name' does not exist or if N is not an integer constant. Otherwise, // return true and update 'result' with N. @@ -1826,7 +1830,7 @@ public byte[] MD5DependencyChecksum public string Checksum { - get { return FindStringAttribute("checksum"); } + get { return (this as ICarriesAttributes).FindStringAttribute("checksum"); } } string dependencyChecksum; @@ -3632,7 +3636,7 @@ public string Id { get { - var id = FindStringAttribute("id"); + var id = (this as ICarriesAttributes).FindStringAttribute("id"); if (id == null) { id = Name + GetHashCode().ToString() + ":0"; diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index b988b1f18..af0bbc161 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -3720,7 +3720,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Dictionary substMapBound = new Dictionary(); List /*!*/ tempVars = new List(); - string idAttr = QKeyValue.FindStringAttribute(Attributes, "id"); + string id = (this as ICarriesAttributes).FindStringAttribute("id"); // proc P(ins) returns (outs) // requires Pre @@ -3849,8 +3849,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) } // Do this after copying the attributes so it doesn't get overwritten - if (idAttr is not null) { - ICarriesAttributes.CopyStringAttributeWithSuffix(tok, req, "id", $"${idAttr}$requires", a); + if (id is not null) { + (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${id}$requires"); } a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; @@ -3865,8 +3865,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition)); Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. - if (idAttr is not null) { - ICarriesAttributes.CopyStringAttributeWithSuffix(tok, req, "id", $"${idAttr}$requires_assumed", a); + if (id is not null) { + (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${id}$requires_assumed"); } newBlockBody.Add(a); @@ -4015,9 +4015,6 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(e != null); Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition); AssumeCmd assume = new AssumeCmd(this.tok, copy); - if (idAttr is not null) { - ICarriesAttributes.CopyStringAttributeWithSuffix(tok, e, "id", $"${idAttr}$ensures", assume); - } #region stratified inlining support @@ -4034,6 +4031,10 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #endregion + if (id is not null) { + (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${id}$ensures"); + } + newBlockBody.Add(assume); } @@ -4051,8 +4052,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i])); Contract.Assert(cout_exp != null); AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp); - if (idAttr is not null) { - Attributes = new QKeyValue(param_i.tok, "id", new List(){ $"{idAttr}$out{i}" }, Attributes); + if (id is not null) { + Attributes = new QKeyValue(param_i.tok, "id", new List(){ $"{id}$out{i}" }, Attributes); } newBlockBody.Add(assign); } diff --git a/Source/Core/AST/AbsyType.cs b/Source/Core/AST/AbsyType.cs index 76b4f7941..ff7d90e95 100644 --- a/Source/Core/AST/AbsyType.cs +++ b/Source/Core/AST/AbsyType.cs @@ -3604,7 +3604,7 @@ public override bool IsSeq // be represented using the provided string (and also does not need to be explicitly declared). public string GetBuiltin() { - return this.Decl.FindStringAttribute("builtin"); + return (this.Decl as ICarriesAttributes).FindStringAttribute("builtin"); } //----------- Cloning ---------------------------------- diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs index 0004d7060..e09b44592 100644 --- a/Source/Core/Monomorphization.cs +++ b/Source/Core/Monomorphization.cs @@ -13,7 +13,7 @@ public class MonomorphismChecker : ReadOnlyVisitor public static bool DoesTypeCtorDeclNeedMonomorphization(TypeCtorDecl typeCtorDecl) { - return typeCtorDecl.Arity > 0 && typeCtorDecl.FindStringAttribute("builtin") == null; + return typeCtorDecl.Arity > 0 && (typeCtorDecl as ICarriesAttributes).FindStringAttribute("builtin") == null; } public static bool IsMonomorphic(Program program) diff --git a/Source/ExecutionEngine/VerificationResult.cs b/Source/ExecutionEngine/VerificationResult.cs index b1ccf7ab4..0a685c2fd 100644 --- a/Source/ExecutionEngine/VerificationResult.cs +++ b/Source/ExecutionEngine/VerificationResult.cs @@ -11,7 +11,7 @@ public sealed class VerificationResult { private readonly Implementation implementation; public readonly string ProgramId; - public string MessageIfVerifies => implementation.FindStringAttribute("msg_if_verifies"); + public string MessageIfVerifies => (implementation as ICarriesAttributes).FindStringAttribute("msg_if_verifies"); public string Checksum => implementation.Checksum; public string DependenciesChecksum => implementation.DependencyChecksum; diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 567b536cd..0985109ee 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -239,7 +239,7 @@ public string ExtractBuiltin(Function f) { Contract.Requires(f != null); string retVal = null; - retVal = f.FindStringAttribute("bvbuiltin"); + retVal = (f as ICarriesAttributes).FindStringAttribute("bvbuiltin"); // It used to be "sign_extend 12" in Simplify, and is "(_ sign_extend 12)" with SMT if (retVal != null && (retVal.StartsWith("sign_extend ") || retVal.StartsWith("zero_extend "))) @@ -249,7 +249,7 @@ public string ExtractBuiltin(Function f) if (retVal == null) { - retVal = f.FindStringAttribute("builtin"); + retVal = (f as ICarriesAttributes).FindStringAttribute("builtin"); } if (retVal != null && !LibOptions.UseArrayTheory && SMTLibOpLineariser.ArrayOps.Contains(retVal)) diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 094b6abdf..0016e4675 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -257,7 +257,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu if (options.PrintVerificationCoverage) { // Copy any {:id ...} from the precondition to the assumption, so // we can track it as a "necessary assumption". - ICarriesAttributes.CopyAttribute(req, "id", c); + (c as ICarriesAttributes).CopyIdFrom(req.tok, req); } c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); @@ -324,7 +324,7 @@ protected static void InjectPostConditions(VCGenOptions options, ImplementationR if (options.PrintVerificationCoverage) { // Copy any {:id ...} from the precondition to the assumption, so // we can track it as a "necessary assumption". - ICarriesAttributes.CopyAttribute(ens, "id", c); + (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); } unifiedExitBlock.Cmds.Add(c); if (debugWriter != null) @@ -1395,7 +1395,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing if (Options.PrintVerificationCoverage) { // Copy any {:id ...} from the assignment to the assumption, so // we can track it as a "necessary assumption". - ICarriesAttributes.CopyAttribute(assign, "id", assumeCmd); + (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); } passiveCmds.Add(assumeCmd); } diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 1f5148524..4d7537a93 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -59,7 +59,7 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a var assume = new AssumeCmd(assrt.tok, expr); if (options.PrintVerificationCoverage) { - ICarriesAttributes.CopyAttribute(assrt, "id", assume); + (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); } return assume; } @@ -736,7 +736,7 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary Date: Fri, 2 Jun 2023 10:32:52 -0700 Subject: [PATCH 16/27] Remove `/printNecessaryAssumes` option Now `/printVerificationCoverage` subsumes it. --- Source/ExecutionEngine/CommandLineOptions.cs | 11 +---------- Source/ExecutionEngine/ExecutionEngine.cs | 3 --- .../Provers/SMTLib/SMTLibInteractiveTheoremProver.cs | 4 ++-- Source/Provers/SMTLib/SMTLibOptions.cs | 1 - Source/Provers/SMTLib/TypeDeclCollector.cs | 2 +- Source/VCGeneration/Wlp.cs | 2 +- Test/unnecessaryassumes/unnecessaryassumes0.bpl | 4 ++-- Test/unnecessaryassumes/unnecessaryassumes1.bpl | 4 ++-- .../unnecessaryassumes/unnecessaryassumes1.bpl.expect | 2 +- 9 files changed, 10 insertions(+), 23 deletions(-) diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 115894494..54d7aa9a6 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -201,8 +201,7 @@ public bool NormalizeDeclarationOrder public bool ImmediatelyAcceptCommands => StratifiedInlining > 0 || ContractInfer; - public bool ProduceUnsatCores => PrintNecessaryAssumes || - PrintVerificationCoverage || + public bool ProduceUnsatCores => PrintVerificationCoverage || EnableUnSatCoreExtract == 1 || ContractInfer && (UseUnsatCoreForContractInfer || ExplainHoudini); @@ -281,12 +280,6 @@ public bool UseUnsatCoreForContractInfer { public bool PrintAssignment { get; set; } - // TODO(wuestholz): Add documentation for this flag. - public bool PrintNecessaryAssumes { - get => printNecessaryAssumes; - set => printNecessaryAssumes = value; - } - public bool PrintVerificationCoverage { get => printVerificationCoverage; set => printVerificationCoverage = value; @@ -551,7 +544,6 @@ void ObjectInvariant5() private bool reverseHoudiniWorklist = false; private bool houdiniUseCrossDependencies = false; private bool useUnsatCoreForContractInfer = false; - private bool printNecessaryAssumes = false; private bool printVerificationCoverage = false; private bool useProverEvaluate; private bool trustMoverTypes = false; @@ -1305,7 +1297,6 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("crossDependencies", x => houdiniUseCrossDependencies = x) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", x => useUnsatCoreForContractInfer = x) || ps.CheckBooleanFlag("printAssignment", x => PrintAssignment = x) || - ps.CheckBooleanFlag("printNecessaryAssumes", x => printNecessaryAssumes = x) || ps.CheckBooleanFlag("printVerificationCoverage", x => printVerificationCoverage = x) || ps.CheckBooleanFlag("useProverEvaluate", x => useProverEvaluate = x) || ps.CheckBooleanFlag("deterministicExtractLoops", x => DeterministicExtractLoops = x) || diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 50fd595ee..0f0a2fb37 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -673,9 +673,6 @@ private async Task VerifyEachImplementation(TextWriter output, CleanupRequest(requestId); } - if (Options.PrintNecessaryAssumes && processedProgram.Program.AllCoveredElements.Any()) { - Options.OutputWriter.WriteLine("Necessary assume command(s): {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); - } if (Options.PrintVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index fd1c007eb..67c2c9b8d 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -223,7 +223,7 @@ public async Task CheckSat(CancellationToken cancellationToken, if (resp.Name != "") { usedNamedAssumes.Add(resp.Name); - if (libOptions.PrintNecessaryAssumes || libOptions.PrintVerificationCoverage) + if (libOptions.PrintVerificationCoverage) { reporter.AddCoveredElement(resp.Name.Substring("aux$$assume$$".Length)); } @@ -232,7 +232,7 @@ public async Task CheckSat(CancellationToken cancellationToken, foreach (var arg in resp.Arguments) { usedNamedAssumes.Add(arg.Name); - if (libOptions.PrintNecessaryAssumes || libOptions.PrintVerificationCoverage) + if (libOptions.PrintVerificationCoverage) { reporter.AddCoveredElement(arg.Name.Substring("aux$$assume$$".Length)); } diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs index 81c487216..519edf3d3 100644 --- a/Source/Provers/SMTLib/SMTLibOptions.cs +++ b/Source/Provers/SMTLib/SMTLibOptions.cs @@ -14,7 +14,6 @@ public interface SMTLibOptions : CoreOptions bool ProduceUnsatCores { get; } bool ImmediatelyAcceptCommands { get; } bool RunningBoogieFromCommandLine { get; } - bool PrintNecessaryAssumes { get; } bool PrintVerificationCoverage { get; } string ProverPreamble { get; } bool TraceDiagnosticsOnTimeout { get; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index a6c41ee7f..0e3f64459 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -216,7 +216,7 @@ public override bool Visit(VCExprNAry node, bool arg) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); - if (options.PrintNecessaryAssumes || options.PrintVerificationCoverage) + if (options.PrintVerificationCoverage) { AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); } diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 416cb26e6..3c94be8b8 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -204,7 +204,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var assumeId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (assumeId != null && (ctxt.Options.PrintVerificationCoverage || ctxt.Options.PrintNecessaryAssumes)) + if (assumeId != null && ctxt.Options.PrintVerificationCoverage) { var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); var v = gen.Variable((isTry ? "try$$" : "assume$$") + assumeId, Microsoft.Boogie.Type.Bool); diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl index 927b4adaa..89744fe50 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes0.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl @@ -1,5 +1,5 @@ -// We use boogie instead of parallel-boogie here to fix the order of the output from /printNecessaryAssumes -// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// We use boogie instead of parallel-boogie here to fix the order of the output from /printVerificationCoverage +// RUN: %boogie /printVerificationCoverage "%s" > "%t" // RUN: %diff "%s.expect" "%t" procedure test0(n: int) diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl index cb9f18bb4..aed1d4958 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -1,5 +1,5 @@ -// We use boogie instead of parallel-boogie here to fix the order of the output from /printNecessaryAssumes -// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// We use boogie instead of parallel-boogie here to fix the order of the output from /printVerificationCoverage +// RUN: %boogie /printVerificationCoverage "%s" > "%t" // RUN: %diff "%s.expect" "%t" // UNSUPPORTED: batch_mode diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect index 0d3aeca22..34f57618e 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect @@ -1,3 +1,3 @@ -Necessary assume command(s): s0, s2, s3 +Elements covered by verification: s0, s2, s3 Boogie program verifier finished with 3 verified, 0 errors From d1861c0a42a3e866d2635c373ebbc53ceeb7ec75 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 2 Jun 2023 10:36:28 -0700 Subject: [PATCH 17/27] Typo in comment --- Source/VCGeneration/ConditionGeneration.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 0016e4675..ca2ee07f6 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -322,7 +322,7 @@ protected static void InjectPostConditions(VCGenOptions options, ImplementationR AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; if (options.PrintVerificationCoverage) { - // Copy any {:id ...} from the precondition to the assumption, so + // Copy any {:id ...} from the postcondition to the assumption, so // we can track it as a "necessary assumption". (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); } From a07fe28fe6e7d08b80e1cdb1aa590863b0c688b4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 2 Jun 2023 10:36:49 -0700 Subject: [PATCH 18/27] Documentation for /printVerificationCoverage, :id --- Source/ExecutionEngine/CommandLineOptions.cs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 54d7aa9a6..91d71b0b8 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -1508,7 +1508,10 @@ order in which implementations are verified (default: N = 1). {:id } Assign a unique ID to an implementation to be used for verification - result caching (default: "":0""). + result caching (default: "":0""), or assign a unique ID + to a statement or contract clause for use in identifying which program + elements were necessary to complete verification. The latter form is + used by the `/printVerificationCoverage` option. {:timeLimit N} Set the time limit for verifying a given implementation. @@ -1896,6 +1899,12 @@ without requiring the user to actually make those changes. This option is implemented by renaming variables and reordering declarations in the input, and by setting solver options that have similar effects. + /printVerificationCoverage + Report which program elements labeled with an `{:id ...}` attribute + were necessary to complete verification. Assumptions, assertions, + requires clauses, ensures clauses, assignments, and calls can be + labeled for inclusion in this report. This generalizes and replaces + the previous (undocumented) `/printNecessaryAssertions` option. ---- Verification-condition splitting -------------------------------------- From 82e7e24a9c406d0830b0cf4675c703dccc796715 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 2 Jun 2023 11:20:04 -0700 Subject: [PATCH 19/27] Remove conditionals on magic variable prefixes --- Source/Provers/SMTLib/TypeDeclCollector.cs | 5 +--- Source/VCExpr/VCExprAST.cs | 29 ++++++++++++++++++++-- Source/VCExpr/VCExpressionGenerator.cs | 4 +-- Source/VCGeneration/Wlp.cs | 6 ++--- 4 files changed, 33 insertions(+), 11 deletions(-) diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 0e3f64459..7628fdd95 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -270,10 +270,7 @@ public override bool Visit(VCExprVar node, bool arg) RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - if (!(printedName.StartsWith("assume$$") || - printedName.StartsWith("assert$$") || - printedName.StartsWith("soft$$") || - printedName.StartsWith("try$$"))) + if (node.VarKind == VCExprVarKind.Normal) { AddDeclaration(decl); } diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index a713c0987..a8f68dcbe 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -1771,6 +1771,15 @@ public override Result Accept( // Binders (quantifiers and let-expressions). We introduce our own class for // term variables, but use the Boogie-AST class for type variables + public enum VCExprVarKind + { + Normal, // A normal variable + Soft, // A variable used for tracking an assumption labeled with the `:soft` attribute + Try, // A variable used for tracking an assumption labeled with the `:try` attribute + Assert, // A variable used for tracking an assertion labeled with the `:id` attribute + Assume // A variable used for tracking an assumption labeled with the `:id` attribute + } + public class VCExprVar : VCExpr { // the name of the variable. Note that the name is not used for comparison, @@ -1788,6 +1797,8 @@ public readonly string /*!*/ private readonly Type /*!*/ VarType; + public VCExprVarKind VarKind { get; } + public override Type /*!*/ Type { get @@ -1797,12 +1808,26 @@ public override Type /*!*/ Type } } - internal VCExprVar(string name, Type type) + internal VCExprVar(string name, Type type, VCExprVarKind kind = VCExprVarKind.Normal) { Contract.Requires(type != null); Contract.Requires(name != null); - this.Name = name; + this.Name = KindPrefix(kind) + name; this.VarType = type; + this.VarKind = kind; + } + + private string KindPrefix(VCExprVarKind kind) + { + return kind switch + { + VCExprVarKind.Assert => "assert$$", + VCExprVarKind.Assume => "assume$$", + VCExprVarKind.Soft => "soft$$", + VCExprVarKind.Try => "try$$", + VCExprVarKind.Normal => "", + _ => throw new cce.UnreachableException() + }; } public override Result Accept(IVCExprVisitor visitor, Arg arg) diff --git a/Source/VCExpr/VCExpressionGenerator.cs b/Source/VCExpr/VCExpressionGenerator.cs index 9ebe816ef..c81843fc5 100644 --- a/Source/VCExpr/VCExpressionGenerator.cs +++ b/Source/VCExpr/VCExpressionGenerator.cs @@ -781,12 +781,12 @@ public VCTrigger Trigger(bool pos, params VCExpr[] exprs) // Reference to a bound or free variable - public VCExprVar Variable(string name, Type type) + public VCExprVar Variable(string name, Type type, VCExprVarKind kind = VCExprVarKind.Normal) { Contract.Requires(type != null); Contract.Requires(name != null); Contract.Ensures(Contract.Result() != null); - return new VCExprVar(name, type); + return new VCExprVar(name, type, kind); } } } diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 3c94be8b8..8dccab23b 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -112,7 +112,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var assertId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); if (assertId != null && ctxt.Options.PrintVerificationCoverage) { - var v = gen.Variable($"assert$${assertId}", Microsoft.Boogie.Type.Bool); + var v = gen.Variable(assertId, Microsoft.Boogie.Type.Bool, VCExprVarKind.Assert); C = gen.Function(VCExpressionGenerator.NamedAssertOp, v, gen.AndSimp(v, C)); } @@ -207,7 +207,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) if (assumeId != null && ctxt.Options.PrintVerificationCoverage) { var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); - var v = gen.Variable((isTry ? "try$$" : "assume$$") + assumeId, Microsoft.Boogie.Type.Bool); + var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, isTry ? VCExprVarKind.Try : VCExprVarKind.Assume); expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); } @@ -215,7 +215,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0); if ((soft || 0 < softWeight) && assumeId != null) { - var v = gen.Variable("soft$$" + assumeId, Microsoft.Boogie.Type.Bool); + var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, VCExprVarKind.Soft); expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr)); } From 98dcf9ffcc8468be5330ece10ec725bc2c4a1290 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 2 Jun 2023 11:55:43 -0700 Subject: [PATCH 20/27] Copy `:id` attributes unconditionally --- Source/VCGeneration/ConditionGeneration.cs | 24 +++++++---------- Source/VCGeneration/VCGen.cs | 30 +++++++++------------- 2 files changed, 21 insertions(+), 33 deletions(-) diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ca2ee07f6..171afd917 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -254,11 +254,9 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu Contract.Assert(req != null); Expr e = Substituter.Apply(formalProcImplSubst, req.Condition); AssumeCmd c = new AssumeCmd(req.tok, e); - if (options.PrintVerificationCoverage) { - // Copy any {:id ...} from the precondition to the assumption, so - // we can track it as a "necessary assumption". - (c as ICarriesAttributes).CopyIdFrom(req.tok, req); - } + // Copy any {:id ...} from the precondition to the assumption, so + // we can track it while analyzing verification coverage. + (c as ICarriesAttributes).CopyIdFrom(req.tok, req); c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) @@ -321,11 +319,9 @@ protected static void InjectPostConditions(VCGenOptions options, ImplementationR ensCopy.Condition = e; AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; - if (options.PrintVerificationCoverage) { - // Copy any {:id ...} from the postcondition to the assumption, so - // we can track it as a "necessary assumption". - (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); - } + // Copy any {:id ...} from the postcondition to the assumption, so + // we can track it while analyzing verification coverage. + (c as ICarriesAttributes).CopyIdFrom(ens.tok, ens); unifiedExitBlock.Cmds.Add(c); if (debugWriter != null) { @@ -1392,11 +1388,9 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing } var assumeCmd = new AssumeCmd(c.tok, assumption); - if (Options.PrintVerificationCoverage) { - // Copy any {:id ...} from the assignment to the assumption, so - // we can track it as a "necessary assumption". - (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); - } + // Copy any {:id ...} from the assignment to the assumption, so + // we can track it while analyzing verification coverage. + (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); passiveCmds.Add(assumeCmd); } diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 4d7537a93..470b4a2b5 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -58,9 +58,9 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a } var assume = new AssumeCmd(assrt.tok, expr); - if (options.PrintVerificationCoverage) { - (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); - } + // Copy any {:id ...} from the assertion to the assumption, so + // we can track it while analyzing verification coverage. + (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); return assume; } @@ -733,11 +733,9 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary Date: Mon, 5 Jun 2023 09:10:18 -0700 Subject: [PATCH 21/27] Rename variable for `id` on `CallCmd`s --- Source/Core/AST/AbsyCmd.cs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index af0bbc161..19697003b 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -3720,7 +3720,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Dictionary substMapBound = new Dictionary(); List /*!*/ tempVars = new List(); - string id = (this as ICarriesAttributes).FindStringAttribute("id"); + string callId = (this as ICarriesAttributes).FindStringAttribute("id"); // proc P(ins) returns (outs) // requires Pre @@ -3849,8 +3849,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) } // Do this after copying the attributes so it doesn't get overwritten - if (id is not null) { - (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${id}$requires"); + if (callId is not null) { + (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires"); } a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; @@ -3865,8 +3865,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition)); Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. - if (id is not null) { - (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${id}$requires_assumed"); + if (callId is not null) { + (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires_assumed"); } newBlockBody.Add(a); @@ -4031,8 +4031,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #endregion - if (id is not null) { - (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${id}$ensures"); + if (callId is not null) { + (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${callId}$ensures"); } newBlockBody.Add(assume); @@ -4052,8 +4052,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i])); Contract.Assert(cout_exp != null); AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp); - if (id is not null) { - Attributes = new QKeyValue(param_i.tok, "id", new List(){ $"{id}$out{i}" }, Attributes); + if (callId is not null) { + Attributes = new QKeyValue(param_i.tok, "id", new List(){ $"{callId}$out{i}" }, Attributes); } newBlockBody.Add(assign); } From 6d48d32a229ca453381f23ed6a83384522ff3d4c Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 5 Jun 2023 09:10:38 -0700 Subject: [PATCH 22/27] Add comment about dummy operators --- Source/VCExpr/VCExpressionGenerator.cs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Source/VCExpr/VCExpressionGenerator.cs b/Source/VCExpr/VCExpressionGenerator.cs index c81843fc5..6cc61ce05 100644 --- a/Source/VCExpr/VCExpressionGenerator.cs +++ b/Source/VCExpr/VCExpressionGenerator.cs @@ -442,6 +442,8 @@ int AndSize(VCExpr e) public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool); + // These operators are temporarily added to VCExprs to track where labels for optimization and unsat + // core generation should go, but don't appear in the final SMT-Lib output. public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool); public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool); public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool); From e43e4f2131eea950a8c3ae51d58249cd3ca95dfd Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 5 Jun 2023 09:09:51 -0700 Subject: [PATCH 23/27] PrintVerificationCoverage -> TrackVerificationCoverage --- Source/ExecutionEngine/CommandLineOptions.cs | 27 ++++++++++--------- Source/ExecutionEngine/ExecutionEngine.cs | 2 +- .../SMTLib/SMTLibInteractiveTheoremProver.cs | 4 +-- Source/Provers/SMTLib/SMTLibOptions.cs | 2 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 2 +- Source/VCGeneration/Split.cs | 2 +- Source/VCGeneration/Wlp.cs | 4 +-- 7 files changed, 22 insertions(+), 21 deletions(-) diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 91d71b0b8..938d10495 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -201,7 +201,7 @@ public bool NormalizeDeclarationOrder public bool ImmediatelyAcceptCommands => StratifiedInlining > 0 || ContractInfer; - public bool ProduceUnsatCores => PrintVerificationCoverage || + public bool ProduceUnsatCores => TrackVerificationCoverage || EnableUnSatCoreExtract == 1 || ContractInfer && (UseUnsatCoreForContractInfer || ExplainHoudini); @@ -280,9 +280,9 @@ public bool UseUnsatCoreForContractInfer { public bool PrintAssignment { get; set; } - public bool PrintVerificationCoverage { - get => printVerificationCoverage; - set => printVerificationCoverage = value; + public bool TrackVerificationCoverage { + get => trackVerificationCoverage; + set => trackVerificationCoverage = value; } public int InlineDepth { get; set; } = -1; @@ -544,7 +544,7 @@ void ObjectInvariant5() private bool reverseHoudiniWorklist = false; private bool houdiniUseCrossDependencies = false; private bool useUnsatCoreForContractInfer = false; - private bool printVerificationCoverage = false; + private bool trackVerificationCoverage = false; private bool useProverEvaluate; private bool trustMoverTypes = false; private bool trustNoninterference = false; @@ -1297,7 +1297,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("crossDependencies", x => houdiniUseCrossDependencies = x) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", x => useUnsatCoreForContractInfer = x) || ps.CheckBooleanFlag("printAssignment", x => PrintAssignment = x) || - ps.CheckBooleanFlag("printVerificationCoverage", x => printVerificationCoverage = x) || + ps.CheckBooleanFlag("trackVerificationCoverage", x => trackVerificationCoverage = x) || ps.CheckBooleanFlag("useProverEvaluate", x => useProverEvaluate = x) || ps.CheckBooleanFlag("deterministicExtractLoops", x => DeterministicExtractLoops = x) || ps.CheckBooleanFlag("verifySeparately", x => VerifySeparately = x) || @@ -1511,7 +1511,7 @@ order in which implementations are verified (default: N = 1). result caching (default: "":0""), or assign a unique ID to a statement or contract clause for use in identifying which program elements were necessary to complete verification. The latter form is - used by the `/printVerificationCoverage` option. + used by the `/trackVerificationCoverage` option. {:timeLimit N} Set the time limit for verifying a given implementation. @@ -1899,12 +1899,13 @@ without requiring the user to actually make those changes. This option is implemented by renaming variables and reordering declarations in the input, and by setting solver options that have similar effects. - /printVerificationCoverage - Report which program elements labeled with an `{:id ...}` attribute - were necessary to complete verification. Assumptions, assertions, - requires clauses, ensures clauses, assignments, and calls can be - labeled for inclusion in this report. This generalizes and replaces - the previous (undocumented) `/printNecessaryAssertions` option. + /trackVerificationCoverage + Track and report which program elements labeled with an + `{:id ...}` attribute were necessary to complete verification. + Assumptions, assertions, requires clauses, ensures clauses, + assignments, and calls can be labeled for inclusion in this + report. This generalizes and replaces the previous + (undocumented) `/printNecessaryAssertions` option. ---- Verification-condition splitting -------------------------------------- diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 0f0a2fb37..20e799519 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -673,7 +673,7 @@ private async Task VerifyEachImplementation(TextWriter output, CleanupRequest(requestId); } - if (Options.PrintVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { + if (Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 67c2c9b8d..1f5693470 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -223,7 +223,7 @@ public async Task CheckSat(CancellationToken cancellationToken, if (resp.Name != "") { usedNamedAssumes.Add(resp.Name); - if (libOptions.PrintVerificationCoverage) + if (libOptions.TrackVerificationCoverage) { reporter.AddCoveredElement(resp.Name.Substring("aux$$assume$$".Length)); } @@ -232,7 +232,7 @@ public async Task CheckSat(CancellationToken cancellationToken, foreach (var arg in resp.Arguments) { usedNamedAssumes.Add(arg.Name); - if (libOptions.PrintVerificationCoverage) + if (libOptions.TrackVerificationCoverage) { reporter.AddCoveredElement(arg.Name.Substring("aux$$assume$$".Length)); } diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs index 519edf3d3..354c91979 100644 --- a/Source/Provers/SMTLib/SMTLibOptions.cs +++ b/Source/Provers/SMTLib/SMTLibOptions.cs @@ -14,7 +14,7 @@ public interface SMTLibOptions : CoreOptions bool ProduceUnsatCores { get; } bool ImmediatelyAcceptCommands { get; } bool RunningBoogieFromCommandLine { get; } - bool PrintVerificationCoverage { get; } + bool TrackVerificationCoverage { get; } string ProverPreamble { get; } bool TraceDiagnosticsOnTimeout { get; } uint TimeLimitPerAssertionInPercent { get; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 7628fdd95..632d56942 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -216,7 +216,7 @@ public override bool Visit(VCExprNAry node, bool arg) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); - if (options.PrintVerificationCoverage) + if (options.TrackVerificationCoverage) { AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index ccac566e4..2c98735aa 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1271,7 +1271,7 @@ public int GetHashCode(List obj) run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, checker.ProverRunTime.TotalSeconds, outcome); } - if (options.Trace && options.PrintVerificationCoverage) { + if (options.Trace && options.TrackVerificationCoverage) { run.OutputWriter.WriteLine("Covered elements: {0}", string.Join(", ", reporter.CurrentCoveredElements.OrderBy(s => s))); } diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 8dccab23b..67d8b54f4 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -110,7 +110,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var assertId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (assertId != null && ctxt.Options.PrintVerificationCoverage) + if (assertId != null && ctxt.Options.TrackVerificationCoverage) { var v = gen.Variable(assertId, Microsoft.Boogie.Type.Bool, VCExprVarKind.Assert); C = gen.Function(VCExpressionGenerator.NamedAssertOp, v, gen.AndSimp(v, C)); @@ -204,7 +204,7 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var assumeId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (assumeId != null && ctxt.Options.PrintVerificationCoverage) + if (assumeId != null && ctxt.Options.TrackVerificationCoverage) { var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, isTry ? VCExprVarKind.Try : VCExprVarKind.Assume); From 94cf1eabba9ad66a35e3669f2a7305a560289cf9 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 5 Jun 2023 09:13:00 -0700 Subject: [PATCH 24/27] CurrentCoveredElements -> ProofRun.CoveredElements --- Source/Houdini/HoudiniSession.cs | 1 + Source/VCGeneration/ProofRun.cs | 2 ++ Source/VCGeneration/Split.cs | 6 ++++-- Source/VCGeneration/VCGen.cs | 5 +---- 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 5dc098482..81b0b541e 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -126,6 +126,7 @@ public class HoudiniStatistics private readonly Houdini houdini; public HoudiniStatistics stats; public List Counterexamples { get; } = new(); + public HashSet CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; ConditionGeneration.VerificationResultCollector collector; diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index 3bec8b330..752fb4372 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -7,4 +7,6 @@ public interface ProofRun { string Description { get; } List Counterexamples { get; } + + HashSet CoveredElements { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 2c98735aa..b9c97ffa6 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1273,7 +1273,7 @@ public int GetHashCode(List obj) } if (options.Trace && options.TrackVerificationCoverage) { run.OutputWriter.WriteLine("Covered elements: {0}", - string.Join(", ", reporter.CurrentCoveredElements.OrderBy(s => s))); + string.Join(", ", CoveredElements.OrderBy(s => s))); } var resourceCount = await checker.GetProverResourceCount(); @@ -1286,7 +1286,7 @@ public int GetHashCode(List obj) maxCounterExamples: checker.Options.ErrorLimit, counterExamples: Counterexamples, asserts: Asserts, - coveredElements: reporter.CurrentCoveredElements, + coveredElements: CoveredElements, resourceCount: resourceCount); callback.OnVCResult(result); @@ -1300,6 +1300,8 @@ public int GetHashCode(List obj) public List Counterexamples { get; } = new(); + public HashSet CoveredElements { get; } = new(); + /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". /// diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 470b4a2b5..a43b23703 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -462,12 +462,10 @@ void ObjectInvariant() Program program; - public HashSet CurrentCoveredElements { get; } - public override void AddCoveredElement(string id) { program.AllCoveredElements.Add(id); - CurrentCoveredElements.Add(id); + split.CoveredElements.Add(id); } public ErrorReporter(VCGenOptions options, @@ -497,7 +495,6 @@ public ErrorReporter(VCGenOptions options, this.program = program; this.split = split; this.options = options; - this.CurrentCoveredElements = new(); } public override void OnModel(IList labels /*!*/ /*!*/, Model model, From 449364c726888e3035ed8cd5874b8d673cd28581 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 5 Jun 2023 09:13:42 -0700 Subject: [PATCH 25/27] Rename command variables in VCGen for loops --- Source/VCGeneration/VCGen.cs | 45 ++++++++++++++++++------------------ 1 file changed, 23 insertions(+), 22 deletions(-) diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index a43b23703..8d9c5066d 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -704,78 +704,79 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary prefixOfPredicateCmdsMaintained = new List(); for (int i = 0, n = header.Cmds.Count; i < n; i++) { - PredicateCmd a = header.Cmds[i] as PredicateCmd; - if (a != null) + PredicateCmd predicateCmd = header.Cmds[i] as PredicateCmd; + if (predicateCmd != null) { - if (a is AssertCmd) + if (predicateCmd is AssertCmd) { - AssertCmd c = (AssertCmd) a; - AssertCmd b = null; + AssertCmd assertCmd = (AssertCmd) predicateCmd; + AssertCmd initAssertCmd = null; if (Options.ConcurrentHoudini) { Contract.Assert(taskID >= 0); if (Options.Cho[taskID].DisableLoopInvEntryAssert) { - b = new LoopInitAssertCmd(c.tok, Expr.True, c); + initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, Expr.True, assertCmd); } else { - b = new LoopInitAssertCmd(c.tok, c.Expr, c); + initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); } } else { - b = new LoopInitAssertCmd(c.tok, c.Expr, c); + initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); } - b.Attributes = (QKeyValue)c.Attributes?.Clone(); + initAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone(); // Copy any {:id ...} from the invariant to the assertion that it's established, so // we can track it while analyzing verification coverage. - (b as ICarriesAttributes).CopyIdWithSuffixFrom(c.tok, c, "$established"); + (initAssertCmd as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$established"); - prefixOfPredicateCmdsInit.Add(b); + prefixOfPredicateCmdsInit.Add(initAssertCmd); + LoopInvMaintainedAssertCmd maintainedAssertCmd; if (Options.ConcurrentHoudini) { Contract.Assert(taskID >= 0); if (Options.Cho[taskID].DisableLoopInvMaintainedAssert) { - b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True, c); + maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, Expr.True, assertCmd); } else { - b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr, c); + maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); } } else { - b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr, c); + maintainedAssertCmd = new Bpl.LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd); } - b.Attributes = (QKeyValue)c.Attributes?.Clone(); + maintainedAssertCmd.Attributes = (QKeyValue)assertCmd.Attributes?.Clone(); // Copy any {:id ...} from the invariant to the assertion that it's maintained, so // we can track it while analyzing verification coverage. - (b as ICarriesAttributes).CopyIdWithSuffixFrom(c.tok, c, "$maintained"); + (maintainedAssertCmd as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$maintained"); - prefixOfPredicateCmdsMaintained.Add(b); - AssumeCmd assume = new AssumeCmd(c.tok, c.Expr); + prefixOfPredicateCmdsMaintained.Add(maintainedAssertCmd); + AssumeCmd assume = new AssumeCmd(assertCmd.tok, assertCmd.Expr); // Copy any {:id ...} from the invariant to the assumption used within the body, so // we can track it while analyzing verification coverage. - (assume as ICarriesAttributes).CopyIdWithSuffixFrom(c.tok, c, "$assume_in_body"); + (assume as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$assume_in_body"); header.Cmds[i] = assume; } else { - Contract.Assert(a is AssumeCmd); + Contract.Assert(predicateCmd is AssumeCmd); if (Options.AlwaysAssumeFreeLoopInvariants) { // Usually, "free" stuff, like free loop invariants (and the assume statements // that stand for such loop invariants) are ignored on the checking side. This // command-line option changes that behavior to always assume the conditions. - prefixOfPredicateCmdsInit.Add(a); - prefixOfPredicateCmdsMaintained.Add(a); + prefixOfPredicateCmdsInit.Add(predicateCmd); + prefixOfPredicateCmdsMaintained.Add(predicateCmd); } } } From 725fe2dcc5e2f84d39c1b069a88906c5cf030b95 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 5 Jun 2023 09:14:30 -0700 Subject: [PATCH 26/27] Update verification coverage test * Use new option name * Depend on different postconditions from different calls to same target --- Test/coverage/verificationCoverage.bpl | 3 ++- Test/coverage/verificationCoverage.bpl.expect.coverage | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index 064a946f8..e5e27f135 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -1,6 +1,6 @@ // RUN: %boogie "%s" > "%t.plain" // RUN: %diff "%s.expect.plain" "%t.plain" -// RUN: %boogie -printVerificationCoverage "%s" > "%t.coverage" +// RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage" // RUN: %diff "%s.expect.coverage" "%t.coverage" // UNSUPPORTED: batch_mode @@ -80,6 +80,7 @@ procedure testEnsuresCaller(n: int) returns (r: int) var y: int; call {:id "call1"} x := testEnsuresCallee(n+1); // requires and ensures covered call {:id "call2"} y := testEnsuresCallee(n+1); // requires and ensures covered + assert {:id "call2_tee1"} y > 0; r := {:id "xy_sum"} x + y; // covered } diff --git a/Test/coverage/verificationCoverage.bpl.expect.coverage b/Test/coverage/verificationCoverage.bpl.expect.coverage index 9d7da48a0..32f5d2408 100644 --- a/Test/coverage/verificationCoverage.bpl.expect.coverage +++ b/Test/coverage/verificationCoverage.bpl.expect.coverage @@ -1,3 +1,3 @@ -Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum +Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum Boogie program verifier finished with 10 verified, 0 errors From cd50eef00c5a5ee308eb1f404d27127f47b5f762 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 5 Jun 2023 09:36:55 -0700 Subject: [PATCH 27/27] Remove uses of /printVerificationCoverage --- Test/unnecessaryassumes/unnecessaryassumes0.bpl | 2 +- Test/unnecessaryassumes/unnecessaryassumes1.bpl | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl index 89744fe50..6bc21cddb 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes0.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl @@ -1,5 +1,5 @@ // We use boogie instead of parallel-boogie here to fix the order of the output from /printVerificationCoverage -// RUN: %boogie /printVerificationCoverage "%s" > "%t" +// RUN: %boogie /trackVerificationCoverage "%s" > "%t" // RUN: %diff "%s.expect" "%t" procedure test0(n: int) diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl index aed1d4958..34377644f 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -1,5 +1,5 @@ -// We use boogie instead of parallel-boogie here to fix the order of the output from /printVerificationCoverage -// RUN: %boogie /printVerificationCoverage "%s" > "%t" +// We use boogie instead of parallel-boogie here to fix the order of the output from /trackVerificationCoverage +// RUN: %boogie /trackVerificationCoverage "%s" > "%t" // RUN: %diff "%s.expect" "%t" // UNSUPPORTED: batch_mode