From bcbeb3c587bb53136eeca4386bec36a3f2e3a5ff Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 17:51:16 +0000 Subject: [PATCH 1/2] Register every ghost and state set before any spec is read Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/ErrorStateSetNames.java | 5 +++ .../Client.java | 11 +++++ .../FrameRefinements.java | 22 ++++++++++ .../processor/RefinementProcessor.java | 13 +++++- .../ExternalRefinementTypeChecker.java | 31 ++++++++++--- .../GhostsFirstChecker.java | 44 +++++++++++++++++++ .../MethodsFirstChecker.java | 2 - .../refinement_checker/TypeChecker.java | 11 ++--- 8 files changed, 124 insertions(+), 15 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/Client.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/FrameRefinements.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java index c38a69b1a..144922bc5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java @@ -1,6 +1,7 @@ package testSuite; import liquidjava.specification.Ghost; +import liquidjava.specification.RefinementPredicate; import liquidjava.specification.StateSet; // A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses @@ -18,3 +19,7 @@ class ErrorStateSetNameOfAGhost {} @StateSet(name = "door", value = {"closed", "opened"}) // Expect: Error @StateSet(name = "door", value = {"unlocked", "locked"}) class ErrorStateSetNameOfAnotherSet {} + +@StateSet(name = "size", value = {"empty", "full"}) // Expect: Error +@RefinementPredicate("int size(ErrorStateSetNameOfARefinementPredicate b)") +class ErrorStateSetNameOfARefinementPredicate {} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/Client.java b/liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/Client.java new file mode 100644 index 000000000..63aa8c63e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/Client.java @@ -0,0 +1,11 @@ +package testSuite.classes.state_set_declared_later_correct; + +import java.awt.Frame; + +public class Client { + public static void main(String[] args) { + Frame f = new Frame(); + f.setUndecorated(true); + f.pack(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/FrameRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/FrameRefinements.java new file mode 100644 index 000000000..73de66b1b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_set_declared_later_correct/FrameRefinements.java @@ -0,0 +1,22 @@ +package testSuite.classes.state_set_declared_later_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// uses the states of WindowRefinements, declared after it in this file +@ExternalRefinementsFor("java.awt.Frame") +public interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} + +@ExternalRefinementsFor("java.awt.Window") +@StateSet({"notDisplayable", "displayable"}) +interface WindowRefinements { + @StateRefinement(to = "displayable(this)") + void pack(); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 42e018d5e..de08649f5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -5,6 +5,7 @@ import liquidjava.processor.ann_generation.FieldGhostsGeneration; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.ExternalRefinementTypeChecker; +import liquidjava.processor.refinement_checker.GhostsFirstChecker; import liquidjava.processor.refinement_checker.MethodsFirstChecker; import liquidjava.processor.refinement_checker.RefinementTypeChecker; import spoon.processing.AbstractProcessor; @@ -32,9 +33,20 @@ public boolean isToBeProcessed(CtPackage pkg) { public void process(CtPackage pkg) { Context c = Context.getInstance(); c.reinitializeAllContext(); + registerGhosts(pkg, c); processPackage(pkg, c); } + /** + * Registers the ghosts and state sets of every type of the package and its sub-packages, before any spec is read, + * the ghosts of fields included + */ + private void registerGhosts(CtPackage pkg, Context c) { + pkg.getTypes().forEach(type -> type.accept(new FieldGhostsGeneration(c, factory))); + pkg.getTypes().forEach(type -> type.accept(new GhostsFirstChecker(c, factory))); + pkg.getPackages().forEach(subPkg -> registerGhosts(subPkg, c)); + } + private void processPackage(CtPackage pkg, Context c) { try { // first pass: gather refinements. External specifications are registered for every type before any class's @@ -42,7 +54,6 @@ private void processPackage(CtPackage pkg, Context c) { // the // specified super constructor it calls; an override is checked against its supertype's spec), whatever the // order of the types in the package. - pkg.getTypes().forEach(type -> type.accept(new FieldGhostsGeneration(c, factory))); pkg.getTypes().forEach(type -> type.accept(new ExternalRefinementTypeChecker(c, factory))); pkg.getTypes().forEach(type -> type.accept(new MethodsFirstChecker(c, factory))); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index d152d9c45..759807f57 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -54,22 +54,39 @@ public > void visitCtEnum(CtEnum ctEnum) { @Override public void visitCtInterface(CtInterface intrface) { - Optional> externalRef = getExternalRefinement(intrface); - if (externalRef.isPresent()) { - @SuppressWarnings("unchecked") - CtLiteral literal = (CtLiteral) externalRef.get().getAllValues().get("value"); - this.prefix = literal.getValue(); + Optional> target = targetOf(intrface); + if (target.isPresent()) { + this.prefix = target.get().getValue(); if (!classExists(prefix)) { String message = String.format("Could not find class '%s'", prefix); - diagnostics.add(new ExternalClassNotFoundWarning(literal.getPosition(), message, prefix)); + diagnostics.add(new ExternalClassNotFoundWarning(target.get().getPosition(), message, prefix)); return; } getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); } } + /** Registers the ghosts and state sets of an external spec under the class it refines, when that class exists */ + public void registerGhosts(CtInterface intrface) { + Optional> target = targetOf(intrface); + if (target.isEmpty() || !classExists(target.get().getValue())) + return; + this.prefix = target.get().getValue(); + try { + handleStateSetsFromAnnotation(intrface); + } catch (LJError e) { + diagnostics.add(e); + } + } + + /** The name of the class an external spec refines, as written in its annotation */ + @SuppressWarnings("unchecked") + private Optional> targetOf(CtInterface intrface) { + return getExternalRefinement(intrface) + .map(annotation -> (CtLiteral) annotation.getAllValues().get("value")); + } + @Override public void visitCtField(CtField f) { Optional oc = getRefinementFromAnnotation(f); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java new file mode 100644 index 000000000..ca2ded7cb --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java @@ -0,0 +1,44 @@ +package liquidjava.processor.refinement_checker; + +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.Context; +import spoon.reflect.declaration.CtClass; +import spoon.reflect.declaration.CtInterface; +import spoon.reflect.declaration.CtType; +import spoon.reflect.factory.Factory; + +/** + * First visit to the Spoon AST: registers the state sets and ghosts of every type, so that a spec read afterwards can + * use those of any type, whatever the order of the types in the package or of the interfaces in a spec file + */ +public class GhostsFirstChecker extends TypeChecker { + private final Diagnostics diagnostics = Diagnostics.getInstance(); + + public GhostsFirstChecker(Context context, Factory factory) { + super(context, factory); + } + + @Override + public void visitCtClass(CtClass ctClass) { + register(ctClass); + super.visitCtClass(ctClass); + } + + @Override + public void visitCtInterface(CtInterface intrface) { + if (getExternalRefinement(intrface).isPresent()) + new ExternalRefinementTypeChecker(context, factory).registerGhosts(intrface); + else + register(intrface); + super.visitCtInterface(intrface); + } + + private void register(CtType type) { + try { + handleStateSetsFromAnnotation(type); + } catch (LJError e) { + diagnostics.add(e); + } + } +} 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 fcfdea182..82660c2b9 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 @@ -58,7 +58,6 @@ public void visitCtClass(CtClass ctClass) { // errors here should not prevent visiting methods, constructors or fields of the class try { getRefinementFromAnnotation(ctClass); - handleStateSetsFromAnnotation(ctClass); } catch (LJError e) { diagnostics.add(e); } @@ -87,7 +86,6 @@ public void visitCtInterface(CtInterface intrface) { // errors here should not prevent visiting the interface's methods try { getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); } catch (LJError e) { diagnostics.add(e); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index ed01d33ec..066fe9267 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -116,11 +116,6 @@ public Optional getRefinementFromAnnotation(CtElement element) throws String value = getStringFromAnnotation(ann.getValue("value")); ref = Optional.of(value); - } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { - CtExpression rawValue = ann.getValue("value"); - String value = getStringFromAnnotation(rawValue); - getGhostFunction(value, element, Utils.getAnnotationValuePosition(rawValue)); - } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) { CtExpression rawValue = ann.getValue("value"); String value = getStringFromAnnotation(rawValue); @@ -198,6 +193,7 @@ public Optional getMessageFromAnnotation(CtElement element) { return Optional.empty(); } + /** Registers the ghosts and state sets a type declares, then checks the names given to its state sets */ @SuppressWarnings("unchecked") public void handleStateSetsFromAnnotation(CtElement element) throws LJError { int set = 0; @@ -218,6 +214,11 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); createStateGhost(s.getValue(), element, Utils.getAnnotationValuePosition(s)); } + if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { + CtExpression rawValue = ann.getValue("value"); + getGhostFunction(getStringFromAnnotation(rawValue), element, + Utils.getAnnotationValuePosition(rawValue)); + } } // checked once every set and ghost of the class exists, so the order of the annotations does not matter for (Map.Entry named : namedSets.entrySet()) From fe644ba2700d5c6da73ce620366f028d1bedc7a2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 17:56:10 +0000 Subject: [PATCH 2/2] Name the method that registers a type's ghosts and state sets after what it does Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/ExternalRefinementTypeChecker.java | 2 +- .../processor/refinement_checker/GhostsFirstChecker.java | 2 +- .../liquidjava/processor/refinement_checker/TypeChecker.java | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 759807f57..5625babdb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -74,7 +74,7 @@ public void registerGhosts(CtInterface intrface) { return; this.prefix = target.get().getValue(); try { - handleStateSetsFromAnnotation(intrface); + registerGhostsAndStateSets(intrface); } catch (LJError e) { diagnostics.add(e); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java index ca2ded7cb..41b4f2fc4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/GhostsFirstChecker.java @@ -36,7 +36,7 @@ public void visitCtInterface(CtInterface intrface) { private void register(CtType type) { try { - handleStateSetsFromAnnotation(type); + registerGhostsAndStateSets(type); } catch (LJError e) { diagnostics.add(e); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 066fe9267..ad9955a60 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -195,7 +195,7 @@ public Optional getMessageFromAnnotation(CtElement element) { /** Registers the ghosts and state sets a type declares, then checks the names given to its state sets */ @SuppressWarnings("unchecked") - public void handleStateSetsFromAnnotation(CtElement element) throws LJError { + public void registerGhostsAndStateSets(CtElement element) throws LJError { int set = 0; Map namedSets = new LinkedHashMap<>(); for (CtAnnotation ann : element.getAnnotations()) {