summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/AbsyCmd.cs6
-rw-r--r--Source/Core/AbsyQuant.cs17
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs21
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs17
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs2
-rw-r--r--Source/VCExpr/VCExprAST.cs3
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs12
-rw-r--r--Source/VCGeneration/Wlp.cs21
-rw-r--r--Test/optimization/Optimization0.bpl86
-rw-r--r--Test/optimization/Optimization0.bpl.expect182
-rw-r--r--Test/optimization/Optimization1.bpl32
-rw-r--r--Test/optimization/Optimization1.bpl.expect5
-rw-r--r--Test/optimization/Optimization2.bpl12
-rw-r--r--Test/optimization/Optimization2.bpl.expect3
-rw-r--r--Test/optimization/lit.local.cfg3
15 files changed, 410 insertions, 12 deletions
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<string> OptimizationRequests = new List<string>();
+
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<bool, LineariserOptions/*!*/>
{
- public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts)
+ public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
{
Contract.Requires(e != null);
Contract.Requires(namer != null);
Contract.Ensures(Contract.Result<string>() != 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<string> OptimizationRequests;
+
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> 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<bool, LineariserOptions/*!*/>(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<VCExprOp>() != 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 01:53:28 +0000