@@ -174,9 +174,21 @@ class PointerType extends @pointertype, CompositeType {
174174 }
175175}
176176
177+ private predicate isInterfaceComponentWithQualifiedName (
178+ InterfaceType intf , int idx , string qualifiedName , Type tp
179+ ) {
180+ exists ( string name | component_types ( intf , idx , name , tp ) |
181+ interface_private_method_ids ( intf , idx , qualifiedName )
182+ or
183+ not interface_private_method_ids ( intf , idx , _) and qualifiedName = name
184+ )
185+ }
186+
177187private newtype TOptInterfaceComponent =
178188 MkNoIComponent ( ) or
179- MkSomeIComponent ( string name , Type tp ) { component_types ( any ( InterfaceType i ) , _, name , tp ) }
189+ MkSomeIComponent ( string name , Type tp ) {
190+ isInterfaceComponentWithQualifiedName ( any ( InterfaceType i ) , _, name , tp )
191+ }
180192
181193private class OptInterfaceComponent extends TOptInterfaceComponent {
182194 OptInterfaceComponent getWithDeepUnaliasedType ( ) {
@@ -196,7 +208,7 @@ private class InterfaceComponent extends MkSomeIComponent {
196208
197209 predicate isComponentOf ( InterfaceType intf , int i ) {
198210 exists ( string name , Type tp |
199- component_types ( intf , i , name , tp ) and
211+ isInterfaceComponentWithQualifiedName ( intf , i , name , tp ) and
200212 this = MkSomeIComponent ( name , tp )
201213 )
202214 }
@@ -206,10 +218,16 @@ pragma[nomagic]
206218predicate unpackInterfaceType (
207219 InterfaceType intf , TOptInterfaceComponent c0 , TOptInterfaceComponent c1 ,
208220 TOptInterfaceComponent c2 , TOptInterfaceComponent c3 , TOptInterfaceComponent c4 ,
209- TOptInterfaceComponent e1 , TOptInterfaceComponent e2 , int nComponents , int nEmbeds
221+ TOptInterfaceComponent e1 , TOptInterfaceComponent e2 , int nComponents , int nEmbeds ,
222+ boolean isComparable
210223) {
211- nComponents = count ( int i | component_types ( intf , i , _, _) and i >= 0 ) and
212- nEmbeds = count ( int i | component_types ( intf , i , _, _) and i < 0 ) and
224+ nComponents = count ( int i | isInterfaceComponentWithQualifiedName ( intf , i , _, _) and i >= 0 ) and
225+ nEmbeds = count ( int i | isInterfaceComponentWithQualifiedName ( intf , i , _, _) and i < 0 ) and
226+ (
227+ if intf = any ( ComparableType comparable ) .getBaseType ( )
228+ then isComparable = true
229+ else isComparable = false
230+ ) and
213231 (
214232 if nComponents >= 1
215233 then c0 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , 0 ) )
@@ -251,14 +269,15 @@ pragma[nomagic]
251269predicate unpackAndUnaliasInterfaceType (
252270 InterfaceType intf , TOptInterfaceComponent c0 , TOptInterfaceComponent c1 ,
253271 TOptInterfaceComponent c2 , TOptInterfaceComponent c3 , TOptInterfaceComponent c4 ,
254- TOptInterfaceComponent e1 , TOptInterfaceComponent e2 , int nComponents , int nEmbeds
272+ TOptInterfaceComponent e1 , TOptInterfaceComponent e2 , int nComponents , int nEmbeds ,
273+ boolean isComparable
255274) {
256275 exists (
257276 OptInterfaceComponent c0a , OptInterfaceComponent c1a , OptInterfaceComponent c2a ,
258277 OptInterfaceComponent c3a , OptInterfaceComponent c4a , OptInterfaceComponent e1a ,
259278 OptInterfaceComponent e2a
260279 |
261- unpackInterfaceType ( intf , c0a , c1a , c2a , c3a , c4a , e1a , e2a , nComponents , nEmbeds ) and
280+ unpackInterfaceType ( intf , c0a , c1a , c2a , c3a , c4a , e1a , e2a , nComponents , nEmbeds , isComparable ) and
262281 c0 = c0a .getWithDeepUnaliasedType ( ) and
263282 c1 = c1a .getWithDeepUnaliasedType ( ) and
264283 c2 = c2a .getWithDeepUnaliasedType ( ) and
@@ -272,7 +291,7 @@ predicate unpackAndUnaliasInterfaceType(
272291/** An interface type. */
273292class InterfaceType extends @interfacetype, CompositeType {
274293 private Type getMethodType ( int i , string name ) {
275- i >= 0 and component_types ( this , i , name , result )
294+ i >= 0 and isInterfaceComponentWithQualifiedName ( this , i , name , result )
276295 }
277296
278297 /**
@@ -282,17 +301,18 @@ class InterfaceType extends @interfacetype, CompositeType {
282301 * interface type.
283302 */
284303 private predicate hasDirectlyEmbeddedType ( int index , Type tp ) {
285- index >= 0 and component_types ( this , - ( index + 1 ) , _, tp )
304+ index >= 0 and isInterfaceComponentWithQualifiedName ( this , - ( index + 1 ) , _, tp )
286305 }
287306
288307 private InterfaceType getDeepUnaliasedTypeCandidate ( ) {
289308 exists (
290309 OptInterfaceComponent c0 , OptInterfaceComponent c1 , OptInterfaceComponent c2 ,
291310 OptInterfaceComponent c3 , OptInterfaceComponent c4 , OptInterfaceComponent e1 ,
292- OptInterfaceComponent e2 , int nComponents , int nEmbeds
311+ OptInterfaceComponent e2 , int nComponents , int nEmbeds , boolean isComparable
293312 |
294- unpackAndUnaliasInterfaceType ( this , c0 , c1 , c2 , c3 , c4 , e1 , e2 , nComponents , nEmbeds ) and
295- unpackInterfaceType ( result , c0 , c1 , c2 , c3 , c4 , e1 , e2 , nComponents , nEmbeds )
313+ unpackAndUnaliasInterfaceType ( this , c0 , c1 , c2 , c3 , c4 , e1 , e2 , nComponents , nEmbeds ,
314+ isComparable ) and
315+ unpackInterfaceType ( result , c0 , c1 , c2 , c3 , c4 , e1 , e2 , nComponents , nEmbeds , isComparable )
296316 )
297317 }
298318
@@ -377,7 +397,7 @@ class TupleType extends @tupletype, CompositeType {
377397 or
378398 this .isDeepUnaliasedTypeUpTo ( tt , i - 1 )
379399 ) and
380- tt .getComponentType ( i ) . getDeepUnaliasedType ( ) = this .getComponentType ( i )
400+ tt .getComponentType ( i ) = this .getComponentType ( i ) . getDeepUnaliasedType ( )
381401 }
382402
383403 override TupleType getDeepUnaliasedType ( ) {
@@ -558,6 +578,18 @@ class SendRecvChanType extends @sendrcvchantype, ChanType {
558578 }
559579}
560580
581+ /** A named type. */
582+ class NamedType extends @namedtype, CompositeType {
583+ Type getBaseType ( ) { underlying_type ( this , result ) }
584+ }
585+
586+ /**
587+ * The predeclared `comparable` type.
588+ */
589+ class ComparableType extends NamedType {
590+ ComparableType ( ) { typename ( this , "comparable" ) }
591+ }
592+
561593/** An alias type. */
562594class AliasType extends @typealias, CompositeType {
563595 /** Gets the aliased type (i.e. that appears on the RHS of the alias definition). */
0 commit comments