Abstracting Pointers for a Verifying Compiler

摘要

Gregory Kulczycki Virginia Tech Falls Church, VA, USA gregwk@vt.edu Heather Keown, Murali Sitaraman Clemson University Clemson, SC, USA {hkeown, murali}@cs.clemson.edu Bruce W. Weide The Ohio State University Columbus, OH, USA weide.1@osu.edu Abstract The ultimate objective of a verifying compiler is to prove that proposed code implements a full behavioral specification. Experience reveals this to be especially difficult for programs that involve pointers or refer- ences and linked data structures. In some situations, pointers are unavoidable; in some others, verification can be simplified through suitable abstractions. Re- gardless, a verifying compiler should be able to handle both cases, preferably using the same set of rules. To illustrate how this can be done, we examine two ap- proaches to full verification. One replaces language- supplied indirection with software components whose specifications abstract pointers and pointer- manipulation operations. Another approach uses ab- stract specifications to encapsulate data structures that pointers and references are often used to implement, limiting verification complications to inside the imple- mentations of these components. Using a modular, specification-based tool we have developed for verifi- cation condition generation, we show that full verifica- tion of programs with and without the direct use of pointers can be handled similarly. There is neither a need to focus on selected pointer properties, such as the absence of null references or cycles, nor a need for special rules to handle pointers.