From 21f1cfff139759d9b9f91ed800da2158daca8ed4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Aug 2015 20:10:41 -0700 Subject: Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code. --- Source/VCGeneration/VC.cs | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3a483a58..8e5c853c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1763,9 +1763,18 @@ namespace VC { { var checksum = a.Checksum; var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample; - if (oldCex != null) - { - callback.OnCounterexample(oldCex, null); + if (oldCex != null) { + if (CommandLineOptions.Clo.VerifySnapshots < 3) { + callback.OnCounterexample(oldCex, null); + } else { + // If possible, we use the old counterexample, but with the location information of "a" + var cex = AssertCmdToCloneCounterexample(a, oldCex); + callback.OnCounterexample(cex, null); + // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields. We make + // any such updates available in oldCex. (Is this really a good design? --KRML) + oldCex.RequestId = cex.RequestId; + oldCex.OriginalRequestId = cex.OriginalRequestId; + } } } } @@ -3137,6 +3146,31 @@ namespace VC { } } + /// + /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". + /// + public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) { + Contract.Requires(assrt != null); + Contract.Requires(cex != null); + Contract.Ensures(Contract.Result() != null); + + List relatedInformation = new List(); + + Counterexample cc; + if (assrt is AssertRequiresCmd) { + var aa = (AssertRequiresCmd)assrt; + cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum); + } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) { + var aa = (AssertEnsuresCmd)assrt; + var oldCex = (ReturnCounterexample)cex; + cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum); + } else { + cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context); + } + cc.relatedInformation = relatedInformation; + return cc; + } + static VCExpr LetVC(Block startBlock, VCExpr controlFlowVariableExpr, Dictionary label2absy, -- cgit v1.2.3 From 7a2aec84f1d924086b6f8e0f3dcbde036e12345c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 28 Sep 2015 09:47:27 -0700 Subject: update --- Source/Core/CommandLineOptions.cs | 6 +++--- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- Source/VCGeneration/VC.cs | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2dda1dd9..f4cba1dc 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -588,7 +588,7 @@ namespace Microsoft.Boogie { } } - public string OwickiGriesDesugaredOutputFile = null; + public string CivlDesugaredFile = null; public bool TrustAtomicityTypes = false; public bool TrustNonInterference = false; public int TrustLayersUpto = -1; @@ -915,9 +915,9 @@ namespace Microsoft.Boogie { } return true; - case "OwickiGries": + case "CivlDesugaredFile": if (ps.ConfirmArgumentCount(1)) { - OwickiGriesDesugaredOutputFile = args[ps.i]; + CivlDesugaredFile = args[ps.i]; } return true; diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cf44a77f..15fdc081 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -502,11 +502,11 @@ namespace Microsoft.Boogie { Concurrency.Transform(linearTypeChecker, civlTypeChecker); (new LinearEraser()).VisitProgram(program); - if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null) + if (CommandLineOptions.Clo.CivlDesugaredFile != null) { int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; CommandLineOptions.Clo.PrintUnstructured = 1; - PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); + PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b457b383..94584027 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1632,7 +1632,7 @@ namespace VC { //use Duplicator and Substituter rather than new //nested IToken? //document expand attribute (search for {:ignore}, for example) - //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs + //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs Func withType = (Expr from, Expr to) => { NAryExpr nFrom = from as NAryExpr; -- cgit v1.2.3 From 597a558b2fde558b7f5c581481fd51258aa37c46 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 30 Sep 2015 21:53:31 +0200 Subject: Improve output for diagnosing timeouts. --- Source/ExecutionEngine/ExecutionEngine.cs | 37 ++++++++++++++++++++++++++++-- Source/VCGeneration/ConditionGeneration.cs | 13 ++++++++++- Source/VCGeneration/VC.cs | 1 + 3 files changed, 48 insertions(+), 3 deletions(-) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 15fdc081..4ab0a9c5 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1459,11 +1459,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw); - ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit); + ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors); } - private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit) + private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List errors) { ErrorInformation errorInfo = null; @@ -1476,6 +1476,35 @@ namespace Microsoft.Boogie if (implName != null && implTok != null) { errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId); + + // Report timed out assertions as auxiliary info. + if (errors != null) + { + var cmpr = new CounterexampleComparer(); + var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList(); + timedOutAssertions.Sort(cmpr); + int idx = 1; + foreach (Counterexample error in timedOutAssertions) + { + var callError = error as CallCounterexample; + var returnError = error as ReturnCounterexample; + var assertError = error as AssertCounterexample; + IToken tok = null; + if (callError != null) + { + tok = callError.FailingCall.tok; + } + else if (returnError != null) + { + tok = returnError.FailingReturn.tok; + } + else + { + tok = assertError.FailingAssert.tok; + } + errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count)); + } + } } break; case VCGen.Outcome.OutOfMemory: @@ -1592,6 +1621,10 @@ namespace Microsoft.Boogie errors.Sort(new CounterexampleComparer()); foreach (Counterexample error in errors) { + if (error.IsAuxiliaryCexForDiagnosingTimeouts) + { + continue; + } var errorInfo = CreateErrorInformation(error, outcome); errorInfo.ImplementationName = implName; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 1f010757..ae0a1147 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -85,6 +85,7 @@ namespace Microsoft.Boogie { public string RequestId; public abstract byte[] Checksum { get; } public byte[] SugaredCmdChecksum; + public bool IsAuxiliaryCexForDiagnosingTimeouts; public Dictionary calleeCounterexamples; @@ -313,7 +314,7 @@ namespace Microsoft.Boogie { public abstract int GetLocation(); } - public class CounterexampleComparer : IComparer { + public class CounterexampleComparer : IComparer, IEqualityComparer { private int Compare(List bs1, List bs2) { @@ -375,6 +376,16 @@ namespace Microsoft.Boogie { } return -1; } + + public bool Equals(Counterexample x, Counterexample y) + { + return Compare(x, y) == 0; + } + + public int GetHashCode(Counterexample obj) + { + return 0; + } } public class AssertCounterexample : Counterexample { diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 94584027..33e2f928 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2113,6 +2113,7 @@ namespace VC { foreach (var cmd in assertCmds) { Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List(), null, null, context); + cex.IsAuxiliaryCexForDiagnosingTimeouts = true; callback.OnCounterexample(cex, msg); } } -- cgit v1.2.3 From 0732077773c80e86f8fbbc0be94ae9c034ad1924 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 29 Oct 2015 18:40:23 -0500 Subject: Add support for annotating implementations with k-ind. depth. --- Source/VCGeneration/VC.cs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 33e2f928..79f56934 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2229,10 +2229,11 @@ namespace VC { impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List(), new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); ResetPredecessors(impl.Blocks); - if(CommandLineOptions.Clo.KInductionDepth < 0) { + var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1)); + if(k < 0) { ConvertCFG2DAGStandard(impl, edgesCut, taskID); } else { - ConvertCFG2DAGKInduction(impl, edgesCut, taskID); + ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k); } #region Debug Tracing @@ -2497,14 +2498,12 @@ namespace VC { return referencedVars; } - private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary> edgesCut, int taskID) { + private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary> edgesCut, int taskID, int inductionK) { // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses Contract.Requires(edgesCut == null); Contract.Requires(taskID == -1); - - int inductionK = CommandLineOptions.Clo.KInductionDepth; - Contract.Assume(inductionK >= 0); + Contract.Requires(0 <= inductionK); bool contRuleApplication = true; while (contRuleApplication) { -- cgit v1.2.3 From f049d2ec646244bc40964b36d961966fe2a3e4dc Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 16 Nov 2015 12:04:37 -0600 Subject: Add support for identifying unnecessary assumes. --- Source/Core/Absy.cs | 2 ++ Source/Core/AbsyCmd.cs | 12 +++++++++ Source/Core/CommandLineOptions.cs | 3 +++ Source/Core/ResolutionContext.cs | 12 +++++++++ Source/ExecutionEngine/ExecutionEngine.cs | 5 ++++ Source/Provers/SMTLib/ProverInterface.cs | 30 ++++++++++++++++++++-- Source/VCGeneration/Check.cs | 16 ++++++++++-- Source/VCGeneration/VC.cs | 28 ++++++++++++++------ Source/VCGeneration/Wlp.cs | 17 +++++++++--- Test/unnecessaryassumes/unnecessaryassumes0.bpl | 13 ++++++++++ .../unnecessaryassumes0.bpl.expect | 3 +++ Test/unnecessaryassumes/unnecessaryassumes1.bpl | 23 +++++++++++++++++ .../unnecessaryassumes1.bpl.expect | 3 +++ 13 files changed, 151 insertions(+), 16 deletions(-) create mode 100644 Test/unnecessaryassumes/unnecessaryassumes0.bpl create mode 100644 Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect create mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl create mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d2243085..8be4f24e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -696,6 +696,8 @@ namespace Microsoft.Boogie { } } + public readonly ISet NecessaryAssumes = new HashSet(); + public IEnumerable Blocks() { return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 404945a9..c33f0743 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie { } finally { rc.TypeBinderState = previousTypeBinderState; } + + var id = QKeyValue.FindStringAttribute(Attributes, "id"); + if (id != null) + { + rc.AddStatementId(tok, id); + } } public override void AddAssignedVariables(List vars) { @@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie { public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); Expr.Resolve(rc); + + var id = QKeyValue.FindStringAttribute(Attributes, "id"); + if (id != null) + { + rc.AddStatementId(tok, id); + } } public override void AddAssignedVariables(List vars) { //Contract.Requires(vars != null); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 3892bbc0..e9aa3ceb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -479,6 +479,8 @@ namespace Microsoft.Boogie { public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; + // TODO(wuestholz): Add documentation for this flag. + public bool PrintNecessaryAssumes = false; public int InlineDepth = -1; public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values public bool UseUncheckedContracts = false; @@ -1619,6 +1621,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) || ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) || ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) || diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 474a91dd..279e00bf 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -339,6 +339,18 @@ namespace Microsoft.Boogie { varContext = varContext.ParentContext; } + public readonly ISet StatementIds = new HashSet(); + + public void AddStatementId(IToken tok, string name) + { + if (StatementIds.Contains(name)) + { + Error(tok, "more than one statement with same id: " + name); + return; + } + StatementIds.Add(name); + } + public void AddVariable(Variable var, bool global) { Contract.Requires(var != null); var previous = FindVariable(cce.NonNull(var.Name), !global); diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 9623139a..9bc855be 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1008,6 +1008,11 @@ namespace Microsoft.Boogie CleanupCheckers(requestId); } + if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any()) + { + Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes)); + } + cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); outputCollector.WriteMoreOutput(); diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index e93ecee9..cb8442e5 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -246,9 +246,9 @@ namespace Microsoft.Boogie.SMTLib // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 ) - if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)) + if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))) { - SendThisVC("(set-option :produce-unsat-cores true)"); + SendCommon("(set-option :produce-unsat-cores true)"); this.usingUnsatCore = true; } @@ -408,6 +408,15 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + + if (NamedAssumeVars != null) + { + foreach (var v in NamedAssumeVars) + { + SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name)); + } + } + SendThisVC(vcString); FlushLogFile(); @@ -446,6 +455,7 @@ namespace Microsoft.Boogie.SMTLib if (options.Solver == SolverKind.Z3) { this.gen = gen; + SendThisVC("(reset)"); Namer.Reset(); common.Clear(); SetupAxiomBuilder(gen); @@ -1264,6 +1274,22 @@ namespace Microsoft.Boogie.SMTLib result = GetResponse(); + var reporter = handler as VC.VCGen.ErrorReporter; + // TODO(wuestholz): Is the reporter ever null? + if (NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null) + { + SendThisVC("(get-unsat-core)"); + var resp = Process.GetProverResponse(); + if (resp.Name != "") + { + reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + } + foreach (var arg in resp.Arguments) + { + reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + } + } + if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) { #region Run timeout diagnostics diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3c3b5cae..da445a00 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -346,7 +346,7 @@ namespace Microsoft.Boogie { } } - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList namedAssumeVars = null) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); @@ -357,9 +357,18 @@ namespace Microsoft.Boogie { outputExn = null; this.handler = handler; - thmProver.Reset(gen); + if (namedAssumeVars != null && namedAssumeVars.Any()) + { + // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug. + thmProver.FullReset(gen); + } + else + { + thmProver.Reset(gen); + } SetTimeout(); proverStart = DateTime.UtcNow; + thmProver.NamedAssumeVars = namedAssumeVars; thmProver.BeginCheck(descriptiveName, vc, handler); // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy @@ -386,6 +395,9 @@ namespace Microsoft.Boogie { // ----------------------------------------------------------------------------------------------- public abstract class ProverInterface { + + public IList NamedAssumeVars; + public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) { Contract.Requires(prog != null); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 79f56934..2762fc72 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1386,7 +1386,8 @@ namespace VC { var exprGen = ctx.ExprGen; VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context); + var namedAssumeVars = new List(); + VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars); Contract.Assert(vc != null); if (!CommandLineOptions.Clo.UseLabels) @@ -1414,7 +1415,7 @@ namespace VC { string desc = cce.NonNull(impl.Name); if (no >= 0) desc += "_split" + no; - checker.BeginCheck(desc, vc, reporter); + checker.BeginCheck(desc, vc, reporter, namedAssumeVars); } private void SoundnessCheck(HashSet/*!*/>/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { @@ -1519,7 +1520,7 @@ namespace VC { } } - public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext) + public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext, IList namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); @@ -1527,10 +1528,10 @@ namespace VC { Contract.Ensures(Contract.Result() != null); label2absy = new Dictionary(); - return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext); + return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars); } - public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext) { + public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext, IList namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); Contract.Ensures(Contract.Result() != null); @@ -1567,7 +1568,8 @@ namespace VC { } break; case CommandLineOptions.VCVariety.DagIterative: - vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount); + // TODO(wuestholz): Support named assume statements not just for this encoding. + vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars); break; case CommandLineOptions.VCVariety.Doomed: vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount); @@ -2021,6 +2023,16 @@ namespace VC { protected ProverContext/*!*/ context; Program/*!*/ program; + public IEnumerable NecessaryAssumes + { + get { return program.NecessaryAssumes; } + } + + public void AddNecessaryAssume(string id) + { + program.NecessaryAssumes.Add(id); + } + public ErrorReporter(Dictionary/*!*/ gotoCmdOrigins, Dictionary/*!*/ label2absy, List/*!*/ blocks, @@ -3192,7 +3204,7 @@ namespace VC { Dictionary label2absy, ProverContext proverCtxt, out int assertionCount, - bool isPositiveContext = true) + bool isPositiveContext = true, IList namedAssumeVars = null) { Contract.Requires(blocks != null); Contract.Requires(proverCtxt != null); @@ -3252,7 +3264,7 @@ namespace VC { } VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext); - VCExpr vc = Wlp.Block(block, SuccCorrect, context); + VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars); assertionCount += context.AssertionCount; VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index b4ee4c09..74b77188 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -48,7 +48,7 @@ namespace VC { public class Wlp { - public static VCExpr Block(Block b, VCExpr N, VCContext ctxt) + public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) //modifies ctxt.*; { Contract.Requires(b != null); @@ -63,7 +63,7 @@ namespace VC { for (int i = b.Cmds.Count; --i >= 0; ) { - res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt); + res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars); } int id = b.UniqueId; @@ -87,7 +87,7 @@ namespace VC { /// /// Computes the wlp for an assert or assume command "cmd". /// - public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { + internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) { Contract.Requires(cmd != null); Contract.Requires(N != null); Contract.Requires(ctxt != null); @@ -190,7 +190,16 @@ namespace VC { } } } - return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N); + var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); + + var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); + if (aid != null && namedAssumeVars != null) + { + var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); + namedAssumeVars.Add(v); + expr = gen.ImpliesSimp(v, expr); + } + return gen.ImpliesSimp(expr, N); } else { Console.WriteLine(cmd.ToString()); Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl new file mode 100644 index 00000000..a955495a --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assume {:id "s0"} 0 < n; +} + +procedure test1(n: int) +{ + assume {:id "s0"} 0 < n; +} diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect new file mode 100644 index 00000000..9e420fa7 --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect @@ -0,0 +1,3 @@ +unnecessaryassumes0.bpl(7,4): Error: more than one statement with same id: s0 +unnecessaryassumes0.bpl(12,4): Error: more than one statement with same id: s0 +2 name resolution errors detected in unnecessaryassumes0.bpl diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl new file mode 100644 index 00000000..04226dfd --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assert 0 <= n; // verified under s0 +} + +procedure test1(n: int) +{ + assume 0 < n; + assume {:id "s1"} n == 3; + assert 0 <= n; // verified under true +} + +procedure test2(n: int) +{ + assume 0 < n; + assume {:id "s2"} n <= 42; + assume {:id "s3"} 42 <= n; + assert n == 42; // verified under s2 and s3 +} diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect new file mode 100644 index 00000000..dd04bb46 --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect @@ -0,0 +1,3 @@ +Necessary assume command(s): s0, s3, s2 + +Boogie program verifier finished with 3 verified, 0 errors -- cgit v1.2.3 From f19110ec25d4ee962558627150d22e4c8a26a2a0 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 20 Nov 2015 11:24:17 -0600 Subject: Add simplified may-unverified analysis and instrumentation. --- Source/Core/Absy.cs | 2 + Source/VCGeneration/VC.cs | 189 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 191 insertions(+) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8be4f24e..8a8558bf 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2241,6 +2241,7 @@ namespace Microsoft.Boogie { } public class Incarnation : LocalVariable { public int incarnationNumber; + public readonly Variable OriginalVariable; public Incarnation(Variable/*!*/ var, int i) : base( var.tok, @@ -2248,6 +2249,7 @@ namespace Microsoft.Boogie { ) { Contract.Requires(var != null); incarnationNumber = i; + OriginalVariable = var; } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 2762fc72..ad067c04 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2830,6 +2830,11 @@ namespace VC { mvInfo = new ModelViewInfo(program, impl); Convert2PassiveCmd(impl, mvInfo); + if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation")) + { + InstrumentWithMayUnverifiedConditions(impl, exitBlock); + } + #region Peep-hole optimizations if (CommandLineOptions.Clo.RemoveEmptyBlocks){ #region Get rid of empty blocks @@ -2865,6 +2870,190 @@ namespace VC { return gotoCmdOrigins; } + #region Simplified May-Unverified Analysis and Instrumentation + + static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock) + { + var q = new Queue(); + q.Enqueue(unifiedExitBlock); + var conditionOnBlockEntry = new Dictionary>(); + while (q.Any()) + { + var block = q.Dequeue(); + + if (conditionOnBlockEntry.ContainsKey(block)) + { + continue; + } + + var gotoCmd = block.TransferCmd as GotoCmd; + if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b))) + { + q.Enqueue(block); + continue; + } + + HashSet cond = new HashSet(); + if (gotoCmd != null) + { + var mayInstrs = new List(); + bool noInstr = true; + foreach (var succ in gotoCmd.labelTargets) + { + var c = conditionOnBlockEntry[succ]; + if (c != null) + { + mayInstrs.Add(succ); + } + else + { + noInstr = false; + } + cond = JoinVariableSets(cond, c); + } + if (!noInstr) + { + foreach (var instr in mayInstrs) + { + InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]); + } + } + } + + for (int i = block.Cmds.Count - 1; 0 <= i; i--) + { + var cmd = block.Cmds[i]; + if (cond == null) { break; } + + var assertCmd = cmd as AssertCmd; + if (assertCmd != null) + { + var litExpr = assertCmd.Expr as LiteralExpr; + if (litExpr != null && litExpr.IsTrue) + { + continue; + } + + HashSet vu = null; + if (assertCmd.VerifiedUnder == null) + { + vu = null; + } + else + { + HashSet vars; + if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars)) + { + vu = vars; + // TODO(wuestholz): Maybe drop the :verified_under attribute. + } + else + { + vu = null; + } + } + + if (vu == null) + { + InstrumentWithCondition(block, i + 1, cond); + } + + cond = JoinVariableSets(cond, vu); + } + } + + if (cond != null && block.Predecessors.Count == 0) + { + // TODO(wuestholz): Should we rather instrument each block? + InstrumentWithCondition(block, 0, cond); + } + + foreach (var pred in block.Predecessors) + { + q.Enqueue(pred); + } + + conditionOnBlockEntry[block] = cond; + } + } + + private static void InstrumentWithCondition(Block block, int idx, HashSet condition) + { + var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList()); + block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj))); + } + + static HashSet JoinVariableSets(HashSet c0, HashSet c1) + { + // We use the following lattice: + // - Top: null (i.e., true) + // - Bottom: new HashSet() (i.e., false) + // - Other Elements: new HashSet(...) (i.e., conjunctions of assumption variables) + + if (c0 == null || c1 == null) + { + return null; + } + var result = new HashSet(c0); + result.UnionWith(c1); + return result; + } + + static bool IsAssumptionVariableOrIncarnation(Variable v) + { + if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; } + var incar = v as Incarnation; + return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption"); + } + + static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet variables) + { + Contract.Requires(expr != null); + + variables = null; + var litExpr = expr as LiteralExpr; + if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue)) + { + if (litExpr.IsTrue) + { + variables = new HashSet(); + } + return true; + } + + var idExpr = expr as IdentifierExpr; + if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl)) + { + variables = new HashSet(); + variables.Add(idExpr.Decl); + return true; + } + + var andExpr = expr as NAryExpr; + if (andExpr != null) + { + var fun = andExpr.Fun as BinaryOperator; + if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null) + { + bool res = true; + variables = new HashSet(); + foreach (var op in andExpr.Args) + { + HashSet vars; + var r = IsConjunctionOfAssumptionVariables(op, out vars); + res &= r; + variables = JoinVariableSets(variables, vars); + if (!res) { break; } + } + return res; + } + } + + return false; + } + + #endregion + private static void HandleSelectiveChecking(Implementation impl) { if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") || -- cgit v1.2.3 From 502942a53a6db2b3a900d7570807216372d49ad0 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 3 Mar 2016 17:32:31 -0600 Subject: Improve support for optimization and identifying unnecessary assumes. --- Source/Provers/SMTLib/ProverInterface.cs | 34 +++++++++------------- Source/Provers/SMTLib/SMTLibLineariser.cs | 22 ++++++++++++-- Source/Provers/SMTLib/TypeDeclCollector.cs | 12 ++++++-- Source/VCExpr/VCExprAST.cs | 2 ++ Source/VCGeneration/Check.cs | 7 ++--- Source/VCGeneration/VC.cs | 12 ++++---- Source/VCGeneration/Wlp.cs | 17 +++++++---- .../unnecessaryassumes1.bpl.expect | 2 +- 8 files changed, 64 insertions(+), 44 deletions(-) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 7e98e8f8..432d7f3e 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -411,15 +411,6 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); - if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null) - { - foreach (var v in NamedAssumeVars) - { - SendThisVC(string.Format("(declare-fun {0} () Bool)", v)); - SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name)); - } - } - SendThisVC(vcString); SendOptimizationRequests(); @@ -1293,7 +1284,7 @@ namespace Microsoft.Boogie.SMTLib var reporter = handler as VC.VCGen.ErrorReporter; // TODO(wuestholz): Is the reporter ever null? - if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null) + if (CommandLineOptions.Clo.PrintNecessaryAssumes && ContainsNamedAssumes && result == Outcome.Valid && reporter != null) { SendThisVC("(get-unsat-core)"); var resp = Process.GetProverResponse(); @@ -1993,6 +1984,8 @@ namespace Microsoft.Boogie.SMTLib readonly IList OptimizationRequests = new List(); + bool ContainsNamedAssumes; + protected string VCExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); @@ -2032,8 +2025,8 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Collect(sortedExpr); FeedTypeDeclsToProver(); - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options)); - string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests); + AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, ref ContainsNamedAssumes)); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, ref ContainsNamedAssumes, OptimizationRequests); Contract.Assert(res != null); if (CommandLineOptions.Clo.Trace) @@ -2141,20 +2134,19 @@ namespace Microsoft.Boogie.SMTLib throw new NotImplementedException(); } - public override void Assert(VCExpr vc, bool polarity) + public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { OptimizationRequests.Clear(); - string a = ""; - if (polarity) - { - a = "(assert " + VCExpr2String(vc, 1) + ")"; + string assert = "assert"; + if (options.Solver == SolverKind.Z3 && isSoft) { + assert += "-soft"; } - else - { - a = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)"; + if (options.Solver == SolverKind.Z3 && isSoft) { + expr += " :weight " + weight; } AssertAxioms(); - SendThisVC(a); + SendThisVC("(" + assert + " " + expr + ")"); SendOptimizationRequests(); } diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index de8798b8..6df44c2f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,7 +34,7 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ref bool containsNamedAssumes, IList optReqs = null) { Contract.Requires(e != null); Contract.Requires(namer != null); @@ -44,6 +44,7 @@ namespace Microsoft.Boogie.SMTLib SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); + containsNamedAssumes |= lin.ContainsNamedAssumes; return cce.NonNull(sw.ToString()); } @@ -76,6 +77,12 @@ namespace Microsoft.Boogie.SMTLib readonly IList OptimizationRequests; + bool containsNamedAssumes; + public bool ContainsNamedAssumes + { + get { return containsNamedAssumes; } + } + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); @@ -270,7 +277,18 @@ namespace Microsoft.Boogie.SMTLib && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp))) { string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize"; - OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions))); + OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, ref containsNamedAssumes))); + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.SoftOp)) + { + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) + { + containsNamedAssumes = true; Linearise(node[1], options); return true; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 1c23c22f..72540c9c 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -210,7 +210,15 @@ void ObjectInvariant() if (node.Op is VCExprStoreOp) RegisterStore(node); else if (node.Op is VCExprSelectOp) RegisterSelect(node); - else { + else if (node.Op.Equals(VCExpressionGenerator.SoftOp)) { + var exprVar = node[0] as VCExprVar; + AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); + AddDeclaration(string.Format("(assert-soft {0} :weight 1)", exprVar.Name)); + } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) { + var exprVar = node[0] as VCExprVar; + AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); + AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); + } else { VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; if (op != null && !(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) && @@ -255,7 +263,7 @@ void ObjectInvariant() RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - if (!printedName.StartsWith("assume$$")) + if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$"))) { AddDeclaration(decl); } diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 2fbb102c..a58cfb7f 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -343,6 +343,8 @@ namespace Microsoft.Boogie { 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 SoftOp = new VCExprCustomOp("soft##dummy", 2, Type.Bool); public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 8c1ae407..ae4d158a 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -346,7 +346,7 @@ namespace Microsoft.Boogie { } } - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList namedAssumeVars = null) { + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); @@ -360,7 +360,6 @@ namespace Microsoft.Boogie { thmProver.Reset(gen); SetTimeout(); proverStart = DateTime.UtcNow; - thmProver.NamedAssumeVars = namedAssumeVars; thmProver.BeginCheck(descriptiveName, vc, handler); // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy @@ -388,8 +387,6 @@ namespace Microsoft.Boogie { public abstract class ProverInterface { - public IList NamedAssumeVars; - public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) { Contract.Requires(prog != null); @@ -546,7 +543,7 @@ namespace Microsoft.Boogie { } // (assert vc) - public virtual void Assert(VCExpr vc, bool polarity) + public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { throw new NotImplementedException(); } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index ad067c04..6e43e917 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1386,8 +1386,7 @@ namespace VC { var exprGen = ctx.ExprGen; VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - var namedAssumeVars = new List(); - VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars); + VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context); Contract.Assert(vc != null); if (!CommandLineOptions.Clo.UseLabels) @@ -1415,7 +1414,7 @@ namespace VC { string desc = cce.NonNull(impl.Name); if (no >= 0) desc += "_split" + no; - checker.BeginCheck(desc, vc, reporter, namedAssumeVars); + checker.BeginCheck(desc, vc, reporter); } private void SoundnessCheck(HashSet/*!*/>/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { @@ -1568,8 +1567,7 @@ namespace VC { } break; case CommandLineOptions.VCVariety.DagIterative: - // TODO(wuestholz): Support named assume statements not just for this encoding. - vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars); + vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount); break; case CommandLineOptions.VCVariety.Doomed: vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount); @@ -3393,7 +3391,7 @@ namespace VC { Dictionary label2absy, ProverContext proverCtxt, out int assertionCount, - bool isPositiveContext = true, IList namedAssumeVars = null) + bool isPositiveContext = true) { Contract.Requires(blocks != null); Contract.Requires(proverCtxt != null); @@ -3453,7 +3451,7 @@ namespace VC { } VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext); - VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars); + VCExpr vc = Wlp.Block(block, SuccCorrect, context); assertionCount += context.AssertionCount; VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 508a1400..07db709d 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -48,7 +48,7 @@ namespace VC { public class Wlp { - public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) + public static VCExpr Block(Block b, VCExpr N, VCContext ctxt) //modifies ctxt.*; { Contract.Requires(b != null); @@ -63,7 +63,7 @@ namespace VC { for (int i = b.Cmds.Count; --i >= 0; ) { - res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars); + res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt); } int id = b.UniqueId; @@ -87,7 +87,7 @@ namespace VC { /// /// Computes the wlp for an assert or assume command "cmd". /// - internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) { + internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { Contract.Requires(cmd != null); Contract.Requires(N != null); Contract.Requires(ctxt != null); @@ -193,11 +193,16 @@ namespace VC { var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null) + if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null) { var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); - namedAssumeVars.Add(v); - expr = gen.ImpliesSimp(v, expr); + expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); + } + var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); + if (soft && aid != null) + { + var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool); + expr = gen.Function(VCExpressionGenerator.SoftOp, v, gen.ImpliesSimp(v, expr)); } return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N)); } else { diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect index dd04bb46..0d3aeca2 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect @@ -1,3 +1,3 @@ -Necessary assume command(s): s0, s3, s2 +Necessary assume command(s): s0, s2, s3 Boogie program verifier finished with 3 verified, 0 errors -- cgit v1.2.3