Add missing Clone() when storing incarnation maps; update testcase to make this clear

Construct states in Model properly, nuke direct printing.

5 files changed, 107 insertions, 166 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index eda5cfda..addb92de 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -195,98 +195,6 @@ namespace Microsoft.Boogie {
           m.Write(wr);

         }      

       }

-

-      /*

-      if (Model == null || MvInfo == null) {

-        return;

-      }

-      if (!Model.definedFunctions.ContainsKey("@MV_state")) {

-        return;

-      }

-      Console.WriteLine("Captured states:");

-      List<List<int>> defs = Model.definedFunctions["@MV_state"];

-      List<int> states = new List<int>();

-      foreach (List<int> parameters in defs) {

-        if (parameters.Count == 2) {  // we expect this for all but possibly the last row

-          int argPartition = parameters[0];

-          object val = Model.partitionToValue[argPartition];

-          if (val is BigNum) {

-            BigNum n = (BigNum)val;

-            states.Add(n.ToInt);

-          }

-        }

-      }

-      // we now have the list of states in 'states'

-      states.Sort();

-#if DEBUG_PRINT

-      Console.WriteLine("DEBUG: ---------- start ----------");

-      foreach (Variable v in MvInfo.AllVariables) {

-        List<string> names = new List<string>();

-

-        {

-          string ss = v.Name;

-          VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);

-          if (vvar != null) {

-            string uniqueName = Context.Lookup(vvar);

-            ss += " -> " + uniqueName;

-          }

-          names.Add(ss);

-        }

-

-        foreach (int s in states) {

-          if (0 <= s && s < MvInfo.CapturePoints.Count) {

-            VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];

-            var map = m.IncarnationMap;

-            if (map.ContainsKey(v)) {

-              Expr e = (Expr)map[v];

-              var ss = string.Format("[{0}: {1}", m.Description, e.ToString());

-              IdentifierExpr ide = e as IdentifierExpr;

-              if (ide != null) {

-                VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);

-                if (vvar != null) {

-                  string uniqueName = Context.Lookup(vvar);

-                  ss += " -> " + uniqueName;

-                }

-              }

-              ss += "]";

-              names.Add(ss);

-            }

-          }

-        }

-

-        foreach (var nm in names) {

-          Console.Write("{0} ", nm);

-        }

-        Console.WriteLine();

-      }

-      Console.WriteLine("DEBUG: ---------- end ----------");

-#endif

-      List<Variable> changedVariables;

-      if (states.Count <= 1) {

-        changedVariables = MvInfo.AllVariables;

-      } else {

-        VC.ModelViewInfo.Mapping last = MvInfo.CapturePoints[MvInfo.CapturePoints.Count-1];

-        changedVariables = new List<Variable>();

-        List<Variable> unchangedVariables = new List<Variable>();

-        foreach (Variable v in MvInfo.AllVariables) {

-          if (last.IncarnationMap.ContainsKey(v)) {

-            changedVariables.Add(v);

-          } else {

-            unchangedVariables.Add(v);

-          }

-        }

-        PrintCapturedState(8, unchangedVariables, new Hashtable());

-      }

-      foreach (int s in states) {

-        if (0 <= s && s < MvInfo.CapturePoints.Count) {

-          VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];

-          Console.WriteLine("    {0}", m.Description);

-          PrintCapturedState(8, changedVariables, m.IncarnationMap);

-        } else {

-          Console.WriteLine("    undefined captured-state ID {0}", s);

-        }

-      }

-      */

     }

 

     public Model GetModelWithStates()

@@ -314,23 +222,36 @@ namespace Microsoft.Boogie {
 

       states.Sort();

 

-      foreach (int s in states) {

-        if (0 <= s && s < MvInfo.CapturePoints.Count) {

+      for (int i = 0; i < states.Count; ++i) {

+        var s = states[i];

+        if (0 <= s && s < MvInfo.CapturePoints.Count) {          

           VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];

+          var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable();

           var cs = m.MkState(map.Description);

 

           foreach (Variable v in MvInfo.AllVariables) {

             var e = (Expr)map.IncarnationMap[v];

             if (e == null) continue;

 

+            // if (prevInc[v] == e) continue; // skip unchanged variables

+

             Model.Element elt;

 

             if (e is IdentifierExpr) {

               IdentifierExpr ide = (IdentifierExpr)e;

 

-              var f = m.TryGetFunc(ide.Decl.Name);

+              // first, get the unique name

+              string uniqueName;

+              VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);

+              if (vvar == null) {

+                uniqueName = ide.Decl.Name;

+              } else {

+                uniqueName = Context.Lookup(vvar);

+              }

+

+              var f = m.TryGetFunc(uniqueName);

               if (f == null) {

-                f = m.MkFunc(ide.Decl.Name, 0);

+                f = m.MkFunc(uniqueName, 0);

               }              

               elt = f.GetConstant();

             } else if (e is LiteralExpr) {

@@ -351,54 +272,6 @@ namespace Microsoft.Boogie {
       return m;

     }

 

-    void PrintCapturedState(int indent, List<Variable> varSet, Hashtable/*Variable -> Expr*/ incarnations) {

-      Contract.Requires(0 <= indent);

-      Contract.Requires(varSet != null);

-      Contract.Requires(Model != null && MvInfo != null);

-      string ind = new string(' ', indent);

-

-      foreach (Variable v in varSet) {

-        string varName = v.Name;

-        Variable incarnation = v;

-        string val = null;

-        if (incarnations.ContainsKey(v)) {

-          Expr e = (Expr)incarnations[v];

-          if (e is IdentifierExpr) {

-            IdentifierExpr ide = (IdentifierExpr)e;

-            incarnation = ide.Decl;

-          } else if (e is LiteralExpr) {

-            LiteralExpr lit = (LiteralExpr)e;

-            val = lit.Val.ToString();

-          } else {

-            val = e.ToString();  // temporary hack to have something to do in this case

-          }

-        }

-        if (val == null) {

-          // first, get the unique name

-          string uniqueName;

-          VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(incarnation);

-          if (vvar == null) {

-            uniqueName = incarnation.Name;

-          } else {

-            uniqueName = Context.Lookup(vvar);

-          }

-          // look up the value in the model

-          int zid;

-          if (Model.identifierToPartition.TryGetValue(uniqueName, out zid)) {

-            object pvalue = Model.partitionToValue[zid];

-            if (pvalue != null) {

-              val = pvalue.ToString();

-            } else {

-              val = "*" + zid;  // temporary hack to have something to do in this case

-            }

-          } else {

-            val = uniqueName;  // temporary hack to have something to do in this case

-          }

-        }

-        Console.WriteLine("{0}{1} = {2}", ind, varName, val);

-      }

-    }

-

     public abstract int GetLocation();

   }

 

@@ -1427,7 +1300,7 @@ namespace VC {
           if (description != null) {

             Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));

             copy = Bpl.Expr.And(mv, copy);

-            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, incarnationMap));

+            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone()));

           }

         }

         Contract.Assert(copy != null);

diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
index 5e4a0a0f..d309c01d 100644
--- a/Source/VCGeneration/Model.cs
+++ b/Source/VCGeneration/Model.cs
@@ -370,7 +370,7 @@ namespace Microsoft.Boogie
           continue;

         wr.WriteLine("*** STATE {0}", s.Name);

         foreach (var v in s.Variables)

-          wr.WriteLine("{0} -> {1}", v, s.TryGet(v));

+          wr.WriteLine("  {0} -> {1}", v, s.TryGet(v));

         wr.WriteLine("*** END_STATE", s.Name);

       }

       wr.WriteLine("*** END_MODEL");

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 974f24fc..47bff793 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -192,29 +192,91 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 3 errors

 

 -------------------- CaptureState --------------------

-CaptureState.bpl(26,1): Error BP5003: A postcondition might not hold on this return path.

+CaptureState.bpl(27,1): Error BP5003: A postcondition might not hold on this return path.

 CaptureState.bpl(8,3): Related location: This is the postcondition that might not hold.

 Execution trace:

     CaptureState.bpl(12,3): anon0

     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

-Captured states:

-        Heap = *8

-        F = *10

-        this = *9

-        x = 797

-        y = y@@1

-    top

-        r = r

-        m = -2

-    then

-        r = r

-        m = -1

-    postUpdate0

-        r = r

-        m = -1

-    end

-        r = -2

-        m = -1

+*** MODEL

+@true -> 6

+@false -> 7

+intType -> *4

+boolType -> *5

+RefType -> *6

+FieldNameType -> *7

+Heap -> *8

+this -> *9

+F -> *10

+m@0 -> -2

+r@0 -> -2

+x@@4 -> 797

+m@1 -> -1

+m@3 -> -1

+$pow2 -> {

+  0 -> 1

+}

+tickleBool -> {

+  false -> true

+  true -> true

+}

+Ctor -> {

+  *4 -> 0

+  *5 -> 1

+  *6 -> 3

+  *7 -> 4

+  *18 -> 2

+}

+type -> {

+  *8 -> *18

+  *9 -> *6

+  *10 -> *7

+  *20 -> *4

+}

+MapType0Type -> {

+  *6 *7 *4 -> *18

+}

+MapType0TypeInv2 -> {

+  *18 -> *4

+}

+MapType0TypeInv1 -> {

+  *18 -> *7

+}

+MapType0TypeInv0 -> {

+  *18 -> *6

+}

+@MV_state -> {

+  0 -> true

+  1 -> true

+  2 -> true

+  5 -> true

+}

+MapType0Select -> {

+  *8 *9 *10 -> *20

+}

+U_2_int -> {

+  *20 -> -2

+}

+int_2_U -> {

+  -2 -> *20

+}

+*** STATE <initial>

+  Heap -> *8

+  F -> *10

+  this -> *9

+*** END_STATE

+*** STATE top

+*** END_STATE

+*** STATE then

+  m -> -2

+*** END_STATE

+*** STATE postUpdate0

+  m -> -1

+*** END_STATE

+*** STATE end

+  r -> -2

+  m -> 7

+*** END_STATE

+*** END_MODEL

 

 Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl
index 7c73c411..7635ecdc 100644
--- a/Test/test15/CaptureState.bpl
+++ b/Test/test15/CaptureState.bpl
@@ -22,5 +22,6 @@ procedure P(this: Ref, x: int, y: int) returns (r: int)
     assume {:captureState "postUpdate1"} true;

   }

   r := m + m;

+  m := 7;

   assume {:captureState "end"} true;

 }

diff --git a/Test/test15/runtest.bat b/Test/test15/runtest.bat
index fc25c876..83452323 100644
--- a/Test/test15/runtest.bat
+++ b/Test/test15/runtest.bat
@@ -9,8 +9,13 @@ for %%f in (NullInModel IntInModel ModelTest) do (
   echo -------------------- %%f --------------------

   "%BGEXE%" %* %%f.bpl /printModel:2

 )

-for %%f in (InterpretedFunctionTests CaptureState) do (

+for %%f in (InterpretedFunctionTests) do (

   echo.

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

   "%BGEXE%" %* %%f.bpl

 )

+for %%f in (CaptureState) do (

+  echo.

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

+  "%BGEXE%" %* %%f.bpl /mv:-

+)