summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/Absy.cs7
-rw-r--r--Source/Core/AbsyCmd.cs7
-rw-r--r--Source/ExecutionEngine/VerificationResultCache.cs90
-rw-r--r--Test/snapshots/runtest.snapshot.expect76
4 files changed, 147 insertions, 33 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9d446ebd..a5955c7a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1250,6 +1250,13 @@ namespace Microsoft.Boogie {
return visitor.VisitProgram(this);
}
+ int extractedFunctionCount;
+ public string FreshExtractedFunctionName()
+ {
+ var c = System.Threading.Interlocked.Increment(ref extractedFunctionCount);
+ return string.Format("##extracted_function##{0}", c);
+ }
+
private int invariantGenerationCounter = 0;
public Constant MakeExistentialBoolean(int StageId) {
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index d143e480..046d97b9 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2592,10 +2592,17 @@ namespace Microsoft.Boogie {
if (result != null)
{
result = LiteralExpr.And(result, c);
+ result.Type = Type.Bool;
+ var nAryExpr = result as NAryExpr;
+ if (nAryExpr != null)
+ {
+ nAryExpr.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ }
}
else
{
result = c;
+ result.Type = Type.Bool;
}
}
return result;
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index d8a446a7..86a614e9 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -188,6 +188,7 @@ namespace Microsoft.Boogie
var before = new List<Cmd>();
var beforePrecondtionCheck = new List<Cmd>();
var after = new List<Cmd>();
+ var axioms = new List<Axiom>();
Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
// TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.
var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);
@@ -198,7 +199,7 @@ namespace Microsoft.Boogie
var precond = node.CheckedPrecondition(oldProc, Program);
if (precond != null)
{
- var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+ var assume = new AssumeCmd(node.tok, FunctionExtractor.Extract(precond, Program, axioms), new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
beforePrecondtionCheck.Add(assume);
}
@@ -211,7 +212,10 @@ namespace Microsoft.Boogie
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));
var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);
before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));
- eqs.Add(LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl)));
+ var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl));
+ eq.Type = Type.Bool;
+ eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ eqs.Add(eq);
}
var mods = node.ModifiedBefore(oldProc);
@@ -237,7 +241,8 @@ namespace Microsoft.Boogie
node.AssignedAssumptionVariable = lv;
currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
- var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
+ // TODO(wuestholz): Try to extract functions for each clause.
+ var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), FunctionExtractor.Extract(assumedExpr, Program, axioms));
var assumed = new AssignCmd(node.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
after.Add(assumed);
}
@@ -249,6 +254,12 @@ namespace Microsoft.Boogie
{
var loc = node.tok != null && node.tok != Token.NoToken ? string.Format("{0}({1},{2})", node.tok.filename, node.tok.line, node.tok.col) : "<unknown location>";
Console.Out.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.Name, currentImplementation.Name, loc);
+ foreach (var a in axioms)
+ {
+ Console.Out.Write(" >>> added axiom: ");
+ a.Expr.Emit(tokTxtWr);
+ Console.Out.WriteLine();
+ }
foreach (var b in before)
{
Console.Out.Write(" >>> added before: ");
@@ -273,6 +284,79 @@ namespace Microsoft.Boogie
}
+ sealed class FunctionExtractor : StandardVisitor
+ {
+ readonly Dictionary<Variable, BoundVariable> Substitutions = new Dictionary<Variable, BoundVariable>();
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ if (node.Decl == null || !(node.Decl is LocalVariable || node.Decl is Formal))
+ {
+ return node;
+ }
+ else
+ {
+ BoundVariable boundVar;
+ if (!Substitutions.TryGetValue(node.Decl, out boundVar))
+ {
+ boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, node.Name, node.Type));
+ Substitutions[node.Decl] = boundVar;
+ }
+ return new IdentifierExpr(node.tok, boundVar);
+ }
+ }
+
+ public static Expr Extract(Expr expr, Program program, List<Axiom> axioms)
+ {
+ Contract.Requires(expr != null && program != null && !program.TopLevelDeclarationsAreFrozen && axioms != null);
+
+ if (expr is LiteralExpr)
+ {
+ return expr;
+ }
+
+ var extractor = new FunctionExtractor();
+
+ var body = extractor.VisitExpr(expr);
+
+ var name = program.FreshExtractedFunctionName();
+ var originalVars = extractor.Substitutions.Keys.ToList();
+ var formalInArgs = originalVars.Select(v => new Formal(Token.NoToken, new TypedIdent(Token.NoToken, extractor.Substitutions[v].Name, extractor.Substitutions[v].TypedIdent.Type), true)).ToList<Variable>();
+ var formalOutArg = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, name + "$result$", expr.Type), false);
+ var func = new Function(Token.NoToken, name, formalInArgs, formalOutArg);
+ func.AddAttribute("never_pattern");
+
+ var boundVars = originalVars.Select(k => extractor.Substitutions[k]);
+ var axiomCall = new NAryExpr(Token.NoToken, new FunctionCall(func), boundVars.Select(b => new IdentifierExpr(Token.NoToken, b)).ToList<Expr>());
+ axiomCall.Type = expr.Type;
+ axiomCall.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ var eq = LiteralExpr.Eq(axiomCall, body);
+ eq.Type = body.Type;
+ eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ if (0 < formalInArgs.Count)
+ {
+ body = new ForallExpr(Token.NoToken, boundVars.ToList<Variable>(), new Trigger(Token.NoToken, true, new List<Expr> { axiomCall }), eq);
+ body.Type = Type.Bool;
+ }
+ else
+ {
+ body = eq;
+ }
+
+ var axiom = new Axiom(Token.NoToken, body);
+ func.DefinitionAxiom = axiom;
+ program.AddTopLevelDeclaration(func);
+ program.AddTopLevelDeclaration(axiom);
+ axioms.Add(axiom);
+
+ var call = new NAryExpr(Token.NoToken, new FunctionCall(func), originalVars.Select(v => new IdentifierExpr(Token.NoToken, v)).ToList<Expr>());
+ call.Type = expr.Type;
+ call.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ return call;
+ }
+ }
+
+
sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor
{
Axiom currentAxiom;
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 7f912427..c0aced32 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -66,8 +66,9 @@ Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):
- >>> added before precondition check: assume {:precondition_previous_snapshot} F0();
-Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} F0();
+ >>> added axiom: ##extracted_function##1() == F0()
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
+Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();
>>> MarkAsFullyVerified
@@ -112,9 +113,10 @@ Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):
+ >>> added axiom: (forall y##old##0: int :: { ##extracted_function##1(y##old##0) } ##extracted_function##1(y##old##0) == (y##old##0 == y))
>>> added before: y##old##0 := y;
- >>> added after: a##post##0 := a##post##0 && y##old##0 == y;
-Processing command (at <unknown location>) a##post##0 := a##post##0 && y##old##0 == y;
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0);
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;
>>> MarkAsPartiallyVerified
@@ -126,9 +128,10 @@ Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):
+ >>> added axiom: ##extracted_function##1() == (y < z)
>>> added before: y##old##0 := y;
- >>> added after: a##post##0 := a##post##0 && y < z;
-Processing command (at <unknown location>) a##post##0 := a##post##0 && y < z;
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1();
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;
>>> MarkAsPartiallyVerified
@@ -141,13 +144,15 @@ Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
- >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
- >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r;
-Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
+ >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+ >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
>>> MarkAsFullyVerified
Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
>>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && 0 < call1formal#AT#r;
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;
>>> MarkAsPartiallyVerified
@@ -162,13 +167,15 @@ Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
- >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n && true;
- >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r && true;
-Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n && true;
+ >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))
+ >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
>>> MarkAsFullyVerified
Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
>>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && 0 < call1formal#AT#r && true;
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;
>>> MarkAsPartiallyVerified
@@ -181,13 +188,15 @@ Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
- >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
- >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r;
-Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
+ >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+ >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
>>> MarkAsFullyVerified
Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
>>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && 0 < call1formal#AT#r;
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;
>>> MarkAsPartiallyVerified
@@ -202,9 +211,11 @@ Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might
Boogie program verifier finished with 0 verified, 1 error
Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
- >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
- >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r;
-Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
+ >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+ >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
>>> DropAssume
Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
>>> RecycleError
@@ -241,8 +252,9 @@ Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):
- >>> added after: a##post##0 := a##post##0 && F() && G();
-Processing command (at <unknown location>) a##post##0 := a##post##0 && F() && G();
+ >>> added axiom: ##extracted_function##1() == (F() && G())
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1();
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots14.v1.bpl(7,5)) assert false;
>>> MarkAsPartiallyVerified
@@ -337,8 +349,9 @@ Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 1 error
Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):
- >>> added before precondition check: assume {:precondition_previous_snapshot} 2 == 2;
-Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} 2 == 2;
+ >>> added axiom: ##extracted_function##1() == (2 == 2)
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
+Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
>>> MarkAsFullyVerified
Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;
>>> MarkAsFullyVerified
@@ -357,7 +370,8 @@ Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 1 error
Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):
- >>> added after: a##post##0 := a##post##0 && 0 != 0;
+ >>> added axiom: ##extracted_function##1() == (0 != 0)
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;
>>> MarkAsPartiallyVerified
Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;
@@ -552,8 +566,9 @@ Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):
- >>> added after: a##post##0 := a##post##0 && call0old#AT#g < g;
-Processing command (at <unknown location>) a##post##0 := a##post##0 && call0old#AT#g < g;
+ >>> added axiom: (forall call0old#AT#g: int :: { ##extracted_function##1(call0old#AT#g) } ##extracted_function##1(call0old#AT#g) == (call0old#AT#g < g))
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g);
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;
>>> MarkAsPartiallyVerified
@@ -565,9 +580,10 @@ Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g;
Boogie program verifier finished with 1 verified, 0 errors
Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):
+ >>> added axiom: (forall g##old##0: int :: { ##extracted_function##1(g##old##0) } ##extracted_function##1(g##old##0) == (g##old##0 < g))
>>> added before: g##old##0 := g;
- >>> added after: a##post##0 := a##post##0 && g##old##0 < g;
-Processing command (at <unknown location>) a##post##0 := a##post##0 && g##old##0 < g;
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0);
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;
>>> MarkAsPartiallyVerified
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 12:49:15 +0000