Framework for pluggable analysis?

[jtrakk]

I wonder if it's possible to provide type checking as just one of many analyses that could be used with the JET framework. For example, performance analysis, numerical stability, taint analysis. It could be a pluggable framework.

[aviatesk]

Hi, sorry for my late response.

Could you provide a concrete example of what kind of reports you'd like to have (or even ignore) by implementing a plugin ?

It would be easy to make it possible for users to inject their own analysis code into JET's abstract interpretation routine (just like JET itself does for Julia's abstract interpretation routine) by subtyping JETInterpreter (probably better to be renamed to JETAbstractInterpreter then).
But what I'm wondering is that JET relies on Julia's abstract interpretation, which in turn is based on its own lattice implementation, and so some analysis which can't be expressed by the lattice (e.g. shape analysis) can't be easily implemented by the framework; we would need implement the new lattice implementation and to re-implement most abstract interpretation routines according on the new lattice, because Julia's abstract interpretation routine is tightly bound to its lattice implementation.
Back to the pluggable framework, some analysis that doesn't require another (extended) lattice implementation like performance analysis (I assume you meant by "performance analysis" a report on "too many matching methods" or something like that) still can be implemented as a pluggin, yes, but I'm not sure why it can't just implemented within JET. I guess maybe implementing more report passes and setting up some interface to configure which kind of reports we want to get would be enough for such a case.

[samarthkishor]

I think the idea is that other libraries can use JET as a framework to provide their own static analyses without having to write the abstract interpretation and error reporting logic themselves. For example, MLStyle.jl could extend JET to statically detect type errors in pattern matching just like an ML language. It's kind of like using JET to write a domain-specific linter.

[aviatesk]

yeah, I've actually implemented something locally that makes JET pluggable. Let's see how it fits. Let me ping you once I've pushed changes.

[AriMKatz]

Related: JuliaLang/julia#40992

[jtrakk]

I meant checks like https://fbinfer.com/docs/next/checker-cost/ and https://fbinfer.com/docs/next/checker-liveness/

[aviatesk]

Implemented by #208.

You can take a look at an example plug-in analyzer and the API documentation.

The framework API is very experimental, and its documentation is very WIP,
and so I've not tagged a new version with that included, but you can try it out by checking out to master.
Any kind of feedback is very welcomed !

[jtrakk]

Very cool, @aviatesk.

In the part

For that purpose, it's suffice to overload Core.Compiler.abstract_eval_special_value and Core.Compiler.builtin_tfunction.

that section might benefit from some higher-level APIs. I don't know too much about the Core.Compiler interface. Maybe there are some common cases that JET could wrap so I don't have to touch CC?