A Precise Yet Efficient Memory Model For C

Verification for OO programs typically starts from a strongly typed object model in which distinct objects/fields are guaranteed not to overlap. This model simplifies verification by eliminating all "uninteresting" aliasing and allowing the use of more efficient frame axioms. Unfortunately, this model is unsound and incomplete for languages like C, where "objects" can overlap almost arbitrarily. Sound verification for C therefore typically starts from an untyped memory model, where memory is just an array of bytes. The untyped model, however, adds substantial annotation burden, and reasoning in the untyped model is computationally expensive. We propose a sound, typed semantics for C that provides the annotational and computational advantages of the typed object model while remaining sound and complete for C. We maintain a predicate identifying where the "valid" objects are, and introduce invariants and proof obligations that guarantee that the valid objects are suitably antialiased, and that (almost) all objects appearing in the program are valid. We describe the implementation of this approach in VCC (a sound verifier for C being used to verify the Microsoft Hypervisor) and the resulting performance gains.