Skip to content

Commit 19b2049

Browse files
rcosta358rcosta358
committed
Error Updates
1 parent 308ad81 commit 19b2049

File tree

12 files changed

+57
-74
lines changed

12 files changed

+57
-74
lines changed

‎liquidjava-verifier/pom.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111

1212
<groupId>io.github.liquid-java</groupId>
1313
<artifactId>liquidjava-verifier</artifactId>
14-
<version>0.0.2</version>
14+
<version>0.0.3</version>
1515
<name>liquidjava-verifier</name>
1616
<description>LiquidJava Verifier</description>
1717
<url>https://github.com/liquid-java/liquidjava</url>

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ public LJDiagnostic(String title, String message, String details, SourcePosition
1919
this.title = title;
2020
this.message = message;
2121
this.details = details;
22-
this.file = pos != null ? pos.getFile().getPath() : null;
22+
this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
2323
this.position = ErrorPosition.fromSpoonPosition(pos);
2424
this.accentColor = accentColor;
2525
}
@@ -44,6 +44,10 @@ public String getFile() {
4444
return file;
4545
}
4646

47+
public String getAccentColor() {
48+
return accentColor;
49+
}
50+
4751
@Override
4852
public String toString() {
4953
StringBuilder sb = new StringBuilder();

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

Lines changed: 0 additions & 25 deletions
This file was deleted.

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

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

33
import liquidjava.diagnostics.TranslationTable;
4+
import liquidjava.utils.Utils;
45
import spoon.reflect.declaration.CtElement;
56

67
/**
@@ -9,8 +10,15 @@
910
* @see LJError
1011
*/
1112
public class NotFoundError extends LJError {
13+
14+
private final String name;
1215

13-
public NotFoundError(CtElement element, String message, TranslationTable translationTable) {
16+
public NotFoundError(CtElement element, String message, String name, TranslationTable translationTable) {
1417
super("Not Found Error", message, "", element.getPosition(), translationTable);
18+
this.name = Utils.getSimpleName(name);
19+
}
20+
21+
public String getName() {
22+
return name;
1523
}
1624
}

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

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,22 +11,16 @@
1111
*/
1212
public class StateConflictError extends LJError {
1313

14-
private final String state;
15-
private final String className;
14+
private final String state;;
1615

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

2523
public String getState() {
2624
return state;
2725
}
28-
29-
public String getClassName() {
30-
return className;
31-
}
3226
}

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

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

3-
import java.util.Arrays;
4-
53
import liquidjava.diagnostics.TranslationTable;
64
import liquidjava.rj_language.ast.Expression;
75
import spoon.reflect.declaration.CtElement;
@@ -13,28 +11,18 @@
1311
*/
1412
public class StateRefinementError extends LJError {
1513

16-
private final String method;
17-
private final String[] expected;
14+
private final String expected;
1815
private final String found;
1916

20-
public StateRefinementError(CtElement element, String method, Expression[] expected, Expression found,
17+
public StateRefinementError(CtElement element, Expression expected, Expression found,
2118
TranslationTable translationTable) {
22-
super("State Refinement Error", "State refinement transition violation",
23-
String.format("Expected: %s\nFound: %s",
24-
String.join(", ",
25-
Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new)),
26-
found.toSimplifiedString()),
19+
super("State Refinement Error", String.format("Expected state '%s' but found '%s'", expected.toSimplifiedString(), found.toSimplifiedString()), null,
2720
element.getPosition(), translationTable);
28-
this.method = method;
29-
this.expected = Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new);
21+
this.expected = expected.toSimplifiedString();
3022
this.found = found.toSimplifiedString();
3123
}
3224

33-
public String getMethod() {
34-
return method;
35-
}
36-
37-
public String[] getExpected() {
25+
public String getExpected() {
3826
return expected;
3927
}
4028

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -303,7 +303,7 @@ public void createSameStateError(CtElement element, Predicate expectedType, Stri
303303
vcChecker.raiseSameStateError(element, expectedType, klass);
304304
}
305305

306-
public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected)
306+
public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate expected)
307307
throws LJError {
308308
vcChecker.raiseStateMismatchError(element, method, found, expected);
309309
}

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

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
import java.util.stream.Collectors;
1010

1111
import liquidjava.diagnostics.errors.CustomError;
12-
import liquidjava.diagnostics.errors.GhostInvocationError;
1312
import liquidjava.diagnostics.errors.LJError;
1413
import liquidjava.diagnostics.errors.NotFoundError;
1514
import liquidjava.diagnostics.TranslationTable;
@@ -225,14 +224,14 @@ public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition
225224
new SMTEvaluator().verifySubtype(found, expectedType, context);
226225
} catch (TypeCheckError e) {
227226
return false;
228-
} catch (Exception e) {
227+
}
228+
//TODO: handle NotFoundError properly
229+
catch (Exception e) {
229230
String msg = e.getLocalizedMessage().toLowerCase();
230231
if (msg.contains("wrong number of arguments")) {
231-
throw new GhostInvocationError("Wrong number of arguments in ghost invocation", p,
232-
expectedType.getExpression(), null);
232+
throw new CustomError("Wrong number of arguments in ghost invocation", p);
233233
} else if (msg.contains("sort mismatch")) {
234-
throw new GhostInvocationError("Type mismatch in arguments of ghost invocation", p,
235-
expectedType.getExpression(), null);
234+
throw new CustomError("Type mismatch in arguments of ghost invocation", p);
236235
} else {
237236
throw new CustomError(e.getMessage(), p);
238237
}
@@ -286,28 +285,28 @@ protected void raiseSubtypingError(CtElement element, Predicate expectedType, Pr
286285

287286
public void raiseSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError {
288287
TranslationTable map = createMap(expectedType);
289-
throw new StateConflictError(element, expectedType.getExpression(), klass, map);
288+
throw new StateConflictError(element, expectedType.getExpression(), map);
290289
}
291290

292291
private void raiseError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element,
293292
TranslationTable map) throws LJError {
294293
if (e instanceof TypeCheckError) {
295294
throw new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map);
296-
} else if (e instanceof liquidjava.smt.errors.NotFoundError) {
297-
throw new NotFoundError(element, e.getMessage(), map);
295+
} else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) {
296+
throw new NotFoundError(element, e.getMessage(), nfe.getName(), map);
298297
} else {
299298
throw new CustomError(e.getMessage(), element);
300299
}
301300
}
302301

303-
public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states)
302+
public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate expected)
304303
throws LJError {
305304
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
306305
gatherVariables(found, lrv, mainVars);
307306
TranslationTable map = new TranslationTable();
308307
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
309-
throw new StateRefinementError(element, method,
310-
Arrays.stream(states).map(Predicate::getExpression).toArray(Expression[]::new),
308+
throw new StateRefinementError(element,
309+
expected.getExpression(),
311310
foundState.toConjunctions().simplify().getValue(), map);
312311
}
313312
}

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -406,8 +406,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
406406
.changeOldMentions(vi.getName(), instanceName);
407407

408408
if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
409-
Predicate[] states = { stateChange.getFrom() };
410-
tc.createStateMismatchError(fw, fw.toString(), prevState, states);
409+
tc.createStateMismatchError(fw, fw.toString(), prevState, stateChange.getFrom());
411410
return;
412411
}
413412

@@ -486,10 +485,10 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
486485
}
487486
}
488487
if (!found) { // Reaches the end of stateChange no matching states
489-
Predicate[] states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
490-
.toArray(Predicate[]::new);
488+
Predicate expectedStatesDisjunction = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
489+
.reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction);
491490
String simpleInvocation = invocation.toString();
492-
tc.createStateMismatchError(invocation, simpleInvocation, prevState, states);
491+
tc.createStateMismatchError(invocation, simpleInvocation, prevState, expectedStatesDisjunction);
493492
}
494493
}
495494

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,15 @@ public static Predicate createConjunction(Predicate c1, Predicate c2) {
204204
return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression()));
205205
}
206206

207+
public static Predicate createDisjunction(Predicate c1, Predicate c2) {
208+
// simplification: (false || x) = x, (true || x) = true
209+
if (isBooleanLiteral(c1.getExpression(), false)) return c2;
210+
if (isBooleanLiteral(c2.getExpression(), false)) return c1;
211+
if (isBooleanLiteral(c1.getExpression(), true)) return c1;
212+
if (isBooleanLiteral(c2.getExpression(), true)) return c2;
213+
return new Predicate(new BinaryExpression(c1.getExpression(), Ops.OR, c2.getExpression()));
214+
}
215+
207216
public static Predicate createEquals(Predicate c1, Predicate c2) {
208217
return new Predicate(new BinaryExpression(c1.getExpression(), Ops.EQ, c2.getExpression()));
209218
}

0 commit comments

Comments
 (0)