We have implemented four plugins in our module pluggable analysis framework.
- A flag plugin, which assigns abstract set membership (and therefore typestate) according to integer or boolean flag values;
- A PALE plugin, which assigns abstract set membership based on shape properties of tree-like pointer-based data structures using the Pointer Analysis Logic Engine tool by Anders Møller and Michael I. Schwartzbach.
- A Bohne plugin, which implements field constraint analysis, a sophisticated shape analysis that is more powerful than PALE and less brittle.
- A theorem proving plugin, which assigns abstract set membership arbitrarily, for example, according to membership in array-based data structures. It generates verification conditions to be discharged using the Isabelle theorem proving environment.
A plugin's basic obligation is to show
1) that every procedure's ensures is implied at all of its
exit points, given the requires clause and the statements in
the procedure; and 2) the requires clause of all callees is
satisfied at the callsite. A plugin may discharge its obligations however
it chooses to.
Flag Plugin
The flag analysis plugin is designed to verify modules that use
integer or boolean flags to indicate the typestates of the objects
that they manipulate, and propagates boolean formulas through
requires and ensures clauses of callee
procedures. Flag abstraction sections specify the correspondence
between the concrete flag values and the abstract sets from the
specification, as well as the correspondence between the concrete and
the abstract boolean variables.
The flag plugin uses the boolean algebra libraries implemented in BA.ml
and the transfer function itself is implemented in typestate.ml.
The main loop is in the analyze_module procedure, and the
per-statement transfer functions are in analyze_stmt.
It's a big match statement, and takes advantage of the
fact that we have an Abstract Syntax Tree. This analysis propagates
boolean formulas directly (the same language we use in the
requires and ensures clauses), and it updates
the value of abstract sets whenever values are assigned to fields of
objects.
PALE Plugin
Unlike the flag analysis, which we designed to operate within our analysis framework, the PALE analysis is a previously implemented analysis package that we integrated into our framework. During the course of this adaptation, we did not modify the PALE analysis package itself — our plugin instead takes the form of a translator that enables PALE to work within our analysis framework.
The bulk of the PALE plugin's implementation is in pale.ml. For each procedure in the module to be analyzed, this
plugin creates a separate PALE output file, which is then fed to the
PALE analysis tool. The common headers for PALE input files are generated by
palestd.ml, while the code is emitted by
paleprinter.ml. After emitting PALE output, we spawn
the PALE binary on the emitted output. We did modify PALE to return an output
code of 42 upon success, so that we don't have to parse the output to
figure out whether PALE succeeded or not.
Theorem Proving Plugin
The theorem proving plugin generates verification conditions using weakest preconditions and discharges them using the Isabelle theorem prover. We have chosen this technique as a last resort for verifying arbitrarily complicated data structure implementations. The logic for specifying abstraction functions is based on typed set theory and proof obligations can be discharged using automated theorem proving or a proof checker for manually generated proofs, which means that there is no \emph{a priori} bound on the complexity of the data structures (and data structure consistency properties) that can be verified.
The verification condition generator is implemented in
vcgen.ml. It uses verification condition formula parsing
libraries (we have a ocamlyacc grammar for these formulas, and the
formula manipulation library is in vcform.ml). The engine is the
decide_sq procedure of vcgen.ml; given
a verification condition, it uses the vclemmas.ml library to verify
whether the condition is cached as being true. If not, it invokes Isabelle
to attempt to automatically discharge the verification condition.
When using this plugin to prove arbitrarily complicated properties, one
adds lemmas to the proof base until the property goes through.
