summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-07-03 01:15:07 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-07-03 01:15:07 -0700
commitfee0fd863eb338d310baecebb0e92dba0bb74ca2 (patch)
treefdbabc52dcc83c19c80312b41b26be5c6333d452 /Source/GPUVerify
parentf5b08b01bd06a4ce88f6cc28f30eb180b45d1419 (diff)
parent8505b37ece6701ac653e8fb856a78eaafefce577 (diff)
Merge
Diffstat (limited to 'Source/GPUVerify')
-rw-r--r--Source/GPUVerify/CrossThreadInvariantProcessor.cs44
-rw-r--r--Source/GPUVerify/GPUVerifier.cs12
-rw-r--r--Source/GPUVerify/RaceInstrumenter.cs1042
-rw-r--r--Source/GPUVerify/ReducedStrengthAnalysis.cs166
-rw-r--r--Source/GPUVerify/StrideConstraint.cs141
5 files changed, 1387 insertions, 18 deletions
diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
index 4d215f24..3d64f8dc 100644
--- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs
+++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
@@ -43,7 +43,7 @@ namespace GPUVerify
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
- if (call.Func.Name.Equals("__at_most_one"))
+ if (call.Func.Name.Equals("__exclusive"))
{
return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName)
@@ -85,11 +85,36 @@ namespace GPUVerify
}
}
+ internal void ProcessCrossThreadInvariants(List<Block> blocks)
+ {
+ foreach (Block b in blocks)
+ {
+ b.Cmds = ProcessCrossThreadInvariants(b.Cmds);
+ }
+ }
+
private void ProcessCrossThreadInvariants(BigBlock bb)
{
+ bb.simpleCmds = ProcessCrossThreadInvariants(bb.simpleCmds);
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd whileCmd = bb.ec as WhileCmd;
+ List<PredicateCmd> newInvariants = new List<PredicateCmd>();
+ foreach (PredicateCmd p in whileCmd.Invariants)
+ {
+ newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
+ }
+ whileCmd.Invariants = newInvariants;
+ ProcessCrossThreadInvariants(whileCmd.Body);
+ }
+ }
+
+ private CmdSeq ProcessCrossThreadInvariants(CmdSeq cmds)
+ {
CmdSeq newCommands = new CmdSeq();
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in cmds)
{
if (c is AssertCmd)
{
@@ -104,20 +129,7 @@ namespace GPUVerify
newCommands.Add(c);
}
}
-
- bb.simpleCmds = newCommands;
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd whileCmd = bb.ec as WhileCmd;
- List<PredicateCmd> newInvariants = new List<PredicateCmd>();
- foreach (PredicateCmd p in whileCmd.Invariants)
- {
- newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
- }
- whileCmd.Invariants = newInvariants;
- ProcessCrossThreadInvariants(whileCmd.Body);
- }
+ return newCommands;
}
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 932b9f1f..79a73a29 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -633,8 +633,16 @@ namespace GPUVerify
}
if (d is Implementation)
{
- Implementation i = d as Implementation;
- new CrossThreadInvariantProcessor(this, i.Name).ProcessCrossThreadInvariants(i.StructuredStmts);
+ Implementation impl = d as Implementation;
+
+ if (CommandLineOptions.Unstructured)
+ {
+ new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.Blocks);
+ }
+ else
+ {
+ new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.StructuredStmts);
+ }
}
}
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
new file mode 100644
index 00000000..620f7d1a
--- /dev/null
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -0,0 +1,1042 @@
+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 RaceInstrumenter : IRaceInstrumenter
+ {
+ protected GPUVerifier verifier;
+
+ public INonLocalState 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 NonLocalStateLists();
+ foreach(Variable v in verifier.NonLocalState.getGlobalVariables())
+ {
+ NonLocalStateToCheck.getGlobalVariables().Add(v);
+ }
+ foreach(Variable v in verifier.NonLocalState.getGroupSharedVariables())
+ {
+ NonLocalStateToCheck.getGroupSharedVariables().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");
+ }
+
+ 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 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());
+ }
+
+ public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)
+ {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
+ {
+ 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.MakeOffsetXVariable(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;
+
+ if (!nary.Fun.FunctionName.Equals("BV32_ADD"))
+ {
+ return false;
+ }
+
+ 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;
+ }
+
+ 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));
+ }
+
+
+ private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)
+ {
+ if (!(e is NAryExpr))
+ {
+ return false;
+ }
+
+ NAryExpr nary = e as NAryExpr;
+
+ 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 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));
+ }
+
+
+ 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;
+ }
+
+ return (literalExpr.Val as BvConst).Value.ToInt == ((expr as LiteralExpr).Val as BvConst).Value.ToInt;
+ }
+ }
+
+ 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)
+ {
+
+ if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool"))
+ {
+ expr = (expr as NAryExpr).Args[0];
+ }
+
+ if (!(expr is NAryExpr))
+ {
+ return new KeyValuePair<IdentifierExpr, Expr>(null, null);
+ }
+
+ NAryExpr nary = expr as NAryExpr;
+
+ 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);
+ }
+
+ if (!IsConstant(nary.Args[1]))
+ {
+ return new KeyValuePair<IdentifierExpr, Expr>(null, null);
+ }
+
+ return new KeyValuePair<IdentifierExpr, Expr>(nary.Args[0] as IdentifierExpr, nary.Args[1]);
+
+ }
+
+ private static bool IsConstant(Expr e)
+ {
+ return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);
+ }
+
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)
+ {
+ AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);
+ AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 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.getAllNonLocalVariables())
+ {
+ 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)));
+ }
+ }
+ }
+
+ public bool AddRaceCheckingInstrumentation()
+ {
+
+ if (onlyLog1 != -1)
+ {
+ addedLogWrite = false;
+ failedToFindSecondAccess = true;
+ }
+ else
+ {
+ addedLogWrite = true;
+ failedToFindSecondAccess = false;
+ }
+
+ foreach (Declaration d in verifier.Program.TopLevelDeclarations)
+ {
+ if (d is Implementation)
+ {
+ AddRaceCheckCalls(d as Implementation);
+ }
+ }
+
+ if (failedToFindSecondAccess || !addedLogWrite)
+ return false;
+
+ 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 Block AddRaceCheckCalls(Block b)
+ {
+ b.Cmds = AddRaceCheckCalls(b.Cmds);
+ return b;
+ }
+
+ private void AddRaceCheckCalls(Implementation impl)
+ {
+ if (CommandLineOptions.Unstructured)
+ impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
+ else
+ 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 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;
+
+ }
+ }
+ }
+ }
+ }
+ 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;
+ }
+
+ 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;
+ }
+
+
+ public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
+ {
+ BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
+ if (Thread == 2)
+ {
+ 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"))));
+
+ if (CommandLineOptions.InterGroupRaceChecking && verifier.NonLocalState.getGlobalVariables().Contains(v))
+ {
+ ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
+ ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
+ }
+
+ result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));
+ result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));
+ return result;
+ }
+
+ protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)
+ {
+ VariableSeq inParams = new VariableSeq();
+
+ 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));
+
+ inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
+ inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
+
+ inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));
+ inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));
+
+ string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;
+
+ Procedure result = GetLogAccessProcedure(v.tok, LogProcedureName);
+
+ result.InParams = inParams;
+
+ result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });
+
+ return result;
+ }
+
+ public void AddRaceCheckingCandidateRequires(Procedure Proc)
+ {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
+ {
+ AddNoReadOrWriteCandidateRequires(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
+ }
+ }
+
+ public void AddRaceCheckingCandidateEnsures(Procedure Proc)
+ {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
+ {
+ AddNoReadOrWriteCandidateEnsures(Proc, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
+ }
+ }
+
+ 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>();
+
+ 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);
+ }
+
+ }
+
+ }
+
+ return result;
+ }
+
+ public void AddRaceCheckingDeclarations()
+ {
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
+ {
+ AddRaceCheckingDecsAndProcsForVar(v);
+ }
+ }
+
+ protected void AddLogAccessProcedure(Variable v, string Access)
+ {
+ Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);
+
+ Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);
+ Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetXVariable(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 WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");
+ Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
+ WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ ));
+ }
+
+ if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)
+ {
+ WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());
+ }
+
+ WriteReadGuard = Expr.Not(WriteReadGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard));
+ }
+ 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 WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(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, WriteOffsetXVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
+ ));
+ }
+
+ if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)
+ {
+ WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());
+ }
+
+ WriteWriteGuard = Expr.Not(WriteWriteGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard));
+
+ // Check write by thread 2 does not conflict with read by thread 1
+ Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");
+ Variable ReadOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "READ");
+
+ Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
+ ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));
+ ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)),
+ new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)), 1, "WRITE"),
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ ));
+ }
+
+ if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)
+ {
+ ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());
+ }
+
+ ReadWriteGuard = Expr.Not(ReadWriteGuard);
+ simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard));
+
+ }
+
+ bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));
+
+ LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));
+ LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));
+
+ 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)) });
+
+ LogAccessImplementation.Proc = LogAccessProcedure;
+
+ verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);
+ verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);
+ }
+
+ private Variable VariableForThread(int thread, Variable v)
+ {
+ return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);
+ }
+
+ protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ {
+ Variable AccessHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
+
+ // Assumes full symmetry reduction
+
+ verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessHasOccurred.Clone() as Variable));
+
+ Debug.Assert(v.TypedIdent.Type is MapType);
+ MapType mt = v.TypedIdent.Type as MapType;
+ Debug.Assert(mt.Arguments.Length == 1);
+
+ Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);
+ verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessOffsetX.Clone() as Variable));
+
+ }
+
+
+ private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)
+ {
+ 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 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;
+ }
+
+ 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")));
+
+ verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));
+ }
+
+ 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;
+ }
+
+
+ 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));
+ }
+
+ private Expr AccessedOffsetIsThreadLocalIdExpr(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, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(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.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(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.MakeOffsetXVariable(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)));
+
+ Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
+ new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);
+
+ Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));
+
+ 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.MakeOffsetXVariable(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);
+ }
+ }
+
+
+
+}
diff --git a/Source/GPUVerify/ReducedStrengthAnalysis.cs b/Source/GPUVerify/ReducedStrengthAnalysis.cs
new file mode 100644
index 00000000..0e58ff7d
--- /dev/null
+++ b/Source/GPUVerify/ReducedStrengthAnalysis.cs
@@ -0,0 +1,166 @@
+using Microsoft.Boogie;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace GPUVerify {
+
+class ReducedStrengthAnalysis {
+
+ GPUVerifier verifier;
+ Implementation impl;
+ VariableDefinitionAnalysis varDefs;
+
+ Dictionary<Variable, List<Tuple<object, Expr>>> multiDefMap = new Dictionary<Variable, List<Tuple<object, Expr>>>();
+ Dictionary<string, ModStrideConstraint> strideConstraintMap = new Dictionary<string, ModStrideConstraint>();
+ Dictionary<object, List<string>> loopCounterMap = new Dictionary<object, List<string>>();
+
+ ReducedStrengthAnalysis(GPUVerifier v, Implementation i) {
+ verifier = v;
+ impl = i;
+ varDefs = verifier.varDefAnalyses[impl];
+ }
+
+ void AddAssignment(object regionId, AssignLhs lhs, Expr rhs) {
+ if (lhs is SimpleAssignLhs) {
+ var sLhs = (SimpleAssignLhs)lhs;
+ var theVar = sLhs.DeepAssignedVariable;
+ List<Tuple<object, Expr>> defs;
+ if (multiDefMap.ContainsKey(theVar))
+ defs = multiDefMap[theVar];
+ else
+ defs = multiDefMap[theVar] = new List<Tuple<object, Expr>>();
+ defs.Add(new Tuple<object, Expr>(regionId, rhs));
+ }
+ }
+
+ void AnalyseRegion(IRegion region) {
+ foreach (var c in region.CmdsChildRegions()) {
+ var ac = c as AssignCmd;
+ if (ac != null) {
+ foreach (var a in ac.Lhss.Zip(ac.Rhss)) {
+ AddAssignment(region.Identifier(), a.Item1, a.Item2);
+ }
+ }
+ var child = c as IRegion;
+ if (child != null)
+ AnalyseRegion(child);
+ }
+ }
+
+ void Analyse() {
+ AnalyseRegion(verifier.RootRegion(impl));
+ foreach (var v in multiDefMap.Keys) {
+ var defs = multiDefMap[v];
+ if (defs.Count != 2)
+ continue;
+ bool def0IsConst, def1IsConst;
+ var def0 = varDefs.SubstDefinitions(defs[0].Item2, impl.Name, out def0IsConst);
+ var def1 = varDefs.SubstDefinitions(defs[1].Item2, impl.Name, out def1IsConst);
+ if (def0IsConst && !def1IsConst) {
+ AddDefinitionPair(v, def0, def1, defs[1].Item1);
+ } else if (!def0IsConst && def1IsConst) {
+ AddDefinitionPair(v, def1, def0, defs[0].Item1);
+ }
+ }
+ multiDefMap = null;
+ }
+
+ private class StrideForm {
+ public StrideForm(Kind kind) { this.kind = kind; this.op = null; }
+ public StrideForm(Kind kind, Expr op) { this.kind = kind; this.op = op; }
+ public enum Kind { Bottom, Identity, Constant, Product, PowerMul, PowerDiv };
+ public Kind kind;
+ public Expr op;
+ }
+
+ private StrideForm ComputeStrideForm(Variable v, Expr e) {
+ Expr lhs, rhs;
+
+ if (e is LiteralExpr)
+ return new StrideForm(StrideForm.Kind.Constant, e);
+
+ var ie = e as IdentifierExpr;
+ if (ie != null) {
+ if (ie.Decl is Constant)
+ return new StrideForm(StrideForm.Kind.Constant, e);
+ if (ie.Decl == v)
+ return new StrideForm(StrideForm.Kind.Identity, e);
+ }
+
+ if (GPUVerifier.IsBVAdd(e, out lhs, out rhs)) {
+ var lhssf = ComputeStrideForm(v, lhs);
+ var rhssf = ComputeStrideForm(v, rhs);
+ if (lhssf.kind == StrideForm.Kind.Constant &&
+ rhssf.kind == StrideForm.Kind.Constant)
+ return new StrideForm(StrideForm.Kind.Constant, e);
+ else if (lhssf.kind == StrideForm.Kind.Constant &&
+ rhssf.kind == StrideForm.Kind.Identity)
+ return new StrideForm(StrideForm.Kind.Product, lhs);
+ else if (lhssf.kind == StrideForm.Kind.Identity &&
+ rhssf.kind == StrideForm.Kind.Constant)
+ return new StrideForm(StrideForm.Kind.Product, rhs);
+ else if (lhssf.kind == StrideForm.Kind.Constant &&
+ rhssf.kind == StrideForm.Kind.Product)
+ return new StrideForm(StrideForm.Kind.Product, verifier.MakeBVAdd(lhs, rhssf.op));
+ else if (lhssf.kind == StrideForm.Kind.Product &&
+ rhssf.kind == StrideForm.Kind.Constant)
+ return new StrideForm(StrideForm.Kind.Product, verifier.MakeBVAdd(lhssf.op, rhs));
+ else
+ return new StrideForm(StrideForm.Kind.Bottom);
+ }
+
+ var ne = e as NAryExpr;
+ if (ne != null) {
+ foreach (Expr op in ne.Args)
+ if (ComputeStrideForm(v, op).kind != StrideForm.Kind.Constant)
+ return new StrideForm(StrideForm.Kind.Bottom);
+ return new StrideForm(StrideForm.Kind.Constant, e);
+ }
+
+ return new StrideForm(StrideForm.Kind.Bottom);
+ }
+
+ private void AddDefinitionPair(Variable v, Expr constDef, Expr nonConstDef, object nonConstId) {
+ var sf = ComputeStrideForm(v, nonConstDef);
+ if (sf.kind == StrideForm.Kind.Product) {
+ var sc = new ModStrideConstraint(sf.op, constDef);
+ if (!sc.IsBottom()) {
+ strideConstraintMap[v.Name] = sc;
+ List<string> lcs;
+ if (loopCounterMap.ContainsKey(nonConstId))
+ lcs = loopCounterMap[nonConstId];
+ else
+ lcs = loopCounterMap[nonConstId] = new List<string>();
+ lcs.Add(v.Name);
+ }
+ }
+ }
+
+ public StrideConstraint GetStrideConstraint(string varName) {
+ int id;
+ var strippedVarName = GPUVerifier.StripThreadIdentifier(varName, out id);
+ if (!strideConstraintMap.ContainsKey(strippedVarName))
+ return null;
+
+ var msc = strideConstraintMap[strippedVarName];
+ if (id == 0)
+ return msc;
+ return new ModStrideConstraint(verifier.MaybeDualise(msc.mod, id, impl.Name),
+ verifier.MaybeDualise(msc.modEq, id, impl.Name));
+ }
+
+ public IEnumerable<string> StridedLoopCounters(object loopId) {
+ if (!loopCounterMap.ContainsKey(loopId))
+ return Enumerable.Empty<string>();
+ return loopCounterMap[loopId];
+ }
+
+ public static ReducedStrengthAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
+ var a = new ReducedStrengthAnalysis(verifier, impl);
+ a.Analyse();
+ return a;
+ }
+}
+
+}
diff --git a/Source/GPUVerify/StrideConstraint.cs b/Source/GPUVerify/StrideConstraint.cs
new file mode 100644
index 00000000..948786b7
--- /dev/null
+++ b/Source/GPUVerify/StrideConstraint.cs
@@ -0,0 +1,141 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Basetypes;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+
+class StrideConstraint {
+
+ public static StrideConstraint Bottom(Expr e) {
+ int width = e.Type.BvBits;
+ return new ModStrideConstraint(new LiteralExpr(Token.NoToken, BigNum.FromInt(1), width),
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(0), width));
+ }
+
+ public bool IsBottom() {
+ var msc = this as ModStrideConstraint;
+ if (msc == null)
+ return false;
+
+ var le = msc.mod as LiteralExpr;
+ if (le == null)
+ return false;
+
+ var bvc = le.Val as BvConst;
+ if (bvc == null)
+ return false;
+
+ return bvc.Value.InInt32 && bvc.Value.ToInt == 1;
+ }
+
+ private Expr ExprModPow2(GPUVerifier verifier, Expr expr, Expr powerOfTwoExpr) {
+ Expr Pow2Minus1 = verifier.MakeBVSub(powerOfTwoExpr,
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));
+
+ return verifier.MakeBVAnd(Pow2Minus1, expr);
+ }
+
+ public Expr MaybeBuildPredicate(GPUVerifier verifier, Expr e) {
+ var msc = this as ModStrideConstraint;
+ if (msc != null && !msc.IsBottom()) {
+ Expr modEqExpr = Expr.Eq(ExprModPow2(verifier, e, msc.mod), ExprModPow2(verifier, msc.modEq, msc.mod));
+ return modEqExpr;
+ }
+
+ return null;
+ }
+
+ private static StrideConstraint BuildAddStrideConstraint(GPUVerifier verifier, Expr e, StrideConstraint lhsc, StrideConstraint rhsc) {
+ if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint) {
+ return new EqStrideConstraint(e);
+ }
+
+ if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
+ return BuildAddStrideConstraint(verifier, e, rhsc, lhsc);
+
+ if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint) {
+ var lhsmc = (ModStrideConstraint)lhsc;
+ var rhsec = (EqStrideConstraint)rhsc;
+
+ return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsec.eq));
+ }
+
+ if (lhsc is ModStrideConstraint && rhsc is ModStrideConstraint) {
+ var lhsmc = (ModStrideConstraint)lhsc;
+ var rhsmc = (ModStrideConstraint)rhsc;
+
+ if (lhsmc.mod == rhsmc.mod)
+ return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsmc.modEq));
+ }
+
+ return Bottom(e);
+ }
+
+ private static StrideConstraint BuildMulStrideConstraint(GPUVerifier verifier, Expr e, StrideConstraint lhsc, StrideConstraint rhsc) {
+ if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint) {
+ return new EqStrideConstraint(e);
+ }
+
+ if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
+ return BuildMulStrideConstraint(verifier, e, rhsc, lhsc);
+
+ if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint) {
+ var lhsmc = (ModStrideConstraint)lhsc;
+ var rhsec = (EqStrideConstraint)rhsc;
+
+ return new ModStrideConstraint(verifier.MakeBVMul(lhsmc.mod, rhsec.eq),
+ verifier.MakeBVMul(lhsmc.modEq, rhsec.eq));
+ }
+
+ return Bottom(e);
+ }
+
+ public static StrideConstraint FromExpr(GPUVerifier verifier, Implementation impl, Expr e) {
+ if (e is LiteralExpr)
+ return new EqStrideConstraint(e);
+
+ var ie = e as IdentifierExpr;
+ if (ie != null) {
+ if (ie.Decl is Constant)
+ return new EqStrideConstraint(e);
+
+ var rsa = verifier.reducedStrengthAnalyses[impl];
+ var sc = rsa.GetStrideConstraint(ie.Decl.Name);
+ if (sc == null)
+ return Bottom(e);
+ return sc;
+ }
+
+ Expr lhs, rhs;
+
+ if (GPUVerifier.IsBVAdd(e, out lhs, out rhs)) {
+ var lhsc = FromExpr(verifier, impl, lhs);
+ var rhsc = FromExpr(verifier, impl, rhs);
+ return BuildAddStrideConstraint(verifier, e, lhsc, rhsc);
+ }
+
+ if (GPUVerifier.IsBVMul(e, out lhs, out rhs)) {
+ var lhsc = FromExpr(verifier, impl, lhs);
+ var rhsc = FromExpr(verifier, impl, rhs);
+ return BuildMulStrideConstraint(verifier, e, lhsc, rhsc);
+ }
+
+ return Bottom(e);
+ }
+
+}
+
+class EqStrideConstraint : StrideConstraint {
+ public EqStrideConstraint(Expr eq) { this.eq = eq; }
+ public Expr eq;
+}
+
+class ModStrideConstraint : StrideConstraint {
+ public ModStrideConstraint(Expr mod, Expr modEq) { this.mod = mod; this.modEq = modEq; }
+ public Expr mod, modEq;
+}
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 20:06:00 +0000