@@ -1225,29 +1225,71 @@ class ComparableType extends NamedType {
12251225 ComparableType ( ) { this .getName ( ) = "comparable" }
12261226}
12271227
1228+ pragma [ nomagic]
1229+ private predicate unpackTupleType ( TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents ) {
1230+ nComponents = count ( int i | component_types ( tt , i , _, _) ) and
1231+ (
1232+ if nComponents >= 1
1233+ then c0 = MkSomeType ( tt .getComponentType ( 0 ) )
1234+ else c0 = MkNoType ( )
1235+ ) and
1236+ (
1237+ if nComponents >= 2
1238+ then c1 = MkSomeType ( tt .getComponentType ( 1 ) )
1239+ else c1 = MkNoType ( )
1240+ ) and
1241+ (
1242+ if nComponents >= 3
1243+ then c2 = MkSomeType ( tt .getComponentType ( 2 ) )
1244+ else c2 = MkNoType ( )
1245+ )
1246+ }
1247+
1248+ pragma [ nomagic]
1249+ private predicate unpackAndUnaliasTupleType ( TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents ) {
1250+ exists (
1251+ OptType c0a , OptType c1a , OptType c2a
1252+ |
1253+ unpackTupleType ( tt , c0a , c1a , c2a , nComponents ) and
1254+ c0 = c0a .getDeepUnaliasedType ( ) and
1255+ c1 = c1a .getDeepUnaliasedType ( ) and
1256+ c2 = c2a .getDeepUnaliasedType ( )
1257+ )
1258+ }
1259+
12281260/** A tuple type. */
12291261class TupleType extends @tupletype, CompositeType {
12301262 /** Gets the `i`th component type of this tuple type. */
12311263 Type getComponentType ( int i ) { component_types ( this , i , _, result ) }
12321264
1265+ private TupleType getCandidateDeepUnaliasedType ( ) {
1266+ exists (
1267+ OptType c0 , OptType c1 , OptType c2 , int nComponents
1268+ |
1269+ unpackAndUnaliasTupleType ( this , c0 , c1 , c2 , nComponents ) and
1270+ unpackTupleType ( result , c0 , c1 , c2 , nComponents )
1271+ )
1272+ }
1273+
12331274 private predicate isDeepUnaliasedTypeUpTo ( TupleType tt , int i ) {
1234- tt .getComponentType ( i ) = this .getDeepUnaliasedType ( ) and
1275+ tt = this .getCandidateDeepUnaliasedType ( ) and
1276+ i >= 3 and
12351277 (
1236- i = 0
1278+ i = 3
12371279 or
12381280 this .isDeepUnaliasedTypeUpTo ( tt , i - 1 )
1281+ ) and
1282+ exists ( Type tp | component_types ( this , i , _, tp ) |
1283+ component_types ( tt , i , _, tp .getDeepUnaliasedType ( ) )
12391284 )
12401285 }
12411286
12421287 override TupleType getDeepUnaliasedType ( ) {
1243- exists ( int nComponents |
1244- nComponents = count ( int i | exists ( this .getComponentType ( i ) ) ) and
1245- nComponents = count ( int i | exists ( result .getComponentType ( i ) ) )
1246- |
1288+ result = this .getCandidateDeepUnaliasedType ( ) and
1289+ exists ( int nComponents | nComponents = count ( int i | component_types ( this , i , _, _) ) |
12471290 this .isDeepUnaliasedTypeUpTo ( result , nComponents - 1 )
12481291 or
1249- // I don't think Go allows empty tuples in any context, but this is at least harmless.
1250- nComponents = 0
1292+ nComponents <= 3
12511293 )
12521294 }
12531295
0 commit comments