@@ -1186,29 +1186,71 @@ class ComparableType extends NamedType {
11861186 ComparableType ( ) { this .getName ( ) = "comparable" }
11871187}
11881188
1189+ pragma [ nomagic]
1190+ private predicate unpackTupleType ( TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents ) {
1191+ nComponents = count ( int i | component_types ( tt , i , _, _) ) and
1192+ (
1193+ if nComponents >= 1
1194+ then c0 = MkSomeType ( tt .getComponentType ( 0 ) )
1195+ else c0 = MkNoType ( )
1196+ ) and
1197+ (
1198+ if nComponents >= 2
1199+ then c1 = MkSomeType ( tt .getComponentType ( 1 ) )
1200+ else c1 = MkNoType ( )
1201+ ) and
1202+ (
1203+ if nComponents >= 3
1204+ then c2 = MkSomeType ( tt .getComponentType ( 2 ) )
1205+ else c2 = MkNoType ( )
1206+ )
1207+ }
1208+
1209+ pragma [ nomagic]
1210+ private predicate unpackAndUnaliasTupleType ( TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents ) {
1211+ exists (
1212+ OptType c0a , OptType c1a , OptType c2a
1213+ |
1214+ unpackTupleType ( tt , c0a , c1a , c2a , nComponents ) and
1215+ c0 = c0a .getDeepUnaliasedType ( ) and
1216+ c1 = c1a .getDeepUnaliasedType ( ) and
1217+ c2 = c2a .getDeepUnaliasedType ( )
1218+ )
1219+ }
1220+
11891221/** A tuple type. */
11901222class TupleType extends @tupletype, CompositeType {
11911223 /** Gets the `i`th component type of this tuple type. */
11921224 Type getComponentType ( int i ) { component_types ( this , i , _, result ) }
11931225
1226+ private TupleType getCandidateDeepUnaliasedType ( ) {
1227+ exists (
1228+ OptType c0 , OptType c1 , OptType c2 , int nComponents
1229+ |
1230+ unpackAndUnaliasTupleType ( this , c0 , c1 , c2 , nComponents ) and
1231+ unpackTupleType ( result , c0 , c1 , c2 , nComponents )
1232+ )
1233+ }
1234+
11941235 private predicate isDeepUnaliasedTypeUpTo ( TupleType tt , int i ) {
1195- tt .getComponentType ( i ) = this .getDeepUnaliasedType ( ) and
1236+ tt = this .getCandidateDeepUnaliasedType ( ) and
1237+ i >= 3 and
11961238 (
1197- i = 0
1239+ i = 3
11981240 or
11991241 this .isDeepUnaliasedTypeUpTo ( tt , i - 1 )
1242+ ) and
1243+ exists ( Type tp | component_types ( this , i , _, tp ) |
1244+ component_types ( tt , i , _, tp .getDeepUnaliasedType ( ) )
12001245 )
12011246 }
12021247
12031248 override TupleType getDeepUnaliasedType ( ) {
1204- exists ( int nComponents |
1205- nComponents = count ( int i | exists ( this .getComponentType ( i ) ) ) and
1206- nComponents = count ( int i | exists ( result .getComponentType ( i ) ) )
1207- |
1249+ result = this .getCandidateDeepUnaliasedType ( ) and
1250+ exists ( int nComponents | nComponents = count ( int i | component_types ( this , i , _, _) ) |
12081251 this .isDeepUnaliasedTypeUpTo ( result , nComponents - 1 )
12091252 or
1210- // I don't think Go allows empty tuples in any context, but this is at least harmless.
1211- nComponents = 0
1253+ nComponents <= 3
12121254 )
12131255 }
12141256
0 commit comments