Started adding support for annotation intrinsics for unstructured programs.

3 files changed, 345 insertions, 325 deletions

diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
index 4d215f24..3d64f8dc 100644
--- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs
+++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
@@ -43,7 +43,7 @@ namespace GPUVerify
                                    new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));

                 }

 

-                if (call.Func.Name.Equals("__at_most_one"))

+                if (call.Func.Name.Equals("__exclusive"))

                 {

                     return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),

                                    new VariableDualiser(2, verifier.uniformityAnalyser, procName)

@@ -85,11 +85,36 @@ namespace GPUVerify
             }

         }

 

+        internal void ProcessCrossThreadInvariants(List<Block> blocks)

+        {

+            foreach (Block b in blocks)

+            {

+                b.Cmds = ProcessCrossThreadInvariants(b.Cmds);

+            }

+        }

+

         private void ProcessCrossThreadInvariants(BigBlock bb)

         {

+            bb.simpleCmds = ProcessCrossThreadInvariants(bb.simpleCmds);

+

+            if (bb.ec is WhileCmd)

+            {

+                WhileCmd whileCmd = bb.ec as WhileCmd;

+                List<PredicateCmd> newInvariants = new List<PredicateCmd>();

+                foreach (PredicateCmd p in whileCmd.Invariants)

+                {

+                    newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));

+                }

+                whileCmd.Invariants = newInvariants;

+                ProcessCrossThreadInvariants(whileCmd.Body);

+            }

+        }

+

+        private CmdSeq ProcessCrossThreadInvariants(CmdSeq cmds)

+        {

             CmdSeq newCommands = new CmdSeq();

 

-            foreach (Cmd c in bb.simpleCmds)

+            foreach (Cmd c in cmds)

             {

                 if (c is AssertCmd)

                 {

@@ -104,20 +129,7 @@ namespace GPUVerify
                     newCommands.Add(c);

                 }

             }

-

-            bb.simpleCmds = newCommands;

-

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd whileCmd = bb.ec as WhileCmd;

-                List<PredicateCmd> newInvariants = new List<PredicateCmd>();

-                foreach (PredicateCmd p in whileCmd.Invariants)

-                {

-                    newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));

-                }

-                whileCmd.Invariants = newInvariants;

-                ProcessCrossThreadInvariants(whileCmd.Body);

-            }

+            return newCommands;

         }

 

     }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 932b9f1f..79a73a29 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -633,8 +633,16 @@ namespace GPUVerify
                 }

                 if (d is Implementation)

                 {

-                    Implementation i = d as Implementation;

-                    new CrossThreadInvariantProcessor(this, i.Name).ProcessCrossThreadInvariants(i.StructuredStmts);

+                    Implementation impl = d as Implementation;

+

+                    if (CommandLineOptions.Unstructured)

+                    {

+                        new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.Blocks);

+                    }

+                    else

+                    {

+                        new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.StructuredStmts);

+                    }

                 }

 

             }

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index dcdb087f..226b05e7 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -1,125 +1,125 @@
-using Graphing;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace Microsoft.Boogie {
-
-public class BlockPredicator {
-
-  Program prog;
-  Implementation impl;
-  Graph<Block> blockGraph;
-
-  bool createCandidateInvariants = true;
-  bool useProcedurePredicates = true;
-
-  Expr returnBlockId;
-
-  LocalVariable curVar, pVar;
-  IdentifierExpr cur, p, fp;
-  Expr pExpr;
-  Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
-    new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
-  Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
-  HashSet<Block> doneBlocks = new HashSet<Block>();
-
-  BlockPredicator(Program p, Implementation i, bool cci, bool upp) {
-    prog = p;
-    impl = i;
-    createCandidateInvariants = cci;
-    useProcedurePredicates = upp;
-  }
-
-  void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
-    if (!useProcedurePredicates && cmd is CallCmd) {
-      var trueBlock = new Block();
-      blocks.Add(trueBlock);
-      trueBlock.Label = block.Label + ".call.true";
-      trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
-      trueBlock.Cmds.Add(cmd);
-
-      var falseBlock = new Block();
-      blocks.Add(falseBlock);
-      falseBlock.Label = block.Label + ".call.false";
-      falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));
-
-      var contBlock = new Block();
-      blocks.Add(contBlock);
-      contBlock.Label = block.Label + ".call.cont";
-
-      block.TransferCmd =
-        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
-      trueBlock.TransferCmd = falseBlock.TransferCmd =
-        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
-      nextBlock = contBlock;
-    } else {
-      PredicateCmd(block.Cmds, cmd);
-      nextBlock = block;
-    }
-  }
-
-  void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
-    if (cmd is AssignCmd) {
-      var aCmd = (AssignCmd)cmd;
-      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
-                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
-                     new NAryExpr(Token.NoToken,
-                       new IfThenElse(Token.NoToken),
-                       new ExprSeq(p, rhs, lhs.AsExpr))))));
-    } else if (cmd is AssertCmd) {
-      var aCmd = (AssertCmd)cmd;
-      if (cmdSeq.Last() is AssignCmd &&
-          cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {
-        // This may be a loop invariant.  Make sure it continues to appear as
-        // the first statement in the block.
-        var assign = cmdSeq.Last();
-        cmdSeq.Truncate(cmdSeq.Length-1);
-        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);
-        cmdSeq.Add(aCmd);
-        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
-        cmdSeq.Add(assign);
-      } else {
-        aCmd.Expr = Expr.Imp(p, aCmd.Expr);
-        cmdSeq.Add(aCmd);
-        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
-      }
-    } else if (cmd is AssumeCmd) {
-      var aCmd = (AssumeCmd)cmd;
-      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
-    } else if (cmd is HavocCmd) {
-      var hCmd = (HavocCmd)cmd;
-      foreach (IdentifierExpr v in hCmd.Vars) {
-        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
-        Contract.Assert(type != null);
-
-        IdentifierExpr havocTempExpr;
-        if (havocVars.ContainsKey(type)) {
-          havocTempExpr = havocVars[type];
-        } else {
-          var havocVar = new LocalVariable(Token.NoToken,
-                             new TypedIdent(Token.NoToken,
-                                            "_HAVOC_" + type.ToString(), type));
-          impl.LocVars.Add(havocVar);
-          havocVars[type] = havocTempExpr =
-            new IdentifierExpr(Token.NoToken, havocVar);
-        }
-        cmdSeq.Add(new HavocCmd(Token.NoToken,
-                                new IdentifierExprSeq(havocTempExpr)));
-        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
-                                    new NAryExpr(Token.NoToken,
-                                      new IfThenElse(Token.NoToken),
-                                      new ExprSeq(p, havocTempExpr, v))));
-      }
-    } else if (cmd is CallCmd) {
-      Debug.Assert(useProcedurePredicates);
-      var cCmd = (CallCmd)cmd;
-      cCmd.Ins.Insert(0, p);
-      cmdSeq.Add(cCmd);
-    }
-    else if (cmd is CommentCmd) {
+using Graphing;

+using System;

+using System.Collections.Generic;

+using System.Diagnostics;

+using System.Diagnostics.Contracts;

+using System.Linq;

+

+namespace Microsoft.Boogie {

+

+public class BlockPredicator {

+

+  Program prog;

+  Implementation impl;

+  Graph<Block> blockGraph;

+

+  bool createCandidateInvariants = true;

+  bool useProcedurePredicates = true;

+

+  Expr returnBlockId;

+

+  LocalVariable curVar, pVar;

+  IdentifierExpr cur, p, fp;

+  Expr pExpr;

+  Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =

+    new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();

+  Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();

+  HashSet<Block> doneBlocks = new HashSet<Block>();

+

+  BlockPredicator(Program p, Implementation i, bool cci, bool upp) {

+    prog = p;

+    impl = i;

+    createCandidateInvariants = cci;

+    useProcedurePredicates = upp;

+  }

+

+  void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {

+    if (!useProcedurePredicates && cmd is CallCmd) {

+      var trueBlock = new Block();

+      blocks.Add(trueBlock);

+      trueBlock.Label = block.Label + ".call.true";

+      trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));

+      trueBlock.Cmds.Add(cmd);

+

+      var falseBlock = new Block();

+      blocks.Add(falseBlock);

+      falseBlock.Label = block.Label + ".call.false";

+      falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));

+

+      var contBlock = new Block();

+      blocks.Add(contBlock);

+      contBlock.Label = block.Label + ".call.cont";

+

+      block.TransferCmd =

+        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));

+      trueBlock.TransferCmd = falseBlock.TransferCmd =

+        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));

+      nextBlock = contBlock;

+    } else {

+      PredicateCmd(block.Cmds, cmd);

+      nextBlock = block;

+    }

+  }

+

+  void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {

+    if (cmd is AssignCmd) {

+      var aCmd = (AssignCmd)cmd;

+      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,

+                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>

+                     new NAryExpr(Token.NoToken,

+                       new IfThenElse(Token.NoToken),

+                       new ExprSeq(p, rhs, lhs.AsExpr))))));

+    } else if (cmd is AssertCmd) {

+      var aCmd = (AssertCmd)cmd;

+      if (cmdSeq.Last() is AssignCmd &&

+          cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {

+        // This may be a loop invariant.  Make sure it continues to appear as

+        // the first statement in the block.

+        var assign = cmdSeq.Last();

+        cmdSeq.Truncate(cmdSeq.Length-1);

+        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);

+        cmdSeq.Add(aCmd);

+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));

+        cmdSeq.Add(assign);

+      } else {

+        aCmd.Expr = Expr.Imp(p, aCmd.Expr);

+        cmdSeq.Add(aCmd);

+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));

+      }

+    } else if (cmd is AssumeCmd) {

+      var aCmd = (AssumeCmd)cmd;

+      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));

+    } else if (cmd is HavocCmd) {

+      var hCmd = (HavocCmd)cmd;

+      foreach (IdentifierExpr v in hCmd.Vars) {

+        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;

+        Contract.Assert(type != null);

+

+        IdentifierExpr havocTempExpr;

+        if (havocVars.ContainsKey(type)) {

+          havocTempExpr = havocVars[type];

+        } else {

+          var havocVar = new LocalVariable(Token.NoToken,

+                             new TypedIdent(Token.NoToken,

+                                            "_HAVOC_" + type.ToString(), type));

+          impl.LocVars.Add(havocVar);

+          havocVars[type] = havocTempExpr =

+            new IdentifierExpr(Token.NoToken, havocVar);

+        }

+        cmdSeq.Add(new HavocCmd(Token.NoToken,

+                                new IdentifierExprSeq(havocTempExpr)));

+        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

+                                    new NAryExpr(Token.NoToken,

+                                      new IfThenElse(Token.NoToken),

+                                      new ExprSeq(p, havocTempExpr, v))));

+      }

+    } else if (cmd is CallCmd) {

+      Debug.Assert(useProcedurePredicates);

+      var cCmd = (CallCmd)cmd;

+      cCmd.Ins.Insert(0, p);

+      cmdSeq.Add(cCmd);

+    }

+    else if (cmd is CommentCmd) {

       // skip

     }

     else if (cmd is StateCmd) {

@@ -132,198 +132,198 @@ public class BlockPredicator {
     }

     else {

       Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

-    }
-  }
-
-  void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {
-    if (cmd is GotoCmd) {
-      var gCmd = (GotoCmd)cmd;
-      var targets = new List<Expr>(
-        gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));
-      if (targets.Count == 1) {
-        PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));
-      } else {
-        PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,
-                                          new IdentifierExprSeq(cur)));
-        PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
-               targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
-      }
-
-      foreach (Block b in gCmd.labelTargets) {
-        if (blockGraph.Predecessors(b).Count() == 1) {
-          if (!doneBlocks.Contains(b)) {
-            var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd);
-            if (assumes.Count() > 0) {
-              foreach (AssumeCmd aCmd in assumes) {
-                cmdSeq.Add(new AssumeCmd(Token.NoToken,
-                                         Expr.Imp(Expr.Eq(cur, blockIds[b]),
-                                         aCmd.Expr)));
-              }
-              b.Cmds =
-                new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());
-            }
-          }
-        }
-      }
-    } else if (cmd is ReturnCmd) {
-      PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));
-    } else {
-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
-    }
-  }
-
-  void PredicateImplementation() {
-    blockGraph = prog.ProcessLoops(impl);
-    var sortedBlocks = blockGraph.LoopyTopSort();
-
-    int blockId = 0;
-    foreach (var block in impl.Blocks)
-      blockIds[block] = Expr.Literal(blockId++);
-    returnBlockId = Expr.Literal(blockId++);
-
-    curVar = new LocalVariable(Token.NoToken,
-                               new TypedIdent(Token.NoToken, "cur",
-                                              Microsoft.Boogie.Type.Int));
-    impl.LocVars.Add(curVar);
-    cur = Expr.Ident(curVar);
-
-    pVar = new LocalVariable(Token.NoToken,
-                             new TypedIdent(Token.NoToken, "p",
-                                            Microsoft.Boogie.Type.Bool));
-    impl.LocVars.Add(pVar);
-    p = Expr.Ident(pVar);
-
-    if (useProcedurePredicates)
-      fp = Expr.Ident(impl.InParams[0]);
-
-    var newBlocks = new List<Block>();
-
-    Block entryBlock = new Block();
-    entryBlock.Label = "entry";
-    entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
-                        CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],
-                                           returnBlockId)));
-    newBlocks.Add(entryBlock);
-
-    var prevBlock = entryBlock;
-    foreach (var n in sortedBlocks) {
-      if (n.Item2) {
-        var backedgeBlock = new Block();
-        newBlocks.Add(backedgeBlock);
-
-        backedgeBlock.Label = n.Item1.Label + ".backedge";
-        backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
-          Expr.Eq(cur, blockIds[n.Item1]),
-          new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
-        backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
-                                                new BlockSeq(n.Item1));
-
-        var tailBlock = new Block();
-        newBlocks.Add(tailBlock);
-
-        tailBlock.Label = n.Item1.Label + ".tail";
-        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
-                                             Expr.Neq(cur, blockIds[n.Item1])));
-
-        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
-                                        new BlockSeq(backedgeBlock, tailBlock));
-        prevBlock = tailBlock;
-      } else {
-        var runBlock = n.Item1;
-        var oldCmdSeq = runBlock.Cmds;
-        runBlock.Cmds = new CmdSeq();
-        newBlocks.Add(runBlock);
-        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
-                                            new BlockSeq(runBlock));
-
-        pExpr = Expr.Eq(cur, blockIds[runBlock]);
-        if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {
-          AddUniformCandidateInvariant(runBlock.Cmds, runBlock);
-          AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock);
-        }
-        runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
-        var transferCmd = runBlock.TransferCmd;
-        foreach (Cmd cmd in oldCmdSeq)
-          PredicateCmd(newBlocks, runBlock, cmd, out runBlock);
-        PredicateTransferCmd(runBlock.Cmds, transferCmd);
-
-        prevBlock = runBlock;
-        doneBlocks.Add(runBlock);
-      }
-    }
-
-    prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
-    impl.Blocks = newBlocks;
-  }
-
-  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
-    if (useProcedurePredicates) {
-      return new NAryExpr(Token.NoToken,
-                 new IfThenElse(Token.NoToken),
-                 new ExprSeq(fp, then, eElse));
-    } else {
-      return then;
-    }
-  }
-
-  private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
-    cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,
-               CreateIfFPThenElse(blockIds[header], returnBlockId)),
-             "uniform loop"));
-  }
-
-  private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {
-    var loopNodes = new HashSet<Block>();
-    foreach (var b in blockGraph.BackEdgeNodes(header))
-      loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));
-    var exits = new HashSet<Expr>();
-    foreach (var ln in loopNodes) {
-      if (ln.TransferCmd is GotoCmd) {
-        var gCmd = (GotoCmd) ln.TransferCmd;
-        foreach (var exit in gCmd.labelTargets.Cast<Block>()
-                                 .Where(b => !loopNodes.Contains(b)))
-          exits.Add(blockIds[exit]);
-      }
-      if (ln.TransferCmd is ReturnCmd)
-        exits.Add(returnBlockId);
-    }
-    var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]),
-                                            (e, exit) => Expr.Or(e, Expr.Eq(cur, exit)));
-    cs.Add(prog.CreateCandidateInvariant(
-             CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)),
-             "non-uniform loop"));
-  }
-
-  public static void Predicate(Program p,
-                               bool createCandidateInvariants = true,
-                               bool useProcedurePredicates = true) {
-    foreach (var decl in p.TopLevelDeclarations.ToList()) {
-      if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {
-        var dwf = (DeclWithFormals)decl;
-        var fpVar = new Formal(Token.NoToken,
-                               new TypedIdent(Token.NoToken, "_P",
-                                              Microsoft.Boogie.Type.Bool),
-                               /*incoming=*/true);
-        dwf.InParams = new VariableSeq(
-          (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
-            .ToArray());
+    }

+  }

+

+  void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {

+    if (cmd is GotoCmd) {

+      var gCmd = (GotoCmd)cmd;

+      var targets = new List<Expr>(

+        gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));

+      if (targets.Count == 1) {

+        PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));

+      } else {

+        PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,

+                                          new IdentifierExprSeq(cur)));

+        PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,

+               targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));

+      }

+

+      foreach (Block b in gCmd.labelTargets) {

+        if (blockGraph.Predecessors(b).Count() == 1) {

+          if (!doneBlocks.Contains(b)) {

+            var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd);

+            if (assumes.Count() > 0) {

+              foreach (AssumeCmd aCmd in assumes) {

+                cmdSeq.Add(new AssumeCmd(Token.NoToken,

+                                         Expr.Imp(Expr.Eq(cur, blockIds[b]),

+                                         aCmd.Expr)));

+              }

+              b.Cmds =

+                new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());

+            }

+          }

+        }

+      }

+    } else if (cmd is ReturnCmd) {

+      PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));

+    } else {

+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

+    }

+  }

+

+  void PredicateImplementation() {

+    blockGraph = prog.ProcessLoops(impl);

+    var sortedBlocks = blockGraph.LoopyTopSort();

+

+    int blockId = 0;

+    foreach (var block in impl.Blocks)

+      blockIds[block] = Expr.Literal(blockId++);

+    returnBlockId = Expr.Literal(blockId++);

+

+    curVar = new LocalVariable(Token.NoToken,

+                               new TypedIdent(Token.NoToken, "cur",

+                                              Microsoft.Boogie.Type.Int));

+    impl.LocVars.Add(curVar);

+    cur = Expr.Ident(curVar);

+

+    pVar = new LocalVariable(Token.NoToken,

+                             new TypedIdent(Token.NoToken, "p",

+                                            Microsoft.Boogie.Type.Bool));

+    impl.LocVars.Add(pVar);

+    p = Expr.Ident(pVar);

+

+    if (useProcedurePredicates)

+      fp = Expr.Ident(impl.InParams[0]);

+

+    var newBlocks = new List<Block>();

+

+    Block entryBlock = new Block();

+    entryBlock.Label = "entry";

+    entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,

+                        CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],

+                                           returnBlockId)));

+    newBlocks.Add(entryBlock);

+

+    var prevBlock = entryBlock;

+    foreach (var n in sortedBlocks) {

+      if (n.Item2) {

+        var backedgeBlock = new Block();

+        newBlocks.Add(backedgeBlock);

+

+        backedgeBlock.Label = n.Item1.Label + ".backedge";

+        backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

+          Expr.Eq(cur, blockIds[n.Item1]),

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

+        backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

+                                                new BlockSeq(n.Item1));

+

+        var tailBlock = new Block();

+        newBlocks.Add(tailBlock);

+

+        tailBlock.Label = n.Item1.Label + ".tail";

+        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

+                                             Expr.Neq(cur, blockIds[n.Item1])));

+

+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

+                                        new BlockSeq(backedgeBlock, tailBlock));

+        prevBlock = tailBlock;

+      } else {

+        var runBlock = n.Item1;

+        var oldCmdSeq = runBlock.Cmds;

+        runBlock.Cmds = new CmdSeq();

+        newBlocks.Add(runBlock);

+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

+                                            new BlockSeq(runBlock));

+

+        pExpr = Expr.Eq(cur, blockIds[runBlock]);

+        if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {

+          AddUniformCandidateInvariant(runBlock.Cmds, runBlock);

+          AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock);

+        }

+        runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));

+        var transferCmd = runBlock.TransferCmd;

+        foreach (Cmd cmd in oldCmdSeq)

+          PredicateCmd(newBlocks, runBlock, cmd, out runBlock);

+        PredicateTransferCmd(runBlock.Cmds, transferCmd);

+

+        prevBlock = runBlock;

+        doneBlocks.Add(runBlock);

+      }

+    }

+

+    prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);

+    impl.Blocks = newBlocks;

+  }

+

+  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {

+    if (useProcedurePredicates) {

+      return new NAryExpr(Token.NoToken,

+                 new IfThenElse(Token.NoToken),

+                 new ExprSeq(fp, then, eElse));

+    } else {

+      return then;

+    }

+  }

+

+  private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {

+    cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,

+               CreateIfFPThenElse(blockIds[header], returnBlockId)),

+             "uniform loop"));

+  }

+

+  private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {

+    var loopNodes = new HashSet<Block>();

+    foreach (var b in blockGraph.BackEdgeNodes(header))

+      loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));

+    var exits = new HashSet<Expr>();

+    foreach (var ln in loopNodes) {

+      if (ln.TransferCmd is GotoCmd) {

+        var gCmd = (GotoCmd) ln.TransferCmd;

+        foreach (var exit in gCmd.labelTargets.Cast<Block>()

+                                 .Where(b => !loopNodes.Contains(b)))

+          exits.Add(blockIds[exit]);

+      }

+      if (ln.TransferCmd is ReturnCmd)

+        exits.Add(returnBlockId);

+    }

+    var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]),

+                                            (e, exit) => Expr.Or(e, Expr.Eq(cur, exit)));

+    cs.Add(prog.CreateCandidateInvariant(

+             CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)),

+             "non-uniform loop"));

+  }

+

+  public static void Predicate(Program p,

+                               bool createCandidateInvariants = true,

+                               bool useProcedurePredicates = true) {

+    foreach (var decl in p.TopLevelDeclarations.ToList()) {

+      if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {

+        var dwf = (DeclWithFormals)decl;

+        var fpVar = new Formal(Token.NoToken,

+                               new TypedIdent(Token.NoToken, "_P",

+                                              Microsoft.Boogie.Type.Bool),

+                               /*incoming=*/true);

+        dwf.InParams = new VariableSeq(

+          (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))

+            .ToArray());

       }

       try {

         var impl = decl as Implementation;

         if (impl != null)

           new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();

       }

-      catch (Program.IrreducibleLoopException) { }
-    }
-  }
-
+      catch (Program.IrreducibleLoopException) { }

+    }

+  }

+

   public static void Predicate(Program p, Implementation impl) {

     try {

       new BlockPredicator(p, impl, false, false).PredicateImplementation();

     }

-    catch (Program.IrreducibleLoopException) { }
-  }
-
-}
-
-}
+    catch (Program.IrreducibleLoopException) { }

+  }

+

+}

+

+}