Skip to content

Latest commit

 

History

History
 
 

DirectRefinement

CompCertO

A version of CompCert featuring an open module semantics, designed to target the framework of refinement-based game semantics.

Overview

This is a modified version of CompCert v3.6. The language semantics and correctness proofs have been updated to describe the behavior of individual compilation units. Most passes from Clight to Asm have been update, for the x86 architecture.

Building

Since our compiler uses Clight as the source language, the first few passes are not available and the full extracted compiler cannot be built. However the Coq version of the Clight to Asm compiler can be compiled in the following way.

Requirements

Build requirements are identical to those of CompCert v3.6. We recommend using the opam package manager to set up a build environment. We have tested CompCertO on Linux with the following opam installation:

% opam list
# Packages matching: installed
# Name          # Installed # Synopsis
base-bigarray   base
base-threads    base
base-unix       base
camlp5          7.14        Preprocessor-pretty-printer of OCaml
conf-findutils  1           Virtual package relying on findutils
conf-m4         1           Virtual package relying on m4
conf-perl       1           Virtual package relying on perl
conf-pkg-config 1.3         Virtual package relying on pkg-config installation
coq             8.9.1       pinned to version 8.9.1
coq-coq2html    1.2         Generates HTML documentation from Coq source files.  Alternative to coqdoc
dune            2.8.2       Fast, portable, and opinionated build system
menhir          20201216    An LR(1) parser generator
menhirLib       20201216    Runtime support library for parsers generated by Menhir
menhirSdk       20201216    Compile-time library for auxiliary tools related to Menhir
num             1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml           4.08.1      The OCaml compiler (virtual package)
ocaml-config    1           OCaml Switch Configuration
ocaml-system    4.08.1      The OCaml compiler (system version, from outside of opam)
ocamlfind       1.8.1       A library manager for OCaml

You should be able to reproduce this installation with the following sequence of shell commands:

# Initialize opam (if you haven't used it before)
opam init --bare

# Create an "opam switch" dedicated to building CompCertO
opam switch create compcerto ocaml-base-compiler.4.08.1

# Install the necessary packages
opam repository add coq-released https://coq.inria.fr/opam/released
opam install coq.8.9.1 camlp5.7.14 menhir.20201216 coq-coq2html.1.2

# Configure the current shell to use the newly created opam switch
eval $(opam env)

Build instructions

In addition, our modifications rely on the Coqrel library, which must be built first. We will include Coqrel in any self-contained archive we distribute, but if you are working in a git clone, you must first retreive it with the following commands:

% git submodule init
% git submodule update

In any case, to build Coqrel, proceed in the following way:

% (cd coqrel && ./configure && make)

You can then build the updated proof as follows:

% ./configure x86_64-linux
% make
% make documentation

If appropriate to your setting, we recommend you use a -j option when invoking make so as to enable parallel compilation.

Documentation

After running make documentation you will be able to browse the generated documentation. We have annotated the index file to highlight the changes and additions made in CompCertO.