diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 287 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 11 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 5 |
3 files changed, 239 insertions, 64 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 60a54346..aca9d3f8 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -84,6 +84,7 @@ namespace Microsoft.Boogie { public string OriginalRequestId;
public string RequestId;
public abstract byte[] Checksum { get; }
+ public byte[] SugaredCmdChecksum;
public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
@@ -420,7 +421,7 @@ namespace Microsoft.Boogie { }
- public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
+ public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null)
: base(trace, model, mvInfo, context) {
Contract.Requires(!failingRequires.Free);
Contract.Requires(trace != null);
@@ -429,20 +430,23 @@ namespace Microsoft.Boogie { Contract.Requires(failingRequires != null);
this.FailingCall = failingCall;
this.FailingRequires = failingRequires;
+ this.checksum = checksum;
+ this.SugaredCmdChecksum = failingCall.Checksum;
}
public override int GetLocation() {
return FailingCall.tok.line * 1000 + FailingCall.tok.col;
}
+ byte[] checksum;
public override byte[] Checksum
{
- get { return FailingCall.Checksum; }
+ get { return checksum; }
}
public override Counterexample Clone()
{
- var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context);
+ var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum);
ret.calleeCounterexamples = calleeCounterexamples;
return ret;
}
@@ -1298,7 +1302,7 @@ namespace VC { Dictionary<Variable, Expr> preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement
- protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, byte[] currentChecksum = null) {
+ protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, MutableVariableCollector variableCollector, byte[] currentChecksum = null) {
Contract.Requires(b != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(mvInfo != null);
@@ -1308,7 +1312,8 @@ namespace VC { List<Cmd> passiveCmds = new List<Cmd>();
foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction
- ChecksumHelper.ComputeChecksums(c, currentImplementation, currentChecksum);
+ ChecksumHelper.ComputeChecksums(c, currentImplementation, variableCollector.UsedVariables, currentChecksum);
+ variableCollector.Visit(c);
currentChecksum = c.Checksum;
TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, b);
}
@@ -1330,7 +1335,32 @@ namespace VC { currentImplementation = impl;
currentTemporaryVariableForAssertions = null;
+
+ var start = DateTime.UtcNow;
+
Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
+
+ var end = DateTime.UtcNow;
+
+ if (3 <= CommandLineOptions.Clo.TraceCaching)
+ {
+ Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);
+ }
+
+ if (2 <= CommandLineOptions.Clo.TraceCaching)
+ {
+ using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
+ {
+ var pd = CommandLineOptions.Clo.PrintDesugarings;
+ var pu = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintDesugarings = true;
+ CommandLineOptions.Clo.PrintUnstructured = 1;
+ impl.Emit(tokTxtWr, 0);
+ CommandLineOptions.Clo.PrintDesugarings = pd;
+ CommandLineOptions.Clo.PrintUnstructured = pu;
+ }
+ }
+
currentTemporaryVariableForAssertions = null;
currentImplementation = null;
@@ -1383,6 +1413,7 @@ namespace VC { Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation = new Dictionary<Block, Dictionary<Variable, Expr>>();
Block exitBlock = null;
Dictionary<Variable, Expr> exitIncarnationMap = null;
+ var variableCollectors = new Dictionary<Block, MutableVariableCollector>();
foreach (Block b in sortedNodes) {
Contract.Assert(b != null);
Contract.Assert(!block2Incarnation.ContainsKey(b));
@@ -1394,6 +1425,8 @@ namespace VC { // Decrement the succCount field in each predecessor. Once the field reaches zero in any block,
// all its successors have been passified. Consequently, its entry in block2Incarnation can be removed.
byte[] currentChecksum = null;
+ var mvc = new MutableVariableCollector();
+ variableCollectors[b] = mvc;
foreach (Block p in b.Predecessors) {
p.succCount--;
if (p.Checksum != null)
@@ -1401,6 +1434,7 @@ namespace VC { // Compute the checksum based on the checksums of the predecessor. The order should not matter.
currentChecksum = ChecksumHelper.CombineChecksums(p.Checksum, currentChecksum, true);
}
+ mvc.AddUsedVariables(variableCollectors[p].UsedVariables);
if (p.succCount == 0)
block2Incarnation.Remove(p);
}
@@ -1417,11 +1451,13 @@ namespace VC { }
#endregion Each block's map needs to be available to successor blocks
- TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, currentChecksum);
+ TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, mvc, currentChecksum);
exitBlock = b;
exitIncarnationMap = incarnationMap;
}
+ variableCollectors.Clear();
+
// Verify that exitBlock is indeed the unique exit block
Contract.Assert(exitBlock != null);
Contract.Assert(exitBlock.TransferCmd is ReturnCmd);
@@ -1445,6 +1481,36 @@ namespace VC { return Substituter.SubstitutionFromHashtable(oldFrameMap);
}
+ public enum CachingAction : byte
+ {
+ DoNothingToAssert,
+ MarkAsPartiallyVerified,
+ MarkAsFullyVerified,
+ RecycleError,
+ AssumeNegationOfAssumptionVariable,
+ DropAssume
+ }
+
+ public long[] CachingActionCounts;
+
+ void TraceCachingAction(Cmd cmd, CachingAction action)
+ {
+ if (1 <= CommandLineOptions.Clo.TraceCaching)
+ {
+ using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
+ {
+ var loc = cmd.tok != null && cmd.tok != Token.NoToken ? string.Format("{0}({1},{2})", cmd.tok.filename, cmd.tok.line, cmd.tok.col) : "<unknown location>";
+ Console.Write("Processing command (at {0}) ", loc);
+ cmd.Emit(tokTxtWr, 0);
+ Console.Out.WriteLine(" >>> {0}", action);
+ }
+ if (CachingActionCounts != null)
+ {
+ Interlocked.Increment(ref CachingActionCounts[(int)action]);
+ }
+ }
+ }
+
/// <summary>
/// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc
/// Meanwhile, record any information needed to later reconstruct a model view.
@@ -1475,73 +1541,160 @@ namespace VC { }
}
Contract.Assert(copy != null);
- var isAssumePre = false;
+ var dropCmd = false;
+ var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();
+ var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();
+ var checksum = pc.Checksum;
if (pc is AssertCmd) {
var ac = (AssertCmd)pc;
ac.OrigExpr = ac.Expr;
Contract.Assert(ac.IncarnationMap == null);
ac.IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));
- if (currentImplementation != null
- && ((currentImplementation.NoErrorsInCachedSnapshot
- && currentImplementation.InjectedAssumptionVariables != null
- && 2 <= currentImplementation.InjectedAssumptionVariables.Count)
- || (currentImplementation.AnyErrorsInCachedSnapshot
- && currentImplementation.InjectedAssumptionVariables != null
- && currentImplementation.InjectedAssumptionVariables.Any()
- && ac.Checksum != null
- && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
- && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum))))
+ var subsumption = Wlp.Subsumption(ac);
+ var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;
+ if (relevantDoomedAssumpVars.Any())
{
- // Bind the assertion expression to a local variable.
- var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
- var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
- incarnationMap[incarnation] = identExpr;
- ac.IncarnationMap[incarnation] = identExpr;
- passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
- copy = identExpr;
- var expr = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy);
- passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
}
else if (currentImplementation != null
- && ac.Checksum != null
- && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
- && currentImplementation.ErrorChecksumToCachedError != null
- && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
- && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
+ && currentImplementation.HasCachedSnapshot
+ && checksum != null
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
+ && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
{
- // Turn it into an assume statement.
- pc = new AssumeCmd(ac.tok, copy);
- pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+ if (!currentImplementation.AnyErrorsInCachedSnapshot
+ && currentImplementation.InjectedAssumptionVariables.Count == 1
+ && relevantAssumpVars.Count == 1)
+ {
+ TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
+ }
+ else
+ {
+ bool isTrue;
+ var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
+ if (!isTrue && alwaysUseSubsumption)
+ {
+ TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
+ var litExpr = ac.Expr as LiteralExpr;
+ if (litExpr == null || !litExpr.IsTrue)
+ {
+ // Bind the assertion expression to a local variable.
+ var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
+ var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
+ incarnationMap[incarnation] = identExpr;
+ ac.IncarnationMap[incarnation] = identExpr;
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
+ copy = identExpr;
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
+ }
+ else
+ {
+ dropCmd = true;
+ }
+ }
+ else if (isTrue)
+ {
+ if (alwaysUseSubsumption)
+ {
+ TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
+ var litExpr = ac.Expr as LiteralExpr;
+ if (litExpr == null || !litExpr.IsTrue)
+ {
+ // Turn it into an assume statement.
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+ }
+ else
+ {
+ dropCmd = true;
+ }
+ }
+ else if (subsumption == CommandLineOptions.SubsumptionOption.Never)
+ {
+ TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
+ dropCmd = true;
+ }
+ else
+ {
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
+ }
+ }
+ else
+ {
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
+ }
+ }
}
else if (currentImplementation != null
- && currentImplementation.AnyErrorsInCachedSnapshot
- && ac.Checksum != null
- && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
- && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
- && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
+ && currentImplementation.HasCachedSnapshot
+ && relevantAssumpVars.Count == 0
+ && checksum != null
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
+ && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
+ {
+ if (alwaysUseSubsumption)
+ {
+ // Turn it into an assume statement.
+ TraceCachingAction(pc, CachingAction.RecycleError);
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
+ currentImplementation.AddRecycledFailingAssertion(ac);
+ }
+ else if (subsumption == CommandLineOptions.SubsumptionOption.Never)
+ {
+ TraceCachingAction(pc, CachingAction.RecycleError);
+ dropCmd = true;
+ currentImplementation.AddRecycledFailingAssertion(ac);
+ }
+ else
+ {
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
+ }
+ }
+ else
{
- // Turn it into an assume statement.
- pc = new AssumeCmd(ac.tok, copy);
- pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
- currentImplementation.AddRecycledFailingAssertion(ac);
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
}
}
else if (pc is AssumeCmd
&& QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")
- && currentImplementation.InjectedAssumptionVariables != null
- && currentImplementation.InjectedAssumptionVariables.Any())
+ && pc.SugaredCmdChecksum != null)
+ {
+ if (!relevantDoomedAssumpVars.Any()
+ && currentImplementation.HasCachedSnapshot
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum)
+ && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum))
+ {
+ bool isTrue;
+ var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
+ if (!isTrue)
+ {
+ copy = LiteralExpr.Imp(assmVars, copy);
+ TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
+ }
+ else
+ {
+ TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
+ }
+ }
+ else
+ {
+ TraceCachingAction(pc, CachingAction.DropAssume);
+ dropCmd = true;
+ }
+ }
+ else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization"))
{
- copy = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy);
- isAssumePre = true;
+ var identExpr = pc.Expr as IdentifierExpr;
+ if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl))
+ {
+ incarnationMap[identExpr.Decl] = LiteralExpr.True;
+ dropCmd = true;
+ }
}
pc.Expr = copy;
- if (!isAssumePre
- || currentImplementation.NoErrorsInCachedSnapshot
- || (currentImplementation.AnyErrorsInCachedSnapshot
- && pc.Checksum != null
- && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum))
- && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(pc.Checksum)))
+ if (!dropCmd)
{
passiveCmds.Add(pc);
}
@@ -1595,6 +1748,24 @@ namespace VC { newIncarnationMappings[lhs] = x_prime_exp;
}
#endregion
+
+ var nAryExpr = copies[i] as NAryExpr;
+ if (nAryExpr != null)
+ {
+ var binOp = nAryExpr.Fun as BinaryOperator;
+ if (binOp != null
+ && binOp.Op == BinaryOperator.Opcode.And)
+ {
+ var arg0 = nAryExpr.Args[0] as LiteralExpr;
+ var arg1 = nAryExpr.Args[1] as LiteralExpr;
+ if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse))
+ {
+ // Replace the expressions "true && arg1" or "arg0 && false" by "arg1".
+ copies[i] = nAryExpr.Args[1];
+ }
+ }
+ }
+
#region Create an assume command with the new variable
assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));
#endregion
@@ -1617,15 +1788,17 @@ namespace VC { }
if (currentImplementation != null
- && currentImplementation.NoErrorsInCachedSnapshot
- && currentImplementation.InjectedAssumptionVariables != null
+ && currentImplementation.HasCachedSnapshot
+ && !currentImplementation.AnyErrorsInCachedSnapshot
&& currentImplementation.InjectedAssumptionVariables.Count == 1
&& assign.Lhss.Count == 1)
{
var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;
- if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption"))
+ Expr incarnation;
+ if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation))
{
- passiveCmds.Add(new AssumeCmd(c.tok, new IdentifierExpr(Token.NoToken, currentImplementation.InjectedAssumptionVariables.First())));
+ TraceCachingAction(assign, CachingAction.AssumeNegationOfAssumptionVariable);
+ passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation)));
}
}
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 1471f30f..fcd126e4 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1084,8 +1084,6 @@ namespace VC { Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));
Debug.Assert(this.program == program);
- var computeUnderBound = true;
-
// Record current time
var startTime = DateTime.UtcNow;
@@ -1159,7 +1157,7 @@ namespace VC { }
#endregion
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1) {
Console.WriteLine(">> SI: Size of VC after eager inlining: {0}", vState.vcSize);
}
@@ -1233,6 +1231,9 @@ namespace VC { {
if (block.Count == 0)
{
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
+ Console.WriteLine(">> SI: Exhausted Bound {0}", bound);
+
// Increment bound
bound++;
@@ -1255,7 +1256,7 @@ namespace VC { Contract.Assert(reporter.candidatesToExpand.Count != 0);
#region expand call tree
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1)
{
Console.Write(">> SI Inlining: ");
reporter.candidatesToExpand
@@ -1285,7 +1286,7 @@ namespace VC { // this call to VerifyImplementation
vState.checker.prover.Pop();
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 1) {
Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => isSkipped(i, calls)).Count());
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6a039923..5e83a337 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1626,7 +1626,8 @@ namespace VC { outcome = Outcome.Errors;
foreach (var a in impl.RecycledFailingAssertions)
{
- var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;
+ var checksum = a.Checksum;
+ var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;
if (oldCex != null)
{
callback.OnCounterexample(oldCex, null);
@@ -2964,7 +2965,7 @@ namespace VC { {
AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd;
Contract.Assert(assertCmd != null);
- CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context);
+ CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context, assertCmd.Checksum);
cc.relatedInformation = relatedInformation;
return cc;
}
|