@@ -478,16 +478,14 @@ module TypeTracking<TypeTrackingInput I> {
478
478
}
479
479
480
480
pragma [ nomagic]
481
- private predicate smallStepProj ( LocalSourceNode nodeFrom , StepSummary summary ) {
481
+ private predicate smallStepProj ( Node nodeFrom , StepSummary summary ) {
482
482
smallStep ( nodeFrom , _, summary )
483
483
}
484
484
485
485
bindingset [ t, nodeFrom]
486
486
pragma [ inline_late]
487
487
pragma [ noopt]
488
- private TypeTracker smallStepInlineLate (
489
- TypeTracker t , LocalSourceNode nodeFrom , LocalSourceNode nodeTo
490
- ) {
488
+ private TypeTracker smallStepInlineLate ( TypeTracker t , Node nodeFrom , LocalSourceNode nodeTo ) {
491
489
exists ( StepSummary summary |
492
490
smallStepProj ( nodeFrom , summary ) and
493
491
result = append ( t , summary ) and
@@ -657,7 +655,7 @@ module TypeTracking<TypeTrackingInput I> {
657
655
pragma [ inline_late]
658
656
pragma [ noopt]
659
657
private TypeBackTracker backSmallStepInlineLate (
660
- TypeBackTracker t , LocalSourceNode nodeFrom , LocalSourceNode nodeTo
658
+ TypeBackTracker t , Node nodeFrom , LocalSourceNode nodeTo
661
659
) {
662
660
exists ( StepSummary summary |
663
661
backSmallStepProj ( nodeTo , summary ) and
@@ -803,16 +801,35 @@ module TypeTracking<TypeTrackingInput I> {
803
801
* those sources.
804
802
*/
805
803
module TypeTrack< endpoint / 1 source> {
804
+ pragma [ nomagic]
805
+ private predicate sourceSimpleLocalSmallSteps ( Node src , Node n ) {
806
+ source ( src ) and
807
+ not src instanceof LocalSourceNode and
808
+ simpleLocalSmallStep * ( src , n )
809
+ }
810
+
811
+ private predicate firstStep ( TypeTracker tt , Node src , LocalSourceNode n2 ) {
812
+ exists ( Node n1 , TypeTracker tt0 |
813
+ sourceSimpleLocalSmallSteps ( src , n1 ) and
814
+ tt0 .start ( ) and
815
+ tt = smallStepInlineLate ( tt0 , n1 , n2 )
816
+ )
817
+ }
818
+
806
819
private Node flow ( TypeTracker tt ) {
807
820
tt .start ( ) and source ( result )
808
821
or
822
+ firstStep ( tt , _, result )
823
+ or
809
824
exists ( TypeTracker ttMid | tt = ttMid .step ( flow ( ttMid ) , result ) )
810
825
}
811
826
812
827
/**
813
- * Holds if the given source flows to `n`.
828
+ * Holds if a source flows to `n`.
814
829
*/
815
- predicate flowsTo ( Node n ) { flowsTo ( flow ( TypeTracker:: end ( ) ) , n ) }
830
+ predicate flowsTo ( Node n ) {
831
+ flowsTo ( flow ( TypeTracker:: end ( ) ) , n ) or sourceSimpleLocalSmallSteps ( _, n )
832
+ }
816
833
817
834
/**
818
835
* Given a sink definition, constructs the relation of edges that can be used
@@ -849,15 +866,22 @@ module TypeTracking<TypeTrackingInput I> {
849
866
string toString ( ) { result = this .getNode ( ) .toString ( ) + this .ppContent ( ) }
850
867
851
868
/** Holds if this is a source. */
852
- predicate isSource ( ) { source ( this .getNode ( ) ) and this .getTypeTracker ( ) .start ( ) }
869
+ predicate isSource ( ) {
870
+ source ( this .getNode ( ) ) and
871
+ ( this .getTypeTracker ( ) .start ( ) or this instanceof TPathNodeSink )
872
+ }
853
873
854
874
/** Holds if this is a sink. */
855
875
predicate isSink ( ) { this instanceof TPathNodeSink }
856
876
}
857
877
858
878
private predicate edgeCand ( Node n1 , TypeTracker tt1 , Node n2 , TypeTracker tt2 ) {
859
879
n1 = flow ( tt1 ) and
860
- tt2 = tt1 .step ( n1 , n2 )
880
+ (
881
+ tt2 = tt1 .step ( n1 , n2 )
882
+ or
883
+ tt1 .start ( ) and firstStep ( tt2 , n1 , n2 )
884
+ )
861
885
}
862
886
863
887
private predicate edgeCand ( PathNodeFwd n1 , PathNodeFwd n2 ) {
@@ -871,7 +895,13 @@ module TypeTracking<TypeTrackingInput I> {
871
895
or
872
896
n1 .getTypeTracker ( ) .end ( ) and
873
897
flowsTo ( n1 .getNode ( ) , n2 .getNode ( ) ) and
898
+ n1 .getNode ( ) != n2 .getNode ( ) and
874
899
n2 instanceof TPathNodeSink
900
+ or
901
+ sourceSimpleLocalSmallSteps ( n1 .getNode ( ) , n2 .getNode ( ) ) and
902
+ n1 .getNode ( ) != n2 .getNode ( ) and
903
+ n1 .isSource ( ) and
904
+ n2 .isSink ( )
875
905
}
876
906
877
907
private predicate reachRev ( PathNodeFwd n ) {
@@ -896,8 +926,15 @@ module TypeTracking<TypeTrackingInput I> {
896
926
897
927
private predicate stepPlus ( PathNode n1 , PathNode n2 ) = fastTC( edges / 2 ) ( n1 , n2 )
898
928
929
+ /**
930
+ * DEPRECATED: Use `flowPath` instead.
931
+ *
932
+ * Holds if there is a path between `source` and `sink`.
933
+ */
934
+ deprecated predicate hasFlow ( PathNode source , PathNode sink ) { flowPath ( source , sink ) }
935
+
899
936
/** Holds if there is a path between `source` and `sink`. */
900
- predicate hasFlow ( PathNode source , PathNode sink ) {
937
+ predicate flowPath ( PathNode source , PathNode sink ) {
901
938
source .isSource ( ) and
902
939
sink .isSink ( ) and
903
940
( source = sink or stepPlus ( source , sink ) )
0 commit comments