diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java deleted file mode 100644 index 3383f6bf..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java +++ /dev/null @@ -1,12 +0,0 @@ -package liquidjava.diagnostics; - -import spoon.reflect.cu.SourcePosition; - -public record ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { - - public static ErrorPosition fromSpoonPosition(SourcePosition pos) { - if (pos == null || !pos.isValidPosition()) - return null; - return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn()); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index d1a743dc..affc6ae9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -13,14 +13,14 @@ public class LJDiagnostic extends RuntimeException { private final String accentColor; private final String customMessage; private String file; - private ErrorPosition position; + private SourcePosition position; private static final String PIPE = " | "; public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) { this.title = title; this.message = message; this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; - this.position = ErrorPosition.fromSpoonPosition(pos); + this.position = pos; this.accentColor = accentColor; this.customMessage = customMessage; } @@ -41,14 +41,14 @@ public String getDetails() { return ""; // to be overridden by subclasses } - public ErrorPosition getPosition() { + public SourcePosition getPosition() { return position; } public void setPosition(SourcePosition pos) { if (pos == null) return; - this.position = ErrorPosition.fromSpoonPosition(pos); + this.position = pos; this.file = pos.getFile().getPath(); } @@ -82,7 +82,7 @@ public String toString() { // location if (file != null && position != null) { - sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n"); + sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n"); } return sb.toString(); @@ -100,8 +100,8 @@ public String getSnippet() { // before and after lines for context int contextBefore = 2; int contextAfter = 2; - int startLine = Math.max(1, position.lineStart() - contextBefore); - int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter); + int startLine = Math.max(1, position.getLine() - contextBefore); + int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter); // calculate padding for line numbers int padding = String.valueOf(endLine).length(); @@ -115,9 +115,9 @@ public String getSnippet() { sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n"); // add error markers on the line(s) with the error - if (i >= position.lineStart() && i <= position.lineEnd()) { - int colStart = (i == position.lineStart()) ? position.colStart() : 1; - int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length(); + if (i >= position.getLine() && i <= position.getEndLine()) { + int colStart = (i == position.getLine()) ? position.getColumn() : 1; + int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length(); if (colStart > 0 && colEnd > 0) { int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars() diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index 7a04abde..6ec07f42 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -14,6 +14,7 @@ public abstract class RefinedVariable extends Refined { private PlacementInCode placementInCode; private boolean isParameter; private SourcePosition annPosition; + private Predicate failingRefinement; public RefinedVariable(String name, CtTypeReference type, Predicate c) { super(name, type, c); @@ -88,4 +89,12 @@ public void setIsParameter(boolean b) { public boolean isParameter() { return isParameter; } + + public void setFailingRefinement(Predicate failingRefinement) { + this.failingRefinement = failingRefinement; + } + + public Predicate getFailingRefinement() { + return failingRefinement; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 296e4334..b9a07206 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -305,17 +305,23 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam rv.addSuperType(t); context.addRefinementInstanceToVariable(simpleName, newName); String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null); - checkSMT(cEt, usage, customMessage); // TODO CHANGE + checkSMT(cEt, usage, customMessage, mainRV); // TODO CHANGE context.addRefinementToVariableInContext(simpleName, type, cet, usage); } - public void checkSMT(Predicate expectedType, CtElement element) throws LJError { - checkSMT(expectedType, element, null); + public void checkSMT(Predicate expectedType, CtElement element, RefinedVariable rv) throws LJError { + checkSMT(expectedType, element, null, rv); } - public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError { - vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage); - element.putMetadata(Keys.REFINEMENT, expectedType); + public void checkSMT(Predicate expectedType, CtElement element, String customMessage, RefinedVariable rv) + throws LJError { + try { + vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage); + element.putMetadata(Keys.REFINEMENT, expectedType); + } catch (RefinementError e) { + rv.setFailingRefinement(expectedType); + throw e; + } } public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 1f1decda..79edbafc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -200,8 +200,8 @@ public void getReturnRefinements(CtReturn ret) throws LJError { Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName) .substituteVariable(Keys.THIS, returnVarName); - rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); - rtc.checkSMT(cexpectedType, ret, fi.getMessage()); + RefinedVariable rv = rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); + rtc.checkSMT(cexpectedType, ret, fi.getMessage(), rv); rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType); } } @@ -372,7 +372,7 @@ private void checkParameters(CtElement invocation, List> argumen VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET); c = c.substituteVariable(Keys.THIS, vi.getName()); } - rtc.checkSMT(c, invocation, fArg.getMessage()); + rtc.checkSMT(c, invocation, fArg.getMessage(), fArg); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index cb70c2e9..2f7296bf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -440,7 +440,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L // is a subtype of the variable's main refinement if (rv instanceof Variable) { Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName()); - tc.checkSMT(superC, fw); + tc.checkSMT(superC, fw, rv); tc.getContext().addRefinementInstanceToVariable(parentTargetName, newInstanceName); } } @@ -558,7 +558,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin // is a subtype of the variable's main refinement if (rv instanceof Variable) { Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName()); - tc.checkSMT(superC, invocation); + tc.checkSMT(superC, invocation, rv); tc.getContext().addRefinementInstanceToVariable(superName, name2); } }