Compile-Time Debugging of C Programs Working on Trees
We exhibit a technique for automatically verifying the safety of simple C programs working on tree-shaped data structures. We do not consider the complete behavior of programs, but only attempt to verify that they respect the shape and integrity of the store. A verified program is guaranteed to preserve the tree-shapes of data structures, to avoid pointer errors such as NULL dereferences, leaking memory, and dangling references, and furthermore to satisfy assertions specified in a specialized store logic.
A program is transformed into a single formula in WSRT, an extension of WS2S that is decided by the MONA tool. This technique is complete for loop-free code, but for loops and recursive functions we rely on Hoare-style invariants. A default well-formedness invariant is supplied and can be strengthened as needed by programmer annotations. If a program fails to verify, a counterexample in the form of an initial store that leads to an error is automatically generated.
This extends previous work that uses a similar technique to verify a simpler syntax manipulating only list structures. In that case, programs are translated into WS1S formulas. A naive generalization to recursive data-types determines an encoding in WS2S that leads to infeasible computations. To obtain a working tool, we have extended MONA to directly support recursive structures using an encoding that provides a necessary state-space factorization. This extension of MONA defines the new WSRT logic together with its decision procedure.
KeywordsDecision Procedure Null Cell Tree Automaton Initial Store Predicate Transformation
- Abdelwaheb Ayari, David Basin, and Andreas Podelski. LISA: A specification language based on WS2S. In Proceedings of CSL’97. BRICS, 1997.Google Scholar
- Morten Biehl, Nils Klarlund, and Theis Rauhe. Algorithms for guided tree automata. In First International Workshop on Implementing Automata, WIA’96, volume 1260 of LNCS. Springer Verlag, 1996.Google Scholar
- Rational Software Corporation. Purify. URL: http://www.rational.com/.
- Niels Damgaard, Nils Klarlund, and Michael I. Schwartzbach. YakYak: Parsing with logical side constraints. In Proceedings of DLT’99, 1999.Google Scholar
- David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. URL: http://www.research.digital.com/SRC/esc/Esc.html.
- David Evans. LCLint user’s guide. URL: http://www.sds.lcs.mit.edu/lclint/guide/.
- Rakesh Ghiya and Laurie J. Hendren. Putting pointer analysis to work. In Proceedings of POPL’98, 1998.Google Scholar
- GrammaTech Inc. CodeSurfer user guide and reference manual. URL: http://www.grammatech.com/papers/.
- D. Jackson. Aspect: an economical bug-detector. In Proceedings of 13th International Conference on Software Engineering, 1994.Google Scholar
- Jacob L. Jensen, Michael E. Jørgensen, Nils Klarlund, and Michael I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In PLDI’ 97, 1997.Google Scholar
- Nils Klarlund. Mona & Fido: The logic-automaton connection in practice. In Computer Science Logic, CSL’ 97, LNCS, 1998.Google Scholar
- Nils Klarlund and Anders Møller. MONA Version 1.3 User Manual. BRICS Notes Series NS-98-3 (2.revision), Department of Computer Science, University of Aarhus, October 1998. URL: http://www.brics.dk/mona/manual.html.
- Nils Klarlund and Michael I. Schwartzbach. Graph types. In Proc. 20th Symp. on Princ. of Prog. Lang., pages 196–205. ACM, 1993.Google Scholar
- Nils Klarlund and Michael I. Schwartzbach. Graphs and decidable transductions based on edge constraints. In Proc. CAAP’ 94, LNCS 787, 1994.Google Scholar
- Nils Klarlund and Michael I. Schwartzbach. A domain-specific language for regular sets of strings and trees. IEEE Transactions on Software Engineering, 25(3), 1997.Google Scholar
- Adam Kolawa and Arthur Hicken. Insure++: A tool to support total quality software. URL: http://www.parasoft.com/products/insure/papers/tech.htm.
- Anders Møller. MONA project homepage. URL: http://www.brics.dk/mona/.
- Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. MIT Press/Elsevier, 1990.Google Scholar
- Frank Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, September 1995.Google Scholar