Mark Uninitialized Fields as Null

Author: rcosta358

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

@@ -8,6 +8,17 @@
 @SuppressWarnings("unused")
 public class CorrectNullChecks {
 
+    Integer x; // implicit null
+
+    void test() {
+        mustBeNull(x);
+        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;
 
@@ -82,6 +93,9 @@ void testNonNulls() {
 
         @Refinement("_ != null")
         ArrayList<String> lst = new ArrayList<>();
+
+        @Refinement("_ != null")
+        CorrectNullChecks r = this;
     }
 
     void testNullChecksInMethods() {

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

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

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

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

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -127,7 +127,8 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
         if (localVariable.getAssignment() == null) {
             // declaration with no assignment
             Optional<Predicate> pred = getRefinementFromAnnotation(localVariable);
-            RefinedVariable v = context.addVarToContext(varName, localVariable.getType(), pred.orElse(new Predicate()), localVariable);
+            RefinedVariable v = context.addVarToContext(varName, localVariable.getType(), pred.orElse(new Predicate()),
+                    localVariable);
             getMessageFromAnnotation(localVariable).ifPresent(v::setMessage);
         } else {
             // declaration with assignment
@@ -136,7 +137,7 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
             if (refinementFound == null) {
                 refinementFound = new Predicate();
             }
-            if (!Utils.isPrimitiveType(localVariable.getType().getQualifiedName()) && !Utils.isNullLiteral(e)) {
+            if (!Utils.isPrimitiveType(localVariable.getType().getQualifiedName()) && isNonNullExpr(e)) {
                 refinementFound = Predicate.createConjunction(refinementFound, Predicate.createNonNullEq());
             }
             context.addVarToContext(varName, localVariable.getType(), new Predicate(), e);
@@ -245,6 +246,14 @@ public <T> void visitCtField(CtField<T> f) {
         if (v instanceof Variable) {
             ((Variable) v).setLocation("this");
         }
+        // if the field is not initialized and can be null, add instance to context with null equality refinement
+        if (f.getAssignment() == null && !Utils.isPrimitiveType(f.getType().getQualifiedName())) {
+            String instanceName = String.format(Formats.INSTANCE, name, context.getCounter());
+            Predicate initialRefinement = Predicate.createConjunction(ret.substituteVariable(name, instanceName),
+                    Predicate.createNullEq().substituteVariable(Keys.WILDCARD, instanceName));
+            context.addInstanceToContext(instanceName, f.getType(), initialRefinement, f);
+            context.addRefinementInstanceToVariable(name, instanceName);
+        }
     }
 
     @Override
@@ -261,9 +270,12 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
             }
 
         } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
+            // resolve to latest instance of this field for flow-sensitive refinement
             String thisName = String.format(Formats.THIS, fieldName);
+            Optional<VariableInstance> ovi = context.getLastVariableInstance(thisName);
+            String var = ovi.isPresent() ? ovi.get().getName() : thisName;
             fieldRead.putMetadata(Keys.REFINEMENT,
-                    Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
+                    Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(var)));
 
         } else if (fieldRead.getVariable().getSimpleName().equals("length")) {
             String targetName = fieldRead.getTarget().toString();
@@ -402,7 +414,7 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
                 refinementFound = new Predicate();
             }
         }
-        if (!Utils.isPrimitiveType(type.getQualifiedName()) && !Utils.isNullLiteral(assignment)) {
+        if (!Utils.isPrimitiveType(type.getQualifiedName()) && isNonNullExpr(assignment)) {
             refinementFound = Predicate.createConjunction(refinementFound, Predicate.createNonNullEq());
         }
         Optional<VariableInstance> r = context.getLastVariableInstance(name);
@@ -436,6 +448,13 @@ private Predicate getExpressionRefinements(CtExpression<?> element) throws LJErr
         return getRefinement(element);
     }
 
+    private boolean isNonNullExpr(CtExpression<?> exp) {
+        if (exp == null || Utils.isNullLiteral(exp))
+            return false;
+        return exp instanceof CtLiteral<?> || exp instanceof CtConstructorCall<?> || exp instanceof CtNewArray<?>
+                || exp instanceof CtNewClass<?> || exp instanceof CtThisAccess<?>;
+    }
+
     private Predicate substituteAllVariablesForLastInstance(Predicate c) {
         Predicate ret = c;
         List<String> ls = c.getVariableNames();