From 0a9e21307d3abd1612bc95f9552dc2fe110742b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 23 Mar 2013 10:17:10 +0000 Subject: Watch out for behaviors exponential in the nesting of struct/union types. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Initializersproof.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index b0884ac1..75b73ff1 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -605,7 +605,8 @@ Proof. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) assert (data = Init_addrof id ofs0 /\ chunk = Mint32). - destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. + destruct ty; inv EQ2; inv H2. + destruct i; inv H5. intuition congruence. auto. destruct H4; subst. rewrite H. assumption. (* undef *) discriminate. @@ -754,13 +755,13 @@ Proof. repeat rewrite idlsize_app. simpl in H0. rewrite padding_size. - rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite. + rewrite (transl_init_size _ _ _ EQ). 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 (transl_init_size _ _ _ EQ). rewrite padding_size. omega. auto. Qed. @@ -772,8 +773,7 @@ Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list match fl with | Fnil => nil | Fcons id1 ty1 fl' => - (align pos (alignof ty1), unroll_composite id ty ty1) - :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1) + (align pos (alignof ty1), ty1) :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1) end. Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := @@ -791,7 +791,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := 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_compound il) m' | exec_init_compound_union: forall m b ofs id id1 ty1 fl a i m', - exec_init m b ofs (unroll_composite id (Tunion id (Fcons id1 ty1 fl) a) ty1) i m' -> + exec_init m b ofs ty1 i m' -> exec_init m b ofs (Tunion id (Fcons id1 ty1 fl) a) (Init_compound (Init_cons i Init_nil)) m' with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop := @@ -893,9 +893,7 @@ Proof. eapply store_init_data_list_app. eauto. rewrite (transl_init_size _ _ _ EQ). - rewrite <- Zplus_assoc. eapply H2. - rewrite sizeof_unroll_composite. eauto. - rewrite sizeof_unroll_composite. eauto. + rewrite <- Zplus_assoc. eapply H2. eauto. eauto. apply align_le. apply alignof_pos. Qed. -- cgit