Removed unnecessary stage-related attributes from candidate annotations.

5 files changed, 27 insertions, 14 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7622cbdf..2fd442d4 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1287,17 +1287,16 @@ namespace Microsoft.Boogie {
 

     private int invariantGenerationCounter = 0;

 

-    public Constant MakeExistentialBoolean(int StageId) {

+    public Constant MakeExistentialBoolean() {

       Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);

       invariantGenerationCounter++;

       ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });

-      ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) });

       AddTopLevelDeclaration(ExistentialBooleanConstant);

       return ExistentialBooleanConstant;

     }

 

-    public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null, int StageId = 0) {

-      Constant ExistentialBooleanConstant = MakeExistentialBoolean(StageId);

+    public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) {

+      Constant ExistentialBooleanConstant = MakeExistentialBoolean();

       IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);

       PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));

       if (tag != null)

diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
index 70e33581..ab12a47e 100644
--- a/Source/Core/VariableDependenceAnalyser.cs
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -429,7 +429,7 @@ namespace Microsoft.Boogie {
       Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps = new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();

 

       // Work out and union together local control dependences

-      foreach (var Impl in prog.Implementations) {

+      foreach (var Impl in prog.NonInlinedImplementations()) {

         Graph<Block> blockGraph = prog.ProcessLoops(Impl);

         LocalCtrlDeps[Impl] = blockGraph.ControlDependence();

         foreach (var KeyValue in LocalCtrlDeps[Impl]) {

@@ -440,7 +440,7 @@ namespace Microsoft.Boogie {
       Graph<Implementation> callGraph = Program.BuildCallGraph(prog);

 

       // Add inter-procedural control dependence nodes based on calls

-      foreach (var Impl in prog.Implementations) {

+      foreach (var Impl in prog.NonInlinedImplementations()) {

         foreach (var b in Impl.Blocks) {

           foreach (var cmd in b.Cmds.OfType<CallCmd>()) {

             var DirectCallee = GetImplementation(cmd.callee);

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ae833dbf..90da808a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1361,10 +1361,8 @@ namespace Microsoft.Boogie
     private static PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)

     {

       Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();

-      // TODO - pass this in somewhere

-

-      Houdini.StagedHoudini houdini = new Houdini.StagedHoudini(program, ProgramFromFile);

-      Houdini.HoudiniOutcome outcome = houdini.PerformStagedHoudiniInference();

+      Houdini.StagedHoudini stagedHoudini = new Houdini.StagedHoudini(program, houdiniStats, ProgramFromFile);

+      Houdini.HoudiniOutcome outcome = stagedHoudini.PerformStagedHoudiniInference();

 

       if (CommandLineOptions.Clo.PrintAssignment)

       {

diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs
index fd283f3e..7cb43fbd 100644
--- a/Source/Houdini/AnnotationDependenceAnalyser.cs
+++ b/Source/Houdini/AnnotationDependenceAnalyser.cs
@@ -436,8 +436,9 @@ namespace Microsoft.Boogie.Houdini {
 

         if (NoStages())

         {

-          // TODO: need to figure out what to do here

-          throw new NotImplementedException();

+          var TrivialGraph = new Graph<ScheduledStage>();

+          TrivialGraph.AddSource(new ScheduledStage(0, new HashSet<string>()));

+          return new StagedHoudiniPlan(TrivialGraph);

         }

 

         #region Assign annotations to stages at a given level of granularity

diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index 49482b3d..f5ddc92a 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -15,6 +15,7 @@ namespace Microsoft.Boogie.Houdini
   {

 

     private Program program;

+    private HoudiniSession.HoudiniStatistics houdiniStats;

     private Func<string, Program> ProgramFromFile;

     private StagedHoudiniPlan plan;

     private List<Houdini>[] houdiniInstances;

@@ -23,8 +24,9 @@ namespace Microsoft.Boogie.Houdini
 

     private const string tempFilename = "__stagedHoudiniTemp.bpl";

 

-    public StagedHoudini(Program program, Func<string, Program> ProgramFromFile) {

+    public StagedHoudini(Program program, HoudiniSession.HoudiniStatistics houdiniStats, Func<string, Program> ProgramFromFile) {

       this.program = program;

+      this.houdiniStats = houdiniStats;

       this.ProgramFromFile = ProgramFromFile;

       this.houdiniInstances = new List<Houdini>[CommandLineOptions.Clo.StagedHoudiniThreads];

       for (int i = 0; i < CommandLineOptions.Clo.StagedHoudiniThreads; i++) {

@@ -40,16 +42,29 @@ namespace Microsoft.Boogie.Houdini
 

         if(CommandLineOptions.Clo.DebugStagedHoudini) {

           Console.WriteLine("Plan\n====\n");

-          Console.WriteLine(this.plan);

+          if(plan == null) {

+            Console.WriteLine("No plan, as there were no stages");

+          } else {

+            Console.WriteLine(this.plan);

+          }

         }

         

         EmitProgram("staged.bpl");

       }

     }

 

+    private bool NoStages() {

+      return plan == null;

+    }

+

     public HoudiniOutcome PerformStagedHoudiniInference()

     {

 

+      if (NoStages()) {

+        Houdini houdini = new Houdini(program, houdiniStats);

+        return houdini.PerformHoudiniInference();

+      }

+

       EmitProgram(tempFilename);

 

       #region Prepare the tasks, but do not launch them