@@ -419,4 +419,135 @@ module AccessPath {
419
419
or
420
420
result = node .getALocalSource ( )
421
421
}
422
+
423
+ /**
424
+ * A module for reasoning dominating reads and writes to access-paths.
425
+ */
426
+ module DominatingPaths {
427
+ /**
428
+ * A classification of acccess paths into reads and writes.
429
+ */
430
+ cached
431
+ private newtype AccessPathKind =
432
+ AccessPathRead ( ) or
433
+ AccessPathWrite ( )
434
+
435
+ /**
436
+ * Gets the `ranking`th access-path with `root` and `path` within `bb`.
437
+ * And the access-path has type `type`.
438
+ *
439
+ * Only has a result if there exists both a read and write of the access-path within `bb`.
440
+ */
441
+ private ControlFlowNode rankedAccessPath (
442
+ ReachableBasicBlock bb , Root root , string path , int ranking , AccessPathKind type
443
+ ) {
444
+ result =
445
+ rank [ ranking ] ( ControlFlowNode ref |
446
+ ref = getAccessTo ( root , path , _) and
447
+ ref .getBasicBlock ( ) = bb and
448
+ // Prunes the accesses where there does not exists a read and write within the same basicblock.
449
+ // This could be more precise, but doing it like this avoids massive joins.
450
+ hasRead ( bb ) and
451
+ hasWrite ( bb )
452
+ |
453
+ ref order by any ( int i | ref = bb .getNode ( i ) )
454
+ ) and
455
+ result = getAccessTo ( root , path , type )
456
+ }
457
+
458
+ /**
459
+ * Holds if there exists an access-path read inside the basic-block `bb`.
460
+ *
461
+ * INTERNAL: This predicate is only meant to be used inside `rankedAccessPath`.
462
+ */
463
+ pragma [ noinline]
464
+ private predicate hasRead ( ReachableBasicBlock bb ) {
465
+ bb = getAccessTo ( _, _, AccessPathRead ( ) ) .getBasicBlock ( )
466
+ }
467
+
468
+ /**
469
+ * Holds if there exists an access-path write inside the basic-block `bb`.
470
+ *
471
+ * INTERNAL: This predicate is only meant to be used inside `rankedAccessPath`.
472
+ */
473
+ pragma [ noinline]
474
+ private predicate hasWrite ( ReachableBasicBlock bb ) {
475
+ bb = getAccessTo ( _, _, AccessPathRead ( ) ) .getBasicBlock ( )
476
+ }
477
+
478
+ /**
479
+ * Gets a `ControlFlowNode` for an access to `path` from `root` with type `type`.
480
+ *
481
+ * This predicate uses both the AccessPath API, and the SourceNode API.
482
+ * This ensures that we have basic support for access-paths with ambiguous roots.
483
+ *
484
+ * There is only a result if both a read and a write of the access-path exists.
485
+ */
486
+ pragma [ nomagic]
487
+ private ControlFlowNode getAccessTo ( Root root , string path , AccessPathKind type ) {
488
+ exists ( getAReadNode ( root , path ) ) and
489
+ exists ( getAWriteNode ( root , path ) ) and
490
+ (
491
+ type = AccessPathRead ( ) and
492
+ result = getAReadNode ( root , path )
493
+ or
494
+ type = AccessPathWrite ( ) and
495
+ result = getAWriteNode ( root , path )
496
+ )
497
+ }
498
+
499
+ /**
500
+ * Gets a `ControlFlowNode` for a read to `path` from `root`.
501
+ *
502
+ * Only used within `getAccessTo`.
503
+ */
504
+ private ControlFlowNode getAReadNode ( Root root , string path ) {
505
+ exists ( DataFlow:: PropRead read | read .asExpr ( ) = result |
506
+ path = fromReference ( read , root ) or
507
+ read = root .getAPropertyRead ( path )
508
+ )
509
+ }
510
+
511
+ /**
512
+ * Gets a `ControlFlowNode` for a write to `path` from `root`.
513
+ *
514
+ * Only used within `getAccessTo`.
515
+ */
516
+ private ControlFlowNode getAWriteNode ( Root root , string path ) {
517
+ result = root .getAPropertyWrite ( path ) .getWriteNode ( )
518
+ or
519
+ exists ( DataFlow:: PropWrite write | path = fromRhs ( write .getRhs ( ) , root ) |
520
+ result = write .getWriteNode ( )
521
+ )
522
+ }
523
+
524
+ /**
525
+ * Gets a basic-block where the access path defined by `root` and `path` is written to.
526
+ * And a read to the same access path exists.
527
+ */
528
+ private ReachableBasicBlock getAWriteBlock ( Root root , string path ) {
529
+ result = getAccessTo ( root , path , AccessPathWrite ( ) ) .getBasicBlock ( ) and
530
+ exists ( getAccessTo ( root , path , AccessPathRead ( ) ) ) // helps performance
531
+ }
532
+
533
+ /**
534
+ * EXPERIMENTAL. This API may change in the future.
535
+ *
536
+ * Holds for `read` if there exists a previous write to the same access-path that dominates this read.
537
+ */
538
+ cached
539
+ predicate hasDominatingWrite ( DataFlow:: PropRead read ) {
540
+ // within the same basic block.
541
+ exists ( ReachableBasicBlock bb , Root root , string path , int ranking |
542
+ read .asExpr ( ) = rankedAccessPath ( bb , root , path , ranking , AccessPathRead ( ) ) and
543
+ exists ( rankedAccessPath ( bb , root , path , any ( int prev | prev < ranking ) , AccessPathWrite ( ) ) )
544
+ )
545
+ or
546
+ // across basic blocks.
547
+ exists ( Root root , string path |
548
+ read .asExpr ( ) = getAccessTo ( root , path , AccessPathRead ( ) ) and
549
+ getAWriteBlock ( root , path ) .strictlyDominates ( read .getBasicBlock ( ) )
550
+ )
551
+ }
552
+ }
422
553
}
0 commit comments