PaperlayerView exact revision on arXiv

Source-linked AI summary

Mechanized semantics for the Clight subset of the C language

Sandrine Blazy, Xavier Leroy

arXiv:0901.3619v1cs.PL

TL;DR

The paper addresses the need for mechanized formal semantics for realistic C subsets. It defines Clight’s deterministic big-step semantics in Coq and integrates it with CompCert, whose preservation proofs help validate the semantics. The paper also identifies limits of validation through shared formal components and unresolved trace-equivalence issues.

  • Problem

    Formal semantics are important for compiler verification and program analysis, yet only a few semantics for lower-level languages such as C have been mechanized.

  • Method

    The paper defines Clight’s pure-expression, deterministic big-step operational semantics in Coq and uses it within the CompCert verified compiler.

  • Results

    The CompCert front-end preservation proof for Clight-to-Cminor requires about 2200 lines of Coq plus 800 lines formalizing memory injections.

  • Takeaways & Limitations

    Semantic-preservation proofs can expose errors in both translation algorithms and the source and target semantics, providing an effective validation approach for Clight.

  • Takeaways & Limitations

    Validation is weakened when compared semantics share formalized components, and trace-based equivalence with alternate semantics remains unresolved.

Abstract

from arXiv · show

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.

1 Introduction

The paper defines and mechanizes Clight, a substantial C subset, to support precise language semantics and verified compilation. It also explains how CompCert integration and validation approaches build confidence in the semantics.

  • Motivation: The work addresses the comparatively limited mechanization of formal semantics for lower-level languages such as C.The paper notes that many C-subset semantics exist, but few have been mechanized.
  • Contribution: Clight covers most C types and operators, including pointer arithmetic, function pointers, structs, unions, and structured control flow except goto.Its semantics is mechanized in Coq as a big-step semantics covering termination, divergence, and input/output traces.
  • CompCert integration: CompCert uses Clight as the source language for a verified compiler whose correctness proofs establish semantic preservation through compiler transformations.The reported project includes a Clight-to-Cminor front end and a verified back end producing PowerPC assembly.
  • Validation: The paper considers compiler correctness, expert review, and other comparisons as ways to validate a large and complicated formal semantics.It specifically presents CompCert’s correctness proof as an indirect validation method for Clight.
  • Availability: The underlying Coq development is available online for consultation.The paper gives the CompCert website as the access point.

2 Abstract syntax of Clight

Clight uses a deeply embedded, statically typed abstract syntax for a broad but deliberately restricted C subset. Expressions are pure and terminating, while assignments and calls are statements, simplifying deterministic reasoning and program analysis.

  • Abstract syntax: Clight’s Coq abstract syntax is represented by inductive data types, providing a deep embedding of expressions, statements, and functions.The syntax is organized into expressions, statements, and functions.
  • Types: Clight types include integers, floats, arrays, pointers, function types, structs, and unions, while typedef names are removed during parsing and type-checking.Pointers may include pointers to functions, and named types are omitted from the syntax.
  • Expressions: Expressions carry static type annotations that determine overloaded and type-dependent operator behavior, and l-values include variables, dereferences, and field accesses.The expression syntax includes arithmetic, bitwise, and relational operators.
  • Expressions: Clight expressions exclude assignments and calls, making every expression pure and terminating; these properties support deterministic semantics and simplify logic and static analysis.Assignments and calls are instead represented as statements.
  • Statements: Statements support structured conditionals, loops, switch, break, continue, return, assignment, and calls, but exclude goto and unstructured switch constructs.Function-call results may be assigned or discarded.
  • Control flow: A for loop uses statements rather than C expressions for initialization and iteration because Clight expressions are pure, and these statements must terminate normally.The loop body and condition follow Clight’s structured syntax.
  • Programs: Clight programs contain global declarations, functions, and an entry-point identifier, with internal and external functions distinguished in the function syntax.Global initialization is limited to sequences of integer or floating-point constants.

3 Formal semantics for Clight

Clight’s dynamic semantics is a deterministic Coq mechanization of big-step execution that represents termination, divergence, memory effects, outcomes, and external I/O traces. Its judgements cover expressions, statements, functions, and whole programs.

  • 3 Formal semantics for Clight: The semantics uses natural, or big-step, operational semantics to observe either termination or divergence together with traces of external-function invocations.Because expressions are pure, the dynamic semantics is deterministic.
  • 3 Formal semantics for Clight: The dynamic semantics is defined without a formal static typing specification and may go wrong when expression type annotations are inconsistent.Such programs may be undefined or may differ from C-standard behavior.
  • 3.1 Evaluation judgements: Ten judgements relate syntactic elements to locations, values, statement outcomes, function results, diverging executions, and whole-program behaviors.The listed judgements distinguish l-value and r-value evaluation, statement execution, switch execution, and function invocation.
  • 3.1 Evaluation judgements: Clight values comprise 32-bit integers, 64-bit floating-point values, pointers represented by locations, and undef values from uninitialized memory.Locations pair a block identifier with a byte offset.
  • 3.1 Evaluation judgements: Global and local environments resolve program entities and variables, while local variables reside in memory blocks allocated at function entry and freed at return.The indirection permits the address-of operator to take variable addresses.
  • 3.1 Evaluation judgements: Memory states consist of separated blocks with allocation-time bounds and support operations including allocation, deallocation, loading, and storing.The memory model identifies blocks by integers and represents byte offsets within their bounds.
  • 3.1 Evaluation judgements: Statement and function executions return updated memory states and traces recording external-function events, whereas pure expression evaluation leaves memory unchanged.Each event records an external invocation and its program-provided arguments.
  • 3.1 Evaluation judgements: Terminating and diverging executions are encoded in Coq by mutually inductive and mutually coinductive predicates corresponding to inference rules.Divergence produces a possibly infinite trace of input/output events.

3.2 Evaluation of expressions

Clight evaluates pure expressions through typed l-value, r-value, conversion, and operator rules, then executes statements and calls by threading outcomes, memory states, and event traces. The semantics intentionally excludes several C behaviors and composite assignments.

  • Expressions: Variable and dereference expressions evaluate in l-value position to memory locations, while struct fields add field offsets and union fields share one location.A variable’s location is determined from local or global environments.
  • Expressions: In r-value position, scalar l-values load values from memory, arrays yield their locations, and void, struct, and union values are not readable.The loadval function handles the conversion from locations to values.
  • Expressions: Unary and binary operators evaluate operands and combine their typed values through eval_binop, including pointer arithmetic scaled by the pointed-to type size.Pointer-plus-integer computes a pointer offset using n × sizeof(τ).
  • Expressions: Conditional expressions use type-dependent truth predicates, with zero integers and null pointers false, nonzero integers and pointers true, and other combinations causing the semantics to go wrong.For floats, only 0.0 is false.
  • Expressions: Casts evaluate an expression and apply a partial typed conversion function that handles integer and floating-point conversions and selected pointer-integer conversions.Conversions between pointers and floats or small integers may fail.
  • Statements: Assignments evaluate a destination l-value and source r-value, then store the source value without implicit casting because the parser inserts explicit casts beforehand.Assignments between struct and union values are unsupported.
  • Statements: Sequences concatenate traces and use the first statement’s outcome to determine whether the second statement executes.Skip, break, continue, and return produce corresponding outcomes under the statement rules.
  • Loops and switch: Loops propagate break, continue, and return outcomes according to dedicated rules, while for loops execute initialization and iteration statements before re-entering the loop.Switch cases execute with fall-through, and break terminates the switch normally.

4 Using Clight in the CompCert compiler

Clight is integrated into CompCert through a CIL-based producer and verified front-end transformations into Cminor. The compiler preserves semantics across these transformations, while the producer remains only partially trusted because CIL is unverified.

  • Producing Clight abstract syntax: CIL parses, type-checks, elaborates, and simplifies C code before a translator produces Clight abstract syntax.The simplifier lifts function calls and assignments to statement level and adjusts variable scope.
  • Producing Clight abstract syntax: The translator erases selected C information, converts named struct and union types to Clight’s structural representation, and rejects unsupported constructs.String literals become global initialized character arrays.
  • Producing Clight abstract syntax: CIL was patched to preserve native while, do, and for loops because its original loop simplification introduced problematic goto statements.The patch addresses Clight’s lack of goto while retaining these C loop forms.
  • Producing Clight abstract syntax: CIL and the hand-written translator are not formally verified, and testing found two bugs in this part of CompCert.One bug arose in added for-loop support; another existed in unmodified CIL version 1.3.6 and was later corrected.
  • Compiling Clight: Semantic-preservation proofs cover the compiler passes, including a 2200-line Coq proof plus 800 lines formalizing memory injections for one transformation.Memory injections handle differing allocation patterns and require reasoning about separation between blocks and sub-areas.
  • Compiling Clight: The front-end translates Clight to Cminor by resolving type-dependent behavior, then compiling expressions and statements through a proof-manageable two-pass design.The split introduced C#minor between the first and second passes, replacing an earlier single-pass implementation with a large preservation proof.

5 Validating the Clight semantics

The Clight semantics was validated through expert review, mechanized property proofs, executable testing, and comparisons with alternate semantics, each exposing different classes of errors and limitations.

  • 5.1 Manual reviews: Expert review is difficult but feasible because the Clight formalization spans about 800 lines of core semantics and 1000 lines of dependencies.Coq type-checking prevents type errors and undefined predicates, but domain experts may prefer conventional inference-rule presentations.
  • 5.2 Proving properties of the semantics: Type soundness is limited for Clight because C's coarse, unsound type system prevents the progress property from holding.The formalization instead supports narrower checks, including subject reduction, field_offset properties, and determinism of evaluation.
  • 5.3 Verified translations: Semantic-preservation proofs can expose errors in both translations and the source and target semantics, complementing type-soundness proofs.The two proof styles detect different failures: preservation can reveal an incorrect operator interpretation, while type soundness can reveal missing evaluation rules.
  • 5.4 Testing executable semantics: Executable testing is constrained because Coq offers no efficient execution for Clight's large, non-syntax-directed inductive semantics.A reference interpreter was being implemented to test both defined and undefined programs, whereas CompCert may compile undefined programs into correct PowerPC code.
  • 5.5 Equivalence with alternate semantics: Alternate-semantics proofs can reveal mistakes, but shared implementation components and unresolved trace issues limit the strength of equivalence-based validation.The authors note that independently written semantics would provide more convincing validation, while relating Clight to Cholera is complicated by Coq-versus-HOL formalization.

6 Related work

Prior work spans mechanized and paper-based semantics for C and related languages, differing in language coverage, evaluation strategy, and treatment of nontermination or nondeterminism.

  • Mechanized semantics for C: Cholera mechanizes static and dynamic semantics for a large C subset in HOL, supporting expression side effects and partially specified evaluation order.Expressions use a nondeterministic small-step relation, while statements use big-step semantics.
  • Subsets of C: Other mechanized C subsets trade language coverage for specialized goals, omitting features such as pointer arithmetic, general loops, recursion, or control-flow statements.These include Lustre-oriented C, Verisoft’s C0, and other Pascal-like subsets.
  • Paper and pencil semantics for C: Paper-based C semantics include monadic denotational and big-step approaches, with nondeterministic expression evaluation modeled or validated using a reference interpreter.Papaspyrou’s semantics covers most of ISO C and was tested against a Haskell interpreter.
  • Other examples of mechanized semantics: Abstract state machines have been used for C and C#, while proof assistants have also mechanized semantics for Standard ML, OCaml, and Java.Several higher-level language formalizations were validated through type soundness proofs.
  • Subsets of C: MISRA C shares some restrictions with Clight but differs substantially, notably by prohibiting recursive functions while permitting all uses of goto.Its restrictions are driven by coding guidelines for embedded or critical applications.
  • Subsets of C: Intermediate representations for C analysis and verification vary in scope: CIL is richer than Clight, whereas Newspeak is lower-level and differently targeted.Frama-C extends CIL with logical assertions.

7 Conclusions and future work

The paper defines and mechanizes Clight’s dynamic semantics as a proposal suited to compiler verification. It identifies future extensions for memory modeling and missing C constructs, while noting trade-offs from pure expressions.

  • Conclusions: The article formally defines the Clight subset of C and its dynamic semantics.This is presented as the paper’s central formal contribution.
  • Conclusions: Clight is presented as a reasonable proposal that works well for formal verification of a compiler.The authors suggest possible future use in static analyzers and program provers.
  • Future work: A proposed extension would relax the memory model to represent byte- and bit-level accesses to in-memory data representations.The motivation is common systems-programming practice.
  • Future work: Adding goto requires a dynamic semantics that supports proofs; one natural-semantics approach would nearly double the semantics’ size.Transition semantics offer an easier route for adding goto.
  • Future work: Pure expressions simplify compilation, static analysis, and program verification but require nontrivial untrusted parser transformations because programmers cannot be expected to write only pure expressions.The paper characterizes purity as both a blessing and a curse.
Loading 0901.3619v1…