Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions hold. Previous work on formalizing C-like languages has ignored this issue, either by assuming that programs do not make such assumptions or by assuming that all valid programs target only one platform. In the latter case, the platform's choices are hard-wired in the language semantics.

In this paper, we present a practically-motivated model for a C-like language in which the memory layouts of types are left largely unspecified. The dynamic semantics is parameterized by a platform's layout policy and makes manifest the consequence of platform-dependent (i.e., unspecified) steps. A type-and-effect system produces a layout constraint: a logic formula encoding layout conditions under which the program is memory-safe. We prove that if a program type-checks, it is memory-safe on all platforms satisfying its constraint.

Based on our theory, we have implemented a tool that discovers unportable layout assumptions in C programs. Our approach should generalize to other kinds of platform-dependent assumptions.

REFERENCES

• 1: Amal Ahmed , David Walker, The logical approach to stack typing, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 2: Aleph One Limited. The ARMLinux Book Online, Chapter 10. 2005. http://www.aleph1.co.uk/armlinux/book.
• 3: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 4: David F. Bacon. Kava: a Java dialect with a uniform object model for lightweight classes. Concurrency and Computation: Practice and Experience, 15 (3--5), 2003.
• 5: Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In 14th International Symposium on Formal Methods, 2006.
• 6: C Standard 1999. ISO/IEC 9899:1999, International Standard-Programming Languages-C. International Standards Organization, 1999.
• 7: Satish Chandra , Thomas Reps, Physical type checking for C, Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.66-75, September 06-06, 1999, Toulouse, France
• 8: Juan Chen , Dinghao Wu , Andrew W. Appel , Hai Fang, A provably sound TAL for back-end optimization, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 9: Jeremy Condit , Matthew Harren , Scott McPeak , George C. Necula , Westley Weimer, CCured in the real world, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 10: Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George Necula. Dependent types for low-level programming. In European Symposium on Programming, 2007.
• 11: Karl Crary, Toward a foundational typed assembly language, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.198-212, January 15-17, 2003, New Orleans, Louisiana, USA
• 12: Dinakar Dhurjati , Sumant Kowshik , Vikram Adve, SAFECode: enforcing alias analysis for weakly typed languages, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 13: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 14: Dan Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.3, p.429-475, May 2006 [doi>10.1145/1133651.1133653]
• 15: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 17: Nadeem A. Hamid , Zhong Shao , Valery Trifonov , Stefan Monnier , Zhaozhong Ni, A Syntactic Approach to Foundational Proof-Carrying Code, Journal of Automated Reasoning, v.31 n.3-4, p.191-229, 2003 [doi>10.1023/B:JARS.0000021012.97318.e9]
• 18: IBM. Developing embedded software for the IBM PowerPC 970FX processor. Application Note 970, IBM, 2004. http://www.ibm.com/chips/techlib/.
• 19: 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 of the annual conference on USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 20: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 21: Robert Love, Linux Kernel Development (2nd Edition) (Novell Press), Novell Press, 2005
• 22: Brad Martin, Anita Rettinger, and Jasmit Singh. Multiplatform porting to 64 bits. Dr. Dobb's Journal, 2005.
• 23: Antoine Miné, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 24: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 25: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 26: 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
• 27: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 28: 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]
• 29: Marius Nita, Dan Grossman, and Craig Chambers. A theory of platform-dependent low-level software (extended version). 2007. Available at http://www.cs.washington.edu/homes/marius/papers/tpd/.
• 30: Michael Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998.
• 31: Leaf Petersen , Robert Harper , Karl Crary , Frank Pfenning, A type theory for memory allocation and data layout, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.172-184, January 15-17, 2003, New Orleans, Louisiana, USA
• 32: Norman Ramsey, Simon~Peyton Jones, and Christian Lindig. The C-language specification version 2.0, 2005. http://www.cminusminus.org/extern/man2.pdf.
• 33: Michael Siff , Satish Chandra , Thomas Ball , Krishna Kunchithapadam , Thomas Reps, Coping with type casts in C, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.180-198, September 06-10, 1999, Toulouse, France
• 34: 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

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages, Theory, Verification

Keywords:
casts, low-level software, portability, type safety