From ac1296d77aaa3e678c2fd70402de481b0a20a50f Mon Sep 17 00:00:00 2001
From: allydonaldson <unknown>
Date: Tue, 2 Jul 2013 23:55:32 +0100
Subject: Fixed bug with unifomity analysis

---
 Source/Predication/UniformityAnalyser.cs | 47 ++++++++++++++++++++++----------
 1 file changed, 32 insertions(+), 15 deletions(-)

(limited to 'Source/Predication')

diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index 2e0f4074..ca5a0df6 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -232,6 +232,17 @@ namespace Microsoft.Boogie
                       SetNonUniform(Impl.Name, v.Name);
                   }
                 }
+
+                foreach (Block b in Impl.Blocks) {
+                  foreach (Cmd c in b.Cmds) {
+                    CallCmd callCmd = c as CallCmd;
+                    if (callCmd != null) {
+                      if (IsUniform(callCmd.callee)) {
+                        SetNonUniform(callCmd.callee);
+                      }
+                    }
+                  }
+                }
                         
                 return;
             }
@@ -243,6 +254,12 @@ namespace Microsoft.Boogie
             ctrlDep.TransitiveClosure();
 
             var nonUniformBlockSet = new HashSet<Block>();
+            /*// If procedure is non-uniform, so are all of its blocks
+            if (!uniformityInfo[Impl.Name].Key) {
+              foreach (var block in Impl.Blocks) {
+                nonUniformBlockSet.Add(block);
+              }
+            }*/
             nonUniformBlocks[Impl.Name] = nonUniformBlockSet;
 
             bool changed;
@@ -314,32 +331,32 @@ namespace Microsoft.Boogie
                     DeclWithFormals Callee = GetProcedure(callCmd.callee);
                     Debug.Assert(Callee != null);
 
-                        if (!ControlFlowIsUniform)
+                    if (!ControlFlowIsUniform)
+                    {
+                        if (IsUniform(callCmd.callee))
                         {
-                            if (IsUniform(callCmd.callee))
-                            {
-                                SetNonUniform(callCmd.callee);
-                            }
+                            SetNonUniform(callCmd.callee);
                         }
+                    }
                     for (int i = 0; i < Callee.InParams.Length; i++)
-                        {
+                    {
                         if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
-                                && !IsUniform(impl.Name, callCmd.Ins[i]))
-                            {
+                            && !IsUniform(impl.Name, callCmd.Ins[i]))
+                        {
                             SetNonUniform(callCmd.callee, Callee.InParams[i].Name);
-                            }
                         }
+                    }
 
                     for (int i = 0; i < Callee.OutParams.Length; i++)
+                    {
+                        if (IsUniform(impl.Name, callCmd.Outs[i].Name)
+                        && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
                         {
-                            if (IsUniform(impl.Name, callCmd.Outs[i].Name)
-                            && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
-                            {
-                                SetNonUniform(impl.Name, callCmd.Outs[i].Name);
-                            }
+                            SetNonUniform(impl.Name, callCmd.Outs[i].Name);
                         }
-
                     }
+
+                }
                 else if (c is AssumeCmd)
                 {
                     var ac = (AssumeCmd)c;
-- 
cgit v1.2.3