Add Null Support

liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java

@@ -0,0 +1,139 @@
+package testSuite;
+
+import java.util.ArrayList;
+import java.util.Date;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectNullChecks {
+
+    Integer x;
+
+    void test() {
+        if (x == null) {
+            mustBeNull(x);
+        } else {
+            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;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java

@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorAliasNotFound {
 
     public static void main(String[] args) {

liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java

@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorGhostNotFound {
 
     public void test() {

liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java

@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorLongUsagePredicates1 {
     void testUUID(){
         @Refinement("((v/4096) % 16) == 2")

liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java

@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorLongUsagePredicates2 {
       void testLargeSubtractionWrong() {                                                                                                                    
       @Refinement("v - 9007199254740992 == 2")                                                                                                          

liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java

@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorLongUsagePredicates3 {
     void testWrongSign() {                                                                                                                                
       @Refinement("v < 0")                                                                                                                              

liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java

@@ -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";
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java

@@ -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;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java

@@ -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
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java

@@ -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;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java

@@ -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
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorNullableFieldNonNullAssumption.java

@@ -0,0 +1,14 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorNullableFieldNonNullAssumption {
+    Integer x;
+
+    void test() {
+        mustBeNonNull(x); // we dont know if x is null or not
+    }
+
+    void mustBeNonNull(@Refinement("_ != null") Integer i) {}
+}

liquidjava-example/src/main/java/testSuite/ErrorNullableFieldNullAssumption.java

@@ -0,0 +1,14 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorNullableFieldNullAssumption {
+    Integer x;
+
+    void test() {
+        mustBeNull(x); // we dont know if x is null or not
+    }
+
+    void mustBeNull(@Refinement("_ == null") Integer i) {}
+}

liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java

@@ -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);
+}

liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java

@@ -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();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java

@@ -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);
+}

liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java

@@ -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
+    }
+}
+

liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4

@@ -62,7 +62,8 @@ literal:
 		BOOL
 	|	STRING
 	|	INT
-	|	REAL;
+	|	REAL
+	|	NULL;
 
 //----------------------- Declarations -----------------------
 
@@ -93,6 +94,7 @@ BOOLOP	 : '=='|'!='|'>='|'>'|'<='|'<';
 ARITHOP : '+'|'*'|'/'|'%';//|'-';
 
 BOOL    : 'true' | 'false';
+NULL    : 'null';
 ID_UPPER: ([A-Z][a-zA-Z0-9]*);
 OBJECT_TYPE:
 		  (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);