From a3c1aed82d88df7592e63531dc8ce24482da1c28 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 17 Nov 2016 13:39:06 +0100 Subject: Initializers: introduce 'constval_cast' to cast constant value to desired type This comes handy in the next commit where constval_cast is used from C2C. --- cfrontend/Initializers.v | 10 +++++++--- cfrontend/Initializersproof.v | 36 ++++++++++++++++++------------------ 2 files changed, 25 insertions(+), 21 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 19518aea..388b6544 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -133,6 +133,11 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := Error(msg "not a compile-time constant") end. +(** [constval_cast ce a ty] evaluates [a] then converts its value to type [ty]. *) + +Definition constval_cast (ce: composite_env) (a: expr) (ty: type): res val := + do v <- constval ce a; do_cast v (typeof a) ty. + (** * Translation of initializers *) Inductive initializer := @@ -148,9 +153,8 @@ with initializer_list := of type [ty]. Return the corresponding initialization datum. *) Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data := - do v1 <- constval ce a; - do v2 <- do_cast v1 (typeof a) ty; - match v2, ty with + do v <- constval_cast ce a ty; + match v, ty with | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n) | Vint n, Tint I16 sg _ => OK(Init_int16 n) | Vint n, Tint I32 sg _ => OK(Init_int32 n) diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index fee25c48..524bc631 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -601,35 +601,35 @@ Theorem transl_init_single_steps: Mem.store chunk m' b ofs v = Some m'' -> Genv.store_init_data ge m b ofs data = Some m''. Proof. - intros. monadInv H. + intros. monadInv H. monadInv EQ. exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. exploit sem_cast_match; eauto. intros D. unfold Genv.store_init_data. inv D. - (* int *) - remember Archi.ptr64 as ptr64. destruct ty; try discriminate EQ2. -+ destruct i0; inv EQ2. + remember Archi.ptr64 as ptr64. destruct ty; try discriminate EQ0. ++ destruct i0; inv EQ0. 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. simpl in H2; inv H2. assumption. -+ destruct ptr64; inv EQ2. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption. ++ destruct ptr64; inv EQ0. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption. - (* Long *) - remember Archi.ptr64 as ptr64. destruct ty; inv EQ2. + remember Archi.ptr64 as ptr64. destruct ty; inv EQ0. + simpl in H2; inv H2. assumption. + simpl in H2; unfold Mptr in H2; destruct Archi.ptr64; inv H4. inv H2; assumption. - (* float *) destruct ty; try discriminate. - destruct f1; inv EQ2; simpl in H2; inv H2; assumption. + destruct f1; inv EQ0; simpl in H2; inv H2; assumption. - (* single *) destruct ty; try discriminate. - destruct f1; inv EQ2; simpl in H2; inv H2; assumption. + destruct f1; inv EQ0; simpl in H2; inv H2; assumption. - (* pointer *) unfold inj in H. assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr). { remember Archi.ptr64 as ptr64. - destruct ty; inversion EQ2. + destruct ty; inversion EQ0. destruct i; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto. subst ptr64. unfold Mptr. destruct Archi.ptr64; inv H5; inv H2; auto. inv H2. auto. } @@ -646,24 +646,24 @@ Lemma transl_init_single_size: transl_init_single ge ty a = OK data -> init_data_size data = sizeof ge ty. Proof. - intros. monadInv H. remember Archi.ptr64 as ptr64. destruct x0. -- monadInv EQ2. + intros. monadInv H. monadInv EQ. remember Archi.ptr64 as ptr64. destruct x. +- monadInv EQ0. - destruct ty; try discriminate. - destruct i0; inv EQ2; auto. - destruct ptr64; inv EQ2. + destruct i0; inv EQ0; auto. + destruct ptr64; inv EQ0. Local Transparent sizeof. unfold sizeof. rewrite <- Heqptr64; auto. -- destruct ty; inv EQ2; auto. +- destruct ty; inv EQ0; auto. unfold sizeof. destruct Archi.ptr64; inv H0; auto. - destruct ty; try discriminate. - destruct f0; inv EQ2; auto. + destruct f0; inv EQ0; auto. - destruct ty; try discriminate. - destruct f0; inv EQ2; auto. + destruct f0; inv EQ0; auto. - destruct ty; try discriminate. - destruct i0; inv EQ2; auto. + destruct i0; inv EQ0; auto. destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto. - destruct ptr64; inv EQ2. simpl. rewrite <- Heqptr64; auto. - inv EQ2. unfold init_data_size, sizeof. auto. + destruct ptr64; inv EQ0. simpl. rewrite <- Heqptr64; auto. + inv EQ0. unfold init_data_size, sizeof. auto. Qed. Notation idlsize := init_data_list_size. -- cgit