diff options
| -rw-r--r-- | Source/GPUVerify/AccessCollector.cs | 6 | ||||
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 52 | ||||
| -rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 428 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 1290 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 6 | ||||
| -rw-r--r-- | Source/GPUVerify/IRaceInstrumenter.cs | 29 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 117 | ||||
| -rw-r--r-- | Source/GPUVerify/NoConflictingAccessOptimiser.cs | 116 | ||||
| -rw-r--r-- | Source/GPUVerify/NonLocalAccessCollector.cs | 12 | ||||
| -rw-r--r-- | Source/GPUVerify/NonLocalAccessExtractor.cs | 6 | ||||
| -rw-r--r-- | Source/GPUVerify/NullRaceInstrumenter.cs | 47 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 463 | ||||
| -rw-r--r-- | Source/GPUVerify/ReadCollector.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/SetEncodingRaceInstrumenter.cs | 786 | ||||
| -rw-r--r-- | Source/GPUVerify/WriteCollector.cs | 2 |
15 files changed, 2737 insertions, 627 deletions
diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs index c0e1e217..43491460 100644 --- a/Source/GPUVerify/AccessCollector.cs +++ b/Source/GPUVerify/AccessCollector.cs @@ -8,10 +8,10 @@ namespace GPUVerify {
abstract class AccessCollector : StandardVisitor
{
- protected List<Variable> GlobalVariables;
- protected List<Variable> TileStaticVariables;
+ protected ICollection<Variable> GlobalVariables;
+ protected ICollection<Variable> TileStaticVariables;
- public AccessCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public AccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
{
this.GlobalVariables = GlobalVariables;
this.TileStaticVariables = TileStaticVariables;
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 1d20e48f..9e7ba32c 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -22,6 +22,14 @@ namespace GPUVerify public static bool FullAbstraction;
public static bool Inference;
public static string invariantsFile = null;
+ public static bool DividedArray = false;
+ public static bool DividedAccesses = false;
+ public static bool Eager = false;
+
+ public static bool Symmetry = false;
+ public static bool SetEncoding = false;
+
+ public static bool RaceCheckingContract = false;
public static int Parse(string[] args)
{
@@ -92,6 +100,44 @@ namespace GPUVerify break;
+ case "-dividedArray":
+ case "/dividedArray":
+ DividedArray = true;
+
+ break;
+
+ case "-dividedAccesses":
+ case "/dividedAccesses":
+ DividedAccesses = true;
+
+ break;
+
+ case "-divided":
+ case "/divided":
+ DividedAccesses = true;
+ 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 "-raceCheckingContract":
+ case "/raceCheckingContract":
+ RaceCheckingContract = true;
+ break;
+
case "-inference":
case "/inference":
Inference = true;
@@ -107,6 +153,12 @@ namespace GPUVerify inputFiles.Add(args[i]);
break;
}
+
+ if (OnlyDivergence)
+ {
+ DividedArray = false;
+ DividedAccesses = false;
+ }
}
return 0;
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs new file mode 100644 index 00000000..78ace202 --- /dev/null +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -0,0 +1,428 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify
+{
+ class ElementEncodingRaceInstrumenter : RaceInstrumenterBase
+ {
+
+ public ElementEncodingRaceInstrumenter() : base()
+ {
+ }
+
+
+
+ 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);
+
+ IdentifierExprSeq modifies = LogReadOrWriteProcedure.Modifies;
+ Variable ReadOrWriteHasOccurredVariable = MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
+ Variable ReadOrWriteOffsetXVariable = null;
+ Variable ReadOrWriteOffsetYVariable = null;
+ Variable ReadOrWriteOffsetZVariable = null;
+
+ 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));
+
+ VariableSeq locals = new VariableSeq();
+ Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));
+ locals.Add(TrackVariable);
+
+ List<BigBlock> bigblocks = new List<BigBlock>();
+
+ 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);
+
+ 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)) });
+
+ verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
+ verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
+ }
+
+ protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ {
+ IdentifierExprSeq newVars = new IdentifierExprSeq();
+
+ Variable AccessHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
+
+ if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ {
+ verifier.HalfDualisedVariableNames.Add(AccessHasOccurred.Name);
+ }
+
+ newVars.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
+
+ verifier.Program.TopLevelDeclarations.Add(AccessHasOccurred);
+ 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]));
+
+ Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);
+
+ if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ {
+ verifier.HalfDualisedVariableNames.Add(AccessOffsetX.Name);
+ }
+
+ newVars.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]));
+
+ Variable AccessOffsetY = GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite);
+
+ if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ {
+ verifier.HalfDualisedVariableNames.Add(AccessOffsetY.Name);
+ }
+
+ newVars.Add(new IdentifierExpr(v.tok, AccessOffsetY));
+ verifier.Program.TopLevelDeclarations.Add(AccessOffsetY);
+
+ 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));
+
+ Variable AccessOffsetZ = GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite);
+
+ if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ {
+ verifier.HalfDualisedVariableNames.Add(AccessOffsetZ.Name);
+ }
+
+ newVars.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>();
+ List<Expr> rhss = new List<Expr>();
+ lhss.Add(new SimpleAssignLhs(lhs.tok, new IdentifierExpr(lhs.tok, lhs)));
+ rhss.Add(new NAryExpr(rhs.tok, new IfThenElse(rhs.tok), new ExprSeq(new Expr[] { condition, rhs, new IdentifierExpr(lhs.tok, lhs) })));
+ return new AssignCmd(lhs.tok, lhss, rhss);
+ }
+
+ protected override void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)
+ {
+ IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
+ IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
+
+ 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);
+
+ if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ {
+ lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));
+ rhss.Add(Expr.False);
+ verifier.BarrierProcedure.Modifies.Add(AccessOccurred2);
+ }
+
+ bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
+ }
+
+ public override void CheckForRaces(IToken tok, BigBlock bb, Variable v)
+ {
+ bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "WRITE", "WRITE"))));
+ bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "READ", "WRITE"))));
+ if (!CommandLineOptions.Symmetry)
+ {
+ bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "WRITE", "READ"))));
+ }
+ }
+
+ private static Expr GenerateRaceCondition(IToken tok, Variable v, string FirstAccessType, string SecondAccessType)
+ {
+ Expr RaceCondition = Expr.And(
+ new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, FirstAccessType))),
+ new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, SecondAccessType))));
+
+ if (GPUVerifier.HasXDimension(v))
+ {
+ RaceCondition = Expr.And(RaceCondition, Expr.Eq(
+ new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, FirstAccessType))),
+ new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, SecondAccessType)))
+ ));
+ }
+
+ if (GPUVerifier.HasYDimension(v))
+ {
+ RaceCondition = Expr.And(RaceCondition, Expr.Eq(
+ new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, FirstAccessType))),
+ new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, SecondAccessType)))
+ ));
+ }
+
+ if (GPUVerifier.HasZDimension(v))
+ {
+ RaceCondition = Expr.And(RaceCondition, Expr.Eq(
+ new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, FirstAccessType))),
+ new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, SecondAccessType)))
+ ));
+ }
+
+ return RaceCondition;
+ }
+
+ internal static GlobalVariable MakeReadOrWriteHasOccurredVariable(Variable v, string ReadOrWrite)
+ {
+ return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
+ }
+
+ protected override void AddRequiresNoPendingAccess(Variable v)
+ {
+ IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));
+ IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));
+ IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
+ IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "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))))));
+ }
+ }
+
+
+
+ protected override void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
+
+ private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ Variable ReadOrWriteHasOccurred = ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
+ ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
+ ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;
+ Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));
+ return expr;
+ }
+
+
+ protected override void AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, int Thread)
+ {
+ AddReadOrWrittenXOffsetIsThreadIdCandidateInvariant(wc, v, ReadOrWrite, Thread);
+ AddReadOrWrittenYOffsetIsThreadIdCandidateInvariant(wc, v, ReadOrWrite, Thread);
+ AddReadOrWrittenZOffsetIsThreadIdCandidateInvariant(wc, v, ReadOrWrite, Thread);
+ }
+
+ private void AddReadOrWrittenZOffsetIsThreadIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ verifier.AddCandidateInvariant(wc, expr);
+ }
+ }
+
+ private Expr ReadOrWrittenZOffsetIsThreadIdExpr(Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = null;
+ if (GPUVerifier.HasZDimension(v) && verifier.KernelHasIdZ() && GPUVerifier.IndexTypeOfZDimension(v).Equals(verifier.GetTypeOfIdZ()))
+ {
+ expr = Expr.Imp(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread))));
+ }
+ return expr;
+ }
+
+ private void AddReadOrWrittenYOffsetIsThreadIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ verifier.AddCandidateInvariant(wc, expr);
+ }
+ }
+
+ private Expr ReadOrWrittenYOffsetIsThreadIdExpr(Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = null;
+ if (GPUVerifier.HasYDimension(v) && verifier.KernelHasIdY() && GPUVerifier.IndexTypeOfYDimension(v).Equals(verifier.GetTypeOfIdY()))
+ {
+ expr = Expr.Imp(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread))));
+ }
+ return expr;
+ }
+
+ private void AddReadOrWrittenXOffsetIsThreadIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ verifier.AddCandidateInvariant(wc, expr);
+ }
+ }
+
+ private Expr ReadOrWrittenXOffsetIsThreadIdExpr(Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = null;
+ if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
+ {
+ expr = Expr.Imp(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
+ }
+ return expr;
+ }
+
+ protected override void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ AddReadOrWrittenXOffsetIsThreadIdCandidateRequires(Proc, v, ReadOrWrite, Thread);
+ AddReadOrWrittenYOffsetIsThreadIdCandidateRequires(Proc, v, ReadOrWrite, Thread);
+ AddReadOrWrittenZOffsetIsThreadIdCandidateRequires(Proc, v, ReadOrWrite, Thread);
+ }
+
+ protected override void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ AddReadOrWrittenXOffsetIsThreadIdCandidateEnsures(Proc, v, ReadOrWrite, Thread);
+ AddReadOrWrittenYOffsetIsThreadIdCandidateEnsures(Proc, v, ReadOrWrite, Thread);
+ AddReadOrWrittenZOffsetIsThreadIdCandidateEnsures(Proc, v, ReadOrWrite, Thread);
+ }
+
+ protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
+ }
+
+ protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
+ }
+
+ private void AddReadOrWrittenXOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ Proc.Requires.Add(new Requires(false, expr));
+ }
+ }
+
+ private void AddReadOrWrittenYOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ Proc.Requires.Add(new Requires(false, expr));
+ }
+ }
+
+ private void AddReadOrWrittenZOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ Proc.Requires.Add(new Requires(false, expr));
+ }
+ }
+
+ private void AddReadOrWrittenXOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ Proc.Ensures.Add(new Ensures(false, expr));
+ }
+ }
+
+ private void AddReadOrWrittenYOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ Proc.Ensures.Add(new Ensures(false, expr));
+ }
+ }
+
+ private void AddReadOrWrittenZOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null)
+ {
+ Proc.Ensures.Add(new Ensures(false, expr));
+ }
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index afe437cd..52e227f2 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -12,17 +12,21 @@ namespace GPUVerify {
class GPUVerifier : CheckingContext
{
- private Program Program;
+ public string ouputFilename;
+ public Program Program;
- private Procedure KernelProcedure;
- private Implementation KernelImplementation;
- private Procedure BarrierProcedure;
+ public Procedure KernelProcedure;
+ public Implementation KernelImplementation;
+ public Procedure BarrierProcedure;
- private List<Variable> TileStaticVariables = new List<Variable>();
- private List<Variable> GlobalVariables = new List<Variable>();
+ public ICollection<Variable> TileStaticVariables = new List<Variable>();
+ public ICollection<Variable> GlobalVariables = new List<Variable>();
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;
@@ -62,11 +66,25 @@ namespace GPUVerify private const string _NUM_TILES_Y_name = "_NUM_TILES_Y";
private const string _NUM_TILES_Z_name = "_NUM_TILES_Z";
- public GPUVerifier(Program program)
+ public IRaceInstrumenter RaceInstrumenter;
+
+ public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter) : this(filename, program, raceInstrumenter, false)
+ {
+ }
+
+ public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter, bool skipCheck)
: base((IErrorSink)null)
{
+ this.ouputFilename = filename;
this.Program = program;
- CheckWellFormedness();
+ this.RaceInstrumenter = raceInstrumenter;
+ if(!skipCheck)
+ CheckWellFormedness();
+ }
+
+ public void setRaceInstrumenter(IRaceInstrumenter ri)
+ {
+ this.RaceInstrumenter = ri;
}
private void CheckWellFormedness()
@@ -278,26 +296,37 @@ namespace GPUVerify // TODO!
}
- internal List<Variable> GetTileStaticVariables()
+ internal ICollection<Variable> GetTileStaticVariables()
{
return TileStaticVariables;
}
- internal List<Variable> GetGlobalVariables()
+ internal ICollection<Variable> GetGlobalVariables()
{
return GlobalVariables;
}
- internal void doit()
+ internal void preProcess()
{
+ RemoveElseIfs();
AddStartAndEndBarriers();
PullOutNonLocalAccesses();
+ }
+
+
+
+
- if (!CommandLineOptions.OnlyDivergence)
+ internal void doit()
+ {
+
+ preProcess();
+
+ if (RaceInstrumenter.AddRaceCheckingInstrumentation() == false)
{
- AddRaceCheckingInstrumentation();
+ return;
}
AbstractSharedState();
@@ -306,6 +335,11 @@ namespace GPUVerify MakeKernelDualised();
+ if (CommandLineOptions.Eager)
+ {
+ AddEagerRaceChecking();
+ }
+
GenerateBarrierImplementation();
GenerateKernelPrecondition();
@@ -314,31 +348,122 @@ namespace GPUVerify {
ComputeInvariant();
}
+
- if (CommandLineOptions.outputFile == null)
+ using (TokenTextWriter writer = new TokenTextWriter(ouputFilename + ".bpl"))
{
- CommandLineOptions.outputFile = "temp_ready_to_verify.bpl";
+ Program.Emit(writer);
}
- using (TokenTextWriter writer = new TokenTextWriter(CommandLineOptions.outputFile))
+
+ if (CommandLineOptions.DividedAccesses)
{
- Program.Emit(writer);
+
+ Program p = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { ouputFilename + ".bpl" }), true);
+ p.Resolve();
+ p.Typecheck();
+
+ Contract.Assert(p != null);
+
+ Implementation impl = null;
+
+ {
+ GPUVerifier tempGPUV = new GPUVerifier("not_used", p, new NullRaceInstrumenter(), true);
+ tempGPUV.KernelProcedure = tempGPUV.CheckExactlyOneKernelProcedure();
+ tempGPUV.GetKernelImplementation();
+ impl = tempGPUV.KernelImplementation;
+ }
+
+ Contract.Assert(impl != null);
+
+ NoConflictingAccessOptimiser opt = new NoConflictingAccessOptimiser(impl);
+ Contract.Assert(opt.NumLogCalls() <= 2);
+ if (opt.NumLogCalls() == 2 && !opt.HasConflicting())
+ {
+ FileInfo f = new FileInfo(ouputFilename);
+
+ string newName = f.Directory.FullName + "\\" + "NO_CONFLICTS_" + f.Name + ".bpl";
+ //File.Delete(newName);
+ if (File.Exists(newName))
+ {
+ File.Delete(newName);
+ }
+ File.Move(ouputFilename + ".bpl", newName);
+ //Console.WriteLine("Renamed " + ouputFilename + "; no conflicting accesses (that are not already tested by other output files).");
+ }
+
+
}
+ }
+
+ private void AddEagerRaceChecking()
+ {
+ foreach(Variable v in GlobalVariables)
+ {
+ 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;
+ }
+ }
+ }
+ 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()
{
List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants();
-
+
invariantGenerationCounter = 0;
for (int i = 0; i < Program.TopLevelDeclarations.Count; i++)
{
if (Program.TopLevelDeclarations[i] is Implementation)
{
+
Implementation Impl = Program.TopLevelDeclarations[i] as Implementation;
if (QKeyValue.FindIntAttribute(Impl.Attributes, "inline", -1) == 1)
@@ -363,12 +488,9 @@ namespace GPUVerify LocalNames.Add(basicName);
}
- AddCandidateInvariants(Impl.StructuredStmts, LocalNames, UserSuppliedInvariants);
- }
+ AddCandidateInvariants(Impl.StructuredStmts, LocalNames, UserSuppliedInvariants, Impl);
- if (Program.TopLevelDeclarations[i] is Procedure)
- {
- Procedure Proc = Program.TopLevelDeclarations[i] as Procedure;
+ Procedure Proc = Impl.Proc;
if (QKeyValue.FindIntAttribute(Proc.Attributes, "inline", -1) == 1)
{
@@ -380,51 +502,142 @@ namespace GPUVerify continue;
}
- HashSet<string> InParamNames = new HashSet<string>();
- foreach (Variable v in Proc.InParams)
+ AddCandidateRequires(Proc);
+ if (CommandLineOptions.RaceCheckingContract)
{
- string basicName = StripThreadIdentifier(v.Name);
- InParamNames.Add(basicName);
+ RaceInstrumenter.AddRaceCheckingCandidateRequires(Proc);
}
- AddCandidateRequires(Proc, InParamNames); // TODO - add support for user-supplied invariants
- HashSet<string> OutParamNames = new HashSet<string>();
- foreach (Variable v in Proc.OutParams)
+ AddUserSuppliedCandidateRequires(Proc, UserSuppliedInvariants);
+
+ AddCandidateEnsures(Proc);
+ if (CommandLineOptions.RaceCheckingContract)
{
- string basicName = StripThreadIdentifier(v.Name);
- OutParamNames.Add(basicName);
+ RaceInstrumenter.AddRaceCheckingCandidateEnsures(Proc);
}
- AddCandidateEnsures(Proc, OutParamNames); // TODO - add support for user-supplied invariants
+ AddUserSuppliedCandidateEnsures(Proc, UserSuppliedInvariants);
+
}
+
}
}
- private void AddCandidateEnsures(Procedure Proc, HashSet<string> LocalNames)
+ private void AddCandidateEnsures(Procedure Proc)
{
- foreach (string lv in LocalNames)
+ HashSet<string> names = new HashSet<String>();
+ foreach (Variable v in Proc.OutParams)
{
- AddCandidateEnsures(Proc, Expr.Eq(
- // Int type used here, but it doesn't matter as we will print and then re-parse the program
- new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, lv + "$1", Microsoft.Boogie.Type.Int))),
- new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, lv + "$2", Microsoft.Boogie.Type.Int)))
- ));
+ names.Add(StripThreadIdentifier(v.Name));
}
+
+ foreach (string name in names)
+ {
+ AddEqualityCandidateEnsures(Proc, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, name, Microsoft.Boogie.Type.Int)));
+ }
+
}
- private void AddCandidateRequires(Procedure Proc, HashSet<string> LocalNames)
+ private void AddCandidateRequires(Procedure Proc)
{
- foreach (string lv in LocalNames)
+ HashSet<string> names = new HashSet<String>();
+ foreach (Variable v in Proc.InParams)
{
- AddCandidateRequires(Proc, Expr.Eq(
- // Int type used here, but it doesn't matter as we will print and then re-parse the program
- new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, lv + "$1", Microsoft.Boogie.Type.Int))),
- new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, lv + "$2", Microsoft.Boogie.Type.Int)))
+ names.Add(StripThreadIdentifier(v.Name));
+ }
+
+ bool hasPredicateParameter = false;
+
+ foreach (string name in names)
+ {
+
+ if (IsPredicateOrTemp(name))
+ {
+ Debug.Assert(name.Equals("_P"));
+ hasPredicateParameter = true;
+ AddCandidateRequires(Proc, Expr.Eq(
+ new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, name + "$1", Microsoft.Boogie.Type.Bool))),
+ new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, name + "$2", Microsoft.Boogie.Type.Bool)))
+ ));
+ }
+ else
+ {
+ AddPredicatedEqualityCandidateRequires(Proc, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, name, Microsoft.Boogie.Type.Int)));
+ AddEqualityCandidateRequires(Proc, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, name, Microsoft.Boogie.Type.Int)));
+ }
+ }
+
+ Debug.Assert(hasPredicateParameter);
+
+ }
+
+ private void AddPredicatedEqualityCandidateRequires(Procedure Proc, Variable v)
+ {
+ AddCandidateRequires(Proc, Expr.Imp(
+ Expr.And(
+ new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, "_P$1", Microsoft.Boogie.Type.Bool))),
+ new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))
+ ),
+ Expr.Eq(
+ new IdentifierExpr(Proc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Proc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ )
+ ));
+ }
+
+ private void AddEqualityCandidateRequires(Procedure Proc, Variable v)
+ {
+ AddCandidateRequires(Proc,
+ Expr.Eq(
+ new IdentifierExpr(Proc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Proc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ )
+ );
+ }
+
+ private void AddEqualityCandidateEnsures(Procedure Proc, Variable v)
+ {
+ AddCandidateEnsures(Proc,
+ Expr.Eq(
+ new IdentifierExpr(Proc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Proc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
));
+ }
+
+
+ private void AddUserSuppliedCandidateRequires(Procedure Proc, List<Expr> UserSuppliedInvariants)
+ {
+ foreach (Expr e in UserSuppliedInvariants)
+ {
+ Requires r = new Requires(false, e);
+ Proc.Requires.Add(r);
+ bool OK = ProgramIsOK(Proc);
+ Proc.Requires.Remove(r);
+ if (OK)
+ {
+ AddCandidateRequires(Proc, e);
+ }
+ }
+ }
+
+ private void AddUserSuppliedCandidateEnsures(Procedure Proc, List<Expr> UserSuppliedInvariants)
+ {
+ foreach (Expr e in UserSuppliedInvariants)
+ {
+ Ensures ens = new Ensures(false, e);
+ Proc.Ensures.Add(ens);
+ bool OK = ProgramIsOK(Proc);
+ Proc.Ensures.Remove(ens);
+ if (OK)
+ {
+ AddCandidateEnsures(Proc, e);
+ }
}
}
+
+
private void AddCandidateRequires(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
@@ -478,37 +691,66 @@ namespace GPUVerify return result;
}
- private void AddCandidateInvariants(StmtList stmtList, HashSet<string> LocalNames, List<Expr> UserSuppliedInvariants)
+ private void AddCandidateInvariants(StmtList stmtList, HashSet<string> LocalNames, List<Expr> UserSuppliedInvariants, Implementation Impl)
{
foreach (BigBlock bb in stmtList.BigBlocks)
{
- AddCandidateInvariants(bb, LocalNames, UserSuppliedInvariants);
+ AddCandidateInvariants(bb, LocalNames, UserSuppliedInvariants, Impl);
}
}
- private void AddCandidateInvariants(BigBlock bb, HashSet<string> LocalNames, List<Expr> UserSuppliedInvariants)
+ private void AddCandidateInvariants(BigBlock bb, HashSet<string> LocalNames, List<Expr> UserSuppliedInvariants, Implementation Impl)
{
if (bb.ec is WhileCmd)
{
WhileCmd wc = bb.ec as WhileCmd;
- foreach(string lv in LocalNames)
+ Debug.Assert(wc.Guard is NAryExpr);
+ Debug.Assert((wc.Guard as NAryExpr).Args.Length == 2);
+ Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);
+ string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;
+
+ LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));
+
+ AddCandidateInvariant(wc, Expr.Eq(
+ // Int type used here, but it doesn't matter as we will print and then re-parse the program
+ new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),
+ new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))
+ ));
+
+ foreach (string lv in LocalNames)
{
- AddCandidateInvariant(wc, Expr.Eq(
- // Int type used here, but it doesn't matter as we will print and then re-parse the program
- new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv + "$1", Microsoft.Boogie.Type.Int))),
- new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv + "$2", Microsoft.Boogie.Type.Int)))
- ));
+ if (IsPredicateOrTemp(lv))
+ {
+ continue;
+ }
+
+ AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
+
+ if (Impl != KernelImplementation)
+ {
+ AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
+ }
}
- if (!CommandLineOptions.OnlyDivergence)
+ if (!CommandLineOptions.FullAbstraction)
{
- AddRaceCheckingCandidateInvariants(wc);
+ foreach (Variable v in GlobalVariables)
+ {
+ AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ }
+
+ foreach (Variable v in TileStaticVariables)
+ {
+ AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ }
}
- AddUserSuppliedInvariants(wc, UserSuppliedInvariants);
+ RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);
- AddCandidateInvariants(wc.Body, LocalNames, UserSuppliedInvariants);
+ AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);
+
+ AddCandidateInvariants(wc.Body, LocalNames, UserSuppliedInvariants, Impl);
}
else if (bb.ec is IfCmd)
{
@@ -521,45 +763,82 @@ namespace GPUVerify }
}
- private void AddRaceCheckingCandidateInvariants(WhileCmd wc)
+ private void AddEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
{
- foreach (Variable v in GlobalVariables)
- {
- AddNoReadOrWriteCandidateInvariants(wc, v);
- AddReadOrWrittenOffsetIsThreadId(wc, v, "READ");
- AddReadOrWrittenOffsetIsThreadId(wc, v, "WRITE");
- }
+ AddCandidateInvariant(wc,
+ Expr.Eq(
+ new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ ));
+ }
- foreach (Variable v in TileStaticVariables)
- {
- AddNoReadOrWriteCandidateInvariants(wc, v);
- AddReadOrWrittenOffsetIsThreadId(wc, v, "READ");
- AddReadOrWrittenOffsetIsThreadId(wc, v, "WRITE");
- }
+ private void AddPredicatedEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
+ {
+ AddCandidateInvariant(wc, Expr.Imp(
+ Expr.And(
+ new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),
+ new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))
+ ),
+ Expr.Eq(
+ new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ )));
}
- private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants)
+
+ private bool IsPredicateOrTemp(string lv)
+ {
+ return (lv.Length >= 2 && lv.Substring(0,2).Equals("_P")) ||
+ (lv.Length > 3 && lv.Substring(0,3).Equals("_LC")) ||
+ (lv.Length > 5 && lv.Substring(0,5).Equals("_temp"));
+ }
+
+
+
+ private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants, Implementation Impl)
{
foreach (Expr e in UserSuppliedInvariants)
{
wc.Invariants.Add(new AssertCmd(wc.tok, e));
- TokenTextWriter writer = new TokenTextWriter("temp_out.bpl");
- Program.Emit(writer);
- writer.Close();
+ bool OK = ProgramIsOK(Impl);
wc.Invariants.RemoveAt(wc.Invariants.Count - 1);
-
- Program temp_program = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { "temp_out.bpl" }), false);
-
- if(IsOK(temp_program))
+ if (OK)
{
AddCandidateInvariant(wc, e);
}
}
}
- private bool IsOK(Microsoft.Boogie.Program temp_program)
+ private bool ProgramIsOK(Declaration d)
{
- if(temp_program == null)
+ Debug.Assert(d is Procedure || d is Implementation);
+ TokenTextWriter writer = new TokenTextWriter("temp_out.bpl");
+ List<Declaration> RealDecls = Program.TopLevelDeclarations;
+ List<Declaration> TempDecls = new List<Declaration>();
+ foreach (Declaration d2 in RealDecls)
+ {
+ if (d is Procedure)
+ {
+ if ((d == d2) || !(d2 is Implementation || d2 is Procedure))
+ {
+ TempDecls.Add(d2);
+ }
+ }
+ else if (d is Implementation)
+ {
+ if ((d == d2) || !(d2 is Implementation))
+ {
+ TempDecls.Add(d2);
+ }
+ }
+ }
+ Program.TopLevelDeclarations = TempDecls;
+ Program.Emit(writer);
+ writer.Close();
+ Program.TopLevelDeclarations = RealDecls;
+ Program temp_program = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { "temp_out.bpl" }), false);
+
+ if (temp_program == null)
{
return false;
}
@@ -576,71 +855,27 @@ namespace GPUVerify return true;
}
- private void AddReadOrWrittenOffsetIsThreadId(WhileCmd wc, Variable v, string ReadOrWrite)
- {
- if (HasXDimension(v) && IndexTypeOfXDimension(v).Equals(GetTypeOfIdX()))
- {
- AddCandidateInvariant(wc,
- Expr.Imp(
- new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "X", 1))))
- );
- AddCandidateInvariant(wc,
- Expr.Imp(
- new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "X", 2))))
- );
- }
-
- if (HasYDimension(v) && KernelHasIdY() && IndexTypeOfYDimension(v).Equals(GetTypeOfIdY()))
- {
- AddCandidateInvariant(wc,
- Expr.Imp(
- new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Y", 1))))
- );
- AddCandidateInvariant(wc,
- Expr.Imp(
- new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Y", 2))))
- );
- }
-
- if (HasZDimension(v) && KernelHasIdZ() && IndexTypeOfZDimension(v).Equals(GetTypeOfIdZ()))
- {
- AddCandidateInvariant(wc,
- Expr.Imp(
- new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Z", 1))))
- );
- AddCandidateInvariant(wc,
- Expr.Imp(
- new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Z", 2))))
- );
- }
-
- }
+
- private Microsoft.Boogie.Type GetTypeOfIdX()
+ public Microsoft.Boogie.Type GetTypeOfIdX()
{
Contract.Requires(_X != null);
return _X.TypedIdent.Type;
}
- private Microsoft.Boogie.Type GetTypeOfIdY()
+ public Microsoft.Boogie.Type GetTypeOfIdY()
{
Contract.Requires(_Y != null);
return _Y.TypedIdent.Type;
}
- private Microsoft.Boogie.Type GetTypeOfIdZ()
+ public Microsoft.Boogie.Type GetTypeOfIdZ()
{
Contract.Requires(_Z != null);
return _Z.TypedIdent.Type;
}
- private Microsoft.Boogie.Type GetTypeOfId(string dimension)
+ public Microsoft.Boogie.Type GetTypeOfId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
if (dimension.Equals("X")) return GetTypeOfIdX();
@@ -650,67 +885,67 @@ namespace GPUVerify return null;
}
- private bool KernelHasIdX()
+ public bool KernelHasIdX()
{
return _X != null;
}
- private bool KernelHasIdY()
+ public bool KernelHasIdY()
{
return _Y != null;
}
- private bool KernelHasIdZ()
+ public bool KernelHasIdZ()
{
return _Z != null;
}
- private bool KernelHasTileIdX()
+ public bool KernelHasTileIdX()
{
return _TILE_X != null;
}
- private bool KernelHasTileIdY()
+ public bool KernelHasTileIdY()
{
return _TILE_Y != null;
}
- private bool KernelHasTileIdZ()
+ public bool KernelHasTileIdZ()
{
return _TILE_Z != null;
}
- private bool KernelHasNumTilesX()
+ public bool KernelHasNumTilesX()
{
return _NUM_TILES_X != null;
}
- private bool KernelHasNumTilesY()
+ public bool KernelHasNumTilesY()
{
return _NUM_TILES_Y != null;
}
- private bool KernelHasNumTilesZ()
+ public bool KernelHasNumTilesZ()
{
return _NUM_TILES_Z != null;
}
- private bool KernelHasTileSizeX()
+ public bool KernelHasTileSizeX()
{
return _TILE_SIZE_X != null;
}
- private bool KernelHasTileSizeY()
+ public bool KernelHasTileSizeY()
{
return _TILE_SIZE_Y != null;
}
- private bool KernelHasTileSizeZ()
+ public bool KernelHasTileSizeZ()
{
return _TILE_SIZE_Z != null;
}
- private bool KernelHasId(string dimension)
+ public bool KernelHasId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
if (dimension.Equals("X")) return KernelHasIdX();
@@ -720,23 +955,9 @@ namespace GPUVerify return false;
}
- private void AddNoReadOrWriteCandidateInvariants(WhileCmd wc, Variable v)
- {
- AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "1");
- AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "1");
- AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "2");
- AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "2");
- }
+
- private void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Variable ReadHasOccurred1 = MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
- ReadHasOccurred1.Name = ReadHasOccurred1.Name + "$" + OneOrTwo;
- ReadHasOccurred1.TypedIdent.Name = ReadHasOccurred1.TypedIdent.Name + "$" + OneOrTwo;
- AddCandidateInvariant(wc, Expr.Not(new IdentifierExpr(wc.tok, ReadHasOccurred1)));
- }
-
- private void AddCandidateInvariant(WhileCmd wc, Expr e)
+ public void AddCandidateInvariant(WhileCmd wc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(wc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(wc.tok, ExistentialBooleanConstant);
@@ -764,7 +985,7 @@ namespace GPUVerify CmdSeq newCommands = new CmdSeq();
newCommands.Add(FirstBarrier);
- foreach(Cmd c in KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds)
+ foreach (Cmd c in KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds)
{
newCommands.Add(c);
}
@@ -779,18 +1000,7 @@ namespace GPUVerify private void GenerateKernelPrecondition()
{
-
- if (!CommandLineOptions.OnlyDivergence)
- {
- foreach (Variable v in GlobalVariables)
- {
- AddRequiresNoPendingAccess(v);
- }
- foreach (Variable v in TileStaticVariables)
- {
- AddRequiresNoPendingAccess(v);
- }
- }
+ RaceInstrumenter.AddKernelPrecondition();
Expr AssumeDistinctThreads = null;
Expr AssumeThreadIdsInRange = null;
@@ -806,9 +1016,6 @@ namespace GPUVerify KernelProcedure.Requires.Add(new Requires(false, AssumeDistinctThreads));
KernelProcedure.Requires.Add(new Requires(false, AssumeThreadIdsInRange));
-
- //Program.TopLevelDeclarations.Add(new Axiom(tok, AssumeDistinctThreads));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, AssumeThreadIdsInRange));
}
else
{
@@ -828,11 +1035,6 @@ namespace GPUVerify KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));
KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));
KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
-
- //Program.TopLevelDeclarations.Add(new Axiom(tok, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
}
else
{
@@ -840,12 +1042,6 @@ namespace GPUVerify KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));
KernelProcedure.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));
KernelProcedure.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
-
- //Program.TopLevelDeclarations.Add(new Axiom(tok, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));
- //Program.TopLevelDeclarations.Add(new Axiom(tok, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
-
}
Expr AssumeThreadsDistinctInDimension =
Expr.Neq(
@@ -892,9 +1088,9 @@ namespace GPUVerify private Constant GetTileSize(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if(dimension.Equals("X")) return _TILE_SIZE_X;
- if(dimension.Equals("Y")) return _TILE_SIZE_Y;
- if(dimension.Equals("Z")) return _TILE_SIZE_Z;
+ if (dimension.Equals("X")) return _TILE_SIZE_X;
+ if (dimension.Equals("Y")) return _TILE_SIZE_Y;
+ if (dimension.Equals("Z")) return _TILE_SIZE_Z;
Debug.Assert(false);
return null;
}
@@ -909,7 +1105,7 @@ namespace GPUVerify return null;
}
- private Constant MakeThreadId(IToken tok, string dimension, int number)
+ public Constant MakeThreadId(IToken tok, string dimension, int number)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
string name = null;
@@ -941,14 +1137,7 @@ namespace GPUVerify return new LiteralExpr(tok, BigNum.FromInt(0), 32);
}
- private void AddRequiresNoPendingAccess(Variable v)
- {
- IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "READ")));
- IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "READ")));
- IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
- IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
- KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.And(Expr.Not(ReadAccessOccurred2), Expr.And(Expr.Not(WriteAccessOccurred1), Expr.Not(WriteAccessOccurred2))))));
- }
+
private void GenerateBarrierImplementation()
{
@@ -971,29 +1160,7 @@ namespace GPUVerify checkNonDivergence.ec = new IfCmd(tok, Expr.And(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);
}
- if (!CommandLineOptions.OnlyDivergence)
- {
- BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
- bigblocks.Add(checkForRaces);
- foreach (Variable v in GlobalVariables)
- {
- CheckForRaces(tok, checkForRaces, v);
- }
- foreach (Variable v in TileStaticVariables)
- {
- CheckForRaces(tok, checkForRaces, v);
- }
-
- foreach (Variable v in GlobalVariables)
- {
- SetNoAccessOccurred(tok, checkForRaces, v);
- }
- foreach (Variable v in TileStaticVariables)
- {
- SetNoAccessOccurred(tok, checkForRaces, v);
- }
-
- }
+ bigblocks.Add(RaceInstrumenter.MakeRaceCheckingStatements(tok));
if (!CommandLineOptions.FullAbstraction)
{
@@ -1019,69 +1186,8 @@ namespace GPUVerify Program.TopLevelDeclarations.Add(BarrierImplementation);
}
- private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v)
- {
- SetNoAccessOccurred(tok, bb, v, "READ");
- SetNoAccessOccurred(tok, bb, v, "WRITE");
- }
-
- private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)
- {
- IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
- IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
-
- BarrierProcedure.Modifies.Add(AccessOccurred1);
- BarrierProcedure.Modifies.Add(AccessOccurred2);
-
- List<AssignLhs> lhss = new List<AssignLhs>();
- lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));
- lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));
- List<Expr> rhss = new List<Expr>();
- rhss.Add(Expr.False);
- rhss.Add(Expr.False);
- bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
- }
-
- private void CheckForRaces(IToken tok, BigBlock bb, Variable v)
- {
- bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "WRITE", "WRITE"))));
- bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "READ", "WRITE"))));
- }
-
- private static Expr GenerateRaceCondition(IToken tok, Variable v, string FirstAccessType, string SecondAccessType)
- {
- Expr RaceCondition = Expr.And(
- new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, FirstAccessType))),
- new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, SecondAccessType))));
-
- if (HasXDimension(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeOffsetXVariable(v, FirstAccessType))),
- new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeOffsetXVariable(v, SecondAccessType)))
- ));
- }
-
- if (HasYDimension(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeOffsetYVariable(v, FirstAccessType))),
- new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeOffsetYVariable(v, SecondAccessType)))
- ));
- }
-
- if (HasZDimension(v))
- {
- RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeOffsetZVariable(v, FirstAccessType))),
- new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeOffsetZVariable(v, SecondAccessType)))
- ));
- }
-
- return RaceCondition;
- }
- private static bool HasZDimension(Variable v)
+ public static bool HasZDimension(Variable v)
{
if (v.TypedIdent.Type is MapType)
{
@@ -1100,12 +1206,12 @@ namespace GPUVerify return false;
}
- private static bool HasYDimension(Variable v)
+ public static bool HasYDimension(Variable v)
{
return v.TypedIdent.Type is MapType && (v.TypedIdent.Type as MapType).Result is MapType;
}
- private static bool HasXDimension(Variable v)
+ public static bool HasXDimension(Variable v)
{
return v.TypedIdent.Type is MapType;
}
@@ -1120,13 +1226,74 @@ namespace GPUVerify BarrierProcedure.Modifies.Add(v1);
BarrierProcedure.Modifies.Add(v2);
- if (!KernelProcedure.Modifies.Has(v1))
+ foreach (Declaration d in Program.TopLevelDeclarations)
{
- Debug.Assert(!KernelProcedure.Modifies.Has(v2));
- KernelProcedure.Modifies.Add(v1);
- KernelProcedure.Modifies.Add(v2);
+ 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);
+ }
+ }
+ }
}
+
+ }
+
+ private bool ModifiesSetContains(IdentifierExprSeq seq, IdentifierExpr v)
+ {
+ foreach (IdentifierExpr ie in seq)
+ {
+ if (ie.Name.Equals(v.Name))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private bool CallsBarrier(Implementation impl)
+ {
+ return CallsBarrier(impl.StructuredStmts);
+ }
+
+ private bool CallsBarrier(StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ if (CallsBarrier(bb))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private bool CallsBarrier(BigBlock bb)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is CallCmd && (c as CallCmd).callee.Equals(BarrierProcedure.Name))
+ {
+ return true;
+ }
+ }
+ if (bb.ec is WhileCmd)
+ {
+ return CallsBarrier((bb.ec as WhileCmd).Body);
+ }
+ else
+ {
+ Debug.Assert(bb.ec == null);
+ return false;
+ }
}
private void AbstractSharedState()
@@ -1140,7 +1307,7 @@ namespace GPUVerify foreach (Declaration d in Program.TopLevelDeclarations)
{
- if (d is Variable && GlobalVariables.Contains(d as Variable))
+ if (d is Variable && GlobalVariables.Contains(d as Variable) || TileStaticVariables.Contains(d as Variable))
{
continue;
}
@@ -1169,7 +1336,7 @@ namespace GPUVerify foreach (IdentifierExpr e in proc.Modifies)
{
- if (!(GlobalVariables.Contains(e.Decl)))
+ if (!(GlobalVariables.Contains(e.Decl) || TileStaticVariables.Contains(e.Decl)))
{
NewModifies.Add(e);
}
@@ -1201,7 +1368,7 @@ namespace GPUVerify private StmtList PerformFullSharedStateAbstraction(StmtList stmtList)
{
Contract.Requires(stmtList != null);
-
+
StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
foreach (BigBlock bodyBlock in stmtList.BigBlocks)
@@ -1268,259 +1435,23 @@ namespace GPUVerify - private void AddRaceCheckingInstrumentation()
- {
- foreach(Variable v in GlobalVariables)
- {
- AddRaceCheckingInstrumentation(v);
- }
- foreach (Variable v in TileStaticVariables)
- {
- AddRaceCheckingInstrumentation(v);
- }
-
- AddRaceCheckCalls(KernelImplementation);
-
- }
-
- private void AddRaceCheckingInstrumentation(Variable v)
- {
- IdentifierExprSeq vars = AddRaceCheckingDeclarations(v);
- foreach (IdentifierExpr e in vars)
- {
- KernelProcedure.Modifies.Add(e);
- }
- AddRaceCheckingProcedures(v);
- }
-
- private void AddRaceCheckCalls(Implementation impl)
- {
- impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
- }
-
- private StmtList AddRaceCheckCalls(StmtList stmtList)
- {
- Contract.Requires(stmtList != null);
-
- StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
-
- foreach (BigBlock bodyBlock in stmtList.BigBlocks)
- {
- result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));
- }
- return result;
- }
-
- private BigBlock AddRaceCheckCalls(BigBlock bb)
- {
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
- foreach (Cmd c in bb.simpleCmds)
- {
- if (c is AssignCmd)
- {
- AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1);
- Debug.Assert(assign.Rhss.Count == 1);
- AssignLhs lhs = assign.Lhss[0];
- Expr rhs = assign.Rhss[0];
-
- ReadCollector rc = new ReadCollector(GlobalVariables, TileStaticVariables);
- rc.Visit(rhs);
- if (rc.accesses.Count > 0)
- {
- Debug.Assert(rc.accesses.Count == 1);
- AccessRecord ar = rc.accesses.ToList()[0];
- ExprSeq inParams = new ExprSeq();
- if (ar.IndexZ != null)
- {
- inParams.Add(ar.IndexZ);
- }
- if (ar.IndexY != null)
- {
- inParams.Add(ar.IndexY);
- }
- if (ar.IndexX != null)
- {
- inParams.Add(ar.IndexX);
- }
-
- result.simpleCmds.Add(new CallCmd(c.tok, "_LOG_READ_" + ar.v.Name, inParams, new IdentifierExprSeq()));
- }
-
- WriteCollector wc = new WriteCollector(GlobalVariables, TileStaticVariables);
- wc.Visit(lhs);
- if (wc.GetAccess() != null)
- {
- AccessRecord ar = wc.GetAccess();
- ExprSeq inParams = new ExprSeq();
- if (ar.IndexZ != null)
- {
- inParams.Add(ar.IndexZ);
- }
- if (ar.IndexY != null)
- {
- inParams.Add(ar.IndexY);
- }
- if (ar.IndexX != null)
- {
- inParams.Add(ar.IndexX);
- }
-
- result.simpleCmds.Add(new CallCmd(c.tok, "_LOG_WRITE_" + ar.v.Name, inParams, new IdentifierExprSeq()));
- }
-
-
-
- }
- result.simpleCmds.Add(c);
- }
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd WhileCommand = bb.ec as WhileCmd;
- result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, AddRaceCheckCalls(WhileCommand.Body));
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd IfCommand = bb.ec as IfCmd;
- Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
- result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, AddRaceCheckCalls(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? AddRaceCheckCalls(IfCommand.elseBlock) : null);
- }
- else
- {
- Debug.Assert(bb.ec == null);
- }
-
- return result;
-
- }
-
- private void AddRaceCheckingProcedures(Variable v)
- {
- AddLogAccessProcedure(v, "READ");
- AddLogAccessProcedure(v, "WRITE");
- }
-
- private void AddLogAccessProcedure(Variable v, string ReadOrWrite)
- {
- VariableSeq inParams = new VariableSeq();
- IdentifierExprSeq modifies = new IdentifierExprSeq();
- Variable ReadOrWriteHasOccurredVariable = MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
- Variable ReadOrWriteOffsetXVariable = null;
- Variable ReadOrWriteOffsetYVariable = null;
- Variable ReadOrWriteOffsetZVariable = null;
- Variable XParameterVariable = null;
- Variable YParameterVariable = null;
- Variable ZParameterVariable = null;
-
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteHasOccurredVariable));
-
- if (v.TypedIdent.Type is MapType)
- {
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Debug.Assert(IsIntOrBv32(mt.Arguments[0]));
-
- ReadOrWriteOffsetXVariable = MakeOffsetXVariable(v, ReadOrWrite);
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetXVariable));
- 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(IsIntOrBv32(mt2.Arguments[0]));
- ReadOrWriteOffsetYVariable = MakeOffsetYVariable(v, ReadOrWrite);
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetYVariable));
- 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(IsIntOrBv32(mt3.Arguments[0]));
- Debug.Assert(!(mt3.Result is MapType));
- ReadOrWriteOffsetZVariable = MakeOffsetZVariable(v, ReadOrWrite);
- modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetZVariable));
- ZParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Z_index", mt3.Arguments[0]));
- }
- }
- }
-
- if (ZParameterVariable != null)
- {
- inParams.Add(ZParameterVariable);
- }
-
- if (YParameterVariable != null)
- {
- inParams.Add(YParameterVariable);
- }
-
- if (XParameterVariable != null)
- {
- inParams.Add(XParameterVariable);
- }
-
- Procedure LogReadOrWriteProcedure = new Procedure(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), inParams, new VariableSeq(), new RequiresSeq(), modifies, new EnsuresSeq());
- LogReadOrWriteProcedure.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
-
-
- VariableSeq locals = new VariableSeq();
- Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));
- locals.Add(TrackVariable);
-
- List<BigBlock> bigblocks = new List<BigBlock>();
-
- 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);
-
- Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), inParams, new VariableSeq(), locals, statements);
- LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
-
- Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
- Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
- }
-
- private static GlobalVariable MakeOffsetZVariable(Variable v, string ReadOrWrite)
+ internal static GlobalVariable MakeOffsetZVariable(Variable v, string ReadOrWrite)
{
return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_Z_" + v.Name, IndexTypeOfZDimension(v)));
}
- private static GlobalVariable MakeOffsetYVariable(Variable v, string ReadOrWrite)
+ internal static GlobalVariable MakeOffsetYVariable(Variable v, string ReadOrWrite)
{
return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_Y_" + v.Name, IndexTypeOfYDimension(v)));
}
- private static GlobalVariable MakeOffsetXVariable(Variable v, string ReadOrWrite)
+ internal static GlobalVariable MakeOffsetXVariable(Variable v, string ReadOrWrite)
{
return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_X_" + v.Name, IndexTypeOfXDimension(v)));
}
- private static GlobalVariable MakeReadOrWriteHasOccurredVariable(Variable v, string ReadOrWrite)
- {
- return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
- }
-
- private static Microsoft.Boogie.Type IndexTypeOfZDimension(Variable v)
+ public static Microsoft.Boogie.Type IndexTypeOfZDimension(Variable v)
{
Contract.Requires(HasZDimension(v));
MapType mt = v.TypedIdent.Type as MapType;
@@ -1529,7 +1460,7 @@ namespace GPUVerify return mt3.Arguments[0];
}
- private static Microsoft.Boogie.Type IndexTypeOfYDimension(Variable v)
+ public static Microsoft.Boogie.Type IndexTypeOfYDimension(Variable v)
{
Contract.Requires(HasYDimension(v));
MapType mt = v.TypedIdent.Type as MapType;
@@ -1537,31 +1468,22 @@ namespace GPUVerify return mt2.Arguments[0];
}
- private static Microsoft.Boogie.Type IndexTypeOfXDimension(Variable v)
+ public static Microsoft.Boogie.Type IndexTypeOfXDimension(Variable v)
{
Contract.Requires(HasXDimension(v));
MapType mt = v.TypedIdent.Type as MapType;
return mt.Arguments[0];
}
- private AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)
+ private void AddRaceCheckingDeclarations(Variable v)
{
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- lhss.Add(new SimpleAssignLhs(lhs.tok, new IdentifierExpr(lhs.tok, lhs)));
- rhss.Add(new NAryExpr(rhs.tok, new IfThenElse(rhs.tok), new ExprSeq(new Expr[] { condition, rhs, new IdentifierExpr(lhs.tok, lhs) })));
- return new AssignCmd(lhs.tok, lhss, rhss);
- }
-
- private IdentifierExprSeq AddRaceCheckingDeclarations(Variable v)
- {
- IdentifierExprSeq result = new IdentifierExprSeq();
+ IdentifierExprSeq newVars = new IdentifierExprSeq();
Variable ReadHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_READ_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
Variable WriteHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_WRITE_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
- result.Add(new IdentifierExpr(v.tok, ReadHasOccurred));
- result.Add(new IdentifierExpr(v.tok, WriteHasOccurred));
+ newVars.Add(new IdentifierExpr(v.tok, ReadHasOccurred));
+ newVars.Add(new IdentifierExpr(v.tok, WriteHasOccurred));
Program.TopLevelDeclarations.Add(ReadHasOccurred);
Program.TopLevelDeclarations.Add(WriteHasOccurred);
@@ -1573,8 +1495,8 @@ namespace GPUVerify Variable ReadOffsetX = MakeOffsetXVariable(v, "READ");
Variable WriteOffsetX = MakeOffsetXVariable(v, "WRITE");
- result.Add(new IdentifierExpr(v.tok, ReadOffsetX));
- result.Add(new IdentifierExpr(v.tok, WriteOffsetX));
+ newVars.Add(new IdentifierExpr(v.tok, ReadOffsetX));
+ newVars.Add(new IdentifierExpr(v.tok, WriteOffsetX));
Program.TopLevelDeclarations.Add(ReadOffsetX);
Program.TopLevelDeclarations.Add(WriteOffsetX);
@@ -1586,8 +1508,8 @@ namespace GPUVerify Variable ReadOffsetY = MakeOffsetYVariable(v, "READ");
Variable WriteOffsetY = MakeOffsetYVariable(v, "WRITE");
- result.Add(new IdentifierExpr(v.tok, ReadOffsetY));
- result.Add(new IdentifierExpr(v.tok, WriteOffsetY));
+ newVars.Add(new IdentifierExpr(v.tok, ReadOffsetY));
+ newVars.Add(new IdentifierExpr(v.tok, WriteOffsetY));
Program.TopLevelDeclarations.Add(ReadOffsetY);
Program.TopLevelDeclarations.Add(WriteOffsetY);
@@ -1600,8 +1522,8 @@ namespace GPUVerify Variable ReadOffsetZ = MakeOffsetZVariable(v, "READ");
Variable WriteOffsetZ = MakeOffsetZVariable(v, "WRITE");
- result.Add(new IdentifierExpr(v.tok, ReadOffsetZ));
- result.Add(new IdentifierExpr(v.tok, WriteOffsetZ));
+ newVars.Add(new IdentifierExpr(v.tok, ReadOffsetZ));
+ newVars.Add(new IdentifierExpr(v.tok, WriteOffsetZ));
Program.TopLevelDeclarations.Add(ReadOffsetZ);
Program.TopLevelDeclarations.Add(WriteOffsetZ);
@@ -1609,34 +1531,102 @@ namespace GPUVerify }
}
- return result;
+ foreach (IdentifierExpr e in newVars)
+ {
+ KernelProcedure.Modifies.Add(e);
+ }
}
- private bool IsIntOrBv32(Microsoft.Boogie.Type type)
+
+
+ internal static bool IsIntOrBv32(Microsoft.Boogie.Type type)
{
return type.Equals(Microsoft.Boogie.Type.Int) || type.Equals(Microsoft.Boogie.Type.GetBvType(32));
}
private void PullOutNonLocalAccesses()
{
- KernelImplementation.StructuredStmts = PullOutNonLocalAccesses(KernelImplementation.StructuredStmts);
+ foreach (Declaration d in Program.TopLevelDeclarations)
+ {
+ if (d is Implementation)
+ {
+ (d as Implementation).StructuredStmts = PullOutNonLocalAccesses((d as Implementation).StructuredStmts, (d as Implementation));
+ }
+ }
+ }
+
+ private void RemoveElseIfs()
+ {
+ foreach (Declaration d in Program.TopLevelDeclarations)
+ {
+ if (d is Implementation)
+ {
+ (d as Implementation).StructuredStmts = RemoveElseIfs((d as Implementation).StructuredStmts);
+ }
+ }
+ }
+
+ private StmtList RemoveElseIfs(StmtList stmtList)
+ {
+ Contract.Requires(stmtList != null);
+
+ StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
+
+ foreach (BigBlock bodyBlock in stmtList.BigBlocks)
+ {
+ result.BigBlocks.Add(RemoveElseIfs(bodyBlock));
+ }
+
+ return result;
+ }
+
+ private BigBlock RemoveElseIfs(BigBlock bb)
+ {
+ BigBlock result = bb;
+ if (bb.ec is IfCmd)
+ {
+ IfCmd IfCommand = bb.ec as IfCmd;
+
+ Debug.Assert(IfCommand.elseIf == null || IfCommand.elseBlock == null);
+
+ if (IfCommand.elseIf != null)
+ {
+ IfCommand.elseBlock = new StmtList(new List<BigBlock>(new BigBlock[] {
+ new BigBlock(bb.tok, null, new CmdSeq(), IfCommand.elseIf, null)
+ }), bb.tok);
+ IfCommand.elseIf = null;
+ }
+
+ IfCommand.thn = RemoveElseIfs(IfCommand.thn);
+ if (IfCommand.elseBlock != null)
+ {
+ IfCommand.elseBlock = RemoveElseIfs(IfCommand.elseBlock);
+ }
+
+ }
+ else if (bb.ec is WhileCmd)
+ {
+ (bb.ec as WhileCmd).Body = RemoveElseIfs((bb.ec as WhileCmd).Body);
+ }
+
+ return result;
}
- private StmtList PullOutNonLocalAccesses(StmtList stmtList)
+ private StmtList PullOutNonLocalAccesses(StmtList stmtList, Implementation impl)
{
- Contract.Requires(stmtList != null);
+ Contract.Requires(stmtList != null);
StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
foreach (BigBlock bodyBlock in stmtList.BigBlocks)
{
- result.BigBlocks.Add(PullOutNonLocalAccesses(bodyBlock));
+ result.BigBlocks.Add(PullOutNonLocalAccesses(bodyBlock, impl));
}
return result;
}
- private BigBlock PullOutNonLocalAccesses(BigBlock bb)
+ private BigBlock PullOutNonLocalAccesses(BigBlock bb, Implementation impl)
{
BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
@@ -1660,7 +1650,7 @@ namespace GPUVerify LocalVariable tempDecl;
e = ExtractLocalAccessToTemp(e, out assignToTemp, out tempDecl);
result.simpleCmds.Add(assignToTemp);
- KernelImplementation.LocVars.Add(tempDecl);
+ impl.LocVars.Add(tempDecl);
}
newIns.Add(e);
@@ -1684,7 +1674,7 @@ namespace GPUVerify }
else
{
- rhs = PullOutNonLocalAccessesIntoTemps(result, rhs);
+ rhs = PullOutNonLocalAccessesIntoTemps(result, rhs, impl);
List<AssignLhs> newLhss = new List<AssignLhs>();
newLhss.Add(lhs);
List<Expr> newRhss = new List<Expr>();
@@ -1699,11 +1689,11 @@ namespace GPUVerify }
else if (c is AssertCmd)
{
- result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr)));
+ result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr, impl)));
}
else if (c is AssumeCmd)
{
- result.simpleCmds.Add(new AssumeCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssumeCmd).Expr)));
+ result.simpleCmds.Add(new AssumeCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssumeCmd).Expr, impl)));
}
else
{
@@ -1721,11 +1711,11 @@ namespace GPUVerify LocalVariable tempDecl;
WhileCommand.Guard = ExtractLocalAccessToTemp(WhileCommand.Guard, out assignToTemp, out tempDecl);
result.simpleCmds.Add(assignToTemp);
- KernelImplementation.LocVars.Add(tempDecl);
+ impl.LocVars.Add(tempDecl);
}
- result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, PullOutNonLocalAccesses(WhileCommand.Body));
+ result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, PullOutNonLocalAccesses(WhileCommand.Body, impl));
}
- else if(bb.ec is IfCmd)
+ else if (bb.ec is IfCmd)
{
IfCmd IfCommand = bb.ec as IfCmd;
Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
@@ -1735,9 +1725,13 @@ namespace GPUVerify LocalVariable tempDecl;
IfCommand.Guard = ExtractLocalAccessToTemp(IfCommand.Guard, out assignToTemp, out tempDecl);
result.simpleCmds.Add(assignToTemp);
- KernelImplementation.LocVars.Add(tempDecl);
+ impl.LocVars.Add(tempDecl);
}
- result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, PullOutNonLocalAccesses(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? PullOutNonLocalAccesses(IfCommand.elseBlock) : null);
+ result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, PullOutNonLocalAccesses(IfCommand.thn, impl), IfCommand.elseIf, IfCommand.elseBlock != null ? PullOutNonLocalAccesses(IfCommand.elseBlock, impl) : null);
+ }
+ else if (bb.ec is BreakCmd)
+ {
+ result.ec = bb.ec;
}
else
{
@@ -1748,7 +1742,7 @@ namespace GPUVerify }
- private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e)
+ private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e, Implementation impl)
{
while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
{
@@ -1756,7 +1750,7 @@ namespace GPUVerify LocalVariable tempDecl;
e = ExtractLocalAccessToTemp(e, out assignToTemp, out tempDecl);
result.simpleCmds.Add(assignToTemp);
- KernelImplementation.LocVars.Add(tempDecl);
+ impl.LocVars.Add(tempDecl);
}
return e;
}
@@ -1780,18 +1774,29 @@ namespace GPUVerify {
if (d is Procedure)
{
+
// DuplicateParameters
Procedure proc = d as Procedure;
- proc.InParams = DualiseVariableSequence(proc.InParams);
- proc.OutParams = DualiseVariableSequence(proc.OutParams);
+
+ bool HalfDualise = HalfDualisedProcedureNames.Contains(proc.Name);
+
+ 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).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
}
- foreach (IdentifierExpr v in proc.Modifies)
+
+ if (!HalfDualise)
{
- NewModifies.Add(new VariableDualiser(2).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
+ foreach (IdentifierExpr v in proc.Modifies)
+ {
+ if (!CommandLineOptions.Symmetry || !HalfDualisedVariableNames.Contains(v.Name))
+ {
+ NewModifies.Add(new VariableDualiser(2).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
+ }
+ }
}
proc.Modifies = NewModifies;
@@ -1805,10 +1810,13 @@ namespace GPUVerify {
// DuplicateParameters
Implementation impl = d as Implementation;
- impl.InParams = DualiseVariableSequence(impl.InParams);
- impl.OutParams = DualiseVariableSequence(impl.OutParams);
- MakeDualLocalVariables(impl);
- impl.StructuredStmts = MakeDual(impl.StructuredStmts);
+
+ bool HalfDualise = 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);
NewTopLevelDeclarations.Add(impl);
@@ -1819,7 +1827,11 @@ namespace GPUVerify if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)))
{
NewTopLevelDeclarations.Add(new VariableDualiser(1).VisitVariable((Variable)d.Clone()));
- NewTopLevelDeclarations.Add(new VariableDualiser(2).VisitVariable((Variable)d.Clone()));
+
+ if (!HalfDualisedVariableNames.Contains((d as Variable).Name))
+ {
+ NewTopLevelDeclarations.Add(new VariableDualiser(2).VisitVariable((Variable)d.Clone()));
+ }
continue;
}
@@ -1832,16 +1844,20 @@ namespace GPUVerify }
- private static VariableSeq DualiseVariableSequence(VariableSeq seq)
+ private static VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise)
{
VariableSeq result = new VariableSeq();
foreach (Variable v in seq)
{
result.Add(new VariableDualiser(1).VisitVariable((Variable)v.Clone()));
}
- foreach (Variable v in seq)
+
+ if (!HalfDualise)
{
- result.Add(new VariableDualiser(2).VisitVariable((Variable)v.Clone()));
+ foreach (Variable v in seq)
+ {
+ result.Add(new VariableDualiser(2).VisitVariable((Variable)v.Clone()));
+ }
}
return result;
}
@@ -1898,11 +1914,11 @@ namespace GPUVerify WhileLoopCounter = 0;
IfCounter = 0;
RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
- impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate);
+ impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);
AddPredicateLocalVariables(impl);
}
- private StmtList MakeDual(StmtList stmtList)
+ private StmtList MakeDual(StmtList stmtList, bool HalfDualise)
{
Contract.Requires(stmtList != null);
@@ -1910,13 +1926,13 @@ namespace GPUVerify foreach (BigBlock bodyBlock in stmtList.BigBlocks)
{
- result.BigBlocks.Add(MakeDual(bodyBlock));
+ result.BigBlocks.Add(MakeDual(bodyBlock, HalfDualise));
}
return result;
}
- private BigBlock MakeDual(BigBlock bb)
+ private BigBlock MakeDual(BigBlock bb, bool HalfDualise)
{
// Not sure what to do about the transfer command
@@ -1933,9 +1949,12 @@ namespace GPUVerify {
newIns.Add(new VariableDualiser(1).VisitExpr(e));
}
- foreach (Expr e in Call.Ins)
+ if (!HalfDualise && !HalfDualisedProcedureNames.Contains(Call.callee))
{
- newIns.Add(new VariableDualiser(2).VisitExpr(e));
+ foreach (Expr e in Call.Ins)
+ {
+ newIns.Add(new VariableDualiser(2).VisitExpr(e));
+ }
}
List<IdentifierExpr> newOuts = new List<IdentifierExpr>();
@@ -1943,9 +1962,12 @@ namespace GPUVerify {
newOuts.Add(new VariableDualiser(1).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
}
- foreach (IdentifierExpr ie in Call.Outs)
+ if (!HalfDualise && !HalfDualisedProcedureNames.Contains(Call.callee))
{
- newOuts.Add(new VariableDualiser(2).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
+ foreach (IdentifierExpr ie in Call.Outs)
+ {
+ newOuts.Add(new VariableDualiser(2).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
+ }
}
CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
@@ -1961,12 +1983,20 @@ namespace GPUVerify List<AssignLhs> newLhss = new List<AssignLhs>();
newLhss.Add(new VariableDualiser(1).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
- newLhss.Add(new VariableDualiser(2).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+
+ if (!HalfDualise)
+ {
+ newLhss.Add(new VariableDualiser(2).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+ }
List<Expr> newRhss = new List<Expr>();
newRhss.Add(new VariableDualiser(1).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
- newRhss.Add(new VariableDualiser(2).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+
+ if (!HalfDualise)
+ {
+ newRhss.Add(new VariableDualiser(2).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ }
AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
@@ -1976,21 +2006,47 @@ namespace GPUVerify {
HavocCmd havoc = c as HavocCmd;
Debug.Assert(havoc.Vars.Length == 1);
- HavocCmd newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
- (IdentifierExpr)(new VariableDualiser(2).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
+
+ HavocCmd newHavoc;
+
+ if (HalfDualise)
+ {
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
+ }
+ else
+ {
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
+ (IdentifierExpr)(new VariableDualiser(2).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
+ }
result.simpleCmds.Add(newHavoc);
}
else if (c is AssertCmd)
{
AssertCmd ass = c as AssertCmd;
- result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
+ if (HalfDualise)
+ {
+ result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
+ else
+ {
+ result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
+ }
}
else if (c is AssumeCmd)
{
AssumeCmd ass = c as AssumeCmd;
- result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
+ if (HalfDualise)
+ {
+ result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
+ else
+ {
+ result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
+ }
}
else
{
@@ -2000,7 +2056,7 @@ namespace GPUVerify if (bb.ec is WhileCmd)
{
- result.ec = new WhileCmd(bb.ec.tok, Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard), new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)), (bb.ec as WhileCmd).Invariants, MakeDual((bb.ec as WhileCmd).Body));
+ result.ec = new WhileCmd(bb.ec.tok, Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard), new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)), (bb.ec as WhileCmd).Invariants, MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
}
else
{
@@ -2011,14 +2067,17 @@ namespace GPUVerify }
- private void MakeDualLocalVariables(Implementation impl)
+ private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)
{
VariableSeq NewLocalVars = new VariableSeq();
foreach (LocalVariable v in impl.LocVars)
{
NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$1", v.TypedIdent.Type)));
- NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$2", v.TypedIdent.Type)));
+ if (!HalfDualise)
+ {
+ NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$2", v.TypedIdent.Type)));
+ }
}
impl.LocVars = NewLocalVars;
@@ -2041,13 +2100,13 @@ namespace GPUVerify }
- private StmtList MakePredicated(StmtList sl, Expr predicate)
+ 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);
+ List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);
foreach (BigBlock newBigBlock in newBigBlocks)
{
result.BigBlocks.Add(newBigBlock);
@@ -2058,7 +2117,7 @@ namespace GPUVerify }
- private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate)
+ private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)
{
// Not sure what to do about the transfer command
@@ -2085,7 +2144,7 @@ namespace GPUVerify 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);
@@ -2154,7 +2213,7 @@ namespace GPUVerify 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));
+ 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));
@@ -2187,7 +2246,7 @@ namespace GPUVerify Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
- StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr));
+ StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);
foreach (BigBlock bb in PredicatedThen.BigBlocks)
{
@@ -2196,7 +2255,7 @@ namespace GPUVerify if (IfCommand.elseBlock != null)
{
- StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)));
+ StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);
foreach (BigBlock bb in PredicatedElse.BigBlocks)
{
@@ -2208,6 +2267,17 @@ namespace GPUVerify }
+ 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);
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 0e07f573..fcf68350 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -75,12 +75,18 @@ <Compile Include="AccessCollector.cs" />
<Compile Include="AccessRecord.cs" />
<Compile Include="CommandLineOptions.cs" />
+ <Compile Include="ElementEncodingraceInstrumenter.cs" />
<Compile Include="GPUVerifier.cs" />
+ <Compile Include="IRaceInstrumenter.cs" />
<Compile Include="Main.cs" />
+ <Compile Include="NoConflictingAccessOptimiser.cs" />
<Compile Include="NonLocalAccessCollector.cs" />
<Compile Include="NonLocalAccessExtractor.cs" />
+ <Compile Include="NullRaceInstrumenter.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="RaceInstrumenterBase.cs" />
<Compile Include="ReadCollector.cs" />
+ <Compile Include="SetEncodingRaceInstrumenter.cs" />
<Compile Include="VariableDualiser.cs" />
<Compile Include="WriteCollector.cs" />
</ItemGroup>
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs new file mode 100644 index 00000000..2540c9d7 --- /dev/null +++ b/Source/GPUVerify/IRaceInstrumenter.cs @@ -0,0 +1,29 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ interface IRaceInstrumenter
+ {
+ void AddRaceCheckingCandidateInvariants(WhileCmd wc);
+ void AddKernelPrecondition();
+
+ // Summary:
+ // Returns whether we should continue.
+ // E.g. if race checking code could not be added because
+ // the specified accesses to check were read/read or did not exist,
+ // this will return false.
+ bool AddRaceCheckingInstrumentation();
+
+ BigBlock MakeRaceCheckingStatements(IToken tok);
+
+ void CheckForRaces(IToken tok, BigBlock bb, Variable v);
+
+ void AddRaceCheckingCandidateRequires(Procedure Proc);
+
+ void AddRaceCheckingCandidateEnsures(Procedure Proc);
+ }
+}
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 6c101e7f..06fe70c6 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -9,6 +9,7 @@ using System.Windows.Forms; using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
namespace GPUVerify
{
@@ -71,6 +72,11 @@ namespace GPUVerify }
+ parseProcessOutput();
+ }
+
+ public static Program parse()
+ {
Program program = ParseBoogieProgram(CommandLineOptions.inputFiles, false);
if (program == null)
{
@@ -92,14 +98,121 @@ namespace GPUVerify Environment.Exit(1);
}
- GPUVerifier verifier = new GPUVerifier(program);
+ return program;
+ }
- verifier.doit();
+ private static Variable findClonedVar(Variable v1, ICollection<Variable> vars)
+ {
+ foreach (Variable v2 in vars)
+ {
+ if (v1.Name.Equals(v2.Name))
+ {
+ return v2;
+ }
+ }
+ return null;
+ }
+ 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();
+ GPUVerifier newGp = new GPUVerifier(filename, newProgram, ri);
+ ri.setVerifier(newGp);
+
+
+ Variable newG = findClonedVar(v, newGp.GlobalVariables);
+ Variable newT = findClonedVar(v, newGp.TileStaticVariables);
+ Contract.Assert(newG == null || newT == null);
+
+ ri.globalVarsToCheck.Clear();
+ ri.tileStaticVarsToCheck.Clear();
+ ri.onlyLog1 = a1;
+ ri.onlyLog2 = a2;
+
+ if (newG != null)
+ {
+ ri.globalVarsToCheck.Add(newG);
+ }
+
+ if (newT != null)
+ {
+ ri.globalVarsToCheck.Add(newT);
+ }
+
+ newGp.doit();
+
+ return !ri.failedToFindSecondAccess;
}
+ public static IList<GPUVerifier> parseProcessOutput()
+ {
+ string fn = "temp";
+ if (CommandLineOptions.outputFile != null)
+ {
+ fn = CommandLineOptions.outputFile;
+ }
+ Program program = parse();
+ IList<GPUVerifier> result = new List<GPUVerifier>();
+ GPUVerifier g = new GPUVerifier(fn, program, new NullRaceInstrumenter());
+
+ if (CommandLineOptions.DividedArray)
+ {
+ List<Variable> nonLocalVars = new List<Variable>();
+ nonLocalVars.AddRange(g.GlobalVariables);
+ nonLocalVars.AddRange(g.TileStaticVariables);
+ foreach (Variable v in nonLocalVars)
+ {
+ if (CommandLineOptions.DividedAccesses)
+ {
+ int i = 0;
+ int j = 0;
+ while (true)
+ {
+ bool res = doit(fn + "." + v.Name + "." + i + "." + (i + j), v, i, j);
+ if (!res)
+ {
+ if (j == 0)
+ {
+ break;
+ }
+ else
+ {
+ i++;
+ j = 0;
+ }
+ }
+ else
+ {
+ j++;
+ }
+ }
+ }
+ else
+ {
+ doit("temp_" + v.Name + ".bpl", v, -1, -1);
+ }
+ }
+ }
+ else
+ {
+ if (!CommandLineOptions.OnlyDivergence)
+ {
+ RaceInstrumenterBase ri = CommandLineOptions.SetEncoding ? (RaceInstrumenterBase)new SetEncodingRaceInstrumenter() : (RaceInstrumenterBase)new ElementEncodingRaceInstrumenter();
+ ri.setVerifier(g);
+ g.setRaceInstrumenter(ri);
+ }
+
+ g.doit();
+ result.Add(g);
+
+ }
+
+ return result;
+
+ }
diff --git a/Source/GPUVerify/NoConflictingAccessOptimiser.cs b/Source/GPUVerify/NoConflictingAccessOptimiser.cs new file mode 100644 index 00000000..f003a3a9 --- /dev/null +++ b/Source/GPUVerify/NoConflictingAccessOptimiser.cs @@ -0,0 +1,116 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+
+namespace GPUVerify
+{
+ class NoConflictingAccessOptimiser
+ {
+ private Implementation impl;
+ private IList<CallCmdPos> ccs;
+
+ public NoConflictingAccessOptimiser(Implementation impl)
+ {
+ this.impl = impl;
+ ccs = new List<CallCmdPos>();
+ FindCallCmds();
+ }
+
+ private class CallCmdPos
+ {
+ public Block block;
+ public int cmdIndex;
+ public CallCmd cc;
+
+ public CallCmdPos(Block block, int cmdIndex, CallCmd cc)
+ {
+ this.block = block;
+ this.cmdIndex = cmdIndex;
+ this.cc = cc;
+ }
+ }
+
+ public int NumLogCalls()
+ {
+ return ccs.Count;
+ }
+
+ private void FindCallCmds()
+ {
+ foreach (Block b in impl.Blocks)
+ {
+ for(int i=0; i < b.Cmds.Length; i++)
+ {
+ Cmd c = b.Cmds[i];
+ CallCmd cc = c as CallCmd;
+ if (cc != null)
+ {
+ if (cc.Proc.Name.Contains("_LOG"))
+ {
+ ccs.Add(new CallCmdPos(b, i, cc));
+ }
+ }
+ }
+ }
+ }
+
+ public bool HasConflicting()
+ {
+ Contract.Assert(ccs.Count == 2);
+
+ return
+ Reachable(ccs[0].block, ccs[0].cmdIndex, ccs[1].cc, new HashSet<Block>()) ||
+ Reachable(ccs[1].block, ccs[1].cmdIndex, ccs[0].cc, new HashSet<Block>());
+ }
+
+ public bool Reachable(Block startBlock, int cmdStartIndex, CallCmd target, ISet<Block> visited)
+ {
+ Block currBlock = startBlock;
+ int i = cmdStartIndex;
+
+ if(i == 0)
+ {
+ visited.Add(currBlock);
+ }
+
+ while (i < currBlock.Cmds.Length)
+ {
+ CallCmd cc = currBlock.Cmds[i] as CallCmd;
+ if (cc != null)
+ {
+ if (cc.Proc.Name.Equals("BARRIER"))
+ {
+ return false;
+ }
+
+ if (target == cc)
+ {
+ return true;
+ }
+ }
+ i++;
+ }
+
+
+ //end of block
+
+ GotoCmd gc = currBlock.TransferCmd as GotoCmd;
+ Contract.Assert(gc != null);
+ foreach (Block t in gc.labelTargets)
+ {
+ if(visited.Contains(t))
+ continue;
+
+ if (Reachable(t, 0, target, visited))
+ return true;
+ }
+
+ return false;
+
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs index e7aac939..bbab9040 100644 --- a/Source/GPUVerify/NonLocalAccessCollector.cs +++ b/Source/GPUVerify/NonLocalAccessCollector.cs @@ -12,16 +12,16 @@ namespace GPUVerify {
public HashSet<Expr> Accesses = new HashSet<Expr>();
- private List<Variable> GlobalVariables;
- private List<Variable> TileStaticVariables;
+ private ICollection<Variable> GlobalVariables;
+ private ICollection<Variable> TileStaticVariables;
- public NonLocalAccessCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public NonLocalAccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
{
this.GlobalVariables = GlobalVariables;
this.TileStaticVariables = TileStaticVariables;
}
- public static bool IsNonLocalAccess(Expr n, List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public static bool IsNonLocalAccess(Expr n, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
{
if (n is NAryExpr)
{
@@ -50,7 +50,7 @@ namespace GPUVerify return false;
}
- public static bool ContainsNonLocalAccess(AssignLhs lhs, List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public static bool ContainsNonLocalAccess(AssignLhs lhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
{
NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);
if (lhs is SimpleAssignLhs)
@@ -65,7 +65,7 @@ namespace GPUVerify return collector.Accesses.Count > 0;
}
- public static bool ContainsNonLocalAccess(Expr rhs, List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public static bool ContainsNonLocalAccess(Expr rhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
{
NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);
collector.VisitExpr(rhs);
diff --git a/Source/GPUVerify/NonLocalAccessExtractor.cs b/Source/GPUVerify/NonLocalAccessExtractor.cs index af266446..506ec3c5 100644 --- a/Source/GPUVerify/NonLocalAccessExtractor.cs +++ b/Source/GPUVerify/NonLocalAccessExtractor.cs @@ -14,10 +14,10 @@ namespace GPUVerify public LocalVariable Declaration = null;
public bool done = false;
- private List<Variable> GlobalVariables;
- private List<Variable> TileStaticVariables;
+ private ICollection<Variable> GlobalVariables;
+ private ICollection<Variable> TileStaticVariables;
- public NonLocalAccessExtractor(int TempId, List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public NonLocalAccessExtractor(int TempId, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
{
this.TempId = TempId;
this.GlobalVariables = GlobalVariables;
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs new file mode 100644 index 00000000..3958a94e --- /dev/null +++ b/Source/GPUVerify/NullRaceInstrumenter.cs @@ -0,0 +1,47 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class NullRaceInstrumenter : IRaceInstrumenter
+ {
+
+ public void AddRaceCheckingCandidateInvariants(Microsoft.Boogie.WhileCmd wc)
+ {
+
+ }
+
+ public void AddKernelPrecondition()
+ {
+
+ }
+
+ public void CheckForRaces(IToken tok, BigBlock bb, Variable v)
+ {
+ }
+
+ public bool AddRaceCheckingInstrumentation()
+ {
+ return true;
+ }
+
+ public Microsoft.Boogie.BigBlock MakeRaceCheckingStatements(Microsoft.Boogie.IToken tok)
+ {
+ return new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
+ }
+
+ public void AddRaceCheckingCandidateRequires(Procedure Proc)
+ {
+
+ }
+
+ public void AddRaceCheckingCandidateEnsures(Procedure Proc)
+ {
+
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs new file mode 100644 index 00000000..90229af0 --- /dev/null +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -0,0 +1,463 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify
+{
+ abstract class RaceInstrumenterBase : IRaceInstrumenter
+ {
+ protected GPUVerifier verifier;
+ public ICollection<Variable> globalVarsToCheck;
+ public ICollection<Variable> tileStaticVarsToCheck;
+
+ public int onlyLog1;
+ public int onlyLog2;
+ public bool failedToFindSecondAccess;
+ public bool addedLogWrite;
+ private int logAddCount;
+
+ public RaceInstrumenterBase()
+ {
+ onlyLog1 = -1;
+ onlyLog2 = -1;
+ failedToFindSecondAccess = false;
+ addedLogWrite = false;
+ logAddCount = 0;
+ }
+
+ public void setVerifier(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ globalVarsToCheck = new HashSet<Variable>(verifier.GlobalVariables);
+ tileStaticVarsToCheck = new HashSet<Variable>(verifier.TileStaticVariables);
+ }
+
+ protected abstract void AddRequiresNoPendingAccess(Variable v);
+
+ private void AddNoReadOrWriteCandidateInvariants(WhileCmd wc, Variable v)
+ {
+ AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "1");
+ AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "1");
+ if (!CommandLineOptions.Symmetry)
+ {
+ AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "2");
+ }
+ AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "2");
+ }
+
+ private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v)
+ {
+ 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");
+ }
+
+ protected abstract void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo);
+
+ protected abstract void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);
+
+ protected abstract void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);
+
+ public void AddRaceCheckingCandidateInvariants(WhileCmd wc)
+ {
+ foreach (Variable v in globalVarsToCheck)
+ {
+ AddNoReadOrWriteCandidateInvariants(wc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);
+ }
+
+ foreach (Variable v in tileStaticVarsToCheck)
+ {
+ AddNoReadOrWriteCandidateInvariants(wc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);
+ }
+ }
+
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(WhileCmd wc, Variable v)
+ {
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(wc, v, "WRITE", 1);
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(wc, v, "WRITE", 2);
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(wc, v, "READ", 1);
+ if (!CommandLineOptions.Symmetry)
+ {
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(wc, v, "READ", 2);
+ }
+ }
+
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)
+ {
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v, "WRITE", 1);
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v, "WRITE", 2);
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v, "READ", 1);
+ if (!CommandLineOptions.Symmetry)
+ {
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v, "READ", 2);
+ }
+ }
+
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v)
+ {
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v, "WRITE", 1);
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v, "WRITE", 2);
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v, "READ", 1);
+ if (!CommandLineOptions.Symmetry)
+ {
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v, "READ", 2);
+ }
+ }
+
+ protected abstract void AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, int Thread);
+
+ protected abstract void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
+
+ protected abstract void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
+
+ public void AddKernelPrecondition()
+ {
+ foreach (Variable v in globalVarsToCheck)
+ {
+ AddRequiresNoPendingAccess(v);
+ }
+
+ foreach (Variable v in tileStaticVarsToCheck)
+ {
+ AddRequiresNoPendingAccess(v);
+ }
+ }
+ public bool AddRaceCheckingInstrumentation()
+ {
+
+ if (onlyLog1 != -1)
+ {
+ addedLogWrite = false;
+ failedToFindSecondAccess = true;
+ }
+ else
+ {
+ addedLogWrite = true;
+ failedToFindSecondAccess = false;
+ }
+
+ AddRaceCheckCalls(verifier.KernelImplementation);
+
+ if (failedToFindSecondAccess || !addedLogWrite)
+ return false;
+
+ foreach (Variable v in globalVarsToCheck)
+ {
+ AddRaceCheckingDecsAndProcsForVar(v);
+ }
+
+ foreach (Variable v in tileStaticVarsToCheck)
+ {
+ AddRaceCheckingDecsAndProcsForVar(v);
+ }
+
+ return true;
+
+ }
+
+ private void AddRaceCheckingDecsAndProcsForVar(Variable v)
+ {
+ AddLogRaceDeclarations(v, "READ");
+ AddLogRaceDeclarations(v, "WRITE");
+ AddLogAccessProcedure(v, "READ");
+ AddLogAccessProcedure(v, "WRITE");
+ }
+
+ private StmtList AddRaceCheckCalls(StmtList stmtList)
+ {
+ Contract.Requires(stmtList != null);
+
+ StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
+
+ foreach (BigBlock bodyBlock in stmtList.BigBlocks)
+ {
+ result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));
+ }
+ return result;
+ }
+
+ private void AddRaceCheckCalls(Implementation impl)
+ {
+ impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
+ }
+
+ private bool shouldAddLogCallAndIncr()
+ {
+ Contract.Assert(onlyLog1 >= -1);
+ int oldLogAddCount = logAddCount;
+ ++logAddCount;
+
+ if (onlyLog1 == -1)
+ {
+ return true;
+ }
+
+ if(onlyLog1 + onlyLog2 == oldLogAddCount)
+ {
+ failedToFindSecondAccess = false;
+ return true;
+ }
+
+ if (onlyLog1 == oldLogAddCount)
+ {
+ return true;
+ }
+
+ return false;
+ }
+
+ private BigBlock AddRaceCheckCalls(BigBlock bb)
+ {
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is AssignCmd)
+ {
+ AssignCmd assign = c as AssignCmd;
+ Debug.Assert(assign.Lhss.Count == 1);
+ Debug.Assert(assign.Rhss.Count == 1);
+ AssignLhs lhs = assign.Lhss[0];
+ Expr rhs = assign.Rhss[0];
+
+ ReadCollector rc = new ReadCollector(globalVarsToCheck, tileStaticVarsToCheck);
+ rc.Visit(rhs);
+ if (rc.accesses.Count > 0)
+ {
+ Debug.Assert(rc.accesses.Count == 1);
+ AccessRecord ar = rc.accesses[0];
+
+ if (shouldAddLogCallAndIncr())
+ {
+
+ ExprSeq inParams = new ExprSeq();
+ if (ar.IndexZ != null)
+ {
+ inParams.Add(ar.IndexZ);
+ }
+ if (ar.IndexY != null)
+ {
+ inParams.Add(ar.IndexY);
+ }
+ if (ar.IndexX != null)
+ {
+ inParams.Add(ar.IndexX);
+ }
+
+ result.simpleCmds.Add(new CallCmd(c.tok, "_LOG_READ_" + ar.v.Name, inParams, new IdentifierExprSeq()));
+
+ }
+ }
+
+ WriteCollector wc = new WriteCollector(globalVarsToCheck, tileStaticVarsToCheck);
+ wc.Visit(lhs);
+ if (wc.GetAccess() != null)
+ {
+ AccessRecord ar = wc.GetAccess();
+
+ if (shouldAddLogCallAndIncr())
+ {
+
+ ExprSeq inParams = new ExprSeq();
+ if (ar.IndexZ != null)
+ {
+ inParams.Add(ar.IndexZ);
+ }
+ if (ar.IndexY != null)
+ {
+ inParams.Add(ar.IndexY);
+ }
+ if (ar.IndexX != null)
+ {
+ inParams.Add(ar.IndexX);
+ }
+
+ result.simpleCmds.Add(new CallCmd(c.tok, "_LOG_WRITE_" + ar.v.Name, inParams, new IdentifierExprSeq()));
+ addedLogWrite = true;
+
+ }
+ }
+
+
+
+ }
+ result.simpleCmds.Add(c);
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd WhileCommand = bb.ec as WhileCmd;
+ result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, AddRaceCheckCalls(WhileCommand.Body));
+ }
+ else if (bb.ec is IfCmd)
+ {
+ IfCmd IfCommand = bb.ec as IfCmd;
+ Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
+ result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, AddRaceCheckCalls(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? AddRaceCheckCalls(IfCommand.elseBlock) : null);
+ }
+ else if (bb.ec is BreakCmd)
+ {
+ result.ec = bb.ec;
+ }
+ else
+ {
+ Debug.Assert(bb.ec == null);
+ }
+
+ return result;
+
+ }
+
+
+ protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite);
+
+ protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);
+
+
+ public BigBlock MakeRaceCheckingStatements(IToken tok)
+ {
+ 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)
+ {
+ CheckForRaces(tok, checkForRaces, v);
+ }
+ }
+
+ foreach (Variable v in globalVarsToCheck)
+ {
+ SetNoAccessOccurred(tok, checkForRaces, v);
+ }
+ foreach (Variable v in tileStaticVarsToCheck)
+ {
+ SetNoAccessOccurred(tok, checkForRaces, v);
+ }
+ return checkForRaces;
+ }
+
+ private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v)
+ {
+ SetNoAccessOccurred(tok, bb, v, "READ");
+ SetNoAccessOccurred(tok, bb, v, "WRITE");
+ }
+
+ protected abstract void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType);
+
+ public abstract void CheckForRaces(IToken tok, BigBlock bb, Variable v);
+
+ protected void MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite, out Variable XParameterVariable, out Variable YParameterVariable, out Variable ZParameterVariable, out Procedure LogReadOrWriteProcedure)
+ {
+ 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);
+ Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));
+
+ 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]));
+ }
+ }
+ }
+
+ if (ZParameterVariable != null)
+ {
+ inParams.Add(ZParameterVariable);
+ }
+
+ if (YParameterVariable != null)
+ {
+ inParams.Add(YParameterVariable);
+ }
+
+ if (XParameterVariable != null)
+ {
+ inParams.Add(XParameterVariable);
+ }
+
+ LogReadOrWriteProcedure = new Procedure(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), inParams, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+
+ if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ {
+ verifier.HalfDualisedProcedureNames.Add(LogReadOrWriteProcedure.Name);
+ }
+
+ LogReadOrWriteProcedure.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+
+ }
+
+ public void AddRaceCheckingCandidateRequires(Procedure Proc)
+ {
+ foreach (Variable v in globalVarsToCheck)
+ {
+ AddNoReadOrWriteCandidateRequires(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
+ }
+
+ foreach (Variable v in tileStaticVarsToCheck)
+ {
+ AddNoReadOrWriteCandidateRequires(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
+ }
+ }
+
+ public void AddRaceCheckingCandidateEnsures(Procedure Proc)
+ {
+ foreach (Variable v in globalVarsToCheck)
+ {
+ AddNoReadOrWriteCandidateEnsures(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
+ }
+
+ foreach (Variable v in tileStaticVarsToCheck)
+ {
+ AddNoReadOrWriteCandidateEnsures(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
+ }
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs index 7c2d2dfc..281620c5 100644 --- a/Source/GPUVerify/ReadCollector.cs +++ b/Source/GPUVerify/ReadCollector.cs @@ -15,9 +15,9 @@ namespace GPUVerify class ReadCollector : AccessCollector
{
- public HashSet<AccessRecord> accesses = new HashSet<AccessRecord>();
+ public List<AccessRecord> accesses = new List<AccessRecord>();
- public ReadCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public ReadCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
: base(GlobalVariables, TileStaticVariables)
{
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs new file mode 100644 index 00000000..c4f42923 --- /dev/null +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -0,0 +1,786 @@ +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)
+ {
+ Variable AccessSet = MakeAccessSetVariable(v, ReadOrWrite);
+
+ if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))
+ {
+ verifier.HalfDualisedVariableNames.Add(AccessSet.Name);
+ }
+
+ verifier.Program.TopLevelDeclarations.Add(AccessSet);
+
+ // TODO: add modiies to every procedure that calls BARRIER
+
+ verifier.KernelProcedure.Modifies.Add(new IdentifierExpr(v.tok, AccessSet));
+ }
+
+ 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)) });
+
+ 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).VisitVariable(
+ 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));
+
+ 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));
+
+ Add3DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
+
+ }
+ else
+ {
+ Add2DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0], mt2.Arguments[0]);
+ }
+ }
+ else
+ {
+ Add1DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0]);
+ }
+ }
+ else
+ {
+ Add0DAssumeNoAccess(tok, bb, v, AccessType);
+ }
+ }
+
+ public override void CheckForRaces(IToken tok, BigBlock bb, Variable v)
+ {
+ 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));
+
+ Add3DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
+ Add3DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
+ if (!CommandLineOptions.Symmetry)
+ {
+ Add3DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);
+ }
+
+
+ }
+ else
+ {
+
+ Add2DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0], mt2.Arguments[0]);
+ Add2DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0], mt2.Arguments[0]);
+ if (!CommandLineOptions.Symmetry)
+ {
+ Add2DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0], mt2.Arguments[0]);
+ }
+ }
+ }
+ else
+ {
+ Add1DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0]);
+ Add1DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0]);
+ if (!CommandLineOptions.Symmetry)
+ {
+ Add1DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0]);
+ }
+ }
+ }
+ else
+ {
+ Add0DRaceCheck(tok, bb, v, "WRITE", "WRITE");
+ Add0DRaceCheck(tok, bb, v, "READ", "WRITE");
+ if (!CommandLineOptions.Symmetry)
+ {
+ Add0DRaceCheck(tok, bb, v, "WRITE", "READ");
+ }
+ }
+ }
+
+ private static void Add0DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2)
+ {
+ bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(Expr.And(
+ new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))),
+ new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2)))
+ ))));
+ }
+
+ private static void Add1DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexType)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexType));
+ bb.simpleCmds.Add(new AssertCmd(tok,
+ new ForallExpr(tok, new VariableSeq(new Variable[] { DummyX }),
+ Expr.Not(Expr.And(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyX) }),
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyX) })
+ ))
+ )
+ ));
+ }
+
+ private static void Add2DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));
+ bb.simpleCmds.Add(new AssertCmd(tok,
+ new ForallExpr(tok, new VariableSeq(new Variable[] { DummyY, DummyX }),
+ Expr.Not(Expr.And(
+ Expr.Select(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyY) }),
+ new Expr[] { new IdentifierExpr(tok, DummyX) }
+ ),
+ Expr.Select(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyY) }),
+ new Expr[] { new IdentifierExpr(tok, DummyX) }
+ )
+ ))
+ )
+ ));
+ }
+
+ private static void Add3DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));
+ Variable DummyZ = new LocalVariable(tok, new TypedIdent(tok, "__z", IndexTypeX));
+ bb.simpleCmds.Add(new AssertCmd(tok,
+ new ForallExpr(tok, new VariableSeq(new Variable[] { DummyZ, DummyY, DummyX }),
+ Expr.Not(Expr.And(
+ Expr.Select(
+ Expr.Select(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),
+ new Expr[] { new IdentifierExpr(tok, DummyY) }
+ ),
+ new Expr[] { new IdentifierExpr(tok, DummyX) }
+ ),
+ Expr.Select(
+ Expr.Select(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),
+ new Expr[] { new IdentifierExpr(tok, DummyY) }
+ ),
+ new Expr[] { new IdentifierExpr(tok, DummyX) }
+ )
+ ))
+ )
+ ));
+ }
+
+
+ private static void Add0DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType)
+ {
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess0DExpr(tok, v, AccessType, 1)
+ ));
+
+ if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ {
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess0DExpr(tok, v, AccessType, 2)
+ ));
+ }
+ }
+
+
+ private static void Add1DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeX)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess1DExpr(tok, v, AccessType, IndexTypeX, 1)
+ ));
+
+ if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ {
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess1DExpr(tok, v, AccessType, IndexTypeX, 2)
+ ));
+ }
+ }
+
+
+ private static void Add2DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess2DExpr(tok, v, AccessType, IndexTypeY, IndexTypeX, 1)
+ ));
+
+ if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ {
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess2DExpr(tok, v, AccessType, IndexTypeY, IndexTypeX, 2)
+ ));
+ }
+ }
+
+
+ private static void Add3DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)
+ {
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess3DExpr(tok, v, AccessType, IndexTypeZ, IndexTypeY, IndexTypeX, 1)
+ ));
+
+ if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
+ {
+ bb.simpleCmds.Add(new AssumeCmd(tok,
+ NoAccess3DExpr(tok, v, AccessType, IndexTypeZ, IndexTypeY, IndexTypeX, 2)
+ ));
+ }
+ }
+
+ private static Expr NoAccess3DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX, int Thread)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeY));
+ Variable DummyZ = new LocalVariable(tok, new TypedIdent(tok, "__z", IndexTypeZ));
+ return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyZ, DummyY, DummyX }),
+ Expr.Not(
+ Expr.Select(
+ Expr.Select(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),
+ new Expr[] { new IdentifierExpr(tok, DummyY) }
+ ),
+ new Expr[] { new IdentifierExpr(tok, DummyX) }
+ )
+ )
+ )
+ ;
+ }
+
+ private static Expr NoAccess2DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX, int Thread)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeY));
+ return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyY, DummyX }),
+ Expr.Not(
+ Expr.Select(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyY) }),
+ new Expr[] { new IdentifierExpr(tok, DummyX) }
+ )
+ )
+ )
+ ;
+ }
+
+ private static Expr NoAccess1DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeX, int Thread)
+ {
+ Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));
+ return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyX }),
+ Expr.Not(
+ Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyX) })
+ )
+ );
+ }
+
+ private static Expr NoAccess0DExpr(IToken tok, Variable v, String AccessType, int Thread)
+ {
+ return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))));
+ }
+
+
+ protected override void AddRequiresNoPendingAccess(Variable v)
+ {
+ 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));
+
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess3DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 1)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess3DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 2)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess3DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 1)));
+ if (!CommandLineOptions.Symmetry)
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess3DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 2)));
+ }
+
+
+ }
+ else
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess2DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], 1)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess2DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], 2)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess2DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], 1)));
+ if(!CommandLineOptions.Symmetry)
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess2DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], 2)));
+ }
+ }
+ }
+ else
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess1DExpr(v.tok, v, "WRITE", mt.Arguments[0], 1)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess1DExpr(v.tok, v, "WRITE", mt.Arguments[0], 2)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess1DExpr(v.tok, v, "READ", mt.Arguments[0], 1)));
+ if(!CommandLineOptions.Symmetry)
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess1DExpr(v.tok, v, "READ", mt.Arguments[0], 2)));
+ }
+ }
+ }
+ else
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess0DExpr(v.tok, v, "WRITE", 1)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess0DExpr(v.tok, v, "WRITE", 2)));
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess0DExpr(v.tok, v, "READ", 1)));
+ if(!CommandLineOptions.Symmetry)
+ {
+ verifier.KernelProcedure.Requires.Add(new Requires(false,
+ NoAccess0DExpr(v.tok, v, "READ", 2)));
+ }
+ }
+ }
+
+ protected override void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
+
+ private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
+ {
+ int OneOrTwo = Int32.Parse(OneOrTwoString);
+ Expr expr = null;
+
+ 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));
+ expr = NoAccess3DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], OneOrTwo);
+ }
+ else
+ {
+ expr = NoAccess2DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], mt2.Arguments[0], OneOrTwo);
+ }
+ }
+ else
+ {
+ expr = NoAccess1DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], OneOrTwo);
+ }
+ }
+ else
+ {
+ expr = NoAccess0DExpr(v.tok, v, ReadOrWrite, OneOrTwo);
+ }
+ return expr;
+ }
+
+
+
+ protected override void AddReadOrWrittenOffsetIsThreadIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);
+
+ if (expr != null)
+ {
+ verifier.AddCandidateInvariant(wc, expr);
+ }
+ }
+
+ private Expr AccessOnlyAtThreadId(Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = null;
+
+ 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));
+
+ if (verifier.KernelHasIdZ() && mt.Arguments[0].Equals(verifier.GetTypeOfIdZ()) &&
+ mt2.Arguments[0].Equals(verifier.GetTypeOfIdY()) &&
+ mt3.Arguments[0].Equals(verifier.GetTypeOfIdX()))
+ {
+ expr = No3DAccessExceptAtThreadId(v, ReadOrWrite, Thread);
+ }
+
+ }
+ else
+ {
+ if (verifier.KernelHasIdY() && mt.Arguments[0].Equals(verifier.GetTypeOfIdY()) &&
+ mt2.Arguments[0].Equals(verifier.GetTypeOfIdX()))
+ {
+ expr = No2DAccessExceptAtThreadId(v, ReadOrWrite, Thread);
+ }
+ }
+ }
+ else
+ {
+ if (mt.Arguments[0].Equals(verifier.GetTypeOfIdX()))
+ {
+ expr = No1DAccessExceptAtThreadId(v, ReadOrWrite, Thread);
+ }
+ }
+ }
+ return expr;
+ }
+
+ private Expr No1DAccessExceptAtThreadId(Variable v, string ReadOrWrite, int Thread)
+ {
+ Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));
+
+ return new ForallExpr(v.tok,
+ new VariableSeq(new Variable[] { DummyX }),
+ Expr.Imp(
+ Expr.Neq(new IdentifierExpr(v.tok, DummyX), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
+ Expr.Not(
+ Expr.Select(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),
+ new IdentifierExpr(v.tok, DummyX)
+ )
+ )
+ )
+ );
+ }
+
+
+ private Expr No2DAccessExceptAtThreadId(Variable v, string ReadOrWrite, int Thread)
+ {
+ Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));
+ Variable DummyY = new LocalVariable(v.tok, new TypedIdent(v.tok, "__y", verifier.GetTypeOfIdY()));
+
+ return new ForallExpr(v.tok,
+ new VariableSeq(new Variable[] { DummyY, DummyX }),
+ Expr.Imp(
+ Expr.Or(
+ Expr.Neq(new IdentifierExpr(v.tok, DummyX), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
+ Expr.Neq(new IdentifierExpr(v.tok, DummyY), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
+ ),
+
+ Expr.Not(
+ Expr.Select(
+ Expr.Select(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),
+ new IdentifierExpr(v.tok, DummyY)
+ ),
+ new IdentifierExpr(v.tok, DummyX)
+ )
+ )
+ )
+ );
+ }
+
+ private Expr No3DAccessExceptAtThreadId(Variable v, string ReadOrWrite, int Thread)
+ {
+ Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));
+ Variable DummyY = new LocalVariable(v.tok, new TypedIdent(v.tok, "__y", verifier.GetTypeOfIdY()));
+ Variable DummyZ = new LocalVariable(v.tok, new TypedIdent(v.tok, "__z", verifier.GetTypeOfIdY()));
+
+ return new ForallExpr(v.tok,
+ new VariableSeq(new Variable[] { DummyY, DummyX }),
+ Expr.Imp(
+ Expr.Or(
+ Expr.Or(
+ Expr.Neq(new IdentifierExpr(v.tok, DummyX), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),
+ Expr.Neq(new IdentifierExpr(v.tok, DummyY), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))
+ ),
+ Expr.Neq(new IdentifierExpr(v.tok, DummyZ), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread)))
+ ),
+
+ Expr.Not(
+ Expr.Select(
+ Expr.Select(
+ Expr.Select(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),
+ new IdentifierExpr(v.tok, DummyZ)
+ ),
+ new IdentifierExpr(v.tok, DummyY)
+ ),
+ new IdentifierExpr(v.tok, DummyX)
+ )
+ )
+ )
+ );
+ }
+
+ protected override void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);
+
+ if (expr != null)
+ {
+ Proc.Requires.Add(new Requires(false, expr));
+ }
+ }
+
+ protected override void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
+ {
+ Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);
+
+ if (expr != null)
+ {
+ Proc.Ensures.Add(new Ensures(false, expr));
+ }
+ }
+
+ protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
+ }
+
+ protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs index 14472f85..e8623e3b 100644 --- a/Source/GPUVerify/WriteCollector.cs +++ b/Source/GPUVerify/WriteCollector.cs @@ -13,7 +13,7 @@ namespace GPUVerify private AccessRecord access = null;
- public WriteCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)
+ public WriteCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
: base(GlobalVariables, TileStaticVariables)
{
}
|