Merge

7 files changed, 291 insertions, 240 deletions

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

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+using System.Diagnostics.Contracts;

+

+namespace GPUVerify {

+

+  class AdversarialAbstraction {

+

+    private GPUVerifier verifier;

+

+    internal AdversarialAbstraction(GPUVerifier verifier) {

+      this.verifier = verifier;

+    }

+

+    internal void Abstract() {

+      List<Declaration> NewTopLevelDeclarations = new List<Declaration>();

+      foreach (Declaration d in verifier.Program.TopLevelDeclarations) {

+        if (d is Variable && verifier.KernelArrayInfo.Contains(d as Variable) &&

+          verifier.ArrayModelledAdversarially(d as Variable)) {

+          continue;

+        }

+

+        if (d is Implementation) {

+          Abstract(d as Implementation);

+        }

+

+        if (d is Procedure) {

+          Abstract(d as Procedure);

+        }

+

+        NewTopLevelDeclarations.Add(d);

+

+      }

+

+      verifier.Program.TopLevelDeclarations = NewTopLevelDeclarations;

+

+      AbstractRequiresClauses(verifier.KernelProcedure);

+    }

+

+

+    private void AbstractRequiresClauses(Procedure proc) {

+      RequiresSeq newRequires = new RequiresSeq();

+      foreach (Requires r in proc.Requires) {

+        var visitor = new AccessesAdversarialArrayVisitor(verifier);

+        visitor.VisitRequires(r);

+        if (!visitor.found) {

+          newRequires.Add(r);

+        }

+      }

+      proc.Requires = newRequires;

+    }

+

+    private void Abstract(Procedure proc) {

+      AbstractModifiesSet(proc);

+    }

+

+    private void AbstractModifiesSet(Procedure proc) {

+      IdentifierExprSeq NewModifies = new IdentifierExprSeq();

+      foreach (IdentifierExpr e in proc.Modifies) {

+        var visitor = new AccessesAdversarialArrayVisitor(verifier);

+        visitor.VisitIdentifierExpr(e);

+        if(!visitor.found) {

+          NewModifies.Add(e);

+        }

+      }

+      proc.Modifies = NewModifies;

+    }

+

+    private void Abstract(Implementation impl) {

+      VariableSeq NewLocVars = new VariableSeq();

+

+      foreach (Variable v in impl.LocVars) {

+        Debug.Assert(!verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v));

+        NewLocVars.Add(v);

+      }

+

+      impl.LocVars = NewLocVars;

+

+      if (CommandLineOptions.Unstructured)

+        impl.Blocks = impl.Blocks.Select(Abstract).ToList();

+      else

+        impl.StructuredStmts = Abstract(impl.StructuredStmts);

+    }

+

+

+    private StmtList Abstract(StmtList stmtList) {

+      Contract.Requires(stmtList != null);

+

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

+

+      foreach (BigBlock bodyBlock in stmtList.BigBlocks) {

+        result.BigBlocks.Add(Abstract(bodyBlock));

+      }

+      return result;

+    }

+

+    private CmdSeq Abstract(CmdSeq cs) {

+      var result = new CmdSeq();

+

+      foreach (Cmd c in cs) {

+        if (c is AssignCmd) {

+          AssignCmd assign = c as AssignCmd;

+

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

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

+

+          for (int i = 0; i != assign.Lhss.Count; i++) {

+            AssignLhs lhs = assign.Lhss[i];

+            Expr rhs = assign.Rhss[i];

+            ReadCollector rc = new ReadCollector(verifier.KernelArrayInfo);

+            rc.Visit(rhs);

+

+            bool foundAdversarial = false;

+            foreach (AccessRecord ar in rc.accesses) {

+              if (verifier.ArrayModelledAdversarially(ar.v)) {

+                foundAdversarial = true;

+                break;

+              }

+            }

+

+            if (foundAdversarial) {

+              Debug.Assert(lhs is SimpleAssignLhs);

+              result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));

+              continue;

+            }

+

+            WriteCollector wc = new WriteCollector(verifier.KernelArrayInfo);

+            wc.Visit(lhs);

+            if (wc.GetAccess() != null && verifier.ArrayModelledAdversarially(wc.GetAccess().v)) {

+              continue; // Just remove the write

+            }

+

+            lhss.Add(lhs);

+            rhss.Add(rhs);

+          }

+

+          if (lhss.Count != 0) {

+            result.Add(new AssignCmd(assign.tok, lhss, rhss));

+          }

+          continue;

+        }

+        result.Add(c);

+      }

+

+      return result;

+    }

+

+    private Block Abstract(Block b) {

+      b.Cmds = Abstract(b.Cmds);

+      return b;

+    }

+

+    private BigBlock Abstract(BigBlock bb) {

+      BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

+

+      result.simpleCmds = Abstract(bb.simpleCmds);

+

+      if (bb.ec is WhileCmd) {

+        WhileCmd WhileCommand = bb.ec as WhileCmd;

+        result.ec =

+            new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, Abstract(WhileCommand.Body));

+      }

+      else if (bb.ec is IfCmd) {

+        IfCmd IfCommand = bb.ec as IfCmd;

+        Debug.Assert(IfCommand.elseIf == null);

+        result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, Abstract(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? Abstract(IfCommand.elseBlock) : null);

+      }

+      else {

+        Debug.Assert(bb.ec == null || bb.ec is BreakCmd);

+      }

+

+      return result;

+

+    }

+

+    class AccessesAdversarialArrayVisitor : StandardVisitor {

+      internal bool found;

+      private GPUVerifier verifier;

+

+      internal AccessesAdversarialArrayVisitor(GPUVerifier verifier) {

+        this.found = false;

+        this.verifier = verifier;

+      }

+

+      public override Variable VisitVariable(Variable v) {

+        if (verifier.KernelArrayInfo.Contains(v)) {

+          if (verifier.ArrayModelledAdversarially(v)) {

+            found = true;

+          }

+        }

+        return base.VisitVariable(v);

+      }

+

+    }

+  

+  }

+

+

+}

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 0144174f..d2ae0ad8 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -61,9 +61,6 @@ namespace GPUVerify
         internal static Constant _NUM_GROUPS_Y = null;

         internal static Constant _NUM_GROUPS_Z = null;

 

-        internal const int CLK_LOCAL_MEM_FENCE = 1;

-        internal const int CLK_GLOBAL_MEM_FENCE = 2;

-

         public IRaceInstrumenter RaceInstrumenter;

 

         public UniformityAnalyser uniformityAnalyser;

@@ -120,7 +117,9 @@ namespace GPUVerify
             if (p == null)

             {

                 p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),

-                                  new VariableSeq(new Variable[] { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__flags", new BvType(32)), true) }),

+                                  new VariableSeq(new Variable[] { 

+                                    new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__local_fence", new BvType(1)), true),

+                                    new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__global_fence", new BvType(1)), true) }),

                                   new VariableSeq(),

                                   new RequiresSeq(), new IdentifierExprSeq(),

                                   new EnsuresSeq(),

@@ -366,6 +365,10 @@ namespace GPUVerify
 

             preProcess();

 

+            if (CommandLineOptions.ShowStages) {

+              emitProgram(outputFilename + "_preprocessed");

+            }

+

             DoLiveVariableAnalysis();

 

             DoUniformityAnalysis();

@@ -378,17 +381,17 @@ namespace GPUVerify
 

             DoArrayControlFlowAnalysis();

 

-            if (CommandLineOptions.ShowStages)

-            {

-                emitProgram(outputFilename + "_preprocessed");

-            }

-

             if (CommandLineOptions.Inference)

             {

                 foreach (var impl in Program.TopLevelDeclarations.OfType<Implementation>().ToList())

                 {

                     LoopInvariantGenerator.PreInstrument(this, impl);

                 }

+

+                if (CommandLineOptions.ShowStages) {

+                  emitProgram(outputFilename + "_pre_inference");

+                }

+

             }

 

             RaceInstrumenter.AddRaceCheckingInstrumentation();

@@ -433,11 +436,6 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_dualised");

             }

 

-            if (CommandLineOptions.ShowStages)

-            {

-                emitProgram(outputFilename + "_cross_thread_invariants");

-            }

-

             RaceInstrumenter.AddRaceCheckingDeclarations();

 

             GenerateBarrierImplementation();

@@ -1337,8 +1335,11 @@ namespace GPUVerify
             IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));

             IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread].TypedIdent));

 

-            IdentifierExpr Flags1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));

-            IdentifierExpr Flags2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread + 1].TypedIdent));

+            Expr LocalFence1 = MakeFenceExpr(BarrierProcedure.InParams[1]);

+            Expr LocalFence2 = MakeFenceExpr(BarrierProcedure.InParams[paramsPerThread + 1]);

+

+            Expr GlobalFence1 = MakeFenceExpr(BarrierProcedure.InParams[2]);

+            Expr GlobalFence2 = MakeFenceExpr(BarrierProcedure.InParams[paramsPerThread + 2]);

 

             Expr DivergenceCondition = Expr.Imp(ThreadsInSameGroup(), Expr.Eq(P1, P2));

 

@@ -1359,8 +1360,8 @@ namespace GPUVerify
 

             if(KernelArrayInfo.getGroupSharedArrays().Count > 0) {

 

-                Expr IfGuard1 = Expr.And(P1, CLK_LOCAL_MEM_FENCE_isSet(Flags1));

-                Expr IfGuard2 = Expr.And(P2, CLK_LOCAL_MEM_FENCE_isSet(Flags2));

+                Expr IfGuard1 = Expr.And(P1, LocalFence1);

+                Expr IfGuard2 = Expr.And(P2, LocalFence2);

 

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

                     new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

@@ -1372,8 +1373,8 @@ namespace GPUVerify
 

             if (KernelArrayInfo.getGlobalArrays().Count > 0)

             {

-                Expr IfGuard1 = Expr.And(P1, CLK_GLOBAL_MEM_FENCE_isSet(Flags1));

-                Expr IfGuard2 = Expr.And(P2, CLK_GLOBAL_MEM_FENCE_isSet(Flags2));

+                Expr IfGuard1 = Expr.And(P1, GlobalFence1);

+                Expr IfGuard2 = Expr.And(P2, GlobalFence2);

 

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

                     new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

@@ -1387,7 +1388,7 @@ namespace GPUVerify
             {

                 if (!ArrayModelledAdversarially(v))

                 {

-                    bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2, Flags1, Flags2));

+                    bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2, LocalFence1, LocalFence2, GlobalFence1, GlobalFence2));

                 }

             }

 

@@ -1407,6 +1408,11 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(BarrierImplementation);

         }

 

+        private static NAryExpr MakeFenceExpr(Variable v) {

+          return Expr.Eq(new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, v.TypedIdent)), 

+            new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));

+        }

+

         private static Expr flagIsSet(Expr Flags, int flag)

         {

             return Expr.Eq(new BvExtractExpr(

@@ -1414,16 +1420,6 @@ namespace GPUVerify
                                     new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));

         }

 

-        private static Expr CLK_GLOBAL_MEM_FENCE_isSet(Expr Flags)

-        {

-            return flagIsSet(Flags, CLK_GLOBAL_MEM_FENCE);

-        }

-

-        private static Expr CLK_LOCAL_MEM_FENCE_isSet(Expr Flags)

-        {

-            return flagIsSet(Flags, CLK_LOCAL_MEM_FENCE);

-        }

-

         private List<BigBlock> MakeResetAndHavocBlocks(int Thread, ICollection<Variable> variables)

         {

             Debug.Assert(variables.Count > 0);

@@ -1466,7 +1462,7 @@ namespace GPUVerify
             return new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { new HavocCmd(Token.NoToken, new IdentifierExprSeq(new IdentifierExpr[] { vForThread })) }), null, null);

         }

 

-        private BigBlock AssumeEqualityBetweenSharedArrays(Variable v, Expr P1, Expr P2, Expr Flags1, Expr Flags2)

+        private BigBlock AssumeEqualityBetweenSharedArrays(Variable v, Expr P1, Expr P2, Expr LocalFence1, Expr LocalFence2, Expr GlobalFence1, Expr GlobalFence2)

         {

             IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));

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

@@ -1478,12 +1474,12 @@ namespace GPUVerify
             if (KernelArrayInfo.getGroupSharedArrays().Contains(v))

             {

                 EqualityCondition = Expr.And(EqualityCondition,

-                    Expr.And(CLK_LOCAL_MEM_FENCE_isSet(Flags1), CLK_LOCAL_MEM_FENCE_isSet(Flags2)));

+                    Expr.And(LocalFence1, LocalFence2));

             }

             else if (KernelArrayInfo.getGlobalArrays().Contains(v))

             {

                 EqualityCondition = Expr.And(EqualityCondition,

-                    Expr.And(CLK_GLOBAL_MEM_FENCE_isSet(Flags1), CLK_GLOBAL_MEM_FENCE_isSet(Flags2)));

+                    Expr.And(GlobalFence1, GlobalFence2));

             }

 

             AssumeGuard = Expr.Imp(EqualityCondition, AssumeGuard);

@@ -1506,172 +1502,7 @@ namespace GPUVerify
 

         private void AbstractSharedState()

         {

-            List<Declaration> NewTopLevelDeclarations = new List<Declaration>();

-

-            foreach (Declaration d in Program.TopLevelDeclarations)

-            {

-                if (d is Variable && KernelArrayInfo.Contains(d as Variable) && ArrayModelledAdversarially(d as Variable))

-                {

-                    continue;

-                }

-

-                if (d is Implementation)

-                {

-                    PerformFullSharedStateAbstraction(d as Implementation);

-                }

-

-                if (d is Procedure)

-                {

-                    PerformFullSharedStateAbstraction(d as Procedure);

-                }

-

-                NewTopLevelDeclarations.Add(d);

-

-            }

-

-            Program.TopLevelDeclarations = NewTopLevelDeclarations;

-

-        }

-

-        private void PerformFullSharedStateAbstraction(Procedure proc)

-        {

-            IdentifierExprSeq NewModifies = new IdentifierExprSeq();

-

-            foreach (IdentifierExpr e in proc.Modifies)

-            {

-                if (!KernelArrayInfo.Contains(e.Decl) || !ArrayModelledAdversarially(e.Decl))

-                {

-                    NewModifies.Add(e);

-                }

-            }

-

-            proc.Modifies = NewModifies;

-

-        }

-

-        private void PerformFullSharedStateAbstraction(Implementation impl)

-        {

-            VariableSeq NewLocVars = new VariableSeq();

-

-            foreach (Variable v in impl.LocVars)

-            {

-                Debug.Assert(!KernelArrayInfo.getGroupSharedArrays().Contains(v));

-                NewLocVars.Add(v);

-            }

-

-            impl.LocVars = NewLocVars;

-

-            if (CommandLineOptions.Unstructured)

-                impl.Blocks = impl.Blocks.Select(PerformFullSharedStateAbstraction).ToList();

-            else

-                impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);

-        }

-

-

-        private StmtList PerformFullSharedStateAbstraction(StmtList stmtList)

-        {

-            Contract.Requires(stmtList != null);

-

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

-

-            foreach (BigBlock bodyBlock in stmtList.BigBlocks)

-            {

-                result.BigBlocks.Add(PerformFullSharedStateAbstraction(bodyBlock));

-            }

-            return result;

-        }

-

-        private CmdSeq PerformFullSharedStateAbstraction(CmdSeq cs)

-        {

-            var result = new CmdSeq();

-

-            foreach (Cmd c in cs)

-            {

-                if (c is AssignCmd)

-                {

-                    AssignCmd assign = c as AssignCmd;

-

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

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

-

-                    for (int i = 0; i != assign.Lhss.Count; i++)

-                    {

-                        AssignLhs lhs = assign.Lhss[i];

-                        Expr rhs = assign.Rhss[i];

-                        ReadCollector rc = new ReadCollector(KernelArrayInfo);

-                        rc.Visit(rhs);

-

-                        bool foundAdversarial = false;

-                        foreach (AccessRecord ar in rc.accesses)

-                        {

-                            if (ArrayModelledAdversarially(ar.v))

-                            {

-                                foundAdversarial = true;

-                                break;

-                            }

-                        }

-

-                        if (foundAdversarial)

-                        {

-                            Debug.Assert(lhs is SimpleAssignLhs);

-                            result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));

-                            continue;

-                        }

-

-                        WriteCollector wc = new WriteCollector(KernelArrayInfo);

-                        wc.Visit(lhs);

-                        if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))

-                        {

-                            continue; // Just remove the write

-                        }

-

-                        lhss.Add(lhs);

-                        rhss.Add(rhs);

-                    }

-

-                    if (lhss.Count != 0)

-                    {

-                        result.Add(new AssignCmd(assign.tok, lhss, rhss));

-                    }

-                    continue;

-                }

-                result.Add(c);

-            }

-

-            return result;

-        }

-

-        private Block PerformFullSharedStateAbstraction(Block b)

-        {

-            b.Cmds = PerformFullSharedStateAbstraction(b.Cmds);

-            return b;

-        }

-

-        private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)

-        {

-            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

-

-            result.simpleCmds = PerformFullSharedStateAbstraction(bb.simpleCmds);

-

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd WhileCommand = bb.ec as WhileCmd;

-                result.ec = 

-                    new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, PerformFullSharedStateAbstraction(WhileCommand.Body));

-            }

-            else if (bb.ec is IfCmd)

-            {

-                IfCmd IfCommand = bb.ec as IfCmd;

-                Debug.Assert(IfCommand.elseIf == null);

-                result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, PerformFullSharedStateAbstraction(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? PerformFullSharedStateAbstraction(IfCommand.elseBlock) : null);

-            }

-            else

-            {

-                Debug.Assert(bb.ec == null || bb.ec is BreakCmd);

-            }

-

-            return result;

-

+          new AdversarialAbstraction(this).Abstract();

         }

 

         internal static string MakeOffsetVariableName(string Name, string AccessType)

@@ -2150,13 +1981,16 @@ namespace GPUVerify
                 return ErrorCount;

             }

 

-            if (BarrierProcedure.InParams.Length != 1)

+            if (BarrierProcedure.InParams.Length != 2)

             {

-                Error(BarrierProcedure, "Barrier procedure must take exactly one argument");

+                Error(BarrierProcedure, "Barrier procedure must take exactly two arguments");

             }

-            else if (!BarrierProcedure.InParams[0].TypedIdent.Type.Equals(new BvType(32)))

+            else if (!BarrierProcedure.InParams[0].TypedIdent.Type.Equals(new BvType(1)))

             {

-                Error(BarrierProcedure, "Argument to barrier procedure must have type bv32");

+                Error(BarrierProcedure, "First argument to barrier procedure must have type bv1");

+            }

+            else if (!BarrierProcedure.InParams[1].TypedIdent.Type.Equals(new BvType(1))) {

+              Error(BarrierProcedure, "Second argument to barrier procedure must have type bv1");

             }

 

             if (BarrierProcedure.OutParams.Length != 0)

@@ -2359,6 +2193,13 @@ namespace GPUVerify
             else

                 return (Expr)new VariableDualiser(id, uniformityAnalyser, procName).Visit(e.Clone());

         }

+

+        internal static bool IsConstantInCurrentRegion(IdentifierExpr expr) {

+          return (expr.Decl is Constant) ||

+                 (expr.Decl is Formal && ((Formal)expr.Decl).InComing);

+        }

+    

     }

 

+

 }

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 47965b43..08913944 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -105,6 +105,7 @@
   <ItemGroup>

     <Compile Include="AccessCollector.cs" />

     <Compile Include="AccessRecord.cs" />

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

     <Compile Include="ArrayControlFlowAnalyser.cs" />

     <Compile Include="AsymmetricExpressionFinder.cs" />

     <Compile Include="StrideConstraint.cs" />

diff --git a/Source/GPUVerify/StrideConstraint.cs b/Source/GPUVerify/StrideConstraint.cs
index 948786b7..da970365 100644
--- a/Source/GPUVerify/StrideConstraint.cs
+++ b/Source/GPUVerify/StrideConstraint.cs
@@ -99,7 +99,7 @@ class StrideConstraint {
 

     var ie = e as IdentifierExpr;

     if (ie != null) {

-      if (ie.Decl is Constant)

+      if(GPUVerifier.IsConstantInCurrentRegion(ie))

         return new EqStrideConstraint(e);

 

       var rsa = verifier.reducedStrengthAnalyses[impl];

diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs
index 100dbc0e..824c1b17 100644
--- a/Source/GPUVerify/VariableDefinitionAnalysis.cs
+++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs
@@ -2,6 +2,7 @@ using System;
 using Microsoft.Boogie;

 using System.Collections.Generic;

 using System.Linq;

+using System.Diagnostics;

 

 namespace GPUVerify {

 

@@ -43,7 +44,7 @@ class VariableDefinitionAnalysis {
     }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

-      if (expr.Decl is Constant)

+      if (GPUVerifier.IsConstantInCurrentRegion(expr))

         return expr;

       if (!analysis.defMap.ContainsKey(expr.Decl) || !analysis.defMap[expr.Decl].Item2)

         isDerivedFromConstants = false;

@@ -117,7 +118,7 @@ class VariableDefinitionAnalysis {
     }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

-      if (expr.Decl is Constant)

+      if (GPUVerifier.IsConstantInCurrentRegion(expr))

         return expr;

       var def = analysis.BuildNamedDefFor(expr.Decl, expr);

       if (def == null)

@@ -178,7 +179,7 @@ class VariableDefinitionAnalysis {
     }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

-      if (expr.Decl is Constant)

+      if (GPUVerifier.IsConstantInCurrentRegion(expr))

         return expr;

       int id;

       var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name, out id);

diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index 110e6a17..d5d9917a 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -29,22 +29,27 @@ namespace GPUVerify
 

         public override Expr VisitIdentifierExpr(IdentifierExpr node)

         {

-            if (!(node.Decl is Constant))

-            {

-                return new IdentifierExpr(node.tok, new LocalVariable(node.tok, DualiseTypedIdent(node.Decl)));

-            }

-

-            if (GPUVerifier.IsThreadLocalIdConstant(node.Decl))

-            {

-                return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));

-            }

-

-            if (GPUVerifier.IsGroupIdConstant(node.Decl))

-            {

-                return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));

-            }

-

-            return node;

+          if (node.Decl is Formal) {

+            return new IdentifierExpr(node.tok, new Formal(node.tok, DualiseTypedIdent(node.Decl),

+              (node.Decl as Formal).InComing));

+          }

+

+          if (!(node.Decl is Constant))

+          {

+              return new IdentifierExpr(node.tok, new LocalVariable(node.tok, DualiseTypedIdent(node.Decl)));

+          }

+

+          if (GPUVerifier.IsThreadLocalIdConstant(node.Decl))

+          {

+              return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));

+          }

+

+          if (GPUVerifier.IsGroupIdConstant(node.Decl))

+          {

+              return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));

+          }

+

+          return node;

         }

 

         private TypedIdent DualiseTypedIdent(Variable v)

diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
index 4374a0cc..5b823791 100644
--- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
+++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
@@ -602,14 +602,13 @@ namespace Microsoft.Boogie
     static QKeyValue GetSourceLocInfo(Counterexample error, string AccessType) {

       string sourceVarName = null;

       int sourceLocLineNo = -1;

-      int currLineNo = -1;

-      string fileLine;

-      string[] slocTokens = null;

-      int line = -1;

-      int col = -1;

-      string fname = null;

-      string dir = null;

-      TextReader tr = new StreamReader(Path.GetFileNameWithoutExtension(CommandLineOptions.Clo.Files[0]) + ".loc");

+

+      string sourceLocFileName = Path.GetDirectoryName(CommandLineOptions.Clo.Files[0]) +

+                 Path.DirectorySeparatorChar +

+                 Path.GetFileNameWithoutExtension(CommandLineOptions.Clo.Files[0]) +

+                 ".loc";

+

+      TextReader tr = new StreamReader(sourceLocFileName);

 

       foreach (Block b in error.Trace)

       {

@@ -632,9 +631,10 @@ namespace Microsoft.Boogie
       

       if (sourceLocLineNo != 0 && sourceLocLineNo != -1)

       {

-        while ((fileLine = tr.ReadLine()) != null)

+        string fileLine;

+        int currLineNo;

+        for(currLineNo = 0; ((fileLine = tr.ReadLine()) != null); currLineNo++)

         {

-          currLineNo++;

           if (currLineNo == sourceLocLineNo)

           {

             break;

@@ -648,12 +648,12 @@ namespace Microsoft.Boogie
         }

         if (fileLine != null)

         {

-          slocTokens = Regex.Split(fileLine, "#");

-          line = System.Convert.ToInt32(slocTokens[0]);

-          col = System.Convert.ToInt32(slocTokens[1]);

-          fname = slocTokens[2];

-          dir = slocTokens[3];

-          return CreateSourceLocQKV(line, col, fname, dir);

+          string[] slocTokens = Regex.Split(fileLine, "#");

+          return CreateSourceLocQKV(

+                  System.Convert.ToInt32(slocTokens[0]),

+                  System.Convert.ToInt32(slocTokens[1]),

+                  slocTokens[2], 

+                  slocTokens[3]);

         }

       }

       else