Skip to content

Commit 99ebc66

Browse files
rcosta358rcosta358
committed
Improve Syntax Errors
1 parent 62cf349 commit 99ebc66

3 files changed

Lines changed: 31 additions & 28 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
import liquidjava.rj_language.parsing.RefinementsParser;
1616
import liquidjava.utils.Utils;
1717
import spoon.reflect.code.CtLiteral;
18-
import spoon.reflect.cu.SourcePosition;
1918
import spoon.reflect.declaration.CtAnnotation;
2019
import spoon.reflect.declaration.CtClass;
2120
import spoon.reflect.declaration.CtElement;
@@ -94,8 +93,8 @@ public <R> void visitCtMethod(CtMethod<R> method) {
9493
super.visitCtMethod(method);
9594
}
9695

97-
protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
98-
GhostDTO f = getGhostDeclaration(value, position);
96+
protected void getGhostFunction(String value, CtElement element) throws LJError {
97+
GhostDTO f = getGhostDeclaration(value, element);
9998
if (element.getParent() instanceof CtInterface<?>) {
10099
GhostFunction gh = new GhostFunction(f, factory, prefix);
101100
context.addGhostFunction(gh);

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java‎

Lines changed: 26 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -66,24 +66,25 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
6666
for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
6767
String an = ann.getActualAnnotation().annotationType().getCanonicalName();
6868
if (an.contentEquals("liquidjava.specification.Refinement")) {
69-
String value = getStringFromAnnotation(ann.getValue("value"));
70-
ref = Optional.of(value);
69+
String st = getStringFromAnnotation(ann.getValue("value"));
70+
ref = Optional.of(st);
7171

7272
} else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
73-
String value = getStringFromAnnotation(ann.getValue("value"));
74-
getGhostFunction(value, element, ann.getPosition());
73+
String st = getStringFromAnnotation(ann.getValue("value"));
74+
getGhostFunction(st, element);
7575

7676
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
77-
String value = getStringFromAnnotation(ann.getValue("value"));
78-
handleAlias(value, element, ann.getPosition());
77+
String st = getStringFromAnnotation(ann.getValue("value"));
78+
handleAlias(st, element);
7979
}
8080
}
8181
if (ref.isPresent()) {
8282
Predicate p = new Predicate(ref.get(), element);
83+
84+
// check if refinement is valid
8385
if (!p.getExpression().isBooleanExpression()) {
84-
SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
85-
throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
86-
ref.get());
86+
throw new InvalidRefinementError(element.getPosition(),
87+
"Refinement predicate must be a boolean expression", ref.get());
8788
}
8889
constr = Optional.of(p);
8990
}
@@ -116,7 +117,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
116117
}
117118
if (an.contentEquals("liquidjava.specification.Ghost")) {
118119
CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
119-
createStateGhost(s.getValue(), element, ann.getPosition());
120+
createStateGhost(s.getValue(), ann, element);
120121
}
121122
}
122123
}
@@ -162,22 +163,24 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
162163
}
163164
}
164165

165-
protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError {
166+
protected GhostDTO getGhostDeclaration(String value, CtElement element) throws LJError {
166167
try {
167168
return RefinementsParser.getGhostDeclaration(value);
168169
} catch (LJError e) {
169170
// add location info to error
170-
e.setPosition(position);
171+
SourcePosition annPosition = Utils.getAnnotationPosition(element, value);
172+
e.setPosition(annPosition);
171173
throw e;
172174
}
173175
}
174176

175-
private void createStateGhost(String string, CtElement element, SourcePosition position) throws LJError {
176-
GhostDTO gd = getGhostDeclaration(string, position);
177+
private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
178+
throws LJError {
179+
GhostDTO gd = getGhostDeclaration(string, ann);
177180
if (!gd.paramTypes().isEmpty()) {
178181
throw new CustomError(
179182
"Ghost States have the class as parameter " + "by default, no other parameters are allowed",
180-
position);
183+
ann.getPosition());
181184
}
182185
// Set class as parameter of Ghost
183186
String qn = getQualifiedClassName(element);
@@ -228,15 +231,15 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
228231
return Optional.empty();
229232
}
230233

231-
protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
232-
GhostDTO f = getGhostDeclaration(value, position);
234+
protected void getGhostFunction(String value, CtElement element) throws LJError {
235+
GhostDTO f = getGhostDeclaration(value, element);
233236
if (element.getParent()instanceof CtClass<?> klass) {
234237
GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
235238
context.addGhostFunction(gh);
236239
}
237240
}
238241

239-
protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {
242+
protected void handleAlias(String ref, CtElement element) throws LJError {
240243
try {
241244
AliasDTO a = RefinementsParser.getAliasDeclaration(ref);
242245
String klass = null;
@@ -250,16 +253,18 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
250253
}
251254
if (klass != null && path != null) {
252255
a.parse(path);
256+
// refinement alias must return a boolean expression
253257
if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
254-
throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
255-
ref);
258+
throw new InvalidRefinementError(element.getPosition(),
259+
"Refinement alias must return a boolean expression", ref);
256260
}
257261
AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
258262
context.addAlias(aw);
259263
}
260264
} catch (LJError e) {
261265
// add location info to error
262-
e.setPosition(position);
266+
SourcePosition pos = Utils.getAnnotationPosition(element, ref);
267+
e.setPosition(pos);
263268
throw e;
264269
}
265270
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ public static GhostDTO getGhostDeclaration(String s) throws LJError {
3535
ParseTree rc = compile(s);
3636
GhostDTO g = GhostVisitor.getGhostDecl(rc);
3737
if (g == null)
38-
throw new SyntaxError("Invalid ghost declaration, expected e.g. @Ghost(\"int size\")", s);
38+
throw new SyntaxError("Invalid ghost declaration, e.g. \"int size\"", s);
3939
return g;
4040
}
4141

@@ -56,15 +56,14 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError {
5656
AliasVisitor av = new AliasVisitor(input);
5757
AliasDTO alias = av.getAlias(rc);
5858
if (alias == null)
59-
throw new SyntaxError(
60-
"Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s);
59+
throw new SyntaxError("Invalid alias definition, e.g. \"Positive(int v) { v >= 0 }\"", s);
6160
return alias;
6261
}
6362

6463
private static ParseTree compile(String toParse) throws LJError {
6564
Optional<String> s = getErrors(toParse);
6665
if (s.isPresent())
67-
throw new SyntaxError("Invalid refinement expression, expected a logical predicate", toParse);
66+
throw new SyntaxError("Invalid refinement expression, e.g. \"v > 0\"", toParse);
6867

6968
CodePointCharStream input = CharStreams.fromString(toParse);
7069
RJErrorListener err = new RJErrorListener();

0 commit comments

Comments
 (0)