@@ -198,123 +198,130 @@ private module Cached {
198
198
/**
199
199
* The final flow-through calculation:
200
200
*
201
- * - Input access paths are abstracted with a `ContentOption` parameter
202
- * that represents the head of the access path. `TContentNone()` means that
203
- * the access path is unrestricted .
201
+ * - Calculated flow is either value-preserving (`read = TReadStepTypesNone()`)
202
+ * or summarized as a single read step with before and after types recorded
203
+ * in the `ReadStepTypesOption` parameter .
204
204
* - Types are checked using the `compatibleTypes()` relation.
205
205
*/
206
206
private module Final {
207
207
/**
208
208
* Holds if `p` can flow to `node` in the same callable using only
209
- * value-preserving steps, not taking call contexts into account.
209
+ * value-preserving steps and possibly a single read step, not taking
210
+ * call contexts into account.
210
211
*
211
- * `contentIn` describes the content of `p` that can flow to `node`
212
- * (if any) .
212
+ * If a read step was taken, then `read` captures the `Content`, the
213
+ * container type, and the content type .
213
214
*/
214
- predicate parameterValueFlow ( ParameterNode p , Node node , ContentOption contentIn ) {
215
- parameterValueFlow0 ( p , node , contentIn ) and
215
+ predicate parameterValueFlow ( ParameterNode p , Node node , ReadStepTypesOption read ) {
216
+ parameterValueFlow0 ( p , node , read ) and
216
217
if node instanceof CastingNode
217
218
then
218
219
// normal flow through
219
- contentIn = TContentNone ( ) and
220
+ read = TReadStepTypesNone ( ) and
220
221
compatibleTypes ( getErasedNodeTypeBound ( p ) , getErasedNodeTypeBound ( node ) )
221
222
or
222
223
// getter
223
- exists ( Content fIn |
224
- contentIn .getContent ( ) = fIn and
225
- compatibleTypes ( fIn .getType ( ) , getErasedNodeTypeBound ( node ) )
226
- )
224
+ compatibleTypes ( read .getContentType ( ) , getErasedNodeTypeBound ( node ) )
227
225
else any ( )
228
226
}
229
227
230
228
pragma [ nomagic]
231
- private predicate parameterValueFlow0 ( ParameterNode p , Node node , ContentOption contentIn ) {
229
+ private predicate parameterValueFlow0 ( ParameterNode p , Node node , ReadStepTypesOption read ) {
232
230
p = node and
233
231
Cand:: cand ( p , _) and
234
- contentIn = TContentNone ( )
232
+ read = TReadStepTypesNone ( )
235
233
or
236
234
// local flow
237
235
exists ( Node mid |
238
- parameterValueFlow ( p , mid , contentIn ) and
236
+ parameterValueFlow ( p , mid , read ) 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 , TReadStepTypesNone ( ) ) and
243
+ readStepWithTypes ( mid , read . getContainerType ( ) , read . getContent ( ) , node ,
244
+ read . getContentType ( ) ) and
247
245
Cand:: parameterValueFlowReturnCand ( p , _, true ) and
248
- compatibleTypes ( getErasedNodeTypeBound ( p ) , f .getContainerType ( ) )
246
+ compatibleTypes ( getErasedNodeTypeBound ( p ) , read .getContainerType ( ) )
249
247
)
250
248
or
251
249
// flow through: no prior read
252
250
exists ( ArgumentNode arg |
253
- parameterValueFlowArg ( p , arg , TContentNone ( ) ) and
254
- argumentValueFlowsThrough ( arg , contentIn , node )
251
+ parameterValueFlowArg ( p , arg , TReadStepTypesNone ( ) ) and
252
+ argumentValueFlowsThrough ( arg , read , node )
255
253
)
256
254
or
257
255
// flow through: no read inside method
258
256
exists ( ArgumentNode arg |
259
- parameterValueFlowArg ( p , arg , contentIn ) and
260
- argumentValueFlowsThrough ( arg , TContentNone ( ) , node )
257
+ parameterValueFlowArg ( p , arg , read ) and
258
+ argumentValueFlowsThrough ( arg , TReadStepTypesNone ( ) , node )
261
259
)
262
260
}
263
261
264
262
pragma [ nomagic]
265
263
private predicate parameterValueFlowArg (
266
- ParameterNode p , ArgumentNode arg , ContentOption contentIn
264
+ ParameterNode p , ArgumentNode arg , ReadStepTypesOption read
267
265
) {
268
- parameterValueFlow ( p , arg , contentIn ) and
266
+ parameterValueFlow ( p , arg , read ) and
269
267
Cand:: argumentValueFlowsThroughCand ( arg , _, _)
270
268
}
271
269
272
270
pragma [ nomagic]
273
271
private predicate argumentValueFlowsThrough0 (
274
- DataFlowCall call , ArgumentNode arg , ReturnKind kind , ContentOption contentIn
272
+ DataFlowCall call , ArgumentNode arg , ReturnKind kind , ReadStepTypesOption read
275
273
) {
276
274
exists ( ParameterNode param | viableParamArg ( call , param , arg ) |
277
- parameterValueFlowReturn ( param , kind , contentIn )
275
+ parameterValueFlowReturn ( param , kind , read )
278
276
)
279
277
}
280
278
281
279
/**
282
- * Holds if `arg` flows to `out` through a call using only value-preserving steps,
283
- * not taking call contexts into account.
280
+ * Holds if `arg` flows to `out` through a call using only
281
+ * value-preserving steps and possibly a single read step, not taking
282
+ * call contexts into account.
284
283
*
285
- * `contentIn` describes the content of `arg` that can flow to `out` (if any).
284
+ * If a read step was taken, then `read` captures the `Content`, the
285
+ * container type, and the content type.
286
286
*/
287
287
pragma [ nomagic]
288
- predicate argumentValueFlowsThrough ( ArgumentNode arg , ContentOption contentIn , Node out ) {
288
+ predicate argumentValueFlowsThrough ( ArgumentNode arg , ReadStepTypesOption read , Node out ) {
289
289
exists ( DataFlowCall call , ReturnKind kind |
290
- argumentValueFlowsThrough0 ( call , arg , kind , contentIn ) and
290
+ argumentValueFlowsThrough0 ( call , arg , kind , read ) and
291
291
out = getAnOutNode ( call , kind )
292
292
|
293
293
// normal flow through
294
- contentIn = TContentNone ( ) and
294
+ read = TReadStepTypesNone ( ) and
295
295
compatibleTypes ( getErasedNodeTypeBound ( arg ) , getErasedNodeTypeBound ( out ) )
296
296
or
297
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
- )
298
+ compatibleTypes ( getErasedNodeTypeBound ( arg ) , read .getContainerType ( ) ) and
299
+ compatibleTypes ( read .getContentType ( ) , getErasedNodeTypeBound ( out ) )
303
300
)
304
301
}
305
302
303
+ /**
304
+ * Holds if `arg` flows to `out` through a call using only
305
+ * value-preserving steps and a single read step, not taking call
306
+ * contexts into account, thus representing a getter-step.
307
+ */
308
+ predicate getterStep ( ArgumentNode arg , Content c , Node out ) {
309
+ argumentValueFlowsThrough ( arg , TReadStepTypesSome ( _, c , _) , out )
310
+ }
311
+
306
312
/**
307
313
* Holds if `p` can flow to a return node of kind `kind` in the same
308
- * callable using only value-preserving steps.
314
+ * callable using only value-preserving steps and possibly a single read
315
+ * step.
309
316
*
310
- * `contentIn` describes the content of `p` that can flow to the return
311
- * node (if any) .
317
+ * If a read step was taken, then `read` captures the `Content`, the
318
+ * container type, and the content type .
312
319
*/
313
320
private predicate parameterValueFlowReturn (
314
- ParameterNode p , ReturnKind kind , ContentOption contentIn
321
+ ParameterNode p , ReturnKind kind , ReadStepTypesOption read
315
322
) {
316
323
exists ( ReturnNode ret |
317
- parameterValueFlow ( p , ret , contentIn ) and
324
+ parameterValueFlow ( p , ret , read ) and
318
325
kind = ret .getKind ( )
319
326
)
320
327
}
@@ -329,7 +336,27 @@ private module Cached {
329
336
*/
330
337
cached
331
338
predicate parameterValueFlowsToPreUpdate ( ParameterNode p , PostUpdateNode n ) {
332
- parameterValueFlow ( p , n .getPreUpdateNode ( ) , TContentNone ( ) )
339
+ parameterValueFlow ( p , n .getPreUpdateNode ( ) , TReadStepTypesNone ( ) )
340
+ }
341
+
342
+ private predicate store (
343
+ Node node1 , Content c , Node node2 , DataFlowType contentType , DataFlowType containerType
344
+ ) {
345
+ storeStep ( node1 , c , node2 ) and
346
+ readStep ( _, c , _) and
347
+ contentType = getErasedNodeTypeBound ( node1 ) and
348
+ containerType = getErasedNodeTypeBound ( node2 )
349
+ or
350
+ exists ( Node n1 , Node n2 |
351
+ n1 = node1 .( PostUpdateNode ) .getPreUpdateNode ( ) and
352
+ n2 = node2 .( PostUpdateNode ) .getPreUpdateNode ( )
353
+ |
354
+ argumentValueFlowsThrough ( n2 , TReadStepTypesSome ( containerType , c , contentType ) , n1 )
355
+ or
356
+ readStep ( n2 , c , n1 ) and
357
+ contentType = getErasedNodeTypeBound ( n1 ) and
358
+ containerType = getErasedNodeTypeBound ( n2 )
359
+ )
333
360
}
334
361
335
362
/**
@@ -340,17 +367,8 @@ private module Cached {
340
367
* been stored into, in order to handle cases like `x.f1.f2 = y`.
341
368
*/
342
369
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
- )
370
+ predicate store ( Node node1 , TypedContent tc , Node node2 , DataFlowType contentType ) {
371
+ store ( node1 , tc .getContent ( ) , node2 , contentType , tc .getContainerType ( ) )
354
372
}
355
373
356
374
import FlowThrough
@@ -397,10 +415,13 @@ private module Cached {
397
415
TBooleanNone ( ) or
398
416
TBooleanSome ( boolean b ) { b = true or b = false }
399
417
418
+ cached
419
+ newtype TTypedContent = MkTypedContent ( Content c , DataFlowType t ) { store ( _, c , _, _, t ) }
420
+
400
421
cached
401
422
newtype TAccessPathFront =
402
423
TFrontNil ( DataFlowType t ) or
403
- TFrontHead ( Content f )
424
+ TFrontHead ( TypedContent tc )
404
425
405
426
cached
406
427
newtype TAccessPathFrontOption =
@@ -415,25 +436,38 @@ class CastingNode extends Node {
415
436
CastingNode ( ) {
416
437
this instanceof ParameterNode or
417
438
this instanceof CastNode or
418
- this instanceof OutNodeExt
439
+ this instanceof OutNodeExt or
440
+ // For reads, `x.f`, we want to check that the tracked type after the read (which
441
+ // is obtained by popping the head of the access path stack) is compatible with
442
+ // the type of `x.f`.
443
+ readStep ( _, _, this )
419
444
}
420
445
}
421
446
422
- newtype TContentOption =
423
- TContentNone ( ) or
424
- TContentSome ( Content f )
447
+ private predicate readStepWithTypes (
448
+ Node n1 , DataFlowType container , Content c , Node n2 , DataFlowType content
449
+ ) {
450
+ readStep ( n1 , c , n2 ) and
451
+ container = getErasedNodeTypeBound ( n1 ) and
452
+ content = getErasedNodeTypeBound ( n2 )
453
+ }
425
454
426
- private class ContentOption extends TContentOption {
427
- Content getContent ( ) { this = TContentSome ( result ) }
455
+ private newtype TReadStepTypesOption =
456
+ TReadStepTypesNone ( ) or
457
+ TReadStepTypesSome ( DataFlowType container , Content c , DataFlowType content ) {
458
+ readStepWithTypes ( _, container , c , _, content )
459
+ }
428
460
429
- predicate hasContent ( ) { exists ( this .getContent ( ) ) }
461
+ private class ReadStepTypesOption extends TReadStepTypesOption {
462
+ predicate isSome ( ) { this instanceof TReadStepTypesSome }
430
463
431
- string toString ( ) {
432
- result = this .getContent ( ) .toString ( )
433
- or
434
- not this .hasContent ( ) and
435
- result = "<none>"
436
- }
464
+ DataFlowType getContainerType ( ) { this = TReadStepTypesSome ( result , _, _) }
465
+
466
+ Content getContent ( ) { this = TReadStepTypesSome ( _, result , _) }
467
+
468
+ DataFlowType getContentType ( ) { this = TReadStepTypesSome ( _, _, result ) }
469
+
470
+ string toString ( ) { if this .isSome ( ) then result = "Some(..)" else result = "None()" }
437
471
}
438
472
439
473
/**
@@ -692,6 +726,23 @@ class BooleanOption extends TBooleanOption {
692
726
}
693
727
}
694
728
729
+ /** Content tagged with the type of a containing object. */
730
+ class TypedContent extends MkTypedContent {
731
+ private Content c ;
732
+ private DataFlowType t ;
733
+
734
+ TypedContent ( ) { this = MkTypedContent ( c , t ) }
735
+
736
+ /** Gets the content. */
737
+ Content getContent ( ) { result = c }
738
+
739
+ /** Gets the container type. */
740
+ DataFlowType getContainerType ( ) { result = t }
741
+
742
+ /** Gets a textual representation of this content. */
743
+ string toString ( ) { result = c .toString ( ) }
744
+ }
745
+
695
746
/**
696
747
* The front of an access path. This is either a head or a nil.
697
748
*/
@@ -702,25 +753,29 @@ abstract class AccessPathFront extends TAccessPathFront {
702
753
703
754
abstract boolean toBoolNonEmpty ( ) ;
704
755
705
- predicate headUsesContent ( Content f ) { this = TFrontHead ( f ) }
756
+ predicate headUsesContent ( TypedContent tc ) { this = TFrontHead ( tc ) }
706
757
}
707
758
708
759
class AccessPathFrontNil extends AccessPathFront , TFrontNil {
709
- override string toString ( ) {
710
- exists ( DataFlowType t | this = TFrontNil ( t ) | result = ppReprType ( t ) )
711
- }
760
+ private DataFlowType t ;
712
761
713
- override DataFlowType getType ( ) { this = TFrontNil ( result ) }
762
+ AccessPathFrontNil ( ) { this = TFrontNil ( t ) }
763
+
764
+ override string toString ( ) { result = ppReprType ( t ) }
765
+
766
+ override DataFlowType getType ( ) { result = t }
714
767
715
768
override boolean toBoolNonEmpty ( ) { result = false }
716
769
}
717
770
718
771
class AccessPathFrontHead extends AccessPathFront , TFrontHead {
719
- override string toString ( ) { exists ( Content f | this = TFrontHead ( f ) | result = f . toString ( ) ) }
772
+ private TypedContent tc ;
720
773
721
- override DataFlowType getType ( ) {
722
- exists ( Content head | this = TFrontHead ( head ) | result = head .getContainerType ( ) )
723
- }
774
+ AccessPathFrontHead ( ) { this = TFrontHead ( tc ) }
775
+
776
+ override string toString ( ) { result = tc .toString ( ) }
777
+
778
+ override DataFlowType getType ( ) { result = tc .getContainerType ( ) }
724
779
725
780
override boolean toBoolNonEmpty ( ) { result = true }
726
781
}
0 commit comments