summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
diff options
context:
space:
mode:
Diffstat (limited to 'Source/GPUVerify')
-rw-r--r--Source/GPUVerify/BlockPredicator.cs260
-rw-r--r--Source/GPUVerify/ElementEncodingRaceInstrumenter.cs69
-rw-r--r--Source/GPUVerify/GPUVerifier.cs46
-rw-r--r--Source/GPUVerify/GPUVerify.csproj9
-rw-r--r--Source/GPUVerify/GraphAlgorithms.cs84
-rw-r--r--Source/GPUVerify/IRegion.cs1
-rw-r--r--Source/GPUVerify/KernelDualiser.cs23
-rw-r--r--Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs322
-rw-r--r--Source/GPUVerify/MayBeGlobalSizeAnalyser.cs287
-rw-r--r--Source/GPUVerify/RaceInstrumenterBase.cs52
-rw-r--r--Source/GPUVerify/StructuredRegion.cs37
-rw-r--r--Source/GPUVerify/UnstructuredRegion.cs6
-rw-r--r--Source/GPUVerify/VariableDefinitionAnalysis.cs155
13 files changed, 221 insertions, 1130 deletions
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
deleted file mode 100644
index 5e61734d..00000000
--- a/Source/GPUVerify/BlockPredicator.cs
+++ /dev/null
@@ -1,260 +0,0 @@
-using Graphing;
-using Microsoft.Boogie;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace GPUVerify {
-
-class BlockPredicator {
-
- GPUVerifier verifier;
- Program prog;
- Implementation impl;
- Graph<Block> blockGraph;
-
- Expr returnBlockId;
-
- LocalVariable curVar, pVar;
- IdentifierExpr cur, p, fp;
- Expr pExpr;
- Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
- new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
- Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
- HashSet<Block> doneBlocks = new HashSet<Block>();
-
- BlockPredicator(GPUVerifier v, Program p, Implementation i) {
- verifier = v;
- prog = p;
- impl = i;
- }
-
- void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
- if (cmd is AssignCmd) {
- var aCmd = (AssignCmd)cmd;
- cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
- new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(p, rhs, lhs.AsExpr))))));
- } else if (cmd is AssertCmd) {
- var aCmd = (AssertCmd)cmd;
- if (cmdSeq.Last() is AssignCmd &&
- cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {
- // This may be a loop invariant. Make sure it continues to appear as
- // the first statement in the block.
- var assign = cmdSeq.Last();
- cmdSeq.Truncate(cmdSeq.Length-1);
- cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr)));
- cmdSeq.Add(assign);
- } else {
- cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
- }
- } else if (cmd is AssumeCmd) {
- var aCmd = (AssumeCmd)cmd;
- cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
- } else if (cmd is HavocCmd) {
- var hCmd = (HavocCmd)cmd;
- foreach (IdentifierExpr v in hCmd.Vars) {
- Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
- Contract.Assert(type != null);
-
- IdentifierExpr havocTempExpr;
- if (havocVars.ContainsKey(type)) {
- havocTempExpr = havocVars[type];
- } else {
- var havocVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken,
- "_HAVOC_" + type.ToString(), type));
- impl.LocVars.Add(havocVar);
- havocVars[type] = havocTempExpr =
- new IdentifierExpr(Token.NoToken, havocVar);
- }
- cmdSeq.Add(new HavocCmd(Token.NoToken,
- new IdentifierExprSeq(havocTempExpr)));
- cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(p, havocTempExpr, v))));
- }
- } else if (cmd is CallCmd) {
- var cCmd = (CallCmd)cmd;
- cCmd.Ins.Insert(0, p);
- cmdSeq.Add(cCmd);
- } else {
- Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- }
- }
-
- void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {
- if (cmd is GotoCmd) {
- var gCmd = (GotoCmd)cmd;
- var targets = new List<Expr>(
- gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));
- if (targets.Count == 1) {
- PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));
- } else {
- PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,
- new IdentifierExprSeq(cur)));
- PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
- targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
- }
-
- foreach (Block b in gCmd.labelTargets) {
- if (blockGraph.Predecessors(b).Count() == 1) {
- if (!doneBlocks.Contains(b)) {
- var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd);
- if (assumes.Count() > 0) {
- foreach (AssumeCmd aCmd in assumes) {
- cmdSeq.Add(new AssumeCmd(Token.NoToken,
- Expr.Imp(Expr.Eq(cur, blockIds[b]),
- aCmd.Expr)));
- }
- b.Cmds =
- new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());
- }
- }
- }
- }
- } else if (cmd is ReturnCmd) {
- PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));
- } else {
- Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- }
- }
-
- void PredicateImplementation() {
- blockGraph = prog.ProcessLoops(impl);
- var sortedBlocks = blockGraph.LoopyTopSort();
-
- int blockId = 0;
- foreach (var block in impl.Blocks)
- blockIds[block] = Expr.Literal(blockId++);
- returnBlockId = Expr.Literal(blockId++);
-
- curVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken, "cur",
- Microsoft.Boogie.Type.Int));
- impl.LocVars.Add(curVar);
- cur = Expr.Ident(curVar);
-
- pVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken, "p",
- Microsoft.Boogie.Type.Bool));
- impl.LocVars.Add(pVar);
- p = Expr.Ident(pVar);
-
- var newBlocks = new List<Block>();
-
- fp = Expr.Ident(impl.InParams[0]);
- Block entryBlock = new Block();
- entryBlock.Label = "entry";
- entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(fp, blockIds[sortedBlocks[0].Item1],
- returnBlockId))));
- newBlocks.Add(entryBlock);
-
- var prevBlock = entryBlock;
- foreach (var n in sortedBlocks) {
- if (n.Item2) {
- var backedgeBlock = new Block();
- newBlocks.Add(backedgeBlock);
-
- backedgeBlock.Label = n.Item1.Label + ".backedge";
- backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
- Expr.Eq(cur, blockIds[n.Item1]),
- new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
- backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(n.Item1));
-
- var tailBlock = new Block();
- newBlocks.Add(tailBlock);
-
- tailBlock.Label = n.Item1.Label + ".tail";
- tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
- Expr.Neq(cur, blockIds[n.Item1])));
-
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(backedgeBlock, tailBlock));
- prevBlock = tailBlock;
- } else {
- var runBlock = n.Item1;
- newBlocks.Add(runBlock);
-
- pExpr = Expr.Eq(cur, blockIds[runBlock]);
- CmdSeq newCmdSeq = new CmdSeq();
- AddNonUniformInvariant(newCmdSeq, runBlock);
- if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) {
- AddUniformCandidateInvariant(newCmdSeq, runBlock);
- }
- newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
- foreach (Cmd cmd in runBlock.Cmds)
- PredicateCmd(newCmdSeq, cmd);
- PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd);
- runBlock.Cmds = newCmdSeq;
-
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(runBlock));
- prevBlock = runBlock;
- doneBlocks.Add(runBlock);
- }
- }
-
- prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
- impl.Blocks = newBlocks;
- }
-
- private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
- cs.Add(verifier.CreateCandidateInvariant(Expr.Eq(cur,
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(fp, blockIds[header], returnBlockId))),
- "uniform loop"));
- }
-
- private void AddNonUniformInvariant(CmdSeq cs, Block header) {
- var loopNodes = new HashSet<Block>();
- foreach (var b in blockGraph.BackEdgeNodes(header))
- loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));
- var exits = new HashSet<Expr>();
- foreach (var ln in loopNodes) {
- if (ln.TransferCmd is GotoCmd) {
- var gCmd = (GotoCmd) ln.TransferCmd;
- foreach (var exit in gCmd.labelTargets.Cast<Block>()
- .Where(b => !loopNodes.Contains(b)))
- exits.Add(blockIds[exit]);
- }
- if (ln.TransferCmd is ReturnCmd)
- exits.Add(returnBlockId);
- }
- var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]),
- (e, exit) => Expr.Or(e, Expr.Eq(cur, exit)));
- cs.Add(new AssertCmd(Token.NoToken, new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)))));
- }
-
- public static void Predicate(GPUVerifier v, Program p) {
- foreach (var decl in p.TopLevelDeclarations.ToList()) {
- if (decl is DeclWithFormals && !(decl is Function)) {
- var dwf = (DeclWithFormals)decl;
- var fpVar = new Formal(Token.NoToken,
- new TypedIdent(Token.NoToken, "_P",
- Microsoft.Boogie.Type.Bool),
- /*incoming=*/true);
- dwf.InParams = new VariableSeq(
- (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
- .ToArray());
- }
- var impl = decl as Implementation;
- if (impl != null)
- new BlockPredicator(v, p, impl).PredicateImplementation();
- }
- }
-
-}
-
-}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 3cd29367..cb880767 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -205,16 +205,16 @@ namespace GPUVerify
}
- protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
+ protected override void AddAccessedOffsetsAreConstantCandidateInvariant(IRegion region, Variable v, IEnumerable<Expr> offsets, string ReadOrWrite)
{
- Expr expr = AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is global id");
+ Expr expr = AccessedOffsetsAreConstantExpr(v, offsets, ReadOrWrite, 1);
+ verifier.AddCandidateInvariant(region, expr, "accessed offsets are constant");
}
- protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is local id");
+ private Expr AccessedOffsetsAreConstantExpr(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.Select(ofs => (Expr)Expr.Eq(new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), ofs)).Aggregate(Expr.Or));
}
private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
@@ -250,61 +250,6 @@ namespace GPUVerify
return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);
}
- private Expr GlobalSizeExpr(string dimension)
- {
- return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
- new IdentifierExpr(Token.NoToken, verifier.GetNumGroups(dimension)),
- new IdentifierExpr(Token.NoToken, verifier.GetGroupSize(dimension)));
- }
-
- protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D local id");
- }
-
- private Expr AccessedOffsetIsThreadFlattened2DLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = null;
- if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
- {
- expr = Expr.Imp(
- AccessHasOccurred(v, ReadOrWrite, Thread),
- Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),
- GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
- new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)), new IdentifierExpr(v.tok, verifier.GetGroupSize("X"))),
- new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread)))
- )
- );
- }
- return expr;
- }
-
- protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
- {
- Expr expr = AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D global id");
- }
-
- private Expr AccessedOffsetIsThreadFlattened2DGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)
- {
- Expr expr = null;
- if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
- {
- expr = Expr.Imp(
- AccessHasOccurred(v, ReadOrWrite, Thread),
- Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),
- GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
- GlobalIdExpr("Y", Thread), GlobalSizeExpr("X")),
- GlobalIdExpr("X", Thread))
- )
- );
- }
- return expr;
- }
-
protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
{
Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index a49461c7..40e27310 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -25,7 +25,6 @@ namespace GPUVerify
private HashSet<string> ReservedNames = new HashSet<string>();
private int TempCounter = 0;
- private int invariantGenerationCounter = 0;
internal const string LOCAL_ID_X_STRING = "local_id_x";
internal const string LOCAL_ID_Y_STRING = "local_id_y";
@@ -64,13 +63,12 @@ namespace GPUVerify
public UniformityAnalyser uniformityAnalyser;
public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;
public MayBeGidAnalyser mayBeGidAnalyser;
- public MayBeGlobalSizeAnalyser mayBeGlobalSizeAnalyser;
- public MayBeFlattened2DTidOrGidAnalyser mayBeFlattened2DTidOrGidAnalyser;
public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;
public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;
public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;
public LiveVariableAnalyser liveVariableAnalyser;
public ArrayControlFlowAnalyser arrayControlFlowAnalyser;
+ public Dictionary<Implementation, VariableDefinitionAnalysis> varDefAnalyses;
public GPUVerifier(string filename, Program program, ResolutionContext rc, IRaceInstrumenter raceInstrumenter) : this(filename, program, rc, raceInstrumenter, false)
{
@@ -371,6 +369,8 @@ namespace GPUVerify
DoArrayControlFlowAnalysis();
+ DoVariableDefinitionAnalysis();
+
if (CommandLineOptions.ShowStages)
{
emitProgram(outputFilename + "_preprocessed");
@@ -490,12 +490,6 @@ namespace GPUVerify
mayBeGidAnalyser = new MayBeGidAnalyser(this);
mayBeGidAnalyser.Analyse();
-
- mayBeGlobalSizeAnalyser = new MayBeGlobalSizeAnalyser(this);
- mayBeGlobalSizeAnalyser.Analyse();
-
- mayBeFlattened2DTidOrGidAnalyser = new MayBeFlattened2DTidOrGidAnalyser(this);
- mayBeFlattened2DTidOrGidAnalyser.Analyse();
}
private void DoMayBeIdPlusConstantAnalysis()
@@ -524,6 +518,12 @@ namespace GPUVerify
liveVariableAnalyser.Analyse();
}
+ private void DoVariableDefinitionAnalysis()
+ {
+ varDefAnalyses = Program.TopLevelDeclarations
+ .OfType<Implementation>()
+ .ToDictionary(i => i, i => VariableDefinitionAnalysis.Analyse(this, i));
+ }
private void ProcessAccessInvariants()
{
@@ -814,18 +814,16 @@ namespace GPUVerify
internal void AddCandidateRequires(Procedure Proc, Expr e)
{
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
+ Constant ExistentialBooleanConstant = Program.MakeExistentialBoolean();
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
Proc.Requires.Add(new Requires(false, Expr.Imp(ExistentialBoolean, e)));
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
internal void AddCandidateEnsures(Procedure Proc, Expr e)
{
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
+ Constant ExistentialBooleanConstant = Program.MakeExistentialBoolean();
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
Proc.Ensures.Add(new Ensures(false, Expr.Imp(ExistentialBoolean, e)));
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
private List<Expr> GetUserSuppliedInvariants(string ProcedureName)
@@ -1042,14 +1040,6 @@ namespace GPUVerify
return _GROUP_SIZE_Z != null;
}
- internal Constant MakeExistentialBoolean(IToken tok)
- {
- Constant ExistentialBooleanConstant = new Constant(tok, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
- invariantGenerationCounter++;
- ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
- return ExistentialBooleanConstant;
- }
-
internal static string StripThreadIdentifier(string p)
{
if (p.Contains("$"))
@@ -2152,7 +2142,7 @@ namespace GPUVerify
{
if (CommandLineOptions.Unstructured)
{
- BlockPredicator.Predicate(this, Program);
+ BlockPredicator.Predicate(Program, /*createCandidateInvariants=*/CommandLineOptions.Inference);
return;
}
@@ -2256,19 +2246,9 @@ namespace GPUVerify
internal void AddCandidateInvariant(IRegion region, Expr e, string tag)
{
- region.AddInvariant(CreateCandidateInvariant(e, tag));
+ region.AddInvariant(Program.CreateCandidateInvariant(e, tag));
}
- internal PredicateCmd CreateCandidateInvariant(Expr e, string tag)
- {
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(Token.NoToken);
- IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
- PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
- invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
- return invariant;
- }
-
internal Implementation GetImplementation(string procedureName)
{
foreach (Declaration D in Program.TopLevelDeclarations)
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 376d67b5..eba91cd2 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -108,15 +108,11 @@
<Compile Include="AccessRecord.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
- <Compile Include="BlockPredicator.cs" />
<Compile Include="UnstructuredRegion.cs" />
<Compile Include="IRegion.cs" />
- <Compile Include="GraphAlgorithms.cs" />
<Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
<Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
<Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
- <Compile Include="MayBeGlobalSizeAnalyser.cs" />
- <Compile Include="MayBeFlattened2DTidOrGidAnalyser.cs" />
<Compile Include="MayBeGidAnalyser.cs" />
<Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
<Compile Include="KernelDualiser.cs" />
@@ -147,6 +143,7 @@
<Compile Include="UniformityAnalyser.cs" />
<Compile Include="VariableDualiser.cs" />
<Compile Include="VariablesOccurringInExpressionVisitor.cs" />
+ <Compile Include="VariableDefinitionAnalysis.cs" />
<Compile Include="StructuredRegion.cs" />
<Compile Include="WriteCollector.cs" />
</ItemGroup>
@@ -171,6 +168,10 @@
<Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
+ <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+ <Name>VCGeneration</Name>
+ </ProjectReference>
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/GPUVerify/GraphAlgorithms.cs
deleted file mode 100644
index 3442a64d..00000000
--- a/Source/GPUVerify/GraphAlgorithms.cs
+++ /dev/null
@@ -1,84 +0,0 @@
-using Graphing;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace GPUVerify {
-
-public static class GraphAlgorithms {
-
- public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) {
- Contract.Assert(g.Reducible);
-
- int n = g.Nodes.Count;
- var nodeToNumber = new Dictionary<Node, int>(n);
- var numberToNode = new Node[n];
- var allNodes = new List<int>();
- int counter = 0;
- foreach (Node node in g.Nodes) {
- numberToNode[counter] = node;
- nodeToNumber[node] = counter;
- allNodes.Add(counter);
- counter++;
- }
-
- var loops = new List<int>[n];
- foreach (var h in g.Headers) {
- var loopNodes = new HashSet<Node>();
- foreach (var b in g.BackEdgeNodes(h))
- loopNodes.UnionWith(g.NaturalLoops(h, b));
- loops[nodeToNumber[h]] =
- new List<int>(loopNodes.Select(node => nodeToNumber[node]));
- }
-
- var successors = new List<int>[n];
- int[] incomingEdges = new int[n];
-
- foreach (var e in g.Edges) {
- Contract.Assert(e.Item1 != null);
- Contract.Assert(e.Item2 != null);
- int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
- if (loops[target] == null || !loops[target].Contains(source)) {
- if (successors[source] == null)
- successors[source] = new List<int>();
- successors[source].Add(target);
- incomingEdges[target]++;
- }
- }
-
- var sortedNodes = new List<Tuple<Node, bool>>();
-
- var regionStack = new Stack<Tuple<Node, List<int>>>();
- regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
-
- while (regionStack.Count != 0) {
- int rootIndex = -1;
- foreach (var i in regionStack.Peek().Item2) {
- if (incomingEdges[i] == 0) {
- rootIndex = i;
- break;
- }
- }
- if (rootIndex == -1) {
- var region = regionStack.Pop();
- if (regionStack.Count != 0)
- sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
- continue;
- }
- incomingEdges[rootIndex] = -1;
- sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
- if (successors[rootIndex] != null)
- foreach (int s in successors[rootIndex])
- incomingEdges[s]--;
- if (loops[rootIndex] != null)
- regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
- loops[rootIndex]));
- }
-
- return sortedNodes;
- }
-
-}
-
-}
diff --git a/Source/GPUVerify/IRegion.cs b/Source/GPUVerify/IRegion.cs
index 26adaa4e..c6655b06 100644
--- a/Source/GPUVerify/IRegion.cs
+++ b/Source/GPUVerify/IRegion.cs
@@ -7,6 +7,7 @@ using Microsoft.Boogie;
namespace GPUVerify {
interface IRegion {
+ object Identifier();
IEnumerable<Cmd> Cmds();
IEnumerable<object> CmdsChildRegions();
IEnumerable<IRegion> SubRegions();
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 614659b6..967b69ef 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -186,32 +186,27 @@ namespace GPUVerify
else if (c is AssertCmd)
{
AssertCmd ass = c as AssertCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
+ if (!ContainsAsymmetricExpression(ass.Expr))
{
- cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
- }
- else
- {
- cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)), ass.Attributes));
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
}
}
else if (c is AssumeCmd)
{
AssumeCmd ass = c as AssumeCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else if (QKeyValue.FindBoolAttribute(ass.Attributes, "backedge"))
+ if (QKeyValue.FindBoolAttribute(ass.Attributes, "backedge"))
{
cs.Add(new AssumeCmd(c.tok, Expr.Or(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
else
{
- cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ if (!ContainsAsymmetricExpression(ass.Expr))
+ {
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
}
}
else
diff --git a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs
deleted file mode 100644
index ea9b85fa..00000000
--- a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs
+++ /dev/null
@@ -1,322 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- class MayBeFlattened2DTidOrGidAnalyser
- {
- private static string[] cases = { "local", "global" };
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;
-
- public MayBeFlattened2DTidOrGidAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
-
- mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();
- foreach (string s in cases)
- {
- mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
-
- foreach (string s in cases)
- {
- mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();
- }
-
- foreach (Variable v in Impl.LocVars)
- {
- foreach (string s in cases)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams)
- {
- foreach (string s in cases)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- foreach (string s in cases)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, verifier.RootRegion(Impl));
- }
-
- private void Analyse(Implementation impl, IRegion region)
- {
- foreach (Cmd c in region.Cmds())
- {
- if (c is AssignCmd)
- {
- foreach (string s in cases)
- {
- TransferAssign(impl, c as AssignCmd, s);
- }
- }
- else if (c is CallCmd)
- {
- foreach (string s in cases)
- {
- TransferCall(impl, c as CallCmd, s);
- }
- }
- else if (c is HavocCmd)
- {
- foreach (string s in cases)
- {
- TransferHavoc(impl, c as HavocCmd, s);
- }
- }
- }
- }
-
- private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
- {
- Debug.Assert(havoc.Vars.Length == 1);
- if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
-
- private void TransferCall(Implementation impl, CallCmd callCmd, string component)
- {
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBe(component, impl.Name, callCmd.Ins[i]))
- {
- SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBe(component, impl.Name, callCmd.Outs[i].Name)
- && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNot(component, impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
-
- private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
- {
- for (int i = 0; i != assignCmd.Lhss.Count; ++i)
- {
- if (assignCmd.Lhss[i] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[i];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
- {
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
- }
- }
- }
-
- private void SetNot(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBe(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = true;
- }
-
- internal bool MayBe(string component, string proc, string v)
- {
- if (!mayBeInfo[component].ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeInfo[component][proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeInfo[component][proc][v];
- }
-
- internal bool MayBe(string component, string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);
- }
-
- if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))
- {
- NAryExpr nary = e as NAryExpr;
-
- if (component.Equals("local"))
- {
- if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, proc, nary.Args[1]))
- {
- return IsLocalIdYTimesGroupSizeX(proc, nary.Args[0]);
- }
-
- if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, proc, nary.Args[0]))
- {
- return IsLocalIdYTimesGroupSizeX(proc, nary.Args[1]);
- }
- }
- else
- {
- Debug.Assert(component.Equals("global"));
- if (verifier.mayBeGidAnalyser.MayBe("x", proc, nary.Args[1]))
- {
- return IsGlobalIdYTimesGlobalSizeX(proc, nary.Args[0]);
- }
-
- if (verifier.mayBeGidAnalyser.MayBe("x", proc, nary.Args[0]))
- {
- return IsGlobalIdYTimesGlobalSizeX(proc, nary.Args[1]);
- }
- }
- }
-
- return false;
- }
-
- private bool IsLocalIdYTimesGroupSizeX(string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsLocalIdYAndGroupSizeX(proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsLocalIdYAndGroupSizeX(proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsLocalIdYAndGroupSizeX(string proc, Expr maybeLocalIdY, Expr maybeGroupSizeX)
- {
- return verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_Y_STRING, proc, maybeLocalIdY) &&
- verifier.mayBeTidAnalyser.MayBe(GPUVerifier.GROUP_SIZE_X_STRING, proc, maybeGroupSizeX);
- }
-
-
- private bool IsGlobalIdYTimesGlobalSizeX(string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsGlobalIdYAndGlobalSizeX(proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsGlobalIdYAndGlobalSizeX(proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsGlobalIdYAndGlobalSizeX(string proc, Expr maybeGlobalIdY, Expr maybeGlobalSizeX)
- {
- return verifier.mayBeGidAnalyser.MayBe("y", proc, maybeGlobalIdY) &&
- verifier.mayBeGlobalSizeAnalyser.MayBe("x", proc, maybeGlobalSizeX);
- }
-
-
- private void dump()
- {
- foreach (string s in cases)
- {
- Console.WriteLine("*** flattened " + s + " id ***");
-
- foreach (string p in mayBeInfo[s].Keys)
- {
- Console.WriteLine(" Procedure " + p);
-
- foreach (string v in mayBeInfo[s][p].Keys)
- {
- if (mayBeInfo[s][p][v])
- {
- Console.WriteLine(" " + v + ": may be flattened " + s + " id");
- }
- }
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
deleted file mode 100644
index 98e71179..00000000
--- a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
+++ /dev/null
@@ -1,287 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- class MayBeGlobalSizeAnalyser
- {
- private static string[] dimensions = { "x", "y", "z" };
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;
-
- public MayBeGlobalSizeAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
-
- mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();
- foreach (string s in dimensions)
- {
- mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
-
- foreach (string s in dimensions)
- {
- mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();
- }
-
- foreach (Variable v in Impl.LocVars)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, verifier.RootRegion(Impl));
- }
-
- private void Analyse(Implementation impl, IRegion region)
- {
- foreach (Cmd c in region.Cmds())
- {
- if (c is AssignCmd)
- {
- foreach (string s in dimensions)
- {
- TransferAssign(impl, c as AssignCmd, s);
- }
- }
- else if (c is CallCmd)
- {
- foreach (string s in dimensions)
- {
- TransferCall(impl, c as CallCmd, s);
- }
- }
- else if (c is HavocCmd)
- {
- foreach (string s in dimensions)
- {
- TransferHavoc(impl, c as HavocCmd, s);
- }
- }
- }
- }
-
- private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
- {
- Debug.Assert(havoc.Vars.Length == 1);
- if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
-
- private void TransferCall(Implementation impl, CallCmd callCmd, string component)
- {
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBe(component, impl.Name, callCmd.Ins[i]))
- {
- SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBe(component, impl.Name, callCmd.Outs[i].Name)
- && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNot(component, impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
-
- private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
- {
- for (int i = 0; i != assignCmd.Lhss.Count; ++i)
- {
- if (assignCmd.Lhss[i] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[i];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
- {
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
- }
- }
- }
-
- private void SetNot(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBe(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = true;
- }
-
- internal bool MayBe(string component, string proc, string v)
- {
- if (!mayBeInfo[component].ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeInfo[component][proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeInfo[component][proc][v];
- }
-
- internal bool MayBe(string component, string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);
- }
-
- return IsNumGroupsTimesGroupSize(component, proc, e);
-
- }
-
- private bool IsNumGroupsTimesGroupSize(string component, string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsNumGroupsAndGroupSize(component, proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsNumGroupsAndGroupSize(component, proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsNumGroupsAndGroupSize(string component, string proc, Expr maybeNumGroups, Expr maybeGroupSize)
- {
- string numGroupsString = null;
- string groupSizeString = null;
- if (component.Equals("x"))
- {
- numGroupsString = GPUVerifier.NUM_GROUPS_X_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_X_STRING;
- }
- else if (component.Equals("y"))
- {
- numGroupsString = GPUVerifier.NUM_GROUPS_Y_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_Y_STRING;
- }
- else if (component.Equals("z"))
- {
- numGroupsString = GPUVerifier.NUM_GROUPS_Z_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_Z_STRING;
- }
- else
- {
- Debug.Assert(false);
- }
-
- return verifier.mayBeTidAnalyser.MayBe(numGroupsString, proc, maybeNumGroups) &&
- verifier.mayBeTidAnalyser.MayBe(groupSizeString, proc, maybeGroupSize);
- }
-
- private void dump()
- {
- foreach (string s in dimensions)
- {
- Console.WriteLine("*** global_size_" + s + " ***");
-
- foreach (string p in mayBeInfo[s].Keys)
- {
- Console.WriteLine(" Procedure " + p);
-
- foreach (string v in mayBeInfo[s][p].Keys)
- {
- if (mayBeInfo[s][p][v])
- {
- Console.WriteLine(" " + v + ": may be global_size_" + s);
- }
- }
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 3b307e64..5155b192 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -452,45 +452,13 @@ namespace GPUVerify
private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)
{
+ var offsets = GetOffsetsAccessed(region, v, accessType)
+ .Select(ofs => verifier.varDefAnalyses[impl].SubstDualisedDefinitions(ofs, 1, impl.Name))
+ .ToList();
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
+ if (!offsets.Contains(null))
{
- if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadLocalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
- }
-
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (verifier.mayBeGidAnalyser.MayBe("x", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
- }
-
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("local", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
- }
-
- foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
- {
- if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("global", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
- {
- AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(region, v, accessType);
- // No point adding it multiple times
- break;
- }
+ AddAccessedOffsetsAreConstantCandidateInvariant(region, v, offsets, accessType);
}
KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
@@ -680,18 +648,12 @@ namespace GPUVerify
AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
}
- protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
- protected abstract void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
- protected abstract void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
- protected abstract void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
-
protected abstract void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);
protected abstract void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetsAreConstantCandidateInvariant(IRegion region, Variable v, IEnumerable<Expr> offsets, string ReadOrWrite);
+
protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
diff --git a/Source/GPUVerify/StructuredRegion.cs b/Source/GPUVerify/StructuredRegion.cs
index 815752dd..366682e0 100644
--- a/Source/GPUVerify/StructuredRegion.cs
+++ b/Source/GPUVerify/StructuredRegion.cs
@@ -7,19 +7,29 @@ using Microsoft.Boogie;
namespace GPUVerify {
class StructuredRegion : IRegion {
+ Implementation impl;
WhileCmd cmd;
- StmtList stmts;
+
+ public StructuredRegion(Implementation impl) {
+ this.impl = impl;
+ }
public StructuredRegion(WhileCmd cmd) {
this.cmd = cmd;
}
- public StructuredRegion(StmtList stmts) {
- this.stmts = stmts;
+ public object Identifier() {
+ if (cmd != null)
+ return cmd;
+ else
+ return impl;
}
- public StructuredRegion(Implementation impl) {
- this.stmts = impl.StructuredStmts;
+ private StmtList StmtList() {
+ if (cmd != null)
+ return cmd.Body;
+ else
+ return impl.StructuredStmts;
}
private IEnumerable<Cmd> Cmds(StmtList stmts) {
@@ -84,24 +94,15 @@ class StructuredRegion : IRegion {
}
public IEnumerable<Cmd> Cmds() {
- if (cmd != null)
- return Cmds(cmd.Body);
- else
- return Cmds(stmts);
+ return Cmds(StmtList());
}
public IEnumerable<object> CmdsChildRegions() {
- if (cmd != null)
- return CmdsChildRegions(cmd.Body);
- else
- return CmdsChildRegions(stmts);
+ return CmdsChildRegions(StmtList());
}
public IEnumerable<IRegion> SubRegions() {
- if (cmd != null)
- return SubRegions(cmd.Body);
- else
- return SubRegions(stmts);
+ return SubRegions(StmtList());
}
public Expr Guard() {
@@ -117,4 +118,4 @@ class StructuredRegion : IRegion {
}
}
-} \ No newline at end of file
+}
diff --git a/Source/GPUVerify/UnstructuredRegion.cs b/Source/GPUVerify/UnstructuredRegion.cs
index 607dc6d7..239f7ca0 100644
--- a/Source/GPUVerify/UnstructuredRegion.cs
+++ b/Source/GPUVerify/UnstructuredRegion.cs
@@ -37,6 +37,10 @@ class UnstructuredRegion : IRegion {
guard = null;
}
+ public object Identifier() {
+ return header;
+ }
+
private HashSet<Block> SubBlocks() {
if (header != null) {
return loopNodes[header];
@@ -90,4 +94,4 @@ class UnstructuredRegion : IRegion {
}
}
-} \ No newline at end of file
+}
diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs
new file mode 100644
index 00000000..f55e51e8
--- /dev/null
+++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs
@@ -0,0 +1,155 @@
+using System;
+using Microsoft.Boogie;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace GPUVerify {
+
+class VariableDefinitionAnalysis {
+ GPUVerifier verifier;
+ Implementation impl;
+
+ Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();
+ Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();
+ bool changed;
+
+ VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {
+ verifier = v;
+ impl = i;
+ }
+
+ private class IsConstantVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+ public bool isConstant = true;
+
+ public IsConstantVisitor(VariableDefinitionAnalysis a) {
+ analysis = a;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr expr) {
+ if (expr.Fun is MapSelect) {
+ isConstant = false;
+ return expr;
+ } else
+ return base.VisitNAryExpr(expr);
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
+ if (expr.Decl is Constant)
+ return expr;
+ if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)
+ isConstant = false;
+ return expr;
+ }
+ };
+
+ bool IsConstant(Expr e) {
+ var v = new IsConstantVisitor(this);
+ v.Visit(e);
+ return v.isConstant;
+ }
+
+ void UpdateDefMap(Variable v, Expr def) {
+ if (!defMap.ContainsKey(v) || defMap[v] != def) {
+ changed = true;
+ defMap[v] = def;
+ }
+ }
+
+ void AddAssignment(AssignLhs lhs, Expr rhs) {
+ if (lhs is SimpleAssignLhs) {
+ var sLhs = (SimpleAssignLhs)lhs;
+ var theVar = sLhs.DeepAssignedVariable;
+ if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {
+ UpdateDefMap(theVar, null);
+ } else {
+ UpdateDefMap(theVar, rhs);
+ }
+ }
+ }
+
+ void Analyse() {
+ do {
+ changed = false;
+ foreach (var c in verifier.RootRegion(impl).Cmds()) {
+ if (c is AssignCmd) {
+ var aCmd = (AssignCmd)c;
+ foreach (var a in aCmd.Lhss.Zip(aCmd.Rhss)) {
+ AddAssignment(a.Item1, a.Item2);
+ }
+ }
+ }
+ } while (changed);
+ }
+
+ private class BuildNamedDefVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+
+ public BuildNamedDefVisitor(VariableDefinitionAnalysis a) {
+ analysis = a;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
+ if (expr.Decl is Constant)
+ return expr;
+ return analysis.BuildNamedDefFor(expr.Decl);
+ }
+ }
+
+ Expr BuildNamedDefFor(Variable v) {
+ Expr def;
+ if (namedDefMap.TryGetValue(v.Name, out def))
+ return def;
+ def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());
+ namedDefMap[v.Name] = def;
+ return def;
+ }
+
+ void BuildNamedDefMap() {
+ foreach (var v in defMap.Keys)
+ if (defMap[v] != null)
+ BuildNamedDefFor(v);
+ }
+
+ private class SubstDualisedDefVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+ private VariableDualiser dualiser;
+ public bool isSubstitutable = true;
+
+ public SubstDualisedDefVisitor(VariableDefinitionAnalysis a, int id, string procName) {
+ analysis = a;
+ dualiser = new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName);
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
+ if (expr.Decl is Constant)
+ return dualiser.VisitIdentifierExpr(expr);
+ var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name);
+ Expr def;
+ if (!analysis.namedDefMap.TryGetValue(varName, out def)) {
+ isSubstitutable = false;
+ return null;
+ }
+ return (Expr)dualiser.Visit(def.Clone());
+ }
+ }
+
+ public Expr SubstDualisedDefinitions(Expr e, int id, string procName) {
+ var v = new SubstDualisedDefVisitor(this, id, procName);
+ Expr result = (Expr)v.Visit(e.Clone());
+ if (!v.isSubstitutable)
+ return null;
+ return result;
+ }
+
+ public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
+ var a = new VariableDefinitionAnalysis(verifier, impl);
+ a.Analyse();
+ a.BuildNamedDefMap();
+ a.defMap = null;
+ return a;
+ }
+
+}
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 02:24:12 +0000