API to obtain the "then" store for boolean function call arguments

[msridhar]

In NullAway, we'd like to add reasoning about methods like Guava's Precondition.checkArgument, for cases like the following:

void foo(@Nullable Object o) {
  Preconditions.checkArgument(o != null, "contrived failure");
  o.toString(); // cannot throw NPE
}

We would like to be able to reason that the o.toString() call cannot throw an NPE. The behavior of checkArgument could be specified with something like a JetBrains @Contract annotation @Contract(false, _ -> fail). This annotation means that any dataflow facts that hold when the first argument evaluates to true can be propagated to the normal (non-exceptional) successor of a checkArgument call.

To implement this, we would need access to the "then" store at the program point after the first parameter to a checkArgument call is evaluated. Do you have a suggestion on the right approach to use to access this information? We're also willing to contribute a new API if needed. Thanks! /cc @lazaroclapp

[smillst]

So basically add a method annotation that makes dataflow treat Preconditions.checkArgument(o != null, "contrived failure") as an assertion?
I'm not familiar with the code that deals with assertions, but I would start looking at CFGTranslationPhaseOne#translateAssertWithAssertionsEnabled to implement this.

[msridhar]

Thanks, @smillst! By poking around that code, I found the CFCFGBuilder class, which shows how to customize CFG building. Probably we can do something similar for our purposes, with a custom build that translates relevant method invocations as if they assert their first argument. I will leave this issue open until we prototype this and see that it works.

[lazaroclapp]

After playing around with this a bit, it's easy enough for us to make our own CFGBuilder and CFGTranslationPhaseOne subclasses, even within NullAway's dataflow package, and then check for this case in a method overriding CFGTranslationPhaseOne.visitMethodInvocation(...).

However, one issue I am running into is that Label is not part of the public API, so I am not sure how to create the required control flow jumps to implement something similar to translateAssertWithAssertionsEnabled or visitIf for these cases.

Another option is to generate an artificial IfTree object, and pass it to CFGTranslationPhaseOne.visitIf, but the CFG builder in general seems to expect ASTs corresponding to actual Java source code (e.g. javacutil.TreeUtils.elementFromTree gets called at some point and that expects the new Error() portion of the artificial AST to be a proper JCTree.JCNewClass). In general, constructing artificial ASTs to feed to CFG seems fragile for many of the same reasons say Lombok mutated ASTs cause trouble for analysis tools. So, my preference right now would be to be able to create Label instances from outside CF.

Not sure what the implications are on the CF side of making Label a public class. But it doesn't seem to me that it would be any more of an exposed internal detail than CFGTranslationPhase[One|Two|Three] already are.

[msridhar]

Thanks for the investigation @lazaroclapp. I opened #5152 to make Label public (which I think is a reasonable change)

[msridhar]

@lazaroclapp Label is now public on the main branch. Are you able to further prototype your changes using a SNAPSHOT build of the Checker Framework?

[lazaroclapp]

Opening a new PR with a few more APIs that I needed to implement uber/NullAway#608.

p.s. @msridhar let me know if the general approach of the NullAway PR makes sense. No need for an in-depth review yet, but worth making sure we will not need other CF APIs for this :)

[msridhar]

#5156 and uber/NullAway#609 have landed so we are all set here. Thanks again for the help!