Skip to content

Commit 62cf349

Browse files
rcosta358rcosta358
authored
Improve Syntax Errors (#166)
1 parent 2a8f9b7 commit 62cf349

File tree

6 files changed

+44
-40
lines changed

6 files changed

+44
-40
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ public String getSnippet() {
129129

130130
// line number padding + pipe + column offset
131131
String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
132-
+ " ".repeat(visualColStart - 1);
132+
+ " ".repeat(visualColStart - 1);
133133
String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
134134
sb.append(indent).append(markers);
135135

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

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

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

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

Lines changed: 29 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -66,25 +66,24 @@ 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 st = getStringFromAnnotation(ann.getValue("value"));
70-
ref = Optional.of(st);
69+
String value = getStringFromAnnotation(ann.getValue("value"));
70+
ref = Optional.of(value);
7171

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

7676
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
77-
String st = getStringFromAnnotation(ann.getValue("value"));
78-
handleAlias(st, element);
77+
String value = getStringFromAnnotation(ann.getValue("value"));
78+
handleAlias(value, element, ann.getPosition());
7979
}
8080
}
8181
if (ref.isPresent()) {
8282
Predicate p = new Predicate(ref.get(), element);
83-
84-
// check if refinement is valid
8583
if (!p.getExpression().isBooleanExpression()) {
86-
throw new InvalidRefinementError(element.getPosition(),
87-
"Refinement predicate must be a boolean expression", ref.get());
84+
SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
85+
throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
86+
ref.get());
8887
}
8988
constr = Optional.of(p);
9089
}
@@ -117,7 +116,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
117116
}
118117
if (an.contentEquals("liquidjava.specification.Ghost")) {
119118
CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
120-
createStateGhost(s.getValue(), ann, element);
119+
createStateGhost(s.getValue(), element, ann.getPosition());
121120
}
122121
}
123122
}
@@ -163,13 +162,22 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
163162
}
164163
}
165164

166-
private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
167-
throws LJError {
168-
GhostDTO gd = RefinementsParser.getGhostDeclaration(string);
165+
protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError {
166+
try {
167+
return RefinementsParser.getGhostDeclaration(value);
168+
} catch (LJError e) {
169+
// add location info to error
170+
e.setPosition(position);
171+
throw e;
172+
}
173+
}
174+
175+
private void createStateGhost(String string, CtElement element, SourcePosition position) throws LJError {
176+
GhostDTO gd = getGhostDeclaration(string, position);
169177
if (!gd.paramTypes().isEmpty()) {
170178
throw new CustomError(
171179
"Ghost States have the class as parameter " + "by default, no other parameters are allowed",
172-
ann.getPosition());
180+
position);
173181
}
174182
// Set class as parameter of Ghost
175183
String qn = getQualifiedClassName(element);
@@ -220,15 +228,15 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
220228
return Optional.empty();
221229
}
222230

223-
protected void getGhostFunction(String value, CtElement element) throws LJError {
224-
GhostDTO f = RefinementsParser.getGhostDeclaration(value);
231+
protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
232+
GhostDTO f = getGhostDeclaration(value, position);
225233
if (element.getParent()instanceof CtClass<?> klass) {
226234
GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
227235
context.addGhostFunction(gh);
228236
}
229237
}
230238

231-
protected void handleAlias(String ref, CtElement element) throws LJError {
239+
protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {
232240
try {
233241
AliasDTO a = RefinementsParser.getAliasDeclaration(ref);
234242
String klass = null;
@@ -242,18 +250,16 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
242250
}
243251
if (klass != null && path != null) {
244252
a.parse(path);
245-
// refinement alias must return a boolean expression
246253
if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
247-
throw new InvalidRefinementError(element.getPosition(),
248-
"Refinement alias must return a boolean expression", ref);
254+
throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
255+
ref);
249256
}
250257
AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
251258
context.addAlias(aw);
252259
}
253260
} catch (LJError e) {
254261
// add location info to error
255-
SourcePosition pos = Utils.getAnnotationPosition(element, ref);
256-
e.setPosition(pos);
262+
e.setPosition(position);
257263
throw e;
258264
}
259265
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import liquidjava.utils.constants.Keys;
1717
import liquidjava.utils.constants.Types;
1818
import spoon.reflect.code.*;
19+
import spoon.reflect.cu.SourcePosition;
1920
import spoon.reflect.declaration.*;
2021
import spoon.reflect.reference.CtTypeReference;
2122

@@ -69,7 +70,7 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
6970
if (to != null) {
7071
Predicate p = new Predicate(to, element);
7172
if (!p.getExpression().isBooleanExpression()) {
72-
throw new InvalidRefinementError(element.getPosition(),
73+
throw new InvalidRefinementError(an.getPosition(),
7374
"State refinement transition must be a boolean expression", to);
7475
}
7576
state.setTo(p);
@@ -208,8 +209,9 @@ private static Predicate createStatePredicate(String value, String targetClass,
208209
boolean isTo, String prefix) throws LJError {
209210
Predicate p = new Predicate(value, e, prefix);
210211
if (!p.getExpression().isBooleanExpression()) {
211-
throw new InvalidRefinementError(e.getPosition(),
212-
"State refinement transition must be a boolean expression", value);
212+
SourcePosition position = Utils.getAnnotationPosition(e, value);
213+
throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
214+
value);
213215
}
214216
CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
215217
String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());

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

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -35,16 +35,12 @@ 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("Ghost declarations should be in format <type> <name> (<parameters>)", s);
38+
throw new SyntaxError("Invalid ghost declaration, expected e.g. @Ghost(\"int size\")", s);
3939
return g;
4040
}
4141

4242
public static AliasDTO getAliasDeclaration(String s) throws LJError {
43-
Optional<String> os = getErrors(s);
44-
if (os.isPresent())
45-
throw new SyntaxError(os.get(), s);
46-
CodePointCharStream input;
47-
input = CharStreams.fromString(s);
43+
CodePointCharStream input = CharStreams.fromString(s);
4844
RJErrorListener err = new RJErrorListener();
4945
RJLexer lexer = new RJLexer(input);
5046
lexer.removeErrorListeners();
@@ -60,14 +56,15 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError {
6056
AliasVisitor av = new AliasVisitor(input);
6157
AliasDTO alias = av.getAlias(rc);
6258
if (alias == null)
63-
throw new SyntaxError("Alias definitions should be in format <name>(<parameters>) { <definition> }", s);
59+
throw new SyntaxError(
60+
"Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s);
6461
return alias;
6562
}
6663

6764
private static ParseTree compile(String toParse) throws LJError {
6865
Optional<String> s = getErrors(toParse);
6966
if (s.isPresent())
70-
throw new SyntaxError(s.get(), toParse);
67+
throw new SyntaxError("Invalid refinement expression, expected a logical predicate", toParse);
7168

7269
CodePointCharStream input = CharStreams.fromString(toParse);
7370
RJErrorListener err = new RJErrorListener();

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,7 @@ public static GhostDTO getGhostDecl(ParseTree rc) {
1919
List<String> ls = args.stream().map(Pair::first).collect(Collectors.toList());
2020
return new GhostDTO(name, ls, type);
2121
} else if (rc.getChildCount() > 0) {
22-
int i = rc.getChildCount();
23-
if (i > 0)
24-
return getGhostDecl(rc.getChild(0));
22+
return getGhostDecl(rc.getChild(0));
2523
}
2624
return null;
2725
}

0 commit comments

Comments
 (0)