From 918f7771bf999086f2e34da83b438bf2e65657a1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 2 Oct 2026 18:21:31 +0100 Subject: [PATCH 1/7] Preserve refinement on forward declared field reads (fix #316) --- .../forward_field_read_correct/ReadBefore.java | 17 +++++++++++++++++ .../RefinementTypeChecker.java | 4 ++++ 2 files changed, 21 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java new file mode 100644 index 000000000..4f7190cff --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java @@ -0,0 +1,17 @@ +package testSuite.classes.forward_field_read_correct; + +import liquidjava.specification.Refinement; + +public class ReadBefore { + private final Job job = new Job(); + + @Refinement("_ >= 0") + public int get() { + return job.port; + } + + static class Job { + @Refinement("_ >= 0") + int port; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index bf6dcc999..564759170 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -308,6 +308,10 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral))); } else if (tryStaticFinalConstantRefinement(fieldRead)) { // refinement metadata set by helper + } else if (fieldRead.getVariable().getDeclaration() != null) { + Predicate declared = getRefinementFromAnnotation(fieldRead.getVariable().getDeclaration()) + .orElseGet(Predicate::new); + fieldRead.putMetadata(Keys.REFINEMENT, declared.substituteVariable(fieldName, Keys.WILDCARD)); } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE? From 26bc7045ca65c78f89c7426811bd2da538400ee6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 2 Oct 2026 18:22:31 +0100 Subject: [PATCH 2/7] Preserve enclosing class refinements across nested classes --- .../CorrectOuterFieldAfterNestedClass.java | 12 ++++ .../java/testSuite/ErrorNestedFieldLeak.java | 14 +++++ .../liquidjava/processor/context/Context.java | 21 +++++++ .../MethodsFirstChecker.java | 62 ++++++++++--------- .../RefinementTypeChecker.java | 7 +-- 5 files changed, 83 insertions(+), 33 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java b/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java new file mode 100644 index 000000000..7c994eb20 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class CorrectOuterFieldAfterNestedClass { + @Refinement("_ > 0") int x = 1; + + static class Inner { int y; } + + @Refinement("_ > 0") + public int get() { return x; } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java b/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java new file mode 100644 index 000000000..3ff32b16e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class ErrorNestedFieldLeak { + int x = 1; + + static class Inner { + @Refinement("_ < 0") int x = -1; + } + + @Refinement("_ < 0") + public int get() { return x; } // Expect: Refinement Error +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 298179e60..b1d30f5fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -47,6 +47,27 @@ public void reinitializeContext() { clearInstanceVariables(); } + public ClassScope enterClassScope() { + ClassScope scope = new ClassScope(ctxVars, ctxInstanceVars); + reinitializeContext(); + return scope; + } + + public void exitClassScope(ClassScope scope) { + ctxVars = scope.variables; + ctxInstanceVars = scope.instances; + } + + public static class ClassScope { + private final Stack> variables; + private final List instances; + + private ClassScope(Stack> variables, List instances) { + this.variables = variables; + this.instances = instances; + } + } + public void clearInstanceVariables() { ctxInstanceVars = new ArrayList<>(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 3dda3881b..fcfdea182 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -32,41 +32,45 @@ public MethodsFirstChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - context.reinitializeContext(); if (visitedClasses.contains(ctClass.getQualifiedName())) return; else visitedClasses.add(ctClass.getQualifiedName()); - // visitInterfaces - if (!ctClass.getSuperInterfaces().isEmpty()) - for (CtTypeReference t : ctClass.getSuperInterfaces()) { - if (t.isInterface()) { - CtType ct = t.getDeclaration(); - if (ct instanceof CtInterface) - visitCtInterface((CtInterface) ct); + Context.ClassScope scope = context.enterClassScope(); + try { + // visitInterfaces + if (!ctClass.getSuperInterfaces().isEmpty()) + for (CtTypeReference t : ctClass.getSuperInterfaces()) { + if (t.isInterface()) { + CtType ct = t.getDeclaration(); + if (ct instanceof CtInterface) + visitCtInterface((CtInterface) ct); + } } + // visitSubclasses + CtTypeReference sup = ctClass.getSuperclass(); + if (sup != null && sup.isClass()) { + CtType ct = sup.getDeclaration(); + if (ct instanceof CtClass) + visitCtClass((CtClass) ct); } - // visitSubclasses - CtTypeReference sup = ctClass.getSuperclass(); - if (sup != null && sup.isClass()) { - CtType ct = sup.getDeclaration(); - if (ct instanceof CtClass) - visitCtClass((CtClass) ct); - } - // first try-catch: process class-level annotations) - // errors here should not prevent visiting methods, constructors or fields of the class - try { - getRefinementFromAnnotation(ctClass); - handleStateSetsFromAnnotation(ctClass); - } catch (LJError e) { - diagnostics.add(e); - } - // second try-catch: visit class children (methods, constructors, fields) - // errors from one child should not prevent visiting sibling elements - try { - super.visitCtClass(ctClass); - } catch (LJError e) { - diagnostics.add(e); + // first try-catch: process class-level annotations) + // errors here should not prevent visiting methods, constructors or fields of the class + try { + getRefinementFromAnnotation(ctClass); + handleStateSetsFromAnnotation(ctClass); + } catch (LJError e) { + diagnostics.add(e); + } + // second try-catch: visit class children (methods, constructors, fields) + // errors from one child should not prevent visiting sibling elements + try { + super.visitCtClass(ctClass); + } catch (LJError e) { + diagnostics.add(e); + } + } finally { + context.exitClassScope(scope); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 564759170..4ec745b27 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -74,15 +74,14 @@ public RefinementTypeChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - // System.out.println("CTCLASS:"+ctClass.getSimpleName()); - context.reinitializeContext(); - + Context.ClassScope scope = context.enterClassScope(); try { super.visitCtClass(ctClass); } catch (LJError e) { diagnostics.add(e); + } finally { + context.exitClassScope(scope); } - } @Override From 4cf66173616acd97c211a8b41a387c07aad7d901 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 2 Oct 2026 18:24:34 +0100 Subject: [PATCH 3/7] Qualify field context keys by declaring type --- .../testSuite/CorrectDistinctClassFields.java | 16 ++++++++++++++++ .../RefinementTypeChecker.java | 9 +++++---- .../general_checkers/OperationsChecker.java | 13 +++++++------ .../object_checkers/AuxStateHandler.java | 5 +++-- .../java/liquidjava/utils/FieldNames.java | 19 +++++++++++++++++++ 5 files changed, 50 insertions(+), 12 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java b/liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java new file mode 100644 index 000000000..a41810cb5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectDistinctClassFields { + @Refinement("_ < 0") int port = -1; + private final Job job = new Job(); + + public void send() { + job.port = 5; + } + + static class Job { + @Refinement("_ >= 0") int port; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 4ec745b27..58250c422 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -15,6 +15,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Enum; import liquidjava.utils.StaticConstants; +import liquidjava.utils.FieldNames; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; @@ -220,7 +221,7 @@ private void visitAssignment(CtAssignment assignment) thr } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); + String updatedVarName = FieldNames.of(cr); checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); // corresponding ghost function update @@ -261,7 +262,7 @@ public void visitCtLiteral(CtLiteral lit) { public void visitCtField(CtField f) { super.visitCtField(f); Optional c = getRefinementFromAnnotation(f); - String name = String.format(Formats.THIS, f.getSimpleName()); + String name = FieldNames.of(f.getReference()); Predicate ret = new Predicate(); if (c.isPresent()) { ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); @@ -291,8 +292,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); } - } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { - String thisName = String.format(Formats.THIS, fieldName); + } else if (context.hasVariable(FieldNames.of(fieldRead.getVariable()))) { + String thisName = FieldNames.of(fieldRead.getVariable()); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 550d67817..831aeb0d0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -10,6 +10,7 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.context.VariableInstance; import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.utils.FieldNames; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Ops; @@ -125,8 +126,8 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro Predicate all; if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); - if (w instanceof CtFieldWrite) - name = String.format(Formats.THIS, name); + if (w instanceof CtFieldWrite fieldWrite) + name = FieldNames.of(fieldWrite.getVariable()); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; @@ -203,8 +204,8 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab if (element instanceof CtVariableRead elemVar) { String elemName = elemVar.getVariable().getSimpleName(); - if (elemVar instanceof CtFieldRead) - elemName = String.format(Formats.THIS, elemName); + if (elemVar instanceof CtFieldRead fieldRead) + elemName = FieldNames.of(fieldRead.getVariable()); Predicate elemRef = rtc.getContext().getVariableRefinements(elemName); String returnName = elemName; @@ -336,8 +337,8 @@ private Predicate getCurrentVariableValue(String name) { private Predicate getOperatorAssignmentRefinement(CtExpression element) throws LJError { if (element instanceof CtVariableRead variableRead) { String name = variableRead.getVariable().getSimpleName(); - if (variableRead instanceof CtFieldRead) - name = String.format(Formats.THIS, name); + if (variableRead instanceof CtFieldRead fieldRead) + name = FieldNames.of(fieldRead.getVariable()); return getCurrentVariableValue(name); } else if (element instanceof CtBinaryOperator binaryOperator) { Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand()); 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 4ed8fcae0..4f6572409 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 @@ -11,6 +11,7 @@ import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; import liquidjava.rj_language.Predicate; +import liquidjava.utils.FieldNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -392,7 +393,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre */ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws LJError { CtField field = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName()); + String updatedVarName = FieldNames.of(fw.getVariable()); String targetClass = field.getDeclaringType().getQualifiedName(); // state transition annotation construction @@ -604,7 +605,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, // means invocation is in a form of `t.method(args)` String name = v.getVariable().getSimpleName(); if (target2 instanceof CtFieldRead fieldRead && fieldRead.getTarget() instanceof CtThisAccess) { - String fieldName = String.format(Formats.THIS, name); + String fieldName = FieldNames.of(fieldRead.getVariable()); if (tc.getContext().hasVariable(fieldName)) name = fieldName; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java b/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java new file mode 100644 index 000000000..798f1229a --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java @@ -0,0 +1,19 @@ +package liquidjava.utils; + +import spoon.reflect.reference.CtFieldReference; + +public final class FieldNames { + private FieldNames() { + } + + public static String of(CtFieldReference field) { + StringBuilder name = new StringBuilder("this#"); + field.getDeclaringType().getQualifiedName().codePoints().forEach(c -> { + if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z' || c >= '0' && c <= '9' || c == '_') + name.appendCodePoint(c); + else + name.append('#').append(Integer.toHexString(c)).append('#'); + }); + return name.append('#').append(field.getSimpleName()).toString(); + } +} From 8bb0b42e29f8c46ae107b8cf5d7817dd8cc5ea3e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 3 Oct 2026 11:41:55 +0100 Subject: [PATCH 4/7] Use readable qualified field names --- .../object_checkers/AuxStateHandler.java | 17 ++++++++++------- .../main/java/liquidjava/utils/FieldNames.java | 9 +-------- 2 files changed, 11 insertions(+), 15 deletions(-) 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 4f6572409..04e4b02d4 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 @@ -181,13 +181,13 @@ private static ObjectState getStates(CtAnnotation ctAnnota // has from if (from != null) { - state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix)); + state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false)); state.setFromPosition(Utils.getLJAnnotationPosition(e, from)); } // has to if (to != null) { - state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix)); + state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true)); state.setToPosition(Utils.getLJAnnotationPosition(e, to)); } @@ -210,10 +210,9 @@ private static ObjectState getStates(CtAnnotation ctAnnota * * @return the created predicate */ - private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e, - boolean isTo, String prefix) throws LJError { + private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc, + CtElement e, boolean isTo) throws LJError { SourcePosition position = Utils.getLJAnnotationPosition(e, value); - Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); @@ -422,8 +421,12 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L ObjectState stateChange = new ObjectState(); String prefix = field.getDeclaringType().getQualifiedName(); - Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix); - Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix); + Predicate fromPredicate = createStatePredicate(new Predicate(), stateChangeRefinementFrom, targetClass, tc, fw, + false); + Predicate toPredicate = Predicate.createEquals(Predicate + .createInvocation(Utils.qualifyName(prefix, field.getSimpleName()), Predicate.createVar(Keys.THIS)), + Predicate.createVar(updatedVarName)); + toPredicate = createStatePredicate(toPredicate, stateChangeRefinementTo, targetClass, tc, fw, true); stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java b/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java index 798f1229a..b75f57feb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java @@ -7,13 +7,6 @@ private FieldNames() { } public static String of(CtFieldReference field) { - StringBuilder name = new StringBuilder("this#"); - field.getDeclaringType().getQualifiedName().codePoints().forEach(c -> { - if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z' || c >= '0' && c <= '9' || c == '_') - name.appendCodePoint(c); - else - name.append('#').append(Integer.toHexString(c)).append('#'); - }); - return name.append('#').append(field.getSimpleName()).toString(); + return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); } } From f833effe19d34843663ae79827c421587ef3c4a7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 3 Oct 2026 11:48:48 +0100 Subject: [PATCH 5/7] Move field naming into Utils --- .../refinement_checker/RefinementTypeChecker.java | 10 +++++----- .../general_checkers/OperationsChecker.java | 8 ++++---- .../object_checkers/AuxStateHandler.java | 5 ++--- .../src/main/java/liquidjava/utils/FieldNames.java | 12 ------------ .../src/main/java/liquidjava/utils/Utils.java | 5 +++++ 5 files changed, 16 insertions(+), 24 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 58250c422..572349481 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -15,7 +15,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Enum; import liquidjava.utils.StaticConstants; -import liquidjava.utils.FieldNames; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; @@ -221,7 +221,7 @@ private void visitAssignment(CtAssignment assignment) thr } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = FieldNames.of(cr); + String updatedVarName = Utils.qualifyFieldName(cr); checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); // corresponding ghost function update @@ -262,7 +262,7 @@ public void visitCtLiteral(CtLiteral lit) { public void visitCtField(CtField f) { super.visitCtField(f); Optional c = getRefinementFromAnnotation(f); - String name = FieldNames.of(f.getReference()); + String name = Utils.qualifyFieldName(f.getReference()); Predicate ret = new Predicate(); if (c.isPresent()) { ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); @@ -292,8 +292,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); } - } else if (context.hasVariable(FieldNames.of(fieldRead.getVariable()))) { - String thisName = FieldNames.of(fieldRead.getVariable()); + } else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) { + String thisName = Utils.qualifyFieldName(fieldRead.getVariable()); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 831aeb0d0..c8641c6f9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -10,7 +10,7 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.context.VariableInstance; import liquidjava.processor.refinement_checker.TypeChecker; -import liquidjava.utils.FieldNames; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Ops; @@ -127,7 +127,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); if (w instanceof CtFieldWrite fieldWrite) - name = FieldNames.of(fieldWrite.getVariable()); + name = Utils.qualifyFieldName(fieldWrite.getVariable()); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; @@ -205,7 +205,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab if (element instanceof CtVariableRead elemVar) { String elemName = elemVar.getVariable().getSimpleName(); if (elemVar instanceof CtFieldRead fieldRead) - elemName = FieldNames.of(fieldRead.getVariable()); + elemName = Utils.qualifyFieldName(fieldRead.getVariable()); Predicate elemRef = rtc.getContext().getVariableRefinements(elemName); String returnName = elemName; @@ -338,7 +338,7 @@ private Predicate getOperatorAssignmentRefinement(CtExpression element) throw if (element instanceof CtVariableRead variableRead) { String name = variableRead.getVariable().getSimpleName(); if (variableRead instanceof CtFieldRead fieldRead) - name = FieldNames.of(fieldRead.getVariable()); + name = Utils.qualifyFieldName(fieldRead.getVariable()); return getCurrentVariableValue(name); } else if (element instanceof CtBinaryOperator binaryOperator) { Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand()); 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 04e4b02d4..03d14b807 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 @@ -11,7 +11,6 @@ import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; import liquidjava.rj_language.Predicate; -import liquidjava.utils.FieldNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -392,7 +391,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre */ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws LJError { CtField field = fw.getVariable().getDeclaration(); - String updatedVarName = FieldNames.of(fw.getVariable()); + String updatedVarName = Utils.qualifyFieldName(fw.getVariable()); String targetClass = field.getDeclaringType().getQualifiedName(); // state transition annotation construction @@ -608,7 +607,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, // means invocation is in a form of `t.method(args)` String name = v.getVariable().getSimpleName(); if (target2 instanceof CtFieldRead fieldRead && fieldRead.getTarget() instanceof CtThisAccess) { - String fieldName = FieldNames.of(fieldRead.getVariable()); + String fieldName = Utils.qualifyFieldName(fieldRead.getVariable()); if (tc.getContext().hasVariable(fieldName)) name = fieldName; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java b/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java deleted file mode 100644 index b75f57feb..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java +++ /dev/null @@ -1,12 +0,0 @@ -package liquidjava.utils; - -import spoon.reflect.reference.CtFieldReference; - -public final class FieldNames { - private FieldNames() { - } - - public static String of(CtFieldReference field) { - return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 38f6b2efb..6c1e1d60b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -19,6 +19,7 @@ import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtMethod; import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtFieldReference; import spoon.reflect.reference.CtTypeReference; import spoon.support.reflect.cu.position.SourcePositionImpl; @@ -50,6 +51,10 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } + public static String qualifyFieldName(CtFieldReference field) { + return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); + } + public static String getFile(CtElement element) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null) From 698cb08d4c399e57d22272531167daa330e1901f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 2 Oct 2026 18:25:02 +0100 Subject: [PATCH 6/7] Cover combined nested field refinements (test #315) --- .../CorrectCombinedNestedFields.java | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java b/liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java new file mode 100644 index 000000000..82c1fa7ae --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java @@ -0,0 +1,33 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectCombinedNestedFields { + @Refinement("_ < 0") + int port = -1; + + private final Job job = new Job(); + + static class Marker { + int value; + } + + @Refinement("_ < 0") + public int getOuterPort() { + return port; + } + + @Refinement("_ >= 0") + public int getJobPort() { + return job.port; + } + + public void send() { + job.port = 5; + } + + static class Job { + @Refinement("_ >= 0") + int port; + } +} From 2546a88e7858f332b03039b17d12fe06d0a25570 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 3 Oct 2026 11:43:16 +0100 Subject: [PATCH 7/7] Keep negative literal values self-contained across methods --- .../general_checkers/OperationsChecker.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index c8641c6f9..e547cdd05 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -18,6 +18,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.UnaryExpression; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -122,6 +123,13 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator @SuppressWarnings({ "unchecked" }) public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJError { CtExpression ex = (CtExpression) operator.getOperand(); + if (operator.getKind() == UnaryOperatorKind.NEG && ex instanceof CtLiteral literal + && literal.getValue() instanceof Number) { + Predicate operand = Predicate.createLit(literal.getValue().toString(), ex.getType().getQualifiedName()); + Predicate value = new Predicate(new UnaryExpression("-", operand.getExpression())); + operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), value)); + return; + } String name = Formats.FRESH; Predicate all; if (ex instanceof CtVariableWrite w) {