Skip to content

Commit 461bcef

Browse files
rcosta358rcosta358
committed
Update Error Constructors
1 parent 57f5ae4 commit 461bcef

File tree

7 files changed

+41
-43
lines changed

7 files changed

+41
-43
lines changed

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,12 @@ public class ErrorEmitter {
1212
private URI filePath;
1313
private ErrorPosition position;
1414
private int errorStatus;
15-
private HashMap<String, PlacementInCode> map;
15+
private TranslationTable map;
1616

1717
public ErrorEmitter() {
1818
}
1919

20-
public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus,
21-
HashMap<String, PlacementInCode> map) {
20+
public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus, TranslationTable map) {
2221
this.titleMessage = titleMessage;
2322
fullMessage = msg;
2423
try {
@@ -86,7 +85,7 @@ public int getErrorStatus() {
8685
return errorStatus;
8786
}
8887

89-
public HashMap<String, PlacementInCode> getVCMap() {
88+
public TranslationTable getVCMap() {
9089
return map;
9190
}
9291
}

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ public class ErrorHandler {
3737
// }
3838

3939
public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
40-
String states, HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
40+
String states, TranslationTable map, ErrorEmitter ee) {
4141

4242
String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
4343
// Found
@@ -66,7 +66,7 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
6666
}
6767

6868
public static <T> void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
69-
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
69+
TranslationTable map, ErrorEmitter ee) {
7070

7171
String resumeMessage = "Encountered unknown variable";
7272

@@ -85,7 +85,7 @@ public static <T> void printErrorUnknownVariable(CtElement var, String et, Strin
8585
}
8686

8787
public static <T> void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
88-
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
88+
TranslationTable map, ErrorEmitter ee) {
8989

9090
StringBuilder sb = new StringBuilder();
9191
sb.append("______________________________________________________\n");
@@ -101,8 +101,8 @@ public static <T> void printNotFound(CtElement var, Predicate constraint, Predic
101101
ee.addError(msg, sb.toString(), var.getPosition(), 2, map);
102102
}
103103

104-
public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg,
105-
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
104+
public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg, TranslationTable map,
105+
ErrorEmitter ee) {
106106
StringBuilder sb = new StringBuilder();
107107
sb.append("______________________________________________________\n");
108108
String title = "Error in ghost invocation: " + msg + "\n";
@@ -116,7 +116,7 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
116116
}
117117

118118
public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
119-
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
119+
TranslationTable map, ErrorEmitter ee) {
120120
StringBuilder sb = new StringBuilder();
121121
sb.append("______________________________________________________\n");
122122
sb.append(message + "\n\n");
@@ -128,8 +128,8 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT
128128
ee.addError(message, sb.toString(), element.getPosition(), 2, map);
129129
}
130130

131-
public static void printSameStateSetError(CtElement element, Predicate p, String name,
132-
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
131+
public static void printSameStateSetError(CtElement element, Predicate p, String name, TranslationTable map,
132+
ErrorEmitter ee) {
133133
String resume = "Error found multiple disjoint states from a State Set in a refinement";
134134

135135
StringBuilder sb = new StringBuilder();
@@ -210,7 +210,7 @@ private static String printLine() {
210210
return sb.toString();
211211
}
212212

213-
private static String printMap(HashMap<String, PlacementInCode> map) {
213+
private static String printMap(TranslationTable map) {
214214
StringBuilder sb = new StringBuilder();
215215
Formatter formatter = new Formatter(sb, Locale.US);
216216
if (map.isEmpty()) {

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

Lines changed: 3 additions & 2 deletions
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.rj_language.Predicate;
45
import spoon.reflect.declaration.CtElement;
56

67
/**
@@ -12,10 +13,10 @@ public class GhostInvocationError extends LJError {
1213

1314
private String expected;
1415

15-
public GhostInvocationError(CtElement element, String expected, TranslationTable translationTable) {
16+
public GhostInvocationError(CtElement element, Predicate expected, TranslationTable translationTable) {
1617
super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element,
1718
translationTable);
18-
this.expected = expected;
19+
this.expected = expected.toString();
1920
}
2021

2122
public String getExpected() {

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

Lines changed: 3 additions & 2 deletions
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.rj_language.Predicate;
45
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
56
import liquidjava.utils.Utils;
67
import spoon.reflect.declaration.CtElement;
@@ -15,11 +16,11 @@ public class RefinementError extends LJError {
1516
private String expected;
1617
private ValDerivationNode found;
1718

18-
public RefinementError(CtElement element, String expected, ValDerivationNode found,
19+
public RefinementError(CtElement element, Predicate expected, ValDerivationNode found,
1920
TranslationTable translationTable) {
2021
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element,
2122
translationTable);
22-
this.expected = expected;
23+
this.expected = expected.toString();
2324
this.found = found;
2425
}
2526

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

Lines changed: 4 additions & 5 deletions
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.rj_language.Predicate;
45
import spoon.reflect.declaration.CtElement;
56

67
/**
@@ -13,11 +14,9 @@ public class StateConflictError extends LJError {
1314
private String state;
1415
private String className;
1516

16-
public StateConflictError(CtElement element, String state, String className, TranslationTable translationTable) {
17-
super("State Conflict Error",
18-
"Found multiple disjoint states in state transition — State transition can only go to one state of each state set",
19-
element, translationTable);
20-
this.state = state;
17+
public StateConflictError(CtElement element, Predicate state, String className, TranslationTable translationTable) {
18+
super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element, translationTable);
19+
this.state = state.toString();
2120
this.className = className;
2221
}
2322

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import java.util.Arrays;
44

55
import liquidjava.diagnostics.TranslationTable;
6+
import liquidjava.rj_language.Predicate;
67
import spoon.reflect.declaration.CtElement;
78

89
/**
@@ -16,12 +17,12 @@ public class StateRefinementError extends LJError {
1617
private final String[] expected;
1718
private final String found;
1819

19-
public StateRefinementError(CtElement element, String method, String[] expected, String found,
20+
public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found,
2021
TranslationTable translationTable) {
2122
super("State Refinement Error", "State refinement transition violation", element, translationTable);
2223
this.method = method;
23-
this.expected = expected;
24-
this.found = found;
24+
this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new);
25+
this.found = found.toString();
2526
}
2627

2728
public String getMethod() {

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

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
import liquidjava.diagnostics.ErrorEmitter;
1515
import liquidjava.diagnostics.ErrorHandler;
1616
import liquidjava.diagnostics.errors.LJError;
17+
import liquidjava.diagnostics.TranslationTable;
1718
import liquidjava.diagnostics.errors.RefinementError;
1819
import liquidjava.diagnostics.errors.StateRefinementError;
1920
import liquidjava.processor.VCImplication;
@@ -48,7 +49,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
4849
if (expectedType.isBooleanTrue())
4950
return;
5051

51-
HashMap<String, PlacementInCode> map = new HashMap<>();
52+
TranslationTable map = new TranslationTable();
5253
String[] s = { Keys.WILDCARD, Keys.THIS };
5354
Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
5455
Predicate premises = new Predicate();
@@ -60,7 +61,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
6061

6162
et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f);
6263
} catch (Exception e) {
63-
diagnostics.add(new RefinementError(element, expectedType, premises.simplify()));
64+
diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map));
6465
// ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter);
6566
return;
6667
}
@@ -89,7 +90,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
8990
return true;
9091

9192
// Predicate premises = joinPredicates(type, element, mainVars, lrv);
92-
HashMap<String, PlacementInCode> map = new HashMap<>();
93+
TranslationTable map = new TranslationTable();
9394
String[] s = { Keys.WILDCARD, Keys.THIS };
9495

9596
Predicate premises = new Predicate();
@@ -152,7 +153,7 @@ private List<GhostState> filterGhostStatesForVariables(List<GhostState> list, Li
152153
}
153154

154155
private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
155-
List<RefinedVariable> vars, HashMap<String, PlacementInCode> map) {
156+
List<RefinedVariable> vars, TranslationTable map) {
156157

157158
VCImplication firstSi = null;
158159
VCImplication lastSi = null;
@@ -192,7 +193,7 @@ private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariabl
192193
return cSMT; // firstSi != null ? firstSi : new VCImplication(new Predicate());
193194
}
194195

195-
private void addMap(RefinedVariable var, HashMap<String, PlacementInCode> map) {
196+
private void addMap(RefinedVariable var, TranslationTable map) {
196197
map.put(var.getName(), var.getPlacementInCode());
197198
// if(var instanceof VariableInstance) {
198199
// VariableInstance vi = (VariableInstance) var;
@@ -313,10 +314,10 @@ void removePathVariableThatIncludes(String otherVar) {
313314

314315
// Errors---------------------------------------------------------------------------------------------------
315316

316-
private HashMap<String, PlacementInCode> createMap(CtElement element, Predicate expectedType) {
317+
private TranslationTable createMap(CtElement element, Predicate expectedType) {
317318
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
318319
gatherVariables(expectedType, lrv, mainVars);
319-
HashMap<String, PlacementInCode> map = new HashMap<>();
320+
TranslationTable map = new TranslationTable();
320321
joinPredicates(expectedType, mainVars, lrv, map);
321322
return map;
322323
}
@@ -326,20 +327,20 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr
326327
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
327328
gatherVariables(expectedType, lrv, mainVars);
328329
gatherVariables(foundType, lrv, mainVars);
329-
HashMap<String, PlacementInCode> map = new HashMap<>();
330+
TranslationTable map = new TranslationTable();
330331
Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
331332

332-
diagnostics.add(new RefinementError(element, expectedType, premises.simplify()));
333+
diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map));
333334
// ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter);
334335
}
335336

336337
public void printSameStateError(CtElement element, Predicate expectedType, String klass) {
337-
HashMap<String, PlacementInCode> map = createMap(element, expectedType);
338+
TranslationTable map = createMap(element, expectedType);
338339
ErrorHandler.printSameStateSetError(element, expectedType, klass, map, errorEmitter);
339340
}
340341

341342
private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element,
342-
HashMap<String, PlacementInCode> map) {
343+
TranslationTable map) {
343344
String s = null;
344345
if (element instanceof CtInvocation) {
345346
CtInvocation<?> ci = (CtInvocation<?>) element;
@@ -354,7 +355,7 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
354355
// Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);
355356
// Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map);
356357
if (e instanceof TypeCheckError) {
357-
diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify()));
358+
diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map));
358359
// ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter);
359360
} else if (e instanceof GhostFunctionError) {
360361
ErrorHandler.printErrorArgs(element, expectedType, e.getMessage(), map, errorEmitter);
@@ -373,13 +374,9 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
373374
public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) {
374375
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
375376
gatherVariables(found, lrv, mainVars);
376-
HashMap<String, PlacementInCode> map = new HashMap<>();
377+
TranslationTable map = new TranslationTable();
377378
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
378-
String[] expectedStates = Arrays.stream(states).toArray(String[]::new);
379-
380-
LJError error = new StateRefinementError(element, method, expectedStates, foundState.toString());
381-
error.setTranslationTable(map);
382-
diagnostics.add(error);
379+
diagnostics.add(new StateRefinementError(element, method, states, foundState.toConjunctions(), map));
383380
// ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter);
384381
}
385382
}

0 commit comments

Comments
 (0)