Integrating the Checker Framework in other static analysis tools?

[jyoo980]

I would like to ask whether it is feasible to use the functionality of the Checker Framework within another static analysis tool.

For example, suppose a static analysis tool performs a number of passes over a program, and a pass may produce some artifacts that might be consumed by future passes/analyses (much like a compiler).

I would like to develop a checker that can execute over the program, just like another analysis/compiler pass, which also has access to the system's own data structures (not just that of the Checker Framework).

I am aware of prior work that does similar things (or perhaps exactly demonstrates what I am asking for), such as NullAway or Error Prone. However, I don't think the process by which tool developers might integrate the Checker Framework with their own tools is documented in the manual – I am happy to update the manual if such a process can be described/standardized!

[mernst]

When the Java compiler runs, an annotation processor may create new source files, which are then processed by the compiler, and so forth until no new source files are created by an annotation processor. (This is probably what you were referring to in your second paragraph.) As far as I know, if both the Checker Framework and another annotation processor (that creates source files) are run, then the Checker Framework will run on the new files. However, I don't know that we have a test case for that in our test suite.

You require access to the other program's data structures. Is that read-only access, or also write access? Will the Checker Framework be invoked many times, or just once? I ask because the Checker Framework is currently tied into javac, which is the main program that makes calls into the Checker Framework as needed. Here is a slightly hacky way to integrate with the Checker Framework, depending on your use case: Your program runs for a while, then serializes its data structures to a file, then runs a javac process with your checker (which reads the serialized data structures and write serialized data for your program to run), then your program reads the checker's output.

Does your program have to be the main program? That is, could the Checker Framework call out to your program? (This might not be possible; it is often difficult to integrate two different programs that both assume they are the main program.)

There might also be some way to start javac, serialize its data structures, and make them available to a version of the Checker Framework that is invoked from your program.

How do NullAway and Error Prone achieve this?

Maybe @smillst has other ideas.

[msridhar]

I would like to develop a checker that can execute over the program, just like another analysis/compiler pass, which also has access to the system's own data structures (not just that of the Checker Framework).

Here what do you mean by "the system"?

I am aware of prior work that does similar things (or perhaps exactly demonstrates what I am asking for), such as NullAway or Error Prone.

Re: NullAway, I'm not exactly sure what you are referring to. I can think of a couple of things related to the NullAway Annotator that might be relevant. The NullAway Annotator is a separate Java program that invokes NullAway repeatedly by just running the build (which has already integrated NullAway). NullAway can serialize its warnings / errors to XML files, which simplifies things for the Annotator (as it doesn't need to parse the javac output). Also, the annotator runs a separate scanner Error Prone check to index various aspects of the program. This scanner does not emit any warnings / errors but instead serializes its output to files.

One thing to check with the serialization approach is to make sure all checkers are reporting their issues at the warning level. We've found that if a compile error gets reported, sometimes javac does not process all the remaining source files.