20pts * Exploring an industrial scale, verified compiler
This assignment will be completely different. In it, you'll explore CompCert,
which is the largest verified compiler, and one of the only ones that is
actually used in industry (including by Airbus).
5pts Exercise 1.
The source for CompCert is located at:
https://github.com/AbsInt/CompCert
Download it, install it, and use the tracing interpreter mode to print the
output for a small C program you write (it can be only a few lines long).
i.e., [ccomp -interp -trace myprog.c]
Include your program and output here, as a comment.
5pts (3pts for identifying, 2pts for description of why both exist) Exercise 2.
In
common/Smallstep.v, there is an inductive definition
forward_simulation and
another
backward_simulation. These are given meaning primarily via the corresponding "properties" records that they contain. They are
similar to one another, and one corresponds to the simulation arguments that we have been using throughout the semester -- which one? Why do you think both exist?
6pts (for at least changes in those six files) Exercise 3.
You've decided that you do not like unary minus, and have decided to remove
support for it from the CompCert frontend. Remove the
Oneg inductive from the
unary_operation Inductive in
cfrontend/Cop.v and fix everything that you need to fix so that you can run
make all and have your newly unary-minus-stripped CompCert build.
Run
git diff --stat in the CompCert repository and include, in a comment, the output that it produces (this is a summary of all the lines you had to change or remove).
4pts Exercise 4.
In
driver/Compiler.v is a theorem called
c_semantic_preservation. Please explain what it is doing at a high level: you don't have to go into incredible detail, a few detailed sentences or a short paragraph will do. One thing your explanation should certainly answer is: why is this proof so short? What does it appeal to and how?