@@ -13,51 +13,81 @@ 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+ isAPropertyWrite ( e , name ) or
65+ isAPropertyRead ( e , name )
66+ |
67+ e order by any ( int i | e = bb .getNode ( i ) )
68+ )
69+ }
70+
71+ /**
72+ * Holds if `e` is a property read of a property `name`.
73+ */
74+ predicate isAPropertyRead ( Expr e , string name ) {
75+ exists ( DataFlow:: PropRead read | read .asExpr ( ) = e and read .getPropertyName ( ) = name )
76+ }
77+
78+ /**
79+ * Holds if `e` is a property write of a property `name`.
80+ */
81+ predicate isAPropertyWrite ( ControlFlowNode e , string name ) {
82+ exists ( DataFlow:: PropWrite write | write .getWriteNode ( ) = e and write .getPropertyName ( ) = name ) // TODO: umambi?
83+ }
84+
5585/**
5686 * Holds if `e` may access a property named `name`.
5787 */
5888bindingset [ name]
5989predicate maybeAccessesProperty ( Expr e , string name ) {
60- e . ( PropAccess ) . getPropertyName ( ) = name and e instanceof RValue
90+ isAPropertyRead ( e , name )
6191 or
6292 // conservatively reject all side-effects
6393 e .isImpure ( )
@@ -67,67 +97,173 @@ predicate maybeAccessesProperty(Expr e, string name) {
6797 * Holds if `assign1` and `assign2` both assign property `name`, but `assign1` is dead because of `assign2`.
6898 */
6999predicate isDeadAssignment ( string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2 ) {
70- postDominatedPropWrite ( name , assign1 , assign2 ) and
71- noPropAccessBetween ( name , assign1 , assign2 ) and
100+ (
101+ noPropAccessBetweenInsideBasicBlock ( name , assign1 , assign2 ) or
102+ noPropAccessBetweenAcrossBasicBlocks ( name , assign1 , assign2 )
103+ ) and
72104 not isDOMProperty ( name )
73105}
74106
75107/**
76- * Holds if `assign` assigns a property `name` that may be accessed somewhere else in the same block,
108+ * 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.
109+ */
110+ predicate noPropAccessBetweenInsideBasicBlock (
111+ string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2
112+ ) {
113+ assign2 .getWriteNode ( ) = getANodeWithNoPropAccessBetweenInsideBlock ( name , assign1 ) and
114+ postDominatedPropWrite ( name , assign1 , assign2 , true )
115+ }
116+
117+ /**
118+ * Holds if `assign` assigns a property that may be accessed somewhere else in the same block,
77119 * `after` indicates if the access happens before or after the node for `assign`.
120+ *
121+ * The access can either be a direct property access of the same name,
122+ * or an impure expression where we assume that the expression can access the property.
78123 */
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 )
85- |
86- after = true and i < j
124+ predicate maybeAssignsAccessedPropInBlock ( DataFlow:: PropWrite assign , boolean after ) {
125+ (
126+ // early pruning - manual magic
127+ after = true and postDominatedPropWrite ( _, assign , _, false )
87128 or
88- after = false and j < i
129+ after = false and postDominatedPropWrite ( _, _, assign , false )
130+ ) and
131+ (
132+ // direct property write before/after assign
133+ exists ( ReachableBasicBlock block , int i , int j , Expr e , string name |
134+ i = getRank ( block , assign .getWriteNode ( ) , name ) and
135+ j = getRank ( block , e , name ) and
136+ isAPropertyRead ( e , name )
137+ |
138+ after = true and i < j
139+ or
140+ after = false and j < i
141+ )
142+ or
143+ // impure expression that might access the property before/after assign
144+ exists ( ReachableBasicBlock block | assign .getWriteNode ( ) .getBasicBlock ( ) = block |
145+ after = true and PurityCheck:: isBeforeImpure ( assign , block )
146+ or
147+ after = false and PurityCheck:: isAfterImpure ( assign , block )
148+ )
89149 )
90150}
91151
92152/**
93- * Holds if `assign1` and `assign2` both assign property `name`, and the assigned property is not accessed between the two assignments .
153+ * Predicates to check if a property-write comes after/before an impure expression within the same basicblock .
94154 */
95- bindingset [ name]
96- predicate noPropAccessBetween ( string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2 ) {
155+ private module PurityCheck {
156+ /**
157+ * Holds if a ControlFlowNode `c` is before an impure expression inside `bb`.
158+ */
159+ predicate isBeforeImpure ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
160+ getANodeAfterWrite ( write , bb ) .( Expr ) .isImpure ( )
161+ }
162+
163+ /**
164+ * Gets a ControlFlowNode that comes after `write` inside `bb`.
165+ * Stops after finding the first impure expression.
166+ *
167+ * This predicate is used as a helper to check if one of the successors to `write` inside `bb` is impure (see `isBeforeImpure`).
168+ */
169+ private ControlFlowNode getANodeAfterWrite ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
170+ // base case
171+ result .getBasicBlock ( ) = bb and
172+ postDominatedPropWrite ( _, write , _, false ) and // early pruning - manual magic
173+ result = write .getWriteNode ( ) .getASuccessor ( )
174+ or
175+ // recursive case
176+ exists ( ControlFlowNode prev | prev = getANodeAfterWrite ( write , bb ) |
177+ not result instanceof BasicBlock and
178+ not prev .( Expr ) .isImpure ( ) and
179+ result = prev .getASuccessor ( )
180+ )
181+ }
182+
183+ /**
184+ * Holds if a ControlFlowNode `c` is after an impure expression inside `bb`.
185+ */
186+ predicate isAfterImpure ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
187+ getANodeBeforeWrite ( write , bb ) .( Expr ) .isImpure ( )
188+ }
189+
190+ /**
191+ * Gets a ControlFlowNode that comes before `write` inside `bb`.
192+ * Stops after finding the first impure expression.
193+ *
194+ * This predicate is used as a helper to check if one of the predecessors to `write` inside `bb` is impure (see `isAfterImpure`).
195+ */
196+ private ControlFlowNode getANodeBeforeWrite ( DataFlow:: PropWrite write , ReachableBasicBlock bb ) {
197+ // base case
198+ result .getBasicBlock ( ) = bb and
199+ postDominatedPropWrite ( _, _, write , false ) and // early pruning - manual magic
200+ result = write .getWriteNode ( ) .getAPredecessor ( )
201+ or
202+ // recursive case
203+ exists ( ControlFlowNode prev | prev = getANodeBeforeWrite ( write , bb ) |
204+ not prev instanceof BasicBlock and
205+ not prev .( Expr ) .isImpure ( ) and
206+ result = prev .getAPredecessor ( )
207+ )
208+ }
209+ }
210+
211+ /**
212+ * 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`.
213+ *
214+ * The predicate is computed recursively by computing transitive successors of `write` while removing the successors that could access `name`.
215+ * Stops at the first write to `name` that occours after `write`.
216+ */
217+ ControlFlowNode getANodeWithNoPropAccessBetweenInsideBlock ( string name , DataFlow:: PropWrite write ) {
218+ (
219+ // base case.
220+ result = write .getWriteNode ( ) .getASuccessor ( ) and
221+ postDominatedPropWrite ( name , write , _, true ) // manual magic - cheap check that there might exist a result we are interrested in,
222+ or
223+ // recursive case
224+ result = getANodeWithNoPropAccessBetweenInsideBlock ( name , write ) .getASuccessor ( )
225+ ) and
226+ // stop at basic-block boundaries
227+ not result instanceof BasicBlock and
228+ // stop at reads of `name` and at impure expressions (except writes to `name`)
229+ not (
230+ maybeAccessesProperty ( result , name ) and
231+ not isAPropertyWrite ( result , name )
232+ ) and
233+ // stop at the first write to `name` that comes after `write`.
234+ (
235+ not isAPropertyWrite ( result .getAPredecessor ( ) , name )
236+ or
237+ result .getAPredecessor ( ) = write .getWriteNode ( )
238+ )
239+ }
240+
241+ /**
242+ * 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.
243+ */
244+ pragma [ nomagic]
245+ predicate noPropAccessBetweenAcrossBasicBlocks (
246+ string name , DataFlow:: PropWrite assign1 , DataFlow:: PropWrite assign2
247+ ) {
97248 exists (
98249 ControlFlowNode write1 , ControlFlowNode write2 , ReachableBasicBlock block1 ,
99250 ReachableBasicBlock block2
100251 |
252+ postDominatedPropWrite ( name , assign1 , assign2 , false ) and // manual magic - early pruning
101253 write1 = assign1 .getWriteNode ( ) and
254+ not maybeAssignsAccessedPropInBlock ( assign1 , true ) and
102255 write2 = assign2 .getWriteNode ( ) and
256+ not maybeAssignsAccessedPropInBlock ( assign2 , false ) and
103257 write1 .getBasicBlock ( ) = block1 and
104258 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- )
259+ not block1 = block2 and
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