Accept a state written as a value of its set: phase(this) == open

liquidjava-example/src/main/java/testSuite/CorrectStateValues.java

@@ -0,0 +1,105 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+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 }")
+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() {}
+
+    // 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
+    @StateRefinement(from = "door(this) == closed", to = "return ? lock(this) == locked : lock(this) == lock(old(this))")
+    public boolean tryLock() {
+        return true;
+    }
+
+    @StateRefinement(from = "locked == this.lock()", to = "lock() != locked")
+    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();
+    }
+}
+
+// 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();
+    }
+}
+
+// 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() {}
+}

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

liquidjava-example/src/main/java/testSuite/ErrorStateValues.java

@@ -0,0 +1,38 @@
+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 {}
+
+// 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
+    }
+}

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() {

liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java

@@ -5,6 +5,7 @@
 
 import liquidjava.diagnostics.errors.LJError;
 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 +51,15 @@ public void resolveStaticFinalConstants(CtElement context, SourcePosition positi
         }
     }
 
+    // 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 = values.toShorthand(expression);
+        }
+    }
+
     public String getName() {
         return name;
     }

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

@@ -24,6 +24,10 @@
 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.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;
@@ -39,8 +43,10 @@
 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.CtParameter;
 import spoon.reflect.declaration.CtTypedElement;
 import spoon.reflect.declaration.CtVariable;
 import spoon.reflect.declaration.CtType;
@@ -126,6 +132,7 @@ public Optional<Predicate> 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,18 +203,19 @@ public Optional<String> getMessageFromAnnotation(CtElement element) {
     @SuppressWarnings("unchecked")
     public void registerGhostsAndStateSets(CtElement element) throws LJError {
         int set = 0;
-        Map<GhostFunction, SourcePosition> namedSets = new LinkedHashMap<>();
+        Map<GhostFunction, SourcePosition> stateSets = new LinkedHashMap<>();
+        Map<String, GhostFunction> setOfState = new HashMap<>();
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
             String an = ann.getAnnotationType().getQualifiedName();
             if (an.contentEquals("liquidjava.specification.StateSet")) {
                 set++;
                 CtExpression<?> nameValue = ann.getValues().get("name");
                 SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue);
                 String name = stateSetName(nameValue, namePosition);
-                GhostFunction g = createStateSet((CtNewArray<String>) ann.getAllValues().get("value"),
-                        name != null ? name : String.format("state%d", set), element);
-                if (name != null)
-                    namedSets.put(g, namePosition);
+                CtNewArray<String> states = (CtNewArray<String>) 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<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
@@ -219,9 +227,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<GhostFunction, SourcePosition> 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<GhostFunction, SourcePosition> 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<String> states,
+            Map<String, GhostFunction> 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 +388,72 @@ 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 {
+        StateValues values = new StateValues(context.getGhostStates(), name -> isVariableIn(element, name),
+                argument -> typeIn(element, argument).map(type -> set -> isOfType(type, set.getPrefix())));
+        try {
+            return new Predicate(values.toShorthand(p.getExpression()));
+        } 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));
+    }
+
+    /** The type of a state's argument where {@code element} is: this, _, a parameter, a variable, or old of one */
+    private Optional<CtTypeReference<?>> 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 -> {
+            int parameter = argument instanceof Var var ? alias.getVarNames().indexOf(var.getName()) : -1;
+            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()));
+        });
+    }
+
+    /** 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);
@@ -376,6 +469,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
             if (klass != null && path != null) {
                 a.parse(path);
                 a.resolveStaticFinalConstants(element, position);
+                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);