@@ -13,45 +13,66 @@ import Expressions.DOMProperties
1313import DeadStore
1414
1515/**
16- * Holds if `write` writes to property `name` of ` base` , and `base` is the only base object of `write`.
16+ * Holds if `write` writes to a property of a base, and there is only one base object of `write`.
1717 */
18- predicate unambiguousPropWrite ( DataFlow:: SourceNode base , string name , DataFlow:: PropWrite write ) {
19- write = base .getAPropertyWrite ( name ) and
20- not exists ( DataFlow:: SourceNode otherBase |
21- otherBase != base and
22- write = otherBase .getAPropertyWrite ( name )
18+ predicate unambiguousPropWrite ( DataFlow:: PropWrite write ) {
19+ exists ( DataFlow:: SourceNode base , string name |
20+ write = base .getAPropertyWrite ( name ) and
21+ not exists ( DataFlow:: SourceNode otherBase |
22+ otherBase != base and
23+ write = otherBase .getAPropertyWrite ( name )
24+ )
2325 )
2426}
2527
2628/**
2729 * Holds if `assign1` and `assign2` both assign property `name` of the same object, and `assign2` post-dominates `assign1`.
2830 */
2931predicate postDominatedPropWrite (
30- string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2
32+ string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2 , boolean local
3133) {
34+ exists ( DataFlow:: SourceNode base |
35+ assign1 = base .getAPropertyWrite ( name ) and
36+ assign2 = base .getAPropertyWrite ( name )
37+ ) and
3238 exists (
33- ControlFlowNode write1 , ControlFlowNode write2 , DataFlow :: SourceNode base ,
34- ReachableBasicBlock block1 , ReachableBasicBlock block2
39+ ControlFlowNode write1 , ControlFlowNode write2 , ReachableBasicBlock block1 ,
40+ ReachableBasicBlock block2
3541 |
3642 write1 = assign1 .getWriteNode ( ) and
3743 write2 = assign2 .getWriteNode ( ) and
3844 block1 = write1 .getBasicBlock ( ) and
3945 block2 = write2 .getBasicBlock ( ) and
40- unambiguousPropWrite ( base , name , assign1 ) and
41- unambiguousPropWrite ( base , name , assign2 ) and
42- block2 .postDominates ( block1 ) and
46+ unambiguousPropWrite ( assign1 ) and
47+ unambiguousPropWrite ( assign2 ) and
4348 (
44- block1 = block2
45- implies
46- exists ( int i1 , int i2 |
47- write1 = block1 .getNode ( i1 ) and
48- write2 = block2 .getNode ( i2 ) and
49- i1 < i2
50- )
49+ block2 .strictlyPostDominates ( block1 ) and local = false
50+ or
51+ block1 = block2 and
52+ local = true and
53+ getRank ( block1 , write1 , name ) < getRank ( block2 , write2 , name )
5154 )
5255 )
5356}
5457
58+ /**
59+ * Gets the rank for the read/write `ref` of a property `name` inside basicblock `bb`.
60+ */
61+ int getRank ( ReachableBasicBlock bb , ControlFlowNode ref , string name ) {
62+ ref =
63+ rank [ result ] ( ControlFlowNode e |
64+ exists ( DataFlow:: PropWrite write |
65+ write .getPropertyName ( ) = name and
66+ e = write .getWriteNode ( ) and
67+ unambiguousPropWrite ( write )
68+ )
69+ or
70+ e .( PropAccess ) .getPropertyName ( ) = name and e instanceof RValue
71+ |
72+ e order by any ( int i | e = bb .getNode ( i ) )
73+ )
74+ }
75+
5576/**
5677 * Holds if `e` may access a property named `name`.
5778 */
@@ -67,67 +88,182 @@ predicate maybeAccessesProperty(Expr e, string name) {
6788 * Holds if `assign1` and `assign2` both assign property `name`, but `assign1` is dead because of `assign2`.
6889 */
6990predicate isDeadAssignment ( string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2 ) {
70- postDominatedPropWrite ( name , assign1 , assign2 ) and
71- noPropAccessBetween ( name , assign1 , assign2 ) and
91+ (
92+ noPropAccessBetweenLocal ( name , assign1 , assign2 )
93+ or
94+ noPropAccessBetweenGlobal ( name , assign1 , assign2 )
95+ ) and
7296 not isDOMProperty ( name )
7397}
7498
7599/**
76100 * Holds if `assign` assigns a property `name` that may be accessed somewhere else in the same block,
77101 * `after` indicates if the access happens before or after the node for `assign`.
78102 */
79- bindingset [ name]
80- predicate maybeAccessesAssignedPropInBlock ( string name , DataFlow:: PropWrite assign , boolean after ) {
81- exists ( ReachableBasicBlock block , int i , int j , Expr e |
82- assign .getWriteNode ( ) = block .getNode ( i ) and
83- e = block .getNode ( j ) and
84- maybeAccessesProperty ( e , name )
103+ predicate maybeAccessesAssignedPropInBlock ( DataFlow:: PropWrite assign , boolean after ) {
104+ (
105+ // early pruning - manual magic
106+ after = true and postDominatedPropWrite ( _, assign , _, false )
107+ or
108+ after = false and postDominatedPropWrite ( _, _, assign , false )
109+ ) and
110+ exists ( ReachableBasicBlock block , int i , int j , Expr e , string name |
111+ i = getRank ( block , assign .getWriteNode ( ) , name ) and
112+ j = getRank ( block , e , name ) and
113+ e instanceof PropAccess and
114+ e instanceof RValue
85115 |
86116 after = true and i < j
87117 or
88118 after = false and j < i
89119 )
120+ or
121+ exists ( ReachableBasicBlock block | assign .getWriteNode ( ) .getBasicBlock ( ) = block |
122+ after = true and isBeforeImpure ( assign , block )
123+ or
124+ after = false and isAfterImpure ( assign , block )
125+ )
90126}
91127
92128/**
93- * Holds if `assign1` and `assign2` both assign property `name`, and the assigned property is not accessed between the two assignments .
129+ * Holds if a ControlFlowNode `c` is before an impure expression inside `bb` .
94130 */
95- bindingset [ name]
96- predicate noPropAccessBetween ( string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2 ) {
131+ predicate isBeforeImpure ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
132+ getANodeAfterWrite ( write , bb ) .( Expr ) .isImpure ( )
133+ }
134+
135+ /**
136+ * Gets a ControlFlowNode that comes after `write` inside `bb`.
137+ * Stops after finding the first impure expression
138+ */
139+ ControlFlowNode getANodeAfterWrite ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
140+ // base case
141+ result .getBasicBlock ( ) = bb and
142+ postDominatedPropWrite ( _, write , _, false ) and // early pruning - manual magic
143+ result = write .getWriteNode ( ) .getASuccessor ( )
144+ or
145+ // recursive case
146+ exists ( ControlFlowNode prev | prev = getANodeAfterWrite ( write , bb ) |
147+ not result instanceof BasicBlock and
148+ not prev .( Expr ) .isImpure ( ) and
149+ result = prev .getASuccessor ( )
150+ )
151+ }
152+
153+ /**
154+ * Holds if a ControlFlowNode `c` is after an impure expression inside `bb`.
155+ */
156+ predicate isAfterImpure ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
157+ getANodeBeforeWrite ( write , bb ) .( Expr ) .isImpure ( )
158+ }
159+
160+ /**
161+ * Gets a ControlFlowNode that comes before `write` inside `bb`.
162+ * Stops after finding the first impure expression.
163+ */
164+ ControlFlowNode getANodeBeforeWrite ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
165+ // base case
166+ result .getBasicBlock ( ) = bb and
167+ postDominatedPropWrite ( _, _, write , false ) and // early pruning - manual magic
168+ result = write .getWriteNode ( ) .getAPredecessor ( )
169+ or
170+ // recursive case
171+ exists ( ControlFlowNode prev | prev = getANodeBeforeWrite ( write , bb ) |
172+ not prev instanceof BasicBlock and
173+ not prev .( Expr ) .isImpure ( ) and
174+ result = prev .getAPredecessor ( )
175+ )
176+ }
177+
178+ /**
179+ * Gets a successor inside `bb` in the control-flow graph that does not pass through an impure expression (except for writes to `name`).
180+ * Stops after the first write to `name` that happens after `node`.
181+ */
182+ ControlFlowNode getAPureSuccessor ( ControlFlowNode node ) {
183+ // stop at impure expressions (except writes to `name`)
184+ not (
185+ maybeAccessesProperty ( result , getPropertyWriteName ( node ) ) and
186+ not result =
187+ any ( DataFlow:: PropWrite write | write .getPropertyName ( ) = getPropertyWriteName ( node ) )
188+ .getWriteNode ( )
189+ ) and
190+ (
191+ // base case.
192+ exists ( DataFlow:: PropWrite write |
193+ node = write .getWriteNode ( ) and
194+ result = node .getASuccessor ( ) and
195+ // cheap check that there might exist a result we are interrested in,
196+ postDominatedPropWrite ( _, write , _, true )
197+ )
198+ or
199+ // recursive case
200+ exists ( ControlFlowNode pred | pred = getAPureSuccessor ( node ) | result = pred .getASuccessor ( ) ) and
201+ // stop at basic-block boundaries
202+ not result instanceof BasicBlock and
203+ // make sure we stop after the first write to `name` that comes after `node`.
204+ (
205+ not result .getAPredecessor ( ) =
206+ any ( DataFlow:: PropWrite write | write .getPropertyName ( ) = getPropertyWriteName ( node ) )
207+ .getWriteNode ( )
208+ or
209+ result .getAPredecessor ( ) = node
210+ )
211+ )
212+ }
213+
214+ /**
215+ * Gets the property name that is written to by the control-flow-node `writeNode`.
216+ */
217+ private string getPropertyWriteName ( ControlFlowNode writeNode ) {
218+ exists ( DataFlow:: PropWrite write |
219+ write .getWriteNode ( ) = writeNode and result = write .getPropertyName ( )
220+ )
221+ }
222+
223+ /**
224+ * 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.
225+ */
226+ predicate noPropAccessBetweenLocal (
227+ string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2
228+ ) {
229+ exists ( ControlFlowNode write1 , ControlFlowNode write2 |
230+ postDominatedPropWrite ( name , assign1 , assign2 , true ) and
231+ write1 = assign1 .getWriteNode ( ) and
232+ write2 = assign2 .getWriteNode ( ) and
233+ getRank ( _, write1 , name ) < getRank ( _, write2 , name ) and
234+ write2 = getAPureSuccessor ( write1 )
235+ )
236+ }
237+
238+ /**
239+ * 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.
240+ *
241+ * Much of this predicate is copy-pasted from `noPropAccessBetweenLocal`, but the predicates are separate to avoid join-order issues.
242+ */
243+ pragma [ nomagic]
244+ predicate noPropAccessBetweenGlobal (
245+ string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2
246+ ) {
97247 exists (
98248 ControlFlowNode write1 , ControlFlowNode write2 , ReachableBasicBlock block1 ,
99249 ReachableBasicBlock block2
100250 |
251+ postDominatedPropWrite ( name , assign1 , assign2 , false ) and // early pruning
101252 write1 = assign1 .getWriteNode ( ) and
253+ not maybeAccessesAssignedPropInBlock ( assign1 , true ) and
102254 write2 = assign2 .getWriteNode ( ) and
255+ not maybeAccessesAssignedPropInBlock ( assign2 , false ) and
103256 write1 .getBasicBlock ( ) = block1 and
104257 write2 .getBasicBlock ( ) = block2 and
105- if block1 = block2
106- then
107- // same block: check for access between
108- not exists ( int i1 , Expr mid , int i2 |
109- write1 = block1 .getNode ( i1 ) and
110- write2 = block2 .getNode ( i2 ) and
111- mid = block1 .getNode ( [ i1 + 1 .. i2 - 1 ] ) and
112- maybeAccessesProperty ( mid , name )
113- )
114- else
115- // other block:
116- not (
117- // check for an access after the first write node
118- maybeAccessesAssignedPropInBlock ( name , assign1 , true )
119- or
120- // check for an access between the two write blocks
121- exists ( ReachableBasicBlock mid |
122- block1 .getASuccessor + ( ) = mid and
123- mid .getASuccessor + ( ) = block2
124- |
125- maybeAccessesProperty ( mid .getANode ( ) , name )
126- )
127- or
128- // check for an access before the second write node
129- maybeAccessesAssignedPropInBlock ( name , assign2 , false )
130- )
258+ not block1 = block2 and
259+ // other block:
260+ // check for an access between the two write blocks
261+ not exists ( ReachableBasicBlock mid |
262+ block1 .getASuccessor + ( ) = mid and
263+ mid .getASuccessor + ( ) = block2
264+ |
265+ maybeAccessesProperty ( mid .getANode ( ) , name )
266+ )
131267 )
132268}
133269
0 commit comments