From 92d1b94e715c8b940770dd1a590516541820ef5c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Sat, 17 Oct 2026 10:32:53 +0100 Subject: [PATCH] Check calls on a constructor call whose constructor has refined parameters A call made directly on new T(args), when T(args) has refined parameters, used the constructor's return-value instance (typed void) as its receiver, so the state ghost was applied to a void argument and verification failed with an Argument Mismatch Error. Check the constructor-call receiver before the TARGET metadata and reuse it across the invocation's checks. Co-Authored-By: Claude Opus 5.5 --- ...ectConstructorReceiverRefinedArgument.java | 23 +++++++++++++++++++ ...rorConstructorReceiverRefinedArgument.java | 23 +++++++++++++++++++ .../object_checkers/AuxStateHandler.java | 22 +++++++++++------- .../java/liquidjava/utils/constants/Keys.java | 1 + 4 files changed, 61 insertions(+), 8 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiverRefinedArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiverRefinedArgument.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiverRefinedArgument.java b/liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiverRefinedArgument.java new file mode 100644 index 000000000..6545695fe --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiverRefinedArgument.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"unbound", "bound"}) +class CorrectRefinedArgListener { + @StateRefinement(to = "unbound(this)") + public CorrectRefinedArgListener() {} + + @StateRefinement(to = "bound(this)") + public CorrectRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {} + + @StateRefinement(from = "bound(this)") + public void accept() {} +} + +public class CorrectConstructorReceiverRefinedArgument { + static void chained() { + new CorrectRefinedArgListener(8080).accept(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiverRefinedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiverRefinedArgument.java new file mode 100644 index 000000000..a57844362 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiverRefinedArgument.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"unbound", "bound"}) +class ErrorRefinedArgListener { + @StateRefinement(to = "unbound(this)") + public ErrorRefinedArgListener() {} + + @StateRefinement(to = "bound(this)") + public ErrorRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {} + + @StateRefinement(from = "unbound(this)", to = "bound(this)") + public void bind() {} +} + +public class ErrorConstructorReceiverRefinedArgument { + static void chained() { + new ErrorRefinedArgListener(8080).bind(); // 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 4ad7852f3..a795f2ea9 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 @@ -744,24 +744,30 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, } return name; - } else if (target2.getMetadata(Keys.TARGET) != null) { - // invocation is in - // who did put the metadata here then? - VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET); - Optional v = target2Vi.getParent(); - invocation.putMetadata(Keys.TARGET, target2Vi); - return v.map(Refined::getName).orElse(target2Vi.getName()); + } else if (target2 instanceof CtConstructorCall newCall + && newCall.getMetadata(Keys.RECEIVER)instanceof RefinedVariable receiver) { + invocation.putMetadata(Keys.TARGET, receiver); + return receiver.getName(); } else if (target2 instanceof CtConstructorCall newCall && newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) { - // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives + // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Checked + // before the TARGET metadata, which a constructor with refined parameters sets to its (void) return value String name = String.format(Formats.FRESH, tc.getContext().getCounter()); CtTypeReference type = newCall.getType(); RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type, state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall); receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); newCall.putMetadata(Keys.TARGET, receiver); + newCall.putMetadata(Keys.RECEIVER, receiver); invocation.putMetadata(Keys.TARGET, receiver); return name; + } else if (target2.getMetadata(Keys.TARGET) != null) { + // invocation is in + // who did put the metadata here then? + VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET); + Optional v = target2Vi.getParent(); + invocation.putMetadata(Keys.TARGET, target2Vi); + return v.map(Refined::getName).orElse(target2Vi.getName()); } return null; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index 0f6cd964f..d41b7c068 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -4,6 +4,7 @@ public final class Keys { public static final String REFINEMENT = "refinement"; public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check"; public static final String TARGET = "target"; + public static final String RECEIVER = "receiver"; public static final String RETURN_VAR_NAME = "return_var_name"; public static final String THIS = "this"; public static final String WILDCARD = "_";