The CH₂O formalization of ISO C11

By Robbert Krebbers, ICIS, Radboud University Nijmegen

This is an ongoing development. If you are looking for the Coq sources corresponding to specific papers, take a look here.

About

The CH₂O project aims at formalizing novel features of the ISO C11 standard of the C programming language. CH₂O provides an operational, executable, and axiomatic semantics for a significant fragment of C11.

Our recent paper A Typed C11 Semantics for Interactive Theorem Proving at CPP 2015 gives a good overview of the CH₂O project.

Papers

1. Robbert Krebbers. A Formal C11 Memory Model for Separation Logic. Draft.
   [pdf]
2. Robbert Krebbers and Freek Wiedijk. A Typed C11 Semantics for Interactive Theorem Proving. In CPP, pages 15-27, 2015.
   [pdf] [at publisher] [slides]
3. Robbert Krebbers. Separation algebras for C verification in Coq. In VSTTE, volume 8471 of LNCS, pages 150-166, 2014.
   [pdf] [at publisher] [slides]
4. Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP, volume 8558 of LNCS, pages 543-548, 2014.
   [pdf] [at publisher] [slides] [coq sources]
5. Robbert Krebbers. An operational and axiomatic semantics for non-determinism and sequence points in C. In POPL, pages 101-112, 2014.
   [pdf] [at publisher] [slides] [coq sources]
6. Robbert Krebbers. Aliasing restrictions of C11 formalized in Coq. In CPP, volume 8307 of LNCS, pages 50-65, 2013.
   [pdf] [at publisher] [slides]
7. Robbert Krebbers and Freek Wiedijk. Separation Logic for Non-local Control Flow and Block Scope Variables. In FoSSaCS, volume 7794 of LNCS, pages 257-272, 2013.
   Awarded best student contribution.
   [pdf] [at publisher] [slides] [coq sources]
8. Robbert Krebbers and Freek Wiedijk. A Formalization of the C99 Standard in HOL, Isabelle and Coq. In CICM, volume 6824 of LNAI, pages 297-299, 2011.
   [pdf] [at publisher] [poster] [slides]

Download

The most recent version of the Coq source code of this development can be downloaded here. Use:

  scons -j [num cores]

to compile the development. This yields an executable called ch2o that can be used to test the CH₂O semantics against actual C source files.

Table of contents

Prelude

• base: interfaces, notations, and general theorems.
• tactics: general purpose tactics.
• proof_irrel: facts about proof irrelevant types/propositions.
• decidable: theorems on decidable structures.
• orders: theorems on ordered structures.
• option: the option monad, and various theorems on the option type.
• error: the error monad.
• list: miscellaneous definitions and theorems on lists.
• streams: miscellaneous definitions and theorems on streams.
• vector: miscellaneous definitions and theorems on vectors.
• numbers: miscellaneous facts on nat, N and Z.
• ars: theorems and definitions on abstract rewriting systems.
• collections: definitions, theorems, and tactics for collections.
• fin_collections: theorems on finite collections.
• listset: finite set implementation using unordered lists.
• fresh_numbers: generation of fresh numbers.
• prelude: exports all of the above.

Finite maps

• fin_maps: an interface and properties of finite maps.
• fin_map_dom: an interface and theorems for the domain function of finite maps.
• mapset: finite maps give rise to finite sets with extensional equality.
• natmap, pmap, nmap, zmap, and stringmap finite maps indexed by nat, positive, N, Z, and string.
• hashset: simple hashsets using finite maps over positive.

Type system and integers

• integer_coding: abstract interface for integer representations.
• integer_operations: abstract interface for integer operations.
• type_classes: classes to overload notations for typing judgments.
• types: C types and type environments.
• type_environment: abstract interface for implementation defined properties.
• architecture_spec: type environment specifications based on concrete architectures.
• architectures: some specific architectures (ilp32, llp64 and lp64).

Permissions and separation algebras

• separation: abstract interface and properties of separation algebras.
• separation_instances: boolean, fractional, counting, lockable and tagged separation algebras.
• permissions: the CH₂O permission system as a separation algebra.
• ctrees: separation algebra of abstract trees representing memory objects.
• cmap: separation algebra of abstract forests representing memories.

Memory model

• memory_basics: basic definitions of the memory model.
• references: paths through types/ctrees.
• addresses (refinements): addresses into the memory.
• pointers (refinements): definition of pointers (address or NULL).
• pointer_bits (refinements): pointer fragment bits (pointer with index).
• bits (refinements): symbolic bits (0, 1, indeterminate, or pointer fragment).
• permission_bits (refinements and separation): bits annotated with permissions.
• memory_trees (refinements and separation): memory operations on C trees.
• memory_map (refinements and separation): memory operations on C maps.
• base_values (refinements): base values (void, indeterminate, integer, or pointer).
• values (refinements and separation): abstract values (base value, array, struct, or union).
• memory (refinements and separation): the CH₂O memory model and its operations.
• aliasing: abstract proof showing that type-based alias analysis is allowed.
• constant_propagation: abstract proof of constant propagation with respect to the memory model.

Operational semantics

• assignments (separation): semantics of assignments.
• operations (refinements): semantics of casts, unary and binary operations.
• expressions: expressions and their decomposition into evaluation contexts.
• statements: statements and program contexts.
• state: the CH₂O core C execution state.
• smallstep: the CH₂O core C small step operational semantics.
• type_system (decidable): type judgments for expressions, statements, and states.
• type_preservation: type preservation and (weak) progress.

Refinements

• memory_injections: functions to map a memory into another.
• refinement_classes: classes to overload notations for refinement judgments.
• refinements: basic definitions of the memory refinements.
• refinement_system: refinement judgments for expressions, statements, and states.
• refinement_preservation: preservation of refinements with respect to the operational semantics.

Executable semantics

• expression_eval (correctness and separation): evaluation of constant expressions.
• executable: the CH₂O core C executable semantics as a Coq function.
• executable_sound and executable_complete: soundness and completeness of the executable semantics with respect to the operational semantics.
• frontend (type soundness): CH₂O abstract C and its type preserving translation into CH₂O core C.
• interpreter (extraction): gluing the frontend and executable semantics together.

Separation logic

• memory_singleton: singleton memory.
• assertions: assertions of the separation logic.
• axiomatic_graph. Interpretation of the judgments of the separation logic.
• axiomatic. Interpretation of the judgments of the separation logic.
• axiomatic_expressions: inferences rules for expressions.
• axiomatic_functions: inferences rules for functions.
• axiomatic_statements: inference rules for statements.
• axiomatic_simple: inferences rules for expressions whose result is known.
• example_gcd: verification of Euclid's gcd algorithm.