diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-05-17 18:07:02 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-08-22 13:29:00 +0200 |
commit | 47fae389c800034e002c9f8a398e9adc79a14b81 (patch) | |
tree | 210933a5a526afe0469a66f59861c13d687c733e /cfrontend/Ctyping.v | |
parent | a94edc576ca2c288c66f710798ab2ada3c485a40 (diff) | |
download | compcert-47fae389c800034e002c9f8a398e9adc79a14b81.tar.gz compcert-47fae389c800034e002c9f8a398e9adc79a14b81.zip |
Native support for bit fields (#400)
This big PR adds support for bit fields in structs and unions to
the verified part of CompCert, namely the CompCert C and Clight
languages.
The compilation of bit field accesses to normal integer accesses +
shifts and masks is done and proved correct as part of the Cshmgen
pass.
The layout of bit fields in memory is done by the functions in module
Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic
soundness properties of the layout are shown, such as "two different
bit fields do not overlap" or "a bit field and a regular field do not
overlap".
All this replaces the previous emulation of bit fields by
source-to-source rewriting in the unverified front-end of CompCert
(module cparse/Bitfield.ml). This emulation was prone to errors (see
nonstandard layout instead.
The core idea for the PR is that expressions in l-value position
denote not just a block, a byte offset and a type, but also a bitfield
designator saying whether all the bits of the type are accessed
(designator Full) or only some of its bits (designator
Bits). Designators of the Bits kind appear when the l-value is a bit
field access; the bit width and bit offset in Bits are computed by the
functions in Ctypes that implement the layout algorithm.
Consequently, both in the semantics of CompCert C and Clight and in
the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a
type and a bitfield designator are used in a number of places where a
single type was used before.
The introduction of bit fields has a big impact on static
initialization (module cfrontend/Initializers.v), which had to be
rewritten in large part, along with its soundness proof
(cfrontend/Initializersproof.v).
Both static initialization and run-time manipulation of bit fields are
tested in test/abi using differential testing against GCC and
randomly-generated structs.
This work exposed subtle interactions between bit fields and the
volatile modifier. Currently, the volatile modifier is ignored when
accessing a bit field (and a warning is printed at compile-time), just
like it is ignored when accessing a struct or union as a r-value.
Currently, the natural alignment of bit fields and their storage units
cannot be modified with the aligned attribute. _Alignas on bit fields
is rejected as per C11, and the packed modifier cannot be applied to a
struct containing bit fields.
Diffstat (limited to 'cfrontend/Ctyping.v')
-rw-r--r-- | cfrontend/Ctyping.v | 54 |
1 files changed, 45 insertions, 9 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 5f0a3e5b..c930a407 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -410,8 +410,8 @@ Inductive wt_rvalue : expr -> Prop := wt_rvalue (Eparen r tycast ty) with wt_lvalue : expr -> Prop := - | wt_Eloc: forall b ofs ty, - wt_lvalue (Eloc b ofs ty) + | wt_Eloc: forall b ofs bf ty, + wt_lvalue (Eloc b ofs bf ty) | wt_Evar: forall x ty, e!x = Some ty -> wt_lvalue (Evar x ty) @@ -440,7 +440,7 @@ Definition wt_expr_kind (k: kind) (a: expr) := Definition expr_kind (a: expr) : kind := match a with - | Eloc _ _ _ => LV + | Eloc _ _ _ _ => LV | Evar _ _ => LV | Ederef _ _ => LV | Efield _ _ _ => LV @@ -596,7 +596,7 @@ Fixpoint check_arguments (el: exprlist) (tyl: typelist) : res unit := Definition check_rval (e: expr) : res unit := match e with - | Eloc _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ => + | Eloc _ _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ => Error (msg "not a r-value") | _ => OK tt @@ -604,7 +604,7 @@ Definition check_rval (e: expr) : res unit := Definition check_lval (e: expr) : res unit := match e with - | Eloc _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ => + | Eloc _ _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ => OK tt | _ => Error (msg "not a l-value") @@ -846,7 +846,7 @@ Fixpoint retype_expr (ce: composite_env) (e: typenv) (a: expr) : res expr := do r1' <- retype_expr ce e r1; do rl' <- retype_exprlist ce e rl; ecall r1' rl' | Ebuiltin ef tyargs rl tyres => do rl' <- retype_exprlist ce e rl; ebuiltin ef tyargs rl' tyres - | Eloc _ _ _ => + | Eloc _ _ _ _ => Error (msg "Eloc in source") | Eparen _ _ _ => Error (msg "Eparen in source") @@ -984,6 +984,7 @@ Lemma binarith_type_cast: forall t1 t2 m t, binarith_type t1 t2 m = OK t -> wt_cast t1 t /\ wt_cast t2 t. Proof. +Local Transparent Ctypes.intsize_eq. unfold wt_cast, binarith_type, classify_binarith; intros; DestructCases; simpl; split; try congruence; try (destruct Archi.ptr64; congruence). @@ -1656,9 +1657,31 @@ Proof. unfold Mptr in *. destruct Archi.ptr64 eqn:SF; auto with ty. Qed. +Remark wt_bitfield_normalize: forall sz sg width sg1 n, + 0 < width <= bitsize_intsize sz -> + sg1 = (if zlt width (bitsize_intsize sz) then Signed else sg) -> + wt_int (bitfield_normalize sz sg width n) sz sg1. +Proof. + intros. destruct sz; cbn in *. + + destruct sg. + * replace sg1 with Signed by (destruct zlt; auto). + apply Int.sign_ext_widen; lia. + * subst sg1; destruct zlt. + ** apply Int.sign_zero_ext_widen; lia. + ** apply Int.zero_ext_widen; lia. + + destruct sg. + * replace sg1 with Signed by (destruct zlt; auto). + apply Int.sign_ext_widen; lia. + * subst sg1; destruct zlt. + ** apply Int.sign_zero_ext_widen; lia. + ** apply Int.zero_ext_widen; lia. + + auto. + + apply Int.zero_ext_widen; lia. +Qed. + Lemma wt_deref_loc: - forall ge ty m b ofs t v, - deref_loc ge ty m b ofs t v -> + forall ge ty m b ofs bf t v, + deref_loc ge ty m b ofs bf t v -> wt_val v ty. Proof. induction 1. @@ -1680,6 +1703,19 @@ Proof. destruct ty; simpl in H; try discriminate; auto with ty. destruct i; destruct s; discriminate. destruct f; discriminate. +- (* bitfield *) + inv H. constructor. + apply wt_bitfield_normalize. lia. auto. +Qed. + +Lemma wt_assign_loc: + forall ge ty m b ofs bf v t m' v', + assign_loc ge ty m b ofs bf v t m' v' -> + wt_val v ty -> wt_val v' ty. +Proof. + induction 1; intros; auto. +- inv H. constructor. + apply wt_bitfield_normalize. lia. auto. Qed. Lemma wt_cast_self: @@ -1770,7 +1806,7 @@ Proof. - (* condition *) constructor. destruct b; auto. destruct b; auto. red; auto. - (* sizeof *) unfold size_t, Vptrofs; destruct Archi.ptr64; constructor; auto with ty. - (* alignof *) unfold size_t, Vptrofs; destruct Archi.ptr64; constructor; auto with ty. -- (* assign *) inversion H5. constructor. eapply pres_sem_cast; eauto. +- (* assign *) inversion H5. constructor. eapply wt_assign_loc; eauto. eapply pres_sem_cast; eauto. - (* assignop *) subst tyres l r. constructor. auto. constructor. constructor. eapply wt_deref_loc; eauto. auto. auto. auto. |