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/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/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/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/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-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/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-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..11fc653c 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)); @@ -202,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..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 @@ -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); } } @@ -675,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); 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;