Assignment: CompCert

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.

AddSub:1202

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

Name: AddSub:1202
%nx = xor %x, -1
%r = add %nx, C
  =>
%r = sub C-1, %x

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.

int foo(int x)
{
	return (x ^ (-1)) + 42;
}

Without your optimizer, CompCert emits the following:

foo:
	...
	mvn     r0, r0
	add     r0, r0, #42
	...

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

foo:
	...
	rsb     r0, r0, #41
	...

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.

Question

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.

Question

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

Question

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.

AddSub:1176

Here’s another LLVM peephole optimization described in Alive:

Name: AddSub:1176
%nb = sub 0, %b
%c = add %a, %nb
  =>
%c = sub %a, %b

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.

int foo(int a, int b)
{
	return a + (0 - b);
}

Without your optimizer, CompCert emits the following:

foo:
	...
	rsb     r1, r1, #0
	add     r0, r0, r1
	...

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

foo:
	...
	sub     r0, r0, r1
	...

Question

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.

Challenge

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.

What to submit

Submit a plain text file named answers.txt, consisting of a git-diff of your peephole optimizations and your answers to the questions.