@@ -888,6 +888,101 @@ class TypeSetLiteralType extends @typesetliteraltype, CompositeType {
888888 override string toString ( ) { result = "type set literal type" }
889889}
890890
891+ private newtype TOptInterfaceComponent =
892+ MkNoIComponent ( ) or
893+ MkSomeIComponent ( string name , Type tp ) { component_types ( any ( InterfaceType i ) , _, name , tp ) }
894+
895+ private class OptInterfaceComponent extends TOptInterfaceComponent {
896+ OptInterfaceComponent getWithDeepUnaliasedType ( ) {
897+ this = MkNoIComponent ( ) and result = MkNoIComponent ( )
898+ or
899+ exists ( string name , Type tp |
900+ this = MkSomeIComponent ( name , tp ) and
901+ result = MkSomeIComponent ( name , tp .getDeepUnaliasedType ( ) )
902+ )
903+ }
904+
905+ string toString ( ) { result = "interface component" }
906+ }
907+
908+ private class InterfaceComponent extends MkSomeIComponent {
909+ string toString ( ) { result = "interface component" }
910+
911+ predicate isComponentOf ( InterfaceType intf , int i ) {
912+ exists ( string name , Type tp |
913+ component_types ( intf , i , name , tp ) and
914+ this = MkSomeIComponent ( name , tp )
915+ )
916+ }
917+ }
918+
919+ pragma [ nomagic]
920+ predicate unpackInterfaceType (
921+ InterfaceType intf , TOptInterfaceComponent c0 , TOptInterfaceComponent c1 ,
922+ TOptInterfaceComponent c2 , TOptInterfaceComponent c3 , TOptInterfaceComponent c4 ,
923+ TOptInterfaceComponent e1 , TOptInterfaceComponent e2 , int nComponents , int nEmbeds
924+ ) {
925+ nComponents = count ( int i | component_types ( intf , i , _, _) and i >= 0 ) and
926+ nEmbeds = count ( int i | component_types ( intf , i , _, _) and i < 0 ) and
927+ (
928+ if nComponents >= 1
929+ then c0 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , 0 ) )
930+ else c0 = MkNoIComponent ( )
931+ ) and
932+ (
933+ if nComponents >= 2
934+ then c1 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , 1 ) )
935+ else c1 = MkNoIComponent ( )
936+ ) and
937+ (
938+ if nComponents >= 3
939+ then c2 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , 2 ) )
940+ else c2 = MkNoIComponent ( )
941+ ) and
942+ (
943+ if nComponents >= 4
944+ then c3 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , 3 ) )
945+ else c3 = MkNoIComponent ( )
946+ ) and
947+ (
948+ if nComponents >= 5
949+ then c4 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , 4 ) )
950+ else c4 = MkNoIComponent ( )
951+ ) and
952+ (
953+ if nEmbeds >= 1
954+ then e1 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , - 1 ) )
955+ else e1 = MkNoIComponent ( )
956+ ) and
957+ (
958+ if nEmbeds >= 2
959+ then e2 = any ( InterfaceComponent ic | ic .isComponentOf ( intf , - 2 ) )
960+ else e2 = MkNoIComponent ( )
961+ )
962+ }
963+
964+ pragma [ nomagic]
965+ predicate unpackAndUnaliasInterfaceType (
966+ InterfaceType intf , TOptInterfaceComponent c0 , TOptInterfaceComponent c1 ,
967+ TOptInterfaceComponent c2 , TOptInterfaceComponent c3 , TOptInterfaceComponent c4 ,
968+ TOptInterfaceComponent e1 , TOptInterfaceComponent e2 , int nComponents , int nEmbeds
969+ ) {
970+ exists (
971+ OptInterfaceComponent c0a , OptInterfaceComponent c1a , OptInterfaceComponent c2a ,
972+ OptInterfaceComponent c3a , OptInterfaceComponent c4a , OptInterfaceComponent e1a ,
973+ OptInterfaceComponent e2a
974+ |
975+ unpackInterfaceType ( intf , c0a , c1a , c2a , c3a , c4a , e1a , e2a , nComponents , nEmbeds ) and
976+ c0 = c0a .getWithDeepUnaliasedType ( ) and
977+ c1 = c1a .getWithDeepUnaliasedType ( ) and
978+ c2 = c2a .getWithDeepUnaliasedType ( ) and
979+ c3 = c3a .getWithDeepUnaliasedType ( ) and
980+ c4 = c4a .getWithDeepUnaliasedType ( ) and
981+ e1 = e1a .getWithDeepUnaliasedType ( ) and
982+ e2 = e2a .getWithDeepUnaliasedType ( )
983+ )
984+ }
985+
891986/** An interface type. */
892987class InterfaceType extends @interfacetype, CompositeType {
893988 /** Gets the type of method `name` of this interface type. */
@@ -969,6 +1064,58 @@ class InterfaceType extends @interfacetype, CompositeType {
9691064 .getAnEmbeddedTypeSetLiteral ( )
9701065 }
9711066
1067+ private InterfaceType getDeepUnaliasedTypeCandidate ( ) {
1068+ exists (
1069+ OptInterfaceComponent c0 , OptInterfaceComponent c1 , OptInterfaceComponent c2 ,
1070+ OptInterfaceComponent c3 , OptInterfaceComponent c4 , OptInterfaceComponent e1 ,
1071+ OptInterfaceComponent e2 , int nComponents , int nEmbeds
1072+ |
1073+ unpackAndUnaliasInterfaceType ( this , c0 , c1 , c2 , c3 , c4 , e1 , e2 , nComponents , nEmbeds ) and
1074+ unpackInterfaceType ( result , c0 , c1 , c2 , c3 , c4 , e1 , e2 , nComponents , nEmbeds )
1075+ )
1076+ }
1077+
1078+ private predicate hasDeepUnaliasedComponentTypesUpTo ( InterfaceType unaliased , int i ) {
1079+ unaliased = this .getDeepUnaliasedTypeCandidate ( ) and
1080+ i >= 5 and
1081+ (
1082+ i = 5 or
1083+ this .hasDeepUnaliasedComponentTypesUpTo ( unaliased , i - 1 )
1084+ ) and
1085+ exists ( string name , Type tp | component_types ( this , i , name , tp ) |
1086+ component_types ( unaliased , i , name , tp .getDeepUnaliasedType ( ) )
1087+ )
1088+ }
1089+
1090+ private predicate hasDeepUnaliasedEmbeddedTypesUpTo ( InterfaceType unaliased , int i ) {
1091+ unaliased = this .getDeepUnaliasedTypeCandidate ( ) and
1092+ i >= 3 and
1093+ (
1094+ i = 3 or
1095+ this .hasDeepUnaliasedEmbeddedTypesUpTo ( unaliased , i - 1 )
1096+ ) and
1097+ exists ( string name , Type tp | component_types ( this , - i , name , tp ) |
1098+ component_types ( unaliased , - i , name , tp .getDeepUnaliasedType ( ) )
1099+ )
1100+ }
1101+
1102+ override InterfaceType getDeepUnaliasedType ( ) {
1103+ result = this .getDeepUnaliasedTypeCandidate ( ) and
1104+ exists ( int nComponents |
1105+ nComponents = count ( int i | component_types ( this , i , _, _) and i >= 0 )
1106+ |
1107+ this .hasDeepUnaliasedComponentTypesUpTo ( result , nComponents - 1 )
1108+ or
1109+ nComponents <= 5
1110+ ) and
1111+ exists ( int nEmbeds | nEmbeds = count ( int i | component_types ( this , i , _, _) and i < 0 ) |
1112+ // Note no -1 here, because the first embedded type is at -1
1113+ this .hasDeepUnaliasedEmbeddedTypesUpTo ( result , nEmbeds )
1114+ or
1115+ nEmbeds <= 2
1116+ )
1117+ }
1118+
9721119 language [ monotonicAggregates]
9731120 override string pp ( ) {
9741121 exists ( string comp , string sep1 , string ts , string sep2 , string meth |
0 commit comments