From 4ca03538ba524bf2ecd52179215be8cff94313a2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 20:53:45 +0000 Subject: [PATCH 1/6] Read constructor delegation from JDK bytecode Add ConstructorDelegation, which reads a JDK class with ASM and reports whether a constructor's whole body is a call to a superclass constructor (aload_0, loads of its parameters or constants, invokespecial, return), and what it passes for each superclass parameter. Results are cached per constructor. Adds org.ow2.asm:asm 9.11 (BSD-3-Clause). Co-Authored-By: Claude Opus 5.5 --- liquidjava-verifier/pom.xml | 6 + .../ConstructorDelegation.java | 274 ++++++++++++++++++ .../ConstructorDelegationTest.java | 70 +++++ 3 files changed, 350 insertions(+) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 84891bc2..4ffa83bc 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -368,6 +368,12 @@ picocli 4.7.7 + + + org.ow2.asm + asm + 9.11 + diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java new file mode 100644 index 00000000..c8c83a7d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java @@ -0,0 +1,274 @@ +package liquidjava.processor.refinement_checker.object_checkers; + +import java.io.IOException; +import java.io.InputStream; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.concurrent.ConcurrentHashMap; +import java.util.function.Function; + +import org.objectweb.asm.ClassReader; +import org.objectweb.asm.ClassVisitor; +import org.objectweb.asm.Handle; +import org.objectweb.asm.Label; +import org.objectweb.asm.MethodVisitor; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.Type; + +/** + * A binary constructor whose whole body is a call to a superclass constructor, read from its bytecode: which superclass + * constructor it calls and what it passes for each parameter. Only that exact shape is recognized, so the object ends + * up in whatever state the superclass constructor leaves it in: + * + * 
+ * aload_0
+ * (a load of one of its parameters | a constant [checkcast])*
+ * invokespecial Superclass.<init>
+ * return
+ *
+ * + * Anything else (field writes, method calls, this(...), branches) is not a delegation. Classes are read from the JDK + * only: the verifier runs without the analyzed program's classpath, and the verifier's own libraries may differ from + * the versions the program uses. + * + * @param superclass + * qualified name of the superclass whose constructor is called + * @param superParameterTypes + * qualified names of that constructor's parameter types + * @param arguments + * what is passed for each of them + */ +public record ConstructorDelegation(String superclass, List superParameterTypes, List arguments) { + + /** A value passed to the superclass constructor. */ + public sealed interface Argument permits Parameter,Constant { + } + + /** The delegating constructor's parameter at {@code index}, unchanged. */ + public record Parameter(int index) implements Argument { + } + + /** + * A constant, with how a state can refer to it ({@code 0}, {@code true}); empty when it cannot (e.g. {@code null}). + */ + public record Constant(Optional value) implements Argument { + } + + private static final Map> CACHE = new ConcurrentHashMap<>(); + + /** + * How the constructor of {@code className} with these parameter types delegates to a superclass constructor, if its + * bytecode is available and has exactly that shape. + */ + public static Optional of(String className, List parameterTypes) { + return CACHE.computeIfAbsent(className + parameterTypes, k -> read(className, parameterTypes)); + } + + private static Optional read(String className, List parameterTypes) { + String resource = className.replace('.', '/') + ".class"; + try (InputStream in = ClassLoader.getPlatformClassLoader().getResourceAsStream(resource)) { + if (in == null) + return Optional.empty(); + ClassReader reader = new ClassReader(in); + ConstructorFinder finder = new ConstructorFinder(reader.getSuperName(), parameterTypes); + reader.accept(finder, ClassReader.SKIP_DEBUG); + return finder.delegation(); + } catch (IOException | RuntimeException e) { + return Optional.empty(); // unreadable or unsupported class file: not known to delegate + } + } + + /** Hands the constructor with the wanted parameter types to a {@link DelegationMatcher}. */ + private static final class ConstructorFinder extends ClassVisitor { + private final String superclass; + private final List parameterTypes; + private DelegationMatcher matcher; + + ConstructorFinder(String superclass, List parameterTypes) { + super(Opcodes.ASM9); + this.superclass = superclass; + this.parameterTypes = parameterTypes; + } + + @Override + public MethodVisitor visitMethod(int access, String name, String descriptor, String signature, + String[] exceptions) { + Type[] params = Type.getArgumentTypes(descriptor); + if (superclass == null || !name.equals("") + || !Arrays.stream(params).map(Type::getClassName).toList().equals(parameterTypes)) + return null; + matcher = new DelegationMatcher(superclass, params); + return matcher; + } + + Optional delegation() { + return matcher == null ? Optional.empty() : matcher.delegation(); + } + } + + /** + * Follows a constructor's instructions through the delegating shape, failing on the first one that does not fit. + * Labels, line numbers, frames and local variable tables are not instructions and are ignored. + */ + private static final class DelegationMatcher extends MethodVisitor { + private enum Step { + RECEIVER, ARGUMENTS, RETURN, DONE, FAILED + } + + private final String superclass; + private final Type[] params; + /** What each pushed value is, given the type of the superclass parameter it ends up passed for. */ + private final List> pushed = new ArrayList<>(); + private boolean lastPushedNull; + private Step step = Step.RECEIVER; + private ConstructorDelegation delegation; + + DelegationMatcher(String superclass, Type[] params) { + super(Opcodes.ASM9); + this.superclass = superclass; + this.params = params; + } + + Optional delegation() { + return step == Step.DONE ? Optional.of(delegation) : Optional.empty(); + } + + @Override + public void visitVarInsn(int opcode, int slot) { + if (step == Step.RECEIVER && opcode == Opcodes.ALOAD && slot == 0) + step = Step.ARGUMENTS; + else if (step == Step.ARGUMENTS) + parameterAt(slot).filter(i -> opcode == params[i].getOpcode(Opcodes.ILOAD)) + .ifPresentOrElse(i -> push(t -> new Parameter(i)), this::fail); + else + fail(); + } + + /** The parameter stored in local variable {@code slot} (slot 0 is {@code this}; long and double take two). */ + private Optional parameterAt(int slot) { + int next = 1; + for (int i = 0; i < params.length; next += params[i].getSize(), i++) + if (next == slot) + return Optional.of(i); + return Optional.empty(); + } + + @Override + public void visitInsn(int opcode) { + if (step == Step.RETURN && opcode == Opcodes.RETURN) + step = Step.DONE; + else if (step == Step.ARGUMENTS && opcode == Opcodes.ACONST_NULL) { + push(t -> new Constant(Optional.empty())); + lastPushedNull = true; + } else if (step == Step.ARGUMENTS && opcode >= Opcodes.ICONST_M1 && opcode <= Opcodes.ICONST_5) + pushInt(opcode - Opcodes.ICONST_0); + else if (step == Step.ARGUMENTS && opcode >= Opcodes.LCONST_0 && opcode <= Opcodes.DCONST_1) + push(t -> new Constant(Optional.empty())); + else + fail(); + } + + @Override + public void visitIntInsn(int opcode, int operand) { + if (step == Step.ARGUMENTS && (opcode == Opcodes.BIPUSH || opcode == Opcodes.SIPUSH)) + pushInt(operand); + else + fail(); + } + + /** An int constant: a boolean, a number, or a char a state cannot write, depending on the parameter. */ + private void pushInt(int value) { + push(t -> new Constant(switch (t.getSort()) { + case Type.BOOLEAN -> Optional.of(Boolean.toString(value != 0)); + case Type.INT, Type.SHORT, Type.BYTE -> Optional.of(Integer.toString(value)); + default -> Optional.empty(); + })); + } + + private void push(Function argument) { + pushed.add(argument); + lastPushedNull = false; + } + + @Override + public void visitLdcInsn(Object value) { + if (step == Step.ARGUMENTS && value instanceof Integer i) + pushInt(i); + else if (step == Step.ARGUMENTS) + push(t -> new Constant(Optional.empty())); // strings, classes, other constants + else + fail(); + } + + @Override + public void visitTypeInsn(int opcode, String type) { + // javac casts a null argument to pick an overload, e.g. super((Throwable) null) + if (step != Step.ARGUMENTS || opcode != Opcodes.CHECKCAST || !lastPushedNull) + fail(); + } + + @Override + public void visitMethodInsn(int opcode, String owner, String name, String descriptor, boolean isInterface) { + Type[] superParams = Type.getArgumentTypes(descriptor); + if (step != Step.ARGUMENTS || opcode != Opcodes.INVOKESPECIAL || !owner.equals(superclass) + || !name.equals("") || superParams.length != pushed.size()) { + fail(); + return; + } + List arguments = new ArrayList<>(); + for (int i = 0; i < superParams.length; i++) + arguments.add(pushed.get(i).apply(superParams[i])); + delegation = new ConstructorDelegation(Type.getObjectType(superclass).getClassName(), + Arrays.stream(superParams).map(Type::getClassName).toList(), arguments); + step = Step.RETURN; + } + + @Override + public void visitFieldInsn(int opcode, String owner, String name, String descriptor) { + fail(); + } + + @Override + public void visitInvokeDynamicInsn(String name, String descriptor, Handle bootstrap, + Object... bootstrapArguments) { + fail(); + } + + @Override + public void visitJumpInsn(int opcode, Label label) { + fail(); + } + + @Override + public void visitIincInsn(int slot, int increment) { + fail(); + } + + @Override + public void visitTableSwitchInsn(int min, int max, Label dflt, Label... labels) { + fail(); + } + + @Override + public void visitLookupSwitchInsn(Label dflt, int[] keys, Label[] labels) { + fail(); + } + + @Override + public void visitMultiANewArrayInsn(String descriptor, int dimensions) { + fail(); + } + + @Override + public void visitTryCatchBlock(Label start, Label end, Label handler, String type) { + fail(); + } + + private void fail() { + step = Step.FAILED; + } + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java new file mode 100644 index 00000000..ca33a52b --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java @@ -0,0 +1,70 @@ +package liquidjava.processor.refinement_checker.object_checkers; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.util.List; +import java.util.Optional; + +import liquidjava.processor.refinement_checker.object_checkers.ConstructorDelegation.Constant; +import liquidjava.processor.refinement_checker.object_checkers.ConstructorDelegation.Parameter; +import org.junit.jupiter.api.Test; + +class ConstructorDelegationTest { + + private static final Constant UNNAMED = new Constant(Optional.empty()); + + @Test + void passesItsParametersOnUnchanged() { + assertEquals(Optional.of(new ConstructorDelegation("java.lang.Throwable", + List.of("java.lang.String", "java.lang.Throwable"), List.of(new Parameter(0), new Parameter(1)))), + ConstructorDelegation.of("java.lang.Exception", List.of("java.lang.String", "java.lang.Throwable"))); + } + + @Test + void passesNullCastToPickAnOverload() { + // aload_0; aconst_null; checkcast Throwable; invokespecial ReflectiveOperationException(Throwable) + assertEquals( + Optional.of(new ConstructorDelegation("java.lang.ReflectiveOperationException", + List.of("java.lang.Throwable"), List.of(UNNAMED))), + ConstructorDelegation.of("java.lang.ClassNotFoundException", List.of())); + } + + @Test + void passesAParameterAndAConstant() { + assertEquals( + Optional.of(new ConstructorDelegation("java.lang.ReflectiveOperationException", + List.of("java.lang.String", "java.lang.Throwable"), List.of(new Parameter(0), UNNAMED))), + ConstructorDelegation.of("java.lang.ClassNotFoundException", List.of("java.lang.String"))); + } + + @Test + void namesBooleanAndIntConstantsBySuperParameterType() { + // ReferenceHandler(ThreadGroup g, String name) { super(g, null, name, 0, false); } + Optional d = ConstructorDelegation.of("java.lang.ref.Reference$ReferenceHandler", + List.of("java.lang.ThreadGroup", "java.lang.String")); + assertTrue(d.isPresent()); + assertEquals(List.of(new Parameter(0), UNNAMED, new Parameter(1), UNNAMED, new Constant(Optional.of("false"))), + d.get().arguments()); + } + + @Test + void rejectsAConstructorThatDoesMoreThanDelegate() { + // super(s); this.className = className; this.key = key; + assertEquals(Optional.empty(), ConstructorDelegation.of("java.util.MissingResourceException", + List.of("java.lang.String", "java.lang.String", "java.lang.String"))); + } + + @Test + void rejectsObjectAndUnknownConstructorsAndClasses() { + assertEquals(Optional.empty(), ConstructorDelegation.of("java.lang.Object", List.of())); + assertEquals(Optional.empty(), ConstructorDelegation.of("java.lang.Exception", List.of("int"))); + assertEquals(Optional.empty(), ConstructorDelegation.of("does.not.Exist", List.of())); + } + + @Test + void readsOnlyJdkClasses() { + // on the test classpath, but not part of the JDK + assertEquals(Optional.empty(), ConstructorDelegation.of(getClass().getName(), List.of())); + } +} From 560167a8c5d2a7252c78f91ad1e9c586c0a92a8d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 20:53:45 +0000 Subject: [PATCH 2/6] Walk to an ancestor's constructor spec through bytecode delegation Replace the hard-coded DELEGATING_JDK_CLASSES list: a constructor without a spec is followed through JDK constructors that only delegate, mapping each spec parameter back to the argument or constant passed for it, and looking up each ancestor's spec by exact parameter types. The walk is used both for super(...) in user constructors and for a direct new XException(...): new RuntimeException("m") now gets Throwable(String)'s state, and new ClassNotFoundException() gets Throwable(Throwable)'s withThrowable state. Anything else falls back to the default state as before. Co-Authored-By: Claude Opus 5.5 --- .../MyException.java | 10 ++ .../throwable_jdk_subclass_correct/Test.java | 29 ++++ .../ThrowableRefinements.java | 24 +++ .../NotFound.java | 7 + .../throwable_jdk_subclass_error/Test.java | 34 ++++ .../ThrowableRefinements.java | 24 +++ .../MethodsFunctionsChecker.java | 7 +- .../object_checkers/AuxStateHandler.java | 149 +++++++++++++----- 8 files changed, 246 insertions(+), 38 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java new file mode 100644 index 00000000..64a15673 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java @@ -0,0 +1,10 @@ +package testSuite.classes.throwable_jdk_subclass_correct; + +import java.io.IOException; + +// super(message) runs IOException(String), Exception(String) and then Throwable(String): no cause. +public class MyException extends IOException { + public MyException(String message) { + super(message); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java new file mode 100644 index 00000000..69727b29 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java @@ -0,0 +1,29 @@ +package testSuite.classes.throwable_jdk_subclass_correct; + +// JDK exceptions whose constructors only pass their arguments up to Throwable(String) or Throwable() are created +// without a cause, so one initCause is allowed. +public class Test { + static RuntimeException wrap(Throwable t) { + RuntimeException e = new RuntimeException("failed"); + e.initCause(t); + return e; + } + + static IllegalStateException illegalState(Throwable t) { + IllegalStateException e = new IllegalStateException("failed"); + e.initCause(t); + return e; + } + + static Exception noMessage(Throwable t) { + Exception e = new Exception(); + e.initCause(t); + return e; + } + + static MyException mine(Throwable t) { + MyException e = new MyException("failed"); + e.initCause(t); + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java new file mode 100644 index 00000000..abf87ffa --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java @@ -0,0 +1,24 @@ +package testSuite.classes.throwable_jdk_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); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java new file mode 100644 index 00000000..5544ed35 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java @@ -0,0 +1,7 @@ +package testSuite.classes.throwable_jdk_subclass_error; + +public class NotFound extends ClassNotFoundException { + public NotFound(String message) { + super(message); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java new file mode 100644 index 00000000..4fa6d6c0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java @@ -0,0 +1,34 @@ +package testSuite.classes.throwable_jdk_subclass_error; + +import java.util.MissingResourceException; + +public class Test { + // ClassNotFoundException() runs Throwable(Throwable) with a null cause, so initCause throws + // IllegalStateException("Can't overwrite cause") (scijava-common CommandInfo, fixed in a6fd9cf) + static ClassNotFoundException notFound(Throwable exc) throws ClassNotFoundException { + final ClassNotFoundException cnfe = new ClassNotFoundException(); + cnfe.initCause(exc); // Expect: State Refinement Error + throw cnfe; + } + + static RuntimeException causeTwice(Throwable cause, Throwable other) { + RuntimeException e = new RuntimeException("failed", cause); + e.initCause(other); // Expect: State Refinement Error + return e; + } + + // super(message) runs ClassNotFoundException(String), which passes a null cause on to Throwable(String, Throwable) + static NotFound notFoundSubclass(Throwable exc) { + NotFound e = new NotFound("missing"); + e.initCause(exc); // Expect: State Refinement Error + return e; + } + + // MissingResourceException(String, String, String) also writes fields after super(message), so it is not known to + // delegate and gets the default state, in which initCause cannot be shown to be allowed (#367) + static MissingResourceException notDelegating(Throwable exc) { + MissingResourceException e = new MissingResourceException("missing", "Bundle", "key"); + e.initCause(exc); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java new file mode 100644 index 00000000..46ed475d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java @@ -0,0 +1,24 @@ +package testSuite.classes.throwable_jdk_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); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 92f0b9d2..272c1e83 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -78,10 +78,13 @@ public void getConstructorInvocationRefinements(CtConstructorCall ctConstruct f.getTargetClass(), paramTypes); AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall); } else { - // default constructor refinements + // the state of a specified ancestor constructor it delegates to, else the default CtTypeReference type = exe.getDeclaringType() != null ? exe.getDeclaringType() : ctConstructorCall.getType(); - if (type != null) + Optional delegated = AuxStateHandler.delegatedConstructorState(rtc, ctConstructorCall); + if (delegated.isPresent()) + ctConstructorCall.putMetadata(Keys.REFINEMENT, delegated.get()); + else if (type != null) ctConstructorCall.putMetadata(Keys.REFINEMENT, AuxStateHandler.getDefaultState(rtc, type.getQualifiedName(), Predicate.createVar(Keys.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 a03c2824..51f03af9 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 @@ -76,25 +76,55 @@ private static boolean inheritSuperConstructorState(CtConstructor c, RefinedF || 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> args = call.getArguments(); - if (superF == null || superF.getToStates().isEmpty() || superF.getArguments().size() != args.size()) - return false; + List> names = call.getArguments().stream().map(AuxStateHandler::argumentName).toList(); + Optional> states = specifiedStates(tc, call.getExecutable(), names); + states.ifPresent( + to -> f.setAllStates(to.stream().map(p -> new ObjectState(null, p)).collect(Collectors.toList()))); + return states.isPresent(); + } + + /** + * The state that {@code new C(...)} gives when {@code C}'s constructor has no specification of its own but is a + * binary constructor that delegates to a specified one of an ancestor (e.g. {@code new RuntimeException(m)} runs + * {@code Throwable(String)}), with the arguments renamed as in {@link #inheritSuperConstructorState}. + */ + public static Optional delegatedConstructorState(TypeChecker tc, CtConstructorCall call) { + List> names = call.getArguments().stream().map(a -> callArgumentName(tc, a)).toList(); + return specifiedStates(tc, call.getExecutable(), names).filter(to -> !to.isEmpty()).map(to -> to.get(0)); + } + + /** + * The to-states of the specified constructor that {@code exe} ends up running, with each of its parameters renamed + * to how a state can refer to the value passed for it. Empty if no specified constructor is known, or if a state + * mentions a parameter whose value cannot be named. + * + * @param argumentNames + * how a state can refer to each argument of the call to {@code exe} + */ + private static Optional> specifiedStates(TypeChecker tc, CtExecutableReference exe, + List> argumentNames) { + if (exe.getDeclaringType() == null || argumentNames.size() != exe.getParameters().size()) + return Optional.empty(); // e.g. a varargs call + Optional spec = specifiedConstructor(tc, exe); + if (spec.isEmpty() || spec.get().function().getToStates().isEmpty()) + return Optional.empty(); - // rename each super parameter to the argument passed for it; a state may not mention an unnamed one + // rename each spec parameter to the value passed for it; a state may not mention an unnamed one Map rename = new HashMap<>(); Set 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; + List params = spec.get().function().getArguments(); + for (int i = 0; i < params.size(); i++) { + String param = params.get(i).getName(); + ConstructorDelegation.Argument passed = spec.get().arguments().get(i); + Optional name = passed instanceof ConstructorDelegation.Parameter p ? argumentNames.get(p.index()) + : ((ConstructorDelegation.Constant) passed).value(); + name.ifPresentOrElse(n -> rename.put(param, n), () -> unnamed.add(param)); + } + List states = spec.get().function().getToStates(); + if (states.stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unnamed::contains))) + return Optional.empty(); + return Optional.of(states.stream().map(to -> rename.entrySet().stream().reduce(to, + (p, r) -> p.substituteVariable(r.getKey(), r.getValue()), (p, q) -> p)).toList()); } /** How a state can refer to {@code arg}: by the caller's parameter name or a non-string literal's value. */ @@ -102,34 +132,81 @@ private static Optional argumentName(CtExpression arg) { if (arg instanceof CtVariableRead vr && vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference) return Optional.of(vr.getVariable().getSimpleName()); + return literalName(arg); + } + + /** How a state can refer to {@code arg} at a call: by the local variable's current instance or a literal. */ + private static Optional callArgumentName(TypeChecker tc, CtExpression arg) { + if (arg instanceof CtVariableRead vr && !(arg instanceof CtFieldRead)) + return tc.getContext().getLastVariableInstance(vr.getVariable().getSimpleName()).map(Refined::getName); + return literalName(arg); + } + + private static Optional literalName(CtExpression arg) { 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. + * A constructor specification, and what a call passes for each of its parameters. + * + * @param arguments + * for each parameter of {@code function}: an index into the call's arguments, or a constant */ - private static final Set 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; - } + private record SpecifiedConstructor(RefinedFunction function, List arguments) { + } + + /** + * The specified constructor that {@code exe} ends up running, if one is known. A binary constructor without a + * specification is walked through only when its bytecode just passes values on to a superclass constructor (e.g. + * {@code RuntimeException(String)} to {@code Exception(String)} to {@code Throwable(String)}); assuming any other + * constructor did so would hide real errors (e.g. {@code ClassNotFoundException(String)} also sets a null cause). + */ + private static Optional specifiedConstructor(TypeChecker tc, CtExecutableReference exe) { + List arguments = new ArrayList<>(); + for (int i = 0; i < exe.getParameters().size(); i++) + arguments.add(new ConstructorDelegation.Parameter(i)); + String klass = exe.getDeclaringType().getQualifiedName(); + RefinedFunction f = tc.getContext().getFunction(exe.getSimpleName(), klass, exe.getParameters()); + Optional> types = erasedNames(exe.getParameters()); + while (f == null && types.isPresent()) { + Optional delegation = ConstructorDelegation.of(klass, types.get()); + if (delegation.isEmpty()) + return Optional.empty(); + arguments = passedOn(arguments, delegation.get().arguments()); + klass = delegation.get().superclass(); + types = Optional.of(delegation.get().superParameterTypes()); + // exact types: the arity fallback of getFunction could pick another overload's spec + f = tc.getContext().getFunctionExact(exe.getSimpleName(), klass, typeReferences(tc, types.get())); } - return null; + return f == null ? Optional.empty() : Optional.of(new SpecifiedConstructor(f, arguments)); + } + + /** + * What reaches the superclass constructor, in terms of the original call: a parameter passed on refers back to the + * value the call gave for it. + */ + private static List passedOn(List callArguments, + List delegated) { + return delegated.stream() + .map(a -> a instanceof ConstructorDelegation.Parameter p ? callArguments.get(p.index()) : a).toList(); + } + + /** The erased qualified names of {@code types}, as in bytecode descriptors, if they can be resolved. */ + private static Optional> erasedNames(List> types) { + try { + return Optional.of(types.stream().map(t -> t.getTypeErasure().getQualifiedName()).toList()); + } catch (RuntimeException e) { + return Optional.empty(); + } + } + + private static List> typeReferences(TypeChecker tc, List names) { + List> refs = new ArrayList<>(); + for (String name : names) + refs.add(tc.getFactory().Type().createReference(name)); + return refs; } /** From 1dfb337c78a5388cccda9de4ddb4430dbb854e3b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 21:23:39 +0000 Subject: [PATCH 3/6] Tighten state inheritance from delegated constructors - Inherit a super constructor's state only when the constructor body is just that super(...) call and the class has no instance initializers or field initializers: anything after super(...) may change the state (e.g. super(m); initCause(c);), which was missed, also before this branch, for subclasses of RuntimeException. - Pass constant arguments to the spec as literals of the refinement language instead of variables named after their value. - Keep the default value of the constructed class's own state sets that the ancestor's spec does not mention (e.g. Stack's, after Vector()). - Pass a method parameter given to new by its name when it has no instance yet, as for other calls. - Leave anonymous classes (new C() { ... }) to the default state. - ConstructorDelegation: say that results depend on the JDK the verifier runs on; record cache key; check for a missing superclass once. Co-Authored-By: Claude Opus 5.5 --- .../HashSetRefinements.java | 20 +++ .../Test.java | 22 +++ .../StackRefinements.java | 15 ++ .../delegated_subclass_sets_error/Test.java | 17 +++ .../VectorRefinements.java | 12 ++ .../CauseAfterImplicitSuper.java | 16 +++ .../CauseAfterSuper.java | 16 +++ .../CauseInInitializer.java | 18 +++ .../ThrowableRefinements.java | 24 ++++ .../object_checkers/AuxStateHandler.java | 134 ++++++++++++------ .../ConstructorDelegation.java | 23 +-- .../liquidjava/rj_language/Predicate.java | 5 + .../ConstructorDelegationTest.java | 20 ++- 13 files changed, 286 insertions(+), 56 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java new file mode 100644 index 00000000..4171829f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java @@ -0,0 +1,20 @@ +package testSuite.classes.delegated_constant_arguments_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.HashSet") +@Ghost("int capacity") +@StateSet({ "plain", "linked" }) +public interface HashSetRefinements { + @StateRefinement(to = "capacity(this) == initialCapacity && (dummy --> linked(this)) && (!dummy --> plain(this))") + void HashSet(int initialCapacity, float loadFactor, boolean dummy); + + @StateRefinement(from = "capacity(this) == 16 && linked(this)") + boolean add(E e); + + @StateRefinement(from = "plain(this)") + void clear(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java new file mode 100644 index 00000000..b33a51f0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java @@ -0,0 +1,22 @@ +package testSuite.classes.delegated_constant_arguments_error; + +import java.util.LinkedHashSet; + +// LinkedHashSet() runs HashSet(16, .75f, true) and LinkedHashSet(int n) runs HashSet(n, .75f, true): the constants +// passed reach the spec as literals +public class Test { + static void defaultCapacity() { + LinkedHashSet s = new LinkedHashSet<>(); + s.add("x"); + } + + static void linked() { + LinkedHashSet s = new LinkedHashSet<>(); + s.clear(); // Expect: State Refinement Error + } + + static void otherCapacity(int n) { + LinkedHashSet s = new LinkedHashSet<>(n); + s.add("x"); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java new file mode 100644 index 00000000..640fce87 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.delegated_subclass_sets_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.Stack") +@StateSet({ "empty", "nonEmpty" }) +public interface StackRefinements { + @StateRefinement(from = "empty(this)", to = "nonEmpty(this)") + E push(E item); + + @StateRefinement(from = "nonEmpty(this)") + E peek(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java new file mode 100644 index 00000000..a55c1b87 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java @@ -0,0 +1,17 @@ +package testSuite.classes.delegated_subclass_sets_error; + +import java.util.Stack; + +// Stack() runs Vector(), whose spec sets only Vector's ghost: Stack's own state set starts at its default (empty) +public class Test { + static void pushThenPeek() { + Stack s = new Stack<>(); + s.push("a"); + s.peek(); + } + + static void peekEmpty() { + Stack s = new Stack<>(); + s.peek(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java new file mode 100644 index 00000000..9c029a16 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java @@ -0,0 +1,12 @@ +package testSuite.classes.delegated_subclass_sets_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.Vector") +@Ghost("int elements") +public interface VectorRefinements { + @StateRefinement(to = "elements(this) == 0") + void Vector(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java new file mode 100644 index 00000000..95227b24 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java @@ -0,0 +1,16 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +import java.io.IOException; + +// the implicit super() leaves no cause, but the constructor then sets one +public class CauseAfterImplicitSuper extends IOException { + public CauseAfterImplicitSuper(Throwable cause) { + initCause(cause); + } + + static CauseAfterImplicitSuper wrap(Throwable cause, Throwable other) { + CauseAfterImplicitSuper e = new CauseAfterImplicitSuper(cause); + e.initCause(other); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java new file mode 100644 index 00000000..41dbc89e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java @@ -0,0 +1,16 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +// super(message) leaves no cause, but the constructor then sets one, so it gets the default state, not +// Throwable(String)'s, and a second initCause is reported +public class CauseAfterSuper extends RuntimeException { + public CauseAfterSuper(String message, Throwable cause) { + super(message); + initCause(cause); + } + + static CauseAfterSuper wrap(Throwable cause, Throwable other) { + CauseAfterSuper e = new CauseAfterSuper("failed", cause); + e.initCause(other); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java new file mode 100644 index 00000000..6274034a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java @@ -0,0 +1,18 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +// an instance initializer runs right after super(message) and sets the cause +public class CauseInInitializer extends RuntimeException { + { + initCause(null); + } + + public CauseInInitializer(String message) { + super(message); + } + + static CauseInInitializer wrap(Throwable other) { + CauseInInitializer e = new CauseInInitializer("failed"); + e.initCause(other); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java new file mode 100644 index 00000000..a6f282c8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java @@ -0,0 +1,24 @@ +package testSuite.classes.throwable_subclass_more_than_super_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); +} 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 51f03af9..804a24e8 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 @@ -62,7 +62,7 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, } /** - * An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the + * An unannotated constructor whose body is only a {@code super(...)} call 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. @@ -70,81 +70,124 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, * @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) - List> names = call.getArguments().stream().map(AuxStateHandler::argumentName).toList(); - Optional> states = specifiedStates(tc, call.getExecutable(), names); + Optional> call = onlySuperCall(c); + if (call.isEmpty()) + return false; + List> values = call.get().getArguments().stream().map(AuxStateHandler::argumentValue) + .toList(); + Optional> states = specifiedStates(tc, call.get().getExecutable(), values, + c.getDeclaringType().getQualifiedName()); states.ifPresent( to -> f.setAllStates(to.stream().map(p -> new ObjectState(null, p)).collect(Collectors.toList()))); return states.isPresent(); } + /** + * The {@code super(...)} call that is all {@code c} runs, if so. Anything after it, or an instance initializer or + * field initializer of the class (which run right after it), may change the state, as in {@code super(m); + * initCause(c);}. This is the source counterpart of what {@link ConstructorDelegation} accepts in bytecode. + */ + private static Optional> onlySuperCall(CtConstructor c) { + CtType owner = c.getDeclaringType(); + if (owner == null || c.getBody() == null || c.getBody().getStatements().size() != 1 + || !(c.getBody().getStatement(0)instanceof CtInvocation call) + || !call.getExecutable().isConstructor() + || owner.getReference().equals(call.getExecutable().getDeclaringType())) + return Optional.empty(); // not only a super(...) call (this(...) delegates within the class) + boolean initializers = owner instanceof CtClass klass + && klass.getAnonymousExecutables().stream().anyMatch(block -> !block.isStatic()); + boolean fieldInitializers = owner.getFields().stream() + .anyMatch(field -> !field.isStatic() && field.getDefaultExpression() != null); + return initializers || fieldInitializers ? Optional.empty() : Optional.of(call); + } + /** * The state that {@code new C(...)} gives when {@code C}'s constructor has no specification of its own but is a * binary constructor that delegates to a specified one of an ancestor (e.g. {@code new RuntimeException(m)} runs * {@code Throwable(String)}), with the arguments renamed as in {@link #inheritSuperConstructorState}. */ public static Optional delegatedConstructorState(TypeChecker tc, CtConstructorCall call) { - List> names = call.getArguments().stream().map(a -> callArgumentName(tc, a)).toList(); - return specifiedStates(tc, call.getExecutable(), names).filter(to -> !to.isEmpty()).map(to -> to.get(0)); + if (call instanceof CtNewClass || call.getExecutable().getDeclaringType() == null) + return Optional.empty(); // an anonymous class body may change the state + List> values = call.getArguments().stream().map(a -> callArgumentValue(tc, a)).toList(); + return specifiedStates(tc, call.getExecutable(), values, + call.getExecutable().getDeclaringType().getQualifiedName()).filter(to -> !to.isEmpty()) + .map(to -> to.get(0)); } /** - * The to-states of the specified constructor that {@code exe} ends up running, with each of its parameters renamed - * to how a state can refer to the value passed for it. Empty if no specified constructor is known, or if a state - * mentions a parameter whose value cannot be named. + * The to-states of the specified constructor that {@code exe} ends up running, with each of its parameters replaced + * by the value passed for it, and the default value for each state set of {@code constructed} that they leave + * unconstrained. Empty if no specified constructor is known, or if a state mentions a parameter whose value cannot + * be written. * - * @param argumentNames - * how a state can refer to each argument of the call to {@code exe} + * @param argumentValues + * how a state can write each argument of the call to {@code exe} */ private static Optional> specifiedStates(TypeChecker tc, CtExecutableReference exe, - List> argumentNames) { - if (exe.getDeclaringType() == null || argumentNames.size() != exe.getParameters().size()) + List> argumentValues, String constructed) { + if (exe.getDeclaringType() == null || argumentValues.size() != exe.getParameters().size()) return Optional.empty(); // e.g. a varargs call Optional spec = specifiedConstructor(tc, exe); if (spec.isEmpty() || spec.get().function().getToStates().isEmpty()) return Optional.empty(); - // rename each spec parameter to the value passed for it; a state may not mention an unnamed one - Map rename = new HashMap<>(); - Set unnamed = new HashSet<>(); + // replace each spec parameter by the value passed for it; a state may not mention one without a value + Map values = new HashMap<>(); + Set unknown = new HashSet<>(); List params = spec.get().function().getArguments(); for (int i = 0; i < params.size(); i++) { String param = params.get(i).getName(); ConstructorDelegation.Argument passed = spec.get().arguments().get(i); - Optional name = passed instanceof ConstructorDelegation.Parameter p ? argumentNames.get(p.index()) - : ((ConstructorDelegation.Constant) passed).value(); - name.ifPresentOrElse(n -> rename.put(param, n), () -> unnamed.add(param)); + Optional value = passed instanceof ConstructorDelegation.Parameter p + ? argumentValues.get(p.index()) + : ((ConstructorDelegation.Constant) passed).value().flatMap(AuxStateHandler::literal); + value.ifPresentOrElse(v -> values.put(param, v), () -> unknown.add(param)); } List states = spec.get().function().getToStates(); - if (states.stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unnamed::contains))) + if (states.stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unknown::contains))) return Optional.empty(); - return Optional.of(states.stream().map(to -> rename.entrySet().stream().reduce(to, - (p, r) -> p.substituteVariable(r.getKey(), r.getValue()), (p, q) -> p)).toList()); + return Optional.of(states.stream() + .map(to -> values.entrySet().stream().reduce(to, + (p, v) -> p.substituteVariable(v.getKey(), v.getValue()), (p, q) -> p)) + .map(to -> withDefaultsForOtherSets(tc, constructed, to)).toList()); } - /** How a state can refer to {@code arg}: by the caller's parameter name or a non-string literal's value. */ - private static Optional argumentName(CtExpression arg) { + /** + * {@code to} and the default value of each state set of {@code klass} it does not mention: an ancestor's + * constructor spec says nothing about the sets a subclass adds (e.g. {@code Stack}'s, after {@code Vector()}). + */ + private static Predicate withDefaultsForOtherSets(TypeChecker tc, String klass, Predicate to) { + return Predicate.createConjunction(to, + defaultValues(unmentionedSets(tc, klass, to), Predicate.createVar(Keys.THIS))); + } + + /** How a state can write {@code arg}: by the caller's parameter name or a literal. */ + private static Optional argumentValue(CtExpression arg) { if (arg instanceof CtVariableRead vr && vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference) - return Optional.of(vr.getVariable().getSimpleName()); - return literalName(arg); + return Optional.of(Predicate.createVar(vr.getVariable().getSimpleName())); + return arg instanceof CtLiteral lit ? literal(lit.getValue()) : Optional.empty(); } - /** How a state can refer to {@code arg} at a call: by the local variable's current instance or a literal. */ - private static Optional callArgumentName(TypeChecker tc, CtExpression arg) { - if (arg instanceof CtVariableRead vr && !(arg instanceof CtFieldRead)) - return tc.getContext().getLastVariableInstance(vr.getVariable().getSimpleName()).map(Refined::getName); - return literalName(arg); + /** How a state can write {@code arg} at a call: by the variable's current instance (as for calls) or a literal. */ + private static Optional callArgumentValue(TypeChecker tc, CtExpression arg) { + if (arg instanceof CtVariableRead vr && !(arg instanceof CtFieldRead)) { + String name = vr.getVariable().getSimpleName(); + return Optional.of(Predicate + .createVar(tc.getContext().getLastVariableInstance(name).map(Refined::getName).orElse(name))); + } + return arg instanceof CtLiteral lit ? literal(lit.getValue()) : Optional.empty(); } - private static Optional literalName(CtExpression arg) { - if (arg instanceof CtLiteral lit && lit.getValue() != null && !(lit.getValue() instanceof String)) - return Optional.of(lit.getValue().toString()); + /** {@code value} as a literal of the refinement language, for booleans and whole numbers. */ + private static Optional literal(Object value) { + if (value instanceof Boolean) + return Optional.of(Predicate.createLit(value.toString(), Types.BOOLEAN)); + if (value instanceof Integer || value instanceof Short || value instanceof Byte) + return Optional.of(Predicate.createLit(value.toString(), Types.INT)); + if (value instanceof Long) + return Optional.of(Predicate.createLit(value.toString(), Types.LONG)); return Optional.empty(); } @@ -257,8 +300,12 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { } public static Predicate getDefaultState(TypeChecker tc, String klass, Predicate target) { + return defaultValues(getDifferentSets(tc, klass), target); + } + + /** Each of {@code sets} at its default value on {@code target}. */ + private static Predicate defaultValues(List sets, Predicate target) { Predicate c = new Predicate(); - List sets = getDifferentSets(tc, klass); for (GhostFunction sg : sets) { String retType = sg.getReturnType().toString(); Predicate typePredicate = switch (retType) { @@ -420,6 +467,11 @@ private static Predicate createStatePredicate(Predicate p, String value, String * @return the updated predicate */ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) { + return addOldStates(p, Predicate.createVar(Keys.THIS), unmentionedSets(tc, t, p)); + } + + /** The ghost state sets of class {@code t} that {@code p} does not mention. */ + private static List unmentionedSets(TypeChecker tc, String t, Predicate p) { List gs = p.getStateInvocations(getGhostStatesFor(t, tc)); List sets = getDifferentSets(tc, t); for (GhostState g : gs) { @@ -429,7 +481,7 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) sets.remove(g.getParent()); } } - return addOldStates(p, Predicate.createVar(Keys.THIS), sets); + return sets; } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java index c8c83a7d..1b46a1b4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java @@ -32,7 +32,8 @@ * * Anything else (field writes, method calls, this(...), branches) is not a delegation. Classes are read from the JDK * only: the verifier runs without the analyzed program's classpath, and the verifier's own libraries may differ from - * the versions the program uses. + * the versions the program uses. The result therefore depends on the JDK the verifier runs on, which may not be the one + * the program is compiled against. * * @param superclass * qualified name of the superclass whose constructor is called @@ -52,19 +53,23 @@ public record Parameter(int index) implements Argument { } /** - * A constant, with how a state can refer to it ({@code 0}, {@code true}); empty when it cannot (e.g. {@code null}). + * A constant, with its value when a state can refer to it (an {@link Integer} or a {@link Boolean}, by the type of + * the parameter it is passed for); empty when it cannot (e.g. {@code null}, a string). */ - public record Constant(Optional value) implements Argument { + public record Constant(Optional value) implements Argument { } - private static final Map> CACHE = new ConcurrentHashMap<>(); + private record Key(String className, List parameterTypes) { + } + + private static final Map> CACHE = new ConcurrentHashMap<>(); /** * How the constructor of {@code className} with these parameter types delegates to a superclass constructor, if its * bytecode is available and has exactly that shape. */ public static Optional of(String className, List parameterTypes) { - return CACHE.computeIfAbsent(className + parameterTypes, k -> read(className, parameterTypes)); + return CACHE.computeIfAbsent(new Key(className, parameterTypes), k -> read(className, parameterTypes)); } private static Optional read(String className, List parameterTypes) { @@ -73,6 +78,8 @@ private static Optional read(String className, List") + if (!name.equals("") || !Arrays.stream(params).map(Type::getClassName).toList().equals(parameterTypes)) return null; matcher = new DelegationMatcher(superclass, params); @@ -182,8 +189,8 @@ public void visitIntInsn(int opcode, int operand) { /** An int constant: a boolean, a number, or a char a state cannot write, depending on the parameter. */ private void pushInt(int value) { push(t -> new Constant(switch (t.getSort()) { - case Type.BOOLEAN -> Optional.of(Boolean.toString(value != 0)); - case Type.INT, Type.SHORT, Type.BYTE -> Optional.of(Integer.toString(value)); + case Type.BOOLEAN -> Optional.of(value != 0); + case Type.INT, Type.SHORT, Type.BYTE -> Optional.of(value); default -> Optional.empty(); })); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 1bac14c9..2e9e8c79 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -178,6 +178,11 @@ public Predicate substituteVariable(String from, String to) { return new Predicate(ec); } + /** Replaces the variable {@code from} with the expression {@code to} (e.g. a literal). */ + public Predicate substituteVariable(String from, Predicate to) { + return new Predicate(exp.clone().substitute(new Var(from), to.getExpression().clone())); + } + public List getVariableNames() { List l = new ArrayList<>(); exp.getVariableNames(l); diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java index ca33a52b..ed0ef409 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java @@ -39,13 +39,19 @@ void passesAParameterAndAConstant() { } @Test - void namesBooleanAndIntConstantsBySuperParameterType() { - // ReferenceHandler(ThreadGroup g, String name) { super(g, null, name, 0, false); } - Optional d = ConstructorDelegation.of("java.lang.ref.Reference$ReferenceHandler", - List.of("java.lang.ThreadGroup", "java.lang.String")); - assertTrue(d.isPresent()); - assertEquals(List.of(new Parameter(0), UNNAMED, new Parameter(1), UNNAMED, new Constant(Optional.of("false"))), - d.get().arguments()); + void typesIntConstantsBySuperParameterType() { + // LinkedHashSet() { super(16, .75f, true); } + assertEquals( + Optional.of(new ConstructorDelegation("java.util.HashSet", List.of("int", "float", "boolean"), + List.of(new Constant(Optional.of(16)), UNNAMED, new Constant(Optional.of(true))))), + ConstructorDelegation.of("java.util.LinkedHashSet", List.of())); + } + + @Test + void passesAParameterAmongConstants() { + // LinkedHashSet(int initialCapacity) { super(initialCapacity, .75f, true); } + assertEquals(List.of(new Parameter(0), UNNAMED, new Constant(Optional.of(true))), + ConstructorDelegation.of("java.util.LinkedHashSet", List.of("int")).orElseThrow().arguments()); } @Test From a1749dbd118f39589a68a3cd52f4e03572f5630f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 21:23:40 +0000 Subject: [PATCH 4/6] Check the state found after a delegating JDK constructor The test suite only checks where errors are reported, and main reports the same lines of throwable_jdk_subclass_error with an unknown state. Assert that the state found is withThrowable. Co-Authored-By: Claude Opus 5.5 --- .../tests/TestDelegatedConstructorStates.java | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java new file mode 100644 index 00000000..f05645d6 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java @@ -0,0 +1,38 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.StateRefinementError; + +/** + * The test suite only checks where errors are reported. These check the state found there: a JDK constructor that + * delegates to a specified one gets that spec's state, not an unknown one. + */ +class TestDelegatedConstructorStates { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + private static final List> WITH_CAUSE = List.of(List.of("withThrowable")); + + @Test + void delegatingJdkConstructorsGiveTheSpecifiedState() { + Map>> found = foundStatesByLine("classes/throwable_jdk_subclass_error"); + assertEquals(WITH_CAUSE, found.get(10)); // new ClassNotFoundException() + assertEquals(WITH_CAUSE, found.get(16)); // new RuntimeException(message, cause) + assertEquals(WITH_CAUSE, found.get(23)); // subclass calling ClassNotFoundException(String) + assertNotEquals(WITH_CAUSE, found.get(31)); // MissingResourceException: not delegating, default state + } + + private static Map>> foundStatesByLine(String test) { + CommandLineLauncher.launch(TEST_SUITE + test); + return Diagnostics.getInstance().getErrors().stream().map(e -> assertInstanceOf(StateRefinementError.class, e)) + .collect(Collectors.toMap(e -> e.getPosition().getLine(), e -> e.getContext().possibleStates())); + } +} From 69a62e854027e65f4ac4063f34a942cc2b64c288 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 21:47:04 +0000 Subject: [PATCH 5/6] Use only known argument values in delegated constructor states - A variable passed to new is referred to only through its current instance. Its raw name made the state follow a later assignment (new PrinterStateReasons(n); n = 5;), and a lambda parameter reached Z3 with the wrong sort; with no instance the value is unknown and the walk stops. - Skip a spec whose to-state mentions old(this) (it leaves another state set unchanged): a new object has no old state, and the delegated call failed with "Ghost 'old' could not be found". - Literals: booleans and ints only; extract the shared CtLiteral case. Co-Authored-By: Claude Opus 5.5 --- .../HashMapRefinements.java | 15 ++++++++ .../Test.java | 34 +++++++++++++++++++ .../HashMapRefinements.java | 16 +++++++++ .../Test.java | 12 +++++++ .../object_checkers/AuxStateHandler.java | 27 +++++++++------ .../liquidjava/rj_language/Predicate.java | 7 ++++ 6 files changed, 101 insertions(+), 10 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java new file mode 100644 index 00000000..9f6a9239 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.delegated_argument_reassigned_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.HashMap") +@Ghost("int capacity") +public interface HashMapRefinements { + @StateRefinement(to = "capacity(this) == initialCapacity") + void HashMap(int initialCapacity); + + @StateRefinement(from = "capacity(this) == 5") + V get(Object key); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java new file mode 100644 index 00000000..b34ece26 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java @@ -0,0 +1,34 @@ +package testSuite.classes.delegated_argument_reassigned_error; + +import java.util.function.IntFunction; +import javax.print.attribute.standard.PrinterStateReasons; + +// PrinterStateReasons(int) runs HashMap(int): the capacity is the argument's value at the call, not a later one +public class Test { + static void assignedBefore(int n) { + n = 5; + PrinterStateReasons r = new PrinterStateReasons(n); + r.get("k"); + } + + static void assignedAfter(int n) { + PrinterStateReasons r = new PrinterStateReasons(n); + n = 5; + r.get("k"); // Expect: State Refinement Error + } + + static void assignedBeforeAndAfter(int n) { + n = 6; + PrinterStateReasons r = new PrinterStateReasons(n); + n = 5; + r.get("k"); // Expect: State Refinement Error + } + + static IntFunction lambdaParameter() { + return k -> { + PrinterStateReasons r = new PrinterStateReasons(k); + r.get("k"); // Expect: State Refinement Error + return r; + }; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java new file mode 100644 index 00000000..b3e63107 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java @@ -0,0 +1,16 @@ +package testSuite.classes.delegated_spec_keeping_other_sets_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.HashMap") +@StateSet({ "a1", "a2" }) +@StateSet({ "b1", "b2" }) +public interface HashMapRefinements { + @StateRefinement(to = "a2(this)") + void HashMap(int initialCapacity); + + @StateRefinement(from = "b1(this)") + V get(Object key); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java new file mode 100644 index 00000000..7b26e257 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java @@ -0,0 +1,12 @@ +package testSuite.classes.delegated_spec_keeping_other_sets_correct; + +import javax.print.attribute.standard.PrinterStateReasons; + +// HashMap(int)'s spec leaves the b set unchanged, which refers to the old object: a new object has none, so the +// delegated call gets the default state (b1) instead of that spec +public class Test { + static void get() { + PrinterStateReasons r = new PrinterStateReasons(5); + r.get("k"); + } +} 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 804a24e8..ca35028f 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 @@ -147,6 +147,9 @@ private static Optional> specifiedStates(TypeChecker tc, CtExecu List states = spec.get().function().getToStates(); if (states.stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unknown::contains))) return Optional.empty(); + // a spec that leaves some state sets unchanged refers to old(this), which a new object does not have + if (states.stream().anyMatch(to -> to.invokes(Keys.OLD))) + return Optional.empty(); return Optional.of(states.stream() .map(to -> values.entrySet().stream().reduce(to, (p, v) -> p.substituteVariable(v.getKey(), v.getValue()), (p, q) -> p)) @@ -167,27 +170,31 @@ private static Optional argumentValue(CtExpression arg) { if (arg instanceof CtVariableRead vr && vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference) return Optional.of(Predicate.createVar(vr.getVariable().getSimpleName())); - return arg instanceof CtLiteral lit ? literal(lit.getValue()) : Optional.empty(); + return literalValue(arg); } - /** How a state can write {@code arg} at a call: by the variable's current instance (as for calls) or a literal. */ + /** + * How a state can write {@code arg} at a call: by the variable's current instance, which keeps the value it has now + * even if the variable is assigned later, or a literal. A variable without an instance (e.g. a parameter not + * assigned yet) has no known value here. + */ private static Optional callArgumentValue(TypeChecker tc, CtExpression arg) { - if (arg instanceof CtVariableRead vr && !(arg instanceof CtFieldRead)) { - String name = vr.getVariable().getSimpleName(); - return Optional.of(Predicate - .createVar(tc.getContext().getLastVariableInstance(name).map(Refined::getName).orElse(name))); - } + if (arg instanceof CtVariableRead vr && !(arg instanceof CtFieldRead)) + return tc.getContext().getLastVariableInstance(vr.getVariable().getSimpleName()) + .map(vi -> Predicate.createVar(vi.getName())); + return literalValue(arg); + } + + /** {@code arg} as a literal of the refinement language, if it is a boolean or int literal. */ + private static Optional literalValue(CtExpression arg) { return arg instanceof CtLiteral lit ? literal(lit.getValue()) : Optional.empty(); } - /** {@code value} as a literal of the refinement language, for booleans and whole numbers. */ private static Optional literal(Object value) { if (value instanceof Boolean) return Optional.of(Predicate.createLit(value.toString(), Types.BOOLEAN)); if (value instanceof Integer || value instanceof Short || value instanceof Byte) return Optional.of(Predicate.createLit(value.toString(), Types.INT)); - if (value instanceof Long) - return Optional.of(Predicate.createLit(value.toString(), Types.LONG)); return Optional.empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 2e9e8c79..0dfc158f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -183,6 +183,13 @@ public Predicate substituteVariable(String from, Predicate to) { return new Predicate(exp.clone().substitute(new Var(from), to.getExpression().clone())); } + /** Whether the function {@code name} is called anywhere in this predicate. */ + public boolean invokes(String name) { + List found = new ArrayList<>(); + exp.getStateInvocations(found, List.of(name)); + return !found.isEmpty(); + } + public List getVariableNames() { List l = new ArrayList<>(); exp.getVariableNames(l); From 4c8da0172452f04b712d0878866a6d27d6365bc8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 29 Oct 2026 10:49:26 +0000 Subject: [PATCH 6/6] Replace a super constructor's parameters by their arguments at once With Sub(boolean y, boolean x) { super(y, x); } for Base(boolean x, boolean y), replacing x by y and then y by x turned both into x, so a state that mentions both parameters was wrong. Co-Authored-By: Claude Opus 5.5 --- .../super_swapped_arguments_correct/Base.java | 13 ++++++++++++ .../super_swapped_arguments_correct/Sub.java | 14 +++++++++++++ .../super_swapped_arguments_error/Base.java | 13 ++++++++++++ .../super_swapped_arguments_error/Sub.java | 14 +++++++++++++ .../object_checkers/AuxStateHandler.java | 20 ++++++++++++++++--- 5 files changed, 71 insertions(+), 3 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java new file mode 100644 index 00000000..c1101d4b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java @@ -0,0 +1,13 @@ +package testSuite.classes.super_swapped_arguments_correct; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class Base { + @StateRefinement(to = "(x && !y && open(this)) || (!(x && !y) && closed(this))") + public Base(boolean x, boolean y) {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java new file mode 100644 index 00000000..b134e0ec --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java @@ -0,0 +1,14 @@ +package testSuite.classes.super_swapped_arguments_correct; + +// The parameters of Sub are named like those of Base, in the other order: each Base parameter is replaced by the Sub +// parameter passed for it, all at once, so a name is not replaced twice +public class Sub extends Base { + public Sub(boolean y, boolean x) { + super(y, x); + } + + static void test() { + Sub s = new Sub(true, false); // Base(true, false): open + s.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java new file mode 100644 index 00000000..c054560c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java @@ -0,0 +1,13 @@ +package testSuite.classes.super_swapped_arguments_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class Base { + @StateRefinement(to = "(x && !y && open(this)) || (!(x && !y) && closed(this))") + public Base(boolean x, boolean y) {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java new file mode 100644 index 00000000..9d654f14 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java @@ -0,0 +1,14 @@ +package testSuite.classes.super_swapped_arguments_error; + +// The parameters of Sub are named like those of Base, in the other order: each Base parameter is replaced by the Sub +// parameter passed for it, all at once, so a name is not replaced twice +public class Sub extends Base { + public Sub(boolean y, boolean x) { + super(y, x); + } + + static void test() { + Sub s = new Sub(false, true); // Base(false, true): closed + s.close(); // Expect: State Refinement Error + } +} 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 ca35028f..5b951912 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 @@ -150,12 +150,26 @@ private static Optional> specifiedStates(TypeChecker tc, CtExecu // a spec that leaves some state sets unchanged refers to old(this), which a new object does not have if (states.stream().anyMatch(to -> to.invokes(Keys.OLD))) return Optional.empty(); - return Optional.of(states.stream() - .map(to -> values.entrySet().stream().reduce(to, - (p, v) -> p.substituteVariable(v.getKey(), v.getValue()), (p, q) -> p)) + return Optional.of(states.stream().map(to -> substituteAll(to, values)) .map(to -> withDefaultsForOtherSets(tc, constructed, to)).toList()); } + /** + * Replaces each variable of {@code values} at once, so a value that is also a name in {@code values} is not + * replaced again (e.g. {@code Sub(boolean y, boolean x) { super(y, x); }} for {@code Base(boolean x, boolean y)}). + */ + private static Predicate substituteAll(Predicate p, Map values) { + Map placeholders = new HashMap<>(); + for (String name : values.keySet()) { + String placeholder = "#param_" + placeholders.size(); + placeholders.put(name, placeholder); + p = p.substituteVariable(name, placeholder); + } + for (Map.Entry e : placeholders.entrySet()) + p = p.substituteVariable(e.getValue(), values.get(e.getKey())); + return p; + } + /** * {@code to} and the default value of each state set of {@code klass} it does not mention: an ancestor's * constructor spec says nothing about the sets a subclass adds (e.g. {@code Stack}'s, after {@code Vector()}).