CompCert planned change: adding a `Mbool` memory chunk

[xavierleroy]

Just drawing your attention to an upcoming change in CompCert's memory model and C semantics: https://github.com/AbsInt/CompCert/pull/513 .

This change tightens the semantics of loading from l-values of type _Bool: the result is now Vundef if the byte read from memory is neither 0 nor 1, while it was 1 before. Maybe this will require a similar tightening of VST's "points-to" assertions for l-values of type _Bool; or maybe those assertions are already "tight enough" to guarantee that the value is 0 or 1.

Let me know if you see big problems with this change.

[andrew-appel]

Here's my "at first glance" report, which may be inaccurate. I'm looking at VST 3.0beta (which is where we should be looking in the future) but I suspect it will be the same in VST 2.x. The address_mapsto predicate at line 164 of res_predicates.v uses CompCert's decode_val in its definition, so very possibly the assertion is already "tight enough".

[xavierleroy]

Thanks for the pointers. I agree that everything defined in terms of CompCert's decode_val, encode_val, and load_result should extend automatically to the new Mbool chunks, and that the properties of the other chunks will not change.

I was more concerned about what happens at the Veri-C level. With the current CompCert, mapsto sh (Tint IBool Unsigned noattr) v1 v2 and mapsto sh (Tint I8 Unsigned noattr) v1 v2 are equivalent, since both _Bool and unsigned char types map to the Mint8unsigned chunk. With the PR proposal, they are not equivalent: "mapsto" at type _Bool implies "mapsto" at type unsigned char, not the other way around.

I think the semax_store rule remains valid with the PR proposal, and is applicable in exactly the same cases. The semax_store_union_hack rules should remain valid if the definition of decode_encode_val_ok is unchanged, or is extended with a case Mbool, Mint8unsigned => True.

But there are examples that could be proved correct with semax_store_union_hack and that can no longer be proved correct with the PR, and rightfully so because they become undefined behavior. A typical example:

unsigned char f(unsigned char x) {
    union { unsigned char c; _Bool b } u;
    u.c = x; return u.b;
}

With Veri-C and the current CompCert, I think you can prove that f(42) = 42. Once the PR is applied, this will no longer be provable, and for good reasons since f(42) becomes undefined behavior ( u.b reads as Vundef, not Vint 42).

[andrew-appel]

The original motivation for semax_store_union_hack is to access the bits of a floating-point number. If that still works, then I am not concerned about the inability to use semax_store_union_hack to convert between Bool and char.

[xavierleroy]

The change concerns exclusively the type _Bool. int/float and long/double unions will not be affected.

Feel free to close this issue, or leave it open as a reminder that VST will need updating when the change in CompCert is released.

[andrew-appel]

I am happy to report that P.R. #781 incorporates this change with no problem (and other changes to the CompCert master without much problem), so I can close this issue.

[xavierleroy]

Excellent! Thanks for the early testing. The next release of CompCert, incorporating these changes, will take place this Fall. I'm not expecting more AST changes than those you've already addressed.