diff options
| author |  Unknown <afd@afd-THINK.doc.ic.ac.uk> | 2012-04-05 10:20:57 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.doc.ic.ac.uk> | 2012-04-05 10:20:57 +0100 |
| commit | 7860cf038c2a5d6d535f6be3ff461ae8e62db51c (patch) | |
| tree | 6938d9a3f50bf1c39551f9d602e24a1080292b6a /Source/GPUVerify | |
| parent | 562ea75667e8eabf6703eb62b8716a920b2c02c6 (diff) | |
Started generalising thread id inference
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/ArrayControlFlowAnalyser.cs | 264 | ||||
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 28 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs | 262 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeTidAnalyser.cs | 220 | ||||
| -rw-r--r-- | Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 2 |
8 files changed, 545 insertions, 239 deletions
diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs new file mode 100644 index 00000000..bb51ae64 --- /dev/null +++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs @@ -0,0 +1,264 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class ArrayControlFlowAnalyser
+ {
+ private GPUVerifier verifier;
+
+ private bool ProcedureChanged;
+
+ private Dictionary<string, Dictionary<string, HashSet<string>>> mayBeDerivedFrom;
+
+ private HashSet<string> arraysWhichMayAffectControlFlow;
+
+ public ArrayControlFlowAnalyser(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ mayBeDerivedFrom = new Dictionary<string, Dictionary<string, HashSet<string>>>();
+ arraysWhichMayAffectControlFlow = new HashSet<string>();
+ }
+
+ internal void Analyse()
+ {
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation)
+ {
+ Implementation Impl = D as Implementation;
+ mayBeDerivedFrom.Add(Impl.Name, new Dictionary<string, HashSet<string>>());
+
+ SetNotDerivedFromSharedState(Impl.Name, GPUVerifier._X.Name);
+ SetNotDerivedFromSharedState(Impl.Name, GPUVerifier._Y.Name);
+ SetNotDerivedFromSharedState(Impl.Name, GPUVerifier._Z.Name);
+
+ foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())
+ {
+ SetMayBeDerivedFrom(Impl.Name, v.Name, v.Name);
+ }
+
+ foreach (Variable v in Impl.LocVars)
+ {
+ SetNotDerivedFromSharedState(Impl.Name, v.Name);
+ }
+
+ foreach (Variable v in Impl.InParams)
+ {
+ SetNotDerivedFromSharedState(Impl.Name, v.Name);
+ }
+
+ foreach (Variable v in Impl.OutParams)
+ {
+ SetNotDerivedFromSharedState(Impl.Name, v.Name);
+ }
+
+ ProcedureChanged = true;
+ }
+ }
+
+ while (ProcedureChanged)
+ {
+ ProcedureChanged = false;
+
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation)
+ {
+ Implementation Impl = D as Implementation;
+ Analyse(Impl);
+ }
+ }
+ }
+
+ if (CommandLineOptions.ShowArrayControlFlowAnalysis)
+ {
+ dump();
+ }
+ }
+
+ private void SetNotDerivedFromSharedState(string p, string v)
+ {
+ mayBeDerivedFrom[p][v] = new HashSet<string>();
+ }
+
+ private void SetMayBeDerivedFrom(string p, string v, string w)
+ {
+ if (!mayBeDerivedFrom[p].ContainsKey(v))
+ {
+ mayBeDerivedFrom[p][v] = new HashSet<string>();
+ }
+ Debug.Assert(!mayBeDerivedFrom[p][v].Contains(w));
+ mayBeDerivedFrom[p][v].Add(w);
+ ProcedureChanged = true;
+ }
+
+ private void Analyse(Implementation Impl)
+ {
+ Analyse(Impl, Impl.StructuredStmts);
+ }
+
+ private void Analyse(Implementation impl, StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ Analyse(impl, bb);
+ }
+ }
+
+ private void Analyse(Implementation impl, BigBlock bb)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is AssignCmd)
+ {
+ AssignCmd assignCmd = c as AssignCmd;
+ Debug.Assert(assignCmd.Lhss.Count == 1);
+ Debug.Assert(assignCmd.Rhss.Count == 1);
+ if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ {
+ SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[0];
+
+ VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
+ visitor.VisitExpr(rhs);
+
+ foreach (Variable v in visitor.GetVariables())
+ {
+ if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))
+ {
+ continue;
+ }
+ foreach (String s in mayBeDerivedFrom[impl.Name][v.Name])
+ {
+ if (!mayBeDerivedFrom[impl.Name][lhs.AssignedVariable.Name].Contains(s))
+ {
+ SetMayBeDerivedFrom(impl.Name, lhs.AssignedVariable.Name, s);
+ }
+ }
+ }
+ }
+ }
+ else if (c is CallCmd)
+ {
+ CallCmd callCmd = c as CallCmd;
+
+ if (callCmd.callee != verifier.BarrierProcedure.Name)
+ {
+
+ Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
+ for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+ {
+ VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
+ visitor.VisitExpr(callCmd.Ins[i]);
+
+ foreach (Variable v in visitor.GetVariables())
+ {
+ if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))
+ {
+ continue;
+ }
+
+
+ foreach (String s in mayBeDerivedFrom[impl.Name][v.Name])
+ {
+ if (!mayBeDerivedFrom[callCmd.callee][CalleeImplementation.InParams[i].Name].Contains(s))
+ {
+ SetMayBeDerivedFrom(callCmd.callee, CalleeImplementation.InParams[i].Name, s);
+ }
+ }
+ }
+
+ }
+
+ for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+ {
+ foreach (String s in mayBeDerivedFrom[callCmd.callee][CalleeImplementation.OutParams[i].Name])
+ {
+ if (!mayBeDerivedFrom[impl.Name][callCmd.Outs[i].Name].Contains(s))
+ {
+ SetMayBeDerivedFrom(impl.Name, callCmd.Outs[i].Name, s);
+ }
+ }
+ }
+
+ }
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+
+ VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
+ visitor.VisitExpr(wc.Guard);
+ foreach (Variable v in visitor.GetVariables())
+ {
+ foreach (string s in mayBeDerivedFrom[impl.Name][v.Name])
+ {
+ if (!arraysWhichMayAffectControlFlow.Contains(s))
+ {
+ SetArrayMayAffectControlFlow(s);
+ }
+ }
+ }
+
+ Analyse(impl, wc.Body);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ IfCmd ifCmd = bb.ec as IfCmd;
+
+ VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
+ visitor.VisitExpr(ifCmd.Guard);
+ foreach (Variable v in visitor.GetVariables())
+ {
+ if (!mayBeDerivedFrom[impl.Name].ContainsKey(v.Name))
+ {
+ continue;
+ }
+ foreach (string s in mayBeDerivedFrom[impl.Name][v.Name])
+ {
+ if (!arraysWhichMayAffectControlFlow.Contains(s))
+ {
+ SetArrayMayAffectControlFlow(s);
+ }
+ }
+ }
+
+ Analyse(impl, ifCmd.thn);
+ if (ifCmd.elseBlock != null)
+ {
+ Analyse(impl, ifCmd.elseBlock);
+ }
+ Debug.Assert(ifCmd.elseIf == null);
+ }
+
+ }
+
+ private void SetArrayMayAffectControlFlow(string s)
+ {
+ Debug.Assert(!arraysWhichMayAffectControlFlow.Contains(s));
+ arraysWhichMayAffectControlFlow.Add(s);
+ ProcedureChanged = true;
+ }
+
+ private void dump()
+ {
+ foreach (string s in arraysWhichMayAffectControlFlow)
+ {
+ Console.WriteLine("Array " + s + " may affect control flow");
+ }
+
+ }
+
+ internal bool MayAffectControlFlow(string v)
+ {
+ return arraysWhichMayAffectControlFlow.Contains(v);
+ }
+ }
+}
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index ae6b03a2..06acb694 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -37,7 +37,7 @@ namespace GPUVerify public static bool ShowUniformityAnalysis = false;
public static bool DoUniformityAnalysis = true;
- public static bool ShowMayBeTidAnalysis = false;
+ public static bool ShowMayBeThreadConfigurationVariableAnalysis = false;
public static bool ShowMayBePowerOfTwoAnalysis = false;
public static bool ShowMayBeTidPlusConstantAnalysis = false;
public static bool ShowArrayControlFlowAnalysis = false;
@@ -170,7 +170,7 @@ namespace GPUVerify case "-showMayBeTidAnalysis":
case "/showMayBeTidAnalysis":
- ShowMayBeTidAnalysis = true;
+ ShowMayBeThreadConfigurationVariableAnalysis = true;
break;
case "-showMayBePowerOfTwoAnalysis":
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 03a9f647..1120b086 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -29,9 +29,9 @@ namespace GPUVerify private int TempCounter = 0;
private int invariantGenerationCounter;
- private const string LOCAL_ID_X_STRING = "local_id_x";
- private const string LOCAL_ID_Y_STRING = "local_id_y";
- private const string LOCAL_ID_Z_STRING = "local_id_z";
+ internal const string LOCAL_ID_X_STRING = "local_id_x";
+ internal const string LOCAL_ID_Y_STRING = "local_id_y";
+ internal const string LOCAL_ID_Z_STRING = "local_id_z";
internal static Constant _X = null;
internal static Constant _Y = null;
@@ -41,30 +41,30 @@ namespace GPUVerify private Constant _GROUP_SIZE_Y = null;
private Constant _GROUP_SIZE_Z = null;
- private const string GROUP_SIZE_X_STRING = "group_size_x";
- private const string GROUP_SIZE_Y_STRING = "group_size_y";
- private const string GROUP_SIZE_Z_STRING = "group_size_z";
+ internal const string GROUP_SIZE_X_STRING = "group_size_x";
+ internal const string GROUP_SIZE_Y_STRING = "group_size_y";
+ internal const string GROUP_SIZE_Z_STRING = "group_size_z";
private Constant _GROUP_X = null;
private Constant _GROUP_Y = null;
private Constant _GROUP_Z = null;
- private const string GROUP_ID_X_STRING = "group_id_x";
- private const string GROUP_ID_Y_STRING = "group_id_y";
- private const string GROUP_ID_Z_STRING = "group_id_z";
+ internal const string GROUP_ID_X_STRING = "group_id_x";
+ internal const string GROUP_ID_Y_STRING = "group_id_y";
+ internal const string GROUP_ID_Z_STRING = "group_id_z";
private Constant _NUM_GROUPS_X = null;
private Constant _NUM_GROUPS_Y = null;
private Constant _NUM_GROUPS_Z = null;
- private const string NUM_GROUPS_X_STRING = "num_groups_x";
- private const string NUM_GROUPS_Y_STRING = "num_groups_y";
- private const string NUM_GROUPS_Z_STRING = "num_groups_z";
+ internal const string NUM_GROUPS_X_STRING = "num_groups_x";
+ internal const string NUM_GROUPS_Y_STRING = "num_groups_y";
+ internal const string NUM_GROUPS_Z_STRING = "num_groups_z";
public IRaceInstrumenter RaceInstrumenter;
public UniformityAnalyser uniformityAnalyser;
- public MayBeTidAnalyser mayBeTidAnalyser;
+ public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;
public MayBeTidPlusConstantAnalyser mayBeTidPlusConstantAnalyser;
public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;
public LiveVariableAnalyser liveVariableAnalyser;
@@ -442,7 +442,7 @@ namespace GPUVerify private void DoMayBeTidAnalysis()
{
- mayBeTidAnalyser = new MayBeTidAnalyser(this);
+ mayBeTidAnalyser = new MayBeThreadConfigurationVariableAnalyser(this);
mayBeTidAnalyser.Analyse();
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 91800a70..9f5a4f07 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -113,7 +113,7 @@ <Compile Include="LiveVariableAnalyser.cs" />
<Compile Include="LoopInvariantGenerator.cs" />
<Compile Include="MayBePowerOfTwoAnalyser.cs" />
- <Compile Include="MayBeTidAnalyser.cs" />
+ <Compile Include="MayBeThreadConfigurationVariableAnalyser.cs" />
<Compile Include="MayBeTidPlusConstantAnalyser.cs" />
<Compile Include="StructuredProgramVisitor.cs" />
<Compile Include="CrossThreadInvariantProcessor.cs" />
diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs new file mode 100644 index 00000000..cfc699e5 --- /dev/null +++ b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs @@ -0,0 +1,262 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class MayBeThreadConfigurationVariableAnalyser
+ {
+
+ private GPUVerifier verifier;
+
+ private bool ProcedureChanged;
+
+ private Dictionary<string, Dictionary<string, bool>> mayBeLocalXInfo;
+ private Dictionary<string, Dictionary<string, bool>> mayBeLocalYInfo;
+ private Dictionary<string, Dictionary<string, bool>> mayBeLocalZInfo;
+
+ public MayBeThreadConfigurationVariableAnalyser(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ mayBeLocalXInfo = new Dictionary<string, Dictionary<string, bool>>();
+ mayBeLocalYInfo = new Dictionary<string, Dictionary<string, bool>>();
+ mayBeLocalZInfo = new Dictionary<string, Dictionary<string, bool>>();
+ }
+
+ internal void Analyse()
+ {
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if(D is Implementation)
+ {
+ Implementation Impl = D as Implementation;
+ mayBeLocalXInfo.Add(Impl.Name, new Dictionary<string, bool> ());
+ mayBeLocalYInfo.Add(Impl.Name, new Dictionary<string, bool>());
+ mayBeLocalZInfo.Add(Impl.Name, new Dictionary<string, bool>());
+
+ SetMayBeLocal("X", Impl.Name, GPUVerifier._X.Name);
+ SetNotLocal("X", Impl.Name, GPUVerifier._Y.Name);
+ SetNotLocal("X", Impl.Name, GPUVerifier._Z.Name);
+
+ SetNotLocal("Y", Impl.Name, GPUVerifier._X.Name);
+ SetMayBeLocal("Y", Impl.Name, GPUVerifier._Y.Name);
+ SetNotLocal("Y", Impl.Name, GPUVerifier._Z.Name);
+
+ SetNotLocal("Z", Impl.Name, GPUVerifier._X.Name);
+ SetNotLocal("Z", Impl.Name, GPUVerifier._Y.Name);
+ SetMayBeLocal("Z", Impl.Name, GPUVerifier._Z.Name);
+
+ foreach (Variable v in Impl.LocVars)
+ {
+ SetMayBeLocal("X", Impl.Name, v.Name);
+ SetMayBeLocal("Y", Impl.Name, v.Name);
+ SetMayBeLocal("Z", Impl.Name, v.Name);
+ }
+
+ foreach (Variable v in Impl.InParams)
+ {
+ SetMayBeLocal("X", Impl.Name, v.Name);
+ SetMayBeLocal("Y", Impl.Name, v.Name);
+ SetMayBeLocal("Z", Impl.Name, v.Name);
+ }
+
+ foreach (Variable v in Impl.OutParams)
+ {
+ SetMayBeLocal("X", Impl.Name, v.Name);
+ SetMayBeLocal("Y", Impl.Name, v.Name);
+ SetMayBeLocal("Z", Impl.Name, v.Name);
+ }
+
+ ProcedureChanged = true;
+ }
+ }
+
+ while (ProcedureChanged)
+ {
+ ProcedureChanged = false;
+
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation)
+ {
+ Implementation Impl = D as Implementation;
+ Analyse(Impl);
+ }
+ }
+ }
+
+ if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
+ {
+ dump();
+ }
+ }
+
+ private void Analyse(Implementation Impl)
+ {
+ Analyse(Impl, Impl.StructuredStmts);
+ }
+
+ private void Analyse(Implementation impl, StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ Analyse(impl, bb);
+ }
+ }
+
+ private void Analyse(Implementation impl, BigBlock bb)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is AssignCmd)
+ {
+ AssignCmd assignCmd = c as AssignCmd;
+ Debug.Assert(assignCmd.Lhss.Count == 1);
+ Debug.Assert(assignCmd.Rhss.Count == 1);
+ if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ {
+ SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[0];
+
+ if (MayBeLocal ("X", impl.Name, lhs.AssignedVariable.Name)
+ && !MayBeLocal("X", impl.Name, rhs))
+ {
+ SetNotLocal ("X", impl.Name, lhs.AssignedVariable.Name);
+ }
+
+ }
+ }
+ else if (c is CallCmd)
+ {
+ CallCmd callCmd = c as CallCmd;
+
+ if (callCmd.callee != verifier.BarrierProcedure.Name)
+ {
+
+ Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
+ for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+ {
+ if (MayBeLocal("X", callCmd.callee, CalleeImplementation.InParams[i].Name)
+ && !MayBeLocal("X", impl.Name, callCmd.Ins[i]))
+ {
+ SetNotLocal("X", callCmd.callee, CalleeImplementation.InParams[i].Name);
+ }
+ }
+
+ for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+ {
+ if (MayBeLocal("X", impl.Name, callCmd.Outs[i].Name)
+ && !MayBeLocal("X", callCmd.callee, CalleeImplementation.OutParams[i].Name))
+ {
+ SetNotLocal("X", impl.Name, callCmd.Outs[i].Name);
+ }
+ }
+
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havoc = c as HavocCmd;
+ Debug.Assert(havoc.Vars.Length == 1);
+
+ if (MayBeLocal("X", impl.Name, havoc.Vars[0].Decl.Name))
+ {
+ SetNotLocal("X", impl.Name, havoc.Vars[0].Decl.Name);
+ }
+ }
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+ Analyse(impl, wc.Body);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ IfCmd ifCmd = bb.ec as IfCmd;
+ Analyse(impl, ifCmd.thn);
+ if (ifCmd.elseBlock != null)
+ {
+ Analyse(impl, ifCmd.elseBlock);
+ }
+ Debug.Assert(ifCmd.elseIf == null);
+ }
+
+ }
+
+ private void SetNotLocal(string dim, string proc, string v)
+ {
+ GetMayBeLocalDimInfo(dim)[proc][v] = false;
+ ProcedureChanged = true;
+ }
+
+ private void SetMayBeLocal(string dim, string proc, string v)
+ {
+ GetMayBeLocalDimInfo(dim)[proc][v] = true;
+ }
+
+ internal bool MayBeLocal(string dim, string proc, string v)
+ {
+ if (!GetMayBeLocalDimInfo(dim).ContainsKey(proc))
+ {
+ return false;
+ }
+
+ if (!GetMayBeLocalDimInfo(dim)[proc].ContainsKey(v))
+ {
+ return false;
+ }
+
+ return GetMayBeLocalDimInfo(dim)[proc][v];
+ }
+
+ internal bool MayBeLocal(string dim, string proc, Expr e)
+ {
+ if (e is IdentifierExpr)
+ {
+ return MayBeLocal(dim, proc, (e as IdentifierExpr).Decl.Name);
+ }
+ return false;
+ }
+
+ private void dump()
+ {
+ foreach (string p in mayBeLocalXInfo.Keys)
+ {
+ Console.WriteLine("Procedure " + p);
+ foreach (string v in mayBeLocalXInfo[p].Keys)
+ {
+ Console.WriteLine(" " + v + ": " +
+ (mayBeLocalXInfo[p][v] ? "may be" : "likely not") + " " + GPUVerifier.LOCAL_ID_X_STRING);
+ }
+ }
+
+ }
+
+ private Dictionary<string, Dictionary<string, bool>> GetMayBeLocalDimInfo(string dim)
+ {
+ Dictionary<string, Dictionary<string, bool>> map = null;
+ if (dim.Equals("X"))
+ {
+ map = mayBeLocalXInfo;
+ }
+ else if (dim.Equals("Y"))
+ {
+ map = mayBeLocalYInfo;
+ }
+ else if (dim.Equals("Z"))
+ {
+ map = mayBeLocalZInfo;
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ return map;
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/MayBeTidAnalyser.cs b/Source/GPUVerify/MayBeTidAnalyser.cs deleted file mode 100644 index 990559c2..00000000 --- a/Source/GPUVerify/MayBeTidAnalyser.cs +++ /dev/null @@ -1,220 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- class MayBeTidAnalyser
- {
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, bool>> mayBeTidInfo;
-
- public MayBeTidAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
- mayBeTidInfo = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
- mayBeTidInfo.Add(Impl.Name, new Dictionary<string, bool> ());
-
- SetMayBeTid(Impl.Name, GPUVerifier._X.Name);
- SetNotTid(Impl.Name, GPUVerifier._Y.Name);
- SetNotTid(Impl.Name, GPUVerifier._Z.Name);
-
- foreach (Variable v in Impl.LocVars)
- {
- SetMayBeTid(Impl.Name, v.Name);
- }
-
- foreach (Variable v in Impl.InParams)
- {
- SetMayBeTid(Impl.Name, v.Name);
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- SetMayBeTid(Impl.Name, v.Name);
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeTidAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, Impl.StructuredStmts);
- }
-
- private void Analyse(Implementation impl, StmtList stmtList)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
- {
- if (c is AssignCmd)
- {
- AssignCmd assignCmd = c as AssignCmd;
- Debug.Assert(assignCmd.Lhss.Count == 1);
- Debug.Assert(assignCmd.Rhss.Count == 1);
- if (assignCmd.Lhss[0] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[0];
-
- if (MayBeTid (impl.Name, lhs.AssignedVariable.Name)
- && !MayBeTid(impl.Name, rhs))
- {
- SetNotTid (impl.Name, lhs.AssignedVariable.Name);
- }
-
- }
- }
- else if (c is CallCmd)
- {
- CallCmd callCmd = c as CallCmd;
-
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBeTid(callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBeTid(impl.Name, callCmd.Ins[i]))
- {
- SetNotTid(callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBeTid(impl.Name, callCmd.Outs[i].Name)
- && !MayBeTid(callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNotTid(impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- else if (c is HavocCmd)
- {
- HavocCmd havoc = c as HavocCmd;
- Debug.Assert(havoc.Vars.Length == 1);
-
- if (MayBeTid(impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNotTid(impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
- }
- }
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd wc = bb.ec as WhileCmd;
- Analyse(impl, wc.Body);
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd ifCmd = bb.ec as IfCmd;
- Analyse(impl, ifCmd.thn);
- if (ifCmd.elseBlock != null)
- {
- Analyse(impl, ifCmd.elseBlock);
- }
- Debug.Assert(ifCmd.elseIf == null);
- }
-
- }
-
- private void SetNotTid(string proc, string v)
- {
- mayBeTidInfo[proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBeTid(string proc, string v)
- {
- mayBeTidInfo[proc][v] = true;
- }
-
- internal bool MayBeTid(string proc, string v)
- {
- if (!mayBeTidInfo.ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeTidInfo[proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeTidInfo[proc][v];
- }
-
- internal bool MayBeTid(string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBeTid(proc, (e as IdentifierExpr).Decl.Name);
- }
- return false;
- }
-
- private void dump()
- {
- foreach (string p in mayBeTidInfo.Keys)
- {
- Console.WriteLine("Procedure " + p);
- foreach (string v in mayBeTidInfo[p].Keys)
- {
- Console.WriteLine(" " + v + ": " +
- (mayBeTidInfo[p][v] ? "may be tid" : "likely not tid"));
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs index 0f145296..f87e3afd 100644 --- a/Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs +++ b/Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs @@ -111,7 +111,7 @@ namespace GPUVerify Variable rhsV = (assign.Rhss[0] as IdentifierExpr).Decl;
- if (verifier.mayBeTidAnalyser.MayBeTid(impl.Name, rhsV.Name))
+ if (verifier.mayBeTidAnalyser.MayBeLocal("X", impl.Name, rhsV.Name))
{
mayBeAssignedTid[impl.Name][lhsV.Name] = true;
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index b380a595..7a8baf23 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -351,7 +351,7 @@ namespace GPUVerify string indexVarName =
GPUVerifier.StripThreadIdentifier((e as IdentifierExpr).Decl.Name);
- if (verifier.mayBeTidAnalyser.MayBeTid(impl.Name, indexVarName))
+ if (verifier.mayBeTidAnalyser.MayBeLocal("X", impl.Name, indexVarName))
{
AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(wc, v, accessType, 1);
if (accessType.Equals("WRITE") || !CommandLineOptions.Symmetry)
|