fixed a bug in inlining

changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"

3 files changed, 115 insertions, 48 deletions

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 9af18158..47582868 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -35,6 +35,8 @@ namespace Microsoft.Boogie {
 

     protected List<IdentifierExpr>/*!*/ newModifies;

 

+    protected string prefix;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(program != null);

@@ -72,7 +74,7 @@ namespace Microsoft.Boogie {
         currentId = 0;

         inlinedProcLblMap.Add(procName, currentId);

       }

-      return "inline$" + procName + "$" + currentId;

+      return prefix + procName + "$" + currentId;

     }

 

     protected string GetProcVarName(string procName, string formalName) {

@@ -93,12 +95,58 @@ namespace Microsoft.Boogie {
       this.inlineCallback = cb;

       this.newLocalVars = new List<Variable>();

       this.newModifies = new List<IdentifierExpr>();

+      this.prefix = "inline$";

+    }

+

+    protected static void ComputeInlinerPrefix(Implementation impl, Inliner inliner)

+    {

+        foreach (var v in impl.InParams)

+        {

+            if (!v.Name.StartsWith(inliner.prefix)) continue;

+            for (int i = inliner.prefix.Length; i < v.Name.Length; i++)

+            {

+                inliner.prefix = inliner.prefix + "$";

+                if (v.Name[i] != '$') break;

+            }

+            if (inliner.prefix == v.Name)

+            {

+                inliner.prefix = inliner.prefix + "$";

+            }

+        }

+        foreach (var v in impl.OutParams)

+        {

+            if (!v.Name.StartsWith(inliner.prefix)) continue;

+            for (int i = inliner.prefix.Length; i < v.Name.Length; i++)

+            {

+                inliner.prefix = inliner.prefix + "$";

+                if (v.Name[i] != '$') break;

+            }

+            if (inliner.prefix == v.Name)

+            {

+                inliner.prefix = inliner.prefix + "$";

+            }

+        }

+        foreach (var v in impl.LocVars)

+        {

+            if (!v.Name.StartsWith(inliner.prefix)) continue;

+            for (int i = inliner.prefix.Length; i < v.Name.Length; i++)

+            {

+                inliner.prefix = inliner.prefix + "$";

+                if (v.Name[i] != '$') break;

+            }

+            if (inliner.prefix == v.Name)

+            {

+                inliner.prefix = inliner.prefix + "$";

+            }

+        }

     }

 

     protected static void ProcessImplementation(Implementation impl, Inliner inliner) {

       Contract.Requires(impl != null);

       Contract.Requires(impl.Proc != null);

 

+      ComputeInlinerPrefix(impl, inliner);

+

       inliner.newLocalVars.AddRange(impl.LocVars);

       inliner.newModifies.AddRange(impl.Proc.Modifies);

 

@@ -466,7 +514,7 @@ namespace Microsoft.Boogie {
     }

 

     private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {

-      if (QKeyValue.FindBoolAttribute(ens.Attributes, "assume")) {

+      if (QKeyValue.FindBoolAttribute(ens.Attributes, "HoudiniAssume")) {

         return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));

       } else if (ens.Free) {

         return new AssumeCmd(ens.tok, Expr.True); 

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 716456ea..49273f94 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -2412,7 +2412,7 @@ namespace Microsoft.Boogie.Houdini {
                     QKeyValue.FindStringAttribute(ens.Attributes, "post") == null)

                 .Iter(ens => nensures.Add(ens));

                 foreach (Ensures en in nensures)

-                    en.Attributes = removeAttr("assume", en.Attributes);

+                    en.Attributes = removeAttr("HoudiniAssume", en.Attributes);

 

                 proc.Ensures = nensures;

             }

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() {