diff options
author | 2011-11-09 16:49:09 +0000 | |
---|---|---|
committer | 2011-11-09 16:49:09 +0000 | |
commit | 9865334085ec74d1fe931490f72e6970cc88de64 (patch) | |
tree | 6ac556210b67d66ea3ec894a5101d034f55af109 | |
parent | 2551eb125aae4fd71eec5465fa919cd58163c105 (diff) |
Refactoring, and work on race checking contracts
-rw-r--r-- | Source/GPUVerify/AccessCollector.cs | 8 | ||||
-rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 67 | ||||
-rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 22 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 451 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 93 | ||||
-rw-r--r-- | Source/GPUVerify/INonLocalState.cs | 21 | ||||
-rw-r--r-- | Source/GPUVerify/Main.cs | 59 | ||||
-rw-r--r-- | Source/GPUVerify/NonLocalAccessCollector.cs | 26 | ||||
-rw-r--r-- | Source/GPUVerify/NonLocalAccessExtractor.cs | 14 | ||||
-rw-r--r-- | Source/GPUVerify/NonLocalStateLists.cs | 45 | ||||
-rw-r--r-- | Source/GPUVerify/Predicator.cs | 256 | ||||
-rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 94 | ||||
-rw-r--r-- | Source/GPUVerify/ReadCollector.cs | 8 | ||||
-rw-r--r-- | Source/GPUVerify/SetEncodingRaceInstrumenter.cs | 8 | ||||
-rw-r--r-- | Source/GPUVerify/WriteCollector.cs | 8 |
15 files changed, 584 insertions, 596 deletions
diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs index 43491460..42ca5cc8 100644 --- a/Source/GPUVerify/AccessCollector.cs +++ b/Source/GPUVerify/AccessCollector.cs @@ -8,13 +8,11 @@ namespace GPUVerify {
abstract class AccessCollector : StandardVisitor
{
- protected ICollection<Variable> GlobalVariables;
- protected ICollection<Variable> TileStaticVariables;
+ protected INonLocalState NonLocalState;
- public AccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public AccessCollector(INonLocalState NonLocalState)
{
- this.GlobalVariables = GlobalVariables;
- this.TileStaticVariables = TileStaticVariables;
+ this.NonLocalState = NonLocalState;
}
protected void MultiDimensionalMapError()
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 9e7ba32c..2f08477b 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -14,10 +14,7 @@ namespace GPUVerify public static List<string> inputFiles = new List<string>();
public static string outputFile = null;
- public static string formulaSkeletonsFile = null;
- public static string formulasFile = null;
- public static bool NewRaceDetectionMethod = false;
public static bool OnlyDivergence = false;
public static bool FullAbstraction;
public static bool Inference;
@@ -49,6 +46,12 @@ namespace GPUVerify switch (beforeColon)
{
+ case "-help":
+ case "/help":
+ case "-?":
+ case "/?":
+ return -1;
+
case "-print":
case "/print":
if (!hasColonArgument)
@@ -60,34 +63,6 @@ namespace GPUVerify outputFile = afterColon;
break;
- case "-generateFormulaSkeletons":
- case "/generateFormulaSkeletons":
- if (!hasColonArgument)
- {
- Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
- Environment.Exit(1);
- }
- Debug.Assert(afterColon != null);
- formulaSkeletonsFile = afterColon;
- break;
-
- case "-formulas":
- case "/formulas":
- if (!hasColonArgument)
- {
- Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
- Environment.Exit(1);
- }
- Debug.Assert(afterColon != null);
- formulasFile = afterColon;
- break;
-
- case "-newRaceDetectionMethod":
- case "/newRaceDetectionMethod":
- NewRaceDetectionMethod = true;
-
- break;
-
case "-onlyDivergence":
case "/onlyDivergence":
OnlyDivergence = true;
@@ -163,5 +138,35 @@ namespace GPUVerify return 0;
}
+ private static bool printedHelp = false;
+
+ public static void Usage()
+ {
+ // Ensure that we only print the help message once
+ if (printedHelp)
+ {
+ return;
+ }
+ printedHelp = true;
+
+ Console.WriteLine(@"GPUVerify: usage: GPUVerify [ option ... ] [ filename ... ]
+ where <option> is one of
+
+ /help : this message
+ /fullAbstraction : apply full state abstraction
+ /onlyDivergence : only check for divergence-freedom, not race-freedom
+ /symmetry : apply symmetry breaking
+ /eager : check races eagerly, rather than waiting for barrier
+ /inference:file : use automatic invariant inference. Optional file can include manually supplied candidates
+ /raceCheckingContract : try to infer race-freedom contracts for procedures
+ /setEncoding : check races using set encoding
+ /divided : check individual pairs of possibly racing statements separately
+ /dividedArray : check races on arrays one at a time
+ /dividedElement : ???
+
+");
+ }
+
+
}
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 78ace202..74bdaa5e 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -89,9 +89,10 @@ namespace GPUVerify verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
}
- protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)
{
- IdentifierExprSeq newVars = new IdentifierExprSeq();
+ ModifiedAtLog = new IdentifierExprSeq();
+ ResetAtBarrier = new IdentifierExprSeq();
Variable AccessHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
@@ -100,7 +101,8 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessHasOccurred.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
+ ResetAtBarrier.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
verifier.Program.TopLevelDeclarations.Add(AccessHasOccurred);
if (v.TypedIdent.Type is MapType)
@@ -116,7 +118,7 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessOffsetX.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessOffsetX));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetX));
verifier.Program.TopLevelDeclarations.Add(AccessOffsetX);
if (mt.Result is MapType)
@@ -132,7 +134,7 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessOffsetY.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessOffsetY));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetY));
verifier.Program.TopLevelDeclarations.Add(AccessOffsetY);
if (mt2.Result is MapType)
@@ -149,19 +151,15 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessOffsetZ.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessOffsetZ));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetZ));
verifier.Program.TopLevelDeclarations.Add(AccessOffsetZ);
}
}
}
- foreach (IdentifierExpr e in newVars)
- {
- // TODO: add modiies to every procedure that calls BARRIER
- verifier.KernelProcedure.Modifies.Add(e);
- }
}
+
private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)
{
List<AssignLhs> lhss = new List<AssignLhs>();
@@ -179,7 +177,6 @@ namespace GPUVerify List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
- verifier.BarrierProcedure.Modifies.Add(AccessOccurred1);
lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));
rhss.Add(Expr.False);
@@ -187,7 +184,6 @@ namespace GPUVerify {
lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));
rhss.Add(Expr.False);
- verifier.BarrierProcedure.Modifies.Add(AccessOccurred2);
}
bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 1aac817c..25974225 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -19,18 +19,13 @@ namespace GPUVerify public Implementation KernelImplementation;
public Procedure BarrierProcedure;
- public ICollection<Variable> TileStaticVariables = new List<Variable>();
- public ICollection<Variable> GlobalVariables = new List<Variable>();
+ public INonLocalState NonLocalState = new NonLocalStateLists();
private HashSet<string> ReservedNames = new HashSet<string>();
internal HashSet<string> HalfDualisedProcedureNames = new HashSet<string>();
internal HashSet<string> HalfDualisedVariableNames = new HashSet<string>();
- private static int WhileLoopCounter;
- private static int IfCounter;
- private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;
-
private int TempCounter = 0;
private int invariantGenerationCounter;
@@ -165,11 +160,11 @@ namespace GPUVerify {
if (QKeyValue.FindBoolAttribute(D.Attributes, "tile_static"))
{
- TileStaticVariables.Add(D as Variable);
+ NonLocalState.getTileStaticVariables().Add(D as Variable);
}
else
{
- GlobalVariables.Add(D as Variable);
+ NonLocalState.getGlobalVariables().Add(D as Variable);
}
}
}
@@ -296,16 +291,6 @@ namespace GPUVerify // TODO!
}
- internal ICollection<Variable> GetTileStaticVariables()
- {
- return TileStaticVariables;
- }
-
- internal ICollection<Variable> GetGlobalVariables()
- {
- return GlobalVariables;
- }
-
internal void preProcess()
{
RemoveElseIfs();
@@ -331,7 +316,7 @@ namespace GPUVerify AbstractSharedState();
- MakeKerenelPredicated();
+ MakeKernelPredicated();
MakeKernelDualised();
@@ -399,7 +384,7 @@ namespace GPUVerify private void AddEagerRaceChecking()
{
- foreach(Variable v in GlobalVariables)
+ foreach(Variable v in NonLocalState.getAllNonLocalVariables())
{
foreach (Declaration d in Program.TopLevelDeclarations)
{
@@ -425,32 +410,6 @@ namespace GPUVerify }
}
}
- foreach (Variable v in TileStaticVariables)
- {
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (!(d is Implementation))
- {
- continue;
- }
-
- Implementation impl = d as Implementation;
-
- if (impl.Name.Equals("_LOG_READ_" + v.Name) || impl.Name.Equals("_LOG_WRITE_" + v.Name))
- {
- BigBlock bb = new BigBlock(v.tok, "__CheckForRaces", new CmdSeq(), null, null);
- RaceInstrumenter.CheckForRaces(v.tok, bb, v);
- StmtList newStatements = new StmtList(new List<BigBlock>(), v.tok);
-
- foreach (BigBlock bb2 in impl.StructuredStmts.BigBlocks)
- {
- newStatements.BigBlocks.Add(bb2);
- }
- newStatements.BigBlocks.Add(bb);
- impl.StructuredStmts = newStatements;
- }
- }
- }
}
private void ComputeInvariant()
@@ -735,12 +694,7 @@ namespace GPUVerify if (!CommandLineOptions.FullAbstraction)
{
- foreach (Variable v in GlobalVariables)
- {
- AddEqualityCandidateInvariant(wc, LoopPredicate, v);
- }
-
- foreach (Variable v in TileStaticVariables)
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
AddEqualityCandidateInvariant(wc, LoopPredicate, v);
}
@@ -855,21 +809,23 @@ namespace GPUVerify return true;
}
+
+
public Microsoft.Boogie.Type GetTypeOfIdX()
{
- Contract.Assert(_X != null);
+ Contract.Requires(_X != null);
return _X.TypedIdent.Type;
}
public Microsoft.Boogie.Type GetTypeOfIdY()
{
- Contract.Assert(_Y != null);
+ Contract.Requires(_Y != null);
return _Y.TypedIdent.Type;
}
public Microsoft.Boogie.Type GetTypeOfIdZ()
{
- Contract.Assert(_Z != null);
+ Contract.Requires(_Z != null);
return _Z.TypedIdent.Type;
}
@@ -1164,11 +1120,7 @@ namespace GPUVerify {
BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);
bigblocks.Add(havocSharedState);
- foreach (Variable v in GlobalVariables)
- {
- HavocAndAssumeEquality(tok, havocSharedState, v);
- }
- foreach (Variable v in TileStaticVariables)
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
HavocAndAssumeEquality(tok, havocSharedState, v);
}
@@ -1219,35 +1171,18 @@ namespace GPUVerify IdentifierExpr v1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable));
IdentifierExpr v2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable));
- bb.simpleCmds.Add(new HavocCmd(tok, new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 })));
+ IdentifierExprSeq ModifiedVars = new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 });
+ bb.simpleCmds.Add(new HavocCmd(tok, ModifiedVars));
bb.simpleCmds.Add(new AssumeCmd(tok, Expr.Eq(v1, v2)));
- BarrierProcedure.Modifies.Add(v1);
- BarrierProcedure.Modifies.Add(v2);
-
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Implementation)
- {
- Implementation impl = d as Implementation;
- if (CallsBarrier(impl))
- {
- Procedure proc = impl.Proc;
- if (!ModifiesSetContains(proc.Modifies, v1))
- {
- Debug.Assert(!ModifiesSetContains(proc.Modifies, v2));
- proc.Modifies.Add(v1);
- proc.Modifies.Add(v2);
- }
- }
- }
- }
+ HashSet<string> MayCallBarrier = GetProceduresThatIndirectlyCallProcedure(BarrierProcedure.Name);
+ ExtendModifiesSetOfProcedures(ModifiedVars, MayCallBarrier);
}
- private bool ModifiesSetContains(IdentifierExprSeq seq, IdentifierExpr v)
+ internal static bool ModifiesSetContains(IdentifierExprSeq Modifies, IdentifierExpr v)
{
- foreach (IdentifierExpr ie in seq)
+ foreach (IdentifierExpr ie in Modifies)
{
if (ie.Name.Equals(v.Name))
{
@@ -1257,7 +1192,7 @@ namespace GPUVerify return false;
}
- private bool CallsBarrier(Implementation impl)
+/* private bool CallsBarrier(Implementation impl)
{
return CallsBarrier(impl.StructuredStmts);
}
@@ -1292,7 +1227,7 @@ namespace GPUVerify Debug.Assert(bb.ec == null);
return false;
}
- }
+ }*/
private void AbstractSharedState()
{
@@ -1305,7 +1240,7 @@ namespace GPUVerify foreach (Declaration d in Program.TopLevelDeclarations)
{
- if (d is Variable && GlobalVariables.Contains(d as Variable) || TileStaticVariables.Contains(d as Variable))
+ if (d is Variable && NonLocalState.Contains(d as Variable))
{
continue;
}
@@ -1334,7 +1269,7 @@ namespace GPUVerify foreach (IdentifierExpr e in proc.Modifies)
{
- if (!(GlobalVariables.Contains(e.Decl) || TileStaticVariables.Contains(e.Decl)))
+ if (!NonLocalState.Contains(e.Decl))
{
NewModifies.Add(e);
}
@@ -1350,10 +1285,8 @@ namespace GPUVerify foreach (Variable v in impl.LocVars)
{
- if (!TileStaticVariables.Contains(v))
- {
- NewLocVars.Add(v);
- }
+ Debug.Assert(!NonLocalState.getTileStaticVariables().Contains(v));
+ NewLocVars.Add(v);
}
impl.LocVars = NewLocVars;
@@ -1389,7 +1322,7 @@ namespace GPUVerify Debug.Assert(assign.Rhss.Count == 1);
AssignLhs lhs = assign.Lhss[0];
Expr rhs = assign.Rhss[0];
- ReadCollector rc = new ReadCollector(GlobalVariables, TileStaticVariables);
+ ReadCollector rc = new ReadCollector(NonLocalState);
rc.Visit(rhs);
if (rc.accesses.Count > 0)
{
@@ -1398,7 +1331,7 @@ namespace GPUVerify continue;
}
- WriteCollector wc = new WriteCollector(GlobalVariables, TileStaticVariables);
+ WriteCollector wc = new WriteCollector(NonLocalState);
wc.Visit(lhs);
if (wc.GetAccess() != null)
{
@@ -1642,7 +1575,7 @@ namespace GPUVerify {
Expr e = call.Ins[i];
- while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1666,7 +1599,9 @@ namespace GPUVerify AssignLhs lhs = assign.Lhss.ElementAt(0);
Expr rhs = assign.Rhss.ElementAt(0);
- if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables) || (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, GlobalVariables, TileStaticVariables) && NonLocalAccessCollector.IsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables)))
+ if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) ||
+ (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) &&
+ NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState)))
{
result.simpleCmds.Add(c);
}
@@ -1703,7 +1638,7 @@ namespace GPUVerify if (bb.ec is WhileCmd)
{
WhileCmd WhileCommand = bb.ec as WhileCmd;
- while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, GlobalVariables, TileStaticVariables))
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1716,8 +1651,8 @@ namespace GPUVerify else if (bb.ec is IfCmd)
{
IfCmd IfCommand = bb.ec as IfCmd;
- Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
- while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, GlobalVariables, TileStaticVariables))
+ Debug.Assert(IfCommand.elseIf == null); // "else if" must have been eliminated by this phase
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1742,7 +1677,7 @@ namespace GPUVerify private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e, Implementation impl)
{
- while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1755,7 +1690,7 @@ namespace GPUVerify private Expr ExtractLocalAccessToTemp(Expr rhs, out AssignCmd tempAssignment, out LocalVariable tempDeclaration)
{
- NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, GlobalVariables, TileStaticVariables);
+ NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, NonLocalState);
TempCounter++;
rhs = extractor.VisitExpr(rhs);
tempAssignment = extractor.Assignment;
@@ -1860,7 +1795,7 @@ namespace GPUVerify return result;
}
- private void MakeKerenelPredicated()
+ private void MakeKernelPredicated()
{
foreach (Declaration d in Program.TopLevelDeclarations)
{
@@ -1882,38 +1817,12 @@ namespace GPUVerify }
else if (d is Implementation)
{
- MakePredicated(d as Implementation, d != KernelImplementation);
- }
- }
+ new Predicator(d != KernelImplementation).transform(d as Implementation);
- }
-
- private void MakePredicated(Implementation impl, bool AddPredicateParameter)
- {
- Expr Predicate;
-
- if (AddPredicateParameter)
- {
- VariableSeq NewIns = new VariableSeq();
- Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));
- NewIns.Add(PredicateVariable);
- foreach (Variable v in impl.InParams)
- {
- NewIns.Add(v);
+ //MakePredicated(d as Implementation, d != KernelImplementation);
}
- impl.InParams = NewIns;
- Predicate = new IdentifierExpr(impl.tok, PredicateVariable);
- }
- else
- {
- Predicate = Expr.True;
}
- WhileLoopCounter = 0;
- IfCounter = 0;
- RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
- impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);
- AddPredicateLocalVariables(impl);
}
private StmtList MakeDual(StmtList stmtList, bool HalfDualise)
@@ -2081,208 +1990,6 @@ namespace GPUVerify impl.LocVars = NewLocalVars;
}
- private void AddPredicateLocalVariables(Implementation impl)
- {
- for (int i = 0; i < IfCounter; i++)
- {
- impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));
- }
- for (int i = 0; i < WhileLoopCounter; i++)
- {
- impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));
- }
- foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)
- {
- impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));
- }
-
- }
-
- private StmtList MakePredicated(StmtList sl, Expr predicate, IdentifierExpr EnclosingLoopPredicate)
- {
- StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);
-
- foreach (BigBlock bodyBlock in sl.BigBlocks)
- {
- List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);
- foreach (BigBlock newBigBlock in newBigBlocks)
- {
- result.BigBlocks.Add(newBigBlock);
- }
- }
-
- return result;
-
- }
-
- private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)
- {
- // Not sure what to do about the transfer command
-
- List<BigBlock> result = new List<BigBlock>();
-
- BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);
- result.Add(firstBigBlock);
-
- foreach (Cmd c in b.simpleCmds)
- {
- if (c is CallCmd)
- {
-
- CallCmd Call = c as CallCmd;
-
- List<Expr> NewIns = new List<Expr>();
- NewIns.Add(IncomingPredicate);
-
- foreach (Expr e in Call.Ins)
- {
- NewIns.Add(e);
- }
-
- CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);
-
- firstBigBlock.simpleCmds.Add(NewCallCmd);
- }
- else if (IncomingPredicate.Equals(Expr.True))
- {
- firstBigBlock.simpleCmds.Add(c);
- }
- else if (c is AssignCmd)
- {
- AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- ExprSeq iteArgs = new ExprSeq();
- iteArgs.Add(IncomingPredicate);
- iteArgs.Add(assign.Rhss.ElementAt(0));
- iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);
- NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);
-
- List<Expr> newRhs = new List<Expr>();
- newRhs.Add(ite);
-
- AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);
-
- firstBigBlock.simpleCmds.Add(newAssign);
- }
- else if (c is HavocCmd)
- {
- HavocCmd havoc = c as HavocCmd;
- Debug.Assert(havoc.Vars.Length == 1);
-
- Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;
- Debug.Assert(type != null);
-
- RequiredHavocVariables.Add(type);
-
- IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));
- firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- HavocTempExpr
- })));
-
- List<AssignLhs> lhss = new List<AssignLhs>();
- lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));
-
- List<Expr> rhss = new List<Expr>();
- rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));
-
- }
- else
- {
- Debug.Assert(false);
- }
- }
-
- if (b.ec is WhileCmd)
- {
- string LoopPredicate = "_LC" + WhileLoopCounter;
- WhileLoopCounter++;
-
- IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));
- Expr GuardExpr = (b.ec as WhileCmd).Guard;
-
- List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
- WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
-
- List<Expr> WhilePredicateRhss = new List<Expr>();
- WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));
-
- WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));
-
- List<Expr> UpdatePredicateRhss = new List<Expr>();
- UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));
-
- CmdSeq updateCmd = new CmdSeq();
- updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));
-
- NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));
-
- firstBigBlock.ec = NewWhile;
-
- }
- else if (b.ec is IfCmd)
- {
- IfCmd IfCommand = b.ec as IfCmd;
-
- string IfPredicate = "_P" + IfCounter;
- IfCounter++;
-
- IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
- Expr GuardExpr = IfCommand.Guard;
-
- List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
- IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
-
- List<Expr> IfPredicateRhss = new List<Expr>();
- IfPredicateRhss.Add(GuardExpr);
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));
-
- Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
-
- StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);
-
- foreach (BigBlock bb in PredicatedThen.BigBlocks)
- {
- result.Add(bb);
- }
-
- if (IfCommand.elseBlock != null)
- {
- StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);
-
- foreach (BigBlock bb in PredicatedElse.BigBlocks)
- {
- result.Add(bb);
- }
- }
-
-
-
-
- }
- else if (b.ec is BreakCmd)
- {
-
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(b.tok,
- new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(b.tok, EnclosingLoopPredicate) }),
- new List<Expr>(new Expr[] { new NAryExpr(b.tok, new IfThenElse(b.tok), new ExprSeq(new Expr[] { IncomingPredicate, Expr.False, EnclosingLoopPredicate })) })
- ));
- firstBigBlock.ec = null;
-
- }
- else
- {
- Debug.Assert(b.ec == null);
- }
-
- return result;
- }
private void CheckKernelParameters()
{
@@ -2454,5 +2161,87 @@ namespace GPUVerify return variable is Constant && (variable.Name.Equals(_X_name) || variable.Name.Equals(_Y_name) || variable.Name.Equals(_Z_name));
}
+ internal HashSet<string> GetProceduresThatIndirectlyCallProcedure(string Name)
+ {
+ HashSet<string> MayCallProc = new HashSet<string>();
+ MayCallProc.Add(Name);
+ bool changed = true;
+ while (changed)
+ {
+ changed = false;
+ foreach (Declaration d in Program.TopLevelDeclarations)
+ {
+ if (d is Implementation && !MayCallProc.Contains((d as Implementation).Name))
+ {
+ HashSet<string> CalledProcedures = GetCalledProcedures(d as Implementation);
+ foreach (string p in CalledProcedures)
+ {
+ if (MayCallProc.Contains(p))
+ {
+ changed = true;
+ MayCallProc.Add((d as Implementation).Name);
+ break;
+ }
+ }
+ }
+ }
+ }
+ return MayCallProc;
+ }
+
+ private HashSet<string> GetCalledProcedures(Implementation impl)
+ {
+ HashSet<string> result = new HashSet<string>();
+ return GetCalledProcedures(impl.StructuredStmts, result);
+ }
+
+ private HashSet<string> GetCalledProcedures(StmtList statements, HashSet<string> result)
+ {
+ foreach (BigBlock bb in statements.BigBlocks)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is CallCmd)
+ {
+ result.Add((c as CallCmd).callee);
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ result = GetCalledProcedures((bb.ec as WhileCmd).Body, result);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ result = GetCalledProcedures((bb.ec as IfCmd).thn, result);
+ Debug.Assert((bb.ec as IfCmd).elseIf == null);
+ if ((bb.ec as IfCmd).elseBlock != null)
+ {
+ result = GetCalledProcedures((bb.ec as IfCmd).elseBlock, result);
+ }
+ }
+ }
+
+ return result;
+ }
+
+ internal void ExtendModifiesSetOfProcedures(IdentifierExprSeq ModifiedVariables, HashSet<string> Procedures)
+ {
+ foreach (Declaration d in Program.TopLevelDeclarations)
+ {
+ if (d is Procedure && Procedures.Contains((d as Procedure).Name))
+ {
+ Procedure P = d as Procedure;
+ foreach (IdentifierExpr e in ModifiedVariables)
+ {
+ if (!GPUVerifier.ModifiesSetContains(P.Modifies, e))
+ {
+ P.Modifies.Add(e);
+ }
+ }
+ }
+ }
+ }
+
}
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 3b4e3bc5..7023a2b3 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -2,7 +2,7 @@ <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
<ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>
@@ -15,8 +15,8 @@ <FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
</PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <PlatformTarget>AnyCPU</PlatformTarget>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
@@ -24,7 +24,7 @@ <DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
@@ -51,93 +51,15 @@ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
<CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>
- <CodeContractsInferRequires>False</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
- <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>
</PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <PlatformTarget>AnyCPU</PlatformTarget>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin\Release\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsInferRequires>False</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
- <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -155,12 +77,15 @@ <Compile Include="CommandLineOptions.cs" />
<Compile Include="ElementEncodingraceInstrumenter.cs" />
<Compile Include="GPUVerifier.cs" />
+ <Compile Include="INonLocalState.cs" />
<Compile Include="IRaceInstrumenter.cs" />
<Compile Include="Main.cs" />
<Compile Include="NoConflictingAccessOptimiser.cs" />
<Compile Include="NonLocalAccessCollector.cs" />
<Compile Include="NonLocalAccessExtractor.cs" />
+ <Compile Include="NonLocalStateLists.cs" />
<Compile Include="NullRaceInstrumenter.cs" />
+ <Compile Include="Predicator.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="RaceInstrumenterBase.cs" />
<Compile Include="ReadCollector.cs" />
diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs new file mode 100644 index 00000000..0e03d685 --- /dev/null +++ b/Source/GPUVerify/INonLocalState.cs @@ -0,0 +1,21 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ interface INonLocalState
+ {
+
+ ICollection<Variable> getGlobalVariables();
+
+ ICollection<Variable> getTileStaticVariables();
+
+ ICollection<Variable> getAllNonLocalVariables();
+
+ bool Contains(Variable v);
+
+ }
+}
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 06fe70c6..9791d6cf 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -15,11 +15,16 @@ namespace GPUVerify {
class GPUVerify
{
- static bool ASYNCHRONOUS_METHOD = false;
public static void Main(string[] args)
{
- CommandLineOptions.Parse(args);
+ int showHelp = CommandLineOptions.Parse(args);
+
+ if (showHelp == -1)
+ {
+ CommandLineOptions.Usage();
+ System.Environment.Exit(0);
+ }
if (CommandLineOptions.inputFiles.Count < 1)
{
@@ -42,36 +47,6 @@ namespace GPUVerify }
}
- if (ASYNCHRONOUS_METHOD)
- {
-
- string[] preprocessArguments = new string[CommandLineOptions.inputFiles.Count + 4];
- preprocessArguments[0] = "/noVerify";
- preprocessArguments[1] = "/printUnstructured";
- preprocessArguments[2] = "/print:temp_unstructured.bpl";
- preprocessArguments[3] = Path.GetDirectoryName(Application.ExecutablePath) + "\\..\\..\\BoogieLibrary\\GPUVerifyLibrary.bpl";
- for (int i = 0; i < CommandLineOptions.inputFiles.Count; i++)
- {
- preprocessArguments[i + 4] = CommandLineOptions.inputFiles[i];
- }
-
- OnlyBoogie.Main(preprocessArguments);
-
- if ((CommandLineOptions.formulasFile == null && CommandLineOptions.formulaSkeletonsFile == null) || (CommandLineOptions.formulasFile != null && CommandLineOptions.formulaSkeletonsFile != null))
- {
- Console.WriteLine("Error, specify one of /formulas:... or /generateFormulaSkeletons:...");
- Environment.Exit(1);
- }
-
- CommandLineOptions.inputFiles = new List<string>();
- CommandLineOptions.inputFiles.Add("temp_unstructured.bpl");
- if (CommandLineOptions.formulasFile != null)
- {
- CommandLineOptions.inputFiles.Add(CommandLineOptions.formulasFile);
- }
-
- }
-
parseProcessOutput();
}
@@ -121,23 +96,23 @@ namespace GPUVerify ri.setVerifier(newGp);
- Variable newG = findClonedVar(v, newGp.GlobalVariables);
- Variable newT = findClonedVar(v, newGp.TileStaticVariables);
+ Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());
+ Variable newT = findClonedVar(v, newGp.NonLocalState.getTileStaticVariables());
Contract.Assert(newG == null || newT == null);
-
- ri.globalVarsToCheck.Clear();
- ri.tileStaticVarsToCheck.Clear();
+
+ ri.NonLocalStateToCheck.getGlobalVariables().Clear();
+ ri.NonLocalStateToCheck.getTileStaticVariables().Clear();
ri.onlyLog1 = a1;
ri.onlyLog2 = a2;
if (newG != null)
{
- ri.globalVarsToCheck.Add(newG);
+ ri.NonLocalStateToCheck.getGlobalVariables().Add(newG);
}
if (newT != null)
{
- ri.globalVarsToCheck.Add(newT);
+ ri.NonLocalStateToCheck.getTileStaticVariables().Add(newT);
}
newGp.doit();
@@ -159,11 +134,7 @@ namespace GPUVerify if (CommandLineOptions.DividedArray)
{
- List<Variable> nonLocalVars = new List<Variable>();
- nonLocalVars.AddRange(g.GlobalVariables);
- nonLocalVars.AddRange(g.TileStaticVariables);
-
- foreach (Variable v in nonLocalVars)
+ foreach (Variable v in g.NonLocalState.getAllNonLocalVariables())
{
if (CommandLineOptions.DividedAccesses)
{
diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs index bbab9040..13d8f672 100644 --- a/Source/GPUVerify/NonLocalAccessCollector.cs +++ b/Source/GPUVerify/NonLocalAccessCollector.cs @@ -12,16 +12,14 @@ namespace GPUVerify {
public HashSet<Expr> Accesses = new HashSet<Expr>();
- private ICollection<Variable> GlobalVariables;
- private ICollection<Variable> TileStaticVariables;
+ private INonLocalState NonLocalState;
- public NonLocalAccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public NonLocalAccessCollector(INonLocalState NonLocalState)
{
- this.GlobalVariables = GlobalVariables;
- this.TileStaticVariables = TileStaticVariables;
+ this.NonLocalState = NonLocalState;
}
- public static bool IsNonLocalAccess(Expr n, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public static bool IsNonLocalAccess(Expr n, INonLocalState NonLocalState)
{
if (n is NAryExpr)
{
@@ -37,22 +35,22 @@ namespace GPUVerify Variable v = (temp as IdentifierExpr).Decl;
- return (GlobalVariables.Contains(v) || TileStaticVariables.Contains(v));
+ return (NonLocalState.Contains(v));
}
}
if (n is IdentifierExpr)
{
IdentifierExpr node = n as IdentifierExpr;
- return GlobalVariables.Contains(node.Decl) || TileStaticVariables.Contains(node.Decl);
+ return NonLocalState.Contains(node.Decl);
}
return false;
}
- public static bool ContainsNonLocalAccess(AssignLhs lhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public static bool ContainsNonLocalAccess(AssignLhs lhs, INonLocalState NonLocalState)
{
- NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);
+ NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);
if (lhs is SimpleAssignLhs)
{
collector.VisitSimpleAssignLhs(lhs as SimpleAssignLhs);
@@ -65,9 +63,9 @@ namespace GPUVerify return collector.Accesses.Count > 0;
}
- public static bool ContainsNonLocalAccess(Expr rhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public static bool ContainsNonLocalAccess(Expr rhs, INonLocalState NonLocalState)
{
- NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);
+ NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);
collector.VisitExpr(rhs);
return collector.Accesses.Count > 0;
}
@@ -75,7 +73,7 @@ namespace GPUVerify public override Expr VisitNAryExpr(NAryExpr node)
{
- if (IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (IsNonLocalAccess(node, NonLocalState))
{
Accesses.Add(node);
return node;
@@ -85,7 +83,7 @@ namespace GPUVerify public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
- if (IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (IsNonLocalAccess(node, NonLocalState))
{
Accesses.Add(node);
return node;
diff --git a/Source/GPUVerify/NonLocalAccessExtractor.cs b/Source/GPUVerify/NonLocalAccessExtractor.cs index 506ec3c5..553be683 100644 --- a/Source/GPUVerify/NonLocalAccessExtractor.cs +++ b/Source/GPUVerify/NonLocalAccessExtractor.cs @@ -14,14 +14,12 @@ namespace GPUVerify public LocalVariable Declaration = null;
public bool done = false;
- private ICollection<Variable> GlobalVariables;
- private ICollection<Variable> TileStaticVariables;
+ private INonLocalState NonLocalState;
- public NonLocalAccessExtractor(int TempId, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public NonLocalAccessExtractor(int TempId, INonLocalState NonLocalState)
{
this.TempId = TempId;
- this.GlobalVariables = GlobalVariables;
- this.TileStaticVariables = TileStaticVariables;
+ this.NonLocalState = NonLocalState;
}
@@ -32,7 +30,7 @@ namespace GPUVerify return node;
}
- if (!NonLocalAccessCollector.IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (!NonLocalAccessCollector.IsNonLocalAccess(node, NonLocalState))
{
return base.VisitNAryExpr(node);
}
@@ -42,7 +40,7 @@ namespace GPUVerify {
Debug.Assert((temp as NAryExpr).Args.Length == 2);
- if (NonLocalAccessCollector.ContainsNonLocalAccess((temp as NAryExpr).Args[1], GlobalVariables, TileStaticVariables))
+ if (NonLocalAccessCollector.ContainsNonLocalAccess((temp as NAryExpr).Args[1], NonLocalState))
{
return VisitExpr((temp as NAryExpr).Args[1]);
}
@@ -77,7 +75,7 @@ namespace GPUVerify return node;
}
- if (NonLocalAccessCollector.IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (NonLocalAccessCollector.IsNonLocalAccess(node, NonLocalState))
{
done = true;
Declaration = new LocalVariable(node.tok, new TypedIdent(node.tok, "_temp" + TempId, node.Decl.TypedIdent.Type));
diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs new file mode 100644 index 00000000..a4b5e154 --- /dev/null +++ b/Source/GPUVerify/NonLocalStateLists.cs @@ -0,0 +1,45 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class NonLocalStateLists : INonLocalState
+ {
+ private List<Variable> GlobalVariables;
+ private List<Variable> TileStaticVariables;
+
+ public NonLocalStateLists()
+ {
+ GlobalVariables = new List<Variable>();
+ TileStaticVariables = new List<Variable>();
+ }
+
+ public ICollection<Variable> getGlobalVariables()
+ {
+ return GlobalVariables;
+ }
+
+ public ICollection<Variable> getTileStaticVariables()
+ {
+ return TileStaticVariables;
+ }
+
+ public ICollection<Variable> getAllNonLocalVariables()
+ {
+ List<Variable> all = new List<Variable>();
+ all.AddRange(GlobalVariables);
+ all.AddRange(TileStaticVariables);
+ return all;
+ }
+
+ public bool Contains(Variable v)
+ {
+ return getAllNonLocalVariables().Contains(v);
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs new file mode 100644 index 00000000..cca89b52 --- /dev/null +++ b/Source/GPUVerify/Predicator.cs @@ -0,0 +1,256 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class Predicator
+ {
+ private bool AddPredicateParameter;
+ private int WhileLoopCounter;
+ private int IfCounter;
+ private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;
+
+ internal Predicator(bool AddPredicateParameter)
+ {
+ this.AddPredicateParameter = AddPredicateParameter;
+ WhileLoopCounter = 0;
+ IfCounter = 0;
+ RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
+ }
+
+ internal void transform(Implementation impl)
+ {
+ Expr Predicate;
+
+ if (AddPredicateParameter)
+ {
+ VariableSeq NewIns = new VariableSeq();
+ Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));
+ NewIns.Add(PredicateVariable);
+ foreach (Variable v in impl.InParams)
+ {
+ NewIns.Add(v);
+ }
+ impl.InParams = NewIns;
+ Predicate = new IdentifierExpr(impl.tok, PredicateVariable);
+ }
+ else
+ {
+ Predicate = Expr.True;
+ }
+
+ impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);
+ AddPredicateLocalVariables(impl);
+ }
+
+
+ private StmtList MakePredicated(StmtList sl, Expr predicate, IdentifierExpr EnclosingLoopPredicate)
+ {
+ StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);
+
+ foreach (BigBlock bodyBlock in sl.BigBlocks)
+ {
+ List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);
+ foreach (BigBlock newBigBlock in newBigBlocks)
+ {
+ result.BigBlocks.Add(newBigBlock);
+ }
+ }
+
+ return result;
+
+ }
+
+ private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)
+ {
+ // Not sure what to do about the transfer command
+
+ List<BigBlock> result = new List<BigBlock>();
+
+ BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);
+ result.Add(firstBigBlock);
+
+ foreach (Cmd c in b.simpleCmds)
+ {
+ if (c is CallCmd)
+ {
+
+ CallCmd Call = c as CallCmd;
+
+ List<Expr> NewIns = new List<Expr>();
+ NewIns.Add(IncomingPredicate);
+
+ foreach (Expr e in Call.Ins)
+ {
+ NewIns.Add(e);
+ }
+
+ CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);
+
+ firstBigBlock.simpleCmds.Add(NewCallCmd);
+ }
+ else if (IncomingPredicate.Equals(Expr.True))
+ {
+ firstBigBlock.simpleCmds.Add(c);
+ }
+ else if (c is AssignCmd)
+ {
+ AssignCmd assign = c as AssignCmd;
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+
+ ExprSeq iteArgs = new ExprSeq();
+ iteArgs.Add(IncomingPredicate);
+ iteArgs.Add(assign.Rhss.ElementAt(0));
+ iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);
+ NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);
+
+ List<Expr> newRhs = new List<Expr>();
+ newRhs.Add(ite);
+
+ AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);
+
+ firstBigBlock.simpleCmds.Add(newAssign);
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havoc = c as HavocCmd;
+ Debug.Assert(havoc.Vars.Length == 1);
+
+ Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;
+ Debug.Assert(type != null);
+
+ RequiredHavocVariables.Add(type);
+
+ IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));
+ firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ HavocTempExpr
+ })));
+
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));
+
+ List<Expr> rhss = new List<Expr>();
+ rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));
+
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+
+ if (b.ec is WhileCmd)
+ {
+ string LoopPredicate = "_LC" + WhileLoopCounter;
+ WhileLoopCounter++;
+
+ IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));
+ Expr GuardExpr = (b.ec as WhileCmd).Guard;
+
+ List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
+ WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
+
+ List<Expr> WhilePredicateRhss = new List<Expr>();
+ WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));
+
+ WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));
+
+ List<Expr> UpdatePredicateRhss = new List<Expr>();
+ UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));
+
+ CmdSeq updateCmd = new CmdSeq();
+ updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));
+
+ NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));
+
+ firstBigBlock.ec = NewWhile;
+
+ }
+ else if (b.ec is IfCmd)
+ {
+ IfCmd IfCommand = b.ec as IfCmd;
+
+ string IfPredicate = "_P" + IfCounter;
+ IfCounter++;
+
+ IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
+ Expr GuardExpr = IfCommand.Guard;
+
+ List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
+ IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
+
+ List<Expr> IfPredicateRhss = new List<Expr>();
+ IfPredicateRhss.Add(GuardExpr);
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));
+
+ Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
+
+ StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);
+
+ foreach (BigBlock bb in PredicatedThen.BigBlocks)
+ {
+ result.Add(bb);
+ }
+
+ if (IfCommand.elseBlock != null)
+ {
+ StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);
+
+ foreach (BigBlock bb in PredicatedElse.BigBlocks)
+ {
+ result.Add(bb);
+ }
+ }
+
+
+
+
+ }
+ else if (b.ec is BreakCmd)
+ {
+
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(b.tok,
+ new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(b.tok, EnclosingLoopPredicate) }),
+ new List<Expr>(new Expr[] { new NAryExpr(b.tok, new IfThenElse(b.tok), new ExprSeq(new Expr[] { IncomingPredicate, Expr.False, EnclosingLoopPredicate })) })
+ ));
+ firstBigBlock.ec = null;
+
+ }
+ else
+ {
+ Debug.Assert(b.ec == null);
+ }
+
+ return result;
+ }
+
+
+ private void AddPredicateLocalVariables(Implementation impl)
+ {
+ for (int i = 0; i < IfCounter; i++)
+ {
+ impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));
+ }
+ for (int i = 0; i < WhileLoopCounter; i++)
+ {
+ impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));
+ }
+ foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)
+ {
+ impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));
+ }
+
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 90229af0..0f5f8278 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -12,8 +12,8 @@ namespace GPUVerify abstract class RaceInstrumenterBase : IRaceInstrumenter
{
protected GPUVerifier verifier;
- public ICollection<Variable> globalVarsToCheck;
- public ICollection<Variable> tileStaticVarsToCheck;
+
+ public INonLocalState NonLocalStateToCheck;
public int onlyLog1;
public int onlyLog2;
@@ -33,8 +33,15 @@ namespace GPUVerify public void setVerifier(GPUVerifier verifier)
{
this.verifier = verifier;
- globalVarsToCheck = new HashSet<Variable>(verifier.GlobalVariables);
- tileStaticVarsToCheck = new HashSet<Variable>(verifier.TileStaticVariables);
+ NonLocalStateToCheck = new NonLocalStateLists();
+ foreach(Variable v in verifier.NonLocalState.getGlobalVariables())
+ {
+ NonLocalStateToCheck.getGlobalVariables().Add(v);
+ }
+ foreach(Variable v in verifier.NonLocalState.getTileStaticVariables())
+ {
+ NonLocalStateToCheck.getTileStaticVariables().Add(v);
+ }
}
protected abstract void AddRequiresNoPendingAccess(Variable v);
@@ -80,13 +87,7 @@ namespace GPUVerify public void AddRaceCheckingCandidateInvariants(WhileCmd wc)
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddNoReadOrWriteCandidateInvariants(wc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddNoReadOrWriteCandidateInvariants(wc, v);
AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);
@@ -134,12 +135,7 @@ namespace GPUVerify public void AddKernelPrecondition()
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddRequiresNoPendingAccess(v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddRequiresNoPendingAccess(v);
}
@@ -163,12 +159,7 @@ namespace GPUVerify if (failedToFindSecondAccess || !addedLogWrite)
return false;
- foreach (Variable v in globalVarsToCheck)
- {
- AddRaceCheckingDecsAndProcsForVar(v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddRaceCheckingDecsAndProcsForVar(v);
}
@@ -179,12 +170,29 @@ namespace GPUVerify private void AddRaceCheckingDecsAndProcsForVar(Variable v)
{
- AddLogRaceDeclarations(v, "READ");
- AddLogRaceDeclarations(v, "WRITE");
+ IdentifierExprSeq ReadDeclsResetAtBarrier;
+ IdentifierExprSeq WriteDeclsResetAtBarrier;
+ IdentifierExprSeq ReadDeclsModifiedAtLogRead;
+ IdentifierExprSeq WriteDeclsModifiedAtLogWrite;
+
+ AddLogRaceDeclarations(v, "READ", out ReadDeclsResetAtBarrier, out ReadDeclsModifiedAtLogRead);
+ AddLogRaceDeclarations(v, "WRITE", out WriteDeclsResetAtBarrier, out WriteDeclsModifiedAtLogWrite);
AddLogAccessProcedure(v, "READ");
AddLogAccessProcedure(v, "WRITE");
- }
+ HashSet<string> MayCallBarrier = verifier.GetProceduresThatIndirectlyCallProcedure(verifier.BarrierProcedure.Name);
+
+ verifier.ExtendModifiesSetOfProcedures(ReadDeclsResetAtBarrier, MayCallBarrier);
+ verifier.ExtendModifiesSetOfProcedures(WriteDeclsResetAtBarrier, MayCallBarrier);
+
+ HashSet<string> MayCallLogRead = verifier.GetProceduresThatIndirectlyCallProcedure("_LOG_READ_" + v.Name);
+ HashSet<string> MayCallLogWrite = verifier.GetProceduresThatIndirectlyCallProcedure("_LOG_WRITE_" + v.Name);
+
+ verifier.ExtendModifiesSetOfProcedures(ReadDeclsModifiedAtLogRead, MayCallLogRead);
+ verifier.ExtendModifiesSetOfProcedures(WriteDeclsModifiedAtLogWrite, MayCallLogWrite);
+
+ }
+
private StmtList AddRaceCheckCalls(StmtList stmtList)
{
Contract.Requires(stmtList != null);
@@ -242,7 +250,7 @@ namespace GPUVerify AssignLhs lhs = assign.Lhss[0];
Expr rhs = assign.Rhss[0];
- ReadCollector rc = new ReadCollector(globalVarsToCheck, tileStaticVarsToCheck);
+ ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
rc.Visit(rhs);
if (rc.accesses.Count > 0)
{
@@ -271,7 +279,7 @@ namespace GPUVerify }
}
- WriteCollector wc = new WriteCollector(globalVarsToCheck, tileStaticVarsToCheck);
+ WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
wc.Visit(lhs);
if (wc.GetAccess() != null)
{
@@ -331,7 +339,7 @@ namespace GPUVerify }
- protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite);
+ protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog);
protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);
@@ -341,21 +349,13 @@ namespace GPUVerify BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
if (!CommandLineOptions.Eager)
{
- foreach (Variable v in globalVarsToCheck)
- {
- CheckForRaces(tok, checkForRaces, v);
- }
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
CheckForRaces(tok, checkForRaces, v);
}
}
- foreach (Variable v in globalVarsToCheck)
- {
- SetNoAccessOccurred(tok, checkForRaces, v);
- }
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
SetNoAccessOccurred(tok, checkForRaces, v);
}
@@ -431,13 +431,7 @@ namespace GPUVerify public void AddRaceCheckingCandidateRequires(Procedure Proc)
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddNoReadOrWriteCandidateRequires(Proc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddNoReadOrWriteCandidateRequires(Proc, v);
AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
@@ -446,13 +440,7 @@ namespace GPUVerify public void AddRaceCheckingCandidateEnsures(Procedure Proc)
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddNoReadOrWriteCandidateEnsures(Proc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddNoReadOrWriteCandidateEnsures(Proc, v);
AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs index 281620c5..53d9234e 100644 --- a/Source/GPUVerify/ReadCollector.cs +++ b/Source/GPUVerify/ReadCollector.cs @@ -17,8 +17,8 @@ namespace GPUVerify public List<AccessRecord> accesses = new List<AccessRecord>();
- public ReadCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
- : base(GlobalVariables, TileStaticVariables)
+ public ReadCollector(INonLocalState NonLocalState)
+ : base(NonLocalState)
{
}
@@ -83,7 +83,7 @@ namespace GPUVerify this.VisitExpr(node.Args[1]);
- if (GlobalVariables.Contains(ReadVariable) || TileStaticVariables.Contains(ReadVariable))
+ if (NonLocalState.Contains(ReadVariable))
{
accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));
}
@@ -100,7 +100,7 @@ namespace GPUVerify public override Variable VisitVariable(Variable node)
{
- if (!(GlobalVariables.Contains(node) || TileStaticVariables.Contains(node)))
+ if (!NonLocalState.Contains(node))
{
return node;
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index c4f42923..3b1f877e 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -11,7 +11,7 @@ namespace GPUVerify class SetEncodingRaceInstrumenter : RaceInstrumenterBase
{
- protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)
{
Variable AccessSet = MakeAccessSetVariable(v, ReadOrWrite);
@@ -22,9 +22,9 @@ namespace GPUVerify verifier.Program.TopLevelDeclarations.Add(AccessSet);
- // TODO: add modiies to every procedure that calls BARRIER
+ ResetAtBarrier = new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, AccessSet) });
+ ModifiedAtLog = ResetAtBarrier;
- verifier.KernelProcedure.Modifies.Add(new IdentifierExpr(v.tok, AccessSet));
}
private static Variable MakeAccessSetVariable(Variable v, String ReadOrWrite)
@@ -192,13 +192,11 @@ namespace GPUVerify MakeAccessSetVariable(v, AccessType)));
IdentifierExprSeq VariablesToHavoc = new IdentifierExprSeq();
VariablesToHavoc.Add(AccessSet1);
- verifier.BarrierProcedure.Modifies.Add(AccessSet1);
if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
{
IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(
MakeAccessSetVariable(v, AccessType)));
VariablesToHavoc.Add(AccessSet2);
- verifier.BarrierProcedure.Modifies.Add(AccessSet2);
}
bb.simpleCmds.Add(new HavocCmd(tok, VariablesToHavoc));
diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs index e8623e3b..d55c5d05 100644 --- a/Source/GPUVerify/WriteCollector.cs +++ b/Source/GPUVerify/WriteCollector.cs @@ -13,15 +13,15 @@ namespace GPUVerify private AccessRecord access = null;
- public WriteCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
- : base(GlobalVariables, TileStaticVariables)
+ public WriteCollector(INonLocalState NonLocalState)
+ : base(NonLocalState)
{
}
public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
{
Debug.Assert(NoWrittenVariable());
- if (GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable))
+ if (NonLocalState.Contains(node.DeepAssignedVariable))
{
access = new AccessRecord(node.DeepAssignedVariable, null, null, null);
}
@@ -37,7 +37,7 @@ namespace GPUVerify {
Debug.Assert(NoWrittenVariable());
- if (!(GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable)))
+ if (!NonLocalState.Contains(node.DeepAssignedVariable))
{
return node;
}
|