Adapted Houdini algorithm to take staging into account

4 files changed, 277 insertions, 73 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 3e2b83de..a52d7f53 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -220,10 +220,12 @@ namespace Microsoft.Boogie {
               candidateDependenceAnalyser.ApplyStages();

               if (CommandLineOptions.Clo.Trace)

               {

-                  candidateDependenceAnalyser.dump();

+                candidateDependenceAnalyser.dump();

+                int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

+                CommandLineOptions.Clo.PrintUnstructured = 2;

+                PrintBplFile("staged.bpl", program, false, false);

+                CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

               }

-              PrintBplFile("staged.bpl", program, false, false);

-              Environment.Exit(0);

           }

 

           int errorCount, verified, inconclusives, timeOuts, outOfMemories;

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index a7083497..959eff1e 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -256,90 +256,194 @@ namespace Microsoft.Boogie {
 

     public void ApplyStages() {

 

-      IEnumerable<Constant> candidates = prog.TopLevelDeclarations.OfType<Constant>().

-        Where(Item => QKeyValue.FindBoolAttribute(Item.Attributes, "existential"));

-

-      if (candidates.Count() == 0) {

-        return;

-      }

-

-      if (StagesDAG.Nodes.Count() == 0) {

-        return;

-      }

+        if (NoStages())

+        {

+            return;

+        }

 

-      

-      Debug.Assert(CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES ||

+        #region Assign candidates to stages at a given level of granularity

+        Debug.Assert(CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES ||

                    CommandLineOptions.Clo.StagedHoudini == FINE_STAGES);

-

-      if (CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES) {

-        SCC<string> start = null;

-        foreach (var n in StagesDAG.Nodes) {

-          if (StagesDAG.Successors(n).Count() == 0) {

-            start = n;

-            break;

-          }

+        Dictionary<string, int> candidateToStage =

+            (CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES) ? ComputeCoarseStages()

+            : ComputeFineStages();

+        #endregion

+

+        #region Generate boolean variables to control stages

+        var stageToActiveBoolean = new Dictionary<int, Constant>();

+        var stageToCompleteBoolean = new Dictionary<int, Constant>();

+

+        foreach (var stage in new HashSet<int>(candidateToStage.Values))

+        {

+            var stageActive = new Constant(Token.NoToken,

+                new TypedIdent(Token.NoToken, "_stage_" + stage + "_active", Type.Bool),

+                false);

+            stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage)) });

+            prog.TopLevelDeclarations.Add(stageActive);

+            stageToActiveBoolean[stage] = stageActive;

+

+            var stageComplete = new Constant(Token.NoToken, 

+                new TypedIdent(Token.NoToken, "_stage_" + stage + "_complete", Type.Bool),

+                false);

+            stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage)) });

+            prog.TopLevelDeclarations.Add(stageComplete);

+            stageToCompleteBoolean[stage] = stageComplete;

         }

-        System.Diagnostics.Debug.Assert(start != null);

-

-        HashSet<SCC<string>> done = new HashSet<SCC<string>>();

-        done.Add(start);

-

-        bool finished = false;

-        int stageId = 0;

-        while (!finished) {

-          finished = true;

-          HashSet<SCC<string>> stage = new HashSet<SCC<string>>();

-          foreach (var n in StagesDAG.Nodes) {

-            if (!done.Contains(n)) {

-              finished = false;

-              bool ready = true;

-              foreach (var m in StagesDAG.Successors(n)) {

-                if (!done.Contains(m)) {

-                  ready = false;

-                  break;

+        #endregion

+

+        #region Adapt candidate assertions to take account of stages

+        foreach (var b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item))

+        {

+            CmdSeq newCmds = new CmdSeq();

+            foreach (var cmd in b.Cmds)

+            {

+                var a = cmd as AssertCmd;

+                string c;

+                if (a != null && (Houdini.Houdini.MatchCandidate(a.Expr, candidates, out c)))

+                {

+                    newCmds.Add(new AssertCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr,

+                        new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c), a.Attributes));

+                    newCmds.Add(new AssumeCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr,

+                        new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c), a.Attributes));

+                }

+                else

+                {

+                    newCmds.Add(cmd);

                 }

-              }

-              if (ready) {

-                stage.Add(n);

-                done.Add(n);

-              }

+            }

+            b.Cmds = newCmds;

+        }

+        #endregion

+

+        #region Adapt candidate pre/postconditions to take account of stages

+        foreach (var p in prog.TopLevelDeclarations.OfType<Procedure>())

+        {

+

+          #region Handle the preconditions

+          RequiresSeq newRequires = new RequiresSeq();

+          foreach(Requires r in p.Requires) {

+            string c;

+            if (Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) {

+              newRequires.Add(new Requires(r.tok, false, 

+                Houdini.Houdini.AddConditionToCandidate(r.Condition,

+                new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c),

+                r.Comment, r.Attributes));

+              newRequires.Add(new Requires(r.tok, true, 

+                Houdini.Houdini.AddConditionToCandidate(r.Condition,

+                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c),

+                r.Comment, r.Attributes));

+            } else {

+              newRequires.Add(r);

             }

           }

-

-          foreach (var scc in stage) {

-            foreach (var candidate in candidates) {

-              if (scc.Contains(candidate.Name)) {

-                candidate.Attributes = new QKeyValue(Token.NoToken, "stage_id", new List<object>() {

-                  new LiteralExpr(Token.NoToken, BigNum.FromInt(stageId))

-                }, candidate.Attributes);

-              }

+          p.Requires = newRequires;

+          #endregion

+

+          #region Handle the postconditions

+          EnsuresSeq newEnsures = new EnsuresSeq();

+          foreach(Ensures e in p.Ensures) {

+            string c;

+            if (Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {

+              newEnsures.Add(new Ensures(e.tok, false, 

+                Houdini.Houdini.AddConditionToCandidate(e.Condition,

+                new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c),

+                e.Comment, e.Attributes));

+              newEnsures.Add(new Ensures(e.tok, true, 

+                Houdini.Houdini.AddConditionToCandidate(e.Condition,

+                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c),

+                e.Comment, e.Attributes));

+            } else {

+              newRequires.Add(e);

             }

           }

+          p.Ensures = newEnsures;

+          #endregion

 

-          stageId++;

         }

+        #endregion

 

-      }

-      else {

+    }

+

+    private Dictionary<string, int> ComputeFineStages()

+    {

+        var result = new Dictionary<string, int>();

         List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();

         components.Reverse();

 

         System.Diagnostics.Debug.Assert(components[0].Count() == 0);

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

-          foreach (var c in candidates) {

-            if (components[i].Contains(c.Name)) {

-              c.Attributes = new QKeyValue(Token.NoToken, "stage_id", new List<object>() {

-              new LiteralExpr(Token.NoToken, BigNum.FromInt(i - 1))

-            }, c.Attributes);

+        for (int i = 1; i < components.Count(); i++)

+        {

+            foreach (var c in components[i])

+            {

+                result[c] = i - 1;

             }

-          }

 

         }

+        return result;

 

-      }

+    }

 

+    private Dictionary<string, int> ComputeCoarseStages()

+    {

+        var result = new Dictionary<string, int>();

+        SCC<string> start = null;

+        foreach (var n in StagesDAG.Nodes)

+        {

+            if (StagesDAG.Successors(n).Count() == 0)

+            {

+                start = n;

+                break;

+            }

+        }

+        System.Diagnostics.Debug.Assert(start != null);

+

+        HashSet<SCC<string>> done = new HashSet<SCC<string>>();

+        done.Add(start);

 

+        bool finished = false;

+        int stageId = 0;

+        while (!finished)

+        {

+            finished = true;

+            HashSet<SCC<string>> stage = new HashSet<SCC<string>>();

+            foreach (var n in StagesDAG.Nodes)

+            {

+                if (!done.Contains(n))

+                {

+                    finished = false;

+                    bool ready = true;

+                    foreach (var m in StagesDAG.Successors(n))

+                    {

+                        if (!done.Contains(m))

+                        {

+                            ready = false;

+                            break;

+                        }

+                    }

+                    if (ready)

+                    {

+                        stage.Add(n);

+                        done.Add(n);

+                    }

+                }

+            }

+

+            foreach (var scc in stage)

+            {

+                foreach (var c in scc)

+                {

+                    result[c] = stageId;

+                }

+            }

+

+            stageId++;

+        }

+        return result;

+    }

 

+    private bool NoStages()

+    {

+        return candidates.Count() == 0 || StagesDAG.Nodes.Count() == 0;

     }

   }

 

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 940b355f..b5775424 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -212,6 +212,7 @@ namespace Microsoft.Boogie.Houdini {
         }

       }

        */

+

       return expr;

     }

 

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index a39f4fdb..4f1e2a8b 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -38,6 +38,7 @@ namespace Microsoft.Boogie.Houdini {
 

   public abstract class HoudiniObserver {

     public virtual void UpdateStart(Program program, int numConstants) { }

+    public virtual void UpdateStage(int stage) { }

     public virtual void UpdateIteration() { }

     public virtual void UpdateImplementation(Implementation implementation) { }

     public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment) { }

@@ -132,6 +133,10 @@ namespace Microsoft.Boogie.Houdini {
       currentIteration = -1;

       wr.Flush();

     }

+    public override void UpdateStage(int stage) {

+      wr.WriteLine("Houdini stage " + stage);

+      wr.Flush();

+    }

     public override void UpdateIteration() {

       currentIteration++;

       wr.WriteLine("---------------------------------------");

@@ -210,6 +215,9 @@ namespace Microsoft.Boogie.Houdini {
       NotifyDelegate notifyDelegate = (NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStart(program, numConstants); };

       Notify(notifyDelegate);

     }

+    protected void NotifyStage(int stage) {

+      Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStage(stage); });

+    }

     protected void NotifyIteration() {

       Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateIteration(); });

     }

@@ -540,6 +548,38 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

+    private static Expr AddConditionToCandidateRec(Expr boogieExpr, Expr condition, string candidateConstant, List<Expr> implicationStack)

+    {

+        NAryExpr e = boogieExpr as NAryExpr;

+        if (e != null && e.Fun is BinaryOperator && ((BinaryOperator)e.Fun).Op == BinaryOperator.Opcode.Imp)

+        {

+            Expr antecedent = e.Args[0];

+            Expr consequent = e.Args[1];

+

+            IdentifierExpr id = antecedent as IdentifierExpr;

+            if (id != null && id.Decl is Constant && id.Decl.Name.Equals(candidateConstant))

+            {

+                Expr result = Expr.Imp(antecedent, Expr.Imp(condition, consequent));

+                implicationStack.Reverse();

+                foreach (var expr in implicationStack)

+                {

+                    result = Expr.Imp(expr, result);

+                }

+                return result;

+            }

+

+            implicationStack.Add(antecedent);

+            return AddConditionToCandidateRec(consequent, condition, candidateConstant,

+                implicationStack);

+        }

+        return boogieExpr;

+    }

+

+    public static Expr AddConditionToCandidate(Expr boogieExpr, Expr condition, string candidateConstant)

+    {

+        return AddConditionToCandidateRec(boogieExpr, condition, candidateConstant, new List<Expr>());

+    }

+

     public bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) {

       candidateConstant = null;

       string candidateString;

@@ -761,12 +801,14 @@ namespace Microsoft.Boogie.Houdini {
       private WorkQueue _workQueue;

       private HashSet<string> blackList;

       private Dictionary<Variable, bool> _assignment;

+      private int _stage;

       private Implementation _implementation;

       private HoudiniOutcome _outcome;

 

       public HoudiniState(WorkQueue workQueue, Dictionary<Variable, bool> currentAssignment) {

         this._workQueue = workQueue;

         this._assignment = currentAssignment;

+        this._stage = 0;

         this._implementation = null;

         this._outcome = new HoudiniOutcome();

         this.blackList = new HashSet<string>();

@@ -778,6 +820,9 @@ namespace Microsoft.Boogie.Houdini {
       public Dictionary<Variable, bool> Assignment {

         get { return this._assignment; }

       }

+      public int Stage {

+        get { return this._stage; }

+      }

       public Implementation Implementation {

         get { return this._implementation; }

         set { this._implementation = value; }

@@ -791,6 +836,9 @@ namespace Microsoft.Boogie.Houdini {
       public void addToBlackList(string funcName) {

         blackList.Add(funcName);

       }

+      internal void incrementStage() {

+        _stage++;

+      }

     }

 

     public HoudiniOutcome PerformHoudiniInference() {

@@ -799,15 +847,36 @@ namespace Microsoft.Boogie.Houdini {
         currentHoudiniState.addToBlackList(impl.Name);

       }

 

-      while (currentHoudiniState.WorkQueue.Count > 0) {

-        this.NotifyIteration();

+      while(currentHoudiniState.Stage < NumberOfStages()) {

 

-        currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();

-        this.NotifyImplementation(currentHoudiniState.Implementation);

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("Current stage is " + currentHoudiniState.Stage + " of " + (NumberOfStages() - 1));

+        }

+

+        this.NotifyStage(currentHoudiniState.Stage);

+

+        while (currentHoudiniState.WorkQueue.Count > 0) {

+          this.NotifyIteration();

+

+          currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();

+          this.NotifyImplementation(currentHoudiniState.Implementation);

+

+          HoudiniSession session;

+          this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);

+          HoudiniVerifyCurrent(session);

+        }

+

+        currentHoudiniState.incrementStage();

+

+        #region Re-populate work list for next stage

+        if (currentHoudiniState.Stage < NumberOfStages()) {

+          var workList = BuildWorkList(program);

+          while(workList.Count > 0) {

+            currentHoudiniState.WorkQueue.Enqueue(workList.Dequeue());

+          }

+        }

+        #endregion

 

-        HoudiniSession session;

-        this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);

-        HoudiniVerifyCurrent(session);

       }

       this.NotifyEnd(true);

       Dictionary<string, bool> assignment = new Dictionary<string, bool>();

@@ -824,6 +893,15 @@ namespace Microsoft.Boogie.Houdini {
       return currentHoudiniState.Outcome;

     }

 

+    private int NumberOfStages()

+    {

+      int result = 1;

+      foreach(var c in program.TopLevelDeclarations.OfType<Constant>()) {

+        result = Math.Max(result, 1 + QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1));

+      }

+      return result;

+    }

+

     private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {

       HoudiniSession session;

       List<Implementation> implementations = new List<Implementation>();

@@ -970,7 +1048,7 @@ namespace Microsoft.Boogie.Houdini {
     private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, out List<Counterexample> errors) {

       ProverInterface.Outcome outcome;

       try {

-        outcome = session.Verify(proverInterface, currentHoudiniState.Assignment, out errors);

+        outcome = session.Verify(proverInterface, GetAssignmentWithStages(), out errors);

       }

       catch (UnexpectedProverOutputException upo) {

         Contract.Assume(upo != null);

@@ -980,6 +1058,25 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;

     }

 

+    private Dictionary<Variable, bool> GetAssignmentWithStages()

+    {

+      Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);

+      foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

+      {

+        int stageActive = QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1);

+        if (stageActive != -1)

+        {

+          result[c] = (stageActive == currentHoudiniState.Stage);

+        }

+        int stageComplete = QKeyValue.FindIntAttribute(c.Attributes, "stage_complete", -1);

+        if (stageComplete != -1)

+        {

+          result[c] = (stageComplete < currentHoudiniState.Stage);

+        }

+      }

+      return result;

+    }

+

     private void HoudiniVerifyCurrent(HoudiniSession session) {

       while (true) {

         this.NotifyAssignment(currentHoudiniState.Assignment);