From bc0054690470f4b6cfe63b46fff833804c359dd8 Mon Sep 17 00:00:00 2001 From: Jeff Bezanson Date: Thu, 12 Aug 2021 13:04:53 -0400 Subject: [PATCH] give wider/safer intersection result for vars used in both invariant and covariant position fixes #41738 --- src/subtype.c | 62 ++++++++++++++++++++++++++----------------------- test/subtype.jl | 18 +++++++++++--- 2 files changed, 48 insertions(+), 32 deletions(-) diff --git a/src/subtype.c b/src/subtype.c index 572916a34fe88..55e0fc5e22dbf 100644 --- a/src/subtype.c +++ b/src/subtype.c @@ -92,6 +92,7 @@ typedef struct jl_stenv_t { int ignore_free; // treat free vars as black boxes; used during intersection int intersection; // true iff subtype is being called from intersection int emptiness_only; // true iff intersection only needs to test for emptiness + int triangular; // when intersecting Ref{X} with Ref{<:Y} } jl_stenv_t; // state manipulation utilities @@ -1411,6 +1412,7 @@ static void init_stenv(jl_stenv_t *e, jl_value_t **env, int envsz) e->ignore_free = 0; e->intersection = 0; e->emptiness_only = 0; + e->triangular = 0; e->Lunions.depth = 0; e->Runions.depth = 0; e->Lunions.more = 0; e->Runions.more = 0; } @@ -2169,7 +2171,7 @@ static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_sten return; jl_varbinding_t *btemp = e->vars; while (btemp != NULL) { - if (btemp->lb == (jl_value_t*)v && btemp->ub == (jl_value_t*)v && + if ((btemp->lb == (jl_value_t*)v || btemp->ub == (jl_value_t*)v) && in_union(val, (jl_value_t*)btemp->var)) return; btemp = btemp->prev; @@ -2221,6 +2223,21 @@ static int reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e) return reachable_var(xv->ub, y, e) || reachable_var(xv->lb, y, e); } +// check whether setting v == t implies v == SomeType{v}, which is unsatisfiable. +static int check_unsat_bound(jl_value_t *t, jl_tvar_t *v, jl_stenv_t *e) JL_NOTSAFEPOINT +{ + if (var_occurs_inside(t, v, 0, 0)) + return 1; + jl_varbinding_t *btemp = e->vars; + while (btemp != NULL) { + if (btemp->lb == (jl_value_t*)v && btemp->ub == (jl_value_t*)v && + var_occurs_inside(t, btemp->var, 0, 0)) + return 1; + btemp = btemp->prev; + } + return 0; +} + static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int8_t R, int param) { jl_varbinding_t *bb = lookup(e, b); @@ -2250,7 +2267,9 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int ub = a; } else { + e->triangular++; ub = R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d); + e->triangular--; save_env(e, &root, &se); int issub = subtype_in_env_existential(bb->lb, ub, e, 0, d); restore_env(e, root, &se); @@ -2262,20 +2281,10 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int } if (ub != (jl_value_t*)b) { if (jl_has_free_typevars(ub)) { - // constraint X == Ref{X} is unsatisfiable. also check variables set equal to X. - if (var_occurs_inside(ub, b, 0, 0)) { + if (check_unsat_bound(ub, b, e)) { JL_GC_POP(); return jl_bottom_type; } - jl_varbinding_t *btemp = e->vars; - while (btemp != NULL) { - if (btemp->lb == (jl_value_t*)b && btemp->ub == (jl_value_t*)b && - var_occurs_inside(ub, btemp->var, 0, 0)) { - JL_GC_POP(); - return jl_bottom_type; - } - btemp = btemp->prev; - } } bb->ub = ub; bb->lb = ub; @@ -2286,7 +2295,13 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d); if (ub == jl_bottom_type) return jl_bottom_type; - if (bb->constraintkind == 0) { + if (bb->constraintkind == 1 || e->triangular) { + if (e->triangular && check_unsat_bound(ub, b, e)) + return jl_bottom_type; + set_bound(&bb->ub, ub, b, e); + return (jl_value_t*)b; + } + else if (bb->constraintkind == 0) { JL_GC_PUSH1(&ub); if (!jl_is_typevar(a) && try_subtype_in_env(bb->ub, a, e, 0, d)) { JL_GC_POP(); @@ -2295,10 +2310,6 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int JL_GC_POP(); return ub; } - else if (bb->constraintkind == 1) { - set_bound(&bb->ub, ub, b, e); - return (jl_value_t*)b; - } assert(bb->constraintkind == 2); if (!jl_is_typevar(a)) { if (ub == a && bb->lb != jl_bottom_type) @@ -2563,11 +2574,11 @@ static jl_value_t *intersect_unionall_(jl_value_t *t, jl_unionall_t *u, jl_stenv static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_t *e, int8_t R, int param) { - jl_value_t *res=NULL, *res2=NULL, *save=NULL, *save2=NULL; - jl_savedenv_t se, se2; + jl_value_t *res=NULL, *save=NULL; + jl_savedenv_t se; jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, R ? e->Rinvdepth : e->invdepth, 0, NULL, 0, e->vars }; - JL_GC_PUSH6(&res, &save2, &vb.lb, &vb.ub, &save, &vb.innervars); + JL_GC_PUSH5(&res, &vb.lb, &vb.ub, &save, &vb.innervars); save_env(e, &save, &se); res = intersect_unionall_(t, u, e, R, param, &vb); if (res != jl_bottom_type) { @@ -2577,18 +2588,11 @@ static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_ vb.constraintkind = vb.concrete ? 1 : 2; res = intersect_unionall_(t, u, e, R, param, &vb); } - else if (vb.occurs_cov) { - save_env(e, &save2, &se2); + else if (vb.occurs_cov && !var_occurs_invariant(u->body, u->var, 0)) { restore_env(e, save, &se); vb.occurs_cov = vb.occurs_inv = 0; - vb.lb = u->var->lb; vb.ub = u->var->ub; vb.constraintkind = 1; - res2 = intersect_unionall_(t, u, e, R, param, &vb); - if (res2 != jl_bottom_type) - res = res2; - else - restore_env(e, save2, &se2); - free_env(&se2); + res = intersect_unionall_(t, u, e, R, param, &vb); } } free_env(&se); diff --git a/test/subtype.jl b/test/subtype.jl index 7cca4d88ca1eb..cf30c571973f9 100644 --- a/test/subtype.jl +++ b/test/subtype.jl @@ -1577,7 +1577,7 @@ f31082(::Pair{B, C}, ::C, ::C) where {B, C} = 1 Tuple{Type{Val{T}},Int,T} where T) @testintersect(Tuple{Type{Val{T}},Integer,T} where T, Tuple{Type,Int,Integer}, - Tuple{Type{Val{T}},Int,T} where T<:Integer) + Tuple{Type{Val{T}},Int,Integer} where T) @testintersect(Tuple{Type{Val{T}},Integer,T} where T>:Integer, Tuple{Type,Int,Integer}, Tuple{Type{Val{T}},Int,Integer} where T>:Integer) @@ -1866,7 +1866,7 @@ let A = Tuple{Type{T} where T<:Ref, Ref, Union{T, Union{Ref{T}, T}} where T<:Ref I = typeintersect(A,B) # this was a case where <: disagreed with === (due to a badly-normalized type) @test I == typeintersect(A,B) - @test I == Tuple{Type{T}, Ref{T}, Union{Ref{T}, T}} where T<:Ref + @test I == Tuple{Type{T}, Ref{T}, Ref} where T<:Ref end # issue #39218 @@ -1946,9 +1946,21 @@ let A = Tuple{UnionAll, Vector{Any}}, B = Tuple{Type{T}, T} where T<:AbstractArray, I = typeintersect(A, B) @test !isconcretetype(I) - @test_broken I == Tuple{Type{T}, Vector{Any}} where T<:AbstractArray + @test I == Tuple{Type{T}, Vector{Any}} where T<:AbstractArray end @testintersect(Tuple{Type{Vector{<:T}}, T} where {T<:Integer}, Tuple{Type{T}, AbstractArray} where T<:Array, Bottom) + +let A = Tuple{Any, Type{Ref{_A}} where _A}, + B = Tuple{Type{T}, Type{<:Union{Ref{T}, T}}} where T, + I = typeintersect(A, B) + @test I != Union{} + # TODO: this intersection result is still too narrow + @test_broken Tuple{Type{Ref{Integer}}, Type{Ref{Integer}}} <: I +end + +@testintersect(Tuple{Type{T}, T} where T<:(Tuple{Vararg{_A, _B}} where _B where _A), + Tuple{Type{Tuple{Vararg{_A, N}} where _A<:F}, Pair{N, F}} where F where N, + Bottom)