Apply external class specs to user subclasses

liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_correct/AppException.java

@@ -0,0 +1,14 @@
+package testSuite.classes.throwable_subclass_correct;
+
+// A project exception whose constructor sets no cause (Throwable(String)), so one initCause is allowed.
+public class AppException extends RuntimeException {
+    public AppException(String message) {
+        super(message);
+    }
+
+    static AppException wrap(Exception underlying) {
+        AppException e = new AppException("operation failed");
+        e.initCause(underlying);
+        return e;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_correct/ThrowableRefinements.java

@@ -0,0 +1,24 @@
+package testSuite.classes.throwable_subclass_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({ "noThrowable", "withThrowable" })
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable();
+
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(String message, Throwable cause);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    public Throwable initCause(Throwable cause);
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_error/AppException.java

@@ -0,0 +1,15 @@
+package testSuite.classes.throwable_subclass_error;
+
+// A project exception: its constructor passes the cause up through RuntimeException to Throwable(String, Throwable),
+// so the object already has a cause and initCause throws IllegalStateException("Can't overwrite cause").
+public class AppException extends RuntimeException {
+    public AppException(String message, Throwable cause) {
+        super(message, cause);
+    }
+
+    static AppException wrap(Exception underlying, Exception detail) {
+        AppException e = new AppException("operation failed", underlying);
+        e.initCause(detail); // Expect: State Refinement Error
+        return e;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_error/ThrowableRefinements.java

@@ -0,0 +1,24 @@
+package testSuite.classes.throwable_subclass_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({ "noThrowable", "withThrowable" })
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable();
+
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(String message, Throwable cause);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    public Throwable initCause(Throwable cause);
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -29,6 +29,7 @@ public final class DebugLog {
     private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
     private static final String SMT_CHECK = Colors.SALMON + "[SMT CHECK]" + Colors.RESET;
     private static final String SMP_TAG = Colors.YELLOW + "[SMP]" + Colors.RESET;
+    private static final String WARN_TAG = Colors.SALMON + "[WARN]" + Colors.RESET;
 
     private DebugLog() {
     }
@@ -37,6 +38,17 @@ public static boolean enabled() {
         return CommandLineLauncher.cmdArgs.debugMode;
     }
 
+    /**
+     * A non-fatal problem the verifier worked around (e.g. a supertype it could not resolve), which may explain a
+     * missing or unexpected result.
+     */
+    public static void warn(String message) {
+        if (!enabled()) {
+            return;
+        }
+        System.out.println(WARN_TAG + " " + message);
+    }
+
     /**
      * One-line header for a verification check: emits the absolute file path + line so terminals (iTerm2, VS Code,
      * WezTerm, …) make it ⌘/Ctrl-clickable. Replaces the older two-line {@code info()} prints.

liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java

@@ -37,12 +37,14 @@ public void process(CtPackage pkg) {
 
     private void processPackage(CtPackage pkg, Context c) {
         try {
-            // first pass: gather refinements
-            pkg.getTypes().forEach(type -> {
-                type.accept(new FieldGhostsGeneration(c, factory));
-                type.accept(new ExternalRefinementTypeChecker(c, factory));
-                type.accept(new MethodsFirstChecker(c, factory));
-            });
+            // first pass: gather refinements. External specifications are registered for every type before any class's
+            // own methods and constructors, which may rely on them (an unannotated constructor inherits the state of
+            // the
+            // specified super constructor it calls; an override is checked against its supertype's spec), whatever the
+            // order of the types in the package.
+            pkg.getTypes().forEach(type -> type.accept(new FieldGhostsGeneration(c, factory)));
+            pkg.getTypes().forEach(type -> type.accept(new ExternalRefinementTypeChecker(c, factory)));
+            pkg.getTypes().forEach(type -> type.accept(new MethodsFirstChecker(c, factory)));
 
             // second pass: check refinements
             pkg.getTypes().forEach(type -> {

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

@@ -1,8 +1,11 @@
 package liquidjava.processor.context;
 
 import java.util.ArrayList;
+import java.util.Deque;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.reference.CtTypeReference;
@@ -27,12 +30,29 @@ public List<CtTypeReference<?>> getSuperTypes() {
         return supertypes;
     }
 
+    /**
+     * Records the given superclass and interfaces and, transitively, all of theirs: a spec written for an indirect
+     * supertype must also apply to this variable (e.g. the {@code Throwable} spec on an {@code IOException}, whose
+     * direct superclass is {@code Exception}).
+     */
     public void addSuperTypes(CtTypeReference<?> ts, Set<CtTypeReference<?>> sts) {
-        if (ts != null && !supertypes.contains(ts))
-            supertypes.add(ts);
-        for (CtTypeReference<?> ct : sts)
-            if (ct != null && !supertypes.contains(ct))
-                supertypes.add(ct);
+        // LinkedList, unlike ArrayDeque, accepts the nulls of a missing superclass, skipped when polled
+        Deque<CtTypeReference<?>> todo = new LinkedList<>(sts);
+        todo.addFirst(ts);
+        while (!todo.isEmpty()) {
+            CtTypeReference<?> t = todo.poll();
+            if (t == null || supertypes.contains(t))
+                continue;
+            supertypes.add(t);
+            try {
+                todo.add(t.getSuperclass());
+                todo.addAll(t.getSuperInterfaces());
+            } catch (RuntimeException | LinkageError e) {
+                // a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch
+                DebugLog.warn("Could not resolve the supertypes of " + t.getQualifiedName()
+                        + "; specs declared above it will not apply to " + getName() + " (" + e + ")");
+            }
+        }
     }
 
     public void setPlacementInCode(CtElement element) {

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

@@ -19,6 +19,7 @@
 import spoon.reflect.code.*;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.*;
+import spoon.reflect.reference.CtExecutableReference;
 import spoon.reflect.reference.CtTypeReference;
 
 public class AuxStateHandler {
@@ -44,11 +45,82 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
                 }
             }
             setConstructorStates(f, an, c);
-        } else {
+        } else if (!inheritSuperConstructorState(c, f, tc)) {
             setDefaultState(f, tc);
         }
     }
 
+    /**
+     * An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the
+     * called superclass constructor's specification gives it (e.g. {@code MyException(String m, Throwable c) { super(m,
+     * c); }} with the {@code Throwable(String, Throwable)} spec: {@code withThrowable(this)}). The super constructor's
+     * parameters are renamed to the arguments passed, which must be parameters of this constructor or literals.
+     *
+     * @return whether a state was inherited (otherwise the caller falls back to the default state)
+     */
+    private static boolean inheritSuperConstructorState(CtConstructor<?> c, RefinedFunction f, TypeChecker tc) {
+        CtStatement first = c.getBody() == null || c.getBody().getStatements().isEmpty() ? null
+                : c.getBody().getStatement(0);
+        if (!(first instanceof CtInvocation<?> call) || !call.getExecutable().isConstructor()
+                || c.getDeclaringType() == null
+                || c.getDeclaringType().getReference().equals(call.getExecutable().getDeclaringType()))
+            return false; // not a super(...) call (this(...) delegates within the class)
+        RefinedFunction superF = specifiedConstructor(tc, call.getExecutable());
+        List<CtExpression<?>> args = call.getArguments();
+        if (superF == null || superF.getToStates().isEmpty() || superF.getArguments().size() != args.size())
+            return false;
+
+        // rename each super parameter to the argument passed for it; a state may not mention an unnamed one
+        Map<String, String> rename = new HashMap<>();
+        Set<String> unnamed = new HashSet<>();
+        for (int i = 0; i < args.size(); i++) {
+            String param = superF.getArguments().get(i).getName();
+            argumentName(args.get(i)).ifPresentOrElse(a -> rename.put(param, a), () -> unnamed.add(param));
+        }
+        if (superF.getToStates().stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unnamed::contains)))
+            return false;
+        f.setAllStates(superF.getToStates().stream()
+                .map(to -> new ObjectState(null, rename.entrySet().stream().reduce(to,
+                        (p, r) -> p.substituteVariable(r.getKey(), r.getValue()), (p, q) -> p)))
+                .collect(Collectors.toList()));
+        return true;
+    }
+
+    /** How a state can refer to {@code arg}: by the caller's parameter name or a non-string literal's value. */
+    private static Optional<String> argumentName(CtExpression<?> arg) {
+        if (arg instanceof CtVariableRead<?> vr
+                && vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference<?>)
+            return Optional.of(vr.getVariable().getSimpleName());
+        if (arg instanceof CtLiteral<?> lit && lit.getValue() != null && !(lit.getValue() instanceof String))
+            return Optional.of(lit.getValue().toString());
+        return Optional.empty();
+    }
+
+    /**
+     * JDK classes whose constructors all pass their arguments unchanged to the superclass constructor with the same
+     * parameter types (documented in their Javadoc), so a spec on that superclass constructor describes them too. Only
+     * these are walked through: other binary classes may not (e.g. {@code ClassNotFoundException(String)} sets a null
+     * cause), and assuming they did would hide real errors.
+     */
+    private static final Set<String> DELEGATING_JDK_CLASSES = Set.of("java.lang.Exception",
+            "java.lang.RuntimeException", "java.lang.Error");
+
+    /** The specified constructor that {@code exe} ends up running, if one is known. */
+    private static RefinedFunction specifiedConstructor(TypeChecker tc, CtExecutableReference<?> exe) {
+        for (CtTypeReference<?> t = exe.getDeclaringType(); t != null;) {
+            RefinedFunction f = tc.getContext().getFunction(exe.getSimpleName(), t.getQualifiedName(),
+                    exe.getParameters());
+            if (f != null || !DELEGATING_JDK_CLASSES.contains(t.getQualifiedName()))
+                return f;
+            try {
+                t = t.getSuperclass();
+            } catch (RuntimeException | LinkageError e) {
+                return null;
+            }
+        }
+        return null;
+    }
+
     /**
      * Creates the list of states and adds them to the function
      *