Boogie: Fixed a crash due to old expressions in lambda expressions that were not replaced after lambda expansion.

(reported by Florian Egli)

4 files changed, 61 insertions, 9 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index cb28cd7d..6752a2b7 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1201,14 +1201,7 @@ namespace VC {
       Contract.Assert(sortedNodes != null);

       #endregion

 

-      // Create substitution for old expressions

-      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

-      foreach (IdentifierExpr ie in modifies) {

-        Contract.Assert(ie != null);

-        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

-          oldFrameMap.Add(ie.Decl, ie);

-      }

-      Substitution oldFrameSubst = Substituter.SubstitutionFromHashtable(oldFrameMap);

+      Substitution oldFrameSubst = ComputeOldExpressionSubstitution(modifies);

 

       // Now we can process the nodes in an order so that we're guaranteed to have

       // processed all of a node's predecessors before we process the node.

@@ -1257,6 +1250,21 @@ namespace VC {
     }

 

     /// <summary>

+    /// Compute the substitution for old expressions.

+    /// </summary>

+    protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)

+    {

+      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

+      foreach (IdentifierExpr ie in modifies)

+      {

+        Contract.Assert(ie != null);

+        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

+          oldFrameMap.Add(ie.Decl, ie);

+      }

+      return Substituter.SubstitutionFromHashtable(oldFrameMap);

+    }

+

+    /// <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.

     /// </summary>

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 486f940f..36b9edc2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2388,6 +2388,10 @@ namespace VC {
           Block entryBlock = cce.NonNull( impl.Blocks[0]);

           cmds.AddRange(entryBlock.Cmds);

           entryBlock.Cmds = cmds;

+          // Make sure that all added commands are passive commands.

+          Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());

+          TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,

+                               ComputeOldExpressionSubstitution(impl.Proc.Modifies));

         }

       }

 

diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl
new file mode 100644
index 00000000..c26b0198
--- /dev/null
+++ b/Test/test2/LambdaOldExpressions.bpl
@@ -0,0 +1,39 @@
+var b: bool;

+

+

+procedure p0();

+  requires b;

+  modifies b;

+  ensures (lambda x: bool :: old(b))[true];

+  ensures !(lambda x: bool :: b)[true];

+

+implementation p0()

+{

+    b := !b;

+    assert (lambda x: bool :: old(b))[true];

+    assert !(lambda x: bool :: b)[true];

+}

+

+

+procedure p1();

+  requires !b;

+  modifies b;

+  ensures (lambda x: bool :: old(b))[true];  // error

+

+implementation p1()

+{

+    b := !b;

+    assert !(lambda x: bool :: old(b))[true];

+}

+

+

+procedure p2();

+  requires b;

+  modifies b;

+  ensures (lambda x: bool :: old(b) != b)[true];

+

+implementation p2()

+{

+    b := !b;

+    assert (lambda x: bool :: old(b) != b)[true];

+}

diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 8ce2f66e..f32bf844 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,8 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             strings-no-where.bpl strings-where.bpl

             Structured.bpl Where.bpl UpdateExpr.bpl

             NeverPattern.bpl NullaryMaps.bpl Implies.bpl

-            IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl FreeCall.bpl) do (

+            IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl LambdaOldExpressions.bpl

+            SelectiveChecking.bpl FreeCall.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /noinfer %%f