Refactoring, and work on race checking contracts

15 files changed, 584 insertions, 596 deletions

diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs
index 43491460..42ca5cc8 100644
--- a/Source/GPUVerify/AccessCollector.cs
+++ b/Source/GPUVerify/AccessCollector.cs
@@ -8,13 +8,11 @@ namespace GPUVerify
 {

     abstract class AccessCollector : StandardVisitor

     {

-        protected ICollection<Variable> GlobalVariables;

-        protected ICollection<Variable> TileStaticVariables;

+        protected INonLocalState NonLocalState;

 

-        public AccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

+        public AccessCollector(INonLocalState NonLocalState)

         {

-            this.GlobalVariables = GlobalVariables;

-            this.TileStaticVariables = TileStaticVariables;

+            this.NonLocalState = NonLocalState;

         }

 

         protected void MultiDimensionalMapError()

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 9e7ba32c..2f08477b 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -14,10 +14,7 @@ namespace GPUVerify
         public static List<string> inputFiles = new List<string>();

 

         public static string outputFile = null;

-        public static string formulaSkeletonsFile = null;

-        public static string formulasFile = null;

 

-        public static bool NewRaceDetectionMethod = false;

         public static bool OnlyDivergence = false;

         public static bool FullAbstraction;

         public static bool Inference;

@@ -49,6 +46,12 @@ namespace GPUVerify
 

                 switch (beforeColon)

                 {

+                    case "-help":

+                    case "/help":

+                    case "-?":

+                    case "/?":

+                    return -1;

+                    

                     case "-print":

                     case "/print":

                         if (!hasColonArgument)

@@ -60,34 +63,6 @@ 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;

-

-                    case "-formulas":

-                    case "/formulas":

-                    if (!hasColonArgument)

-                    {

-                        Console.WriteLine("Error: filename expected after " + beforeColon + " argument");

-                        Environment.Exit(1);

-                    }

-                    Debug.Assert(afterColon != null);

-                    formulasFile = afterColon;

-                    break;

-

-                    case "-newRaceDetectionMethod":

-                    case "/newRaceDetectionMethod":

-                    NewRaceDetectionMethod = true;

-

-                    break;

-

                     case "-onlyDivergence":

                     case "/onlyDivergence":

                     OnlyDivergence = true;

@@ -163,5 +138,35 @@ namespace GPUVerify
             return 0;

         }

 

+        private static bool printedHelp = false;

+

+        public static void Usage()

+        {

+            // Ensure that we only print the help message once

+            if (printedHelp)

+            {

+                return;

+            }

+            printedHelp = true;

+

+            Console.WriteLine(@"GPUVerify: usage:  GPUVerify [ option ... ] [ filename ... ]

+  where <option> is one of

+

+  /help            : this message

+  /fullAbstraction : apply full state abstraction

+  /onlyDivergence  : only check for divergence-freedom, not race-freedom

+  /symmetry        : apply symmetry breaking

+  /eager           : check races eagerly, rather than waiting for barrier

+  /inference:file  : use automatic invariant inference.  Optional file can include manually supplied candidates

+  /raceCheckingContract : try to infer race-freedom contracts for procedures

+  /setEncoding     : check races using set encoding

+  /divided         : check individual pairs of possibly racing statements separately

+  /dividedArray    : check races on arrays one at a time

+  /dividedElement  : ???

+

+");

+        }

+

+

     }

 }

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 78ace202..74bdaa5e 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -89,9 +89,10 @@ namespace GPUVerify
             verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);

         }

 

-        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)

+        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)

         {

-            IdentifierExprSeq newVars = new IdentifierExprSeq();

+            ModifiedAtLog = new IdentifierExprSeq();

+            ResetAtBarrier = new IdentifierExprSeq();

 

             Variable AccessHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));

 

@@ -100,7 +101,8 @@ namespace GPUVerify
                 verifier.HalfDualisedVariableNames.Add(AccessHasOccurred.Name);

             }

 

-            newVars.Add(new IdentifierExpr(v.tok, AccessHasOccurred));

+            ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessHasOccurred));

+            ResetAtBarrier.Add(new IdentifierExpr(v.tok, AccessHasOccurred));

 

             verifier.Program.TopLevelDeclarations.Add(AccessHasOccurred);

             if (v.TypedIdent.Type is MapType)

@@ -116,7 +118,7 @@ namespace GPUVerify
                     verifier.HalfDualisedVariableNames.Add(AccessOffsetX.Name);

                 }

 

-                newVars.Add(new IdentifierExpr(v.tok, AccessOffsetX));

+                ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetX));

                 verifier.Program.TopLevelDeclarations.Add(AccessOffsetX);

 

                 if (mt.Result is MapType)

@@ -132,7 +134,7 @@ namespace GPUVerify
                         verifier.HalfDualisedVariableNames.Add(AccessOffsetY.Name);

                     }

 

-                    newVars.Add(new IdentifierExpr(v.tok, AccessOffsetY));

+                    ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetY));

                     verifier.Program.TopLevelDeclarations.Add(AccessOffsetY);

 

                     if (mt2.Result is MapType)

@@ -149,19 +151,15 @@ namespace GPUVerify
                             verifier.HalfDualisedVariableNames.Add(AccessOffsetZ.Name);

                         }

 

-                        newVars.Add(new IdentifierExpr(v.tok, AccessOffsetZ));

+                        ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetZ));

                         verifier.Program.TopLevelDeclarations.Add(AccessOffsetZ);

                     }

                 }

             }

 

-            foreach (IdentifierExpr e in newVars)

-            {

-                // TODO: add modiies to every procedure that calls BARRIER

-                verifier.KernelProcedure.Modifies.Add(e);

-            }

         }

 

+

         private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)

         {

             List<AssignLhs> lhss = new List<AssignLhs>();

@@ -179,7 +177,6 @@ namespace GPUVerify
             List<AssignLhs> lhss = new List<AssignLhs>();

             List<Expr> rhss = new List<Expr>();

 

-            verifier.BarrierProcedure.Modifies.Add(AccessOccurred1);

             lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));

             rhss.Add(Expr.False);

 

@@ -187,7 +184,6 @@ namespace GPUVerify
             {

                 lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));

                 rhss.Add(Expr.False);

-                verifier.BarrierProcedure.Modifies.Add(AccessOccurred2);

             }

 

             bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 1aac817c..25974225 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -19,18 +19,13 @@ namespace GPUVerify
         public Implementation KernelImplementation;

         public Procedure BarrierProcedure;

 

-        public ICollection<Variable> TileStaticVariables = new List<Variable>();

-        public ICollection<Variable> GlobalVariables = new List<Variable>();

+        public INonLocalState NonLocalState = new NonLocalStateLists();

 

         private HashSet<string> ReservedNames = new HashSet<string>();

 

         internal HashSet<string> HalfDualisedProcedureNames = new HashSet<string>();

         internal HashSet<string> HalfDualisedVariableNames = new HashSet<string>();

 

-        private static int WhileLoopCounter;

-        private static int IfCounter;

-        private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;

-

         private int TempCounter = 0;

         private int invariantGenerationCounter;

 

@@ -165,11 +160,11 @@ namespace GPUVerify
                     {

                         if (QKeyValue.FindBoolAttribute(D.Attributes, "tile_static"))

                         {

-                            TileStaticVariables.Add(D as Variable);

+                            NonLocalState.getTileStaticVariables().Add(D as Variable);

                         }

                         else

                         {

-                            GlobalVariables.Add(D as Variable);

+                            NonLocalState.getGlobalVariables().Add(D as Variable);

                         }

                     }

                 }

@@ -296,16 +291,6 @@ namespace GPUVerify
             // TODO!

         }

 

-        internal ICollection<Variable> GetTileStaticVariables()

-        {

-            return TileStaticVariables;

-        }

-

-        internal ICollection<Variable> GetGlobalVariables()

-        {

-            return GlobalVariables;

-        }

-

         internal void preProcess()

         {

             RemoveElseIfs();

@@ -331,7 +316,7 @@ namespace GPUVerify
 

             AbstractSharedState();

 

-            MakeKerenelPredicated();

+            MakeKernelPredicated();

 

             MakeKernelDualised();

 

@@ -399,7 +384,7 @@ namespace GPUVerify
 

         private void AddEagerRaceChecking()

         {

-            foreach(Variable v in GlobalVariables)

+            foreach(Variable v in NonLocalState.getAllNonLocalVariables())

             {

                 foreach (Declaration d in Program.TopLevelDeclarations)

                 {

@@ -425,32 +410,6 @@ namespace GPUVerify
                     }

                 }

             }

-            foreach (Variable v in TileStaticVariables)

-            {

-                foreach (Declaration d in Program.TopLevelDeclarations)

-                {

-                    if (!(d is Implementation))

-                    {

-                        continue;

-                    }

-

-                    Implementation impl = d as Implementation;

-

-                    if (impl.Name.Equals("_LOG_READ_" + v.Name) || impl.Name.Equals("_LOG_WRITE_" + v.Name))

-                    {

-                        BigBlock bb = new BigBlock(v.tok, "__CheckForRaces", new CmdSeq(), null, null);

-                        RaceInstrumenter.CheckForRaces(v.tok, bb, v);

-                        StmtList newStatements = new StmtList(new List<BigBlock>(), v.tok);

-                        

-                        foreach (BigBlock bb2 in impl.StructuredStmts.BigBlocks)

-                        {

-                            newStatements.BigBlocks.Add(bb2);

-                        }

-                        newStatements.BigBlocks.Add(bb);

-                        impl.StructuredStmts = newStatements;

-                    }

-                }

-            }

         }

 

         private void ComputeInvariant()

@@ -735,12 +694,7 @@ namespace GPUVerify
 

                 if (!CommandLineOptions.FullAbstraction)

                 {

-                    foreach (Variable v in GlobalVariables)

-                    {

-                        AddEqualityCandidateInvariant(wc, LoopPredicate, v);

-                    }

-

-                    foreach (Variable v in TileStaticVariables)

+                    foreach (Variable v in NonLocalState.getAllNonLocalVariables())

                     {

                         AddEqualityCandidateInvariant(wc, LoopPredicate, v);

                     }

@@ -855,21 +809,23 @@ namespace GPUVerify
             return true;

         }

 

+        

+

         public Microsoft.Boogie.Type GetTypeOfIdX()

         {

-            Contract.Assert(_X != null);

+            Contract.Requires(_X != null);

             return _X.TypedIdent.Type;

         }

 

         public Microsoft.Boogie.Type GetTypeOfIdY()

         {

-            Contract.Assert(_Y != null);

+            Contract.Requires(_Y != null);

             return _Y.TypedIdent.Type;

         }

 

         public Microsoft.Boogie.Type GetTypeOfIdZ()

         {

-            Contract.Assert(_Z != null);

+            Contract.Requires(_Z != null);

             return _Z.TypedIdent.Type;

         }

 

@@ -1164,11 +1120,7 @@ namespace GPUVerify
             {

                 BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);

                 bigblocks.Add(havocSharedState);

-                foreach (Variable v in GlobalVariables)

-                {

-                    HavocAndAssumeEquality(tok, havocSharedState, v);

-                }

-                foreach (Variable v in TileStaticVariables)

+                foreach (Variable v in NonLocalState.getAllNonLocalVariables())

                 {

                     HavocAndAssumeEquality(tok, havocSharedState, v);

                 }

@@ -1219,35 +1171,18 @@ namespace GPUVerify
             IdentifierExpr v1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable));

             IdentifierExpr v2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable));

 

-            bb.simpleCmds.Add(new HavocCmd(tok, new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 })));

+            IdentifierExprSeq ModifiedVars = new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 });

+            bb.simpleCmds.Add(new HavocCmd(tok, ModifiedVars));

             bb.simpleCmds.Add(new AssumeCmd(tok, Expr.Eq(v1, v2)));

-            BarrierProcedure.Modifies.Add(v1);

-            BarrierProcedure.Modifies.Add(v2);

-

-            foreach (Declaration d in Program.TopLevelDeclarations)

-            {

-                if (d is Implementation)

-                {

-                    Implementation impl = d as Implementation;

-                    if (CallsBarrier(impl))

-                    {

-                        Procedure proc = impl.Proc;

-                        if (!ModifiesSetContains(proc.Modifies, v1))

-                        {

-                            Debug.Assert(!ModifiesSetContains(proc.Modifies, v2));

-                            proc.Modifies.Add(v1);

-                            proc.Modifies.Add(v2);

-                        }

-                    }

-                }

-            }

 

+            HashSet<string> MayCallBarrier = GetProceduresThatIndirectlyCallProcedure(BarrierProcedure.Name);

+            ExtendModifiesSetOfProcedures(ModifiedVars, MayCallBarrier);

 

         }

 

-        private bool ModifiesSetContains(IdentifierExprSeq seq, IdentifierExpr v)

+        internal static bool ModifiesSetContains(IdentifierExprSeq Modifies, IdentifierExpr v)

         {

-            foreach (IdentifierExpr ie in seq)

+            foreach (IdentifierExpr ie in Modifies)

             {

                 if (ie.Name.Equals(v.Name))

                 {

@@ -1257,7 +1192,7 @@ namespace GPUVerify
             return false;

         }

 

-        private bool CallsBarrier(Implementation impl)

+/*        private bool CallsBarrier(Implementation impl)

         {

             return CallsBarrier(impl.StructuredStmts);

         }

@@ -1292,7 +1227,7 @@ namespace GPUVerify
                 Debug.Assert(bb.ec == null);

                 return false;

             }

-        }

+        }*/

 

         private void AbstractSharedState()

         {

@@ -1305,7 +1240,7 @@ namespace GPUVerify
 

             foreach (Declaration d in Program.TopLevelDeclarations)

             {

-                if (d is Variable && GlobalVariables.Contains(d as Variable) || TileStaticVariables.Contains(d as Variable))

+                if (d is Variable && NonLocalState.Contains(d as Variable))

                 {

                     continue;

                 }

@@ -1334,7 +1269,7 @@ namespace GPUVerify
 

             foreach (IdentifierExpr e in proc.Modifies)

             {

-                if (!(GlobalVariables.Contains(e.Decl) || TileStaticVariables.Contains(e.Decl)))

+                if (!NonLocalState.Contains(e.Decl))

                 {

                     NewModifies.Add(e);

                 }

@@ -1350,10 +1285,8 @@ namespace GPUVerify
 

             foreach (Variable v in impl.LocVars)

             {

-                if (!TileStaticVariables.Contains(v))

-                {

-                    NewLocVars.Add(v);

-                }

+                Debug.Assert(!NonLocalState.getTileStaticVariables().Contains(v));

+                NewLocVars.Add(v);

             }

 

             impl.LocVars = NewLocVars;

@@ -1389,7 +1322,7 @@ namespace GPUVerify
                     Debug.Assert(assign.Rhss.Count == 1);

                     AssignLhs lhs = assign.Lhss[0];

                     Expr rhs = assign.Rhss[0];

-                    ReadCollector rc = new ReadCollector(GlobalVariables, TileStaticVariables);

+                    ReadCollector rc = new ReadCollector(NonLocalState);

                     rc.Visit(rhs);

                     if (rc.accesses.Count > 0)

                     {

@@ -1398,7 +1331,7 @@ namespace GPUVerify
                         continue;

                     }

 

-                    WriteCollector wc = new WriteCollector(GlobalVariables, TileStaticVariables);

+                    WriteCollector wc = new WriteCollector(NonLocalState);

                     wc.Visit(lhs);

                     if (wc.GetAccess() != null)

                     {

@@ -1642,7 +1575,7 @@ namespace GPUVerify
                     {

                         Expr e = call.Ins[i];

 

-                        while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))

+                        while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))

                         {

                             AssignCmd assignToTemp;

                             LocalVariable tempDecl;

@@ -1666,7 +1599,9 @@ namespace GPUVerify
                     AssignLhs lhs = assign.Lhss.ElementAt(0);

                     Expr rhs = assign.Rhss.ElementAt(0);

 

-                    if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables) || (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, GlobalVariables, TileStaticVariables) && NonLocalAccessCollector.IsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables)))

+                    if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) || 

+                        (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) && 

+                          NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState)))

                     {

                         result.simpleCmds.Add(c);

                     }

@@ -1703,7 +1638,7 @@ namespace GPUVerify
             if (bb.ec is WhileCmd)

             {

                 WhileCmd WhileCommand = bb.ec as WhileCmd;

-                while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, GlobalVariables, TileStaticVariables))

+                while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, NonLocalState))

                 {

                     AssignCmd assignToTemp;

                     LocalVariable tempDecl;

@@ -1716,8 +1651,8 @@ namespace GPUVerify
             else if (bb.ec is IfCmd)

             {

                 IfCmd IfCommand = bb.ec as IfCmd;

-                Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet

-                while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, GlobalVariables, TileStaticVariables))

+                Debug.Assert(IfCommand.elseIf == null); // "else if" must have been eliminated by this phase

+                while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, NonLocalState))

                 {

                     AssignCmd assignToTemp;

                     LocalVariable tempDecl;

@@ -1742,7 +1677,7 @@ namespace GPUVerify
 

         private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e, Implementation impl)

         {

-            while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))

+            while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))

             {

                 AssignCmd assignToTemp;

                 LocalVariable tempDecl;

@@ -1755,7 +1690,7 @@ namespace GPUVerify
 

         private Expr ExtractLocalAccessToTemp(Expr rhs, out AssignCmd tempAssignment, out LocalVariable tempDeclaration)

         {

-            NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, GlobalVariables, TileStaticVariables);

+            NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, NonLocalState);

             TempCounter++;

             rhs = extractor.VisitExpr(rhs);

             tempAssignment = extractor.Assignment;

@@ -1860,7 +1795,7 @@ namespace GPUVerify
             return result;

         }

 

-        private void MakeKerenelPredicated()

+        private void MakeKernelPredicated()

         {

             foreach (Declaration d in Program.TopLevelDeclarations)

             {

@@ -1882,38 +1817,12 @@ namespace GPUVerify
                 }

                 else if (d is Implementation)

                 {

-                    MakePredicated(d as Implementation, d != KernelImplementation);

-                }

-            }

+                    new Predicator(d != KernelImplementation).transform(d as Implementation);

 

-        }

-

-        private void MakePredicated(Implementation impl, bool AddPredicateParameter)

-        {

-            Expr Predicate;

-

-            if (AddPredicateParameter)

-            {

-                VariableSeq NewIns = new VariableSeq();

-                Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));

-                NewIns.Add(PredicateVariable);

-                foreach (Variable v in impl.InParams)

-                {

-                    NewIns.Add(v);

+                    //MakePredicated(d as Implementation, d != KernelImplementation);

                 }

-                impl.InParams = NewIns;

-                Predicate = new IdentifierExpr(impl.tok, PredicateVariable);

-            }

-            else

-            {

-                Predicate = Expr.True;

             }

 

-            WhileLoopCounter = 0;

-            IfCounter = 0;

-            RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();

-            impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);

-            AddPredicateLocalVariables(impl);

         }

 

         private StmtList MakeDual(StmtList stmtList, bool HalfDualise)

@@ -2081,208 +1990,6 @@ namespace GPUVerify
             impl.LocVars = NewLocalVars;

         }

 

-        private void AddPredicateLocalVariables(Implementation impl)

-        {

-            for (int i = 0; i < IfCounter; i++)

-            {

-                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));

-            }

-            for (int i = 0; i < WhileLoopCounter; i++)

-            {

-                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));

-            }

-            foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)

-            {

-                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));

-            }

-

-        }

-

-        private StmtList MakePredicated(StmtList sl, Expr predicate, IdentifierExpr EnclosingLoopPredicate)

-        {

-            StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);

-

-            foreach (BigBlock bodyBlock in sl.BigBlocks)

-            {

-                List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);

-                foreach (BigBlock newBigBlock in newBigBlocks)

-                {

-                    result.BigBlocks.Add(newBigBlock);

-                }

-            }

-

-            return result;

-

-        }

-

-        private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)

-        {

-            // Not sure what to do about the transfer command

-

-            List<BigBlock> result = new List<BigBlock>();

-

-            BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);

-            result.Add(firstBigBlock);

-

-            foreach (Cmd c in b.simpleCmds)

-            {

-                if (c is CallCmd)

-                {

-

-                    CallCmd Call = c as CallCmd;

-

-                    List<Expr> NewIns = new List<Expr>();

-                    NewIns.Add(IncomingPredicate);

-

-                    foreach (Expr e in Call.Ins)

-                    {

-                        NewIns.Add(e);

-                    }

-

-                    CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);

-

-                    firstBigBlock.simpleCmds.Add(NewCallCmd);

-                }

-                else if (IncomingPredicate.Equals(Expr.True))

-                {

-                    firstBigBlock.simpleCmds.Add(c);

-                }

-                else if (c is AssignCmd)

-                {

-                    AssignCmd assign = c as AssignCmd;

-                    Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

-

-                    ExprSeq iteArgs = new ExprSeq();

-                    iteArgs.Add(IncomingPredicate);

-                    iteArgs.Add(assign.Rhss.ElementAt(0));

-                    iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);

-                    NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);

-

-                    List<Expr> newRhs = new List<Expr>();

-                    newRhs.Add(ite);

-

-                    AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);

-

-                    firstBigBlock.simpleCmds.Add(newAssign);

-                }

-                else if (c is HavocCmd)

-                {

-                    HavocCmd havoc = c as HavocCmd;

-                    Debug.Assert(havoc.Vars.Length == 1);

-

-                    Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;

-                    Debug.Assert(type != null);

-

-                    RequiredHavocVariables.Add(type);

-

-                    IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));

-                    firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

-                        HavocTempExpr 

-                    })));

-

-                    List<AssignLhs> lhss = new List<AssignLhs>();

-                    lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));

-

-                    List<Expr> rhss = new List<Expr>();

-                    rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));

-

-                    firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));

-

-                }

-                else

-                {

-                    Debug.Assert(false);

-                }

-            }

-

-            if (b.ec is WhileCmd)

-            {

-                string LoopPredicate = "_LC" + WhileLoopCounter;

-                WhileLoopCounter++;

-

-                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));

-                Expr GuardExpr = (b.ec as WhileCmd).Guard;

-

-                List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();

-                WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));

-

-                List<Expr> WhilePredicateRhss = new List<Expr>();

-                WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));

-

-                firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));

-

-                WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));

-

-                List<Expr> UpdatePredicateRhss = new List<Expr>();

-                UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));

-

-                CmdSeq updateCmd = new CmdSeq();

-                updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));

-

-                NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));

-

-                firstBigBlock.ec = NewWhile;

-

-            }

-            else if (b.ec is IfCmd)

-            {

-                IfCmd IfCommand = b.ec as IfCmd;

-

-                string IfPredicate = "_P" + IfCounter;

-                IfCounter++;

-

-                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));

-                Expr GuardExpr = IfCommand.Guard;

-

-                List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();

-                IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));

-

-                List<Expr> IfPredicateRhss = new List<Expr>();

-                IfPredicateRhss.Add(GuardExpr);

-

-                firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));

-

-                Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away

-

-                StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);

-

-                foreach (BigBlock bb in PredicatedThen.BigBlocks)

-                {

-                    result.Add(bb);

-                }

-

-                if (IfCommand.elseBlock != null)

-                {

-                    StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);

-

-                    foreach (BigBlock bb in PredicatedElse.BigBlocks)

-                    {

-                        result.Add(bb);

-                    }

-                }

-

-

-

-

-            }

-            else if (b.ec is BreakCmd)

-            {

-

-

-                firstBigBlock.simpleCmds.Add(new AssignCmd(b.tok,

-                    new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(b.tok, EnclosingLoopPredicate) }),

-                    new List<Expr>(new Expr[] { new NAryExpr(b.tok, new IfThenElse(b.tok), new ExprSeq(new Expr[] { IncomingPredicate, Expr.False, EnclosingLoopPredicate })) })

-                    ));

-                firstBigBlock.ec = null;            

-            

-            }

-            else

-            {

-                Debug.Assert(b.ec == null);

-            }

-

-            return result;

-        }

 

         private void CheckKernelParameters()

         {

@@ -2454,5 +2161,87 @@ namespace GPUVerify
             return variable is Constant && (variable.Name.Equals(_X_name) || variable.Name.Equals(_Y_name) || variable.Name.Equals(_Z_name));

         }

 

+        internal HashSet<string> GetProceduresThatIndirectlyCallProcedure(string Name)

+        {

+            HashSet<string> MayCallProc = new HashSet<string>();

+            MayCallProc.Add(Name);

+            bool changed = true;

+            while (changed)

+            {

+                changed = false;

+                foreach (Declaration d in Program.TopLevelDeclarations)

+                {

+                    if (d is Implementation && !MayCallProc.Contains((d as Implementation).Name))

+                    {

+                        HashSet<string> CalledProcedures = GetCalledProcedures(d as Implementation);

+                        foreach (string p in CalledProcedures)

+                        {

+                            if (MayCallProc.Contains(p))

+                            {

+                                changed = true;

+                                MayCallProc.Add((d as Implementation).Name);

+                                break;

+                            }

+                        }

+                    }

+                }

+            }

+            return MayCallProc;

+        }

+

+        private HashSet<string> GetCalledProcedures(Implementation impl)

+        {

+            HashSet<string> result = new HashSet<string>();

+            return GetCalledProcedures(impl.StructuredStmts, result);

+        }

+

+        private HashSet<string> GetCalledProcedures(StmtList statements, HashSet<string> result)

+        {

+            foreach (BigBlock bb in statements.BigBlocks)

+            {

+                foreach (Cmd c in bb.simpleCmds)

+                {

+                    if (c is CallCmd)

+                    {

+                        result.Add((c as CallCmd).callee);

+                    }

+                }

+

+                if (bb.ec is WhileCmd)

+                {

+                    result = GetCalledProcedures((bb.ec as WhileCmd).Body, result);

+                }

+                else if (bb.ec is IfCmd)

+                {

+                    result = GetCalledProcedures((bb.ec as IfCmd).thn, result);

+                    Debug.Assert((bb.ec as IfCmd).elseIf == null);

+                    if ((bb.ec as IfCmd).elseBlock != null)

+                    {

+                        result = GetCalledProcedures((bb.ec as IfCmd).elseBlock, result);

+                    }

+                }

+            }

+

+            return result;

+        }

+

+        internal void ExtendModifiesSetOfProcedures(IdentifierExprSeq ModifiedVariables, HashSet<string> Procedures)

+        {

+            foreach (Declaration d in Program.TopLevelDeclarations)

+            {

+                if (d is Procedure && Procedures.Contains((d as Procedure).Name))

+                {

+                    Procedure P = d as Procedure;

+                    foreach (IdentifierExpr e in ModifiedVariables)

+                    {

+                        if (!GPUVerifier.ModifiesSetContains(P.Modifies, e))

+                        {

+                            P.Modifies.Add(e);

+                        }

+                    }

+                }

+            }

+        }

+

     }

 }

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 3b4e3bc5..7023a2b3 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -2,7 +2,7 @@
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <Platform Condition=" '$(Platform)' == '' ">x86</Platform>

     <ProductVersion>8.0.30703</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

     <ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>

@@ -15,8 +15,8 @@
     <FileAlignment>512</FileAlignment>

     <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

   </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

-    <PlatformTarget>AnyCPU</PlatformTarget>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">

+    <PlatformTarget>x86</PlatformTarget>

     <DebugSymbols>true</DebugSymbols>

     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

@@ -24,7 +24,7 @@
     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

     <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

     <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

     <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

@@ -51,93 +51,15 @@
     <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

     <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>

-    <CodeContractsInferRequires>False</CodeContractsInferRequires>

-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>

-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>

-    <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>

   </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

-    <PlatformTarget>AnyCPU</PlatformTarget>

+  <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>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsInferRequires>False</CodeContractsInferRequires>

-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>

-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>

-    <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-  </PropertyGroup>

-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\Checked\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>

-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

@@ -155,12 +77,15 @@
     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="ElementEncodingraceInstrumenter.cs" />

     <Compile Include="GPUVerifier.cs" />

+    <Compile Include="INonLocalState.cs" />

     <Compile Include="IRaceInstrumenter.cs" />

     <Compile Include="Main.cs" />

     <Compile Include="NoConflictingAccessOptimiser.cs" />

     <Compile Include="NonLocalAccessCollector.cs" />

     <Compile Include="NonLocalAccessExtractor.cs" />

+    <Compile Include="NonLocalStateLists.cs" />

     <Compile Include="NullRaceInstrumenter.cs" />

+    <Compile Include="Predicator.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="RaceInstrumenterBase.cs" />

     <Compile Include="ReadCollector.cs" />

diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs
new file mode 100644
index 00000000..0e03d685
--- /dev/null
+++ b/Source/GPUVerify/INonLocalState.cs
@@ -0,0 +1,21 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    interface INonLocalState

+    {

+

+        ICollection<Variable> getGlobalVariables();

+

+        ICollection<Variable> getTileStaticVariables();

+

+        ICollection<Variable> getAllNonLocalVariables();

+

+        bool Contains(Variable v);

+

+    }

+}

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 06fe70c6..9791d6cf 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -15,11 +15,16 @@ namespace GPUVerify
 {

     class GPUVerify

     {

-        static bool ASYNCHRONOUS_METHOD = false;

 

         public static void Main(string[] args)

         {

-            CommandLineOptions.Parse(args);

+            int showHelp = CommandLineOptions.Parse(args);

+

+            if (showHelp == -1)

+            {

+                CommandLineOptions.Usage();

+                System.Environment.Exit(0);

+            }

 

             if (CommandLineOptions.inputFiles.Count < 1)

             {

@@ -42,36 +47,6 @@ namespace GPUVerify
                 }

             }

 

-            if (ASYNCHRONOUS_METHOD)

-            {

-

-                string[] preprocessArguments = new string[CommandLineOptions.inputFiles.Count + 4];

-                preprocessArguments[0] = "/noVerify";

-                preprocessArguments[1] = "/printUnstructured";

-                preprocessArguments[2] = "/print:temp_unstructured.bpl";

-                preprocessArguments[3] = Path.GetDirectoryName(Application.ExecutablePath) + "\\..\\..\\BoogieLibrary\\GPUVerifyLibrary.bpl";

-                for (int i = 0; i < CommandLineOptions.inputFiles.Count; i++)

-                {

-                    preprocessArguments[i + 4] = CommandLineOptions.inputFiles[i];

-                }

-

-                OnlyBoogie.Main(preprocessArguments);

-

-                if ((CommandLineOptions.formulasFile == null && CommandLineOptions.formulaSkeletonsFile == null) || (CommandLineOptions.formulasFile != null && CommandLineOptions.formulaSkeletonsFile != null))

-                {

-                    Console.WriteLine("Error, specify one of /formulas:... or /generateFormulaSkeletons:...");

-                    Environment.Exit(1);

-                }

-

-                CommandLineOptions.inputFiles = new List<string>();

-                CommandLineOptions.inputFiles.Add("temp_unstructured.bpl");

-                if (CommandLineOptions.formulasFile != null)

-                {

-                    CommandLineOptions.inputFiles.Add(CommandLineOptions.formulasFile);

-                }

-

-            }

-

             parseProcessOutput();

         }

 

@@ -121,23 +96,23 @@ namespace GPUVerify
             ri.setVerifier(newGp);

 

             

-            Variable newG = findClonedVar(v, newGp.GlobalVariables);

-            Variable newT = findClonedVar(v, newGp.TileStaticVariables);

+            Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());

+            Variable newT = findClonedVar(v, newGp.NonLocalState.getTileStaticVariables());

             Contract.Assert(newG == null || newT == null);

-            

-            ri.globalVarsToCheck.Clear();

-            ri.tileStaticVarsToCheck.Clear();

+

+            ri.NonLocalStateToCheck.getGlobalVariables().Clear();

+            ri.NonLocalStateToCheck.getTileStaticVariables().Clear();

             ri.onlyLog1 = a1;

             ri.onlyLog2 = a2;

 

             if (newG != null)

             {

-                ri.globalVarsToCheck.Add(newG);

+                ri.NonLocalStateToCheck.getGlobalVariables().Add(newG);

             }

 

             if (newT != null)

             {

-                ri.globalVarsToCheck.Add(newT);

+                ri.NonLocalStateToCheck.getTileStaticVariables().Add(newT);

             }

             

             newGp.doit();

@@ -159,11 +134,7 @@ namespace GPUVerify
 

             if (CommandLineOptions.DividedArray)

             {

-                List<Variable> nonLocalVars = new List<Variable>();

-                nonLocalVars.AddRange(g.GlobalVariables);

-                nonLocalVars.AddRange(g.TileStaticVariables);

-

-                foreach (Variable v in nonLocalVars)

+                foreach (Variable v in g.NonLocalState.getAllNonLocalVariables())

                 {

                     if (CommandLineOptions.DividedAccesses)

                     {

diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs
index bbab9040..13d8f672 100644
--- a/Source/GPUVerify/NonLocalAccessCollector.cs
+++ b/Source/GPUVerify/NonLocalAccessCollector.cs
@@ -12,16 +12,14 @@ namespace GPUVerify
     {

         public HashSet<Expr> Accesses = new HashSet<Expr>();

 

-        private ICollection<Variable> GlobalVariables;

-        private ICollection<Variable> TileStaticVariables;

+        private INonLocalState NonLocalState;

 

-        public NonLocalAccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

+        public NonLocalAccessCollector(INonLocalState NonLocalState)

         {

-            this.GlobalVariables = GlobalVariables;

-            this.TileStaticVariables = TileStaticVariables;

+            this.NonLocalState = NonLocalState;

         }

 

-        public static bool IsNonLocalAccess(Expr n, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

+        public static bool IsNonLocalAccess(Expr n, INonLocalState NonLocalState)

         {

             if (n is NAryExpr)

             {

@@ -37,22 +35,22 @@ namespace GPUVerify
 

                     Variable v = (temp as IdentifierExpr).Decl;

 

-                    return (GlobalVariables.Contains(v) || TileStaticVariables.Contains(v));

+                    return (NonLocalState.Contains(v));

                 }

             }

 

             if (n is IdentifierExpr)

             {

                 IdentifierExpr node = n as IdentifierExpr;

-                return GlobalVariables.Contains(node.Decl) || TileStaticVariables.Contains(node.Decl);

+                return NonLocalState.Contains(node.Decl);

             }

 

             return false;

         }

 

-        public static bool ContainsNonLocalAccess(AssignLhs lhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

+        public static bool ContainsNonLocalAccess(AssignLhs lhs, INonLocalState NonLocalState)

         {

-            NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);

+            NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);

             if (lhs is SimpleAssignLhs)

             {

                 collector.VisitSimpleAssignLhs(lhs as SimpleAssignLhs);

@@ -65,9 +63,9 @@ namespace GPUVerify
             return collector.Accesses.Count > 0;

         }

 

-        public static bool ContainsNonLocalAccess(Expr rhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

+        public static bool ContainsNonLocalAccess(Expr rhs, INonLocalState NonLocalState)

         {

-            NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);

+            NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);

             collector.VisitExpr(rhs);

             return collector.Accesses.Count > 0;

         }

@@ -75,7 +73,7 @@ namespace GPUVerify
 

         public override Expr VisitNAryExpr(NAryExpr node)

         {

-            if (IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))

+            if (IsNonLocalAccess(node, NonLocalState))

             {

                 Accesses.Add(node);

                 return node;

@@ -85,7 +83,7 @@ namespace GPUVerify
 

         public override Expr VisitIdentifierExpr(IdentifierExpr node)

         {

-            if (IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))

+            if (IsNonLocalAccess(node, NonLocalState))

             {

                 Accesses.Add(node);

                 return node;

diff --git a/Source/GPUVerify/NonLocalAccessExtractor.cs b/Source/GPUVerify/NonLocalAccessExtractor.cs
index 506ec3c5..553be683 100644
--- a/Source/GPUVerify/NonLocalAccessExtractor.cs
+++ b/Source/GPUVerify/NonLocalAccessExtractor.cs
@@ -14,14 +14,12 @@ namespace GPUVerify
         public LocalVariable Declaration = null;

         public bool done = false;

 

-        private ICollection<Variable> GlobalVariables;

-        private ICollection<Variable> TileStaticVariables;

+        private INonLocalState NonLocalState;

 

-        public NonLocalAccessExtractor(int TempId, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

+        public NonLocalAccessExtractor(int TempId, INonLocalState NonLocalState)

         {

             this.TempId = TempId;

-            this.GlobalVariables = GlobalVariables;

-            this.TileStaticVariables = TileStaticVariables;

+            this.NonLocalState = NonLocalState;

         }

 

 

@@ -32,7 +30,7 @@ namespace GPUVerify
                 return node;

             }

 

-            if (!NonLocalAccessCollector.IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))

+            if (!NonLocalAccessCollector.IsNonLocalAccess(node, NonLocalState))

             {

                 return base.VisitNAryExpr(node);

             }

@@ -42,7 +40,7 @@ namespace GPUVerify
             {

                 Debug.Assert((temp as NAryExpr).Args.Length == 2);

 

-                if (NonLocalAccessCollector.ContainsNonLocalAccess((temp as NAryExpr).Args[1], GlobalVariables, TileStaticVariables))

+                if (NonLocalAccessCollector.ContainsNonLocalAccess((temp as NAryExpr).Args[1], NonLocalState))

                 {

                     return VisitExpr((temp as NAryExpr).Args[1]);

                 }

@@ -77,7 +75,7 @@ namespace GPUVerify
                 return node;

             }

 

-            if (NonLocalAccessCollector.IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))

+            if (NonLocalAccessCollector.IsNonLocalAccess(node, NonLocalState))

             {

                 done = true;

                 Declaration = new LocalVariable(node.tok, new TypedIdent(node.tok, "_temp" + TempId, node.Decl.TypedIdent.Type));

diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs
new file mode 100644
index 00000000..a4b5e154
--- /dev/null
+++ b/Source/GPUVerify/NonLocalStateLists.cs
@@ -0,0 +1,45 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+using System.Diagnostics;

+

+namespace GPUVerify

+{

+    class NonLocalStateLists : INonLocalState

+    {

+        private List<Variable> GlobalVariables;

+        private List<Variable> TileStaticVariables;

+

+        public NonLocalStateLists()

+        {

+            GlobalVariables = new List<Variable>();

+            TileStaticVariables = new List<Variable>();

+        }

+

+        public ICollection<Variable> getGlobalVariables()

+        {

+            return GlobalVariables;

+        }

+

+        public ICollection<Variable> getTileStaticVariables()

+        {

+            return TileStaticVariables;

+        }

+

+        public ICollection<Variable> getAllNonLocalVariables()

+        {

+            List<Variable> all = new List<Variable>();

+            all.AddRange(GlobalVariables);

+            all.AddRange(TileStaticVariables);

+            return all;

+        }

+

+        public bool Contains(Variable v)

+        {

+            return getAllNonLocalVariables().Contains(v);

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
new file mode 100644
index 00000000..cca89b52
--- /dev/null
+++ b/Source/GPUVerify/Predicator.cs
@@ -0,0 +1,256 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class Predicator

+    {

+        private bool AddPredicateParameter;

+        private int WhileLoopCounter;

+        private int IfCounter;

+        private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;

+

+        internal Predicator(bool AddPredicateParameter)

+        {

+            this.AddPredicateParameter = AddPredicateParameter;

+            WhileLoopCounter = 0;

+            IfCounter = 0;

+            RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();

+        }

+

+        internal void transform(Implementation impl)

+        {

+            Expr Predicate;

+

+            if (AddPredicateParameter)

+            {

+                VariableSeq NewIns = new VariableSeq();

+                Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));

+                NewIns.Add(PredicateVariable);

+                foreach (Variable v in impl.InParams)

+                {

+                    NewIns.Add(v);

+                }

+                impl.InParams = NewIns;

+                Predicate = new IdentifierExpr(impl.tok, PredicateVariable);

+            }

+            else

+            {

+                Predicate = Expr.True;

+            }

+

+            impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);

+            AddPredicateLocalVariables(impl);            

+        }

+

+

+        private StmtList MakePredicated(StmtList sl, Expr predicate, IdentifierExpr EnclosingLoopPredicate)

+        {

+            StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);

+

+            foreach (BigBlock bodyBlock in sl.BigBlocks)

+            {

+                List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);

+                foreach (BigBlock newBigBlock in newBigBlocks)

+                {

+                    result.BigBlocks.Add(newBigBlock);

+                }

+            }

+

+            return result;

+

+        }

+

+        private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)

+        {

+            // Not sure what to do about the transfer command

+

+            List<BigBlock> result = new List<BigBlock>();

+

+            BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);

+            result.Add(firstBigBlock);

+

+            foreach (Cmd c in b.simpleCmds)

+            {

+                if (c is CallCmd)

+                {

+

+                    CallCmd Call = c as CallCmd;

+

+                    List<Expr> NewIns = new List<Expr>();

+                    NewIns.Add(IncomingPredicate);

+

+                    foreach (Expr e in Call.Ins)

+                    {

+                        NewIns.Add(e);

+                    }

+

+                    CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);

+

+                    firstBigBlock.simpleCmds.Add(NewCallCmd);

+                }

+                else if (IncomingPredicate.Equals(Expr.True))

+                {

+                    firstBigBlock.simpleCmds.Add(c);

+                }

+                else if (c is AssignCmd)

+                {

+                    AssignCmd assign = c as AssignCmd;

+                    Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

+

+                    ExprSeq iteArgs = new ExprSeq();

+                    iteArgs.Add(IncomingPredicate);

+                    iteArgs.Add(assign.Rhss.ElementAt(0));

+                    iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);

+                    NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);

+

+                    List<Expr> newRhs = new List<Expr>();

+                    newRhs.Add(ite);

+

+                    AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);

+

+                    firstBigBlock.simpleCmds.Add(newAssign);

+                }

+                else if (c is HavocCmd)

+                {

+                    HavocCmd havoc = c as HavocCmd;

+                    Debug.Assert(havoc.Vars.Length == 1);

+

+                    Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;

+                    Debug.Assert(type != null);

+

+                    RequiredHavocVariables.Add(type);

+

+                    IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));

+                    firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

+                        HavocTempExpr 

+                    })));

+

+                    List<AssignLhs> lhss = new List<AssignLhs>();

+                    lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));

+

+                    List<Expr> rhss = new List<Expr>();

+                    rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));

+

+                    firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));

+

+                }

+                else

+                {

+                    Debug.Assert(false);

+                }

+            }

+

+            if (b.ec is WhileCmd)

+            {

+                string LoopPredicate = "_LC" + WhileLoopCounter;

+                WhileLoopCounter++;

+

+                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));

+                Expr GuardExpr = (b.ec as WhileCmd).Guard;

+

+                List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();

+                WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));

+

+                List<Expr> WhilePredicateRhss = new List<Expr>();

+                WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));

+

+                firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));

+

+                WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));

+

+                List<Expr> UpdatePredicateRhss = new List<Expr>();

+                UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));

+

+                CmdSeq updateCmd = new CmdSeq();

+                updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));

+

+                NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));

+

+                firstBigBlock.ec = NewWhile;

+

+            }

+            else if (b.ec is IfCmd)

+            {

+                IfCmd IfCommand = b.ec as IfCmd;

+

+                string IfPredicate = "_P" + IfCounter;

+                IfCounter++;

+

+                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));

+                Expr GuardExpr = IfCommand.Guard;

+

+                List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();

+                IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));

+

+                List<Expr> IfPredicateRhss = new List<Expr>();

+                IfPredicateRhss.Add(GuardExpr);

+

+                firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));

+

+                Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away

+

+                StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);

+

+                foreach (BigBlock bb in PredicatedThen.BigBlocks)

+                {

+                    result.Add(bb);

+                }

+

+                if (IfCommand.elseBlock != null)

+                {

+                    StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);

+

+                    foreach (BigBlock bb in PredicatedElse.BigBlocks)

+                    {

+                        result.Add(bb);

+                    }

+                }

+

+

+

+

+            }

+            else if (b.ec is BreakCmd)

+            {

+

+

+                firstBigBlock.simpleCmds.Add(new AssignCmd(b.tok,

+                    new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(b.tok, EnclosingLoopPredicate) }),

+                    new List<Expr>(new Expr[] { new NAryExpr(b.tok, new IfThenElse(b.tok), new ExprSeq(new Expr[] { IncomingPredicate, Expr.False, EnclosingLoopPredicate })) })

+                    ));

+                firstBigBlock.ec = null;

+

+            }

+            else

+            {

+                Debug.Assert(b.ec == null);

+            }

+

+            return result;

+        }

+

+

+        private void AddPredicateLocalVariables(Implementation impl)

+        {

+            for (int i = 0; i < IfCounter; i++)

+            {

+                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));

+            }

+            for (int i = 0; i < WhileLoopCounter; i++)

+            {

+                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));

+            }

+            foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)

+            {

+                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));

+            }

+

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 90229af0..0f5f8278 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -12,8 +12,8 @@ namespace GPUVerify
     abstract class RaceInstrumenterBase : IRaceInstrumenter

     {

         protected GPUVerifier verifier;

-        public ICollection<Variable> globalVarsToCheck;

-        public ICollection<Variable> tileStaticVarsToCheck;

+

+        public INonLocalState NonLocalStateToCheck;

 

         public int onlyLog1;

         public int onlyLog2;

@@ -33,8 +33,15 @@ namespace GPUVerify
         public void setVerifier(GPUVerifier verifier)

         {

             this.verifier = verifier;

-            globalVarsToCheck = new HashSet<Variable>(verifier.GlobalVariables);

-            tileStaticVarsToCheck = new HashSet<Variable>(verifier.TileStaticVariables);

+            NonLocalStateToCheck = new NonLocalStateLists();

+            foreach(Variable v in verifier.NonLocalState.getGlobalVariables())

+            {

+                NonLocalStateToCheck.getGlobalVariables().Add(v);

+            }

+            foreach(Variable v in verifier.NonLocalState.getTileStaticVariables())

+            {

+                NonLocalStateToCheck.getTileStaticVariables().Add(v);

+            }

         }

 

         protected abstract void AddRequiresNoPendingAccess(Variable v);

@@ -80,13 +87,7 @@ namespace GPUVerify
 

         public void AddRaceCheckingCandidateInvariants(WhileCmd wc)

         {

-            foreach (Variable v in globalVarsToCheck)

-            {

-                AddNoReadOrWriteCandidateInvariants(wc, v);

-                AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);

-            }

-

-            foreach (Variable v in tileStaticVarsToCheck)

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 AddNoReadOrWriteCandidateInvariants(wc, v);

                 AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);

@@ -134,12 +135,7 @@ namespace GPUVerify
 

         public void AddKernelPrecondition()

         {

-            foreach (Variable v in globalVarsToCheck)

-            {

-                AddRequiresNoPendingAccess(v);

-            }

-

-            foreach (Variable v in tileStaticVarsToCheck)

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 AddRequiresNoPendingAccess(v);

             }

@@ -163,12 +159,7 @@ namespace GPUVerify
             if (failedToFindSecondAccess || !addedLogWrite)

                 return false;

 

-            foreach (Variable v in globalVarsToCheck)

-            {

-                AddRaceCheckingDecsAndProcsForVar(v);

-            }

-

-            foreach (Variable v in tileStaticVarsToCheck)

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 AddRaceCheckingDecsAndProcsForVar(v);

             }

@@ -179,12 +170,29 @@ namespace GPUVerify
 

         private void AddRaceCheckingDecsAndProcsForVar(Variable v)

         {

-            AddLogRaceDeclarations(v, "READ");

-            AddLogRaceDeclarations(v, "WRITE");

+            IdentifierExprSeq ReadDeclsResetAtBarrier;

+            IdentifierExprSeq WriteDeclsResetAtBarrier;

+            IdentifierExprSeq ReadDeclsModifiedAtLogRead;

+            IdentifierExprSeq WriteDeclsModifiedAtLogWrite;

+                

+            AddLogRaceDeclarations(v, "READ", out ReadDeclsResetAtBarrier, out ReadDeclsModifiedAtLogRead);

+            AddLogRaceDeclarations(v, "WRITE", out WriteDeclsResetAtBarrier, out WriteDeclsModifiedAtLogWrite);

             AddLogAccessProcedure(v, "READ");

             AddLogAccessProcedure(v, "WRITE");

-        }

 

+            HashSet<string> MayCallBarrier = verifier.GetProceduresThatIndirectlyCallProcedure(verifier.BarrierProcedure.Name);

+

+            verifier.ExtendModifiesSetOfProcedures(ReadDeclsResetAtBarrier, MayCallBarrier);

+            verifier.ExtendModifiesSetOfProcedures(WriteDeclsResetAtBarrier, MayCallBarrier);

+

+            HashSet<string> MayCallLogRead = verifier.GetProceduresThatIndirectlyCallProcedure("_LOG_READ_" + v.Name);

+            HashSet<string> MayCallLogWrite = verifier.GetProceduresThatIndirectlyCallProcedure("_LOG_WRITE_" + v.Name);

+

+            verifier.ExtendModifiesSetOfProcedures(ReadDeclsModifiedAtLogRead, MayCallLogRead);

+            verifier.ExtendModifiesSetOfProcedures(WriteDeclsModifiedAtLogWrite, MayCallLogWrite);

+

+        }

+        

         private StmtList AddRaceCheckCalls(StmtList stmtList)

         {

             Contract.Requires(stmtList != null);

@@ -242,7 +250,7 @@ namespace GPUVerify
                     AssignLhs lhs = assign.Lhss[0];

                     Expr rhs = assign.Rhss[0];

 

-                    ReadCollector rc = new ReadCollector(globalVarsToCheck, tileStaticVarsToCheck);

+                    ReadCollector rc = new ReadCollector(NonLocalStateToCheck);

                     rc.Visit(rhs);

                     if (rc.accesses.Count > 0)

                     {

@@ -271,7 +279,7 @@ namespace GPUVerify
                         }

                     }

 

-                    WriteCollector wc = new WriteCollector(globalVarsToCheck, tileStaticVarsToCheck);

+                    WriteCollector wc = new WriteCollector(NonLocalStateToCheck);

                     wc.Visit(lhs);

                     if (wc.GetAccess() != null)

                     {

@@ -331,7 +339,7 @@ namespace GPUVerify
         }

 

 

-        protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite);

+        protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog);

 

         protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);

 

@@ -341,21 +349,13 @@ namespace GPUVerify
             BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);

             if (!CommandLineOptions.Eager)

             {

-                foreach (Variable v in globalVarsToCheck)

-                {

-                    CheckForRaces(tok, checkForRaces, v);

-                }

-                foreach (Variable v in tileStaticVarsToCheck)

+                foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

                 {

                     CheckForRaces(tok, checkForRaces, v);

                 }

             }

 

-            foreach (Variable v in globalVarsToCheck)

-            {

-                SetNoAccessOccurred(tok, checkForRaces, v);

-            }

-            foreach (Variable v in tileStaticVarsToCheck)

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 SetNoAccessOccurred(tok, checkForRaces, v);

             }

@@ -431,13 +431,7 @@ namespace GPUVerify
 

         public void AddRaceCheckingCandidateRequires(Procedure Proc)

         {

-            foreach (Variable v in globalVarsToCheck)

-            {

-                AddNoReadOrWriteCandidateRequires(Proc, v);

-                AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);

-            }

-

-            foreach (Variable v in tileStaticVarsToCheck)

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 AddNoReadOrWriteCandidateRequires(Proc, v);

                 AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);

@@ -446,13 +440,7 @@ namespace GPUVerify
 

         public void AddRaceCheckingCandidateEnsures(Procedure Proc)

         {

-            foreach (Variable v in globalVarsToCheck)

-            {

-                AddNoReadOrWriteCandidateEnsures(Proc, v);

-                AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);

-            }

-

-            foreach (Variable v in tileStaticVarsToCheck)

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 AddNoReadOrWriteCandidateEnsures(Proc, v);

                 AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);

diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs
index 281620c5..53d9234e 100644
--- a/Source/GPUVerify/ReadCollector.cs
+++ b/Source/GPUVerify/ReadCollector.cs
@@ -17,8 +17,8 @@ namespace GPUVerify
 

         public List<AccessRecord> accesses = new List<AccessRecord>();

 

-        public ReadCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

-            : base(GlobalVariables, TileStaticVariables)

+        public ReadCollector(INonLocalState NonLocalState)

+            : base(NonLocalState)

         {

         }

 

@@ -83,7 +83,7 @@ namespace GPUVerify
                 this.VisitExpr(node.Args[1]);

 

 

-                if (GlobalVariables.Contains(ReadVariable) || TileStaticVariables.Contains(ReadVariable))

+                if (NonLocalState.Contains(ReadVariable))

                 {

                     accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));

                 }

@@ -100,7 +100,7 @@ namespace GPUVerify
 

         public override Variable VisitVariable(Variable node)

         {

-            if (!(GlobalVariables.Contains(node) || TileStaticVariables.Contains(node)))

+            if (!NonLocalState.Contains(node))

             {

                 return node;

             }

diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
index c4f42923..3b1f877e 100644
--- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
@@ -11,7 +11,7 @@ namespace GPUVerify
     class SetEncodingRaceInstrumenter : RaceInstrumenterBase

     {

 

-        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)

+        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)

         {

             Variable AccessSet = MakeAccessSetVariable(v, ReadOrWrite);

 

@@ -22,9 +22,9 @@ namespace GPUVerify
 

             verifier.Program.TopLevelDeclarations.Add(AccessSet);

 

-            // TODO: add modiies to every procedure that calls BARRIER

+            ResetAtBarrier = new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, AccessSet) });

+            ModifiedAtLog = ResetAtBarrier;

 

-            verifier.KernelProcedure.Modifies.Add(new IdentifierExpr(v.tok, AccessSet));

         }

 

         private static Variable MakeAccessSetVariable(Variable v, String ReadOrWrite)

@@ -192,13 +192,11 @@ namespace GPUVerify
                             MakeAccessSetVariable(v, AccessType)));

             IdentifierExprSeq VariablesToHavoc = new IdentifierExprSeq();

             VariablesToHavoc.Add(AccessSet1);

-            verifier.BarrierProcedure.Modifies.Add(AccessSet1);

             if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))

             {

                 IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(

                                 MakeAccessSetVariable(v, AccessType)));

                 VariablesToHavoc.Add(AccessSet2);

-                verifier.BarrierProcedure.Modifies.Add(AccessSet2);

             }

             bb.simpleCmds.Add(new HavocCmd(tok, VariablesToHavoc));

 

diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs
index e8623e3b..d55c5d05 100644
--- a/Source/GPUVerify/WriteCollector.cs
+++ b/Source/GPUVerify/WriteCollector.cs
@@ -13,15 +13,15 @@ namespace GPUVerify
 

         private AccessRecord access = null;

 

-        public WriteCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)

-            : base(GlobalVariables, TileStaticVariables)

+        public WriteCollector(INonLocalState NonLocalState)

+            : base(NonLocalState)

         {

         }

 

         public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

         {

             Debug.Assert(NoWrittenVariable());

-            if (GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable))

+            if (NonLocalState.Contains(node.DeepAssignedVariable))

             {

                 access = new AccessRecord(node.DeepAssignedVariable, null, null, null);

             }

@@ -37,7 +37,7 @@ namespace GPUVerify
         {

             Debug.Assert(NoWrittenVariable());

 

-            if (!(GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable)))

+            if (!NonLocalState.Contains(node.DeepAssignedVariable))

             {

                 return node;

             }