Boogie:

* Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators.
* Added a rudimentary printing of variables for captured states.  It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes.  A more complete implementation will be added at a later time.

9 files changed, 198 insertions, 21 deletions

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 33e622ba..4a16e6b6 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -597,6 +597,13 @@ namespace Microsoft.Boogie.Z3
           int k = s.IndexOfAny(new char[] { ' ', '}' }, j);

           Contract.Assume(j <= k);

           string id = s.Substring(j, k - j);

+#if IS_THIS_A_GOOD_IDEA

+          // remove any @@-suffix

+          int doubleAt = id.IndexOf("@@");

+          if (doubleAt != -1) {

+            id = id.Substring(0, doubleAt);

+          }

+#endif

           j = k + 1;

           Contract.Assume(!identifierToPartition.ContainsKey(id));  // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class

           identifierToPartition.Add(id, zID);

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index aac288b9..a449dc82 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -196,15 +196,55 @@ namespace Microsoft.Boogie {
       // we now have the list of states in 'states'

       states.Sort();

       foreach (int s in states) {

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

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

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

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

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

+          PrintCapturedState(8, m.IncarnationMap);

         } else {

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

         }

       }

     }

 

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

+      Contract.Requires(0 <= indent);

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

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

+

+      foreach (Variable v in MvInfo.AllVariables) {

+        string varName = v.Name;

+        string incarnationName = varName;

+        string val = null;

+        if (incarnations.ContainsKey(v)) {

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

+          if (e is IdentifierExpr) {

+            IdentifierExpr ide = (IdentifierExpr)e;

+            incarnationName = ide.Decl.Name;

+          } 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) {

+          // look up the value in the model

+          int partition;

+          if (Model.identifierToPartition.TryGetValue(incarnationName, out partition)) {

+            object pvalue = Model.partitionToValue[partition];

+            if (pvalue != null) {

+              val = pvalue.ToString();

+            } else {

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

+            }

+          } else {

+            val = incarnationName;  // temporary hack to have something to do in this case

+          }

+        }

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

+      }

+    }

+

     public abstract int GetLocation();

   }

 

@@ -1134,10 +1174,11 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, out ModelViewInfo mvInfo) {

+    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

+      Contract.Requires(mvInfo != null);

 

-      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, out mvInfo);

+      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

 

       RestoreParamWhereClauses(impl);

 

@@ -1151,9 +1192,10 @@ namespace VC {
       return r;

     }

 

-    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, out ModelViewInfo mvInfo) {

+    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

       Contract.Requires(blocks != null);

       Contract.Requires(modifies != null);

+      Contract.Requires(mvInfo != null);

       #region Convert to Passive Commands

 

       #region Topological sort -- need to process in a linearization of the partial order

@@ -1186,7 +1228,6 @@ namespace VC {
       // processed all of a node's predecessors before we process the node.

       Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

       Block exitBlock = null;

-      mvInfo = new ModelViewInfo();

       foreach (Block b in sortedNodes) {

         Contract.Assert(b != null);

         Contract.Assert(!block2Incarnation.Contains(b));

@@ -1230,9 +1271,9 @@ namespace VC {
         if (0 < CommandLineOptions.Clo.ModelView && pc is AssumeCmd) {

           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");

           if (description != null) {

-            Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState), new ExprSeq(Bpl.Expr.Literal(mvInfo.Info.Count)));

+            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.Info.Add(new ModelViewInfo.Mapping(description, incarnationMap));

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

           }

         }

         Contract.Assert(copy != null);

@@ -1479,11 +1520,45 @@ namespace VC {
 

   public class ModelViewInfo

   {

-    public readonly List<Mapping> Info = new List<Mapping>();

-    public readonly Function MVState = new Function(Token.NoToken, "@MV_state",

+    public readonly List<Variable> AllVariables = new List<Variable>();

+    public readonly List<Mapping> CapturePoints = new List<Mapping>();

+    public readonly Function MVState_FunctionDef = new Function(Token.NoToken, "@MV_state",

       new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),

       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));

 

+    public ModelViewInfo(Program program, Implementation impl) {

+      Contract.Requires(program != null);

+      Contract.Requires(impl != null);

+

+      // global variables

+      foreach (Declaration d in program.TopLevelDeclarations) {

+        if (d is Variable) {

+          AllVariables.Add((Variable)d);

+        }

+      }

+      // implementation parameters

+      foreach (Variable p in impl.InParams) {

+        AllVariables.Add(p);

+      }

+      foreach (Variable p in impl.OutParams) {

+        AllVariables.Add(p);

+      }

+      // implementation locals

+      foreach (Variable v in impl.LocVars) {

+        AllVariables.Add(v);

+      }

+    }

+

+    public ModelViewInfo(CodeExpr codeExpr) {

+      Contract.Requires(codeExpr != null);

+      // TODO: also need all variables of enclosing scopes (the global variables of the program, the parameters

+      // and perhaps locals of the implementation (if any), any enclosing code expressions).

+

+      foreach (Variable v in codeExpr.LocVars) {

+        AllVariables.Add(v);

+      }

+    }

+

     public class Mapping

     {

       public readonly string Description;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 80934bc2..b332477f 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1556,8 +1556,7 @@ namespace VC {
 

             vcgen.ComputePredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            ModelViewInfo mvInfoCodeExpr;

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), out mvInfoCodeExpr);

+            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

             VCExpr startCorrect = VCGen.LetVC(

 		      codeExpr.Blocks[0],

               null,

@@ -3699,8 +3698,9 @@ namespace VC {
       if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {

         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }

-      

-      Hashtable exitIncarnationMap = Convert2PassiveCmd(impl, out mvInfo);

+

+      mvInfo = new ModelViewInfo(program, impl);

+      Hashtable exitIncarnationMap = Convert2PassiveCmd(impl, mvInfo);

 

       if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name))

       {

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index d97ee0fd..f833d6e9 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -327,8 +327,7 @@ namespace VC {
       if (UseItAsDebugger)

         RemoveReachVars(cce.NonNull(firstDebugBlock));

 

-      ModelViewInfo mvInfo;

-      PassifyProgram(impl, out mvInfo);

+      PassifyProgram(impl, new ModelViewInfo(program, impl));

 

       #endregion

       //EmitImpl(impl,false);

@@ -1313,12 +1312,13 @@ namespace VC {
     }

 

 

-    private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, out ModelViewInfo mvInfo) {

+    private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

+      Contract.Requires(mvInfo != null);

       Contract.Ensures(Contract.Result<Hashtable>() != null);

 

       CurrentLocalVariables = impl.LocVars;

-      Convert2PassiveCmd(impl, out mvInfo);

+      Convert2PassiveCmd(impl, mvInfo);

       return new Hashtable();

     }

 

diff --git a/Test/alltests.txt b/Test/alltests.txt
index 589908bf..48f132de 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -9,7 +9,7 @@ aitest0          Use    Constant propagation test
 aitest1          Use    Linear ineqality test

 aitest9          Use    Test for the abstract domain of intervals

 lock             Use    SLAM example

-test13           Use    ExistsUnique

+test13           Use    error messages for failing asserts vs. loop invariants

 inline           Use    Procedure inlining

 textbook         Use    Some textbook examples

 test15           Use    Benchmarks for error messages

@@ -28,5 +28,5 @@ vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks
 livevars         Use    STORM benchmarks for testing correctness of live variable analysis

 lazyinline       Use    Lazy inlining benchmarks

 stratifiedinline Use    Stratified inlining benchmarks

-extractloops	 Use    Extract loops benchmarks

+extractloops     Use    Extract loops benchmarks

 VSComp2010       Use    Dafny solutions to VSComp (verified software competition) problems

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 969bbe41..825df64f 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -200,8 +200,36 @@ Execution trace:
     CaptureState.bpl(24,5): anon3

 Captured states:

     top

+        Heap = *8

+        F = *10

+        this = *9

+        x = x

+        y = y

+        r = r

+        m = -2

     then

+        Heap = *8

+        F = *10

+        this = *9

+        x = x

+        y = y

+        r = r

+        m = -1

     postUpdate0

+        Heap = *8

+        F = *10

+        this = *9

+        x = x

+        y = y

+        r = r

+        m = -1

     end

+        Heap = *8

+        F = *10

+        this = *9

+        x = x

+        y = y

+        r = -2

+        m = -1

 

 Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/textbook/Answer b/Test/textbook/Answer
index 9e2227dc..538109f5 100644
--- a/Test/textbook/Answer
+++ b/Test/textbook/Answer
@@ -10,3 +10,7 @@ Boogie program verifier finished with 1 verified, 0 errors
 ------------------------------ Bubble.bpl ---------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

+

+------------------------------ DivMod.bpl ---------------------

+

+Boogie program verifier finished with 2 verified, 0 errors

diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl
new file mode 100644
index 00000000..4a551b6e
--- /dev/null
+++ b/Test/textbook/DivMod.bpl
@@ -0,0 +1,63 @@
+// This file contains two definitions of integer div/mod (truncated division, as is

+// used in C, C#, Java, and several other languages, and Euclidean division, which

+// has mathematical appeal and is used by SMT Lib) and proves the correct

+// correspondence between the two.

+//

+// Rustan Leino, 23 Sep 2010

+

+function abs(x: int): int { if 0 <= x then x else -x }

+

+function divt(int, int): int;

+function modt(int, int): int;

+

+axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a);

+axiom (forall a,b: int ::

+  (0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) &&

+  (a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0));

+

+function dive(int, int): int;

+function mode(int, int): int;

+

+axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a);

+axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b));

+

+procedure T_from_E(a,b: int) returns (q,r: int)

+  requires b != 0;

+  // It would be nice to prove:

+  //   ensures q == divt(a,b);

+  //   ensures r == modt(a,b);

+  // but since we know that the axioms about divt/modt have unique solutions (for

+  // non-zero b), we just prove that the axioms hold.

+  ensures q*b + r == a;

+  ensures 0 <= a ==> 0 <= r && r < abs(b);

+  ensures a < 0 ==> -abs(b) < r && r <= 0;

+{

+  // note, this implementation uses only dive/mode

+  var qq,rr: int;

+  qq := dive(a,b);

+  rr := mode(a,b);

+

+  q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1;

+  r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b;

+  assume {:captureState "end of T_from_E"} true;

+}

+

+procedure E_from_T(a,b: int) returns (q,r: int)

+  requires b != 0;

+  // It would be nice to prove:

+  //   ensures q == dive(a,b);

+  //   ensures r == mode(a,b);

+  // but since we know that the axioms about dive/mode have unique solutions (for

+  // non-zero b), we just prove that the axioms hold.

+  ensures q*b + r == a;

+  ensures 0 <= r;

+  ensures r < abs(b);

+{

+  // note, this implementation uses only divt/modt

+  var qq,rr: int;

+  qq := divt(a,b);

+  rr := modt(a,b);

+

+  q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1;

+  r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b;

+}

diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat
index 6e39e589..bdfdd7d5 100644
--- a/Test/textbook/runtest.bat
+++ b/Test/textbook/runtest.bat
@@ -6,7 +6,7 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe
 REM ======================

 REM ====================== Examples written in Boogie

 REM ======================

-for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl) do (

+for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl) do (

   echo.

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

   %BPLEXE% %* %%f