Merge pull request #3762 from hvitved/dataflow/clear-contents

Data flow: Model field clearing

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImpl.qll

@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
 }
 
 private module LocalFlowBigStep {
+  /**
+   * A node where some checking is required, and hence the big-step relation
+   * is not allowed to step over.
+   */
+  private class FlowCheckNode extends Node {
+    FlowCheckNode() {
+      this instanceof CastNode or
+      clearsContent(this, _)
+    }
+  }
+
   /**
    * Holds if `node` can be the first node in a maximal subsequence of local
    * flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
       node instanceof OutNodeExt or
       store(_, _, node, _) or
       read(_, _, node) or
-      node instanceof CastNode
+      node instanceof FlowCheckNode
     )
   }
 
@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
       read(node, _, next)
     )
     or
-    node instanceof CastNode
+    node instanceof FlowCheckNode
     or
     config.isSink(node)
   }
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
       exists(Node mid |
         localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
         localFlowStepNodeCand1(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         nodeCand2(node2, unbind(config))
       )
       or
       exists(Node mid |
         localFlowStepPlus(node1, mid, _, _, config, cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getErasedNodeTypeBound(node2) and
         nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
   Configuration config
 ) {
   flowCandFwd0(node, fromArg, argApf, apf, config) and
+  not apf.isClearedAt(node) and
   if node instanceof CastingNode
   then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
   else any()

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImpl2.qll

@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
 }
 
 private module LocalFlowBigStep {
+  /**
+   * A node where some checking is required, and hence the big-step relation
+   * is not allowed to step over.
+   */
+  private class FlowCheckNode extends Node {
+    FlowCheckNode() {
+      this instanceof CastNode or
+      clearsContent(this, _)
+    }
+  }
+
   /**
    * Holds if `node` can be the first node in a maximal subsequence of local
    * flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
       node instanceof OutNodeExt or
       store(_, _, node, _) or
       read(_, _, node) or
-      node instanceof CastNode
+      node instanceof FlowCheckNode
     )
   }
 
@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
       read(node, _, next)
     )
     or
-    node instanceof CastNode
+    node instanceof FlowCheckNode
     or
     config.isSink(node)
   }
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
       exists(Node mid |
         localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
         localFlowStepNodeCand1(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         nodeCand2(node2, unbind(config))
       )
       or
       exists(Node mid |
         localFlowStepPlus(node1, mid, _, _, config, cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getErasedNodeTypeBound(node2) and
         nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
   Configuration config
 ) {
   flowCandFwd0(node, fromArg, argApf, apf, config) and
+  not apf.isClearedAt(node) and
   if node instanceof CastingNode
   then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
   else any()

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImpl3.qll

@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
 }
 
 private module LocalFlowBigStep {
+  /**
+   * A node where some checking is required, and hence the big-step relation
+   * is not allowed to step over.
+   */
+  private class FlowCheckNode extends Node {
+    FlowCheckNode() {
+      this instanceof CastNode or
+      clearsContent(this, _)
+    }
+  }
+
   /**
    * Holds if `node` can be the first node in a maximal subsequence of local
    * flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
       node instanceof OutNodeExt or
       store(_, _, node, _) or
       read(_, _, node) or
-      node instanceof CastNode
+      node instanceof FlowCheckNode
     )
   }
 
@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
       read(node, _, next)
     )
     or
-    node instanceof CastNode
+    node instanceof FlowCheckNode
     or
     config.isSink(node)
   }
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
       exists(Node mid |
         localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
         localFlowStepNodeCand1(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         nodeCand2(node2, unbind(config))
       )
       or
       exists(Node mid |
         localFlowStepPlus(node1, mid, _, _, config, cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getErasedNodeTypeBound(node2) and
         nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
   Configuration config
 ) {
   flowCandFwd0(node, fromArg, argApf, apf, config) and
+  not apf.isClearedAt(node) and
   if node instanceof CastingNode
   then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
   else any()

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImpl4.qll

@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
 }
 
 private module LocalFlowBigStep {
+  /**
+   * A node where some checking is required, and hence the big-step relation
+   * is not allowed to step over.
+   */
+  private class FlowCheckNode extends Node {
+    FlowCheckNode() {
+      this instanceof CastNode or
+      clearsContent(this, _)
+    }
+  }
+
   /**
    * Holds if `node` can be the first node in a maximal subsequence of local
    * flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
       node instanceof OutNodeExt or
       store(_, _, node, _) or
       read(_, _, node) or
-      node instanceof CastNode
+      node instanceof FlowCheckNode
     )
   }
 
@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
       read(node, _, next)
     )
     or
-    node instanceof CastNode
+    node instanceof FlowCheckNode
     or
     config.isSink(node)
   }
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
       exists(Node mid |
         localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
         localFlowStepNodeCand1(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         nodeCand2(node2, unbind(config))
       )
       or
       exists(Node mid |
         localFlowStepPlus(node1, mid, _, _, config, cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getErasedNodeTypeBound(node2) and
         nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
   Configuration config
 ) {
   flowCandFwd0(node, fromArg, argApf, apf, config) and
+  not apf.isClearedAt(node) and
   if node instanceof CastingNode
   then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
   else any()

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImpl5.qll

@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
 }
 
 private module LocalFlowBigStep {
+  /**
+   * A node where some checking is required, and hence the big-step relation
+   * is not allowed to step over.
+   */
+  private class FlowCheckNode extends Node {
+    FlowCheckNode() {
+      this instanceof CastNode or
+      clearsContent(this, _)
+    }
+  }
+
   /**
    * Holds if `node` can be the first node in a maximal subsequence of local
    * flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
       node instanceof OutNodeExt or
       store(_, _, node, _) or
       read(_, _, node) or
-      node instanceof CastNode
+      node instanceof FlowCheckNode
     )
   }
 
@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
       read(node, _, next)
     )
     or
-    node instanceof CastNode
+    node instanceof FlowCheckNode
     or
     config.isSink(node)
   }
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
       exists(Node mid |
         localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
         localFlowStepNodeCand1(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         nodeCand2(node2, unbind(config))
       )
       or
       exists(Node mid |
         localFlowStepPlus(node1, mid, _, _, config, cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
-        not mid instanceof CastNode and
+        not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getErasedNodeTypeBound(node2) and
         nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
   Configuration config
 ) {
   flowCandFwd0(node, fromArg, argApf, apf, config) and
+  not apf.isClearedAt(node) and
   if node instanceof CastingNode
   then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
   else any()

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplCommon.qll

@@ -754,6 +754,13 @@ abstract class AccessPathFront extends TAccessPathFront {
   abstract boolean toBoolNonEmpty();
 
   predicate headUsesContent(TypedContent tc) { this = TFrontHead(tc) }
+
+  predicate isClearedAt(Node n) {
+    exists(TypedContent tc |
+      this.headUsesContent(tc) and
+      clearsContent(n, tc.getContent())
+    )
+  }
 }
 
 class AccessPathFrontNil extends AccessPathFront, TFrontNil {

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

@@ -195,6 +195,15 @@ predicate readStep(Node node1, Content f, Node node2) {
   )
 }
 
+/**
+ * Holds if values stored inside content `c` are cleared at node `n`. For example,
+ * any value stored inside `f` is cleared at the pre-update node associated with `x`
+ * in `x.f = newValue`.
+ */
+predicate clearsContent(Node n, Content c) {
+  n = any(PostUpdateNode pun | storeStep(_, c, pun)).getPreUpdateNode()
+}
+
 /**
  * Gets a representative (boxed) type for `t` for the purpose of pruning
  * possible flow. A single type is used for all numeric types to account for

java/ql/test/library-tests/dataflow/fields/F.java

@@ -0,0 +1,38 @@
+public class F {
+  Object Field1;
+  Object Field2;
+  public F() {
+    Field1 = new Object();
+    Field2 = new Object();
+  }
+
+  private void m() {
+    Object o = new Object();
+    F f = new F();
+    f.Field1 = o;
+    f.Field2 = o;
+    f.Field2 = null;
+    sink(f.Field1); // flow
+    sink(f.Field2); // no flow
+
+    f = new F();
+    f.Field2 = null;
+    sink(f.Field1); // flow
+    sink(f.Field2); // no flow
+
+    f = new F();
+    o = new Object();
+    f.Field1 = o;
+    f.Field2 = o;
+    m2(f);
+  }
+
+  private void m2(F f)
+  {
+    f.Field2 = null;
+    sink(f.Field1); // flow
+    sink(f.Field2); // no flow
+  }
+
+  public static void sink(Object o) { }
+}

java/ql/test/library-tests/dataflow/fields/flow.expected

@@ -26,3 +26,6 @@
 | E.java:2:32:2:43 | new Object(...) | E.java:21:10:21:24 | bh2.buf.content |
 | E.java:2:32:2:43 | new Object(...) | E.java:24:10:24:28 | p2.data.buf.content |
 | E.java:2:32:2:43 | new Object(...) | E.java:30:10:30:27 | p.data.buf.content |
+| F.java:5:14:5:25 | new Object(...) | F.java:20:10:20:17 | f.Field1 |
+| F.java:10:16:10:27 | new Object(...) | F.java:15:10:15:17 | f.Field1 |
+| F.java:24:9:24:20 | new Object(...) | F.java:33:10:33:17 | f.Field1 |