Abstract
Real life C programs are often written using C dialects which, for the ISO C standard, have undefined behaviours. In particular, according to the ISO C standard, reading an uninitialised variable has an undefined behaviour and low-level pointer operations are implementation defined. We propose a formal semantics which gives a well-defined meaning to those behaviours for the C dialect of the CompCert compiler. Our semantics builds upon a novel memory model leveraging a notion of symbolic values. Symbolic values are used by the semantics to delay the evaluation of operations and are normalised lazily to genuine values when needed. We show that the most precise normalisation is computable and that a slightly relaxed normalisation can be efficiently implemented using an SMT solver. The semantics is executable and our experiments show that the enhancements of our semantics are mandatory to give a meaning to low-levels idioms such as those found in the allocation functions of a C standard library.
This work was supported by Agence Nationale de la Recherche, grant number ANR-12-INSE-002 BinSec.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bedin França, R., Blazy, S., Favre-Felix, D., Leroy, X., Pantel, M., Souyris, J.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS2 2012: Embedded Real Time Software and Systems (2012)
Bernstein, D.J., Lange, T., Schwabe, P.: The Security Impact of a New Cryptographic Library. In: Hevia, A., Neven, G. (eds.) LATINCRYPT 2012. LNCS, vol. 7533, pp. 159–176. Springer, Heidelberg (2012)
Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reasoning 43(3), 263–288 (2009)
Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A Precise Yet Efficient Memory Model for C. ENTCS 254, 85–103 (2009)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544. ACM (2012)
Greenaway, D., Andronick, J., Klein, G.: Bridging the Gap: Automatic Verified Abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 99–115. Springer, Heidelberg (2012)
Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don’t sweat the small stuff: Formal verification of C code without the pain. In: PLDI. ACM (2014)
ISO. ISO C Standard 1999. Technical report (1999)
Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 50–65. Springer, Heidelberg (2013)
Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL, pp. 101–112. ACM (2014)
Lee, D.: A memory allocator, http://gee.cs.oswego.edu/dl/html/malloc.html
Leroy, X.: Formal verification of a realistic compiler. Comm. ACM 52(7), 107–115 (2009)
Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014)
Lucanu, D., Şerbănuţă, T.F., Roşu, G.: \(\mathbb{K}\) Framework Distilled. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 31–53. Springer, Heidelberg (2012)
Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97–108. ACM (2007)
Wang, X., Chen, H., Cheung, A., Jia, Z., Zeldovich, N., Kaashoek, M.F.: Undefined behavior: What happened to my code? In: APSYS 2012, pp. 1–7 (2012)
Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards Optimization-safe Systems: Analyzing the Impact of Undefined Behavior. In: SOSP 2013, pp. 260–275. ACM (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Besson, F., Blazy, S., Wilke, P. (2014). A Precise and Abstract Memory Model for C Using Symbolic Values. In: Garrigue, J. (eds) Programming Languages and Systems. APLAS 2014. Lecture Notes in Computer Science, vol 8858. Springer, Cham. https://doi.org/10.1007/978-3-319-12736-1_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-12736-1_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12735-4
Online ISBN: 978-3-319-12736-1
eBook Packages: Computer ScienceComputer Science (R0)