The notion of a correct compiler seems to be self-explaining. Compilation is correct when the compiled program behaves exactly as the source program specifies. Recently I read a paper about the formally verified C compiler CompCert1 and it turns out that there are some points worth thinking about when specifying compiler correctness. The straight-forward specification would be to say that source program and compiled program have the same observable behaviors.


Notion (1) is too strong to be usable. If the source language is not deterministic, compilers are allowed to select one of the possible behaviors of the source program. (For instance, C compilers choose one particular evaluation order for expressions among the several orders allowed by the C specifications.) In this case, C will have fewer behaviors than S. Additionally, compiler optimizations can optimize away “going wrong” behaviors.

from “Formal verification of a realistic compiler”1, page 2 section 2.1

Here Notion (1) refers to the straight-forward specification. While the point about non-determinism made sense (why have non-determinism otherwise?), I did not understand the one about optimizations at first. Compiler optimizations should preserve program semantics after all I thought? I thought about it and came up with an example to illustrate the point.

A concrete example

The following C program throws an error when its compiled without optimization, but runs fine with optimization flags on. I use gcc version 7.3.0 to compile it to assembly using the -S flag.

int main {
  int* p = NULL;
  int x = *p;
  return 0;

Compiling this without optimization flag results in a literal translation of the main function:

  pushq	%rbp
  .cfi_def_cfa_offset 16
  .cfi_offset 6, -16
  movq	%rsp, %rbp
  .cfi_def_cfa_register 6
  movq	$0, -8(%rbp)
  movq	-8(%rbp), %rax
  movl	(%rax), %eax
  movl	%eax, -12(%rbp)
  movl	$0, %eax
  popq	%rbp
  .cfi_def_cfa 7, 8

This includes the code for creating and dereferencing the null pointer which results in a segmentation fault if you run it. Obviously both p and x are completely useless though for the “computation” though. The first level of optimization (-O1) is smart enough to see that and produces:

  movl	$0, %eax

No more segfault!

The solution

As you can see it skipped all the pointer business and just produced code to return the integer 0. I guess in most cases this is desired behavior of the compiler and should be allowed in a correctness specification. Therefore the straight-forward specification is not enough. CompCert uses the following (In my wording):

If the source program does not go wrong then the compiled program does not go wrong either. Moreover, all observable behaviors of the compiled program are acceptable behaviors of the source program.

This allows both things mentioned at the beginning of the post: Compilers are allowed to choose one behavior in case of non-determinism in the source language and optimize away wrong behaviors. Note that it does not say anything about programs that contain “going wrong behavior”.

  1.  2