Revised candidate invariant generation for barrier divergence checking.

3 files changed, 248 insertions, 198 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index e64ace68..85d559d0 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -27,9 +27,6 @@ namespace GPUVerify
 

         public static bool ShowStages = false;

 

-        public static bool AddDivergenceCandidatesOnlyIfModified = true;

-        public static bool AddDivergenceCandidatesOnlyToBarrierLoops = true;

-

         public static bool ShowUniformityAnalysis = false;

         public static bool DoUniformityAnalysis = true;

 

@@ -139,12 +136,6 @@ namespace GPUVerify
                     ArrayEqualities = true;

                     break;

 

-                    case "-alwaysAddDivergenceCandidates":

-                    case "/alwaysAddDivergenceCandidates":

-                    AddDivergenceCandidatesOnlyIfModified = false;

-                    AddDivergenceCandidatesOnlyToBarrierLoops = false;

-                    break;

-

                     case "-showUniformityAnalysis":

                     case "/showUniformityAnalysis":

                     ShowUniformityAnalysis = true;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 5c746f7e..b402ab44 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -784,12 +784,45 @@ namespace GPUVerify
             return false;

         }

 

+        internal static bool IsPredicate(string v) {

+          if (v.Length < 2) {

+            return false;

+          }

+          if (!v.Substring(0, 1).Equals("p")) {

+            return false;

+          }

+          for (int i = 1; i < v.Length; i++) {

+            if (!Char.IsDigit(v.ToCharArray()[i])) {

+              return false;

+            }

+          }

+          return true;

+        }

 

-        internal static bool IsPredicateOrTemp(string lv)

-        {

-            return (lv.Length >= 2 && lv.Substring(0,2).Equals("_P")) ||

-                    (lv.Length > 3 && lv.Substring(0,3).Equals("_LC")) ||

-                    (lv.Length > 5 && lv.Substring(0,5).Equals("_temp"));

+        internal static bool IsPredicateOrTemp(string lv) {

+          

+          // We should improve this by having a general convention

+          // for names of temporary or predicate variables

+

+          if (lv.Length >= 2) {

+            if (lv.Substring(0, 1).Equals("p") || lv.Substring(0, 1).Equals("v")) {

+              for (int i = 1; i < lv.Length; i++) {

+                if (!Char.IsDigit(lv.ToCharArray()[i])) {

+                  return false;

+                }

+              }

+              return true;

+            }

+

+          }

+

+          if (lv.Contains("_HAVOC_")) {

+            return true;

+          }

+

+          return (lv.Length >= 2 && lv.Substring(0,2).Equals("_P")) ||

+                  (lv.Length > 3 && lv.Substring(0,3).Equals("_LC")) ||

+                  (lv.Length > 5 && lv.Substring(0,5).Equals("_temp"));

         }

 

         

diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs
index 300089eb..1c15f5e6 100644
--- a/Source/GPUVerify/LoopInvariantGenerator.cs
+++ b/Source/GPUVerify/LoopInvariantGenerator.cs
@@ -8,225 +8,251 @@ using System.Diagnostics;
 

 using GPUVerify.InvariantGenerationRules;

 

-namespace GPUVerify

-{

-    class LoopInvariantGenerator

-    {

-        private GPUVerifier verifier;

-        private Implementation Impl;

-

-        private List<InvariantGenerationRule> invariantGenerationRules;

-

-        LoopInvariantGenerator(GPUVerifier verifier, Implementation Impl)

-        {

-            this.verifier = verifier;

-            this.Impl = Impl;

-

-            invariantGenerationRules = new List<InvariantGenerationRule>();

-            invariantGenerationRules.Add(new PowerOfTwoInvariantGenerator(verifier));

-            invariantGenerationRules.Add(new LoopVariableBoundsInvariantGenerator(verifier));

-        }

-

-        public static void PreInstrument(GPUVerifier verifier, Implementation impl)

-        {

-            foreach (var region in verifier.RootRegion(impl).SubRegions())

-            {

-                GenerateCandidateForReducedStrengthStrideVariables(verifier, impl, region);

-            }

-        }

+namespace GPUVerify {

+  class LoopInvariantGenerator {

+    private GPUVerifier verifier;

+    private Implementation Impl;

 

-        private static void GenerateCandidateForReducedStrengthStrideVariables(GPUVerifier verifier, Implementation impl, IRegion region)

-        {

-            var rsa = verifier.reducedStrengthAnalyses[impl];

-            foreach (string lc in rsa.StridedLoopCounters(region.Identifier()))

-            {

-                var sc = rsa.GetStrideConstraint(lc);

-                Variable lcVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lc,

-                        Microsoft.Boogie.Type.GetBvType(32)));

-                var lcExpr = new IdentifierExpr(Token.NoToken, lcVariable);

-                var lcPred = sc.MaybeBuildPredicate(verifier, lcExpr);

-

-                if (lcPred != null)

-                {

-                    verifier.AddCandidateInvariant(region, lcPred, "variable " + lc + " is strided");

-                }

-            }

-        }

+    private List<InvariantGenerationRule> invariantGenerationRules;

 

-        public static void PostInstrument(GPUVerifier verifier, Implementation Impl, List<Expr> UserSuppliedInvariants)

-        {

-            new LoopInvariantGenerator(verifier, Impl).PostInstrument(UserSuppliedInvariants);

-        }

+    LoopInvariantGenerator(GPUVerifier verifier, Implementation Impl) {

+      this.verifier = verifier;

+      this.Impl = Impl;

 

-        internal void PostInstrument(List<Expr> UserSuppliedInvariants)

-        {

-                HashSet<Variable> LocalVars = new HashSet<Variable>();

-                foreach (Variable v in Impl.LocVars)

-                {

-                    LocalVars.Add(v);

-                }

-                foreach (Variable v in Impl.InParams)

-                {

-                    LocalVars.Add(v);

-                }

-                foreach (Variable v in Impl.OutParams)

-                {

-                    LocalVars.Add(v);

-                }

+      invariantGenerationRules = new List<InvariantGenerationRule>();

+      invariantGenerationRules.Add(new PowerOfTwoInvariantGenerator(verifier));

+      invariantGenerationRules.Add(new LoopVariableBoundsInvariantGenerator(verifier));

+    }

 

-                AddCandidateInvariants(verifier.RootRegion(Impl), LocalVars, UserSuppliedInvariants, Impl);

+    public static void PreInstrument(GPUVerifier verifier, Implementation impl) {

+      foreach (var region in verifier.RootRegion(impl).SubRegions()) {

+        GenerateCandidateForReducedStrengthStrideVariables(verifier, impl, region);

+      }

+    }

 

+    private static void GenerateCandidateForReducedStrengthStrideVariables(GPUVerifier verifier, Implementation impl, IRegion region) {

+      var rsa = verifier.reducedStrengthAnalyses[impl];

+      foreach (string lc in rsa.StridedLoopCounters(region.Identifier())) {

+        var sc = rsa.GetStrideConstraint(lc);

+        Variable lcVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lc,

+                Microsoft.Boogie.Type.GetBvType(32)));

+        var lcExpr = new IdentifierExpr(Token.NoToken, lcVariable);

+        var lcPred = sc.MaybeBuildPredicate(verifier, lcExpr);

+

+        if (lcPred != null) {

+          verifier.AddCandidateInvariant(region, lcPred, "variable " + lc + " is strided");

         }

+      }

+    }

 

-        private void AddEqualityCandidateInvariant(IRegion region, string LoopPredicate, Variable v)

-        {

-            verifier.AddCandidateInvariant(region,

-                Expr.Eq(

-                    new IdentifierExpr(Token.NoToken, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),

-                    new IdentifierExpr(Token.NoToken, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))

-            ), "equality");

-        }

+    public static void PostInstrument(GPUVerifier verifier, Implementation Impl, List<Expr> UserSuppliedInvariants) {

+      new LoopInvariantGenerator(verifier, Impl).PostInstrument(UserSuppliedInvariants);

+    }

 

-        private void AddPredicatedEqualityCandidateInvariant(IRegion region, string LoopPredicate, Variable v)

-        {

-            verifier.AddCandidateInvariant(region, Expr.Imp(

-                Expr.And(

-                    new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),

-                    new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))

-                ),

-                Expr.Eq(

-                    new IdentifierExpr(Token.NoToken, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),

-                    new IdentifierExpr(Token.NoToken, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))

-            )), "predicated equality");

-        }

+    internal void PostInstrument(List<Expr> UserSuppliedInvariants) {

+      HashSet<Variable> LocalVars = new HashSet<Variable>();

+      foreach (Variable v in Impl.LocVars) {

+        LocalVars.Add(v);

+      }

+      foreach (Variable v in Impl.InParams) {

+        LocalVars.Add(v);

+      }

+      foreach (Variable v in Impl.OutParams) {

+        LocalVars.Add(v);

+      }

 

+      AddCandidateInvariants(verifier.RootRegion(Impl), LocalVars, UserSuppliedInvariants, Impl);

 

-        private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, IRegion region)

-        {

+    }

 

-            if (CommandLineOptions.AddDivergenceCandidatesOnlyToBarrierLoops)

-            {

-                if (!verifier.ContainsBarrierCall(region))

-                {

-                    return;

+    private void AddEqualityCandidateInvariant(IRegion region, string LoopPredicate, Variable v) {

+      verifier.AddCandidateInvariant(region,

+          Expr.Eq(

+              new IdentifierExpr(Token.NoToken, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),

+              new IdentifierExpr(Token.NoToken, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))

+      ), "equality");

+    }

+

+    private void AddPredicatedEqualityCandidateInvariant(IRegion region, string LoopPredicate, Variable v) {

+      verifier.AddCandidateInvariant(region, Expr.Imp(

+          Expr.And(

+              new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),

+              new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))

+          ),

+          Expr.Eq(

+              new IdentifierExpr(Token.NoToken, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),

+              new IdentifierExpr(Token.NoToken, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))

+      )), "predicated equality");

+    }

+

+    private Dictionary<string, int> GetAssignmentCounts(Implementation impl) {

+

+      Dictionary<string, int> result = new Dictionary<string, int>();

+

+      foreach (var c in verifier.RootRegion(impl).Cmds()) {

+        if (c is AssignCmd) {

+          var aCmd = (AssignCmd)c;

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

+          foreach (var a in aCmd.Lhss) {

+            if (a is SimpleAssignLhs) {

+              var v = GPUVerifier.StripThreadIdentifier(

+                ((SimpleAssignLhs)a).AssignedVariable.Name);

+              if (!alreadySeenInThisAssignment.Contains(v)) {

+                if (result.ContainsKey(v)) {

+                  result[v]++;

+                }

+                else {

+                  result[v] = 1;

                 }

+                alreadySeenInThisAssignment.Add(v);

+              }

             }

+          }

+        }

+      }

+      return result;

+    }

 

-            Expr guard = region.Guard();

-            if (verifier.uniformityAnalyser.IsUniform(Impl.Name, guard))

-            {

-                return;

-            }

 

-            if (guard is NAryExpr &&

-                (guard as NAryExpr).Args.Length == 2 &&

-                (guard as NAryExpr).Args[0] is IdentifierExpr)

-            {

-                string LoopPredicate = ((guard as NAryExpr).Args[0] as IdentifierExpr).Name;

+    private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, IRegion region)

+      {

 

-                LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));

+          if (!verifier.ContainsBarrierCall(region))

+          {

+              return;

+          }

 

-                verifier.AddCandidateInvariant(region, Expr.Eq(

-                    // Int type used here, but it doesn't matter as we will print and then re-parse the program

-                    new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),

-                    new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))

-                ), "loop predicate equality");

+          Expr guard = region.Guard();

+          if (verifier.uniformityAnalyser.IsUniform(Impl.Name, guard))

+          {

+              return;

+          }

 

-                foreach (Variable v in LocalVars)

-                {

+          if (IsDisjunctionOfPredicates(guard))

+          {

+              string LoopPredicate = ((guard as NAryExpr).Args[0] as IdentifierExpr).Name;

+              LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));

+

+              verifier.AddCandidateInvariant(region, Expr.Eq(

+                  // Int type used here, but it doesn't matter as we will print and then re-parse the program

+                  new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),

+                  new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))

+              ), "loop predicate equality");

+

+              Dictionary<string, int> assignmentCounts = GetAssignmentCounts(Impl);

+

+              HashSet<string> alreadyConsidered = new HashSet<String>();  

 

-                    if (verifier.uniformityAnalyser.IsUniform(Impl.Name, v.Name))

-                    {

-                        continue;

-                    }

-

-                    string lv = GPUVerifier.StripThreadIdentifier(v.Name);

-

-                    if (GPUVerifier.IsPredicateOrTemp(lv))

-                    {

-                        continue;

-                    }

-

-                    if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)

-                    {

-                        if (!verifier.ContainsNamedVariable(GetModifiedVariables(region),

-                            GPUVerifier.StripThreadIdentifier(v.Name)))

-                        {

-                            continue;

-                        }

-                    }

-

-                    AddEqualityCandidateInvariant(region, LoopPredicate, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lv, Microsoft.Boogie.Type.Int)));

-

-                    if (Impl != verifier.KernelImplementation)

-                    {

-                        AddPredicatedEqualityCandidateInvariant(region, LoopPredicate, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lv, Microsoft.Boogie.Type.Int)));

-                    }

+              foreach (var v in LocalVars)

+              {

+                string lv = GPUVerifier.StripThreadIdentifier(v.Name);

+                if (alreadyConsidered.Contains(lv)) {

+                  continue;

                 }

+                alreadyConsidered.Add(lv);

 

-                if (CommandLineOptions.ArrayEqualities)

+                if (verifier.uniformityAnalyser.IsUniform(Impl.Name, v.Name))

                 {

-                    foreach (Variable v in verifier.KernelArrayInfo.getAllNonLocalArrays())

-                    {

-                        if (!verifier.ArrayModelledAdversarially(v))

-                        {

-                            AddEqualityCandidateInvariant(region, LoopPredicate, v);

-                        }

-                    }

+                    continue;

                 }

-            }

-        }

 

-        private void AddCandidateInvariants(IRegion region, HashSet<Variable> LocalVars, List<Expr> UserSuppliedInvariants, Implementation Impl)

-        {

-            foreach (IRegion subregion in region.SubRegions())

-            {

-                foreach (InvariantGenerationRule r in invariantGenerationRules)

+                if (GPUVerifier.IsPredicate(lv))

                 {

-                    r.GenerateCandidates(Impl, subregion);

+                    continue;

                 }

 

-                AddBarrierDivergenceCandidates(LocalVars, Impl, subregion);

-

-                verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, subregion);

-

-                AddUserSuppliedInvariants(subregion, UserSuppliedInvariants, Impl);

-            }

-        }

+                if (!assignmentCounts.ContainsKey(lv) || assignmentCounts[lv] <= 1) {

+                  continue;

+                }

 

-        private void AddUserSuppliedInvariants(IRegion region, List<Expr> UserSuppliedInvariants, Implementation Impl)

-        {

-            foreach (Expr e in UserSuppliedInvariants)

-            {

-              /*

-                wc.Invariants.Add(new AssertCmd(wc.tok, e));

-                bool OK = verifier.ProgramIsOK(Impl);

-                wc.Invariants.RemoveAt(wc.Invariants.Count - 1);

-                if (OK)

+                if (!verifier.ContainsNamedVariable(

+                      GetModifiedVariables(region), lv))

                 {

-                    verifier.AddCandidateInvariant(wc, e, "user supplied");

+                    continue;

                 }

-              */

-                verifier.AddCandidateInvariant(region, e, "user supplied");

-            }

+

+                AddPredicatedEqualityCandidateInvariant(region, LoopPredicate, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lv, Microsoft.Boogie.Type.Int)));

+              }

+

+              if (CommandLineOptions.ArrayEqualities)

+              {

+                  foreach (Variable v in verifier.KernelArrayInfo.getAllNonLocalArrays())

+                  {

+                      if (!verifier.ArrayModelledAdversarially(v))

+                      {

+                          AddEqualityCandidateInvariant(region, LoopPredicate, v);

+                      }

+                  }

+              }

+          }

+      }

+

+    private static bool IsDisjunctionOfPredicates(Expr guard) {

+      if (!(guard is NAryExpr)) {

+        return false;

+      }

+      NAryExpr nary = (NAryExpr)guard;

+      if(nary.Args.Length != 2) {

+        return false;

+      }

+      if(!(nary.Fun is BinaryOperator)) {

+        return false;

+      }

+      BinaryOperator binOp = (BinaryOperator)nary.Fun;

+      if(binOp.Op != BinaryOperator.Opcode.Or) {

+        return false;

+      }

+      if(!(nary.Args[0] is IdentifierExpr && nary.Args[1] is IdentifierExpr)) {

+        return false;

+      }

+      return GPUVerifier.IsPredicate(GPUVerifier.StripThreadIdentifier(

+                ((IdentifierExpr)nary.Args[0]).Name)) &&

+             GPUVerifier.IsPredicate(GPUVerifier.StripThreadIdentifier(

+                ((IdentifierExpr)nary.Args[1]).Name));

+    }

+

+    private void AddCandidateInvariants(IRegion region, HashSet<Variable> LocalVars, List<Expr> UserSuppliedInvariants, Implementation Impl) {

+      foreach (IRegion subregion in region.SubRegions()) {

+        foreach (InvariantGenerationRule r in invariantGenerationRules) {

+          r.GenerateCandidates(Impl, subregion);

         }

 

-        internal static HashSet<Variable> GetModifiedVariables(IRegion region)

-        {

-            HashSet<Variable> result = new HashSet<Variable>();

+        AddBarrierDivergenceCandidates(LocalVars, Impl, subregion);

 

-            foreach (Cmd c in region.Cmds())

-            {

-                VariableSeq vars = new VariableSeq();

-                c.AddAssignedVariables(vars);

-                foreach (Variable v in vars)

-                {

-                    result.Add(v);

-                }

-            }

+        verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, subregion);

 

-            return result;

+        AddUserSuppliedInvariants(subregion, UserSuppliedInvariants, Impl);

+      }

+    }

+

+    private void AddUserSuppliedInvariants(IRegion region, List<Expr> UserSuppliedInvariants, Implementation Impl) {

+      foreach (Expr e in UserSuppliedInvariants) {

+        /*

+          wc.Invariants.Add(new AssertCmd(wc.tok, e));

+          bool OK = verifier.ProgramIsOK(Impl);

+          wc.Invariants.RemoveAt(wc.Invariants.Count - 1);

+          if (OK)

+          {

+              verifier.AddCandidateInvariant(wc, e, "user supplied");

+          }

+        */

+        verifier.AddCandidateInvariant(region, e, "user supplied");

+      }

+    }

+

+    internal static HashSet<Variable> GetModifiedVariables(IRegion region) {

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

+

+      foreach (Cmd c in region.Cmds()) {

+        VariableSeq vars = new VariableSeq();

+        c.AddAssignedVariables(vars);

+        foreach (Variable v in vars) {

+          result.Add(v);

         }

+      }

 

+      return result;

     }

+

+  }

 }