research-article

Formal verification of object layout for c++ multiple inheritance

Authors:

Tahina Ramananandro,

Gabriel Dos Reis,

Xavier LeroyAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 1

Pages 67 - 80

https://doi.org/10.1145/1925844.1926395

Published: 26 January 2011 Publication History

Get Access

Abstract

Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ object layout schemes and mechanically proves their correctness against the operational semantics for multiple inheritance of Wasserrab et al. This formalization is flexible enough to account for space-saving techniques such as empty base class optimization and tail-padding optimization. As an application, we obtain the first formal correctness proofs for realistic, optimized object layout algorithms, including one based on the popular "common vendor" Itanium C++ application binary interface. This work provides semantic foundations to discover and justify new layout optimizations; it is also a first step towards the verification of a C++ compiler front-end.

Supplementary Material

MP4 File (8-mpeg-4.mp4)

Download
457.48 MB

References

[1]

S. Blazy and X. Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263--288, 2009.

Crossref

Google Scholar

[2]

J. Chen. A typed intermediate language for compiling multiple inheritance. In 34th symp. Principles of Programming Languages, pages 25--30. ACM, 2007.

Digital Library

Google Scholar

[3]

CodeSourcery, Compaq, EDG, HP, IBM, Intel, Red Hat, and SGI. Itanium C++ ABI, 2001. URL http://www.codesourcery.com/public/cxx-abi.

Google Scholar

[4]

B. Dawes. PODs Revisited; Resolving Core Issue 568 (Revision 2). Technical report, ISO/IEC SC22/JTC1/WG21, March 2007. URL http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2007/n2172.html.

Google Scholar

[5]

M. A. Ellis and B. Stroustrup. The Annotated C++ Reference Manual. Addison-Wesley, 1990.

Digital Library

Google Scholar

[6]

J. Gil and P. F. Sweeney. Space and time-efficient memory layout for multiple inheritance. In 14th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1999), pages 256--275. ACM, 1999.

Digital Library

Google Scholar

[7]

J. Y. Gil, W. Pugh, G. E. Weddell, and Y. Zibin. Two-dimensional bidirectional object layout. ACM Trans. Program. Lang. Syst., 30(5): 1--38, 2008.

Digital Library

Google Scholar

[8]

International Standard ISO/IEC 14882:2003. Programming Languages C++. International Organization for Standards, 2003.

Google Scholar

[9]

G. Klein and T. Nipkow. A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Prog. Lang. Syst., 28(4):619--695, 2006.

Digital Library

Google Scholar

[10]

D. Leinenbach, W. Paul, and E. Petrova. Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In Int. Conf. on Software Engineering and Formal Methods (SEFM 2005), pages 2--11. IEEE, 2005.

Digital Library

Google Scholar

[11]

X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107--115, 2009.

Digital Library

Google Scholar

[12]

C. Luo and S. Qin. Separation Logic for Multiple Inheritance. Electron. Notes Theor. Comput. Sci., 212:27--40, 2008.

Digital Library

Google Scholar

[13]

N. Myers. The empty member C++ optimization. Dr Dobbs Journal, Aug. 1997. URL http://www.cantrip.org/emptyopt.html.

Google Scholar

[14]

G. Ramalingam and H. Srinivasan. A member lookup algorithm for C++. In Programming Language Design and Implementation (PLDI97), pages 18--30. ACM, 1997.

Digital Library

Google Scholar

[15]

T. Ramananandro. Formal verification of object layout for C++ multiple inheritance Coq development and supplementary material, 2010. URL http://gallium.inria.fr/~tramanan/cxx/.

Digital Library

Google Scholar

[16]

J. G. Rossie and D. P. Friedman. An algebraic semantics of subobjects. In 10th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1995), pages 187--199. ACM, 1995.

Digital Library

Google Scholar

[17]

P. F. Sweeney and M. G. Burke. Quantifying and evaluating the space overhead for alternative C++ memory layouts. Software: Practice and Experience, 33(7):595--636, 2003.

Digital Library

Google Scholar

[18]

H. Tuch. Formal verification of C systems code: Structured types, separation logic and theorem proving. Journal of Automated Reasoning, 42(2):125--187, 2009.

Digital Library

Google Scholar

[19]

D. Wasserrab, T. Nipkow, G. Snelting, and F. Tip. An operational semantics and type safety proof for multiple inheritance in C++. In 21st conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2006), pages 345--362. ACM, 2006.

Digital Library

Google Scholar

Cited By

View all

Malecha GStewart GFarka FHaag JHirai Y(2022)Developing With Formal Methods at BedRock Systems, Inc.IEEE Security & Privacy10.1109/MSEC.2022.315819620:3(33-42)Online publication date: May-2022
https://doi.org/10.1109/MSEC.2022.3158196
Monteiro FGadelha MCordeiro L(2021)Model checking C++ programsSoftware Testing, Verification and Reliability10.1002/stvr.179332:1Online publication date: 8-Sep-2021
https://doi.org/10.1002/stvr.1793
Hirai Y(2017)Defining the Ethereum Virtual Machine for Interactive Theorem ProversFinancial Cryptography and Data Security10.1007/978-3-319-70278-0_33(520-535)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-70278-0_33
Show More Cited By

Index Terms

Formal verification of object layout for c++ multiple inheritance

Recommendations

An operational semantics and type safety prooffor multiple inheritance in C++
OOPSLA '06: Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

We present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behaviour of method calls, field accesses, and two forms of casts in C++ class hierarchies exactly, and the type safety proof was ...
Formal verification of object layout for c++ multiple inheritance
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ ...
An operational semantics and type safety prooffor multiple inheritance in C++
Proceedings of the 2006 OOPSLA Conference

We present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behaviour of method calls, field accesses, and two forms of casts in C++ class hierarchies exactly, and the type safety proof was ...

Reviews

Reviewer: Scott Arthur Moody

Efficient language translation, optimized code generation, and runtime memory layout are cornerstones of modern computer language compilers. Squeezing a user's data structures, especially with C++ multiple inheritance, into fewer but efficiently accessed bits leads to smaller footprints needed for newer mobile and embedded applications. However, proving that the compiler is managing the correct bit layout has been lacking for C++. This paper provides a formal verification approach based on semantic foundations that justify new layout optimizations. It introduces families of various memory layout algorithms and describes them by means of an operational semantics notation that is complex but still independent of the target architecture. These extensive formal layout details, provided using the Coq proof tools and the resulting semantic preservation correctness proofs, are a valuable contribution to the compiler field. Compiler technology has come a long way from the classic optimization steps of the basic language for implementation of system software (BLISS) compiler or the famous Nicholas Wirth Pascal compilers (with comments written in German). Though this paper provides some overview of previous C++ memory layout solutions, the authors' main contribution is their formal semantic proofs for complex multiple inheritance memory layouts. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 46, Issue 1

POPL '11

January 2011

624 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1925844

Issue’s Table of Contents

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2011
652 pages
ISBN:9781450304900
DOI:10.1145/1926385
General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Published in SIGPLAN Volume 46, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
545
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)2

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Malecha GStewart GFarka FHaag JHirai Y(2022)Developing With Formal Methods at BedRock Systems, Inc.IEEE Security & Privacy10.1109/MSEC.2022.315819620:3(33-42)Online publication date: May-2022
https://doi.org/10.1109/MSEC.2022.3158196
Monteiro FGadelha MCordeiro L(2021)Model checking C++ programsSoftware Testing, Verification and Reliability10.1002/stvr.179332:1Online publication date: 8-Sep-2021
https://doi.org/10.1002/stvr.1793
Hirai Y(2017)Defining the Ethereum Virtual Machine for Interactive Theorem ProversFinancial Cryptography and Data Security10.1007/978-3-319-70278-0_33(520-535)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-70278-0_33
Krebbers R(2013)Aliasing Restrictions of C11 Formalized in CoqCertified Programs and Proofs10.1007/978-3-319-03545-1_4(50-65)Online publication date: 2013
https://doi.org/10.1007/978-3-319-03545-1_4
Monteiro FGadelha MCordeiro L(2021)Model checking C++ programsSoftware Testing, Verification and Reliability10.1002/stvr.1793Online publication date: 8-Sep-2021
https://doi.org/10.1002/stvr.1793
Stroustrup B(2020)Thriving in a crowded and changing world: C++ 2006–2020Proceedings of the ACM on Programming Languages10.1145/33863204:HOPL(1-168)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3386320
Lochbihler A(2018)Mechanising a Type-Safe Model of Multithreaded Java with a Verified CompilerJournal of Automated Reasoning10.1007/s10817-018-9452-x61:1-4(243-332)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-018-9452-x
Krebbers R(2018)A Formal C Memory Model for Separation LogicJournal of Automated Reasoning10.1007/s10817-016-9369-157:4(319-387)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s10817-016-9369-1
Zakrzewski J(2018)Towards Verification of Ethereum Smart Contracts: A Formalization of Core of SolidityVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-03592-1_13(229-247)Online publication date: 24-Nov-2018
https://doi.org/10.1007/978-3-030-03592-1_13
Becker HCrespo JGalowicz JHensel UHirai YKunz CNakata KSacchini JTews HTuerk T(2016)Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a HypervisorFM 2016: Formal Methods10.1007/978-3-319-48989-6_5(69-84)Online publication date: 8-Nov-2016
https://doi.org/10.1007/978-3-319-48989-6_5
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

An operational semantics and type safety prooffor multiple inheritance in C++