From dbeef312cac2615d59ddbefc85bacdfac792a744 Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Thu, 9 Jul 2020 10:05:23 +0200
Subject: [PATCH 01/10] add some TypeScript tests to DeadStoreOfProperty

---
 .../DeadStoreOfProperty.expected                 |  2 ++
 .../DeadStoreOfProperty/fieldInit.ts             | 16 ++++++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected
index 68890cc34da7..0e895b542dbe 100644
--- a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected
+++ b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected
@@ -1,4 +1,6 @@
 | fieldInit.ts:10:3:10:8 | f = 4; | This write to property 'f' is useless, since $@ always overrides it. | fieldInit.ts:13:5:13:14 | this.f = 5 | another property write |
+| fieldInit.ts:18:22:18:22 | h | This write to property 'h' is useless, since $@ always overrides it. | fieldInit.ts:19:5:19:14 | this.h = h | another property write |
+| fieldInit.ts:24:3:24:20 | static static() {} | This write to property 'static' is useless, since $@ always overrides it. | fieldInit.ts:30:3:30:20 | static static() {} | another property write |
 | real-world-examples.js:5:4:5:11 | o.p = 42 | This write to property 'p' is useless, since $@ always overrides it. | real-world-examples.js:10:2:10:9 | o.p = 42 | another property write |
 | real-world-examples.js:15:9:15:18 | o.p1 += 42 | This write to property 'p1' is useless, since $@ always overrides it. | real-world-examples.js:15:2:15:18 | o.p1 = o.p1 += 42 | another property write |
 | real-world-examples.js:16:11:16:20 | o.p2 *= 42 | This write to property 'p2' is useless, since $@ always overrides it. | real-world-examples.js:16:2:16:21 | o.p2 -= (o.p2 *= 42) | another property write |
diff --git a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts
index bc2338f25a0a..7768e25f79f1 100644
--- a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts
+++ b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts
@@ -13,3 +13,19 @@ class D {
     this.f = 5;
   }
 }
+
+class G {
+  constructor(public h: string) { // NOT OK
+    this.h = h;
+  }
+}
+
+class Foo {
+  static static() {}
+
+  static *foo() {}
+
+  static set() {}
+
+  static static() {}
+}
\ No newline at end of file

From 97aa3cc8a3c4e41be873b283b5b7065b8a1d5686 Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Thu, 9 Jul 2020 10:09:20 +0200
Subject: [PATCH 02/10] rewrite DeadStoreOfProperty to improve worst-case
 complexity

---
 .../src/Declarations/DeadStoreOfProperty.ql   | 248 ++++++++++++++----
 .../semmle/javascript/GlobalAccessPaths.qll   |   2 +-
 .../DeadStoreOfProperty.expected              |   1 -
 .../DeadStoreOfProperty/fieldInit.ts          |  10 -
 .../Declarations/DeadStoreOfProperty/tst.js   |  14 +-
 5 files changed, 205 insertions(+), 70 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index 1470f164ab28..74d42bf33e4f 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -13,13 +13,15 @@ import Expressions.DOMProperties
 import DeadStore
 
 /**
- * Holds if `write` writes to property `name` of `base`, and `base` is the only base object of `write`.
+ * Holds if `write` writes to a property of a base, and there is only one base object of `write`.
  */
-predicate unambiguousPropWrite(DataFlow::SourceNode base, string name, DataFlow::PropWrite write) {
-  write = base.getAPropertyWrite(name) and
-  not exists(DataFlow::SourceNode otherBase |
-    otherBase != base and
-    write = otherBase.getAPropertyWrite(name)
+predicate unambiguousPropWrite(DataFlow::PropWrite write) {
+  exists(DataFlow::SourceNode base, string name |
+    write = base.getAPropertyWrite(name) and
+    not exists(DataFlow::SourceNode otherBase |
+      otherBase != base and
+      write = otherBase.getAPropertyWrite(name)
+    )
   )
 }
 
@@ -27,31 +29,50 @@ predicate unambiguousPropWrite(DataFlow::SourceNode base, string name, DataFlow:
  * Holds if `assign1` and `assign2` both assign property `name` of the same object, and `assign2` post-dominates `assign1`.
  */
 predicate postDominatedPropWrite(
-  string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2
+  string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2, boolean local
 ) {
+  exists(DataFlow::SourceNode base |
+    assign1 = base.getAPropertyWrite(name) and
+    assign2 = base.getAPropertyWrite(name)
+  ) and
   exists(
-    ControlFlowNode write1, ControlFlowNode write2, DataFlow::SourceNode base,
-    ReachableBasicBlock block1, ReachableBasicBlock block2
+    ControlFlowNode write1, ControlFlowNode write2, ReachableBasicBlock block1,
+    ReachableBasicBlock block2
   |
     write1 = assign1.getWriteNode() and
     write2 = assign2.getWriteNode() and
     block1 = write1.getBasicBlock() and
     block2 = write2.getBasicBlock() and
-    unambiguousPropWrite(base, name, assign1) and
-    unambiguousPropWrite(base, name, assign2) and
-    block2.postDominates(block1) and
+    unambiguousPropWrite(assign1) and
+    unambiguousPropWrite(assign2) and
     (
-      block1 = block2
-      implies
-      exists(int i1, int i2 |
-        write1 = block1.getNode(i1) and
-        write2 = block2.getNode(i2) and
-        i1 < i2
-      )
+      block2.strictlyPostDominates(block1) and local = false
+      or
+      block1 = block2 and
+      local = true and
+      getRank(block1, write1, name) < getRank(block2, write2, name)
     )
   )
 }
 
+/**
+ * Gets the rank for the read/write `ref` of a property `name` inside basicblock `bb`.
+ */
+int getRank(ReachableBasicBlock bb, ControlFlowNode ref, string name) {
+  ref =
+    rank[result](ControlFlowNode e |
+      exists(DataFlow::PropWrite write |
+        write.getPropertyName() = name and
+        e = write.getWriteNode() and
+        unambiguousPropWrite(write)
+      )
+      or
+      e.(PropAccess).getPropertyName() = name and e instanceof RValue
+    |
+      e order by any(int i | e = bb.getNode(i))
+    )
+}
+
 /**
  * Holds if `e` may access a property named `name`.
  */
@@ -67,8 +88,11 @@ predicate maybeAccessesProperty(Expr e, string name) {
  * Holds if `assign1` and `assign2` both assign property `name`, but `assign1` is dead because of `assign2`.
  */
 predicate isDeadAssignment(string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2) {
-  postDominatedPropWrite(name, assign1, assign2) and
-  noPropAccessBetween(name, assign1, assign2) and
+  (
+    noPropAccessBetweenLocal(name, assign1, assign2)
+    or
+    noPropAccessBetweenGlobal(name, assign1, assign2)
+  ) and
   not isDOMProperty(name)
 }
 
@@ -76,58 +100,170 @@ predicate isDeadAssignment(string name, DataFlow::PropWrite assign1, DataFlow::P
  * Holds if `assign` assigns a property `name` that may be accessed somewhere else in the same block,
  * `after` indicates if the access happens before or after the node for `assign`.
  */
-bindingset[name]
-predicate maybeAccessesAssignedPropInBlock(string name, DataFlow::PropWrite assign, boolean after) {
-  exists(ReachableBasicBlock block, int i, int j, Expr e |
-    assign.getWriteNode() = block.getNode(i) and
-    e = block.getNode(j) and
-    maybeAccessesProperty(e, name)
+predicate maybeAccessesAssignedPropInBlock(DataFlow::PropWrite assign, boolean after) {
+  (
+    // early pruning - manual magic
+    after = true and postDominatedPropWrite(_, assign, _, false)
+    or
+    after = false and postDominatedPropWrite(_, _, assign, false)
+  ) and
+  exists(ReachableBasicBlock block, int i, int j, Expr e, string name |
+    i = getRank(block, assign.getWriteNode(), name) and
+    j = getRank(block, e, name) and
+    e instanceof PropAccess and
+    e instanceof RValue
   |
     after = true and i < j
     or
     after = false and j < i
   )
+  or
+  exists(ReachableBasicBlock block | assign.getWriteNode().getBasicBlock() = block |
+    after = true and isBeforeImpure(assign, block)
+    or
+    after = false and isAfterImpure(assign, block)
+  )
 }
 
 /**
- * Holds if `assign1` and `assign2` both assign property `name`, and the assigned property is not accessed between the two assignments.
+ * Holds if a ControlFlowNode `c` is before an impure expression inside `bb`.
  */
-bindingset[name]
-predicate noPropAccessBetween(string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2) {
+predicate isBeforeImpure(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+  getANodeAfterWrite(write, bb).(Expr).isImpure()
+}
+
+/**
+ * Gets a ControlFlowNode that comes after `write` inside `bb`.
+ * Stops after finding the first impure expression
+ */
+ControlFlowNode getANodeAfterWrite(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+  // base case
+  result.getBasicBlock() = bb and
+  postDominatedPropWrite(_, write, _, false) and // early pruning - manual magic
+  result = write.getWriteNode().getASuccessor()
+  or
+  // recursive case
+  exists(ControlFlowNode prev | prev = getANodeAfterWrite(write, bb) |
+    not result instanceof BasicBlock and
+    not prev.(Expr).isImpure() and
+    result = prev.getASuccessor()
+  )
+}
+
+/**
+ * Holds if a ControlFlowNode `c` is after an impure expression inside `bb`.
+ */
+predicate isAfterImpure(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+  getANodeBeforeWrite(write, bb).(Expr).isImpure()
+}
+
+/**
+ * Gets a ControlFlowNode that comes before `write` inside `bb`.
+ * Stops after finding the first impure expression.
+ */
+ControlFlowNode getANodeBeforeWrite(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+  // base case
+  result.getBasicBlock() = bb and
+  postDominatedPropWrite(_, _, write, false) and // early pruning - manual magic
+  result = write.getWriteNode().getAPredecessor()
+  or
+  // recursive case
+  exists(ControlFlowNode prev | prev = getANodeBeforeWrite(write, bb) |
+    not prev instanceof BasicBlock and
+    not prev.(Expr).isImpure() and
+    result = prev.getAPredecessor()
+  )
+}
+
+/**
+ * Gets a successor inside `bb` in the control-flow graph that does not pass through an impure expression (except for writes to `name`).
+ * Stops after the first write to `name` that happens after `node`.
+ */
+ControlFlowNode getAPureSuccessor(ControlFlowNode node) {
+  // stop at impure expressions (except writes to `name`)
+  not (
+    maybeAccessesProperty(result, getPropertyWriteName(node)) and
+    not result =
+      any(DataFlow::PropWrite write | write.getPropertyName() = getPropertyWriteName(node))
+          .getWriteNode()
+  ) and
+  (
+    // base case.
+    exists(DataFlow::PropWrite write |
+      node = write.getWriteNode() and
+      result = node.getASuccessor() and
+      // cheap check that there might exist a result we are interrested in,
+      postDominatedPropWrite(_, write, _, true)
+    )
+    or
+    // recursive case
+    exists(ControlFlowNode pred | pred = getAPureSuccessor(node) | result = pred.getASuccessor()) and
+    // stop at basic-block boundaries
+    not result instanceof BasicBlock and
+    // make sure we stop after the first write to `name` that comes after `node`.
+    (
+      not result.getAPredecessor() =
+        any(DataFlow::PropWrite write | write.getPropertyName() = getPropertyWriteName(node))
+            .getWriteNode()
+      or
+      result.getAPredecessor() = node
+    )
+  )
+}
+
+/**
+ * Gets the property name that is written to by the control-flow-node `writeNode`.
+ */
+private string getPropertyWriteName(ControlFlowNode writeNode) {
+  exists(DataFlow::PropWrite write |
+    write.getWriteNode() = writeNode and result = write.getPropertyName()
+  )
+}
+
+/**
+ * Holds if `assign1` and `assign2` are inside the same basicblock and both assign property `name`, and the assigned property is not accessed between the two assignments.
+ */
+predicate noPropAccessBetweenLocal(
+  string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2
+) {
+  exists(ControlFlowNode write1, ControlFlowNode write2 |
+    postDominatedPropWrite(name, assign1, assign2, true) and
+    write1 = assign1.getWriteNode() and
+    write2 = assign2.getWriteNode() and
+    getRank(_, write1, name) < getRank(_, write2, name) and
+    write2 = getAPureSuccessor(write1)
+  )
+}
+
+/**
+ * Holds if `assign1` and `assign2` are in different basicblocks and both assign property `name`, and the assigned property is not accessed between the two assignments.
+ *
+ * Much of this predicate is copy-pasted from `noPropAccessBetweenLocal`, but the predicates are separate to avoid join-order issues.
+ */
+pragma[nomagic]
+predicate noPropAccessBetweenGlobal(
+  string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2
+) {
   exists(
     ControlFlowNode write1, ControlFlowNode write2, ReachableBasicBlock block1,
     ReachableBasicBlock block2
   |
+    postDominatedPropWrite(name, assign1, assign2, false) and // early pruning
     write1 = assign1.getWriteNode() and
+    not maybeAccessesAssignedPropInBlock(assign1, true) and
     write2 = assign2.getWriteNode() and
+    not maybeAccessesAssignedPropInBlock(assign2, false) and
     write1.getBasicBlock() = block1 and
     write2.getBasicBlock() = block2 and
-    if block1 = block2
-    then
-      // same block: check for access between
-      not exists(int i1, Expr mid, int i2 |
-        write1 = block1.getNode(i1) and
-        write2 = block2.getNode(i2) and
-        mid = block1.getNode([i1 + 1 .. i2 - 1]) and
-        maybeAccessesProperty(mid, name)
-      )
-    else
-      // other block:
-      not (
-        // check for an access after the first write node
-        maybeAccessesAssignedPropInBlock(name, assign1, true)
-        or
-        // check for an access between the two write blocks
-        exists(ReachableBasicBlock mid |
-          block1.getASuccessor+() = mid and
-          mid.getASuccessor+() = block2
-        |
-          maybeAccessesProperty(mid.getANode(), name)
-        )
-        or
-        // check for an access before the second write node
-        maybeAccessesAssignedPropInBlock(name, assign2, false)
-      )
+    not block1 = block2 and
+    // other block:
+    // check for an access between the two write blocks
+    not exists(ReachableBasicBlock mid |
+      block1.getASuccessor+() = mid and
+      mid.getASuccessor+() = block2
+    |
+      maybeAccessesProperty(mid.getANode(), name)
+    )
   )
 }
 
diff --git a/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll b/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll
index cfea69c70bbe..7a7577c6191d 100644
--- a/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll
+++ b/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll
@@ -440,7 +440,7 @@ module AccessPath {
      *
      * Only has a result if there exists both a read and write of the access-path within `bb`.
      */
-    private ControlFlowNode rankedAccessPath(
+    ControlFlowNode rankedAccessPath(
       ReachableBasicBlock bb, Root root, string path, int ranking, AccessPathKind type
     ) {
       result =
diff --git a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected
index 0e895b542dbe..12bc75ba7255 100644
--- a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected
+++ b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/DeadStoreOfProperty.expected
@@ -1,6 +1,5 @@
 | fieldInit.ts:10:3:10:8 | f = 4; | This write to property 'f' is useless, since $@ always overrides it. | fieldInit.ts:13:5:13:14 | this.f = 5 | another property write |
 | fieldInit.ts:18:22:18:22 | h | This write to property 'h' is useless, since $@ always overrides it. | fieldInit.ts:19:5:19:14 | this.h = h | another property write |
-| fieldInit.ts:24:3:24:20 | static static() {} | This write to property 'static' is useless, since $@ always overrides it. | fieldInit.ts:30:3:30:20 | static static() {} | another property write |
 | real-world-examples.js:5:4:5:11 | o.p = 42 | This write to property 'p' is useless, since $@ always overrides it. | real-world-examples.js:10:2:10:9 | o.p = 42 | another property write |
 | real-world-examples.js:15:9:15:18 | o.p1 += 42 | This write to property 'p1' is useless, since $@ always overrides it. | real-world-examples.js:15:2:15:18 | o.p1 = o.p1 += 42 | another property write |
 | real-world-examples.js:16:11:16:20 | o.p2 *= 42 | This write to property 'p2' is useless, since $@ always overrides it. | real-world-examples.js:16:2:16:21 | o.p2 -= (o.p2 *= 42) | another property write |
diff --git a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts
index 7768e25f79f1..a2b922684dda 100644
--- a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts
+++ b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/fieldInit.ts
@@ -19,13 +19,3 @@ class G {
     this.h = h;
   }
 }
-
-class Foo {
-  static static() {}
-
-  static *foo() {}
-
-  static set() {}
-
-  static static() {}
-}
\ No newline at end of file
diff --git a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js
index 2fd07a91d17b..ee8643b0a152 100644
--- a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js
+++ b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js
@@ -92,7 +92,7 @@
     o.defaulted2 = 42;
 
     var o = {};
-    o.pure18 = 42; // NOT OK
+    o.pure18 = 42; // NOT OK TODO: Currently have duplicate result.
     o.pure18 = 42; // NOT OK
     o.pure18 = 42;
 
@@ -124,5 +124,15 @@
 
 	var o = {};
 	Object.defineProperty(o, "prop", {writable:!0,configurable:!0,enumerable:!1}) // OK
-	o.prop = 42;
+    o.prop = 42;
+    
+    var o = {};
+    o.pure19 = 42; // OK
+    o.some_other_property = 42;
+    o.pure19 = 42;
+
+    var o = {};
+    o.pure20 = 42; // OK
+    some_other_obj.some_other_property = 42;
+    o.pure20 = 42;
 });

From 8131618382896178c70f102715497dfbf7909633 Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Mon, 3 Aug 2020 14:25:25 +0200
Subject: [PATCH 03/10] revert making `rankedAccessPath` private

---
 javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll b/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll
index 7a7577c6191d..cfea69c70bbe 100644
--- a/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll
+++ b/javascript/ql/src/semmle/javascript/GlobalAccessPaths.qll
@@ -440,7 +440,7 @@ module AccessPath {
      *
      * Only has a result if there exists both a read and write of the access-path within `bb`.
      */
-    ControlFlowNode rankedAccessPath(
+    private ControlFlowNode rankedAccessPath(
       ReachableBasicBlock bb, Root root, string path, int ranking, AccessPathKind type
     ) {
       result =

From e629e6bbb023fed9a0d14bc86dafdfc031202b95 Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Mon, 3 Aug 2020 14:55:12 +0200
Subject: [PATCH 04/10] changes based on review

---
 .../src/Declarations/DeadStoreOfProperty.ql   | 20 ++++++++++---------
 .../Declarations/DeadStoreOfProperty/tst.js   |  2 +-
 2 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index 74d42bf33e4f..6072f39c7499 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -97,10 +97,10 @@ predicate isDeadAssignment(string name, DataFlow::PropWrite assign1, DataFlow::P
 }
 
 /**
- * Holds if `assign` assigns a property `name` that may be accessed somewhere else in the same block,
+ * Holds if `assign` assigns a property that may be accessed somewhere else in the same block,
  * `after` indicates if the access happens before or after the node for `assign`.
  */
-predicate maybeAccessesAssignedPropInBlock(DataFlow::PropWrite assign, boolean after) {
+predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean after) {
   (
     // early pruning - manual magic
     after = true and postDominatedPropWrite(_, assign, _, false)
@@ -176,11 +176,13 @@ ControlFlowNode getANodeBeforeWrite(DataFlow::PropWrite write, ReachableBasicBlo
 }
 
 /**
- * Gets a successor inside `bb` in the control-flow graph that does not pass through an impure expression (except for writes to `name`).
- * Stops after the first write to `name` that happens after `node`.
+ * Gets a successor inside `bb` in the control-flow graph that does not pass through an impure expression (except for writes to the same property).
+ * Stops after the first write to same property that happens after `node`.
+ * 
+ * `node` always corresponds to the CFG node of a `DataFlow::PropWrite` with a known name.
  */
 ControlFlowNode getAPureSuccessor(ControlFlowNode node) {
-  // stop at impure expressions (except writes to `name`)
+  // stop at reads of `name` and at impure expressions (except writes to `name`)
   not (
     maybeAccessesProperty(result, getPropertyWriteName(node)) and
     not result =
@@ -197,10 +199,10 @@ ControlFlowNode getAPureSuccessor(ControlFlowNode node) {
     )
     or
     // recursive case
-    exists(ControlFlowNode pred | pred = getAPureSuccessor(node) | result = pred.getASuccessor()) and
+    result = getAPureSuccessor(node).getASuccessor() and
     // stop at basic-block boundaries
     not result instanceof BasicBlock and
-    // make sure we stop after the first write to `name` that comes after `node`.
+    // make sure we stop after the first write to the same property that comes after `node`.
     (
       not result.getAPredecessor() =
         any(DataFlow::PropWrite write | write.getPropertyName() = getPropertyWriteName(node))
@@ -250,9 +252,9 @@ predicate noPropAccessBetweenGlobal(
   |
     postDominatedPropWrite(name, assign1, assign2, false) and // early pruning
     write1 = assign1.getWriteNode() and
-    not maybeAccessesAssignedPropInBlock(assign1, true) and
+    not maybeAssignsAccessedPropInBlock(assign1, true) and
     write2 = assign2.getWriteNode() and
-    not maybeAccessesAssignedPropInBlock(assign2, false) and
+    not maybeAssignsAccessedPropInBlock(assign2, false) and
     write1.getBasicBlock() = block1 and
     write2.getBasicBlock() = block2 and
     not block1 = block2 and
diff --git a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js
index ee8643b0a152..39db5056b77b 100644
--- a/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js
+++ b/javascript/ql/test/query-tests/Declarations/DeadStoreOfProperty/tst.js
@@ -92,7 +92,7 @@
     o.defaulted2 = 42;
 
     var o = {};
-    o.pure18 = 42; // NOT OK TODO: Currently have duplicate result.
+    o.pure18 = 42; // NOT OK
     o.pure18 = 42; // NOT OK
     o.pure18 = 42;
 

From eccfade9288d0651451be1d6fbac0b266008fb9c Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Tue, 4 Aug 2020 10:24:49 +0200
Subject: [PATCH 05/10] rewrite parts of the DeadStoreOfProperty query

---
 .../src/Declarations/DeadStoreOfProperty.ql   | 95 +++++++------------
 1 file changed, 34 insertions(+), 61 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index 6072f39c7499..ebc6eede34d1 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -67,18 +67,25 @@ int getRank(ReachableBasicBlock bb, ControlFlowNode ref, string name) {
         unambiguousPropWrite(write)
       )
       or
-      e.(PropAccess).getPropertyName() = name and e instanceof RValue
+      isAPropertyRead(e, name)
     |
       e order by any(int i | e = bb.getNode(i))
     )
 }
 
+/**
+ * Holds if `e` is a property read of a property `name`.
+ */
+predicate isAPropertyRead(Expr e, string name) {
+  exists(DataFlow::PropRead read | read.asExpr() = e and read.getPropertyName() = name)
+}
+
 /**
  * Holds if `e` may access a property named `name`.
  */
 bindingset[name]
 predicate maybeAccessesProperty(Expr e, string name) {
-  e.(PropAccess).getPropertyName() = name and e instanceof RValue
+  isAPropertyRead(e, name)
   or
   // conservatively reject all side-effects
   e.isImpure()
@@ -89,7 +96,8 @@ predicate maybeAccessesProperty(Expr e, string name) {
  */
 predicate isDeadAssignment(string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2) {
   (
-    noPropAccessBetweenLocal(name, assign1, assign2)
+    assign2.getWriteNode() = getANodeWithNoPropAccessBetweenInsideBlock(name, assign1) and
+    postDominatedPropWrite(name, assign1, assign2, true)
     or
     noPropAccessBetweenGlobal(name, assign1, assign2)
   ) and
@@ -110,8 +118,7 @@ predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean af
   exists(ReachableBasicBlock block, int i, int j, Expr e, string name |
     i = getRank(block, assign.getWriteNode(), name) and
     j = getRank(block, e, name) and
-    e instanceof PropAccess and
-    e instanceof RValue
+    isAPropertyRead(e, name)
   |
     after = true and i < j
     or
@@ -176,71 +183,38 @@ ControlFlowNode getANodeBeforeWrite(DataFlow::PropWrite write, ReachableBasicBlo
 }
 
 /**
- * Gets a successor inside `bb` in the control-flow graph that does not pass through an impure expression (except for writes to the same property).
- * Stops after the first write to same property that happens after `node`.
- * 
- * `node` always corresponds to the CFG node of a `DataFlow::PropWrite` with a known name.
+ * Holds if `write` and `result` are inside the same basicblock, and `write` assigns property `name`, and `result` is a (transitive) successor of `write`, and `name` is not accessed between `write` and `result`.
+ *
+ * The predicate is computed recursively by computing transitive successors of `write` while removing the successors that could access `name`.
+ * Stops at the first write to `name` that occours after `write`.
  */
-ControlFlowNode getAPureSuccessor(ControlFlowNode node) {
+ControlFlowNode getANodeWithNoPropAccessBetweenInsideBlock(string name, DataFlow::PropWrite write) {
+  (
+    // base case.
+    result = write.getWriteNode().getASuccessor() and
+    postDominatedPropWrite(name, write, _, true) // manual magic - cheap check that there might exist a result we are interrested in,
+    or
+    // recursive case
+    result = getANodeWithNoPropAccessBetweenInsideBlock(name, write).getASuccessor()
+  ) and
+  // stop at basic-block boundaries
+  not result instanceof BasicBlock and
   // stop at reads of `name` and at impure expressions (except writes to `name`)
   not (
-    maybeAccessesProperty(result, getPropertyWriteName(node)) and
-    not result =
-      any(DataFlow::PropWrite write | write.getPropertyName() = getPropertyWriteName(node))
-          .getWriteNode()
+    maybeAccessesProperty(result, name) and
+    not result = any(DataFlow::PropWrite w | w.getPropertyName() = name).getWriteNode()
   ) and
+  // stop at the first write to `name` that comes after `write`.
   (
-    // base case.
-    exists(DataFlow::PropWrite write |
-      node = write.getWriteNode() and
-      result = node.getASuccessor() and
-      // cheap check that there might exist a result we are interrested in,
-      postDominatedPropWrite(_, write, _, true)
-    )
+    not result.getAPredecessor() =
+      any(DataFlow::PropWrite w | w.getPropertyName() = name).getWriteNode()
     or
-    // recursive case
-    result = getAPureSuccessor(node).getASuccessor() and
-    // stop at basic-block boundaries
-    not result instanceof BasicBlock and
-    // make sure we stop after the first write to the same property that comes after `node`.
-    (
-      not result.getAPredecessor() =
-        any(DataFlow::PropWrite write | write.getPropertyName() = getPropertyWriteName(node))
-            .getWriteNode()
-      or
-      result.getAPredecessor() = node
-    )
-  )
-}
-
-/**
- * Gets the property name that is written to by the control-flow-node `writeNode`.
- */
-private string getPropertyWriteName(ControlFlowNode writeNode) {
-  exists(DataFlow::PropWrite write |
-    write.getWriteNode() = writeNode and result = write.getPropertyName()
-  )
-}
-
-/**
- * Holds if `assign1` and `assign2` are inside the same basicblock and both assign property `name`, and the assigned property is not accessed between the two assignments.
- */
-predicate noPropAccessBetweenLocal(
-  string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2
-) {
-  exists(ControlFlowNode write1, ControlFlowNode write2 |
-    postDominatedPropWrite(name, assign1, assign2, true) and
-    write1 = assign1.getWriteNode() and
-    write2 = assign2.getWriteNode() and
-    getRank(_, write1, name) < getRank(_, write2, name) and
-    write2 = getAPureSuccessor(write1)
+    result.getAPredecessor() = write.getWriteNode()
   )
 }
 
 /**
  * Holds if `assign1` and `assign2` are in different basicblocks and both assign property `name`, and the assigned property is not accessed between the two assignments.
- *
- * Much of this predicate is copy-pasted from `noPropAccessBetweenLocal`, but the predicates are separate to avoid join-order issues.
  */
 pragma[nomagic]
 predicate noPropAccessBetweenGlobal(
@@ -250,7 +224,7 @@ predicate noPropAccessBetweenGlobal(
     ControlFlowNode write1, ControlFlowNode write2, ReachableBasicBlock block1,
     ReachableBasicBlock block2
   |
-    postDominatedPropWrite(name, assign1, assign2, false) and // early pruning
+    postDominatedPropWrite(name, assign1, assign2, false) and // manual magic - early pruning
     write1 = assign1.getWriteNode() and
     not maybeAssignsAccessedPropInBlock(assign1, true) and
     write2 = assign2.getWriteNode() and
@@ -258,7 +232,6 @@ predicate noPropAccessBetweenGlobal(
     write1.getBasicBlock() = block1 and
     write2.getBasicBlock() = block2 and
     not block1 = block2 and
-    // other block:
     // check for an access between the two write blocks
     not exists(ReachableBasicBlock mid |
       block1.getASuccessor+() = mid and

From 374b1b7b97720b89654bb0fe80048fe907a96922 Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Tue, 11 Aug 2020 14:24:49 +0200
Subject: [PATCH 06/10] apply manual magic in both cases in
 `maybeAssignsAccessedPropInBlock`

---
 .../src/Declarations/DeadStoreOfProperty.ql   | 28 ++++++++++---------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index ebc6eede34d1..d7ddf6e906fe 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -115,20 +115,22 @@ predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean af
     or
     after = false and postDominatedPropWrite(_, _, assign, false)
   ) and
-  exists(ReachableBasicBlock block, int i, int j, Expr e, string name |
-    i = getRank(block, assign.getWriteNode(), name) and
-    j = getRank(block, e, name) and
-    isAPropertyRead(e, name)
-  |
-    after = true and i < j
-    or
-    after = false and j < i
-  )
-  or
-  exists(ReachableBasicBlock block | assign.getWriteNode().getBasicBlock() = block |
-    after = true and isBeforeImpure(assign, block)
+  (
+    exists(ReachableBasicBlock block, int i, int j, Expr e, string name |
+      i = getRank(block, assign.getWriteNode(), name) and
+      j = getRank(block, e, name) and
+      isAPropertyRead(e, name)
+    |
+      after = true and i < j
+      or
+      after = false and j < i
+    )
     or
-    after = false and isAfterImpure(assign, block)
+    exists(ReachableBasicBlock block | assign.getWriteNode().getBasicBlock() = block |
+      after = true and isBeforeImpure(assign, block)
+      or
+      after = false and isAfterImpure(assign, block)
+    )
   )
 }
 

From 9e768375ce0639fcfc6cf8d9eb25f4ca096948aa Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Tue, 11 Aug 2020 14:27:12 +0200
Subject: [PATCH 07/10] mention purity check in docstring for
 `maybeAssignsAccessedPropInBlock`

---
 javascript/ql/src/Declarations/DeadStoreOfProperty.ql | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index d7ddf6e906fe..291c279f96af 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -107,6 +107,9 @@ predicate isDeadAssignment(string name, DataFlow::PropWrite assign1, DataFlow::P
 /**
  * Holds if `assign` assigns a property that may be accessed somewhere else in the same block,
  * `after` indicates if the access happens before or after the node for `assign`.
+ *
+ * The access can either be a direct property access of the same name,
+ * or an impure expression where we assume that the expression can access the property.
  */
 predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean after) {
   (
@@ -116,6 +119,7 @@ predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean af
     after = false and postDominatedPropWrite(_, _, assign, false)
   ) and
   (
+    // direct property write before/after assign
     exists(ReachableBasicBlock block, int i, int j, Expr e, string name |
       i = getRank(block, assign.getWriteNode(), name) and
       j = getRank(block, e, name) and
@@ -126,6 +130,7 @@ predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean af
       after = false and j < i
     )
     or
+    // impure expression that might access the property before/after assign
     exists(ReachableBasicBlock block | assign.getWriteNode().getBasicBlock() = block |
       after = true and isBeforeImpure(assign, block)
       or

From 8f6721e0876836d52683d671be4b8cec84603c6f Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Tue, 11 Aug 2020 14:40:13 +0200
Subject: [PATCH 08/10] add explanation for purity-check in
 `getANodeAfterWrite`/`getANodeBeforeWrite` and move them into an internal
 module

---
 .../src/Declarations/DeadStoreOfProperty.ql   | 99 ++++++++++---------
 1 file changed, 54 insertions(+), 45 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index 291c279f96af..e609bf96c049 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -132,61 +132,70 @@ predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean af
     or
     // impure expression that might access the property before/after assign
     exists(ReachableBasicBlock block | assign.getWriteNode().getBasicBlock() = block |
-      after = true and isBeforeImpure(assign, block)
+      after = true and PurityCheck::isBeforeImpure(assign, block)
       or
-      after = false and isAfterImpure(assign, block)
+      after = false and PurityCheck::isAfterImpure(assign, block)
     )
   )
 }
 
 /**
- * Holds if a ControlFlowNode `c` is before an impure expression inside `bb`.
+ * Predicates to check if a property-write comes after/before an impure expression within the same basicblock.
  */
-predicate isBeforeImpure(DataFlow::PropWrite write, ReachableBasicBlock bb) {
-  getANodeAfterWrite(write, bb).(Expr).isImpure()
-}
+private module PurityCheck {
+  /**
+   * Holds if a ControlFlowNode `c` is before an impure expression inside `bb`.
+   */
+  predicate isBeforeImpure(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+    getANodeAfterWrite(write, bb).(Expr).isImpure()
+  }
 
-/**
- * Gets a ControlFlowNode that comes after `write` inside `bb`.
- * Stops after finding the first impure expression
- */
-ControlFlowNode getANodeAfterWrite(DataFlow::PropWrite write, ReachableBasicBlock bb) {
-  // base case
-  result.getBasicBlock() = bb and
-  postDominatedPropWrite(_, write, _, false) and // early pruning - manual magic
-  result = write.getWriteNode().getASuccessor()
-  or
-  // recursive case
-  exists(ControlFlowNode prev | prev = getANodeAfterWrite(write, bb) |
-    not result instanceof BasicBlock and
-    not prev.(Expr).isImpure() and
-    result = prev.getASuccessor()
-  )
-}
+  /**
+   * Gets a ControlFlowNode that comes after `write` inside `bb`.
+   * Stops after finding the first impure expression.
+   *
+   * This predicate is used as a helper to check if one of the successors to `write` inside `bb` is impure (see `isBeforeImpure`).
+   */
+  private ControlFlowNode getANodeAfterWrite(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+    // base case
+    result.getBasicBlock() = bb and
+    postDominatedPropWrite(_, write, _, false) and // early pruning - manual magic
+    result = write.getWriteNode().getASuccessor()
+    or
+    // recursive case
+    exists(ControlFlowNode prev | prev = getANodeAfterWrite(write, bb) |
+      not result instanceof BasicBlock and
+      not prev.(Expr).isImpure() and
+      result = prev.getASuccessor()
+    )
+  }
 
-/**
- * Holds if a ControlFlowNode `c` is after an impure expression inside `bb`.
- */
-predicate isAfterImpure(DataFlow::PropWrite write, ReachableBasicBlock bb) {
-  getANodeBeforeWrite(write, bb).(Expr).isImpure()
-}
+  /**
+   * Holds if a ControlFlowNode `c` is after an impure expression inside `bb`.
+   */
+  predicate isAfterImpure(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+    getANodeBeforeWrite(write, bb).(Expr).isImpure()
+  }
 
-/**
- * Gets a ControlFlowNode that comes before `write` inside `bb`.
- * Stops after finding the first impure expression.
- */
-ControlFlowNode getANodeBeforeWrite(DataFlow::PropWrite write, ReachableBasicBlock bb) {
-  // base case
-  result.getBasicBlock() = bb and
-  postDominatedPropWrite(_, _, write, false) and // early pruning - manual magic
-  result = write.getWriteNode().getAPredecessor()
-  or
-  // recursive case
-  exists(ControlFlowNode prev | prev = getANodeBeforeWrite(write, bb) |
-    not prev instanceof BasicBlock and
-    not prev.(Expr).isImpure() and
-    result = prev.getAPredecessor()
-  )
+  /**
+   * Gets a ControlFlowNode that comes before `write` inside `bb`.
+   * Stops after finding the first impure expression.
+   *
+   * This predicate is used as a helper to check if one of the predecessors to `write` inside `bb` is impure (see `isAfterImpure`).
+   */
+  private ControlFlowNode getANodeBeforeWrite(DataFlow::PropWrite write, ReachableBasicBlock bb) {
+    // base case
+    result.getBasicBlock() = bb and
+    postDominatedPropWrite(_, _, write, false) and // early pruning - manual magic
+    result = write.getWriteNode().getAPredecessor()
+    or
+    // recursive case
+    exists(ControlFlowNode prev | prev = getANodeBeforeWrite(write, bb) |
+      not prev instanceof BasicBlock and
+      not prev.(Expr).isImpure() and
+      result = prev.getAPredecessor()
+    )
+  }
 }
 
 /**

From 2974c4923f3bdb39ed67f9051cbd3ec20285cac3 Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Tue, 11 Aug 2020 14:43:25 +0200
Subject: [PATCH 09/10] introduce and use `isAPropertyWrite`

---
 .../src/Declarations/DeadStoreOfProperty.ql   | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index e609bf96c049..d864695e5659 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -61,12 +61,7 @@ predicate postDominatedPropWrite(
 int getRank(ReachableBasicBlock bb, ControlFlowNode ref, string name) {
   ref =
     rank[result](ControlFlowNode e |
-      exists(DataFlow::PropWrite write |
-        write.getPropertyName() = name and
-        e = write.getWriteNode() and
-        unambiguousPropWrite(write)
-      )
-      or
+      isAPropertyWrite(e, name) or
       isAPropertyRead(e, name)
     |
       e order by any(int i | e = bb.getNode(i))
@@ -80,6 +75,13 @@ predicate isAPropertyRead(Expr e, string name) {
   exists(DataFlow::PropRead read | read.asExpr() = e and read.getPropertyName() = name)
 }
 
+/**
+ * Holds if `e` is a property write of a property `name`.
+ */
+predicate isAPropertyWrite(ControlFlowNode e, string name) {
+  exists(DataFlow::PropWrite write | write.getWriteNode() = e and write.getPropertyName() = name) // TODO: umambi?
+}
+
 /**
  * Holds if `e` may access a property named `name`.
  */
@@ -218,12 +220,11 @@ ControlFlowNode getANodeWithNoPropAccessBetweenInsideBlock(string name, DataFlow
   // stop at reads of `name` and at impure expressions (except writes to `name`)
   not (
     maybeAccessesProperty(result, name) and
-    not result = any(DataFlow::PropWrite w | w.getPropertyName() = name).getWriteNode()
+    not isAPropertyWrite(result, name)
   ) and
   // stop at the first write to `name` that comes after `write`.
   (
-    not result.getAPredecessor() =
-      any(DataFlow::PropWrite w | w.getPropertyName() = name).getWriteNode()
+    not isAPropertyWrite(result.getAPredecessor(), name)
     or
     result.getAPredecessor() = write.getWriteNode()
   )

From a1394c363a9c4dc4e2f7f50bdd59a11074d1ab6b Mon Sep 17 00:00:00 2001
From: Erik Krogh Kristensen <erik-krogh@github.com>
Date: Tue, 11 Aug 2020 14:49:51 +0200
Subject: [PATCH 10/10] more consistent naming of predicates

---
 .../ql/src/Declarations/DeadStoreOfProperty.ql | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
index d864695e5659..834441dbe6d4 100644
--- a/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
+++ b/javascript/ql/src/Declarations/DeadStoreOfProperty.ql
@@ -98,14 +98,22 @@ predicate maybeAccessesProperty(Expr e, string name) {
  */
 predicate isDeadAssignment(string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2) {
   (
-    assign2.getWriteNode() = getANodeWithNoPropAccessBetweenInsideBlock(name, assign1) and
-    postDominatedPropWrite(name, assign1, assign2, true)
-    or
-    noPropAccessBetweenGlobal(name, assign1, assign2)
+    noPropAccessBetweenInsideBasicBlock(name, assign1, assign2) or
+    noPropAccessBetweenAcrossBasicBlocks(name, assign1, assign2)
   ) and
   not isDOMProperty(name)
 }
 
+/**
+ * Holds if `assign1` and `assign2` are in the same basicblock and both assign property `name`, and the assigned property is not accessed between the two assignments.
+ */
+predicate noPropAccessBetweenInsideBasicBlock(
+  string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2
+) {
+  assign2.getWriteNode() = getANodeWithNoPropAccessBetweenInsideBlock(name, assign1) and
+  postDominatedPropWrite(name, assign1, assign2, true)
+}
+
 /**
  * Holds if `assign` assigns a property that may be accessed somewhere else in the same block,
  * `after` indicates if the access happens before or after the node for `assign`.
@@ -234,7 +242,7 @@ ControlFlowNode getANodeWithNoPropAccessBetweenInsideBlock(string name, DataFlow
  * Holds if `assign1` and `assign2` are in different basicblocks and both assign property `name`, and the assigned property is not accessed between the two assignments.
  */
 pragma[nomagic]
-predicate noPropAccessBetweenGlobal(
+predicate noPropAccessBetweenAcrossBasicBlocks(
   string name, DataFlow::PropWrite assign1, DataFlow::PropWrite assign2
 ) {
   exists(