diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java index c38a69b1..144922bc 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 00000000..63aa8c63 --- /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 00000000..73de66b1 --- /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 42e018d5..de08649f 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 d152d9c4..5625babd 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 { + registerGhostsAndStateSets(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 00000000..41b4f2fc --- /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 { + registerGhostsAndStateSets(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 fcfdea18..82660c2b 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 ed01d33e..ad9955a6 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,8 +193,9 @@ 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 { + public void registerGhostsAndStateSets(CtElement element) throws LJError { int set = 0; Map namedSets = new LinkedHashMap<>(); for (CtAnnotation ann : element.getAnnotations()) { @@ -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())