Implemented an optimization for assignments to assumption variables that are injected by the verification result caching for calls within loops.

2 files changed, 14 insertions, 1 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 8c6685e4..a7693b00 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1886,6 +1886,7 @@ namespace Microsoft.Boogie {
   public class CallCmd : CallCommonality, IPotentialErrorNode {

     public string/*!*/ callee { get; set; }

     public Procedure Proc;

+    public LocalVariable AssignedAssumptionVariable;

 

     // Element of the following lists can be null, which means that

     // the call happens with * as these parameters

@@ -2086,6 +2087,10 @@ namespace Microsoft.Boogie {
         Contract.Assert(e != null);

         vars.Add(e.Decl);

       }

+      if (AssignedAssumptionVariable != null)

+      {

+        vars.Add(AssignedAssumptionVariable);

+      }

     }

 

     public override void Typecheck(TypecheckingContext tc)

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index fbc46de8..b54a45c1 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -429,6 +429,14 @@ namespace Microsoft.Boogie {
       foreach (Block/*!*/ block in sortedNodes) {

         Contract.Assert(block != null);

         HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

+        if (impl.InjectedAssumptionVariables != null)

+        {

+          // The injected assumption variables should always be considered to be live.

+          foreach (var v in impl.InjectedAssumptionVariables)

+          {

+            liveVarsAfter.Add(v);

+          }

+        }

         if (block.TransferCmd is GotoCmd) {

           GotoCmd gotoCmd = (GotoCmd)block.TransferCmd;

           if (gotoCmd.labelTargets != null) {

@@ -497,7 +505,7 @@ namespace Microsoft.Boogie {
         HavocCmd/*!*/ havocCmd = (HavocCmd)cmd;

         foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) {

           Contract.Assert(expr != null);

-          if (expr.Decl != null) {

+          if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##post##"))) {

             liveSet.Remove(expr.Decl);

           }

         }