Merge pull request #4161 from yoff/SharedDataflow_PostUpdateNodes

codeql-ci · web-flow · commit dc9cc20fdd94 · 2020-08-31T11:57:44.000+01:00
Approved by RasmusWL, aschackmull, hvitved, jbj
diff --git a/cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll b/cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll
@@ -123,8 +123,18 @@ module Consistency {
     n.getEnclosingCallable() != call.getEnclosingCallable()
   }
 
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a result of `getPreUpdateNode` to be an
+  // instance of `PostUpdateNode`.
+  private Node getPre(PostUpdateNode n) {
+    result = n.getPreUpdateNode()
+    or
+    none()
+  }
+
   query predicate postIsNotPre(PostUpdateNode n, string msg) {
-    n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
+    getPre(n) = n and
+    msg = "PostUpdateNode should not equal its pre-update node."
   }
 
   query predicate postHasUniquePre(PostUpdateNode n, string msg) {
@@ -152,12 +162,6 @@ module Consistency {
     msg = "Origin of readStep is missing a PostUpdateNode."
   }
 
-  query predicate storeIsPostUpdate(Node n, string msg) {
-    storeStep(_, _, n) and
-    not n instanceof PostUpdateNode and
-    msg = "Store targets should be PostUpdateNodes."
-  }
-
   query predicate argHasPostUpdate(ArgumentNode n, string msg) {
     not hasPost(n) and
     not isImmutableOrUnobservable(n) and
diff --git a/cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll b/cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll
@@ -123,8 +123,18 @@ module Consistency {
     n.getEnclosingCallable() != call.getEnclosingCallable()
   }
 
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a result of `getPreUpdateNode` to be an
+  // instance of `PostUpdateNode`.
+  private Node getPre(PostUpdateNode n) {
+    result = n.getPreUpdateNode()
+    or
+    none()
+  }
+
   query predicate postIsNotPre(PostUpdateNode n, string msg) {
-    n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
+    getPre(n) = n and
+    msg = "PostUpdateNode should not equal its pre-update node."
   }
 
   query predicate postHasUniquePre(PostUpdateNode n, string msg) {
@@ -152,12 +162,6 @@ module Consistency {
     msg = "Origin of readStep is missing a PostUpdateNode."
   }
 
-  query predicate storeIsPostUpdate(Node n, string msg) {
-    storeStep(_, _, n) and
-    not n instanceof PostUpdateNode and
-    msg = "Store targets should be PostUpdateNodes."
-  }
-
   query predicate argHasPostUpdate(ArgumentNode n, string msg) {
     not hasPost(n) and
     not isImmutableOrUnobservable(n) and
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/dataflow-consistency.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/dataflow-consistency.expected
@@ -14,7 +14,6 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
 argHasPostUpdate
 | lambdas.cpp:18:7:18:7 | a | ArgumentNode is missing PostUpdateNode. |
 | lambdas.cpp:25:2:25:2 | b | ArgumentNode is missing PostUpdateNode. |
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/dataflow-ir-consistency.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/dataflow-ir-consistency.expected
@@ -29,5 +29,4 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
 argHasPostUpdate
diff --git a/cpp/ql/test/library-tests/dataflow/fields/dataflow-consistency.expected b/cpp/ql/test/library-tests/dataflow/fields/dataflow-consistency.expected
@@ -16,7 +16,6 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
 argHasPostUpdate
 | A.cpp:41:15:41:21 | new | ArgumentNode is missing PostUpdateNode. |
 | A.cpp:55:12:55:19 | new | ArgumentNode is missing PostUpdateNode. |
diff --git a/cpp/ql/test/library-tests/dataflow/fields/dataflow-ir-consistency.expected b/cpp/ql/test/library-tests/dataflow/fields/dataflow-ir-consistency.expected
@@ -23,5 +23,4 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
 argHasPostUpdate
diff --git a/cpp/ql/test/library-tests/syntax-zoo/dataflow-consistency.expected b/cpp/ql/test/library-tests/syntax-zoo/dataflow-consistency.expected
@@ -60,7 +60,6 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
 argHasPostUpdate
 | builtin.cpp:15:31:15:35 | * ... | ArgumentNode is missing PostUpdateNode. |
 | conditional_destructors.cpp:30:9:30:13 | call to C1 | ArgumentNode is missing PostUpdateNode. |
diff --git a/cpp/ql/test/library-tests/syntax-zoo/dataflow-ir-consistency.expected b/cpp/ql/test/library-tests/syntax-zoo/dataflow-ir-consistency.expected
@@ -1473,5 +1473,4 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
 argHasPostUpdate
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll
@@ -123,8 +123,18 @@ module Consistency {
     n.getEnclosingCallable() != call.getEnclosingCallable()
   }
 
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a result of `getPreUpdateNode` to be an
+  // instance of `PostUpdateNode`.
+  private Node getPre(PostUpdateNode n) {
+    result = n.getPreUpdateNode()
+    or
+    none()
+  }
+
   query predicate postIsNotPre(PostUpdateNode n, string msg) {
-    n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
+    getPre(n) = n and
+    msg = "PostUpdateNode should not equal its pre-update node."
   }
 
   query predicate postHasUniquePre(PostUpdateNode n, string msg) {
@@ -152,12 +162,6 @@ module Consistency {
     msg = "Origin of readStep is missing a PostUpdateNode."
   }
 
-  query predicate storeIsPostUpdate(Node n, string msg) {
-    storeStep(_, _, n) and
-    not n instanceof PostUpdateNode and
-    msg = "Store targets should be PostUpdateNodes."
-  }
-
   query predicate argHasPostUpdate(ArgumentNode n, string msg) {
     not hasPost(n) and
     not isImmutableOrUnobservable(n) and
diff --git a/java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll b/java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll
@@ -123,8 +123,18 @@ module Consistency {
     n.getEnclosingCallable() != call.getEnclosingCallable()
   }
 
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a result of `getPreUpdateNode` to be an
+  // instance of `PostUpdateNode`.
+  private Node getPre(PostUpdateNode n) {
+    result = n.getPreUpdateNode()
+    or
+    none()
+  }
+
   query predicate postIsNotPre(PostUpdateNode n, string msg) {
-    n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
+    getPre(n) = n and
+    msg = "PostUpdateNode should not equal its pre-update node."
   }
 
   query predicate postHasUniquePre(PostUpdateNode n, string msg) {
@@ -152,12 +162,6 @@ module Consistency {
     msg = "Origin of readStep is missing a PostUpdateNode."
   }
 
-  query predicate storeIsPostUpdate(Node n, string msg) {
-    storeStep(_, _, n) and
-    not n instanceof PostUpdateNode and
-    msg = "Store targets should be PostUpdateNodes."
-  }
-
   query predicate argHasPostUpdate(ArgumentNode n, string msg) {
     not hasPost(n) and
     not isImmutableOrUnobservable(n) and
diff --git a/python/ql/src/experimental/dataflow/internal/DataFlowImplConsistency.qll b/python/ql/src/experimental/dataflow/internal/DataFlowImplConsistency.qll
@@ -123,8 +123,18 @@ module Consistency {
     n.getEnclosingCallable() != call.getEnclosingCallable()
   }
 
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a result of `getPreUpdateNode` to be an
+  // instance of `PostUpdateNode`.
+  private Node getPre(PostUpdateNode n) {
+    result = n.getPreUpdateNode()
+    or
+    none()
+  }
+
   query predicate postIsNotPre(PostUpdateNode n, string msg) {
-    n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."
+    getPre(n) = n and
+    msg = "PostUpdateNode should not equal its pre-update node."
   }
 
   query predicate postHasUniquePre(PostUpdateNode n, string msg) {
@@ -152,12 +162,6 @@ module Consistency {
     msg = "Origin of readStep is missing a PostUpdateNode."
   }
 
-  query predicate storeIsPostUpdate(Node n, string msg) {
-    storeStep(_, _, n) and
-    not n instanceof PostUpdateNode and
-    msg = "Store targets should be PostUpdateNodes."
-  }
-
   query predicate argHasPostUpdate(ArgumentNode n, string msg) {
     not hasPost(n) and
     not isImmutableOrUnobservable(n) and
diff --git a/python/ql/src/experimental/dataflow/internal/DataFlowPrivate.qll b/python/ql/src/experimental/dataflow/internal/DataFlowPrivate.qll
@@ -15,6 +15,32 @@ class DataFlowCfgNode extends ControlFlowNode {
   DataFlowCfgNode() { isExpressionNode(this) }
 }
 
+/** A data flow node which should have an associated post-update node. */
+abstract class PreUpdateNode extends Node { }
+
+/** An argument might have its value changed as a result of a call. */
+class ArgumentPreUpdateNode extends PreUpdateNode, ArgumentNode { }
+
+/** An object might have its value changed after a store. */
+class StorePreUpdateNode extends PreUpdateNode, CfgNode {
+  StorePreUpdateNode() {
+    exists(Attribute a |
+      node = a.getObject().getAFlowNode() and
+      a.getCtx() instanceof Store
+    )
+  }
+}
+
+/** A node marking the state change of an object after a read */
+class ReadPreUpdateNode extends PreUpdateNode, CfgNode {
+  ReadPreUpdateNode() {
+    exists(Attribute a |
+      node = a.getObject().getAFlowNode() and
+      a.getCtx() instanceof Load
+    )
+  }
+}
+
 /**
  * A node associated with an object after an operation that might have
  * changed its state.
@@ -24,12 +50,21 @@ class DataFlowCfgNode extends ControlFlowNode {
  * an update to the field.
  *
  * Nodes corresponding to AST elements, for example `ExprNode`, usually refer
- * to the value before the update with the exception of `ObjectCreation`,
- * which represents the value after the constructor has run.
+ * to the value before the update.
  */
-abstract class PostUpdateNode extends Node {
+class PostUpdateNode extends Node, TPostUpdateNode {
+  PreUpdateNode pre;
+
+  PostUpdateNode() { this = TPostUpdateNode(pre) }
+
   /** Gets the node before the state update. */
-  abstract Node getPreUpdateNode();
+  Node getPreUpdateNode() { result = pre }
+
+  override string toString() { result = "[post] " + pre.toString() }
+
+  override Scope getScope() { result = pre.getScope() }
+
+  override Location getLocation() { result = pre.getLocation() }
 }
 
 class DataFlowExpr = Expr;
@@ -98,7 +133,17 @@ module EssaFlow {
 predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo) {
   not nodeFrom.(EssaNode).getVar() instanceof GlobalSsaVariable and
   not nodeTo.(EssaNode).getVar() instanceof GlobalSsaVariable and
-  EssaFlow::essaFlowStep(nodeFrom, nodeTo)
+  EssaFlow::essaFlowStep(update(nodeFrom), nodeTo)
+}
+
+private Node update(Node node) {
+  exists(PostUpdateNode pun |
+    node = pun.getPreUpdateNode() and
+    result = pun
+  )
+  or
+  not exists(PostUpdateNode pun | node = pun.getPreUpdateNode()) and
+  result = node
 }
 
 // TODO: Make modules for these headings
diff --git a/python/ql/src/experimental/dataflow/internal/DataFlowPublic.qll b/python/ql/src/experimental/dataflow/internal/DataFlowPublic.qll
@@ -20,7 +20,9 @@ newtype TNode =
   /** A node corresponding to an SSA variable. */
   TEssaNode(EssaVariable var) or
   /** A node corresponding to a control flow node. */
-  TCfgNode(DataFlowCfgNode node)
+  TCfgNode(DataFlowCfgNode node) or
+  /** A node representing the value of an object after a state change */
+  TPostUpdateNode(PreUpdateNode pre)
 
 /**
  * An element, viewed as a node in a data flow graph. Either an SSA variable
diff --git a/python/ql/test/experimental/dataflow/basic/local.expected b/python/ql/test/experimental/dataflow/basic/local.expected
@@ -38,3 +38,4 @@
 | test.py:7:5:7:20 | ControlFlowNode for obfuscated_id() | test.py:7:5:7:20 | ControlFlowNode for obfuscated_id() |
 | test.py:7:5:7:20 | GSSA Variable a | test.py:7:5:7:20 | GSSA Variable a |
 | test.py:7:19:7:19 | ControlFlowNode for a | test.py:7:19:7:19 | ControlFlowNode for a |
+| test.py:7:19:7:19 | [post] ControlFlowNode for a | test.py:7:19:7:19 | [post] ControlFlowNode for a |
diff --git a/python/ql/test/experimental/dataflow/basic/sinks.expected b/python/ql/test/experimental/dataflow/basic/sinks.expected
@@ -23,3 +23,4 @@
 | test.py:7:5:7:20 | ControlFlowNode for obfuscated_id() |
 | test.py:7:5:7:20 | GSSA Variable a |
 | test.py:7:19:7:19 | ControlFlowNode for a |
+| test.py:7:19:7:19 | [post] ControlFlowNode for a |
diff --git a/python/ql/test/experimental/dataflow/basic/sources.expected b/python/ql/test/experimental/dataflow/basic/sources.expected
@@ -23,3 +23,4 @@
 | test.py:7:5:7:20 | ControlFlowNode for obfuscated_id() |
 | test.py:7:5:7:20 | GSSA Variable a |
 | test.py:7:19:7:19 | ControlFlowNode for a |
+| test.py:7:19:7:19 | [post] ControlFlowNode for a |
diff --git a/python/ql/test/experimental/dataflow/consistency/dataflow-consistency.expected b/python/ql/test/experimental/dataflow/consistency/dataflow-consistency.expected
@@ -85,21 +85,4 @@ postHasUniquePre
 uniquePostUpdate
 postIsInSameCallable
 reverseRead
-storeIsPostUpdate
-| test.py:152:9:152:16 | ControlFlowNode for List | Store targets should be PostUpdateNodes. |
-| test.py:153:9:153:24 | ControlFlowNode for Dict | Store targets should be PostUpdateNodes. |
 argHasPostUpdate
-| test.py:25:10:25:10 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:29:10:29:10 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:48:19:48:21 | ControlFlowNode for arg | ArgumentNode is missing PostUpdateNode. |
-| test.py:51:10:51:12 | ControlFlowNode for arg | ArgumentNode is missing PostUpdateNode. |
-| test.py:55:14:55:16 | ControlFlowNode for arg | ArgumentNode is missing PostUpdateNode. |
-| test.py:59:11:59:11 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:67:11:67:14 | ControlFlowNode for cond | ArgumentNode is missing PostUpdateNode. |
-| test.py:67:17:67:17 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:74:11:74:14 | ControlFlowNode for cond | ArgumentNode is missing PostUpdateNode. |
-| test.py:74:17:74:17 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:81:13:81:13 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:86:13:86:13 | ControlFlowNode for t | ArgumentNode is missing PostUpdateNode. |
-| test.py:158:15:158:15 | ControlFlowNode for l | ArgumentNode is missing PostUpdateNode. |
-| test.py:159:15:159:15 | ControlFlowNode for d | ArgumentNode is missing PostUpdateNode. |
diff --git a/python/ql/test/experimental/dataflow/coverage/classes.py b/python/ql/test/experimental/dataflow/coverage/classes.py
@@ -93,7 +93,7 @@ class With_str:
 
     def __str__(self):
         SINK1(self)  # Flow not found
-        OK()  # Call not found  # Call not found
+        OK()  # Call not found
         return "Awesome"
 
 
@@ -108,7 +108,7 @@ class With_bytes:
 
     def __bytes__(self):
         SINK1(self)  # Flow not found
-        OK()  # Call not found  # Call not found
+        OK()  # Call not found
         return b"Awesome"
 
 
@@ -124,7 +124,7 @@ class With_format:
     def __format__(self, format_spec):
         SINK2(format_spec)  # Flow not found
         SINK1(self)  # Flow not found
-        OK()  # Call not found  # Call not found
+        OK()  # Call not found
         return "Awesome"
 
 
@@ -151,7 +151,7 @@ class With_lt:
     def __lt__(self, other):
         SINK2(other)  # Flow not found
         SINK1(self)  # Flow not found
-        OK()  # Call not found  # Call not found
+        OK()  # Call not found
         return ""
 
 
