diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-13 11:02:38 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-13 11:02:38 +0000 |
commit | 5c46f0c4ba077bb6e21edbc32f5f23230c45380b (patch) | |
tree | b42330865cbdebfb2c688572ff629e11f944fd8e | |
parent | 8fb2eba8404a1355d8867e0cfa0028ea941fcdaf (diff) |
More global initialization work done and proved in Coq.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1603 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | cfrontend/C2C.ml | 87 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 77 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 324 | ||||
-rw-r--r-- | driver/Compiler.v | 2 |
4 files changed, 410 insertions, 80 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index eefc813..966bb76 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -23,6 +23,7 @@ open Camlcoq open AST open Values open Csyntax +open Initializers (** Record the declarations of global variables and associate them with the corresponding atom. *) @@ -745,75 +746,33 @@ let convertFundecl env (sto, id, ty, optinit) = (** Initializers *) -let init_data_size = function - | Init_int8 _ -> 1 - | Init_int16 _ -> 2 - | Init_int32 _ -> 4 - | Init_float32 _ -> 4 - | Init_float64 _ -> 8 - | Init_addrof _ -> 4 - | Init_space _ -> assert false - let string_of_errmsg msg = let string_of_err = function | CompcertErrors.MSG s -> camlstring_of_coqstring s | CompcertErrors.CTX i -> extern_atom i in String.concat "" (List.map string_of_err msg) -let convertInit env ty init = - - let k = ref [] - and pos = ref 0 in - let emit size datum = - k := datum :: !k; - pos := !pos + size in - let emit_space size = - emit size (Init_space (z_of_camlint (Int32.of_int size))) in - let align size = - let n = !pos land (size - 1) in - if n > 0 then emit_space (size - n) in - let check_align size = - assert (!pos land (size - 1) = 0) in - - let rec cvtInit ty = function - | Init_single e -> - begin match Initializers.transl_init_single - (convertTyp env ty) (convertExpr env e) with - | CompcertErrors.OK init -> - let sz = init_data_size init in - check_align sz; - emit sz init - | CompcertErrors.Error msg -> - Format.printf "%a@." Cprint.exp (0, e); - error ("in initializing expression above: " ^ string_of_errmsg msg) - end - | Init_array il -> - let ty_elt = - match Cutil.unroll env ty with - | C.TArray(t, _, _) -> t - | _ -> error "array type expected in initializer"; C.TVoid [] in - List.iter (cvtInit ty_elt) il - | Init_struct(_, flds) -> - cvtPadToSizeof ty (fun () -> List.iter cvtFieldInit flds) - | Init_union(_, fld, i) -> - cvtPadToSizeof ty (fun () -> cvtFieldInit (fld,i)) - - and cvtFieldInit (fld, i) = - let ty' = convertTyp env fld.fld_typ in - let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in - align al; - cvtInit fld.fld_typ i - - and cvtPadToSizeof ty fn = - let ty' = convertTyp env ty in - let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in - let pos0 = !pos in - fn(); - let pos1 = !pos in - assert (pos1 <= pos0 + sz); - if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1) - - in cvtInit ty init; List.rev !k +let rec convertInit env init = + match init with + | C.Init_single e -> + Init_single (convertExpr env e) + | C.Init_array il -> + Init_compound (convertInitList env il) + | C.Init_struct(_, flds) -> + Init_compound (convertInitList env (List.map snd flds)) + | C.Init_union(_, fld, i) -> + Init_compound (Init_cons(convertInit env i, Init_nil)) + +and convertInitList env il = + match il with + | [] -> Init_nil + | i :: il' -> Init_cons(convertInit env i, convertInitList env il') + +let convertInitializer env ty i = + match Initializers.transl_init (convertTyp env ty) (convertInit env i) + with + | CompcertErrors.OK init -> init + | CompcertErrors.Error msg -> error (string_of_errmsg msg); [] (** Global variable *) @@ -840,7 +799,7 @@ let convertGlobvar env (sto, id, ty, optinit) = | None -> if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')] | Some i -> - convertInit env ty i in + convertInitializer env ty i in Hashtbl.add decl_atom id' { a_storage = sto; a_env = env; diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 926a826..5df8243 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -149,8 +149,15 @@ Fixpoint constval (a: expr) : res val := (** * Translation of initializers *) +Inductive initializer := + | Init_single (a: expr) + | Init_compound (il: initializer_list) +with initializer_list := + | Init_nil + | Init_cons (i: initializer) (il: initializer_list). + (** Translate an initializing expression [a] for a scalar variable - of type [ty]. Return the corresponding [init_data]. *) + of type [ty]. Return the corresponding initialization datum. *) Definition transl_init_single (ty: type) (a: expr) : res init_data := do v1 <- constval a; @@ -168,6 +175,70 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := | _, _ => Error (msg "type mismatch in initializer") end. -(** To come later: translation of compound initializers, currently - still done in Caml (module [C2C]). *) +(** Translate an initializer [i] for a variable of type [ty]. + Return the corresponding list of initialization data. *) + +Definition padding (frm to: Z) : list init_data := + let n := to - frm in + if zle n 0 then nil else Init_space n :: nil. + +Fixpoint transl_init (ty: type) (i: initializer) + {struct i} : res (list init_data) := + match i, ty with + | Init_single a, _ => + do d <- transl_init_single ty a; OK (d :: nil) + | Init_compound il, Tarray tyelt sz => + if zle sz 0 + then OK (Init_space(sizeof tyelt) :: nil) + else transl_init_array tyelt il sz + | Init_compound il, Tstruct _ Fnil => + OK (Init_space (sizeof ty) :: nil) + | Init_compound il, Tstruct id fl => + transl_init_struct id ty fl il 0 + | Init_compound il, Tunion _ Fnil => + OK (Init_space (sizeof ty) :: nil) + | Init_compound il, Tunion id (Fcons _ ty1 _) => + transl_init_union id ty ty1 il + | _, _ => + Error (msg "wrong type for compound initializer") + end + +with transl_init_array (ty: type) (il: initializer_list) (sz: Z) + {struct il} : res (list init_data) := + match il with + | Init_nil => + if zeq sz 0 + then OK nil + else Error (msg "wrong number of elements in array initializer") + | Init_cons i1 il' => + do d1 <- transl_init ty i1; + do d2 <- transl_init_array ty il' (sz - 1); + OK (d1 ++ d2) + end + +with transl_init_struct (id: ident) (ty: type) + (fl: fieldlist) (il: initializer_list) (pos: Z) + {struct il} : res (list init_data) := + match il, fl with + | Init_nil, Fnil => + OK (padding pos (sizeof ty)) + | Init_cons i1 il', Fcons _ ty1 fl' => + let pos1 := align pos (alignof ty1) in + do d1 <- transl_init (unroll_composite id ty ty1) i1; + do d2 <- transl_init_struct id ty fl' il' (pos1 + sizeof ty1); + OK (padding pos pos1 ++ d1 ++ d2) + | _, _ => + Error (msg "wrong number of elements in struct initializer") + end + +with transl_init_union (id: ident) (ty ty1: type) (il: initializer_list) + {struct il} : res (list init_data) := + match il with + | Init_nil => + Error (msg "empty union initializer") + | Init_cons i1 _ => + do d <- transl_init (unroll_composite id ty ty1) i1; + OK (d ++ padding (sizeof ty1) (sizeof ty)) + end. + diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index fde3c4e..2bc4b7c 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -520,36 +520,336 @@ Qed. (** * Soundness of the translation of initializers *) +(** Soundness for single initializers. *) + Theorem transl_init_single_steps: - forall ty a data f m w v1 ty1 m' v b ofs m'', + forall ty a data f m w v1 ty1 m' v chunk b ofs m'', transl_init_single ty a = OK data -> star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') -> cast v1 ty1 ty v -> - store_value_of_type ty m' b ofs v = Some m'' -> - Genv.store_init_data ge m b (Int.signed ofs) data = Some m''. + access_mode ty = By_value chunk -> + Mem.store chunk m' b ofs v = Some m'' -> + Genv.store_init_data ge m b ofs data = Some m''. Proof. intros. monadInv H. exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. exploit cast_match; eauto. intros D. - unfold Genv.store_init_data. unfold store_value_of_type in H2. simpl in H2. + unfold Genv.store_init_data. inv D. (* int *) destruct ty; try discriminate. destruct i; inv EQ2. - destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. - destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. - assumption. - inv EQ2. assumption. + destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. + destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. + simpl in H2; inv H2. assumption. + inv EQ2. simpl in H2; inv H2. assumption. (* float *) destruct ty; try discriminate. - destruct f1; inv EQ2; assumption. + destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) - assert (data = Init_addrof id ofs0 /\ access_mode ty = By_value Mint32). - destruct ty; inv EQ2; auto. destruct i; inv H4; auto. - destruct H3; subst. rewrite H4 in H2. rewrite H. assumption. + assert (data = Init_addrof id ofs0 /\ chunk = Mint32). + destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. + destruct H4; subst. rewrite H. assumption. (* undef *) discriminate. Qed. +(** Size properties for initializers. *) + +Lemma transl_init_single_size: + forall ty a data, + transl_init_single ty a = OK data -> + Genv.init_data_size data = sizeof ty. +Proof. + intros. monadInv H. destruct x0. + monadInv EQ2. + destruct ty; try discriminate. + destruct i0; inv EQ2; reflexivity. + inv EQ2; reflexivity. + destruct ty; try discriminate. + destruct f0; inv EQ2; reflexivity. + destruct b; try discriminate. + destruct ty; try discriminate. + destruct i0; inv EQ2; reflexivity. + inv EQ2; reflexivity. +Qed. + +Notation idlsize := Genv.init_data_list_size. + +Remark padding_size: + forall frm to, + frm <= to -> idlsize (padding frm to) = to - frm. +Proof. + intros. unfold padding. + destruct (zle (to - frm) 0). + simpl. omega. + simpl. rewrite Zmax_spec. rewrite zlt_true. omega. omega. +Qed. + +Remark idlsize_app: + forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2. +Proof. + induction d1; simpl; intros. + auto. + rewrite IHd1. omega. +Qed. + +Remark sizeof_struct_incr: + forall fl pos, pos <= sizeof_struct fl pos. +Proof. + induction fl; intros; simpl. + omega. + eapply Zle_trans. apply align_le with (y := alignof t). apply alignof_pos. + eapply Zle_trans. 2: apply IHfl. + generalize (sizeof_pos t); omega. +Qed. + +Remark sizeof_struct_eq: + forall id fl, + fl <> Fnil -> + sizeof (Tstruct id fl) = align (sizeof_struct fl 0) (alignof (Tstruct id fl)). +Proof. + intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. + destruct fl. congruence. simpl. + apply Zle_ge. eapply Zle_trans. 2: apply sizeof_struct_incr. + assert (0 <= align 0 (alignof t)). apply align_le. apply alignof_pos. + generalize (sizeof_pos t). omega. +Qed. + +Remark sizeof_union_eq: + forall id fl, + fl <> Fnil -> + sizeof (Tunion id fl) = align (sizeof_union fl) (alignof (Tunion id fl)). +Proof. + intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. + destruct fl. congruence. simpl. + apply Zle_ge. apply Zmax_bound_l. generalize (sizeof_pos t). omega. +Qed. + +Lemma transl_init_size: + forall i ty data, + transl_init ty i = OK data -> + idlsize data = sizeof ty + +with transl_init_list_size: + forall il, + (forall ty sz data, + transl_init_array ty il sz = OK data -> + idlsize data = sizeof ty * sz) + /\ + (forall id ty fl pos data, + transl_init_struct id ty fl il pos = OK data -> + sizeof_struct fl pos <= sizeof ty -> + idlsize data + pos = sizeof ty) + /\ + (forall id ty ty1 data, + transl_init_union id ty ty1 il = OK data -> + sizeof ty1 <= sizeof ty -> + idlsize data = sizeof ty). + +Proof. + induction i; intros. + (* single *) + monadInv H. simpl. rewrite (transl_init_single_size _ _ _ EQ). omega. + (* compound *) + simpl in H. destruct ty; try discriminate. + (* compound array *) + destruct (zle z 0). + monadInv H. simpl. repeat rewrite Zmax_spec. rewrite zlt_true. rewrite zlt_true. ring. + omega. generalize (sizeof_pos ty); omega. + simpl. rewrite Zmax_spec. rewrite zlt_false. + eapply (proj1 (transl_init_list_size il)). auto. omega. + (* compound struct *) + destruct f. + inv H. reflexivity. + replace (idlsize data) with (idlsize data + 0) by omega. + eapply (proj1 (proj2 (transl_init_list_size il))). eauto. + rewrite sizeof_struct_eq. 2: congruence. + apply align_le. apply alignof_pos. + (* compound union *) + destruct f. + inv H. reflexivity. + eapply (proj2 (proj2 (transl_init_list_size il))). eauto. + rewrite sizeof_union_eq. 2: congruence. + eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega. + apply alignof_pos. + + induction il. + (* base cases *) + simpl. intuition. + (* arrays *) + destruct (zeq sz 0); inv H. simpl. ring. + (* structs *) + destruct fl; inv H. + simpl in H0. generalize (padding_size pos (sizeof ty) H0). omega. + (* unions *) + inv H. + (* inductive cases *) + destruct IHil as [A [B C]]. split. + (* arrays *) + intros. monadInv H. + rewrite idlsize_app. + rewrite (transl_init_size _ _ _ EQ). + rewrite (A _ _ _ EQ1). + ring. + (* structs *) + split. intros. simpl in H. destruct fl; monadInv H. + repeat rewrite idlsize_app. + simpl in H0. + rewrite padding_size. + rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite. + rewrite <- (B _ _ _ _ _ EQ1). omega. + auto. apply align_le. apply alignof_pos. + (* unions *) + intros. simpl in H. monadInv H. + rewrite idlsize_app. + rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite. + rewrite padding_size. omega. auto. +Qed. + +(** A semantics for general initializers *) + +Definition dummy_function := mkfunction Tvoid nil nil Sskip. + +Require Import Events. + +Fixpoint fieldlist_map (f: type -> type) (l: fieldlist) : fieldlist := + match l with + | Fnil => Fnil + | Fcons id ty l' => Fcons id (f ty) (fieldlist_map f l') + end. + +Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := + | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'', + star step ge (ExprState dummy_function a Kstop empty_env m) + E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') -> + cast v1 ty1 ty v -> + access_mode ty = By_value chunk -> + Mem.store chunk m' b ofs v = Some m'' -> + exec_init m b ofs ty (Init_single a) m'' + | exec_init_compound_array: forall m b ofs ty sz il m', + exec_init_array m b ofs ty sz il m' -> + exec_init m b ofs (Tarray ty sz) (Init_compound il) m' + | exec_init_compound_struct: forall m b ofs id fl il m', + exec_init_struct m b ofs 0 (fieldlist_map (unroll_composite id (Tstruct id fl)) fl) il m' -> + exec_init m b ofs (Tstruct id fl) (Init_compound il) m' + | exec_init_compound_union: forall m b ofs id id1 ty1 fl i m', + exec_init m b ofs (unroll_composite id (Tunion id (Fcons id1 ty1 fl)) ty1) i m' -> + exec_init m b ofs (Tunion id (Fcons id1 ty1 fl)) (Init_compound (Init_cons i Init_nil)) m' + +with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop := + | exec_init_array_nil: forall m b ofs ty, + exec_init_array m b ofs ty 0 Init_nil m + | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'', + exec_init m b ofs ty i1 m' -> + exec_init_array m' b (ofs + sizeof ty) ty (sz - 1) il m'' -> + exec_init_array m b ofs ty sz (Init_cons i1 il) m'' + +with exec_init_struct: mem -> block -> Z -> Z -> fieldlist -> initializer_list -> mem -> Prop := + | exec_init_struct_nil: forall m b ofs pos, + exec_init_struct m b ofs pos Fnil Init_nil m + | exec_init_struct_cons: forall m b ofs pos id ty fl i1 il m' m'', + exec_init m b (ofs + align pos (alignof ty)) ty i1 m' -> + exec_init_struct m' b ofs (align pos (alignof ty) + sizeof ty) fl il m'' -> + exec_init_struct m b ofs pos (Fcons id ty fl) (Init_cons i1 il) m''. + +Scheme exec_init_ind3 := Minimality for exec_init Sort Prop + with exec_init_array_ind3 := Minimality for exec_init_array Sort Prop + with exec_init_struct_ind3 := Minimality for exec_init_struct Sort Prop. +Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_struct_ind3. + +Remark exec_init_array_length: + forall m b ofs ty sz il m', + exec_init_array m b ofs ty sz il m' -> + match il with Init_nil => sz = 0 | Init_cons _ _ => sz > 0 end. +Proof. + induction 1. auto. destruct il; omega. +Qed. + +Lemma store_init_data_list_app: + forall data1 m b ofs m' data2 m'', + Genv.store_init_data_list ge m b ofs data1 = Some m' -> + Genv.store_init_data_list ge m' b (ofs + idlsize data1) data2 = Some m'' -> + Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''. +Proof. + induction data1; simpl; intros. + inv H. rewrite Zplus_0_r in H0. auto. + destruct (Genv.store_init_data ge m b ofs a); try discriminate. + rewrite Zplus_assoc in H0. eauto. +Qed. + +Remark store_init_data_list_padding: + forall frm to b ofs m, + Genv.store_init_data_list ge m b ofs (padding frm to) = Some m. +Proof. + intros. unfold padding. destruct (zle (to - frm) 0); auto. +Qed. + +Lemma transl_init_sound_gen: + (forall m b ofs ty i m', exec_init m b ofs ty i m' -> + forall data, transl_init ty i = OK data -> + Genv.store_init_data_list ge m b ofs data = Some m') +/\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> + forall data, transl_init_array ty il sz = OK data -> + Genv.store_init_data_list ge m b ofs data = Some m') +/\(forall m b ofs pos fl il m', exec_init_struct m b ofs pos fl il m' -> + forall id ty fl' data, + fl = fieldlist_map (unroll_composite id ty) fl' -> + transl_init_struct id ty fl' il pos = OK data -> + Genv.store_init_data_list ge m b (ofs + pos) data = Some m'). +Proof. + apply exec_init_scheme; simpl; intros. + (* single *) + monadInv H3. + exploit transl_init_single_steps; eauto. intros. + simpl. rewrite H3. auto. + (* array *) + destruct (zle sz 0). + exploit exec_init_array_length; eauto. destruct il; intros. + subst. inv H. inv H1. auto. omegaContradiction. + eauto. + (* struct *) + destruct fl. + inv H. inv H1. auto. + replace ofs with (ofs + 0) by omega. eauto. + (* union *) + monadInv H1. eapply store_init_data_list_app. eauto. apply store_init_data_list_padding. + + (* array, empty *) + inv H. auto. + (* array, nonempty *) + monadInv H3. + eapply store_init_data_list_app. + eauto. + rewrite (transl_init_size _ _ _ EQ). eauto. + + (* struct, empty *) + destruct fl'; simpl in H; inv H. + inv H0. apply store_init_data_list_padding. + (* struct, nonempty *) + destruct fl'; simpl in H3; inv H3. + monadInv H4. + eapply store_init_data_list_app. apply store_init_data_list_padding. + rewrite padding_size. + replace (ofs + pos + (align pos (alignof t) - pos)) + with (ofs + align pos (alignof t)) by omega. + eapply store_init_data_list_app. + rewrite <- (alignof_unroll_composite id0 ty0 t). + eauto. + rewrite (transl_init_size _ _ _ EQ). + rewrite <- Zplus_assoc. rewrite <- (alignof_unroll_composite id0 ty0 t). + eapply H2. eauto. rewrite alignof_unroll_composite. rewrite sizeof_unroll_composite. eauto. + apply align_le. apply alignof_pos. +Qed. + +Theorem transl_init_sound: + forall m b ty i m' data, + exec_init m b 0 ty i m' -> + transl_init ty i = OK data -> + Genv.store_init_data_list ge m b 0 data = Some m'. +Proof. + intros. eapply (proj1 transl_init_sound_gen); eauto. +Qed. + End SOUNDNESS. diff --git a/driver/Compiler.v b/driver/Compiler.v index 7849d64..b0dce15 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -176,7 +176,7 @@ Definition transf_c_program (p: Csyntax.program) : res Asm.program := (** Force [Initializers] to be extracted as well. *) -Definition transl_single_init := Initializers.transl_init_single. +Definition transl_init := Initializers.transl_init. (** The following lemmas help reason over compositions of passes. *) |