From a51f4e6cba57b6711e36ef482f4e320c9cf0542f Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 18 Nov 2015 15:46:24 -0600 Subject: Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). --- Source/Core/AbsyCmd.cs | 6 + Source/Core/AbsyQuant.cs | 17 ++- Source/Provers/SMTLib/ProverInterface.cs | 21 +++- Source/Provers/SMTLib/SMTLibLineariser.cs | 17 ++- Source/Provers/SMTLib/SMTLibNamer.cs | 2 +- Source/VCExpr/VCExprAST.cs | 3 + Source/VCGeneration/ConditionGeneration.cs | 12 ++ Source/VCGeneration/Wlp.cs | 21 +++- Test/optimization/Optimization0.bpl | 86 ++++++++++++++ Test/optimization/Optimization0.bpl.expect | 182 +++++++++++++++++++++++++++++ Test/optimization/Optimization1.bpl | 32 +++++ Test/optimization/Optimization1.bpl.expect | 5 + Test/optimization/Optimization2.bpl | 12 ++ Test/optimization/Optimization2.bpl.expect | 3 + Test/optimization/lit.local.cfg | 3 + 15 files changed, 410 insertions(+), 12 deletions(-) create mode 100644 Test/optimization/Optimization0.bpl create mode 100644 Test/optimization/Optimization0.bpl.expect create mode 100644 Test/optimization/Optimization1.bpl create mode 100644 Test/optimization/Optimization1.bpl.expect create mode 100644 Test/optimization/Optimization2.bpl create mode 100644 Test/optimization/Optimization2.bpl.expect create mode 100644 Test/optimization/lit.local.cfg diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index c33f0743..2e33e1dd 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -3218,8 +3218,14 @@ namespace Microsoft.Boogie { this.Expr.Emit(stream); stream.WriteLine(";"); } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + ResolveAttributes(Attributes, rc); + base.Resolve(rc); + } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); + TypecheckAttributes(Attributes, tc); Expr.Typecheck(tc); Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition if (!Expr.Type.Unify(Type.Bool)) { diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 9f94490b..39f18657 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -338,6 +338,12 @@ namespace Microsoft.Boogie { public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); + + if ((Key == "minimize" || Key == "maximize") && Params.Count != 1) + { + rc.Error(this, "attributes :minimize and :maximize accept only one argument"); + } + foreach (object p in Params) { if (p is Expr) { ((Expr)p).Resolve(rc); @@ -348,8 +354,15 @@ namespace Microsoft.Boogie { public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); foreach (object p in Params) { - if (p is Expr) { - ((Expr)p).Typecheck(tc); + var expr = p as Expr; + if (expr != null) { + expr.Typecheck(tc); + } + if ((Key == "minimize" || Key == "maximize") + && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv))) + { + tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv"); + break; } } } diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index cb8442e5..ca530da2 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -401,6 +401,8 @@ namespace Microsoft.Boogie.SMTLib PrepareCommon(); + OptimizationRequests.Clear(); + string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; FlushAxioms(); @@ -418,6 +420,15 @@ namespace Microsoft.Boogie.SMTLib } SendThisVC(vcString); + + if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count) + { + foreach (var r in OptimizationRequests) + { + SendThisVC(r); + } + } + FlushLogFile(); if (Process != null) { @@ -1838,6 +1849,7 @@ namespace Microsoft.Boogie.SMTLib private Model GetErrorModel() { if (!options.ExpectingModel()) return null; + SendThisVC("(get-model)"); Process.Ping(); Model theModel = null; @@ -1932,6 +1944,9 @@ namespace Microsoft.Boogie.SMTLib result = Outcome.Invalid; wasUnknown = true; break; + case "objectives": + // We ignore this. + break; default: HandleProverError("Unexpected prover response: " + resp.ToString()); break; @@ -1970,6 +1985,8 @@ namespace Microsoft.Boogie.SMTLib return result; } + readonly IList OptimizationRequests = new List(); + protected string VCExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); @@ -2009,10 +2026,8 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Collect(sortedExpr); FeedTypeDeclsToProver(); - - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options)); - string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests); Contract.Assert(res != null); if (CommandLineOptions.Clo.Trace) diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index dcf95bd2..de8798b8 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) { Contract.Requires(e != null); Contract.Requires(namer != null); Contract.Ensures(Contract.Result() != null); StringWriter sw = new StringWriter(); - SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts); + SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); return cce.NonNull(sw.ToString()); @@ -74,12 +74,15 @@ namespace Microsoft.Boogie.SMTLib internal int UnderQuantifier = 0; internal readonly SMTLibProverOptions ProverOptions; - public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts) + readonly IList OptimizationRequests; + + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); this.wr = wr; this.Namer = namer; this.ProverOptions = opts; + this.OptimizationRequests = optReqs; } public void Linearise(VCExpr expr, LineariserOptions options) @@ -263,6 +266,14 @@ namespace Microsoft.Boogie.SMTLib } return true; } + if (OptimizationRequests != null + && (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))); + Linearise(node[1], options); + return true; + } return node.Accept(OpLineariser, options); } diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 900bdbcc..f1179159 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie.SMTLib "flet", "implies", "!=", "if_then_else", // Z3 extensions "lblneg", "lblpos", "lbl-lit", - "if", "&&", "||", "equals", "equiv", "bool", + "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize", // Boogie-defined "real_pow", "UOrdering2", "UOrdering3", // Floating point (final draft SMTLIB-v2.5) diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 0a9ba6b3..2a06447e 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -341,6 +341,9 @@ namespace Microsoft.Boogie { public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool); + public static readonly VCExprOp MinimizeOp = new VCExprNAryOp(2, Type.Bool); + public static readonly VCExprOp MaximizeOp = new VCExprNAryOp(2, Type.Bool); + public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ae0a1147..5971d6f8 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1539,6 +1539,18 @@ namespace VC { PredicateCmd pc = (PredicateCmd)c.Clone(); Contract.Assert(pc != null); + QKeyValue current = pc.Attributes; + while (current != null) + { + if (current.Key == "minimize" || current.Key == "maximize") { + Contract.Assume(current.Params.Count == 1); + var param = current.Params[0] as Expr; + Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv)); + current.ClearParams(); + current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param)); + } + current = current.Next; + } Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr); if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) { string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState"); diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 74b77188..741ed723 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -186,7 +186,7 @@ namespace VC { if (naryExpr.Fun is FunctionCall) { int id = ac.UniqueId; ctxt.Label2absy[id] = ac; - return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N); + return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N)); } } } @@ -199,13 +199,28 @@ namespace VC { namedAssumeVars.Add(v); expr = gen.ImpliesSimp(v, expr); } - return gen.ImpliesSimp(expr, N); + return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N)); } else { Console.WriteLine(cmd.ToString()); Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command } } - + + private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr) + { + var min = QKeyValue.FindExprAttribute(attrs, "minimize"); + if (min != null) + { + expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr); + } + var max = QKeyValue.FindExprAttribute(attrs, "maximize"); + if (max != null) + { + expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr); + } + return expr; + } + public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) { Contract.Requires(ac != null); int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1); diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl new file mode 100644 index 00000000..c704c855 --- /dev/null +++ b/Test/optimization/Optimization0.bpl @@ -0,0 +1,86 @@ +// RUN: %boogie /doNotUseLabels /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function may_fail(f: int) : bool; + +procedure test0() +{ + var x: int; + + havoc x; + assume 42 < x; + assume {:minimize x} true; + assert may_fail(x); +} + +procedure test1() +{ + var x: int; + + x := 24; + if (*) { + x := 42; + } + assume {:minimize x} true; + assert may_fail(x); +} + +procedure test2() +{ + var x: int; + + x := 1; + while (*) { + x := x + 1; + } + assume {:minimize x} true; + assert x < 10; +} + +procedure test3() +{ + var x: int; + + havoc x; + assume x < 42; + assume {:maximize x} true; + assert may_fail(x); +} + +procedure test4() +{ + var x: int; + + x := 24; + if (*) { + x := 42; + } + assume {:maximize x} true; + assert may_fail(x); +} + +procedure test5() +{ + var x: int; + + x := 1; + while (*) { + x := x - 1; + } + assume {:maximize x} true; + assert x < 1; +} + +procedure test6() +{ + var x: int; + + x := 1; + if (*) { + x := 2; + } + assume {:maximize x} true; + assert may_fail(x); +} + +// TODO(wuestholz): Make this work without the /doNotUseLabels flag. diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect new file mode 100644 index 00000000..d2f9b606 --- /dev/null +++ b/Test/optimization/Optimization0.bpl.expect @@ -0,0 +1,182 @@ +*** MODEL +%lbl%@280 -> false +%lbl%+260 -> true +%lbl%+39 -> true +x@0 -> 43 +ControlFlow -> { + 0 0 -> 260 + 0 260 -> 39 + 0 39 -> (- 280) + else -> 260 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 43 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(10,5): anon0 +*** MODEL +%lbl%@328 -> false +%lbl%+306 -> true +%lbl%+66 -> true +%lbl%+68 -> true +x@0@@0 -> 24 +ControlFlow -> { + 0 0 -> 306 + 0 306 -> 66 + 0 68 -> (- 328) + 0 66 -> 68 + else -> 306 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 24 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(25,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(20,7): anon0 + Optimization0.bpl(21,5): anon3_Else + Optimization0.bpl(24,5): anon2 +*** MODEL +%lbl%@360 -> false +%lbl%+342 -> true +%lbl%+95 -> true +%lbl%+99 -> true +x@0@@1 -> 10 +ControlFlow -> { + 0 0 -> 342 + 0 342 -> 95 + 0 95 -> 99 + 0 99 -> (- 360) + else -> 342 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization0.bpl(37,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(32,7): anon0 + Optimization0.bpl(33,5): anon3_LoopHead + Optimization0.bpl(33,5): anon3_LoopDone +*** MODEL +%lbl%@393 -> false +%lbl%+122 -> true +%lbl%+382 -> true +x@0@@2 -> 41 +ControlFlow -> { + 0 0 -> 382 + 0 382 -> 122 + 0 122 -> (- 393) + else -> 382 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 41 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(44,5): anon0 +*** MODEL +%lbl%@421 -> false +%lbl%+147 -> true +%lbl%+151 -> true +%lbl%+399 -> true +x@0@@3 -> 42 +ControlFlow -> { + 0 0 -> 399 + 0 399 -> 147 + 0 147 -> 151 + 0 151 -> (- 421) + else -> 399 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 42 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(59,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(54,7): anon0 + Optimization0.bpl(56,11): anon3_Then + Optimization0.bpl(58,5): anon2 +*** MODEL +%lbl%@453 -> false +%lbl%+178 -> true +%lbl%+182 -> true +%lbl%+435 -> true +x@0@@4 -> 1 +ControlFlow -> { + 0 0 -> 435 + 0 435 -> 178 + 0 178 -> 182 + 0 182 -> (- 453) + else -> 435 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization0.bpl(71,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(66,7): anon0 + Optimization0.bpl(67,5): anon3_LoopHead + Optimization0.bpl(67,5): anon3_LoopDone +*** MODEL +%lbl%@497 -> false +%lbl%+209 -> true +%lbl%+213 -> true +%lbl%+475 -> true +x@0@@5 -> 2 +ControlFlow -> { + 0 0 -> 475 + 0 475 -> 209 + 0 209 -> 213 + 0 213 -> (- 497) + else -> 475 +} +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 2 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(83,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(78,7): anon0 + Optimization0.bpl(80,11): anon3_Then + Optimization0.bpl(82,5): anon2 + +Boogie program verifier finished with 0 verified, 7 errors diff --git a/Test/optimization/Optimization1.bpl b/Test/optimization/Optimization1.bpl new file mode 100644 index 00000000..60df1edd --- /dev/null +++ b/Test/optimization/Optimization1.bpl @@ -0,0 +1,32 @@ +// RUN: %boogie /noVerify /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:minimize} true; +} + +procedure test1(n: int) +{ + assume {:maximize} true; +} + +procedure test2(n: int) +{ + assume {:minimize n, n} true; +} + +procedure test3(n: int) +{ + assume {:maximize n, n} true; +} + +procedure test4(n: int) +{ + assume {:minimize true} true; +} + +procedure test5(n: int) +{ + assume {:maximize true} true; +} diff --git a/Test/optimization/Optimization1.bpl.expect b/Test/optimization/Optimization1.bpl.expect new file mode 100644 index 00000000..d8508807 --- /dev/null +++ b/Test/optimization/Optimization1.bpl.expect @@ -0,0 +1,5 @@ +Optimization1.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(16,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(21,11): Error: attributes :minimize and :maximize accept only one argument +4 name resolution errors detected in Optimization1.bpl diff --git a/Test/optimization/Optimization2.bpl b/Test/optimization/Optimization2.bpl new file mode 100644 index 00000000..7d80d735 --- /dev/null +++ b/Test/optimization/Optimization2.bpl @@ -0,0 +1,12 @@ +// RUN: %boogie /noVerify /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:minimize true} true; +} + +procedure test1(n: int) +{ + assume {:maximize true} true; +} diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect new file mode 100644 index 00000000..cab2fd3d --- /dev/null +++ b/Test/optimization/Optimization2.bpl.expect @@ -0,0 +1,3 @@ +Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +2 type checking errors detected in Optimization2.bpl diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg new file mode 100644 index 00000000..158a1e4d --- /dev/null +++ b/Test/optimization/lit.local.cfg @@ -0,0 +1,3 @@ +# Do not run tests in this directory and below +config.unsupported = True +# TODO(wuestholz): Enable these tests once we can rely on Z3 4.4.2 or higher. -- cgit v1.2.3