inference: track reaching defs for slots

[topolarity]

This PR implements the "Path-Convergence Criterion" for SSA / ϕ-nodes as part of type-inference.

The VarState.ssadef field corresponds to the "reaching definition" of the slot in SSA form, which allows us to conveniently reason about the identity of a slot across multiple program points. If the reaching def is equal at two program points, then the slot contents are guaranteed to be egal (i.e. x₀ === x₁)

Tasks:

• Split StateRefinement change to separate PR
• Split VarTable plumbing to separate PR
• Remove old Conditional invalidation logic
• Add tests

Fixes #55548 (alternative to #55551), by having Conditional remember the reaching definition that it narrows.

[topolarity]

This is the core of the reaching def computation

It might be surprising that this doesn't use dominance, etc. but that's because dominance-based algorithms are optimized versions of the "path-convergence criterion" we solve here (both algorithms compute the same thing). Since we're solving the dataflow equations in this way for inference already, the SSA information comes mostly for free

[aviatesk]

Thanks, this looks much better than my PR in general.
Still I would like to add the test case from it, i.e.

# JuliaLang/julia#55548: invalidate stale slot wrapper types in `ssavaluetypes`
_issue55548_proj1(a, b) = a
function issue55548(a)
    a = Base.inferencebarrier(a)::Union{Int64,Float64}
    if _issue55548_proj1(isa(a, Int64), (a = Base.inferencebarrier(1.0)::Union{Int64,Float64}; true))
        return a
    end
    return 2
end
@test Float64 <: Base.infer_return_type(issue55548, (Int,))

[aviatesk]

Suggested change

	function abstract_call(interp::AbstractInterpreter, arginfo::ArgInfo, vtypes::Union{VarTable,Nothing}, irsv::IRInterpretationState)
	function abstract_call(interp::AbstractInterpreter, arginfo::ArgInfo, ::Nothing, irsv::IRInterpretationState)

vtypes is never available for irinterp, so it's better to restrict this signature?

[aviatesk]

Better to check this at the topmost if condition?

[aviatesk]

We require vtypes !== nothing for this path.

[aviatesk]

Suggested change

	(thentype, elsetype) = if then_or_else === :then
	(condt.thentype, Union{})
	elseif then_or_else === :else
	(Union{}, condt.elsetype)
	else @assert false end
	if then_or_else === :then
	thentype = condt.thentype
	elsetype = Union{}
	elseif then_or_else === :else
	thentype = Union{}
	elsetype = condt.elsetype
	else @assert false end

the previous version creates Tuple objects whose types aren't known.

[aviatesk]

What does "virtual φ-block" mean? I still don't quite grasp its meaning.
Also, it might be good to mention the case when ssadef == 0, meaning it was passed as an argument IIUC.

[topolarity]

The "virtual ϕ-block" is just the usual block of ϕ-nodes that in proper SSA form would appear at the beginning of the BasicBlock. We're not actually inserting / re-indexing instructions though, so instead you get a negative index at the insertion point where the ϕ "would" go.

Also, it might be good to mention the case when ssadef == 0, meaning it was passed as an argument IIUC.

Yeah, great point - will do

[aviatesk]

Okay, well, is the use of the "virtual φ block" the same as the meaning of -pc passed to stupdate! in abstractinterpretation.jl? I might be misunderstanding, but my intuition is that negative ssadef means something like "we can't track the def of this slot." If that interpretation feels more natural, then maybe it would be better to represent it as ssadef::Union{Nothing,UInt}.

[topolarity]

This is the same meaning as in stupdate!, but it doesn't mean "we can't track the def"

An ssadef of -pc means "If this code were in SSA form, a use of this slot would be replaced with a use of a ϕ-node." Which ϕ-node? The one that would have been inserted at pc

That's important because the rule given above:

If the reaching def is equal at two program points, then the slot contents are guaranteed to be egal (i.e. x₀ === x₁)

Also works for -pc ssadefs

[aviatesk]

@nanosoldier runbenchmarks("inference", vs=":master")

[topolarity]

Thanks for the test case and review @aviatesk

fwiw, there's also a precision regression that I encountered w/ this PR:

function foo()
    value = @noinline rand((true, false, 1))
    is_bool = value isa Bool
    if inferencebarrier(@noinline rand(Bool))
        value = 1.0
        is_bool = false
    end
    # at this merge point, only the "false half" of the Conditional should be invalidated
    return is_bool ? value : false
end
@assert only(Base.return_types(foo, ())) === Bool # fails w/ PR

but I think this can be mostly fixed by widening the Conditional at the merge point and giving it a new .ssadef to match

[nanosoldier]

Your benchmark job has completed - possible performance regressions were detected. A full report can be found here.

[vtjnash]

bump? are we able to land this and backport to v1.11/v1.10?