Java: Introduce 'with/without content' summary components

Author: hvitved

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

@@ -164,7 +164,9 @@ predicate clearsContent(Node n, Content c) {
  * Holds if the value that is being tracked is expected to be stored inside content `c`
  * at node `n`.
  */
-predicate expectsContent(Node n, ContentSet c) { none() }
+predicate expectsContent(Node n, ContentSet c) {
+  FlowSummaryImpl::Private::Steps::summaryExpectsContent(n, c)
+}
 
 /**
  * Gets a representative (boxed) type for `t` for the purpose of pruning

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

@@ -136,7 +136,7 @@ predicate simpleLocalFlowStep(Node node1, Node node2) {
   not exists(FieldRead fr |
     hasNonlocalValue(fr) and fr.getField().isStatic() and fr = node1.asExpr()
   ) and
-  not FlowSummaryImpl::Private::Steps::summaryClearsContentArg(node1, _)
+  not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(node1)
   or
   ThisFlow::adjacentThisRefs(node1, node2)
   or

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

@@ -26,6 +26,10 @@ module Public {
     string toString() {
       exists(ContentSet c | this = TContentSummaryComponent(c) and result = c.toString())
       or
+      exists(ContentSet c | this = TWithoutContentSummaryComponent(c) and result = "without " + c)
+      or
+      exists(ContentSet c | this = TWithContentSummaryComponent(c) and result = "with " + c)
+      or
       exists(ArgumentPosition pos |
         this = TParameterSummaryComponent(pos) and result = "parameter " + pos
       )
@@ -43,6 +47,12 @@ module Public {
     /** Gets a summary component for content `c`. */
     SummaryComponent content(ContentSet c) { result = TContentSummaryComponent(c) }
 
+    /** Gets a summary component where data is not allowed to be stored in `c`. */
+    SummaryComponent withoutContent(ContentSet c) { result = TWithoutContentSummaryComponent(c) }
+
+    /** Gets a summary component where data must be stored in `c`. */
+    SummaryComponent withContent(ContentSet c) { result = TWithContentSummaryComponent(c) }
+
     /** Gets a summary component for a parameter at position `pos`. */
     SummaryComponent parameter(ArgumentPosition pos) { result = TParameterSummaryComponent(pos) }
 
@@ -216,6 +226,8 @@ module Public {
     /**
      * Holds if values stored inside `content` are cleared on objects passed as
      * arguments at position `pos` to this callable.
+     *
+     * TODO: Remove once all languages support `WithoutContent` tokens.
      */
     pragma[nomagic]
     predicate clearsContent(ParameterPosition pos, ContentSet content) { none() }
@@ -234,7 +246,9 @@ module Private {
     TContentSummaryComponent(ContentSet c) or
     TParameterSummaryComponent(ArgumentPosition pos) or
     TArgumentSummaryComponent(ParameterPosition pos) or
-    TReturnSummaryComponent(ReturnKind rk)
+    TReturnSummaryComponent(ReturnKind rk) or
+    TWithoutContentSummaryComponent(ContentSet c) or
+    TWithContentSummaryComponent(ContentSet c)
 
   private TParameterSummaryComponent thisParam() {
     result = TParameterSummaryComponent(instanceParameterPosition())
@@ -296,6 +310,23 @@ module Private {
           SummaryComponentStack::singleton(TArgumentSummaryComponent(_))) and
       preservesValue = preservesValue1.booleanAnd(preservesValue2)
     )
+    or
+    exists(ParameterPosition ppos, ContentSet cs |
+      c.clearsContent(ppos, cs) and
+      input = SummaryComponentStack::push(SummaryComponent::withoutContent(cs), output) and
+      output = SummaryComponentStack::argument(ppos) and
+      preservesValue = true
+    )
+  }
+
+  private class MkClearStack extends RequiredSummaryComponentStack {
+    override predicate required(SummaryComponent head, SummaryComponentStack tail) {
+      exists(SummarizedCallable sc, ParameterPosition ppos, ContentSet cs |
+        sc.clearsContent(ppos, cs) and
+        head = SummaryComponent::withoutContent(cs) and
+        tail = SummaryComponentStack::argument(ppos)
+      )
+    }
   }
 
   /**
@@ -378,10 +409,7 @@ module Private {
 
   private newtype TSummaryNodeState =
     TSummaryNodeInputState(SummaryComponentStack s) { inputState(_, s) } or
-    TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) } or
-    TSummaryNodeClearsContentState(ParameterPosition pos, boolean post) {
-      any(SummarizedCallable sc).clearsContent(pos, _) and post in [false, true]
-    }
+    TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) }
 
   /**
    * A state used to break up (complex) flow summaries into atomic flow steps.
@@ -428,12 +456,6 @@ module Private {
         this = TSummaryNodeOutputState(s) and
         result = "to write: " + s
       )
-      or
-      exists(ParameterPosition pos, boolean post, string postStr |
-        this = TSummaryNodeClearsContentState(pos, post) and
-        (if post = true then postStr = " (post)" else postStr = "") and
-        result = "clear: " + pos + postStr
-      )
     }
   }
 
@@ -457,11 +479,6 @@ module Private {
     not parameterReadState(c, state, _)
     or
     state.isOutputState(c, _)
-    or
-    exists(ParameterPosition pos |
-      c.clearsContent(pos, _) and
-      state = TSummaryNodeClearsContentState(pos, _)
-    )
   }
 
   pragma[noinline]
@@ -497,24 +514,22 @@ module Private {
     parameterReadState(c, _, pos)
     or
     isParameterPostUpdate(_, c, pos)
-    or
-    c.clearsContent(pos, _)
   }
 
   private predicate callbackOutput(
     SummarizedCallable c, SummaryComponentStack s, Node receiver, ReturnKind rk
   ) {
     any(SummaryNodeState state).isInputState(c, s) and
     s.head() = TReturnSummaryComponent(rk) and
-    receiver = summaryNodeInputState(c, s.drop(1))
+    receiver = summaryNodeInputState(c, s.tail())
   }
 
   private predicate callbackInput(
     SummarizedCallable c, SummaryComponentStack s, Node receiver, ArgumentPosition pos
   ) {
     any(SummaryNodeState state).isOutputState(c, s) and
     s.head() = TParameterSummaryComponent(pos) and
-    receiver = summaryNodeInputState(c, s.drop(1))
+    receiver = summaryNodeInputState(c, s.tail())
   }
 
   /** Holds if a call targeting `receiver` should be synthesized inside `c`. */
@@ -540,15 +555,21 @@ module Private {
     exists(SummarizedCallable c, SummaryComponentStack s, SummaryComponent head | head = s.head() |
       n = summaryNodeInputState(c, s) and
       (
+        exists(ContentSet cont | result = getContentType(cont) |
+          head = TContentSummaryComponent(cont) or
+          head = TWithContentSummaryComponent(cont)
+        )
+        or
         exists(ContentSet cont |
-          head = TContentSummaryComponent(cont) and result = getContentType(cont)
+          head = TWithoutContentSummaryComponent(cont) and
+          result = getNodeType(summaryNodeInputState(c, s.tail()))
         )
         or
         exists(ReturnKind rk |
           head = TReturnSummaryComponent(rk) and
           result =
             getCallbackReturnType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
-                  s.drop(1))), rk)
+                  s.tail())), rk)
         )
       )
       or
@@ -567,16 +588,10 @@ module Private {
         exists(ArgumentPosition pos | head = TParameterSummaryComponent(pos) |
           result =
             getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
-                  s.drop(1))), pos)
+                  s.tail())), pos)
         )
       )
     )
-    or
-    exists(SummarizedCallable c, ParameterPosition pos, ParamNode p |
-      n = summaryNode(c, TSummaryNodeClearsContentState(pos, false)) and
-      p.isParameterOf(c, pos) and
-      result = getNodeType(p)
-    )
   }
 
   /** Holds if summary node `out` contains output of kind `rk` from call `c`. */
@@ -602,9 +617,6 @@ module Private {
     exists(SummarizedCallable c, ParameterPosition pos |
       isParameterPostUpdate(post, c, pos) and
       pre.(ParamNode).isParameterOf(c, pos)
-      or
-      pre = summaryNode(c, TSummaryNodeClearsContentState(pos, false)) and
-      post = summaryNode(c, TSummaryNodeClearsContentState(pos, true))
     )
     or
     exists(SummarizedCallable callable, SummaryComponentStack s |
@@ -628,8 +640,6 @@ module Private {
    */
   predicate summaryAllowParameterReturnInSelf(ParamNode p) {
     exists(SummarizedCallable c, ParameterPosition ppos | p.isParameterOf(c, ppos) |
-      c.clearsContent(ppos, _)
-      or
       exists(SummaryComponentStack inputContents, SummaryComponentStack outputContents |
         summary(c, inputContents, outputContents, _) and
         inputContents.bottom() = pragma[only_bind_into](TArgumentSummaryComponent(ppos)) and
@@ -658,9 +668,10 @@ module Private {
         preservesValue = false and not summary(c, inputContents, outputContents, true)
       )
       or
-      exists(SummarizedCallable c, ParameterPosition pos |
-        pred.(ParamNode).isParameterOf(c, pos) and
-        succ = summaryNode(c, TSummaryNodeClearsContentState(pos, _)) and
+      exists(SummarizedCallable c, SummaryComponentStack s |
+        pred = summaryNodeInputState(c, s.tail()) and
+        succ = summaryNodeInputState(c, s) and
+        s.head() = [SummaryComponent::withContent(_), SummaryComponent::withoutContent(_)] and
         preservesValue = true
       )
     }
@@ -671,7 +682,7 @@ module Private {
      */
     predicate summaryReadStep(Node pred, ContentSet c, Node succ) {
       exists(SummarizedCallable sc, SummaryComponentStack s |
-        pred = summaryNodeInputState(sc, s.drop(1)) and
+        pred = summaryNodeInputState(sc, s.tail()) and
         succ = summaryNodeInputState(sc, s) and
         SummaryComponent::content(c) = s.head()
       )
@@ -684,7 +695,7 @@ module Private {
     predicate summaryStoreStep(Node pred, ContentSet c, Node succ) {
       exists(SummarizedCallable sc, SummaryComponentStack s |
         pred = summaryNodeOutputState(sc, s) and
-        succ = summaryNodeOutputState(sc, s.drop(1)) and
+        succ = summaryNodeOutputState(sc, s.tail()) and
         SummaryComponent::content(c) = s.head()
       )
     }
@@ -709,9 +720,22 @@ module Private {
      * node where field `b` is cleared).
      */
     predicate summaryClearsContent(Node n, ContentSet c) {
-      exists(SummarizedCallable sc, ParameterPosition pos |
-        n = summaryNode(sc, TSummaryNodeClearsContentState(pos, true)) and
-        sc.clearsContent(pos, c)
+      exists(SummarizedCallable sc, SummaryNodeState state, SummaryComponentStack stack |
+        n = summaryNode(sc, state) and
+        state.isInputState(sc, stack) and
+        stack.head() = SummaryComponent::withoutContent(c)
+      )
+    }
+
+    /**
+     * Holds if the value that is being tracked is expected to be stored inside
+     * content `c` at `n`.
+     */
+    predicate summaryExpectsContent(Node n, ContentSet c) {
+      exists(SummarizedCallable sc, SummaryNodeState state, SummaryComponentStack stack |
+        n = summaryNode(sc, state) and
+        state.isInputState(sc, stack) and
+        stack.head() = SummaryComponent::withContent(c)
       )
     }
 
@@ -723,27 +747,32 @@ module Private {
       sc = viableCallable(call)
     }
 
-    /**
-     * Holds if values stored inside content `c` are cleared inside a
-     * callable to which `arg` is an argument.
-     *
-     * In such cases, it is important to prevent use-use flow out of
-     * `arg` (see comment for `summaryClearsContent`).
-     */
     pragma[nomagic]
-    predicate summaryClearsContentArg(ArgNode arg, ContentSet c) {
-      exists(DataFlowCall call, SummarizedCallable sc, ParameterPosition ppos |
+    private ParamNode summaryArgParam0(DataFlowCall call, ArgNode arg) {
+      exists(ParameterPosition ppos, SummarizedCallable sc |
         argumentPositionMatch(call, arg, ppos) and
-        viableParam(call, sc, ppos, _) and
-        sc.clearsContent(ppos, c)
+        viableParam(call, sc, ppos, result)
       )
     }
 
+    /**
+     * Holds if use-use flow starting from `arg` should be prohibited.
+     *
+     * This is the case when `arg` is the argument of a call that targets a
+     * flow summary where the corresponding parameter either clears contents
+     * or expects contents.
+     */
     pragma[nomagic]
-    private ParamNode summaryArgParam0(DataFlowCall call, ArgNode arg) {
-      exists(ParameterPosition ppos, SummarizedCallable sc |
-        argumentPositionMatch(call, arg, ppos) and
-        viableParam(call, sc, ppos, result)
+    predicate prohibitsUseUseFlow(ArgNode arg) {
+      exists(ParamNode p, Node mid, ParameterPosition ppos, Node ret |
+        p = summaryArgParam0(_, arg) and
+        p.isParameterOf(_, ppos) and
+        summaryLocalStep(p, mid, true) and
+        summaryLocalStep(mid, ret, true) and
+        isParameterPostUpdate(ret, _, ppos)
+      |
+        summaryClearsContent(mid, _) or
+        summaryExpectsContent(mid, _)
       )
     }
 
@@ -1141,6 +1170,10 @@ module Private {
         Private::Steps::summaryClearsContent(a.asNode(), c) and
         b = a and
         value = "clear (" + c + ")"
+        or
+        Private::Steps::summaryExpectsContent(a.asNode(), c) and
+        b = a and
+        value = "expect (" + c + ")"
       )
       or
       summaryPostUpdateNode(b.asNode(), a.asNode()) and