From 089dc0ae6e8a53d0318820d9fbe666d201462d73 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Feb 2026 14:15:42 +0000 Subject: [PATCH 1/8] Add Counterexamples to Refinement Errors --- .../diagnostics/Counterexample.java | 6 ++++ .../diagnostics/errors/RefinementError.java | 21 ++++++++++-- .../refinement_checker/TypeChecker.java | 7 ++-- .../refinement_checker/VCChecker.java | 32 +++++++++++-------- .../AuxHierarchyRefinementsPassage.java | 2 +- .../object_checkers/AuxStateHandler.java | 7 ++-- .../java/liquidjava/smt/SMTEvaluator.java | 13 +++++--- .../java/liquidjava/smt/TranslatorToZ3.java | 32 +++++++++++++++---- .../java/liquidjava/smt/TypeCheckError.java | 13 ++++++-- 9 files changed, 99 insertions(+), 34 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java new file mode 100644 index 00000000..5a14c528 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java @@ -0,0 +1,6 @@ +package liquidjava.diagnostics; + +import java.util.List; + +public record Counterexample(List assignments) { +} 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 93a8a447..a54e98d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,7 +1,7 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import spoon.reflect.cu.SourcePosition; @@ -14,13 +14,30 @@ public class RefinementError extends LJError { private final ValDerivationNode expected; private final ValDerivationNode found; + private final Counterexample counterexample; public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, - TranslationTable translationTable) { + TranslationTable translationTable, Counterexample counterexample) { super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), position, translationTable); this.expected = expected; this.found = found; + this.counterexample = counterexample; + } + + @Override + public String getDetails() { + if (counterexample == null || counterexample.assignments().isEmpty()) + return ""; + + // filter fresh variables and join assignements with && + String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_")) + .reduce((a, b) -> a + " && " + b).orElse(""); + + // check if counterexample is trivial (same as the found value) + if (counterexampleExp.equals(found.getValue().toSimplifiedString())) + return ""; + return "Counterexample: " + counterexampleExp; } public ValDerivationNode getExpected() { 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 e154a3dc..34d57830 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 @@ -5,6 +5,7 @@ import java.util.List; import java.util.Optional; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -292,8 +293,10 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, factory); } - public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { - return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); + public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { + Counterexample counterexample = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), + p, factory); + return counterexample == null; } public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType) 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 0c2fba5e..4763e2c2 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 @@ -8,6 +8,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.*; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; @@ -50,10 +51,10 @@ public void processSubtyping(Predicate expectedType, List list, CtEl e.setPosition(element.getPosition()); throw e; } - boolean isSubtype = smtChecks(expected, premises, element.getPosition()); - if (!isSubtype) + Counterexample counterexample = smtChecks(expected, premises, element.getPosition()); + if (counterexample != null) throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), - map); + map, counterexample); } /** @@ -69,9 +70,9 @@ public void processSubtyping(Predicate expectedType, List list, CtEl */ public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, Factory f) throws LJError { - boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); - if (!b) - throwRefinementError(element.getPosition(), expectedType, type); + Counterexample counterexample = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); + if (counterexample != null) + throwRefinementError(element.getPosition(), expectedType, type, counterexample); } /** @@ -81,16 +82,16 @@ public void processSubtyping(Predicate type, Predicate expectedType, List list, + public Counterexample canProcessSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition position, Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); if (expectedType.isBooleanTrue() && type.isBooleanTrue()) - return true; + return null; TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; @@ -258,12 +259,17 @@ void removePathVariableThatIncludes(String otherVar) { protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found) throws RefinementError { + throwRefinementError(position, expected, found, null); + } + + protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found, + Counterexample counterexample) throws RefinementError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expected, lrv, mainVars); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(position, expected.simplify(), premises.simplify(), map); + throw new RefinementError(position, expected.simplify(), premises.simplify(), map, counterexample); } protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 88dcf683..6f68a205 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -81,7 +81,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF if (argRef.isBooleanTrue()) { arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName())); } else { - boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); + boolean ok = tc.checkStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!ok) { tc.throwRefinementError(method.getPosition(), argRef, superArgRef); } 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 bd76950b..d0d21df8 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 @@ -213,7 +213,7 @@ private static Predicate createStatePredicate(String value, String targetClass, Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; Predicate c = c1.substituteVariable(Keys.THIS, name); c = c.changeOldMentions(nameOld, name); - boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); + boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition()); if (ok) { tc.throwStateConflictError(e.getPosition(), p); } @@ -406,7 +406,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) .changeOldMentions(vi.getName(), instanceName); - if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition + if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom()); return; } @@ -471,7 +471,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List e = exp.accept(visitor); - s = tz3.verifyExpression(e); - if (s.equals(Status.SATISFIABLE)) { - throw new TypeCheckError(subRef + " not a subtype of " + supRef); + Solver solver = tz3.makeSolverForExpression(e); + Status result = solver.check(); + if (result.equals(Status.SATISFIABLE)) { + Model model = solver.getModel(); + Counterexample counterexample = tz3.getCounterexample(model); + throw new TypeCheckError(counterexample); } } } catch (SyntaxException e1) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b207552f..404e1943 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -1,22 +1,25 @@ package liquidjava.smt; -import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; +import com.microsoft.z3.FuncInterp; import com.microsoft.z3.IntExpr; import com.microsoft.z3.IntNum; import com.microsoft.z3.RealExpr; import com.microsoft.z3.Solver; import com.microsoft.z3.Sort; -import com.microsoft.z3.Status; +import com.microsoft.z3.Model; + +import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; @@ -42,10 +45,27 @@ public TranslatorToZ3(liquidjava.processor.context.Context c) { } @SuppressWarnings("unchecked") - public Status verifyExpression(Expr e) { - Solver s = z3.mkSolver(); - s.add((BoolExpr) e); - return s.check(); + public Solver makeSolverForExpression(Expr e) { + Solver solver = z3.mkSolver(); + solver.add((BoolExpr) e); + return solver; + } + + /** + * Extracts the counterexample from the Z3 model + */ + public Counterexample getCounterexample(Model model) { + List assignments = new ArrayList<>(); + for (FuncDecl decl : model.getDecls()) { + // extract variable assignments with constants + if (decl.getArity() == 0) { + String name = decl.getName().toString(); + String value = model.getConstInterp(decl).toString(); + assignments.add(name + " == " + value); + } + // TODO: extract function assignments (arity > 0)? + } + return new Counterexample(assignments); } // #####################Literals and Variables##################### diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java index 04c6c07d..a96f6f69 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java @@ -1,8 +1,17 @@ package liquidjava.smt; +import liquidjava.diagnostics.Counterexample; + public class TypeCheckError extends Exception { - public TypeCheckError(String message) { - super(message); + private final Counterexample counterexample; + + public TypeCheckError(Counterexample counterexample) { + super("Refinement was violated"); + this.counterexample = counterexample; + } + + public Counterexample getCounterexample() { + return counterexample; } } From b3f11125546d30ddaf3abb886535a0467d274aa5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Feb 2026 14:39:35 +0000 Subject: [PATCH 2/8] Fix Merge --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ca9f5514..69adfb4e 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 @@ -318,7 +318,7 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { - vcChecker.throwRefinementError(position, expectedType, foundType, customMessage); + vcChecker.throwRefinementError(position, expectedType, foundType, null, customMessage); } public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, From 76a7c99f49df5d4308fcb8eda16f022821a7c843 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Feb 2026 21:01:22 +0000 Subject: [PATCH 3/8] Improve Readability of Ghosts in Counterexamples Co-Authored-By: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> --- .../java/liquidjava/smt/TranslatorToZ3.java | 40 +++++++++++++++---- 1 file changed, 32 insertions(+), 8 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 404e1943..2ca2548b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -15,9 +15,11 @@ import com.microsoft.z3.Model; import java.util.ArrayList; +import java.util.Arrays; import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.stream.Collectors; import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.LJError; @@ -35,6 +37,8 @@ public class TranslatorToZ3 implements AutoCloseable { private final Map>> varSuperTypes = new HashMap<>(); private final Map aliasTranslation = new HashMap<>(); // this is not being used private final Map> funcTranslation = new HashMap<>(); + private final Map> funcAppTranslation = new HashMap<>(); + private final Map, String> exprToNameTranslation = new HashMap<>(); public TranslatorToZ3(liquidjava.processor.context.Context c) { TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation); @@ -56,14 +60,22 @@ public Solver makeSolverForExpression(Expr e) { */ public Counterexample getCounterexample(Model model) { List assignments = new ArrayList<>(); + // Extract constant variable assignments for (FuncDecl decl : model.getDecls()) { - // extract variable assignments with constants if (decl.getArity() == 0) { String name = decl.getName().toString(); String value = model.getConstInterp(decl).toString(); - assignments.add(name + " == " + value); + // Skip opaque Z3 object values + if (!value.contains("!val!")) + assignments.add(name + " == " + value); } - // TODO: extract function assignments (arity > 0)? + } + // Extract function application values + for (Map.Entry> entry : funcAppTranslation.entrySet()) { + String label = entry.getKey(); + Expr application = entry.getValue(); + Expr value = model.eval(application, true); + assignments.add(label + " = " + value); } return new Counterexample(assignments); } @@ -101,7 +113,9 @@ private Expr getVariableTranslation(String name) throws LJError { } public Expr makeVariable(String name) throws LJError { - return getVariableTranslation(name); // int[] not in varTranslation + Expr expr = getVariableTranslation(name); // int[] not in varTranslation + exprToNameTranslation.put(expr, name); // Track for readable labels + return expr; } public Expr makeFunctionInvocation(String name, Expr[] params) throws LJError { @@ -111,7 +125,7 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws LJEr return makeSelect(params); FuncDecl fd = funcTranslation.get(name); if (fd == null) - fd = resolveFunctionDeclFallback(name, params); + fd = resolveFunctionDecl(name, params); Sort[] s = fd.getDomain(); for (int i = 0; i < s.length; i++) { @@ -125,15 +139,18 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws LJEr params[i] = e; } } - return z3.mkApp(fd, params); + String label = buildFunctionLabel(name, params); + Expr app = z3.mkApp(fd, params); + funcAppTranslation.put(label, app); + return app; } /** - * Fallback resolver for function declarations when an exact qualified name lookup fails. Tries to match by simple + * Gets function declarations when an exact qualified name lookup fails. Tries to match by simple * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise * returns the first compatible candidate and relies on later coercion via var supertypes. */ - private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) throws LJError { + private FuncDecl resolveFunctionDecl(String name, Expr[] params) throws LJError { String simple = Utils.getSimpleName(name); FuncDecl candidate = null; for (Map.Entry> entry : funcTranslation.entrySet()) { @@ -330,6 +347,13 @@ public Expr makeIte(Expr c, Expr t, Expr e) { throw new RuntimeException("Condition is not a boolean expression"); } + private String buildFunctionLabel(String functionName, Expr[] params) { + String simpleName = Utils.getSimpleName(functionName); + String argsString = Arrays.stream(params).map(p -> exprToNameTranslation.getOrDefault(p, p.toString())) + .collect(Collectors.joining(", ")); + return simpleName + "(" + argsString + ")"; + } + @Override public void close() throws Exception { z3.close(); From ea87100fbf60b1e9d14a4d5bcf2ad2a2b4b4d06c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Feb 2026 21:09:29 +0000 Subject: [PATCH 4/8] Fix --- .../java/liquidjava/diagnostics/errors/RefinementError.java | 2 +- .../src/main/java/liquidjava/smt/TranslatorToZ3.java | 6 +++--- .../src/main/java/liquidjava/utils/Utils.java | 3 +-- 3 files changed, 5 insertions(+), 6 deletions(-) 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 620be6a6..f702d995 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -35,7 +35,7 @@ public String getDetails() { .reduce((a, b) -> a + " && " + b).orElse(""); // check if counterexample is trivial (same as the found value) - if (counterexampleExp.equals(found.getValue().toSimplifiedString())) + if (counterexampleExp.equals(found.getValue().toString())) return ""; return "Counterexample: " + counterexampleExp; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 2ca2548b..aeab3d19 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -146,9 +146,9 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws LJEr } /** - * Gets function declarations when an exact qualified name lookup fails. Tries to match by simple - * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise - * returns the first compatible candidate and relies on later coercion via var supertypes. + * Gets function declarations when an exact qualified name lookup fails. Tries to match by simple name and number of + * parameters, preferring an exact qualified-name match if found among candidates; otherwise returns the first + * compatible candidate and relies on later coercion via var supertypes. */ private FuncDecl resolveFunctionDecl(String name, Expr[] params) throws LJError { String simple = Utils.getSimpleName(name); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1cf45bc7..1e99e3f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -50,7 +50,6 @@ private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { private static boolean hasRefinementValue(CtAnnotation annotation, String refinement) { Map values = annotation.getValues(); - return Stream.of("value", "to", "from") - .anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); + return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); } } From 5e003b7ef3ba453930daac02d8e9d9a62850b03d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Feb 2026 21:27:13 +0000 Subject: [PATCH 5/8] Skip Uninterpreted Constants --- .../src/main/java/liquidjava/smt/TranslatorToZ3.java | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index aeab3d19..997195b4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -12,6 +12,7 @@ import com.microsoft.z3.RealExpr; import com.microsoft.z3.Solver; import com.microsoft.z3.Sort; +import com.microsoft.z3.Symbol; import com.microsoft.z3.Model; import java.util.ArrayList; @@ -27,6 +28,7 @@ import liquidjava.processor.context.AliasWrapper; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; +import com.microsoft.z3.enumerations.Z3_sort_kind; import org.apache.commons.lang3.NotImplementedException; @@ -63,10 +65,10 @@ public Counterexample getCounterexample(Model model) { // Extract constant variable assignments for (FuncDecl decl : model.getDecls()) { if (decl.getArity() == 0) { - String name = decl.getName().toString(); - String value = model.getConstInterp(decl).toString(); - // Skip opaque Z3 object values - if (!value.contains("!val!")) + Symbol name = decl.getName(); + Expr value = model.getConstInterp(decl); + // Skip values of uninterpreted sorts + if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT) assignments.add(name + " == " + value); } } From cb9a1b545586ea18f8c89e099b4a3ae9b4dc7f39 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 13 Feb 2026 14:16:12 +0000 Subject: [PATCH 6/8] Extract `getCounterexampleString` from `getDetails` --- .../liquidjava/diagnostics/errors/RefinementError.java | 9 +++++++++ 1 file changed, 9 insertions(+) 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 f702d995..9d5ffc2e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -27,6 +27,10 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD @Override public String getDetails() { + return getCounterexampleString(); + } + + private String getCounterexampleString() { if (counterexample == null || counterexample.assignments().isEmpty()) return ""; @@ -37,9 +41,14 @@ public String getDetails() { // check if counterexample is trivial (same as the found value) if (counterexampleExp.equals(found.getValue().toString())) return ""; + return "Counterexample: " + counterexampleExp; } + public Counterexample getCounterexample() { + return counterexample; + } + public ValDerivationNode getExpected() { return expected; } From 18ccf116667a2e644c3a5dfdc601de4849abfa02 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 13 Feb 2026 14:44:36 +0000 Subject: [PATCH 7/8] Add `SMTResult` --- .../diagnostics/errors/RefinementError.java | 2 +- .../refinement_checker/TypeChecker.java | 8 ++--- .../refinement_checker/VCChecker.java | 28 +++++++++--------- .../{diagnostics => smt}/Counterexample.java | 2 +- .../java/liquidjava/smt/SMTEvaluator.java | 6 ++-- .../main/java/liquidjava/smt/SMTResult.java | 29 +++++++++++++++++++ .../java/liquidjava/smt/TranslatorToZ3.java | 1 - .../java/liquidjava/smt/TypeCheckError.java | 17 ----------- 8 files changed, 51 insertions(+), 42 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/{diagnostics => smt}/Counterexample.java (72%) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java 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 9d5ffc2e..21a9a4c2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,8 +1,8 @@ package liquidjava.diagnostics.errors; -import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.smt.Counterexample; import spoon.reflect.cu.SourcePosition; /** 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 57051ef2..c4358ba9 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 @@ -6,7 +6,6 @@ import java.util.Map; import java.util.Optional; -import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -17,6 +16,8 @@ import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.smt.Counterexample; +import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -314,9 +315,8 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen } public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { - Counterexample counterexample = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), - p, factory); - return counterexample == null; + SMTResult result = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); + return result.isOk(); } public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType, 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 693ab5f4..f0634a67 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 @@ -8,13 +8,13 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.*; -import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; +import liquidjava.smt.Counterexample; import liquidjava.smt.SMTEvaluator; -import liquidjava.smt.TypeCheckError; +import liquidjava.smt.SMTResult; import liquidjava.utils.constants.Keys; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -56,10 +56,11 @@ public void processSubtyping(Predicate expectedType, List list, CtEl e.setPosition(element.getPosition()); throw e; } - Counterexample counterexample = smtChecks(expected, premises, element.getPosition()); - if (counterexample != null) + SMTResult result = smtChecks(expected, premises, element.getPosition()); + if (result.isError()) { throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), - map, counterexample, customMessage); + map, result.getCounterexample(), customMessage); + } } /** @@ -75,9 +76,9 @@ public void processSubtyping(Predicate expectedType, List list, CtEl */ public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, Factory f) throws LJError { - Counterexample counterexample = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); - if (counterexample != null) - throwRefinementError(element.getPosition(), expectedType, type, counterexample, null); + SMTResult result = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); + if (result.isError()) + throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null); } /** @@ -91,12 +92,9 @@ public void processSubtyping(Predicate type, Predicate expectedType, List list, + public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition position, Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); if (expectedType.isBooleanTrue() && type.isBooleanTrue()) - return null; + return SMTResult.ok(); TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java similarity index 72% rename from liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java rename to liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java index 5a14c528..2bef12b6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java @@ -1,4 +1,4 @@ -package liquidjava.diagnostics; +package liquidjava.smt; import java.util.List; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index be461a47..338a885d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -7,14 +7,13 @@ import com.microsoft.z3.Status; import com.microsoft.z3.Z3Exception; -import liquidjava.diagnostics.Counterexample; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; public class SMTEvaluator { - public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception { + public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception { // Creates a parser for our SMT-ready refinement language // Discharges the verification to z3 Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); @@ -28,7 +27,7 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); Counterexample counterexample = tz3.getCounterexample(model); - throw new TypeCheckError(counterexample); + return SMTResult.error(counterexample); } } } catch (SyntaxException e1) { @@ -37,5 +36,6 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws } catch (Z3Exception e) { throw new Z3Exception(e.getLocalizedMessage()); } + return SMTResult.ok(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java new file mode 100644 index 00000000..6cd9869d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java @@ -0,0 +1,29 @@ +package liquidjava.smt; + +public class SMTResult { + private final Counterexample counterexample; + + private SMTResult(Counterexample counterexample) { + this.counterexample = counterexample; + } + + public static SMTResult ok() { + return new SMTResult(null); + } + + public static SMTResult error(Counterexample counterexample) { + return new SMTResult(counterexample); + } + + public boolean isOk() { + return counterexample == null; + } + + public boolean isError() { + return !isOk(); + } + + public Counterexample getCounterexample() { + return counterexample; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 997195b4..1e960590 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -22,7 +22,6 @@ import java.util.Map; import java.util.stream.Collectors; -import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java deleted file mode 100644 index a96f6f69..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java +++ /dev/null @@ -1,17 +0,0 @@ -package liquidjava.smt; - -import liquidjava.diagnostics.Counterexample; - -public class TypeCheckError extends Exception { - - private final Counterexample counterexample; - - public TypeCheckError(Counterexample counterexample) { - super("Refinement was violated"); - this.counterexample = counterexample; - } - - public Counterexample getCounterexample() { - return counterexample; - } -} From ae2d7623acbe9e626743150a997daf5e639c4c6b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 14 Feb 2026 13:53:14 +0000 Subject: [PATCH 8/8] Improve Method Names & Javadocs --- .../refinement_checker/TypeChecker.java | 4 +- .../refinement_checker/VCChecker.java | 46 +++++++++++-------- .../java/liquidjava/smt/SMTEvaluator.java | 22 ++++++--- 3 files changed, 46 insertions(+), 26 deletions(-) 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 c4358ba9..31c6655b 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 @@ -16,7 +16,6 @@ import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; -import liquidjava.smt.Counterexample; import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -315,7 +314,8 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen } public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { - SMTResult result = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); + SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostState(), p, + factory); return result.isOk(); } 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 f0634a67..51084672 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 @@ -56,7 +56,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl e.setPosition(element.getPosition()); throw e; } - SMTResult result = smtChecks(expected, premises, element.getPosition()); + SMTResult result = verifySMTSubtype(expected, premises, element.getPosition()); if (result.isError()) { throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), map, result.getCounterexample(), customMessage); @@ -64,35 +64,33 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } /** - * Check that type is a subtype of expectedType Throws RefinementError otherwise - * + * Checks if type is a subtype of expectedType + * * @param type * @param expectedType * @param list * @param element * @param f - * + * * @throws LJError */ public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, Factory f) throws LJError { - SMTResult result = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); + SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f); if (result.isError()) throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null); } /** - * Checks the expected against the found constraint - * + * Verifies whether the found predicate is a subtype of the expected predicate + * * @param expected * @param found * @param position - * - * @return counterexample if expected type is not subtype of found type, otherwise null - * - * @throws LJError + * + * @return the result of the verification, containing a counterexample if the verification fails */ - public SMTResult smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError { + public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePosition position) throws LJError { try { return new SMTEvaluator().verifySubtype(found, expected, context); } catch (LJError e) { @@ -103,8 +101,19 @@ public SMTResult smtChecks(Predicate expected, Predicate found, SourcePosition p } } - public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, List list, - SourcePosition position, Factory f) throws LJError { + /** + * Verifies whether the found predicate is a subtype of the expected predicate, taking into account the ghost states + * + * @param type + * @param expectedType + * @param states + * @param position + * @param factory + * + * @return the result of the verification, containing a counterexample if the verification fails + */ + public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List states, + SourcePosition position, Factory factory) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); @@ -114,13 +123,14 @@ public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, Lis TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - List filtered = filterGhostStatesForVariables(list, mainVars, lrv); + List filtered = filterGhostStatesForVariables(states, mainVars, lrv); premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s) - .changeAliasToRefinement(context, f); - Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); + .changeAliasToRefinement(context, factory); + Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, + factory); // check subtyping - return smtChecks(expected, premises, position); + return verifySMTSubtype(expected, premises, position); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 338a885d..03cfd94e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -13,26 +13,36 @@ public class SMTEvaluator { - public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception { - // Creates a parser for our SMT-ready refinement language - // Discharges the verification to z3 + /** + * Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser + * for our SMT-ready refinement language and discharges the verification to Z3 + * + * @param subRef + * @param supRef + * @param context + * + * @return the result of the verification, containing a counterexample if the verification fails + */ + public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception { Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); try { Expression exp = toVerify.getExpression(); - try (TranslatorToZ3 tz3 = new TranslatorToZ3(c)) { + try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) { ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3); Expr e = exp.accept(visitor); Solver solver = tz3.makeSolverForExpression(e); Status result = solver.check(); + + // subRef is not a subtype of supRef if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); Counterexample counterexample = tz3.getCounterexample(model); return SMTResult.error(counterexample); } } - } catch (SyntaxException e1) { + } catch (SyntaxException e) { System.out.println("Could not parse: " + toVerify); - e1.printStackTrace(); + e.printStackTrace(); } catch (Z3Exception e) { throw new Z3Exception(e.getLocalizedMessage()); }