Advertisement

A Precise and Abstract Memory Model for C Using Symbolic Values

  • Frédéric Besson
  • Sandrine Blazy
  • Pierre Wilke
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)

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.

Keywords

Memory Model Formal Semantic Complete Normalisation Allocation Function Alignment Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reasoning 43(3), 263–288 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A Precise Yet Efficient Memory Model for C. ENTCS 254, 85–103 (2009)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544. ACM (2012)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    ISO. ISO C Standard 1999. Technical report (1999)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL, pp. 101–112. ACM (2014)Google Scholar
  13. 13.
    Lee, D.: A memory allocator, http://gee.cs.oswego.edu/dl/html/malloc.html
  14. 14.
    Leroy, X.: Formal verification of a realistic compiler. Comm. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  15. 15.
    Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)Google Scholar
  18. 18.
    Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97–108. ACM (2007)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Frédéric Besson
    • 1
  • Sandrine Blazy
    • 2
  • Pierre Wilke
    • 2
  1. 1.InriaRennesFrance
  2. 2.Irisa - Université Rennes 1RennesFrance

Personalised recommendations