From bb6e253feab04cc13de3132520eac3ffc8150f01 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sun, 6 Jul 2014 21:34:07 +0200 Subject: Did some refactoring, fixed minor issues, and made it apply the more advanced verification result caching even for implementations with errors. --- Source/VCGeneration/ConditionGeneration.cs | 73 ++++++++++++++++++++++++------ 1 file changed, 59 insertions(+), 14 deletions(-) (limited to 'Source/VCGeneration/ConditionGeneration.cs') diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 0898641b..9d8669dd 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -82,6 +82,7 @@ namespace Microsoft.Boogie { [Peer] public List/*!>!*/ relatedInformation; public string RequestId; + public abstract byte[] Checksum { get; } public Dictionary calleeCounterexamples; @@ -395,6 +396,11 @@ namespace Microsoft.Boogie { return FailingAssert.tok.line * 1000 + FailingAssert.tok.col; } + public override byte[] Checksum + { + get { return FailingAssert.Checksum; } + } + public override Counterexample Clone() { var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context); @@ -428,6 +434,11 @@ namespace Microsoft.Boogie { return FailingCall.tok.line * 1000 + FailingCall.tok.col; } + public override byte[] Checksum + { + get { return FailingCall.Checksum; } + } + public override Counterexample Clone() { var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context); @@ -446,7 +457,7 @@ namespace Microsoft.Boogie { } - public ReturnCounterexample(List trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context) + public ReturnCounterexample(List trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum) : base(trace, model, mvInfo, context) { Contract.Requires(trace != null); Contract.Requires(context != null); @@ -455,15 +466,29 @@ namespace Microsoft.Boogie { Contract.Requires(!failingEnsures.Free); this.FailingReturn = failingReturn; this.FailingEnsures = failingEnsures; + this.checksum = checksum; } public override int GetLocation() { return FailingReturn.tok.line * 1000 + FailingReturn.tok.col; } + byte[] checksum; + + /// + /// Returns the checksum of the corresponding assertion. + /// + public override byte[] Checksum + { + get + { + return checksum; + } + } + public override Counterexample Clone() { - var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context); + var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context, checksum); ret.calleeCounterexamples = calleeCounterexamples; return ret; } @@ -1297,7 +1322,7 @@ namespace VC { Dictionary 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 incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) { + protected void TurnIntoPassiveBlock(Block b, Dictionary incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, byte[] currentChecksum = null) { Contract.Requires(b != null); Contract.Requires(incarnationMap != null); Contract.Requires(mvInfo != null); @@ -1307,8 +1332,11 @@ namespace VC { List passiveCmds = new List(); 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); + currentChecksum = c.Checksum; TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo); } + b.Checksum = currentChecksum; b.Cmds = passiveCmds; if (b.TransferCmd is ReturnExprCmd) { @@ -1389,8 +1417,14 @@ 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; foreach (Block p in b.Predecessors) { p.succCount--; + if (b.Checksum != null) + { + // Compute the checksum based on the checksums of the predecessor. The order should not matter. + currentChecksum = ChecksumHelper.CombineChecksums(b.Checksum, currentChecksum, true); + } if (p.succCount == 0) block2Incarnation.Remove(p); } @@ -1407,7 +1441,7 @@ namespace VC { } #endregion Each block's map needs to be available to successor blocks - TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst); + TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, currentChecksum); exitBlock = b; exitIncarnationMap = incarnationMap; } @@ -1463,15 +1497,22 @@ namespace VC { } } Contract.Assert(copy != null); + var isAssumePre = false; if (pc is AssertCmd) { ((AssertCmd)pc).OrigExpr = pc.Expr; Contract.Assert(((AssertCmd)pc).IncarnationMap == null); ((AssertCmd)pc).IncarnationMap = (Dictionary)cce.NonNull(new Dictionary(incarnationMap)); if (currentImplementation != null - && currentImplementation.NoErrorsInCachedSnapshot - && currentImplementation.InjectedAssumptionVariables != null - && 2 <= currentImplementation.InjectedAssumptionVariables.Count) + && ((currentImplementation.NoErrorsInCachedSnapshot + && currentImplementation.InjectedAssumptionVariables != null + && 2 <= currentImplementation.InjectedAssumptionVariables.Count) + || (currentImplementation.AnyErrorsInCachedSnapshot + && currentImplementation.InjectedAssumptionVariables != null + && currentImplementation.InjectedAssumptionVariables.Any() + && pc.Checksum != null + && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum)) + && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(pc.Checksum)))) { // Bind the assertion expression to a local variable. var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, new IdentifierExpr(Token.NoToken, CurrentTemporaryVariableForAssertions)); @@ -1483,21 +1524,25 @@ namespace VC { var expr = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy); passiveCmds.Add(new AssumeCmd(Token.NoToken, expr)); } - else if (currentImplementation != null - && currentImplementation.AnyErrorsInCachedSnapshot) - { - // TODO(wuestholz): Add an assume statement if the assertion was verified in the previous snapshot. - } } else if (pc is AssumeCmd - && QKeyValue.FindStringAttribute(pc.Attributes, "precondition_previous_snapshot") != null + && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") && currentImplementation.InjectedAssumptionVariables != null && currentImplementation.InjectedAssumptionVariables.Any()) { copy = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy); + isAssumePre = true; } pc.Expr = copy; - passiveCmds.Add(pc); + if (!isAssumePre + || currentImplementation.NoErrorsInCachedSnapshot + || (currentImplementation.AnyErrorsInCachedSnapshot + && pc.Checksum != null + && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum)) + && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(pc.Checksum))) + { + passiveCmds.Add(pc); + } } #endregion #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below] -- cgit v1.2.3