aviatesk / JET.jl

An experimental code analyzer for Julia. No need for additional type annotations.
https://aviatesk.github.io/JET.jl/dev/
MIT License
742 stars 30 forks source link

[inference] relational anaysis #153

Open aviatesk opened 3 years ago

aviatesk commented 3 years ago

something like described in this paper: https://www-apr.lip6.fr/~mine/publi/article-monat-al-ecoop20.pdf

I found there're certainly cases where a relational analysis can improve the analysis accuracy:

adapted from https://github.com/JuliaLang/julia/blob/90bea0319ec29e09123ab4c678fa6a30753c8849/base/multidimensional.jl#L126-L133

# comparison
@inline isless(I1::CartesianIndex{N}, I2::CartesianIndex{N}) where {N} = _isless(0, I1.I, I2.I)
@inline function _isless(ret, I1::NTuple{N,Int}, I2::NTuple{N,Int}) where N
newret = ifelse(ret==0, icmp(I1[N], I2[N]), ret)
# NOTE relational analysis can exclude a false positive no method error for 
# `isless(ret, ::Tuple{}, ::NTuple{N,Int})` and `_isless(ret, ::NTuple{N,Int}, ::Tuple{})`
_isless(newret, 
Base.front(I1)#=::Union{Tuple{},Tuple{Int,Vararg{Int}}=#,
Base.front(I2)#=::Union{Tuple{},Tuple{Int,Vararg{Int}}=#)
end
_isless(ret, ::Tuple{}, ::Tuple{}) = ifelse(ret==1, true, false)
icmp(a, b) = ifelse(isless(a,b), 1, ifelse(a==b, 0, -1))
aviatesk commented 3 years ago

Another target example would be:

https://github.com/JuliaLang/julia/blob/ac7974acef22b357e790be418b750987e86cb386/base/tuple.jl#L360-L371

isequal(t1::Tuple, t2::Tuple) = (length(t1) == length(t2)) && _isequal(t1, t2)
_isequal(t1::Tuple{}, t2::Tuple{}) = true
_isequal(t1::Tuple{Any}, t2::Tuple{Any}) = isequal(t1[1], t2[1])
_isequal(t1::Tuple, t2::Tuple) = isequal(t1[1], t2[1]) && _isequal(tail(t1), tail(t2))
function _isequal(t1::Any32, t2::Any32)
for i = 1:length(t1)
if !isequal(t1[i], t2[i])
return false
end
end
return true
end

isequal(::Any, ::Tuple{Any}) is always valid given the definition above, but JET reports false positive on this:

julia> report_call((Any, Tuple{Any}); annotate_types=true) do t1, t2
           isequal(t1, t2)
       end
═════ 1 possible error found ═════
┌ @ none:2 Main.isequal(t1::Any, t2::Tuple{Any})
│┌ @ /Users/aviatesk/julia/julia/base/tuple.jl:360 Base._isequal(t1::Tuple, t2::Tuple{Any})
││┌ @ /Users/aviatesk/julia/julia/base/tuple.jl:363 Base._isequal(Base.tail(t1::Tuple)::Tuple, Base.tail(t2::Tuple{Any})::Tuple{})
│││┌ @ /Users/aviatesk/julia/julia/base/tuple.jl:363 Base.getindex(t2::Tuple{}, 1)
││││┌ @ tuple.jl:29 Base.getfield(t::Tuple{}, i::Int64, $(Expr(:boundscheck)))
│││││ invalid builtin function call: Base.getfield(t::Tuple{}, i::Int64, $(Expr(:boundscheck)))
││││└───────────────
Any
aviatesk commented 3 years ago

https://github.com/JuliaLang/julia/pull/40594 is a band-aid for the time being.