Add minimal example demonstrating -fno-strict-aliasing

[andres-erbsen]

I read that VST can be used to verify an idiomatic memory allocator, so I wanted to see if it can be used to verify straightforward memory access as well. Turns out it can!

Edit: The first example goes through as expected just because clightgen interprets long as int, so it's not that interesting. The second example uses a int and void * which remain distinct throughout VST, so the proof actually argues that their memory representations are compatible.

[andrew-appel]

Can you combine the examples into a single .c file, if you really want to have two tests? Can you add a more explanatory comment at the beginning of the .c file, saying more about why this is important? And do you have a theory about why the clight version of this works consistently in all C compilers -- does it have something to do with sequence points? If so, please explain that too in the comment.

[andres-erbsen]

I think combining the files would not be great for clarity, so maybe we can just omit the first one. Is there already an example that demonstrates clightgen substantially refining the behavior of a program like with alias.c, or should we omit it regardless?

My understanding of what is going on with alias.c is that the key part is clightgen replacing long with int. This turns a program that has undefined behavior according to ISO C into a program that has the expected behavior even according to ISO C. The standard says compilers are allowed to treat int and long as equivalent, but programmers are not, even if these types have the same size.

If there is no example of clightgen doing nontrivial refinement yet but you'd prefer one where the refinement results from ordering operations that are not separated by sequence points, the following (non-ISO-C-conformant) program returns 1 with clang and gcc but 0 with ccomp and clightgen+clang/gcc. I believe the clightgen output again conforms to ISO C.

int main() {
        int x = 0;
        return (!x) - (x++);
}

As for alias2.c, the generated clight program is essentially identical to the original C program and still needs -fno-strict-aliasing to work correctly. Again, the reason is that while void* and int have the same size, ISO C assumes that accesses with different non-char types do not touch the same location in memory. This rule is controversial to say the least, and I don't want this PR to about deciding what position to take on it. This canonical example I am proposing just documents what is currently formalized.

[andrew-appel]

That's all fine, but if you would like to document this within VST more permanently, I suggest:

1. Prune the example down to one file, progs/alias.c (with progs/verif_alias.v)
2. Add a long explanatory comment (taking material from your P.R. comments above) inside alias.c, explaining what the point of all this is
3. Change this from a Draft P.R. to a regular P.R. (and, thank you)

[andres-erbsen]

Okay, I just removed the clightgen gotcha example. Feel free to squash or not during merging depending on whether it should stay in git history.

[andrew-appel]

More questions:

I presume you are testing your stuff with BITSIZE=32. Can you use size_t instead of int, therefore making your demonstration portable to BITSIZE=64 as well? (Or do I misunderstand, and the whole point is that int is not the same size as (void). In that case, you could use "short" to make sure your demonstration is portable to both sizeof(void)=4 and sizeof(void*)=8.)

Also, you say "even though int and void have size and alignment." Do you mean, "even though int and void have the same size and alignment."

And I'm still not sure what the point is. Are you trying to demonstrate that clightgen does not change any properties of the program relevant to strict aliasing, so that the input to clightgen will behave the same as the output of clightgen when compiled with -fno-strict-aliasing, and the input to clightgen will behave the same as the output of clightgen when compiled without -fno-strict-aliasing?

And finally, is VST sound if the Clight program is compiled with -fno-strict-aliasing? Is VST sound if the Clight program is compiled without -fno-strict-aliasing?

[andres-erbsen]

I changed int to long and added a 64-bit proof (long not size_t because CompCert failed to parse the stddef.h on my system). I am not sure whether clightgen can in general affect strict aliasing, but it conveniently doesn't here. For alias.c, VST is sound only if the Clight program is compiled with -fno-strict-aliasing.

[andrew-appel]

Sorry, in 64-bit C compilers, long is the same as int. If you want 64-bit integers, you have to say long long. Is that what you meant?

Also, can you add to the comment inside the .c file, the following remarks (if they are accurate): VST is proved sound only for CompCert, but VST will be "less unsound" for clang or gcc if you compile using the -fno-strict-aliasing flag to clang or gcc. CompCert does not have that option, because its only mode is no-strict-aliasing.

[andres-erbsen]

I added a comment along the lines of what you suggested. The size of long and size_t varies across ABIs for the same bitwidth, they're both 64-bit on 64-bit Linux and in the checked-in clightgen output. If you want to change it to size_t so that it gets the same size on Windows, I'd be happy with it, but I don't feel up to troubleshooting CompCert's issues with the C standard library headers on my system right now.