From f523621612cae348ce1059e0200ed5d9bd4e41bb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 4 Mar 2026 16:44:50 +0000 Subject: [PATCH 1/5] Improve Counterexamples --- .../java/liquidjava/diagnostics/Colors.java | 1 + .../liquidjava/diagnostics/LJDiagnostic.java | 2 +- .../diagnostics/errors/RefinementError.java | 14 +++++---- .../java/liquidjava/smt/TranslatorToZ3.java | 29 ++++++++++++------- 4 files changed, 28 insertions(+), 18 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java index 7b72d190..8f1abea1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java @@ -6,4 +6,5 @@ public class Colors { public static final String GREY = "\u001B[90m"; public static final String BOLD_RED = "\u001B[1;31m"; public static final String BOLD_YELLOW = "\u001B[1;33m"; + public static final String CYAN = "\u001B[36m"; } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 1c548648..19491a43 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -77,7 +77,7 @@ public String toString() { // details String details = getDetails(); if (!details.isEmpty()) { - sb.append(" --> ").append(String.join("\n ", details.split("\n"))).append("\n"); + sb.append(Colors.CYAN).append(" --> ").append(String.join("\n ", details.split("\n"))).append(Colors.RESET).append("\n"); } // location 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 24c27336..0a9d4e98 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -27,20 +27,22 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD @Override public String getDetails() { - return "Counterexample: " + getCounterExampleString(); + String counterexampleString = getCounterExampleString(); + if (counterexampleString == null) + return ""; + return "Counterexample: " + counterexampleString; } public String getCounterExampleString() { if (counterexample == null || counterexample.assignments().isEmpty()) - return ""; + return null; - // filter fresh variables and join assignements with && - String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_")) - .reduce((a, b) -> a + " && " + b).orElse(""); + // join assignements with && + String counterexampleExp = String.join(" && ", counterexample.assignments()); // check if counterexample is trivial (same as the found value) if (counterexampleExp.equals(found.getValue().toString())) - return ""; + return null; return counterexampleExp; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 96f32f66..08afcb9b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -18,8 +18,10 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Set; import java.util.stream.Collectors; import liquidjava.diagnostics.errors.LJError; @@ -40,13 +42,15 @@ public class TranslatorToZ3 implements AutoCloseable { private final Map> funcTranslation = new HashMap<>(); private final Map> funcAppTranslation = new HashMap<>(); private final Map, String> exprToNameTranslation = new HashMap<>(); + private final Set instanceVariableRefinements; - public TranslatorToZ3(liquidjava.processor.context.Context c) { - TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation); - TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes); - TranslatorContextToZ3.addAliases(c.getAliases(), aliasTranslation); - TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation); - TranslatorContextToZ3.addGhostStates(z3, c.getGhostStates(), funcTranslation); + public TranslatorToZ3(liquidjava.processor.context.Context context) { + TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation); + TranslatorContextToZ3.storeVariablesSubtypes(z3, context.getAllVariablesWithSupertypes(), varSuperTypes); + TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation); + TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation); + TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation); + instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString()).collect(Collectors.toSet()); } @SuppressWarnings("unchecked") @@ -66,18 +70,21 @@ public Counterexample getCounterexample(Model model) { if (decl.getArity() == 0) { Symbol name = decl.getName(); Expr value = model.getConstInterp(decl); + String assignment = name + " == " + value; // Skip values of uninterpreted sorts - if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT) - assignments.add(name + " == " + value); + if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT && !instanceVariableRefinements.contains(assignment)) + assignments.add(assignment); } } // Extract function application values for (Map.Entry> entry : funcAppTranslation.entrySet()) { - String label = entry.getKey(); + String name = entry.getKey(); Expr application = entry.getValue(); Expr value = model.eval(application, true); - assignments.add(label + " = " + value); - } + String assignment = name + " == " + value; + if (!instanceVariableRefinements.contains(assignment)) + assignments.add(assignment); + } return new Counterexample(assignments); } From f7f37092263c85901f97444ed150bf7b10db9302 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 4 Mar 2026 17:01:35 +0000 Subject: [PATCH 2/5] Remove Details Color --- .../src/main/java/liquidjava/diagnostics/Colors.java | 1 - .../src/main/java/liquidjava/diagnostics/LJDiagnostic.java | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java index 8f1abea1..7b72d190 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java @@ -6,5 +6,4 @@ public class Colors { public static final String GREY = "\u001B[90m"; public static final String BOLD_RED = "\u001B[1;31m"; public static final String BOLD_YELLOW = "\u001B[1;33m"; - public static final String CYAN = "\u001B[36m"; } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 19491a43..1c548648 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -77,7 +77,7 @@ public String toString() { // details String details = getDetails(); if (!details.isEmpty()) { - sb.append(Colors.CYAN).append(" --> ").append(String.join("\n ", details.split("\n"))).append(Colors.RESET).append("\n"); + sb.append(" --> ").append(String.join("\n ", details.split("\n"))).append("\n"); } // location From ba28952d7f4d93f6eeb2c64357c9cb9805cc61dc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 4 Mar 2026 17:29:30 +0000 Subject: [PATCH 3/5] Formatting --- .../main/java/liquidjava/diagnostics/LJDiagnostic.java | 2 +- .../src/main/java/liquidjava/smt/TranslatorToZ3.java | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 1c548648..d1a743dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -129,7 +129,7 @@ public String getSnippet() { // line number padding + pipe + column offset String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET - + " ".repeat(visualColStart - 1); + + " ".repeat(visualColStart - 1); String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1)); sb.append(indent).append(markers); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 08afcb9b..07fa4fe4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -50,7 +50,8 @@ public TranslatorToZ3(liquidjava.processor.context.Context context) { TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation); TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation); TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation); - instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString()).collect(Collectors.toSet()); + instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString()) + .collect(Collectors.toSet()); } @SuppressWarnings("unchecked") @@ -72,7 +73,8 @@ public Counterexample getCounterexample(Model model) { Expr value = model.getConstInterp(decl); String assignment = name + " == " + value; // Skip values of uninterpreted sorts - if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT && !instanceVariableRefinements.contains(assignment)) + if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT + && !instanceVariableRefinements.contains(assignment)) assignments.add(assignment); } } @@ -84,7 +86,7 @@ public Counterexample getCounterexample(Model model) { String assignment = name + " == " + value; if (!instanceVariableRefinements.contains(assignment)) assignments.add(assignment); - } + } return new Counterexample(assignments); } From bdbd8c045af7c8e80699adde0b42e66f7ca9a2ab Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 13:38:55 +0000 Subject: [PATCH 4/5] Check All Variable Refinements In counterexample, check if assignment is already present in all variable refinements, not just instance variable refinements. --- .../liquidjava/processor/context/Context.java | 46 +++++++++---------- .../processor/context/ContextHistory.java | 2 +- .../java/liquidjava/smt/SMTEvaluator.java | 5 +- .../java/liquidjava/smt/TranslatorToZ3.java | 11 ++--- 4 files changed, 31 insertions(+), 33 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 23176dfd..fa94adf4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -55,7 +55,7 @@ public void reinitializeAllContext() { public void enterContext() { ctxVars.push(new ArrayList<>()); // make each variable enter context - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).enterContext(); } @@ -63,7 +63,7 @@ public void enterContext() { public void exitContext() { ctxVars.pop(); // make each variable exit context - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).exitContext(); } @@ -86,6 +86,19 @@ public Map> getContext() { return ret; } + public Set getAllVariableRefinements() { + Set vars = new HashSet<>(); + vars.addAll(getAllCtxVars()); + vars.addAll(ctxInstanceVars); + vars.addAll(ctxGlobalVars); + Set refinements = new HashSet<>(); + for (RefinedVariable var : vars) { + if (var.getRefinement() != null) + refinements.add(var.getRefinement().toString()); + } + return refinements; + } + // ---------------------- Global variables ---------------------- public void addGlobalVariableToContext(String simpleName, String location, CtTypeReference type, Predicate c) { RefinedVariable vi = new Variable(simpleName, location, type, c); @@ -172,22 +185,9 @@ public boolean hasVariable(String name) { return getVariableByName(name) != null; } - /** - * Lists all variables inside the stack - * - * @return list of all variables - */ - public List getAllVariables() { - List lvi = new ArrayList<>(); - for (List l : ctxVars) { - lvi.addAll(l); - } - return lvi; - } - public List getAllVariablesWithSupertypes() { List lvi = new ArrayList<>(); - for (RefinedVariable rv : getAllVariables()) { + for (RefinedVariable rv : getAllCtxVars()) { if (!rv.getSuperTypes().isEmpty()) lvi.add(rv); } @@ -229,7 +229,7 @@ public Variable getVariableFromInstance(VariableInstance vi) { return vi.getParent().orElse(null); } - public List getCtxVars() { + public List getAllCtxVars() { List lvi = new ArrayList<>(); for (List l : ctxVars) { lvi.addAll(l); @@ -243,37 +243,37 @@ public List getCtxInstanceVars() { // ---------------------- Variables - if information storing ---------------------- public void variablesSetBeforeIf() { - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).saveInstanceBeforeIf(); } public void variablesSetThenIf() { - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).saveInstanceThen(); } public void variablesSetElseIf() { - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).saveInstanceElse(); } public void variablesNewIfCombination() { - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).newIfCombination(); } public void variablesFinishIfCombination() { - for (RefinedVariable vi : getAllVariables()) + for (RefinedVariable vi : getAllCtxVars()) if (vi instanceof Variable) ((Variable) vi).finishIfCombination(); } public void variablesCombineFromIf(Predicate cond) { - for (RefinedVariable vi : getAllVariables()) { + for (RefinedVariable vi : getAllCtxVars()) { if (vi instanceof Variable) { Optional ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond); if (ovi.isPresent()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 0e4db162..5a47adcf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -49,7 +49,7 @@ public void saveContext(CtElement element, Context context) { String file = pos.getFile().getAbsolutePath(); String scope = getScopePosition(element); fileScopeVars.putIfAbsent(file, new HashMap<>()); - fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); + fileScopeVars.get(file).put(scope, new HashSet<>(context.getAllCtxVars())); // add other elements in context instanceVars.addAll(context.getCtxInstanceVars()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 03cfd94e..f1f71456 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -1,5 +1,7 @@ package liquidjava.smt; +import java.util.Set; + import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.Expr; import com.microsoft.z3.Model; @@ -36,7 +38,8 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte // subRef is not a subtype of supRef if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); - Counterexample counterexample = tz3.getCounterexample(model); + Set variableRefinements = context.getAllVariableRefinements(); + Counterexample counterexample = tz3.getCounterexample(model, variableRefinements); return SMTResult.error(counterexample); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 07fa4fe4..684bc118 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -6,7 +6,6 @@ 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; @@ -18,7 +17,6 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; -import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; @@ -42,7 +40,6 @@ public class TranslatorToZ3 implements AutoCloseable { private final Map> funcTranslation = new HashMap<>(); private final Map> funcAppTranslation = new HashMap<>(); private final Map, String> exprToNameTranslation = new HashMap<>(); - private final Set instanceVariableRefinements; public TranslatorToZ3(liquidjava.processor.context.Context context) { TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation); @@ -50,8 +47,6 @@ public TranslatorToZ3(liquidjava.processor.context.Context context) { TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation); TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation); TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation); - instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString()) - .collect(Collectors.toSet()); } @SuppressWarnings("unchecked") @@ -64,7 +59,7 @@ public Solver makeSolverForExpression(Expr e) { /** * Extracts the counterexample from the Z3 model */ - public Counterexample getCounterexample(Model model) { + public Counterexample getCounterexample(Model model, Set variableRefinements) { List assignments = new ArrayList<>(); // Extract constant variable assignments for (FuncDecl decl : model.getDecls()) { @@ -74,7 +69,7 @@ public Counterexample getCounterexample(Model model) { String assignment = name + " == " + value; // Skip values of uninterpreted sorts if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT - && !instanceVariableRefinements.contains(assignment)) + && !variableRefinements.contains(assignment)) assignments.add(assignment); } } @@ -84,7 +79,7 @@ public Counterexample getCounterexample(Model model) { Expr application = entry.getValue(); Expr value = model.eval(application, true); String assignment = name + " == " + value; - if (!instanceVariableRefinements.contains(assignment)) + if (!variableRefinements.contains(assignment)) assignments.add(assignment); } return new Counterexample(assignments); From 0d2d9e76d6d345338df5210ee1a910ee66b08e74 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 13:44:55 +0000 Subject: [PATCH 5/5] Only Get `ctxVars` in the Current Scope --- .../src/main/java/liquidjava/processor/context/Context.java | 4 ++-- .../src/main/java/liquidjava/smt/SMTEvaluator.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index fa94adf4..6c1d5c5f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -86,9 +86,9 @@ public Map> getContext() { return ret; } - public Set getAllVariableRefinements() { + public Set getVariableRefinements() { Set vars = new HashSet<>(); - vars.addAll(getAllCtxVars()); + vars.addAll(ctxVars.peek()); vars.addAll(ctxInstanceVars); vars.addAll(ctxGlobalVars); Set refinements = new HashSet<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index f1f71456..7bad03ba 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -38,7 +38,7 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte // subRef is not a subtype of supRef if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); - Set variableRefinements = context.getAllVariableRefinements(); + Set variableRefinements = context.getVariableRefinements(); Counterexample counterexample = tz3.getCounterexample(model, variableRefinements); return SMTResult.error(counterexample); }