Skip to content

Commit fdd5604

Browse files
rcosta358rcosta358
authored
Add Declaration Location to Refinement Errors (#285)
1 parent cdc46e3 commit fdd5604

8 files changed

Lines changed: 100 additions & 63 deletions

File tree

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

Lines changed: 33 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,10 @@ public SourcePosition getPosition() {
4747
return position;
4848
}
4949

50+
public SourcePosition getDeclarationPosition() {
51+
return null;
52+
}
53+
5054
public void setPosition(SourcePosition pos) {
5155
if (pos == null || pos.getFile() == null)
5256
return;
@@ -91,23 +95,38 @@ public String toString() {
9195
sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n");
9296
}
9397

98+
// declaration position
99+
SourcePosition declPos = getDeclarationPosition();
100+
if (declPos != null && declPos.getFile() != null && !declPos.equals(position)) {
101+
sb.append(Colors.CYAN).append("\n--> Refinement declared here:\n").append(Colors.RESET);
102+
String declarationSnippet = getSnippet(declPos, 1, 0, Colors.CYAN, null, true);
103+
if (declarationSnippet != null) {
104+
sb.append(declarationSnippet);
105+
}
106+
sb.append(declPos.getFile().getPath()).append(":").append(declPos.getLine()).append(Colors.RESET)
107+
.append("\n");
108+
}
109+
94110
return sb.toString();
95111
}
96112

97113
public String getSnippet() {
98-
if (file == null || position == null)
114+
return getSnippet(position, 2, 2, accentColor, customMessage, false);
115+
}
116+
117+
private String getSnippet(SourcePosition snippetPosition, int contextBefore, int contextAfter, String markerColor,
118+
String markerMessage, boolean firstLineOnly) {
119+
if (snippetPosition == null || snippetPosition.getFile() == null)
99120
return null;
100121

101-
Path path = Path.of(file);
122+
Path path = snippetPosition.getFile().toPath();
102123
try {
103124
List<String> lines = Files.readAllLines(path);
104125
StringBuilder sb = new StringBuilder();
105126

106-
// before and after lines for context
107-
int contextBefore = 2;
108-
int contextAfter = 2;
109-
int startLine = Math.max(1, position.getLine() - contextBefore);
110-
int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter);
127+
int startLine = Math.max(1, snippetPosition.getLine() - contextBefore);
128+
int highlightedEndLine = firstLineOnly ? snippetPosition.getLine() : snippetPosition.getEndLine();
129+
int endLine = Math.min(lines.size(), highlightedEndLine + contextAfter);
111130

112131
// calculate padding for line numbers
113132
int padding = String.valueOf(endLine).length();
@@ -121,9 +140,10 @@ public String getSnippet() {
121140
sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
122141

123142
// add error markers on the line(s) with the error
124-
if (i >= position.getLine() && i <= position.getEndLine()) {
125-
int colStart = (i == position.getLine()) ? position.getColumn() : 1;
126-
int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length();
143+
if (i >= snippetPosition.getLine() && i <= highlightedEndLine) {
144+
int colStart = (i == snippetPosition.getLine()) ? snippetPosition.getColumn() : 1;
145+
int colEnd = (i == snippetPosition.getEndLine()) ? snippetPosition.getEndColumn()
146+
: rawLine.length();
127147

128148
if (colStart > 0 && colEnd > 0) {
129149
int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()
@@ -136,13 +156,13 @@ public String getSnippet() {
136156
// line number padding + pipe + column offset
137157
String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
138158
+ " ".repeat(visualColStart - 1);
139-
String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
159+
String markers = markerColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
140160
sb.append(indent).append(markers);
141161

142162
// custom message
143-
if (customMessage != null && !customMessage.isBlank()) {
163+
if (markerMessage != null && !markerMessage.isBlank()) {
144164
String offset = " ".repeat(padding + visualColEnd + PIPE.length() + 1);
145-
sb.append(" " + customMessage.replace("\n", "\n" + offset));
165+
sb.append(" " + markerMessage.replace("\n", "\n" + offset));
146166
}
147167
sb.append(Colors.RESET).append("\n");
148168
}

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

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,11 @@ public class RefinementError extends LJError {
2222
private final Predicate expected;
2323
private final VCSimplificationResult found;
2424
private final Counterexample counterexample;
25+
private final SourcePosition declarationPosition;
2526

26-
public RefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found,
27-
TranslationTable translationTable, Counterexample counterexample, String customMessage) {
27+
public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
28+
VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
29+
String customMessage) {
2830
super("Refinement Error",
2931
String.format("%s is not a subtype of %s",
3032
found.getImplication().toPredicate().getExpression().toDisplayString(),
@@ -33,6 +35,12 @@ public RefinementError(SourcePosition position, Predicate expected, VCSimplifica
3335
this.expected = expected;
3436
this.found = found;
3537
this.counterexample = counterexample;
38+
this.declarationPosition = declarationPosition;
39+
}
40+
41+
@Override
42+
public SourcePosition getDeclarationPosition() {
43+
return declarationPosition;
3644
}
3745

3846
@Override

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

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,25 @@ public class StateRefinementError extends LJError {
1515

1616
private final Predicate expected;
1717
private final VCSimplificationResult found;
18+
private final SourcePosition declarationPosition;
1819

19-
public StateRefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found,
20-
TranslationTable translationTable, String customMessage) {
20+
public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
21+
VCSimplificationResult found, TranslationTable translationTable, String customMessage) {
2122
super("State Refinement Error",
22-
String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(),
23-
found.getImplication().toPredicate().getExpression().toDisplayString()),
23+
String.format("found %s but expected %s",
24+
found.getImplication().toPredicate().getExpression().toDisplayString(),
25+
expected.getExpression().toDisplayString()),
2426
position, translationTable, customMessage);
27+
this.declarationPosition = declarationPosition;
2528
this.expected = expected;
2629
this.found = found;
2730
}
2831

32+
@Override
33+
public SourcePosition getDeclarationPosition() {
34+
return declarationPosition;
35+
}
36+
2937
public Predicate getExpected() {
3038
return expected;
3139
}

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

Lines changed: 15 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -364,22 +364,21 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
364364
rv.addSuperType(t);
365365
context.addRefinementInstanceToVariable(simpleName, newName);
366366
String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null);
367-
checkSMT(cEt, usage, customMessage); // TODO CHANGE
367+
checkSMT(cEt, usage, variable.getPosition(), customMessage); // TODO CHANGE
368368
context.addRefinementToVariableInContext(simpleName, type, cet, usage);
369369
}
370370

371-
public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
372-
checkSMT(expectedType, element, null);
373-
}
374-
375-
public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError {
376-
vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage);
371+
public void checkSMT(Predicate expectedType, CtElement element, SourcePosition declarationPosition,
372+
String customMessage) throws LJError {
373+
vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, declarationPosition,
374+
customMessage);
377375
element.putMetadata(Keys.REFINEMENT, expectedType);
378376
}
379377

380-
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo)
381-
throws LJError {
382-
vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, factory);
378+
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target,
379+
SourcePosition declarationPosition, String moreInfo) throws LJError {
380+
vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, declarationPosition,
381+
factory);
383382
}
384383

385384
public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
@@ -393,14 +392,14 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc
393392
return result.isOk();
394393
}
395394

396-
public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType,
397-
String customMessage) throws LJError {
398-
vcChecker.throwRefinementError(position, expectedType, foundType, null, customMessage);
395+
public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition,
396+
Predicate expectedType, Predicate foundType, String customMessage) throws LJError {
397+
vcChecker.throwRefinementError(position, declarationPosition, expectedType, foundType, null, customMessage);
399398
}
400399

401-
public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
402-
String customMessage) throws LJError {
403-
vcChecker.throwStateRefinementError(position, found, expected, customMessage);
400+
public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
401+
Predicate expected, String customMessage) throws LJError {
402+
vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage);
404403
}
405404

406405
public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

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

Lines changed: 14 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -38,13 +38,8 @@ public VCChecker() {
3838
pathVariables = new Stack<>();
3939
}
4040

41-
public void processSubtyping(Predicate expectedType, List<GhostState> list, CtElement element, Factory f)
42-
throws LJError {
43-
processSubtyping(expectedType, list, element, f, null);
44-
}
45-
4641
public void processSubtyping(Predicate expectedType, List<GhostState> list, CtElement element, Factory f,
47-
String customMessage) throws LJError {
42+
SourcePosition declarationPosition, String customMessage) throws LJError {
4843
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
4944
gatherVariables(expectedType, lrv, mainVars);
5045
if (expectedType.isBooleanTrue())
@@ -82,8 +77,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
8277
}
8378
DebugLog.smtResult(result);
8479
if (result.isError()) {
85-
throw new RefinementError(element.getPosition(), expectedType, implBeforeChange.simplify(), map,
86-
result.getCounterexample(), customMessage);
80+
throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
81+
implBeforeChange.simplify(), map, result.getCounterexample(), customMessage);
8782
}
8883
}
8984

@@ -99,10 +94,11 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
9994
* @throws LJError
10095
*/
10196
public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
102-
Factory f) throws LJError {
97+
SourcePosition declarationPosition, Factory f) throws LJError {
10398
SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
10499
if (result.isError())
105-
throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null);
100+
throwRefinementError(element.getPosition(), declarationPosition, expectedType, type,
101+
result.getCounterexample(), null);
106102
}
107103

108104
/**
@@ -407,18 +403,20 @@ private VCImplication buildPremiseChain(TranslationTable map, Predicate... predi
407403
return joinPredicates(predicates[0], mainVars, lrv, map);
408404
}
409405

410-
protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
411-
Counterexample counterexample, String customMessage) throws RefinementError {
406+
protected void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
407+
Predicate found, Counterexample counterexample, String customMessage) throws RefinementError {
412408
TranslationTable map = new TranslationTable();
413409
VCImplication premises = buildPremiseChain(map, expected, found);
414-
throw new RefinementError(position, expected, premises.simplify(), map, counterexample, customMessage);
410+
throw new RefinementError(position, declarationPosition, expected, premises.simplify(), map, counterexample,
411+
customMessage);
415412
}
416413

417-
protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
418-
String customMessage) throws StateRefinementError {
414+
protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
415+
Predicate found, Predicate expected, String customMessage) throws StateRefinementError {
419416
TranslationTable map = new TranslationTable();
420417
VCImplication foundState = buildPremiseChain(map, expected, found);
421-
throw new StateRefinementError(position, expected, foundState.simplify(), map, customMessage);
418+
throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map,
419+
customMessage);
422420
}
423421

424422
protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
220220
.substituteVariable(Keys.THIS, returnVarName);
221221

222222
rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
223-
rtc.checkSMT(cexpectedType, ret, fi.getMessage());
223+
rtc.checkSMT(cexpectedType, ret, fi.getPlacementInCode().getPosition(), fi.getMessage());
224224
rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
225225

226226
}
@@ -426,7 +426,7 @@ private void checkParameters(CtElement invocation, List<CtExpression<?>> argumen
426426
VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET);
427427
c = c.substituteVariable(Keys.THIS, vi.getName());
428428
}
429-
rtc.checkSMT(c, invocation, fArg.getMessage());
429+
rtc.checkSMT(c, invocation, fArg.getPlacementInCode().getPosition(), fArg.getMessage());
430430
}
431431
}
432432

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,8 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
8383
} else {
8484
boolean ok = tc.checkStateSMT(superArgRef, argRef, params.get(i).getPosition());
8585
if (!ok) {
86-
tc.throwRefinementError(method.getPosition(), argRef, superArgRef, function.getMessage());
86+
tc.throwRefinementError(method.getPosition(), function.getPlacementInCode().getPosition(), argRef,
87+
superArgRef, function.getMessage());
8788
}
8889
}
8990
}
@@ -107,7 +108,7 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct
107108
for (String m : super2function.keySet())
108109
functionRef = functionRef.substituteVariable(m, super2function.get(m));
109110

110-
tc.checkStateSMT(functionRef, superRef, method,
111+
tc.checkStateSMT(functionRef, superRef, method, function.getPlacementInCode().getPosition(),
111112
"Return of subclass must be subtype of the return of the superclass");
112113
}
113114
}
@@ -143,13 +144,13 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
143144
Predicate subConst = matchVariableNames(thisName, superFunction, subFunction, subState.getFrom());
144145

145146
// fromSup <: fromSub <==> fromSup is sub type and fromSub is expectedType
146-
tc.checkStateSMT(superConst, subConst, method,
147+
tc.checkStateSMT(superConst, subConst, method, subFunction.getPlacementInCode().getPosition(),
147148
"FROM State from Superclass must be subtype of FROM State from Subclass");
148149

149150
superConst = matchVariableNames(thisName, superState.getTo());
150151
subConst = matchVariableNames(thisName, superFunction, subFunction, subState.getTo());
151152
// toSub <: toSup <==> ToSub is sub type and toSup is expectedType
152-
tc.checkStateSMT(subConst, superConst, method,
153+
tc.checkStateSMT(subConst, superConst, method, superFunction.getPlacementInCode().getPosition(),
153154
"TO State from Subclass must be subtype of TO State from Superclass");
154155

155156
}

0 commit comments

Comments
 (0)