@@ -419,4 +419,79 @@ 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
+ private DataFlow:: Node rankedAccessPath (
440
+ ReachableBasicBlock bb , Root root , string path , int ranking , AccessPathKind type
441
+ ) {
442
+ result =
443
+ rank [ ranking ] ( DataFlow:: Node ref |
444
+ ref = getAccessTo ( root , path , _) and
445
+ ref .getBasicBlock ( ) = bb
446
+ |
447
+ ref order by any ( int i | ref .asExpr ( ) = bb .getNode ( i ) )
448
+ ) and
449
+ result = getAccessTo ( root , path , type )
450
+ }
451
+
452
+ /**
453
+ * Gets an access to `path` from `root` with type `type`.
454
+ *
455
+ * This predicate uses both the AccessPath API, and the SourceNode API.
456
+ * This ensures that we have basic support for access-paths with ambiguous roots.
457
+ */
458
+ pragma [ nomagic]
459
+ private DataFlow:: Node getAccessTo ( Root root , string path , AccessPathKind type ) {
460
+ ( path = fromReference ( result , root ) or result = root .getAPropertyRead ( path ) ) and
461
+ type = AccessPathRead ( )
462
+ or
463
+ ( path = fromRhs ( result , root ) or result = root .getAPropertyWrite ( path ) ) and
464
+ type = AccessPathWrite ( )
465
+ }
466
+
467
+ /**
468
+ * Gets a basicblock that is domminated by a assignment to an access-path identified by `root` and `path`.
469
+ */
470
+ private ReachableBasicBlock getADominatedBlock ( Root root , string path ) {
471
+ getAccessTo ( root , path , AccessPathWrite ( ) )
472
+ .getBasicBlock ( )
473
+ .( ReachableBasicBlock )
474
+ .strictlyDominates ( result )
475
+ }
476
+
477
+ /**
478
+ * EXPERIMENTAL. This API may change in the future.
479
+ *
480
+ * Holds for `read` if there exists a previous write to the same access-path that dominates this read.
481
+ */
482
+ cached
483
+ predicate hasDominatingWrite ( DataFlow:: PropRead read ) {
484
+ // within the same basic block.
485
+ exists ( ReachableBasicBlock bb , Root root , string path , int ranking |
486
+ read = rankedAccessPath ( bb , root , path , ranking , AccessPathRead ( ) ) and
487
+ exists ( rankedAccessPath ( bb , root , path , any ( int prev | prev < ranking ) , AccessPathWrite ( ) ) )
488
+ )
489
+ or
490
+ // across basic blocks.
491
+ exists ( Root root , string path |
492
+ read = getAccessTo ( root , path , AccessPathRead ( ) ) and
493
+ read .getBasicBlock ( ) = getADominatedBlock ( root , path )
494
+ )
495
+ }
496
+ }
422
497
}
0 commit comments