Add Null & Boxed Types Support

[rcosta358]

This PR adds support for null checking in LiquidJava.
It also allows us to refine boxed types which previously were also not supported (Integer, Boolean, Short, Long, Float and Double).

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

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
• Boxed types are now mapped to the same Z3 sorts as their primitive types (e.g., java.lang.Integer => Int) to avoid errors like “Sorts java.lang.Integer and Int are incompatible"

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]

why is this necessary? and why wouldnt we put a createNullEq in the "only declaration, no assignment"?

[rcosta358]

• That's the case where we declare a variable of boxed type (e.g. Integer) and it is not null, so it carries the refinement "_ != null"
• I didn't consider uninitialized variables, should we handle that case?

[rcosta358]

• In Java if a variable is declared without a value it is not null, right? It's just not initialized. In those cases if one tried to use it it would be a Java error. Do we need to worry about that?
• Fair point, but I needed the boxed types working to test the nulls properly. I'll try to make more atomic PRs in the future!