@@ -209,97 +209,99 @@ private module Cached {
209
209
* value-preserving steps, not taking call contexts into account.
210
210
*
211
211
* `contentIn` describes the content of `p` that can flow to `node`
212
- * (if any).
212
+ * (if any), `t2` is the type of the tracked value, and `t1` is the
213
+ * type before reading `contentIn` (`= t2` when no content is read).
213
214
*/
214
- predicate parameterValueFlow ( ParameterNode p , Node node , ContentOption contentIn ) {
215
- parameterValueFlow0 ( p , node , contentIn ) and
215
+ predicate parameterValueFlow (
216
+ ParameterNode p , Node node , ContentOption contentIn , DataFlowType t1 , DataFlowType t2
217
+ ) {
218
+ parameterValueFlow0 ( p , node , contentIn , t1 , t2 ) and
216
219
if node instanceof CastingNode
217
- then
218
- // normal flow through
219
- contentIn = TContentNone ( ) and
220
- compatibleTypes ( getErasedNodeTypeBound ( p ) , getErasedNodeTypeBound ( node ) )
221
- or
222
- // getter
223
- exists ( Content fIn |
224
- contentIn .getContent ( ) = fIn and
225
- compatibleTypes ( fIn .getType ( ) , getErasedNodeTypeBound ( node ) )
226
- )
220
+ then compatibleTypes ( t2 , getErasedNodeTypeBound ( node ) )
227
221
else any ( )
228
222
}
229
223
230
224
pragma [ nomagic]
231
- private predicate parameterValueFlow0 ( ParameterNode p , Node node , ContentOption contentIn ) {
225
+ private predicate parameterValueFlow0 (
226
+ ParameterNode p , Node node , ContentOption contentIn , DataFlowType t1 , DataFlowType t2
227
+ ) {
232
228
p = node and
233
229
Cand:: cand ( p , _) and
234
- contentIn = TContentNone ( )
230
+ contentIn = TContentNone ( ) and
231
+ t1 = getErasedNodeTypeBound ( p ) and
232
+ t2 = t1
235
233
or
236
234
// local flow
237
235
exists ( Node mid |
238
- parameterValueFlow ( p , mid , contentIn ) and
236
+ parameterValueFlow ( p , mid , contentIn , t1 , t2 ) and
239
237
LocalFlowBigStep:: localFlowBigStep ( mid , node )
240
238
)
241
239
or
242
240
// read
243
- exists ( Node mid , Content f |
244
- parameterValueFlow ( p , mid , TContentNone ( ) ) and
245
- readStep ( mid , f , node ) and
246
- contentIn .getContent ( ) = f and
241
+ exists ( Node mid |
242
+ parameterValueFlow ( p , mid , TContentNone ( ) , _, t1 ) and
243
+ readStep ( mid , contentIn .getContent ( ) , node ) and
247
244
Cand:: parameterValueFlowReturnCand ( p , _, true ) and
248
- compatibleTypes ( getErasedNodeTypeBound ( p ) , f .getContainerType ( ) )
245
+ compatibleTypes ( t1 , getErasedNodeTypeBound ( mid ) ) and
246
+ t2 = getErasedNodeTypeBound ( node )
249
247
)
250
248
or
251
249
// flow through: no prior read
252
- exists ( ArgumentNode arg |
253
- parameterValueFlowArg ( p , arg , TContentNone ( ) ) and
254
- argumentValueFlowsThrough ( arg , contentIn , node )
250
+ exists ( ArgumentNode arg , DataFlowType t0_ , DataFlowType t1_ , DataFlowType t2_ |
251
+ parameterValueFlowArg ( p , arg , TContentNone ( ) , _, t0_ ) and
252
+ argumentValueFlowsThrough ( arg , contentIn , node , t1_ , t2_ ) and
253
+ if contentIn = TContentNone ( )
254
+ then t1 = t0_ and t2 = t1
255
+ else (
256
+ t1 = t1_ and
257
+ t2 = t2_
258
+ )
255
259
)
256
260
or
257
261
// flow through: no read inside method
258
262
exists ( ArgumentNode arg |
259
- parameterValueFlowArg ( p , arg , contentIn ) and
260
- argumentValueFlowsThrough ( arg , TContentNone ( ) , node )
263
+ parameterValueFlowArg ( p , arg , contentIn , t1 , t2 ) and
264
+ argumentValueFlowsThrough ( arg , TContentNone ( ) , node , _ , _ )
261
265
)
262
266
}
263
267
264
268
pragma [ nomagic]
265
269
private predicate parameterValueFlowArg (
266
- ParameterNode p , ArgumentNode arg , ContentOption contentIn
270
+ ParameterNode p , ArgumentNode arg , ContentOption contentIn , DataFlowType t1 , DataFlowType t2
267
271
) {
268
- parameterValueFlow ( p , arg , contentIn ) and
272
+ parameterValueFlow ( p , arg , contentIn , t1 , t2 ) and
269
273
Cand:: argumentValueFlowsThroughCand ( arg , _, _)
270
274
}
271
275
272
276
pragma [ nomagic]
273
277
private predicate argumentValueFlowsThrough0 (
274
- DataFlowCall call , ArgumentNode arg , ReturnKind kind , ContentOption contentIn
278
+ DataFlowCall call , ArgumentNode arg , ReturnKind kind , ContentOption contentIn ,
279
+ DataFlowType t1 , DataFlowType t2
275
280
) {
276
281
exists ( ParameterNode param | viableParamArg ( call , param , arg ) |
277
- parameterValueFlowReturn ( param , kind , contentIn )
282
+ parameterValueFlowReturn ( param , kind , contentIn , t1 , t2 )
278
283
)
279
284
}
280
285
281
286
/**
282
287
* Holds if `arg` flows to `out` through a call using only value-preserving steps,
283
288
* not taking call contexts into account.
284
289
*
285
- * `contentIn` describes the content of `arg` that can flow to `out` (if any).
290
+ * `contentIn` describes the content of `arg` that can flow to `out` (if any),
291
+ * `t2` is the type of the tracked value, and `t1` is the type before reading
292
+ * `contentIn` (`= t2` when no content is read).
286
293
*/
287
294
pragma [ nomagic]
288
- predicate argumentValueFlowsThrough ( ArgumentNode arg , ContentOption contentIn , Node out ) {
295
+ predicate argumentValueFlowsThrough (
296
+ ArgumentNode arg , ContentOption contentIn , Node out , DataFlowType t1 , DataFlowType t2
297
+ ) {
289
298
exists ( DataFlowCall call , ReturnKind kind |
290
- argumentValueFlowsThrough0 ( call , arg , kind , contentIn ) and
291
- out = getAnOutNode ( call , kind )
292
- |
293
- // normal flow through
294
- contentIn = TContentNone ( ) and
295
- compatibleTypes ( getErasedNodeTypeBound ( arg ) , getErasedNodeTypeBound ( out ) )
296
- or
297
- // getter
298
- exists ( Content fIn |
299
- contentIn .getContent ( ) = fIn and
300
- compatibleTypes ( getErasedNodeTypeBound ( arg ) , fIn .getContainerType ( ) ) and
301
- compatibleTypes ( fIn .getType ( ) , getErasedNodeTypeBound ( out ) )
302
- )
299
+ argumentValueFlowsThrough0 ( call , arg , kind , contentIn , t1 , t2 ) and
300
+ out = getAnOutNode ( call , kind ) and
301
+ compatibleTypes ( t2 , getErasedNodeTypeBound ( out ) ) and
302
+ if contentIn = TContentNone ( )
303
+ then compatibleTypes ( getErasedNodeTypeBound ( arg ) , getErasedNodeTypeBound ( out ) )
304
+ else compatibleTypes ( getErasedNodeTypeBound ( arg ) , t1 )
303
305
)
304
306
}
305
307
@@ -308,13 +310,14 @@ private module Cached {
308
310
* callable using only value-preserving steps.
309
311
*
310
312
* `contentIn` describes the content of `p` that can flow to the return
311
- * node (if any).
313
+ * node (if any), `t2` is the type of the tracked value, and `t1` is the
314
+ * type before reading `contentIn` (`= t2` when no content is read).
312
315
*/
313
316
private predicate parameterValueFlowReturn (
314
- ParameterNode p , ReturnKind kind , ContentOption contentIn
317
+ ParameterNode p , ReturnKind kind , ContentOption contentIn , DataFlowType t1 , DataFlowType t2
315
318
) {
316
319
exists ( ReturnNode ret |
317
- parameterValueFlow ( p , ret , contentIn ) and
320
+ parameterValueFlow ( p , ret , contentIn , t1 , t2 ) and
318
321
kind = ret .getKind ( )
319
322
)
320
323
}
@@ -329,7 +332,23 @@ private module Cached {
329
332
*/
330
333
cached
331
334
predicate parameterValueFlowsToPreUpdate ( ParameterNode p , PostUpdateNode n ) {
332
- parameterValueFlow ( p , n .getPreUpdateNode ( ) , TContentNone ( ) )
335
+ parameterValueFlow ( p , n .getPreUpdateNode ( ) , TContentNone ( ) , _, _)
336
+ }
337
+
338
+ private predicate store ( Node node1 , Content c , Node node2 , DataFlowType containerType ) {
339
+ storeStep ( node1 , c , node2 ) and
340
+ readStep ( _, c , _) and
341
+ containerType = getErasedNodeTypeBound ( node2 )
342
+ or
343
+ exists ( Node n1 , Node n2 |
344
+ n1 = node1 .( PostUpdateNode ) .getPreUpdateNode ( ) and
345
+ n2 = node2 .( PostUpdateNode ) .getPreUpdateNode ( )
346
+ |
347
+ argumentValueFlowsThrough ( n2 , TContentSome ( c ) , n1 , containerType , _)
348
+ or
349
+ readStep ( n2 , c , n1 ) and
350
+ containerType = getErasedNodeTypeBound ( n2 )
351
+ )
333
352
}
334
353
335
354
/**
@@ -340,17 +359,8 @@ private module Cached {
340
359
* been stored into, in order to handle cases like `x.f1.f2 = y`.
341
360
*/
342
361
cached
343
- predicate store ( Node node1 , Content f , Node node2 ) {
344
- storeStep ( node1 , f , node2 ) and readStep ( _, f , _)
345
- or
346
- exists ( Node n1 , Node n2 |
347
- n1 = node1 .( PostUpdateNode ) .getPreUpdateNode ( ) and
348
- n2 = node2 .( PostUpdateNode ) .getPreUpdateNode ( )
349
- |
350
- argumentValueFlowsThrough ( n2 , TContentSome ( f ) , n1 )
351
- or
352
- readStep ( n2 , f , n1 )
353
- )
362
+ predicate store ( Node node1 , TypedContent tc , Node node2 ) {
363
+ store ( node1 , tc .getContent ( ) , node2 , tc .getContainerType ( ) )
354
364
}
355
365
356
366
import FlowThrough
@@ -397,10 +407,13 @@ private module Cached {
397
407
TBooleanNone ( ) or
398
408
TBooleanSome ( boolean b ) { b = true or b = false }
399
409
410
+ cached
411
+ newtype TTypedContent = MkTypedContent ( Content c , DataFlowType t ) { store ( _, c , _, t ) }
412
+
400
413
cached
401
414
newtype TAccessPathFront =
402
415
TFrontNil ( DataFlowType t ) or
403
- TFrontHead ( Content f )
416
+ TFrontHead ( TypedContent tc )
404
417
405
418
cached
406
419
newtype TAccessPathFrontOption =
@@ -415,13 +428,17 @@ class CastingNode extends Node {
415
428
CastingNode ( ) {
416
429
this instanceof ParameterNode or
417
430
this instanceof CastNode or
418
- this instanceof OutNodeExt
431
+ this instanceof OutNodeExt or
432
+ // For reads, `x.f`, we want to check that the tracked type after the read (which
433
+ // is obtained by popping the head of the access path stack) is compatible with
434
+ // the type of `x.f`.
435
+ readStep ( _, _, this )
419
436
}
420
437
}
421
438
422
439
newtype TContentOption =
423
440
TContentNone ( ) or
424
- TContentSome ( Content f )
441
+ TContentSome ( Content c )
425
442
426
443
private class ContentOption extends TContentOption {
427
444
Content getContent ( ) { this = TContentSome ( result ) }
@@ -692,6 +709,23 @@ class BooleanOption extends TBooleanOption {
692
709
}
693
710
}
694
711
712
+ /** Content tagged with the type of a containing object. */
713
+ class TypedContent extends MkTypedContent {
714
+ private Content c ;
715
+ private DataFlowType t ;
716
+
717
+ TypedContent ( ) { this = MkTypedContent ( c , t ) }
718
+
719
+ /** Gets the content. */
720
+ Content getContent ( ) { result = c }
721
+
722
+ /** Gets the container type. */
723
+ DataFlowType getContainerType ( ) { result = t }
724
+
725
+ /** Gets a textual representation of this content. */
726
+ string toString ( ) { result = c .toString ( ) }
727
+ }
728
+
695
729
/**
696
730
* The front of an access path. This is either a head or a nil.
697
731
*/
@@ -702,25 +736,29 @@ abstract class AccessPathFront extends TAccessPathFront {
702
736
703
737
abstract boolean toBoolNonEmpty ( ) ;
704
738
705
- predicate headUsesContent ( Content f ) { this = TFrontHead ( f ) }
739
+ predicate headUsesContent ( TypedContent tc ) { this = TFrontHead ( tc ) }
706
740
}
707
741
708
742
class AccessPathFrontNil extends AccessPathFront , TFrontNil {
709
- override string toString ( ) {
710
- exists ( DataFlowType t | this = TFrontNil ( t ) | result = ppReprType ( t ) )
711
- }
743
+ private DataFlowType t ;
712
744
713
- override DataFlowType getType ( ) { this = TFrontNil ( result ) }
745
+ AccessPathFrontNil ( ) { this = TFrontNil ( t ) }
746
+
747
+ override string toString ( ) { result = ppReprType ( t ) }
748
+
749
+ override DataFlowType getType ( ) { result = t }
714
750
715
751
override boolean toBoolNonEmpty ( ) { result = false }
716
752
}
717
753
718
754
class AccessPathFrontHead extends AccessPathFront , TFrontHead {
719
- override string toString ( ) { exists ( Content f | this = TFrontHead ( f ) | result = f . toString ( ) ) }
755
+ private TypedContent tc ;
720
756
721
- override DataFlowType getType ( ) {
722
- exists ( Content head | this = TFrontHead ( head ) | result = head .getContainerType ( ) )
723
- }
757
+ AccessPathFrontHead ( ) { this = TFrontHead ( tc ) }
758
+
759
+ override string toString ( ) { result = tc .toString ( ) }
760
+
761
+ override DataFlowType getType ( ) { result = tc .getContainerType ( ) }
724
762
725
763
override boolean toBoolNonEmpty ( ) { result = true }
726
764
}
0 commit comments