From e89f1e606bc8c9c425628392adc9c69cec666b5e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 Dec 2014 19:34:45 +0100 Subject: Represent struct and union types by name instead of by structure. --- cfrontend/Initializersproof.v | 162 +++++++++++++++++++++++------------------- 1 file changed, 89 insertions(+), 73 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 73fd90b7..225dc23e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -90,13 +90,13 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop := | esl_deref: forall r ty b ofs, eval_simple_rvalue r (Vptr b ofs) -> eval_simple_lvalue (Ederef r ty) b ofs - | esl_field_struct: forall r f ty b ofs id fList a delta, + | esl_field_struct: forall r f ty b ofs id co a delta, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tstruct id fList a -> field_offset f fList = OK delta -> + typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) - | esl_field_union: forall r f ty b ofs id fList a, + | esl_field_union: forall r f ty b ofs id a, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tunion id fList a -> + typeof r = Tunion id a -> eval_simple_lvalue (Efield r f ty) b ofs with eval_simple_rvalue: expr -> val -> Prop := @@ -116,16 +116,16 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> - sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v -> + sem_binary_operation ge op v1 (typeof r1) v2 (typeof r2) m = Some v -> eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> sem_cast v1 (typeof r1) ty = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, - eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) + eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, - eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1))) + eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> eval_simple_rvalue r2 v2 -> @@ -372,13 +372,13 @@ Lemma constval_rvalue: forall m a v, eval_simple_rvalue empty_env m a v -> forall v', - constval a = OK v' -> + constval ge a = OK v' -> val_inject inj v' v with constval_lvalue: forall m a b ofs, eval_simple_lvalue empty_env m a b ofs -> forall v', - constval a = OK v' -> + constval ge a = OK v' -> val_inject inj v' (Vptr b ofs). Proof. (* rvalue *) @@ -394,7 +394,7 @@ Proof. exploit sem_unary_operation_inject. eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) - destruct (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. + destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. exploit (sem_binary_operation_inj inj Mem.empty m). intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. @@ -443,8 +443,9 @@ Proof. (* deref *) eauto. (* field struct *) - rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV. - simpl. replace x with delta by congruence. econstructor; eauto. + rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. + exploit constval_rvalue; eauto. intro MV. inv MV. + simpl. replace x0 with delta by congruence. econstructor; eauto. rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. simpl. auto. (* field union *) @@ -452,7 +453,7 @@ Proof. Qed. Lemma constval_simple: - forall a v, constval a = OK v -> simple a. + forall a v, constval ge a = OK v -> simple a. Proof. induction a; simpl; intros vx CV; try (monadInv CV); eauto. destruct (typeof a); discriminate || eauto. @@ -466,7 +467,7 @@ Qed. Theorem constval_steps: forall f r m v v' ty m', star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> - constval r = OK v -> + constval ge r = OK v -> m' = m /\ ty = typeof r /\ val_inject inj v v'. Proof. intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. @@ -479,7 +480,7 @@ Qed. Theorem transl_init_single_steps: forall ty a data f m v1 ty1 m' v chunk b ofs m'', - transl_init_single ty a = OK data -> + transl_init_single ge ty a = OK data -> star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') -> sem_cast v1 ty1 ty = Some v -> access_mode ty = By_value chunk -> @@ -522,15 +523,14 @@ Qed. Lemma transl_init_single_size: forall ty a data, - transl_init_single ty a = OK data -> - Genv.init_data_size data = sizeof ty. + transl_init_single ge ty a = OK data -> + Genv.init_data_size data = sizeof ge ty. Proof. intros. monadInv H. destruct x0. - monadInv EQ2. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. inv EQ2; auto. - inv EQ2; auto. - destruct ty; inv EQ2; auto. - destruct ty; try discriminate. destruct f0; inv EQ2; auto. @@ -539,7 +539,6 @@ Proof. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. inv EQ2; auto. - inv EQ2; auto. Qed. Notation idlsize := Genv.init_data_list_size. @@ -561,30 +560,32 @@ Proof. Qed. Remark union_field_size: - forall f ty fl, field_type f fl = OK ty -> sizeof ty <= sizeof_union fl. + forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl. Proof. - induction fl; simpl; intros. + induction fl as [|[i t]]; simpl; intros. - inv H. - destruct (ident_eq f i). + inv H. xomega. + specialize (IHfl H). xomega. Qed. +Hypothesis ce_consistent: composite_env_consistent ge. + Lemma transl_init_size: forall i ty data, - transl_init ty i = OK data -> - idlsize data = sizeof ty + transl_init ge ty i = OK data -> + idlsize data = sizeof ge 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) + transl_init_array ge ty il sz = OK data -> + idlsize data = sizeof ge 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 ty fl pos data, + transl_init_struct ge ty fl il pos = OK data -> + sizeof_struct ge pos fl <= sizeof ge ty -> + idlsize data + pos = sizeof ge ty). Proof. - induction i; intros. @@ -595,27 +596,35 @@ Proof. simpl. eapply (proj1 (transl_init_list_size il)); eauto. + (* struct *) simpl in H. destruct ty; try discriminate. + monadInv H. destruct (co_su x) eqn:?; try discriminate. replace (idlsize data) with (idlsize data + 0) by omega. eapply (proj2 (transl_init_list_size il)). eauto. -Local Opaque alignof. - simpl. apply align_le. apply alignof_pos. + unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i) as [co|] eqn:?; inv EQ. + exploit ce_consistent; eauto. intros (A & B & C). + rewrite C. unfold sizeof_composite. rewrite Heqs. apply align_le. + destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + (* union *) simpl in H. destruct ty; try discriminate. - set (sz := sizeof (Tunion i0 f0 a)) in *. - monadInv H. rewrite idlsize_app. rewrite (IHi _ _ EQ1). - rewrite padding_size. omega. unfold sz. simpl. - apply Zle_trans with (sizeof_union f0). eapply union_field_size; eauto. - apply align_le. apply alignof_pos. + monadInv H. destruct (co_su x) eqn:?; try discriminate. + monadInv EQ0. + rewrite idlsize_app. rewrite (IHi _ _ EQ0). + unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i0) as [co|] eqn:?; inv EQ. + rewrite padding_size. omega. + apply Zle_trans with (sizeof_union ge (co_members x)). + eapply union_field_size; eauto. + exploit ce_consistent; eauto. intros (A & B & C). + rewrite C. unfold sizeof_composite. rewrite Heqs. apply align_le. + destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - induction il. + (* base cases *) - simpl. intuition. + simpl. intuition auto. * (* arrays *) destruct (zeq sz 0). inv H. simpl; ring. destruct (zle 0 sz); inv H. simpl. rewrite Z.mul_comm. - assert (0 <= sizeof ty * sz). - { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ty); omega. } + assert (0 <= sizeof ge ty * sz). + { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } zify; omega. * (* structs *) destruct fl; inv H. @@ -629,12 +638,12 @@ Local Opaque alignof. rewrite (A _ _ _ EQ1). ring. * (* structs *) - intros. simpl in H. destruct fl; monadInv H. + intros. simpl in H. destruct fl as [|[i1 t1]]; monadInv H. rewrite ! idlsize_app. simpl in H0. rewrite padding_size. rewrite (transl_init_size _ _ _ EQ). - rewrite <- (B _ _ _ _ _ EQ1). omega. + rewrite <- (B _ _ _ _ EQ1). omega. auto. apply align_le. apply alignof_pos. Qed. @@ -642,11 +651,11 @@ Qed. Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip. -Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) := +Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) := match fl with - | Fnil => nil - | Fcons id1 ty1 fl' => - (align pos (alignof ty1), ty1) :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1) + | nil => nil + | (id1, ty1) :: fl' => + (align pos (alignof ge ty1), ty1) :: fields_of_struct fl' (align pos (alignof ge ty1) + sizeof ge ty1) end. Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := @@ -660,13 +669,15 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := | exec_init_array_: forall m b ofs ty sz a il m', exec_init_array m b ofs ty sz il m' -> exec_init m b ofs (Tarray ty sz a) (Init_array il) m' - | exec_init_struct: forall m b ofs id fl a il m', - exec_init_list m b ofs (fields_of_struct id (Tstruct id fl a) fl 0) il m' -> - exec_init m b ofs (Tstruct id fl a) (Init_struct il) m' - | exec_init_union: forall m b ofs id fl a f i ty m', - field_type f fl = OK ty -> + | exec_init_struct: forall m b ofs id a il co m', + ge.(genv_cenv)!id = Some co -> co_su co = Struct -> + exec_init_list m b ofs (fields_of_struct (co_members co) 0) il m' -> + exec_init m b ofs (Tstruct id a) (Init_struct il) m' + | exec_init_union: forall m b ofs id a f i ty co m', + ge.(genv_cenv)!id = Some co -> co_su co = Union -> + field_type f (co_members co) = OK ty -> exec_init m b ofs ty i m' -> - exec_init m b ofs (Tunion id fl a) (Init_union f i) m' + exec_init m b ofs (Tunion id a) (Init_union f i) m' with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop := | exec_init_array_nil: forall m b ofs ty sz, @@ -674,7 +685,7 @@ with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem exec_init_array m b ofs ty sz 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 + sizeof ge ty) ty (sz - 1) il m'' -> exec_init_array m b ofs ty sz (Init_cons i1 il) m'' with exec_init_list: mem -> block -> Z -> list (Z * type) -> initializer_list -> mem -> Prop := @@ -718,15 +729,15 @@ 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 -> + forall data, transl_init ge 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 -> + forall data, transl_init_array ge ty il sz = OK data -> Genv.store_init_data_list ge m b ofs data = Some m') /\(forall m b ofs l il m', exec_init_list m b ofs l il m' -> - forall id ty fl data pos, - l = fields_of_struct id ty fl pos -> - transl_init_struct id ty fl il pos = OK data -> + forall ty fl data pos, + l = fields_of_struct fl pos -> + transl_init_struct ge ty fl il pos = OK data -> Genv.store_init_data_list ge m b (ofs + pos) data = Some m'). Proof. Local Opaque sizeof. @@ -737,9 +748,11 @@ Local Opaque sizeof. replace (Z.max 0 sz) with sz in H1. eauto. assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. - (* struct *) + unfold lookup_composite in H3. rewrite H in H3. simpl in H3. rewrite H0 in H3. replace ofs with (ofs + 0) by omega. eauto. - (* union *) - rewrite H in H2. monadInv H2. inv EQ. + unfold lookup_composite in H4. rewrite H in H4. simpl in H4. rewrite H0 in H4. + monadInv H4. assert (x = ty) by congruence. subst x. eapply store_init_data_list_app. eauto. apply store_init_data_list_padding. @@ -753,15 +766,15 @@ Local Opaque sizeof. eauto. rewrite (transl_init_size _ _ _ EQ). eauto. - (* struct, empty *) - destruct fl; simpl in H; inv H. - inv H0. apply store_init_data_list_padding. + destruct fl as [|[i t]]; simpl in H0; inv H0. + apply store_init_data_list_padding. - (* struct, nonempty *) - destruct fl; simpl in H3; inv H3. - monadInv H4. + destruct fl as [|[i t]]; simpl in H4; monadInv H4. + simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. rewrite padding_size. - replace (ofs + pos0 + (align pos0 (alignof t) - pos0)) - with (ofs + align pos0 (alignof t)) by omega. + replace (ofs + pos0 + (align pos0 (alignof ge t) - pos0)) + with (ofs + align pos0 (alignof ge t)) by omega. eapply store_init_data_list_app. eauto. rewrite (transl_init_size _ _ _ EQ). @@ -769,15 +782,18 @@ Local Opaque sizeof. apply align_le. apply alignof_pos. Qed. +End SOUNDNESS. + 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'. + forall p m b ty i m' data, + exec_init (globalenv p) m b 0 ty i m' -> + transl_init (prog_comp_env p) ty i = OK data -> + Genv.store_init_data_list (globalenv p) m b 0 data = Some m'. Proof. - intros. eapply (proj1 transl_init_sound_gen); eauto. + intros. + set (ge := globalenv p) in *. + change (prog_comp_env p) with (genv_cenv ge) in H0. + destruct (transl_init_sound_gen ge) as (A & B & C). + eapply build_composite_env_consistent. apply prog_comp_env_eq. + eapply A; eauto. Qed. - -End SOUNDNESS. - - -- cgit