Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

inference: inter-procedural conditional constraint back-propagation #38905

Merged
merged 3 commits into from
Feb 26, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions base/boot.jl
Original file line number Diff line number Diff line change
Expand Up @@ -425,6 +425,7 @@ eval(Core, :(CodeInstance(mi::MethodInstance, @nospecialize(rettype), @nospecial
eval(Core, :(Const(@nospecialize(v)) = $(Expr(:new, :Const, :v))))
eval(Core, :(PartialStruct(@nospecialize(typ), fields::Array{Any, 1}) = $(Expr(:new, :PartialStruct, :typ, :fields))))
eval(Core, :(PartialOpaque(@nospecialize(typ), @nospecialize(env), isva::Bool, parent::MethodInstance, source::Method) = $(Expr(:new, :PartialOpaque, :typ, :env, :isva, :parent, :source))))
eval(Core, :(InterConditional(slot::Int, @nospecialize(vtype), @nospecialize(elsetype)) = $(Expr(:new, :InterConditional, :slot, :vtype, :elsetype))))
eval(Core, :(MethodMatch(@nospecialize(spec_types), sparams::SimpleVector, method::Method, fully_covers::Bool) =
$(Expr(:new, :MethodMatch, :spec_types, :sparams, :method, :fully_covers))))

Expand Down
256 changes: 224 additions & 32 deletions base/compiler/abstractinterpretation.jl

Large diffs are not rendered by default.

19 changes: 13 additions & 6 deletions base/compiler/typeinfer.jl
Original file line number Diff line number Diff line change
Expand Up @@ -298,6 +298,9 @@ function CodeInstance(result::InferenceResult, @nospecialize(inferred_result::An
elseif isa(result_type, PartialStruct)
rettype_const = result_type.fields
const_flags = 0x2
elseif isa(result_type, InterConditional)
rettype_const = result_type
const_flags = 0x2
else
rettype_const = nothing
const_flags = 0x00
Expand Down Expand Up @@ -773,16 +776,20 @@ function typeinf_edge(interp::AbstractInterpreter, method::Method, @nospecialize
code = get(code_cache(interp), mi, nothing)
if code isa CodeInstance # return existing rettype if the code is already inferred
update_valid_age!(caller, WorldRange(min_world(code), max_world(code)))
rettype = code.rettype
if isdefined(code, :rettype_const)
if isa(code.rettype_const, Vector{Any}) && !(Vector{Any} <: code.rettype)
return PartialStruct(code.rettype, code.rettype_const), mi
elseif code.rettype <: Core.OpaqueClosure && isa(code.rettype_const, PartialOpaque)
return code.rettype_const, mi
rettype_const = code.rettype_const
if isa(rettype_const, Vector{Any}) && !(Vector{Any} <: rettype)
return PartialStruct(rettype, rettype_const), mi
elseif rettype <: Core.OpaqueClosure && isa(rettype_const, PartialOpaque)
return rettype_const, mi
elseif isa(rettype_const, InterConditional)
return rettype_const, mi
else
return Const(code.rettype_const), mi
return Const(rettype_const), mi
end
else
return code.rettype, mi
return rettype, mi
end
end
if ccall(:jl_get_module_infer, Cint, (Any,), method.module) == 0
Expand Down
43 changes: 29 additions & 14 deletions base/compiler/typelattice.jl
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
# structs/constants #
#####################

# N.B.: Const/PartialStruct are defined in Core, to allow them to be used
# N.B.: Const/PartialStruct/InterConditional are defined in Core, to allow them to be used
# inside the global code cache.
#
# # The type of a value might be constant
Expand All @@ -18,7 +18,6 @@
# end
import Core: Const, PartialStruct


# The type of this value might be Bool.
# However, to enable a limited amount of back-propagagation,
# we also keep some information about how this Bool value was created.
Expand All @@ -45,6 +44,18 @@ struct Conditional
end
end

# # Similar to `Conditional`, but conveys inter-procedural constraints imposed on call arguments.
# # This is separate from `Conditional` to catch logic errors: the lattice element name is InterConditional
# # while processing a call, then Conditional everywhere else. Thus InterConditional does not appear in
# # CompilerTypes—these type's usages are disjoint—though we define the lattice for InterConditional.
# struct InterConditional
# slot::Int
# vtype
# elsetype
# end
import Core: InterConditional
const AnyConditional = Union{Conditional,InterConditional}
aviatesk marked this conversation as resolved.
Show resolved Hide resolved

struct PartialTypeVar
tv::TypeVar
# N.B.: Currently unused, but would allow turning something back
Expand Down Expand Up @@ -101,11 +112,10 @@ const CompilerTypes = Union{MaybeUndef, Const, Conditional, NotFound, PartialStr
# lattice logic #
#################

function issubconditional(a::Conditional, b::Conditional)
avar = a.var
bvar = b.var
if (isa(avar, Slot) && isa(bvar, Slot) && slot_id(avar) === slot_id(bvar)) ||
(isa(avar, SSAValue) && isa(bvar, SSAValue) && avar === bvar)
# `Conditional` and `InterConditional` are valid in opposite contexts
# (i.e. local inference and inter-procedural call), as such they will never be compared
function issubconditional(a::C, b::C) where {C<:AnyConditional}
if is_same_conditionals(a, b)
if a.vtype ⊑ b.vtype
if a.elsetype ⊑ b.elsetype
return true
Expand All @@ -115,8 +125,13 @@ function issubconditional(a::Conditional, b::Conditional)
return false
end

maybe_extract_const_bool(c::Const) = isa(c.val, Bool) ? c.val : nothing
function maybe_extract_const_bool(c::Conditional)
is_same_conditionals(a::Conditional, b::Conditional) = slot_id(a.var) === slot_id(b.var)
is_same_conditionals(a::InterConditional, b::InterConditional) = a.slot === b.slot

is_lattice_bool(@nospecialize(typ)) = typ !== Bottom && typ ⊑ Bool

maybe_extract_const_bool(c::Const) = (val = c.val; isa(val, Bool)) ? val : nothing
function maybe_extract_const_bool(c::AnyConditional)
(c.vtype === Bottom && !(c.elsetype === Bottom)) && return false
(c.elsetype === Bottom && !(c.vtype === Bottom)) && return true
nothing
Expand Down Expand Up @@ -145,14 +160,14 @@ function ⊑(@nospecialize(a), @nospecialize(b))
b === Union{} && return false
@assert !isa(a, TypeVar) "invalid lattice item"
@assert !isa(b, TypeVar) "invalid lattice item"
if isa(a, Conditional)
if isa(b, Conditional)
if isa(a, AnyConditional)
if isa(b, AnyConditional)
return issubconditional(a, b)
elseif isa(b, Const) && isa(b.val, Bool)
return maybe_extract_const_bool(a) === b.val
end
a = Bool
elseif isa(b, Conditional)
elseif isa(b, AnyConditional)
return false
end
if isa(a, PartialStruct)
Expand Down Expand Up @@ -251,7 +266,7 @@ function is_lattice_equal(@nospecialize(a), @nospecialize(b))
return a ⊑ b && b ⊑ a
end

widenconst(c::Conditional) = Bool
widenconst(c::AnyConditional) = Bool
function widenconst(c::Const)
if isa(c.val, Type)
if isvarargtype(c.val)
Expand Down Expand Up @@ -286,7 +301,7 @@ end
@inline schanged(@nospecialize(n), @nospecialize(o)) = (n !== o) && (o === NOT_FOUND || (n !== NOT_FOUND && !issubstate(n, o)))

widenconditional(@nospecialize typ) = typ
function widenconditional(typ::Conditional)
function widenconditional(typ::AnyConditional)
if typ.vtype === Union{}
return Const(false)
elseif typ.elsetype === Union{}
Expand Down
32 changes: 31 additions & 1 deletion base/compiler/typelimits.jl
Original file line number Diff line number Diff line change
Expand Up @@ -334,7 +334,7 @@ function tmerge(@nospecialize(typea), @nospecialize(typeb))
end
end
if isa(typea, Conditional) && isa(typeb, Conditional)
if typea.var === typeb.var
if is_same_conditionals(typea, typeb)
vtype = tmerge(typea.vtype, typeb.vtype)
elsetype = tmerge(typea.elsetype, typeb.elsetype)
if vtype != elsetype
Expand All @@ -347,6 +347,36 @@ function tmerge(@nospecialize(typea), @nospecialize(typeb))
end
return Bool
end
# type-lattice for InterConditional wrapper, InterConditional will never be merged with Conditional
if isa(typea, InterConditional) && isa(typeb, Const)
if typeb.val === true
typeb = InterConditional(typea.slot, Any, Union{})
elseif typeb.val === false
typeb = InterConditional(typea.slot, Union{}, Any)
end
end
if isa(typeb, InterConditional) && isa(typea, Const)
if typea.val === true
typea = InterConditional(typeb.slot, Any, Union{})
elseif typea.val === false
typea = InterConditional(typeb.slot, Union{}, Any)
end
end
if isa(typea, InterConditional) && isa(typeb, InterConditional)
if is_same_conditionals(typea, typeb)
vtype = tmerge(typea.vtype, typeb.vtype)
elsetype = tmerge(typea.elsetype, typeb.elsetype)
if vtype != elsetype
return InterConditional(typea.slot, vtype, elsetype)
end
end
val = maybe_extract_const_bool(typea)
if val isa Bool && val === maybe_extract_const_bool(typeb)
return Const(val)
end
return Bool
end
# type-lattice for Const and PartialStruct wrappers
if (isa(typea, PartialStruct) || isa(typea, Const)) &&
(isa(typeb, PartialStruct) || isa(typeb, Const)) &&
widenconst(typea) === widenconst(typeb)
Expand Down
3 changes: 1 addition & 2 deletions base/essentials.jl
Original file line number Diff line number Diff line change
Expand Up @@ -817,8 +817,7 @@ const missing = Missing()

Indicate whether `x` is [`missing`](@ref).
"""
ismissing(::Any) = false
ismissing(::Missing) = true
ismissing(x) = x === missing
aviatesk marked this conversation as resolved.
Show resolved Hide resolved
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@vtjnash should I revert back to the previous ismissing/isnothing definitions ?
I believe the less method definitions the better, because we can keep to use InterConditional logic as far as there're ≦3 methods even after a package defines new methods for them.

xref: https://github.com/JuliaLang/julia/pull/38905/files#r552878124


function popfirst! end

Expand Down
2 changes: 1 addition & 1 deletion base/show.jl
Original file line number Diff line number Diff line change
Expand Up @@ -1382,7 +1382,7 @@ function operator_associativity(s::Symbol)
end

is_expr(@nospecialize(ex), head::Symbol) = isa(ex, Expr) && (ex.head === head)
is_expr(@nospecialize(ex), head::Symbol, n::Int) = is_expr(ex, head) && length((ex::Expr).args) == n
is_expr(@nospecialize(ex), head::Symbol, n::Int) = is_expr(ex, head) && length(ex.args) == n

is_quoted(ex) = false
is_quoted(ex::QuoteNode) = true
Expand Down
3 changes: 1 addition & 2 deletions base/some.jl
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,7 @@ Return `true` if `x === nothing`, and return `false` if not.
!!! compat "Julia 1.1"
This function requires at least Julia 1.1.
"""
isnothing(::Any) = false
isnothing(::Nothing) = true
isnothing(x) = x === nothing


"""
Expand Down
1 change: 1 addition & 0 deletions src/builtins.c
Original file line number Diff line number Diff line change
Expand Up @@ -1616,6 +1616,7 @@ void jl_init_primitives(void) JL_GC_DISABLED
add_builtin("Const", (jl_value_t*)jl_const_type);
add_builtin("PartialStruct", (jl_value_t*)jl_partial_struct_type);
add_builtin("PartialOpaque", (jl_value_t*)jl_partial_opaque_type);
add_builtin("InterConditional", (jl_value_t*)jl_interconditional_type);
add_builtin("MethodMatch", (jl_value_t*)jl_method_match_type);
add_builtin("IntrinsicFunction", (jl_value_t*)jl_intrinsic_type);
add_builtin("Function", (jl_value_t*)jl_function_type);
Expand Down
1 change: 1 addition & 0 deletions src/jl_exported_data.inc
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@
XX(jl_number_type) \
XX(jl_partial_struct_type) \
XX(jl_partial_opaque_type) \
XX(jl_interconditional_type) \
XX(jl_phicnode_type) \
XX(jl_phinode_type) \
XX(jl_pinode_type) \
Expand Down
4 changes: 4 additions & 0 deletions src/jltypes.c
Original file line number Diff line number Diff line change
Expand Up @@ -2308,6 +2308,10 @@ void jl_init_types(void) JL_GC_DISABLED
jl_perm_symsvec(2, "typ", "fields"),
jl_svec2(jl_any_type, jl_array_any_type), 0, 0, 2);

jl_interconditional_type = jl_new_datatype(jl_symbol("InterConditional"), core, jl_any_type, jl_emptysvec,
jl_perm_symsvec(3, "slot", "vtype", "elsetype"),
jl_svec(3, jl_long_type, jl_any_type, jl_any_type), 0, 0, 3);

jl_method_match_type = jl_new_datatype(jl_symbol("MethodMatch"), core, jl_any_type, jl_emptysvec,
jl_perm_symsvec(4, "spec_types", "sparams", "method", "fully_covers"),
jl_svec(4, jl_type_type, jl_simplevector_type, jl_method_type, jl_bool_type), 0, 0, 4);
Expand Down
1 change: 1 addition & 0 deletions src/julia.h
Original file line number Diff line number Diff line change
Expand Up @@ -634,6 +634,7 @@ extern JL_DLLIMPORT jl_datatype_t *jl_argument_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_datatype_t *jl_const_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_datatype_t *jl_partial_struct_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_datatype_t *jl_partial_opaque_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_datatype_t *jl_interconditional_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_datatype_t *jl_method_match_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_datatype_t *jl_simplevector_type JL_GLOBALLY_ROOTED;
extern JL_DLLIMPORT jl_typename_t *jl_tuple_typename JL_GLOBALLY_ROOTED;
Expand Down
3 changes: 2 additions & 1 deletion src/staticdata.c
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ extern "C" {
// TODO: put WeakRefs on the weak_refs list during deserialization
// TODO: handle finalizers

#define NUM_TAGS 146
#define NUM_TAGS 147

// An array of references that need to be restored from the sysimg
// This is a manually constructed dual of the gvars array, which would be produced by codegen for Julia code, for C.
Expand Down Expand Up @@ -69,6 +69,7 @@ jl_value_t **const*const get_tags(void) {
INSERT_TAG(jl_const_type);
INSERT_TAG(jl_partial_struct_type);
INSERT_TAG(jl_partial_opaque_type);
INSERT_TAG(jl_interconditional_type);
INSERT_TAG(jl_method_match_type);
INSERT_TAG(jl_pinode_type);
INSERT_TAG(jl_phinode_type);
Expand Down
75 changes: 74 additions & 1 deletion test/compiler/inference.jl
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ tmerge_test(Tuple{}, Tuple{Complex, Vararg{Union{ComplexF32, ComplexF64}}},
@test Core.Compiler.tmerge(Vector{Int}, Core.Compiler.tmerge(Vector{String}, Vector{Bool})) == Vector
@test Core.Compiler.tmerge(Base.BitIntegerType, Union{}) === Base.BitIntegerType
@test Core.Compiler.tmerge(Union{}, Base.BitIntegerType) === Base.BitIntegerType
@test Core.Compiler.tmerge(Core.Compiler.InterConditional(1, Int, Union{}), Core.Compiler.InterConditional(2, String, Union{})) === Core.Compiler.Const(true)

struct SomethingBits
x::Base.BitIntegerType
Expand Down Expand Up @@ -1255,7 +1256,8 @@ end
push!(constvec, 10)
@test @inferred(sizeof_constvec()) == sizeof(Int) * 4

test_const_return((x)->isdefined(x, :re), Tuple{ComplexF64}, true)
test_const_return(x->isdefined(x, :re), Tuple{ComplexF64}, true)

isdefined_f3(x) = isdefined(x, 3)
@test @inferred(isdefined_f3(())) == false
@test find_call(first(code_typed(isdefined_f3, Tuple{Tuple{Vararg{Int}}})[1]), isdefined, 3)
Expand Down Expand Up @@ -1722,6 +1724,77 @@ for expr25261 in opt25261[i:end]
end
@test foundslot

@testset "inter-procedural conditional constraint propagation" begin
# simple cases
isaint(a) = isa(a, Int)
@test Base.return_types((Any,)) do a
isaint(a) && return a # a::Int
return 0
end == Any[Int]
eqnothing(a) = a === nothing
@test Base.return_types((Union{Nothing,Int},)) do a
eqnothing(a) && return 0
return a # a::Int
end == Any[Int]

# more complicated cases
ispositive(a) = isa(a, Int) && a > 0
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This may be fixable, and highlights a complex oddity of how Conditional behaves in the lattice. The problem is this PR doesn't scan the vtypes list to realize the type of a is actually constrained in BB#3, so it over-approximates the true return type to be Bool. The true result type in BB#2 is Conditional(:a@2, Int, Int). Along with the result type in BB#3 being Conditional(:a@2, Union{}, Any). Thus the correctly computed return type should have been InterConditional(:a@2, Int, Any) after the tmerge of those two.

julia> @code_lowered ispositive(1)
CodeInfo(
1 ─ %1 = a isa Main.Int
└──      goto #3 if not %1
2 ─ %3 = a > 0
└──      return %3
3 ─      return false

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes, I think we can change our local inference logic so that we can annotate Conditional for a statement (e.g. %5) with considering where it comes from (e.g. %1), but I didn't try to tackle that in this PR because I felt the changes can be huge.
Maybe we can merge this PR with only introducing InterConditional and leave this as a future work (in a separate PR) ?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The change should be pretty simple, though probably doesn't need to be in this PR: if the inferred result is <: Bool, then it is actually Conditional for the entire VarTable s[pc][1:nargs]. The annoying part then is that InterConditional can only represent exactly one of those args, so you may have to just pick the first interesting one. (conceptually, this is a also a generalizable observation on what Conditional represents: either it's an alternative VarTable based on a particular value comparison result—or the main VarTable s is a Conditional on the program state)

Copy link
Member Author

@aviatesk aviatesk Dec 26, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, with the following diff, we can back-propagate constraints in cases like ispositive and also some cases like
the original definitions of isnothing and ismissing (it looks dirty, though):

diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 98b8b1c9c9..0e74c83787 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -1300,6 +1300,7 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
     W = frame.ip
     s = frame.stmt_types
     n = frame.nstmts
+    nargs = frame.nargs
     while frame.pc´´ <= n
         # make progress on the active ip set
         local pc::Int = frame.pc´´ # current program-counter
@@ -1362,6 +1363,25 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
             elseif isa(stmt, ReturnNode)
                 pc´ = n + 1
                 rt = abstract_eval_value(interp, stmt.val, s[pc], frame)
+                if isa(rt, Conditional) && !(1  slot_id(rt.var)  nargs)
+                    # discard this `Conditional` imposed on non-call arguments,
+                    # since it's not interesting in inter-procedural context;
+                    # we may give constraints on other call argument
+                    rt = widenconditional(rt)
+                end
+                if !isa(rt, Conditional) && rt !== Bottom && rt  Bool
+                    if isa(frame.bestguess, Conditional)
+                        # if the bestguess so far is already `Conditional`, try to convert
+                        # this `rt` into `Conditional` on the slot to avoid overapproximation
+                        # due to conflict of different slots
+                        rt = boolean_rt_to_conditional(rt, changes, slot_id(frame.bestguess.var))
+                    elseif nargs  1
+                        # pick up the first "interesting" slot, convert `rt` to its `Conditional`
+                        # TODO: this is very naive heuristic, ideally we want something like
+                        # alternative `VarTable` that keeps conditional constraints on all the variables
+                        rt = boolean_rt_to_conditional(rt, changes, nargs == 1 ? 1 : 2)
+                    end
+                end
                 if !isa(rt, Const) &&
                    !isa(rt, Type) &&
                    !isa(rt, PartialStruct) &&
@@ -1478,6 +1498,20 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
     nothing
 end
 
+function boolean_rt_to_conditional(@nospecialize(rt), state::VarTable, slot_id::Int)
+    typ = widenconditional((state[slot_id]::VarState).typ) # avoid nested conditional
+    if isa(rt, Const)
+        if rt.val === true
+            return Conditional(SlotNumber(slot_id), typ, Bottom)
+        elseif rt.val === false
+            return Conditional(SlotNumber(slot_id), Bottom, typ)
+        end
+    elseif rt === Bool
+        return Conditional(SlotNumber(slot_id), typ, typ)
+    end
+    return rt # when `rt` is Union{}, etc.
+end
+
 # make as much progress on `frame` as possible (by handling cycles)
 function typeinf_nocycle(interp::AbstractInterpreter, frame::InferenceState)
     typeinf_local(interp, frame)

But I couldn't succeed to bootstrap with this (with fatal error in type inference (type bound) error)..
Do you have any pointer about where to fix ?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On closer inspection, I think you're missing bestguess_to_interprocedural on some of the uses of bestguess. While you could grep each usage, I think it might be better to consolidate it here: (I thought the new assert should have caught that)

diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 98b8b1c9c9..c76c61e89b 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -1362,14 +1362,11 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
             elseif isa(stmt, ReturnNode)
                 pc´ = n + 1
                 rt = abstract_eval_value(interp, stmt.val, s[pc], frame)
-                if !isa(rt, Const) &&
-                   !isa(rt, Type) &&
-                   !isa(rt, PartialStruct) &&
-                   !isa(rt, Conditional)
-                    # only propagate information we know we can store
-                    # and is valid inter-procedurally
-                    # some of them will further be transformed by `bestguess_to_interprocedural`
-                    # in `finish(::InferenceState, ::AbstractInterpreter)`
+                # only propagate information we know we can store
+                # and is valid inter-procedurally
+                if isa(rt, Conditional)
+                    rt = bestguess_to_interprocedural(rt, frame.nargs)
+                elseif !isa(rt, Const) && !isa(rt, Type) && !isa(rt, PartialStruct)
                     rt = widenconst(rt)
                 end
                 if tchanged(rt, frame.bestguess)
diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl
index 8a2d22b252..6cbe1fb5f0 100644
--- a/base/compiler/typeinfer.jl
+++ b/base/compiler/typeinfer.jl
@@ -416,11 +416,10 @@ function finish(me::InferenceState, interp::AbstractInterpreter)
         me.result.src = OptimizationState(me, OptimizationParams(interp), interp)
     end
     me.result.valid_worlds = me.valid_worlds
-    me.result.result = me.bestguess = bestguess_to_interprocedural(me.bestguess, me.nargs)
+    me.result.result = me.bestguess
     nothing
 end
 
-bestguess_to_interprocedural(@nospecialize(bestguess), _::Int) = bestguess
 function bestguess_to_interprocedural(bestguess::Conditional, nargs::Int)
     # convert `Conditional` into `InterConditional` only when it imposes constrains on
     # any of call argument
@@ -787,7 +786,7 @@ function typeinf_edge(interp::AbstractInterpreter, method::Method, @nospecialize
     # return the current knowledge about this cycle
     frame = frame::InferenceState
     update_valid_age!(frame, caller)
-    return bestguess_to_interprocedural(frame.bestguess, frame.nargs), nothing
+    return frame.bestguess, nothing
 end
 
 #### entry points for inferring a MethodInstance given a type signature ####

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, dug deeper and found it is due to missing handling of Vararg expansion in this PR. Here's a reduced repro. Note how the x... turned into a x::Tuple{Symbol} type description (which will fail at runtime, because actually we know that x::Symbol there)

julia> code_typed(mapfilter, (typeof((x...) -> !isa(x, Tuple{Integer})), typeof(Base.delete!), Base.Set{Union{Int64, Symbol}}, Base.Set{Union{Int64, Symbol}}) , optimize=false)                       
1-element Vector{Any}:                                                                             
 CodeInfo(                                                                                         
    @ REPL[8]:2 within `mapfilter'                                                                                                                                                                     
1 ─ %1  = a::Set{Union{Int64, Symbol}}                                                                                                                                                                 
│         (@_6 = Base.iterate(%1))::Union{Nothing, Tuple{Union{Int64, Symbol}, Int64}}             
│   %3  = (@_6 === nothing)::Bool                                                                  
│   %4  = Base.not_int(%3)::Bool                                                                   
└──       goto #6 if not %4                                                                        
2 ┄ %6  = @_6::Tuple{Union{Int64, Symbol}, Int64}::Tuple{Union{Int64, Symbol}, Int64}              
│         (x = Core.getfield(%6, 1))::Union{Int64, Symbol}                                                                                                                                             
│   %8  = Core.getfield(%6, 2)::Int64                                                              
│   @ REPL[8]:3 within `mapfilter'                                                                 
│   %9  = (pred)(x)::Bool                                                                          
└──       goto #4 if not %9                                                                        
3 ─       (f)(b, x::Tuple{Symbol})::Any                                                                                                                                                                
└──       goto #4                                                                                  
4 ┄       (@_6 = Base.iterate(%1, %8))::Union{Nothing, Tuple{Union{Int64, Symbol}, Int64}}         
│   %14 = (@_6 === nothing)::Bool                                                                                                                                                                      
│   %15 = Base.not_int(%14)::Bool                                                                  
└──       goto #6 if not %15                                                                                                                                                                           
5 ─       goto #2                                                                                  
6 ┄       return nothing                                                                           
) => Nothing                              

julia> s = Set{Union{Int,Symbol}}((:a, 1)); mapfilter((x...) -> !isa(x, Tuple{Integer}), delete!, s, s)
signal (11): Segmentation fault                                                         

(was hoping to be able to explain simply how I found this, but ended up being a bit convoluted. Mostly I ran under rr until exit, then ran backwards to break jl_throw, then back to watch on the value of $rip, then back to eval_function a couple times, until I could see the printing of p jl_(src) for the correct p jl_(li) function. I searched this for "fatal" and saw Tuple{Int}, which I could tell was bad, so then it was "just" a matter of guessing different IR inputs until one propagated the type wrong)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks so much for your help !
Unfortunately I'm on macOS and it seems to me that debugging w/ gdb is hard on that platform (rr seems even unavailable ...).
I'll try to get Linux or docker environment to develop Julia, but for now I'd like to move forward this PR.

12e1e79 enhances this PR by eagerly converting boolean conditions into (Inter)Conditionals following your idea.
Now I succeed in bootstrapping but it seems that there're few inference accuracy regressions.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay I just fixed the inference accuracy regression; there're some code that make good use of Const(val::Bool) to improve inference quality (e.g. ifelse tfunc), but now we turn Const(val::Bool) return type into Conditional, and so we need to respect its constant-ness to keep accuracy.
As for ifelse one, I fixed that in fe6accd, but there may be other points that should be tweaked.

Once we've done all of them, I think this PR should be good to go.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, on macOS, lldb is better, but setting up a VM just to run rr in linux is also great (Can you tell rr is one of my favorite magic tools?)

I think we also might want to stick with using Const(::Bool) as the result object when the new type doesn't refine the old type of the Argument (e.g. except when ⊑(s[pc][i], s[1][i])), then choose later (in abstract_call_gf_by_type) to form a tighter bound if union-splitting with napplicable > 1. Note, you can examine fieldtype(sig, n) to find out the type of the nth argument.

@test Base.return_types((Any,)) do a
ispositive(a) && return a # a::Int
return 0
end == Any[Int]
global isaint2
isaint2(a::Int) = true
isaint2(@nospecialize(_)) = false
@test Base.return_types((Any,)) do a
isaint2(a) && return a # a::Int
return 0
end == Any[Int]
global ispositive2
ispositive2(a::Int) = a > 0
ispositive2(@nospecialize(_)) = false
@test Base.return_types((Any,)) do a
ispositive2(a) && return a # a::Int
return 0
end == Any[Int]

# type constraints from multiple constant boolean return types
function f(x)
isa(x, Int) && return true
isa(x, Symbol) && return true
return false
end
@test Base.return_types((Any,)) do x
f(x) && return x # x::Union{Int,Symbol}
return nothing
end == Any[Union{Int,Symbol,Nothing}]

# constraint on non-vararg argument of `isva` method
isaint_isvapositive(a, va...) = isa(a, Int) && sum(va) > 0
@test Base.return_types((Any,Int,Int)) do a, b, c
isaint_isvapositive(a, b, c) && return a # a::Int
0
end == Any[Int]

# with Base functions
@test Base.return_types((Any,)) do a
Base.Fix2(isa, Int)(a) && return a # a::Int
return 0
end == Any[Int]
@test Base.return_types((Union{Nothing,Int},)) do a
isnothing(a) && return 0
return a # a::Int
end == Any[Int]
@test Base.return_types((Union{Missing,Int},)) do a
ismissing(a) && return 0
return a # a::Int
end == Any[Int]
@test Base.return_types((Any,)) do x
Meta.isexpr(x, :call) && return x # x::Expr
return nothing
end == Any[Union{Nothing,Expr}]
end

function f25579(g)
h = g[]
t = (h === nothing)
Expand Down