Skip to content

Commit a80fc02

Browse files
committed
Expend more Vararg elements during re-intersection if valid.
This should be valid if the type var is used only for `Vararg` length. This commit add a new field `max_offset` to our type env. which is used to tracks the minimum length of a `Vararg` during the 1st round intersection. (It's value would be set to `-1` if this var has other usage.) If we got a positive value, then we can expand more elements during the 2nd round intersection safely. With these extra elements, the offset between 2 `Vararg`s will reduce to 0 (hopefully), and thus we get a more accurate result.
1 parent 9374e49 commit a80fc02

File tree

2 files changed

+110
-60
lines changed

2 files changed

+110
-60
lines changed

src/subtype.c

Lines changed: 96 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,8 @@ typedef struct jl_varbinding_t {
6969
int8_t occurs_inv; // occurs in invariant position
7070
int8_t occurs_cov; // # of occurrences in covariant position
7171
int8_t concrete; // 1 if another variable has a constraint forcing this one to be concrete
72+
int8_t max_offset; // record the maximum positive offset of the variable (up to 32)
73+
// max_offset < 0 if this variable occurs outside VarargNum.
7274
// constraintkind: in covariant position, we try three different ways to compute var ∩ type:
7375
// let ub = var.ub ∩ type
7476
// 0 - var.ub <: type ? var : ub
@@ -77,6 +79,7 @@ typedef struct jl_varbinding_t {
7779
int8_t constraintkind;
7880
int8_t intvalued; // intvalued: must be integer-valued; i.e. occurs as N in Vararg{_,N}
7981
int8_t limited;
82+
int8_t intersected; // whether this variable has been intersected
8083
int16_t depth0; // # of invariant constructors nested around the UnionAll type for this var
8184
// array of typevars that our bounds depend on, whose UnionAlls need to be
8285
// moved outside ours.
@@ -168,9 +171,9 @@ static int current_env_length(jl_stenv_t *e)
168171
typedef struct {
169172
int8_t *buf;
170173
int rdepth;
171-
int8_t _space[24]; // == 8 * 3
174+
int8_t _space[32]; // == 8 * 4
172175
jl_gcframe_t gcframe;
173-
jl_value_t *roots[24];
176+
jl_value_t *roots[24]; // == 8 * 3
174177
} jl_savedenv_t;
175178

176179
static void re_save_env(jl_stenv_t *e, jl_savedenv_t *se, int root)
@@ -200,6 +203,7 @@ static void re_save_env(jl_stenv_t *e, jl_savedenv_t *se, int root)
200203
se->buf[j++] = v->occurs;
201204
se->buf[j++] = v->occurs_inv;
202205
se->buf[j++] = v->occurs_cov;
206+
se->buf[j++] = v->max_offset;
203207
v = v->prev;
204208
}
205209
assert(i == nroots); (void)nroots;
@@ -231,7 +235,7 @@ static void alloc_env(jl_stenv_t *e, jl_savedenv_t *se, int root)
231235
ct->gcstack = &se->gcframe;
232236
}
233237
}
234-
se->buf = (len > 8 ? (int8_t*)malloc_s(len * 3) : se->_space);
238+
se->buf = (len > 8 ? (int8_t*)malloc_s(len * 4) : se->_space);
235239
#ifdef __clang_gcanalyzer__
236240
memset(se->buf, 0, len * 3);
237241
#endif
@@ -281,6 +285,7 @@ static void restore_env(jl_stenv_t *e, jl_savedenv_t *se, int root) JL_NOTSAFEPO
281285
v->occurs = se->buf[j++];
282286
v->occurs_inv = se->buf[j++];
283287
v->occurs_cov = se->buf[j++];
288+
v->max_offset = se->buf[j++];
284289
v = v->prev;
285290
}
286291
assert(i == nroots); (void)nroots;
@@ -677,6 +682,10 @@ static void record_var_occurrence(jl_varbinding_t *vb, jl_stenv_t *e, int param)
677682
else if (vb->occurs_cov < 2) {
678683
vb->occurs_cov++;
679684
}
685+
// Always set `max_offset` to `-1` during the 1st round intersection.
686+
// Would be recovered in `intersect_varargs`/`subtype_tuple_varargs` if needed.
687+
if (!vb->intersected)
688+
vb->max_offset = -1;
680689
}
681690
}
682691

@@ -888,7 +897,7 @@ static jl_unionall_t *unalias_unionall(jl_unionall_t *u, jl_stenv_t *e)
888897
static int subtype_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_t *e, int8_t R, int param)
889898
{
890899
u = unalias_unionall(u, e);
891-
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, 0, 0, 0,
900+
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, 0, 0, 0, 0, 0,
892901
e->invdepth, NULL, e->vars };
893902
JL_GC_PUSH4(&u, &vb.lb, &vb.ub, &vb.innervars);
894903
e->vars = &vb;
@@ -1008,39 +1017,30 @@ static int subtype_tuple_varargs(
10081017
jl_value_t *xp0 = jl_unwrap_vararg(vtx); jl_value_t *xp1 = jl_unwrap_vararg_num(vtx);
10091018
jl_value_t *yp0 = jl_unwrap_vararg(vty); jl_value_t *yp1 = jl_unwrap_vararg_num(vty);
10101019

1020+
jl_varbinding_t *xlv = NULL, *ylv = NULL;
1021+
if (xp1 && jl_is_typevar(xp1))
1022+
xlv = lookup(e, (jl_tvar_t*)xp1);
1023+
if (yp1 && jl_is_typevar(yp1))
1024+
ylv = lookup(e, (jl_tvar_t*)yp1);
1025+
1026+
int8_t max_offsetx = xlv ? xlv->max_offset : 0;
1027+
int8_t max_offsety = ylv ? ylv->max_offset : 0;
1028+
1029+
jl_value_t *xl = xlv ? xlv->lb : xp1;
1030+
jl_value_t *yl = ylv ? ylv->lb : yp1;
1031+
10111032
if (!xp1) {
1012-
jl_value_t *yl = yp1;
1013-
if (yl) {
1014-
// Unconstrained on the left, constrained on the right
1015-
if (jl_is_typevar(yl)) {
1016-
jl_varbinding_t *ylv = lookup(e, (jl_tvar_t*)yl);
1017-
if (ylv)
1018-
yl = ylv->lb;
1019-
}
1020-
if (jl_is_long(yl)) {
1021-
return 0;
1022-
}
1023-
}
1033+
// Unconstrained on the left, constrained on the right
1034+
if (yl && jl_is_long(yl))
1035+
return 0;
10241036
}
10251037
else {
1026-
jl_value_t *xl = jl_unwrap_vararg_num(vtx);
1027-
if (jl_is_typevar(xl)) {
1028-
jl_varbinding_t *xlv = lookup(e, (jl_tvar_t*)xl);
1029-
if (xlv)
1030-
xl = xlv->lb;
1031-
}
10321038
if (jl_is_long(xl)) {
10331039
if (jl_unbox_long(xl) + 1 == vx) {
10341040
// LHS is exhausted. We're a subtype if the RHS is either
10351041
// exhausted as well or unbounded (in which case we need to
10361042
// set it to 0).
1037-
jl_value_t *yl = jl_unwrap_vararg_num(vty);
10381043
if (yl) {
1039-
if (jl_is_typevar(yl)) {
1040-
jl_varbinding_t *ylv = lookup(e, (jl_tvar_t*)yl);
1041-
if (ylv)
1042-
yl = ylv->lb;
1043-
}
10441044
if (jl_is_long(yl)) {
10451045
return jl_unbox_long(yl) + 1 == vy;
10461046
}
@@ -1090,6 +1090,8 @@ static int subtype_tuple_varargs(
10901090
// appropriately.
10911091
e->invdepth++;
10921092
int ans = subtype((jl_value_t*)jl_any_type, yp1, e, 2);
1093+
if (ylv && !ylv->intersected)
1094+
ylv->max_offset = max_offsety;
10931095
e->invdepth--;
10941096
return ans;
10951097
}
@@ -1130,6 +1132,10 @@ static int subtype_tuple_varargs(
11301132
e->Loffset = 0;
11311133
}
11321134
JL_GC_POP();
1135+
if (ylv && !ylv->intersected)
1136+
ylv->max_offset = max_offsety;
1137+
if (xlv && !xlv->intersected)
1138+
xlv->max_offset = max_offsetx;
11331139
e->invdepth--;
11341140
return ans;
11351141
}
@@ -3134,14 +3140,15 @@ static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_
31343140
{
31353141
jl_value_t *res = NULL;
31363142
jl_savedenv_t se;
3137-
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, 0, 0, 0,
3143+
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, 0, 0, 0, 0, 0,
31383144
e->invdepth, NULL, e->vars };
31393145
JL_GC_PUSH4(&res, &vb.lb, &vb.ub, &vb.innervars);
31403146
save_env(e, &se, 1);
31413147
int noinv = !var_occurs_invariant(u->body, u->var);
31423148
if (is_leaf_typevar(u->var) && noinv && always_occurs_cov(u->body, u->var, param))
31433149
vb.constraintkind = 1;
31443150
res = intersect_unionall_(t, u, e, R, param, &vb);
3151+
vb.intersected = 1;
31453152
if (vb.limited) {
31463153
// if the environment got too big, avoid tree recursion and propagate the flag
31473154
if (e->vars)
@@ -3218,17 +3225,20 @@ static jl_value_t *intersect_varargs(jl_vararg_t *vmx, jl_vararg_t *vmy, ssize_t
32183225
assert(e->Loffset == 0);
32193226
e->Loffset = offset;
32203227
jl_varbinding_t *xb = NULL, *yb = NULL;
3228+
int8_t max_offsetx = 0, max_offsety = 0;
32213229
if (xp2) {
32223230
assert(jl_is_typevar(xp2));
32233231
xb = lookup(e, (jl_tvar_t*)xp2);
32243232
if (xb) xb->intvalued = 1;
3233+
if (xb) max_offsetx = xb->max_offset;
32253234
if (!yp2)
32263235
i2 = bound_var_below((jl_tvar_t*)xp2, xb, e, 0);
32273236
}
32283237
if (yp2) {
32293238
assert(jl_is_typevar(yp2));
32303239
yb = lookup(e, (jl_tvar_t*)yp2);
32313240
if (yb) yb->intvalued = 1;
3241+
if (yb) max_offsety = yb->max_offset;
32323242
if (!xp2)
32333243
i2 = bound_var_below((jl_tvar_t*)yp2, yb, e, 1);
32343244
}
@@ -3243,14 +3253,27 @@ static jl_value_t *intersect_varargs(jl_vararg_t *vmx, jl_vararg_t *vmy, ssize_t
32433253
}
32443254
assert(e->Loffset == offset);
32453255
e->Loffset = 0;
3246-
if (i2 == jl_bottom_type)
3256+
if (i2 == jl_bottom_type) {
32473257
ii = (jl_value_t*)jl_bottom_type;
3248-
else if (xp2 && obviously_egal(xp1, ii) && obviously_egal(xp2, i2))
3249-
ii = (jl_value_t*)vmx;
3250-
else if (yp2 && obviously_egal(yp1, ii) && obviously_egal(yp2, i2))
3251-
ii = (jl_value_t*)vmy;
3252-
else
3253-
ii = (jl_value_t*)jl_wrap_vararg(ii, i2, 1);
3258+
}
3259+
else {
3260+
if (xb && !xb->intersected) {
3261+
xb->max_offset = max_offsetx;
3262+
if (offset > xb->max_offset && xb->max_offset >= 0)
3263+
xb->max_offset = offset > 32 ? 32 : offset;
3264+
}
3265+
if (yb && !yb->intersected) {
3266+
yb->max_offset = max_offsety;
3267+
if (-offset > yb->max_offset && yb->max_offset >= 0)
3268+
yb->max_offset = -offset > 32 ? 32 : -offset;
3269+
}
3270+
if (xp2 && obviously_egal(xp1, ii) && obviously_egal(xp2, i2))
3271+
ii = (jl_value_t*)vmx;
3272+
else if (yp2 && obviously_egal(yp1, ii) && obviously_egal(yp2, i2))
3273+
ii = (jl_value_t*)vmy;
3274+
else
3275+
ii = (jl_value_t*)jl_wrap_vararg(ii, i2, 1);
3276+
}
32543277
JL_GC_POP();
32553278
return ii;
32563279
}
@@ -3269,6 +3292,24 @@ static jl_value_t *intersect_tuple(jl_datatype_t *xd, jl_datatype_t *yd, jl_sten
32693292
llx += jl_unbox_long(jl_unwrap_vararg_num((jl_vararg_t *)jl_tparam(xd, lx-1))) - 1;
32703293
if (vvy == JL_VARARG_INT)
32713294
lly += jl_unbox_long(jl_unwrap_vararg_num((jl_vararg_t *)jl_tparam(yd, ly-1))) - 1;
3295+
if (vvx == JL_VARARG_BOUND && (vvy == JL_VARARG_BOUND || vvy == JL_VARARG_UNBOUND)) {
3296+
jl_value_t *xlen = jl_unwrap_vararg_num((jl_vararg_t*)jl_tparam(xd, lx-1));
3297+
assert(xlen && jl_is_typevar(xlen));
3298+
jl_varbinding_t *xb = lookup(e, (jl_tvar_t*)xlen);
3299+
if (xb && xb->intersected && xb->max_offset > 0) {
3300+
assert(xb->max_offset <= 32);
3301+
llx += xb->max_offset;
3302+
}
3303+
}
3304+
if (vvy == JL_VARARG_BOUND && (vvx == JL_VARARG_BOUND || vvx == JL_VARARG_UNBOUND)) {
3305+
jl_value_t *ylen = jl_unwrap_vararg_num((jl_vararg_t*)jl_tparam(yd, ly-1));
3306+
assert(ylen && jl_is_typevar(ylen));
3307+
jl_varbinding_t *yb = lookup(e, (jl_tvar_t*)ylen);
3308+
if (yb && yb->intersected && yb->max_offset > 0) {
3309+
assert(yb->max_offset <= 32);
3310+
lly += yb->max_offset;
3311+
}
3312+
}
32723313

32733314
if ((vvx == JL_VARARG_NONE || vvx == JL_VARARG_INT) &&
32743315
(vvy == JL_VARARG_NONE || vvy == JL_VARARG_INT)) {
@@ -3301,8 +3342,8 @@ static jl_value_t *intersect_tuple(jl_datatype_t *xd, jl_datatype_t *yd, jl_sten
33013342
assert(i == j && i == np);
33023343
break;
33033344
}
3304-
if (xi && jl_is_vararg(xi)) vx = vvx != JL_VARARG_INT;
3305-
if (yi && jl_is_vararg(yi)) vy = vvy != JL_VARARG_INT;
3345+
if (xi && jl_is_vararg(xi)) vx = vvx == JL_VARARG_UNBOUND || (vvx == JL_VARARG_BOUND && i == llx - 1);
3346+
if (yi && jl_is_vararg(yi)) vy = vvy == JL_VARARG_UNBOUND || (vvy == JL_VARARG_BOUND && j == lly - 1);
33063347
if (xi == NULL || yi == NULL) {
33073348
if (vx && intersect_vararg_length(xi, lly+1-llx, e, 0)) {
33083349
np = j;
@@ -3845,15 +3886,15 @@ static int merge_env(jl_stenv_t *e, jl_savedenv_t *se, int count)
38453886
roots = se->roots;
38463887
nroots = se->gcframe.nroots >> 2;
38473888
}
3848-
int n = 0;
3889+
int m = 0, n = 0;
38493890
jl_varbinding_t *v = e->vars;
3850-
v = e->vars;
38513891
while (v != NULL) {
38523892
if (count == 0) {
38533893
// need to initialize this
3854-
se->buf[n] = 0;
3855-
se->buf[n+1] = 0;
3856-
se->buf[n+2] = 0;
3894+
se->buf[m] = 0;
3895+
se->buf[m+1] = 0;
3896+
se->buf[m+2] = 0;
3897+
se->buf[m+3] = v->max_offset;
38573898
}
38583899
if (v->occurs) {
38593900
// only merge lb/ub/innervars if this var occurs.
@@ -3879,13 +3920,17 @@ static int merge_env(jl_stenv_t *e, jl_savedenv_t *se, int count)
38793920
roots[n+2] = b2;
38803921
}
38813922
// record the meeted vars.
3882-
se->buf[n] = 1;
3923+
se->buf[m] = 1;
38833924
}
38843925
// always merge occurs_inv/cov by max (never decrease)
3885-
if (v->occurs_inv > se->buf[n+1])
3886-
se->buf[n+1] = v->occurs_inv;
3887-
if (v->occurs_cov > se->buf[n+2])
3888-
se->buf[n+2] = v->occurs_cov;
3926+
if (v->occurs_inv > se->buf[m+1])
3927+
se->buf[m+1] = v->occurs_inv;
3928+
if (v->occurs_cov > se->buf[m+2])
3929+
se->buf[m+2] = v->occurs_cov;
3930+
// always merge max_offset by min
3931+
if (!v->intersected && v->max_offset < se->buf[m+3])
3932+
se->buf[m+3] = v->max_offset;
3933+
m = m + 4;
38893934
n = n + 3;
38903935
v = v->prev;
38913936
}
@@ -3917,7 +3962,7 @@ static void final_merge_env(jl_stenv_t *e, jl_savedenv_t *me, jl_savedenv_t *se)
39173962
}
39183963
assert(nroots == current_env_length(e) * 3);
39193964
assert(nroots % 3 == 0);
3920-
for (int n = 0; n < nroots; n = n + 3) {
3965+
for (int n = 0, m = 0; n < nroots; n += 3, m += 4) {
39213966
if (merged[n] == NULL)
39223967
merged[n] = saved[n];
39233968
if (merged[n+1] == NULL)
@@ -3933,7 +3978,7 @@ static void final_merge_env(jl_stenv_t *e, jl_savedenv_t *me, jl_savedenv_t *se)
39333978
else
39343979
merged[n+2] = b2;
39353980
}
3936-
me->buf[n] |= se->buf[n];
3981+
me->buf[m] |= se->buf[m];
39373982
}
39383983
}
39393984

@@ -4489,7 +4534,7 @@ static jl_value_t *_widen_diagonal(jl_value_t *t, jl_varbinding_t *troot) {
44894534

44904535
static jl_value_t *widen_diagonal(jl_value_t *t, jl_unionall_t *u, jl_varbinding_t *troot)
44914536
{
4492-
jl_varbinding_t vb = { u->var, NULL, NULL, 1, 0, 0, 0, 0, 0, 0, 0, 0, NULL, troot };
4537+
jl_varbinding_t vb = { u->var, NULL, NULL, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, NULL, troot };
44934538
jl_value_t *nt;
44944539
JL_GC_PUSH2(&vb.innervars, &nt);
44954540
if (jl_is_unionall(u->body))

test/subtype.jl

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2210,13 +2210,19 @@ let A = Tuple{NTuple{N, Int}, NTuple{N, Int}} where N,
22102210
Bs = (Tuple{Tuple{Int, Vararg{Any}}, Tuple{Int, Int, Vararg{Any}}},
22112211
Tuple{Tuple{Int, Vararg{Any,N1}}, Tuple{Int, Int, Vararg{Any,N2}}} where {N1,N2},
22122212
Tuple{Tuple{Int, Vararg{Any,N}} where {N}, Tuple{Int, Int, Vararg{Any,N}} where {N}})
2213-
Cerr = Tuple{Tuple{Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
2213+
C = Tuple{Tuple{Int, Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
22142214
for B in Bs
2215-
C = typeintersect(A, B)
2216-
@test C == typeintersect(B, A) != Union{}
2217-
@test C != Cerr
2218-
# TODO: The ideal result is Tuple{Tuple{Int, Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
2219-
@test_broken C != Tuple{Tuple{Int, Vararg{Int}}, Tuple{Int, Int, Vararg{Int}}}
2215+
@testintersect(A, B, C)
2216+
end
2217+
A = Tuple{NTuple{N, Int}, Tuple{Int, Vararg{Int, N}}} where N
2218+
C = Tuple{Tuple{Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
2219+
for B in Bs
2220+
@testintersect(A, B, C)
2221+
end
2222+
A = Tuple{Tuple{Int, Vararg{Int, N}}, NTuple{N, Int}} where N
2223+
C = Tuple{Tuple{Int, Int, Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
2224+
for B in Bs
2225+
@testintersect(A, B, C)
22202226
end
22212227
end
22222228

@@ -2229,9 +2235,8 @@ let A = Pair{NTuple{N, Int}, NTuple{N, Int}} where N,
22292235
Bs = (Pair{<:Tuple{Int, Vararg{Int}}, <:Tuple{Int, Int, Vararg{Int}}},
22302236
Pair{Tuple{Int, Vararg{Int,N1}}, Tuple{Int, Int, Vararg{Int,N2}}} where {N1,N2},
22312237
Pair{<:Tuple{Int, Vararg{Int,N}} where {N}, <:Tuple{Int, Int, Vararg{Int,N}} where {N}})
2232-
Cs = (Bs[2], Bs[2], Bs[3])
2233-
for (B, C) in zip(Bs, Cs)
2234-
# TODO: The ideal result is Pair{Tuple{Int, Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
2238+
C = Pair{Tuple{Int, Int, Vararg{Int, N}}, Tuple{Int, Int, Vararg{Int, N}}} where {N}
2239+
for B in Bs
22352240
@testintersect(A, B, C)
22362241
end
22372242
end

0 commit comments

Comments
 (0)