Modular information hiding and type-safe linking for C

ABSTRACT

This paper presents CMod, a novel tool that provides a sound module system for C. CMod works by enforcing a set of four rules that are based on principles of modular reasoning and on current programming practice. CMod's rules flesh out the convention that .h header files are module interfaces and .c source files are module implementations. Although this convention is well-known, developing CMod's rules revealed there are many subtleties in applying the basic pattern correctly. We have proven formally that CMod's rules enforce both information hiding and type-safe linking. We evaluated CMod on a number of benchmarks, and found that most programs obey CMod's rules, or can be made to with minimal effort, while rule violations reveal brittle coding practices including numerous information hiding violations and occasional type errors.

REFERENCES

• 1: Anindya Banerjee , David A. Naumann, Representation independence, confinement and access control [extended abstract], Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-177, January 16-18, 2002, Portland, Oregon
• 2: L. Cannon, R. Elliott, L. Kirchoff, J. Miller, R. Mitze, E. Schan, N. Whittington, H. Spencer, D. Keppel, and M. Brader. Recommended C Style and Coding Standards. sixth edition, 1990.
• 3: COM: Component object model technologies. http://www.microsoft.com/com/default.mspx.
• 4: Brad J. Cox , Andrew Novobilski, Object-Oriented Programming; An Evolutionary Approach, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1991
• 5: Exhuberant ctags. http://ctags.sourceforge.net/.
• 6: Michael D. Ernst , Greg J. Badros , David Notkin, An Empirical Analysis of C Preprocessor Use, IEEE Transactions on Software Engineering, v.28 n.12, p.1146-1170, December 2002 [doi>10.1109/TSE.2002.1158288]
• 7: J.-M. Favre. CPP Denotational Semantics. In SCAM, 2003.
• 8: Neal Glew , Greg Morrisett, Type-safe linking and modular assembly language, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292563]
• 9: David R. Hanson, C interfaces and implementations: techniques for creating reusable software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 10: Once-only headers - the C preprocessor. gcc on-line documentation, section 2.4, http://gcc.gnu.org/onlinedocs/gcc-4.1.1/cpp/Once_002dOnly-Headers.html.
• 11: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 12: S. Johnson. Lint, a C program checker. Technical Report 65, Bell Labs, Murray Hill, N.J., Sept. 1977.
• 13: Brian W. Kernighan , Rob Pike, The practice of programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 14: Brian W. Kernighan , Dennis M. Ritchie, The C programming language, Prentice Hall Press, Upper Saddle River, NJ, 1989
• 15: K. N. King, C programming: a modern approach, W. W. Norton & Co., Inc., New York, NY, 1996
• 16: Bill McCloskey , Eric Brewer, ASTEC: a new approach to refactoring C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 17: S. McConnell. Code Complete. Microsoft Press, 1993.
• 18: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 19: Robert Morris , Eddie Kohler , John Jannotti , M. Frans Kaashoek, The Click modular router, Proceedings of the seventeenth ACM symposium on Operating systems principles, p.217-231, December 12-15, 1999, Charleston, South Carolina, United States
• 20: G. Morrisett. Personal communication, July 2006.
• 21: George C. Necula , Jeremy Condit , Matthew Harren , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy software, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.3, p.477-526, May 2005 [doi>10.1145/1065887.1065892]
• 22: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 23: D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
• 24: PC-lint/FlexeLint. http://www.gimpel.com/lintinfo.htm, 1999. Product of Gimpel Software.
• 25: Benjamin C. Pierce, Advanced Topics in Types and Programming Languages, The MIT Press, 2004
• 26: A. Reid, M. Flatt, L. Stoller, J. Lepreau, and E. Eide. Knit: Component composition for systems software. In OSDI, 2000.
• 27: J. C. Reynolds. Types, abstractions and parametric polymorphism. Information Processing 83, pages 513--523.
• 28: D. Spuler and A. Sajeev. Static detection of preprocessor macro errors in C. Technical Report 92/7, James Cook University, Australia, '92.
• 29: S. Srivastava, M. Hicks, J. S. Foster, and B. Kanagal. Defining and Enforcing C's Module System. Technical Report CS-TR-4816, University of Maryland, College Park, 2006.
• 30: W. P. Stevens, G. J. Myers, and L. L. Constantine. Structured design. IBM Systems Journal, 13(2):115--139, 1974.
• 31: R. van Ommering, F. van der Linden, J. Kramer, and J. Magee. The Koala component model for consumer electronics software. IEEE Software, 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages

General Terms:
Design, Languages

Keywords:
C, information hiding, module systems, type-safety