@@ -419,4 +419,79 @@ module AccessPath {
419419 or
420420 result = node .getALocalSource ( )
421421 }
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+ }
422497}
0 commit comments