GPUVerify: make VarDefAnalysis capable of analysing non-constants

1 files changed, 72 insertions, 27 deletions

diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs
index 5c04a6f8..5dac47d6 100644
--- a/Source/GPUVerify/VariableDefinitionAnalysis.cs
+++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs
@@ -5,12 +5,14 @@ using System.Linq;
 

 namespace GPUVerify {

 

+using VarDef = Tuple<Expr, bool>;

+

 class VariableDefinitionAnalysis {

   GPUVerifier verifier;

   Implementation impl;

 

-  Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();

-  Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();

+  Dictionary<Variable, VarDef> defMap = new Dictionary<Variable, VarDef>();

+  Dictionary<string, VarDef> namedDefMap = new Dictionary<string, VarDef>();

   bool changed;

 

   VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {

@@ -19,12 +21,9 @@ class VariableDefinitionAnalysis {
   }

 

   private class IsConstantVisitor : StandardVisitor {

-    private VariableDefinitionAnalysis analysis;

     public bool isConstant = true;

 

-    public IsConstantVisitor(VariableDefinitionAnalysis a) {

-      analysis = a;

-    }

+    public IsConstantVisitor() {}

 

     public override Expr VisitNAryExpr(NAryExpr expr) {

       if (expr.Fun is MapSelect) {

@@ -33,26 +32,48 @@ class VariableDefinitionAnalysis {
       } else

         return base.VisitNAryExpr(expr);

     }

+  };

+

+  private class IsDerivedFromConstantsVisitor : StandardVisitor {

+    private VariableDefinitionAnalysis analysis;

+    public bool isDerivedFromConstants = true;

+

+    public IsDerivedFromConstantsVisitor(VariableDefinitionAnalysis a) {

+      analysis = a;

+    }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

       if (expr.Decl is Constant)

         return expr;

-      if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)

-        isConstant = false;

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

+        isDerivedFromConstants = false;

       return expr;

     }

   };

 

   bool IsConstant(Expr e) {

-    var v = new IsConstantVisitor(this);

+    var v = new IsConstantVisitor();

     v.Visit(e);

     return v.isConstant;

   }

 

-  void UpdateDefMap(Variable v, Expr def) {

-    if (!defMap.ContainsKey(v) || defMap[v] != def) {

+  bool IsDerivedFromConstants(Expr e) {

+    var v = new IsDerivedFromConstantsVisitor(this);

+    v.Visit(e);

+    return v.isDerivedFromConstants;

+  }

+

+  void UpdateDefMap(Variable v, Expr def, bool isConstant) {

+    if (!defMap.ContainsKey(v)) {

       changed = true;

-      defMap[v] = def;

+      defMap[v] = new VarDef(def, isConstant);

+      return;

+    }

+

+    var d = defMap[v];

+    if (d.Item1 != def || d.Item2 != isConstant) {

+      changed = true;

+      defMap[v] = new VarDef(def, isConstant);

     }

   }

 

@@ -60,10 +81,10 @@ class VariableDefinitionAnalysis {
     if (lhs is SimpleAssignLhs) {

       var sLhs = (SimpleAssignLhs)lhs;

       var theVar = sLhs.DeepAssignedVariable;

-      if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {

-        UpdateDefMap(theVar, null);

+      if ((defMap.ContainsKey(theVar) && defMap[theVar].Item1 != rhs) || !IsConstant(rhs)) {

+        UpdateDefMap(theVar, null, false);

       } else {

-        UpdateDefMap(theVar, rhs);

+        UpdateDefMap(theVar, rhs, IsDerivedFromConstants(rhs));

       }

     }

   }

@@ -78,6 +99,11 @@ class VariableDefinitionAnalysis {
             AddAssignment(a.Item1, a.Item2);

           }

         }

+        if (c is HavocCmd) {

+          var hCmd = (HavocCmd)c;

+          foreach (Variable v in hCmd.Vars)

+            UpdateDefMap(v, null, false);

+        }

       }

     } while (changed);

   }

@@ -92,22 +118,29 @@ class VariableDefinitionAnalysis {
     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

       if (expr.Decl is Constant)

         return expr;

-      return analysis.BuildNamedDefFor(expr.Decl);

+      return analysis.BuildNamedDefFor(expr.Decl, expr);

     }

   }

 

-  Expr BuildNamedDefFor(Variable v) {

-    Expr def;

+  Expr BuildNamedDefFor(Variable v, Expr e = null) {

+    VarDef def;

     if (namedDefMap.TryGetValue(v.Name, out def))

-      return def;

-    def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());

-    namedDefMap[v.Name] = def;

-    return def;

+      return def.Item1;

+

+    def = defMap[v];

+    Expr defExpr;

+    if (def.Item1 == null)

+      defExpr = e;

+    else

+      defExpr = (Expr)new BuildNamedDefVisitor(this).Visit(def.Item1.Clone());

+    namedDefMap[v.Name] = new VarDef(defExpr, def.Item2);

+

+    return defExpr;

   }

 

   void BuildNamedDefMap() {

     foreach (var v in defMap.Keys)

-      if (defMap[v] != null)

+      if (defMap[v].Item1 != null)

         BuildNamedDefFor(v);

   }

 

@@ -115,6 +148,7 @@ class VariableDefinitionAnalysis {
     private VariableDefinitionAnalysis analysis;

     private string procName;

     public bool isSubstitutable = true;

+    public bool isConstant = true;

 

     public SubstDefVisitor(VariableDefinitionAnalysis a, string p) {

       analysis = a;

@@ -126,26 +160,37 @@ class VariableDefinitionAnalysis {
         return expr;

       int id;

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

-      Expr def;

+      VarDef def;

       if (!analysis.namedDefMap.TryGetValue(varName, out def)) {

         isSubstitutable = false;

         return null;

       }

+      if (!def.Item2)

+        isConstant = false;

       if (id == 0)

-        return def;

+        return def.Item1;

       else

-        return (Expr)new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName).Visit(def.Clone());

+        return (Expr)new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName).Visit(def.Item1.Clone());

     }

   }

 

-  public Expr SubstDefinitions(Expr e, string procName) {

+  public Expr SubstDefinitions(Expr e, string procName, out bool isConstant) {

     var v = new SubstDefVisitor(this, procName);

     Expr result = (Expr)v.Visit(e.Clone());

+    isConstant = v.isConstant;

     if (!v.isSubstitutable)

       return null;

     return result;

   }

 

+  public Expr SubstDefinitions(Expr e, string procName) {

+    bool isConstant;

+    var result = SubstDefinitions(e, procName, out isConstant);

+    if (!isConstant)

+      return null;

+    return result;

+  }

+

   public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {

     var a = new VariableDefinitionAnalysis(verifier, impl);

     a.Analyse();