@@ -846,24 +846,26 @@ module Private {
846
846
* Holds if `spec` specifies summary component stack `stack`.
847
847
*/
848
848
predicate interpretSpec ( AccessPath spec , SummaryComponentStack stack ) {
849
- interpretSpec ( spec , 0 , stack )
849
+ interpretSpec ( spec , spec . getNumToken ( ) , stack )
850
850
}
851
851
852
- private predicate interpretSpec ( AccessPath spec , int idx , SummaryComponentStack stack ) {
853
- idx = spec .getNumToken ( ) - 1 and
854
- stack = SummaryComponentStack:: singleton ( interpretComponent ( spec .getLastToken ( idx ) ) )
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 ) ) )
855
856
or
856
857
exists ( SummaryComponent head , SummaryComponentStack tail |
857
- interpretSpec ( spec , idx , head , tail ) and
858
+ interpretSpec ( spec , n , head , tail ) and
858
859
stack = SummaryComponentStack:: push ( head , tail )
859
860
)
860
861
}
861
862
863
+ /** Holds if the first `n` tokens of `spec` resolves to `head` followed by `tail` */
862
864
private predicate interpretSpec (
863
- AccessPath output , int idx , SummaryComponent head , SummaryComponentStack tail
865
+ AccessPath spec , int n , SummaryComponent head , SummaryComponentStack tail
864
866
) {
865
- interpretSpec ( output , idx + 1 , tail ) and
866
- head = interpretComponent ( output . getLastToken ( idx ) )
867
+ interpretSpec ( spec , n - 1 , tail ) and
868
+ head = interpretComponent ( spec . getToken ( n - 1 ) )
867
869
}
868
870
869
871
private class MkStack extends RequiredSummaryComponentStack {
@@ -924,11 +926,12 @@ module Private {
924
926
)
925
927
}
926
928
929
+ /** Holds if the first `n` tokens of `output` resolve to the given interpretation. */
927
930
private predicate interpretOutput (
928
- AccessPath output , int idx , InterpretNode ref , InterpretNode node
931
+ AccessPath output , int n , InterpretNode ref , InterpretNode node
929
932
) {
930
933
sourceElementRef ( ref , output , _) and
931
- idx = output . getNumToken ( ) and
934
+ n = 0 and
932
935
(
933
936
if output = ""
934
937
then
@@ -938,8 +941,8 @@ module Private {
938
941
)
939
942
or
940
943
exists ( InterpretNode mid , AccessPathToken c |
941
- interpretOutput ( output , idx + 1 , ref , mid ) and
942
- c = output .getLastToken ( idx )
944
+ interpretOutput ( output , n - 1 , ref , mid ) and
945
+ c = output .getToken ( n - 1 )
943
946
|
944
947
exists ( ArgumentPosition apos , ParameterPosition ppos |
945
948
node .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) .( ArgNode ) .argumentOf ( mid .asCall ( ) , apos ) and
@@ -962,11 +965,12 @@ module Private {
962
965
)
963
966
}
964
967
968
+ /** Holds if the first `n` tokens of `input` resolve to the given interpretation. */
965
969
private predicate interpretInput (
966
- AccessPath input , int idx , InterpretNode ref , InterpretNode node
970
+ AccessPath input , int n , InterpretNode ref , InterpretNode node
967
971
) {
968
972
sinkElementRef ( ref , input , _) and
969
- idx = input . getNumToken ( ) and
973
+ n = 0 and
970
974
(
971
975
if input = ""
972
976
then
@@ -976,8 +980,8 @@ module Private {
976
980
)
977
981
or
978
982
exists ( InterpretNode mid , AccessPathToken c |
979
- interpretInput ( input , idx + 1 , ref , mid ) and
980
- c = input .getLastToken ( idx )
983
+ interpretInput ( input , n - 1 , ref , mid ) and
984
+ c = input .getToken ( n - 1 )
981
985
|
982
986
exists ( ArgumentPosition apos , ParameterPosition ppos |
983
987
node .asNode ( ) .( ArgNode ) .argumentOf ( mid .asCall ( ) , apos ) and
@@ -1002,9 +1006,9 @@ module Private {
1002
1006
* model.
1003
1007
*/
1004
1008
predicate isSourceNode ( InterpretNode node , string kind ) {
1005
- exists ( InterpretNode ref , string output |
1009
+ exists ( InterpretNode ref , AccessPath output |
1006
1010
sourceElementRef ( ref , output , kind ) and
1007
- interpretOutput ( output , 0 , ref , node )
1011
+ interpretOutput ( output , output . getNumToken ( ) , ref , node )
1008
1012
)
1009
1013
}
1010
1014
@@ -1013,9 +1017,9 @@ module Private {
1013
1017
* model.
1014
1018
*/
1015
1019
predicate isSinkNode ( InterpretNode node , string kind ) {
1016
- exists ( InterpretNode ref , string input |
1020
+ exists ( InterpretNode ref , AccessPath input |
1017
1021
sinkElementRef ( ref , input , kind ) and
1018
- interpretInput ( input , 0 , ref , node )
1022
+ interpretInput ( input , input . getNumToken ( ) , ref , node )
1019
1023
)
1020
1024
}
1021
1025
}
0 commit comments