diff options
Diffstat (limited to 'Source/GPUVerify/GPUVerifier.cs')
-rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 46 |
1 files changed, 13 insertions, 33 deletions
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)
|