Bit level types for high level reasoning

Bitwise operations are commonly used in low-level systems code to access multiple data fields that have been packed into a single word. Program analysis tools that reason about such programs must model the semantics of bitwise operations precisely in order to capture program control and data flow through these operations. We present a type system for subword data structures that explitictly tracks the flow of bit values in the program and identifies consecutive sections of vits as logical entities manipulated atomically by the programmer. Our type inference algorithm tags each integer value of the program with a bitvector type that identifies the data layout at the subword level. These types are used in a translation phase to remove bitwise operations from the program. We have applied our bitvector type inference algorithm to generate program documentation for a virtual memory subsystem of an OS kernel, and to verify Linux drivers and a memory protection system. For the verifica...

• Type: Conference
• Year: 2006
• Where: SIGSOFT
• Authors: Ranjit Jhala, Rupak Majumdar
• Keywords: Bitvector Types, Bitwise Operations, SIGSOFT 2006, Software Engineering, Type Inference Algorithm