Using VST with GCC

Question

The Verifiable-C manual says

Whatever observable property about a C program you prove using the Verifiable C program logic, that property will actually hold on the assembly-language program that comes out of the C compiler.

and then

The program logic is proved sound with respect to the semantics of CompCert C (...).

What if I use another compiler (say gcc - assuming gcc itself is correct wrt the C standard)?

Does the logic (or clightgen) assumes facts that may not be verified by some C compliant compiler that is not Compcert?

Edit:

I made a little experiment, I compiled the following with gcc and compcert.

#include<stdio.h>
#include<limits.h>

int signed_overflow_expression(int x, int y) {
    return (x+y) > y;
}

int main(){
    printf("%i",signed_overflow_expression(INT_MAX,1));
}

gcc prints 1 as explained here https://stackoverflow.com/a/54510856/1891138.

Compcert prints 0, because signed overflow is actually defined behaviour in Compcert C (see §6.5 in Compcert manual https://compcert.org/man/manual005.html).

However, VST does require that there are no signed overflows so I cannot prove anything that would be correct for Compcert and not gcc. This means that VST does not exactly model Compcert C but something that is closer from Standard C.

This seems to indicate that indeed I can use gcc, but I wonder if there are other situations where things can go wrong.

Answer 1

From the CompCert manual:

A formal semantics is a mathematically-defined relation between programs and their possible behaviors. Several such semantics are defined as part of CompCert’s verification, including one for the CompCert ‍C language [...]. These semantics can be viewed as mathematically-precise renditions of (relevant parts of) the ISO ‍C ‍99 standard document. So the semantics given for Clightgen (and used in Verifiable C) corresponds to (a more precise version of) the C standard. The fact that it is more precise means that it assumes more facts than that standard, but none of them contradicts it.

This means that you can use any other C compiler instead of CompCert, with two caveats:

• Even if the compiler complies with the C standard, it might not comply with the more restrictive semantics of Clightgen. This means that gcc might introduce a behaviour that, while valid within the C standard, is invalid with respect to Clightgen’s semantic.
• As explained in that same manual page (with links to primary references), all non-verified C compilers (including gcc) have miscompilation bugs.

I think the bottom line is this: if you want to compile your verified C program with gcc, you will probably be fine, as there are no large discrepancies between Clightgen and the C standard. But if you care enough about the behaviour of said program to go all the way to verify it, using CompCert rather than gcc as a compiler is probably still a good idea, as it ensures your whole verification chain is consistent.