Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Unifying Type Checking and Property Checking for Low-Level Code

Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, and Shaz Qadeer

Abstract

We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific invariants that are difficult for traditional type checkers to express. Conversely, property checking for low-level code is challenging because it is difficult to write concise specifications that distinguish between locations in an untyped program’s heap. We address both problems simultaneously by implementing a type checker for low-level code as part of our property checker. We present a low-level formalization of a C program’s heap and its types that can be checked with an SMT solver, and we provide a decision procedure for checking type safety. Our type system is flexible enough to support a combination of nominal and structural subtyping for C, on a per-structure basis. We discuss several case studies that demonstrate the ability of this tool to express and check complex type invariants in low-level C code, including several small Windows device drivers.

Details

Publication typeInproceedings
Published inPrinciples of Programming Languages (POPL '09)
PublisherAssociation for Computing Machinery, Inc.

Previous versions

Jeremy Condit, Brian Hackett, Shuvendu Lahiri, and Shaz Qadeer. Unifying Type Checking and Property Checking for Low-Level Code, July 2008.

> Publications > Unifying Type Checking and Property Checking for Low-Level Code