1

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.

rsaill
  • 91
  • 1
  • 7

1 Answers1

2

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.

Meven Lennon-Bertrand
  • 1,251
  • 2
  • 9
  • The whole community conjectures that formal verification helps catching more bugs than careful testing. formal verification always relies on a model of the system at hand, but there is always a risk that the model is far from the reality. With VST, you are performing formal verification with a tool that is itself formally verified, so even less bugs are possible. If you compile with ComCert, the model is close to the reality, less if you compile with gcc, but there is still a benefit. – Yves Sep 29 '22 at 06:44
  • Thanks for your answer. I am indeed worried that (quoting your answer) __gcc might introduce a behaviour that, while valid within the C standard, is invalid with respect to Clightgen’s semantic.__ I edited my question to make it more precise. – rsaill Sep 30 '22 at 07:30
  • As you noticed, these difference in behaviour between gcc and Clightgen are mainly located in corner cases, typically when something is undefined behaviour according to standard C (and thus the compiler is free to do anything it wants). I’m not an expert of VST, but I would guess it prevents (most) UB by rejecting such programs, even if they have a semantic according to Clightgen. Thus, there should be very little difference between Clightgen and gcc semantics (barring bugs) on VST’s Verifiable C fragment. But as far as I know there are no formal guarantees of any kind for this… – Meven Lennon-Bertrand Sep 30 '22 at 08:48