@@ -419,4 +419,135 @@ 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+ * 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+ }
422553}
0 commit comments