Note: You are viewing an old revision of this page. View the current version.

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>

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 focuc 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