Fixes to StagedHoudini

2 files changed, 91 insertions, 12 deletions

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index b477e7de..d75a4b7d 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -12,8 +12,8 @@ namespace Microsoft.Boogie
   public interface IInterproceduralReachabilityGraph {

 

     bool MayReach(Block src, Block dst);

-    void dump();

 

+    void dump();

 

     Block GetNewEntryBlock(string p);

 

@@ -58,7 +58,15 @@ namespace Microsoft.Boogie
           }

         }

       }

-      

+

+      foreach(var n in nodes) {

+        // If there are disconnected nodes, put them into the

+        // graph as self-loops so that every node is represented in

+        // the graph

+        if(!reachabilityGraph.Nodes.Contains(n)) {

+          reachabilityGraph.AddEdge(n, n);

+        }

+      }

     }

 

     private IEnumerable<Block> OriginalProgramBlocks()

@@ -142,10 +150,9 @@ namespace Microsoft.Boogie
         newProcedureExitNodes[impl.Name] = newExit;

         foreach (Block b in impl.Blocks)

         {

-          List<List<Cmd>> partition = PartitionCmdsAccordingToPredicate(b.Cmds, Item => Item is CallCmd);

           Block prev = null;

           int i = 0;

-          foreach (List<Cmd> cmds in partition)

+          foreach (List<Cmd> cmds in SeparateCallCmds(b.Cmds))

           {

             Block newBlock;

             if (prev == null)

@@ -190,16 +197,24 @@ namespace Microsoft.Boogie
       #endregion

     }

 

-    public static List<List<Cmd>> PartitionCmdsAccordingToPredicate(List<Cmd> Cmds, Func<Cmd, bool> Predicate) {

+    private static List<List<Cmd>> SeparateCallCmds(List<Cmd> Cmds) {

       List<List<Cmd>> result = new List<List<Cmd>>();

-      List<Cmd> current = new List<Cmd>();

-      result.Add(current);

-      foreach(Cmd cmd in Cmds) {

-        if(Predicate(cmd) && current.Count > 0) {

-           current = new List<Cmd>();

-           result.Add(current);

+      int currentIndex = 0;

+      while(currentIndex < Cmds.Count) {

+        if(Cmds[currentIndex] is CallCmd) {

+          result.Add(new List<Cmd> { Cmds[currentIndex] });

+          currentIndex++;

+        } else {

+          List<Cmd> nonCallCmds = new List<Cmd>();

+          while(currentIndex < Cmds.Count && !(Cmds[currentIndex] is CallCmd)) {

+            nonCallCmds.Add(Cmds[currentIndex]);

+            currentIndex++;

+          }

+          result.Add(nonCallCmds);

         }

-        current.Add(cmd);

+      }

+      if(result.Count == 0) {

+        result.Add(new List<Cmd>());

       }

       return result;

     }

diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index f5ddc92a..40a750bb 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -33,6 +33,8 @@ namespace Microsoft.Boogie.Houdini
         houdiniInstances[i] = new List<Houdini>();

       }

 

+      BreakApartConjunctionsInAnnotations();

+

       var annotationDependenceAnalyser = new AnnotationDependenceAnalyser(program);

       annotationDependenceAnalyser.Analyse();

       this.plan = annotationDependenceAnalyser.ApplyStages();

@@ -53,6 +55,68 @@ namespace Microsoft.Boogie.Houdini
       }

     }

 

+    private void BreakApartConjunctionsInAnnotations()

+    {

+      // StagedHoudini works on a syntactic basis, so that

+      // if x and y occur in the same annotation, any annotation

+      // referring to either x or y will be in the same stage

+      // as this annotation.  It is thus desirable to separate

+      // conjunctive annotations into multiple annotations,

+      // to reduce these syntactic dependencies.

+

+      foreach(var b in program.Blocks()) {

+        List<Cmd> newCmds = new List<Cmd>();

+        foreach(var c in b.Cmds) {

+          var assertion = c as AssertCmd;

+          if (assertion != null) {

+            foreach(var e in BreakIntoConjuncts(assertion.Expr)) {

+              newCmds.Add(new AssertCmd(assertion.tok, e, assertion.Attributes));

+            }

+          } else {

+            newCmds.Add(c);

+          }

+        }

+        b.Cmds = newCmds;

+      }

+

+      foreach(var proc in program.Procedures) {

+        {

+          var newRequires = new List<Requires>();

+          foreach(var r in proc.Requires) {

+            foreach(var c in BreakIntoConjuncts(r.Condition)) {

+              newRequires.Add(new Requires(r.tok, r.Free, c, r.Comment, r.Attributes));

+            }

+          }

+          proc.Requires = newRequires;

+        }

+        {

+          var newEnsures = new List<Ensures>();

+          foreach(var e in proc.Ensures) {

+            foreach(var c in BreakIntoConjuncts(e.Condition)) {

+              newEnsures.Add(new Ensures(e.tok, e.Free, c, e.Comment, e.Attributes));

+            }

+          }

+          proc.Ensures = newEnsures;

+        }

+      }

+    }

+

+    private List<Expr> BreakIntoConjuncts(Expr expr)

+    {

+      var nary = expr as NAryExpr;

+      if(nary == null) {

+        return new List<Expr> { expr };

+      }

+      var fun = nary.Fun as BinaryOperator;

+      if(fun == null || (fun.Op != BinaryOperator.Opcode.And)) {

+        return new List<Expr> { expr };

+      }

+      var result = new List<Expr>();

+      result.AddRange(BreakIntoConjuncts(nary.Args[0]));

+      result.AddRange(BreakIntoConjuncts(nary.Args[1]));

+      return result;

+    }

+

     private bool NoStages() {

       return plan == null;

     }