Interesting issue with typestate and pointer analysis combination

[khatchad]

I am running into a rather interesting issue regarding the typestate analysis in combination with using pointer analysis. Assume the following simplified example:

class C {
    C m() {return new C();}  // 2.
    C n() {return this;}
    void p() {}
}

// client code:
C c = new C(); // 1.
if (...) {
    c = c.m();
    c = c.n();
} else
    c = c.n();
c.p();

Suppose I'd like to know the possible states of the objects c points to at the line c.p(). Also assume that my DFA has states, namely, "start" and "n." The "start" state is the initial state and calls to n() transitions us to state "n." The numbered comments are abstract objects created at the corresponding lines.

The points-to set of c at the call c.p() should be {1,2}. If we run the typestate analysis and use the resulting domain to give us the facts regarding these two objects at the basic block corresponding to call c.p(), we'd have that object 1 may either have the state "n" (in the case that the else branch is taken) or the state "start" (in the case that the if branch is taken). The former scenario is troubling because in the case that the if branch is taken, c would never point to object 1 because it is overwritten with object 2. As such, object 1 could only really be in the "n" state at this point.

My question is threefold:

1. Is this an inherent limitation of typestate analysis when combined with points-to analysis? Or, am I not using the points-to analysis correctly?
2. Is this some sort of sensitivity or precision problem that can be fixed?
3. Or, is this a limitation of SAFE, for which it can be improved upon?

[yahave]

What typestate domain are you using? Does APMust (domain using access paths) solve your problem?

[khatchad]

What typestate domain are you using? Does APMust (domain using access paths) solve your problem?

Looks like I'm using Unique. I'll have a look at APMust, but would there be any tradeoffs in using APMust over Unique? Thanks!

[khatchad]

What typestate domain are you using? Does APMust (domain using access paths) solve your problem?

OK, interestingly, I tried switching from Unique to APMust as well as APMustMustNot, all with the same result as Unique.