×

zbMATH — the first resource for mathematics

A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. (English) Zbl 07048640
Summary: The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data. We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive low-level C idioms that require the additional expressiveness provided by our memory model. We also show that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics. Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value. We show how to tame the expressive power of the normalisation so that the memory model fits the proof framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert’s front-end, thus demonstrating that our model is well-suited for proving compiler transformations.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Leroy, X., Formal verification of a realistic compiler, Commun. ACM, 52, 107-115, (2009)
[2] Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL (2015). doi:10.1145/2676726.2676966
[3] Clements, A.T., Kaashoek, M.F., Zeldovich, N., Morris, R.T., Kohler, E.: The scalable commutativity rule: designing scalable software for multicore processors. In: SOSP. ACM (2013)
[4] Wang, X., Chen, H., Cheung, A., Jia, Z., Zeldovich, N., Kaashoek, M.: Undefined behavior: what happened to my code? In: APSYS ’12 (2012)
[5] Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014). http://hal.inria.fr/hal-00905435 · Zbl 1298.68009
[6] Leroy, X.; Blazy, S., Formal verification of a C-like memory model and its uses for verifying program transformations, J. Autom. Reason., 41, 1-31, (2008) · Zbl 1154.68039
[7] Besson, F., Blazy, S., Wilke, P.: Companion website with Coq development. http://www.irisa.fr/celtique/ext/frontend-symbolic
[8] ISO: C Standard 1999. Technical report, ISO (1999). http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf
[9] Leroy, X., A formally verified compiler back-end, J. Autom. Reason., 43, 363-446, (2009) · Zbl 1185.68215
[10] MIRA Ltd: MISRA-C:2004 Guidelines for the use of the C language in critical systems (2004). www.misra.org.uk
[11] Kang, J., Hur, C.K., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal C memory model supporting integer-pointer casts. In: PLDI. ACM (2015)
[12] de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS, LNCS, vol. 4963. Springer (2008)
[13] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, chap. CVC4, pp. 171-177. Springer, Berlin, Heidelberg (2011). 10.1007/978-3-642-22110-1_14
[14] Lee, D.: A memory allocator. http://gee.cs.oswego.edu/dl/html/malloc.html
[15] Bernstein, D.J., Lange, T., Schwabe, P.: The Security Impact of a New Cryptographic Library. In: LATINCRYPT’12, LNCS, vol. 7533, pp. 159-176. Springer (2012) · Zbl 1303.94067
[16] Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI. ACM (2011)
[17] Blazy, S.: Experiments in validating formal semantics for C. In: C/C\(++\) Verification Workshop. Raboud University Nijmegen report ICIS-R07015 (2007)
[18] ISO: C Standard 2011. Technical report, ISO (1999). http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1570.pdf
[19] Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)
[20] Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL. ACM (2007) · Zbl 1295.68094
[21] Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. ENTCS 254 (2009)
[22] Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., al.: VCC: A practical system for verifying concurrent C. In: TPHOLs, LNCS, vol. 5674. Springer (2009)
[23] Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: ITP, LNCS, vol. 7406. Springer (2012) · Zbl 1360.68751
[24] 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)
[25] Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL. ACM (2012)
[26] Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of c. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15), pp. 336-345. ACM (2015). doi:10.1145/2813885.2737979
[27] Blazy, S., Leroy, X.: Mechanized semantics for the clight subset of the C language. J. Autom. Reason. 43(3) (2009) · Zbl 1185.68136
[28] 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). https://hal.inria.fr/hal-00653367
[29] Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: Compcert and the C standard. In: ITP 2014, LNCS, vol. 8558. Springer (2014) · Zbl 06341505
[30] Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL. ACM (2014) · Zbl 1284.68404
[31] Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: CPP, LNCS, vol. 8307. Springer (2013). doi:10.1007/978-3-319-03545-1_4 · Zbl 1426.68055
[32] Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: PLDI’14, p. 30. ACM (2014)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.