diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-06 11:29:20 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-06 11:29:20 +0100 |
| commit | 5dcb1f8e4f28db2f449cb318fc8f114e2982cc7c (patch) | |
| tree | d1a47b7f223d2db43fbb589e5f6dddc2d03c3a44 /Source/Predication | |
| parent | 6e773bb7b5dff32ca7ba552b2562ccc18b02fece (diff) | |
| parent | 5fe9141ded93f6eab4e213c1d082b68ac557d81a (diff) | |
merge
Diffstat (limited to 'Source/Predication')
| -rw-r--r-- | Source/Predication/UniformityAnalyser.cs | 47 |
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;
|