From b805f58353d4c0681c42c9a0e127024af438bfa0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Aug 2026 16:47:42 +0100 Subject: [PATCH] Restore Baseline Error Messages --- liquidjava-verifier/pom.xml | 118 +++++++++--------- .../liquidjava/diagnostics/Diagnostics.java | 2 +- .../diagnostics/errors/LJError.java | 34 +++++ .../diagnostics/errors/RefinementError.java | 105 ++++++++-------- .../errors/StateRefinementError.java | 39 ++++-- .../processor/context/PlacementInCode.java | 7 ++ .../refinement_checker/TypeChecker.java | 10 +- .../refinement_checker/VCChecker.java | 17 ++- .../AuxHierarchyRefinementsPassage.java | 2 +- .../object_checkers/AuxStateHandler.java | 4 +- 10 files changed, 198 insertions(+), 140 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index cbb415ce9..2e1542be9 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.27 + 0.0.1 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava @@ -89,43 +89,43 @@ 20 - - org.apache.maven.plugins - maven-surefire-plugin - 3.2.1 + + org.apache.maven.plugins + maven-surefire-plugin + 3.2.1 - true - - - - - org.codehaus.mojo - flatten-maven-plugin - 1.6.0 - - ossrh - true - - - - flatten - process-resources - - flatten - - - - flatten.clean - clean - - clean - - - - - - - org.antlr + true + + + + + org.codehaus.mojo + flatten-maven-plugin + 1.6.0 + + ossrh + true + + + + flatten + process-resources + + flatten + + + + flatten.clean + clean + + clean + + + + + + + org.antlr antlr4-maven-plugin 4.7.1 @@ -301,28 +301,28 @@ junit-vintage-engine test - - org.junit.jupiter - junit-jupiter-params - test - - - com.pholser - junit-quickcheck-core - 1.0 - test - - - com.pholser - junit-quickcheck-generators - 1.0 - test - - - ch.qos.logback - logback-classic - 1.4.12 - + + org.junit.jupiter + junit-jupiter-params + test + + + com.pholser + junit-quickcheck-core + 1.0 + test + + + com.pholser + junit-quickcheck-generators + 1.0 + test + + + ch.qos.logback + logback-classic + 1.4.12 + org.mdkt.compiler InMemoryJavaCompiler diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index f125f5fc0..7c9974596 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java @@ -55,7 +55,7 @@ public void clear() { } public String getErrorOutput() { - return String.join("\n", errors.stream().map(LJError::toString).toList()); + return String.join("\n", errors.stream().map(LJError::getFullMessage).toList()); } public String getWarningOutput() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index 66ff9fd21..303e56107 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -1,8 +1,12 @@ package liquidjava.diagnostics.errors; +import java.util.Formatter; +import java.util.Locale; + import liquidjava.diagnostics.LJDiagnostic; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.Colors; +import liquidjava.processor.context.PlacementInCode; import spoon.reflect.cu.SourcePosition; /** @@ -10,6 +14,9 @@ */ public abstract class LJError extends LJDiagnostic { + protected static final String SEPARATOR = "_".repeat(54); + protected static final String TABLE_SEPARATOR = "-".repeat(130); + private final TranslationTable translationTable; public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) { @@ -25,4 +32,31 @@ public LJError(String title, String message, SourcePosition pos, TranslationTabl public TranslationTable getTranslationTable() { return translationTable; } + + public String getTitleMessage() { + return getTitle(); + } + + public String getFullMessage() { + return getMessage(); + } + + protected String formatTranslationTable() { + if (translationTable.isEmpty()) + return ""; + + StringBuilder sb = new StringBuilder(); + try (Formatter formatter = new Formatter(sb, Locale.US)) { + formatter.format("%nInstance translation table:%n"); + formatter.format("%s%n", TABLE_SEPARATOR); + formatter.format("| %-32s | %-60s | %-1s %n", "Variable Name", "Created in", "File"); + formatter.format("%s%n", TABLE_SEPARATOR); + for (String name : translationTable.keySet()) { + PlacementInCode placement = translationTable.get(name); + formatter.format("| %-32s | %-60s | %-1s %n", name, placement.getText(), placement.getSimplePosition()); + } + formatter.format("%s%n%n", TABLE_SEPARATOR); + } + return sb.toString(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 78b5e0aad..44f7e3b8d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,17 +1,10 @@ package liquidjava.diagnostics.errors; -import java.util.ArrayList; -import java.util.List; -import java.util.stream.Collectors; - import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.formatter.VariableFormatter; -import liquidjava.rj_language.opt.VCSimplificationResult; -import liquidjava.smt.Counterexample; -import spoon.reflect.cu.SourcePosition; +import spoon.reflect.code.CtInvocation; +import spoon.reflect.declaration.CtElement; /** * Error indicating that a refinement constraint either was violated or cannot be proven @@ -21,66 +14,74 @@ public class RefinementError extends LJError { private final Predicate expected; - private final VCSimplificationResult found; - private final Counterexample counterexample; + private final VCImplication found; + private final String element; + private final String moreInfo; - public RefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found, - TranslationTable translationTable, Counterexample counterexample, String customMessage) { + public RefinementError(CtElement element, Predicate expected, VCImplication found, + TranslationTable translationTable, String customMessage) { super("Refinement Error", - String.format("%s is not a subtype of %s", - found.getImplication().toPredicate().getExpression().toDisplayString(), + String.format("%s is not a subtype of %s", found.toPredicate().getExpression().toDisplayString(), expected.getExpression().toDisplayString()), - position, translationTable, customMessage); + element.getPosition(), translationTable, customMessage); this.expected = expected; this.found = found; - this.counterexample = counterexample; + this.element = element.toString(); + this.moreInfo = customMessage != null ? customMessage : getInvocationInfo(element); } @Override - public String getDetails() { - String counterexampleString = getCounterExampleString(); - if (counterexampleString == null) - return ""; - return "Counterexample: " + counterexampleString; + public String getTitleMessage() { + return "Type expected:" + formatExpected(); } - public String getCounterExampleString() { - if (counterexample == null || counterexample.assignments().isEmpty()) - return null; - - List foundVarNames = new ArrayList<>(); - Expression foundExpression = getFound().getImplication().toPredicate().getExpression(); - Expression expectedExpression = expected.getExpression(); - foundExpression.getVariableNames(foundVarNames); - // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the - // subtyping check, so the counterexample maps the symbolic name back to its compile-time value - foundExpression.getResolvedConstantNames(foundVarNames); - expectedExpression.getResolvedConstantNames(foundVarNames); - List foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList(); - String counterexampleString = counterexample.assignments().stream() - // only include variables that appear in the found value and are not already fixed there - .filter(a -> foundVarNames.contains(a.first()) - && !foundAssignments.contains(a.first() + " == " + a.second())) - // format as "var == value" - .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) - // join with "&&" - .collect(Collectors.joining(" && ")); + @Override + public String getFullMessage() { + StringBuilder sb = new StringBuilder(); + sb.append(SEPARATOR).append("\n"); + sb.append("Failed to check refinement at: \n\n"); + if (moreInfo != null) + sb.append(moreInfo).append("\n"); + sb.append(element).append("\n\n"); + sb.append("Type expected:").append(formatExpected()).append("\n"); + sb.append("Refinement found:").append(formatFound()).append("\n"); + sb.append(formatTranslationTable()); + sb.append("Location: ").append(getPosition()).append("\n"); + sb.append(SEPARATOR).append("\n"); + return sb.toString(); + } - if (counterexampleString.isEmpty()) - return null; + public Predicate getExpected() { + return expected; + } - return counterexampleString; + public VCImplication getFound() { + return found; } - public Counterexample getCounterexample() { - return counterexample; + private String formatExpected() { + return "(" + expected + ")"; } - public Predicate getExpected() { - return expected; + private String formatFound() { + if (!found.hasBinder() && !found.hasNext() && found.getRefinement().isBooleanTrue()) + return "true"; + + StringBuilder sb = new StringBuilder("true"); + for (VCImplication implication = found; implication != null; implication = implication.getNext()) + sb.append(" && ").append(implication.getRefinement()); + return sb.toString(); } - public VCSimplificationResult getFound() { - return found; + private static String getInvocationInfo(CtElement element) { + if (!(element instanceof CtInvocation invocation)) + return null; + + String invocationText = invocation.getExecutable().toString(); + if (invocation.getTarget() != null) { + int targetLength = invocation.getTarget().toString().length(); + invocationText = invocation.toString().substring(targetLength + 1); + } + return "Method invocation " + invocationText + " in:"; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 763c8579f..c0f546308 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -3,8 +3,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.opt.VCSimplificationResult; -import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; /** * Error indicating that a state refinement transition was violated @@ -14,16 +13,40 @@ public class StateRefinementError extends LJError { private final Predicate expected; - private final VCSimplificationResult found; + private final VCImplication found; + private final String element; - public StateRefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found, + public StateRefinementError(CtElement element, Predicate expected, VCImplication found, TranslationTable translationTable, String customMessage) { super("State Refinement Error", String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(), - found.getImplication().toPredicate().getExpression().toDisplayString()), - position, translationTable, customMessage); + found.toPredicate().getExpression().toDisplayString()), + element.getPosition(), translationTable, customMessage); this.expected = expected; this.found = found; + this.element = element.toString(); + } + + @Override + public String getTitleMessage() { + return "Failed to check state transitions. Expected possible states:" + expected; + } + + @Override + public String getFullMessage() { + StringBuilder sb = new StringBuilder(); + sb.append(SEPARATOR).append("\n"); + sb.append("Failed to check state transitions when calling ").append(element).append(" in:\n\n"); + sb.append(element).append("\n\n"); + sb.append("Expected possible states:").append(expected).append("\n"); + sb.append("\nState found:\n"); + sb.append(TABLE_SEPARATOR).append("\n"); + sb.append(found).append("\n"); + sb.append(TABLE_SEPARATOR).append("\n\n"); + sb.append(formatTranslationTable()); + sb.append("Location: ").append(getPosition()).append("\n"); + sb.append(SEPARATOR).append("\n"); + return sb.toString(); } public Predicate getExpected() { @@ -31,10 +54,6 @@ public Predicate getExpected() { } public VCImplication getFound() { - return found.getImplication(); - } - - public VCSimplificationResult getFoundSimplification() { return found; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java index d3014faa4..8ed6707e2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java @@ -50,6 +50,13 @@ public static PlacementInCode createPlacement(CtElement elem) { return new PlacementInCode(elemText, elem.getPosition(), annotationPosition); } + public String getSimplePosition() { + if (position.getFile() == null) { + return "No position provided. Possibly asking for generated code"; + } + return position.getFile().getName() + ":" + position.getLine() + ", " + position.getColumn(); + } + public String toString() { if (position.getFile() == null) { return "No position provided. Possibly asking for generated code"; 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 4935b4579..d5ffc7f3b 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 @@ -391,14 +391,14 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc return result.isOk(); } - public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType, + public void throwRefinementError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { - vcChecker.throwRefinementError(position, expectedType, foundType, null, customMessage); + vcChecker.throwRefinementError(element, expectedType, foundType, customMessage); } - public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, - String customMessage) throws LJError { - vcChecker.throwStateRefinementError(position, found, expected, customMessage); + public void throwStateRefinementError(CtElement element, Predicate found, Predicate expected, String customMessage) + throws LJError { + vcChecker.throwStateRefinementError(element, found, expected, customMessage); } public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index d2ba3cc17..5eed60f40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -18,12 +18,10 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.Var; -import liquidjava.smt.Counterexample; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; -import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; @@ -82,8 +80,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } DebugLog.smtResult(result); if (result.isError()) { - throw new RefinementError(element.getPosition(), expectedType, implBeforeChange.simplify(), map, - result.getCounterexample(), customMessage); + throw new RefinementError(element, expectedType, implBeforeChange, map, customMessage); } } @@ -102,7 +99,7 @@ public void processSubtyping(Predicate type, Predicate expectedType, List fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - tc.throwStateRefinementError(fw.getPosition(), prevState, expectState, stateChange.getMessage()); + tc.throwStateRefinementError(fw, prevState, expectState, stateChange.getMessage()); return; } @@ -520,7 +520,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n")); - tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction, message); + tc.throwStateRefinementError(invocation, prevState, expectedStatesDisjunction, message); } }