diff options
| author |  allydonaldson <unknown> | 2013-07-02 23:55:32 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-07-02 23:55:32 +0100 |
| commit | ac1296d77aaa3e678c2fd70402de481b0a20a50f (patch) | |
| tree | 1605f052e1ff85ee069c3aae69153ef269760597 | |
| parent | 5ced6412ed00204204ebd9351dab36e555f2e718 (diff) | |
Fixed bug with unifomity analysis
| -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;
|