Comparison to the Fink et al. "typestates paper"

The abstraction they use consists mainly of two parts:

  1. a typestate (state of the automaton)
  2. an association of an abstract object with information about what points to it (unique,Must,MustNot,May)

In contrast, for tracematches we would have to associate a typestate with a disjunct, i.e. a mapping from variables to tuples of the form 2) above:

  1. a state of the TM automaton
  2. a mapping from variables to tuples <o,unique,Must,May,MustNot>

There seems to be a mistake in the description of the focus operation

Pathological case

About their different analyses

Flow-insensitive feasibility checking

This is exactly what our stage 2 does. Replace "each abstract object" in their formulation with "each set of objects with the right type" and you have exactly what we do.

Intraprocedural verifier

Here, there is a small but essential difference if we have more than one variable in the tracematch. If this is the case, this statement they make does not suffice any more: "Method calls are treated conservatively, without analyzing the method." In the case of multiple tracematch variables, if not all of the objects we currently care about (in the current disjunct) are known to be local, we have to assume that any method we call might modify such a non-local object. So we need locality on all variables. If we don't have this locality, we have to analyze the called methods, which can be done in two ways:

  1. cheap: see if the called methods transitively have any shadows of interest at all
  2. more expensive: if we find such a shadow, see if the points-to sets at this shadow overlap with the ones we currently investigate

Strong Updates: Uniqueness analysis

This solver is flow- and context-sensitive. It uses only the "unique" flag of the abovementioned abstraction. This flag is to be set if an allocation site in a program can be proven to be visited only once. (for instance, Singleton pattern)

An enhancement is to prove that if the allocation site is visited more than once, every time it is visited, the last object created at this point is not alive any more. (that's what Fink et al. do) This requires a possibly interprocedural liveness analysis.

We have an approximation of this: A only-visited-once analysis

See OnlyVisitedOnceAnalsysis for more information. We might still wanna use liveness information for enhanced precision.

Integrated verifier

This is the one which uses the full abstraction. In addition to the "unique" verifier, it is able to handle cases where the allocation site is not unique, for instance the "funny loop" example. Here, in paricular, the focus operation can be applied. When this is done, any tuple is split into two tuples, where one must point to the object in question and one must not. The former will lead to a strong update and the latter to a nop (!!!). Hence, no false positive is generated.

Further comments

Invariant methods

Formal Definition of Invariant Methods

Interestingly, there are, for example, some enumerations which clearly do not escape the method they are created in but apparently context information is not good enough to distinguish them from other enumerations. For those cases we found the following solution. Assume this example:

void foo() {
  Enumeration e = v.elements();
  while(e.hasMoreElements()) {
    Object o = e.nextElement();

Assume the pattern "hasNextElem", i.e. "always call hasNextElem() before nextElement()". Further assume that enumeration e is aliased with enumerations used in other methods due to imprecision. Then we can still decide that the method foo() is "invariant" with respect to the tracematch, because when leaving foo() we are in the initial state configuration, assuming we have local must-alias information and hence can do strong updates. Because we are in this initial configuration, it does not matter what happens after execution foo() so even if e is aliased with something else, we don't have to care. Note however, that it is crucial that we really get back to the initial configuration. For instance in the following case, we would not reach a final state but also not end up in the initial configuration...

void foo() {
  Enumeration e = v.elements();
  Object o = e.nextElement();

In this case, foo() is not invariant and hence we could not rule out the shadows in foo().

Determining invariant methods generally means a shift from the shadow-group centric view to a shadow centric view.

Agenda for the conference call Feb 27th