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 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