Expand aliases before translating states

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
+    }
+}

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);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -59,8 +59,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         Predicate expected;
         try {
             List<GhostState> 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<GhostState> 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<GhostState> filterGhostStatesForVariables(List<GhostState> 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<GhostState> filtered, String[] s, Factory f) {
         if (!DebugLog.enabled())
@@ -261,8 +259,7 @@ private void transformChainForDebug(VCImplication chain, List<GhostState> 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
             }

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<GhostState> ghostStates, String[] toChange, Context context, Factory f)
+            throws LJError {
         Map<String, AliasDTO> 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);
     }