From bdbc1febe585ea725e67e4d114e8097c912fe52d Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 16 Oct 2014 16:05:02 +0200 Subject: Did some refactoring. --- Source/Core/Absy.cs | 39 +++++++++++---- Source/Core/DeadVarElim.cs | 11 ++--- Source/ExecutionEngine/VerificationResultCache.cs | 12 ++--- Source/VCGeneration/ConditionGeneration.cs | 58 ++++++++++++----------- 4 files changed, 72 insertions(+), 48 deletions(-) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index a419fead..a9466f8d 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3128,7 +3128,14 @@ namespace Microsoft.Boogie { assertionChecksums.Add(checksum); } - public ISet AssertionChecksumsInPreviousSnapshot { get; set; } + public ISet AssertionChecksumsInCachedSnapshot { get; set; } + + public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum) + { + Contract.Requires(AssertionChecksumsInCachedSnapshot != null); + + return AssertionChecksumsInCachedSnapshot.Contains(checksum); + } public IList RecycledFailingAssertions { get; protected set; } @@ -3214,6 +3221,13 @@ namespace Microsoft.Boogie { public IDictionary ErrorChecksumToCachedError { get; private set; } + public bool IsErrorChecksumInCachedSnapshot(byte[] checksum) + { + Contract.Requires(ErrorChecksumToCachedError != null); + + return ErrorChecksumToCachedError.ContainsKey(checksum); + } + public void SetErrorChecksumToCachedError(IEnumerable> errors) { Contract.Requires(errors != null); @@ -3225,11 +3239,11 @@ namespace Microsoft.Boogie { } } - public bool NoErrorsInCachedSnapshot + public bool HasCachedSnapshot { get { - return ErrorChecksumToCachedError != null && !ErrorChecksumToCachedError.Any(); + return ErrorChecksumToCachedError != null && AssertionChecksumsInCachedSnapshot != null; } } @@ -3237,7 +3251,9 @@ namespace Microsoft.Boogie { { get { - return ErrorChecksumToCachedError != null && ErrorChecksumToCachedError.Any(); + Contract.Requires(ErrorChecksumToCachedError != null); + + return ErrorChecksumToCachedError.Any(); } } @@ -3246,15 +3262,22 @@ namespace Microsoft.Boogie { { get { - return injectedAssumptionVariables; + return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List(); } } - public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary incarnationMap) + public List PossiblyFalseAssumptionVariables(Dictionary incarnationMap) + { + return InjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList(); + } + + public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary incarnationMap, out bool isTrue) { - Contract.Requires(InjectedAssumptionVariables != null && InjectedAssumptionVariables.Any() && incarnationMap != null); + Contract.Requires(incarnationMap != null); - return LiteralExpr.BinaryTreeAnd(injectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).Select(v => incarnationMap[v]).ToList()); + var vars = PossiblyFalseAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList(); + isTrue = vars.Count == 0; + return LiteralExpr.BinaryTreeAnd(vars); } public void InjectAssumptionVariable(LocalVariable variable) diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index e9975fe5..2993feb7 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -421,14 +421,13 @@ namespace Microsoft.Boogie { foreach (Block/*!*/ block in sortedNodes) { Contract.Assert(block != null); HashSet/*!*/ liveVarsAfter = new HashSet(); - if (impl.InjectedAssumptionVariables != null) + + // The injected assumption variables should always be considered to be live. + foreach (var v in impl.InjectedAssumptionVariables) { - // The injected assumption variables should always be considered to be live. - foreach (var v in impl.InjectedAssumptionVariables) - { - liveVarsAfter.Add(v); - } + liveVarsAfter.Add(v); } + if (block.TransferCmd is GotoCmd) { GotoCmd gotoCmd = (GotoCmd)block.TransferCmd; if (gotoCmd.labelTargets != null) { diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index eed92d31..e647ea3b 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -136,7 +136,7 @@ namespace Microsoft.Boogie var p = ExecutionEngine.CachedProgram(vr.ProgramId); if (p != null) { - SetAssertionChecksumsInPreviousSnapshot(impl, p); + SetAssertionChecksumsInCachedSnapshot(impl, p); eai.Inject(impl, p); run.RewrittenImplementationCount++; } @@ -154,7 +154,7 @@ namespace Microsoft.Boogie var p = ExecutionEngine.CachedProgram(vr.ProgramId); if (p != null) { - SetAssertionChecksumsInPreviousSnapshot(impl, p); + SetAssertionChecksumsInCachedSnapshot(impl, p); } } } @@ -202,12 +202,12 @@ namespace Microsoft.Boogie } } - private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program) + private static void SetAssertionChecksumsInCachedSnapshot(Implementation implementation, Program program) { - var implPrevSnap = program.FindImplementation(implementation.Id); - if (implPrevSnap != null) + var cachedImpl = program.FindImplementation(implementation.Id); + if (cachedImpl != null) { - implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums; + implementation.AssertionChecksumsInCachedSnapshot = cachedImpl.AssertionChecksums; } } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 36f38ab8..8295a873 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1489,6 +1489,7 @@ namespace VC { } Contract.Assert(copy != null); var dropCmd = false; + var possiblyFalseAssumpVars = currentImplementation != null ? currentImplementation.PossiblyFalseAssumptionVariables(incarnationMap) : null; if (pc is AssertCmd) { var ac = (AssertCmd)pc; ac.OrigExpr = ac.Expr; @@ -1499,15 +1500,14 @@ namespace VC { var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always; if (alwaysUseSubsumption && 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)))) + && currentImplementation.HasCachedSnapshot + && ((!currentImplementation.AnyErrorsInCachedSnapshot + && 2 <= possiblyFalseAssumpVars.Count) + || (currentImplementation.AnyErrorsInCachedSnapshot + && possiblyFalseAssumpVars.Any() + && ac.Checksum != null + && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum) + && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum)))) { // Bind the assertion expression to a local variable. var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock); @@ -1516,9 +1516,10 @@ namespace VC { ac.IncarnationMap[incarnation] = identExpr; passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy))); copy = identExpr; - var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap); + bool isTrue; + var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); Expr expr = identExpr; - if (assmVars != Expr.True) + if (!isTrue) { expr = LiteralExpr.Imp(assmVars, expr); } @@ -1530,10 +1531,10 @@ namespace VC { } 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 + && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum) + && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum) + && possiblyFalseAssumpVars.Count == 0) { if (alwaysUseSubsumption) { @@ -1544,11 +1545,12 @@ namespace VC { dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never; } else if (currentImplementation != null + && currentImplementation.HasCachedSnapshot && 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.IsAssertionChecksumInCachedSnapshot(ac.Checksum) + && currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum) + && possiblyFalseAssumpVars.Count == 0) { if (alwaysUseSubsumption) { @@ -1564,12 +1566,11 @@ namespace VC { } } else if (pc is AssumeCmd - && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") - && currentImplementation.InjectedAssumptionVariables != null - && currentImplementation.InjectedAssumptionVariables.Any()) + && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")) { - var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap); - if (assmVars != Expr.True) + bool isTrue; + var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); + if (!isTrue) { copy = LiteralExpr.Imp(assmVars, copy); } @@ -1577,11 +1578,12 @@ namespace VC { } pc.Expr = copy; if (!dropCmd - || currentImplementation.NoErrorsInCachedSnapshot + || !currentImplementation.HasCachedSnapshot + || !currentImplementation.AnyErrorsInCachedSnapshot || (currentImplementation.AnyErrorsInCachedSnapshot && pc.Checksum != null - && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum)) - && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(pc.Checksum))) + && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.Checksum) + && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.Checksum))) { passiveCmds.Add(pc); } @@ -1657,8 +1659,8 @@ namespace VC { } if (currentImplementation != null - && currentImplementation.NoErrorsInCachedSnapshot - && currentImplementation.InjectedAssumptionVariables != null + && currentImplementation.HasCachedSnapshot + && !currentImplementation.AnyErrorsInCachedSnapshot && currentImplementation.InjectedAssumptionVariables.Count == 1 && assign.Lhss.Count == 1) { -- cgit v1.2.3