From 055e9335aa9ebd109c09b5bdaf92fd6b66d749d8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 22 May 2026 18:04:56 +0100 Subject: [PATCH 1/2] fix bug gathering predicates --- .../java/liquidjava/processor/refinement_checker/VCChecker.java | 1 + 1 file changed, 1 insertion(+) 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 d01b03e5..a9232810 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 @@ -389,6 +389,7 @@ protected void throwStateRefinementError(SourcePosition position, Predicate foun String customMessage) throws StateRefinementError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); + gatherVariables(expected, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); throw new StateRefinementError(position, expected.simplify(context), From 1fa001a26e3508123f162f1a57e9b90f369e4f2d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 22 May 2026 18:29:16 +0100 Subject: [PATCH 2/2] extract to a function --- .../refinement_checker/VCChecker.java | 41 ++++++++++++++----- 1 file changed, 30 insertions(+), 11 deletions(-) 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 a9232810..39a155d3 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 @@ -374,24 +374,45 @@ private boolean hasVariable(Expression exp, String var) { // Errors--------------------------------------------------------------------------------------------------- + /** + * Builds the {@link VCImplication} premise chain that backs an error message. Every refined variable named in + * {@code predicates} — and, transitively, the path variables those drag in — is gathered, and their refinements are + * joined into a chain. + * + *

+ * Callers pass every predicate that should contribute variables, not just one: a bare predicate such as + * {@code true} carries no variable names and would gather nothing on its own, leaving the chain (and the displayed + * premises) empty. Passing both the {@code found} and {@code expected} refinements ensures the variable that is + * only named on one side still seeds the chain. + * + * @param map + * translation table populated, as a side effect, with the gathered variables' code placements + * @param predicates + * predicates whose variables seed the chain; {@code predicates[0]} is also passed to + * {@code joinPredicates} + * + * @return the joined premise chain + */ + private VCImplication buildPremiseChain(TranslationTable map, Predicate... predicates) { + List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); + for (Predicate p : predicates) { + gatherVariables(p, lrv, mainVars); + } + return joinPredicates(predicates[0], mainVars, lrv, map); + } + protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found, Counterexample counterexample, String customMessage) 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(); + Predicate premises = buildPremiseChain(map, expected, found).toConjunctions(); throw new RefinementError(position, expected.simplify(context), premises.simplify(context), map, counterexample, customMessage); } protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, String customMessage) throws StateRefinementError { - List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(found, lrv, mainVars); - gatherVariables(expected, lrv, mainVars); TranslationTable map = new TranslationTable(); - VCImplication foundState = joinPredicates(found, mainVars, lrv, map); + VCImplication foundState = buildPremiseChain(map, expected, found); throw new StateRefinementError(position, expected.simplify(context), foundState.toConjunctions().simplify(context), map, customMessage); } @@ -402,10 +423,8 @@ protected void throwStateConflictError(SourcePosition position, Predicate expect } private TranslationTable createMap(Predicate expectedType) { - List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(expectedType, lrv, mainVars); TranslationTable map = new TranslationTable(); - joinPredicates(expectedType, mainVars, lrv, map); + buildPremiseChain(map, expectedType); return map; }