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