Skip to content

Commit 360b5bb

Browse files
standardize error messages inside latte
1 parent b7bfb55 commit 360b5bb

7 files changed

Lines changed: 39 additions & 26 deletions

File tree

latte-umbrella/src/main/java/latte/latte_umbrella/App.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ public static void launcher(String filePath) {
9595
CtElement ce = e.getElement();
9696
SourcePosition sp = ce.getPosition();
9797
JsonError error = new JsonError(sp.getLine(), sp.getColumn(),
98-
sp.getEndLine(), sp.getEndColumn(), e.getMessage());
98+
sp.getEndLine(), sp.getEndColumn(), e.getMessage(), e.getShortMessage());
9999
String json = new Gson().toJson(error); // using Gson to convert object to JSON
100100
System.err.println(json);
101101

latte-umbrella/src/main/java/latte/latte_umbrella/JsonError.java

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,16 @@ public class JsonError {
55
private int startColumn;
66
private int endLine;
77
private int endColumn;
8-
private String message;
8+
private String shortMessage;
9+
private String fullMessage;
910

10-
public JsonError(int startLine, int startColumn, int endLine, int endColumn, String message) {
11+
public JsonError(int startLine, int startColumn, int endLine, int endColumn, String fullMessage, String shortMessage) {
1112
this.startLine = startLine;
1213
this.startColumn = startColumn;
1314
this.endLine = endLine;
1415
this.endColumn = endColumn;
15-
this.message = message;
16+
this.shortMessage = shortMessage;
17+
this.fullMessage = fullMessage;
1618
}
1719

1820
// Getters and setters (optional if you're using a serialization library)
@@ -32,7 +34,11 @@ public int getEndColumn() {
3234
return endColumn;
3335
}
3436

35-
public String getMessage() {
36-
return message;
37+
public String getShortMessage() {
38+
return shortMessage;
39+
}
40+
41+
public String getFullMessage() {
42+
return fullMessage;
3743
}
3844
}

latte-umbrella/src/main/java/typechecking/LatteChecker.java renamed to latte-umbrella/src/main/java/typechecking/LatteAbstractChecker.java

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@
99
import spoon.reflect.declaration.CtElement;
1010
import spoon.reflect.visitor.CtScanner;
1111

12-
abstract class LatteChecker extends CtScanner{
12+
abstract class LatteAbstractChecker extends CtScanner{
1313
SymbolicEnvironment symbEnv;
1414
PermissionEnvironment permEnv;
1515
ClassLevelMaps maps;
16-
private static Logger logger = LoggerFactory.getLogger(LatteChecker.class);
16+
private static Logger logger = LoggerFactory.getLogger(LatteAbstractChecker.class);
1717

1818
final String THIS = "this";
1919

@@ -23,7 +23,7 @@ abstract class LatteChecker extends CtScanner{
2323

2424
int loggingSpaces = 0;
2525

26-
public LatteChecker( SymbolicEnvironment symbEnv,
26+
public LatteAbstractChecker( SymbolicEnvironment symbEnv,
2727
PermissionEnvironment permEnv, ClassLevelMaps maps) {
2828
this.symbEnv = symbEnv;
2929
this.permEnv = permEnv;
@@ -68,7 +68,7 @@ protected void logError(String text, CtElement ce) throws LatteException {
6868
.append("\tFile: ")
6969
.append(filePath).append(":").append(line).append(":").append(column).append("\n"); // Clickable format
7070

71-
throw new LatteException(sb.toString(), ce);
71+
throw new LatteException(sb.toString(), text, ce);
7272
}
7373

7474
/**

latte-umbrella/src/main/java/typechecking/LatteClassFirstPass.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
import spoon.reflect.declaration.CtMethod;
1212
import spoon.reflect.reference.CtTypeReference;
1313

14-
public class LatteClassFirstPass extends LatteChecker{
14+
public class LatteClassFirstPass extends LatteAbstractChecker{
1515

1616
public LatteClassFirstPass(SymbolicEnvironment se, PermissionEnvironment pe,
1717
ClassLevelMaps mtc) {

latte-umbrella/src/main/java/typechecking/LatteException.java

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

55
public class LatteException extends RuntimeException {
66
private CtElement ce;
7-
public LatteException(String message, CtElement ce) {
8-
super(message);
7+
private String shortMessage;
8+
public LatteException(String shortMessage, String fullMessage, CtElement ce) {
9+
super(fullMessage);
910
this.ce = ce;
1011
}
1112

@@ -15,4 +16,8 @@ public LatteException(String message, CtElement ce) {
1516
public CtElement getElement(){
1617
return ce;
1718
}
19+
20+
public String getShortMessage(){
21+
return shortMessage;
22+
}
1823
}

latte-umbrella/src/main/java/typechecking/LatteTypeChecker.java

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@
3939
* In the type checker we go through the code, add metadata regarding the types and their permissions
4040
* and check if the code is well-typed
4141
*/
42-
public class LatteTypeChecker extends LatteChecker {
42+
public class LatteTypeChecker extends LatteAbstractChecker {
4343

4444
public LatteTypeChecker( SymbolicEnvironment symbEnv,
4545
PermissionEnvironment permEnv, ClassLevelMaps mtc) {
@@ -226,8 +226,8 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
226226
logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA));
227227
// Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′
228228
if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA))
229-
logError(String.format("Constructor argument %s expected an assignment with permission %s but got %s from %s",
230-
p.getSimpleName(), expectedUA, permEnv.get(vv), vv), arg);
229+
logError(String.format("Expected %s but got %s from %s", expectedUA, vvPerm, vv), arg);
230+
231231
paramSymbValues.add(vv);
232232
}
233233

@@ -262,8 +262,9 @@ private void handleInvocation(CtInvocation<?> value, CtVariableWriteImpl<?> assi
262262
UniquenessAnnotation valuePerm = permEnv.get(valueSV);
263263
UniquenessAnnotation targetPerm = permEnv.get(targetSV);
264264
if (!permEnv.usePermissionAs(valueSV, valuePerm, targetPerm))
265-
logError(String.format("%s expected an assignment with permission %s but got %s:%s",
266-
assignee, targetPerm, valueSV, valuePerm), value);
265+
// logError(String.format("%s expected an assignment with permission %s but got %s:%s",
266+
// assignee, targetPerm, valueSV, valuePerm), value);
267+
logError(String.format("Expected %s but got %s in %s", targetPerm, valuePerm, value), value);
267268
SymbolicValue fresh = symbEnv.addVariable(assignee.getVariable().getSimpleName());
268269
permEnv.add(fresh, targetPerm);
269270
}
@@ -456,9 +457,10 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) {
456457

457458
// Check if we can use the permission of vv as the permission of the field
458459
if (!permEnv.usePermissionAs(vv, vvPerm, fieldPerm))
459-
logError(String.format("Field %s expected an assignment with permission %s but got %s from %s",
460-
f.getSimpleName(), fieldPerm, vvPerm, vv, assignment), assignment);
461-
460+
// logError(String.format("Field %s expected an assignment with permission %s but got %s from %s", f.getSimpleName(), fieldPerm, vvPerm, vv, assignment), assignment);
461+
logError(String.format("Expected %s but got %s from %s",
462+
fieldPerm, vvPerm, assignment), assignment);
463+
462464
// Δ′′ [𝜈.𝑓 → 𝜈′]; Σ′′′ ⪰ Δ′′′; Σ′′′′
463465
symbEnv.addFieldSymbolicValue(v, f.getSimpleName(), vv);
464466
}
@@ -502,8 +504,8 @@ private void handleConstructorArgs (CtConstructorCall<?> constCall){
502504
logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA));
503505
// Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′
504506
if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA))
505-
logError(String.format("Constructor argument %s expected an assignment with permission %s but got %s from %s",
506-
p.getSimpleName(), expectedUA, permEnv.get(vv), vv), arg);
507+
logError(String.format("Expected %s but got %s from %s",
508+
expectedUA, vvPerm, vv), arg);
507509
paramSymbValues.add(vv);
508510
}
509511

@@ -567,7 +569,7 @@ public <R> void visitCtReturn(CtReturn<R> returnStatement) {
567569
UniquenessAnnotation expectedUA = new UniquenessAnnotation(cmet);
568570

569571
if(!permEnv.usePermissionAs(vRet, ua, expectedUA)){
570-
logError(String.format("Return value expected %s but got %s in %s",
572+
logError(String.format("Expected %s but got %s in return %s",
571573
expectedUA, ua, returnStatement.toString()), returned);
572574
}
573575
}

latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ public void testMyNode(){
2323
App.launcher("src/test/examples/MyNode.java");
2424
} catch (Exception e) {
2525
assertTrue(e instanceof LatteException);
26-
assertTrue(e.getMessage().contains("expected an assignment with permission UNIQUE but got BORROWED"));
26+
assertTrue(e.getMessage().contains("UNIQUE but got BORROWED"));
2727
}
2828

2929
}
@@ -73,7 +73,7 @@ public void testSmallestIncorrectExample(){
7373
App.launcher("src/test/examples/SmallestIncorrectExample.java");
7474
} catch (Exception e) {
7575
assertTrue(e instanceof LatteException);
76-
assertTrue(e.getMessage().contains("expected an assignment with permission UNIQUE but got BORROWED"));
76+
assertTrue(e.getMessage().contains("UNIQUE but got BORROWED"));
7777
}
7878

7979
}

0 commit comments

Comments
 (0)