Compute loop typestates as a fixpoint over iterations

liquidjava-api/src/main/java/liquidjava/specification/StateSet.java

@@ -9,9 +9,10 @@
 /**
  * Annotation to create a set of disjoint states in which class objects can be.
  * <p>
- * An object will always be in exactly one state from each state set at any given time,
- * and cannot be in more than one state from the same state set (e.g., {@code open} and {@code closed} simultaneously).
- * To allow an object to be in multiple states at once, they must be from different state sets.
+ * An object cannot be in more than one state from the same state set at a time (e.g., {@code open} and
+ * {@code closed} simultaneously). To allow an object to be in multiple states at once, they must be from different
+ * state sets. An object may also be in none of the states of a set, e.g. after
+ * {@code @StateRefinement(to = "!open(this) && !closed(this)")}.
  * <p>
  * <strong>Example:</strong>
  * <pre>
@@ -21,6 +22,7 @@
  * public class File {
  *    // ...
  * }
+ * }
  * </pre>
  *
  * @see StateRefinement

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

@@ -0,0 +1,32 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// A loop body checked more than once creates fresh receivers in each check, not reusing one of an earlier check
+@StateSet({"open", "marked", "closed"})
+public class CorrectLoopFreshReceivers {
+    @StateRefinement(to = "open(this)")
+    CorrectLoopFreshReceivers() {}
+
+    @StateRefinement(from = "open(this)", to = "marked(this)")
+    @StateRefinement(from = "marked(this)")
+    void mark() {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    @StateRefinement(from = "!closed(this)", to = "closed(this)")
+    void close() {}
+
+    static void freshReceivers(int n) {
+        CorrectLoopFreshReceivers b = new CorrectLoopFreshReceivers();
+        while (n > 0) {
+            b.mark(); // the body is checked from open, then from open or marked
+            new CorrectLoopFreshReceivers().close();
+            new CorrectLoopFreshReceivers().mark();
+            Runnable r = () -> new CorrectLoopFreshReceivers().close();
+            n--;
+        }
+    }
+}

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

@@ -0,0 +1,113 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// The states of an object at the start of every iteration of a loop are those before the loop and those at the end of
+// any iteration, computed until they stop changing
+@StateSet({"open", "marked", "closed"})
+public class CorrectLoopStateFixpoint {
+    @StateRefinement(to = "open(this)")
+    CorrectLoopStateFixpoint() {}
+
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    void read() {}
+
+    @StateRefinement(from = "open(this)", to = "marked(this)")
+    @StateRefinement(from = "marked(this)")
+    void mark() {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    @StateRefinement(from = "!closed(this)", to = "closed(this)")
+    void close() {}
+
+    // b is open or marked in every iteration: both allow read and mark
+    static void openOrMarked(int n) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        for (int i = 0; i < n; i++) {
+            b.read();
+            b.mark();
+        }
+        b.read();
+        b.close();
+    }
+
+    // the body restores the state it starts from
+    static void restoredInBody(int n) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        while (n > 0) {
+            b.mark();
+            b.reset();
+            n--;
+        }
+        b.mark();
+        b.reset();
+    }
+
+    static void nestedLoops(int n) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        for (int i = 0; i < n; i++) {
+            for (int j = 0; j < i; j++)
+                b.mark();
+            b.read();
+        }
+        b.close();
+    }
+
+    static void doWhile(int n) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        do {
+            b.mark();
+            n--;
+        } while (n > 0);
+        b.reset();
+    }
+
+    static void forEach(int[] values) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        for (int value : values) {
+            b.mark();
+            b.read();
+        }
+        b.read();
+    }
+
+    // the only exit is the break, with b marked
+    static void exitOnlyThroughBreak(int n) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        for (;;) {
+            b.mark();
+            if (n > 3)
+                break;
+            b.reset();
+            n++;
+        }
+        b.reset();
+    }
+
+    // a continue skips the close, which ends the loop with a return
+    static void continueOrClose(int n) {
+        CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint();
+        for (int i = 0; i < n; i++) {
+            b.read();
+            if (i < 5)
+                continue;
+            b.close();
+            return;
+        }
+        b.close();
+    }
+
+    @StateRefinement(from = "open(this)")
+    void thisOpenOrMarked(int n) {
+        while (n > 0) {
+            read();
+            this.mark();
+            n--;
+        }
+        read();
+    }
+}

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

@@ -0,0 +1,31 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// An object may be in none of the states of a set, before the loop or after a call in its body
+@StateSet({"open", "closed"})
+public class CorrectLoopStateNone {
+    @StateRefinement(to = "!open(this) && !closed(this)")
+    CorrectLoopStateNone() {}
+
+    @StateRefinement(from = "!open(this) && !closed(this)", to = "open(this)")
+    void open() {}
+
+    @StateRefinement(from = "open(this)", to = "!open(this) && !closed(this)")
+    void read() {}
+
+    @StateRefinement(from = "!closed(this)", to = "closed(this)")
+    void close() {}
+
+    // every iteration starts and ends in no state
+    static void openAndRead(int n) {
+        CorrectLoopStateNone value = new CorrectLoopStateNone();
+        for (int i = 0; i < n; i++) {
+            value.open();
+            value.read();
+        }
+        value.open();
+        value.close();
+    }
+}

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

@@ -0,0 +1,38 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// A call whose entry states are each unprovable but whose union is provable is allowed, and the object ends up in a
+// state given by any alternative whose entry state it may be in
+@StateSet({"open", "marked", "closed"})
+public class CorrectStateChangeFromUnion {
+    @StateRefinement(to = "open(this)")
+    CorrectStateChangeFromUnion() {}
+
+    @StateRefinement(from = "open(this)", to = "marked(this)")
+    @StateRefinement(from = "marked(this)")
+    void mark() {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    @StateRefinement(from = "marked(this)", to = "closed(this)")
+    void close() {}
+
+    // open goes to marked, marked stays marked
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    void markFromEither() {
+        mark();
+        reset();
+    }
+
+    // both alternatives go to closed
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    void closeFromEither() {
+        close();
+    }
+}

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

@@ -0,0 +1,28 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// A block left by a labelled break completes normally: the state it leaves reaches the code after the if
+@StateSet({"open", "closed"})
+public class ErrorLabelledBlockInIf {
+    @StateRefinement(to = "open(this)")
+    ErrorLabelledBlockInIf() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    void close() {}
+
+    @StateRefinement(from = "open(this)")
+    void read() {}
+
+    static void closedInLabelledBlock(boolean c) {
+        ErrorLabelledBlockInIf b = new ErrorLabelledBlockInIf();
+        if (c) {
+            done: {
+                b.close();
+                break done;
+            }
+        }
+        b.read(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,31 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// A loop body checked more than once creates fresh receivers in each check, not reusing one of an earlier check
+@StateSet({"open", "marked", "closed"})
+public class ErrorLoopFreshReceivers {
+    @StateRefinement(to = "open(this)")
+    ErrorLoopFreshReceivers() {}
+
+    @StateRefinement(from = "open(this)", to = "marked(this)")
+    @StateRefinement(from = "marked(this)")
+    void mark() {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    @StateRefinement(from = "!closed(this)", to = "closed(this)")
+    void close() {}
+
+    // a fresh object is open, and reset needs it marked
+    static void freshReceiverInLambda(int n) {
+        ErrorLoopFreshReceivers b = new ErrorLoopFreshReceivers();
+        while (n > 0) {
+            b.mark(); // the body is checked from open, then from open or marked
+            Runnable r = () -> new ErrorLoopFreshReceivers().reset(); // Expect: State Refinement Error
+            n--;
+        }
+    }
+}

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

@@ -0,0 +1,53 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// The states of an object at the start of every iteration of a loop are those before the loop and those at the end of
+// any iteration, computed until they stop changing
+@StateSet({"first", "second", "third"})
+public class ErrorLoopStateFixpoint {
+    @StateRefinement(to = "first(this)")
+    ErrorLoopStateFixpoint() {}
+
+    @StateRefinement(from = "first(this)", to = "second(this)")
+    @StateRefinement(from = "second(this)", to = "third(this)")
+    @StateRefinement(from = "third(this)")
+    void step() {}
+
+    @StateRefinement(from = "first(this)")
+    @StateRefinement(from = "second(this)")
+    void early() {}
+
+    @StateRefinement(from = "third(this)")
+    void last() {}
+
+    // third is reached in the third iteration only, after the states grow twice
+    static void thirdIteration(int n) {
+        ErrorLoopStateFixpoint o = new ErrorLoopStateFixpoint();
+        for (int i = 0; i < n; i++) {
+            o.early(); // Expect: State Refinement Error
+            o.step();
+        }
+    }
+
+    // after two steps in the loop, o may still be first or second
+    static void notEnoughIterations(int n) {
+        ErrorLoopStateFixpoint o = new ErrorLoopStateFixpoint();
+        while (n > 0) {
+            o.step();
+            o.step();
+            n--;
+        }
+        o.last(); // Expect: State Refinement Error
+    }
+
+    // the error in the lambda is reported once, although the loop body is checked from more than one set of states
+    static void errorInLambdaInLoop(int n) {
+        ErrorLoopStateFixpoint o = new ErrorLoopStateFixpoint();
+        for (int i = 0; i < n; i++) {
+            o.step();
+            Runnable r = () -> o.last(); // Expect: State Refinement Error
+        }
+    }
+}