Actually, if you take a look at the semantic preservation theorems that CompCert actually proves, you can see that it allows for compilation to fail, even in optimization and code generation:

http://compcert.inria.fr/doc/html/Compiler.html

As one particular example, register allocation is performed by an untrusted oracle that may not even terminate, and then verified a posteriori:

http://compcert.inria.fr/doc/html/Allocation.html

They proved a traditional register allocator correct in a paper (https://www.cs.princeton.edu/~appel/papers/regalloc.pdf), but I guess there are practical reasons why they are not using it in CompCert by default.