Fix crashes on unresolved types and on empty for bodies

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

@@ -0,0 +1,33 @@
+package testSuite;
+
+import java.util.Iterator;
+
+import liquidjava.specification.Refinement;
+
+// Loops whose body is an empty statement (#395)
+@SuppressWarnings("unused")
+public class CorrectEmptyLoopBody {
+    static int total(int[] counts) {
+        int total = 0;
+        for (int i = 0; i < counts.length; total += counts[i], i++)
+            ;
+        return total;
+    }
+
+    static void countDown() {
+        @Refinement("_ >= 0")
+        int n = 10;
+        for (; n > 0; n--)
+            ;
+    }
+
+    static void skip(Iterator<String> it, int[] xs) {
+        while (it.hasNext() && it.next() != null)
+            ;
+        do
+            ;
+        while (it.hasNext() && it.next() != null);
+        for (int x : xs)
+            ;
+    }
+}

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

@@ -0,0 +1,26 @@
+package testSuite;
+
+import org.example.missing.Cookie;
+
+import liquidjava.specification.Refinement;
+
+// Array elements whose type cannot be resolved (#425)
+@SuppressWarnings("unused")
+public class CorrectUnresolvedArrayElement {
+    static void any(@Refinement("_ == _") Object o) {
+    }
+
+    void createAll(Cookie[] cookies) {
+        for (int i = 0; i < cookies.length; i++) {
+            cookies[i].create();
+        }
+    }
+
+    Cookie first(Cookie[] cookies) {
+        return cookies[0];
+    }
+
+    void passed(Cookie[] cookies) {
+        any(cookies[0]); // the element is part of the SMT query
+    }
+}

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import java.awt.Point;
+
+import org.example.missing.Options;
+
+// Writes to fields whose declaration is not in the analyzed sources (#426)
+@SuppressWarnings("unused")
+public class CorrectUnresolvedFieldWrite {
+    void configure() {
+        Options opts = new Options();
+        opts.sampleSize = 1;
+    }
+
+    void update(Options opts) {
+        opts.sampleSize += 1;
+        opts.error = true;
+    }
+
+    void move(Point p) {
+        p.x = 3;
+    }
+}

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

@@ -0,0 +1,15 @@
+package testSuite;
+
+import org.example.missing.Request;
+
+// Lambda parameters whose type cannot be resolved (#396)
+@SuppressWarnings("unused")
+public class CorrectUnresolvedLambdaParameter {
+    static void print(Request request) {
+        request.names().forEach(name -> System.out.println(name));
+    }
+
+    static void headers(Request request) {
+        request.headerNames().forEach(header -> request.copy(header, request.header(header)));
+    }
+}

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

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// The update of a for loop whose body is an empty statement is still checked (#395)
+@SuppressWarnings("unused")
+public class ErrorEmptyLoopBody {
+    static void countDown() {
+        @Refinement("_ >= 0")
+        int n = 10;
+        for (; n > 0; n -= 2) // Expect: Refinement Error
+            ;
+    }
+}

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

@@ -0,0 +1,18 @@
+package testSuite;
+
+import org.example.missing.Cookie;
+
+import liquidjava.specification.Refinement;
+
+// A violation after reading an array element whose type cannot be resolved is still reported (#425)
+@SuppressWarnings("unused")
+public class ErrorUnresolvedArrayElement {
+    static void positive(@Refinement("_ > 0") int x) {
+    }
+
+    static void first(Cookie[] cookies) {
+        Cookie cookie = cookies[0];
+        cookie.create();
+        positive(-1); // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,17 @@
+package testSuite;
+
+import org.example.missing.Options;
+
+import liquidjava.specification.Refinement;
+
+// A violation after a write to a field of a class that cannot be resolved is still reported (#426)
+@SuppressWarnings("unused")
+public class ErrorUnresolvedFieldWrite {
+    static void positive(@Refinement("_ > 0") int x) {
+    }
+
+    static void configure(Options opts) {
+        opts.sampleSize = 1;
+        positive(-1); // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,17 @@
+package testSuite;
+
+import org.example.missing.Request;
+
+import liquidjava.specification.Refinement;
+
+// A violation after a lambda whose parameter type cannot be resolved is still reported (#396)
+@SuppressWarnings("unused")
+public class ErrorUnresolvedLambdaParameter {
+    static void positive(@Refinement("_ > 0") int x) {
+    }
+
+    static void print(Request request) {
+        request.names().forEach(name -> System.out.println(name));
+        positive(-1); // Expect: Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -188,21 +188,28 @@ public void addVarToContext(RefinedVariable var) {
     }
 
     public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c, CtElement element) {
-        RefinedVariable vi = new Variable(simpleName, type, c);
+        RefinedVariable vi = new Variable(simpleName, typeOrObject(type, element), c);
         vi.setPlacementInCode(element);
-        vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
         addVarToContext(vi);
         return vi;
     }
 
+    /**
+     * Spoon leaves the type unset when it cannot be resolved (e.g. its class is not on the classpath). A variable of
+     * such a type is typed as Object, as every variable needs a type for its supertypes and its SMT sort.
+     */
+    private static CtTypeReference<?> typeOrObject(CtTypeReference<?> type, CtElement element) {
+        return type != null ? type : element.getFactory().Type().objectType();
+    }
+
     public void removeVarFromContext(String name) {
         for (List<RefinedVariable> l : ctxVars)
             l.removeIf(var -> var.getName().equals(name));
     }
 
     public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?> type, Predicate c,
             CtElement element) {
-        RefinedVariable vi = new VariableInstance(simpleName, type, c);
+        RefinedVariable vi = new VariableInstance(simpleName, typeOrObject(type, element), c);
         vi.setPlacementInCode(element);
         if (!ctxInstanceVars.contains(vi))
             addInstanceVariable(vi);

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

@@ -256,10 +256,13 @@ private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) thr
             CtFieldReference<?> cr = fw.getVariable();
             CtField<?> f = fw.getVariable().getDeclaration();
             String updatedVarName = Utils.qualifyFieldName(cr);
-            checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f);
+            // a field declared outside the analyzed sources (e.g. a library field) has no declared refinement: the
+            // write stands in for its declaration
+            checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment,
+                    f != null ? f : assignment);
 
-            // corresponding ghost function update
-            if (fw.getVariable().getType().toString().equals("int")) {
+            // corresponding ghost function update, for fields declared in the analyzed sources
+            if (f != null && fw.getVariable().getType().toString().equals("int")) {
                 AuxStateHandler.updateGhostField(fw, this);
             }
         }
@@ -675,8 +678,9 @@ public void visitCtFor(CtFor forLoop) {
             scan(forLoop.getExpression());
             assumeLoopCondition(forLoop.getExpression());
             List<RefinedVariable> pathVariables = vcChecker.getPathVariables();
-            scan(forLoop.getBody());
-            if (!forLoop.getBody().getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) {
+            CtStatement body = forLoop.getBody(); // null for an empty statement body, as in for (...);
+            scan(body);
+            if (body != null && !body.getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) {
                 // a continue reaches the update from any point of the body, skipping its facts and assignments
                 vcChecker.restorePathVariables(pathVariables);
                 havocChangedIn(forLoop);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -849,10 +849,8 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Must come
             // before the TARGET case: a constructor with refined parameters puts its (void) return value in TARGET
             String name = String.format(Formats.FRESH, tc.getContext().getCounter());
-            CtTypeReference<?> type = newCall.getType();
-            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type,
+            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, newCall.getType(),
                     state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall);
-            receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
             newCall.putMetadata(Keys.TARGET, receiver);
             newCall.putMetadata(Keys.RECEIVER, receiver);
             invocation.putMetadata(Keys.TARGET, receiver);
@@ -866,9 +864,8 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             // `a.get().method()` where get() has no return refinement: the call's TARGET is its own receiver (a), not
             // the value it returns, so the receiver is a fresh value of the call's type, in a state not known here
             String name = String.format(Formats.FRESH, tc.getContext().getCounter());
-            CtTypeReference<?> type = call.getType();
-            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type, new Predicate(), call);
-            receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
+            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, call.getType(), new Predicate(),
+                    call);
             call.putMetadata(Keys.RECEIVER, receiver);
             invocation.putMetadata(Keys.TARGET, receiver);
             return name;