@@ -707,22 +707,6 @@ module DataFlowMake<InputSig Lang> {
707707 // non-sink PathNode with the same `(node, toString)` value and the same successors, but is transitively
708708 // reachable from a different set of PathNodes. (And conversely for sources).
709709 //
710- /**
711- * Gets a successor of `node`, taking `subpaths` into account.
712- */
713- private InputPathNode getASuccessorLike ( InputPathNode node ) {
714- Graph:: edges ( node , result )
715- or
716- Graph:: subpaths ( node , _, _, result ) // arg -> out
717- //
718- // Note that there is no case for `arg -> param` or `ret -> out` for subpaths.
719- // It is OK to collapse nodes inside a subpath while calls to that subpaths aren't collapsed and vice versa.
720- }
721-
722- private InputPathNode getAPredecessorLike ( InputPathNode node ) {
723- node = getASuccessorLike ( result )
724- }
725-
726710 pragma [ nomagic]
727711 private InputPathNode getAPathNode ( Node node , string toString ) {
728712 result .getNode ( ) = node and
@@ -731,7 +715,11 @@ module DataFlowMake<InputSig Lang> {
731715
732716 private signature predicate collapseCandidateSig ( Node node , string toString ) ;
733717
734- private signature InputPathNode stepSig ( InputPathNode node ) ;
718+ private signature predicate stepSig ( InputPathNode node1 , InputPathNode node2 ) ;
719+
720+ private signature predicate subpathStepSig (
721+ InputPathNode arg , InputPathNode param , InputPathNode ret , InputPathNode out
722+ ) ;
735723
736724 /**
737725 * Performs a forward or backward pass computing which `(node, toString)` pairs can subsume their corresponding
@@ -744,12 +732,14 @@ module DataFlowMake<InputSig Lang> {
744732 * Comments are written as if this checks for outgoing edges and propagates backward, though the module is also
745733 * used to perform the opposite direction.
746734 */
747- private module MakeDiscriminatorPass< collapseCandidateSig / 2 collapseCandidate, stepSig / 1 step> {
735+ private module MakeDiscriminatorPass<
736+ collapseCandidateSig / 2 collapseCandidate, stepSig / 2 step, subpathStepSig / 4 subpathStep>
737+ {
748738 /**
749739 * Gets the number of `(node, toString)` pairs reachable in one step from `pathNode`.
750740 */
751741 private int getOutDegreeFromPathNode ( InputPathNode pathNode ) {
752- result = count ( Node node , string toString | step ( pathNode ) = getAPathNode ( node , toString ) )
742+ result = count ( Node node , string toString | step ( pathNode , getAPathNode ( node , toString ) ) )
753743 }
754744
755745 /**
@@ -758,13 +748,46 @@ module DataFlowMake<InputSig Lang> {
758748 private int getOutDegreeFromNode ( Node node , string toString ) {
759749 result =
760750 strictcount ( Node node2 , string toString2 |
761- step ( getAPathNode ( node , toString ) ) = getAPathNode ( node2 , toString2 )
751+ step ( getAPathNode ( node , toString ) , getAPathNode ( node2 , toString2 ) )
752+ )
753+ }
754+
755+ /**
756+ * Like `getOutDegreeFromPathNode` except counts `subpath` tuples.
757+ */
758+ private int getSubpathOutDegreeFromPathNode ( InputPathNode pathNode ) {
759+ result =
760+ count ( Node n1 , string s1 , Node n2 , string s2 , Node n3 , string s3 |
761+ subpathStep ( pathNode , getAPathNode ( n1 , s1 ) , getAPathNode ( n2 , s2 ) , getAPathNode ( n3 , s3 ) )
762762 )
763763 }
764764
765+ /**
766+ * Like `getOutDegreeFromNode` except counts `subpath` tuples.
767+ */
768+ private int getSubpathOutDegreeFromNode ( Node node , string toString ) {
769+ result =
770+ strictcount ( Node n1 , string s1 , Node n2 , string s2 , Node n3 , string s3 |
771+ subpathStep ( getAPathNode ( node , toString ) , getAPathNode ( n1 , s1 ) , getAPathNode ( n2 , s2 ) ,
772+ getAPathNode ( n3 , s3 ) )
773+ )
774+ }
775+
776+ /** Gets a successor of `node` including subpath flow-through. */
777+ InputPathNode stepEx ( InputPathNode node ) {
778+ step ( node , result )
779+ or
780+ subpathStep ( node , _, _, result ) // assuming the input is pruned properly, all subpaths have flow-through
781+ }
782+
783+ InputPathNode enterSubpathStep ( InputPathNode node ) { subpathStep ( node , result , _, _) }
784+
785+ InputPathNode exitSubpathStep ( InputPathNode node ) { subpathStep ( _, _, node , result ) }
786+
765787 /** Holds if `(node, toString)` cannot be collapsed (but was a candidate for being collapsed). */
766- predicate discriminatedPair ( Node node , string toString ) {
788+ predicate discriminatedPair ( Node node , string toString , boolean hasEnter ) {
767789 collapseCandidate ( node , toString ) and
790+ hasEnter = false and
768791 (
769792 // Check if all corresponding PathNodes have the same successor sets when projected to `(node, toString)`.
770793 // To do this, we check that each successor set has the same size as the union of the succesor sets.
@@ -774,27 +797,62 @@ module DataFlowMake<InputSig Lang> {
774797 getOutDegreeFromPathNode ( getAPathNode ( node , toString ) ) <
775798 getOutDegreeFromNode ( node , toString )
776799 or
800+ // Same as above but counting associated subpath triples instead
801+ getSubpathOutDegreeFromPathNode ( getAPathNode ( node , toString ) ) <
802+ getSubpathOutDegreeFromNode ( node , toString )
803+ )
804+ or
805+ collapseCandidate ( node , toString ) and
806+ (
777807 // Retain flow state if one of the successors requires it to be retained
778- discriminatedPathNode ( step ( getAPathNode ( node , toString ) ) )
808+ discriminatedPathNode ( stepEx ( getAPathNode ( node , toString ) ) , hasEnter )
809+ or
810+ // Enter a subpath
811+ discriminatedPathNode ( enterSubpathStep ( getAPathNode ( node , toString ) ) , _) and
812+ hasEnter = true
813+ or
814+ // Exit a subpath
815+ discriminatedPathNode ( exitSubpathStep ( getAPathNode ( node , toString ) ) , false ) and
816+ hasEnter = false
779817 )
780818 }
781819
782820 /** Holds if `pathNode` cannot be collapsed. */
783- predicate discriminatedPathNode ( InputPathNode pathNode ) {
821+ private predicate discriminatedPathNode ( InputPathNode pathNode , boolean hasEnter ) {
784822 exists ( Node node , string toString |
785- discriminatedPair ( node , toString ) and
823+ discriminatedPair ( node , toString , hasEnter ) and
786824 getAPathNode ( node , toString ) = pathNode
787825 )
788826 }
827+
828+ /** Holds if `(node, toString)` cannot be collapsed (but was a candidate for being collapsed). */
829+ predicate discriminatedPair ( Node node , string toString ) {
830+ discriminatedPair ( node , toString , _)
831+ }
832+
833+ /** Holds if `pathNode` cannot be collapsed. */
834+ predicate discriminatedPathNode ( InputPathNode pathNode ) { discriminatedPathNode ( pathNode , _) }
789835 }
790836
791837 private predicate initialCandidate ( Node node , string toString ) {
792838 exists ( getAPathNode ( node , toString ) )
793839 }
794840
795- private module Pass1 = MakeDiscriminatorPass< initialCandidate / 2 , getASuccessorLike / 1 > ;
841+ private module Pass1 =
842+ MakeDiscriminatorPass< initialCandidate / 2 , Graph:: edges / 2 , Graph:: subpaths / 4 > ;
843+
844+ private predicate edgesRev ( InputPathNode node1 , InputPathNode node2 ) {
845+ Graph:: edges ( node2 , node1 )
846+ }
847+
848+ private predicate subpathsRev (
849+ InputPathNode n1 , InputPathNode n2 , InputPathNode n3 , InputPathNode n4
850+ ) {
851+ Graph:: subpaths ( n4 , n3 , n2 , n1 )
852+ }
796853
797- private module Pass2 = MakeDiscriminatorPass< Pass1:: discriminatedPair / 2 , getAPredecessorLike / 1 > ;
854+ private module Pass2 =
855+ MakeDiscriminatorPass< Pass1:: discriminatedPair / 2 , edgesRev / 2 , subpathsRev / 4 > ;
798856
799857 private newtype TPathNode =
800858 TPreservedPathNode ( InputPathNode node ) { Pass2:: discriminatedPathNode ( node ) } or
0 commit comments