Java: Less caching

Author: hvitved

java/ql/lib/semmle/code/java/dataflow/SSA.qll

@@ -206,13 +206,7 @@ class SsaUpdate extends SsaVariable instanceof WriteDefinition {
 class SsaExplicitUpdate extends SsaUpdate {
   private VariableUpdate upd;
 
-  SsaExplicitUpdate() {
-    exists(SsaSourceVariable v, BasicBlock bb, int i |
-      this.definesAt(v, bb, i) and
-      certainVariableUpdate(v, upd, bb, i) and
-      getDestVar(upd) = this.getSourceVariable()
-    )
-  }
+  SsaExplicitUpdate() { ssaExplicitUpdate(this, upd) }
 
   override string toString() { result = "SSA def(" + this.getSourceVariable() + ")" }
 
@@ -233,13 +227,27 @@ class SsaImplicitUpdate extends SsaUpdate {
     result = "SSA impl upd[" + this.getKind() + "](" + this.getSourceVariable() + ")"
   }
 
+  private predicate hasExplicitQualifierUpdate() {
+    exists(SsaExplicitUpdate qdef, BasicBlock bb, int i |
+      qdef.definesAt(this.getSourceVariable().getQualifier(), bb, i) and
+      this.definesAt(_, bb, i)
+    )
+  }
+
+  private predicate hasImplicitQualifierUpdate() {
+    exists(SsaUncertainImplicitUpdate qdef, BasicBlock bb, int i |
+      qdef.definesAt(this.getSourceVariable().getQualifier(), bb, i) and
+      this.definesAt(_, bb, i)
+    )
+  }
+
   private string getKind() {
     this instanceof UntrackedDef and result = "untracked"
     or
-    certainVariableUpdate(this.getSourceVariable().getQualifier(), this.getCfgNode(), _, _) and
+    this.hasExplicitQualifierUpdate() and
     result = "explicit qualifier"
     or
-    if uncertainVariableUpdate(this.getSourceVariable().getQualifier(), this.getCfgNode(), _, _)
+    if this.hasImplicitQualifierUpdate()
     then
       if exists(this.getANonLocalUpdate())
       then result = "nonlocal + nonlocal qualifier"
@@ -252,13 +260,7 @@ class SsaImplicitUpdate extends SsaUpdate {
   /**
    * Gets a reachable `FieldWrite` that might represent this ssa update, if any.
    */
-  FieldWrite getANonLocalUpdate() {
-    exists(SsaSourceField f, Callable setter |
-      f = this.getSourceVariable() and
-      relevantFieldUpdate(setter, f.getField(), result) and
-      updatesNamedField(this.getCfgNode(), f, setter)
-    )
-  }
+  FieldWrite getANonLocalUpdate() { result = getANonLocalUpdate(this) }
 
   /**
    * Holds if this ssa variable might change the value to something unknown.
@@ -268,9 +270,11 @@ class SsaImplicitUpdate extends SsaUpdate {
    * of its qualifiers is volatile.
    */
   predicate assignsUnknownValue() {
-    this instanceof UntrackedDef or
-    certainVariableUpdate(this.getSourceVariable().getQualifier(), this.getCfgNode(), _, _) or
-    uncertainVariableUpdate(this.getSourceVariable().getQualifier(), this.getCfgNode(), _, _)
+    this instanceof UntrackedDef
+    or
+    this.hasExplicitQualifierUpdate()
+    or
+    this.hasImplicitQualifierUpdate()
   }
 }
 
@@ -280,12 +284,7 @@ class SsaImplicitUpdate extends SsaUpdate {
  * its qualifiers.
  */
 class SsaUncertainImplicitUpdate extends SsaImplicitUpdate {
-  SsaUncertainImplicitUpdate() {
-    exists(SsaSourceVariable v, BasicBlock bb, int i |
-      this.definesAt(v, bb, i) and
-      uncertainVariableUpdate(v, _, bb, i)
-    )
-  }
+  SsaUncertainImplicitUpdate() { ssaUncertainImplicitUpdate(this) }
 
   /**
    * Gets the immediately preceding definition. Since this update is uncertain
@@ -299,13 +298,7 @@ class SsaUncertainImplicitUpdate extends SsaImplicitUpdate {
  * includes initial values of parameters, fields, and closure variables.
  */
 class SsaImplicitInit extends SsaVariable instanceof WriteDefinition {
-  SsaImplicitInit() {
-    exists(SsaSourceVariable v, BasicBlock bb, int i |
-      this.definesAt(v, bb, i) and
-      hasEntryDef(v, bb) and
-      i = 0
-    )
-  }
+  SsaImplicitInit() { ssaImplicitInit(this) }
 
   override string toString() { result = "SSA init(" + this.getSourceVariable() + ")" }
 

java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll

@@ -269,30 +269,41 @@ private module Cached {
     result.getAnAccess() = upd.(UnaryAssignExpr).getExpr()
   }
 
-  /**
-   * Holds if `f` is a field that is interesting as a basis for SSA.
-   *
-   * - A field that is read twice is interesting as we want to know whether the
-   *   reads refer to the same value.
-   * - A field that is both written and read is interesting as we want to know
-   *   whether the read might get the written value.
-   * - A field that is read in a loop is interesting as we want to know whether
-   *   the value is the same in different iterations (that is, whether the SSA
-   *   definition can be placed outside the loop).
-   * - A volatile field is never interesting, since all reads must reread from
-   *   memory and we are forced to assume that the value can change at any point.
-   */
-  cached
-  predicate trackField(SsaSourceField f) { multiAccessed(f) and not f.isVolatile() }
+  private module NotCached1 {
+    /**
+     * Holds if `f` is a field that is interesting as a basis for SSA.
+     *
+     * - A field that is read twice is interesting as we want to know whether the
+     *   reads refer to the same value.
+     * - A field that is both written and read is interesting as we want to know
+     *   whether the read might get the written value.
+     * - A field that is read in a loop is interesting as we want to know whether
+     *   the value is the same in different iterations (that is, whether the SSA
+     *   definition can be placed outside the loop).
+     * - A volatile field is never interesting, since all reads must reread from
+     *   memory and we are forced to assume that the value can change at any point.
+     */
+    pragma[nomagic]
+    predicate trackField(SsaSourceField f) { multiAccessed(f) and not f.isVolatile() }
+
+    /** Holds if `n` must update the locally tracked variable `v`. */
+    pragma[nomagic]
+    predicate certainVariableUpdate(TrackedVar v, ControlFlowNode n, BasicBlock b, int i) {
+      exists(VariableUpdate a | a = n | getDestVar(a) = v) and
+      b.getNode(i) = n and
+      hasDominanceInformation(b)
+      or
+      certainVariableUpdate(v.getQualifier(), n, b, i)
+    }
+  }
 
-  /** Holds if `n` must update the locally tracked variable `v`. */
   cached
-  predicate certainVariableUpdate(TrackedVar v, ControlFlowNode n, BasicBlock b, int i) {
-    exists(VariableUpdate a | a = n | getDestVar(a) = v) and
-    b.getNode(i) = n and
-    hasDominanceInformation(b)
-    or
-    certainVariableUpdate(v.getQualifier(), n, b, i)
+  predicate ssaExplicitUpdate(SsaUpdate def, VariableUpdate upd) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      certainVariableUpdate(v, upd, bb, i) and
+      getDestVar(upd) = def.getSourceVariable()
+    )
   }
 
   /*
@@ -333,8 +344,8 @@ private module Cached {
   /**
    * Holds if `fw` is an update of `f` in `c` that is relevant for SSA construction.
    */
-  cached
-  predicate relevantFieldUpdate(Callable c, Field f, FieldWrite fw) {
+  pragma[nomagic]
+  private predicate relevantFieldUpdate(Callable c, Field f, FieldWrite fw) {
     fw = f.getAnAccess() and
     not init(fw) and
     fw.getEnclosingCallable() = c and
@@ -483,34 +494,66 @@ private module Cached {
    * `FieldRead` of `f` is reachable from `call`.
    */
   pragma[noopt]
-  cached
-  predicate updatesNamedField(Call call, TrackedField f, Callable setter) {
+  private predicate updatesNamedField(Call call, TrackedField f, Callable setter) {
     exists(TCallableNode src, TCallableNode sink, Field field |
       source(call, f, field, src) and
       sink(setter, field, sink) and
       (src = sink or edgePlus(src, sink))
     )
   }
 
-  /** Holds if `n` might update the locally tracked variable `v`. */
+  /**
+   * Gets a reachable `FieldWrite` that might represent this ssa update, if any.
+   */
   cached
-  predicate uncertainVariableUpdate(TrackedVar v, ControlFlowNode n, BasicBlock b, int i) {
-    exists(Call c | c = n | updatesNamedField(c, v, _)) and
-    b.getNode(i) = n and
-    hasDominanceInformation(b)
-    or
-    uncertainVariableUpdate(v.getQualifier(), n, b, i)
+  FieldWrite getANonLocalUpdate(SsaImplicitUpdate def) {
+    exists(SsaSourceField f, Callable setter |
+      f = def.getSourceVariable() and
+      relevantFieldUpdate(setter, f.getField(), result) and
+      updatesNamedField(def.getCfgNode(), f, setter)
+    )
+  }
+
+  private module NotCached2 {
+    /** Holds if `n` might update the locally tracked variable `v`. */
+    pragma[nomagic]
+    predicate uncertainVariableUpdate(TrackedVar v, ControlFlowNode n, BasicBlock b, int i) {
+      exists(Call c | c = n | updatesNamedField(c, v, _)) and
+      b.getNode(i) = n and
+      hasDominanceInformation(b)
+      or
+      uncertainVariableUpdate(v.getQualifier(), n, b, i)
+    }
   }
 
-  /** Holds if `v` has an implicit definition at the entry, `b`, of the callable. */
   cached
-  predicate hasEntryDef(TrackedVar v, BasicBlock b) {
-    exists(LocalScopeVariable l, Callable c | v = TLocalVar(c, l) and c.getBody() = b |
-      l instanceof Parameter or
-      l.getCallable() != c
+  predicate ssaUncertainImplicitUpdate(SsaImplicitUpdate def) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      uncertainVariableUpdate(v, _, bb, i)
+    )
+  }
+
+  private module NotCached3 {
+    /** Holds if `v` has an implicit definition at the entry, `b`, of the callable. */
+    pragma[nomagic]
+    predicate hasEntryDef(TrackedVar v, BasicBlock b) {
+      exists(LocalScopeVariable l, Callable c | v = TLocalVar(c, l) and c.getBody() = b |
+        l instanceof Parameter or
+        l.getCallable() != c
+      )
+      or
+      v instanceof SsaSourceField and v.getEnclosingCallable().getBody() = b
+    }
+  }
+
+  cached
+  predicate ssaImplicitInit(WriteDefinition def) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      hasEntryDef(v, bb) and
+      i = 0
     )
-    or
-    v instanceof SsaSourceField and v.getEnclosingCallable().getBody() = b
   }
 
   /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
@@ -636,9 +679,21 @@ private module Cached {
       )
     }
   }
+
+  /**
+   * Provides internal implementation predicates that are not cached and should not
+   * be used outside of this file.
+   */
+  cached // needed to avoid compilation error; has no actual effect
+  module Internal {
+    import NotCached1
+    import NotCached2
+    import NotCached3
+  }
 }
 
 import Cached
+private import Internal
 
 /**
  * An SSA definition excluding those variables that use a trivial SSA construction.
@@ -682,6 +737,10 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
       )
   }
 
+  predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) {
+    def instanceof SsaUncertainImplicitUpdate
+  }
+
   class Guard extends Guards::Guard {
     predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
   }