Conditional lattice element is semantically broken in the presence of SSAValues

[Keno]

Ooops:

julia> proj1(a, b) = a
proj1 (generic function with 2 methods)

julia> function foo(a)
           a = Base.inferencebarrier(a)::Union{Int64, Float64}
           if proj1(isa(a, Int64), (a = Base.inferencebarrier(1.0)::Union{Int64, Float64}; true))
                          return a
           end
           return 2
       end
foo (generic function with 2 methods)

julia> foo(1)
4607182418800017408

Basically, this code doesn't know about SSAValues:

julia/base/compiler/typelattice.jl

Lines 749 to 757 in 86cba99

	function invalidate_slotwrapper(vt::VarState, changeid::Int, ignore_conditional::Bool)
	newtyp = ignorelimited(vt.typ)
	if (!ignore_conditional && isa(newtyp, Conditional) && newtyp.slot == changeid) ||
	(isa(newtyp, MustAlias) && newtyp.slot == changeid)
	newtyp = @noinline widenwrappedslotwrapper(vt.typ)
	return VarState(newtyp, vt.undef)
	end
	return nothing
	end

But it's not clear what a sound way to change that is.

[aviatesk]

We might need to pass InferenceState to stupdate! or stoverwrite! and call ssa_def_slot from there

julia/base/compiler/abstractinterpretation.jl

Lines 1443 to 1492 in 8483130

	# This is only for use with `Conditional`.
	# In general, usage of this is wrong.
	function ssa_def_slot(@nospecialize(arg), sv::InferenceState)
	code = sv.src.code
	init = sv.currpc
	while isa(arg, SSAValue)
	init = arg.id
	arg = code[init]
	end
	if arg isa SlotNumber
	# found this kind of pattern:
	# %init = SlotNumber(x)
	# [...]
	# goto if not isa(%init, T)
	# now conservatively make sure there isn't potentially another conflicting assignment
	# to the same slot between the def and usage
	# we can assume the IR is sorted, since the front-end only creates SSA values in order
	for i = init:(sv.currpc-1)
	e = code[i]
	if isexpr(e, :(=)) && e.args[1] === arg
	return nothing
	end
	end
	else
	# there might still be the following kind of pattern (see #45499):
	# %init = ...
	# [...]
	# SlotNumber(x) = %init
	# [...]
	# goto if not isa(%init, T)
	# let's check if there is a slot assigned to the def SSA value but also there isn't
	# any potentially conflicting assignment to the same slot
	arg = nothing
	def = SSAValue(init)
	for i = (init+1):(sv.currpc-1)
	e = code[i]
	if isexpr(e, :(=))
	lhs = e.args[1]
	if isa(lhs, SlotNumber)
	lhs === arg && return nothing
	rhs = e.args[2]
	if rhs === def
	arg = lhs
	end
	end
	end
	end
	end
	return arg
	end

Although ssa_def_slot might not be entirely sound either...
That being said, the correct way to replace Conditional would be to implement proper backward abstract interpretation, which would be quite a big work. It might be something we should do, but for now, I'll look for a short-term fix.