summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar allydonaldson <unknown>2013-07-02 23:55:32 +0100
committerGravatar allydonaldson <unknown>2013-07-02 23:55:32 +0100
commitac1296d77aaa3e678c2fd70402de481b0a20a50f (patch)
tree1605f052e1ff85ee069c3aae69153ef269760597
parent5ced6412ed00204204ebd9351dab36e555f2e718 (diff)
Fixed bug with unifomity analysis
-rw-r--r--Source/Predication/UniformityAnalyser.cs47
1 files changed, 32 insertions, 15 deletions
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;