Introduction

Hob is a static analysis framework that verifies that program implementations satisfy their specifications. Using Hob, developers can apply multiple pluggable analyses to different parts of a program, applying each analysis to the modules for which it is most appropriate. Each Hob analysis plugin verifies that program modules 1) properly implement their specifications; and 2) respect the preconditions of the procedures that they call. Program modules often encapsulate data structures, and many data structures maintain a dynamically changing set of objects as their primary purpose; we have therefore found that set specifications allow developers to express crucial data structure interface properties, including in particular, the preconditions needed by typical data structure operations to successfully execute. Hob's common set specification language therefore enables different analyses to effectively communicate with each other.

The Hob project addresses the program verification problem [1, 6]. Our tool supports assume/guarantee reasoning and data refinement. The techniques embodied in the Hob tool are particularly suited for expressing and verifying data structure consistency properties: Hob allows static analysis plugins to verify that data structure preconditions hold upon entry to a data structure, that data structure operations preserve data structure invariants, and that data structure operations conform to their specifications.

Our technique is designed to support programs that encapsulate the implementations of complex data structures in instantiatable leaf modules, with these modules analyzed once by very precise, potentially expensive analyses (such as shape analyses or even analyses that generate verification conditions that must be manually discharged using a theorem prover or proof checker). The rest of the program uses these modules but does not directly manipulate the encapsulated data structures. These modules can then be analyzed by more efficient analyses that operate primarily at the level of the common set abstraction. Given the scalability issues associated with precise data structure verification techniques, this kind of approach is the only way to make these analyses viable in practice.

We have implemented our analysis framework [4] and populated this framework with three analysis plugins: 1) the flags plugin, which is designed to analyze modules that use a flag field to indicate the typestate of the objects that they manipulate [3]; 2) the PALE plugin, which implements a shape analysis for linked data structures (we integrated the Pointer Analysis Logic Engine analysis tool [5] into our system); and 3) the theorem proving plugin, which generates verification conditions designed to be discharged manually using the Isabelle interactive theorem prover [7]. We have used our analysis framework to analyze several programs; our experience shows that it can effectively 1) verify the consistency of data structures encapsulated within a single module and 2) combine analysis results from different analysis plugins to verify properties involving objects shared by multiple modules analyzed by different analyses. We have observed that our approach reduces the program annotation effort, improves the performance of the resulting analysis, and extends the range of programs to which each component analysis is applicable in isolation.

Approach

We next describe the Hob approach. A program to be analyzed contains a number of modules. Each module is analyzed by an analysis plugin; plugins ensure that the module's implementation conforms to its specification and that the module satisfies all preconditions for the calls that it makes.

How Analysis Plugins Work

The basic task of an analysis plugin is to certify that the implementation for a module conforms to its specification and that the module meets all preconditions for calls that it makes. Implementation sections for modules in our system are written in a standard Java-like memory-safe imperative language supporting arrays and dynamic object allocation. Module specification sections give preconditions and postconditions for procedures in the boolean algebra of sets; these conditions are augmented with a modifies clause, which states the frame condition for the procedure. Specification modules may also name global boolean predicates to be tracked by the analysis. Finally, since modules may implement their specifications in a variety of ways, the abstraction section of a module describes the relationship between the module's implementation and its specification; each analysis plugin has a specialized syntax for abstraction settings, suitable for the type of properties checked by that plugin. An abstraction section may additionally state representation invariants applicable to the data structure implemented in that module.

In general, the Hob system analyzes individual modules as follows. For each module, Hob examines the implementation, specification, and abstraction sections of that module, as well as the specifications of all procedures that the module invokes. Hob first uses the abstraction function (from the abstraction section) to translate the requires and ensures clauses into the internal representation of the specialized analysis that will analyze the module (as specified in the abstraction section). Hob then conjoins the representation invariant to the translated requires and ensures clauses. Finally, Hob invokes the specified analysis plugin to verify that each procedure conforms to its translated requires and ensures clauses.

Progress

We have coded up several benchmark programs, using our system during the development of the programs. Our benchmarks include the water scientific computation benchmark, a minesweeper game, and programs with computational patterns from operating-system schedulers, air-traffic control, and program transformation passes. These benchmarks use a variety of data structures, and we have therefore implemented and verified sets, set iterators, queues, stacks, and priority queues. Our implementations range from singly-linked and doubly-linked lists and tree insertion (all verified using the PALE plugin) through array data structures (verified using the theorem proving plugin with the Isabelle theorem prover used to discharge verification conditions); our largest benchmark (water) contains approximately 2000 lines of implementation and 500 lines of specification.

The Hob project homepage is at http://hob.csail.mit.edu. Note that the Hob homepage is served by an HTTP server implemented in, and verified by, the Hob system. This homepage links to the O'Caml source tarball and publicly readable Subversion repository, further explains our example applications, and includes past presentations about Hob. Hob is distributed under the GNU General Public License.

Future

The future development of Hob will be primarily guided by the verification of additional benchmark programs. We have already started annotating these programs. We expect new benchmark programs to give us more experience using the Hob system and to help us select a productive future research direction.

Research Support

This research was supported in part by DARPA Contract F33615-00-C-1692, NSF Grant CCROO-86154, NSF Grant CCROO-63513, and the Singapore-MIT Alliance.

References:

[1] C. A. R. Hoare. The verifying compiler: still a Grand Challenge for computing research. ETAPS Invited Lecture, Warsaw, Poland, April 2003.

[2] Patrick Lam, Viktor Kuncak and Martin Rinard. Crosscutting techniques in program specification and analysis. In Proceedings of the Fourth Conference on Aspect-Oriented Software Development, pp. 169--180, Chicago, IL, USA, March 2005.

[3] Patrick Lam, Viktor Kuncak and Martin Rinard. Generalized typestate checking for data structure consistency. In Proceedings of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation, pp. 430--447, Paris, France, January 2005.

[4] Patrick Lam, Viktor Kuncak and Martin Rinard. Hob: A Tool for Verifying Data Structure Consistency (tool demo). In Proceedings of the Fourteenth International Conference on Compiler Construction, pp. 237--241, Edinburgh, Scotland, April 2005.

[5] Anders Møller and Michael I. Schwartzbach. The Pointer Assertion Logic Engine. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 221--231, Snowbird, UT, USA, June 2001.

[6] Charles Gregory Nelson. Techniques for Program Verification. Technical report, XEROX Palo Alto Research Center, 1981.

[7] Karen Zee, Patrick Lam, Viktor Kuncak and Martin Rinard. Combining theorem proving with static analysis for data structure consistency. In Proceedings of the International Workshop on Software Verification and Validation (SVV 2004), Seattle, WA, USA, November 2004.