From bf65ebf6145df56f3198dbed788f6dd3058f3507 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 19 Sep 2014 15:55:19 -0700
Subject: a bug fix in Houdini (also AbsHoudini)

---
 Source/Core/Inline.cs | 75 +++++++++++++++++++++------------------------------
 1 file changed, 30 insertions(+), 45 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index fe61a765..d6707f1f 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -69,21 +69,14 @@ namespace Microsoft.Boogie {
     protected string GetInlinedProcLabel(string procName) {
       Contract.Requires(procName != null);
       Contract.Ensures(Contract.Result<string>() != null);
-      int currentId;
-      if (!inlinedProcLblMap.TryGetValue(procName, out currentId)) {
-        currentId = 0;
-        inlinedProcLblMap.Add(procName, currentId);
-      }
-      return prefix + procName + "$" + currentId;
+      return prefix + procName + "$" + inlinedProcLblMap[procName];
     }
 
     protected string GetProcVarName(string procName, string formalName) {
       Contract.Requires(formalName != null);
       Contract.Requires(procName != null);
       Contract.Ensures(Contract.Result<string>() != null);
-      string/*!*/ prefix = GetInlinedProcLabel(procName);
-      Contract.Assert(prefix != null);
-      return prefix + "$" + formalName;
+      return GetInlinedProcLabel(procName) + "$" + formalName;
     }
 
     public Inliner(Program program, InlineCallback cb, int inlineDepth) {
@@ -95,59 +88,51 @@ namespace Microsoft.Boogie {
       this.inlineCallback = cb;
       this.newLocalVars = new List<Variable>();
       this.newModifies = new List<IdentifierExpr>();
-      this.prefix = "inline$";
+      this.prefix = null;
     }
 
     // This method updates inliner.prefix so that prepending it to any string is guaranteed 
     // not to create a conflict with any of the in/out/local variables of impl
-    protected static void ComputeInlinerPrefix(Implementation impl, Inliner inliner)
+    protected void ComputePrefix(Program program, Implementation impl)
     {
+        this.prefix = "inline$";
         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 + "$";
-            }
+            DistinguishPrefix(v);
         }
         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 + "$";
-            }
+            DistinguishPrefix(v);
         }
         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 + "$";
-            }
+            DistinguishPrefix(v);
+        }
+        foreach (var v in program.GlobalVariables())
+        {
+            DistinguishPrefix(v);
+        }
+    }
+
+    private void DistinguishPrefix(Variable v)
+    {
+        if (!v.Name.StartsWith(prefix)) return;
+        for (int i = prefix.Length; i < v.Name.Length; i++)
+        {
+            prefix = prefix + "$";
+            if (v.Name[i] != '$') break;
+        }
+        if (prefix == v.Name)
+        {
+            prefix = prefix + "$";
         }
     }
 
-    protected static void ProcessImplementation(Implementation impl, Inliner inliner) {
+    protected static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) {
       Contract.Requires(impl != null);
       Contract.Requires(impl.Proc != null);
 
-      ComputeInlinerPrefix(impl, inliner);
+      inliner.ComputePrefix(program, impl);
 
       inliner.newLocalVars.AddRange(impl.LocVars);
       inliner.newModifies.AddRange(impl.Proc.Modifies);
@@ -179,14 +164,14 @@ namespace Microsoft.Boogie {
       Contract.Requires(impl != null);
       Contract.Requires(program != null);
       Contract.Requires(impl.Proc != null);
-      ProcessImplementation(impl, new Inliner(program, null, CommandLineOptions.Clo.InlineDepth));
+      ProcessImplementation(program, impl, new Inliner(program, null, CommandLineOptions.Clo.InlineDepth));
     }
 
     public static void ProcessImplementation(Program program, Implementation impl) {
       Contract.Requires(impl != null);
       Contract.Requires(program != null);
       Contract.Requires(impl.Proc != null);
-      ProcessImplementation(impl, new Inliner(program, null, -1));
+      ProcessImplementation(program, impl, new Inliner(program, null, -1));
     }
 
     protected void EmitImpl(Implementation impl) {
-- 
cgit v1.2.3