From 9ab3738ae87a554fb742420b8c81ced4cd3c66c7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 8 Sep 2020 13:56:01 +0200 Subject: Changed cc_varargs to an option type Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs. --- cfrontend/Ctyping.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 00fcf8ab..d9637b6a 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -170,7 +170,7 @@ Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}. Proof. decide equality. Defined. Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention := - if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then + if option_eq Z.eq_dec cc1.(cc_vararg) cc2.(cc_vararg) then OK {| cc_vararg := cc1.(cc_vararg); cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto); cc_structret := cc1.(cc_structret) |} -- cgit From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- cfrontend/Ctyping.v | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index d9637b6a..83f3cfe0 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1428,8 +1428,8 @@ Lemma pres_cast_int_int: forall sz sg n, wt_int (cast_int_int sz sg n) sz sg. Proof. intros. unfold cast_int_int. destruct sz; simpl. -- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. -- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. +- destruct sg. apply Int.sign_ext_idem; lia. apply Int.zero_ext_idem; lia. +- destruct sg. apply Int.sign_ext_idem; lia. apply Int.zero_ext_idem; lia. - auto. - destruct (Int.eq n Int.zero); auto. Qed. @@ -1616,12 +1616,12 @@ Proof. unfold access_mode, Val.load_result. remember Archi.ptr64 as ptr64. intros until v; intros AC. destruct ty; simpl in AC; try discriminate AC. - destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl. - destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega. - destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. - destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega. - destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; lia. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia. + destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; lia. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. - destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia. - inv AC. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. - destruct f; inv AC; destruct v; auto with ty. - inv AC. unfold Mptr. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. @@ -1637,16 +1637,16 @@ Proof. destruct ty; simpl in ACC; try discriminate. - destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; lia. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; lia. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; lia. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; lia. destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. destruct (proj_bytes vl); auto with ty. - constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; lia. - inv ACC. unfold decode_val. destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. - destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty. -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- cfrontend/Ctyping.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 83f3cfe0..87e3506c 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -537,9 +537,9 @@ Inductive wt_program : program -> Prop := wt_fundef p.(prog_comp_env) e fd) -> wt_program p. -Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. -Hint Extern 1 (wt_int _ _ _) => exact I: ty. -Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. +Global Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. +Global Hint Extern 1 (wt_int _ _ _) => exact I: ty. +Global Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. Ltac DestructCases := match goal with @@ -955,7 +955,7 @@ Proof. destruct (classify_bool t); congruence. Qed. -Hint Resolve check_cast_sound check_bool_sound: ty. +Global Hint Resolve check_cast_sound check_bool_sound: ty. Lemma check_arguments_sound: forall el tl x, check_arguments el tl = OK x -> wt_arguments el tl. -- cgit From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 May 2021 10:46:17 +0200 Subject: Use the LGPL instead of the GPL for dual-licensed files The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. --- cfrontend/Ctyping.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 87e3506c..5f0a3e5b 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) -- cgit From 47fae389c800034e002c9f8a398e9adc79a14b81 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 May 2021 18:07:02 +0200 Subject: 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. --- cfrontend/Ctyping.v | 54 ++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 45 insertions(+), 9 deletions(-) (limited to 'cfrontend/Ctyping.v') 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. -- cgit