Patrick Lam

Associate Professor, Department of Electrical and Computer Engineering
Director, Software Engineering Programme
University of Waterloo
email: patrick.lam@uwaterloo.ca (no unsolicited commercial email)
phone: use email instead!

Picture of Patrick Lam

We have implemented four plugins in our module pluggable analysis framework.

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.

Valid HTML 5!