Skip to content

Commit c9c22e9

Browse files
rcosta358rcosta358
committed
Refactor Errors
1 parent 19b2049 commit c9c22e9

File tree

15 files changed

+112
-98
lines changed

15 files changed

+112
-98
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,8 @@ public String toString() {
5353
StringBuilder sb = new StringBuilder();
5454

5555
// title
56-
sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET)
57-
.append(message.toLowerCase()).append("\n");
56+
sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
57+
.append("\n");
5858

5959
// snippet
6060
String snippet = getSnippet();

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java‎

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package liquidjava.diagnostics.errors;
22

33
import spoon.reflect.cu.SourcePosition;
4-
import spoon.reflect.declaration.CtElement;
54

65
/**
76
* Custom error with an arbitrary message
@@ -14,15 +13,11 @@ public CustomError(String message) {
1413
super("Error", message, null, null, null);
1514
}
1615

17-
public CustomError(String message, SourcePosition pos) {
18-
super("Error", message, null, pos, null);
16+
public CustomError(String message, SourcePosition position) {
17+
super("Error", message, null, position, null);
1918
}
2019

21-
public CustomError(String message, String detail, CtElement element) {
22-
super("Error", message, detail, element.getPosition(), null);
23-
}
24-
25-
public CustomError(String message, CtElement element) {
26-
super("Error", message, null, element.getPosition(), null);
20+
public CustomError(String message, SourcePosition position, String detail) {
21+
super("Error", message, detail, position, null);
2722
}
2823
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
package liquidjava.diagnostics.errors;
22

3-
import spoon.reflect.declaration.CtElement;
3+
import spoon.reflect.cu.SourcePosition;
44

55
/**
66
* Error indicating that a refinement is invalid (e.g., not a boolean expression)
@@ -11,8 +11,8 @@ public class InvalidRefinementError extends LJError {
1111

1212
private final String refinement;
1313

14-
public InvalidRefinementError(CtElement element, String message, String refinement) {
15-
super("Invalid Refinement", message, "", element.getPosition(), null);
14+
public InvalidRefinementError(SourcePosition position, String message, String refinement) {
15+
super("Invalid Refinement", message, "", position, null);
1616
this.refinement = refinement;
1717
}
1818

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,23 +2,30 @@
22

33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.utils.Utils;
5-
import spoon.reflect.declaration.CtElement;
5+
import spoon.reflect.cu.SourcePosition;
66

77
/**
88
* Error indicating that an element referenced in a refinement was not found
99
*
1010
* @see LJError
1111
*/
1212
public class NotFoundError extends LJError {
13-
13+
1414
private final String name;
15+
private final String kind; // "Variable" or "Ghost"
1516

16-
public NotFoundError(CtElement element, String message, String name, TranslationTable translationTable) {
17-
super("Not Found Error", message, "", element.getPosition(), translationTable);
17+
public NotFoundError(SourcePosition position, String message, String name, String kind,
18+
TranslationTable translationTable) {
19+
super("Not Found Error", message, "", position, translationTable);
1820
this.name = Utils.getSimpleName(name);
21+
this.kind = kind;
1922
}
2023

2124
public String getName() {
2225
return name;
2326
}
27+
28+
public String getKind() {
29+
return kind;
30+
}
2431
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.rj_language.ast.Expression;
55
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
6-
import spoon.reflect.declaration.CtElement;
6+
import spoon.reflect.cu.SourcePosition;
77

88
/**
99
* Error indicating that a refinement constraint either was violated or cannot be proven
@@ -15,11 +15,11 @@ public class RefinementError extends LJError {
1515
private final String expected;
1616
private final ValDerivationNode found;
1717

18-
public RefinementError(CtElement element, Expression expected, ValDerivationNode found,
18+
public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found,
1919
TranslationTable translationTable) {
2020
super("Refinement Error",
2121
String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "",
22-
element.getPosition(), translationTable);
22+
position, translationTable);
2323
this.expected = expected.toSimplifiedString();
2424
this.found = found;
2525
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.rj_language.ast.Expression;
5-
import spoon.reflect.declaration.CtElement;
5+
import spoon.reflect.cu.SourcePosition;
66

77
/**
88
* Error indicating that two disjoint states were found in a state refinement
@@ -13,10 +13,9 @@ public class StateConflictError extends LJError {
1313

1414
private final String state;;
1515

16-
public StateConflictError(CtElement element, Expression state,
17-
TranslationTable translationTable) {
16+
public StateConflictError(SourcePosition position, Expression state, TranslationTable translationTable) {
1817
super("State Conflict Error", "Found multiple disjoint states in state transition",
19-
"State transition can only go to one state of each state set", element.getPosition(), translationTable);
18+
"State transition can only go to one state of each state set", position, translationTable);
2019
this.state = state.toSimplifiedString();
2120
}
2221

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.rj_language.ast.Expression;
5-
import spoon.reflect.declaration.CtElement;
5+
import spoon.reflect.cu.SourcePosition;
66

77
/**
88
* Error indicating that a state refinement transition was violated
@@ -14,10 +14,10 @@ public class StateRefinementError extends LJError {
1414
private final String expected;
1515
private final String found;
1616

17-
public StateRefinementError(CtElement element, Expression expected, Expression found,
17+
public StateRefinementError(SourcePosition position, Expression expected, Expression found,
1818
TranslationTable translationTable) {
19-
super("State Refinement Error", String.format("Expected state '%s' but found '%s'", expected.toSimplifiedString(), found.toSimplifiedString()), null,
20-
element.getPosition(), translationTable);
19+
super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(),
20+
found.toSimplifiedString()), null, position, translationTable);
2121
this.expected = expected.toSimplifiedString();
2222
this.found = found.toSimplifiedString();
2323
}

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

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,8 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
8282

8383
// check if refinement is valid
8484
if (!p.getExpression().isBooleanExpression()) {
85-
throw new InvalidRefinementError(element, "Refinement predicate must be a boolean expression",
86-
ref.get());
85+
throw new InvalidRefinementError(element.getPosition(),
86+
"Refinement predicate must be a boolean expression", ref.get());
8787
}
8888
constr = Optional.of(p);
8989
}
@@ -115,7 +115,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
115115
CtLiteral<String> s = (CtLiteral<String>) ce;
116116
String f = s.getValue();
117117
if (Character.isUpperCase(f.charAt(0))) {
118-
throw new CustomError("State names must start with lowercase", s);
118+
throw new CustomError("State names must start with lowercase", s.getPosition());
119119
}
120120
}
121121
}
@@ -152,7 +152,8 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
152152
GhostDTO gd = RefinementsParser.getGhostDeclaration(string);
153153
if (!gd.paramTypes().isEmpty()) {
154154
throw new CustomError(
155-
"Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann);
155+
"Ghost States have the class as parameter " + "by default, no other parameters are allowed",
156+
ann.getPosition());
156157
}
157158
// Set class as parameter of Ghost
158159
String qn = getQualifiedClassName(element);
@@ -224,8 +225,8 @@ protected void handleAlias(String value, CtElement element) throws LJError {
224225
a.parse(path);
225226
// refinement alias must return a boolean expression
226227
if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
227-
throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression",
228-
value);
228+
throw new InvalidRefinementError(element.getPosition(),
229+
"Refinement alias must return a boolean expression", value);
229230
}
230231
AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
231232
context.addAlias(aw);
@@ -295,16 +296,16 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour
295296
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
296297
}
297298

298-
public void createError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError {
299-
vcChecker.raiseSubtypingError(element, expectedType, foundType);
299+
public void createError(SourcePosition position, Predicate expectedType, Predicate foundType) throws LJError {
300+
vcChecker.raiseSubtypingError(position, expectedType, foundType);
300301
}
301302

302-
public void createSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError {
303-
vcChecker.raiseSameStateError(element, expectedType, klass);
303+
public void createSameStateError(SourcePosition position, Predicate expectedType, String klass) throws LJError {
304+
vcChecker.raiseSameStateError(position, expectedType, klass);
304305
}
305306

306-
public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate expected)
307+
public void createStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected)
307308
throws LJError {
308-
vcChecker.raiseStateMismatchError(element, method, found, expected);
309+
vcChecker.raiseStateMismatchError(position, method, found, expected);
309310
}
310311
}

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

Lines changed: 38 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package liquidjava.processor.refinement_checker;
22

33
import java.util.ArrayList;
4-
import java.util.Arrays;
54
import java.util.List;
65
import java.util.Set;
76
import java.util.Stack;
@@ -18,7 +17,6 @@
1817
import liquidjava.processor.VCImplication;
1918
import liquidjava.processor.context.*;
2019
import liquidjava.rj_language.Predicate;
21-
import liquidjava.rj_language.ast.Expression;
2220
import liquidjava.smt.SMTEvaluator;
2321
import liquidjava.smt.errors.TypeCheckError;
2422
import liquidjava.utils.constants.Keys;
@@ -53,26 +51,26 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
5351
premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
5452
et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
5553
} catch (Exception e) {
56-
throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map);
54+
throw new RefinementError(element.getPosition(), expectedType.getExpression(), premises.simplify(), map);
5755
}
5856

5957
try {
6058
smtChecking(premises, et);
6159
} catch (Exception e) {
6260
// To emit the message we use the constraints before the alias and state change
63-
raiseError(e, premisesBeforeChange, expectedType, element, map);
61+
raiseError(e, element.getPosition(), premisesBeforeChange, expectedType, map);
6462
}
6563
}
6664

6765
public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
6866
Factory f) throws LJError {
6967
boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
7068
if (!b)
71-
raiseSubtypingError(element, expectedType, type);
69+
raiseSubtypingError(element.getPosition(), expectedType, type);
7270
}
7371

74-
public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, SourcePosition p,
75-
Factory f) throws LJError {
72+
public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
73+
SourcePosition position, Factory f) throws LJError {
7674
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
7775
gatherVariables(expectedType, lrv, mainVars);
7876
gatherVariables(type, lrv, mainVars);
@@ -93,7 +91,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
9391
} catch (Exception e) {
9492
return false;
9593
}
96-
return smtChecks(premises, et, p);
94+
return smtChecks(et, premises, position, map);
9795
}
9896

9997
/**
@@ -219,22 +217,14 @@ private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
219217
getVariablesFromContext(l, newVars, varName);
220218
}
221219

222-
public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) throws LJError {
220+
public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position, TranslationTable map)
221+
throws LJError {
223222
try {
224-
new SMTEvaluator().verifySubtype(found, expectedType, context);
223+
new SMTEvaluator().verifySubtype(found, expected, context);
225224
} catch (TypeCheckError e) {
226225
return false;
227-
}
228-
//TODO: handle NotFoundError properly
229-
catch (Exception e) {
230-
String msg = e.getLocalizedMessage().toLowerCase();
231-
if (msg.contains("wrong number of arguments")) {
232-
throw new CustomError("Wrong number of arguments in ghost invocation", p);
233-
} else if (msg.contains("sort mismatch")) {
234-
throw new CustomError("Type mismatch in arguments of ghost invocation", p);
235-
} else {
236-
throw new CustomError(e.getMessage(), p);
237-
}
226+
} catch (Exception e) {
227+
raiseError(e, position, found, expected, map);
238228
}
239229
return true;
240230
}
@@ -274,39 +264,45 @@ private TranslationTable createMap(Predicate expectedType) {
274264
return map;
275265
}
276266

277-
protected void raiseSubtypingError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError {
278-
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
279-
gatherVariables(expectedType, lrv, mainVars);
280-
gatherVariables(foundType, lrv, mainVars);
281-
TranslationTable map = new TranslationTable();
282-
Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
283-
throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map);
284-
}
285-
286-
public void raiseSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError {
287-
TranslationTable map = createMap(expectedType);
288-
throw new StateConflictError(element, expectedType.getExpression(), map);
289-
}
290-
291-
private void raiseError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element,
267+
protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected,
292268
TranslationTable map) throws LJError {
293269
if (e instanceof TypeCheckError) {
294-
throw new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map);
270+
throw new RefinementError(position, expected.getExpression(), found.simplify(), map);
295271
} else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) {
296-
throw new NotFoundError(element, e.getMessage(), nfe.getName(), map);
272+
throw new NotFoundError(position, e.getMessage(), nfe.getName(), nfe.getKind(), map);
297273
} else {
298-
throw new CustomError(e.getMessage(), element);
274+
String msg = e.getLocalizedMessage().toLowerCase();
275+
if (msg.contains("wrong number of arguments")) {
276+
throw new CustomError("Wrong number of arguments in ghost invocation", position);
277+
} else if (msg.contains("sort mismatch")) {
278+
throw new CustomError("Type mismatch in arguments of ghost invocation", position);
279+
} else {
280+
throw new CustomError(e.getMessage(), position);
281+
}
299282
}
300283
}
301284

302-
public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate expected)
285+
protected void raiseSubtypingError(SourcePosition position, Predicate expected, Predicate found) throws LJError {
286+
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
287+
gatherVariables(expected, lrv, mainVars);
288+
gatherVariables(found, lrv, mainVars);
289+
TranslationTable map = new TranslationTable();
290+
Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
291+
throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
292+
}
293+
294+
protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError {
295+
TranslationTable map = createMap(expected);
296+
throw new StateConflictError(position, expected.getExpression(), map);
297+
}
298+
299+
protected void raiseStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected)
303300
throws LJError {
304301
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
305302
gatherVariables(found, lrv, mainVars);
306303
TranslationTable map = new TranslationTable();
307304
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
308-
throw new StateRefinementError(element,
309-
expected.getExpression(),
305+
throw new StateRefinementError(position, expected.getExpression(),
310306
foundState.toConjunctions().simplify().getValue(), map);
311307
}
312308
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
8383
} else {
8484
boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
8585
if (!ok) {
86-
tc.createError(method, argRef, superArgRef);
86+
tc.createError(method.getPosition(), argRef, superArgRef);
8787
}
8888
}
8989
}

0 commit comments

Comments
 (0)