Repository navigation
Soundness: after a loop, an object with an external spec keeps the state set inside the loop body #427
Description
Impact: a real bug passes verification (false negative). It is the shape of a real bug in marcomicera/tabu-timetabling (fixed in 5ea97d1, "Stream not marked" IOException).
Description
#338 (fixed by #384) makes the state after a loop the join of the state before the loop and after the body. On main (0d489e1) this works for a class specified in the same file, but not for an object whose class has an external spec (@ExternalRefinementsFor): a state set only inside the loop is still assumed after it, and a call that is refused from the second iteration on is accepted.
Minimal reproducer (two files)
import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;
@ExternalRefinementsFor("java.io.BufferedReader")
@StateSet({"open", "marked", "closed"})
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();
}import java.io.BufferedReader;
import java.io.IOException;
import java.io.Reader;
public class Repro {
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(); // with n == 0 the loop never runs and br was never marked
}
static void laterIteration(Reader in, int n) throws IOException {
BufferedReader br = new BufferedReader(in);
for (int i = 0; i < n; i++) {
br.readLine(); // from the second iteration on, br is closed
br.close();
}
}
}Expected: a State Refinement Error at br.reset() (br may be open) and at br.readLine() in laterIteration (br may be closed).
Actual:
Correct! Passed Verification.
Control: the same loop with a class specified in the file is reported (the reproducer of #338)
@StateSet({"open", "marked"})
class Buf {
@StateRefinement(to = "open(this)")
public Buf() {}
@StateRefinement(to = "marked(this)")
public void mark() {}
@StateRefinement(from = "marked(this)", to = "open(this)")
public void reset() {}
}
public class Repro {
static void rewind(int n) {
Buf b = new Buf();
int k = 0;
while (k < n) {
b.mark();
k++;
}
b.reset();
}
}State Refinement Error: found true but expected marked(b²⁰)
The real bug (abridged): the inner loop may stop at once, when the next line already belongs to another student, and then reset() runs without a mark().
br = new BufferedReader(fr);
while ((currentLine = br.readLine()) != null) {
...
while ((nextLine = br.readLine()) != null && currentLine.split(" ")[0].equals(nextLine.split(" ")[0])) {
...
br.mark(10000);
}
br.reset(); // IOException: Stream not marked
Activity
Compute the typestate at a loop head as a fixpoint over its iterations