diff options
| author |  Unknown <afd@afd-THINK> | 2012-08-13 17:32:44 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK> | 2012-08-13 17:32:44 +0100 |
| commit | cac395ed490262542e7aca6b6cdd30f0c281d2c7 (patch) | |
| tree | 6d0ceb4b2fdbd46d098ac9b9715fba7e553374a9 | |
| parent | ae9f8b1f4e149106710b13032cfa671755b15a30 (diff) | |
Removed code related to "divided" option.
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 30 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 41 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 1 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 68 | ||||
| -rw-r--r-- | Source/GPUVerify/NoConflictingAccessOptimiser.cs | 116 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenter.cs | 1706 |
6 files changed, 779 insertions, 1183 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index f28535c2..2f9ed792 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -21,9 +21,6 @@ namespace GPUVerify public static bool Inference = false;
public static bool ArrayEqualities = false;
public static string invariantsFile = null;
- public static bool DividedArray = false;
- public static string ArrayToCheck = null;
- public static bool DividedAccesses = false;
public static bool ShowStages = false;
@@ -93,28 +90,6 @@ namespace GPUVerify break;
- case "-dividedArray":
- case "/dividedArray":
- if (hasColonArgument)
- {
- ArrayToCheck = afterColon;
- }
- DividedArray = true;
-
- break;
-
- case "-dividedAccesses":
- case "/dividedAccesses":
- DividedAccesses = true;
-
- break;
-
- case "-divided":
- case "/divided":
- DividedAccesses = true;
- DividedArray = true;
- break;
-
case "-showStages":
case "/showStages":
ShowStages = true;
@@ -181,11 +156,6 @@ namespace GPUVerify break;
}
- if (OnlyDivergence)
- {
- DividedArray = false;
- DividedAccesses = false;
- }
}
return 0;
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 68e43242..9fad81f9 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -455,47 +455,6 @@ namespace GPUVerify emitProgram(outputFilename);
-
- if (CommandLineOptions.DividedAccesses)
- {
-
- Program p = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { outputFilename + ".bpl" }), true);
- ResolutionContext rc = new ResolutionContext(null);
- p.Resolve(rc);
- p.Typecheck();
-
- Contract.Assert(p != null);
-
- Implementation impl = null;
-
- {
- GPUVerifier tempGPUV = new GPUVerifier("not_used", p, rc, 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(outputFilename);
-
- string newName = f.Directory.FullName + "\\" + "NO_CONFLICTS_" + f.Name + ".bpl";
- //File.Delete(newName);
- if (File.Exists(newName))
- {
- File.Delete(newName);
- }
- File.Move(outputFilename + ".bpl", newName);
- //Console.WriteLine("Renamed " + ouputFilename + "; no conflicting accesses (that are not already tested by other output files).");
- }
-
-
- }
-
}
private void DoMayBePowerOfTwoAnalysis()
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 4cb24f2c..47965b43 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -126,7 +126,6 @@ <Compile Include="IKernelArrayInfo.cs" />
<Compile Include="IRaceInstrumenter.cs" />
<Compile Include="Main.cs" />
- <Compile Include="NoConflictingAccessOptimiser.cs" />
<Compile Include="NonLocalAccessCollector.cs" />
<Compile Include="NonLocalAccessExtractor.cs" />
<Compile Include="KernelArrayInfoLists.cs" />
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index e5a094d5..c6600d61 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -122,7 +122,7 @@ namespace GPUVerify }
- public static IList<GPUVerifier> parseProcessOutput()
+ public static void parseProcessOutput()
{
string fn = "temp";
if (CommandLineOptions.outputFile != null)
@@ -137,72 +137,16 @@ namespace GPUVerify }
ResolutionContext rc;
Program program = parse(out rc);
- IList<GPUVerifier> result = new List<GPUVerifier>();
GPUVerifier g = new GPUVerifier(fn, program, rc, new NullRaceInstrumenter());
- if (CommandLineOptions.DividedArray)
+ if (!CommandLineOptions.OnlyDivergence)
{
- bool FoundArray = CommandLineOptions.ArrayToCheck == null;
-
- foreach (Variable v in g.KernelArrayInfo.getAllNonLocalArrays())
- {
- 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
- {
- if (CommandLineOptions.ArrayToCheck == null || CommandLineOptions.ArrayToCheck.Equals(v.Name))
- {
- FoundArray = true;
- doit("temp_" + v.Name, v, -1, -1);
- }
- }
- }
-
- if (!FoundArray)
- {
- Console.WriteLine("Did not find a non-local array named " + CommandLineOptions.ArrayToCheck);
- Environment.Exit(1);
- }
-
- }
- else
- {
- if (!CommandLineOptions.OnlyDivergence)
- {
- RaceInstrumenter ri = new RaceInstrumenter();
- ri.setVerifier(g);
- g.setRaceInstrumenter(ri);
- }
-
- g.doit();
- result.Add(g);
-
+ RaceInstrumenter ri = new RaceInstrumenter();
+ ri.setVerifier(g);
+ g.setRaceInstrumenter(ri);
}
- return result;
+ g.doit();
}
diff --git a/Source/GPUVerify/NoConflictingAccessOptimiser.cs b/Source/GPUVerify/NoConflictingAccessOptimiser.cs deleted file mode 100644 index f003a3a9..00000000 --- a/Source/GPUVerify/NoConflictingAccessOptimiser.cs +++ /dev/null @@ -1,116 +0,0 @@ -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/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs index 2e7e42d2..6d76c65e 100644 --- a/Source/GPUVerify/RaceInstrumenter.cs +++ b/Source/GPUVerify/RaceInstrumenter.cs @@ -7,1108 +7,948 @@ using System.Diagnostics.Contracts; using Microsoft.Boogie;
using Microsoft.Basetypes;
-namespace GPUVerify
-{
- class RaceInstrumenter : IRaceInstrumenter
- {
- protected GPUVerifier verifier;
-
- public IKernelArrayInfo NonLocalStateToCheck;
-
- public int onlyLog1;
- public int onlyLog2;
- public bool failedToFindSecondAccess;
- public bool addedLogWrite;
- private int logAddCount;
-
- private Dictionary<string, Procedure> logAccessProcedures = new Dictionary<string, Procedure>();
-
- public RaceInstrumenter()
- {
- onlyLog1 = -1;
- onlyLog2 = -1;
- failedToFindSecondAccess = false;
- addedLogWrite = false;
- logAddCount = 0;
- }
+namespace GPUVerify {
+ class RaceInstrumenter : IRaceInstrumenter {
+ protected GPUVerifier verifier;
+
+ public IKernelArrayInfo NonLocalStateToCheck;
+
+ public int onlyLog1;
+ public int onlyLog2;
+ public bool failedToFindSecondAccess;
+ public bool addedLogWrite;
+ private int logAddCount;
+
+ private Dictionary<string, Procedure> logAccessProcedures = new Dictionary<string, Procedure>();
+
+ public RaceInstrumenter() {
+ onlyLog1 = -1;
+ onlyLog2 = -1;
+ failedToFindSecondAccess = false;
+ addedLogWrite = false;
+ logAddCount = 0;
+ }
- public void setVerifier(GPUVerifier verifier)
- {
- this.verifier = verifier;
- NonLocalStateToCheck = new KernelArrayInfoLists();
- foreach(Variable v in verifier.KernelArrayInfo.getGlobalArrays())
- {
- NonLocalStateToCheck.getGlobalArrays().Add(v);
- }
- foreach(Variable v in verifier.KernelArrayInfo.getGroupSharedArrays())
- {
- NonLocalStateToCheck.getGroupSharedArrays().Add(v);
- }
- }
+ public void setVerifier(GPUVerifier verifier) {
+ this.verifier = verifier;
+ NonLocalStateToCheck = new KernelArrayInfoLists();
+ foreach (Variable v in verifier.KernelArrayInfo.getGlobalArrays()) {
+ NonLocalStateToCheck.getGlobalArrays().Add(v);
+ }
+ foreach (Variable v in verifier.KernelArrayInfo.getGroupSharedArrays()) {
+ NonLocalStateToCheck.getGroupSharedArrays().Add(v);
+ }
+ }
- private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v)
- {
- // Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the
- // loop then there is no point adding an invariant
- //
- // If READ_HAS_OCCURRED_v is in the modifies set, but the loop does not
- // contain a barrier, then it is almost certain that a read CAN be
- // pending at the loop head, so the invariant will not hold
- //
- // If there is a barrier in the loop body then READ_HAS_OCCURRED_v will
- // be in the modifies set, but there may not be a live read at the loop
- // head, so it is worth adding the loop invariant candidate.
- //
- // The same reasoning applies for WRITE
-
- if (verifier.ContainsBarrierCall(region))
- {
- if (verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")))
- {
- AddNoReadOrWriteCandidateInvariant(region, v, "READ");
- }
+ private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v) {
+ // Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the
+ // loop then there is no point adding an invariant
+ //
+ // If READ_HAS_OCCURRED_v is in the modifies set, but the loop does not
+ // contain a barrier, then it is almost certain that a read CAN be
+ // pending at the loop head, so the invariant will not hold
+ //
+ // If there is a barrier in the loop body then READ_HAS_OCCURRED_v will
+ // be in the modifies set, but there may not be a live read at the loop
+ // head, so it is worth adding the loop invariant candidate.
+ //
+ // The same reasoning applies for WRITE
+
+ if (verifier.ContainsBarrierCall(region)) {
+ if (verifier.ContainsNamedVariable(
+ LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ"))) {
+ AddNoReadOrWriteCandidateInvariant(region, v, "READ");
+ }
+
+ if (verifier.ContainsNamedVariable(
+ LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE"))) {
+ AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");
+ }
+ }
+ }
- if (verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE")))
- {
- AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");
- }
- }
- }
+ private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v) {
+ AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");
+ AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");
+ }
- private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v)
- {
- AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");
- AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");
- }
+ private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v) {
+ AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");
+ AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");
+ }
- private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v)
- {
- AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");
- AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");
- }
+ private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite) {
+ Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");
+ verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());
+ }
- private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");
- verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());
- }
+ public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region) {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
+ AddNoReadOrWriteCandidateInvariants(region, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");
+ AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "READ", CollectOffsetPredicates(impl, region, v, "READ"));
+ AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "WRITE", CollectOffsetPredicates(impl, region, v, "WRITE"));
+ }
+ }
- public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())
- {
- AddNoReadOrWriteCandidateInvariants(region, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");
- AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");
- AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "READ", CollectOffsetPredicates(impl, region, v, "READ"));
- AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "WRITE", CollectOffsetPredicates(impl, region, v, "WRITE"));
- }
+ private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag) {
+ Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
+ verifier.AddCandidateInvariant(region, candidate, tag);
+ }
+
+ private bool DoesNotReferTo(Expr expr, string v) {
+ FindReferencesToNamedVariableVisitor visitor = new FindReferencesToNamedVariableVisitor(v);
+ visitor.VisitExpr(expr);
+ return !visitor.found;
+ }
+
+ private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType) {
+ var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, accessType));
+ var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);
+ var offsetPreds = new List<Expr>();
+
+ foreach (var offset in GetOffsetsAccessed(region, v, accessType)) {
+ bool isConstant;
+ var def = verifier.varDefAnalyses[impl].SubstDefinitions(offset, impl.Name, out isConstant);
+ if (def == null)
+ continue;
+
+ if (isConstant) {
+ offsetPreds.Add(Expr.Eq(offsetExpr, def));
+ }
+ else {
+ var sc = StrideConstraint.FromExpr(verifier, impl, def);
+ var pred = sc.MaybeBuildPredicate(verifier, offsetExpr);
+ if (pred != null)
+ offsetPreds.Add(pred);
}
+ }
- private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)
- {
- Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
- verifier.AddCandidateInvariant(region, candidate, tag);
+ return offsetPreds;
+ }
+
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType) {
+ KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
+ if (iLessThanC.Key != null) {
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType)) {
+ if (HasFormIPlusLocalIdTimesC(e, iLessThanC, impl)) {
+ AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);
+ break;
+ }
}
- private bool DoesNotReferTo(Expr expr, string v)
- {
- FindReferencesToNamedVariableVisitor visitor = new FindReferencesToNamedVariableVisitor(v);
- visitor.VisitExpr(expr);
- return !visitor.found;
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType)) {
+ if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl)) {
+ AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);
+ break;
+ }
}
- private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType)
- {
- var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, accessType));
- var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);
- var offsetPreds = new List<Expr>();
-
- foreach (var offset in GetOffsetsAccessed(region, v, accessType))
- {
- bool isConstant;
- var def = verifier.varDefAnalyses[impl].SubstDefinitions(offset, impl.Name, out isConstant);
- if (def == null)
- continue;
-
- if (isConstant)
- {
- offsetPreds.Add(Expr.Eq(offsetExpr, def));
- }
- else
- {
- var sc = StrideConstraint.FromExpr(verifier, impl, def);
- var pred = sc.MaybeBuildPredicate(verifier, offsetExpr);
- if (pred != null)
- offsetPreds.Add(pred);
- }
- }
+ }
- return offsetPreds;
- }
- private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)
- {
- KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
- if (iLessThanC.Key != null)
- {
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if(HasFormIPlusLocalIdTimesC(e, iLessThanC, impl))
- {
- AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);
- break;
- }
- }
+ }
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl))
- {
- AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);
- break;
- }
- }
-
- }
+ private bool HasFormIPlusLocalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl) {
+ if (!(e is NAryExpr)) {
+ return false;
+ }
-
- }
+ NAryExpr nary = e as NAryExpr;
- private bool HasFormIPlusLocalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)
- {
- if (!(e is NAryExpr))
- {
- return false;
- }
+ if (!nary.Fun.FunctionName.Equals("BV32_ADD")) {
+ return false;
+ }
- NAryExpr nary = e as NAryExpr;
+ return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
+ IsLocalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
+ (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
+ IsLocalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
+ }
- if (!nary.Fun.FunctionName.Equals("BV32_ADD"))
- {
- return false;
- }
+ private bool IsLocalIdTimesConstant(Expr maybeLocalIdTimesConstant, Expr constant, Implementation impl) {
+ if (!(maybeLocalIdTimesConstant is NAryExpr)) {
+ return false;
+ }
+ NAryExpr nary = maybeLocalIdTimesConstant as NAryExpr;
+ if (!nary.Fun.FunctionName.Equals("BV32_MUL")) {
+ return false;
+ }
+
+ return
+ (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||
+ (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));
+ }
- return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
- IsLocalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
- (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
- IsLocalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
- }
- private bool IsLocalIdTimesConstant(Expr maybeLocalIdTimesConstant, Expr constant, Implementation impl)
- {
- if (!(maybeLocalIdTimesConstant is NAryExpr))
- {
- return false;
- }
- NAryExpr nary = maybeLocalIdTimesConstant as NAryExpr;
- if(!nary.Fun.FunctionName.Equals("BV32_MUL"))
- {
- return false;
- }
+ private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl) {
+ if (!(e is NAryExpr)) {
+ return false;
+ }
- return
- (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||
- (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));
- }
+ NAryExpr nary = e as NAryExpr;
+ if (!nary.Fun.FunctionName.Equals("BV32_ADD")) {
+ return false;
+ }
- private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)
- {
- if (!(e is NAryExpr))
- {
- return false;
- }
+ return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
+ IsGlobalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
+ (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
+ IsGlobalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
+ }
- NAryExpr nary = e as NAryExpr;
+ private bool IsGlobalIdTimesConstant(Expr maybeGlobalIdTimesConstant, Expr constant, Implementation impl) {
+ if (!(maybeGlobalIdTimesConstant is NAryExpr)) {
+ return false;
+ }
+ NAryExpr nary = maybeGlobalIdTimesConstant as NAryExpr;
+ if (!nary.Fun.FunctionName.Equals("BV32_MUL")) {
+ return false;
+ }
+
+ return
+ (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||
+ (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));
+ }
- if (!nary.Fun.FunctionName.Equals("BV32_ADD"))
- {
- return false;
- }
- return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
- IsGlobalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
- (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
- IsGlobalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
+ private bool SameConstant(Expr expr, Expr constant) {
+ if (constant is IdentifierExpr) {
+ IdentifierExpr identifierExpr = constant as IdentifierExpr;
+ Debug.Assert(identifierExpr.Decl is Constant);
+ return expr is IdentifierExpr && (expr as IdentifierExpr).Decl is Constant && (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Decl.Name);
+ }
+ else {
+ Debug.Assert(constant is LiteralExpr);
+ LiteralExpr literalExpr = constant as LiteralExpr;
+ if (!(expr is LiteralExpr)) {
+ return false;
+ }
+ if (!(literalExpr.Val is BvConst) || !((expr as LiteralExpr).Val is BvConst)) {
+ return false;
}
- private bool IsGlobalIdTimesConstant(Expr maybeGlobalIdTimesConstant, Expr constant, Implementation impl)
- {
- if (!(maybeGlobalIdTimesConstant is NAryExpr))
- {
- return false;
- }
- NAryExpr nary = maybeGlobalIdTimesConstant as NAryExpr;
- if (!nary.Fun.FunctionName.Equals("BV32_MUL"))
- {
- return false;
- }
+ return (literalExpr.Val as BvConst).Value.ToInt == ((expr as LiteralExpr).Val as BvConst).Value.ToInt;
+ }
+ }
- return
- (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||
- (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));
- }
+ private bool SameIdentifierExpression(Expr expr, IdentifierExpr identifierExpr) {
+ if (!(expr is IdentifierExpr)) {
+ return false;
+ }
+ return (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Name);
+ }
+ private KeyValuePair<IdentifierExpr, Expr> GetILessThanC(Expr expr) {
- private bool SameConstant(Expr expr, Expr constant)
- {
- if (constant is IdentifierExpr)
- {
- IdentifierExpr identifierExpr = constant as IdentifierExpr;
- Debug.Assert(identifierExpr.Decl is Constant);
- return expr is IdentifierExpr && (expr as IdentifierExpr).Decl is Constant && (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Decl.Name);
- }
- else
- {
- Debug.Assert(constant is LiteralExpr);
- LiteralExpr literalExpr = constant as LiteralExpr;
- if (!(expr is LiteralExpr))
- {
- return false;
- }
- if (!(literalExpr.Val is BvConst) || !((expr as LiteralExpr).Val is BvConst))
- {
- return false;
- }
+ if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool")) {
+ expr = (expr as NAryExpr).Args[0];
+ }
- return (literalExpr.Val as BvConst).Value.ToInt == ((expr as LiteralExpr).Val as BvConst).Value.ToInt;
- }
- }
+ if (!(expr is NAryExpr)) {
+ return new KeyValuePair<IdentifierExpr, Expr>(null, null);
+ }
- private bool SameIdentifierExpression(Expr expr, IdentifierExpr identifierExpr)
- {
- if (!(expr is IdentifierExpr))
- {
- return false;
- }
- return (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Name);
- }
+ NAryExpr nary = expr as NAryExpr;
- private KeyValuePair<IdentifierExpr, Expr> GetILessThanC(Expr expr)
- {
+ if (!(nary.Fun.FunctionName.Equals("BV32_C_LT") || nary.Fun.FunctionName.Equals("BV32_LT"))) {
+ return new KeyValuePair<IdentifierExpr, Expr>(null, null);
+ }
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool"))
- {
- expr = (expr as NAryExpr).Args[0];
- }
+ if (!(nary.Args[0] is IdentifierExpr)) {
+ return new KeyValuePair<IdentifierExpr, Expr>(null, null);
+ }
- if (!(expr is NAryExpr))
- {
- return new KeyValuePair<IdentifierExpr, Expr>(null, null);
- }
+ if (!IsConstant(nary.Args[1])) {
+ return new KeyValuePair<IdentifierExpr, Expr>(null, null);
+ }
- NAryExpr nary = expr as NAryExpr;
+ return new KeyValuePair<IdentifierExpr, Expr>(nary.Args[0] as IdentifierExpr, nary.Args[1]);
- if (!(nary.Fun.FunctionName.Equals("BV32_C_LT") || nary.Fun.FunctionName.Equals("BV32_LT")))
- {
- return new KeyValuePair<IdentifierExpr, Expr>(null, null);
- }
+ }
- if (!(nary.Args[0] is IdentifierExpr))
- {
- return new KeyValuePair<IdentifierExpr, Expr>(null, null);
- }
+ private static bool IsConstant(Expr e) {
+ return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);
+ }
- if (!IsConstant(nary.Args[1]))
- {
- return new KeyValuePair<IdentifierExpr, Expr>(null, null);
- }
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v) {
+ AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);
+ AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);
+ }
- return new KeyValuePair<IdentifierExpr, Expr>(nary.Args[0] as IdentifierExpr, nary.Args[1]);
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v) {
+ AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);
+ AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
+ }
- }
+ public void AddKernelPrecondition() {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
+ AddRequiresNoPendingAccess(v);
- private static bool IsConstant(Expr e)
- {
- return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);
+ if (!verifier.ArrayModelledAdversarially(v)) {
+ IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
+ IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
+ verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));
}
+ }
+ }
- private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)
- {
- AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);
- AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);
- }
+ public bool AddRaceCheckingInstrumentation() {
- private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v)
- {
- AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);
- AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
- }
+ if (onlyLog1 != -1) {
+ addedLogWrite = false;
+ failedToFindSecondAccess = true;
+ }
+ else {
+ addedLogWrite = true;
+ failedToFindSecondAccess = false;
+ }
- public void AddKernelPrecondition()
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())
- {
- AddRequiresNoPendingAccess(v);
-
- if (!verifier.ArrayModelledAdversarially(v))
- {
- IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
- IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
- verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));
- }
- }
+ foreach (Declaration d in verifier.Program.TopLevelDeclarations) {
+ if (d is Implementation) {
+ AddRaceCheckCalls(d as Implementation);
}
+ }
- public bool AddRaceCheckingInstrumentation()
- {
+ if (failedToFindSecondAccess || !addedLogWrite)
+ return false;
- if (onlyLog1 != -1)
- {
- addedLogWrite = false;
- failedToFindSecondAccess = true;
- }
- else
- {
- addedLogWrite = true;
- failedToFindSecondAccess = false;
- }
+ return true;
- foreach (Declaration d in verifier.Program.TopLevelDeclarations)
- {
- if (d is Implementation)
- {
- AddRaceCheckCalls(d as Implementation);
- }
- }
+ }
- if (failedToFindSecondAccess || !addedLogWrite)
- return false;
+ private void AddRaceCheckingDecsAndProcsForVar(Variable v) {
+ AddLogRaceDeclarations(v, "READ");
+ AddLogRaceDeclarations(v, "WRITE");
+ AddLogAccessProcedure(v, "READ");
+ AddLogAccessProcedure(v, "WRITE");
- return true;
+ }
- }
+ private StmtList AddRaceCheckCalls(StmtList stmtList) {
+ Contract.Requires(stmtList != null);
- private void AddRaceCheckingDecsAndProcsForVar(Variable v)
- {
- AddLogRaceDeclarations(v, "READ");
- AddLogRaceDeclarations(v, "WRITE");
- AddLogAccessProcedure(v, "READ");
- AddLogAccessProcedure(v, "WRITE");
+ StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
- }
-
- private StmtList AddRaceCheckCalls(StmtList stmtList)
- {
- Contract.Requires(stmtList != null);
+ foreach (BigBlock bodyBlock in stmtList.BigBlocks) {
+ result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));
+ }
+ return result;
+ }
- StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
+ private Block AddRaceCheckCalls(Block b) {
+ b.Cmds = AddRaceCheckCalls(b.Cmds);
+ return b;
+ }
- foreach (BigBlock bodyBlock in stmtList.BigBlocks)
- {
- result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));
- }
- return result;
- }
+ private void AddRaceCheckCalls(Implementation impl) {
+ if (CommandLineOptions.Unstructured)
+ impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
+ else
+ impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
+ }
- private Block AddRaceCheckCalls(Block b)
- {
- b.Cmds = AddRaceCheckCalls(b.Cmds);
- return b;
- }
+ private bool shouldAddLogCallAndIncr() {
+ Contract.Assert(onlyLog1 >= -1);
+ int oldLogAddCount = logAddCount;
+ ++logAddCount;
- private void AddRaceCheckCalls(Implementation impl)
- {
- if (CommandLineOptions.Unstructured)
- impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
- else
- impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
- }
+ if (onlyLog1 == -1) {
+ return true;
+ }
- private bool shouldAddLogCallAndIncr()
- {
- Contract.Assert(onlyLog1 >= -1);
- int oldLogAddCount = logAddCount;
- ++logAddCount;
+ if (onlyLog1 + onlyLog2 == oldLogAddCount) {
+ failedToFindSecondAccess = false;
+ return true;
+ }
- if (onlyLog1 == -1)
- {
- return true;
- }
+ if (onlyLog1 == oldLogAddCount) {
+ return true;
+ }
- if(onlyLog1 + onlyLog2 == oldLogAddCount)
- {
- failedToFindSecondAccess = false;
- return true;
- }
+ return false;
+ }
+
+ private CmdSeq AddRaceCheckCalls(CmdSeq cs) {
+ var result = new CmdSeq();
+ foreach (Cmd c in cs) {
+ result.Add(c);
+ if (c is AssignCmd) {
+ AssignCmd assign = c as AssignCmd;
+
+ ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
+ foreach (var rhs in assign.Rhss)
+ rc.Visit(rhs);
+ if (rc.accesses.Count > 0) {
+ foreach (AccessRecord ar in rc.accesses) {
+ 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);
+ }
- if (onlyLog1 == oldLogAddCount)
- {
- return true;
+ Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
+
+ CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
+
+ logAccessCallCmd.Proc = logProcedure;
+
+ result.Add(logAccessCallCmd);
+
+ }
}
+ }
- return false;
- }
+ foreach (var lhs in assign.Lhss) {
+ WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
+ wc.Visit(lhs);
+ if (wc.GetAccess() != null) {
+ AccessRecord ar = wc.GetAccess();
+
+ if (shouldAddLogCallAndIncr()) {
- private CmdSeq AddRaceCheckCalls(CmdSeq cs)
- {
- var result = new CmdSeq();
- foreach (Cmd c in cs)
- {
- result.Add(c);
- if (c is AssignCmd)
- {
- AssignCmd assign = c as AssignCmd;
-
- ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
- foreach (var rhs in assign.Rhss)
- rc.Visit(rhs);
- if (rc.accesses.Count > 0)
- {
- foreach (AccessRecord ar in rc.accesses)
- {
- 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);
- }
-
- Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
-
- CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
-
- logAccessCallCmd.Proc = logProcedure;
-
- result.Add(logAccessCallCmd);
-
- }
- }
- }
-
- foreach (var lhs in assign.Lhss)
- {
- WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
- 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);
- }
-
- Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
-
- CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
-
- logAccessCallCmd.Proc = logProcedure;
-
- result.Add(logAccessCallCmd);
-
- addedLogWrite = true;
-
- }
- }
- }
+ 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);
}
- }
- return result;
- }
- private BigBlock AddRaceCheckCalls(BigBlock bb)
- {
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, AddRaceCheckCalls(bb.simpleCmds), null, bb.tc);
+ Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
- 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);
- }
+ CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
- return result;
- }
+ logAccessCallCmd.Proc = logProcedure;
+
+ result.Add(logAccessCallCmd);
+
+ addedLogWrite = true;
- private Procedure GetLogAccessProcedure(IToken tok, string name)
- {
- if (logAccessProcedures.ContainsKey(name))
- {
- return logAccessProcedures[name];
+ }
}
- Procedure newProcedure = new Procedure(tok, name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
- logAccessProcedures[name] = newProcedure;
- return newProcedure;
+ }
}
+ }
+ return result;
+ }
+ private BigBlock AddRaceCheckCalls(BigBlock bb) {
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, AddRaceCheckCalls(bb.simpleCmds), null, bb.tc);
+
+ 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;
+ }
- public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
- {
- BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
- if (Thread == 2)
- {
- return result;
- }
+ private Procedure GetLogAccessProcedure(IToken tok, string name) {
+ if (logAccessProcedures.ContainsKey(name)) {
+ return logAccessProcedures[name];
+ }
+ Procedure newProcedure = new Procedure(tok, name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ logAccessProcedures[name] = newProcedure;
+ return newProcedure;
+ }
- Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
- new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));
- Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
- new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));
- if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v))
- {
- ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
- ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
- }
+ public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) {
+ BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
+ if (Thread == 2) {
+ return result;
+ }
- result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));
- result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));
- return result;
- }
+ Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
+ new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));
+ Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
+ new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));
- protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)
- {
- VariableSeq inParams = new VariableSeq();
+ if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {
+ ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
+ ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
+ }
- Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));
+ result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));
+ result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));
+ return result;
+ }
- Debug.Assert(v.TypedIdent.Type is MapType);
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
- Debug.Assert(!(mt.Result is MapType));
+ protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite) {
+ VariableSeq inParams = new VariableSeq();
- inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
- inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
+ Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));
- inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
- inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+ Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
+ Debug.Assert(!(mt.Result is MapType));
- string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;
+ inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
+ inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
- Procedure result = GetLogAccessProcedure(v.tok, LogProcedureName);
+ inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
+ inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
- result.InParams = inParams;
+ string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;
- result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+ Procedure result = GetLogAccessProcedure(v.tok, LogProcedureName);
- return result;
- }
+ result.InParams = inParams;
- public void AddRaceCheckingCandidateRequires(Procedure Proc)
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())
- {
- AddNoReadOrWriteCandidateRequires(Proc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
- }
+ result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
- DoHoudiniPointerAnalysis(Proc);
+ return result;
+ }
- }
+ public void AddRaceCheckingCandidateRequires(Procedure Proc) {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
+ AddNoReadOrWriteCandidateRequires(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
+ }
- private void DoHoudiniPointerAnalysis(Procedure Proc)
- {
- HashSet<string> alreadyConsidered = new HashSet<string>();
+ DoHoudiniPointerAnalysis(Proc);
- foreach (Variable v in Proc.InParams)
- {
- string strippedVarName = GPUVerifier.StripThreadIdentifier(v.Name);
- if (alreadyConsidered.Contains(strippedVarName))
- {
- continue;
- }
- alreadyConsidered.Add(strippedVarName);
- if (v.TypedIdent.Type is CtorType)
- {
- CtorType ct = v.TypedIdent.Type as CtorType;
- if (ct.Decl.Name.Equals("ptr"))
- {
- foreach (var arrayCollection in new ICollection<Variable>[] {
- verifier.KernelArrayInfo.getGlobalArrays(), verifier.KernelArrayInfo.getGroupSharedArrays(),
- verifier.KernelArrayInfo.getPrivateArrays() })
- {
- if (arrayCollection.Count == 0)
- {
- continue;
- }
-
- // This will need to be adapted to work with uniformity analysis
- foreach (string thread in new string[] { "1", "2" })
- {
- Expr DisjunctionOverPointerSet = null;
- foreach (var array in arrayCollection)
- {
- Expr PointerSetDisjunct = Expr.Eq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array));
- DisjunctionOverPointerSet = (DisjunctionOverPointerSet == null ? PointerSetDisjunct : Expr.Or(DisjunctionOverPointerSet, PointerSetDisjunct));
- verifier.AddCandidateRequires(Proc,
- Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
- Expr.Neq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array))));
- }
- Debug.Assert(DisjunctionOverPointerSet != null);
- verifier.AddCandidateRequires(Proc,
- Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
- DisjunctionOverPointerSet));
- verifier.AddCandidateRequires(Proc,
- Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
- Expr.Eq(MakePtrOffsetExpr(v, strippedVarName, thread), GPUVerifier.ZeroBV())));
- }
- }
- }
- }
- }
- }
+ }
- private static IdentifierExpr MakeArrayIdExpr(Variable array)
- {
- return new IdentifierExpr(Token.NoToken, "$arrayId" + array.Name, null);
- }
+ private void DoHoudiniPointerAnalysis(Procedure Proc) {
+ HashSet<string> alreadyConsidered = new HashSet<string>();
- private static NAryExpr MakePtrBaseExpr(Variable v, string strippedVarName, string thread)
- {
- return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "base#MKPTR", v.TypedIdent.Type)),
- new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));
+ foreach (Variable v in Proc.InParams) {
+ string strippedVarName = GPUVerifier.StripThreadIdentifier(v.Name);
+ if (alreadyConsidered.Contains(strippedVarName)) {
+ continue;
}
+ alreadyConsidered.Add(strippedVarName);
+ if (v.TypedIdent.Type is CtorType) {
+ CtorType ct = v.TypedIdent.Type as CtorType;
+ if (ct.Decl.Name.Equals("ptr")) {
+ foreach (var arrayCollection in new ICollection<Variable>[] {
+ verifier.KernelArrayInfo.getGlobalArrays(), verifier.KernelArrayInfo.getGroupSharedArrays(),
+ verifier.KernelArrayInfo.getPrivateArrays() }) {
+ if (arrayCollection.Count == 0) {
+ continue;
+ }
+
+ // This will need to be adapted to work with uniformity analysis
+ foreach (string thread in new string[] { "1", "2" }) {
+ Expr DisjunctionOverPointerSet = null;
+ foreach (var array in arrayCollection) {
+ Expr PointerSetDisjunct = Expr.Eq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array));
+ DisjunctionOverPointerSet = (DisjunctionOverPointerSet == null ? PointerSetDisjunct : Expr.Or(DisjunctionOverPointerSet, PointerSetDisjunct));
+ verifier.AddCandidateRequires(Proc,
+ Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
+ Expr.Neq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array))));
+ }
+ Debug.Assert(DisjunctionOverPointerSet != null);
+ verifier.AddCandidateRequires(Proc,
+ Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
+ DisjunctionOverPointerSet));
+ verifier.AddCandidateRequires(Proc,
+ Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),
+ Expr.Eq(MakePtrOffsetExpr(v, strippedVarName, thread), GPUVerifier.ZeroBV())));
+ }
+ }
+ }
+ }
+ }
+ }
- private static NAryExpr MakePtrOffsetExpr(Variable v, string strippedVarName, string thread)
- {
- return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "offset#MKPTR", v.TypedIdent.Type)),
- new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));
- }
+ private static IdentifierExpr MakeArrayIdExpr(Variable array) {
+ return new IdentifierExpr(Token.NoToken, "$arrayId" + array.Name, null);
+ }
- public void AddRaceCheckingCandidateEnsures(Procedure Proc)
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())
- {
- AddNoReadOrWriteCandidateEnsures(Proc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
- }
- }
+ private static NAryExpr MakePtrBaseExpr(Variable v, string strippedVarName, string thread) {
+ return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "base#MKPTR", v.TypedIdent.Type)),
+ new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));
+ }
- private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
- }
+ private static NAryExpr MakePtrOffsetExpr(Variable v, string strippedVarName, string thread) {
+ return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "offset#MKPTR", v.TypedIdent.Type)),
+ new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));
+ }
- private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
- }
+ public void AddRaceCheckingCandidateEnsures(Procedure Proc) {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
+ AddNoReadOrWriteCandidateEnsures(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
+ }
+ }
- private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType)
- {
- HashSet<Expr> result = new HashSet<Expr>();
-
- foreach (Cmd c in region.Cmds())
- {
- if (c is CallCmd)
- {
- CallCmd call = c as CallCmd;
-
- if (call.callee == "_LOG_" + AccessType + "_" + v.Name)
- {
- // Ins[0] is thread 1's predicate,
- // Ins[1] is the offset to be read
- // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),
- // we are looking for the second parameter to this BV32_ADD
- Expr offset = call.Ins[1];
- if (offset is NAryExpr)
- {
- var nExpr = (NAryExpr)offset;
- if (nExpr.Fun.FunctionName == "BV32_ADD" &&
- nExpr.Args[0] is NAryExpr)
- {
- var n0Expr = (NAryExpr)nExpr.Args[0];
- if (n0Expr.Fun.FunctionName.StartsWith("offset#"))
- offset = nExpr.Args[1];
- }
- }
- result.Add(offset);
- }
+ private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo) {
+ verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
- }
+ private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo) {
+ verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
- }
+ private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType) {
+ HashSet<Expr> result = new HashSet<Expr>();
- return result;
- }
+ foreach (Cmd c in region.Cmds()) {
+ if (c is CallCmd) {
+ CallCmd call = c as CallCmd;
- public void AddRaceCheckingDeclarations()
- {
- foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())
- {
- AddRaceCheckingDecsAndProcsForVar(v);
+ if (call.callee == "_LOG_" + AccessType + "_" + v.Name) {
+ // Ins[0] is thread 1's predicate,
+ // Ins[1] is the offset to be read
+ // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),
+ // we are looking for the second parameter to this BV32_ADD
+ Expr offset = call.Ins[1];
+ if (offset is NAryExpr) {
+ var nExpr = (NAryExpr)offset;
+ if (nExpr.Fun.FunctionName == "BV32_ADD" &&
+ nExpr.Args[0] is NAryExpr) {
+ var n0Expr = (NAryExpr)nExpr.Args[0];
+ if (n0Expr.Fun.FunctionName.StartsWith("offset#"))
+ offset = nExpr.Args[1];
+ }
}
+ result.Add(offset);
+ }
+
}
- protected void AddLogAccessProcedure(Variable v, string Access)
- {
- Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);
-
- Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);
- Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetVariable(v, Access);
-
- Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));
-
- Debug.Assert(v.TypedIdent.Type is MapType);
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
- Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
- Debug.Assert(!(mt.Result is MapType));
-
- VariableSeq locals = new VariableSeq();
- Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));
- 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(VariableForThread(1, AccessHasOccurredVariable),
- Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));
- simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable),
- Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)),
- new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));
-
- if (Access.Equals("READ"))
- {
- // Check read by thread 2 does not conflict with write by thread 1
- Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
- Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");
- Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
- WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
- WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),
- new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
- if (!verifier.ArrayModelledAdversarially(v))
- {
- WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
- ));
- }
+ }
- if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))
- {
- WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());
- }
+ return result;
+ }
- WriteReadGuard = Expr.Not(WriteReadGuard);
- simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard,
- new QKeyValue(Token.NoToken, "write_read_race", new List<object>(new object[] { }), null)
- ));
- }
- else
- {
- Debug.Assert(Access.Equals("WRITE"));
-
- // Check write by thread 2 does not conflict with write by thread 1
- Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
- Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");
-
- Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
- WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
- WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),
- new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
- if (!verifier.ArrayModelledAdversarially(v))
- {
- WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
- ));
- }
+ public void AddRaceCheckingDeclarations() {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
+ AddRaceCheckingDecsAndProcsForVar(v);
+ }
+ }
- if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))
- {
- WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());
- }
+ protected void AddLogAccessProcedure(Variable v, string Access) {
+ Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);
- WriteWriteGuard = Expr.Not(WriteWriteGuard);
- simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard,
- new QKeyValue(Token.NoToken, "write_write_race", new List<object>(new object[] { }), null)
- ));
-
- // Check write by thread 2 does not conflict with read by thread 1
- Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");
- Variable ReadOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "READ");
-
- Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
- ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));
- ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)),
- new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
- if (!verifier.ArrayModelledAdversarially(v))
- {
- ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
- ));
- }
+ Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);
+ Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetVariable(v, Access);
- if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))
- {
- ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());
- }
+ Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));
- ReadWriteGuard = Expr.Not(ReadWriteGuard);
- simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard,
- new QKeyValue(Token.NoToken, "read_write_race", new List<object>(new object[] { }), null)
- ));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+ Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
+ Debug.Assert(!(mt.Result is MapType));
- }
+ VariableSeq locals = new VariableSeq();
+ Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));
+ locals.Add(TrackVariable);
- bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));
+ List<BigBlock> bigblocks = new List<BigBlock>();
- LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));
- LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));
+ CmdSeq simpleCmds = new CmdSeq();
- Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));
- LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+ simpleCmds.Add(new HavocCmd(v.tok, new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, TrackVariable) })));
- LogAccessImplementation.Proc = LogAccessProcedure;
+ simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable),
+ Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));
+ simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable),
+ Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)),
+ new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));
- verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);
- verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);
+ if (Access.Equals("READ")) {
+ // Check read by thread 2 does not conflict with write by thread 1
+ Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
+ Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");
+ Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
+ WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v)) {
+ WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ ));
}
- private Variable VariableForThread(int thread, Variable v)
- {
- return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);
+ if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
+ WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());
}
- protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
- {
- verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);
+ WriteReadGuard = Expr.Not(WriteReadGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard,
+ new QKeyValue(Token.NoToken, "write_read_race", new List<object>(new object[] { }), null)
+ ));
+ }
+ else {
+ Debug.Assert(Access.Equals("WRITE"));
- Debug.Assert(v.TypedIdent.Type is MapType);
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
+ // Check write by thread 2 does not conflict with write by thread 1
+ Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
+ Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");
- verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);
-
- }
-
-
- 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);
+ Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
+ WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v)) {
+ WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
+ ));
}
- private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType)
- {
- Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));
- Debug.Assert(v.TypedIdent.Type is MapType);
- MapType mt = v.TypedIdent.Type as MapType;
- Debug.Assert(mt.Arguments.Length == 1);
-
- result = Expr.Select(result,
- new Expr[] { offsetExpr });
- Debug.Assert(!(mt.Result is MapType));
- return result;
+ if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
+ WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());
}
- protected void AddRequiresNoPendingAccess(Variable v)
- {
- IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));
- IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));
+ WriteWriteGuard = Expr.Not(WriteWriteGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard,
+ new QKeyValue(Token.NoToken, "write_write_race", new List<object>(new object[] { }), null)
+ ));
- verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));
+ // Check write by thread 2 does not conflict with read by thread 1
+ Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");
+ Variable ReadOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "READ");
+
+ Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));
+ ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v)) {
+ ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ ));
}
- protected Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Variable ReadOrWriteHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
- ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
- ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;
- Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));
- return expr;
+ if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
+ ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());
}
+ ReadWriteGuard = Expr.Not(ReadWriteGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard,
+ new QKeyValue(Token.NoToken, "read_write_race", new List<object>(new object[] { }), null)
+ ));
- protected void AddOffsetsSatisfyPredicatesCandidateInvariant(IRegion region, Variable v, string ReadOrWrite, List<Expr> preds)
- {
- if (preds.Count != 0)
- {
- Expr expr = AccessedOffsetsSatisfyPredicatesExpr(v, preds, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offsets satisfy predicates");
- }
- }
+ }
- private Expr AccessedOffsetsSatisfyPredicatesExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {
- return Expr.Imp(
- new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
- offsets.Aggregate(Expr.Or));
- }
+ bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));
- private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = null;
- if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX()))
- {
- expr = Expr.Imp(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
- }
- return expr;
- }
+ LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));
+ LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));
- private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = null;
- if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX()))
- {
- expr = Expr.Imp(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
- Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))),
- GlobalIdExpr("X", Thread)
- )
- );
- }
- return expr;
- }
+ Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));
+ LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
- private Expr GlobalIdExpr(string dimension, int Thread)
- {
- return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);
- }
+ LogAccessImplementation.Proc = LogAccessProcedure;
- protected void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
- {
- Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region,
- expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");
- }
+ verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);
+ verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);
+ }
- private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread)
- {
- Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr,
- new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));
+ private Variable VariableForThread(int thread, Variable v) {
+ return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);
+ }
- Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
- new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);
+ protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite) {
+ verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);
- Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
- Expr AccessedOffsetLtCTimesLocalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);
+ verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);
- return Expr.Imp(
- AccessHasOccurred(v, ReadOrWrite, Thread),
- Expr.And(CTimesLocalIdLeqAccessedOffset, AccessedOffsetLtCTimesLocalIdPlusC));
- }
+ }
- private static IdentifierExpr AccessHasOccurred(Variable v, string ReadOrWrite, int Thread)
- {
- return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite)));
- }
- private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread)
- {
- return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite)));
- }
+ 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 void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
- {
- Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region,
- expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");
- }
+ private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType) {
+ Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
- private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread)
- {
- Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,
- GlobalIdExpr("X", Thread));
+ result = Expr.Select(result,
+ new Expr[] { offsetExpr });
+ Debug.Assert(!(mt.Result is MapType));
+ return result;
+ }
- Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
- GlobalIdExpr("X", Thread)), constant.Clone() as Expr);
+ protected void AddRequiresNoPendingAccess(Variable v) {
+ IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));
+ IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));
- Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));
+ verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));
+ }
- Expr AccessedOffsetLtCTimesGlobalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);
+ protected Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo) {
+ Variable ReadOrWriteHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
+ ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
+ ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;
+ Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));
+ return expr;
+ }
- Expr implication = Expr.Imp(
- AccessHasOccurred(v, ReadOrWrite, Thread),
- Expr.And(CTimesGlobalIdLeqAccessedOffset, AccessedOffsetLtCTimesGlobalIdPlusC));
- return implication;
- }
- protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
- if (expr != null)
- {
- verifier.AddCandidateRequires(Proc, expr);
- }
- }
+ protected void AddOffsetsSatisfyPredicatesCandidateInvariant(IRegion region, Variable v, string ReadOrWrite, List<Expr> preds) {
+ if (preds.Count != 0) {
+ Expr expr = AccessedOffsetsSatisfyPredicatesExpr(v, preds, ReadOrWrite, 1);
+ verifier.AddCandidateInvariant(region, expr, "accessed offsets satisfy predicates");
+ }
+ }
- protected void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
- if (expr != null)
- {
- verifier.AddCandidateEnsures(Proc, expr);
- }
- }
+ private Expr AccessedOffsetsSatisfyPredicatesExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {
+ return Expr.Imp(
+ new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
+ offsets.Aggregate(Expr.Or));
+ }
+ private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread) {
+ Expr expr = null;
+ if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX())) {
+ expr = Expr.Imp(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
+ }
+ return expr;
+ }
+ private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread) {
+ Expr expr = null;
+ if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX())) {
+ expr = Expr.Imp(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
+ Expr.Eq(
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))),
+ GlobalIdExpr("X", Thread)
+ )
+ );
+ }
+ return expr;
+ }
+ private Expr GlobalIdExpr(string dimension, int Thread) {
+ return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);
}
+ protected void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite) {
+ Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
+ verifier.AddCandidateInvariant(region,
+ expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");
+ }
+ private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread) {
+ Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr,
+ new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));
- class FindReferencesToNamedVariableVisitor : StandardVisitor
- {
- internal bool found = false;
- private string name;
+ Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
+ new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);
- internal FindReferencesToNamedVariableVisitor(string name)
- {
- this.name = name;
- }
+ Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));
- public override Variable VisitVariable(Variable node)
- {
- if (GPUVerifier.StripThreadIdentifier(node.Name).Equals(name))
- {
- found = true;
- }
- return base.VisitVariable(node);
- }
+ Expr AccessedOffsetLtCTimesLocalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);
+
+ return Expr.Imp(
+ AccessHasOccurred(v, ReadOrWrite, Thread),
+ Expr.And(CTimesLocalIdLeqAccessedOffset, AccessedOffsetLtCTimesLocalIdPlusC));
+ }
+
+ private static IdentifierExpr AccessHasOccurred(Variable v, string ReadOrWrite, int Thread) {
+ return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite)));
+ }
+
+ private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread) {
+ return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite)));
+ }
+
+ protected void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite) {
+ Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);
+ verifier.AddCandidateInvariant(region,
+ expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");
+ }
+
+ private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread) {
+ Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,
+ GlobalIdExpr("X", Thread));
+
+ Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
+ GlobalIdExpr("X", Thread)), constant.Clone() as Expr);
+
+ Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));
+
+ Expr AccessedOffsetLtCTimesGlobalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);
+
+ Expr implication = Expr.Imp(
+ AccessHasOccurred(v, ReadOrWrite, Thread),
+ Expr.And(CTimesGlobalIdLeqAccessedOffset, AccessedOffsetLtCTimesGlobalIdPlusC));
+ return implication;
+ }
+
+ protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {
+ Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null) {
+ verifier.AddCandidateRequires(Proc, expr);
+ }
+ }
+
+ protected void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {
+ Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
+ if (expr != null) {
+ verifier.AddCandidateEnsures(Proc, expr);
+ }
+ }
+
+
+
+ }
+
+
+
+ class FindReferencesToNamedVariableVisitor : StandardVisitor {
+ internal bool found = false;
+ private string name;
+
+ internal FindReferencesToNamedVariableVisitor(string name) {
+ this.name = name;
+ }
+
+ public override Variable VisitVariable(Variable node) {
+ if (GPUVerifier.StripThreadIdentifier(node.Name).Equals(name)) {
+ found = true;
+ }
+ return base.VisitVariable(node);
}
+ }
|