Skip to content

Commit 152ec18

Browse files
rcosta358rcosta358
authored
Merge branch 'main' into context-history-improvements
2 parents eb535e7 + 5430ba1 commit 152ec18

File tree

6 files changed

+77
-95
lines changed

6 files changed

+77
-95
lines changed

‎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
@@ -16,6 +16,7 @@
1616
import liquidjava.rj_language.parsing.RefinementsParser;
1717
import liquidjava.utils.Utils;
1818
import spoon.reflect.code.CtLiteral;
19+
import spoon.reflect.cu.SourcePosition;
1920
import spoon.reflect.declaration.CtAnnotation;
2021
import spoon.reflect.declaration.CtClass;
2122
import spoon.reflect.declaration.CtElement;
@@ -95,8 +96,8 @@ public <R> void visitCtMethod(CtMethod<R> method) {
9596
super.visitCtMethod(method);
9697
}
9798

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

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

Lines changed: 30 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -68,25 +68,24 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
6868
for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
6969
String an = ann.getActualAnnotation().annotationType().getCanonicalName();
7070
if (an.contentEquals("liquidjava.specification.Refinement")) {
71-
String st = getStringFromAnnotation(ann.getValue("value"));
72-
ref = Optional.of(st);
71+
String value = getStringFromAnnotation(ann.getValue("value"));
72+
ref = Optional.of(value);
7373

7474
} else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
75-
String st = getStringFromAnnotation(ann.getValue("value"));
76-
getGhostFunction(st, element);
75+
String value = getStringFromAnnotation(ann.getValue("value"));
76+
getGhostFunction(value, element, ann.getPosition());
7777

7878
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
79-
String st = getStringFromAnnotation(ann.getValue("value"));
80-
handleAlias(st, element);
79+
String value = getStringFromAnnotation(ann.getValue("value"));
80+
handleAlias(value, element, ann.getPosition());
8181
}
8282
}
8383
if (ref.isPresent()) {
8484
Predicate p = new Predicate(ref.get(), element);
85-
86-
// check if refinement is valid
8785
if (!p.getExpression().isBooleanExpression()) {
88-
throw new InvalidRefinementError(element.getPosition(),
89-
"Refinement predicate must be a boolean expression", ref.get());
86+
SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
87+
throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
88+
ref.get());
9089
}
9190
constr = Optional.of(p);
9291
}
@@ -119,7 +118,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
119118
}
120119
if (an.contentEquals("liquidjava.specification.Ghost")) {
121120
CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
122-
createStateGhost(s.getValue(), ann, element);
121+
createStateGhost(s.getValue(), element, ann.getPosition());
123122
}
124123
}
125124
}
@@ -166,13 +165,22 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
166165
}
167166
}
168167

169-
private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
170-
throws LJError {
171-
GhostDTO gd = RefinementsParser.getGhostDeclaration(string);
168+
protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError {
169+
try {
170+
return RefinementsParser.parseGhostDeclaration(value);
171+
} catch (LJError e) {
172+
// add location info to error
173+
e.setPosition(position);
174+
throw e;
175+
}
176+
}
177+
178+
private void createStateGhost(String string, CtElement element, SourcePosition position) throws LJError {
179+
GhostDTO gd = getGhostDeclaration(string, position);
172180
if (!gd.paramTypes().isEmpty()) {
173181
throw new CustomError(
174182
"Ghost States have the class as parameter " + "by default, no other parameters are allowed",
175-
ann.getPosition());
183+
position);
176184
}
177185
// Set class as parameter of Ghost
178186
String qn = getQualifiedClassName(element);
@@ -224,17 +232,17 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
224232
return Optional.empty();
225233
}
226234

227-
protected void getGhostFunction(String value, CtElement element) throws LJError {
228-
GhostDTO f = RefinementsParser.getGhostDeclaration(value);
235+
protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
236+
GhostDTO f = getGhostDeclaration(value, position);
229237
if (element.getParent()instanceof CtClass<?> klass) {
230238
GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
231239
context.addGhostFunction(gh);
232240
}
233241
}
234242

235-
protected void handleAlias(String ref, CtElement element) throws LJError {
243+
protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {
236244
try {
237-
AliasDTO a = RefinementsParser.getAliasDeclaration(ref);
245+
AliasDTO a = RefinementsParser.parseAliasDefinition(ref);
238246
String klass = null;
239247
String path = null;
240248
if (element instanceof CtClass) {
@@ -246,18 +254,16 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
246254
}
247255
if (klass != null && path != null) {
248256
a.parse(path);
249-
// refinement alias must return a boolean expression
250257
if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
251-
throw new InvalidRefinementError(element.getPosition(),
252-
"Refinement alias must return a boolean expression", ref);
258+
throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
259+
ref);
253260
}
254261
AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
255262
context.addAlias(aw);
256263
}
257264
} catch (LJError e) {
258265
// add location info to error
259-
SourcePosition pos = Utils.getLJAnnotationPosition(element, ref);
260-
e.setPosition(pos);
266+
e.setPosition(position);
261267
throw e;
262268
}
263269
}

‎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: 37 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22

33
import java.util.Optional;
44

5-
import liquidjava.diagnostics.errors.LJError;
65
import liquidjava.diagnostics.errors.SyntaxError;
76
import liquidjava.processor.facade.AliasDTO;
87
import liquidjava.processor.facade.GhostDTO;
@@ -13,102 +12,85 @@
1312
import org.antlr.v4.runtime.CharStreams;
1413
import org.antlr.v4.runtime.CodePointCharStream;
1514
import org.antlr.v4.runtime.CommonTokenStream;
16-
import org.antlr.v4.runtime.RuleContext;
1715
import org.antlr.v4.runtime.tree.ParseTree;
1816
import rj.grammar.RJLexer;
1917
import rj.grammar.RJParser;
2018

2119
public class RefinementsParser {
2220

23-
public static Expression createAST(String toParse, String prefix) throws LJError {
24-
ParseTree pt = compile(toParse);
21+
/**
22+
* Parses a refinement expression from a string
23+
*/
24+
public static Expression createAST(String toParse, String prefix) throws SyntaxError {
25+
ParseTree pt = compile(toParse, "Invalid refinement expression, expected a logical predicate");
2526
CreateASTVisitor visitor = new CreateASTVisitor(prefix);
2627
return visitor.create(pt);
2728
}
2829

2930
/**
30-
* The triple information of the ghost declaration in the order <type, name, list<type,name>>
31-
*
32-
* @param s
31+
* Parses the ghost declaration from the given string
3332
*/
34-
public static GhostDTO getGhostDeclaration(String s) throws LJError {
35-
ParseTree rc = compile(s);
33+
public static GhostDTO parseGhostDeclaration(String toParse) throws SyntaxError {
34+
String errorMessage = "Invalid ghost declaration, expected e.g. @Ghost(\"int size\")";
35+
ParseTree rc = compile(toParse, errorMessage);
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(errorMessage, toParse);
3939
return g;
4040
}
4141

42-
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);
48-
RJErrorListener err = new RJErrorListener();
49-
RJLexer lexer = new RJLexer(input);
50-
lexer.removeErrorListeners();
51-
lexer.addErrorListener(err);
52-
53-
CommonTokenStream tokens = new CommonTokenStream(lexer);
54-
RJParser parser = new RJParser(tokens);
55-
parser.setBuildParseTree(true);
56-
parser.removeErrorListeners();
57-
parser.addErrorListener(err);
58-
59-
RuleContext rc = parser.prog();
60-
AliasVisitor av = new AliasVisitor(input);
42+
/**
43+
* Parses the alias declaration from the given string, throwing a SyntaxError if it is not valid
44+
*/
45+
public static AliasDTO parseAliasDefinition(String toParse) throws SyntaxError {
46+
String errorMessage = "Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")";
47+
ParseTree rc = compile(toParse, errorMessage);
48+
AliasVisitor av = new AliasVisitor();
6149
AliasDTO alias = av.getAlias(rc);
6250
if (alias == null)
63-
throw new SyntaxError("Alias definitions should be in format <name>(<parameters>) { <definition> }", s);
51+
throw new SyntaxError(errorMessage, toParse);
6452
return alias;
6553
}
6654

67-
private static ParseTree compile(String toParse) throws LJError {
55+
/**
56+
* Compiles the given string into a parse tree
57+
*/
58+
private static ParseTree compile(String toParse, String errorMessage) throws SyntaxError {
6859
Optional<String> s = getErrors(toParse);
6960
if (s.isPresent())
70-
throw new SyntaxError(s.get(), toParse);
61+
throw new SyntaxError(errorMessage, toParse);
7162

72-
CodePointCharStream input = CharStreams.fromString(toParse);
7363
RJErrorListener err = new RJErrorListener();
74-
75-
RJLexer lexer = new RJLexer(input);
76-
lexer.removeErrorListeners();
77-
lexer.addErrorListener(err);
78-
79-
CommonTokenStream tokens = new CommonTokenStream(lexer);
80-
81-
RJParser parser = new RJParser(tokens);
82-
parser.setBuildParseTree(true);
83-
parser.removeErrorListeners();
84-
parser.addErrorListener(err);
64+
RJParser parser = createParser(toParse, err);
8565
return parser.prog();
8666
}
8767

8868
/**
89-
* First passage to check if there are syntax errors
90-
*
91-
* @param toParse
92-
*
93-
* @return
69+
* Checks if the given string can be parsed without syntax errors, returning the error messages if any
9470
*/
9571
private static Optional<String> getErrors(String toParse) {
96-
CodePointCharStream input = CharStreams.fromString(toParse);
9772
RJErrorListener err = new RJErrorListener();
73+
RJParser parser = createParser(toParse, err);
74+
parser.start(); // all consumed
75+
if (err.getErrors() > 0)
76+
return Optional.of(err.getMessages());
77+
return Optional.empty();
78+
}
9879

80+
/**
81+
* Creates a parser for the given input string and error listener
82+
*/
83+
private static RJParser createParser(String toParse, RJErrorListener err) {
84+
CodePointCharStream input = CharStreams.fromString(toParse);
9985
RJLexer lexer = new RJLexer(input);
10086
lexer.removeErrorListeners();
10187
lexer.addErrorListener(err);
10288

10389
CommonTokenStream tokens = new CommonTokenStream(lexer);
104-
10590
RJParser parser = new RJParser(tokens);
10691
parser.setBuildParseTree(true);
10792
parser.removeErrorListeners();
10893
parser.addErrorListener(err);
109-
parser.start(); // all consumed
110-
if (err.getErrors() > 0)
111-
return Optional.of(err.getMessages());
112-
return Optional.empty();
94+
return parser;
11395
}
11496
}

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

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,13 @@
55
import java.util.stream.Collectors;
66
import liquidjava.processor.facade.AliasDTO;
77
import liquidjava.utils.Pair;
8-
import org.antlr.v4.runtime.CodePointCharStream;
98
import org.antlr.v4.runtime.misc.Interval;
109
import org.antlr.v4.runtime.tree.ParseTree;
1110
import rj.grammar.RJParser.AliasContext;
1211
import rj.grammar.RJParser.ArgDeclIDContext;
1312
import rj.grammar.RJParser.PredContext;
1413

1514
public class AliasVisitor {
16-
CodePointCharStream input;
17-
18-
public AliasVisitor(CodePointCharStream input) {
19-
this.input = input;
20-
}
21-
2215
/**
2316
* Gets information about the alias
2417
*
@@ -56,7 +49,7 @@ private String getText(PredContext pred) {
5649
int a = pred.start.getStartIndex();
5750
int b = pred.stop.getStopIndex();
5851
Interval interval = new Interval(a, b);
59-
return input.getText(interval);
52+
return pred.start.getInputStream().getText(interval);
6053
}
6154

6255
private List<Pair<String, String>> getArgsDecl(ArgDeclIDContext argDeclID) {

‎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)