diff options
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 12 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 522 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 16 | ||||
| -rw-r--r-- | Source/GPUVerify/Scripts/GPUVerifyDriver.bat | 60 |
4 files changed, 574 insertions, 36 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 812d9f20..ecbee795 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -14,6 +14,7 @@ namespace GPUVerify public static List<string> inputFiles = new List<string>();
public static string outputFile = null;
+ public static string formulaSkeletonsFile = null;
public static int Parse(string[] args)
{
@@ -44,6 +45,17 @@ namespace GPUVerify outputFile = afterColon;
break;
+ case "-generateFormulaSkeletons":
+ case "/generateFormulaSkeletons":
+ if (!hasColonArgument)
+ {
+ Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
+ Environment.Exit(1);
+ }
+ Debug.Assert(afterColon != null);
+ formulaSkeletonsFile = afterColon;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index f90e521e..8ea3cdfd 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -4,6 +4,7 @@ using System.Linq; using System.Text;
using System.Diagnostics;
using Microsoft.Boogie;
+using Microsoft.Basetypes;
namespace GPUVerify
{
@@ -21,9 +22,9 @@ namespace GPUVerify 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>();
+ private List<Variable> ThreadLocalVariables = new List<Variable>();
+ private List<Variable> TileStaticVariables = new List<Variable>();
+ private List<Variable> GlobalVariables = new List<Variable>();
public GPUVerifier(Program program)
@@ -36,6 +37,7 @@ namespace GPUVerify ReservedNames.Add("offset_x");
ReservedNames.Add("offset_y");
ReservedNames.Add("offset_z");
+ ReservedNames.Add("is_write");
ReservedNames.Add("AT_BARRIER");
CheckWellFormedness();
@@ -88,7 +90,7 @@ namespace GPUVerify {
if (!ReservedNames.Contains((D as Variable).Name))
{
- GloalVariables.Add(D as Variable);
+ GlobalVariables.Add(D as Variable);
}
}
}
@@ -283,17 +285,17 @@ namespace GPUVerify return result;
}
- internal HashSet<Variable> GetGlobalVariables()
+ internal List<Variable> GetGlobalVariables()
{
- return GloalVariables;
+ return GlobalVariables;
}
- internal HashSet<Variable> GetTileStaticVariables()
+ internal List<Variable> GetTileStaticVariables()
{
return TileStaticVariables;
}
- internal HashSet<Variable> GetThreadLocalVariables()
+ internal List<Variable> GetThreadLocalVariables()
{
return ThreadLocalVariables;
}
@@ -510,29 +512,39 @@ namespace GPUVerify }
- private void ComputeBarrierToNextBarriersProcedure(Block B)
+ private void GenerateBarrierToNextBarriersProcedure(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);
+ String NewProcedureName = MakeBarrierToNextBarriersProcedureName(B);
+ Procedure NewProcedure = CloneKernelProcedure(NewProcedureName);
- NewProcedure.Modifies.Add(MakeBaseVariable(B.tok));
- NewProcedure.Modifies.Add(MakeOffsetXVariable(B.tok));
- NewProcedure.Modifies.Add(MakeOffsetYVariable(B.tok));
- NewProcedure.Modifies.Add(MakeOffsetZVariable(B.tok));
- NewProcedure.Modifies.Add(MakeIsWriteVariable(B.tok));
+ AddTrackingVariablesToModifiesSet(B.tok, NewProcedure.Modifies);
+
+ AddInlineAttribute(NewProcedure);
Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName);
InstrumentWithRaceDetection(NewImplementation);
+ AddBarrierTracking(NewImplementation);
+
Program.TopLevelDeclarations.Add(NewProcedure);
Program.TopLevelDeclarations.Add(NewImplementation);
}
+ private string MakeBarrierToNextBarriersProcedureName(Block B)
+ {
+ return "Barrier_" + GetBarrierId(B) + "_to_next_barriers";
+ }
+
+ private string MakeBarrierAToBProcedureName(Block A, Block B)
+ {
+ return "Barrier_" + GetBarrierId(A) + "_to_" + GetBarrierId(B);
+ }
+
private static CtorType MakeArrayBaseType(IToken tok)
{
return new CtorType(tok, new TypeCtorDecl(tok, "ArrayBase", 0), new TypeSeq());
@@ -617,15 +629,24 @@ namespace GPUVerify return InParams;
}
- private void ComputeBarrierAToBarrierBProcedure(Block A, Block B)
+ private void GenerateBarrierAToBarrierBProcedure(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);
+ if (!BarrierReachesBarrier(A, B))
+ {
+ return;
+ }
+
+ String NewProcedureName = MakeBarrierAToBProcedureName(A, B);
+ Procedure NewProcedure = CloneKernelProcedure(NewProcedureName);
Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, NewProcedureName);
+ AddInlineAttribute(NewProcedure);
+
+ NewProcedure.Modifies.Add(MakeAtBarrierVariable(B.tok));
+
Block NewA = NewImplementation.Blocks[0];
Block NewB = null;
for (int i = 1; i < NewImplementation.Blocks.Count; i++)
@@ -636,11 +657,7 @@ namespace GPUVerify break;
}
}
- if (NewB == null)
- {
- // No path between the barriers -- nothing to do
- return;
- }
+ Debug.Assert(NewB != null);
NewImplementation.ComputePredecessorsForBlocks();
@@ -668,11 +685,116 @@ namespace GPUVerify NewImplementation.PruneUnreachableBlocks();
+ AddBarrierTracking(NewImplementation);
+
Program.TopLevelDeclarations.Add(NewProcedure);
Program.TopLevelDeclarations.Add(NewImplementation);
}
+ private bool BarrierReachesBarrier(Block A, Block B)
+ {
+ Debug.Assert(IsBarrier(A));
+ Debug.Assert(IsBarrier(B));
+
+ Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, "noname");
+
+ for (int i = 1; i < NewImplementation.Blocks.Count; i++)
+ {
+ if (IsBarrier(NewImplementation.Blocks[i]) && GetBarrierId(B) == GetBarrierId(NewImplementation.Blocks[i]))
+ {
+ return true;
+ }
+ }
+
+ return false;
+ }
+
+ private static void AddInlineAttribute(Procedure NewProcedure)
+ {
+ NewProcedure.AddAttribute("inline", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(1)) });
+ }
+
+ private Procedure CloneKernelProcedure(string NewProcedureName)
+ {
+ RequiresSeq NewRequiresSeq = new RequiresSeq();
+ foreach(Requires r in KernelProcedure.Requires)
+ {
+ NewRequiresSeq.Add(r);
+ }
+ EnsuresSeq NewEnsuresSeq = new EnsuresSeq();
+ foreach (Ensures e in KernelProcedure.Ensures)
+ {
+ NewEnsuresSeq.Add(e);
+ }
+ IdentifierExprSeq NewModifiesSeq = new IdentifierExprSeq();
+ foreach (IdentifierExpr ies in KernelProcedure.Modifies)
+ {
+ NewModifiesSeq.Add(ies);
+ }
+ return new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, NewRequiresSeq, NewModifiesSeq, NewEnsuresSeq);
+ }
+
+ private void AddBarrierTracking(Implementation Impl)
+ {
+ Debug.Assert(IsBarrier(Impl.Blocks[0]));
+ CmdSeq NewBlock0Commands = new CmdSeq();
+
+ NewBlock0Commands.Add(Impl.Blocks[0].Cmds[0]);
+
+ NewBlock0Commands.Add(MakeAssignToAtBarrier(Impl.Blocks[0].Cmds[0].tok, -1));
+
+ for (int i = 1; i < Impl.Blocks[0].Cmds.Length; i++)
+ {
+ NewBlock0Commands.Add(Impl.Blocks[0].Cmds[i]);
+ }
+
+ Impl.Blocks[0].Cmds = NewBlock0Commands;
+
+ for (int i = 1; i < Impl.Blocks.Count; i++)
+ {
+ if (IsBarrier(Impl.Blocks[i]))
+ {
+ // At this stage, the barrier should be followed immediately by a return
+ Debug.Assert(Impl.Blocks[i].Cmds.Length == 1);
+
+ Impl.Blocks[i].Cmds.Add(MakeAssignToAtBarrier(Impl.Blocks[i].Cmds[0].tok, GetBarrierId(Impl.Blocks[i])));
+
+ }
+ }
+
+
+
+
+ }
+
+ private AssignCmd MakeAssignToAtBarrier(IToken tok, int p)
+ {
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ List<Expr> rhss = new List<Expr>();
+
+ List<Expr> indexes = new List<Expr>();
+ indexes.Add(MakeThreadIdExpr(tok, "i"));
+ lhss.Add(new MapAssignLhs(tok, new SimpleAssignLhs(tok, MakeAtBarrierVariable(tok)), indexes));
+ rhss.Add(new LiteralExpr(tok, BigNum.FromInt(p)));
+ return new AssignCmd(tok, lhss, rhss);
+ }
+
+ private NAryExpr MakeAtBarrierAccess(IToken tok, string ThreadIdName)
+ {
+ ExprSeq args = new ExprSeq();
+ args.Add(MakeAtBarrierVariable(tok));
+ args.Add(MakeThreadIdExpr(tok, ThreadIdName));
+ return new NAryExpr(tok, new MapSelect(tok, 1), args);
+ }
+
+ private IdentifierExpr MakeAtBarrierVariable(IToken tok)
+ {
+ TypeSeq IndexType = new TypeSeq();
+ IndexType.Add(ThreadIdType);
+ return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "AT_BARRIER", new MapType(tok, new TypeVariableSeq(), IndexType, Microsoft.Boogie.Type.Int))));
+ }
+
private static HashSet<Block> BlocksReaching(Block B)
{
HashSet<Block> Result = new HashSet<Block>();
@@ -843,18 +965,18 @@ namespace GPUVerify return KernelImplementation;
}
- internal void ComputeBarrierToNextBarriersProcedures()
+ internal void GenerateBarrierToNextBarriersProcedures()
{
foreach (Block B in KernelImplementation.Blocks)
{
if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))
{
- ComputeBarrierToNextBarriersProcedure(B);
+ GenerateBarrierToNextBarriersProcedure(B);
}
}
}
- internal void ComputeBarrierToBarrierPairs()
+ internal void GenerateBarrierToBarrierPairProcedures()
{
foreach (Block A in KernelImplementation.Blocks)
{
@@ -864,18 +986,22 @@ namespace GPUVerify {
if (IsBarrier(B))
{
- ComputeBarrierAToBarrierBProcedure(A, B);
+ GenerateBarrierAToBarrierBProcedure(A, B);
}
}
}
}
}
- internal IdentifierExpr MakeThreadIdExpr(IToken tok)
+ internal IdentifierExpr MakeThreadIdExpr(IToken tok, string name)
{
- return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, ThreadIdParameterName, ThreadIdType)));
+ return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, name, ThreadIdType)));
}
+ internal IdentifierExpr MakeThreadIdExpr(IToken tok)
+ {
+ return MakeThreadIdExpr(tok, ThreadIdParameterName);
+ }
internal void AddArrayBaseDeclarations()
@@ -890,6 +1016,342 @@ namespace GPUVerify Program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V.tok)), true));
}
}
+
+ internal void GenerateBarrierToNextBarriersVCs()
+ {
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))
+ {
+ GenerateBarrierToNextBarriersVC(B);
+ }
+ }
+ }
+
+ private void GenerateBarrierToNextBarriersVC(Block B)
+ {
+ VariableSeq InParams = new VariableSeq();
+ InParams.Add(new LocalVariable(B.tok, new TypedIdent(B.tok, "i", ThreadIdType)));
+ InParams.Add(new LocalVariable(B.tok, new TypedIdent(B.tok, "j", ThreadIdType)));
+
+ VariableSeq OutParams = new VariableSeq();
+
+ IdentifierExprSeq Modifies = new IdentifierExprSeq();
+ foreach (IdentifierExpr ie in KernelProcedure.Modifies)
+ {
+ Modifies.Add(ie);
+ }
+
+ AddTrackingVariablesToModifiesSet(B.tok, Modifies);
+
+ RequiresSeq Requires = new RequiresSeq();
+ Requires.Add(new Requires(false, MakePreconditionExpr(B)));
+ AddDistinctSameTile(B.tok, Requires, "i", "j");
+ AddNothingInitiallyTracked(B.tok, Requires, "i", "j");
+
+
+ EnsuresSeq Ensures = new EnsuresSeq();
+ AddNoRace(B.tok, Ensures, "i", "j");
+ AddSameBarrier(B.tok, Ensures, "i", "j");
+
+ string BarrierIsRaceAndDivergenceFree = "Check_Barrier_" + GetBarrierId(B) + "_Race_And_Divergence_Free";
+
+ Procedure NewProcedure = new Procedure(B.tok, BarrierIsRaceAndDivergenceFree, new TypeVariableSeq(), InParams, OutParams, Requires, Modifies, Ensures);
+
+ List<Block> Blocks = new List<Block>();
+
+ Blocks.Add(new Block());
+
+ Blocks[0].TransferCmd = new ReturnCmd(B.tok);
+
+ Blocks[0].Label = "entry";
+
+ Blocks[0].Cmds = new CmdSeq();
+
+ ExprSeq i = new ExprSeq();
+ i.Add(new IdentifierExpr(B.tok, new LocalVariable(B.tok, new TypedIdent(B.tok, "i", ThreadIdType))));
+ Blocks[0].Cmds.Add(new CallCmd(B.tok, MakeBarrierToNextBarriersProcedureName(B), i, new IdentifierExprSeq()));
+
+ ExprSeq j = new ExprSeq();
+ j.Add(new IdentifierExpr(B.tok, new LocalVariable(B.tok, new TypedIdent(B.tok, "j", ThreadIdType))));
+ Blocks[0].Cmds.Add(new CallCmd(B.tok, MakeBarrierToNextBarriersProcedureName(B), j, new IdentifierExprSeq()));
+
+ Implementation NewImplementation = new Implementation(B.tok, BarrierIsRaceAndDivergenceFree, new TypeVariableSeq(), InParams, OutParams, new VariableSeq(), Blocks);
+
+ Program.TopLevelDeclarations.Add(NewProcedure);
+ Program.TopLevelDeclarations.Add(NewImplementation);
+
+ }
+
+ private void AddNothingInitiallyTracked(IToken tok, RequiresSeq Requires, string i, string j)
+ {
+ Requires.Add(new Requires(false, Expr.And(BaseEqualsNothing(tok, i), BaseEqualsNothing(tok, j))));
+ }
+
+ private Expr BaseEqualsNothing(IToken tok, string i)
+ {
+ ExprSeq MapSelectArgs = new ExprSeq();
+ MapSelectArgs.Add(MakeBaseVariable(tok));
+ MapSelectArgs.Add(MakeThreadIdExpr(tok, i));
+ return Expr.Eq(new NAryExpr(tok, new MapSelect(tok, 1), MapSelectArgs), new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "nothing", MakeArrayBaseType(tok)))));
+ }
+
+ private void AddSameBarrier(IToken tok, EnsuresSeq Ensures, string i, string j)
+ {
+ ExprSeq args1 = new ExprSeq();
+ args1.Add(MakeAtBarrierVariable(tok));
+ args1.Add(MakeThreadIdExpr(tok, i));
+
+ ExprSeq args2 = new ExprSeq();
+ args2.Add(MakeAtBarrierVariable(tok));
+ args2.Add(MakeThreadIdExpr(tok, j));
+
+ Ensures.Add(new Ensures(false, Expr.Eq( new NAryExpr(tok, new MapSelect(tok, 1), args1), new NAryExpr(tok, new MapSelect(tok, 1), args2) ) ) );
+
+ }
+
+ private void AddNoRace(IToken tok, EnsuresSeq Ensures, string i, string j)
+ {
+ ExprSeq RaceArgs = new ExprSeq();
+ RaceArgs.Add(MakeBaseVariable(tok));
+ RaceArgs.Add(MakeOffsetZVariable(tok));
+ RaceArgs.Add(MakeOffsetYVariable(tok));
+ RaceArgs.Add(MakeOffsetXVariable(tok));
+ RaceArgs.Add(MakeIsWriteVariable(tok));
+ RaceArgs.Add(MakeThreadIdExpr(tok, i));
+ RaceArgs.Add(MakeThreadIdExpr(tok, j));
+
+ NAryExpr RaceExpr = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, "race", Microsoft.Boogie.Type.Bool)), RaceArgs);
+ Ensures.Add(new Ensures(false, Expr.Not(RaceExpr)));
+ }
+
+ private void AddDistinctSameTile(IToken tok, RequiresSeq Requires, string i, string j)
+ {
+ ExprSeq args = new ExprSeq();
+ args.Add(new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, i, ThreadIdType))));
+ args.Add(new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, j, ThreadIdType))));
+ Requires.Add(new Requires(false, new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, "distinct_same_tile", Microsoft.Boogie.Type.Bool)), args)));
+ }
+
+ private NAryExpr MakePreconditionExpr(Block B)
+ {
+ ExprSeq PreconditionArgs = new ExprSeq();
+ foreach (Variable v in MakeFormulaFunctionArguments(B.tok))
+ {
+ PreconditionArgs.Add(new IdentifierExpr(B.tok, v));
+ }
+
+ NAryExpr nary = new NAryExpr(B.tok, new FunctionCall(new IdentifierExpr(B.tok, MakePreconditionName(B), Microsoft.Boogie.Type.Bool)), PreconditionArgs);
+ return nary;
+ }
+
+ private void AddTrackingVariablesToModifiesSet(IToken tok, IdentifierExprSeq Modifies)
+ {
+ Modifies.Add(MakeBaseVariable(tok));
+ Modifies.Add(MakeOffsetXVariable(tok));
+ Modifies.Add(MakeOffsetYVariable(tok));
+ Modifies.Add(MakeOffsetZVariable(tok));
+ Modifies.Add(MakeIsWriteVariable(tok));
+ Modifies.Add(MakeAtBarrierVariable(tok));
+ }
+
+ internal void GenerateBarrierToBarrierPairVCs()
+ {
+ foreach (Block A in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(A))
+ {
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(B) && BarrierReachesBarrier(A, B))
+ {
+ GenerateBarrierAToBarrierBVCs(A, B);
+ }
+ }
+ }
+ }
+ }
+
+ private void GenerateBarrierAToBarrierBVCs(Block A, Block B)
+ {
+ GenerateVC_AToBPreconditionA(A, B);
+ GenerateVC_AToBInduction(A, B);
+ GenerateVC_AToBPreconditionB(A, B);
+ }
+
+ private ForallExpr MakeAllAtBarrierExpr(Block A)
+ {
+ VariableSeq i = new VariableSeq();
+ i.Add(MakeThreadIdExpr(A.tok, "i").Decl);
+ Expr body = Expr.Eq(MakeAtBarrierAccess(A.tok, "i"), new LiteralExpr(A.tok, BigNum.FromInt(GetBarrierId(A))));
+ ForallExpr forallexpr = new ForallExpr(A.tok, i, body);
+ return forallexpr;
+ }
+
+ private string MakeIHName(Block A, Block B)
+ {
+ return "IH_" + GetBarrierId(A) + "_" + GetBarrierId(B);
+ }
+
+
+ private NAryExpr MakeIHExpr(Block A, Block B)
+ {
+ ExprSeq IHArgs = new ExprSeq();
+ foreach (Variable v in MakeFormulaFunctionArguments(B.tok))
+ {
+ IHArgs.Add(new IdentifierExpr(B.tok, v));
+ }
+
+ NAryExpr nary = new NAryExpr(B.tok, new FunctionCall(new IdentifierExpr(A.tok, MakeIHName(A, B), Microsoft.Boogie.Type.Bool)), IHArgs);
+ return nary;
+ }
+
+ private Expr MakeThreadAtBarrierExpr(Block A, string p)
+ {
+ return Expr.Eq(MakeAtBarrierAccess(A.tok, "i"), new LiteralExpr(A.tok, BigNum.FromInt(GetBarrierId(A))));
+ }
+
+ private void GenerateVC_AToBPreconditionA(Block A, Block B)
+ {
+ string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Precondition_" + GetBarrierId(A);
+
+ Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ NewProcedure.Requires.Add(new Requires(false, MakePreconditionExpr(A)));
+ NewProcedure.Requires.Add(new Requires(false, MakeAllAtBarrierExpr(A)));
+ NewProcedure.Ensures.Add(new Ensures(false, MakeIHExpr(A, B)));
+
+ Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), new List<Block>());
+
+ Program.TopLevelDeclarations.Add(NewProcedure);
+ Program.TopLevelDeclarations.Add(NewImplementation);
+ }
+
+ private void GenerateVC_AToBInduction(Block A, Block B)
+ {
+ string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Induction";
+
+ VariableSeq InParams = new VariableSeq();
+ InParams.Add(MakeThreadIdExpr(A.tok).Decl);
+
+ IdentifierExprSeq Modifies = new IdentifierExprSeq();
+ foreach (IdentifierExpr ie in KernelProcedure.Modifies)
+ {
+ Modifies.Add(ie);
+ }
+
+ AddTrackingVariablesToModifiesSet(A.tok, Modifies);
+
+ Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), InParams, new VariableSeq(), new RequiresSeq(), Modifies, new EnsuresSeq());
+ NewProcedure.Requires.Add(new Requires(false, MakeIHExpr(A, B)));
+ NewProcedure.Requires.Add(new Requires(false, MakeThreadAtBarrierExpr(A, "i")));
+ NewProcedure.Ensures.Add(new Ensures(false, MakeIHExpr(A, B)));
+
+ Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), InParams, new VariableSeq(), new VariableSeq(), new List<Block>());
+ NewImplementation.Blocks.Add(new Block());
+ NewImplementation.Blocks[0].Label = "entry";
+ NewImplementation.Blocks[0].TransferCmd = new ReturnCmd(A.tok);
+ NewImplementation.Blocks[0].Cmds = new CmdSeq();
+ ExprSeq i = new ExprSeq();
+ i.Add(MakeThreadIdExpr(A.tok));
+ NewImplementation.Blocks[0].Cmds.Add(new CallCmd(A.tok, MakeBarrierAToBProcedureName(A, B), i, new IdentifierExprSeq()));
+
+ Program.TopLevelDeclarations.Add(NewProcedure);
+ Program.TopLevelDeclarations.Add(NewImplementation);
+ }
+
+ private void GenerateVC_AToBPreconditionB(Block A, Block B)
+ {
+ string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Precondition_" + GetBarrierId(B);
+
+ Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ NewProcedure.Requires.Add(new Requires(false, MakeIHExpr(A, B)));
+ NewProcedure.Requires.Add(new Requires(false, MakeAllAtBarrierExpr(B)));
+ NewProcedure.Ensures.Add(new Ensures(false, MakePreconditionExpr(B)));
+
+ Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), new List<Block>());
+
+ Program.TopLevelDeclarations.Add(NewProcedure);
+ Program.TopLevelDeclarations.Add(NewImplementation);
+
+ }
+
+ internal void GenerateFormulaSkeletons(string filename)
+ {
+ Program FormulaSkeletons = new Program();
+
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(B))
+ {
+ FormulaSkeletons.TopLevelDeclarations.Add(MakeSkeletonFormula(B, MakePreconditionName(B)));
+ }
+ }
+
+ foreach (Block A in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(A))
+ {
+ foreach (Block B in KernelImplementation.Blocks)
+ {
+ if (IsBarrier(B) && BarrierReachesBarrier(A, B))
+ {
+ FormulaSkeletons.TopLevelDeclarations.Add(MakeSkeletonFormula(B, MakeIHName(A, B)));
+ }
+ }
+ }
+ }
+
+ using (TokenTextWriter writer = new TokenTextWriter(filename))
+ {
+ FormulaSkeletons.Emit(writer);
+ }
+
+
+ }
+
+ private string MakePreconditionName(Block B)
+ {
+ return "Pre_" + GetBarrierId(B);
+ }
+
+ private Function MakeSkeletonFormula(Block B, string FunctionName)
+ {
+
+ Function precondition = new Function(B.tok, FunctionName, MakeFormulaFunctionArguments(B.tok), MakeFunctionReturnTemp(B.tok));
+
+ precondition.AddAttribute("inline", new object[] { });
+
+ precondition.Body = new LiteralExpr(B.tok, true);
+ return precondition;
+ }
+
+ private Variable MakeFunctionReturnTemp(IToken tok)
+ {
+ return new LocalVariable(tok, new TypedIdent(tok, "result", Microsoft.Boogie.Type.Bool));
+ }
+
+ private VariableSeq MakeFormulaFunctionArguments(IToken tok)
+ {
+ VariableSeq arguments = new VariableSeq();
+
+ foreach (Variable v in ThreadLocalVariables)
+ {
+ arguments.Add(v);
+ }
+
+ foreach (Variable v in TileStaticVariables)
+ {
+ arguments.Add(v);
+ }
+
+ foreach (Variable v in GlobalVariables)
+ {
+ arguments.Add(v);
+ }
+
+ arguments.Add(MakeAtBarrierVariable(tok).Decl);
+ return arguments;
+ }
}
}
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index a0576f45..90524bb1 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -67,9 +67,21 @@ namespace GPUVerify verifier.SplitBlocksAtBarriers();
- verifier.ComputeBarrierToNextBarriersProcedures();
- verifier.ComputeBarrierToBarrierPairs();
+ if (CommandLineOptions.formulaSkeletonsFile != null)
+ {
+ Console.WriteLine("Generating skeleton formulas to \"" + CommandLineOptions.formulaSkeletonsFile + "\" and exiting");
+ verifier.GenerateFormulaSkeletons(CommandLineOptions.formulaSkeletonsFile);
+ Environment.Exit(0);
+ }
+
+ verifier.GenerateBarrierToNextBarriersProcedures();
+
+ verifier.GenerateBarrierToBarrierPairProcedures();
+
+ verifier.GenerateBarrierToNextBarriersVCs();
+
+ verifier.GenerateBarrierToBarrierPairVCs();
verifier.AddArrayBaseDeclarations();
diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat index dda5ddcf..d81c0fc1 100644 --- a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat +++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat @@ -1,9 +1,61 @@ -echo off
+@ECHO OFF
-Boogie /noVerify /printUnstructured /print:temp_instrumented.bpl %1 %~p0..\BoogieLibrary\GPUVerifyLibrary.bpl
+set InputFile=""
+set SkeletonFile=""
+set ScriptDir=%~p0
+
+:Loop
+IF "%1"=="" GOTO Continue
+
+set temp=%1
+
+IF %temp:~0,26%==/generateFormulaSkeletons: GOTO SetSkeletonFile
+
+set InputFile=%1
+
+GOTO LastPartOfLoop
+
+:SetSkeletonFile
+
+set SkeletonFile=%temp:~26%
+
+:LastPartOfLoop
+
+SHIFT
+GOTO Loop
+:Continue
+
+IF %InputFile%=="" GOTO Error
+
+echo Preprocess
+Boogie /noVerify /printUnstructured /print:temp_unstructured.bpl %InputFile% %ScriptDir%..\BoogieLibrary\GPUVerifyLibrary.bpl
+
+IF %SkeletonFile%=="" GOTO Verify
+
+GOTO Generate
+
+
+
+
+:Verify
+echo Verify
GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl
+Boogie temp_ready_to_verify.bpl formulas.bpl /prover:smtlib
+del temp_unstructured.bpl
+GOTO End
+
+:Generate
+echo Generate
+GPUVerify temp_unstructured.bpl /generateFormulaSkeletons:%SkeletonFile%
+del temp_unstructured.bpl
+GOTO End
+
+:Error
+echo Error: Bad command line specified for GPUVerify
+GOTO End
+
+
-Boogie temp_ready_to_verify.bpl /prover:smtlib
-del temp_instrumented.bpl
+:End
\ No newline at end of file |