Unexpected undefined behavior on IA32 ?

[boulme]

On architecture IA32, ./ccomp -interp on the following program printfs ERROR: Initial state undefined (just tested on commit ce0f6ca).

typedef struct {
     char is_float;
     union {
       long long i;
       double f;
     } u;
  } number;

number x={.is_float=0, .u={.i=42}};
number y;

int main(){
  y.u = x.u;
  return y.u.i;
}

I guess that there is no such UB in this program. For example, on x86_64, ./ccomp -interp prints Time 22: program terminated (exit code = 42).

I understand that this issue is related to Csem.assign_loc_copy for assignment y.u = x.u. Formal semantics requires offset to be aligned on Ctypes.alignof_blockcopy. But the trusted frontend (i.e. C2C) aligns global variables on Ctypes.alignof.

And on IA32 architecture (only), alignof_blockcopy may not divide Ctypes.alignof, even on naturally_aligned types, in particular for Tlong and for Tfloat F64.

Thus, a simple fix, would be to define

Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
  match t with
  | Tlong _ _ => Archi.align_int64
  | Tfloat F64 _ => Archi.align_float64
  | ... => (* same as before *)
  end.

[boulme]

Note that I came to imagine this bug, after seeing that the following proof only fails for IA32.

Lemma alignof_alignof_blockcopy_compat:
  forall env ty, naturally_aligned ty -> (alignof_blockcopy env ty | alignof env ty).
Proof.
  intros env ty ACCESS.
  assert (X: forall co, (Z.min 8 (co_alignof co) | co_alignof co)).
  {
    intros.
    destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ.
    destruct n. apply Z.divide_refl.
    destruct n. apply Z.divide_refl.
    destruct n. apply Z.divide_refl.
    apply Z.min_case.
    exists (two_p (Z.of_nat n)).
    change 8 with (two_p 3).
    rewrite <- two_p_is_exp by lia.
    rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. lia.
    apply Z.divide_refl.
  }
  revert ACCESS; induction ty; cbn; intuition (auto with zarith);
  (destruct a; cbn in *; subst; auto with zarith);
  (destruct (env!i); cbn; auto with zarith).
Qed.

I suggest that this lemma would help for arguing that global variable alignment set by C2C are compatible with requirements of Csem.assign_loc_copy. Indeed, C standard requires that alignment directives (aka _Alignas) do not weaken natural alignment, as checked by ccomp -Wreduced-alignment.

[xavierleroy]

Thanks for the report. You're right that align_blockcopy is inconsistent with the reduced alignments for int64 and double of the IA32 ABI. In old versions of CompCert, int64 and double had alignment 8 on all platforms, so this inconsistency may have happened when the reduced IA32 alignments were introduced but not consistently everywhere. I'm testing the obvious fix right now and everything seems to work fine.

[xavierleroy]

However, the "Initial state undefined" error is unrelated to align_blockcopy and is due to Memdata.align_chunk returning 8 for 64-bit integers. There was a reason for this choice, and the incompatibility with the x86-32 ABI was noted at that time, but I'm not sure the reason is still relevant. Let me dig a bit of history to see what has been tried already.

[xavierleroy]

It turns out that the CompCert memory model requires 64-bit integer accesses to be 8-aligned, otherwise they could not be reliably turned into two 32-bit integer accesses (see e.g. Memory.load_int64_split). With 4-alignment, one could load a 64-bit integer at offset 2^32-4, accessing bytes at offsets 2^32-4 to 2^32+3, but two 32-bit loads would access bytes 2^32-4...2^32-1 and 0...3.

So, the 4-alignment mandated by the x86-32 ABI produces struct layouts that may not be semantically defined in CompCert C or the other CompCert languages. I don't think there's anything we can do about this, except to consider removing x86-32 support from CompCert entirely. This target platform is no longer relevant now that x86-64 is ubiquitous and well supported by CompCert.