Java: Introduce SsaCapturedDefinition and replace uses of getAnUltimateDefinition.

Author: aschackmull

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

@@ -34,8 +34,12 @@ predicate useUsePair(VarRead use1, VarRead use2) { adjacentUseUse+(use1, use2) }
  * Other paths may also exist, so the SSA variables in `def` and `use` can be different.
  */
 predicate defUsePair(VariableUpdate def, VarRead use) {
-  exists(SsaVariable v |
-    v.getAUse() = use and v.getAnUltimateDefinition().(SsaExplicitWrite).getDefiningExpr() = def
+  exists(SsaDefinition v, SsaExplicitWrite write |
+    v.getARead() = use and write.getDefiningExpr() = def
+  |
+    v.getAnUltimateDefinition() = write
+    or
+    v.(SsaCapturedDefinition).getAnUltimateCapturedDefinition() = write
   )
 }
 
@@ -46,7 +50,9 @@ predicate defUsePair(VariableUpdate def, VarRead use) {
  * Other paths may also exist, so the SSA variables can be different.
  */
 predicate parameterDefUsePair(Parameter p, VarRead use) {
-  exists(SsaVariable v |
-    v.getAUse() = use and v.getAnUltimateDefinition().(SsaParameterInit).getParameter() = p
+  exists(SsaDefinition v, SsaParameterInit init | v.getARead() = use and init.getParameter() = p |
+    v.getAnUltimateDefinition() = init
+    or
+    v.(SsaCapturedDefinition).getAnUltimateCapturedDefinition() = init
   )
 }

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

@@ -120,8 +120,8 @@ predicate clearlyNotNull(SsaVariable v, Expr reason) {
     reason = decl
   )
   or
-  exists(SsaVariable captured |
-    v.(SsaImplicitInit).captures(captured) and
+  exists(SsaDefinition captured |
+    v.(SsaCapturedDefinition).captures(captured) and
     clearlyNotNull(captured, reason)
   )
   or

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

@@ -278,8 +278,8 @@ predicate nullDeref(SsaSourceVariable v, VarAccess va, string msg, Expr reason)
  * A dereference of a variable that is always `null`.
  */
 predicate alwaysNullDeref(SsaSourceVariable v, VarAccess va) {
-  exists(BasicBlock bb, SsaVariable ssa |
-    forall(SsaVariable def | def = ssa.getAnUltimateDefinition() |
+  exists(BasicBlock bb, SsaDefinition ssa |
+    forall(SsaDefinition def | def = ssa.getAnUltimateDefinition() |
       def.(SsaExplicitWrite).getValue() = alwaysNullExpr()
     )
     or

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

@@ -140,6 +140,25 @@ class SsaSourceField extends SsaSourceVariable {
   }
 }
 
+/** An SSA definition in a closure that captures a variable. */
+class SsaCapturedDefinition extends SsaImplicitEntryDefinition {
+  SsaCapturedDefinition() { captures(this, _) }
+
+  override string toString() { result = "SSA capture def(" + this.getSourceVariable() + ")" }
+
+  /** Holds if this definition captures the value of `capturedvar`. */
+  predicate captures(SsaDefinition capturedvar) { captures(this, capturedvar) }
+
+  /**
+   * Gets a definition that ultimately defines the captured variable and is not itself a phi node.
+   */
+  SsaDefinition getAnUltimateCapturedDefinition() {
+    exists(SsaDefinition capturedvar |
+      captures(this, capturedvar) and result = capturedvar.getAnUltimateDefinition()
+    )
+  }
+}
+
 /**
  * Gets an access of the SSA source variable underlying this SSA variable
  * that can be reached from this SSA variable without passing through any
@@ -194,18 +213,25 @@ class SsaVariable extends Definition {
   predicate isLiveAtEndOfBlock(BasicBlock b) { ssaDefReachesEndOfBlock(b, this) }
 
   /**
+   * DEPRECATED.
+   *
    * Gets an SSA variable whose value can flow to this one in one step. This
    * includes inputs to phi nodes, the prior definition of uncertain updates,
    * and the captured ssa variable for a closure variable.
    */
-  SsaVariable getAPhiInputOrPriorDef() {
+  deprecated SsaVariable getAPhiInputOrPriorDef() {
     result = this.(SsaPhiNode).getAPhiInput() or
     result = this.(SsaUncertainImplicitUpdate).getPriorDef() or
     this.(SsaImplicitInit).captures(result)
   }
 
-  /** Gets a definition that ultimately defines this variable and is not itself a phi node. */
-  SsaVariable getAnUltimateDefinition() {
+  /**
+   * DEPRECATED: Use `SsaCapturedDefinition::getAnUltimateCapturedDefinition()`
+   * and/or `SsaDefinition::getAnUltimateDefinition()` instead.
+   *
+   * Gets a definition that ultimately defines this variable and is not itself a phi node.
+   */
+  deprecated SsaVariable getAnUltimateDefinition() {
     result = this.getAPhiInputOrPriorDef*() and not result instanceof SsaPhiNode
   }
 }
@@ -319,6 +345,8 @@ class SsaUncertainImplicitUpdate extends SsaImplicitUpdate {
 }
 
 /**
+ * DEPRECATED: Use `SsaParameterInit`, `SsaImplicitEntryDefinition`, or `SsaCapturedDefinition` instead.
+ *
  * An SSA variable that is defined by its initial value in the callable. This
  * includes initial values of parameters, fields, and closure variables.
  */

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

@@ -62,9 +62,10 @@ private predicate fieldStep(Node node1, Node node2) {
 private predicate closureFlowStep(Expr e1, Expr e2) {
   simpleAstFlowStep(e1, e2)
   or
-  exists(SsaVariable v |
-    v.getAUse() = e2 and
-    v.getAnUltimateDefinition().(SsaExplicitWrite).getValue() = e1
+  exists(SsaDefinition v, SsaExplicitWrite def | v.getARead() = e2 and def.getValue() = e1 |
+    v.getAnUltimateDefinition() = def
+    or
+    v.(SsaCapturedDefinition).getAnUltimateCapturedDefinition() = def
   )
 }
 

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

@@ -101,7 +101,9 @@ predicate localExprFlow(Expr e1, Expr e2) { localFlow(exprNode(e1), exprNode(e2)
 predicate hasNonlocalValue(FieldRead fr) {
   not exists(SsaVariable v | v.getAUse() = fr)
   or
-  exists(SsaVariable v, SsaVariable def | v.getAUse() = fr and def = v.getAnUltimateDefinition() |
+  exists(SsaDefinition v, SsaDefinition def |
+    v.getARead() = fr and def = v.getAnUltimateDefinition()
+  |
     def instanceof SsaImplicitInit or
     def instanceof SsaImplicitUpdate
   )

java/ql/lib/semmle/code/java/frameworks/InputStream.qll

@@ -41,7 +41,9 @@ private class InputStreamWrapperCapturedJumpStep extends AdditionalTaintStep {
  */
 private class InputStreamWrapperCapturedLocalStep extends AdditionalTaintStep {
   override predicate step(DataFlow::Node n1, DataFlow::Node n2) {
-    exists(InputStreamRead m, NestedClass wrapper, SsaVariable captured, SsaImplicitInit capturer |
+    exists(
+      InputStreamRead m, NestedClass wrapper, SsaDefinition captured, SsaCapturedDefinition capturer
+    |
       wrapper.getASourceSupertype+() instanceof TypeInputStream and
       m.getDeclaringType() = wrapper and
       capturer.captures(captured) and

java/ql/lib/semmle/code/java/security/CommandArguments.qll

@@ -38,9 +38,13 @@ private predicate isShell(Expr ex) {
     cmd.regexpMatch(".*(sh|javac?|python[23]?|osascript|cmd)(\\.exe)?$")
   )
   or
-  exists(SsaVariable ssa |
-    ex = ssa.getAUse() and
-    isShell(ssa.getAnUltimateDefinition().(SsaExplicitWrite).getDefiningExpr())
+  exists(SsaDefinition ssa, SsaExplicitWrite def |
+    ex = ssa.getARead() and
+    isShell(def.getDefiningExpr())
+  |
+    ssa.getAnUltimateDefinition() = def
+    or
+    ssa.(SsaCapturedDefinition).getAnUltimateCapturedDefinition() = def
   )
   or
   isShell(ex.(Assignment).getRhs())

java/ql/src/utils/modelgenerator/internal/CaptureModels.qll

@@ -277,10 +277,7 @@ private module SinkModelGeneratorInput implements SinkModelGeneratorInputSig {
 
   predicate sinkModelSanitizer(DataFlow::Node node) {
     // exclude variable capture jump steps
-    exists(Ssa::SsaImplicitInit closure |
-      closure.captures(_) and
-      node.asExpr() = Ssa::ssaGetAFirstUse(closure)
-    )
+    exists(Ssa::SsaCapturedDefinition closure | node.asExpr() = Ssa::ssaGetAFirstUse(closure))
   }
 
   predicate apiSource(DataFlow::Node source) {

java/ql/test/library-tests/ssa/captures.ql

@@ -1,6 +1,6 @@
 import java
 import semmle.code.java.dataflow.SSA
 
-from SsaImplicitInit closure, SsaVariable captured
+from SsaCapturedDefinition closure, SsaDefinition captured
 where closure.captures(captured)
 select closure, captured