@@ -3,6 +3,276 @@ import experimental.ir.implementation.IRConfiguration
3
3
import experimental.ir.internal.IntegerConstant as Ints
4
4
5
5
module AliasModels {
6
+ class ParameterIndex = int ;
7
+
8
+ /**
9
+ * An input to a function. This can be:
10
+ * - The value of one of the function's parameters
11
+ * - The value pointed to by one of function's pointer or reference parameters
12
+ * - The value of the function's `this` pointer
13
+ * - The value pointed to by the function's `this` pointer
14
+ */
15
+ abstract class FunctionInput extends string {
16
+ FunctionInput ( ) { none ( ) }
17
+
18
+ /**
19
+ * Holds if this is the input value of the parameter with index `index`.
20
+ *
21
+ * Example:
22
+ * ```
23
+ * void func(int n, char* p, float& r);
24
+ * ```
25
+ * - `isParameter(0)` holds for the `FunctionInput` that represents the value of `n` (with type
26
+ * `int`) on entry to the function.
27
+ * - `isParameter(1)` holds for the `FunctionInput` that represents the value of `p` (with type
28
+ * `char*`) on entry to the function.
29
+ * - `isParameter(2)` holds for the `FunctionInput` that represents the "value" of the reference
30
+ * `r` (with type `float&`) on entry to the function, _not_ the value of the referred-to
31
+ * `float`.
32
+ */
33
+ predicate isParameter ( ParameterIndex index ) { none ( ) }
34
+
35
+ /**
36
+ * Holds if this is the input value of the parameter with index `index`.
37
+ * DEPRECATED: Use `isParameter(index)` instead.
38
+ */
39
+ deprecated final predicate isInParameter ( ParameterIndex index ) { isParameter ( index ) }
40
+
41
+ /**
42
+ * Holds if this is the input value pointed to by a pointer parameter to a function, or the input
43
+ * value referred to by a reference parameter to a function, where the parameter has index
44
+ * `index`.
45
+ *
46
+ * Example:
47
+ * ```
48
+ * void func(int n, char* p, float& r);
49
+ * ```
50
+ * - `isParameterDeref(1)` holds for the `FunctionInput` that represents the value of `*p` (with
51
+ * type `char`) on entry to the function.
52
+ * - `isParameterDeref(2)` holds for the `FunctionInput` that represents the value of `r` (with type
53
+ * `float`) on entry to the function.
54
+ * - There is no `FunctionInput` for which `isParameterDeref(0)` holds, because `n` is neither a
55
+ * pointer nor a reference.
56
+ */
57
+ predicate isParameterDeref ( ParameterIndex index ) { none ( ) }
58
+
59
+ /**
60
+ * Holds if this is the input value pointed to by a pointer parameter to a function, or the input
61
+ * value referred to by a reference parameter to a function, where the parameter has index
62
+ * `index`.
63
+ * DEPRECATED: Use `isParameterDeref(index)` instead.
64
+ */
65
+ deprecated final predicate isInParameterPointer ( ParameterIndex index ) {
66
+ isParameterDeref ( index )
67
+ }
68
+
69
+ /**
70
+ * Holds if this is the input value pointed to by the `this` pointer of an instance member
71
+ * function.
72
+ *
73
+ * Example:
74
+ * ```
75
+ * struct C {
76
+ * void mfunc(int n, char* p, float& r) const;
77
+ * };
78
+ * ```
79
+ * - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
80
+ * (with type `C const`) on entry to the function.
81
+ */
82
+ predicate isQualifierObject ( ) { none ( ) }
83
+
84
+ /**
85
+ * Holds if this is the input value pointed to by the `this` pointer of an instance member
86
+ * function.
87
+ * DEPRECATED: Use `isQualifierObject()` instead.
88
+ */
89
+ deprecated final predicate isInQualifier ( ) { isQualifierObject ( ) }
90
+
91
+ /**
92
+ * Holds if this is the input value of the `this` pointer of an instance member function.
93
+ *
94
+ * Example:
95
+ * ```
96
+ * struct C {
97
+ * void mfunc(int n, char* p, float& r) const;
98
+ * };
99
+ * ```
100
+ * - `isQualifierAddress()` holds for the `FunctionInput` that represents the value of `this`
101
+ * (with type `C const *`) on entry to the function.
102
+ */
103
+ predicate isQualifierAddress ( ) { none ( ) }
104
+
105
+ /**
106
+ * Holds if `i >= 0` and `isParameter(i)` holds for this value, or
107
+ * if `i = -1` and `isQualifierAddress()` holds for this value.
108
+ */
109
+ final predicate isParameterOrQualifierAddress ( ParameterIndex i ) {
110
+ i >= 0 and this .isParameter ( i )
111
+ or
112
+ i = - 1 and this .isQualifierAddress ( )
113
+ }
114
+
115
+ /**
116
+ * Holds if this is the input value pointed to by the return value of a
117
+ * function, if the function returns a pointer, or the input value referred
118
+ * to by the return value of a function, if the function returns a reference.
119
+ *
120
+ * Example:
121
+ * ```
122
+ * char* getPointer();
123
+ * float& getReference();
124
+ * int getInt();
125
+ * ```
126
+ * - `isReturnValueDeref()` holds for the `FunctionInput` that represents the
127
+ * value of `*getPointer()` (with type `char`).
128
+ * - `isReturnValueDeref()` holds for the `FunctionInput` that represents the
129
+ * value of `getReference()` (with type `float`).
130
+ * - There is no `FunctionInput` of `getInt()` for which
131
+ * `isReturnValueDeref()` holds because the return type of `getInt()` is
132
+ * neither a pointer nor a reference.
133
+ *
134
+ * Note that data flows in through function return values are relatively
135
+ * rare, but they do occur when a function returns a reference to itself,
136
+ * part of itself, or one of its other inputs.
137
+ */
138
+ predicate isReturnValueDeref ( ) { none ( ) }
139
+
140
+ /**
141
+ * Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
142
+ * if `i = -1` and `isQualifierObject()` holds for this value.
143
+ */
144
+ final predicate isParameterDerefOrQualifierObject ( ParameterIndex i ) {
145
+ i >= 0 and this .isParameterDeref ( i )
146
+ or
147
+ i = - 1 and this .isQualifierObject ( )
148
+ }
149
+ }
150
+
151
+ /**
152
+ * An output from a function. This can be:
153
+ * - The value pointed to by one of function's pointer or reference parameters
154
+ * - The value pointed to by the function's `this` pointer
155
+ * - The function's return value
156
+ * - The value pointed to by the function's return value, if the return value is a pointer or
157
+ * reference
158
+ */
159
+ abstract class FunctionOutput extends string {
160
+ FunctionOutput ( ) { none ( ) }
161
+
162
+ /**
163
+ * Holds if this is the output value pointed to by a pointer parameter to a function, or the
164
+ * output value referred to by a reference parameter to a function, where the parameter has
165
+ * index `index`.
166
+ *
167
+ * Example:
168
+ * ```
169
+ * void func(int n, char* p, float& r);
170
+ * ```
171
+ * - `isParameterDeref(1)` holds for the `FunctionOutput` that represents the value of `*p` (with
172
+ * type `char`) on return from the function.
173
+ * - `isParameterDeref(2)` holds for the `FunctionOutput` that represents the value of `r` (with
174
+ * type `float`) on return from the function.
175
+ * - There is no `FunctionOutput` for which `isParameterDeref(0)` holds, because `n` is neither a
176
+ * pointer nor a reference.
177
+ */
178
+ predicate isParameterDeref ( ParameterIndex i ) { none ( ) }
179
+
180
+ /**
181
+ * Holds if this is the output value pointed to by a pointer parameter to a function, or the
182
+ * output value referred to by a reference parameter to a function, where the parameter has
183
+ * index `index`.
184
+ * DEPRECATED: Use `isParameterDeref(index)` instead.
185
+ */
186
+ deprecated final predicate isOutParameterPointer ( ParameterIndex index ) {
187
+ isParameterDeref ( index )
188
+ }
189
+
190
+ /**
191
+ * Holds if this is the output value pointed to by the `this` pointer of an instance member
192
+ * function.
193
+ *
194
+ * Example:
195
+ * ```
196
+ * struct C {
197
+ * void mfunc(int n, char* p, float& r);
198
+ * };
199
+ * ```
200
+ * - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
201
+ * (with type `C`) on return from the function.
202
+ */
203
+ predicate isQualifierObject ( ) { none ( ) }
204
+
205
+ /**
206
+ * Holds if this is the output value pointed to by the `this` pointer of an instance member
207
+ * function.
208
+ * DEPRECATED: Use `isQualifierObject()` instead.
209
+ */
210
+ deprecated final predicate isOutQualifier ( ) { isQualifierObject ( ) }
211
+
212
+ /**
213
+ * Holds if this is the value returned by a function.
214
+ *
215
+ * Example:
216
+ * ```
217
+ * int getInt();
218
+ * char* getPointer();
219
+ * float& getReference();
220
+ * ```
221
+ * - `isReturnValue()` holds for the `FunctionOutput` that represents the value returned by
222
+ * `getInt()` (with type `int`).
223
+ * - `isReturnValue()` holds for the `FunctionOutput` that represents the value returned by
224
+ * `getPointer()` (with type `char*`).
225
+ * - `isReturnValue()` holds for the `FunctionOutput` that represents the "value" of the reference
226
+ * returned by `getReference()` (with type `float&`), _not_ the value of the referred-to
227
+ * `float`.
228
+ */
229
+ predicate isReturnValue ( ) { none ( ) }
230
+
231
+ /**
232
+ * Holds if this is the value returned by a function.
233
+ * DEPRECATED: Use `isReturnValue()` instead.
234
+ */
235
+ deprecated final predicate isOutReturnValue ( ) { isReturnValue ( ) }
236
+
237
+ /**
238
+ * Holds if this is the output value pointed to by the return value of a function, if the function
239
+ * returns a pointer, or the output value referred to by the return value of a function, if the
240
+ * function returns a reference.
241
+ *
242
+ * Example:
243
+ * ```
244
+ * char* getPointer();
245
+ * float& getReference();
246
+ * int getInt();
247
+ * ```
248
+ * - `isReturnValueDeref()` holds for the `FunctionOutput` that represents the value of
249
+ * `*getPointer()` (with type `char`).
250
+ * - `isReturnValueDeref()` holds for the `FunctionOutput` that represents the value of
251
+ * `getReference()` (with type `float`).
252
+ * - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref()` holds because the
253
+ * return type of `getInt()` is neither a pointer nor a reference.
254
+ */
255
+ predicate isReturnValueDeref ( ) { none ( ) }
256
+
257
+ /**
258
+ * Holds if this is the output value pointed to by the return value of a function, if the function
259
+ * returns a pointer, or the output value referred to by the return value of a function, if the
260
+ * function returns a reference.
261
+ * DEPRECATED: Use `isReturnValueDeref()` instead.
262
+ */
263
+ deprecated final predicate isOutReturnPointer ( ) { isReturnValueDeref ( ) }
264
+
265
+ /**
266
+ * Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
267
+ * if `i = -1` and `isQualifierObject()` holds for this value.
268
+ */
269
+ final predicate isParameterDerefOrQualifierObject ( ParameterIndex i ) {
270
+ i >= 0 and this .isParameterDeref ( i )
271
+ or
272
+ i = - 1 and this .isQualifierObject ( )
273
+ }
274
+ }
275
+
6
276
/**
7
277
* Models the aliasing behavior of a library function.
8
278
*/
@@ -44,5 +314,10 @@ module AliasModels {
44
314
* Holds if the function always returns the value of the parameter at the specified index.
45
315
*/
46
316
abstract predicate parameterIsAlwaysReturned ( int index ) ;
317
+
318
+ /**
319
+ * Holds if the address passed in via `input` is always propagated to `output`.
320
+ */
321
+ abstract predicate hasAddressFlow ( FunctionInput input , FunctionOutput output ) ;
47
322
}
48
323
}
0 commit comments