Add Null Support

[rcosta358]

This PR adds support for null checking in LiquidJava.

Changes

Refinements Language

• Added the null literal to the grammar
• Added the LiteralNull AST node

Typing

• The literal null can be assigned to any non-primitive type
• String literals, literals of boxed types and new object instances implicitly carry the refinement _ != null, while the literal null carries the refinement _ == null
• When a class field is declared without a value, it is implicitly refined with _ == null

Z3 Translation

• Nulls are converted to uninterpreted constants of the uninterpreted sort java.lang.Object
• In equality comparisons, null literals are converted to the sort of the other operand to match both sorts

Simplification

• The simplifier removes redundant null checks when an equality to a non-null literal already implies a non-null value. This way, s == -1 && s != null simplifies to s == -1 instead of -1 != null

Testing

• Added various tests to ensure the correctness of these changes

[CatarinaGamboa]

For the nullness check, I think we need more cases, like what if we declare the var and it doesn't have a value?
There are full tools just for the nullness checking (e.g., NullAway https://github.com/uber/NullAway)

PS: this would be so much easier if it were 2 prs, one for null and one for boxed types -- the boxed types would be an easy squash and merge

[CatarinaGamboa]

This is nice to have, but I have some questions (we already discussed some offline):

• obj != null and state. It would be great if we didnt have to pollute the refinements with always having to write this != null. Maybe we can assume that all object states imply != null?
• null of fields are trickier, check the comment below

[CatarinaGamboa]

this comment

[CatarinaGamboa]

But we don't know if this is null right? how do we know? what if there was a constructor, what if another method is called first and sets this fiels? what are the assumptions here?

[rcosta358]

Yeah you're right. I'll try to handle those cases.