diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java index 376c071bd..ad074c482 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java +++ b/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. *

- * 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)")}. *

* Example: * 

@@ -21,6 +22,7 @@
  * public class File {
  *    // ...
  * }
+ * }
  *
* * @see StateRefinement diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopFreshReceivers.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopFreshReceivers.java new file mode 100644 index 000000000..e1f1b9c61 --- /dev/null +++ b/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--; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopStateFixpoint.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopStateFixpoint.java new file mode 100644 index 000000000..ed5bcff5d --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopStateNone.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopStateNone.java new file mode 100644 index 000000000..8f8698b4e --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateChangeFromUnion.java b/liquidjava-example/src/main/java/testSuite/CorrectStateChangeFromUnion.java new file mode 100644 index 000000000..804fc9510 --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLabelledBlockInIf.java b/liquidjava-example/src/main/java/testSuite/ErrorLabelledBlockInIf.java new file mode 100644 index 000000000..0eca519d5 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopFreshReceivers.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopFreshReceivers.java new file mode 100644 index 000000000..baa585ffa --- /dev/null +++ b/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--; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateFixpoint.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateFixpoint.java new file mode 100644 index 000000000..8e3e520ec --- /dev/null +++ b/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 + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java new file mode 100644 index 000000000..dd82fb1f7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java @@ -0,0 +1,77 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Loops with jumps whose states are not followed (a break to a labelled block, or through a finally) havoc the +// typestates of the objects they change, as before the fixpoint: these tests pin that fallback +@StateSet({"open", "marked", "closed"}) +public class ErrorLoopStateJumps { + @StateRefinement(to = "open(this)") + ErrorLoopStateJumps() {} + + @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() {} + + @StateRefinement(from = "open(this)") + void needOpen() {} + + // break done: the state of b is unknown in the body (the fixpoint would find it closed in the second iteration) + static void labelledBlockEndsBody(int n) { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + while (n > 0) { + b.close(); // Expect: State Refinement Error + n--; + done: { + break done; + } + } + } + + static void labelledBlockEndsDoWhileBody(int n) { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + do { + b.close(); // Expect: State Refinement Error + n--; + done: { + break done; + } + } while (n > 0); + } + + // break out: the state of b is unknown in the body (the fixpoint would miss the marked state at the break) + static void breakOutOfEnclosingBlock(int n) { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + out: { + while (n > 0) { + b.mark(); // Expect: State Refinement Error + if (n == 3) + break out; + b.reset(); + n--; + } + } + b.needOpen(); + } + + // a break through a finally: the state of b is unknown in the body (the finally closes b after the break) + static void breakThroughFinally() { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + while (true) { + try { + b.mark(); // Expect: State Refinement Error + break; + } finally { + b.close(); + } + } + b.reset(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java new file mode 100644 index 000000000..dc699592f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java @@ -0,0 +1,35 @@ +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 ErrorLoopStateNone { + @StateRefinement(to = "!open(this) && !closed(this)") + ErrorLoopStateNone() {} + + @StateRefinement(from = "!open(this) && !closed(this)", to = "open(this)") + void open() {} + + @StateRefinement(from = "open(this)", to = "!open(this) && !closed(this)") + void read() {} + + // value is in no state before the loop, as after the constructor + static void noneBeforeLoop(int count) { + ErrorLoopStateNone value = new ErrorLoopStateNone(); + while (count > 0) { + value.read(); // Expect: State Refinement Error + count--; + } + } + + // read leaves value in no state, so the second iteration cannot read + static void noneInSecondIteration(int n) { + ErrorLoopStateNone value = new ErrorLoopStateNone(); + value.open(); + for (int i = 0; i < n; i++) { + value.read(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java new file mode 100644 index 000000000..4d07a1f53 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java @@ -0,0 +1,49 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Each check of a loop body starts from the same facts: the values left by an earlier check must not leak into it +@StateSet({"open", "closed"}) +public class ErrorLoopStatePasses { + @StateRefinement(to = "open(this)") + ErrorLoopStatePasses() {} + + @StateRefinement(to = "closed(this)") + void close() {} + + @StateRefinement(from = "closed(this)", to = "open(this)") + void reopen() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + @StateRefinement(from = "closed(this)", to = "open(this)") + void toggle() {} + + // the loop is never entered, so b is still open; x == 0 from the previous check must not make the exit impossible + static void neverEntered() { + ErrorLoopStatePasses b = new ErrorLoopStatePasses(); + int x = 100; + while (x < 10) { + b.close(); + x = 0; + } + b.reopen(); // Expect: State Refinement Error + } + + // in the first iteration y == 0; x == 7 from the previous check must not hide the error in the lambda + static void lambdaInFirstIteration(int n) { + ErrorLoopStatePasses t = new ErrorLoopStatePasses(); + int x = 0; + while (n > 0) { + t.toggle(); + final int y = x; + Runnable r = () -> { + @Refinement("_ == 7") + int z = y; // Expect: Refinement Error + }; + x = 7; + n--; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java b/liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java new file mode 100644 index 000000000..4d5182472 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java @@ -0,0 +1,36 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "marked", "closed"}) +public class ErrorStateChangeFromUnion { + @StateRefinement(to = "open(this)") + ErrorStateChangeFromUnion() {} + + @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)") + void closeIfOpen() {} + + // closed is in no entry state of mark + @StateRefinement(from = "open(this)") + @StateRefinement(from = "closed(this)") + void markFromOpenOrClosed() { + mark(); // Expect: State Refinement Error + } + + // after closeIfOpen, the object is closed or still marked, so reset is not allowed + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void resetAfterEither() { + closeIfOpen(); + reset(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java new file mode 100644 index 000000000..4e0b9fcf1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.loop_state_external_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.BufferedReader") +@StateSet({"open", "marked", "closed"}) +public interface BufferedReaderRefinements { + @StateRefinement(to = "open(this)") + void BufferedReader(java.io.Reader in); + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + String readLine(); + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark(int readAheadLimit); + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset(); + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java new file mode 100644 index 000000000..b3bed7f83 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java @@ -0,0 +1,106 @@ +package testSuite.classes.loop_state_external_correct; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.Reader; + +// Issue #427: the states of an object whose class has an external spec, computed over the iterations of a loop +public class Test { + // the body restores the state it starts from + static void markAndResetInLoop(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + while (k < n) { + br.mark(100); + br.readLine(); + br.reset(); + k++; + } + br.mark(100); + br.reset(); + br.close(); + } + + // br is open or marked at the start of every iteration and after the loop + static void openOrMarked(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); + br.mark(100); + } + br.readLine(); + br.close(); + } + + static void doWhile(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + do { + br.mark(100); + br.reset(); + k++; + } while (k < n); + br.close(); + } + + static void forEach(Reader in, int[] values) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int value : values) { + br.mark(value); + br.readLine(); + } + br.readLine(); + br.close(); + } + + // marked on every path to the next iteration and to the exit + static void markBeforeContinueAndBreak(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + br.mark(100); + for (int i = 0; i < n; i++) { + br.reset(); + br.mark(100); + if (i > 2) + continue; + if (i > 5) + break; + } + br.reset(); + br.close(); + } + + // the inner loop leaves br open or marked, which the outer loop allows + static void nestedLoops(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); + for (int j = 0; j < i; j++) + br.mark(100); + } + br.close(); + } + + // the fix of the tabu-timetabling bug: mark before the inner loop + static void markBeforeInnerLoop(Reader in) throws IOException { + BufferedReader br = new BufferedReader(in); + String currentLine; + while ((currentLine = br.readLine()) != null) { + br.mark(10000); + String nextLine; + while ((nextLine = br.readLine()) != null && currentLine.equals(nextLine)) { + br.mark(10000); + } + br.reset(); + } + br.close(); + } + + // closed only when the loop ends + static void closeAfterLoop(Reader in) throws IOException { + BufferedReader br = new BufferedReader(in); + while (br.readLine() != null) { + br.readLine(); + } + br.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java new file mode 100644 index 000000000..d23446171 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.loop_state_external_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.BufferedReader") +@StateSet({"open", "marked", "closed"}) +public interface BufferedReaderRefinements { + @StateRefinement(to = "open(this)") + void BufferedReader(java.io.Reader in); + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + String readLine(); + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark(int readAheadLimit); + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset(); + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java new file mode 100644 index 000000000..ae7a9d095 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java @@ -0,0 +1,98 @@ +package testSuite.classes.loop_state_external_error; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.Reader; + +// Issue #427: the state after a loop, and at the start of every iteration, of an object whose class has an external +// spec +public class Test { + // the loop may run zero times, leaving br open + static void zeroIterations(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + while (k < n) { + br.mark(100); + k++; + } + br.reset(); // Expect: State Refinement Error + } + + // from the second iteration on, br is closed + static void laterIteration(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); // Expect: State Refinement Error + br.close(); + } + } + + static void doWhileLaterIteration(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + do { + br.readLine(); // Expect: State Refinement Error + br.close(); + k++; + } while (k < n); + } + + static void forEachMayBeEmpty(Reader in, int[] values) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int value : values) { + br.mark(value); + } + br.reset(); // Expect: State Refinement Error + } + + // a continue goes on to the next iteration with br closed + static void closedBeforeContinue(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); // Expect: State Refinement Error + if (i > 2) { + br.close(); + continue; + } + } + } + + // the loop exits through its condition with br open, or through the break with br marked + static void breakOrCondition(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + while (k < n) { + br.mark(100); + if (k > 2) + break; + br.reset(); + k++; + } + br.reset(); // Expect: State Refinement Error + } + + // marked by an inner loop, which may run zero times, in the second iteration of the outer one + static void nestedLoops(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.reset(); // Expect: State Refinement Error + for (int j = 0; j < i; j++) + br.mark(100); + } + } + + // tabu-timetabling InputReader: the inner loop may stop at once, when the next line belongs to another student, + // and then reset runs without a mark ("Stream not marked") + static void markOnlyInInnerLoop(Reader in) throws IOException { + BufferedReader br = new BufferedReader(in); + String currentLine; + while ((currentLine = br.readLine()) != null) { + String nextLine; + while ((nextLine = br.readLine()) != null && currentLine.equals(nextLine)) { + br.mark(10000); + } + br.reset(); // Expect: State Refinement Error + } + br.close(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java new file mode 100644 index 000000000..96d20235c --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java @@ -0,0 +1,172 @@ +package liquidjava.processor.refinement_checker; + +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.RefinedVariable; +import liquidjava.processor.context.Variable; +import liquidjava.processor.context.VariableInstance; +import liquidjava.processor.state_machine.State; +import liquidjava.processor.state_machine.StateMachineBuilder; +import liquidjava.processor.state_machine.StateSolver; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtLoop; + +/** + * The typestates of the objects a loop may change, as sets of the states of their class. The states at the loop head + * start as the states before the loop and grow with the states at the end of each checked iteration until they stop + * changing. A class has finitely many states, so they stop changing after at most one growth per state. + * + *

+ * While the body is checked, the states where control leaves the iteration are recorded: where it may exit the loop + * (the condition, a break), and where it goes on to the next iteration (the end of the body, a continue). + */ +class LoopTypestates { + + private final RefinementTypeChecker checker; + private final CtLoop loop; + private final Map> classStates = new LinkedHashMap<>(); + private final Map> head = new LinkedHashMap<>(); + private Map> exit; + private Map> continued; + private Map> nextIteration; + // whether the point of the iteration being checked can be reached + private boolean reachable; + + /** + * @param changed + * the variables the loop may change, of which those whose class has states are tracked + */ + LoopTypestates(RefinementTypeChecker checker, CtLoop loop, Set changed) throws LJError { + this.checker = checker; + this.loop = loop; + for (String name : changed) { + if (!(checker.getContext().getVariableByName(name)instanceof Variable variable) + || variable.getType() == null) + continue; + List states = StateMachineBuilder.statesOf(checker.getContext(), + variable.getType().getQualifiedName(), true); + if (states.isEmpty()) + continue; + classStates.put(name, states); + head.put(name, currentStates(name)); + } + } + + /** The variables whose typestate is tracked, which must not be havocked */ + Set tracked() { + return classStates.keySet(); + } + + CtLoop loop() { + return loop; + } + + /** Starts checking an iteration: each tracked object is in one of the states at the loop head */ + void startIteration() { + head.forEach(this::setStates); + exit = emptyStates(); + continued = emptyStates(); + nextIteration = emptyStates(); + reachable = true; + } + + /** + * The loop may exit here, through its condition, if this point is reachable (the condition of a do-while is not + * when every path through the body returns) + */ + void recordExit() throws LJError { + if (reachable) + addCurrentStates(exit); + } + + void recordBreak() throws LJError { + addCurrentStates(exit); + } + + void recordContinue() throws LJError { + addCurrentStates(continued); + } + + /** + * Marks the end of the body, where the paths through its continues join the path through its last statement: from + * here on, each object is in a state it may be in at the end of the body or at any of the continues + * + * @param completes + * whether the end of the body can be reached without a continue + */ + void endBody(boolean completes) throws LJError { + if (continued.values().stream().allMatch(Set::isEmpty)) { + reachable = completes; + return; + } + if (completes) + recordContinue(); + continued.forEach(this::setStates); + reachable = true; + } + + /** The next iteration starts here, if this point is reachable */ + void recordNextIteration() throws LJError { + if (reachable) + addCurrentStates(nextIteration); + } + + /** + * Adds the states at the start of the next iteration to the states at the loop head + * + * @return whether they were already there, so the iteration just checked is the last one to check + */ + boolean reachedFixpoint() { + boolean grown = false; + for (String name : tracked()) + grown |= head.get(name).addAll(nextIteration.get(name)); + return !grown; + } + + /** + * After the loop, each tracked object is in a state it may be in where the loop exits. With no exit state (the + * solver proves the loop never exits, or its states were not followed), the object is havocked instead: an object + * in no state would make every check after the loop pass, which must not depend on that proof + */ + void finishLoop() { + exit.forEach((name, states) -> { + if (states.isEmpty()) + checker.forgetChanges(name, new Predicate(), loop); + else + setStates(name, states); + }); + } + + private Map> emptyStates() { + Map> states = new LinkedHashMap<>(); + tracked().forEach(name -> states.put(name, new LinkedHashSet<>())); + return states; + } + + private void addCurrentStates(Map> states) throws LJError { + for (String name : tracked()) + states.get(name).addAll(currentStates(name)); + } + + private Set currentStates(String name) throws LJError { + Optional instance = checker.getContext().getLastVariableInstance(name); + String current = instance.map(RefinedVariable::getName).orElse(name); + return new StateSolver(checker, loop.getPosition()).possibleStates(classStates.get(name), new Predicate(), + current); + } + + /** Gives the object a new instance, known only to be in one of {@code states} */ + private void setStates(String name, Set states) { + Predicate inAnyState = states.stream().map(State::predicate).reduce(Predicate::createDisjunction) + .orElseGet(() -> Predicate.createLit("false", Types.BOOLEAN)); + checker.forgetChanges(name, inAnyState, loop); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 3b6e3ac85..8d2388e19 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -1,12 +1,16 @@ package liquidjava.processor.refinement_checker; import java.lang.annotation.Annotation; +import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Arrays; +import java.util.Deque; import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; import java.util.Set; +import java.util.function.Consumer; +import java.util.stream.Collectors; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; @@ -43,6 +47,7 @@ import spoon.reflect.code.CtFor; import spoon.reflect.code.CtForEach; import spoon.reflect.code.CtIf; +import spoon.reflect.code.CtLabelledFlowBreak; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLambda; import spoon.reflect.code.CtLiteral; @@ -54,6 +59,8 @@ import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtSuperAccess; +import spoon.reflect.code.CtSwitch; +import spoon.reflect.code.CtSwitchExpression; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtThrow; import spoon.reflect.code.CtTry; @@ -82,6 +89,11 @@ public class RefinementTypeChecker extends TypeChecker { TryChecker tryChecker; Diagnostics diagnostics = Diagnostics.getInstance(); ContextHistory contextHistory = ContextHistory.getInstance(); + // the metadata that checking an element puts on it + private static final List CHECK_METADATA = List.of(Keys.REFINEMENT, Keys.TARGET, Keys.RECEIVER, + Keys.RETURN_VAR_NAME, Keys.STATE_CHANGE); + // the loops being checked, innermost first + private final Deque loops = new ArrayDeque<>(); public RefinementTypeChecker(Context context, Factory factory) { super(context, factory); @@ -628,12 +640,15 @@ private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpres * must be discarded at the join. * *

+ * A statement that a labelled {@code break} leaves completes normally, since execution goes on after it. + * + *

* Not currently handled (treated conservatively as completing normally): {@code switch} where every case exits, - * labeled {@code break}/{@code continue} targets, {@code try}/{@code catch}/{@code finally} flow, and infinite - * loops such as {@code while (true)}. Extending this list only tightens precision. + * {@code try}/{@code catch}/{@code finally} flow, and infinite loops such as {@code while (true)}. Extending this + * list only tightens precision. */ boolean canCompleteNormally(CtStatement statement) { - if (statement == null) + if (statement == null || isLeftByLabelledBreak(statement)) return true; if (statement instanceof CtReturn || statement instanceof CtThrow || statement instanceof CtBreak || statement instanceof CtContinue) @@ -652,6 +667,11 @@ boolean canCompleteNormally(CtStatement statement) { return true; } + private static boolean isLeftByLabelledBreak(CtStatement statement) { + return statement.getLabel() != null && statement.getElements(new TypeFilter<>(CtBreak.class)).stream() + .anyMatch(jump -> jump.getTargetLabel() != null && jump.getLabelledStatement() == statement); + } + @Override public void visitCtTry(CtTry tryBlock) { tryChecker.visitTry(tryBlock); @@ -664,27 +684,22 @@ public void visitCtTryWithResource(CtTryWithResource tryWithResource) { @Override public void visitCtWhile(CtWhile whileLoop) { - visitLoop(whileLoop, () -> { + visitLoop(whileLoop, states -> { scan(whileLoop.getLoopingExpression()); + recordExit(states, whileLoop.getLoopingExpression()); assumeLoopCondition(whileLoop.getLoopingExpression()); - scan(whileLoop.getBody()); + scanBody(whileLoop, states); }); } @Override public void visitCtFor(CtFor forLoop) { scan(forLoop.getForInit()); - visitLoop(forLoop, () -> { + visitLoop(forLoop, states -> { scan(forLoop.getExpression()); + recordExit(states, forLoop.getExpression()); assumeLoopCondition(forLoop.getExpression()); - List pathVariables = vcChecker.getPathVariables(); - CtStatement body = forLoop.getBody(); // null for an empty statement body, as in for (...); - scan(body); - if (body != null && !body.getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) { - // a continue reaches the update from any point of the body, skipping its facts and assignments - vcChecker.restorePathVariables(pathVariables); - havocChangedIn(forLoop); - } + scanBody(forLoop, states); // the update runs after the body, so the body sees the values the condition was checked on scan(forLoop.getForUpdate()); }); @@ -692,43 +707,212 @@ public void visitCtFor(CtFor forLoop) { @Override public void visitCtDo(CtDo doLoop) { - // the condition is not checked before the first iteration, so it is not assumed in the body - visitLoop(doLoop, () -> super.visitCtDo(doLoop)); + visitLoop(doLoop, states -> { + // the condition is not checked before the first iteration, so it is not assumed in the body + scanBody(doLoop, states); + scan(doLoop.getLoopingExpression()); + recordExit(states, doLoop.getLoopingExpression()); + }); } @Override public void visitCtForEach(CtForEach forEach) { - visitLoop(forEach, () -> super.visitCtForEach(forEach)); + // the iterable is evaluated once, before the first iteration + scan(forEach.getExpression()); + visitLoop(forEach, states -> { + states.recordExit(); + scan(forEach.getVariable()); + scanBody(forEach, states); + }); + } + + @Override + public void visitCtBreak(CtBreak breakStatement) { + super.visitCtBreak(breakStatement); + loopLeftBy(breakStatement).ifPresent(LoopTypestates::recordBreak); + } + + @Override + public void visitCtContinue(CtContinue continueStatement) { + super.visitCtContinue(continueStatement); + loopLeftBy(continueStatement).ifPresent(LoopTypestates::recordContinue); } /** - * Checks one arbitrary iteration of a loop: what the loop may change is havocked (keeps only its declared - * refinement, which every assignment re-checks) before it and again after it, since the loop may run any number of - * times. Path conditions added inside the loop (e.g. the loop condition, or an {@code if (...) break;}) are dropped - * after it. + * Checks a loop for any number of iterations. What the loop may change is havocked (keeps only its declared + * refinement, which every assignment re-checks) before it and again after it, except the typestates of the local + * objects it may change, which are computed over its iterations (see {@link LoopTypestates}). Path conditions added + * inside the loop (e.g. the loop condition, or an {@code if (...) break;}) are dropped after it. */ - private void visitLoop(CtLoop loop, Runnable iteration) { + private void visitLoop(CtLoop loop, Consumer iteration) { List pathVariables = vcChecker.getPathVariables(); - havocChangedIn(loop); - iteration.run(); + // a field may also change in a method the loop calls, out of sight here, so fields are only havocked; and + // typestates are only followed through jumps whose states are recorded, else they are havocked too + Set locals = followsJumps(loop) ? changedIn(loop).stream().filter(name -> !isField(name)) + .collect(Collectors.toCollection(LinkedHashSet::new)) : Set.of(); + LoopTypestates states = new LoopTypestates(this, loop, locals); + havocChangedIn(loop, states.tracked()); + loops.push(states); + try { + checkUntilFixpoint(states, iteration); + } finally { + loops.pop(); + } vcChecker.restorePathVariables(pathVariables); - havocChangedIn(loop); + havocChangedIn(loop, states.tracked()); + states.finishLoop(); } /** - * Havocs what the loop may change: the variables it writes, the objects it calls state-changing methods on, and the - * fields if it calls any method or constructor (which may write them) + * Checks iterations of a loop from the typestates at its head until they stop changing. Every check starts from the + * facts before the loop, with what it changes havocked; only the head typestates differ. What a check adds + * (variables, instances, path conditions, metadata) is dropped before the next one. + * + *

+ * An earlier check starts from fewer states than the last one, so an error that stops it is also an error of the + * last one. Only the last check keeps the errors recorded without stopping it (e.g. in a lambda). */ - private void havocChangedIn(CtLoop loop) { + private void checkUntilFixpoint(LoopTypestates states, Consumer iteration) { + List pathVariables = vcChecker.getPathVariables(); + while (true) { + Set errors = new LinkedHashSet<>(diagnostics.getErrors()); + removeCheckMetadata(states.loop()); + context.enterContext(); + try { + states.startIteration(); + iteration.accept(states); + states.recordNextIteration(); + } finally { + context.exitContext(); + vcChecker.replacePathVariables(pathVariables); + } + if (states.reachedFixpoint()) + return; + diagnostics.getErrors().retainAll(errors); + } + } + + /** + * Removes the metadata that checking a loop puts on its elements: unlike the context it is not scoped, so it could + * refer to what an earlier check dropped (e.g. the receiver of a call in a lambda). The parts checked once before + * the loop (a for's initialization, a for-each's iterable) and local class members, which carry their contracts, + * keep theirs. + */ + private static void removeCheckMetadata(CtLoop loop) { + List checkedBefore = new ArrayList<>(); + if (loop instanceof CtFor forLoop) + checkedBefore.addAll(forLoop.getForInit()); + if (loop instanceof CtForEach forEach) + checkedBefore.add(forEach.getExpression()); + for (CtElement element : loop.getElements((CtElement e) -> true)) { + if (element instanceof CtTypeMember + || (element instanceof CtParameter && element.getParent() instanceof CtTypeMember) + || checkedBefore.stream().anyMatch(before -> element == before || element.hasParent(before))) + continue; + for (String key : CHECK_METADATA) + element.putMetadata(key, null); + } + } + + /** + * Records the states where the loop exits through its condition, which are those where the condition is false: none + * if there is no condition or it is {@code true} + */ + private void recordExit(LoopTypestates states, CtExpression condition) { + if (condition == null) + return; + RefinedVariable conditionIsFalse = assumeCondition(condition, false); + states.recordExit(); + if (conditionIsFalse != null) + vcChecker.removePathVariable(conditionIsFalse); + } + + /** Checks the body of a loop, up to the point after it where its continues join */ + private void scanBody(CtLoop loop, LoopTypestates states) { + List pathVariables = vcChecker.getPathVariables(); + CtStatement body = loop.getBody(); // null for an empty statement body, as in for (...); + scan(body); + if (body != null && !body.getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) { + // a continue reaches the end of the body from any point of it, skipping its facts and assignments + vcChecker.restorePathVariables(pathVariables); + havocChangedIn(loop, states.tracked()); + } + states.endBody(canCompleteNormally(body)); + } + + /** The loop being checked that {@code jump} leaves, if any */ + private Optional loopLeftBy(CtLabelledFlowBreak jump) { + CtElement target = jumpTarget(jump); + return loops.stream().filter(states -> states.loop() == target).findFirst(); + } + + /** The statement a break or continue leaves: its label's, else the innermost loop, or switch for a break */ + private static CtElement jumpTarget(CtLabelledFlowBreak jump) { + if (jump.getTargetLabel() != null) + return jump.getLabelledStatement(); + return jump.getParent(e -> e instanceof CtLoop || (jump instanceof CtBreak && isSwitch(e))); + } + + private static boolean isSwitch(CtElement element) { + return element instanceof CtSwitch || element instanceof CtSwitchExpression; + } + + /** + * Whether the states at every jump in the loop are recorded where it goes: each jump goes to a loop or leaves a + * switch (not a labelled block, which joins no states), and runs no finally block or resource closing on its way, + * which could change states after they are recorded + */ + private static boolean followsJumps(CtLoop loop) { + return loop.getElements(new TypeFilter<>(CtLabelledFlowBreak.class)).stream().allMatch(jump -> { + CtElement target = jumpTarget(jump); + return (target instanceof CtLoop || isSwitch(target)) && !leavesTryWithCleanup(jump, target); + }); + } + + private static boolean leavesTryWithCleanup(CtLabelledFlowBreak jump, CtElement target) { + CtTry enclosing = jump.getParent(CtTry.class); + while (enclosing != null && enclosing.hasParent(target)) { + if (enclosing.getFinalizer() != null || enclosing instanceof CtTryWithResource) + return true; + enclosing = enclosing.getParent(CtTry.class); + } + return false; + } + + /** Havocs what the loop may change, except the {@code tracked} typestates */ + private void havocChangedIn(CtLoop loop, Set tracked) { + for (String name : changedIn(loop)) + if (!tracked.contains(name)) + forgetChanges(name, new Predicate(), loop); + } + + /** + * Gives a variable a new instance that keeps only its declared refinement and {@code known}, since the facts on its + * previous instances may no longer hold + */ + void forgetChanges(String name, Predicate known, CtElement element) { + if (!(context.getVariableByName(name)instanceof Variable variable)) + return; + vcChecker.removePathVariableThatIncludes(name); + String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); + Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); + context.addInstanceToContext(instanceName, variable.getType(), + Predicate.createConjunction(declared, known.substituteVariable(Keys.THIS, instanceName)), element); + context.addRefinementInstanceToVariable(name, instanceName); + } + + /** + * What the loop may change: the variables it writes, the objects it calls state-changing methods on, and the fields + * if it calls any method or constructor (which may write them) + */ + private Set changedIn(CtLoop loop) { List> changed = new ArrayList<>( loop.getElements(new TypeFilter>(CtVariableWrite.class))); List> calls = loop .getElements(new TypeFilter>(CtAbstractInvocation.class)); Set names = new LinkedHashSet<>(); for (CtAbstractInvocation call : calls) { - if (call instanceof CtInvocation inv - && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size()) - .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) { + if (call instanceof CtInvocation inv && mayChangeState(inv)) { if (inv.getTarget()instanceof CtVariableAccess target) changed.add(target); else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTarget())) @@ -743,17 +927,25 @@ else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTar names.add(access instanceof CtFieldAccess ? String.format(Formats.THIS, name) : name); } if (!calls.isEmpty()) - context.getCtxVars().stream().map(RefinedVariable::getName) - .filter(n -> n.startsWith(String.format(Formats.THIS, ""))).forEach(names::add); - for (String name : names) { - if (!(context.getVariableByName(name)instanceof Variable variable)) - continue; - vcChecker.removePathVariableThatIncludes(name); - String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); - Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); - context.addInstanceToContext(instanceName, variable.getType(), declared, loop); - context.addRefinementInstanceToVariable(name, instanceName); - } + context.getCtxVars().stream().map(RefinedVariable::getName).filter(RefinementTypeChecker::isField) + .forEach(names::add); + return names; + } + + /** Whether a name in the context is that of a field of this */ + private static boolean isField(String name) { + return name.startsWith(String.format(Formats.THIS, "")); + } + + /** + * Whether some method with the name and arity of the invoked one changes the state of its receiver. Methods + * specified externally are registered under their qualified name. + */ + private boolean mayChangeState(CtInvocation invocation) { + String name = invocation.getExecutable().getSimpleName(); + int arity = invocation.getArguments().size(); + return context.getCtxFunctions().stream().anyMatch(f -> Utils.getSimpleName(f.getName()).equals(name) + && f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); } /** 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 5b9519120..38fe52cd9 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 @@ -741,12 +741,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc Predicate expected = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom) .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction) .substituteVariable(Keys.THIS, instanceName); - Predicate previous = prevState; - for (String parameter : map.keySet()) { - previous = previous.substituteVariable(parameter, map.get(parameter)); - expected = expected.substituteVariable(parameter, map.get(parameter)); - } - expected = expected.changeOldMentions(vi.getName(), instanceName); + Predicate previous = substituteArguments(prevState, map); + expected = substituteArguments(expected, map).changeOldMentions(vi.getName(), instanceName); try { found = tc.checkStateSMT(previous, expected, invocation.getPosition()); } catch (SMTUnknownError error) { @@ -761,14 +757,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc if (!stateChange.hasFrom()) continue; - // replace "state(this)" to "state(whatever method is called from) and so on" - Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName); - Predicate prevCheck = prevState; - for (String s : map.keySet()) { // substituting function variables into annotation if there are any - prevCheck = prevCheck.substituteVariable(s, map.get(s)); - expectState = expectState.substituteVariable(s, map.get(s)); - } - expectState = expectState.changeOldMentions(vi.getName(), instanceName); + Predicate expectState = entryState(stateChange, instanceName, map); + Predicate prevCheck = substituteArguments(prevState, map); try { found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition()); @@ -778,29 +768,22 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } if (found && stateChange.hasTo()) { String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); - // Non-void: `_` is the return value; void: legacy alias for the new instance. - String returnViName = (String) invocation.getMetadata(Keys.RETURN_VAR_NAME); - String wildcardTarget = returnViName != null ? returnViName : newInstanceName; - Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget) - .substituteVariable(Keys.THIS, newInstanceName); - for (String s : map.keySet()) { - transitionedState = transitionedState.substituteVariable(s, map.get(s)); - } - transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName); + Predicate transitionedState = transitionedState(stateChange, instanceName, newInstanceName, map, + invocation); // update of state of new instance of this#n#(whatever it was + 1) addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation) .setStateChange(new StateChange(function, stateChange, vi, invocation.getPosition())); } } + if (!found && !preservesState) + found = changeToStateOfAnyEntryState(tc, vi, function, name, map, invocation, prevState); if (!found) { // Reaches the end of stateChange no matching states Predicate expectedStatesDisjunction = stateChanges.stream().filter(ObjectState::hasFrom) .map(ObjectState::getFrom) .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction); - expectedStatesDisjunction = expectedStatesDisjunction.substituteVariable(Keys.THIS, instanceName); - for (String s : map.keySet()) { - expectedStatesDisjunction = expectedStatesDisjunction.substituteVariable(s, map.get(s)); - } - expectedStatesDisjunction = expectedStatesDisjunction.changeOldMentions(vi.getName(), instanceName); + expectedStatesDisjunction = substituteArguments( + expectedStatesDisjunction.substituteVariable(Keys.THIS, instanceName), map) + .changeOldMentions(vi.getName(), instanceName); // combine messages of all state changes String message = stateChanges.stream().map(ObjectState::getMessage) @@ -890,6 +873,69 @@ private static String writtenReceiver(CtElement invocation) { return target == null || target.isImplicit() ? Keys.THIS : target.toString(); } + /** The state that {@code stateChange} gives the object after the call, as the instance {@code newInstanceName} */ + private static Predicate transitionedState(ObjectState stateChange, String instanceName, String newInstanceName, + Map map, CtElement invocation) { + // Non-void: `_` is the return value; void: legacy alias for the new instance. + String returnViName = (String) invocation.getMetadata(Keys.RETURN_VAR_NAME); + String wildcardTarget = returnViName != null ? returnViName : newInstanceName; + Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget) + .substituteVariable(Keys.THIS, newInstanceName); + return checkOldMentions(substituteArguments(transitionedState, map), instanceName, newInstanceName); + } + + /** + * A call whose entry states are each unprovable but whose union is provable, e.g. on an object that is in one of + * two states after a loop. The call is allowed, and the object ends up in the state given by any alternative whose + * entry state it may be in: an alternative without a target state leaves the object as it was. + * + * @return whether the call is allowed + */ + private static boolean changeToStateOfAnyEntryState(TypeChecker tc, VariableInstance vi, RefinedFunction function, + String name, Map map, CtElement invocation, Predicate prevState) throws LJError { + List alternatives = function.getAllStates().stream().filter(ObjectState::hasFrom).toList(); + if (alternatives.size() < 2) + return false; + String instanceName = vi.getName(); + Predicate previous = substituteArguments(prevState, map); + List entries = alternatives.stream().map(a -> entryState(a, instanceName, map)).toList(); + try { + if (!tc.checkStateSMT(previous, entries.stream().reduce(Predicate::createDisjunction).orElseThrow(), + invocation.getPosition())) + return false; + } catch (SMTUnknownError error) { + error.setDeclarationPosition(alternatives.get(0).getFromPosition()); + throw error; + } + + String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); + Predicate unchanged = previous.substituteVariable(instanceName, newInstanceName); + Predicate after = Predicate.createLit("false", Types.BOOLEAN); + for (int i = 0; i < alternatives.size(); i++) { + ObjectState alternative = alternatives.get(i); + Predicate entry = entries.get(i); + Predicate exit = alternative.hasTo() + ? transitionedState(alternative, instanceName, newInstanceName, map, invocation) + : Predicate.createConjunction(entry.substituteVariable(instanceName, newInstanceName), unchanged); + after = Predicate.createDisjunction(after, Predicate.createConjunction(entry, exit)); + } + addInstanceWithState(tc, name, newInstanceName, vi, after, invocation); + return true; + } + + /** The entry state of {@code stateChange}, for the object {@code instanceName} */ + private static Predicate entryState(ObjectState stateChange, String instanceName, Map map) { + Predicate entry = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName); + return substituteArguments(entry, map).changeOldMentions(instanceName, instanceName); + } + + /** Replaces the parameters of the called method with the arguments of the call, as given by {@code map} */ + private static Predicate substituteArguments(Predicate predicate, Map map) { + for (String parameter : map.keySet()) + predicate = predicate.substituteVariable(parameter, map.get(parameter)); + return predicate; + } + private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName) { return transitionedState.changeOldMentions(instanceName, newInstanceName); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 3713e0345..617c4c4a0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -65,7 +65,7 @@ public static boolean canModel(RefinedFunction function) { */ public static Optional build(TypeChecker tc, StateSolver solver, String className, CtElement element) throws LJError { - List states = statesOf(tc.getContext(), className); + List states = statesOf(tc.getContext(), className, false); if (states.isEmpty() || states.size() > MAX_STATES) return Optional.empty(); Context context = tc.getContext(); @@ -80,8 +80,14 @@ public static Optional build(TypeChecker tc, StateSolver solver, S } } - /** Every combination of one state from each state set of the class */ - private static List statesOf(Context context, String className) { + /** + * Every combination of one state from each state set of the class + * + * @param withNone + * whether an object may also be in none of the states of a set, named {@code none} (e.g. after + * {@code @StateRefinement(to = "!open(this) && !closed(this)")}) + */ + public static List statesOf(Context context, String className, boolean withNone) { List ghostStates = context.getGhostState(Utils.getSimpleName(className)); if (ghostStates == null) return List.of(); @@ -91,16 +97,29 @@ private static List statesOf(Context context, String className) { return List.of(); List combinations = List.of(new State(List.of(), new Predicate())); - for (List stateSet : stateSets.values()) - combinations = combinations.stream().flatMap(s -> stateSet.stream().map(g -> combine(s, g))).toList(); + for (List stateSet : stateSets.values()) { + List inSet = Stream.concat(stateSet.stream().map(StateMachineBuilder::inState), + withNone ? Stream.of(inNone(stateSet)) : Stream.empty()).toList(); + combinations = combinations.stream().flatMap(s -> inSet.stream().map(a -> combine(s, a))).toList(); + } return combinations; } - private static State combine(State state, GhostState ghostState) { + private static State inState(GhostState ghostState) { + return new State(List.of(ghostState.getName()), + Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS))); + } + + private static State inNone(List stateSet) { + Predicate none = stateSet.stream().map(g -> inState(g).predicate().negate()) + .reduce(Predicate::createConjunction).orElseThrow(); + return new State(List.of("none"), none); + } + + private static State combine(State state, State inSet) { List names = new ArrayList<>(state.names()); - names.add(ghostState.getName()); - Predicate holds = Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS)); - return new State(names, Predicate.createConjunction(state.predicate(), holds)); + names.addAll(inSet.names()); + return new State(names, Predicate.createConjunction(state.predicate(), inSet.predicate())); } private StateMachine build(String className, CtTypeReference type) throws LJError {