diff options
Diffstat (limited to 'Source/GPUVerify')
-rw-r--r-- | Source/GPUVerify/AccessCollector.cs | 25 | ||||
-rw-r--r-- | Source/GPUVerify/AccessRecord.cs | 27 | ||||
-rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 25 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 844 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 86 | ||||
-rw-r--r-- | Source/GPUVerify/LocalVariableAccessReplacer.cs | 54 | ||||
-rw-r--r-- | Source/GPUVerify/Main.cs | 175 | ||||
-rw-r--r-- | Source/GPUVerify/Properties/AssemblyInfo.cs | 36 | ||||
-rw-r--r-- | Source/GPUVerify/ReadCollector.cs | 115 | ||||
-rw-r--r-- | Source/GPUVerify/WriteCollector.cs | 107 |
10 files changed, 1494 insertions, 0 deletions
diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs new file mode 100644 index 00000000..a3821952 --- /dev/null +++ b/Source/GPUVerify/AccessCollector.cs @@ -0,0 +1,25 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ abstract class AccessCollector : StandardVisitor
+ {
+ protected GPUVerifier verifier;
+
+ public AccessCollector(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ }
+
+ protected void MultiDimensionalMapError()
+ {
+ Console.WriteLine("*** Error - multidimensional maps not supported in kernels, use nested maps instead");
+ Environment.Exit(1);
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/AccessRecord.cs b/Source/GPUVerify/AccessRecord.cs new file mode 100644 index 00000000..fedacde3 --- /dev/null +++ b/Source/GPUVerify/AccessRecord.cs @@ -0,0 +1,27 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class AccessRecord
+ {
+ public Variable v;
+ public Expr IndexZ;
+ public Expr IndexY;
+ public Expr IndexX;
+
+ public AccessRecord(Variable v, Expr IndexZ, Expr IndexY, Expr IndexX)
+ {
+ this.v = v;
+ this.IndexZ = IndexZ;
+ this.IndexY = IndexY;
+ this.IndexX = IndexX;
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs new file mode 100644 index 00000000..80dc18ef --- /dev/null +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -0,0 +1,25 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.IO;
+
+namespace GPUVerify
+{
+
+ class CommandLineOptions
+ {
+
+ public static List<string> inputFiles = new List<string>();
+
+ public static int Parse(string[] args)
+ {
+ for (int i = 0; i < args.Length; i++)
+ {
+ inputFiles.Add(args[i]);
+ }
+ return 0;
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs new file mode 100644 index 00000000..391d7bdf --- /dev/null +++ b/Source/GPUVerify/GPUVerifier.cs @@ -0,0 +1,844 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class GPUVerifier : CheckingContext
+ {
+
+ HashSet<string> ReservedNames;
+
+ private Program Program;
+ private Procedure KernelProcedure;
+ private Implementation KernelImplementation;
+ private Procedure BarrierProcedure;
+ private Microsoft.Boogie.Type ThreadIdType;
+ private String ThreadIdParameterName;
+
+ private HashSet<int> BarrierIds = new HashSet<int>();
+
+ private HashSet<Variable> ThreadLocalVariables = new HashSet<Variable>();
+ private HashSet<Variable> TileStaticVariables = new HashSet<Variable>();
+ private HashSet<Variable> GloalVariables = new HashSet<Variable>();
+
+
+ public GPUVerifier(Program program)
+ : base((IErrorSink)null)
+ {
+ this.Program = program;
+
+ ReservedNames = new HashSet<string>();
+ ReservedNames.Add("base");
+ ReservedNames.Add("offset_x");
+ ReservedNames.Add("offset_y");
+ ReservedNames.Add("offset_z");
+ ReservedNames.Add("AT_BARRIER");
+
+ CheckWellFormedness();
+ }
+
+ private void CheckWellFormedness()
+ {
+ int errorCount = check(Program);
+ if (errorCount != 0)
+ {
+ Console.WriteLine("{0} GPUVerify format errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
+ Environment.Exit(1);
+ }
+ }
+
+ internal int check(Program program)
+ {
+ BarrierProcedure = CheckExactlyOneBarrierProcedure(program);
+ KernelProcedure = CheckExactlyOneKernelProcedure(program);
+ TypeSynonymDecl ThreadIdDecl = CheckExactlyOneThreadIdType(program);
+ ThreadIdType = new TypeSynonymAnnotation(ThreadIdDecl.tok, ThreadIdDecl, new TypeSeq());
+
+ if (ErrorCount > 0)
+ {
+ return ErrorCount;
+ }
+
+ if (BarrierProcedure.InParams.Length != 0)
+ {
+ Error(BarrierProcedure, "Barrier procedure must not take any arguments");
+ }
+
+ if (BarrierProcedure.OutParams.Length != 0)
+ {
+ Error(BarrierProcedure, "Barrier procedure must not return any results");
+ }
+
+ FindGlobalVariables(program);
+
+ CheckKernelImplementation(program);
+
+ return ErrorCount;
+ }
+
+ private void FindGlobalVariables(Program program)
+ {
+ foreach (Declaration D in program.TopLevelDeclarations)
+ {
+ if (D is Variable && (D as Variable).IsMutable)
+ {
+ if (!ReservedNames.Contains((D as Variable).Name))
+ {
+ GloalVariables.Add(D as Variable);
+ }
+ }
+ }
+ }
+
+
+ private void CheckKernelImplementation(Program Program)
+ {
+ if (KernelProcedure.InParams.Length != 1)
+ {
+ Error(KernelProcedure, "Kernel procedure must take exactly one argument, of type {0}", ThreadIdType.ToString());
+ }
+ else
+ {
+ if (!KernelProcedure.InParams[0].TypedIdent.Type.Equals(ThreadIdType))
+ {
+ Error(KernelProcedure, "Argument to kernel procedure has wrong type - {0} instead of {1}", KernelProcedure.InParams[0].TypedIdent.Type.ToString(), ThreadIdType.ToString());
+ }
+
+ ThreadIdParameterName = KernelProcedure.InParams[0].TypedIdent.Name;
+
+ }
+
+ if (KernelProcedure.OutParams.Length != 0)
+ {
+ Error(KernelProcedure, "Kernel procedure must not return any results");
+ }
+
+
+ foreach (Declaration decl in Program.TopLevelDeclarations)
+ {
+ if (!(decl is Implementation))
+ {
+ continue;
+ }
+
+ Implementation Impl = decl as Implementation;
+
+ if (Impl.Proc == KernelProcedure)
+ {
+ KernelImplementation = Impl;
+ break;
+ }
+
+ }
+
+ if (KernelImplementation == null)
+ {
+ Error(Token.NoToken, "*** Error: no implementation of kernel procedure");
+ return;
+ }
+
+ // Collect up the local and tile_static variables
+ foreach (LocalVariable LV in KernelImplementation.LocVars)
+ {
+ if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))
+ {
+ TileStaticVariables.Add(LV);
+ }
+ else
+ {
+ ThreadLocalVariables.Add(LV);
+ }
+ }
+
+ // Clear the local variables
+ KernelImplementation.LocVars = new VariableSeq();
+
+ foreach (LocalVariable LV in ThreadLocalVariables)
+ {
+ // Make each local variable a global map from threadid to the usual type
+ GlobalVariable GV = new GlobalVariable(LV.tok, LV.TypedIdent);
+ TypeSeq IndexType = new TypeSeq();
+ IndexType.Add(ThreadIdType);
+ GV.TypedIdent.Type = new MapType(GV.TypedIdent.Type.tok, new TypeVariableSeq(), IndexType, LV.TypedIdent.Type);
+ Program.TopLevelDeclarations.Add(GV);
+ KernelProcedure.Modifies.Add(new IdentifierExpr(GV.tok, GV));
+ }
+
+ foreach (LocalVariable LV in TileStaticVariables)
+ {
+ // Promote each tile-static variable to global
+ GlobalVariable GV = new GlobalVariable(LV.tok, LV.TypedIdent);
+ GV.TypedIdent.Type = LV.TypedIdent.Type;
+ Program.TopLevelDeclarations.Add(GV);
+ KernelProcedure.Modifies.Add(new IdentifierExpr(GV.tok, GV));
+ }
+
+ LocalVariableAccessReplacer replacer = new LocalVariableAccessReplacer(this);
+
+ replacer.VisitImplementation(KernelImplementation);
+
+ Console.WriteLine("After replacement we have ");
+
+ using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))
+ {
+ KernelImplementation.Emit(writer, 1);
+ }
+
+ Environment.Exit(1);
+
+
+ // Check that each barrier has a positive integer id
+ // Check that these ids are all distinct
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ foreach (Cmd C in B.Cmds)
+ {
+ if (IsBarrier(C))
+ {
+ CallCmd Barrier = C as CallCmd;
+
+ int BarrierId = QKeyValue.FindIntAttribute(Barrier.Attributes, "barrier_id", -1);
+ if (BarrierId < 1)
+ {
+ Error(Barrier, "Barrier must have positive integer attribute \"barrier_id\"");
+ }
+ else if (BarrierIds.Contains(BarrierId))
+ {
+ Error(Barrier, "Each barrier call must have a unique integer attribute \"barrier_id\" - duplicate id {0} detected", BarrierId);
+ }
+ else
+ {
+ BarrierIds.Add(BarrierId);
+ }
+ }
+ }
+
+ }
+
+
+ }
+
+
+
+ private Procedure CheckExactlyOneKernelProcedure(Program program)
+ {
+ return CheckSingleInstanceOfAttributedProcedure(program, "kernel");
+ }
+
+ private Procedure CheckExactlyOneBarrierProcedure(Program program)
+ {
+ return CheckSingleInstanceOfAttributedProcedure(program, "barrier");
+ }
+
+ private TypeSynonymDecl CheckExactlyOneThreadIdType(Program program)
+ {
+ return CheckSingleInstanceOfAttributedEntity<TypeSynonymDecl>(program, "thread_id");
+ }
+
+ private T CheckSingleInstanceOfAttributedEntity<T>(Program program, string attribute) where T : Declaration
+ {
+ T attributedEntity = null;
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))
+ {
+ continue;
+ }
+
+ if (decl is T)
+ {
+ if (attributedEntity == null)
+ {
+ attributedEntity = decl as T;
+ }
+ else
+ {
+ Error(decl, "\"{0}\" attribute specified for {1}, but it has already been specified for procedure {2}", attribute, decl.ToString(), attributedEntity.ToString());
+ }
+ }
+ else
+ {
+ Error(decl, "\"{0}\" attribute applied to wrong sort of declaration {1}", attribute, decl.ToString());
+ }
+ }
+
+ if (attributedEntity == null)
+ {
+ Error(program, "\"{0}\" attribute has not been specified for any procedure. You must mark exactly one procedure with this attribute", attribute);
+ }
+
+ return attributedEntity;
+ }
+
+
+ internal void AddBarrierId(int BarrierId)
+ {
+ BarrierIds.Add(BarrierId);
+ }
+
+ internal int MaxBarrierId()
+ {
+ int result = -1;
+ foreach (int i in BarrierIds)
+ {
+ if (i > result)
+ {
+ result = i;
+ }
+ }
+ return result;
+ }
+
+ internal HashSet<Variable> GetGlobalVariables()
+ {
+ return GloalVariables;
+ }
+
+ internal HashSet<Variable> GetTileStaticVariables()
+ {
+ return TileStaticVariables;
+ }
+
+ internal HashSet<Variable> GetThreadLocalVariables()
+ {
+ return ThreadLocalVariables;
+ }
+
+
+ private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)
+ {
+ Procedure attributedProcedure = null;
+
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))
+ {
+ continue;
+ }
+
+ if (decl is Procedure)
+ {
+ if (attributedProcedure == null)
+ {
+ attributedProcedure = decl as Procedure;
+ }
+ else
+ {
+ Error(decl, "\"{0}\" attribute specified for procedure {1}, but it has already been specified for procedure {2}", attribute, (decl as Procedure).Name, attributedProcedure.Name);
+ }
+
+ }
+ else
+ {
+ Error(decl, "\"{0}\" attribute can only be applied to a procedure", attribute);
+ }
+ }
+
+ if (attributedProcedure == null)
+ {
+ Error(program, "\"{0}\" attribute has not been specified for any procedure. You must mark exactly one procedure with this attribute", attribute);
+ }
+
+ return attributedProcedure;
+ }
+
+ public void AddInitialAndFinalBarriers()
+ {
+ // Add barrier to start of first block, if it doesn't already start with a barrier
+ if (!IsBarrier(KernelImplementation.Blocks[0].Cmds[0]))
+ {
+ CmdSeq NewCmds = new CmdSeq();
+ NewCmds.Add(MakeBarrierCmd(0));
+ foreach (Cmd C in KernelImplementation.Blocks[0].Cmds)
+ {
+ NewCmds.Add(C);
+ }
+ KernelImplementation.Blocks[0].Cmds = NewCmds;
+ }
+
+ CmdSeq FinalBarrierCmdSeq = new CmdSeq();
+
+ int FinalBarrierId = MaxBarrierId() + 1;
+
+ FinalBarrierCmdSeq.Add(MakeBarrierCmd(FinalBarrierId));
+
+ string FinalBarrierLabel = "barrier_label" + FinalBarrierId;
+
+ Block FinalBarrierBlock = new Block(Token.NoToken, FinalBarrierLabel, FinalBarrierCmdSeq, new ReturnCmd(Token.NoToken));
+
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (B.TransferCmd is ReturnCmd)
+ {
+ BlockSeq BlockSeq = new BlockSeq();
+ BlockSeq.Add(FinalBarrierBlock);
+ StringSeq StringSeq = new StringSeq();
+ StringSeq.Add(FinalBarrierLabel);
+ B.TransferCmd = new GotoCmd(Token.NoToken, StringSeq, BlockSeq);
+ }
+ }
+
+ KernelImplementation.Blocks.Add(FinalBarrierBlock);
+
+ }
+
+ private Cmd MakeBarrierCmd(int BarrierId)
+ {
+ Debug.Assert(!BarrierIds.Contains(BarrierId));
+ AddBarrierId(BarrierId);
+ CallCmd Result = new CallCmd(Token.NoToken, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());
+ Result.Attributes = new QKeyValue(Token.NoToken, "barrier_id", new List<object>(new object[] { Expr.Literal(BarrierId) }), null);
+ return Result;
+ }
+
+
+ private static Implementation CloneImplementation(Implementation Impl, string NewName)
+ {
+ Implementation Result = new Implementation(Impl.tok, NewName, Impl.TypeParameters, Impl.InParams, Impl.OutParams, Impl.LocVars, new List<Block>());
+
+ Dictionary<Block, Block> OldToNew = new Dictionary<Block, Block>();
+
+ foreach (Block B in Impl.Blocks)
+ {
+ Block NewB = CloneBlock(B);
+
+ OldToNew.Add(B, NewB);
+
+ Result.Blocks.Add(NewB);
+
+ }
+
+ foreach (Block NewB in Result.Blocks)
+ {
+ if (NewB.TransferCmd is GotoCmd)
+ {
+ GotoCmd NewGotoCmd = NewB.TransferCmd as GotoCmd;
+
+ for (int i = 0; i < NewGotoCmd.labelTargets.Length; i++)
+ {
+ Block NewSuccessor;
+ bool found = OldToNew.TryGetValue(NewGotoCmd.labelTargets[i], out NewSuccessor);
+ Debug.Assert(found);
+
+ NewGotoCmd.labelTargets[i] = NewSuccessor;
+ }
+
+ }
+ }
+
+ return Result;
+ }
+
+
+ private static Block CloneBlock(Block B)
+ {
+ Block NewB = new Block(B.tok, B.Label, new CmdSeq(), null);
+
+ foreach (Cmd C in B.Cmds)
+ {
+ NewB.Cmds.Add(C); // The contents of each command is *not* cloned
+ }
+
+ if (B.TransferCmd is ReturnCmd)
+ {
+ NewB.TransferCmd = new ReturnCmd((B.TransferCmd as ReturnCmd).tok);
+ }
+ else
+ {
+ GotoCmd GotoCmd = B.TransferCmd as GotoCmd;
+ NewB.TransferCmd = new GotoCmd(GotoCmd.tok, new StringSeq(), new BlockSeq());
+ GotoCmd NewGotoCmd = NewB.TransferCmd as GotoCmd;
+ for (int i = 0; i < GotoCmd.labelNames.Length; i++)
+ {
+ NewGotoCmd.labelNames.Add(GotoCmd.labelNames[i]);
+ NewGotoCmd.labelTargets.Add(GotoCmd.labelTargets[i]);
+ }
+ }
+ return NewB;
+ }
+
+
+ private static void AppendDuplicateBlockToStartOfImplementation(Implementation Impl, int i)
+ {
+ Block NewBlock = CloneBlock(Impl.Blocks[i]);
+
+ List<Block> NewBlocks = new List<Block>();
+
+ NewBlocks.Add(NewBlock);
+
+ foreach (Block B in Impl.Blocks)
+ {
+ NewBlocks.Add(B);
+ }
+
+ Impl.Blocks = NewBlocks;
+
+ }
+
+ private Implementation ConstructBarrierToNextBarriersImplementation(Block B, String NewProcedureName)
+ {
+ Implementation NewImplementation = CloneImplementation(KernelImplementation, NewProcedureName);
+
+ AppendDuplicateBlockToStartOfImplementation(NewImplementation, KernelImplementation.Blocks.IndexOf(B));
+
+ // Iterate through all blocks except first, immediately following barrier calls with "return"
+
+ for (int i = 1; i < NewImplementation.Blocks.Count; i++)
+ {
+ if (IsBarrier(NewImplementation.Blocks[i]))
+ {
+ // This is a barrier so we don't want control to get any further.
+ // To ensure this, we simply remove any commands following the barrier,
+ // and make the transfer command into a "return".
+ CmdSeq NewCmdSeq = new CmdSeq();
+ NewCmdSeq.Add(NewImplementation.Blocks[i].Cmds[0]);
+ NewImplementation.Blocks[i].Cmds = NewCmdSeq;
+ NewImplementation.Blocks[i].TransferCmd = new ReturnCmd(Token.NoToken);
+ }
+ }
+
+ NewImplementation.PruneUnreachableBlocks();
+ return NewImplementation;
+ }
+
+ private void SanityCheckKernel()
+ {
+ foreach (Block C in KernelImplementation.Blocks)
+ {
+ if (C.TransferCmd is GotoCmd)
+ {
+ foreach (Block D in (C.TransferCmd as GotoCmd).labelTargets)
+ {
+ Debug.Assert(KernelImplementation.Blocks.Contains(D));
+ }
+ }
+ }
+ }
+
+
+ private void ComputeBarrierToNextBarriersProcedure(Block B)
+ {
+ SanityCheckKernel();
+ Debug.Assert(IsBarrier(B));
+
+ String NewProcedureName = "Barrier_" + GetBarrierId(B) + "_to_next_barriers";
+ Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);
+ Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName);
+
+ InstrumentWithRaceDetection(NewImplementation);
+
+ Program.TopLevelDeclarations.Add(NewProcedure);
+ Program.TopLevelDeclarations.Add(NewImplementation);
+
+ }
+
+ private void InstrumentWithRaceDetection(Implementation Impl)
+ {
+ foreach (Block B in Impl.Blocks)
+ {
+ CmdSeq NewCmds = new CmdSeq();
+
+ foreach (Cmd C in B.Cmds)
+ {
+ ReadCollector rc = new ReadCollector(this);
+ rc.Visit(C);
+ WriteCollector wc = new WriteCollector(this);
+ wc.Visit(C);
+
+ if (wc.FoundWrite())
+ {
+ AccessRecord write = wc.GetAccess();
+ ExprSeq InParams = ConstructLogAccessParameters(C, write);
+ NewCmds.Add(new CallCmd(C.tok, "LOG_WRITE", InParams, new IdentifierExprSeq()));
+ }
+
+ foreach (AccessRecord read in rc.accesses)
+ {
+ ExprSeq InParams = ConstructLogAccessParameters(C, read);
+ NewCmds.Add(new CallCmd(C.tok, "LOG_READ", InParams, new IdentifierExprSeq()));
+ }
+
+ NewCmds.Add(C);
+ }
+ B.Cmds = NewCmds;
+ }
+ }
+
+ private ExprSeq ConstructLogAccessParameters(Cmd C, AccessRecord access)
+ {
+ ExprSeq InParams = new ExprSeq();
+ InParams.Add(new IdentifierExpr(C.tok, new GlobalVariable(C.tok, new TypedIdent(C.tok, access.v.Name + "_base", Microsoft.Boogie.Type.Int))));
+ InParams.Add(access.IndexZ);
+ InParams.Add(access.IndexY);
+ InParams.Add(access.IndexX);
+ InParams.Add(MakeThreadIdExpr(C.tok));
+ return InParams;
+ }
+
+ private void ComputeBarrierAToBarrierBProcedure(Block A, Block B)
+ {
+ Debug.Assert(IsBarrier(A));
+ Debug.Assert(IsBarrier(B));
+
+ String NewProcedureName = "Barrier_" + GetBarrierId(A) + "_to_" + GetBarrierId(B);
+ Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);
+ Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, NewProcedureName);
+
+ Block NewA = NewImplementation.Blocks[0];
+ Block NewB = null;
+ for (int i = 1; i < NewImplementation.Blocks.Count; i++)
+ {
+ if (IsBarrier(NewImplementation.Blocks[i]) && GetBarrierId(B) == GetBarrierId(NewImplementation.Blocks[i]))
+ {
+ NewB = NewImplementation.Blocks[i];
+ break;
+ }
+ }
+ if (NewB == null)
+ {
+ // No path between the barriers -- nothing to do
+ return;
+ }
+
+ NewImplementation.ComputePredecessorsForBlocks();
+
+ HashSet<Block> NodesToKeep = BlocksReaching(NewB);
+
+ Debug.Assert(NodesToKeep.Count > 1);
+
+ foreach (Block D in NewImplementation.Blocks)
+ {
+ if (D.TransferCmd is GotoCmd)
+ {
+ GotoCmd GotoCmd = D.TransferCmd as GotoCmd;
+ GotoCmd NewGotoCmd = new GotoCmd(GotoCmd.tok, new StringSeq(), new BlockSeq());
+ for (int i = 0; i < GotoCmd.labelNames.Length; i++)
+ {
+ if (NodesToKeep.Contains(GotoCmd.labelTargets[i]))
+ {
+ NewGotoCmd.labelNames.Add(GotoCmd.labelNames[i]);
+ NewGotoCmd.labelTargets.Add(GotoCmd.labelTargets[i]);
+ }
+ }
+ D.TransferCmd = NewGotoCmd;
+ }
+ }
+
+ NewImplementation.PruneUnreachableBlocks();
+
+ Program.TopLevelDeclarations.Add(NewProcedure);
+ Program.TopLevelDeclarations.Add(NewImplementation);
+
+ }
+
+ private static HashSet<Block> BlocksReaching(Block B)
+ {
+ HashSet<Block> Result = new HashSet<Block>();
+ ComputeReachingBlocksRecursive(B, Result);
+ return Result;
+ }
+
+ private static void ComputeReachingBlocksRecursive(Block B, HashSet<Block> Result)
+ {
+ if (Result.Contains(B))
+ {
+ return;
+ }
+
+ Result.Add(B);
+ foreach (Block C in B.Predecessors)
+ {
+ ComputeReachingBlocksRecursive(C, Result);
+ }
+ }
+
+ private static HashSet<Block> BlocksReachableFrom(Block B)
+ {
+ HashSet<Block> Result = new HashSet<Block>();
+ ComputeReachableBlocksRecursive(B, Result);
+ return Result;
+ }
+
+ private static void ComputeReachableBlocksRecursive(Block B, HashSet<Block> Result)
+ {
+ if (Result.Contains(B))
+ {
+ return;
+ }
+ Result.Add(B);
+ if (B.TransferCmd is GotoCmd)
+ {
+ foreach (Block C in (B.TransferCmd as GotoCmd).labelTargets)
+ {
+ ComputeReachableBlocksRecursive(C, Result);
+ }
+ }
+ }
+
+
+
+
+ private Block FindBarrierBlock(Implementation Impl, int BarrierId)
+ {
+ foreach (Block B in Impl.Blocks)
+ {
+ if (B.Cmds.Length > 0 && IsBarrier(B.Cmds[0]) && GetBarrierId(B) == BarrierId)
+ {
+ return B;
+ }
+ }
+
+ Debug.Assert(false);
+
+ return null;
+ }
+
+ private int GetBarrierId(Cmd C)
+ {
+ Debug.Assert(IsBarrier(C));
+ return QKeyValue.FindIntAttribute((C as CallCmd).Attributes, "barrier_id", -1);
+ }
+
+ public int GetBarrierId(Block A)
+ {
+ Debug.Assert(A.Cmds.Length > 0);
+ return GetBarrierId(A.Cmds[0]);
+ }
+
+ public bool IsBarrier(Cmd C)
+ {
+ return C is CallCmd && (C as CallCmd).callee == BarrierProcedure.Name;
+ }
+
+ public bool IsBarrier(Block B)
+ {
+ return B.Cmds.Length > 0 && IsBarrier(B.Cmds[0]);
+ }
+
+
+
+
+ public void SplitBlocksAtBarriers()
+ {
+
+ int NumBlocksBeforeSplitting = KernelImplementation.Blocks.Count;
+
+ for (int i = 0; i < NumBlocksBeforeSplitting; i++)
+ {
+ Block B = KernelImplementation.Blocks[i];
+
+ List<CmdSeq> Segments = new List<CmdSeq>();
+ CmdSeq CurrentSequence = new CmdSeq();
+ foreach (Cmd C in B.Cmds)
+ {
+ if (IsBarrier(C))
+ {
+ if (CurrentSequence.Length > 0)
+ {
+ Segments.Add(CurrentSequence);
+ CurrentSequence = new CmdSeq();
+ }
+ }
+
+ CurrentSequence.Add(C);
+ }
+ if (CurrentSequence.Length > 0)
+ {
+ Segments.Add(CurrentSequence);
+ }
+
+ if (Segments.Count > 1)
+ {
+ TransferCmd OriginalTransferCmd = B.TransferCmd;
+
+ // Set the block's commands to be the first command sequence
+ B.Cmds = Segments[0];
+ B.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq());
+ Block LastBlock = B;
+ for (int j = 1; j < Segments.Count; j++)
+ {
+ Block NewBlock = new Block(Token.NoToken, "barrier_label_" + GetBarrierId(Segments[j][0]), Segments[j], new GotoCmd(Token.NoToken, new BlockSeq()));
+ KernelImplementation.Blocks.Add(NewBlock);
+ (LastBlock.TransferCmd as GotoCmd).AddTarget(NewBlock);
+ LastBlock = NewBlock;
+ }
+ LastBlock.TransferCmd = OriginalTransferCmd;
+
+ }
+
+ }
+ }
+
+ private bool ContainsInternalBarrier(Block B)
+ {
+ bool first = true;
+ foreach (Cmd C in B.Cmds)
+ {
+ if (first)
+ {
+ first = false;
+ continue;
+ }
+
+ if (C is CallCmd)
+ {
+ CallCmd Call = C as CallCmd;
+ if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "barrier"))
+ {
+ return true;
+ }
+ }
+
+ }
+
+ return false;
+ }
+
+
+
+ internal Implementation GetKernel()
+ {
+ return KernelImplementation;
+ }
+
+ internal void ComputeBarrierToNextBarriersProcedures()
+ {
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))
+ {
+ ComputeBarrierToNextBarriersProcedure(B);
+ }
+ }
+ }
+
+ internal void ComputeBarrierToBarrierPairs()
+ {
+ foreach (Block A in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(A))
+ {
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(B))
+ {
+ ComputeBarrierAToBarrierBProcedure(A, B);
+ }
+ }
+ }
+ }
+ }
+
+ internal IdentifierExpr MakeThreadIdExpr(IToken tok)
+ {
+ return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, ThreadIdParameterName, ThreadIdType)));
+ }
+
+
+ }
+
+}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj new file mode 100644 index 00000000..407ebe5f --- /dev/null +++ b/Source/GPUVerify/GPUVerify.csproj @@ -0,0 +1,86 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>
+ <OutputType>Exe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>GPUVerify</RootNamespace>
+ <AssemblyName>GPUVerify</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <FileAlignment>512</FileAlignment>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="AccessCollector.cs" />
+ <Compile Include="AccessRecord.cs" />
+ <Compile Include="CommandLineOptions.cs" />
+ <Compile Include="GPUVerifier.cs" />
+ <Compile Include="LocalVariableAccessReplacer.cs" />
+ <Compile Include="Main.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="ReadCollector.cs" />
+ <Compile Include="WriteCollector.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\AIFramework\AIFramework.csproj">
+ <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
+ <Name>AIFramework</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\BoogieDriver\BoogieDriver.csproj">
+ <Project>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</Project>
+ <Name>BoogieDriver</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</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.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/GPUVerify/LocalVariableAccessReplacer.cs b/Source/GPUVerify/LocalVariableAccessReplacer.cs new file mode 100644 index 00000000..4ec382ad --- /dev/null +++ b/Source/GPUVerify/LocalVariableAccessReplacer.cs @@ -0,0 +1,54 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class LocalVariableAccessReplacer : StandardVisitor
+ {
+
+ GPUVerifier verifier;
+
+ public LocalVariableAccessReplacer(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ }
+
+
+ public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
+ {
+ if (verifier.GetThreadLocalVariables().Contains(node.AssignedVariable.Decl))
+ {
+ List<Expr> indexes = new List<Expr>();
+ indexes.Add(verifier.MakeThreadIdExpr(node.tok));
+ return new MapAssignLhs(node.tok, node, indexes);
+ }
+ return node;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ if (verifier.GetThreadLocalVariables().Contains(node.Decl))
+ {
+ Console.WriteLine("Replacing " + node);
+
+ ExprSeq MapNameAndThreadID = new ExprSeq();
+ MapNameAndThreadID.Add(new IdentifierExpr(node.tok, node.Decl));
+ MapNameAndThreadID.Add(verifier.MakeThreadIdExpr(node.tok));
+
+ Expr result = new NAryExpr(node.tok, new MapSelect(node.tok, 1), MapNameAndThreadID);
+
+ Console.WriteLine("with " + result);
+ return result;
+
+ }
+
+ return node;
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs new file mode 100644 index 00000000..7c72a87c --- /dev/null +++ b/Source/GPUVerify/Main.cs @@ -0,0 +1,175 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.IO;
+using System.Diagnostics;
+
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class GPUVerify
+ {
+
+
+ public static void Main(string[] args)
+ {
+ CommandLineOptions.Parse(args);
+
+ if (CommandLineOptions.inputFiles.Count < 1)
+ {
+ OnlyBoogie.ErrorWriteLine("*** Error: No input files were specified.");
+ Environment.Exit(1);
+ }
+
+ foreach (string file in CommandLineOptions.inputFiles)
+ {
+ string extension = Path.GetExtension(file);
+ if (extension != null)
+ {
+ extension = extension.ToLower();
+ }
+ if (extension != ".bpl")
+ {
+ OnlyBoogie.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
+ extension == null ? "" : extension);
+ Environment.Exit(1);
+ }
+ }
+
+ Program program = ParseBoogieProgram(CommandLineOptions.inputFiles, false);
+ if (program == null)
+ {
+ Environment.Exit(1);
+ }
+
+ int errorCount = program.Resolve();
+ if (errorCount != 0)
+ {
+ Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
+ Environment.Exit(1);
+ }
+
+ errorCount = program.Typecheck();
+
+ if (errorCount != 0)
+ {
+ Console.WriteLine("{0} type checking errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
+ Environment.Exit(1);
+ }
+
+ GPUVerifier verifier = new GPUVerifier(program);
+
+ // TODO: check that no non-barrier procedures are called from the kernel
+
+ verifier.AddInitialAndFinalBarriers();
+
+ verifier.SplitBlocksAtBarriers();
+
+ verifier.ComputeBarrierToNextBarriersProcedures();
+
+ verifier.ComputeBarrierToBarrierPairs();
+
+ foreach (Variable V in verifier.GetGlobalVariables())
+ {
+ program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true));
+ }
+
+ foreach (Variable V in verifier.GetTileStaticVariables())
+ {
+ program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true));
+ }
+
+ using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))
+ {
+ program.Emit(writer);
+ }
+
+
+ /* errorCount = program.Resolve();
+ if (errorCount != 0)
+ {
+ Console.WriteLine("{0} name resolution errors detected in {1} after transformation", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
+ Environment.Exit(1);
+ }
+
+ errorCount = program.Typecheck();
+
+ if (errorCount != 0)
+ {
+ Console.WriteLine("{0} type checking errors detected in {1} after transformation", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
+ Environment.Exit(1);
+ }
+ */
+ //Console.ReadLine();
+
+ }
+
+ private static CtorType MakeArrayBaseType(Variable V)
+ {
+ return new CtorType(V.tok, new TypeCtorDecl(V.tok, "ArrayBase", 0), new TypeSeq());
+ }
+
+
+
+
+
+
+ static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)
+ {
+ Program program = null;
+ bool okay = true;
+ for (int fileId = 0; fileId < fileNames.Count; fileId++)
+ {
+ string bplFileName = fileNames[fileId];
+
+ Program programSnippet;
+ int errorCount;
+ try
+ {
+ var defines = new List<string>() { "FILE_" + fileId };
+ errorCount = Parser.Parse(bplFileName, defines, out programSnippet);
+ if (programSnippet == null || errorCount != 0)
+ {
+ OnlyBoogie.ErrorWriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
+ okay = false;
+ continue;
+ }
+ }
+ catch (IOException e)
+ {
+ OnlyBoogie.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
+ okay = false;
+ continue;
+ }
+ if (program == null)
+ {
+ program = programSnippet;
+ }
+ else if (programSnippet != null)
+ {
+ program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);
+ }
+ }
+ if (!okay)
+ {
+ return null;
+ }
+ else if (program == null)
+ {
+ return new Program();
+ }
+ else
+ {
+ return program;
+ }
+ }
+
+
+ }
+
+
+
+
+}
diff --git a/Source/GPUVerify/Properties/AssemblyInfo.cs b/Source/GPUVerify/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..cff5de61 --- /dev/null +++ b/Source/GPUVerify/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("GPUVerify")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("Microsoft")]
+[assembly: AssemblyProduct("GPUVerify")]
+[assembly: AssemblyCopyright("Copyright © Microsoft 2011")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("2cda06c5-da64-412f-9c94-7edc5fd9147f")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs new file mode 100644 index 00000000..e7fd1eee --- /dev/null +++ b/Source/GPUVerify/ReadCollector.cs @@ -0,0 +1,115 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+
+
+
+
+ class ReadCollector : AccessCollector
+ {
+
+ public HashSet<AccessRecord> accesses = new HashSet<AccessRecord>();
+
+ public ReadCollector(GPUVerifier verifier)
+ : base(verifier)
+ {
+ }
+
+ public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
+ {
+ return node;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is MapSelect)
+ {
+ if ((node.Fun as MapSelect).Arity > 1)
+ {
+ MultiDimensionalMapError();
+ }
+
+ Variable ReadVariable = null;
+ Expr IndexX = node.Args[1];
+ Expr IndexY = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));
+ Expr IndexZ = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));
+
+ if (node.Args[0] is NAryExpr)
+ {
+ NAryExpr nestedMap = node.Args[0] as NAryExpr;
+ Debug.Assert(nestedMap.Fun is MapSelect);
+ if ((nestedMap.Fun as MapSelect).Arity > 1)
+ {
+ MultiDimensionalMapError();
+ }
+ IndexY = nestedMap.Args[1];
+ if (nestedMap.Args[0] is NAryExpr)
+ {
+ NAryExpr nestedNestedMap = nestedMap.Args[0] as NAryExpr;
+ Debug.Assert(nestedNestedMap.Fun is MapSelect);
+ if ((nestedNestedMap.Fun as MapSelect).Arity > 1)
+ {
+ MultiDimensionalMapError();
+ }
+ IndexZ = nestedMap.Args[1];
+ if (!(nestedNestedMap.Args[0] is IdentifierExpr))
+ {
+ Console.WriteLine("*** Error - maps with more than three levels of nesting are not supported");
+ Environment.Exit(1);
+ }
+ ReadVariable = (nestedNestedMap.Args[0] as IdentifierExpr).Decl;
+ this.VisitExpr(nestedNestedMap.Args[1]);
+ }
+ else
+ {
+ Debug.Assert(nestedMap.Args[0] is IdentifierExpr);
+ ReadVariable = (nestedMap.Args[0] as IdentifierExpr).Decl;
+ }
+ this.VisitExpr(nestedMap.Args[1]);
+
+ }
+ else
+ {
+ Debug.Assert(node.Args[0] is IdentifierExpr);
+ ReadVariable = (node.Args[0] as IdentifierExpr).Decl;
+ }
+ this.VisitExpr(node.Args[1]);
+
+
+ if (verifier.GetGlobalVariables().Contains(ReadVariable) || verifier.GetTileStaticVariables().Contains(ReadVariable))
+ {
+ accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));
+ }
+
+ return node;
+ }
+ else
+ {
+ return base.VisitNAryExpr(node);
+ }
+ }
+
+
+
+ public override Variable VisitVariable(Variable node)
+ {
+ if (!(verifier.GetGlobalVariables().Contains(node) || verifier.GetTileStaticVariables().Contains(node)))
+ {
+ return node;
+ }
+
+ accesses.Add(new AccessRecord(node, new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0))));
+
+ return node;
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs new file mode 100644 index 00000000..e91244cb --- /dev/null +++ b/Source/GPUVerify/WriteCollector.cs @@ -0,0 +1,107 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify
+{
+ class WriteCollector : AccessCollector
+ {
+
+ private AccessRecord access = null;
+
+ public WriteCollector(GPUVerifier verifier)
+ : base(verifier)
+ {
+ }
+
+ public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
+ {
+ Debug.Assert(NoWrittenVariable());
+ if (verifier.GetGlobalVariables().Contains(node.DeepAssignedVariable) || verifier.GetTileStaticVariables().Contains(node.DeepAssignedVariable))
+ {
+ access = new AccessRecord(node.DeepAssignedVariable, new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)));
+ }
+ return node;
+ }
+
+ private bool NoWrittenVariable()
+ {
+ return access == null;
+ }
+
+ public override AssignLhs VisitMapAssignLhs(MapAssignLhs node)
+ {
+ Debug.Assert(NoWrittenVariable());
+
+ if (!(verifier.GetGlobalVariables().Contains(node.DeepAssignedVariable) || verifier.GetTileStaticVariables().Contains(node.DeepAssignedVariable)))
+ {
+ return node;
+ }
+
+ Variable WrittenVariable = node.DeepAssignedVariable;
+
+ MapAssignLhs MapAssignX = node;
+
+ CheckMapIndex(MapAssignX);
+ Expr IndexX = MapAssignX.Indexes[0];
+ Expr IndexY = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));
+ Expr IndexZ = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));
+
+ if (MapAssignX.Map is MapAssignLhs)
+ {
+ MapAssignLhs MapAssignY = MapAssignX.Map as MapAssignLhs;
+ CheckMapIndex(MapAssignY);
+ IndexY = MapAssignY.Indexes[0];
+ if (MapAssignY.Map is MapAssignLhs)
+ {
+ MapAssignLhs MapAssignZ = MapAssignY.Map as MapAssignLhs;
+ CheckMapIndex(MapAssignZ);
+ IndexZ = MapAssignZ.Indexes[0];
+ if (!(MapAssignZ.Map is SimpleAssignLhs))
+ {
+ Console.WriteLine("*** Error - maps with more than three levels of nesting are not supported");
+ Environment.Exit(1);
+ }
+ }
+ else
+ {
+ Debug.Assert(MapAssignY.Map is SimpleAssignLhs);
+ }
+ }
+ else
+ {
+ Debug.Assert(MapAssignX.Map is SimpleAssignLhs);
+ }
+
+ access = new AccessRecord(WrittenVariable, IndexZ, IndexY, IndexX);
+
+ return MapAssignX;
+ }
+
+ private void CheckMapIndex(MapAssignLhs node)
+ {
+ if (node.Indexes.Count > 1)
+ {
+ MultiDimensionalMapError();
+ }
+ }
+
+
+
+
+ internal bool FoundWrite()
+ {
+ return access != null;
+ }
+
+ internal AccessRecord GetAccess()
+ {
+ return access;
+ }
+
+ }
+}
|