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)