Clara

Clara currently ships with three typestate analysis already built-in:

• the syntactic Quick Check,
• the flow-insensitive Orphan-Shadows Analysis, and
• the flow-sensitive Nop-Shadows Analysis.

In the following we give an overview of these analyses. The Clara thesis gives more information.

Quick Check

The Quick Check works on Dependent Advice. Because Clara automatically generates Dependent-Advice declarations from Dependency State Machines, one can also apply the Quick Check to such state-machine declarations.

The Quick Check is purely syntactic and therefore very fast. (hence the name) By default, Clara applies the Quick Check right after having woven the runtime monitor into the program under test. For every dependency, Clara performs the following check:

• For every dependent advice a:
  • For every dependency d that references a (as weak or strong):
    • If every advice that d references as strong matches somewhere in the program,
      • mark a as “live”
  • If a was not marked as “live”,
    • disable a.

As this check is very fast, it makes sense to always apply the Quick Check when resolving advice dependencies.

In Clara, you can enable the Quick-check by including quick in the command-line parameter -static-analyses.

Orphan-Shadows Analysis

As the Quick Check, the Orphan-Shadows Analysis works on Dependent-Advice declarations.

The Orphan-Shadows Analysis performs a check not very different from the Quick Check, but on an object-by-object basis, or rather separated by groups of objects. The check uses Sridharan and Bodik’s Refinement-based Demand-driven Context-sensitive Points-to Analysis to compute groups of related Object Representatives. Then for every such group, Clara performs the following check:

• For every dependent advice a:
  • For every a-shadow s that refers to object representative o:
    • For every dependency d that references a (as weak or strong):
      • If every advice that d references as strong matches somewhere in the program at a shadow s’ that binds an object representative o’ which may-alias o,
        • mark s as “live”
  • If s was not marked as “live”,
    • disable s.

The required points-to analysis is expensive to compute (between 1-5 minutes on an average large program and a reasonably equipped personal computer) and therefore Clara applies, by default, the Orphan-Shadows Analysis only after having applied the Quick Check first.

In Clara, you can enable the Orphan-Shadows Analysis by including osa in the command-line parameter -static-analyses.

Nop-Shadows Analysis

By default, Clara applies the Nop-Shadows Analysis after the other two analysis stages have been applied already, and only if shadows remain active at this stage. The Nop-Shadows Analysis is flow-sensitive and therefore requires a Dependency State Machine as input. Dependent-advice declarations only encode flow-insensitive information and therefore do not suffice.

The Nop-Shadows analysis uses a combination of two deterministic finite-state machines (one accepting the language described by the Dependency State Machine and one accepting the mirror language of that language) to compute for every statement s the following three pieces of information:

• source(s): the set of possible typestates that can reach s,
• target(s): the set of possible typestates just after s, and
• futures(s): a partitioning of states where for every state q1 and q2 in a class c in future(s) it holds that one can reach the Dependency State Machine’s final state(s) from both q1 and q2 either way.

By definition of of future(s) if a statement s can only transition from a state q1 in source(s) to a state q2 in target(s) and in all futures(s), q1 and q2 are in the same class then s is a “Nop shadow” and can be disabled. The Nop-Shadows analysis uses flow-sensitive pointer information to generate Object Representatives. Using Object Representatives, the analysis separates matches on one group of objects from matches on other groups.

To maintain efficiency at compile time, the Nop-Shadows Analysis is designed as a “mostly intra-procedural” analysis that uses very precise, flow-sensitive analysis information with strong updates within individual methods, but uses coarse-grain inter-procedural summary information at method boundaries. We model method calls and continuation through an external-successor function. The figure on the right shows this function as solid arrows.

You can see some examples of what the Nop-Shadows Analysis can and cannot achieve by looking at our test cases. (see here for dependency state machines, and here for tracematches)

In Clara, you can enable the Nop-Shadows Analysis by including nsa in the command-line parameter -static-analyses. This analysis stage requires osa to be enabled, too.

Dynamic code generation for Collaborative Runtime Verification

Clara contains a code generator that can automatically partition instrumentation to enable Collaborative Runtime Verification. The idea of Collaborative Runtime Verification is to distribute to multiple users differently instrumented program versions, where every version only carries partial instrumentation. Clara automatically partitions instrumentation into a set of sensible "probes". Every probe is a set of shadows that can refer to a consistent group of objects (as defined through the monitor specification) and that in combination can trigger a property violation.

In Clara, you can enable the Dynamic code genration by including dyna in the command-line parameter -static-analyses. This analysis stage requires osa to be enabled, too.