This is a work in progress student project on making a certified compiler for a subset of C. For now, I have a working compiler, but some bugs remain and it's not certified. The lexer, parser, and typechecker are written in OCaml, the code generator is written in C. I have also defined the semantics of PetitC and the target subset of x86 assembly (except for the for loop in PetitC, which's semantics I haven't specified yet). I have proven in Coq that the semantics of PeticC is deterministic.
PetitC is a subset of C wich contains integers, booleans, pointers, arithmetic, pointer arithmetic, short circuit operations, calls to putchar and malloc, for and while loops with break and continue, if statements, functions with recursion and retutrn statements, and a GNU C extension - embedded functions.
The full description in French can be found here (you don't need French to understand, the syntax is defined on page 3 and the semantics are the same as in C).
make all
Check the proofs and produce the petitc executable.
make check
Check the proofs.
make clean
Delete compiled files and OCaml files extracted from Coq code.
./petitc [options] file.c
Produces an assembly file file.s. It can then be assembled into an executable with clang -no-pie file.s -o file.out.
The options are:
--type-only don't produce an assembly file, only parse and typecheck.
--parse-only don't produce an assembly file, only check if the syntax is correct.
I would like to thank Jean-Cristophe Filliatre for his wonderful course on programming languages and compilation in ENS de Paris.