@@ -3,6 +3,276 @@ import experimental.ir.implementation.IRConfiguration
33import experimental.ir.internal.IntegerConstant as Ints
44
55module 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+
6276 /**
7277 * Models the aliasing behavior of a library function.
8278 */
@@ -44,5 +314,10 @@ module AliasModels {
44314 * Holds if the function always returns the value of the parameter at the specified index.
45315 */
46316 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 ) ;
47322 }
48323}
0 commit comments