Verify static and default interface method bodies (#385)

Fixes #343.

The verifier assumed every return and `this` access belonged to a class,
so static and default interface methods crashed before verification.
Return checking now uses the nearest method and its declaring type,
resolves overloads by parameter types, and keeps lambda returns separate
from an enclosing method. Interface method invocations also use their
registered contracts.

New passing cases cover the reported `String.length()` call, annotated
static/default methods, `return this`, same-arity overloads, and lambda
returns inside interface bodies. New failing cases require errors for
invalid static/default returns and a bad interface method argument.

Validation: `mvn test` passed all 391 tests, and the four new fixtures
produced their expected outcomes when run directly.

This change does not extend interface supertype contract inheritance.

Author: CatarinaGamboa

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

@@ -0,0 +1,43 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface CorrectInterfaceMethodBodies {
+    static int size(String s) {
+        int n = s.length();
+        return n;
+    }
+
+    @Refinement("_ > 0")
+    static int positive() {
+        return 1;
+    }
+
+    static void checkStaticContract() {
+        @Refinement("_ > 0")
+        int n = positive();
+    }
+
+    @Refinement("_ > 0")
+    default int defaultPositive() {
+        return 1;
+    }
+
+    default CorrectInterfaceMethodBodies self() {
+        return this;
+    }
+
+    @Refinement("_ > 0")
+    default int lambdaReturnIsNotMethodReturn() {
+        java.util.function.IntSupplier supplier = () -> { return -1; };
+        return 1;
+    }
+
+    java.util.function.IntSupplier FIELD_SUPPLIER = () -> { return -1; };
+
+    @Refinement("_ > 0")
+    static int overloaded(int value) { return 1; }
+
+    @Refinement("_ < 0")
+    static int overloaded(boolean value) { return -1; }
+}

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

@@ -0,0 +1,10 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface ErrorInterfaceDefaultReturn {
+    @Refinement("_ > 0")
+    default int positive() {
+        return -1; // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface ErrorInterfaceMethodCall {
+    static void requirePositive(@Refinement("_ > 0") int value) {}
+
+    static void badCall() {
+        requirePositive(-1); // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,10 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface ErrorInterfaceStaticReturn {
+    @Refinement("_ > 0")
+    static int positive() {
+        return -1; // Expect: Refinement Error
+    }
+}

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

@@ -214,7 +214,9 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
     @Override
     public <T> void visitCtThisAccess(CtThisAccess<T> thisAccess) {
         super.visitCtThisAccess(thisAccess);
-        CtClass<?> c = thisAccess.getParent(CtClass.class);
+        CtType<?> c = thisAccess.getParent(CtType.class);
+        if (c == null)
+            return;
         String s = c.getSimpleName();
         if (thisAccess.getParent() instanceof CtReturn) {
             String thisName = String.format(Formats.THIS, s);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -33,6 +33,7 @@
 import spoon.reflect.declaration.CtInterface;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.declaration.CtParameter;
+import spoon.reflect.declaration.CtType;
 import spoon.reflect.reference.CtExecutableReference;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -189,23 +190,31 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
     }
 
     public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
-        CtClass<?> c = ret.getParent(CtClass.class);
-        String className = c.getSimpleName();
         if (ret.getReturnedExpression() == null) {
             return;
         }
 
+        // A return in a lambda belongs to that lambda, even when it is nested in a method.
+        // Looking for any enclosing CtMethod would check it against the outer method's contract.
+        CtExecutable<?> executable = ret.getParent(CtExecutable.class);
+        if (!(executable instanceof CtMethod<?> method))
+            return;
+        CtType<?> owner = method.getDeclaringType();
+        if (owner == null)
+            return;
+
         // check if there are refinements
         if (rtc.getRefinement(ret.getReturnedExpression()) == null)
             ret.getReturnedExpression().putMetadata(Keys.REFINEMENT, new Predicate());
-        CtMethod<?> method = ret.getParent(CtMethod.class);
-
         // check if method has refinements
-        if (rtc.getRefinement(method) == null || !(method.getParent() instanceof CtClass))
+        if (rtc.getRefinement(method) == null)
             return;
 
-        RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
-                ((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
+        List<CtTypeReference<?>> parameterTypes = new ArrayList<>();
+        for (CtParameter<?> parameter : method.getParameters())
+            parameterTypes.add(parameter.getType());
+        RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), owner.getQualifiedName(),
+                parameterTypes);
         if (fi == null)
             return;
 
@@ -215,8 +224,8 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
         }
 
         // Both return and the method have metadata
-        String thisName = String.format(Formats.THIS, className);
-        rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret);
+        String thisName = String.format(Formats.THIS, owner.getSimpleName());
+        rtc.getContext().addInstanceToContext(thisName, owner.getReference(), new Predicate(), ret);
 
         String returnVarName = String.format(Formats.RET, rtc.getContext().getCounter());
         Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression())
@@ -242,8 +251,8 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJEr
             if (cte != null)
                 searchMethodInLibrary(cte, invocation);
 
-        } else if (method.getParent() instanceof CtClass) {
-            String ctype = ((CtClass<?>) method.getParent()).getQualifiedName();
+        } else if (method.getParent()instanceof CtType<?> owner) {
+            String ctype = owner.getQualifiedName();
             List<CtTypeReference<?>> paramTypes = invocation.getExecutable().getParameters();
             RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, paramTypes);
             if (f != null) { // inside rtc.context