2
2
3
3
import csharp
4
4
private import internal.FlowSummaryImpl as Impl
5
- private import internal.DataFlowDispatch
5
+ private import internal.DataFlowDispatch as DataFlowDispatch
6
+
7
+ class ParameterPosition = DataFlowDispatch:: ParameterPosition ;
8
+
9
+ class ArgumentPosition = DataFlowDispatch:: ArgumentPosition ;
6
10
7
11
// import all instances below
8
12
private module Summaries {
@@ -14,7 +18,27 @@ class SummaryComponent = Impl::Public::SummaryComponent;
14
18
15
19
/** Provides predicates for constructing summary components. */
16
20
module SummaryComponent {
17
- import Impl:: Public:: SummaryComponent
21
+ private import Impl:: Public:: SummaryComponent as SummaryComponentInternal
22
+
23
+ predicate content = SummaryComponentInternal:: content / 1 ;
24
+
25
+ /** Gets a summary component for parameter `i`. */
26
+ SummaryComponent parameter ( int i ) {
27
+ exists ( ArgumentPosition pos |
28
+ result = SummaryComponentInternal:: parameter ( pos ) and
29
+ i = pos .getPosition ( )
30
+ )
31
+ }
32
+
33
+ /** Gets a summary component for argument `i`. */
34
+ SummaryComponent argument ( int i ) {
35
+ exists ( ParameterPosition pos |
36
+ result = SummaryComponentInternal:: argument ( pos ) and
37
+ i = pos .getPosition ( )
38
+ )
39
+ }
40
+
41
+ predicate return = SummaryComponentInternal:: return / 1 ;
18
42
19
43
/** Gets a summary component that represents a qualifier. */
20
44
SummaryComponent qualifier ( ) { result = argument ( - 1 ) }
@@ -33,14 +57,14 @@ module SummaryComponent {
33
57
}
34
58
35
59
/** Gets a summary component that represents the return value of a call. */
36
- SummaryComponent return ( ) { result = return ( any ( NormalReturnKind rk ) ) }
60
+ SummaryComponent return ( ) { result = return ( any ( DataFlowDispatch :: NormalReturnKind rk ) ) }
37
61
38
62
/** Gets a summary component that represents a jump to `c`. */
39
63
SummaryComponent jump ( Callable c ) {
40
64
result =
41
- return ( any ( JumpReturnKind jrk |
65
+ return ( any ( DataFlowDispatch :: JumpReturnKind jrk |
42
66
jrk .getTarget ( ) = c .getUnboundDeclaration ( ) and
43
- jrk .getTargetReturnKind ( ) instanceof NormalReturnKind
67
+ jrk .getTargetReturnKind ( ) instanceof DataFlowDispatch :: NormalReturnKind
44
68
) )
45
69
}
46
70
}
@@ -49,7 +73,16 @@ class SummaryComponentStack = Impl::Public::SummaryComponentStack;
49
73
50
74
/** Provides predicates for constructing stacks of summary components. */
51
75
module SummaryComponentStack {
52
- import Impl:: Public:: SummaryComponentStack
76
+ private import Impl:: Public:: SummaryComponentStack as SummaryComponentStackInternal
77
+
78
+ predicate singleton = SummaryComponentStackInternal:: singleton / 1 ;
79
+
80
+ predicate push = SummaryComponentStackInternal:: push / 2 ;
81
+
82
+ /** Gets a singleton stack for argument `i`. */
83
+ SummaryComponentStack argument ( int i ) { result = singleton ( SummaryComponent:: argument ( i ) ) }
84
+
85
+ predicate return = SummaryComponentStackInternal:: return / 1 ;
53
86
54
87
/** Gets a singleton stack representing a qualifier. */
55
88
SummaryComponentStack qualifier ( ) { result = singleton ( SummaryComponent:: qualifier ( ) ) }
@@ -84,12 +117,12 @@ private class SummarizedCallableDefaultClearsContent extends Impl::Public::Summa
84
117
}
85
118
86
119
// By default, we assume that all stores into arguments are definite
87
- override predicate clearsContent ( int i , DataFlow:: Content content ) {
120
+ override predicate clearsContent ( ParameterPosition pos , DataFlow:: Content content ) {
88
121
exists ( SummaryComponentStack output |
89
122
this .propagatesFlow ( _, output , _) and
90
123
output .drop ( _) =
91
124
SummaryComponentStack:: push ( SummaryComponent:: content ( content ) ,
92
- SummaryComponentStack:: argument ( i ) ) and
125
+ SummaryComponentStack:: argument ( pos . getPosition ( ) ) ) and
93
126
not content instanceof DataFlow:: ElementContent
94
127
)
95
128
}
0 commit comments