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