Skip to content

Commit 6c8b204

Browse files
rcosta358rcosta358
committed
Add Declaration Location to Refinement Errors
1 parent d91f256 commit 6c8b204

8 files changed

Lines changed: 78 additions & 50 deletions

File tree

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

Lines changed: 11 additions & 0 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,6 +95,13 @@ 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("↳ ").append(declPos.getFile().getPath()).append(":").append(declPos.getLine())
102+
.append(Colors.RESET).append("\n");
103+
}
104+
94105
return sb.toString();
95106
}
96107

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

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

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

3947
@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
@@ -362,22 +362,21 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
362362
rv.addSuperType(t);
363363
context.addRefinementInstanceToVariable(simpleName, newName);
364364
String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null);
365-
checkSMT(cEt, usage, customMessage); // TODO CHANGE
365+
checkSMT(cEt, usage, variable.getPosition(), customMessage); // TODO CHANGE
366366
context.addRefinementToVariableInContext(simpleName, type, cet, usage);
367367
}
368368

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

378-
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo)
379-
throws LJError {
380-
vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, factory);
376+
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target,
377+
SourcePosition declarationPosition, String moreInfo) throws LJError {
378+
vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, declarationPosition,
379+
factory);
381380
}
382381

383382
public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
@@ -391,14 +390,14 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc
391390
return result.isOk();
392391
}
393392

394-
public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType,
395-
String customMessage) throws LJError {
396-
vcChecker.throwRefinementError(position, expectedType, foundType, null, customMessage);
393+
public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition,
394+
Predicate expectedType, Predicate foundType, String customMessage) throws LJError {
395+
vcChecker.throwRefinementError(position, declarationPosition, expectedType, foundType, null, customMessage);
397396
}
398397

399-
public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
400-
String customMessage) throws LJError {
401-
vcChecker.throwStateRefinementError(position, found, expected, customMessage);
398+
public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
399+
Predicate expected, String customMessage) throws LJError {
400+
vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage);
402401
}
403402

404403
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
/**
@@ -403,18 +399,20 @@ private VCImplication buildPremiseChain(TranslationTable map, Predicate... predi
403399
return joinPredicates(predicates[0], mainVars, lrv, map);
404400
}
405401

406-
protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
407-
Counterexample counterexample, String customMessage) throws RefinementError {
402+
protected void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
403+
Predicate found, Counterexample counterexample, String customMessage) throws RefinementError {
408404
TranslationTable map = new TranslationTable();
409405
VCImplication premises = buildPremiseChain(map, expected, found);
410-
throw new RefinementError(position, expected, premises.simplify(), map, counterexample, customMessage);
406+
throw new RefinementError(position, declarationPosition, expected, premises.simplify(), map, counterexample,
407+
customMessage);
411408
}
412409

413-
protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
414-
String customMessage) throws StateRefinementError {
410+
protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
411+
Predicate found, Predicate expected, String customMessage) throws StateRefinementError {
415412
TranslationTable map = new TranslationTable();
416413
VCImplication foundState = buildPremiseChain(map, expected, found);
417-
throw new StateRefinementError(position, expected, foundState.simplify(), map, customMessage);
414+
throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map,
415+
customMessage);
418416
}
419417

420418
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
}

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

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -373,7 +373,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre
373373
VariableInstance target = getTarget(invocation);
374374
if (target != null) {
375375
if (f.hasStateChange() && !f.getFromStates().isEmpty()) {
376-
changeState(tc, target, f.getAllStates(), parentTargetName, map, invocation);
376+
changeState(tc, target, f, parentTargetName, map, invocation);
377377
}
378378
if (!f.hasStateChange()) {
379379
sameState(tc, target, parentTargetName, invocation);
@@ -428,7 +428,8 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
428428
.changeOldMentions(vi.getName(), instanceName);
429429

430430
if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
431-
tc.throwStateRefinementError(fw.getPosition(), prevState, expectState, stateChange.getMessage());
431+
tc.throwStateRefinementError(fw.getPosition(), field.getDeclaringType().getPosition(), prevState,
432+
expectState, stateChange.getMessage());
432433
return;
433434
}
434435

@@ -451,7 +452,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
451452
// is a subtype of the variable's main refinement
452453
if (rv instanceof Variable) {
453454
Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
454-
tc.checkSMT(superC, fw);
455+
tc.checkSMT(superC, fw, rv.getPlacementInCode().getPosition(), null);
455456
tc.getContext().addRefinementInstanceToVariable(parentTargetName, newInstanceName);
456457
}
457458
}
@@ -466,11 +467,12 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
466467
* @param map
467468
* @param invocation
468469
*/
469-
private static void changeState(TypeChecker tc, VariableInstance vi, List<ObjectState> stateChanges, String name,
470+
private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunction function, String name,
470471
Map<String, String> map, CtElement invocation) throws LJError {
471472
if (vi.getRefinement() == null) {
472473
return;
473474
}
475+
List<ObjectState> stateChanges = function.getAllStates();
474476
String instanceName = vi.getName();
475477
Predicate prevState = vi.getRefinement().substituteVariable(Keys.WILDCARD, instanceName)
476478
.substituteVariable(name, instanceName);
@@ -520,7 +522,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
520522
// combine messages of all state changes
521523
String message = stateChanges.stream().map(ObjectState::getMessage)
522524
.filter(msg -> msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n"));
523-
tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction, message);
525+
tc.throwStateRefinementError(invocation.getPosition(), function.getPlacementInCode().getPosition(),
526+
prevState, expectedStatesDisjunction, message);
524527
}
525528
}
526529

@@ -575,7 +578,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
575578
// is a subtype of the variable's main refinement
576579
if (rv instanceof Variable) {
577580
Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
578-
tc.checkSMT(superC, invocation);
581+
tc.checkSMT(superC, invocation, rv.getPlacementInCode().getPosition(), null);
579582
tc.getContext().addRefinementInstanceToVariable(superName, name2);
580583
}
581584
}

0 commit comments

Comments
 (0)