@@ -217,48 +217,61 @@ signature predicate interestedInEquality(Type a, Type b);
217217 * A module to check the equivalence of two types, as defined by the provided `TypeEquivalenceSig`.
218218 *
219219 * For performance reasons, this module is designed to be used with a predicate
220- * `interestedInEquality` that restricts the set of considered types .
220+ * `interestedInEquality` that restricts the set of considered pairwise comparisons .
221221 *
222222 * To use this module, define a `TypeEquivalenceSig` module and implement a subset of `Type` that
223223 * selects the relevant root types to be considered. Then use the predicate `equalTypes(a, b)`.
224224 * Note that `equalTypes(a, b)` only holds if `interestedIn(a, b)` holds. A type is always
225225 * considered to be equal to itself, and this module does not support configurations that declare
226- * otherwise.
226+ * otherwise. Additionally, `interestedIn(a, b)` implies `interestedIn(b, a)`.
227227 *
228- * Further, `interestedInEquality(a, a)` is treated differently from `interestedInEquality(a, b)`,
229- * assuming that `a` and `b` are not identical. This is so that we can construct a set of types
230- * that are not identical, but still may be equivalent by the specified configuration. We also must
231- * consider all types that are reachable from these types, as the equivalence relation is
232- * recursive. Therefore, this module is more performant when most comparisons are identical, and
233- * only a few are not.
228+ * This module will recursively select pairs of types to be compared. For instance, if
229+ * `interestedInEquality(a, b)` holds, then types `a` and `b` will be compared. If
230+ * `Config::equalPointerTypes(a, b, true)` holds, then the pointed-to types of `a` and `b` will be
231+ * compared. However, if `Config::equalPointerTypes(a, b, false)` holds, then `a` and `b` will be
232+ * compared, but their pointed-to types will not. Similarly, inner types will not be compared if
233+ * `Config::overrideTypeComparison(a, b, _)` holds. For detail, see the module predicates
234+ * `recurses` and `compares`.
234235 */
235236module TypeEquivalence< TypeEquivalenceSig Config, interestedInEquality / 2 interestedIn> {
236-
237237 /**
238238 * Performance related predicate to force top down rather than bottom up evaluation of type
239239 * equivalence.
240+ *
241+ * This interoperates with the predicate `recurses` to find types that will be compared, along
242+ * with the inner types of those types that will be compared. See `recurses` for cases where this
243+ * algorithm will or will not recurse. We still need to know which types are compared, even if
244+ * we do not recurse on them, in order to properly constrain `equalTypes(x, y)` to hold for types
245+ * such as leaf types, where we do not recurse during comparison.
246+ *
247+ * At each stage of recursion, we specify `pragma[only_bind_into]` to ensure that the
248+ * prior `recurses` results are considered first in the pipeline.
240249 */
241250 predicate compares ( Type t1 , Type t2 ) {
242- interestedIn ( t1 , t2 )
251+ // Base case: config specifies that these root types will be compared.
252+ interestedInUnordered ( t1 , t2 )
243253 or
254+ // If derived types are compared, their base types must be compared.
244255 exists ( DerivedType t1Derived , DerivedType t2Derived |
245256 not t1Derived instanceof SpecifiedType and
246257 not t2Derived instanceof SpecifiedType and
247- compares ( pragma [ only_bind_into ] ( t1Derived ) , pragma [ only_bind_into ] ( t2Derived ) ) and
258+ recurses ( pragma [ only_bind_into ] ( t1Derived ) , pragma [ only_bind_into ] ( t2Derived ) ) and
248259 t1 = t1Derived .getBaseType ( ) and
249260 t2 = t2Derived .getBaseType ( )
250261 )
251262 or
263+ // If specified types are compared, their unspecified types must be compared.
252264 exists ( SpecifiedType t1Spec , SpecifiedType t2Spec |
253- compares ( pragma [ only_bind_into ] ( t1Spec ) , pragma [ only_bind_into ] ( t2Spec ) ) and
265+ recurses ( pragma [ only_bind_into ] ( t1Spec ) , pragma [ only_bind_into ] ( t2Spec ) ) and
254266 (
255267 t1 = unspecify ( t1Spec ) and
256268 t2 = unspecify ( t2Spec )
257269 )
258270 )
259271 or
272+ // If function types are compared, their return types and parameter types must be compared.
260273 exists ( FunctionType t1Func , FunctionType t2Func |
261- compares ( pragma [ only_bind_into ] ( t1Func ) , pragma [ only_bind_into ] ( t2Func ) ) and
274+ recurses ( pragma [ only_bind_into ] ( t1Func ) , pragma [ only_bind_into ] ( t2Func ) ) and
262275 (
263276 t1 = t1Func .getReturnType ( ) and
264277 t2 = t2Func .getReturnType ( )
@@ -270,13 +283,79 @@ module TypeEquivalence<TypeEquivalenceSig Config, interestedInEquality/2 interes
270283 )
271284 )
272285 or
286+ // If the config says to resolve typedefs, and a typedef type is compared to a non-typedef
287+ // type, then the non-typedef type must be compared to the base type of the typedef.
273288 Config:: resolveTypedefs ( ) and
274289 exists ( TypedefType tdtype |
275290 tdtype .getBaseType ( ) = t1 and
276- compares ( pragma [ only_bind_into ] ( tdtype ) , t2 )
291+ recurses ( pragma [ only_bind_into ] ( tdtype ) , t2 )
277292 or
278293 tdtype .getBaseType ( ) = t2 and
279- compares ( t1 , pragma [ only_bind_into ] ( tdtype ) )
294+ recurses ( t1 , pragma [ only_bind_into ] ( tdtype ) )
295+ )
296+ or
297+ // If two typedef types are compared, then their base types must be compared.
298+ exists ( TypedefType t1Typedef , TypedefType t2Typedef |
299+ recurses ( pragma [ only_bind_into ] ( t1Typedef ) , pragma [ only_bind_into ] ( t2Typedef ) ) and
300+ (
301+ t1 = t1Typedef .getBaseType ( ) and
302+ t2 = t2Typedef .getBaseType ( )
303+ )
304+ )
305+ }
306+
307+ /**
308+ * Performance related predicate to force top down rather than bottom up evaluation of type
309+ * equivalence.
310+ *
311+ * This predicate is used to determine whether we should recurse on a type. It is used in
312+ * conjunction with the `compares` predicate to only recurse on types that are being compared.
313+ *
314+ * We don't recurse on identical types, as they are already equal. We also don't recurse on
315+ * types that are overriden by `Config::overrideTypeComparison`, as that predicate determines
316+ * their equalivance.
317+ *
318+ * For the other types, we have a set of predicates such as `Config::equalPointerTypes` that
319+ * holds for `(x, y, true)` if the types `x` and `y` should be considered equivalent when the
320+ * pointed-to types of `x` and `y` are equivalent. If the predicate does not hold, or holds for
321+ * `(x, y, false)`, then we do not recurse on the types.
322+ *
323+ * We do not recurse on leaf types.
324+ */
325+ private predicate recurses ( Type t1 , Type t2 ) {
326+ // We only recurse on types we are comparing.
327+ compares ( pragma [ only_bind_into ] ( t1 ) , pragma [ only_bind_into ] ( t2 ) ) and
328+ // We don't recurse on identical types, as they are already equal.
329+ not t1 = t2 and
330+ // We don't recurse on overriden comparisons
331+ not Config:: overrideTypeComparison ( t1 , t2 , _) and
332+ (
333+ // These pointer types are equal if their base types are equal: recurse.
334+ Config:: equalPointerTypes ( t1 , t2 , true )
335+ or
336+ // These array types are equal if their base types are equal: recurse.
337+ Config:: equalArrayTypes ( t1 , t2 , true )
338+ or
339+ // These reference types are equal if their base types are equal: recurse.
340+ Config:: equalReferenceTypes ( t1 , t2 , true )
341+ or
342+ // These routine types are equal if their return and parameter types are equal: recurse.
343+ Config:: equalRoutineTypes ( t1 , t2 , true , true )
344+ or
345+ // These function pointer-ish types are equal if their return and parameter types are equal: recurse.
346+ Config:: equalFunctionPointerIshTypes ( t1 , t2 , true , true )
347+ or
348+ // These typedef types are equal if their base types are equal: recurse.
349+ Config:: equalTypedefTypes ( t1 , t2 , true )
350+ or
351+ // These specified types are equal if their unspecified types are equal: recurse.
352+ Config:: equalSpecifiedTypes ( t1 , t2 , true )
353+ or
354+ // We resolve typedefs, and one of these types is a typedef type: recurse.
355+ Config:: resolveTypedefs ( ) and
356+ t1 instanceof TypedefType
357+ or
358+ t2 instanceof TypedefType
280359 )
281360 }
282361
@@ -288,27 +367,32 @@ module TypeEquivalence<TypeEquivalenceSig Config, interestedInEquality/2 interes
288367 */
289368 predicate equalTypes ( Type t1 , Type t2 ) {
290369 compares ( pragma [ only_bind_into ] ( t1 ) , pragma [ only_bind_into ] ( t2 ) ) and
291- if Config:: overrideTypeComparison ( t1 , t2 , _)
292- then Config:: overrideTypeComparison ( t1 , t2 , true )
293- else
294- if t1 instanceof TypedefType and Config:: resolveTypedefs ( )
295- then equalTypes ( t1 .( TypedefType ) .getBaseType ( ) , t2 )
370+ (
371+ t1 = t2
372+ or
373+ not t1 = t2 and
374+ if Config:: overrideTypeComparison ( t1 , t2 , _)
375+ then Config:: overrideTypeComparison ( t1 , t2 , true )
296376 else
297- if t2 instanceof TypedefType and Config:: resolveTypedefs ( )
298- then equalTypes ( t1 , t2 .( TypedefType ) .getBaseType ( ) )
299- else (
300- not t1 instanceof DerivedType and
301- not t2 instanceof DerivedType and
302- not t1 instanceof TypedefType and
303- not t2 instanceof TypedefType and
304- equalLeafRelation ( t1 , t2 )
305- or
306- equalDerivedTypes ( t1 , t2 )
307- or
308- equalTypedefTypes ( t1 , t2 )
309- or
310- equalFunctionTypes ( t1 , t2 )
311- )
377+ if t1 instanceof TypedefType and Config:: resolveTypedefs ( )
378+ then equalTypes ( t1 .( TypedefType ) .getBaseType ( ) , t2 )
379+ else
380+ if t2 instanceof TypedefType and Config:: resolveTypedefs ( )
381+ then equalTypes ( t1 , t2 .( TypedefType ) .getBaseType ( ) )
382+ else (
383+ not t1 instanceof DerivedType and
384+ not t2 instanceof DerivedType and
385+ not t1 instanceof TypedefType and
386+ not t2 instanceof TypedefType and
387+ equalLeafRelation ( t1 , t2 )
388+ or
389+ equalDerivedTypes ( t1 , t2 )
390+ or
391+ equalTypedefTypes ( t1 , t2 )
392+ or
393+ equalFunctionTypes ( t1 , t2 )
394+ )
395+ )
312396 }
313397
314398 /** Whether two types will be compared, regardless of order (a, b) or (b, a). */
@@ -408,6 +492,7 @@ module FunctionDeclarationTypeEquivalence<
408492 }
409493
410494 predicate equalReturnTypes ( FunctionDeclarationEntry f1 , FunctionDeclarationEntry f2 ) {
495+ interestedInFunctions ( f1 , f2 ) and
411496 TypeEquivalence< Config , interestedInReturnTypes / 2 > :: equalTypes ( f1 .getType ( ) , f2 .getType ( ) )
412497 }
413498
0 commit comments