Advertisement

Compile-Time Debugging of C Programs Working on Trees

  • Jacob Elgaard
  • Anders Møller
  • Michael I. Schwartzbach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)

Abstract

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.

Keywords

Decision Procedure Null Cell Tree Automaton Initial Store Predicate Transformation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [1]
    Abdelwaheb Ayari, David Basin, and Andreas Podelski. LISA: A specification language based on WS2S. In Proceedings of CSL’97. BRICS, 1997.Google Scholar
  2. [2]
    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
  3. [3]
    Rational Software Corporation. Purify. URL: http://www.rational.com/.
  4. [4]
    Niels Damgaard, Nils Klarlund, and Michael I. Schwartzbach. YakYak: Parsing with logical side constraints. In Proceedings of DLT’99, 1999.Google Scholar
  5. [5]
    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.
  6. [6]
    David Evans. LCLint user’s guide. URL: http://www.sds.lcs.mit.edu/lclint/guide/.
  7. [7]
    Rakesh Ghiya and Laurie J. Hendren. Putting pointer analysis to work. In Proceedings of POPL’98, 1998.Google Scholar
  8. [8]
    GrammaTech Inc. CodeSurfer user guide and reference manual. URL: http://www.grammatech.com/papers/.
  9. [9]
    C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, October 1969.zbMATHCrossRefGoogle Scholar
  10. [10]
    D. Jackson. Aspect: an economical bug-detector. In Proceedings of 13th International Conference on Software Engineering, 1994.Google Scholar
  11. [11]
    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
  12. [12]
    Nils Klarlund. Mona & Fido: The logic-automaton connection in practice. In Computer Science Logic, CSL’ 97, LNCS, 1998.Google Scholar
  13. [13]
    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.
  14. [14]
    Nils Klarlund and Michael I. Schwartzbach. Graph types. In Proc. 20th Symp. on Princ. of Prog. Lang., pages 196–205. ACM, 1993.Google Scholar
  15. [15]
    Nils Klarlund and Michael I. Schwartzbach. Graphs and decidable transductions based on edge constraints. In Proc. CAAP’ 94, LNCS 787, 1994.Google Scholar
  16. [16]
    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
  17. [17]
    Adam Kolawa and Arthur Hicken. Insure++: A tool to support total quality software. URL: http://www.parasoft.com/products/insure/papers/tech.htm.
  18. [18]
    Anders Møller. MONA project homepage. URL: http://www.brics.dk/mona/.
  19. [19]
    Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. Transactions on Programming Languages and Systems, 20(1):1–50, January 1998.CrossRefGoogle Scholar
  20. [20]
    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
  21. [21]
    Frank Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, September 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Jacob Elgaard
    • 1
  • Anders Møller
    • 1
  • Michael I. Schwartzbach
    • 1
  1. 1.BRICSUniversity of AarhusAarhus

Personalised recommendations