diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/GPUVerify/AsymmetricExpressionFinder.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 26 | ||||
| -rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 374 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 64 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/IRaceInstrumenter.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs | 22 | ||||
| -rw-r--r-- | Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs | 54 | ||||
| -rw-r--r-- | Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs | 61 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 123 | ||||
| -rw-r--r-- | Source/GPUVerify/LoopInvariantGenerator.cs | 90 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/NullRaceInstrumenter.cs | 16 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 217 | ||||
| -rw-r--r-- | Source/GPUVerify/SetEncodingRaceInstrumenter.cs | 532 |
15 files changed, 346 insertions, 1252 deletions
diff --git a/Source/GPUVerify/AsymmetricExpressionFinder.cs b/Source/GPUVerify/AsymmetricExpressionFinder.cs index 40c7eb32..4fb18352 100644 --- a/Source/GPUVerify/AsymmetricExpressionFinder.cs +++ b/Source/GPUVerify/AsymmetricExpressionFinder.cs @@ -18,7 +18,9 @@ namespace GPUVerify public override Variable VisitVariable(Variable node)
{
if (node.TypedIdent.Name.Contains("_READ_HAS_OCCURRED") ||
- node.TypedIdent.Name.Contains("_READ_OFFSET"))
+ node.TypedIdent.Name.Contains("_READ_OFFSET") ||
+ node.TypedIdent.Name.Contains("_WRITE_HAS_OCCURRED") ||
+ node.TypedIdent.Name.Contains("_WRITE_OFFSET"))
{
found = true;
}
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index b2e54dbd..502844b2 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -24,18 +24,12 @@ namespace GPUVerify public static bool DividedArray = false;
public static string ArrayToCheck = null;
public static bool DividedAccesses = false;
- public static bool Eager = false;
-
- public static bool Symmetry = false;
- public static bool SetEncoding = false;
public static bool ShowStages = false;
public static bool AddDivergenceCandidatesOnlyIfModified = true;
public static bool AddDivergenceCandidatesOnlyToBarrierLoops = true;
- public static bool AssignAtBarriers = false;
-
public static bool ShowUniformityAnalysis = false;
public static bool DoUniformityAnalysis = true;
@@ -121,21 +115,6 @@ namespace GPUVerify DividedArray = true;
break;
- case "-symmetry":
- case "/symmetry":
- Symmetry = true;
- break;
-
- case "-setEncoding":
- case "/setEncoding":
- SetEncoding = true;
- break;
-
- case "-eager":
- case "/eager":
- Eager = true;
- break;
-
case "-showStages":
case "/showStages":
ShowStages = true;
@@ -163,11 +142,6 @@ namespace GPUVerify AddDivergenceCandidatesOnlyToBarrierLoops = false;
break;
- case "-assignAtBarriers":
- case "/assignAtBarriers":
- AssignAtBarriers = true;
- break;
-
case "-showUniformityAnalysis":
case "/showUniformityAnalysis":
ShowUniformityAnalysis = true;
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 1763bb58..c249ef0f 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -18,41 +18,20 @@ namespace GPUVerify - protected override void AddLogAccessProcedure(Variable v, string ReadOrWrite)
+ protected override void AddLogAccessProcedure(Variable v, string Access)
{
- Variable XParameterVariable;
- Variable YParameterVariable;
- Variable ZParameterVariable;
- Procedure LogReadOrWriteProcedure;
+ Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);
- MakeLogAccessProcedureHeader(v, ReadOrWrite, out XParameterVariable, out YParameterVariable, out ZParameterVariable, out LogReadOrWriteProcedure);
+ Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);
+ Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, Access);
- IdentifierExprSeq modifies = LogReadOrWriteProcedure.Modifies;
- Variable ReadOrWriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
- Variable ReadOrWriteOffsetXVariable = null;
- Variable ReadOrWriteOffsetYVariable = null;
- Variable ReadOrWriteOffsetZVariable = null;
+ Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));
- if (XParameterVariable != null)
- {
- ReadOrWriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetXVariable));
- }
- if (YParameterVariable != null)
- {
- Debug.Assert(XParameterVariable != null);
- ReadOrWriteOffsetYVariable = GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite);
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetYVariable));
- }
- if (ZParameterVariable != null)
- {
- Debug.Assert(XParameterVariable != null);
- Debug.Assert(YParameterVariable != null);
- ReadOrWriteOffsetZVariable = GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite);
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetZVariable));
- }
-
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteHasOccurredVariable));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+ Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
+ Debug.Assert(!(mt.Result is MapType));
VariableSeq locals = new VariableSeq();
Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));
@@ -63,103 +42,110 @@ namespace GPUVerify CmdSeq simpleCmds = new CmdSeq();
simpleCmds.Add(new HavocCmd(v.tok, new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, TrackVariable) })));
- simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteHasOccurredVariable, new IdentifierExpr(v.tok, TrackVariable), Expr.True));
- if (ReadOrWriteOffsetXVariable != null)
- {
- simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetXVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, XParameterVariable)));
- }
- if (ReadOrWriteOffsetYVariable != null)
- {
- simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetYVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, YParameterVariable)));
- }
- if (ReadOrWriteOffsetZVariable != null)
- {
- simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetZVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, ZParameterVariable)));
- }
-
-
- bigblocks.Add(new BigBlock(v.tok, "_LOG_" + ReadOrWrite + "", simpleCmds, null, null));
- StmtList statements = new StmtList(bigblocks, v.tok);
+ simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable),
+ Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));
+ simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable),
+ Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)),
+ new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));
- Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), LogReadOrWriteProcedure.InParams, new VariableSeq(), locals, statements);
- LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
-
- LogReadOrWriteImplementation.Proc = LogReadOrWriteProcedure;
-
- verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
- verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
- }
-
- protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)
- {
- ModifiedAtLog = new IdentifierExprSeq();
- ResetAtBarrier = new IdentifierExprSeq();
-
- Variable AccessHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
-
- if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ if (Access.Equals("READ"))
{
- verifier.HalfDualisedVariableNames.Add(AccessHasOccurred.Name);
+ // Check read by thread 2 does not conflict with write by thread 1
+ Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
+ Variable WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");
+ Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
+ WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ ));
+ }
+ WriteReadGuard = Expr.Not(WriteReadGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard));
}
-
- 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)
+ else
{
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
+ Debug.Assert(Access.Equals("WRITE"));
- Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);
+ // Check write by thread 2 does not conflict with write by thread 1
+ Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
+ Variable WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");
- if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
+ WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
+ ));
+ }
+ WriteWriteGuard = Expr.Not(WriteWriteGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard));
+
+ // Check write by thread 2 does not conflict with read by thread 1
+ Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");
+ Variable ReadOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "READ");
+
+ Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));
+ ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v))
{
- verifier.HalfDualisedVariableNames.Add(AccessOffsetX.Name);
+ ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ ));
}
+ ReadWriteGuard = Expr.Not(ReadWriteGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard));
- ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetX));
- verifier.Program.TopLevelDeclarations.Add(AccessOffsetX);
+ }
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
+ bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));
- Variable AccessOffsetY = GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite);
+ LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));
+ LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));
- if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
- {
- verifier.HalfDualisedVariableNames.Add(AccessOffsetY.Name);
- }
+ Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));
+ LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
- ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetY));
- verifier.Program.TopLevelDeclarations.Add(AccessOffsetY);
+ LogAccessImplementation.Proc = LogAccessProcedure;
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
+ verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);
+ verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);
+ }
- Variable AccessOffsetZ = GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite);
+ private Variable VariableForThread(int thread, Variable v)
+ {
+ return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);
+ }
- if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
- {
- verifier.HalfDualisedVariableNames.Add(AccessOffsetZ.Name);
- }
+ protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ {
+ Variable AccessHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
- ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetZ));
- verifier.Program.TopLevelDeclarations.Add(AccessOffsetZ);
- }
- }
- }
+ // Assumes full symmetry reduction
- }
+ verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessHasOccurred.Clone() as Variable));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+
+ Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);
+ verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessOffsetX.Clone() as Variable));
+
+ }
+
private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)
{
@@ -174,144 +160,29 @@ namespace GPUVerify {
IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok,
new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, AccessType)));
- IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok,
- new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, AccessType)));
-
- if (CommandLineOptions.AssignAtBarriers)
- {
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
-
- lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));
- rhss.Add(Expr.False);
-
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
- {
- lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));
- rhss.Add(Expr.False);
- }
-
- bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
- }
- else
- {
- bb.simpleCmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(AccessOccurred1)));
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
- {
- bb.simpleCmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(AccessOccurred2)));
- }
- }
+ bb.simpleCmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(AccessOccurred1)));
}
- public override void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly)
+ private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType)
{
- if (!ReadWriteOnly)
- {
- bb.simpleCmds.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));
- }
- bb.simpleCmds.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));
- if (!CommandLineOptions.Symmetry)
- {
- bb.simpleCmds.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));
- }
- }
-
- protected override Expr GenerateRaceCondition(Variable v, string FirstAccessType, string SecondAccessType)
- {
- Expr RaceCondition = Expr.And(
- new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, SecondAccessType))));
-
- if (GPUVerifier.HasXDimension(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, SecondAccessType)))
- ));
- }
-
- if (GPUVerifier.HasYDimension(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, SecondAccessType)))
- ));
- }
-
- if (GPUVerifier.HasZDimension(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, SecondAccessType)))
- ));
- }
-
- if (FirstAccessType.Equals("WRITE") && SecondAccessType.Equals("WRITE") && !verifier.ArrayModelledAdversarially(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Neq(
- MakeWrittenIndex(v, 1),
- MakeWrittenIndex(v, 2)
- ));
- }
-
- return RaceCondition;
- }
-
- private static Expr MakeWrittenIndex(Variable v, int OneOrTwo)
- {
- Expr result = new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(v.Clone() as Variable));
-
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
-
- result = Expr.Select(result,
- new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, "WRITE"))) });
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- result = Expr.Select(result,
- new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, "WRITE"))) });
-
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
-
- result = Expr.Select(result,
- new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, "WRITE"))) });
-
- }
- }
- }
-
+ Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+
+ result = Expr.Select(result,
+ new Expr[] { offsetExpr });
+ Debug.Assert(!(mt.Result is MapType));
return result;
-
}
protected override void AddRequiresNoPendingAccess(Variable v)
{
IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));
- IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));
IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));
- IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));
- if (CommandLineOptions.Symmetry)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.And(Expr.Not(WriteAccessOccurred1), Expr.Not(WriteAccessOccurred2)))));
- }
- else
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.And(Expr.Not(ReadAccessOccurred2), Expr.And(Expr.Not(WriteAccessOccurred1), Expr.Not(WriteAccessOccurred2))))));
- }
+ verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));
}
protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
@@ -327,24 +198,12 @@ namespace GPUVerify protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 1);
-
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 2));
- }
-
verifier.AddCandidateInvariant(wc, expr, "accessed offset is global id");
}
protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 1);
-
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 2));
- }
-
verifier.AddCandidateInvariant(wc, expr, "accessed offset is local id");
}
@@ -391,11 +250,6 @@ namespace GPUVerify protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 1);
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 2));
- }
-
verifier.AddCandidateInvariant(wc, expr, "accessed offset is flattened 2D local id");
}
@@ -420,11 +274,6 @@ namespace GPUVerify protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 1);
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 2));
- }
-
verifier.AddCandidateInvariant(wc, expr, "accessed offset is flattened 2D global id");
}
@@ -448,14 +297,7 @@ namespace GPUVerify protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)
{
-
Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
-
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 2));
- }
-
verifier.AddCandidateInvariant(wc,
expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");
}
@@ -490,12 +332,6 @@ namespace GPUVerify protected override void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)
{
Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);
-
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 2));
- }
-
verifier.AddCandidateInvariant(wc,
expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 9acf7619..f6ba390b 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -23,9 +23,6 @@ namespace GPUVerify private HashSet<string> ReservedNames = new HashSet<string>();
- internal HashSet<string> HalfDualisedProcedureNames = new HashSet<string>();
- internal HashSet<string> HalfDualisedVariableNames = new HashSet<string>();
-
private int TempCounter = 0;
private int invariantGenerationCounter;
@@ -375,10 +372,7 @@ namespace GPUVerify emitProgram(outputFilename + "_cross_thread_invariants");
}
- if (CommandLineOptions.Eager)
- {
- AddEagerRaceChecking();
- }
+ RaceInstrumenter.AddRaceCheckingDeclarations();
GenerateBarrierImplementation();
@@ -614,36 +608,6 @@ namespace GPUVerify }
}
- private void AddEagerRaceChecking()
- {
- foreach(Variable v in NonLocalState.getAllNonLocalVariables())
- {
- 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(bb, v, impl.Name.Equals("_LOG_READ_" + v.Name));
- 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()
{
@@ -1069,16 +1033,6 @@ namespace GPUVerify }
KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds = newCommands;
- // Last barrier is needed if we don't use eager race checking
- if (!CommandLineOptions.Eager)
- {
- CmdSeq lastCommand = new CmdSeq();
- lastCommand.Add(LastBarrier);
- BigBlock bb = new BigBlock(KernelProcedure.tok, "__lastBarrier", lastCommand, null, null);
-
- KernelImplementation.StructuredStmts.BigBlocks.Add(bb);
- }
-
}
private void GenerateStandardKernelContract()
@@ -1112,11 +1066,7 @@ namespace GPUVerify Proc.Requires.Add(new Requires(false, AssumeDistinctThreads));
Proc.Requires.Add(new Requires(false, AssumeThreadIdsInRange));
- if (Proc != KernelProcedure)
- {
- RaceInstrumenter.AddNoRaceContract(Proc);
- }
- else
+ if (Proc == KernelProcedure)
{
bool foundNonUniform = false;
int indexOfFirstNonUniformParameter;
@@ -1157,8 +1107,6 @@ namespace GPUVerify }
Implementation Impl = D as Implementation;
- RaceInstrumenter.AddNoRaceInvariants(Impl);
-
if (QKeyValue.FindIntAttribute(Impl.Proc.Attributes, "inline", -1) == 1)
{
continue;
@@ -1360,7 +1308,7 @@ namespace GPUVerify checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);
}
- bigblocks.Add(RaceInstrumenter.MakeRaceCheckingStatements(tok));
+ bigblocks.Add(RaceInstrumenter.MakeResetReadWriteSetsStatements(tok));
BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);
bigblocks.Add(havocSharedState);
@@ -1983,11 +1931,7 @@ namespace GPUVerify if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)))
{
NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)d.Clone()));
-
- if (!HalfDualisedVariableNames.Contains((d as Variable).Name))
- {
- NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)d.Clone()));
- }
+ NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)d.Clone()));
continue;
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 9881b0f0..5b0f7e3e 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -108,6 +108,9 @@ <Compile Include="AccessRecord.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
+ <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
+ <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
<Compile Include="MayBeGlobalSizeAnalyser.cs" />
<Compile Include="MayBeFlattened2DTidOrGidAnalyser.cs" />
<Compile Include="MayBeGidAnalyser.cs" />
@@ -136,7 +139,6 @@ <Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="RaceInstrumenterBase.cs" />
<Compile Include="ReadCollector.cs" />
- <Compile Include="SetEncodingRaceInstrumenter.cs" />
<Compile Include="UniformExpressionAnalysisVisitor.cs" />
<Compile Include="UniformityAnalyser.cs" />
<Compile Include="VariableDualiser.cs" />
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs index f1b877a5..65d2cc1b 100644 --- a/Source/GPUVerify/IRaceInstrumenter.cs +++ b/Source/GPUVerify/IRaceInstrumenter.cs @@ -18,16 +18,13 @@ namespace GPUVerify // this will return false.
bool AddRaceCheckingInstrumentation();
- BigBlock MakeRaceCheckingStatements(IToken tok);
+ void AddRaceCheckingDeclarations();
- void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly);
+ BigBlock MakeResetReadWriteSetsStatements(IToken tok);
void AddRaceCheckingCandidateRequires(Procedure Proc);
void AddRaceCheckingCandidateEnsures(Procedure Proc);
- void AddNoRaceContract(Procedure Proc);
-
- void AddNoRaceInvariants(Implementation Impl);
}
}
diff --git a/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs new file mode 100644 index 00000000..1bd66785 --- /dev/null +++ b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs @@ -0,0 +1,22 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify.InvariantGenerationRules
+{
+ abstract class InvariantGenerationRule
+ {
+ protected GPUVerifier verifier;
+
+ public InvariantGenerationRule(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ }
+
+ public abstract void GenerateCandidates(Implementation Impl, WhileCmd wc);
+ }
+
+}
diff --git a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs new file mode 100644 index 00000000..233b3b45 --- /dev/null +++ b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs @@ -0,0 +1,54 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify.InvariantGenerationRules
+{
+ class LoopVariableBoundsInvariantGenerator : InvariantGenerationRule
+ {
+
+ public LoopVariableBoundsInvariantGenerator(GPUVerifier verifier)
+ : base(verifier)
+ {
+
+ }
+
+ public override void GenerateCandidates(Implementation Impl, WhileCmd wc)
+ {
+ if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))
+ {
+ VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
+ visitor.VisitExpr(wc.Guard);
+ foreach (Variable v in visitor.GetVariables())
+ {
+ if (!verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(wc.Body), v.Name))
+ {
+ continue;
+ }
+
+ if (IsBVType (v.TypedIdent.Type))
+ {
+ int BVWidth = (v.TypedIdent.Type as BvType).Bits;
+
+ verifier.AddCandidateInvariant(wc,
+ GPUVerifier.MakeBitVectorBinaryBoolean("BV" + BVWidth + "_GEQ",
+ new IdentifierExpr(v.tok, v),
+ new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");
+ }
+ }
+ }
+ }
+
+ private bool IsBVType(Microsoft.Boogie.Type type)
+ {
+ return type.Equals(Microsoft.Boogie.Type.GetBvType(32))
+ || type.Equals(Microsoft.Boogie.Type.GetBvType(16))
+ || type.Equals(Microsoft.Boogie.Type.GetBvType(8));
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs new file mode 100644 index 00000000..6b2bdc56 --- /dev/null +++ b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs @@ -0,0 +1,61 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify.InvariantGenerationRules
+{
+ class PowerOfTwoInvariantGenerator : InvariantGenerationRule
+ {
+
+ public PowerOfTwoInvariantGenerator(GPUVerifier verifier)
+ : base(verifier)
+ {
+
+ }
+
+ public override void GenerateCandidates(Implementation Impl, WhileCmd wc)
+ {
+ foreach (Variable v in Impl.LocVars)
+ {
+ string basicName = GPUVerifier.StripThreadIdentifier(v.Name);
+ if (verifier.uniformityAnalyser.IsUniform(Impl.Name, basicName))
+ {
+ if (verifier.mayBePowerOfTwoAnalyser.MayBePowerOfTwo(Impl.Name, basicName))
+ {
+ if (verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(wc.Body), basicName))
+ {
+ verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v), "pow2 disjunction");
+ for (int i = (1 << 15); i > 0; i >>= 1)
+ {
+ verifier.AddCandidateInvariant(wc,
+ GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",
+ new IdentifierExpr(v.tok, v),
+ new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);
+ }
+ verifier.AddCandidateInvariant(wc,
+ Expr.Neq(new IdentifierExpr(v.tok, v),
+ new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");
+ }
+ }
+ }
+ }
+ }
+
+ private Expr MakePowerOfTwoExpr(Variable v)
+ {
+ Expr result = null;
+ for (int i = 1 << 15; i > 0; i >>= 1)
+ {
+ Expr eq = Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(i), 32));
+ result = (result == null ? eq : Expr.Or(eq, result));
+ }
+
+ return Expr.Or(Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), result);
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 41546a84..0496a4e0 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -23,30 +23,11 @@ namespace GPUVerify {
procName = proc.Name;
- bool HalfDualise = verifier.HalfDualisedProcedureNames.Contains(proc.Name);
-
proc.Requires = DualiseRequires(proc.Requires);
proc.Ensures = DualiseEnsures(proc.Ensures);
- proc.InParams = DualiseVariableSequence(proc.InParams, HalfDualise);
- proc.OutParams = DualiseVariableSequence(proc.OutParams, HalfDualise);
- IdentifierExprSeq NewModifies = new IdentifierExprSeq();
- foreach (IdentifierExpr v in proc.Modifies)
- {
- NewModifies.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
- }
-
- if (!HalfDualise)
- {
- foreach (IdentifierExpr v in proc.Modifies)
- {
- if (!CommandLineOptions.Symmetry || !verifier.HalfDualisedVariableNames.Contains(v.Name))
- {
- NewModifies.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
- }
- }
- }
- proc.Modifies = NewModifies;
+ proc.InParams = DualiseVariableSequence(proc.InParams);
+ proc.OutParams = DualiseVariableSequence(proc.OutParams);
procName = null;
}
@@ -59,7 +40,7 @@ namespace GPUVerify newRequires.Add(new Requires(r.Free, new VariableDualiser(1, verifier.uniformityAnalyser, procName).
VisitExpr(r.Condition.Clone() as Expr)));
- if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(r.Condition))
+ if (!ContainsAsymmetricExpression(r.Condition)
&& !verifier.uniformityAnalyser.IsUniform(procName, r.Condition))
{
newRequires.Add(new Requires(r.Free, new VariableDualiser(2, verifier.uniformityAnalyser, procName).
@@ -76,7 +57,7 @@ namespace GPUVerify {
newEnsures.Add(new Ensures(e.Free, new VariableDualiser(1, verifier.uniformityAnalyser, procName).
VisitExpr(e.Condition.Clone() as Expr)));
- if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(e.Condition))
+ if (!ContainsAsymmetricExpression(e.Condition)
&& !verifier.uniformityAnalyser.IsUniform(procName, e.Condition))
{
newEnsures.Add(new Ensures(e.Free, new VariableDualiser(2, verifier.uniformityAnalyser, procName).
@@ -87,7 +68,7 @@ namespace GPUVerify }
- private StmtList MakeDual(StmtList stmtList, bool HalfDualise)
+ private StmtList MakeDual(StmtList stmtList)
{
Contract.Requires(stmtList != null);
@@ -95,13 +76,13 @@ namespace GPUVerify foreach (BigBlock bodyBlock in stmtList.BigBlocks)
{
- result.BigBlocks.Add(MakeDual(bodyBlock, HalfDualise));
+ result.BigBlocks.Add(MakeDual(bodyBlock));
}
return result;
}
- private BigBlock MakeDual(BigBlock bb, bool HalfDualise)
+ private BigBlock MakeDual(BigBlock bb)
{
// Not sure what to do about the transfer command
@@ -126,14 +107,11 @@ namespace GPUVerify nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
}
}
- if (!HalfDualise && !verifier.HalfDualisedProcedureNames.Contains(Call.callee))
+ for (int i = 0; i < Call.Ins.Count; i++)
{
- for (int i = 0; i < Call.Ins.Count; i++)
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
{
- if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
- {
- nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
- }
+ nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
}
}
@@ -154,14 +132,11 @@ namespace GPUVerify }
}
- if (!HalfDualise && !verifier.HalfDualisedProcedureNames.Contains(Call.callee))
+ for (int i = 0; i < Call.Outs.Count; i++)
{
- for (int i = 0; i < Call.Outs.Count; i++)
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
{
- if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
- {
- nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
- }
+ nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
}
}
@@ -191,18 +166,10 @@ namespace GPUVerify List<Expr> newRhss = new List<Expr>();
newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
-
- if (!HalfDualise)
- {
- newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
- }
+ newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
-
- if (!HalfDualise)
- {
- newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
- }
+ newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
@@ -216,25 +183,17 @@ namespace GPUVerify HavocCmd newHavoc;
- if (HalfDualise)
- {
- newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
- }
- else
- {
- newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
- (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
- }
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
+ (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
+
result.simpleCmds.Add(newHavoc);
}
else if (c is AssertCmd)
{
AssertCmd ass = c as AssertCmd;
- if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
+ if (ContainsAsymmetricExpression(ass.Expr))
{
result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
}
@@ -247,7 +206,7 @@ namespace GPUVerify else if (c is AssumeCmd)
{
AssumeCmd ass = c as AssumeCmd;
- if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
+ if (ContainsAsymmetricExpression(ass.Expr))
{
result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
}
@@ -278,16 +237,16 @@ namespace GPUVerify }
result.ec = new WhileCmd(bb.ec.tok,
NewGuard,
- MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
+ MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body));
}
else if (bb.ec is IfCmd)
{
Debug.Assert(verifier.uniformityAnalyser.IsUniform(procName, (bb.ec as IfCmd).Guard));
result.ec = new IfCmd(bb.ec.tok,
(bb.ec as IfCmd).Guard,
- MakeDual((bb.ec as IfCmd).thn, HalfDualise),
+ MakeDual((bb.ec as IfCmd).thn),
null,
- (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock, HalfDualise));
+ (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock));
}
else if (bb.ec is BreakCmd)
@@ -314,7 +273,7 @@ namespace GPUVerify newP.Attributes = p.Attributes;
result.Add(newP);
}
- if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr))
+ if (!ContainsAsymmetricExpression(p.Expr)
&& !verifier.uniformityAnalyser.IsUniform(procName, p.Expr))
{
PredicateCmd newP = new AssertCmd(p.tok, Dualise(p.Expr, 2));
@@ -326,7 +285,7 @@ namespace GPUVerify return result;
}
- private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)
+ private void MakeDualLocalVariables(Implementation impl)
{
VariableSeq NewLocalVars = new VariableSeq();
@@ -340,11 +299,8 @@ namespace GPUVerify {
NewLocalVars.Add(
new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));
- if (!HalfDualise)
- {
- NewLocalVars.Add(
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));
- }
+ NewLocalVars.Add(
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));
}
}
@@ -358,7 +314,7 @@ namespace GPUVerify return finder.foundAsymmetricExpr();
}
- private VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise)
+ private VariableSeq DualiseVariableSequence(VariableSeq seq)
{
VariableSeq uniform = new VariableSeq();
VariableSeq nonuniform = new VariableSeq();
@@ -375,14 +331,11 @@ namespace GPUVerify }
}
- if (!HalfDualise)
+ foreach (Variable v in seq)
{
- foreach (Variable v in seq)
+ if (!verifier.uniformityAnalyser.IsUniform(procName, v.Name))
{
- if (!verifier.uniformityAnalyser.IsUniform(procName, v.Name))
- {
- nonuniform.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable((Variable)v.Clone()));
- }
+ nonuniform.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable((Variable)v.Clone()));
}
}
@@ -396,12 +349,10 @@ namespace GPUVerify {
procName = impl.Name;
- bool HalfDualise = verifier.HalfDualisedProcedureNames.Contains(impl.Name);
-
- impl.InParams = DualiseVariableSequence(impl.InParams, HalfDualise);
- impl.OutParams = DualiseVariableSequence(impl.OutParams, HalfDualise);
- MakeDualLocalVariables(impl, HalfDualise);
- impl.StructuredStmts = MakeDual(impl.StructuredStmts, HalfDualise);
+ impl.InParams = DualiseVariableSequence(impl.InParams);
+ impl.OutParams = DualiseVariableSequence(impl.OutParams);
+ MakeDualLocalVariables(impl);
+ impl.StructuredStmts = MakeDual(impl.StructuredStmts);
procName = null;
}
diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs index 6411025d..ead78917 100644 --- a/Source/GPUVerify/LoopInvariantGenerator.cs +++ b/Source/GPUVerify/LoopInvariantGenerator.cs @@ -6,6 +6,8 @@ using Microsoft.Boogie; using Microsoft.Basetypes;
using System.Diagnostics;
+using GPUVerify.InvariantGenerationRules;
+
namespace GPUVerify
{
class LoopInvariantGenerator
@@ -13,10 +15,16 @@ namespace GPUVerify private GPUVerifier verifier;
private Implementation Impl;
+ private List<InvariantGenerationRule> invariantGenerationRules;
+
public LoopInvariantGenerator(GPUVerifier verifier, Implementation Impl)
{
this.verifier = verifier;
this.Impl = Impl;
+
+ invariantGenerationRules = new List<InvariantGenerationRule>();
+ invariantGenerationRules.Add(new PowerOfTwoInvariantGenerator(verifier));
+ invariantGenerationRules.Add(new LoopVariableBoundsInvariantGenerator(verifier));
}
internal void instrument(List<Expr> UserSuppliedInvariants)
@@ -149,11 +157,12 @@ namespace GPUVerify {
WhileCmd wc = bb.ec as WhileCmd;
- AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
-
- AddLoopVariableBoundsCandidateInvariants(Impl, wc);
+ foreach (InvariantGenerationRule r in invariantGenerationRules)
+ {
+ r.GenerateCandidates(Impl, wc);
+ }
- AddPowerOfTwoCandidateInvariants(Impl, wc);
+ AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, wc);
@@ -177,79 +186,6 @@ namespace GPUVerify }
}
- private void AddPowerOfTwoCandidateInvariants(Implementation Impl, WhileCmd wc)
- {
- foreach (Variable v in Impl.LocVars)
- {
- string basicName = GPUVerifier.StripThreadIdentifier(v.Name);
- if (verifier.uniformityAnalyser.IsUniform(Impl.Name, basicName))
- {
- if (verifier.mayBePowerOfTwoAnalyser.MayBePowerOfTwo(Impl.Name, basicName))
- {
- if (verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), basicName))
- {
- verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v), "pow2 disjunction");
- for (int i = (1 << 15); i > 0; i >>= 1)
- {
- verifier.AddCandidateInvariant(wc,
- GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",
- new IdentifierExpr(v.tok, v),
- new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);
- }
- verifier.AddCandidateInvariant(wc,
- Expr.Neq(new IdentifierExpr(v.tok, v),
- new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");
- }
- }
- }
- }
- }
-
- private Expr MakePowerOfTwoExpr(Variable v)
- {
- Expr result = null;
- for (int i = 1 << 15; i > 0; i >>= 1)
- {
- Expr eq = Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(i), 32));
- result = (result == null ? eq : Expr.Or(eq, result));
- }
-
- return Expr.Or(Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), result);
- }
-
- private void AddLoopVariableBoundsCandidateInvariants(Implementation Impl, WhileCmd wc)
- {
- if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))
- {
- VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
- visitor.VisitExpr(wc.Guard);
- foreach (Variable v in visitor.GetVariables())
- {
- if (!verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), v.Name))
- {
- continue;
- }
-
- if (IsBVType (v.TypedIdent.Type))
- {
- int BVWidth = (v.TypedIdent.Type as BvType).Bits;
-
- verifier.AddCandidateInvariant(wc,
- GPUVerifier.MakeBitVectorBinaryBoolean("BV" + BVWidth + "_GEQ",
- new IdentifierExpr(v.tok, v),
- new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");
- }
- }
- }
- }
-
- private bool IsBVType(Microsoft.Boogie.Type type)
- {
- return type.Equals(Microsoft.Boogie.Type.GetBvType(32))
- || type.Equals(Microsoft.Boogie.Type.GetBvType(16))
- || type.Equals(Microsoft.Boogie.Type.GetBvType(8));
- }
-
private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants, Implementation Impl)
{
foreach (Expr e in UserSuppliedInvariants)
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 48cd8a2f..1e0a6b4a 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -91,7 +91,7 @@ namespace GPUVerify public static bool doit(string filename, Variable v, int a1, int a2)
{
Program newProgram = parse();
- RaceInstrumenterBase ri = CommandLineOptions.SetEncoding ? (RaceInstrumenterBase)new SetEncodingRaceInstrumenter() : (RaceInstrumenterBase) new ElementEncodingRaceInstrumenter();
+ RaceInstrumenterBase ri = new ElementEncodingRaceInstrumenter();
GPUVerifier newGp = new GPUVerifier(filename, newProgram, ri);
ri.setVerifier(newGp);
@@ -184,7 +184,7 @@ namespace GPUVerify {
if (!CommandLineOptions.OnlyDivergence)
{
- RaceInstrumenterBase ri = CommandLineOptions.SetEncoding ? (RaceInstrumenterBase)new SetEncodingRaceInstrumenter() : (RaceInstrumenterBase)new ElementEncodingRaceInstrumenter();
+ RaceInstrumenterBase ri = new ElementEncodingRaceInstrumenter();
ri.setVerifier(g);
g.setRaceInstrumenter(ri);
}
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs index b2941815..73f038fb 100644 --- a/Source/GPUVerify/NullRaceInstrumenter.cs +++ b/Source/GPUVerify/NullRaceInstrumenter.cs @@ -19,18 +19,14 @@ namespace GPUVerify }
- public void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly)
- {
- }
-
public bool AddRaceCheckingInstrumentation()
{
return true;
}
- public Microsoft.Boogie.BigBlock MakeRaceCheckingStatements(Microsoft.Boogie.IToken tok)
+ public Microsoft.Boogie.BigBlock MakeResetReadWriteSetsStatements(Microsoft.Boogie.IToken tok)
{
- return new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
+ return new BigBlock(tok, "__ResetReadWriteSets", new CmdSeq(), null, null);
}
public void AddRaceCheckingCandidateRequires(Procedure Proc)
@@ -43,13 +39,7 @@ namespace GPUVerify }
-
- public void AddNoRaceContract(Procedure proc)
- {
-
- }
-
- public void AddNoRaceInvariants(Implementation impl)
+ public void AddRaceCheckingDeclarations()
{
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 33af1965..7ae7ca44 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -66,15 +66,13 @@ namespace GPUVerify if (verifier.ContainsBarrierCall(wc.Body))
{
if (verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ"))
- || CommandLineOptions.AssignAtBarriers)
+ LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")))
{
AddNoReadOrWriteCandidateInvariant(wc, v, "READ");
}
if (verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE"))
- || CommandLineOptions.AssignAtBarriers)
+ LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE")))
{
AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE");
}
@@ -85,31 +83,17 @@ namespace GPUVerify {
AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");
AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");
- if (!CommandLineOptions.Symmetry)
- {
- AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "2");
- }
- AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "2");
}
private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v)
{
AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");
AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");
- if (!CommandLineOptions.Symmetry)
- {
- AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "2");
- }
- AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "2");
}
private void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
{
Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- candidate = Expr.And(candidate, NoReadOrWriteExpr(v, ReadOrWrite, "2"));
- }
verifier.AddCandidateInvariant(wc, candidate, "no " + ReadOrWrite.ToLower());
}
@@ -201,11 +185,6 @@ namespace GPUVerify private void AddAccessRelatedCandidateInvariant(WhileCmd wc, string accessKind, Expr candidateInvariantExpr, string procName, string tag)
{
Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
- if (accessKind.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- candidate = Expr.And(candidate, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr));
- }
-
verifier.AddCandidateInvariant(wc, candidate, tag);
}
@@ -733,23 +712,13 @@ namespace GPUVerify private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)
{
AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);
- AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 2);
AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);
- if (!CommandLineOptions.Symmetry)
- {
- AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 2);
- }
}
private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v)
{
AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);
- AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 2);
AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
- if (!CommandLineOptions.Symmetry)
- {
- AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 2);
- }
}
protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite);
@@ -777,6 +746,7 @@ namespace GPUVerify AddRequiresNoPendingAccess(v);
}
}
+
public bool AddRaceCheckingInstrumentation()
{
@@ -802,24 +772,14 @@ namespace GPUVerify if (failedToFindSecondAccess || !addedLogWrite)
return false;
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
- {
- AddRaceCheckingDecsAndProcsForVar(v);
- }
-
return true;
}
private void AddRaceCheckingDecsAndProcsForVar(Variable v)
{
- IdentifierExprSeq ReadDeclsResetAtBarrier;
- IdentifierExprSeq WriteDeclsResetAtBarrier;
- IdentifierExprSeq ReadDeclsModifiedAtLogRead;
- IdentifierExprSeq WriteDeclsModifiedAtLogWrite;
-
- AddLogRaceDeclarations(v, "READ", out ReadDeclsResetAtBarrier, out ReadDeclsModifiedAtLogRead);
- AddLogRaceDeclarations(v, "WRITE", out WriteDeclsResetAtBarrier, out WriteDeclsModifiedAtLogWrite);
+ AddLogRaceDeclarations(v, "READ");
+ AddLogRaceDeclarations(v, "WRITE");
AddLogAccessProcedure(v, "READ");
AddLogAccessProcedure(v, "WRITE");
@@ -996,27 +956,20 @@ namespace GPUVerify }
- protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog);
+ protected abstract void AddLogRaceDeclarations(Variable v, string ReadOrWrite);
protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);
- public BigBlock MakeRaceCheckingStatements(IToken tok)
+ public BigBlock MakeResetReadWriteSetsStatements(IToken tok)
{
- BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
- if (!CommandLineOptions.Eager)
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
- {
- CheckForRaces(checkForRaces, v, false);
- }
- }
+ BigBlock result = new BigBlock(tok, "__ResetReadWriteSets", new CmdSeq(), null, null);
foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
- SetNoAccessOccurred(tok, checkForRaces, v);
+ SetNoAccessOccurred(tok, result, v);
}
- return checkForRaces;
+ return result;
}
private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v)
@@ -1027,66 +980,33 @@ namespace GPUVerify protected abstract void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType);
- public abstract void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly);
-
- protected void MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite, out Variable XParameterVariable, out Variable YParameterVariable, out Variable ZParameterVariable, out Procedure LogReadOrWriteProcedure)
+ protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)
{
VariableSeq inParams = new VariableSeq();
- XParameterVariable = null;
- YParameterVariable = null;
- ZParameterVariable = null;
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
+ Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));
- XParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_X_index", mt.Arguments[0]));
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
- YParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Y_index", mt2.Arguments[0]));
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
- ZParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Z_index", mt3.Arguments[0]));
- }
- }
- }
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+ Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
+ Debug.Assert(!(mt.Result is MapType));
- if (ZParameterVariable != null)
- {
- inParams.Add(ZParameterVariable);
- }
-
- if (YParameterVariable != null)
- {
- inParams.Add(YParameterVariable);
- }
+ inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
+ inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
- if (XParameterVariable != null)
- {
- inParams.Add(XParameterVariable);
- }
+ inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
+ inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;
- LogReadOrWriteProcedure = GetLogAccessProcedure(v.tok, LogProcedureName);
+ Procedure result = GetLogAccessProcedure(v.tok, LogProcedureName);
- LogReadOrWriteProcedure.InParams = inParams;
+ result.InParams = inParams;
- if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
- {
- verifier.HalfDualisedProcedureNames.Add(LogReadOrWriteProcedure.Name);
- }
-
- LogReadOrWriteProcedure.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+ result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+ return result;
}
public void AddRaceCheckingCandidateRequires(Procedure Proc)
@@ -1119,81 +1039,6 @@ namespace GPUVerify protected abstract Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo);
-
- public void AddNoRaceContract(Procedure proc)
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
- {
- proc.Requires.Add(new Requires(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));
- proc.Requires.Add(new Requires(false, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));
- if (!CommandLineOptions.Symmetry)
- {
- proc.Requires.Add(new Requires(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));
- }
-
- proc.Ensures.Add(new Ensures(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));
- proc.Ensures.Add(new Ensures(false, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));
- if (!CommandLineOptions.Symmetry)
- {
- proc.Ensures.Add(new Ensures(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));
- }
-
- }
- }
-
- public void AddNoRaceInvariants(Implementation impl)
- {
- AddNoRaceInvariants(impl.StructuredStmts);
- }
-
- private void AddNoRaceInvariants(StmtList stmtList)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- AddNoRaceInvariants(bb);
- }
- }
-
- private void AddNoRaceInvariants(BigBlock bb)
- {
- if (bb.ec is WhileCmd)
- {
- WhileCmd wc = bb.ec as WhileCmd;
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
- {
- wc.Invariants.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));
- wc.Invariants.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));
- if (!CommandLineOptions.Symmetry)
- {
- wc.Invariants.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));
- }
- }
-
- AddNoRaceInvariants(wc.Body);
-
- }
- else if (bb.ec is IfCmd)
- {
- AddNoRaceInvariants((bb.ec as IfCmd).thn);
- if ((bb.ec as IfCmd).elseBlock != null)
- {
- AddNoRaceInvariants((bb.ec as IfCmd).elseBlock);
- }
- }
- else if (bb.ec is BreakCmd)
- {
- // Do nothing
- }
- else
- {
- Debug.Assert(bb.ec == null);
- }
- }
-
-
- protected abstract Expr GenerateRaceCondition(Variable v, string FirstAccessType, string SecondAccessType);
-
-
private HashSet<Expr> GetOffsetsAccessed(StmtList stmts, Variable v, string AccessType)
{
HashSet<Expr> result = new HashSet<Expr> ();
@@ -1266,9 +1111,19 @@ namespace GPUVerify return result;
}
+ public void AddRaceCheckingDeclarations()
+ {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
+ {
+ AddRaceCheckingDecsAndProcsForVar(v);
+ }
+ }
+
+
}
+
class FindReferencesToNamedVariableVisitor : StandardVisitor
{
internal bool found = false;
@@ -1289,4 +1144,6 @@ namespace GPUVerify }
}
+
+
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs deleted file mode 100644 index 2a684c98..00000000 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ /dev/null @@ -1,532 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-using Microsoft.Basetypes;
-
-namespace GPUVerify
-{
- class SetEncodingRaceInstrumenter : RaceInstrumenterBase
- {
-
- protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)
- {
- Variable AccessSet = MakeAccessSetVariable(v, ReadOrWrite);
-
- if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
- {
- verifier.HalfDualisedVariableNames.Add(AccessSet.Name);
- }
-
- verifier.Program.TopLevelDeclarations.Add(AccessSet);
-
- ResetAtBarrier = new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, AccessSet) });
- ModifiedAtLog = ResetAtBarrier;
-
- }
-
- private static Variable MakeAccessSetVariable(Variable v, String ReadOrWrite)
- {
- Microsoft.Boogie.Type SetType = GetAccessSetType(v);
-
- Variable AccessSet = new GlobalVariable(v.tok, new TypedIdent(v.tok, MakeAccessSetName(v, ReadOrWrite), SetType));
- return AccessSet;
- }
-
- private static Microsoft.Boogie.Type GetAccessSetType(Variable v)
- {
- Microsoft.Boogie.Type SetType;
-
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
- SetType = new MapType(mt.tok, new TypeVariableSeq(), mt.Arguments,
- new MapType(mt2.tok, new TypeVariableSeq(), mt2.Arguments,
- new MapType(mt3.tok, new TypeVariableSeq(), mt3.Arguments,
- Microsoft.Boogie.Type.Bool
- )
- )
- );
-
- }
- else
- {
- SetType = new MapType(mt.tok, new TypeVariableSeq(), mt.Arguments,
- new MapType(mt2.tok, new TypeVariableSeq(), mt2.Arguments,
- Microsoft.Boogie.Type.Bool
- )
- );
- }
- }
- else
- {
- SetType = new MapType(mt.tok, new TypeVariableSeq(), mt.Arguments,
- Microsoft.Boogie.Type.Bool
- );
- }
- }
- else
- {
- SetType = Microsoft.Boogie.Type.Bool;
- }
- return SetType;
- }
-
- private static string MakeAccessSetName(Variable v, String ReadOrWrite)
- {
- return "_" + ReadOrWrite + "_SET_" + v.Name;
- }
-
- protected override void AddLogAccessProcedure(Variable v, string ReadOrWrite)
- {
- Variable XParameterVariable;
- Variable YParameterVariable;
- Variable ZParameterVariable;
- Procedure LogReadOrWriteProcedure;
-
- MakeLogAccessProcedureHeader(v, ReadOrWrite, out XParameterVariable, out YParameterVariable, out ZParameterVariable, out LogReadOrWriteProcedure);
-
- LogReadOrWriteProcedure.Modifies.Add(new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)));
-
- List<BigBlock> bigblocks = new List<BigBlock>();
-
- CmdSeq simpleCmds = new CmdSeq();
-
- List<Expr> trueExpr = new List<Expr>(new Expr[] { Expr.True });
-
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
-
- simpleCmds.Add(
- new AssignCmd(v.tok,
- new List<AssignLhs>(new AssignLhs[] {
- new MapAssignLhs(v.tok,
- new MapAssignLhs(v.tok,
- new MapAssignLhs(v.tok,
- new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)))
- , new List<Expr>(new Expr[] { new IdentifierExpr(v.tok, ZParameterVariable) }))
- , new List<Expr>(new Expr[] { new IdentifierExpr(v.tok, YParameterVariable) }))
- , new List<Expr>(new Expr[] { new IdentifierExpr(v.tok, XParameterVariable) }))
- }), trueExpr));
-
- }
- else
- {
- simpleCmds.Add(
- new AssignCmd(v.tok,
- new List<AssignLhs>(new AssignLhs[] {
- new MapAssignLhs(v.tok,
- new MapAssignLhs(v.tok,
- new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)))
- , new List<Expr>(new Expr[] { new IdentifierExpr(v.tok, YParameterVariable) }))
- , new List<Expr>(new Expr[] { new IdentifierExpr(v.tok, XParameterVariable) }))
- }), trueExpr));
- }
- }
- else
- {
- simpleCmds.Add(
- new AssignCmd(v.tok,
- new List<AssignLhs>(new AssignLhs[] {
- new MapAssignLhs(v.tok,
- new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)))
- , new List<Expr>(new Expr[] { new IdentifierExpr(v.tok, XParameterVariable) }))
- }), trueExpr));
- }
- }
- else
- {
- simpleCmds.Add(new AssignCmd(v.tok,
- new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite))) }),
- trueExpr));
- }
-
-
- bigblocks.Add(new BigBlock(v.tok, "_LOG_" + ReadOrWrite + "", simpleCmds, null, null));
-
- StmtList statements = new StmtList(bigblocks, v.tok);
-
- Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), LogReadOrWriteProcedure.InParams, new VariableSeq(), new VariableSeq(), statements);
- LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
-
- LogReadOrWriteImplementation.Proc = LogReadOrWriteProcedure;
-
- verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
- verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
- }
-
- protected override void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)
- {
- IdentifierExpr AccessSet1 = new IdentifierExpr(tok, new VariableDualiser(1, null, null).VisitVariable(
- MakeAccessSetVariable(v, AccessType)));
- IdentifierExprSeq VariablesToHavoc = new IdentifierExprSeq();
- VariablesToHavoc.Add(AccessSet1);
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
- {
- IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2, null, null).VisitVariable(
- MakeAccessSetVariable(v, AccessType)));
- VariablesToHavoc.Add(AccessSet2);
- }
- bb.simpleCmds.Add(new HavocCmd(tok, VariablesToHavoc));
-
- AddAssumeNoAccess(bb, v, AccessType);
-
- }
-
- public override void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly)
- {
- if (!ReadWriteOnly)
- {
- AddRaceCheck(bb, v, "WRITE", "WRITE");
- }
- AddRaceCheck(bb, v, "READ", "WRITE");
- if (!CommandLineOptions.Symmetry)
- {
- AddRaceCheck(bb, v, "WRITE", "READ");
- }
-
-
- }
-
-
-
- private static Microsoft.Boogie.Type GetIndexType(Variable v, int index)
- {
- Debug.Assert(index == 1 || index == 2 || index == 3);
-
- Debug.Assert(v.TypedIdent.Type is MapType);
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- if (index == 1)
- {
- return mt.Arguments[0];
- }
-
- Debug.Assert(mt.Result is MapType);
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- if (index == 2)
- {
- return mt2.Arguments[0];
- }
-
- Debug.Assert(mt2.Result is MapType);
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
-
- Debug.Assert(index == 3);
- return mt3.Arguments[0];
- }
-
- private void AddRaceCheck(BigBlock bb, Variable v, String Access1, String Access2)
- {
- Expr AssertExpr = GenerateRaceCondition(v, Access1, Access2);
-
- bb.simpleCmds.Add(new AssertCmd(v.tok, AssertExpr));
- }
-
- protected override Expr GenerateRaceCondition(Variable v, String Access1, String Access2)
- {
- VariableSeq DummyVars1;
- Expr SetExpr1 = AccessExpr(v, Access1, 1, out DummyVars1);
-
- VariableSeq DummyVars2;
- Expr SetExpr2 = AccessExpr(v, Access2, 2, out DummyVars2);
-
- Debug.Assert(DummyVars1.Length == DummyVars2.Length);
- for (int i = 0; i < DummyVars1.Length; i++)
- {
- Debug.Assert(DummyVars1[i].Name.Equals(DummyVars2[i].Name));
- }
-
- Expr AssertExpr = Expr.And(SetExpr1, SetExpr2);
-
- if (Access1.Equals("WRITE") && Access2.Equals("WRITE") && !verifier.ArrayModelledAdversarially(v))
- {
- VariableSeq DummyVarsAccess1;
- VariableSeq DummyVarsAccess2;
- Expr IndexExpr1 = QuantifiedIndexExpr(v, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable), out DummyVarsAccess1);
- Expr IndexExpr2 = QuantifiedIndexExpr(v, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable), out DummyVarsAccess2);
- Debug.Assert(DummyVarsAccess1.Length == DummyVarsAccess2.Length);
- Debug.Assert(DummyVars1.Length == DummyVarsAccess1.Length);
- for (int i = 0; i < DummyVars1.Length; i++)
- {
- Debug.Assert(DummyVarsAccess1[i].Name.Equals(DummyVarsAccess2[i].Name));
- Debug.Assert(DummyVars1[i].Name.Equals(DummyVarsAccess1[i].Name));
- }
- AssertExpr = Expr.And(AssertExpr, Expr.Neq(IndexExpr1, IndexExpr2));
- }
-
- AssertExpr = Expr.Not(AssertExpr);
- if (DummyVars1.Length > 0)
- {
- AssertExpr = new ForallExpr(v.tok, DummyVars1, AssertExpr);
- }
- return AssertExpr;
- }
-
- private static void SetNameDeep(IdentifierExpr e, string name)
- {
- e.Name = e.Decl.Name = e.Decl.TypedIdent.Name = name;
- }
-
- private static LocalVariable MakeDummy(Variable v, int index)
- {
- return new LocalVariable(v.tok, new TypedIdent(v.tok, "__dummy", GetIndexType(v, index)));
- }
-
- private static void AddAssumeNoAccess(BigBlock bb, Variable v, String AccessType)
- {
- bb.simpleCmds.Add(new AssumeCmd(v.tok, NoAccessExpr(v, AccessType, 1)));
-
- if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
- {
- bb.simpleCmds.Add(new AssumeCmd(v.tok, NoAccessExpr(v, AccessType, 2)));
- }
- }
-
- private static Expr NoAccessExpr(Variable v, String AccessType, int Thread)
- {
- VariableSeq DummyVars;
- Expr result = AccessExpr(v, AccessType, Thread, out DummyVars);
-
- result = Expr.Not(result);
-
- if (DummyVars.Length > 0)
- {
- result = new ForallExpr(v.tok, DummyVars, result);
- }
- return result;
-
- }
-
- private static Expr AccessExpr(Variable v, String AccessType, int Thread, out VariableSeq DummyVars)
- {
- return QuantifiedIndexExpr(v, new VariableDualiser(Thread, null, null).VisitVariable(MakeAccessSetVariable(v, AccessType)), out DummyVars);
- }
-
- private static Expr QuantifiedIndexExpr(Variable v, Variable AccessSetVariable, out VariableSeq DummyVars)
- {
- DummyVars = new VariableSeq();
- Expr result = new IdentifierExpr(v.tok, AccessSetVariable);
-
- if (v.TypedIdent.Type is MapType)
- {
- IdentifierExprSeq DummyIdentifierExprs = new IdentifierExprSeq();
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
-
- DummyVars.Add(MakeDummy(v, 1));
- DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[0]));
- result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[0] });
-
- if (mt.Result is MapType)
- {
- MapType mt2 = mt.Result as MapType;
- Debug.Assert(mt2.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
-
- DummyVars.Add(MakeDummy(v, 2));
- DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[1]));
- result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[1] });
-
- if (mt2.Result is MapType)
- {
- MapType mt3 = mt2.Arguments[0] as MapType;
- Debug.Assert(mt3.Arguments.Length == 1);
- Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
-
- DummyVars.Add(MakeDummy(v, 3));
- DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[2]));
- result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[2] });
-
- SetNameDeep(DummyIdentifierExprs[0], "__z");
- SetNameDeep(DummyIdentifierExprs[1], "__y");
- SetNameDeep(DummyIdentifierExprs[2], "__x");
- }
- else
- {
- SetNameDeep(DummyIdentifierExprs[0], "__y");
- SetNameDeep(DummyIdentifierExprs[1], "__x");
- }
- }
- else
- {
- SetNameDeep(DummyIdentifierExprs[0], "__x");
- }
- }
- return result;
- }
-
- private static Expr NoAccess0DExpr(IToken tok, Variable v, String AccessType, int Thread)
- {
- return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread, null, null).VisitVariable(MakeAccessSetVariable(v, AccessType))));
- }
-
-
- protected override void AddRequiresNoPendingAccess(Variable v)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "WRITE", 1)));
- verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "WRITE", 2)));
- verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "READ", 1)));
- if(!CommandLineOptions.Symmetry)
- {
- verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "READ", 2)));
- }
- }
-
-
- protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
- {
- return NoAccessExpr(v, ReadOrWrite, Int32.Parse(OneOrTwoString));
- }
-
-
-
- protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, 1);
-
- if (ReadOrWrite.Equals("WRITE") || !CommandLineOptions.Symmetry)
- {
- expr = Expr.And(expr, AccessOnlyAtThreadId(v, ReadOrWrite, 2));
- }
-
- verifier.AddCandidateInvariant(wc, expr, "accessed offset is local id");
-
- }
-
- protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
- {
- throw new NotImplementedException();
- }
-
- private Expr AccessOnlyAtThreadId(Variable v, string ReadOrWrite, int Thread)
- {
- VariableSeq Dummies;
- Expr Access = AccessExpr(v, ReadOrWrite, Thread, out Dummies);
-
- if (Dummies.Length == 0)
- {
- return null;
- }
-
- Expr ImplicationLhs;
-
- if (Dummies.Length == 1)
- {
- ImplicationLhs = Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread)));
- }
- else if (Dummies.Length == 2)
- {
- if (!verifier.KernelHasIdY())
- {
- return null;
- }
- ImplicationLhs = Expr.Or(
- Expr.Neq(new IdentifierExpr(v.tok, Dummies[1]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
- Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
- );
- }
- else
- {
- Debug.Assert(Dummies.Length == 3);
- if (!verifier.KernelHasIdZ())
- {
- return null;
- }
- ImplicationLhs = Expr.Or(
- Expr.Or(
- Expr.Neq(new IdentifierExpr(v.tok, Dummies[2]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
- Expr.Neq(new IdentifierExpr(v.tok, Dummies[1]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
- ),
- Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread)))
- );
- }
-
- return new ForallExpr(v.tok, Dummies, Expr.Imp(ImplicationLhs, Expr.Not(Access)));
- }
-
- protected override void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);
-
- if (expr != null)
- {
- verifier.AddCandidateRequires(Proc, expr);
- }
- }
-
- protected override void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);
-
- if (expr != null)
- {
- verifier.AddCandidateEnsures(Proc, expr);
- }
- }
-
- protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
- {
- throw new NotImplementedException();
- }
-
- protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
- {
- throw new NotImplementedException();
- }
-
- protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)
- {
- throw new NotImplementedException();
- }
-
- protected override void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)
- {
- throw new NotImplementedException();
- }
-
- }
-}
|