From 3b4b2d1ee8b260b450274ee0ad86d0d2d6743210 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 17 Sep 2014 22:43:09 -0700
Subject: fixed a bug in inlining changed the attribute on callee ensures to
 "HoudiniAssume" rather than "assume"

---
 Source/Houdini/Houdini.cs | 109 +++++++++++++++++++++++++++-------------------
 1 file changed, 64 insertions(+), 45 deletions(-)

(limited to 'Source/Houdini/Houdini.cs')

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 7dfa1bc7..d8adf7d3 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -294,10 +294,11 @@ namespace Microsoft.Boogie.Houdini {
   }
 
   public class InlineEnsuresVisitor : ReadOnlyVisitor {
-    public override Ensures VisitEnsures(Ensures ensures) {
-      ensures.Attributes = new QKeyValue(Token.NoToken, "assume", new List<object>(), ensures.Attributes);
-      return base.VisitEnsures(ensures);
-    }
+      public override Ensures VisitEnsures(Ensures ensures)
+      {
+          ensures.Attributes = new QKeyValue(Token.NoToken, "HoudiniAssume", new List<object>(), ensures.Attributes);
+          return base.VisitEnsures(ensures);
+      }
   }
 
   public class Houdini : ObservableHoudini {
@@ -325,54 +326,72 @@ namespace Microsoft.Boogie.Houdini {
       Initialize(program, stats);
     }
 
-    protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stats) {
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Collecting existential constants...");
-      this.houdiniConstants = CollectExistentialConstants();
+    protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stats)
+    {
+        if (CommandLineOptions.Clo.Trace)
+            Console.WriteLine("Collecting existential constants...");
+        this.houdiniConstants = CollectExistentialConstants();
 
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Building call graph...");
-      this.callGraph = Program.BuildCallGraph(program);
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
+        if (CommandLineOptions.Clo.Trace)
+            Console.WriteLine("Building call graph...");
+        this.callGraph = Program.BuildCallGraph(program);
+        if (CommandLineOptions.Clo.Trace)
+            Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
 
-      if (CommandLineOptions.Clo.HoudiniUseCrossDependencies) {
-        if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
-        this.crossDependencies = new CrossDependencies(this.houdiniConstants);
-        this.crossDependencies.Visit(program);
-      }
+        if (CommandLineOptions.Clo.HoudiniUseCrossDependencies)
+        {
+            if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
+            this.crossDependencies = new CrossDependencies(this.houdiniConstants);
+            this.crossDependencies.Visit(program);
+        }
 
-      Inline();
+        Inline();
+        /*
+        {
+            int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+            CommandLineOptions.Clo.PrintUnstructured = 1;
+            using (TokenTextWriter stream = new TokenTextWriter("houdini_inline.bpl"))
+            {
+                program.Emit(stream);
+            }
+            CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+        }
+        */
 
-      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
+        this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
+        this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
 
-      vcgenFailures = new HashSet<Implementation>();
-      Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Beginning VC generation for Houdini...");
-      foreach (Implementation impl in callGraph.Nodes) {
-        try {
-          if (CommandLineOptions.Clo.Trace)
-            Console.WriteLine("Generating VC for {0}", impl.Name);
-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
-          houdiniSessions.Add(impl, session);
-        } catch (VCGenException) {
-          if (CommandLineOptions.Clo.Trace)
-            Console.WriteLine("VC generation failed");
-          vcgenFailures.Add(impl);
+        vcgenFailures = new HashSet<Implementation>();
+        Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+        if (CommandLineOptions.Clo.Trace)
+            Console.WriteLine("Beginning VC generation for Houdini...");
+        foreach (Implementation impl in callGraph.Nodes)
+        {
+            try
+            {
+                if (CommandLineOptions.Clo.Trace)
+                    Console.WriteLine("Generating VC for {0}", impl.Name);
+                HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
+                houdiniSessions.Add(impl, session);
+            }
+            catch (VCGenException)
+            {
+                if (CommandLineOptions.Clo.Trace)
+                    Console.WriteLine("VC generation failed");
+                vcgenFailures.Add(impl);
+            }
         }
-      }
-      this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
+        this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
 
-      if (CommandLineOptions.Clo.ExplainHoudini) {
-        // Print results of ExplainHoudini to a dotty file
-        explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
-        explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
-        foreach (var constant in houdiniConstants)
-          explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
-        explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
-      }
+        if (CommandLineOptions.Clo.ExplainHoudini)
+        {
+            // Print results of ExplainHoudini to a dotty file
+            explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
+            explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
+            foreach (var constant in houdiniConstants)
+                explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
+            explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
+        }
     }
 
     protected void Inline() {
-- 
cgit v1.2.3