@@ -67,18 +67,25 @@ int getRank(ReachableBasicBlock bb, ControlFlowNode ref, string name) {
6767 unambiguousPropWrite ( write )
6868 )
6969 or
70- e . ( PropAccess ) . getPropertyName ( ) = name and e instanceof RValue
70+ isAPropertyRead ( e , name )
7171 |
7272 e order by any ( int i | e = bb .getNode ( i ) )
7373 )
7474}
7575
76+ /**
77+ * Holds if `e` is a property read of a property `name`.
78+ */
79+ predicate isAPropertyRead ( Expr e , string name ) {
80+ exists ( DataFlow:: PropRead read | read .asExpr ( ) = e and read .getPropertyName ( ) = name )
81+ }
82+
7683/**
7784 * Holds if `e` may access a property named `name`.
7885 */
7986bindingset [ name]
8087predicate maybeAccessesProperty ( Expr e , string name ) {
81- e . ( PropAccess ) . getPropertyName ( ) = name and e instanceof RValue
88+ isAPropertyRead ( e , name )
8289 or
8390 // conservatively reject all side-effects
8491 e .isImpure ( )
@@ -89,7 +96,8 @@ predicate maybeAccessesProperty(Expr e, string name) {
8996 */
9097predicate isDeadAssignment ( string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2 ) {
9198 (
92- noPropAccessBetweenLocal ( name , assign1 , assign2 )
99+ assign2 .getWriteNode ( ) = getANodeWithNoPropAccessBetweenInsideBlock ( name , assign1 ) and
100+ postDominatedPropWrite ( name , assign1 , assign2 , true )
93101 or
94102 noPropAccessBetweenGlobal ( name , assign1 , assign2 )
95103 ) and
@@ -110,8 +118,7 @@ predicate maybeAssignsAccessedPropInBlock(DataFlow::PropWrite assign, boolean af
110118 exists ( ReachableBasicBlock block , int i , int j , Expr e , string name |
111119 i = getRank ( block , assign .getWriteNode ( ) , name ) and
112120 j = getRank ( block , e , name ) and
113- e instanceof PropAccess and
114- e instanceof RValue
121+ isAPropertyRead ( e , name )
115122 |
116123 after = true and i < j
117124 or
@@ -176,71 +183,38 @@ ControlFlowNode getANodeBeforeWrite(DataFlow::PropWrite write, ReachableBasicBlo
176183}
177184
178185/**
179- * 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) .
180- * Stops after the first write to same property that happens after `node`.
181- *
182- * `node` always corresponds to the CFG node of a `DataFlow::PropWrite` with a known name .
186+ * 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` .
187+ *
188+ * The predicate is computed recursively by computing transitive successors of `write` while removing the successors that could access `name`.
189+ * Stops at the first write to `name` that occours after `write` .
183190 */
184- ControlFlowNode getAPureSuccessor ( ControlFlowNode node ) {
191+ ControlFlowNode getANodeWithNoPropAccessBetweenInsideBlock ( string name , DataFlow:: PropWrite write ) {
192+ (
193+ // base case.
194+ result = write .getWriteNode ( ) .getASuccessor ( ) and
195+ postDominatedPropWrite ( name , write , _, true ) // manual magic - cheap check that there might exist a result we are interrested in,
196+ or
197+ // recursive case
198+ result = getANodeWithNoPropAccessBetweenInsideBlock ( name , write ) .getASuccessor ( )
199+ ) and
200+ // stop at basic-block boundaries
201+ not result instanceof BasicBlock and
185202 // stop at reads of `name` and at impure expressions (except writes to `name`)
186203 not (
187- maybeAccessesProperty ( result , getPropertyWriteName ( node ) ) and
188- not result =
189- any ( DataFlow:: PropWrite write | write .getPropertyName ( ) = getPropertyWriteName ( node ) )
190- .getWriteNode ( )
204+ maybeAccessesProperty ( result , name ) and
205+ not result = any ( DataFlow:: PropWrite w | w .getPropertyName ( ) = name ) .getWriteNode ( )
191206 ) and
207+ // stop at the first write to `name` that comes after `write`.
192208 (
193- // base case.
194- exists ( DataFlow:: PropWrite write |
195- node = write .getWriteNode ( ) and
196- result = node .getASuccessor ( ) and
197- // cheap check that there might exist a result we are interrested in,
198- postDominatedPropWrite ( _, write , _, true )
199- )
209+ not result .getAPredecessor ( ) =
210+ any ( DataFlow:: PropWrite w | w .getPropertyName ( ) = name ) .getWriteNode ( )
200211 or
201- // recursive case
202- result = getAPureSuccessor ( node ) .getASuccessor ( ) and
203- // stop at basic-block boundaries
204- not result instanceof BasicBlock and
205- // make sure we stop after the first write to the same property that comes after `node`.
206- (
207- not result .getAPredecessor ( ) =
208- any ( DataFlow:: PropWrite write | write .getPropertyName ( ) = getPropertyWriteName ( node ) )
209- .getWriteNode ( )
210- or
211- result .getAPredecessor ( ) = node
212- )
213- )
214- }
215-
216- /**
217- * Gets the property name that is written to by the control-flow-node `writeNode`.
218- */
219- private string getPropertyWriteName ( ControlFlowNode writeNode ) {
220- exists ( DataFlow:: PropWrite write |
221- write .getWriteNode ( ) = writeNode and result = write .getPropertyName ( )
222- )
223- }
224-
225- /**
226- * 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.
227- */
228- predicate noPropAccessBetweenLocal (
229- string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2
230- ) {
231- exists ( ControlFlowNode write1 , ControlFlowNode write2 |
232- postDominatedPropWrite ( name , assign1 , assign2 , true ) and
233- write1 = assign1 .getWriteNode ( ) and
234- write2 = assign2 .getWriteNode ( ) and
235- getRank ( _, write1 , name ) < getRank ( _, write2 , name ) and
236- write2 = getAPureSuccessor ( write1 )
212+ result .getAPredecessor ( ) = write .getWriteNode ( )
237213 )
238214}
239215
240216/**
241217 * 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.
242- *
243- * Much of this predicate is copy-pasted from `noPropAccessBetweenLocal`, but the predicates are separate to avoid join-order issues.
244218 */
245219pragma [ nomagic]
246220predicate noPropAccessBetweenGlobal (
@@ -250,15 +224,14 @@ predicate noPropAccessBetweenGlobal(
250224 ControlFlowNode write1 , ControlFlowNode write2 , ReachableBasicBlock block1 ,
251225 ReachableBasicBlock block2
252226 |
253- postDominatedPropWrite ( name , assign1 , assign2 , false ) and // early pruning
227+ postDominatedPropWrite ( name , assign1 , assign2 , false ) and // manual magic - early pruning
254228 write1 = assign1 .getWriteNode ( ) and
255229 not maybeAssignsAccessedPropInBlock ( assign1 , true ) and
256230 write2 = assign2 .getWriteNode ( ) and
257231 not maybeAssignsAccessedPropInBlock ( assign2 , false ) and
258232 write1 .getBasicBlock ( ) = block1 and
259233 write2 .getBasicBlock ( ) = block2 and
260234 not block1 = block2 and
261- // other block:
262235 // check for an access between the two write blocks
263236 not exists ( ReachableBasicBlock mid |
264237 block1 .getASuccessor + ( ) = mid and
0 commit comments