Using SAFE for typestate analysis of an object declared in a com.ibm.wala.classLoader.IMethod

[khatchad]

Is it possible to use SAFE to analyze the typestate of an object declared in a com.ibm.wala.classLoader.IMethod that emanating from the WALA framework? It seems that SAFE is very much geared towards running from a command line with specific typestate rules. However, in my case, I don't have a specific typestate to rule to check, instead, I would just like to know the /sequence/ of possible methods called on the object.

[yahave]

yes, it should be possible. You can define a dummy rule that is triggered on every step and record the steps that it goes through. Create a class that inherits from com.ibm.safe.typestate.rules. AbstractTypeStateDFA and make it receive all possible events. Then use matchDispatchEvent to track the events.

[khatchad]

Well, if I subclass com.ibm.safe.typestate.rules.AbstractTypeStateDFA, I hit a snag in com.ibm.safe.typestate.core.TypestateSolverFactory.getSolver(...) on line 136 (https://github.com/tech-srl/safe/blob/master/com.ibm.safe.typestate/src/com/ibm/safe/typestate/core/TypestateSolverFactory.java#L136): TypeStateProperty property = (dfa instanceof TypeStateProperty) ? (TypeStateProperty) dfa : null; Since my class isn't a TypeStateProperty, the property winds up being null, and I get a NullPointerException in com.ibm.safe.typestate.core.AbstractTypestateSolver.toString(). However, if I instead subclass com.ibm.safe.typestate.core.TypeStateProperty, it looks like I'll also need to provide a "dummy" com.ibm.safe.rules.TypestateRule, which I am working on now.

[yahave]

That should work. I think what I've done in the past is to create another solver factory, though. But your approach is also fine.

[khatchad]

OK, I've gotten to the point where I can track events via matchDispatchEvent(), however, I am now realizing that I need all possible states that an object can be in at a particular program point. As such, just tracking events is not necessarily enough; I'll need a state machine. I know that typestate analysis must somehow compute the possible states of an object internally in order to prove or disprove the property, but I am not exactly sure where that happens in SAFE just yet. My bunch is that it may depend on the analysis being used.

[yahave]

You will not be able to know the real possible states of an object based on analysis of client code. Your best bet is to "make up" states based on some limited history (we have often used just the most recent call to name the state). See for example http://www.cs.technion.ac.il/~yahave/papers/oopsla12.pdf

[khatchad]

Thank you for the reference. I am just considering intraprocedural analysis at the moment.