@@ -99,7 +99,7 @@ module Public {
99
99
exists ( SummaryComponent head , SummaryComponentStack tail |
100
100
head = this .head ( ) and
101
101
tail = this .tail ( ) and
102
- result = head + " of " + tail
102
+ result = tail + ". " + head
103
103
)
104
104
or
105
105
exists ( SummaryComponent c |
@@ -164,7 +164,7 @@ module Public {
164
164
exists ( SummaryComponent head , SummaryComponentStack tail |
165
165
head = stack .head ( ) and
166
166
tail = stack .tail ( ) and
167
- result = getComponentCsv ( head ) + " of " + getComponentStackCsv ( tail )
167
+ result = getComponentStackCsv ( tail ) + ". " + getComponentCsv ( head )
168
168
)
169
169
or
170
170
exists ( SummaryComponent c |
@@ -228,6 +228,7 @@ module Public {
228
228
*/
229
229
module Private {
230
230
private import Public
231
+ import AccessPathSyntax
231
232
232
233
newtype TSummaryComponent =
233
234
TContentSummaryComponent ( Content c ) or
@@ -811,84 +812,60 @@ module Private {
811
812
sinkElement ( _, spec , _)
812
813
}
813
814
814
- /** Holds if the `n`th component of specification `s` is `c`. */
815
- predicate specSplit ( string s , string c , int n ) { relevantSpec ( s ) and s .splitAt ( " of " , n ) = c }
816
-
817
- /** Holds if specification `s` has length `len`. */
818
- predicate specLength ( string s , int len ) { len = 1 + max ( int n | specSplit ( s , _, n ) ) }
819
-
820
- /** Gets the last component of specification `s`. */
821
- string specLast ( string s ) {
822
- exists ( int len |
823
- specLength ( s , len ) and
824
- specSplit ( s , result , len - 1 )
825
- )
815
+ private class AccessPathRange extends AccessPath:: Range {
816
+ AccessPathRange ( ) { relevantSpec ( this ) }
826
817
}
827
818
828
819
/** Holds if specification component `c` parses as parameter `n`. */
829
- predicate parseParam ( string c , ArgumentPosition pos ) {
830
- specSplit ( _, c , _) and
831
- exists ( string body |
832
- body = c .regexpCapture ( "Parameter\\[([^\\]]*)\\]" , 1 ) and
833
- pos = parseParamBody ( body )
834
- )
820
+ predicate parseParam ( AccessPathToken token , ArgumentPosition pos ) {
821
+ token .getName ( ) = "Parameter" and
822
+ pos = parseParamBody ( token .getAnArgument ( ) )
835
823
}
836
824
837
825
/** Holds if specification component `c` parses as argument `n`. */
838
- predicate parseArg ( string c , ParameterPosition pos ) {
839
- specSplit ( _, c , _) and
840
- exists ( string body |
841
- body = c .regexpCapture ( "Argument\\[([^\\]]*)\\]" , 1 ) and
842
- pos = parseArgBody ( body )
843
- )
826
+ predicate parseArg ( AccessPathToken token , ParameterPosition pos ) {
827
+ token .getName ( ) = "Argument" and
828
+ pos = parseArgBody ( token .getAnArgument ( ) )
844
829
}
845
830
846
- private SummaryComponent interpretComponent ( string c ) {
847
- specSplit ( _, c , _) and
848
- (
849
- exists ( ParameterPosition pos |
850
- parseArg ( c , pos ) and result = SummaryComponent:: argument ( pos )
851
- )
852
- or
853
- exists ( ArgumentPosition pos |
854
- parseParam ( c , pos ) and result = SummaryComponent:: parameter ( pos )
855
- )
856
- or
857
- c = "ReturnValue" and result = SummaryComponent:: return ( getReturnValueKind ( ) )
858
- or
859
- result = interpretComponentSpecific ( c )
831
+ private SummaryComponent interpretComponent ( AccessPathToken token ) {
832
+ exists ( ParameterPosition pos |
833
+ parseArg ( token , pos ) and result = SummaryComponent:: argument ( pos )
860
834
)
835
+ or
836
+ exists ( ArgumentPosition pos |
837
+ parseParam ( token , pos ) and result = SummaryComponent:: parameter ( pos )
838
+ )
839
+ or
840
+ token = "ReturnValue" and result = SummaryComponent:: return ( getReturnValueKind ( ) )
841
+ or
842
+ result = interpretComponentSpecific ( token )
861
843
}
862
844
863
845
/**
864
846
* Holds if `spec` specifies summary component stack `stack`.
865
847
*/
866
- predicate interpretSpec ( string spec , SummaryComponentStack stack ) {
867
- interpretSpec ( spec , 0 , stack )
848
+ predicate interpretSpec ( AccessPath spec , SummaryComponentStack stack ) {
849
+ interpretSpec ( spec , spec . getNumToken ( ) , stack )
868
850
}
869
851
870
- private predicate interpretSpec ( string spec , int idx , SummaryComponentStack stack ) {
871
- exists ( string c |
872
- relevantSpec ( spec ) and
873
- specLength ( spec , idx + 1 ) and
874
- specSplit ( spec , c , idx ) and
875
- stack = SummaryComponentStack:: singleton ( interpretComponent ( c ) )
876
- )
852
+ /** Holds if the first `n` tokens of `spec` resolves to `stack`. */
853
+ private predicate interpretSpec ( AccessPath spec , int n , SummaryComponentStack stack ) {
854
+ n = 1 and
855
+ stack = SummaryComponentStack:: singleton ( interpretComponent ( spec .getToken ( 0 ) ) )
877
856
or
878
857
exists ( SummaryComponent head , SummaryComponentStack tail |
879
- interpretSpec ( spec , idx , head , tail ) and
858
+ interpretSpec ( spec , n , head , tail ) and
880
859
stack = SummaryComponentStack:: push ( head , tail )
881
860
)
882
861
}
883
862
863
+ /** Holds if the first `n` tokens of `spec` resolves to `head` followed by `tail` */
884
864
private predicate interpretSpec (
885
- string output , int idx , SummaryComponent head , SummaryComponentStack tail
865
+ AccessPath spec , int n , SummaryComponent head , SummaryComponentStack tail
886
866
) {
887
- exists ( string c |
888
- interpretSpec ( output , idx + 1 , tail ) and
889
- specSplit ( output , c , idx ) and
890
- head = interpretComponent ( c )
891
- )
867
+ interpretSpec ( spec , n - 1 , tail ) and
868
+ head = interpretComponent ( spec .getToken ( n - 1 ) )
892
869
}
893
870
894
871
private class MkStack extends RequiredSummaryComponentStack {
@@ -903,7 +880,7 @@ module Private {
903
880
override predicate propagatesFlow (
904
881
SummaryComponentStack input , SummaryComponentStack output , boolean preservesValue
905
882
) {
906
- exists ( string inSpec , string outSpec , string kind |
883
+ exists ( AccessPath inSpec , AccessPath outSpec , string kind |
907
884
summaryElement ( this , inSpec , outSpec , kind ) and
908
885
interpretSpec ( inSpec , input ) and
909
886
interpretSpec ( outSpec , output )
@@ -916,50 +893,56 @@ module Private {
916
893
}
917
894
918
895
/** Holds if component `c` of specification `spec` cannot be parsed. */
919
- predicate invalidSpecComponent ( string spec , string c ) {
920
- specSplit ( spec , c , _) and
896
+ predicate invalidSpecComponent ( AccessPath spec , string c ) {
897
+ c = spec . getToken ( _) and
921
898
not exists ( interpretComponent ( c ) )
922
899
}
923
900
924
- private predicate inputNeedsReference ( string c ) {
925
- c = "Argument" or
926
- parseArg ( c , _) or
901
+ private predicate inputNeedsReference ( AccessPathToken c ) {
902
+ c .getName ( ) = "Argument" or
927
903
inputNeedsReferenceSpecific ( c )
928
904
}
929
905
930
- private predicate outputNeedsReference ( string c ) {
931
- c = "Argument" or
932
- parseArg ( c , _) or
933
- c = "ReturnValue" or
906
+ private predicate outputNeedsReference ( AccessPathToken c ) {
907
+ c .getName ( ) = [ "Argument" , "ReturnValue" ] or
934
908
outputNeedsReferenceSpecific ( c )
935
909
}
936
910
937
- private predicate sourceElementRef ( InterpretNode ref , string output , string kind ) {
911
+ private predicate sourceElementRef ( InterpretNode ref , AccessPath output , string kind ) {
938
912
exists ( SourceOrSinkElement e |
939
913
sourceElement ( e , output , kind ) and
940
- if outputNeedsReference ( specLast ( output ) )
914
+ if outputNeedsReference ( output . getToken ( 0 ) )
941
915
then e = ref .getCallTarget ( )
942
916
else e = ref .asElement ( )
943
917
)
944
918
}
945
919
946
- private predicate sinkElementRef ( InterpretNode ref , string input , string kind ) {
920
+ private predicate sinkElementRef ( InterpretNode ref , AccessPath input , string kind ) {
947
921
exists ( SourceOrSinkElement e |
948
922
sinkElement ( e , input , kind ) and
949
- if inputNeedsReference ( specLast ( input ) )
923
+ if inputNeedsReference ( input . getToken ( 0 ) )
950
924
then e = ref .getCallTarget ( )
951
925
else e = ref .asElement ( )
952
926
)
953
927
}
954
928
955
- private predicate interpretOutput ( string output , int idx , InterpretNode ref , InterpretNode node ) {
929
+ /** Holds if the first `n` tokens of `output` resolve to the given interpretation. */
930
+ private predicate interpretOutput (
931
+ AccessPath output , int n , InterpretNode ref , InterpretNode node
932
+ ) {
956
933
sourceElementRef ( ref , output , _) and
957
- specLength ( output , idx ) and
958
- node = ref
934
+ n = 0 and
935
+ (
936
+ if output = ""
937
+ then
938
+ // Allow language-specific interpretation of the empty access path
939
+ interpretOutputSpecific ( "" , ref , node )
940
+ else node = ref
941
+ )
959
942
or
960
- exists ( InterpretNode mid , string c |
961
- interpretOutput ( output , idx + 1 , ref , mid ) and
962
- specSplit ( output , c , idx )
943
+ exists ( InterpretNode mid , AccessPathToken c |
944
+ interpretOutput ( output , n - 1 , ref , mid ) and
945
+ c = output . getToken ( n - 1 )
963
946
|
964
947
exists ( ArgumentPosition apos , ParameterPosition ppos |
965
948
node .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) .( ArgNode ) .argumentOf ( mid .asCall ( ) , apos ) and
@@ -982,14 +965,21 @@ module Private {
982
965
)
983
966
}
984
967
985
- private predicate interpretInput ( string input , int idx , InterpretNode ref , InterpretNode node ) {
968
+ /** Holds if the first `n` tokens of `input` resolve to the given interpretation. */
969
+ private predicate interpretInput ( AccessPath input , int n , InterpretNode ref , InterpretNode node ) {
986
970
sinkElementRef ( ref , input , _) and
987
- specLength ( input , idx ) and
988
- node = ref
971
+ n = 0 and
972
+ (
973
+ if input = ""
974
+ then
975
+ // Allow language-specific interpretation of the empty access path
976
+ interpretInputSpecific ( "" , ref , node )
977
+ else node = ref
978
+ )
989
979
or
990
- exists ( InterpretNode mid , string c |
991
- interpretInput ( input , idx + 1 , ref , mid ) and
992
- specSplit ( input , c , idx )
980
+ exists ( InterpretNode mid , AccessPathToken c |
981
+ interpretInput ( input , n - 1 , ref , mid ) and
982
+ c = input . getToken ( n - 1 )
993
983
|
994
984
exists ( ArgumentPosition apos , ParameterPosition ppos |
995
985
node .asNode ( ) .( ArgNode ) .argumentOf ( mid .asCall ( ) , apos ) and
@@ -1014,9 +1004,9 @@ module Private {
1014
1004
* model.
1015
1005
*/
1016
1006
predicate isSourceNode ( InterpretNode node , string kind ) {
1017
- exists ( InterpretNode ref , string output |
1007
+ exists ( InterpretNode ref , AccessPath output |
1018
1008
sourceElementRef ( ref , output , kind ) and
1019
- interpretOutput ( output , 0 , ref , node )
1009
+ interpretOutput ( output , output . getNumToken ( ) , ref , node )
1020
1010
)
1021
1011
}
1022
1012
@@ -1025,9 +1015,9 @@ module Private {
1025
1015
* model.
1026
1016
*/
1027
1017
predicate isSinkNode ( InterpretNode node , string kind ) {
1028
- exists ( InterpretNode ref , string input |
1018
+ exists ( InterpretNode ref , AccessPath input |
1029
1019
sinkElementRef ( ref , input , kind ) and
1030
- interpretInput ( input , 0 , ref , node )
1020
+ interpretInput ( input , input . getNumToken ( ) , ref , node )
1031
1021
)
1032
1022
}
1033
1023
}
0 commit comments