Skip to content

Add Null Support #143

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
rcosta358 wants to merge 13 commits into
base: main
Choose a base branch
from
Draft

Add Null Support #143

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
7a8de62
Add Null & Boxed Types Support
rcosta358 Feb 7, 2026
c2ae323
Add Tests
rcosta358 Feb 7, 2026
d73b81c
Minor Changes
rcosta358 Feb 7, 2026
f24dc28
Unused Imports
rcosta358 Feb 8, 2026
cb50d1e
Minor Improvements
rcosta358 Feb 10, 2026
65e938d
Merge branch 'main' into null-support
rcosta358 Feb 11, 2026
aef5189
Mark Uninitialized Fields as Null
rcosta358 Feb 12, 2026
e959ce6
Merge branch 'main' into null-support
rcosta358 Feb 12, 2026
4c4661c
Fix Merge
rcosta358 Feb 12, 2026
8998f23
Remove Boxed Types
rcosta358 Feb 13, 2026
d8e500d
Merge branch 'main' into null-support
rcosta358 Feb 13, 2026
31bd897
Change `CorrectNullChecks` Test
rcosta358 Feb 15, 2026
c739e5f
Remove Fields Implicit Null Refinement
rcosta358 Feb 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
137 changes: 137 additions & 0 deletions liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
package testSuite;

import java.util.ArrayList;
import java.util.Date;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class CorrectNullChecks {

Integer x; // implicit null

void test() {
mustBeNull(x);
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Feb 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

@rcosta358 rcosta358 Feb 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@rcosta358 rcosta358 Feb 15, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, I think that is a different problem, not actually related to nulls.
Consider this example, which fails the verification:

public class TestField {
    boolean x; // even if we initialize x with true the same error occurs btw

    @Refinement("_ == true")
    boolean test() {
        setValue();
        return x; // Refinement Error: #ret_0 == this#x is not a subtype of #ret_0 == true
    }

    void setValue() {
        x = true;
    }
}

However, in this case, the verification passes:

public class TestField {
    boolean x;

    @Refinement("_ == true")
    boolean test() {
        x = true;
        return x; // ok
    }
}

This means that the specific problem you mentioned is about how field updates across method calls are handled. The typechecker does not propagate the effect of setValue(), meaning field mutations are not reflected in the context after a method or constructor is called.

Therefore, I think that problem is unrelated to this PR and we should open its own issue.
What do you think @CatarinaGamboa?

Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Feb 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay several points:
1 - We cannot handle the field tracking atm, only with Latte - aliasing tracking extension, that we are working on in parallel. So you don't need to try and tackle this issue here, definitely, I agree.
2 - I think my main issue in the example was with mustBeNull, like we can't know for sure, we maybe should not track the nullness of them when entering methods, we would need an if to verify its value like

   void test() {
        if ( x == null){
             mustBeNull(x);
        } else {
             mustBeNotNull(x);
        }

This I think we should support, but we cannot be certain of the value at the start of the method.
Does this make sense?
We would have the code slilghtly polluted by ifs bit at least we check the values.

Copy link
Collaborator Author

@rcosta358 rcosta358 Feb 15, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

1 - Yeah you're right, I didn't even think of Latte.
2 - I agree. I'll change that test.

Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Feb 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for 2 - I think we should point out an issue with the call to mustBeNull(x) without the if

x = 1; // implicit non-null after assignment
mustBeNotNull(x);
}

void mustBeNull(@Refinement("_ == null") Integer i) {}
void mustBeNotNull(@Refinement("_ != null") Integer i) {}

void testNullInteger() {
Integer i = null;

@Refinement("_ == null")
Integer i1 = i;

i = 123;

@Refinement("_ != null")
Integer i2 = i;
}

void testNullString() {
String s = null;

@Refinement("_ == null")
String s1 = s;

s = "hello";

@Refinement("_ != null")
String s2 = s;
}

void testNulls() {
@Refinement("_ == null")
String s = null;

@Refinement("_ == null")
Integer i = null;

@Refinement("_ == null")
Boolean b = null;

@Refinement("_ == null")
Double d = null;

@Refinement("_ == null")
Long l = null;

@Refinement("_ == null")
Float f = null;

@Refinement("_ == null")
Date dt = null;

@Refinement("_ == null")
ArrayList<String> lst = null;
}

void testNonNulls() {
@Refinement("_ != null")
String s = "hello";

@Refinement("_ != null")
Integer i = 123;

@Refinement("_ != null")
Boolean b = true;

@Refinement("_ != null")
Double d = 1.0;

@Refinement("_ != null")
Long l = 2L;

@Refinement("_ != null")
Float f = 1.0f;

@Refinement("_ != null")
Date dt = new Date();

@Refinement("_ != null")
ArrayList<String> lst = new ArrayList<>();

@Refinement("_ != null")
CorrectNullChecks r = this;
}

void testNullChecksInMethods() {
@Refinement("_ != null")
String x = returnNotNullIf(null);

@Refinement("_ != null")
String y = returnNotNullTernary(null);

@Refinement("_ != null")
String z = returnNotNullParam("not null");

@Refinement("_ == null")
String w = returnNull();
}

@Refinement("_ != null")
String returnNotNullIf(String s) {
if (s == null)
s = "default";

return s;
}

@Refinement("_ != null")
String returnNotNullTernary(String s) {
return s != null ? s : "default";
}

@Refinement("_ != null")
String returnNotNullParam(@Refinement("_ != null") String s) {
return s;
}

@Refinement("_ == null")
String returnNull() {
return null;
}
}
1 change: 1 addition & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorAliasNotFound {

public static void main(String[] args) {
Expand Down
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorBoxedBoolean {
public static void main(String[] args) {
@Refinement("_ == true")
Boolean b = false;
}
}
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorBoxedDouble {
public static void main(String[] args) {
@Refinement("_ > 0")
Double d = -1.0;
}
}
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorBoxedInteger {
public static void main(String[] args) {
@Refinement("_ > 0")
Integer j = -1;
}
}
1 change: 1 addition & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorGhostNotFound {

public void test() {
Expand Down
1 change: 1 addition & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorLongUsagePredicates1 {
void testUUID(){
@Refinement("((v/4096) % 16) == 2")
Expand Down
1 change: 1 addition & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorLongUsagePredicates2 {
void testLargeSubtractionWrong() {
@Refinement("v - 9007199254740992 == 2")
Expand Down
1 change: 1 addition & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorLongUsagePredicates3 {
void testWrongSign() {
@Refinement("v < 0")
Expand Down
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorNullCheckAssignNonNull {
public static void main(String[] args) {
@Refinement("_ == null")
String s = "not null";
}
}
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorNullCheckAssignNull {
public static void main(String[] args) {
@Refinement("_ != null")
String s = null;
}
}
13 changes: 13 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorNullCheckAssignNullAfter {
public static void main(String[] args) {
@Refinement("_ != null")
String s = "not null";
s = null; // error
}
}
14 changes: 14 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// Refinement Error
package testSuite;

import java.util.Date;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorNullCheckAssignNullObject {
public static void main(String[] args) {
@Refinement("_ != null")
Date date = null;
}
}
17 changes: 17 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckFieldAssignment.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

public class ErrorNullCheckFieldAssignment {

String s; // implicit null

void test() {
mustBeNull(s);
s = "hello"; // implicit non-null after assignment
mustBeNull(s); // error
}

void mustBeNull(@Refinement("_ == null") String s) {}
}
15 changes: 15 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckFieldNonInitialized.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
public class ErrorNullCheckFieldNonInitialized {

Double d; // implicit null

void test() {
@Refinement("_ != null")
Double d2 = d; // should be error
}
}
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

public class ErrorNullCheckMethod {

@Refinement("_ != null")
String returnNotNull(String s) {
return s; // error: s can be null
}
}
19 changes: 19 additions & 0 deletions .../src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
package testSuite.classes.atomic_reference_correct;

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"empty", "holding"})
@ExternalRefinementsFor("java.util.concurrent.atomic.AtomicReference")
public interface AtomicReferenceRefinements<V> {

@StateRefinement(to="initialValue == null ? empty(this) : holding(this)")
public void AtomicReference(V initialValue);

@StateRefinement(from="holding(this)")
public V get();

@StateRefinement(to="newValue == null ? empty(this) : holding(this)")
public void set(V newValue);
}
15 changes: 15 additions & 0 deletions ...example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package testSuite.classes.atomic_reference_correct;

import java.util.concurrent.atomic.AtomicReference;

@SuppressWarnings("unused")
public class AtomicReferenceTest {

public void testOk() {
AtomicReference<String> ref = new AtomicReference<>("hello");
String s = ref.get();

ref.set("world");
String s2 = ref.get();
}
}
1 change: 1 addition & 0 deletions liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
State Refinement Error
19 changes: 19 additions & 0 deletions ...le/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
package testSuite.classes.atomic_reference_error;

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"empty", "holding"})
@ExternalRefinementsFor("java.util.concurrent.atomic.AtomicReference")
public interface AtomicReferenceRefinements<V> {

@StateRefinement(to="initialValue == null ? empty(this) : holding(this)")
public void AtomicReference(V initialValue);

@StateRefinement(from="holding(this)")
public V get();

@StateRefinement(to="newValue == null ? empty(this) : holding(this)")
public void set(V newValue);
}
13 changes: 13 additions & 0 deletions ...a-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
package testSuite.classes.atomic_reference_error;

import java.util.concurrent.atomic.AtomicReference;

@SuppressWarnings("unused")
public class AtomicReferenceTest {

public void testError() {
AtomicReference<String> ref = new AtomicReference<>(null);
String s = ref.get(); // error
}
}

Loading