inference: refine slot undef info within then branch of @isdefined

By adding some information to `Conditional`, it is possible to improve the
`undef` information of `slot` within the `then` branch of
`@isdefined slot`.
As a result, it's now possible to prove the `:nothrow`-ness in cases like:
```julia
@test Base.infer_effects((Bool,Int)) do c, x
    local val
    if c
        val = x
    end
    if @isdefined val
        return val
    end
    return zero(Int)
end |> Core.Compiler.is_nothrow
```

base/compiler/abstractinterpretation.jl

@@ -2733,6 +2733,8 @@ function abstract_eval_isdefined(interp::AbstractInterpreter, e::Expr, vtypes::U
             rt = Const(false) # never assigned previously
         elseif !vtyp.undef
             rt = Const(true) # definitely assigned previously
+        else # form `Conditional` to refine `vtyp.undef` in the then branch
+            rt = Conditional(sym, vtyp.typ, vtyp.typ; isdefined=true)
         end
     elseif isa(sym, GlobalRef)
         if InferenceParams(interp).assume_bindings_static
@@ -3205,7 +3207,7 @@ end
 @inline function abstract_eval_basic_statement(interp::AbstractInterpreter,
     @nospecialize(stmt), pc_vartable::VarTable, frame::InferenceState)
     if isa(stmt, NewvarNode)
-        changes = StateUpdate(stmt.slot, VarState(Bottom, true), false)
+        changes = StateUpdate(stmt.slot, VarState(Bottom, true))
         return BasicStmtChange(changes, nothing, Union{})
     elseif !isa(stmt, Expr)
         (; rt, exct) = abstract_eval_statement(interp, stmt, pc_vartable, frame)
@@ -3220,7 +3222,7 @@ end
         end
         lhs = stmt.args[1]
         if isa(lhs, SlotNumber)
-            changes = StateUpdate(lhs, VarState(rt, false), false)
+            changes = StateUpdate(lhs, VarState(rt, false))
         elseif isa(lhs, GlobalRef)
             handle_global_assignment!(interp, frame, lhs, rt)
         elseif !isa(lhs, SSAValue)
@@ -3230,7 +3232,7 @@ end
     elseif hd === :method
         fname = stmt.args[1]
         if isa(fname, SlotNumber)
-            changes = StateUpdate(fname, VarState(Any, false), false)
+            changes = StateUpdate(fname, VarState(Any, false))
         end
         return BasicStmtChange(changes, nothing, Union{})
     elseif (hd === :code_coverage_effect || (
@@ -3576,7 +3578,7 @@ function apply_refinement!(𝕃ᵢ::AbstractLattice, slot::SlotNumber, @nospecia
     oldtyp = vtype.typ
     ⊏ = strictpartialorder(𝕃ᵢ)
     if newtyp ⊏ oldtyp
-        stmtupdate = StateUpdate(slot, VarState(newtyp, vtype.undef), false)
+        stmtupdate = StateUpdate(slot, VarState(newtyp, vtype.undef))
         stoverwrite1!(currstate, stmtupdate)
     end
 end
@@ -3600,7 +3602,9 @@ function conditional_change(𝕃ᵢ::AbstractLattice, currstate::VarTable, condt
         # "causes" since we ignored those in the comparison
         newtyp = tmerge(𝕃ᵢ, newtyp, LimitedAccuracy(Bottom, oldtyp.causes))
     end
-    return StateUpdate(SlotNumber(condt.slot), VarState(newtyp, vtype.undef), true)
+    # if this `Conditional` is from from `@isdefined condt.slot`, refine its `undef` information
+    newundef = condt.isdefined ? !then_or_else : vtype.undef
+    return StateUpdate(SlotNumber(condt.slot), VarState(newtyp, newundef), #=conditional=#true)
 end
 
 function condition_object_change(currstate::VarTable, condt::Conditional,
@@ -3609,7 +3613,7 @@ function condition_object_change(currstate::VarTable, condt::Conditional,
     newcondt = Conditional(condt.slot,
         then_or_else ? condt.thentype : Union{},
         then_or_else ? Union{} : condt.elsetype)
-    return StateUpdate(condslot, VarState(newcondt, vtype.undef), false)
+    return StateUpdate(condslot, VarState(newcondt, vtype.undef))
 end
 
 # make as much progress on `frame` as possible (by handling cycles)

base/compiler/typelattice.jl

@@ -73,14 +73,19 @@ struct Conditional
     slot::Int
     thentype
     elsetype
-    function Conditional(slot::Int, @nospecialize(thentype), @nospecialize(elsetype))
+    # `isdefined` indicates this `Conditional` is from `@isdefined slot`, implying that
+    # the `undef` information of `slot` can be improved in the then branch.
+    # Since this is only beneficial for local inference, it is not translated into `InterConditional`.
+    isdefined::Bool
+    function Conditional(slot::Int, @nospecialize(thentype), @nospecialize(elsetype);
+                         isdefined::Bool=false)
         assert_nested_slotwrapper(thentype)
         assert_nested_slotwrapper(elsetype)
-        return new(slot, thentype, elsetype)
+        return new(slot, thentype, elsetype, isdefined)
     end
 end
-Conditional(var::SlotNumber, @nospecialize(thentype), @nospecialize(elsetype)) =
-    Conditional(slot_id(var), thentype, elsetype)
+Conditional(var::SlotNumber, @nospecialize(thentype), @nospecialize(elsetype); isdefined::Bool=false) =
+    Conditional(slot_id(var), thentype, elsetype, isdefined)
 
 import Core: InterConditional
 """
@@ -180,6 +185,7 @@ struct StateUpdate
     var::SlotNumber
     vtype::VarState
     conditional::Bool
+    StateUpdate(var::SlotNumber, vtype::VarState, conditional::Bool=false) = new(var, vtype, conditional)
 end
 
 """
@@ -305,11 +311,17 @@ end
 
 # `Conditional` and `InterConditional` are valid in opposite contexts
 # (i.e. local inference and inter-procedural call), as such they will never be compared
-@nospecializeinfer function issubconditional(lattice::AbstractLattice, a::C, b::C) where {C<:AnyConditional}
+@nospecializeinfer issubconditional(𝕃::AbstractLattice, a::Conditional, b::Conditional) =
+    _issubconditional(𝕃, a, b, #=check_isdefined=#true)
+@nospecializeinfer issubconditional(𝕃::AbstractLattice, a::InterConditional, b::InterConditional) =
+    _issubconditional(𝕃, a, b, #=check_isdefined=#false)
+@nospecializeinfer function _issubconditional(𝕃::AbstractLattice, a::C, b::C, check_isdefined::Bool) where C<:AnyConditional
     if is_same_conditionals(a, b)
-        if ⊑(lattice, a.thentype, b.thentype)
-            if ⊑(lattice, a.elsetype, b.elsetype)
-                return true
+        if ⊑(𝕃, a.thentype, b.thentype)
+            if ⊑(𝕃, a.elsetype, b.elsetype)
+                if !check_isdefined || a.isdefined ≥ b.isdefined
+                    return true
+                end
             end
         end
     end

test/compiler/inference.jl

@@ -6050,6 +6050,18 @@ end |> Core.Compiler.is_nothrow
     return nothing
 end |> Core.Compiler.is_nothrow
 
+# refine `undef` information from `@isdefined` check
+@test Base.infer_effects((Bool,Int)) do c, x
+    local val
+    if c
+        val = x
+    end
+    if @isdefined val
+        return val
+    end
+    return zero(Int)
+end |> Core.Compiler.is_nothrow
+
 # End to end test case for the partially initialized struct with `PartialStruct`
 @noinline broadcast_noescape1(a) = (broadcast(identity, a); nothing)
 @test fully_eliminated() do