Automatic merge.

20 files changed, 191 insertions, 98 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 44adce15..ae26d8db 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -18,6 +18,7 @@ namespace Microsoft.Boogie {
   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

   using System.Diagnostics;

+  using System.Linq;

   using VC;

   using AI = Microsoft.AbstractInterpretationFramework;

   using BoogiePL = Microsoft.Boogie;

@@ -178,6 +179,14 @@ namespace Microsoft.Boogie {
           return;

         }

 

+        if (CommandLineOptions.Clo.PrintCFGPrefix != null) {

+          foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>()) {

+            using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot")) {

+              sw.Write(program.ProcessLoops(impl).ToDot());

+            }

+          }

+        }

+

         EliminateDeadVariablesAndInline(program);

 

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 148a739d..041d3a6f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2038,6 +2038,11 @@ namespace Microsoft.Boogie {
     }

   }

 

+  public class Macro : Function {

+    public Macro(IToken tok, string name, VariableSeq args, Variable result)

+      : base(tok, name, args, result) { }

+  }

+

   public class Requires : Absy, IPotentialErrorNode {

     public readonly bool Free;

     public Expr/*!*/ Condition;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c28d8c8a..7d55e177 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -450,6 +450,7 @@ namespace Microsoft.Boogie {
     public string PrintErrorModelFile = null;

     public string/*?*/ ModelViewFile = null;

     public int EnhancedErrorMessages = 0;

+    public string PrintCFGPrefix = null;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

     public bool UseLabels = true;

@@ -834,6 +835,12 @@ namespace Microsoft.Boogie {
           ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

           return true;

 

+        case "printCFG":

+          if (ps.ConfirmArgumentCount(1)) {

+            PrintCFGPrefix = args[ps.i];

+          }

+          return true;

+

         case "inlineDepth":

           ps.GetNumericArgument(ref InlineDepth);

           return true;

@@ -1449,6 +1456,10 @@ namespace Microsoft.Boogie {
                 0 (default) - no enhanced error messages

                 1 - Z3 error model enhanced error messages

 

+  /printCFG:<prefix> : print control flow graph of each implementation in

+                       Graphviz format to files named:

+                         <prefix>.<procedure name>.dot

+

   ---- Inference options -----------------------------------------------------

 

   /infer:<flags>

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index fad4e7fa..58c73561 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -871,7 +871,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

         Indent(indent);

-        wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);

+        wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.UniqueId);

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt)stmt;

         if (s.hiddenUpdate != null)

@@ -1451,7 +1451,7 @@ namespace Microsoft.Dafny {
         TrStmt(ss, indent + IndentAmount);

         if (ss.Labels != null) {

           Indent(indent);  // labels are not indented as much as the statements

-          wr.WriteLine("after_{0}: ;", ss.Labels.UniqueId);

+          wr.WriteLine("after_{0}: ;", ss.Labels.Data.UniqueId);

         }

       }

     }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 97da97e3..56eeb5b6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -691,7 +691,7 @@ OneStmt<out Statement/*!*/ s>
   | ParallelStmt<out s>

   | "label"                            (. x = t; .)

     Ident<out id> ":"

-    OneStmt<out s>                     (. s.Labels = new LabelNode(x, id.val, s.Labels); .)

+    OneStmt<out s>                     (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)

   | "break"                            (. x = t; breakCount = 1; label = null; .)

     ( Ident<out id>                    (. label = id.val; .)

     | { "break"                        (. breakCount++; .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 5fd34e65..0a842025 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1320,7 +1320,7 @@ namespace Microsoft.Dafny {
 

   public abstract class Statement {

     public readonly IToken Tok;

-    public LabelNode Labels;  // mutable during resolution

+    public LList<Label> Labels;  // mutable during resolution

 

     private Attributes attributes;

     public Attributes Attributes {

@@ -1363,19 +1363,43 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class LabelNode

+  public class LList<T>

+  {

+    public readonly T Data;

+    public readonly LList<T> Next;

+    const LList<T> Empty = null;

+

+    public LList(T d, LList<T> next) {

+      Data = d;

+      Next = next;

+    }

+

+    public static LList<T> Append(LList<T> a, LList<T> b) {

+      if (a == null) return b;

+      return new LList<T>(a.Data, Append(a.Next, b));

+      // pretend this is ML

+    }

+    public static int Count(LList<T> n) {

+      int count = 0;

+      while (n != null) {

+        count++;

+        n = n.Next;

+      }

+      return count;

+    }

+  }

+

+  public class Label

   {

     public readonly IToken Tok;

-    public readonly string Label;

+    public readonly string Name;

     public readonly int UniqueId;

-    public readonly LabelNode Next;

     static int nodes = 0;

 

-    public LabelNode(IToken tok, string label, LabelNode next) {

+    public Label(IToken tok, string label) {

       Contract.Requires(tok != null);

       Tok = tok;

-      Label = label;

-      Next = next;

+      Name = label;

       UniqueId = nodes++;

     }

   }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index fe4d58a9..4634c87a 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1098,7 +1098,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Ident(out id);

 			Expect(5);

 			OneStmt(out s);

-			s.Labels = new LabelNode(x, id.val, s.Labels); 

+			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

 		case 50: {

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6cf71fa1..e7cfbf27 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -421,9 +421,9 @@ namespace Microsoft.Dafny {
     /// </summary>

     public void PrintStatement(Statement stmt, int indent) {

       Contract.Requires(stmt != null);

-      for (LabelNode label = stmt.Labels; label != null; label = label.Next) {

-        if (label.Label != null) {

-          wr.WriteLine("label {0}:", label.Label);

+      for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {

+        if (label.Data.Name != null) {

+          wr.WriteLine("label {0}:", label.Data.Name);

           Indent(indent);

         }

       }

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index d966a76f..e73d9762 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -513,13 +513,13 @@ namespace Microsoft.Dafny {
       return r;

     }

 

-    void AddStmtLabels(Statement s, LabelNode node) {

+    void AddStmtLabels(Statement s, LList<Label> node) {

       if (node != null) {

         AddStmtLabels(s, node.Next);

-        if (node.Label == null) {

+        if (node.Data.Name == null) {

           // this indicates an implicit-target break statement that has been resolved; don't add it

         } else {

-          s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);

+          s.Labels = new LList<Label>(new Label(Tok(node.Data.Tok), node.Data.Name), s.Labels);

         }

       }

     }

@@ -1090,8 +1090,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(labels != null);

       Contract.Requires(0 <= loopLevels);

 

-      for (LabelNode n = s.Labels; n != null; n = n.Next) {

-        labels.Push(n.Label);

+      for (LList<Label> n = s.Labels; n != null; n = n.Next) {

+        labels.Push(n.Data.Name);

       }

 

       if (s is SkeletonStatement) {

@@ -1116,7 +1116,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      for (LabelNode n = s.Labels; n != null; n = n.Next) {

+      for (LList<Label> n = s.Labels; n != null; n = n.Next) {

         labels.Pop();

       }

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7be3fca2..23cf892e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1355,7 +1355,7 @@ namespace Microsoft.Dafny {
             Statement target = loopStack[loopStack.Count - s.BreakCount];

             if (target.Labels == null) {

               // make sure there is a label, because the compiler and translator will want to see a unique ID

-              target.Labels = new LabelNode(target.Tok, null, null);

+              target.Labels = new LList<Label>(new Label(target.Tok, null), null);

             }

             s.TargetStmt = target;

             if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {

@@ -2158,17 +2158,18 @@ namespace Microsoft.Dafny {
       foreach (Statement ss in blockStmt.Body) {

         labeledStatements.PushMarker();

         // push labels

-        for (var lnode = ss.Labels; lnode != null; lnode = lnode.Next) {

-          Contract.Assert(lnode.Label != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

-          var prev = labeledStatements.Find(lnode.Label);

+        for (var l = ss.Labels; l != null; l = l.Next) {

+          var lnode = l.Data;

+          Contract.Assert(lnode.Name != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

+          var prev = labeledStatements.Find(lnode.Name);

           if (prev == ss) {

             Error(lnode.Tok, "duplicate label");

           } else if (prev != null) {

             Error(lnode.Tok, "label shadows an enclosing label");

           } else {

-            bool b = labeledStatements.Push(lnode.Label, ss);

+            bool b = labeledStatements.Push(lnode.Name, ss);

             Contract.Assert(b);  // since we just checked for duplicates, we expect the Push to succeed

-            if (lnode == ss.Labels) {  // add it only once

+            if (l == ss.Labels) {  // add it only once

               inSpecOnlyContext.Add(ss, specContextOnly);

             }

           }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0189c11b..58c367b8 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3403,7 +3403,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is BreakStmt) {

         AddComment(builder, stmt, "break statement");

         var s = (BreakStmt)stmt;

-        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));

+        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.Data.UniqueId)));

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt)stmt;

         AddComment(builder, stmt, "return statement");

@@ -3471,7 +3471,7 @@ namespace Microsoft.Dafny {
         foreach (Statement ss in ((BlockStmt)stmt).Body) {

           TrStmt(ss, builder, locals, etran);

           if (ss.Labels != null) {

-            builder.AddLabelCmd("after_" + ss.Labels.UniqueId);

+            builder.AddLabelCmd("after_" + ss.Labels.Data.UniqueId);

           }

         }

       } else if (stmt is IfStmt) {

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 4e30951e..090ddd51 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -124,6 +124,7 @@ namespace GPUVerify
                                   new EnsuresSeq(),

                                   new QKeyValue(Token.NoToken, "barrier", new List<object>(), null));

                 Program.TopLevelDeclarations.Add(p);

+                ResContext.AddProcedure(p);

             }

             return p;

         }

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 49b04251..da9a7a32 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -268,12 +268,13 @@ namespace GPUVerify
 

         private Block MakeDual(Block b)

         {

-            Block result = new Block(b.tok, b.Label, new CmdSeq(), b.TransferCmd);

+            var newCmds = new CmdSeq();

             foreach (Cmd c in b.Cmds)

             {

-                MakeDual(result.Cmds, c);

+                MakeDual(newCmds, c);

             }

-            return result;

+            b.Cmds = newCmds;

+            return b;

         }

 

         private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index a0c4b5f7..a821af15 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -877,7 +877,7 @@ namespace GPUVerify
 

                                 logAccessCallCmd.Proc = logProcedure;

 

-                                cs.Add(logAccessCallCmd);

+                                result.Add(logAccessCallCmd);

 

                             }

                         }

@@ -914,7 +914,7 @@ namespace GPUVerify
 

                                 logAccessCallCmd.Proc = logProcedure;

 

-                                cs.Add(logAccessCallCmd);

+                                result.Add(logAccessCallCmd);

 

                                 addedLogWrite = true;

 

@@ -1076,12 +1076,21 @@ namespace GPUVerify
                     {

                         // Ins[0] is thread 1's predicate,

                         // Ins[1] is the offset to be read

-                        // Ins[1] has the form BV32_ADD(offset#construct...(P), offset)

-                        // We are looking for the second parameter to this BV32_ADD

+                        // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),

+                        // we are looking for the second parameter to this BV32_ADD

                         Expr offset = call.Ins[1];

-                        Debug.Assert(offset is NAryExpr);

-                        Debug.Assert((offset as NAryExpr).Fun.FunctionName == "BV32_ADD");

-                        result.Add((offset as NAryExpr).Args[1]);

+                        if (offset is NAryExpr)

+                        {

+                            var nExpr = (NAryExpr)offset;

+                            if (nExpr.Fun.FunctionName == "BV32_ADD" &&

+                                nExpr.Args[0] is NAryExpr)

+                            {

+                                var n0Expr = (NAryExpr)nExpr.Args[0];

+                                if (n0Expr.Fun.FunctionName.StartsWith("offset#"))

+                                    offset = nExpr.Args[1];

+                            }

+                        }

+                        result.Add(offset);

                     }

 

                 }

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index e5e8444c..b5590865 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -843,6 +843,19 @@ namespace Graphing {
         }

         return dag.TopologicalSort();

     }

+

+    public string ToDot(Func<Node, string> NodeLabel = null, Func<Node, string> NodeStyle = null) {

+      NodeLabel = NodeLabel ?? (n => n.ToString());

+      NodeStyle = NodeStyle ?? (n => "[shape=box]");

+      var s = new StringBuilder();

+      s.AppendLine("digraph G {");

+      foreach (var n in Nodes)

+        s.AppendLine("  \"" + NodeLabel(n) + "\" " + NodeStyle(n) + ";");

+      foreach (var e in Edges)

+        s.AppendLine("  \"" + NodeLabel(e.Item1) + "\" -> \"" + NodeLabel(e.Item2) + "\";");

+      s.AppendLine("}");

+      return s.ToString();

+    }

   } // end: class Graph

 

   public class GraphProgram {

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 19ec088d..ab2fa74f 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -245,11 +245,6 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

-  public class Macro : Function {

-    public Macro(IToken tok, string name, VariableSeq args, Variable result)

-      : base(tok, name, args, result) { }

-  }

-

   public class InlineRequiresVisitor : StandardVisitor {

     public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

       Contract.Requires(cmdSeq != null);

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 65c4e130..31afbdfa 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -770,12 +770,13 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC(a);

     }

 

-    public override void DefineMacro(Function fun, VCExpr vc) {

-      DeclCollector.AddFunction(fun);

-      string name = Namer.GetName(fun, fun.Name);

-      string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";

+    public override void DefineMacro(Macro f, VCExpr vc) {

+      DeclCollector.AddFunction(f);

+      string printedName = Namer.GetQuotedName(f, f.Name);

+      var argTypes = f.InParams.Cast<Variable>().MapConcat(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type), " ");

+      string decl = "(define-fun " + printedName + " (" + argTypes + ") " + DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")";

       AssertAxioms();

-      SendThisVC(a);

+      SendThisVC(decl); 

     }

 

     public override void AssertAxioms()

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index a2564be5..ef3a88cc 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -488,7 +488,7 @@ namespace Microsoft.Boogie {
       get;

     }

 

-    public virtual void DefineMacro(Function fun, VCExpr vc) {

+    public virtual void DefineMacro(Macro fun, VCExpr vc) {

       throw new NotImplementedException();

     }

   }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 563cbf40..2d518a54 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -23,44 +23,20 @@ namespace VC {
     public Dictionary<Block, List<StratifiedCallSite>> callSites;

     public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;

     public VCExpr vcexpr;

-    public Dictionary<Block, VCExprVar> reachVars;

+    public VCExprVar entryExprVar;

+    public Dictionary<Block, Macro> reachMacros;

+    public Dictionary<Block, VCExpr> reachMacroDefinitions;

 

     public StratifiedVC(StratifiedInliningInfo siInfo) {

       info = siInfo;

       info.GenerateVC();

-      vcexpr = info.vcexpr;

       var vcgen = info.vcgen;

       var prover = vcgen.prover;

       VCExpressionGenerator gen = prover.VCExprGen;

-      var bet = prover.Context.BoogieExprTranslator;

-      VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);

+      var bet = prover.Context.BoogieExprTranslator; 

+      

+      vcexpr = info.vcexpr;

       id = vcgen.CreateNewId();

-      VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

-      vcexpr = gen.And(eqExpr, vcexpr);

-

-      var impl = info.impl;

-      reachVars = new Dictionary<Block, VCExprVar>();

-      Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();

-      foreach (Block b in impl.Blocks) {

-        reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);

-        reachExprs[b] = VCExpressionGenerator.False;

-      }

-      foreach (Block currBlock in impl.Blocks) {

-        GotoCmd gotoCmd = currBlock.TransferCmd as GotoCmd;

-        if (gotoCmd == null) continue;

-        foreach (Block successorBlock in gotoCmd.labelTargets) {

-          VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(currBlock.UniqueId)));

-          VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successorBlock.UniqueId)));

-          reachExprs[successorBlock] = gen.Or(reachExprs[successorBlock], gen.And(reachVars[currBlock], controlTransferExpr));

-        }

-      }

-      // The binding for entry block should be left defined;

-      // it will get filled in when the call tree is constructed

-      for (int i = 1; i < impl.Blocks.Count; i++) {

-        Block b = impl.Blocks[i];

-        vcexpr = gen.And(vcexpr, gen.Eq(reachVars[b], reachExprs[b]));

-      }

-

       interfaceExprVars = new List<VCExprVar>();

       Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();

       foreach (VCExprVar v in info.interfaceExprVars) {

@@ -71,15 +47,37 @@ namespace VC {
       foreach (VCExprVar v in info.privateExprVars) {

         substDict.Add(v, vcgen.CreateNewVar(v.Type));

       }

+      substDict.Add(bet.LookupVariable(info.controlFlowVariable), gen.Integer(BigNum.FromInt(id)));

       VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

       SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);

       vcexpr = substVisitor.Mutate(vcexpr, subst);

 

+      var impl = info.impl;

+      reachMacros = new Dictionary<Block, Macro>();

+      reachMacroDefinitions = new Dictionary<Block, VCExpr>();

+      foreach (Block b in impl.Blocks) {

+        reachMacros[b] = vcgen.CreateNewMacro();

+        reachMacroDefinitions[b] = VCExpressionGenerator.False;

+      }

+      entryExprVar = vcgen.CreateNewVar(Microsoft.Boogie.Type.Bool);

+      reachMacroDefinitions[impl.Blocks[0]] = entryExprVar;

+      foreach (Block currBlock in impl.Blocks) {

+        GotoCmd gotoCmd = currBlock.TransferCmd as GotoCmd;

+        if (gotoCmd == null) continue;

+        foreach (Block successorBlock in gotoCmd.labelTargets) {

+          VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(currBlock.UniqueId)));

+          VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successorBlock.UniqueId)));

+          reachMacroDefinitions[successorBlock] = gen.Or(reachMacroDefinitions[successorBlock], gen.And(gen.Function(reachMacros[currBlock]), controlTransferExpr));

+        }

+      }

+

       callSites = new Dictionary<Block, List<StratifiedCallSite>>();

       foreach (Block b in info.callSites.Keys) {

         callSites[b] = new List<StratifiedCallSite>();

         foreach (CallSite cs in info.callSites[b]) {

-          callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

+          VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(b.UniqueId)));

+          VCExpr blockExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.ZERO));

+          callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, gen.Function(reachMacros[cs.block]), blockExpr));

         }

       }

 

@@ -87,7 +85,9 @@ namespace VC {
       foreach (Block b in info.recordProcCallSites.Keys) {

         recordProcCallSites[b] = new List<StratifiedCallSite>();

         foreach (CallSite cs in info.recordProcCallSites[b]) {

-          recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

+          VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(b.UniqueId)));

+          VCExpr blockExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.ZERO));

+          recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, gen.Function(reachMacros[cs.block]), blockExpr));

         }

       }

     }

@@ -121,22 +121,26 @@ namespace VC {
   public class StratifiedCallSite {

     public CallSite callSite;

     public List<VCExpr> interfaceExprs;

-    public VCExprVar reachVar;

+    public VCExpr reachExpr;

+    public VCExpr blockExpr;

 

-    public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {

+    public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, 

+                              VCExpr reachExpression, VCExpr blockExpression) {

       callSite = cs;

       interfaceExprs = new List<VCExpr>();

       foreach (VCExpr v in cs.interfaceExprs) {

         interfaceExprs.Add(substVisitor.Mutate(v, subst));

       }

-      reachVar = reachVars[cs.block];

+      reachExpr = reachExpression;

+      blockExpr = blockExpression;

     }

 

     public VCExpr Attach(StratifiedVC svc) {

       Contract.Assert(interfaceExprs.Count == svc.interfaceExprVars.Count);

       StratifiedInliningInfo info = svc.info;

       VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;

-      VCExpr ret = gen.Eq(reachVar, svc.reachVars[info.impl.Blocks[0]]);

+      // VCExpr ret = gen.Eq(reachExpr, svc.entryExprVar);

+      VCExpr ret = VCExpressionGenerator.True;

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

         ret = gen.And(ret, gen.Eq(interfaceExprs[i], svc.interfaceExprVars[i]));

       }

@@ -157,6 +161,7 @@ namespace VC {
     public ModelViewInfo mvInfo;

     public Dictionary<Block, List<CallSite>> callSites;

     public Dictionary<Block, List<CallSite>> recordProcCallSites;

+    public IEnumerable<Block> sortedBlocks;

     public bool initialized { get; private set; }

 

     public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {

@@ -229,16 +234,16 @@ namespace VC {
       Program program = vcgen.program;

       ProverInterface proverInterface = vcgen.prover;

       vcgen.ConvertCFG2DAG(impl);

-      ModelViewInfo mvInfo;

       vcgen.PassifyImpl(impl, out mvInfo);

 

-      controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

-      impl.LocVars.Add(controlFlowVariable);

-

       VCExpressionGenerator gen = proverInterface.VCExprGen;

       var exprGen = proverInterface.Context.ExprGen;

       var translator = proverInterface.Context.BoogieExprTranslator;

-      VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : translator.LookupVariable(controlFlowVariable);

+      VCExpr controlFlowVariableExpr = null;

+      if (!CommandLineOptions.Clo.UseLabels) {

+        controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

+        controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);

+      }

       vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));

       if (controlFlowVariableExpr != null) {

         VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));

@@ -246,6 +251,18 @@ namespace VC {
         vcexpr = exprGen.And(eqExpr, vcexpr);

       }

 

+      Graph<Block> dag = new Graph<Block>();

+      dag.AddSource(impl.Blocks[0]);

+      foreach (Block b in impl.Blocks) {

+        GotoCmd gtc = b.TransferCmd as GotoCmd;

+        if (gtc != null) {

+          foreach (Block dest in gtc.labelTargets) {

+            dag.AddEdge(b, dest);

+          }

+        }

+      }

+      sortedBlocks = dag.TopologicalSort();

+

       privateExprVars = new List<VCExprVar>();

       foreach (Variable v in impl.LocVars) {

         privateExprVars.Add(translator.LookupVariable(v));

@@ -406,10 +423,16 @@ namespace VC {
       return callSites;

     }

 

-    private int newVarCountForStratifiedInlining = 0;

+    private int macroCountForStratifiedInlining = 0;

+    public Macro CreateNewMacro() {

+      string newName = "StratifiedInliningMacro@" + macroCountForStratifiedInlining.ToString();

+      macroCountForStratifiedInlining++;

+      return new Macro(Token.NoToken, newName, new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));

+    }

+    private int varCountForStratifiedInlining = 0;

     public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

-      string newName = "StratifiedInlining@" + newVarCountForStratifiedInlining.ToString();

-      newVarCountForStratifiedInlining++;

+      string newName = "StratifiedInliningVar@" + varCountForStratifiedInlining.ToString();

+      varCountForStratifiedInlining++;

       Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

       prover.Context.DeclareConstant(newVar, false, null);

       return prover.VCExprGen.Variable(newVar.Name, type);

diff --git a/_admin/Chalice/aste/summary.log b/_admin/Chalice/aste/summary.log
index ade80273..5d8c2a78 100644
--- a/_admin/Chalice/aste/summary.log
+++ b/_admin/Chalice/aste/summary.log
@@ -1,9 +1,9 @@
-# Aste started: 2012-05-25 09:05:16

+# Aste started: 2012-06-04 09:04:51

 # Host id: Boogiebox

 # Configuration: chalice.cfg

 # Task: aste.tasks.chalice.FullBuild

-# [2012-05-25 09:06:05] Chalice revision: 8d9c6d63a543

-[2012-05-25 09:07:29] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"

+# [2012-06-04 09:05:45] Chalice revision: 795dcb79cb27

+[2012-06-04 09:07:10] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"

 

     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:77: case class `class SeqClass' has case class ancestor `class Class'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:111: case class `class TokenClass' has case class ancestor `class Class'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


@@ -11,5 +11,5 @@
     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:141: case class `class TokenType' has case class ancestor `class Type'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:168: case class `class SpecialField' has case class ancestor `class Field'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:227: case class `class SpecialVariable' has case class ancestor `class Variable'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


-[2012-05-25 10:22:31] 0 out of 83 test(s) failed

-# [2012-05-25 10:23:12] Released nightly of Chalice

+[2012-06-04 10:22:15] 0 out of 85 test(s) failed

+# [2012-06-04 10:22:56] Released nightly of Chalice