From 8b3c32bb02faee5951c18cffd1d93c33f89812cf Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 17:32:22 +0000 Subject: [PATCH] Expand aliases before translating states, so a state in an alias body is translated Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/ErrorStateInAlias.java | 26 +++++++++++++++++++ .../refinement_checker/TypeChecker.java | 5 ++-- .../refinement_checker/VCChecker.java | 21 +++++++-------- .../liquidjava/rj_language/Predicate.java | 14 +++++----- 4 files changed, 45 insertions(+), 21 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateInAlias.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateInAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorStateInAlias.java new file mode 100644 index 00000000..1ad50c04 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateInAlias.java @@ -0,0 +1,26 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"closed", "opened"}) +@RefinementAlias("Closed(ErrorStateInAlias x) { closed(x) }") +public class ErrorStateInAlias { + + @StateRefinement(to = "closed(this)") + public ErrorStateInAlias() {} + + @StateRefinement(from = "closed(this)", to = "opened(this)") + public void open() {} + + static void needsClosed(@Refinement("Closed(_)") ErrorStateInAlias door) {} + + public static void main(String[] args) { + ErrorStateInAlias door = new ErrorStateInAlias(); + needsClosed(door); + door.open(); + needsClosed(door); // Expect: Refinement Error + } +} 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 0e886a0e..4677653d 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 @@ -166,9 +166,8 @@ private void checkRefinementSatisfiability(String refinement, Predicate predicat if (qualifiedClassName != null && !context.hasVariable(Keys.THIS)) context.addVarToContext(Keys.THIS, factory.Type().createReference(qualifiedClassName), p, element); - Predicate refinementPredicate = predicate.changeStatesToRefinements(context.getGhostStates(), - new String[] { Keys.WILDCARD, Keys.THIS }); - refinementPredicate = refinementPredicate.changeAliasToRefinement(context, factory); + Predicate refinementPredicate = predicate.toSolverPredicate(context.getGhostStates(), + new String[] { Keys.WILDCARD, Keys.THIS }, context, factory); if (new SMTEvaluator().isUnsatisfiable(refinementPredicate, context)) { SourcePosition position = Utils.getLJAnnotationPosition(element, refinement); 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 34ae996b..7ae0371f 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 @@ -59,8 +59,8 @@ public void processSubtyping(Predicate expectedType, List list, CtEl Predicate expected; try { List filtered = filterGhostStatesForVariables(list, mainVars, lrv); - premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); - expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); + premises = premisesBeforeChange.toSolverPredicate(filtered, s, context, f); + expected = expectedType.toSolverPredicate(filtered, s, context, f); transformChainForDebug(impl, filtered, s, f); } catch (LJError e) { // add location info to error @@ -186,14 +186,12 @@ public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, VCImplication impl = joinPredicates(expectedType, mainVars, lrv, map); Predicate premisesJoined = impl.toConjunctions(); List filtered = filterGhostStatesForVariables(states, mainVars, lrv); - Predicate premises = Predicate.createConjunction(premisesJoined, type).changeStatesToRefinements(filtered, s) - .changeAliasToRefinement(context, factory); - Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, + Predicate premises = Predicate.createConjunction(premisesJoined, type).toSolverPredicate(filtered, s, context, factory); + Predicate expected = expectedType.toSolverPredicate(filtered, s, context, factory); if (!silent) { transformChainForDebug(impl, filtered, s, factory); - Predicate foundExtra = type.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, - factory); + Predicate foundExtra = type.toSolverPredicate(filtered, s, context, factory); DebugLog.smtStart(impl, foundExtra, expected); } @@ -250,9 +248,9 @@ private List filterGhostStatesForVariables(List list, Li } /** - * Apply the same {@code changeStatesToRefinements} / {@code changeAliasToRefinement} pipeline to each node of a - * {@link VCImplication} chain so the structured debug print mirrors the predicates Z3 actually sees. Mutates the - * chain in place; safe because {@code joinPredicates} returns a clone. + * Apply the same {@code toSolverPredicate} pipeline to each node of a {@link VCImplication} chain so the structured + * debug print mirrors the predicates Z3 actually sees. Mutates the chain in place; safe because + * {@code joinPredicates} returns a clone. */ private void transformChainForDebug(VCImplication chain, List filtered, String[] s, Factory f) { if (!DebugLog.enabled()) @@ -261,8 +259,7 @@ private void transformChainForDebug(VCImplication chain, List filter if (n.getRefinement() == null) continue; try { - n.setRefinement( - n.getRefinement().changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f)); + n.setRefinement(n.getRefinement().toSolverPredicate(filtered, s, context, f)); } catch (LJError ignored) { // best-effort transformation for debug; leave node as-is on failure } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 1d660bab..5fbad3f7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -154,17 +154,19 @@ protected Expression innerParse(String ref, String prefix) throws LJError { return RefinementsParser.createAST(ref, prefix); } - public Predicate changeAliasToRefinement(Context context, Factory f) throws LJError { - Expression ref = getExpression(); - + /** + * The predicate the solver checks: aliases expanded first, so that the states their bodies use are replaced too, + * then the states replaced by the refinements of their state sets + */ + public Predicate toSolverPredicate(List ghostStates, String[] toChange, Context context, Factory f) + throws LJError { Map alias = new HashMap<>(); for (AliasWrapper aw : context.getAliases()) { alias.put(aw.getName(), aw.createAliasDTO()); } - - ref = ref.changeAlias(alias, context, f); + Predicate expanded = new Predicate(getExpression().changeAlias(alias, context, f)); + Expression ref = expanded.changeStatesToRefinements(ghostStates, toChange).getExpression(); ref.validateGhostInvocations(context, f); - return new Predicate(ref); }