Physical type checking for C

ABSTRACT

The effectiveness of traditional type checking in C is limited by the presence of type conversions using type casts. Because the C standard allows arbitrary type conversions between pointer types, neither C compilers, nor tools such as lint, can guarantee type safety in the presence of such type conversions. In particular, by using casts involving pointers to structures (C structs), a programmer can interpret any memory region to be of any desired type, further compromising C's weak type system. Not only do type casts make a program vulnerable to type errors, they hinder program comprehension and maintenance by creating latent dependencies between seemingly independent pieces of code.To address these problems, we have developed a stronger form of type checking for C programs, called physical type checking. Physical type checking takes into account the layout of C struct fields in memory. This paper describes an inference-based physical type checking algorithm. Our algorithm can be used to perform static safety checks, as well as compute useful information for software engineering applications.

REFERENCES

• 1: } L. 0. Andersen. Program Analysis and Specialization for the C Pmgmmming Language. PhD thesis, DIKU, University of Copenhagen, May 1994. (DIKU report 94/19).
• 2: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• 3: Satish Chandra and Thomas Reps. Physical type checking for C. Technical Report BL0113590-990302-04, Lucent Technologies, Bell Laboiatories, March 1999. Available at http://vuv.bell-labs.com/'schandra/pubs/checking-tr.ps.
• 4: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 5: Manuel Fähndrich , Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, Proceedings of the 4th International Symposium on Static Analysis, p.114-126, September 08-10, 1997
• 6: Jeffrey S. Foster , Manuel Fahndrich , Alexander Aiken, Flow-Insensitive Points-to Analysis with Term and Set Constraints, University of California at Berkeley, Berkeley, CA, 1997
• 7: F.-J. Grosch and G. Snelting. Polymorphic components for monomorphic languages. In R. Prieto-Diaz and W.B. Frakes, editors, Advances in Software Reuse: Selected Papers from the Second International Workshop on Software Reusability, pages 47-55, Lucca, Italy, March 1993. IEEE Computer Society Press.
• 8: J. Hughes. Backwards analysis of functional programs. Partial Evaluation and Mixed Computation: Proc. of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, (Gammel Avemaes, Denmark, Oct. 18-24, lg87), pages 187-208, 1988.
• 9: S. C. Johnson. Lint, a C program checker, July 1978.
• 10: Yanhong A. Liu, Dependence Analysis for Recursive Data, Proceedings of the 1998 International Conference on Computer Languages, p.206, May 14-16, 1998
• 11: Robert O'Callahan and Daniel Jackson. Detecting shared representations using type inference. Technical Report CMU-CS-95-202, Carnegie Mellon University, September 1995.
• 12: G. Ramalingam , John Field , Frank Tip, Aggregate structure identification and its application to program analysis, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-132, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292553]
• 13: Thomas W. Reps , Todd Turnidge, Program Specialization via Program Slicing, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.409-429, February 12-16, 1996
• 14: Marc Shapiro , Susan Horwitz, Fast and accurate flow-insensitive points-to analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 15-17, 1997, Paris, France [doi>10.1145/263699.263703]
• 15: M. Siff, S. Chandra, T. Ball, K. Kunchithapadam, and T. Reps. Coping with type casts in C. - Tech: nical Renort BL0113590-990202-03. Lucent Technologies, Beli Laboratories, February i999. Available at http://ww.bell-labs.com/-schandra/pubs/coping-tr.ps.
• 16: Michael Siff , Thomas Reps, Program generalization for software reuse: from C to C++, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.135-146, October 16-18, 1996, San Francisco, California, United States
• 17: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States
• 18: Suan Hsi Yong , Susan Horwitz , Thomas Reps, Pointer analysis for programs with structures and casting, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.91-103, May 01-04, 1999, Atlanta, Georgia, United States
• 19: Sean Zhang , Barbara G. Ryder , William Landi, Program decomposition for pointer aliasing: a step toward practical analyses, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.81-92, October 16-18, 1996, San Francisco, California, United States
• 20: Geoffrey Smith , Dennis M. Volpano, Towards an ML-Style Polymorphic Type System for C, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.341-355, April 22-24, 1996
• 21: Bjarne Steensgaard, Points-to Analysis by Type Inference of Programs with Structures and Unions, Proceedings of the 6th International Conference on Compiler Construction, p.136-150, April 24-26, 1996
• 22: Philip Wadler , R. J. M. Hughes, Projections for strictness analysis, Proc. of a conference on Functional programming languages and computer architecture, p.385-407, October 1987, Portland, Oregon, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: C

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Algorithms, Design, Languages, Measurement, Performance, Theory