Due: Mon, 25 Apr 2016 23:00:00 -0700

GCC and LLVM come with a large set of peephole optimizations. In this assignment, you will enhance CompCert with some of these optimizations, with a correctness proof.

Choose one of the CompCert IRs for your peephole optimizations. You may choose an architecture-independent one, such as Cminor, or any of the backends, such as arm, powerpc, and x86. We would suggest you use the arm configuration as in lecture, or try using Peek for x86.

The Alive paper from PLDI’15 describes a peephole optimization in LLVM:

This rewrites `(x ^ (-1)) + C`

to `(C - 1) - x`

.
Implement the optimization in CompCert and verify its correctness.

You may use the following C code for testing.

Without your optimizer, CompCert emits the following:

With your optimizer, CompCert should be able to emit fewer instructions, such as:

Here is a brief description of some arm instructions:

`add dst, src₁, src₂`

(add) means`dst ← src₁ + src₂`

.`mvn dst, src₁`

(move not) means`dst ← ~src₁`

(is this correct for`x ^ (-1)`

?).`rsb dst, src₁, src₂`

(reverse subtract) means`dst ← src₂ - src₁`

.`sub dst, src₁, src₂`

(subtract) means`dst ← src₁ - src₂`

.

See `arm/Asm.v`

for detailed definitions.

Note that CompCert generates the `mvn`

instruction for `x ^ (-1)`

,
which is `~x`

.
Which compiler pass do you think performs this optimization?

Hint: `ccomp`

has a number of `-d*`

options to dump the IRs for inspection.
Use `--help`

to see a complete list.

Briefly describe which IR you choose to implement your optimization and why.

Do you think your optimization provides a stronger, weaker, or the same level of correctness guarantees compared to Alive? How about the quality of generated code? Briefly explain.

Here’s another LLVM peephole optimization described in Alive:

This rewrites `a + (0 - b)`

to `a - b`

.
Implement the optimization in CompCert.
Use `admit`

to skip the proof for now.

You may use the following C code for testing.

Without your optimizer, CompCert emits the following:

With your optimizer, CompCert should be able to emit fewer instructions, such as:

Try to verify the correctness of this optimization. You don’t have to finish the proof. If you get stuck, briefly describe the problem.

A complete proof will receive bonus points.

Up to this point, you have implemented three new optimizations for CompCert. Add more peephole optimizations to CompCert, or design a general framework for writing verified peephole optimizations.

Submit a plain text file named `answers.txt`

,
consisting of a git-diff of your peephole optimizations
and your answers to the questions.