From 3be1b60dc515b4d1ad2bfe9b708da62121166f23 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 17:39:12 +0000 Subject: [PATCH 1/3] Type variables of unresolved types as Object When a class is not on the classpath, Spoon leaves the type of an array element of that class, and of a lambda parameter whose target type is that class, unset. Adding such a variable to the context crashed with a null dereference when looking up its supertypes, and would otherwise crash the SMT translation, which needs a sort for every variable. Such a variable is now typed as Object: it has no supertypes and carries no information. Violations around it are still reported. Fixes #425, fixes #396. Co-Authored-By: Claude Opus 5.5 --- .../CorrectUnresolvedArrayElement.java | 26 +++++++++++++++++++ .../CorrectUnresolvedLambdaParameter.java | 15 +++++++++++ .../ErrorUnresolvedArrayElement.java | 18 +++++++++++++ .../ErrorUnresolvedLambdaParameter.java | 17 ++++++++++++ .../liquidjava/processor/context/Context.java | 11 ++++++-- 5 files changed, 85 insertions(+), 2 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnresolvedArrayElement.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnresolvedLambdaParameter.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedArrayElement.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedLambdaParameter.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedArrayElement.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedArrayElement.java new file mode 100644 index 00000000..8b98e45d --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedLambdaParameter.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedLambdaParameter.java new file mode 100644 index 00000000..5a3b3cd6 --- /dev/null +++ b/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))); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedArrayElement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedArrayElement.java new file mode 100644 index 00000000..cbeec418 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedLambdaParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedLambdaParameter.java new file mode 100644 index 00000000..a33b9636 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index b5d53196..26e3df72 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -188,13 +188,20 @@ 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 l : ctxVars) l.removeIf(var -> var.getName().equals(name)); From dd7ca3d96c85a964cee3bb6f82543490c4819833 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 17:45:00 +0000 Subject: [PATCH 2/3] Check writes to fields declared outside the analyzed sources Writing a field whose declaration is not available, such as a field of a class that is not on the classpath (`opts.sampleSize = 1`) or of a library class (`point.x = 3`), crashed with a null dereference when reading the declaration's annotations. Compound assignments such as `opts.sampleSize += 1` took the same path. The write now stands in for the missing declaration, so it is checked like one to a field without a declared refinement, and the ghost field update only runs for fields declared in the analyzed sources, which are the only ones that have one. An instance whose type cannot be resolved is typed as Object, as variables already are, which also makes two supertype lookups repeated after adding an instance redundant. Fixes #426. Co-Authored-By: Claude Opus 5.5 --- .../CorrectUnresolvedFieldWrite.java | 23 +++++++++++++++++++ .../testSuite/ErrorUnresolvedFieldWrite.java | 17 ++++++++++++++ .../liquidjava/processor/context/Context.java | 2 +- .../RefinementTypeChecker.java | 9 +++++--- .../object_checkers/AuxStateHandler.java | 9 +++----- 5 files changed, 50 insertions(+), 10 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldWrite.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldWrite.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldWrite.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldWrite.java new file mode 100644 index 00000000..811dd799 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldWrite.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldWrite.java new file mode 100644 index 00000000..ee69d2a0 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 26e3df72..11fc653c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -209,7 +209,7 @@ public void removeVarFromContext(String 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); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 2eca46ed..f89d743d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -256,10 +256,13 @@ private void visitAssignment(CtAssignment 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); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 11a1f7e4..a8fd6147 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/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; From f80754bb047a51637e250e0ed2ea044fd1e1c4cf Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 17:49:06 +0000 Subject: [PATCH 3/3] Check for loops whose body is an empty statement `for (...; ...; ...) ;` has no body, so `CtFor.getBody()` is null and looking for a `continue` in it crashed with a null dereference. A missing body is now treated as an empty one: the condition and the update are still checked. `while`, `do` and for-each loops with an empty statement body already verified; the regression covers them too. Fixes #395. Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectEmptyLoopBody.java | 33 +++++++++++++++++++ .../java/testSuite/ErrorEmptyLoopBody.java | 14 ++++++++ .../RefinementTypeChecker.java | 5 +-- 3 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEmptyLoopBody.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEmptyLoopBody.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEmptyLoopBody.java b/liquidjava-example/src/main/java/testSuite/CorrectEmptyLoopBody.java new file mode 100644 index 00000000..71b398ae --- /dev/null +++ b/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 it, int[] xs) { + while (it.hasNext() && it.next() != null) + ; + do + ; + while (it.hasNext() && it.next() != null); + for (int x : xs) + ; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEmptyLoopBody.java b/liquidjava-example/src/main/java/testSuite/ErrorEmptyLoopBody.java new file mode 100644 index 00000000..a9756474 --- /dev/null +++ b/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 + ; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index f89d743d..3b6e3ac8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -678,8 +678,9 @@ public void visitCtFor(CtFor forLoop) { scan(forLoop.getExpression()); assumeLoopCondition(forLoop.getExpression()); List 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);