This is not a flaw...

This rather was a misunderstanding. There are two different things going on. One is the treatment of "v = new T()" where you generate two touples, one of which gets the typestate "init" and one which keeps the original state. Then, for focus, you generate two tuples which both get assigned the original typestate. In the example, this happened to be "init", too, which is confusing.


According to their section 5.2, a focus operator can not only be applied on statements of the form "v = new T()" but also "v = iterator.next()". I (Eric) believe this is wrong. Assume the following example where list is a list holding two references to the same object (and nothing else). The pattern is foo(x) foo(x).

Iterator it = list.iterator();
while(it.hasNext()) {
  Object k = it.next();
  //(1)
  foo(k);
  //(2)
}

Further assume that foo(..) is not called anywhere else in the program. Since list holds the same object twice, the pattern should match. However, Fink et al.'s analysis seems to report a false negative for the following reason.

  1. At (1) you start off with an initial configuration of <o,false,init,{k},false,{}>.
  2. Then at (2) you move to <o,false,1,{k},false,{}>, assuming that 1 is the state after reading one foo.
  3. Going around the loop, we then hit k = it.next() again. This should, according to Section 5.2, lead to two new tuples of the form <o,false,1,{},false,{k}> and <o,false,init,{k},false,{}> where the former denotes the object which k not longer refers to and the latter the object which k now does refer to. I think here is the mistake: It is wrong to state that k cannot not refer to the object in the former tuple. In fact in this particular example, k will refer to this (same) object!
  4. If we go ahead with those tuples, at (2) we propagate <o,false,1,{},false,{k}> to <o,false,1,{},false,{k}> (because we falsely assume that k cannot possibly point to this object) and <o,false,init,{k},false,{}> to <o,false,1,{k},false,{}> which we already had before.

In the next iteration we reach the fixed point. No disjunct ever reaches a final state.

What would this look like if we didn't put k into the must-not set?

Then instead of generating <o,false,1,{},false,{k}> and <o,false,init,{k},false,{}>, we would generate <o,false,1,{},false,{}> and <o,false,init,{k},false,{}>, where the latter states "k must point to o" and the former "k may point to o".

At (2), then <o,false,1,{},false,{}> would move to <o,false,2,{},false,{}>, which gives a correct hit, and <o,false,init,{k},false,{}> would move to <o,false,1,{k},false,{}>, which we had before.

Consequence

It is sound to apply focus on statements of the form v = new T() because here one knows that v points to a new object and so v cannot point any more to the object is used to point to earlier in the code. However, focus may not be applied at any other statements. In particular, new-statements are the only ones which generate variables in the must-not set.