From 4affb6d276be22087eba34fa40add8cb1078ecf4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 18:04:49 +0000 Subject: [PATCH 1/5] Accept a state written as a value of its set: phase(this) == open Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectStateValues.java | 75 ++++++++++++++++ .../java/testSuite/ErrorStateValueQuery.java | 23 +++++ .../main/java/testSuite/ErrorStateValues.java | 19 ++++ .../liquidjava/processor/facade/AliasDTO.java | 10 +++ .../refinement_checker/TypeChecker.java | 65 ++++++++++++-- .../object_checkers/AuxStateHandler.java | 8 +- .../liquidjava/rj_language/StateValues.java | 87 +++++++++++++++++++ .../liquidjava/api/tests/TestStateHints.java | 7 ++ 8 files changed, 283 insertions(+), 11 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStateValues.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateValues.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java new file mode 100644 index 00000000..87db9328 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java @@ -0,0 +1,75 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet(name = "door", value = {"closed", "opened"}) +@StateSet(name = "lock", value = {"unlocked", "locked"}) +@RefinementAlias("Shut(CorrectStateValues d) { door(d) == closed }") +public class CorrectStateValues { + + @StateRefinement(to = "door(this) == closed && lock(this) == unlocked") + public CorrectStateValues() {} + + @StateRefinement(from = "door(this) == closed && lock(this) != locked", to = "door(this) == opened") + public void open() {} + + @StateRefinement(from = "door(this) == opened", to = "door(this) == closed") + public void close() {} + + // when it fails, the lock set keeps its value + @StateRefinement(from = "door(this) == closed", to = "return ? lock(this) == locked : lock(this) == lock(old(this))") + public boolean tryLock() { + return true; + } + + @StateRefinement(from = "lock(this) == locked", to = "lock(this) == unlocked") + public void unlock() {} + + // the parameter closed keeps its meaning: the door takes its value + @StateRefinement(to = "door(this) == closed") + public void choose(int closed) {} + + static void needsShut(@Refinement("Shut(_)") CorrectStateValues d) {} + + public static void main(String[] args) { + CorrectStateValues d = new CorrectStateValues(); + int closed = 1; // the alias body still means the state closed + needsShut(d); + d.open(); + d.close(); + if (d.tryLock()) + d.unlock(); + d.open(); + d.choose(1); + d.close(); + } +} + +// states named like the variables _ and return do not take their place +@StateSet(name = "mode", value = {"_", "return", "on"}) +class CorrectStateValueVariableNames { + + @StateRefinement(to = "mode(this) == on") + public CorrectStateValueVariableNames() {} + + public void check(@Refinement("mode(this) == _") int value) {} + + @Refinement("_ == 2") + @StateRefinement(to = "mode(this) == return") + public int pick() { + return 2; + } + + @StateRefinement(from = "mode(this) == on") + public void needsOn() {} + + static void test() { + CorrectStateValueVariableNames v = new CorrectStateValueVariableNames(); + v.check(2); + v.pick(); + v.needsOn(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java new file mode 100644 index 00000000..a32f76c2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// a query written with its state set is offered as a guard, like one written with the state +@StateSet(name = "lock", value = {"unlocked", "locked"}) +public abstract class ErrorStateValueQuery { + + @StateRefinement(to = "lock(this) == locked") + public ErrorStateValueQuery() {} + + @StateRefinement(from = "lock(this) == unlocked") + public void open() {} + + @Refinement("_ == true --> lock(this) == unlocked") + public abstract boolean isUnlocked(); + + static void use(ErrorStateValueQuery d) { + d.open(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java new file mode 100644 index 00000000..7eac0506 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet(name = "door", value = {"closed", "opened"}) +@StateSet(name = "lock", value = {"unlocked", "locked"}) +public class ErrorStateValues { + + @StateRefinement(from = "door(this) == locked") // Expect: Error + public void wrongSet() {} +} + +@StateSet({"closed", "open"}) +@StateSet({"open", "locked"}) // Expect: Error +class ErrorStateValuesSharedState {} + +@StateSet({"state1", "open"}) // Expect: Error +class ErrorStateValuesGeneratedSetName {} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index 9089873a..dbe40371 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -4,7 +4,9 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.GhostState; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.reflect.cu.SourcePosition; @@ -50,6 +52,14 @@ public void resolveStaticFinalConstants(CtElement context, SourcePosition positi } } + // Read the states written as values of their sets, phase(x) == open, as the shorthand open(x); only the alias's + // parameters are variables, so a variable where the alias is used cannot take the place of a state + public void readStateValues(List states) throws LJError { + if (expression != null) { + this.expression = StateValues.toShorthand(expression, states, varNames::contains); + } + } + public String getName() { return name; } 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 243adf1e..4658d78a 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 @@ -24,6 +24,7 @@ import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; @@ -39,6 +40,7 @@ import spoon.reflect.declaration.CtAnnotation; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtInterface; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtTypedElement; @@ -126,6 +128,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws String prefix = getQualifiedClassName(element); Predicate p = prefix == null ? new Predicate(ref.get(), element) : new Predicate(ref.get(), element, prefix); + p = readStateValues(p, element, Utils.getLJAnnotationPosition(element, ref.get())); if (!p.getExpression().isBooleanExpression()) { SourcePosition position = Utils.getLJAnnotationPosition(element, ref.get()); throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", @@ -196,7 +199,8 @@ public Optional getMessageFromAnnotation(CtElement element) { @SuppressWarnings("unchecked") public void registerGhostsAndStateSets(CtElement element) throws LJError { int set = 0; - Map namedSets = new LinkedHashMap<>(); + Map stateSets = new LinkedHashMap<>(); + Map setOfState = new HashMap<>(); for (CtAnnotation ann : element.getAnnotations()) { String an = ann.getAnnotationType().getQualifiedName(); if (an.contentEquals("liquidjava.specification.StateSet")) { @@ -204,10 +208,10 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError { CtExpression nameValue = ann.getValues().get("name"); SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); String name = stateSetName(nameValue, namePosition); - GhostFunction g = createStateSet((CtNewArray) ann.getAllValues().get("value"), - name != null ? name : String.format("state%d", set), element); - if (name != null) - namedSets.put(g, namePosition); + CtNewArray states = (CtNewArray) ann.getAllValues().get("value"); + GhostFunction g = createStateSet(states, name != null ? name : String.format("state%d", set), element); + stateSets.put(g, name != null ? namePosition : Utils.getAnnotationValuePosition(states)); + checkStatesAreNotInAnotherSet(g, states, setOfState); } if (an.contentEquals("liquidjava.specification.Ghost")) { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); @@ -219,9 +223,28 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError { Utils.getAnnotationValuePosition(rawValue)); } } - // checked once every set and ghost of the class exists, so the order of the annotations does not matter - for (Map.Entry named : namedSets.entrySet()) - checkStateSetNameIsFree(named.getKey(), named.getValue()); + // checked once every set and ghost of the class exists, so the order of the annotations does not matter; a + // generated name such as state1 can clash too + for (Map.Entry stateSet : stateSets.entrySet()) + checkStateSetNameIsFree(stateSet.getKey(), stateSet.getValue()); + } + + /** + * Reports a state of {@code set} that another set of its class also has: {@code open(this)} could not tell which of + * the two sets it is about + */ + private static void checkStatesAreNotInAnotherSet(GhostFunction set, CtNewArray states, + Map setOfState) throws LJError { + for (CtExpression state : states.getElements()) { + if (!(state instanceof CtLiteral literal && literal.getValue()instanceof String name)) + continue; + GhostFunction other = setOfState.putIfAbsent(name, set); + if (other != null) + throw new CustomError( + String.format("State '%s' is in two state sets of %s: %s and %s", name, + set.getParentClassName(), other.getName(), set.getName()), + Utils.getAnnotationValuePosition(literal)); + } } /** The name given to a state set, or null when it has none */ @@ -361,6 +384,31 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition context.addGhostFunction(new GhostFunction(f, factory, type.getQualifiedName())); } + /** + * {@code p} with each state written as a value of its set, {@code phase(x) == open}, read as the shorthand + * {@code open(x)}, in the scope of {@code element}, whose variables keep their meaning + */ + public Predicate readStateValues(Predicate p, CtElement element, SourcePosition position) throws LJError { + try { + return new Predicate(StateValues.toShorthand(p.getExpression(), context.getGhostStates(), + name -> isVariableIn(element, name))); + } catch (LJError e) { + if (e.getPosition() == null) + e.setPosition(position); + throw e; + } + } + + /** + * Whether {@code name} is a variable where {@code element} is: a parameter, _, this, return, or one in the context + */ + private boolean isVariableIn(CtElement element, String name) { + if (name.equals(Keys.WILDCARD) || name.equals(Keys.THIS) || name.equals("return") || context.hasVariable(name)) + return true; + CtExecutable executable = element instanceof CtExecutable e ? e : element.getParent(CtExecutable.class); + return executable != null && executable.getParameters().stream().anyMatch(p -> p.getSimpleName().equals(name)); + } + protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError { try { AliasDTO a = RefinementsParser.parseAliasDefinition(ref); @@ -376,6 +424,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio if (klass != null && path != null) { a.parse(path); a.resolveStaticFinalConstants(element, position); + a.readStateValues(context.getGhostStates()); if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression", ref); 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 f1ce3d1c..c2d00a08 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 @@ -56,7 +56,7 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, throw new IllegalConstructorTransitionError(Utils.getAnnotationValuePosition(from)); } } - setConstructorStates(f, an, c); + setConstructorStates(f, an, c, tc); } else if (!inheritSuperConstructorState(c, f, tc)) { setDefaultState(f, tc); } @@ -283,7 +283,7 @@ private static List> typeReferences(TypeChecker tc, List> anns, - CtElement element) throws LJError { + CtElement element, TypeChecker tc) throws LJError { List l = new ArrayList<>(); for (CtAnnotation an : anns) { Map m = an.getAllValues(); @@ -294,7 +294,8 @@ private static void setConstructorStates(RefinedFunction f, List ctAnnota private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc, CtElement e, boolean isTo) throws LJError { SourcePosition position = Utils.getLJAnnotationPosition(e, value); + p = tc.readStateValues(p, e, position); if (!p.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java new file mode 100644 index 00000000..d0e306cf --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -0,0 +1,87 @@ +package liquidjava.rj_language; + +import java.util.List; +import java.util.Objects; +import java.util.Optional; +import java.util.function.Predicate; +import java.util.stream.Collectors; + +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.GhostFunction; +import liquidjava.processor.context.GhostState; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; + +/** + * Reads a state written as a value of its state set, {@code phase(e) == open}, as the state shorthand {@code open(e)}, + * so that everything that reads states sees one form + */ +public final class StateValues { + + private StateValues() { + } + + /** + * {@code expression} with each {@code set(e) == state} read as {@code state(e)} and each {@code set(e) != state} as + * {@code !state(e)}. A name {@code isVariable} accepts keeps its meaning as a variable + * + * @throws CustomError + * when the name is not a variable and is a state of another set of the same class + */ + public static Expression toShorthand(Expression expression, List states, Predicate isVariable) + throws LJError { + return rewrite(expression.clone(), states, isVariable); + } + + private static Expression rewrite(Expression e, List states, Predicate isVariable) + throws LJError { + if (e instanceof BinaryExpression b && (b.getOperator().equals("==") || b.getOperator().equals("!="))) { + Optional state = stateOf(b.getFirstOperand(), b.getSecondOperand(), states, isVariable); + if (state.isEmpty()) + state = stateOf(b.getSecondOperand(), b.getFirstOperand(), states, isVariable); + if (state.isPresent()) + return b.getOperator().equals("==") ? state.get() : new UnaryExpression("!", state.get()); + } + for (int i = 0; i < e.getChildren().size(); i++) + e.setChild(i, rewrite(e.getChildren().get(i), states, isVariable)); + return e; + } + + /** {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} one of its states */ + private static Optional stateOf(Expression set, Expression name, List states, + Predicate isVariable) throws LJError { + if (!(set instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1 + && name instanceof Var var && !isVariable.test(var.getName()))) + return Optional.empty(); + Optional stateSet = stateSetNamed(invocation.getName(), states); + if (stateSet.isEmpty()) + return Optional.empty(); + List inSet = states.stream().filter(s -> s.getParent() == stateSet.get()).toList(); + Optional state = inSet.stream().filter(s -> s.getName().equals(var.getName())).findFirst(); + if (state.isPresent()) + return Optional.of(new FunctionInvocation(state.get().getQualifiedName(), + List.of(invocation.getArgs().get(0).clone()))); + if (isStateOfAnotherSet(var.getName(), stateSet.get(), states)) + throw new CustomError(String.format("State '%s' is not a state of '%s' (its states are %s)", var.getName(), + stateSet.get().getName(), + inSet.stream().map(GhostState::getName).collect(Collectors.joining(", ")))); + return Optional.empty(); + } + + /** The state set {@code name} refers to, preferring the one whose qualified name it is */ + private static Optional stateSetNamed(String name, List states) { + List sets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct() + .filter(set -> set.matches(name)).toList(); + return sets.stream().filter(set -> set.getQualifiedName().equals(name)).findFirst() + .or(() -> sets.stream().findFirst()); + } + + private static boolean isStateOfAnotherSet(String name, GhostFunction stateSet, List states) { + return states.stream().anyMatch(s -> s.getName().equals(name) && s.getParent() != null + && s.getParent() != stateSet && s.getParent().getPrefix().equals(stateSet.getPrefix())); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 459f460d..ec988afd 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -347,6 +347,13 @@ void foundKeepsANamedStateSetByItsName() { error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } + @Test + void queryWrittenWithItsStateSetIsOfferedAsAGuard() { + assertHints("ErrorStateValueQuery.java", + new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs it to be unlocked"), + new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()): when it returns true, d is unlocked")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general( From f176bb465e895776f72298beaaf9d3dc25c2b6ba Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 18:11:55 +0000 Subject: [PATCH 2/5] Name a state written as a value of its set as the shorthand written in the same place Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectStateValues.java | 18 +++++++++ .../liquidjava/rj_language/StateValues.java | 40 ++++++++++--------- 2 files changed, 40 insertions(+), 18 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java index 87db9328..101b1ccc 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java @@ -5,6 +5,11 @@ import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; +// an unrelated set with the same name and other states, in a class whose sets are listed before those of +// CorrectStateValues +@StateSet(name = "door", value = {"ajar", "shut"}) +class CorrectStateValueDoor {} + @StateSet(name = "door", value = {"closed", "opened"}) @StateSet(name = "lock", value = {"unlocked", "locked"}) @RefinementAlias("Shut(CorrectStateValues d) { door(d) == closed }") @@ -73,3 +78,16 @@ static void test() { v.needsOn(); } } + +// a subclass uses the set of its superclass, not the unrelated one with the same name +class CorrectStateValueSubclass extends CorrectStateValues { + + @StateRefinement(from = "door(this) == opened", to = "door(this) == closed") + public void shut() {} + + static void test() { + CorrectStateValueSubclass s = new CorrectStateValueSubclass(); + s.open(); + s.shut(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index d0e306cf..4468f24e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -51,33 +51,37 @@ private static Expression rewrite(Expression e, List states, Predica return e; } - /** {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} one of its states */ + /** + * {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} one of its states, named + * as the shorthand written in the same place, so that it is resolved the same way, in a subclass too + */ private static Optional stateOf(Expression set, Expression name, List states, Predicate isVariable) throws LJError { if (!(set instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1 && name instanceof Var var && !isVariable.test(var.getName()))) return Optional.empty(); - Optional stateSet = stateSetNamed(invocation.getName(), states); - if (stateSet.isEmpty()) - return Optional.empty(); - List inSet = states.stream().filter(s -> s.getParent() == stateSet.get()).toList(); - Optional state = inSet.stream().filter(s -> s.getName().equals(var.getName())).findFirst(); - if (state.isPresent()) - return Optional.of(new FunctionInvocation(state.get().getQualifiedName(), + List sets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct() + .filter(s -> s.matches(invocation.getName())).toList(); + if (sets.stream().anyMatch(s -> !statesOf(s, states, var.getName()).isEmpty())) + return Optional.of(new FunctionInvocation(qualifiedLike(invocation.getName(), var.getName()), List.of(invocation.getArgs().get(0).clone()))); - if (isStateOfAnotherSet(var.getName(), stateSet.get(), states)) - throw new CustomError(String.format("State '%s' is not a state of '%s' (its states are %s)", var.getName(), - stateSet.get().getName(), - inSet.stream().map(GhostState::getName).collect(Collectors.joining(", ")))); + for (GhostFunction s : sets) + if (isStateOfAnotherSet(var.getName(), s, states)) + throw new CustomError(String.format("State '%s' is not a state of '%s' (its states are %s)", + var.getName(), s.getName(), + statesOf(s, states, null).stream().map(GhostState::getName).collect(Collectors.joining(", ")))); return Optional.empty(); } - /** The state set {@code name} refers to, preferring the one whose qualified name it is */ - private static Optional stateSetNamed(String name, List states) { - List sets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct() - .filter(set -> set.matches(name)).toList(); - return sets.stream().filter(set -> set.getQualifiedName().equals(name)).findFirst() - .or(() -> sets.stream().findFirst()); + /** The states of {@code set}, or only those named {@code name} when it is not null */ + private static List statesOf(GhostFunction set, List states, String name) { + return states.stream().filter(s -> s.getParent() == set && (name == null || s.getName().equals(name))).toList(); + } + + /** {@code state} qualified as {@code setName} is: {@code a.B.phase} gives {@code a.B.open} */ + private static String qualifiedLike(String setName, String state) { + int dot = setName.lastIndexOf('.'); + return dot < 0 ? state : setName.substring(0, dot + 1) + state; } private static boolean isStateOfAnotherSet(String name, GhostFunction stateSet, List states) { From e18e67665a6604034cdf569c4e8d14875d9573f7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 18:20:58 +0000 Subject: [PATCH 3/5] Read a state value only against the sets that apply to the argument's type Co-Authored-By: Claude Opus 5.5 --- .../main/java/testSuite/ErrorStateValues.java | 4 ++ .../processor/context/AliasWrapper.java | 11 ++-- .../liquidjava/processor/facade/AliasDTO.java | 10 +-- .../refinement_checker/TypeChecker.java | 49 +++++++++++++- .../liquidjava/rj_language/StateValues.java | 65 ++++++++++++------- 5 files changed, 103 insertions(+), 36 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java index 7eac0506..b87e1fa6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java @@ -17,3 +17,7 @@ class ErrorStateValuesSharedState {} @StateSet({"state1", "open"}) // Expect: Error class ErrorStateValuesGeneratedSetName {} + +// an unrelated set named door that has a state locked does not make locked a state of the door above +@StateSet(name = "door", value = {"locked", "free"}) +class ErrorStateValuesOtherDoor {} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index 0578e62b..120bc475 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -29,10 +29,13 @@ public AliasWrapper(AliasDTO a, Factory factory, String klass, String path, Sour this.position = position; varTypes = new ArrayList<>(); varNames = a.getVarNames(); - for (String s : a.getVarTypes()) { - CtTypeReference r = Utils.getType(s.equals(klass) ? path : s, factory); - varTypes.add(r); - } + for (String s : a.getVarTypes()) + varTypes.add(parameterType(s, factory, klass, path)); + } + + /** The type of an alias parameter written {@code type}, in an alias declared on class {@code klass} at path */ + public static CtTypeReference parameterType(String type, Factory factory, String klass, String path) { + return Utils.getType(type.equals(klass) ? path : type, factory); } public String getName() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index dbe40371..71ebeeb2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -4,7 +4,6 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.LJError; -import liquidjava.processor.context.GhostState; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.StateValues; import liquidjava.rj_language.ast.Expression; @@ -52,11 +51,12 @@ public void resolveStaticFinalConstants(CtElement context, SourcePosition positi } } - // Read the states written as values of their sets, phase(x) == open, as the shorthand open(x); only the alias's - // parameters are variables, so a variable where the alias is used cannot take the place of a state - public void readStateValues(List states) throws LJError { + // Read the states written as values of their sets, phase(x) == open, as the shorthand open(x), with only the + // alias's + // parameters as variables, so a variable where the alias is used cannot take the place of a state + public void readStateValues(StateValues values) throws LJError { if (expression != null) { - this.expression = StateValues.toShorthand(expression, states, varNames::contains); + this.expression = values.toShorthand(expression); } } 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 4658d78a..40724a3d 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 @@ -25,6 +25,9 @@ import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.StateValues; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; @@ -43,6 +46,7 @@ import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtInterface; import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.CtParameter; import spoon.reflect.declaration.CtTypedElement; import spoon.reflect.declaration.CtVariable; import spoon.reflect.declaration.CtType; @@ -389,9 +393,10 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition * {@code open(x)}, in the scope of {@code element}, whose variables keep their meaning */ public Predicate readStateValues(Predicate p, CtElement element, SourcePosition position) throws LJError { + StateValues values = new StateValues(context.getGhostStates(), name -> isVariableIn(element, name), + (argument, set) -> typeIn(element, argument).map(type -> isOfType(type, set.getPrefix())).orElse(true)); try { - return new Predicate(StateValues.toShorthand(p.getExpression(), context.getGhostStates(), - name -> isVariableIn(element, name))); + return new Predicate(values.toShorthand(p.getExpression())); } catch (LJError e) { if (e.getPosition() == null) e.setPosition(position); @@ -409,6 +414,44 @@ private boolean isVariableIn(CtElement element, String name) { return executable != null && executable.getParameters().stream().anyMatch(p -> p.getSimpleName().equals(name)); } + /** The type of a state's argument where {@code element} is: this, _, a parameter, a variable, or old of one */ + private Optional> typeIn(CtElement element, Expression argument) { + if (argument instanceof FunctionInvocation old && old.getName().equals(Keys.OLD) && old.getArgs().size() == 1) + return typeIn(element, old.getArgs().get(0)); + if (!(argument instanceof Var var)) + return Optional.empty(); + String name = var.getName(); + if (name.equals(Keys.THIS)) + return Optional.ofNullable(getQualifiedClassName(element)).map(c -> factory.Type().createReference(c)); + if (name.equals(Keys.WILDCARD)) + return element instanceof CtTypedElement typed ? Optional.ofNullable(typed.getType()) : Optional.empty(); + CtExecutable executable = element instanceof CtExecutable e ? e : element.getParent(CtExecutable.class); + if (executable != null) + for (CtParameter parameter : executable.getParameters()) + if (parameter.getSimpleName().equals(name)) + return Optional.ofNullable(parameter.getType()); + return context.hasVariable(name) ? Optional.ofNullable(context.getVariableByName(name).getType()) + : Optional.empty(); + } + + /** + * Reads the states written as values of their sets in the body of {@code alias}, declared on class {@code klass} at + * {@code path}: only its parameters are variables, typed as they are declared + */ + private StateValues aliasStateValues(AliasDTO alias, String klass, String path) { + return new StateValues(context.getGhostStates(), alias.getVarNames()::contains, (argument, set) -> { + int parameter = argument instanceof Var var ? alias.getVarNames().indexOf(var.getName()) : -1; + return parameter < 0 + || isOfType(AliasWrapper.parameterType(alias.getVarTypes().get(parameter), factory, klass, path), + set.getPrefix()); + }); + } + + /** Whether {@code type} is the class {@code className} or one of its subtypes */ + private boolean isOfType(CtTypeReference type, String className) { + return type.getQualifiedName().equals(className) || type.isSubtypeOf(factory.Type().createReference(className)); + } + protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError { try { AliasDTO a = RefinementsParser.parseAliasDefinition(ref); @@ -424,7 +467,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio if (klass != null && path != null) { a.parse(path); a.resolveStaticFinalConstants(element, position); - a.readStateValues(context.getGhostStates()); + a.readStateValues(aliasStateValues(a, klass, path)); if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression", ref); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index 4468f24e..2361dd27 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -3,6 +3,7 @@ import java.util.List; import java.util.Objects; import java.util.Optional; +import java.util.function.BiPredicate; import java.util.function.Predicate; import java.util.stream.Collectors; @@ -22,59 +23,75 @@ */ public final class StateValues { - private StateValues() { + private final List states; + private final Predicate isVariable; + private final BiPredicate appliesTo; + + /** + * @param isVariable + * whether a name is a variable where the spec is written; a variable keeps its meaning + * @param appliesTo + * whether a state set can be applied to an argument, by the argument's type; true when it is not known + */ + public StateValues(List states, Predicate isVariable, + BiPredicate appliesTo) { + this.states = states; + this.isVariable = isVariable; + this.appliesTo = appliesTo; } /** * {@code expression} with each {@code set(e) == state} read as {@code state(e)} and each {@code set(e) != state} as - * {@code !state(e)}. A name {@code isVariable} accepts keeps its meaning as a variable + * {@code !state(e)} * * @throws CustomError * when the name is not a variable and is a state of another set of the same class */ - public static Expression toShorthand(Expression expression, List states, Predicate isVariable) - throws LJError { - return rewrite(expression.clone(), states, isVariable); + public Expression toShorthand(Expression expression) throws LJError { + return rewrite(expression.clone()); } - private static Expression rewrite(Expression e, List states, Predicate isVariable) - throws LJError { + private Expression rewrite(Expression e) throws LJError { if (e instanceof BinaryExpression b && (b.getOperator().equals("==") || b.getOperator().equals("!="))) { - Optional state = stateOf(b.getFirstOperand(), b.getSecondOperand(), states, isVariable); + Optional state = stateOf(b.getFirstOperand(), b.getSecondOperand()); if (state.isEmpty()) - state = stateOf(b.getSecondOperand(), b.getFirstOperand(), states, isVariable); + state = stateOf(b.getSecondOperand(), b.getFirstOperand()); if (state.isPresent()) return b.getOperator().equals("==") ? state.get() : new UnaryExpression("!", state.get()); } for (int i = 0; i < e.getChildren().size(); i++) - e.setChild(i, rewrite(e.getChildren().get(i), states, isVariable)); + e.setChild(i, rewrite(e.getChildren().get(i))); return e; } /** - * {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} one of its states, named - * as the shorthand written in the same place, so that it is resolved the same way, in a subclass too + * {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} a state of every set of + * that name that applies to {@code e}. It is named as the shorthand written in the same place, so that it is + * resolved the same way, in a subclass too. When only some of those sets have the state, nothing is read, and the + * name stays an unknown variable */ - private static Optional stateOf(Expression set, Expression name, List states, - Predicate isVariable) throws LJError { + private Optional stateOf(Expression set, Expression name) throws LJError { if (!(set instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1 && name instanceof Var var && !isVariable.test(var.getName()))) return Optional.empty(); + Expression argument = invocation.getArgs().get(0); List sets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct() - .filter(s -> s.matches(invocation.getName())).toList(); - if (sets.stream().anyMatch(s -> !statesOf(s, states, var.getName()).isEmpty())) + .filter(s -> s.matches(invocation.getName()) && appliesTo.test(argument, s)).toList(); + long withState = sets.stream().filter(s -> !statesOf(s, var.getName()).isEmpty()).count(); + if (withState > 0 && withState == sets.size()) return Optional.of(new FunctionInvocation(qualifiedLike(invocation.getName(), var.getName()), - List.of(invocation.getArgs().get(0).clone()))); - for (GhostFunction s : sets) - if (isStateOfAnotherSet(var.getName(), s, states)) - throw new CustomError(String.format("State '%s' is not a state of '%s' (its states are %s)", - var.getName(), s.getName(), - statesOf(s, states, null).stream().map(GhostState::getName).collect(Collectors.joining(", ")))); + List.of(argument.clone()))); + if (withState == 0) + for (GhostFunction s : sets) + if (isStateOfAnotherSet(var.getName(), s)) + throw new CustomError(String.format("State '%s' is not a state of '%s' (its states are %s)", + var.getName(), s.getName(), + statesOf(s, null).stream().map(GhostState::getName).collect(Collectors.joining(", ")))); return Optional.empty(); } /** The states of {@code set}, or only those named {@code name} when it is not null */ - private static List statesOf(GhostFunction set, List states, String name) { + private List statesOf(GhostFunction set, String name) { return states.stream().filter(s -> s.getParent() == set && (name == null || s.getName().equals(name))).toList(); } @@ -84,7 +101,7 @@ private static String qualifiedLike(String setName, String state) { return dot < 0 ? state : setName.substring(0, dot + 1) + state; } - private static boolean isStateOfAnotherSet(String name, GhostFunction stateSet, List states) { + private boolean isStateOfAnotherSet(String name, GhostFunction stateSet) { return states.stream().anyMatch(s -> s.getName().equals(name) && s.getParent() != null && s.getParent() != stateSet && s.getParent().getPrefix().equals(stateSet.getPrefix())); } From a4d52e3f7f6b4d83c1482d7e54bf7dd65321c81c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 18:31:21 +0000 Subject: [PATCH 4/5] Read a state value from any set of the argument's type that has it, as the shorthand does Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectStateValues.java | 11 ++++++++ .../refinement_checker/TypeChecker.java | 12 +++++---- .../liquidjava/rj_language/StateValues.java | 25 ++++++++++--------- 3 files changed, 31 insertions(+), 17 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java index 101b1ccc..2326e7fb 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java @@ -91,3 +91,14 @@ static void test() { s.shut(); } } + +// a subclass that declares its own set named door uses its states, as the shorthand does +@StateSet(name = "door", value = {"open", "closed"}) +class CorrectStateValueBase {} + +@StateSet(name = "door", value = {"ajar", "shut"}) +class CorrectStateValueChild extends CorrectStateValueBase { + + @StateRefinement(from = "door(this) == shut", to = "door(this) == ajar") + public void push() {} +} 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 40724a3d..85c0657c 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 @@ -394,7 +394,7 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition */ public Predicate readStateValues(Predicate p, CtElement element, SourcePosition position) throws LJError { StateValues values = new StateValues(context.getGhostStates(), name -> isVariableIn(element, name), - (argument, set) -> typeIn(element, argument).map(type -> isOfType(type, set.getPrefix())).orElse(true)); + argument -> typeIn(element, argument).map(type -> set -> isOfType(type, set.getPrefix()))); try { return new Predicate(values.toShorthand(p.getExpression())); } catch (LJError e) { @@ -439,11 +439,13 @@ private Optional> typeIn(CtElement element, Expression argume * {@code path}: only its parameters are variables, typed as they are declared */ private StateValues aliasStateValues(AliasDTO alias, String klass, String path) { - return new StateValues(context.getGhostStates(), alias.getVarNames()::contains, (argument, set) -> { + return new StateValues(context.getGhostStates(), alias.getVarNames()::contains, argument -> { int parameter = argument instanceof Var var ? alias.getVarNames().indexOf(var.getName()) : -1; - return parameter < 0 - || isOfType(AliasWrapper.parameterType(alias.getVarTypes().get(parameter), factory, klass, path), - set.getPrefix()); + if (parameter < 0) + return Optional.empty(); + CtTypeReference type = AliasWrapper.parameterType(alias.getVarTypes().get(parameter), factory, klass, + path); + return Optional.of(set -> isOfType(type, set.getPrefix())); }); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index 2361dd27..abcc8236 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -3,7 +3,7 @@ import java.util.List; import java.util.Objects; import java.util.Optional; -import java.util.function.BiPredicate; +import java.util.function.Function; import java.util.function.Predicate; import java.util.stream.Collectors; @@ -25,19 +25,19 @@ public final class StateValues { private final List states; private final Predicate isVariable; - private final BiPredicate appliesTo; + private final Function>> setsFor; /** * @param isVariable * whether a name is a variable where the spec is written; a variable keeps its meaning - * @param appliesTo - * whether a state set can be applied to an argument, by the argument's type; true when it is not known + * @param setsFor + * the state sets that can be applied to an argument, by its type, or empty when its type is not known */ public StateValues(List states, Predicate isVariable, - BiPredicate appliesTo) { + Function>> setsFor) { this.states = states; this.isVariable = isVariable; - this.appliesTo = appliesTo; + this.setsFor = setsFor; } /** @@ -65,20 +65,21 @@ private Expression rewrite(Expression e) throws LJError { } /** - * {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} a state of every set of - * that name that applies to {@code e}. It is named as the shorthand written in the same place, so that it is - * resolved the same way, in a subclass too. When only some of those sets have the state, nothing is read, and the - * name stays an unknown variable + * {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} a state of a set of that + * name that applies to the type of {@code e}, or, when that type is not known, of every set of that name. It is + * named as the shorthand written in the same place, so that it is resolved the same way, in a subclass too. + * Otherwise nothing is read, and the name stays an unknown variable */ private Optional stateOf(Expression set, Expression name) throws LJError { if (!(set instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1 && name instanceof Var var && !isVariable.test(var.getName()))) return Optional.empty(); Expression argument = invocation.getArgs().get(0); + Optional> ofType = setsFor.apply(argument); List sets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct() - .filter(s -> s.matches(invocation.getName()) && appliesTo.test(argument, s)).toList(); + .filter(s -> s.matches(invocation.getName()) && ofType.map(p -> p.test(s)).orElse(true)).toList(); long withState = sets.stream().filter(s -> !statesOf(s, var.getName()).isEmpty()).count(); - if (withState > 0 && withState == sets.size()) + if (withState > 0 && (ofType.isPresent() || withState == sets.size())) return Optional.of(new FunctionInvocation(qualifiedLike(invocation.getName(), var.getName()), List.of(argument.clone()))); if (withState == 0) From 90ddc5543b46d2c245a4a0f3c18380c6171df21b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 19:46:18 +0000 Subject: [PATCH 5/5] Test the set applied as a method of this, and with this left out Co-Authored-By: Claude Opus 5.5 --- .../main/java/testSuite/CorrectStateValues.java | 5 +++-- .../src/main/java/testSuite/ErrorStateValues.java | 15 +++++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java index 2326e7fb..42ce986e 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java @@ -21,7 +21,8 @@ public CorrectStateValues() {} @StateRefinement(from = "door(this) == closed && lock(this) != locked", to = "door(this) == opened") public void open() {} - @StateRefinement(from = "door(this) == opened", to = "door(this) == closed") + // the set can also be applied as a method of this, or with this left out + @StateRefinement(from = "this.door() == opened", to = "door() == closed") public void close() {} // when it fails, the lock set keeps its value @@ -30,7 +31,7 @@ public boolean tryLock() { return true; } - @StateRefinement(from = "lock(this) == locked", to = "lock(this) == unlocked") + @StateRefinement(from = "locked == this.lock()", to = "lock() != locked") public void unlock() {} // the parameter closed keeps its meaning: the door takes its value diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java index b87e1fa6..a75242fd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java @@ -21,3 +21,18 @@ class ErrorStateValuesGeneratedSetName {} // an unrelated set named door that has a state locked does not make locked a state of the door above @StateSet(name = "door", value = {"locked", "free"}) class ErrorStateValuesOtherDoor {} + +// the set applied as a method of this, or with this left out, constrains the same state +@StateSet(name = "door", value = {"shut", "ajar"}) +class ErrorStateValueForms { + + @StateRefinement(to = "door() == shut") + public ErrorStateValueForms() {} + + @StateRefinement(from = "this.door() == ajar") + public void close() {} + + static void test() { + new ErrorStateValueForms().close(); // Expect: State Refinement Error + } +}