Mechanized semantics for the Clight subset of the C language
Sandrine Blazy (CEDRIC, INRIA Rocquencourt), Xavier Leroy (INRIA, Rocquencourt)
TL;DR
This paper defines a formal, mechanized big-step operational semantics for Clight, a substantial subset of C, facilitating verified compilation in the CompCert project with validation of the semantics.
Contribution
It introduces a mechanized formal semantics for Clight, including handling of complex features like pointers and structured types, integrated into a verified compiler.
Findings
Semantics observed both terminating and diverging executions
Mechanized using Coq proof assistant
Validated through integration with the CompCert compiler
Abstract
This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, "struct" and "union" types, C loops and structured "switch" statements. Clight is the source language of the CompCert verified compiler. The formal semantics of Clight is a big-step operational semantics that observes both terminating and diverging executions and produces traces of input/output events. The formal semantics of Clight is mechanized using the Coq proof assistant. In addition to the semantics of Clight, this article describes its integration in the CompCert verified compiler and several ways by which the semantics was validated.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.