@@ -259,83 +259,93 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
259
259
260
260
/**
261
261
* Holds if `node` is reachable from a source in the given configuration
262
- * ignoring call contexts.
262
+ * taking simple call contexts into consideration .
263
263
*/
264
- private predicate nodeCandFwd1 ( Node node , Configuration config ) {
264
+ private predicate nodeCandFwd1 ( Node node , boolean fromArg , Configuration config ) {
265
265
not fullBarrier ( node , config ) and
266
266
(
267
- config .isSource ( node )
267
+ config .isSource ( node ) and
268
+ fromArg = false
268
269
or
269
270
exists ( Node mid |
270
- nodeCandFwd1 ( mid , config ) and
271
+ nodeCandFwd1 ( mid , fromArg , config ) and
271
272
localFlowStep ( mid , node , config )
272
273
)
273
274
or
274
275
exists ( Node mid |
275
- nodeCandFwd1 ( mid , config ) and
276
+ nodeCandFwd1 ( mid , fromArg , config ) and
276
277
additionalLocalFlowStep ( mid , node , config )
277
278
)
278
279
or
279
280
exists ( Node mid |
280
281
nodeCandFwd1 ( mid , config ) and
281
- jumpStep ( mid , node , config )
282
+ jumpStep ( mid , node , config ) and
283
+ fromArg = false
282
284
)
283
285
or
284
286
exists ( Node mid |
285
287
nodeCandFwd1 ( mid , config ) and
286
- additionalJumpStep ( mid , node , config )
288
+ additionalJumpStep ( mid , node , config ) and
289
+ fromArg = false
287
290
)
288
291
or
289
292
// store
290
293
exists ( Node mid |
291
294
useFieldFlow ( config ) and
292
- nodeCandFwd1 ( mid , config ) and
295
+ nodeCandFwd1 ( mid , fromArg , config ) and
293
296
storeDirect ( mid , _, node ) and
294
297
not outBarrier ( mid , config )
295
298
)
296
299
or
297
300
// read
298
301
exists ( Content f |
299
- nodeCandFwd1Read ( f , node , config ) and
302
+ nodeCandFwd1Read ( f , node , fromArg , config ) and
300
303
storeCandFwd1 ( f , config ) and
301
304
not inBarrier ( node , config )
302
305
)
303
306
or
304
307
// flow into a callable
305
308
exists ( Node arg |
306
309
nodeCandFwd1 ( arg , config ) and
307
- viableParamArg ( _, node , arg )
310
+ viableParamArg ( _, node , arg ) and
311
+ fromArg = true
308
312
)
309
313
or
310
314
// flow out of a callable
311
- exists ( DataFlowCall call , ReturnPosition pos , ReturnKindExt kind |
312
- nodeCandFwd1ReturnPosition ( pos , config ) and
313
- pos = viableReturnPos ( call , kind ) and
314
- node = kind .getAnOutNode ( call )
315
+ exists ( DataFlowCall call |
316
+ nodeCandFwd1Out ( call , node , false , config ) and
317
+ fromArg = false
318
+ or
319
+ nodeCandFwd1OutFromArg ( call , node , config ) and
320
+ flowOutCandFwd1 ( call , fromArg , config )
315
321
)
316
322
)
317
323
}
318
324
319
- pragma [ noinline]
320
- private predicate nodeCandFwd1ReturnPosition ( ReturnPosition pos , Configuration config ) {
325
+ private predicate nodeCandFwd1 ( Node node , Configuration config ) { nodeCandFwd1 ( node , _, config ) }
326
+
327
+ pragma [ nomagic]
328
+ private predicate nodeCandFwd1ReturnPosition (
329
+ ReturnPosition pos , boolean fromArg , Configuration config
330
+ ) {
321
331
exists ( ReturnNodeExt ret |
322
- nodeCandFwd1 ( ret , config ) and
332
+ nodeCandFwd1 ( ret , fromArg , config ) and
323
333
getReturnPosition ( ret ) = pos
324
334
)
325
335
}
326
336
327
337
pragma [ nomagic]
328
- private predicate nodeCandFwd1Read ( Content f , Node node , Configuration config ) {
338
+ private predicate nodeCandFwd1Read ( Content f , Node node , boolean fromArg , Configuration config ) {
329
339
exists ( Node mid |
330
- nodeCandFwd1 ( mid , config ) and
340
+ nodeCandFwd1 ( mid , fromArg , config ) and
331
341
readDirect ( mid , f , node )
332
342
)
333
343
}
334
344
335
345
/**
336
346
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
337
347
*/
338
- pragma [ noinline ]
348
+ pragma [ nomagic ]
339
349
private predicate storeCandFwd1 ( Content f , Configuration config ) {
340
350
exists ( Node mid , Node node |
341
351
not fullBarrier ( node , config ) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
345
355
)
346
356
}
347
357
358
+ pragma [ nomagic]
359
+ private predicate nodeCandFwd1ReturnKind (
360
+ DataFlowCall call , ReturnKindExt kind , boolean fromArg , Configuration config
361
+ ) {
362
+ exists ( ReturnPosition pos |
363
+ nodeCandFwd1ReturnPosition ( pos , fromArg , config ) and
364
+ pos = viableReturnPos ( call , kind )
365
+ )
366
+ }
367
+
368
+ pragma [ nomagic]
369
+ private predicate nodeCandFwd1Out (
370
+ DataFlowCall call , Node node , boolean fromArg , Configuration config
371
+ ) {
372
+ exists ( ReturnKindExt kind |
373
+ nodeCandFwd1ReturnKind ( call , kind , fromArg , config ) and
374
+ node = kind .getAnOutNode ( call )
375
+ )
376
+ }
377
+
378
+ pragma [ nomagic]
379
+ private predicate nodeCandFwd1OutFromArg ( DataFlowCall call , Node node , Configuration config ) {
380
+ nodeCandFwd1Out ( call , node , true , config )
381
+ }
382
+
383
+ /**
384
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
385
+ */
386
+ pragma [ nomagic]
387
+ private predicate flowOutCandFwd1 ( DataFlowCall call , boolean fromArg , Configuration config ) {
388
+ exists ( ArgumentNode arg |
389
+ nodeCandFwd1 ( arg , fromArg , config ) and
390
+ viableParamArg ( call , _, arg )
391
+ )
392
+ }
393
+
348
394
bindingset [ result , b]
349
395
private boolean unbindBool ( boolean b ) { result != b .booleanNot ( ) }
350
396
351
397
/**
352
398
* Holds if `node` is part of a path from a source to a sink in the given
353
- * configuration ignoring call contexts.
399
+ * configuration taking simple call contexts into consideration .
354
400
*/
355
401
pragma [ nomagic]
356
- private predicate nodeCand1 ( Node node , Configuration config ) {
402
+ private predicate nodeCand1 ( Node node , boolean toReturn , Configuration config ) {
403
+ nodeCand1_0 ( node , toReturn , config ) and
404
+ nodeCandFwd1 ( node , config )
405
+ }
406
+
407
+ pragma [ nomagic]
408
+ private predicate nodeCand1_0 ( Node node , boolean toReturn , Configuration config ) {
357
409
nodeCandFwd1 ( node , config ) and
358
- config .isSink ( node )
410
+ config .isSink ( node ) and
411
+ toReturn = false
359
412
or
360
- nodeCandFwd1 ( node , unbind ( config ) ) and
361
- (
362
- exists ( Node mid |
363
- localFlowStep ( node , mid , config ) and
364
- nodeCand1 ( mid , config )
365
- )
366
- or
367
- exists ( Node mid |
368
- additionalLocalFlowStep ( node , mid , config ) and
369
- nodeCand1 ( mid , config )
370
- )
371
- or
372
- exists ( Node mid |
373
- jumpStep ( node , mid , config ) and
374
- nodeCand1 ( mid , config )
375
- )
376
- or
377
- exists ( Node mid |
378
- additionalJumpStep ( node , mid , config ) and
379
- nodeCand1 ( mid , config )
380
- )
381
- or
382
- // store
383
- exists ( Content f |
384
- nodeCand1Store ( f , node , config ) and
385
- readCand1 ( f , config )
386
- )
387
- or
388
- // read
389
- exists ( Node mid , Content f |
390
- readDirect ( node , f , mid ) and
391
- storeCandFwd1 ( f , unbind ( config ) ) and
392
- nodeCand1 ( mid , config )
393
- )
394
- or
395
- // flow into a callable
396
- exists ( Node param |
397
- viableParamArg ( _, param , node ) and
398
- nodeCand1 ( param , config )
399
- )
413
+ exists ( Node mid |
414
+ localFlowStep ( node , mid , config ) and
415
+ nodeCand1 ( mid , toReturn , config )
416
+ )
417
+ or
418
+ exists ( Node mid |
419
+ additionalLocalFlowStep ( node , mid , config ) and
420
+ nodeCand1 ( mid , toReturn , config )
421
+ )
422
+ or
423
+ exists ( Node mid |
424
+ jumpStep ( node , mid , config ) and
425
+ nodeCand1 ( mid , _, config ) and
426
+ toReturn = false
427
+ )
428
+ or
429
+ exists ( Node mid |
430
+ additionalJumpStep ( node , mid , config ) and
431
+ nodeCand1 ( mid , _, config ) and
432
+ toReturn = false
433
+ )
434
+ or
435
+ // store
436
+ exists ( Content f |
437
+ nodeCand1Store ( f , node , toReturn , config ) and
438
+ readCand1 ( f , config )
439
+ )
440
+ or
441
+ // read
442
+ exists ( Node mid , Content f |
443
+ readDirect ( node , f , mid ) and
444
+ storeCandFwd1 ( f , unbind ( config ) ) and
445
+ nodeCand1 ( mid , toReturn , config )
446
+ )
447
+ or
448
+ // flow into a callable
449
+ exists ( DataFlowCall call |
450
+ nodeCand1Arg ( call , node , false , config ) and
451
+ toReturn = false
400
452
or
401
- // flow out of a callable
402
- exists ( ReturnPosition pos |
403
- nodeCand1ReturnPosition ( pos , config ) and
404
- getReturnPosition ( node ) = pos
405
- )
453
+ nodeCand1ArgToReturn ( call , node , config ) and
454
+ flowInCand1 ( call , toReturn , config )
455
+ )
456
+ or
457
+ // flow out of a callable
458
+ exists ( ReturnPosition pos |
459
+ nodeCand1ReturnPosition ( pos , config ) and
460
+ getReturnPosition ( node ) = pos and
461
+ toReturn = true
406
462
)
407
463
}
408
464
409
- pragma [ noinline]
465
+ pragma [ nomagic]
466
+ private predicate nodeCand1 ( Node node , Configuration config ) { nodeCand1 ( node , _, config ) }
467
+
468
+ pragma [ nomagic]
410
469
private predicate nodeCand1ReturnPosition ( ReturnPosition pos , Configuration config ) {
411
470
exists ( DataFlowCall call , ReturnKindExt kind , Node out |
412
- nodeCand1 ( out , config ) and
471
+ nodeCand1 ( out , _ , config ) and
413
472
pos = viableReturnPos ( call , kind ) and
414
473
out = kind .getAnOutNode ( call )
415
474
)
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
418
477
/**
419
478
* Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
420
479
*/
421
- pragma [ noinline ]
480
+ pragma [ nomagic ]
422
481
private predicate readCand1 ( Content f , Configuration config ) {
423
482
exists ( Node mid , Node node |
424
483
useFieldFlow ( config ) and
425
484
nodeCandFwd1 ( node , unbind ( config ) ) and
426
485
readDirect ( node , f , mid ) and
427
486
storeCandFwd1 ( f , unbind ( config ) ) and
428
- nodeCand1 ( mid , config )
487
+ nodeCand1 ( mid , _ , config )
429
488
)
430
489
}
431
490
432
491
pragma [ nomagic]
433
- private predicate nodeCand1Store ( Content f , Node node , Configuration config ) {
492
+ private predicate nodeCand1Store ( Content f , Node node , boolean toReturn , Configuration config ) {
434
493
exists ( Node mid |
435
- nodeCand1 ( mid , config ) and
494
+ nodeCand1 ( mid , toReturn , config ) and
436
495
storeCandFwd1 ( f , unbind ( config ) ) and
437
496
storeDirect ( node , f , mid )
438
497
)
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
444
503
*/
445
504
private predicate readStoreCand1 ( Content f , Configuration conf ) {
446
505
readCand1 ( f , conf ) and
447
- nodeCand1Store ( f , _, conf )
506
+ nodeCand1Store ( f , _, _, conf )
507
+ }
508
+
509
+ pragma [ nomagic]
510
+ private predicate viableParamArgCandFwd1 (
511
+ DataFlowCall call , ParameterNode p , ArgumentNode arg , Configuration config
512
+ ) {
513
+ viableParamArg ( call , p , arg ) and
514
+ nodeCandFwd1 ( arg , config )
515
+ }
516
+
517
+ pragma [ nomagic]
518
+ private predicate nodeCand1Arg (
519
+ DataFlowCall call , ArgumentNode arg , boolean toReturn , Configuration config
520
+ ) {
521
+ exists ( ParameterNode p |
522
+ nodeCand1 ( p , toReturn , config ) and
523
+ viableParamArgCandFwd1 ( call , p , arg , config )
524
+ )
525
+ }
526
+
527
+ pragma [ nomagic]
528
+ private predicate nodeCand1ArgToReturn ( DataFlowCall call , ArgumentNode arg , Configuration config ) {
529
+ nodeCand1Arg ( call , arg , true , config )
530
+ }
531
+
532
+ /**
533
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
534
+ */
535
+ pragma [ nomagic]
536
+ private predicate flowInCand1 ( DataFlowCall call , boolean toReturn , Configuration config ) {
537
+ exists ( Node out |
538
+ nodeCand1 ( out , toReturn , config ) and
539
+ nodeCandFwd1OutFromArg ( call , out , config )
540
+ )
448
541
}
449
542
450
543
private predicate throughFlowNodeCand ( Node node , Configuration config ) {
451
- nodeCand1 ( node , config ) and
544
+ nodeCand1 ( node , true , config ) and
452
545
not fullBarrier ( node , config ) and
453
546
not inBarrier ( node , config ) and
454
547
not outBarrier ( node , config )
0 commit comments