@@ -861,22 +861,6 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
861861 // non-sink PathNode with the same `(node, toString)` value and the same successors, but is transitively
862862 // reachable from a different set of PathNodes. (And conversely for sources).
863863 //
864- /**
865- * Gets a successor of `node`, taking `subpaths` into account.
866- */
867- private InputPathNode getASuccessorLike ( InputPathNode node ) {
868- Graph:: edges ( node , result )
869- or
870- Graph:: subpaths ( node , _, _, result ) // arg -> out
871- //
872- // Note that there is no case for `arg -> param` or `ret -> out` for subpaths.
873- // It is OK to collapse nodes inside a subpath while calls to that subpaths aren't collapsed and vice versa.
874- }
875-
876- private InputPathNode getAPredecessorLike ( InputPathNode node ) {
877- node = getASuccessorLike ( result )
878- }
879-
880864 pragma [ nomagic]
881865 private InputPathNode getAPathNode ( Node node , string toString ) {
882866 result .getNode ( ) = node and
@@ -885,7 +869,11 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
885869
886870 private signature predicate collapseCandidateSig ( Node node , string toString ) ;
887871
888- private signature InputPathNode stepSig ( InputPathNode node ) ;
872+ private signature predicate stepSig ( InputPathNode node1 , InputPathNode node2 ) ;
873+
874+ private signature predicate subpathStepSig (
875+ InputPathNode arg , InputPathNode param , InputPathNode ret , InputPathNode out
876+ ) ;
889877
890878 /**
891879 * Performs a forward or backward pass computing which `(node, toString)` pairs can subsume their corresponding
@@ -898,12 +886,14 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
898886 * Comments are written as if this checks for outgoing edges and propagates backward, though the module is also
899887 * used to perform the opposite direction.
900888 */
901- private module MakeDiscriminatorPass< collapseCandidateSig / 2 collapseCandidate, stepSig / 1 step> {
889+ private module MakeDiscriminatorPass<
890+ collapseCandidateSig / 2 collapseCandidate, stepSig / 2 step, subpathStepSig / 4 subpathStep>
891+ {
902892 /**
903893 * Gets the number of `(node, toString)` pairs reachable in one step from `pathNode`.
904894 */
905895 private int getOutDegreeFromPathNode ( InputPathNode pathNode ) {
906- result = count ( Node node , string toString | step ( pathNode ) = getAPathNode ( node , toString ) )
896+ result = count ( Node node , string toString | step ( pathNode , getAPathNode ( node , toString ) ) )
907897 }
908898
909899 /**
@@ -912,13 +902,46 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
912902 private int getOutDegreeFromNode ( Node node , string toString ) {
913903 result =
914904 strictcount ( Node node2 , string toString2 |
915- step ( getAPathNode ( node , toString ) ) = getAPathNode ( node2 , toString2 )
905+ step ( getAPathNode ( node , toString ) , getAPathNode ( node2 , toString2 ) )
916906 )
917907 }
918908
909+ /**
910+ * Like `getOutDegreeFromPathNode` except counts `subpath` tuples.
911+ */
912+ private int getSubpathOutDegreeFromPathNode ( InputPathNode pathNode ) {
913+ result =
914+ count ( Node n1 , string s1 , Node n2 , string s2 , Node n3 , string s3 |
915+ subpathStep ( pathNode , getAPathNode ( n1 , s1 ) , getAPathNode ( n2 , s2 ) , getAPathNode ( n3 , s3 ) )
916+ )
917+ }
918+
919+ /**
920+ * Like `getOutDegreeFromNode` except counts `subpath` tuples.
921+ */
922+ private int getSubpathOutDegreeFromNode ( Node node , string toString ) {
923+ result =
924+ strictcount ( Node n1 , string s1 , Node n2 , string s2 , Node n3 , string s3 |
925+ subpathStep ( getAPathNode ( node , toString ) , getAPathNode ( n1 , s1 ) , getAPathNode ( n2 , s2 ) ,
926+ getAPathNode ( n3 , s3 ) )
927+ )
928+ }
929+
930+ /** Gets a successor of `node` including subpath flow-through. */
931+ InputPathNode stepEx ( InputPathNode node ) {
932+ step ( node , result )
933+ or
934+ subpathStep ( node , _, _, result ) // assuming the input is pruned properly, all subpaths have flow-through
935+ }
936+
937+ InputPathNode enterSubpathStep ( InputPathNode node ) { subpathStep ( node , result , _, _) }
938+
939+ InputPathNode exitSubpathStep ( InputPathNode node ) { subpathStep ( _, _, node , result ) }
940+
919941 /** Holds if `(node, toString)` cannot be collapsed (but was a candidate for being collapsed). */
920- predicate discriminatedPair ( Node node , string toString ) {
942+ predicate discriminatedPair ( Node node , string toString , boolean hasEnter ) {
921943 collapseCandidate ( node , toString ) and
944+ hasEnter = false and
922945 (
923946 // Check if all corresponding PathNodes have the same successor sets when projected to `(node, toString)`.
924947 // To do this, we check that each successor set has the same size as the union of the succesor sets.
@@ -928,27 +951,62 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
928951 getOutDegreeFromPathNode ( getAPathNode ( node , toString ) ) <
929952 getOutDegreeFromNode ( node , toString )
930953 or
954+ // Same as above but counting associated subpath triples instead
955+ getSubpathOutDegreeFromPathNode ( getAPathNode ( node , toString ) ) <
956+ getSubpathOutDegreeFromNode ( node , toString )
957+ )
958+ or
959+ collapseCandidate ( node , toString ) and
960+ (
931961 // Retain flow state if one of the successors requires it to be retained
932- discriminatedPathNode ( step ( getAPathNode ( node , toString ) ) )
962+ discriminatedPathNode ( stepEx ( getAPathNode ( node , toString ) ) , hasEnter )
963+ or
964+ // Enter a subpath
965+ discriminatedPathNode ( enterSubpathStep ( getAPathNode ( node , toString ) ) , _) and
966+ hasEnter = true
967+ or
968+ // Exit a subpath
969+ discriminatedPathNode ( exitSubpathStep ( getAPathNode ( node , toString ) ) , false ) and
970+ hasEnter = false
933971 )
934972 }
935973
936974 /** Holds if `pathNode` cannot be collapsed. */
937- predicate discriminatedPathNode ( InputPathNode pathNode ) {
975+ private predicate discriminatedPathNode ( InputPathNode pathNode , boolean hasEnter ) {
938976 exists ( Node node , string toString |
939- discriminatedPair ( node , toString ) and
977+ discriminatedPair ( node , toString , hasEnter ) and
940978 getAPathNode ( node , toString ) = pathNode
941979 )
942980 }
981+
982+ /** Holds if `(node, toString)` cannot be collapsed (but was a candidate for being collapsed). */
983+ predicate discriminatedPair ( Node node , string toString ) {
984+ discriminatedPair ( node , toString , _)
985+ }
986+
987+ /** Holds if `pathNode` cannot be collapsed. */
988+ predicate discriminatedPathNode ( InputPathNode pathNode ) { discriminatedPathNode ( pathNode , _) }
943989 }
944990
945991 private predicate initialCandidate ( Node node , string toString ) {
946992 exists ( getAPathNode ( node , toString ) )
947993 }
948994
949- private module Pass1 = MakeDiscriminatorPass< initialCandidate / 2 , getASuccessorLike / 1 > ;
995+ private module Pass1 =
996+ MakeDiscriminatorPass< initialCandidate / 2 , Graph:: edges / 2 , Graph:: subpaths / 4 > ;
997+
998+ private predicate edgesRev ( InputPathNode node1 , InputPathNode node2 ) {
999+ Graph:: edges ( node2 , node1 )
1000+ }
1001+
1002+ private predicate subpathsRev (
1003+ InputPathNode n1 , InputPathNode n2 , InputPathNode n3 , InputPathNode n4
1004+ ) {
1005+ Graph:: subpaths ( n4 , n3 , n2 , n1 )
1006+ }
9501007
951- private module Pass2 = MakeDiscriminatorPass< Pass1:: discriminatedPair / 2 , getAPredecessorLike / 1 > ;
1008+ private module Pass2 =
1009+ MakeDiscriminatorPass< Pass1:: discriminatedPair / 2 , edgesRev / 2 , subpathsRev / 4 > ;
9521010
9531011 private newtype TPathNode =
9541012 TPreservedPathNode ( InputPathNode node ) { Pass2:: discriminatedPathNode ( node ) } or
0 commit comments