GeezerVison is showing github.com — Register every ghost and state set before any spec is read by CatarinaGamboa · Pull Request #508 · liquid-java/liquidjava
Register every ghost and state set before any spec is read
#508
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement . We’ll occasionally send you account related emails.
Already on GitHub?
Sign in
to your account
Uh oh!
There was an error while loading. Please reload this page.
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter
Filter by extension
.java
(8)
All 1 file type selected
Viewed files
Conversations
Failed to load comments.
Loading
Uh oh!
There was an error while loading. Please reload this page.
Jump to
Jump to file
Failed to load files.
Loading
Uh oh!
There was an error while loading. Please reload this page.
Diff view
Hide whitespace
Diff view
Hide whitespace
Register every ghost and state set before any spec is read
Loading branch information
Uh oh!
There was an error while loading. Please reload this page.
commit bcbeb3c587bb53136eeca4386bec36a3f2e3a5ff
There are no files selected for viewing
Original file line number
Diff line number
Diff line change
@@ -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
Expand All
@@ -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 {}
Original file line number
Diff line number
Diff line change
@@ -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();
}
}
Original file line number
Diff line number
Diff line change
@@ -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();
}
Original file line number
Diff line number
Diff line change
Expand Up
@@ -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;
Expand Down
Expand Up
@@ -32,17 +33,27 @@ 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
// own methods and constructors, which may rely on them (an unannotated constructor inherits the state of
// 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)));
Expand Down
Original file line number
Diff line number
Diff line change
Expand Up
@@ -54,22 +54,39 @@ public <T extends Enum<?>> void visitCtEnum(CtEnum<T> ctEnum) {
@Override
public <T> void visitCtInterface(CtInterface<T> intrface) {
Optional<CtAnnotation<?>> externalRef = getExternalRefinement(intrface);
if (externalRef.isPresent()) {
@SuppressWarnings("unchecked")
CtLiteral<String> literal = (CtLiteral<String>) externalRef.get().getAllValues().get("value");
this.prefix = literal.getValue();
Optional<CtLiteral<String>> 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<CtLiteral<String>> 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<CtLiteral<String>> targetOf(CtInterface<?> intrface) {
return getExternalRefinement(intrface)
.map(annotation -> (CtLiteral<String>) annotation.getAllValues().get("value"));
}
@Override
public <T> void visitCtField(CtField<T> f) {
Optional<Predicate> oc = getRefinementFromAnnotation(f);
Expand Down
Original file line number
Diff line number
Diff line change
@@ -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 <T> void visitCtClass(CtClass<T> ctClass) {
register(ctClass);
super.visitCtClass(ctClass);
}
@Override
public <T> void visitCtInterface(CtInterface<T> 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);
}
}
}
Original file line number
Diff line number
Diff line change
Expand Up
@@ -58,7 +58,6 @@ public <T> void visitCtClass(CtClass<T> 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);
}
Expand Down
Expand Up
@@ -87,7 +86,6 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
// errors here should not prevent visiting the interface's methods
try {
getRefinementFromAnnotation(intrface);
handleStateSetsFromAnnotation(intrface);
} catch (LJError e) {
diagnostics.add(e);
}
Expand Down
Original file line number
Diff line number
Diff line change
Expand Up
@@ -116,11 +116,6 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
String value = getStringFromAnnotation(ann.getValue("value"));
ref = Optional.of(value);
} else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
CtExpression<String> rawValue = ann.getValue("value");
String value = getStringFromAnnotation(rawValue);
getGhostFunction(value, element, Utils.getAnnotationValuePosition(rawValue));
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
CtExpression<String> rawValue = ann.getValue("value");
String value = getStringFromAnnotation(rawValue);
Expand Down
Expand Up
@@ -198,6 +193,7 @@ public Optional<String> 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;
Expand All
@@ -218,6 +214,11 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
createStateGhost(s.getValue(), element, Utils.getAnnotationValuePosition(s));
}
if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
CtExpression<String> 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<GhostFunction, SourcePosition> named : namedSets.entrySet())
Expand Down
Loading
Oops, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.