diff options
Diffstat (limited to 'cfrontend/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 1199 |
1 files changed, 827 insertions, 372 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 272b929f..00f7e331 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -12,7 +12,7 @@ (** Compile-time evaluation of initializers for global C variables. *) -Require Import Coqlib Maps. +Require Import Zwf Coqlib Maps. Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep. Require Import Ctypes Cop Csyntax Csem. Require Import Initializers. @@ -30,7 +30,7 @@ Variable ge: genv. Fixpoint simple (a: expr) : Prop := match a with - | Eloc _ _ _ => True + | Eloc _ _ _ _ => True | Evar _ _ => True | Ederef r _ => simple r | Efield l1 _ _ => simple l1 @@ -65,38 +65,38 @@ Section SIMPLE_EXPRS. Variable e: env. Variable m: mem. -Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop := - | esl_loc: forall b ofs ty, - eval_simple_lvalue (Eloc b ofs ty) b ofs +Inductive eval_simple_lvalue: expr -> block -> ptrofs -> bitfield -> Prop := + | esl_loc: forall b ofs bf ty, + eval_simple_lvalue (Eloc b ofs bf ty) b ofs bf | esl_var_local: forall x ty b, e!x = Some(b, ty) -> - eval_simple_lvalue (Evar x ty) b Ptrofs.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero Full | esl_var_global: forall x ty b, e!x = None -> Genv.find_symbol ge x = Some b -> - eval_simple_lvalue (Evar x ty) b Ptrofs.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero Full | 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 co a delta, + eval_simple_lvalue (Ederef r ty) b ofs Full + | esl_field_struct: forall r f ty b ofs id co a delta bf, eval_simple_rvalue r (Vptr b ofs) -> - 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 (Ptrofs.add ofs (Ptrofs.repr delta)) - | esl_field_union: forall r f ty b ofs id a, + typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK (delta, bf) -> + eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) bf + | esl_field_union: forall r f ty b ofs id co a delta bf, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tunion id a -> - eval_simple_lvalue (Efield r f ty) b ofs + typeof r = Tunion id a -> ge.(genv_cenv)!id = Some co -> union_field_offset ge f (co_members co) = OK (delta, bf) -> + eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) bf with eval_simple_rvalue: expr -> val -> Prop := | esr_val: forall v ty, eval_simple_rvalue (Eval v ty) v - | esr_rvalof: forall b ofs l ty v, - eval_simple_lvalue l b ofs -> + | esr_rvalof: forall b ofs bf l ty v, + eval_simple_lvalue l b ofs bf -> ty = typeof l -> - deref_loc ge ty m b ofs E0 v -> + deref_loc ge ty m b ofs bf E0 v -> eval_simple_rvalue (Evalof l ty) v | esr_addrof: forall b ofs l ty, - eval_simple_lvalue l b ofs -> + eval_simple_lvalue l b ofs Full -> eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> @@ -153,7 +153,7 @@ End SIMPLE_EXPRS. Definition compat_eval (k: kind) (e: env) (a a': expr) (m: mem) : Prop := typeof a = typeof a' /\ match k with - | LV => forall b ofs, eval_simple_lvalue e m a' b ofs -> eval_simple_lvalue e m a b ofs + | LV => forall b ofs bf, eval_simple_lvalue e m a' b ofs bf -> eval_simple_lvalue e m a b ofs bf | RV => forall v, eval_simple_rvalue e m a' v -> eval_simple_rvalue e m a v end. @@ -167,7 +167,7 @@ Lemma lred_compat: forall e l m l' m', lred ge e l m l' m' -> m = m' /\ compat_eval LV e l l' m. Proof. - induction 1; simpl; split; auto; split; auto; intros bx ofsx EV; inv EV. + induction 1; simpl; split; auto; split; auto; intros bx ofsx bf' EV; inv EV. apply esl_var_local; auto. apply esl_var_global; auto. constructor. constructor. @@ -365,6 +365,22 @@ Proof. intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. Qed. +Lemma add_offset_match: + forall v b ofs delta, + Val.inject inj v (Vptr b ofs) -> + Val.inject inj + (if Archi.ptr64 + then Val.addl v (Vlong (Int64.repr delta)) + else Val.add v (Vint (Int.repr delta))) + (Vptr b (Ptrofs.add ofs (Ptrofs.repr delta))). +Proof. + intros. inv H. +- rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut (Ptrofs.repr delta0)). + unfold Val.addl, Val.add; destruct Archi.ptr64 eqn:SF; + econstructor; eauto; rewrite ! Ptrofs.add_assoc; f_equal; f_equal; symmetry; auto with ptrofs. +- unfold Val.addl, Val.add; destruct Archi.ptr64; auto. +Qed. + (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -374,20 +390,22 @@ Lemma constval_rvalue: 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 m a b ofs bf, + eval_simple_lvalue empty_env m a b ofs bf -> forall v', constval ge a = OK v' -> - Val.inject inj v' (Vptr b ofs). + bf = Full /\ Val.inject inj v' (Vptr b ofs). Proof. (* rvalue *) induction 1; intros vres CV; simpl in CV; try (monadInv CV). (* val *) destruct v; monadInv CV; constructor. (* rval *) - inv H1; rewrite H2 in CV; try congruence. eauto. eauto. + assert (constval ge l = OK vres) by (destruct (access_mode ty); congruence). + exploit constval_lvalue; eauto. intros [A B]. subst bf. + inv H1; rewrite H3 in CV; congruence. (* addrof *) - eauto. + eapply constval_lvalue; eauto. (* unop *) destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0. exploit (sem_unary_operation_inj inj Mem.empty m). @@ -438,28 +456,31 @@ Proof. (* lvalue *) induction 1; intros v' CV; simpl in CV; try (monadInv CV). (* var local *) - unfold empty_env in H. rewrite PTree.gempty in H. congruence. + split; auto. unfold empty_env in H. rewrite PTree.gempty in H. congruence. (* var_global *) - econstructor. unfold inj. rewrite H0. eauto. auto. + split; auto. econstructor. unfold inj. rewrite H0. eauto. auto. (* deref *) - eauto. + split; eauto. (* field struct *) - 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. - replace x0 with delta by congruence. rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut (Ptrofs.repr delta0)). - simpl; destruct Archi.ptr64 eqn:SF; - econstructor; eauto; rewrite ! Ptrofs.add_assoc; f_equal; f_equal; symmetry; auto with ptrofs. - destruct Archi.ptr64; auto. + rewrite H0 in EQ. monadInv EQ. destruct x0; monadInv EQ2. + unfold lookup_composite in EQ0; rewrite H1 in EQ0; monadInv EQ0. + exploit constval_rvalue; eauto. intro MV. + split. congruence. + replace x with delta by congruence. + apply (add_offset_match _ _ _ _ MV). (* field union *) - rewrite H0 in CV. eauto. + rewrite H0 in EQ. monadInv EQ. destruct x0; monadInv EQ2. + unfold lookup_composite in EQ0; rewrite H1 in EQ0; monadInv EQ0. + exploit constval_rvalue; eauto. intro MV. + split. congruence. + replace x with delta by congruence. + apply (add_offset_match _ _ _ _ MV). Qed. Lemma constval_simple: 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. - monadInv CV. eauto. destruct (access_mode ty); discriminate || eauto. intuition eauto. Qed. @@ -476,420 +497,854 @@ Proof. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. Qed. -(** * Relational specification of the translation of initializers *) - -Definition tr_padding (frm to: Z) : list init_data := - if zlt frm to then Init_space (to - frm) :: nil else nil. - -Inductive tr_init: type -> initializer -> list init_data -> Prop := - | tr_init_sgl: forall ty a d, - transl_init_single ge ty a = OK d -> - tr_init ty (Init_single a) (d :: nil) - | tr_init_arr: forall tyelt nelt attr il d, - tr_init_array tyelt il (Z.max 0 nelt) d -> - tr_init (Tarray tyelt nelt attr) (Init_array il) d - | tr_init_str: forall id attr il co d, - lookup_composite ge id = OK co -> co_su co = Struct -> - tr_init_struct (Tstruct id attr) (co_members co) il 0 d -> - tr_init (Tstruct id attr) (Init_struct il) d - | tr_init_uni: forall id attr f i1 co ty1 d, - lookup_composite ge id = OK co -> co_su co = Union -> field_type f (co_members co) = OK ty1 -> - tr_init ty1 i1 d -> - tr_init (Tunion id attr) (Init_union f i1) - (d ++ tr_padding (sizeof ge ty1) (sizeof ge (Tunion id attr))) - -with tr_init_array: type -> initializer_list -> Z -> list init_data -> Prop := - | tr_init_array_nil_0: forall ty, - tr_init_array ty Init_nil 0 nil - | tr_init_array_nil_pos: forall ty sz, - 0 < sz -> - tr_init_array ty Init_nil sz (Init_space (sz * sizeof ge ty) :: nil) - | tr_init_array_cons: forall ty i il sz d1 d2, - tr_init ty i d1 -> tr_init_array ty il (sz - 1) d2 -> - tr_init_array ty (Init_cons i il) sz (d1 ++ d2) - -with tr_init_struct: type -> members -> initializer_list -> Z -> list init_data -> Prop := - | tr_init_struct_nil: forall ty pos, - tr_init_struct ty nil Init_nil pos (tr_padding pos (sizeof ge ty)) - | tr_init_struct_cons: forall ty f1 ty1 fl i1 il pos d1 d2, - let pos1 := align pos (alignof ge ty1) in - tr_init ty1 i1 d1 -> - tr_init_struct ty fl il (pos1 + sizeof ge ty1) d2 -> - tr_init_struct ty ((f1, ty1) :: fl) (Init_cons i1 il) - pos (tr_padding pos pos1 ++ d1 ++ d2). - -Lemma transl_padding_spec: - forall frm to k, padding frm to k = rev (tr_padding frm to) ++ k. -Proof. - unfold padding, tr_padding; intros. - destruct (zlt frm to); auto. -Qed. - -Lemma transl_init_rec_spec: - forall i ty k res, - transl_init_rec ge ty i k = OK res -> - exists d, tr_init ty i d /\ res = rev d ++ k - -with transl_init_array_spec: - forall il ty sz k res, - transl_init_array ge ty il sz k = OK res -> - exists d, tr_init_array ty il sz d /\ res = rev d ++ k - -with transl_init_struct_spec: - forall il ty fl pos k res, - transl_init_struct ge ty fl il pos k = OK res -> - exists d, tr_init_struct ty fl il pos d /\ res = rev d ++ k. - -Proof. -Local Opaque sizeof. -- destruct i; intros until res; intros TR; simpl in TR. -+ monadInv TR. exists (x :: nil); split; auto. constructor; auto. -+ destruct ty; try discriminate. - destruct (transl_init_array_spec _ _ _ _ _ TR) as (d & A & B). - exists d; split; auto. constructor; auto. -+ destruct ty; try discriminate. monadInv TR. destruct (co_su x) eqn:SU; try discriminate. - destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d & A & B). - exists d; split; auto. econstructor; eauto. -+ destruct ty; try discriminate. - monadInv TR. destruct (co_su x) eqn:SU; monadInv EQ0. - destruct (transl_init_rec_spec _ _ _ _ EQ0) as (d & A & B). - exists (d ++ tr_padding (sizeof ge x0) (sizeof ge (Tunion i0 a))); split. - econstructor; eauto. - rewrite rev_app_distr, app_ass, B. apply transl_padding_spec. - -- destruct il; intros until res; intros TR; simpl in TR. -+ destruct (zeq sz 0). - inv TR. exists (@nil init_data); split; auto. constructor. - destruct (zle 0 sz). - inv TR. econstructor; split. constructor. omega. auto. - discriminate. -+ monadInv TR. - destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). - destruct (transl_init_array_spec _ _ _ _ _ EQ0) as (d2 & A2 & B2). - exists (d1 ++ d2); split. econstructor; eauto. - subst res x. rewrite rev_app_distr, app_ass. auto. +(** * Correctness of operations over the initialization state *) + +(** ** Properties of the in-memory bytes denoted by initialization data *) + +Local Notation boid := (Genv.bytes_of_init_data (genv_genv ge)). +Local Notation boidl := (Genv.bytes_of_init_data_list (genv_genv ge)). + +Lemma boidl_app: forall il2 il1, + boidl (il1 ++ il2) = boidl il1 ++ boidl il2. +Proof. + induction il1 as [ | il il1]; simpl. auto. rewrite app_ass. f_equal; auto. +Qed. + +Corollary boidl_rev_cons: forall i il, + boidl (rev il ++ i :: nil) = boidl (rev il) ++ boid i. +Proof. + intros. rewrite boidl_app. simpl. rewrite <- app_nil_end. auto. +Qed. + +Definition byte_of_int (n: int) := Byte.repr (Int.unsigned n). + +Lemma byte_of_int_of_byte: forall b, byte_of_int (int_of_byte b) = b. +Proof. + intros. unfold int_of_byte, byte_of_int. + rewrite Int.unsigned_repr, Byte.repr_unsigned. auto. + assert(Byte.max_unsigned < Int.max_unsigned) by reflexivity. + generalize (Byte.unsigned_range_2 b). lia. +Qed. + +Lemma inj_bytes_1: forall n, + inj_bytes (encode_int 1 n) = Byte (Byte.repr n) :: nil. +Proof. + intros. unfold encode_int, bytes_of_int, rev_if_be. destruct Archi.big_endian; auto. +Qed. + +Lemma inj_bytes_byte: forall b, + inj_bytes (encode_int 1 (Int.unsigned (int_of_byte b))) = Byte b :: nil. +Proof. + intros. rewrite inj_bytes_1. do 2 f_equal. apply byte_of_int_of_byte. +Qed. + +Lemma boidl_init_ints8: forall l, + boidl (map Init_int8 l) = inj_bytes (map byte_of_int l). +Proof. + induction l as [ | i l]; simpl. auto. rewrite inj_bytes_1; simpl. f_equal; auto. +Qed. + +Lemma boidl_init_bytes: forall l, + boidl (map Init_byte l) = inj_bytes l. +Proof. + induction l as [ | b l]; simpl. auto. rewrite inj_bytes_byte, IHl. auto. +Qed. + +Lemma boidl_ints8: forall i n, + boidl (repeat (Init_int8 i) n) = repeat (Byte (byte_of_int i)) n. +Proof. + induction n; simpl. auto. rewrite inj_bytes_1. simpl; f_equal; auto. +Qed. + +(** ** Properties of operations over list of initialization data *) + +Lemma add_rev_bytes_spec: forall l il, + add_rev_bytes l il = List.map Init_byte (List.rev l) ++ il. +Proof. + induction l as [ | b l]; intros; simpl. +- auto. +- rewrite IHl. rewrite map_app. simpl. rewrite app_ass. auto. +Qed. + +Lemma add_rev_bytes_spec': forall l il, + List.rev (add_rev_bytes l il) = List.rev il ++ List.map Init_byte l. +Proof. + intros. rewrite add_rev_bytes_spec. rewrite rev_app_distr, map_rev, rev_involutive. auto. +Qed. + +Lemma add_zeros_spec: forall n il, + 0 <= n -> + add_zeros n il = List.repeat (Init_int8 Int.zero) (Z.to_nat n) ++ il. +Proof. + intros. + unfold add_zeros; rewrite iter_nat_of_Z by auto; rewrite Zabs2Nat.abs_nat_nonneg by auto. + induction (Z.to_nat n); simpl. auto. f_equal; auto. +Qed. + +Lemma decompose_spec: forall il depth bl il', + decompose il depth = OK (bl, il') -> + exists nl, il = List.map Init_int8 nl ++ il' + /\ bl = List.map byte_of_int (rev nl) + /\ List.length nl = Z.to_nat depth. +Proof. + assert (REC: forall il accu depth bl il', + decompose_rec accu il depth = OK (bl, il') -> + exists nl, il = List.map Init_int8 nl ++ il' + /\ bl = List.map byte_of_int (rev nl) ++ accu + /\ List.length nl = Z.to_nat depth). + { induction il as [ | i il ]; intros until il'; intros D; simpl in D. + - destruct (zle depth 0); inv D. + exists (@nil int); simpl. rewrite Z_to_nat_neg by auto. auto. + - destruct (zle depth 0). + + inv D. exists (@nil int); simpl. rewrite Z_to_nat_neg by auto. auto. + + destruct i; try discriminate. + apply IHil in D; destruct D as (nl & P & Q & R). + exists (i :: nl); simpl; split. congruence. split. + rewrite map_app. simpl. rewrite app_ass. exact Q. + rewrite R, <- Z2Nat.inj_succ by lia. f_equal; lia. + } + intros. apply REC in H. destruct H as (nl & P & Q & R). rewrite app_nil_r in Q. + exists nl; auto. +Qed. + +Lemma list_repeat_app: forall (A: Type) (a: A) n2 n1, + List.repeat a n1 ++ List.repeat a n2 = List.repeat a (n1 + n2)%nat. +Proof. + induction n1; simpl; congruence. +Qed. + +Lemma list_rev_repeat: forall (A: Type) (a: A) n, + rev (List.repeat a n) = List.repeat a n. +Proof. + induction n; simpl. auto. rewrite IHn. change (a :: nil) with (repeat a 1%nat). + rewrite list_repeat_app. rewrite Nat.add_comm. auto. +Qed. + +Lemma normalize_boidl: forall il depth il', + normalize il depth = OK il' -> + boidl (rev il') = boidl (rev il). +Proof. + induction il as [ | i il]; simpl; intros depth il' AT. +- destruct (zle depth 0); inv AT. auto. +- destruct (zle depth 0). inv AT. auto. + destruct i; + try (monadInv AT; simpl; + rewrite ? add_rev_bytes_spec', ? boidl_rev_cons, ? boidl_app, ? boidl_init_bytes; + erewrite IHil by eauto; reflexivity). + set (n := Z.max 0 z) in *. destruct (zle n depth); monadInv AT. + + rewrite add_zeros_spec, rev_app_distr, ! boidl_app by lia. + erewrite IHil by eauto. f_equal. + rewrite list_rev_repeat. simpl. rewrite app_nil_r, boidl_ints8. + f_equal. unfold n. apply Z.max_case_strong; intros; auto. rewrite ! Z_to_nat_neg by lia. auto. + + rewrite add_zeros_spec, rev_app_distr, !boidl_app by lia. + simpl. rewrite boidl_rev_cons, list_rev_repeat. simpl. + rewrite app_ass, app_nil_r, !boidl_ints8. f_equal. + rewrite list_repeat_app. f_equal. rewrite <- Z2Nat.inj_add by lia. + unfold n. apply Z.max_case_strong; intros; f_equal; lia. +Qed. + +Lemma trisection_boidl: forall il depth sz bytes1 bytes2 il', + trisection il depth sz = OK (bytes1, bytes2, il') -> + boidl (rev il) = boidl (rev il') ++ inj_bytes bytes2 ++ inj_bytes bytes1 + /\ length bytes1 = Z.to_nat depth + /\ length bytes2 = Z.to_nat sz. +Proof. + unfold trisection; intros. monadInv H. + apply normalize_boidl in EQ. rewrite <- EQ. + apply decompose_spec in EQ1. destruct EQ1 as (nl1 & A1 & B1 & C1). + apply decompose_spec in EQ0. destruct EQ0 as (nl2 & A2 & B2 & C2). + split. +- rewrite A1, A2, !rev_app_distr, !boidl_app, app_ass. + rewrite <- !map_rev, !boidl_init_ints8. rewrite <- B1, <- B2. auto. +- rewrite B1, B2, !map_length, !rev_length. auto. +Qed. + +Lemma store_init_data_loadbytes: + forall m b p i m', + Genv.store_init_data ge m b p i = Some m' -> + match i with Init_space _ => False | _ => True end -> + Mem.loadbytes m' b p (init_data_size i) = Some (boid i). +Proof. + intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). +- contradiction. +- rewrite Genv.init_data_size_addrof. simpl. + destruct (Genv.find_symbol ge i) as [b'|]; try discriminate. + rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H). + unfold encode_val, Mptr; destruct Archi.ptr64; reflexivity. +Qed. + +(** ** Validity and size of initialization data *) + +Definition idvalid (i: init_data) : Prop := + match i with + | Init_addrof symb ofs => exists b, Genv.find_symbol ge symb = Some b + | _ => True + end. + +Fixpoint idlvalid (p: Z) (il: list init_data) {struct il} : Prop := + match il with + | nil => True + | i1 :: il => + (Genv.init_data_alignment i1 | p) + /\ idvalid i1 + /\ idlvalid (p + init_data_size i1) il + end. + +Lemma idlvalid_app: forall l2 l1 pos, + idlvalid pos (l1 ++ l2) <-> idlvalid pos l1 /\ idlvalid (pos + init_data_list_size l1) l2. +Proof. + induction l1 as [ | d l1]; intros; simpl. +- rewrite Z.add_0_r; tauto. +- rewrite IHl1. rewrite Z.add_assoc. tauto. +Qed. + +Lemma add_rev_bytes_valid: forall il bl, + idlvalid 0 (rev il) -> idlvalid 0 (rev (add_rev_bytes bl il)). +Proof. + intros. rewrite add_rev_bytes_spec, rev_app_distr, idlvalid_app. split; auto. + generalize (rev bl) (0 + init_data_list_size (rev il)). induction l; simpl; intros. + auto. + rewrite idlvalid_app; split; auto. simpl. auto using Z.divide_1_l. +Qed. + +Lemma add_zeros_valid: forall il n, + 0 <= n -> idlvalid 0 (rev il) -> idlvalid 0 (rev (add_zeros n il)). +Proof. + intros. rewrite add_zeros_spec, rev_app_distr, idlvalid_app by auto. + split; auto. + generalize (Z.to_nat n) (0 + init_data_list_size (rev il)). induction n0; simpl; intros. + auto. + rewrite idlvalid_app; split; auto. simpl. auto using Z.divide_1_l. +Qed. -- destruct il; intros until res; intros TR; simpl in TR. -+ destruct fl; inv TR. econstructor; split. constructor. apply transl_padding_spec. -+ destruct fl as [ | [f1 ty1] fl ]; monadInv TR. - destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). - destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d2 & A2 & B2). - exists (tr_padding pos (align pos (alignof ge ty1)) ++ d1 ++ d2); split. - econstructor; eauto. - rewrite ! rev_app_distr. subst res x. rewrite ! app_ass. rewrite transl_padding_spec. auto. +Lemma normalize_valid: forall il depth il', + normalize il depth = OK il' -> idlvalid 0 (rev il) -> idlvalid 0 (rev il'). +Proof. + induction il as [ | i il]; simpl; intros. +- destruct (zle depth 0); inv H. simpl. tauto. +- destruct (zle depth 0). inv H. auto. + rewrite idlvalid_app in H0; destruct H0. + destruct i; try (monadInv H; apply add_rev_bytes_valid; eapply IHil; eauto). + + monadInv H. simpl. rewrite idlvalid_app; split. eauto. simpl; auto using Z.divide_1_l. + + destruct (zle (Z.max 0 z)); monadInv H. + * apply add_zeros_valid. lia. eauto. + * apply add_zeros_valid. lia. simpl. rewrite idlvalid_app; split. auto. simpl; auto using Z.divide_1_l. Qed. -Theorem transl_init_spec: - forall ty i d, transl_init ge ty i = OK d -> tr_init ty i d. +Lemma trisection_valid: forall il depth sz bytes1 bytes2 il', + trisection il depth sz = OK (bytes1, bytes2, il') -> + idlvalid 0 (rev il) -> + idlvalid 0 (rev il'). Proof. - unfold transl_init; intros. monadInv H. - exploit transl_init_rec_spec; eauto. intros (d & A & B). - subst x. unfold rev'; rewrite <- rev_alt. - rewrite rev_app_distr; simpl. rewrite rev_involutive. auto. + unfold trisection; intros. monadInv H. + apply decompose_spec in EQ1. destruct EQ1 as (nl1 & A1 & B1 & C1). + apply decompose_spec in EQ0. destruct EQ0 as (nl2 & A2 & B2 & C2). + exploit normalize_valid; eauto. rewrite A1, A2, !rev_app_distr, !idlvalid_app. + tauto. +Qed. + +Lemma init_data_size_boid: forall i, + init_data_size i = Z.of_nat (length (boid i)). +Proof. + intros. destruct i; simpl; rewrite ?length_inj_bytes, ?encode_int_length; auto. +- rewrite repeat_length. rewrite Z_to_nat_max; auto. +- destruct (Genv.find_symbol ge i), Archi.ptr64; reflexivity. +Qed. + +Lemma init_data_list_size_boidl: forall il, + init_data_list_size il = Z.of_nat (length (boidl il)). +Proof. + induction il as [ | i il]; simpl. auto. + rewrite app_length, init_data_size_boid. lia. +Qed. + +Lemma init_data_list_size_app: forall l1 l2, + init_data_list_size (l1 ++ l2) = init_data_list_size l1 + init_data_list_size l2. +Proof. + induction l1 as [ | i l1]; intros; simpl. auto. rewrite IHl1; lia. +Qed. + +(** ** Memory areas that are initialized to zeros *) + +Definition reads_as_zeros (m: mem) (b: block) (from to: Z) : Prop := + forall i, from <= i < to -> Mem.loadbytes m b i 1 = Some (Byte Byte.zero :: nil). + +Lemma reads_as_zeros_mono: forall m b from1 from2 to1 to2, + reads_as_zeros m b from1 to1 -> from1 <= from2 -> to2 <= to1 -> + reads_as_zeros m b from2 to2. +Proof. + intros; red; intros. apply H; lia. +Qed. + +Remark reads_as_zeros_unchanged: + forall (P: block -> Z -> Prop) m b from to m', + reads_as_zeros m b from to -> + Mem.unchanged_on P m m' -> + (forall i, from <= i < to -> P b i) -> + reads_as_zeros m' b from to. +Proof. + intros; red; intros. eapply Mem.loadbytes_unchanged_on; eauto. + intros; apply H1. lia. +Qed. + +Lemma reads_as_zeros_loadbytes: forall m b from to, + reads_as_zeros m b from to -> + forall len pos, from <= pos -> pos + len <= to -> 0 <= len -> + Mem.loadbytes m b pos len = Some (repeat (Byte Byte.zero) (Z.to_nat len)). +Proof. + intros until to; intros RZ. + induction len using (well_founded_induction (Zwf_well_founded 0)). + intros. destruct (zeq len 0). +- subst len. rewrite Mem.loadbytes_empty by lia. auto. +- replace (Z.to_nat len) with (S (Z.to_nat (len - 1))). + change (repeat (Byte Byte.zero) (S (Z.to_nat (len - 1)))) + with ((Byte Byte.zero :: nil) ++ repeat (Byte Byte.zero) (Z.to_nat (len - 1))). + replace len with (1 + (len - 1)) at 1 by lia. + apply Mem.loadbytes_concat; try lia. + + apply RZ. lia. + + apply H; unfold Zwf; lia. + + rewrite <- Z2Nat.inj_succ by lia. f_equal; lia. +Qed. + +Lemma reads_as_zeros_equiv: forall m b from to, + reads_as_zeros m b from to <-> Genv.readbytes_as_zero m b from (to - from). +Proof. + intros; split; intros. +- red; intros. set (len := Z.of_nat n). + replace n with (Z.to_nat len) by apply Nat2Z.id. + eapply reads_as_zeros_loadbytes; eauto. lia. lia. +- red; intros. red in H. apply (H i 1%nat). lia. lia. +Qed. + +(** ** Semantic correctness of state operations *) + +(** Semantic interpretation of states. *) + +Record match_state (s: state) (m: mem) (b: block) : Prop := { + match_range: + 0 <= s.(curr) <= s.(total_size); + match_contents: + Mem.loadbytes m b 0 s.(curr) = Some (boidl (rev s.(init))); + match_valid: + idlvalid 0 (rev s.(init)); + match_uninitialized: + reads_as_zeros m b s.(curr) s.(total_size) +}. + +Lemma match_size: forall s m b, + match_state s m b -> + init_data_list_size (rev s.(init)) = s.(curr). +Proof. + intros. rewrite init_data_list_size_boidl. + erewrite Mem.loadbytes_length by (eapply match_contents; eauto). + apply Z2Nat.id. eapply match_range; eauto. +Qed. + +Lemma curr_pad_to: forall s pos, + curr s <= curr (pad_to s pos) /\ pos <= curr (pad_to s pos). +Proof. + unfold pad_to; intros. destruct (zle pos (curr s)); simpl; lia. +Qed. + +Lemma total_size_pad_to: forall s pos, + total_size (pad_to s pos) = total_size s. +Proof. + unfold pad_to; intros. destruct (zle pos (curr s)); auto. +Qed. + +Lemma pad_to_correct: forall pos s m b, + match_state s m b -> pos <= s.(total_size) -> + match_state (pad_to s pos) m b. +Proof. + intros. unfold pad_to. destruct (zle pos (curr s)); auto. + destruct H; constructor; simpl; intros. +- lia. +- rewrite boidl_rev_cons. simpl. + replace pos with (s.(curr) + (pos - s.(curr))) at 1 by lia. + apply Mem.loadbytes_concat; try lia. + * auto. + * eapply reads_as_zeros_loadbytes; eauto. lia. lia. lia. +- rewrite idlvalid_app. split; auto. simpl. intuition auto using Z.divide_1_l. +- eapply reads_as_zeros_mono; eauto; lia. +Qed. + +Lemma trisection_correct: forall s m b pos sz bytes1 bytes2 il, + match_state s m b -> + trisection s.(init) (s.(curr) - (pos + sz)) sz = OK (bytes1, bytes2, il) -> + 0 <= pos -> pos + sz <= s.(curr) -> 0 <= sz -> + Mem.loadbytes m b 0 pos = Some (boidl (rev il)) + /\ Mem.loadbytes m b pos sz = Some (inj_bytes bytes2) + /\ Mem.loadbytes m b (pos + sz) (s.(curr) - (pos + sz)) = Some (inj_bytes bytes1). +Proof. + intros. apply trisection_boidl in H0. destruct H0 as (A & B & C). + set (depth := curr s - (pos + sz)) in *. + pose proof (match_contents _ _ _ H) as D. + replace (curr s) with ((pos + sz) + depth) in D by lia. + exploit Mem.loadbytes_split. eexact D. lia. lia. + rewrite Z.add_0_l. intros (bytes0 & bytes1' & LB0 & LB1 & E1). + exploit Mem.loadbytes_split. eexact LB0. lia. lia. + rewrite Z.add_0_l. intros (bytes3 & bytes2' & LB3 & LB2 & E2). + rewrite A in E1. rewrite <- app_ass in E1. + exploit list_append_injective_r. eexact E1. + { unfold inj_bytes; rewrite map_length. erewrite Mem.loadbytes_length; eauto. } + intros (E3 & E4). + rewrite E2 in E3. + exploit list_append_injective_r. eexact E3. + { unfold inj_bytes; rewrite map_length. erewrite Mem.loadbytes_length; eauto. } + intros (E5 & E6). + intuition congruence. +Qed. + +Remark decode_int_zero_ext: forall n bytes, + 0 <= n <= 4 -> n = Z.of_nat (length bytes) -> + Int.zero_ext (n * 8) (Int.repr (decode_int bytes)) = Int.repr (decode_int bytes). +Proof. + intros. + assert (0 <= decode_int bytes < two_p (n * 8)). + { rewrite H0. replace (length bytes) with (length (rev_if_be bytes)). + apply int_of_bytes_range. + apply rev_if_be_length. } + assert (two_p (n * 8) <= Int.modulus). + { apply (two_p_monotone (n * 8) 32); lia. } + unfold Int.zero_ext. + rewrite Int.unsigned_repr by (unfold Int.max_unsigned; lia). + rewrite Zbits.Zzero_ext_mod by lia. + rewrite Zmod_small by auto. auto. +Qed. + +Theorem load_int_correct: forall s m b pos isz i v, + match_state s m b -> + load_int s pos isz = OK i -> + Mem.load (chunk_for_carrier isz) m b pos = Some v -> + v = Vint i. +Proof. + intros until v; intros MS RI LD. + exploit Mem.load_valid_access. eauto. intros [PERM ALIGN]. + unfold load_int in RI. + set (chunk := chunk_for_carrier isz) in *. + set (sz := size_chunk chunk) in *. + assert (sz > 0) by (apply size_chunk_pos). + set (s1 := pad_to s (pos + sz)) in *. + assert (pos + sz <= curr s1) by (apply curr_pad_to). + monadInv RI. InvBooleans. destruct x as [[bytes1 bytes2] il]. + assert (MS': match_state s1 m b) by (apply pad_to_correct; auto). + exploit trisection_correct; eauto. lia. + intros (L1 & L2 & L3). + assert (LEN: Z.of_nat (length bytes2) = sz). + { apply Mem.loadbytes_length in L2. unfold inj_bytes in L2. + rewrite map_length in L2. rewrite L2. apply Z2Nat.id; lia. } + exploit Mem.loadbytes_load. eexact L2. exact ALIGN. rewrite LD. + unfold decode_val. rewrite proj_inj_bytes. intros E; inv E; inv EQ0. + unfold chunk, chunk_for_carrier; destruct isz; f_equal. + - apply (decode_int_zero_ext 1). lia. auto. + - apply (decode_int_zero_ext 2). lia. auto. + - apply (decode_int_zero_ext 1). lia. auto. +Qed. + +Remark loadbytes_concat_3: forall m b ofs1 len1 l1 ofs2 len2 l2 ofs3 len3 l3 len, + Mem.loadbytes m b ofs1 len1 = Some l1 -> + Mem.loadbytes m b ofs2 len2 = Some l2 -> + Mem.loadbytes m b ofs3 len3 = Some l3 -> + ofs2 = ofs1 + len1 -> ofs3 = ofs2 + len2 -> 0 <= len1 -> 0 <= len2 -> 0 <= len3 -> + len = len1 + len2 + len3 -> + Mem.loadbytes m b ofs1 len = Some (l1 ++ l2 ++ l3). +Proof. + intros. rewrite H7, <- Z.add_assoc. apply Mem.loadbytes_concat. auto. + apply Mem.loadbytes_concat. rewrite <- H2; auto. rewrite <- H2, <- H3; auto. + lia. lia. lia. lia. +Qed. + +Theorem store_data_correct: forall s m b pos i s' m', + match_state s m b -> + store_data s pos i = OK s' -> + Genv.store_init_data ge m b pos i = Some m' -> + match i with Init_space _ => False | _ => True end -> + match_state s' m' b. +Proof. + intros until m'; intros MS ST SI NOSPACE. + exploit Genv.store_init_data_aligned; eauto. intros ALIGN. + assert (VALID: idvalid i). + { destruct i; simpl; auto. simpl in SI. destruct (Genv.find_symbol ge i); try discriminate. exists b0; auto. } + unfold store_data in ST. + set (sz := init_data_size i) in *. + assert (sz >= 0) by (apply init_data_size_pos). + set (s1 := pad_to s (pos + sz)) in *. + monadInv ST. InvBooleans. + assert (U: Mem.unchanged_on (fun b i => ~(pos <= i < pos + sz)) m m'). + { eapply Genv.store_init_data_unchanged. eauto. tauto. } + exploit store_init_data_loadbytes; eauto. fold sz. intros D. + destruct (zle (curr s) pos). +- inv ST. + set (il := if zlt (curr s) pos then Init_space (pos - curr s) :: init s else init s). + assert (IL: boidl (rev il) = boidl (rev (init s)) ++ repeat (Byte Byte.zero) (Z.to_nat (pos - curr s))). + { unfold il; destruct (zlt (curr s) pos). + - simpl rev. rewrite boidl_rev_cons. simpl. auto. + - rewrite Z_to_nat_neg by lia. simpl. rewrite app_nil_r; auto. + } + constructor; simpl; intros. + + lia. + + rewrite boidl_rev_cons, IL, app_ass. + apply loadbytes_concat_3 with (len1 := curr s) (ofs2 := curr s) (len2 := pos - curr s) (ofs3 := pos) (len3 := sz); try lia. + * eapply Mem.loadbytes_unchanged_on; eauto. + intros. simpl. lia. + eapply match_contents; eauto. + * eapply Mem.loadbytes_unchanged_on; eauto. + intros. simpl. lia. + eapply reads_as_zeros_loadbytes. eapply match_uninitialized; eauto. lia. lia. lia. + * exact D. + * eapply match_range; eauto. + + rewrite idlvalid_app; split. + * unfold il; destruct (zlt (curr s) pos). + ** simpl; rewrite idlvalid_app; split. eapply match_valid; eauto. simpl. auto using Z.divide_1_l. + ** eapply match_valid; eauto. + * simpl. + replace (init_data_list_size (rev il)) with pos. tauto. + unfold il; destruct (zlt (curr s) pos). + ** simpl; rewrite init_data_list_size_app; simpl. + erewrite match_size by eauto. lia. + ** erewrite match_size by eauto. lia. + + eapply reads_as_zeros_unchanged; eauto. + eapply reads_as_zeros_mono. eapply match_uninitialized; eauto. lia. lia. + intros. simpl. lia. +- monadInv ST. destruct x as [[bytes1 bytes2] il]. inv EQ0. + assert (pos + sz <= curr s1) by (apply curr_pad_to). + assert (MS': match_state s1 m b) by (apply pad_to_correct; auto). + exploit trisection_correct; eauto. lia. + intros (L1 & L2 & L3). + constructor; simpl; intros. + + eapply match_range; eauto. + + rewrite add_rev_bytes_spec, rev_app_distr; simpl; rewrite app_ass; simpl. + rewrite <- map_rev, rev_involutive. + rewrite boidl_app. simpl. rewrite boidl_init_bytes. + apply loadbytes_concat_3 with (len1 := pos) (ofs2 := pos) (len2 := sz) (ofs3 := pos + sz) + (len3 := curr s1 - (pos + sz)); try lia. + * eapply Mem.loadbytes_unchanged_on; eauto. + intros. simpl. lia. + * exact D. + * eapply Mem.loadbytes_unchanged_on; eauto. + intros. simpl. lia. + + apply add_rev_bytes_valid. simpl; rewrite idlvalid_app; split. + * eapply trisection_valid; eauto. eapply match_valid; eauto. + * rewrite init_data_list_size_boidl. erewrite Mem.loadbytes_length by eauto. + rewrite Z2Nat.id by lia. simpl. tauto. + + eapply reads_as_zeros_unchanged; eauto. eapply match_uninitialized; eauto. + intros. simpl. lia. +Qed. + +Corollary store_int_correct: forall s m b pos isz n s' m', + match_state s m b -> + store_int s pos isz n = OK s' -> + Mem.store (chunk_for_carrier isz) m b pos (Vint n) = Some m' -> + match_state s' m' b. +Proof. + intros. eapply store_data_correct; eauto. +- destruct isz; exact H1. +- destruct isz; exact I. +Qed. + +Theorem init_data_list_of_state_correct: forall s m b il b' m1, + match_state s m b -> + init_data_list_of_state s = OK il -> + Mem.range_perm m1 b' 0 s.(total_size) Cur Writable -> + reads_as_zeros m1 b' 0 s.(total_size) -> + exists m2, + Genv.store_init_data_list ge m1 b' 0 il = Some m2 + /\ Mem.loadbytes m2 b' 0 (init_data_list_size il) = Mem.loadbytes m b 0 s.(total_size). +Proof. + intros. unfold init_data_list_of_state in H0; monadInv H0. rename l into LE. + set (s1 := pad_to s s.(total_size)) in *. + assert (MS1: match_state s1 m b) by (apply pad_to_correct; auto; lia). + apply reads_as_zeros_equiv in H2. rewrite Z.sub_0_r in H2. + assert (R: rev' (init s1) = rev (init s1)). + { unfold rev'. rewrite <- rev_alt. auto. } + assert (C: curr s1 = total_size s). + { unfold s1, pad_to. destruct zle; simpl; lia. } + assert (A: Genv.init_data_list_aligned 0 (rev (init s1))). + { exploit match_valid; eauto. generalize (rev (init s1)) 0. + induction l as [ | i l]; simpl; intuition. } + assert (B: forall id ofs, In (Init_addrof id ofs) (rev (init s1)) -> + exists b, Genv.find_symbol ge id = Some b). + { intros id ofs. exploit match_valid; eauto. generalize (rev (init s1)) 0. + induction l as [ | i l]; simpl; intuition eauto. subst i; assumption. } + exploit Genv.store_init_data_list_exists. + 2: eexact A. 2: eexact B. + erewrite match_size by eauto. rewrite C. eauto. + intros (m2 & ST). exists m2; split. +- rewrite R. auto. +- rewrite R. transitivity (Some (boidl (rev (init s1)))). + + eapply Genv.store_init_data_list_loadbytes; eauto. + erewrite match_size, C by eauto. auto. + + symmetry. rewrite <- C. eapply match_contents; eauto. +Qed. + +(** ** Total size properties *) + +Lemma total_size_store_data: forall s pos i s', + store_data s pos i = OK s' -> total_size s' = total_size s. +Proof. + unfold store_data; intros. monadInv H. destruct (zle (curr s) pos); monadInv H. +- auto. +- destruct x as [[bytes1 bytes2] il2]. inv EQ0. simpl. apply total_size_pad_to. +Qed. + +Lemma total_size_transl_init_bitfield: forall ce s ty sz p w i pos s', + transl_init_bitfield ce s ty sz p w i pos = OK s' -> total_size s' = total_size s. +Proof. + unfold transl_init_bitfield; intros. destruct i; monadInv H. destruct x; monadInv EQ0. + eapply total_size_store_data. eexact EQ2. +Qed. + +Lemma total_size_transl_init_rec: forall ce s ty i pos s', + transl_init_rec ce s ty i pos = OK s' -> total_size s' = total_size s +with total_size_transl_init_array: forall ce s tyelt il pos s', + transl_init_array ce s tyelt il pos = OK s' -> total_size s' = total_size s +with total_size_transl_init_struct: forall ce s ms il base pos s', + transl_init_struct ce s ms il base pos = OK s' -> total_size s' = total_size s. +Proof. +- destruct i; simpl; intros. + + monadInv H; eauto using total_size_store_data. + + destruct ty; monadInv H. eauto. + + destruct ty; monadInv H. destruct (co_su x); try discriminate. eauto. + + destruct ty; monadInv H. destruct (co_su x); monadInv EQ0. destruct x2. + * eauto. + * eauto using total_size_transl_init_bitfield. +- destruct il; simpl; intros. + + inv H; auto. + + monadInv H. transitivity (total_size x); eauto. +- destruct il; simpl; intros. + + inv H; auto. + + revert ms pos H. induction ms; intros. + * inv H. + * destruct (member_not_initialized a). eapply IHms; eauto. + monadInv H. transitivity (total_size x1). eauto. + destruct x0; eauto using total_size_transl_init_bitfield. Qed. (** * Soundness of the translation of initializers *) (** Soundness for single initializers. *) -Theorem transl_init_single_steps: - forall ty a data f m v1 ty1 m' v chunk b ofs m'', +Inductive exec_assign: mem -> block -> Z -> bitfield -> type -> val -> mem -> Prop := + | exec_assign_full: forall m b ofs ty v m' chunk, + access_mode ty = By_value chunk -> + Mem.store chunk m b ofs v = Some m' -> + exec_assign m b ofs Full ty v m' + | exec_assign_bits: forall m b ofs sz sg sg1 attr pos width ty n m' c, + type_is_volatile ty = false -> + 0 <= pos -> 0 < width -> pos + width <= bitsize_intsize sz -> + sg1 = (if zlt width (bitsize_intsize sz) then Signed else sg) -> + Mem.load (chunk_for_carrier sz) m b ofs = Some (Vint c) -> + Mem.store (chunk_for_carrier sz) m b ofs + (Vint (Int.bitfield_insert (first_bit sz pos width) width c n)) = Some m' -> + exec_assign m b ofs (Bits sz sg pos width) (Tint sz sg1 attr) (Vint n) m'. + +Lemma transl_init_single_sound: + forall ty a data f m v1 ty1 m' v b ofs m'', 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 m' = Some v -> - 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''. + exec_assign m' b ofs Full ty v m'' -> + Genv.store_init_data ge m b ofs data = Some m'' + /\ match data with Init_space _ => False | _ => True end. Proof. - intros. monadInv H. monadInv EQ. + intros until m''; intros TR STEPS CAST ASG. + monadInv TR. 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. + inv ASG. rename H into A. unfold Genv.store_init_data. inv D. - (* int *) 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 EQ0. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption. + destruct s; simpl in A; inv A. rewrite <- Mem.store_signed_unsigned_8; auto. auto. + destruct s; simpl in A; inv A. rewrite <- Mem.store_signed_unsigned_16; auto. auto. + simpl in A; inv A. auto. + simpl in A; inv A. auto. ++ destruct ptr64; inv EQ0. simpl in A; unfold Mptr in A; rewrite <- Heqptr64 in A; inv A. auto. - (* Long *) - 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. + remember Archi.ptr64 as ptr64. destruct ty; monadInv EQ0. ++ simpl in A; inv A. auto. ++ simpl in A; unfold Mptr in A; rewrite <- Heqptr64 in A; inv A. auto. - (* float *) destruct ty; try discriminate. - destruct f1; inv EQ0; simpl in H2; inv H2; assumption. + destruct f1; inv EQ0; simpl in A; inv A; auto. - (* single *) destruct ty; try discriminate. - destruct f1; inv EQ0; simpl in H2; inv H2; assumption. + destruct f1; inv EQ0; simpl in A; inv A; auto. - (* pointer *) unfold inj in H. - assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr). + assert (X: data = Init_addrof b1 ofs1 /\ chunk = Mptr). { remember Archi.ptr64 as ptr64. 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. } - destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. - rewrite Ptrofs.add_zero in H3. auto. + - destruct i; monadInv H2. unfold Mptr. rewrite <- Heqptr64. inv A; auto. + - monadInv H2. unfold Mptr. rewrite <- Heqptr64. inv A; auto. + - inv A; auto. + } + destruct X; subst. destruct (Genv.find_symbol ge b1); inv H. + rewrite Ptrofs.add_zero in H0. auto. - (* undef *) discriminate. Qed. -(** Size properties for initializers. *) - -Lemma transl_init_single_size: - forall ty a data, - transl_init_single ge ty a = OK data -> - init_data_size data = sizeof ge ty. -Proof. - intros. monadInv H. monadInv EQ. remember Archi.ptr64 as ptr64. destruct x. -- monadInv EQ0. -- destruct ty; try discriminate. - destruct i0; inv EQ0; auto. - destruct ptr64; inv EQ0. -Local Transparent sizeof. - unfold sizeof. rewrite <- Heqptr64; auto. -- destruct ty; inv EQ0; auto. - unfold sizeof. destruct Archi.ptr64; inv H0; auto. -- destruct ty; try discriminate. - destruct f0; inv EQ0; auto. -- destruct ty; try discriminate. - destruct f0; inv EQ0; auto. -- destruct ty; try discriminate. - destruct i0; inv EQ0; auto. - destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto. - destruct ptr64; inv EQ0. simpl. rewrite <- Heqptr64; auto. - inv EQ0. unfold init_data_size, sizeof. auto. -Qed. - -Notation idlsize := init_data_list_size. - -Remark padding_size: - forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm. -Proof. - unfold tr_padding; intros. destruct (zlt frm to). - simpl. xomega. - simpl. 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 union_field_size: - forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl. -Proof. - 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 tr_init_size: - forall i ty data, - tr_init ty i data -> - idlsize data = sizeof ge ty -with tr_init_array_size: - forall ty il sz data, - tr_init_array ty il sz data -> - idlsize data = sizeof ge ty * sz -with tr_init_struct_size: - forall ty fl il pos data, - tr_init_struct ty fl il pos data -> - sizeof_struct ge pos fl <= sizeof ge ty -> - idlsize data + pos = sizeof ge ty. -Proof. -Local Opaque sizeof. -- destruct 1; simpl. -+ erewrite transl_init_single_size by eauto. omega. -+ Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. -+ replace (idlsize d) with (idlsize d + 0) by omega. - eapply tr_init_struct_size; eauto. simpl. - unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. - erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). - unfold sizeof_composite. rewrite H0. apply align_le. - destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. -+ rewrite idlsize_app, padding_size. - exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. - simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. - apply Z.le_trans with (sizeof_union ge (co_members co)). - eapply union_field_size; eauto. - erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). - unfold sizeof_composite. rewrite H0. apply align_le. - destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - -- destruct 1; simpl. -+ omega. -+ rewrite Z.mul_comm. - assert (0 <= sizeof ge ty * sz). - { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } - xomega. -+ rewrite idlsize_app. - erewrite tr_init_size by eauto. - erewrite tr_init_array_size by eauto. - ring. - -- destruct 1; simpl; intros. -+ rewrite padding_size by auto. omega. -+ rewrite ! idlsize_app, padding_size. - erewrite tr_init_size by eauto. - rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega. - unfold pos1. apply align_le. apply alignof_pos. -Qed. +(* Hypothesis ce_consistent: composite_env_consistent ge. *) (** A semantics for general initializers *) Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip. -Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) := - match fl with - | nil => nil - | (id1, ty1) :: fl' => - (align pos (alignof ge ty1), ty1) :: fields_of_struct fl' (align pos (alignof ge ty1) + sizeof ge ty1) +Fixpoint initialized_fields_of_struct (ms: members) (pos: Z) : res (list (Z * bitfield * type)) := + match ms with + | nil => + OK nil + | m :: ms' => + let pos' := next_field ge.(genv_cenv) pos m in + if member_not_initialized m + then initialized_fields_of_struct ms' pos' + else + do ofs_bf <- layout_field ge.(genv_cenv) pos m; + do l <- initialized_fields_of_struct ms' pos'; + OK ((ofs_bf, type_member m) :: 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'', +Inductive exec_init: mem -> block -> Z -> bitfield -> type -> initializer -> mem -> Prop := + | exec_init_single_: forall m b ofs bf ty a v1 ty1 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') -> sem_cast v1 ty1 ty m' = Some 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_assign m' b ofs bf ty v m'' -> + exec_init m b ofs bf ty (Init_single a) m'' | 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 a il co m', + exec_init m b ofs Full (Tarray ty sz a) (Init_array il) m' + | exec_init_struct_: forall m b ofs id a il co flds 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', + initialized_fields_of_struct (co_members co) 0 = OK flds -> + exec_init_struct m b ofs flds il m' -> + exec_init m b ofs Full (Tstruct id a) (Init_struct il) m' + | exec_init_union_: forall m b ofs id a f i co ty pos bf 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 a) (Init_union f i) m' + union_field_offset ge f (co_members co) = OK (pos, bf) -> + exec_init m b (ofs + pos) bf ty i m' -> + exec_init m b ofs Full (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, sz >= 0 -> 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 m b ofs Full ty i1 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 := - | exec_init_list_nil: forall m b ofs, - exec_init_list m b ofs nil Init_nil m - | exec_init_list_cons: forall m b ofs pos ty l i1 il m' m'', - exec_init m b (ofs + pos) ty i1 m' -> - exec_init_list m' b ofs l il m'' -> - exec_init_list m b ofs ((pos, ty) :: l) (Init_cons i1 il) m''. +with exec_init_struct: mem -> block -> Z -> list (Z * bitfield * type) -> initializer_list -> mem -> Prop := + | exec_init_struct_nil: forall m b ofs, + exec_init_struct m b ofs nil Init_nil m + | exec_init_struct_cons: forall m b ofs pos bf ty l i1 il m' m'', + exec_init m b (ofs + pos) bf ty i1 m' -> + exec_init_struct m' b ofs l il m'' -> + exec_init_struct m b ofs ((pos, bf, ty) :: l) (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_list_ind3 := Minimality for exec_init_list Sort Prop. -Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_list_ind3. + 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' -> sz >= 0. Proof. - induction 1; 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 Z.add_0_r in H0. auto. - destruct (Genv.store_init_data ge m b ofs a); try discriminate. - rewrite Z.add_assoc in H0. eauto. + induction 1; lia. Qed. -Remark store_init_data_list_padding: - forall frm to b ofs m, - Genv.store_init_data_list ge m b ofs (tr_padding frm to) = Some m. +Lemma transl_init_rec_sound: + (forall m b ofs bf ty i m', + exec_init m b ofs bf ty i m' -> + forall s s', + match_state s m b -> + match bf with + | Full => transl_init_rec ge s ty i ofs + | Bits sz sg p w => transl_init_bitfield ge s ty sz p w i ofs + end = OK s' -> + match_state s' m' b) +/\ (forall m b ofs ty sz il m', + exec_init_array m b ofs ty sz il m' -> + forall s s', + match_state s m b -> + transl_init_array ge s ty il ofs = OK s' -> + match_state s' m' b) +/\ (forall m b ofs flds il m', + exec_init_struct m b ofs flds il m' -> + forall s s' ms pos, + match_state s m b -> + initialized_fields_of_struct ms pos = OK flds -> + transl_init_struct ge s ms il ofs pos = OK s' -> + match_state s' m' b). Proof. - intros. unfold tr_padding. destruct (zlt frm to); auto. -Qed. - -Lemma tr_init_sound: - (forall m b ofs ty i m', exec_init m b ofs ty i m' -> - forall data, tr_init ty i 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, tr_init_array ty il sz 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 ty fl data pos, - l = fields_of_struct fl pos -> - tr_init_struct ty fl il pos data -> - Genv.store_init_data_list ge m b (ofs + pos) data = Some m'). -Proof. -Local Opaque sizeof. - apply exec_init_scheme; simpl; intros. + apply exec_init_scheme. - (* single *) - inv H3. simpl. erewrite transl_init_single_steps by eauto. auto. + intros until m''; intros STEP CAST ASG s s' MS TR. destruct bf; monadInv TR. + + (* full *) + exploit transl_init_single_sound; eauto. intros [P Q]. + eapply store_data_correct; eauto. + + (* bitfield *) + destruct x; monadInv EQ0. monadInv EQ. + exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. + exploit sem_cast_match; eauto. intros D. + inv ASG. inv D. + set (f := first_bit sz pos width) in *. + assert (E: Vint c = Vint x) by (eapply load_int_correct; eauto). + inv E. + eapply store_int_correct; eauto. - (* array *) - inv H1. replace (Z.max 0 sz) with sz in H7. eauto. - assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. + intros. monadInv H2. eauto. - (* struct *) - inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. - replace ofs with (ofs + 0) by omega. eauto. + intros. monadInv H5. unfold lookup_composite in EQ. rewrite H in EQ. inv EQ. + rewrite H0 in EQ0. eauto. - (* union *) - inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. - eapply store_init_data_list_app. eauto. - apply store_init_data_list_padding. - -- (* array, empty *) - inv H0; auto. -- (* array, nonempty *) - inv H3. - eapply store_init_data_list_app. - eauto. - rewrite (tr_init_size _ _ _ H7). eauto. - -- (* struct, empty *) - inv H0. apply store_init_data_list_padding. -- (* struct, nonempty *) - inv H4. simpl in H3; inv H3. - eapply store_init_data_list_app. apply store_init_data_list_padding. - rewrite padding_size. - replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega. - eapply store_init_data_list_app. + intros. monadInv H6. unfold lookup_composite in EQ. rewrite H in EQ. inv EQ. rewrite H0 in EQ0. + rewrite H1, H2 in EQ0. simpl in EQ0. eauto. +- (* array nil *) + intros. monadInv H1. auto. +- (* array cons *) + intros. monadInv H4. eauto. +- (* struct nil *) + intros. monadInv H1. auto. +- (* struct cons *) + intros. simpl in H5. revert H4 H5. generalize pos0. induction ms as [ | m1 ms]. discriminate. + simpl. destruct (member_not_initialized m1). + intros; eapply IHms; eauto. + clear IHms. intros. monadInv H5. rewrite EQ in H4. monadInv H4. inv EQ0. eauto. - rewrite (tr_init_size _ _ _ H9). - rewrite <- Z.add_assoc. eapply H2. eauto. eauto. - apply align_le. apply alignof_pos. Qed. End SOUNDNESS. Theorem transl_init_sound: - forall p m b ty i m' data, - exec_init (globalenv p) m b 0 ty i m' -> + forall p m b ty i m1 data, + let sz := sizeof (prog_comp_env p) ty in + Mem.range_perm m b 0 sz Cur Writable -> + reads_as_zeros m b 0 sz -> + exec_init (globalenv p) m b 0 Full ty i m1 -> transl_init (prog_comp_env p) ty i = OK data -> - Genv.store_init_data_list (globalenv p) m b 0 data = Some m'. + exists m2, + Genv.store_init_data_list (globalenv p) m b 0 data = Some m2 + /\ Mem.loadbytes m2 b 0 (init_data_list_size data) = Mem.loadbytes m1 b 0 sz. Proof. intros. set (ge := globalenv p) in *. - change (prog_comp_env p) with (genv_cenv ge) in H0. - destruct (tr_init_sound ge) as (A & B & C). - eapply build_composite_env_consistent. apply prog_comp_env_eq. - eapply A; eauto. apply transl_init_spec; auto. + change (prog_comp_env p) with (genv_cenv ge) in *. + unfold transl_init in H2; monadInv H2. + fold sz in EQ. set (s0 := initial_state sz) in *. + assert (match_state ge s0 m b). + { constructor; simpl. + - generalize (sizeof_pos ge ty). fold sz. lia. + - apply Mem.loadbytes_empty. lia. + - auto. + - assumption. + } + assert (match_state ge x m1 b). + { eapply (proj1 (transl_init_rec_sound ge)); eauto. } + assert (total_size x = sz). + { change sz with s0.(total_size). eapply total_size_transl_init_rec; eauto. } + rewrite <- H4. eapply init_data_list_of_state_correct; eauto; rewrite H4; auto. Qed. |