JuliaLang / julia

The Julia Programming Language
https://julialang.org/
MIT License
45.07k stars 5.43k forks source link

Track Integer bounds in AbstractInterpretation #46146

Open oscardssmith opened 2 years ago

oscardssmith commented 2 years ago

Right now, Julia is in an awkward place with @inbounds. Effect analysis really doesn't like @inbounds because indexing OOB is inconsistent, but AbstractInterpretation doesn't propagate Integer bounds at all.

I think the best solution to this would be to add an IntegerRange{T<:BitInteger} type to Core.Compiler that tracks ranges of integers through abstract interpretation. Specifically, it would need to support:

All other operations would just widen to T

With these rules, we would be able to remove most un-necessary boundchecks in code that doesn't have loops. Getting this analysis to work well in the presence of loops is harder, and I'm not sure what would need to be done to prove convergence of bounds. Anyone have ideas?

vchuravy commented 1 year ago

LLVM uses a technique called scalar evolution (SCEV) based on the algebra of chaines of recurrences. Some references here https://github.com/JuliaLang/llvm-project/blob/046f90173567535397c97b2d00406c93ee4bc890/llvm/lib/Analysis/ScalarEvolution.cpp#L39-L56

There is a lot of previous work on using abstract interpretation for array bounds as an example see https://hal.univ-reunion.fr/hal-01921666/document.