Merge

28 files changed, 700 insertions, 617 deletions

diff --git a/.hgtags b/.hgtags
index 631a73de..753b727a 100644
--- a/.hgtags
+++ b/.hgtags
@@ -8,3 +8,4 @@ e57f596b36edd27f66ff7400a6610034ce67d19d emicvccbld_build_2.1.30905.0
 8b7a180291a5ecb7d1ffa0dbc3483cc4f7685064 emicvccbld_build_2.1.31020.0
 f59d45429b672bb429d26e1aff6e9df1d9def6b5 emicvccbld_build_2.1.31022.0
 f3b3df39e9877fb2b3fde172f300f995689e6402 emicvccbld_build_2.1.31028.0
+f5c14add09d2f57402c94574eeef490d900d58e8 emicvccbld_build_2.1.31109.0
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1fe21204..c954c019 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -326,6 +326,14 @@ axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
 axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::

   { Seq#FromArray(update(h, a, IndexField(i), v), a) }

     0 <= i && i < array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );

+/**** Someday:

+axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }

+    $IsGoodHeap(h) &&

+    a != null && read(h, a, alloc) && dtype(a) == class.array && TypeParams(a, 0) == class.bool

+    ==>

+    (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }

+      0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==>  $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));

+****/

 

 // Commutability of Take and Drop with Update.

 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::

@@ -379,6 +387,7 @@ const unique class.bool: ClassName;
 const unique class.set: ClassName;

 const unique class.seq: ClassName;

 const unique class.multiset: ClassName;

+const unique class.array: ClassName;

 

 function /*{:never_pattern true}*/ dtype(ref): ClassName;

 function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a4d99bd0..2d3ddcca 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2674,6 +2674,11 @@ namespace Microsoft.Dafny {
                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

                 }

                 expr.Type = Type.Bool;

+              } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsDatatype) {

+                if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {

+                  Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);

+                }

+                expr.Type = Type.Bool;

               } else {

                 bool err = false;

                 if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {

@@ -3768,7 +3773,7 @@ namespace Microsoft.Dafny {
             return BinaryExpr.ResolvedOpcode.Disjoint;

           } 

         case BinaryExpr.Opcode.Lt:

-          if (operandType.IsDatatype) {

+          if (operandType.IsDatatype || operandType is DatatypeProxy) {

             return BinaryExpr.ResolvedOpcode.RankLt;

           } else if (operandType is SetType) {

             return BinaryExpr.ResolvedOpcode.ProperSubset;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2cc15c5a..e455561a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -54,6 +54,7 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type DtCtorId;

       public readonly Bpl.Expr Null;

       private readonly Bpl.Constant allocField;

+      public readonly Bpl.Constant ClassDotArray;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(RefType != null);

@@ -71,6 +72,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(DtCtorId != null);

         Contract.Invariant(Null != null);

         Contract.Invariant(allocField != null);

+        Contract.Invariant(ClassDotArray != null);

       }

 

 

@@ -116,7 +118,7 @@ namespace Microsoft.Dafny {
                              Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,

                              Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,

                              Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,

-                             Bpl.Constant allocField) {

+                             Bpl.Constant allocField, Bpl.Constant classDotArray) {

         #region Non-null preconditions on parameters

         Contract.Requires(refType != null);

         Contract.Requires(boxType != null);

@@ -130,6 +132,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(datatypeType != null);

         Contract.Requires(dtCtorId != null);

         Contract.Requires(allocField != null);

+        Contract.Requires(classDotArray != null);

         #endregion

 

         Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());

@@ -148,6 +151,7 @@ namespace Microsoft.Dafny {
         this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());

         this.allocField = allocField;

         this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);

+        this.ClassDotArray = classDotArray;

       }

     }

 

@@ -171,6 +175,7 @@ namespace Microsoft.Dafny {
       Bpl.TypeCtorDecl tickType = null;

       Bpl.GlobalVariable heap = null;

       Bpl.Constant allocField = null;

+      Bpl.Constant classDotArray = null;

       foreach (var d in prog.TopLevelDeclarations) {

         if (d is Bpl.TypeCtorDecl) {

           Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;

@@ -203,6 +208,8 @@ namespace Microsoft.Dafny {
           Bpl.Constant c = (Bpl.Constant)d;

           if (c.Name == "alloc") {

             allocField = c;

+          } else if (c.Name == "class.array") {

+            classDotArray = c;

           }

         } else if (d is Bpl.GlobalVariable) {

           Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;

@@ -241,10 +248,12 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");

       } else if (allocField == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");

+      } else if (classDotArray == null) {

+        Console.WriteLine("Error: Dafny prelude is missing declaration of class.array");

       } else {

         return new PredefinedDecls(refType, boxType, tickType,

                                    setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,

-                                   allocField);

+                                   allocField, classDotArray);

       }

       return null;

     }

@@ -520,7 +529,11 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(c != null);

-      sink.TopLevelDeclarations.Add(GetClass(c));

+      if (c.Name == "array") {

+        classes.Add(c, predef.ClassDotArray);

+      } else {

+        sink.TopLevelDeclarations.Add(GetClass(c));

+      }

 

       foreach (MemberDecl member in c.Members) {

         if (member is Field) {

@@ -1514,6 +1527,25 @@ namespace Microsoft.Dafny {
       //   }

       // Here go the postconditions (termination checks included, but no reads checks)

       StmtListBuilder postCheckBuilder = new StmtListBuilder();

+      // Assume the type returned by the call itself respects its type (this matter if the type is "nat", for example)

+      {

+        var args = new Bpl.ExprSeq();

+        args.Add(etran.HeapExpr);

+        if (!f.IsStatic) {

+          args.Add(new Bpl.IdentifierExpr(f.tok, etran.This, predef.RefType));

+        }

+        foreach (var p in f.Formals) {

+          args.Add(new Bpl.IdentifierExpr(p.tok, p.UniqueName, TrType(p.Type)));

+        }

+        Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1), TrType(f.ResultType));

+        Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);

+

+        var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);

+        if (wh != null) {

+          postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, wh));

+        }

+      }

+      // Now for the ensures clauses

       foreach (Expression p in f.Ens) {

         CheckWellformed(p, new WFOptions(f, f, false), locals, postCheckBuilder, etran);

         // assume the postcondition for the benefit of checking the remaining postconditions

@@ -3109,7 +3141,7 @@ namespace Microsoft.Dafny {
       } else if (type.IsRefType) {

         // object and class types translate to ref

         return predef.RefType;

-      } else if (type.IsDatatype) {

+      } else if (type.IsDatatype || type is DatatypeProxy) {

         return predef.DatatypeType;

       } else if (type is SetType) {

         return predef.SetType(Token.NoToken, predef.BoxType);

@@ -4513,13 +4545,14 @@ namespace Microsoft.Dafny {
         Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));

         Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);

 

+        Bpl.Expr isGoodMultiset = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);

         Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);

         if (wh != null) {

           Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));

-          return Bpl.Expr.And(FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, Bpl.Type.Bool, x),

-                              new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh)));

+          var q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));

+          isGoodMultiset = Bpl.Expr.And(isGoodMultiset, q);

         }

-        return FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);

+        return isGoodMultiset;

       } else if (type is SeqType) {

         SeqType st = (SeqType)type;

         // (forall i: int :: { Seq#Index(x,i) }

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;

             }

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index c1d7fcd3..afcb0fe6 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -159,7 +159,13 @@ namespace Microsoft.Boogie.ModelViewer
 

       Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>

       {

-        var ch = nodes.ToDictionary(x => x.Name);

+        var ch = new Dictionary<string, IDisplayNode>();

+        foreach (var x in nodes) {

+          if (ch.ContainsKey(x.Name)) {

+            // throw new System.InvalidOperationException("duplicated model entry: " + x.Name);

+          }

+          ch[x.Name] = x;

+        }

         foreach (var k in SortFields(nodes))

           workList.Enqueue(ch[k]);

       };

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index ede520cb..10e4db10 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -307,6 +307,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         res = 1;

       else if (name.EndsWith("#frame"))

         res = 2;

+      else if (name.Contains("#limited#"))

+        res = 2;

       else {

         for (int i = 0; i < prefixes.Length; ++i)

           foreach (var p in prefixes[i])

@@ -314,7 +316,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
               res = i;

               //goto stop;

             }

-      //stop: ;

+        //stop: ;

       }

 

       if (res == -1)

@@ -395,6 +397,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return name.Substring(2);

       }

 

+      if (name.StartsWith("OP#")) {

+        kind = "out-param";

+        return name.Substring(3);

+      }

+

       if (name.StartsWith("SL#")) {

         kind = "spec local";

         return name.Substring(3);

@@ -500,7 +507,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       foreach (var app in elt.Names)

         if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^")) {

-          var n = app.Func.Name.Substring(1); 

+          var n = app.Func.Name.Substring(1);

           switch (n) {

             case "^i1": return "int8_t";

             case "^u1": return "uint8_t";

@@ -511,8 +518,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             case "^i8": return "int64_t";

             case "^u8": return "uint64_t";

             case "^bool": return "bool";

-            default: return n;

-          }          

+            default:

+              var pref = "_vcc_math_type_";

+              if (n.StartsWith(pref)) n = n.Substring(pref.Length);

+              return n;

+          }

         }

 

       return null;

@@ -676,12 +686,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var fldName = tpl.Func.Name.Substring(3);

         var idx = fldName.LastIndexOf('.');

         if (idx > 0) {

-          return fldName.Substring(0, idx);

+          return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");
         }

       }

 

       if (tpl.Args.Length == 1 && tpl.Args[0] == elt && (fname.StartsWith("DSZ#") || fname.StartsWith("RSZ#") || fname.StartsWith("DGH#"))) {

-        return fname.Substring(4);

+        return fname.Substring(4).Replace("_vcc_math_type_", "");

       }

       return null;

     }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bdbb8822..bae3aa50 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -133,8 +133,11 @@ Execution trace:
     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

+NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon3_Then

 

-Dafny program verifier finished with 12 verified, 8 errors

+Dafny program verifier finished with 15 verified, 9 errors

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 47bc22e1..0513591c 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -108,3 +108,30 @@ function Abs(x: int): nat
 {

   if 0 <= x then x else -x

 }

+

+// ----- Here are tests that the type of the result value of a function is known by the

+// ----- time the well-formedness of the function's specification is checked.

+

+function TakesANat(n: nat): bool

+{

+  n < 29

+}

+

+function Naturally(): nat

+  ensures TakesANat(Naturally());  // the wellformedness of this check requires 

+{

+  17

+}

+

+function Integrally_Bad(): int

+  ensures TakesANat(Integrally_Bad());  // error: well-formedness check fails

+{

+  17

+}

+

+function Integrally_Good(): int

+  ensures 0 <= Integrally_Good();

+  ensures TakesANat(Integrally_Good());  // here, the needed information follows from the preceding ensures clause

+{

+  17

+}

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index cf603751..7235303a 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -39,7 +39,7 @@
         "assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"

         "old" "forall" "exists" "new" "parallel" "in" "this" "fresh" "allocated"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

-   `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "nat" "int" "object" "set" "seq")) . font-lock-type-face)

+   `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "nat" "int" "object" "set" "seq")) . font-lock-type-face)

    )

   "Minimal highlighting for Dafny mode")

 

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 6f9ec810..557beb32 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -12,7 +12,8 @@ namespace Demo
         #region 1. Terminals

         NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");

 

-        IdentifierTerminal ident = new IdentifierTerminal("Identifier");

+        IdentifierTerminal ident = new IdentifierTerminal("Identifier", "'_?", "'_?");

+

         StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");

 

         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below

@@ -351,7 +352,6 @@ namespace Demo
           | "==>"

           | "<==>"

           | "#"

-          | "?" // this is not an operator, but a possible character in identifiers

           | n

           | stringLiteral

           ;

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index f80acc26..e8e94e17 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -266,6 +266,7 @@ namespace DafnyLanguage
                 case "method":

                 case "modifies":

                 case "module":

+                case "multiset":

                 case "nat":

                 case "new":

                 case "null":

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 1bbab1b7..34ee3d1d 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,7 +5,7 @@
 \usepackage{listings}

 

 \lstdefinelanguage{dafny}{

-  morekeywords={class,datatype,bool,nat,int,object,set,seq,array,array2,array3,%

+  morekeywords={class,datatype,bool,nat,int,object,set,multiset,seq,array,array2,array3,%

       function,unlimited,

       ghost,var,static,refines,replaces,by,

       method,constructor,returns,module,imports,in,

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 2d0aeab3..b806fb0b 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -11,7 +11,7 @@ syntax keyword dafnyConditional if then else match case
 syntax keyword dafnyRepeat while parallel
 syntax keyword dafnyStatement havoc assume assert return new print break label
 syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
-syntax keyword dafnyType bool nat int seq set object array array2 array3
+syntax keyword dafnyType bool nat int seq set multiset object array array2 array3
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
 syntax keyword dafnyOperator forall exists old fresh allocated choose
 syntax keyword dafnyBoolean true false