File 11

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).
Due2019-12-2 11:45AM
5pts Exercise 1.
The source for CompCert is located at: 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?