@@ -454,6 +454,7 @@ private class FlowStepThroughImport extends AdditionalFlowStep, DataFlow::ValueN
454454private predicate basicFlowStep (
455455 DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
456456) {
457+ isLive ( ) and
457458 isRelevantForward ( pred , cfg ) and
458459 (
459460 // Local flow
@@ -888,9 +889,9 @@ private predicate flowsTo(
888889 PathNode flowsource , DataFlow:: Node source , SinkPathNode flowsink , DataFlow:: Node sink ,
889890 DataFlow:: Configuration cfg
890891) {
891- flowsource = MkPathNode ( source , cfg , _ ) and
892+ flowsource . wraps ( source , cfg ) and
892893 flowsink = flowsource .getASuccessor * ( ) and
893- flowsink = MkPathNode ( sink , id ( cfg ) , _ )
894+ flowsink . wraps ( sink , id ( cfg ) )
894895}
895896
896897/**
@@ -933,19 +934,45 @@ private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg, PathSum
933934}
934935
935936/**
936- * Holds if `cfg` has at least one source and at least one sink.
937+ * Holds if there is a configuration that has at least one source and at least one sink.
937938 */
938939pragma [ noinline]
939- private predicate isLive ( DataFlow:: Configuration cfg ) { isSource ( _, cfg , _) and isSink ( _, cfg , _) }
940+ private predicate isLive ( ) { exists ( DataFlow:: Configuration cfg | isSource ( _, cfg , _) and isSink ( _, cfg , _) ) }
940941
941942/**
942943 * A data flow node on an inter-procedural path from a source.
943944 */
944945private newtype TPathNode =
945- MkPathNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg , PathSummary summary ) {
946- isLive ( cfg ) and
946+ MkSourceNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) { isSourceNode ( nd , cfg , _) }
947+ or
948+ MkMidNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg , PathSummary summary ) {
949+ isLive ( ) and
947950 onPath ( nd , cfg , summary )
948951 }
952+ or
953+ MkSinkNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) { isSinkNode ( nd , cfg , _) }
954+
955+ /**
956+ * Holds if `nd` is a source node for configuration `cfg`, and there is a path from `nd` to a sink
957+ * with the given `summary`.
958+ */
959+ private predicate isSourceNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg , PathSummary summary ) {
960+ exists ( FlowLabel lbl | summary = PathSummary:: level ( lbl ) |
961+ isSource ( nd , cfg , lbl ) and
962+ isLive ( ) and
963+ onPath ( nd , cfg , summary )
964+ )
965+ }
966+
967+ /**
968+ * Holds if `nd` is a sink node for configuration `cfg`, and there is a path from a source to `nd`
969+ * with the given `summary`.
970+ */
971+ private predicate isSinkNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg , PathSummary summary ) {
972+ isSink ( nd , cfg , summary .getEndLabel ( ) ) and
973+ isLive ( ) and
974+ onPath ( nd , cfg , summary )
975+ }
949976
950977/**
951978 * Maps `cfg` to itself.
@@ -957,48 +984,46 @@ bindingset[cfg, result]
957984private DataFlow:: Configuration id ( DataFlow:: Configuration cfg ) { result >= cfg and cfg >= result }
958985
959986/**
960- * A data flow node on an inter-procedural path from a source to a sink.
987+ * A data-flow node on an inter-procedural path from a source to a sink.
988+ *
989+ * A path node wraps a data-flow node `nd` and a data-flow configuration `cfg` such that `nd` is
990+ * on a path from a source to a sink under `cfg`.
961991 *
962- * A path node is a triple `(nd, cfg, summary)` where `nd` is a data flow node and `cfg`
963- * is a data flow tracking configuration such that `nd` is on a path from a source to a
964- * sink under `cfg` summarized by `summary`.
992+ * There are three kinds of path nodes:
993+ *
994+ * - source nodes: wrapping a source node and a configuration such that there is a path from that
995+ * source to some sink under the configuration;
996+ * - sink nodes: wrapping a sink node and a configuration such that there is a path from some source
997+ * to that sink under the configuration;
998+ * - mid nodes: wrapping a node, a configuration and a path summary such that there is a path from
999+ * some source to the node with the given summary that can be extended to a path to some sink node,
1000+ * all under the configuration.
9651001 */
9661002class PathNode extends TPathNode {
9671003 DataFlow:: Node nd ;
968- DataFlow:: Configuration cfg ;
969- PathSummary summary ;
1004+ Configuration cfg ;
9701005
971- PathNode ( ) { this = MkPathNode ( nd , cfg , summary ) }
1006+ PathNode ( ) {
1007+ this = MkSourceNode ( nd , cfg ) or
1008+ this = MkMidNode ( nd , cfg , _) or
1009+ this = MkSinkNode ( nd , cfg )
1010+ }
9721011
973- /** Gets the underlying data flow node of this path node. */
974- DataFlow:: Node getNode ( ) { result = nd }
1012+ /** Holds if this path node wraps data-flow node `nd` and configuration `c`. */
1013+ predicate wraps ( DataFlow:: Node n , DataFlow:: Configuration c ) {
1014+ nd = n and cfg = c
1015+ }
9751016
976- /** Gets the underlying data flow tracking configuration of this path node. */
1017+ /** Gets the underlying configuration of this path node. */
9771018 DataFlow:: Configuration getConfiguration ( ) { result = cfg }
9781019
979- /** Gets the summary of the path underlying this path node. */
980- PathSummary getPathSummary ( ) { result = summary }
981-
982- /**
983- * Gets a successor node of this path node, including hidden nodes.
984- */
985- private PathNode getASuccessorInternal ( ) {
986- exists ( DataFlow:: Node succ , PathSummary newSummary |
987- flowStep ( nd , id ( cfg ) , succ , newSummary ) and
988- result = MkPathNode ( succ , id ( cfg ) , summary .append ( newSummary ) )
989- )
990- }
991-
992- /**
993- * Gets a successor of this path node, if it is a hidden node.
994- */
995- private PathNode getAHiddenSuccessor ( ) {
996- isHidden ( ) and
997- result = getASuccessorInternal ( )
998- }
1020+ /** Gets the underlying data-flow node of this path node. */
1021+ DataFlow:: Node getNode ( ) { result = nd }
9991022
10001023 /** Gets a successor node of this path node. */
1001- PathNode getASuccessor ( ) { result = getASuccessorInternal ( ) .getAHiddenSuccessor * ( ) }
1024+ final PathNode getASuccessor ( ) {
1025+ result = getASuccessor ( this )
1026+ }
10021027
10031028 /** Gets a textual representation of this path node. */
10041029 string toString ( ) { result = nd .toString ( ) }
@@ -1015,6 +1040,68 @@ class PathNode extends TPathNode {
10151040 ) {
10161041 nd .hasLocationInfo ( filepath , startline , startcolumn , endline , endcolumn )
10171042 }
1043+ }
1044+
1045+ /** Gets the mid node corresponding to `src`. */
1046+ private MidPathNode initialMidNode ( SourcePathNode src ) {
1047+ exists ( DataFlow:: Node nd , Configuration cfg , PathSummary summary |
1048+ result .wraps ( nd , cfg , summary ) and
1049+ src = MkSourceNode ( nd , cfg ) and
1050+ isSourceNode ( nd , cfg , summary )
1051+ )
1052+ }
1053+
1054+ /** Gets the mid node corresponding to `snk`. */
1055+ private MidPathNode finalMidNode ( SinkPathNode snk ) {
1056+ exists ( DataFlow:: Node nd , Configuration cfg , PathSummary summary |
1057+ result .wraps ( nd , cfg , summary ) and
1058+ snk = MkSinkNode ( nd , cfg ) and
1059+ isSinkNode ( nd , cfg , summary )
1060+ )
1061+ }
1062+
1063+ /**
1064+ * Gets a node to which data from `nd` may flow in one step.
1065+ */
1066+ private PathNode getASuccessor ( PathNode nd ) {
1067+ // source node to mid node
1068+ result = initialMidNode ( nd )
1069+ or
1070+ // mid node to mid node
1071+ exists ( Configuration cfg , DataFlow:: Node predNd , PathSummary summary , DataFlow:: Node succNd , PathSummary newSummary |
1072+ nd = MkMidNode ( predNd , cfg , summary ) and
1073+ flowStep ( predNd , id ( cfg ) , succNd , newSummary ) and
1074+ result = MkMidNode ( succNd , id ( cfg ) , summary .append ( newSummary ) )
1075+ )
1076+ or
1077+ // mid node to sink node
1078+ nd = finalMidNode ( result )
1079+ }
1080+
1081+ private PathNode getASuccessorIfHidden ( PathNode nd ) {
1082+ nd .( MidPathNode ) .isHidden ( ) and
1083+ result = getASuccessor ( nd )
1084+ }
1085+
1086+ /**
1087+ * A path node corresponding to an intermediate node on a path from a source to a sink.
1088+ *
1089+ * A mid node is a triple `(nd, cfg, summary)` where `nd` is a data-flow node and `cfg`
1090+ * is a configuration such that `nd` is on a path from a source to a sink under `cfg`
1091+ * summarized by `summary`.
1092+ */
1093+ class MidPathNode extends PathNode , MkMidNode {
1094+ PathSummary summary ;
1095+
1096+ MidPathNode ( ) { this = MkMidNode ( nd , cfg , summary ) }
1097+
1098+ /** Gets the summary of the path underlying this path node. */
1099+ PathSummary getPathSummary ( ) { result = summary }
1100+
1101+ /** Holds if this path node wraps data-flow node `nd`, configuration `c` and summary `s`. */
1102+ predicate wraps ( DataFlow:: Node n , DataFlow:: Configuration c , PathSummary s ) {
1103+ nd = n and cfg = c and summary = s
1104+ }
10181105
10191106 /**
10201107 * Holds if this node is hidden from paths in path explanation queries, except
@@ -1034,20 +1121,15 @@ class PathNode extends TPathNode {
10341121/**
10351122 * A path node corresponding to a flow source.
10361123 */
1037- class SourcePathNode extends PathNode {
1038- SourcePathNode ( ) {
1039- exists ( FlowLabel lbl |
1040- summary = PathSummary:: level ( lbl ) and
1041- isSource ( nd , cfg , lbl )
1042- )
1043- }
1124+ class SourcePathNode extends PathNode , MkSourceNode {
1125+ SourcePathNode ( ) { this = MkSourceNode ( nd , cfg ) }
10441126}
10451127
10461128/**
10471129 * A path node corresponding to a flow sink.
10481130 */
1049- class SinkPathNode extends PathNode {
1050- SinkPathNode ( ) { isSink ( nd , cfg , summary . getEndLabel ( ) ) }
1131+ class SinkPathNode extends PathNode , MkSinkNode {
1132+ SinkPathNode ( ) { this = MkSinkNode ( nd , cfg ) }
10511133}
10521134
10531135/**
@@ -1056,11 +1138,51 @@ class SinkPathNode extends PathNode {
10561138module PathGraph {
10571139 /** Holds if `nd` is a node in the graph of data flow path explanations. */
10581140 query predicate nodes ( PathNode nd ) {
1059- not nd .isHidden ( ) or
1060- nd instanceof SourcePathNode or
1061- nd instanceof SinkPathNode
1141+ not nd .( MidPathNode ) .isHidden ( )
1142+ }
1143+
1144+ /**
1145+ * Gets a node to which data from `nd` may flow in one step, skipping over hidden nodes.
1146+ */
1147+ private PathNode succ0 ( PathNode nd ) {
1148+ result = getASuccessorIfHidden * ( nd .getASuccessor ( ) ) and
1149+ // skip hidden nodes
1150+ nodes ( nd ) and nodes ( result )
1151+ }
1152+
1153+ /**
1154+ * Gets a node to which data from `nd` may flow in one step, where outgoing edges from intermediate
1155+ * nodes are merged with any incoming edge from a corresponding source node.
1156+ *
1157+ * For example, assume that `src` is a source node for `nd1`, which has `nd2` as its direct
1158+ * successor. Then `succ0` will yield two edges `src` → `nd1` and `nd1` → `nd2`,
1159+ * to which `succ1` will add the edge `src` → `nd2`.
1160+ */
1161+ private PathNode succ1 ( PathNode nd ) {
1162+ result = succ0 ( nd )
1163+ or
1164+ result = succ0 ( initialMidNode ( nd ) )
1165+ }
1166+
1167+ /**
1168+ * Gets a node to which data from `nd` may flow in one step, where incoming edges into intermediate
1169+ * nodes are merged with any outgoing edge to a corresponding sink node.
1170+ *
1171+ * For example, assume that `snk` is a source node for `nd2`, which has `nd1` as its direct
1172+ * predecessor. Then `succ1` will yield two edges `nd1` → `nd2` and `nd2` → `snk`,
1173+ * while `succ2` will yield just one edge `nd1` → `snk`.
1174+ */
1175+ private PathNode succ2 ( PathNode nd ) {
1176+ result = succ1 ( nd )
1177+ or
1178+ succ1 ( nd ) = finalMidNode ( result )
10621179 }
10631180
10641181 /** Holds if `pred` → `succ` is an edge in the graph of data flow path explanations. */
1065- query predicate edges ( PathNode pred , PathNode succ ) { pred .getASuccessor ( ) = succ }
1182+ query predicate edges ( PathNode pred , PathNode succ ) {
1183+ succ = succ2 ( pred ) and
1184+ // skip over uninteresting edges
1185+ not succ = initialMidNode ( pred ) and
1186+ not pred = finalMidNode ( succ )
1187+ }
10661188}
0 commit comments