(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (** Compile-time evaluation of initializers for global C variables. *) 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. Open Scope error_monad_scope. Section SOUNDNESS. Variable ge: genv. (** * Simple expressions and their big-step semantics *) (** An expression is simple if it contains no assignments and no function calls. *) Fixpoint simple (a: expr) : Prop := match a with | Eloc _ _ _ _ => True | Evar _ _ => True | Ederef r _ => simple r | Efield l1 _ _ => simple l1 | Eval _ _ => True | Evalof l _ => simple l | Eaddrof l _ => simple l | Eunop _ r1 _ => simple r1 | Ebinop _ r1 r2 _ => simple r1 /\ simple r2 | Ecast r1 _ => simple r1 | Eseqand r1 r2 _ => simple r1 /\ simple r2 | Eseqor r1 r2 _ => simple r1 /\ simple r2 | Econdition r1 r2 r3 _ => simple r1 /\ simple r2 /\ simple r3 | Esizeof _ _ => True | Ealignof _ _ => True | Eassign _ _ _ => False | Eassignop _ _ _ _ _ => False | Epostincr _ _ _ => False | Ecomma r1 r2 _ => simple r1 /\ simple r2 | Ecall _ _ _ => False | Ebuiltin _ _ _ _ => False | Eparen r1 _ _ => simple r1 end. (** A big-step semantics for simple expressions. Similar to the big-step semantics from [Cstrategy], with the addition of conditionals, comma and paren operators. It is a pity we do not share definitions with [Cstrategy], but such sharing raises technical difficulties. *) Section SIMPLE_EXPRS. Variable e: env. Variable m: mem. 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 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 Full | esl_deref: forall r ty b ofs, eval_simple_rvalue r (Vptr b ofs) -> 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, 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 -> 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 bf l ty v, eval_simple_lvalue l b ofs bf -> ty = typeof l -> 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 Full -> eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> sem_unary_operation op v1 (typeof r1) m = Some v -> 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 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 m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool m = Some v3 -> eval_simple_rvalue (Eseqand r1 r2 ty) v3 | esr_seqand_false: forall r1 r2 ty v1, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero) | esr_seqor_false: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool m = Some v3 -> eval_simple_rvalue (Eseqor r1 r2 ty) v3 | esr_seqor_true: forall r1 r2 ty v1, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one) | esr_condition: forall r1 r2 r3 ty v v1 b v', eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> eval_simple_rvalue (if b then r2 else r3) v' -> sem_cast v' (typeof (if b then r2 else r3)) ty m = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v | esr_comma: forall r1 r2 ty v1 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v -> eval_simple_rvalue (Ecomma r1 r2 ty) v | esr_paren: forall r tycast ty v v', eval_simple_rvalue r v -> sem_cast v (typeof r) tycast m = Some v' -> eval_simple_rvalue (Eparen r tycast ty) v'. End SIMPLE_EXPRS. (** * Correctness of the big-step semantics with respect to reduction sequences *) (** In this section, we show that if a simple expression [a] reduces to some value (with the transition semantics from module [Csem]), then it evaluates to this value (with the big-step semantics above). *) Definition compat_eval (k: kind) (e: env) (a a': expr) (m: mem) : Prop := typeof a = typeof a' /\ match k with | 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. Lemma lred_simple: forall e l m l' m', lred ge e l m l' m' -> simple l -> simple l'. Proof. induction 1; simpl; tauto. Qed. 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 bf' EV; inv EV. apply esl_var_local; auto. apply esl_var_global; auto. constructor. constructor. eapply esl_field_struct; eauto. constructor. simpl; eauto. eapply esl_field_union; eauto. constructor. simpl; eauto. Qed. Lemma rred_simple: forall r m t r' m', rred ge r m t r' m' -> simple r -> simple r'. Proof. induction 1; simpl; intuition. destruct b; auto. Qed. Lemma rred_compat: forall e r m r' m', rred ge r m E0 r' m' -> simple r -> m = m' /\ compat_eval RV e r r' m. Proof. intros until m'; intros RED SIMP. inv RED; simpl in SIMP; try contradiction; split; auto; split; auto; intros vx EV. inv EV. econstructor. constructor. auto. auto. inv EV. econstructor. constructor. inv EV. econstructor; eauto. constructor. inv EV. econstructor; eauto. constructor. constructor. inv EV. econstructor; eauto. constructor. inv EV. eapply esr_seqand_true; eauto. constructor. inv EV. eapply esr_seqand_false; eauto. constructor. inv EV. eapply esr_seqor_true; eauto. constructor. inv EV. eapply esr_seqor_false; eauto. constructor. inv EV. eapply esr_condition; eauto. constructor. inv EV. constructor. inv EV. constructor. econstructor; eauto. constructor. inv EV. econstructor. constructor. auto. Qed. Lemma compat_eval_context: forall e a a' m from to C, context from to C -> compat_eval from e a a' m -> compat_eval to e (C a) (C a') m. Proof. induction 1; intros CE; auto; try (generalize (IHcontext CE); intros [TY EV]; red; split; simpl; auto; intros). inv H0. constructor; auto. inv H0. eapply esl_field_struct; eauto. rewrite TY; eauto. eapply esl_field_union; eauto. rewrite TY; eauto. inv H0. econstructor. eauto. auto. auto. inv H0. econstructor; eauto. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. inv H0. eapply esr_seqand_true; eauto. rewrite TY; auto. eapply esr_seqand_false; eauto. rewrite TY; auto. inv H0. eapply esr_seqor_false; eauto. rewrite TY; auto. eapply esr_seqor_true; eauto. rewrite TY; auto. inv H0. eapply esr_condition; eauto. congruence. inv H0. inv H0. inv H0. inv H0. inv H0. inv H0. red; split; intros. auto. inv H0. red; split; intros. auto. inv H0. inv H0. econstructor; eauto. inv H0. econstructor; eauto. congruence. Qed. Lemma simple_context_1: forall a from to C, context from to C -> simple (C a) -> simple a. Proof. induction 1; simpl; tauto. Qed. Lemma simple_context_2: forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a'). Proof. induction 2; simpl; try tauto. Qed. Lemma compat_eval_steps_aux f r e m r' m' s2 : simple r -> star step ge s2 nil (ExprState f r' Kstop e m') -> estep ge (ExprState f r Kstop e m) nil s2 -> exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1. Proof. intros. inv H1. (* lred *) assert (S: simple a) by (eapply simple_context_1; eauto). exploit lred_compat; eauto. intros [A B]. subst m'0. econstructor; split. eauto. split. eapply compat_eval_context; eauto. eapply simple_context_2; eauto. eapply lred_simple; eauto. (* rred *) assert (S: simple a) by (eapply simple_context_1; eauto). exploit rred_compat; eauto. intros [A B]. subst m'0. econstructor; split. eauto. split. eapply compat_eval_context; eauto. eapply simple_context_2; eauto. eapply rred_simple; eauto. (* callred *) assert (S: simple a) by (eapply simple_context_1; eauto). inv H8; simpl in S; contradiction. (* stuckred *) inv H0. destruct H1; inv H0. Qed. Lemma compat_eval_steps: forall f r e m r' m', star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') -> simple r -> m' = m /\ compat_eval RV e r r' m. Proof. intros. remember (ExprState f r Kstop e m) as S1. remember E0 as t. remember (ExprState f r' Kstop e m') as S2. revert S1 t S2 H r m r' m' HeqS1 Heqt HeqS2 H0. induction 1; intros; subst. (* base case *) inv HeqS2. split. auto. red; auto. (* inductive case *) destruct (app_eq_nil t1 t2); auto. subst. inv H. (* expression step *) exploit compat_eval_steps_aux; eauto. intros [r1 [A [B C]]]. subst s2. exploit IHstar; eauto. intros [D E]. split. auto. destruct B; destruct E. split. congruence. auto. (* statement steps *) inv H1. Qed. Theorem eval_simple_steps: forall f r e m v ty m', star step ge (ExprState f r Kstop e m) E0 (ExprState f (Eval v ty) Kstop e m') -> simple r -> m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v. Proof. intros. exploit compat_eval_steps; eauto. intros [A [B C]]. intuition. apply C. constructor. Qed. (** * Soundness of the compile-time evaluator *) (** A global environment [ge] induces a memory injection mapping our symbolic pointers [Vptr id ofs] to run-time pointers [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *) Definition inj (b: block) := match Genv.find_symbol ge b with | Some b' => Some (b', 0) | None => None end. Lemma mem_empty_not_valid_pointer: forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. Proof. intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Cur Nonempty); auto. eelim Mem.perm_empty; eauto. Qed. Lemma mem_empty_not_weak_valid_pointer: forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false. Proof. intros. unfold Mem.weak_valid_pointer. now rewrite !mem_empty_not_valid_pointer. Qed. Lemma sem_cast_match: forall v1 ty1 ty2 m v2 v1' v2', sem_cast v1 ty1 ty2 m = Some v2 -> do_cast v1' ty1 ty2 = OK v2' -> Val.inject inj v1' v1 -> Val.inject inj v2' v2. Proof. intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2 Mem.empty) as [v2''|] eqn:E; inv H0. exploit (sem_cast_inj inj Mem.empty m). intros. rewrite mem_empty_not_weak_valid_pointer in H2. discriminate. eexact E. eauto. intros [v' [A B]]. congruence. Qed. Lemma bool_val_match: forall v ty b v' m, bool_val v ty Mem.empty = Some b -> Val.inject inj v v' -> bool_val v' ty m = Some b. 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: forall m a v, eval_simple_rvalue empty_env m a v -> forall v', constval ge a = OK v' -> Val.inject inj v' v with constval_lvalue: forall m a b ofs bf, eval_simple_lvalue empty_env m a b ofs bf -> forall v', constval ge a = OK v' -> 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 *) 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 *) 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). intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) 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. intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. eauto. eauto. eauto. intros [v' [A B]]. congruence. (* cast *) eapply sem_cast_match; eauto. (* sizeof *) auto. (* alignof *) auto. (* seqand *) destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. eapply sem_cast_match; eauto. destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. eapply sem_cast_match; eauto. destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) destruct (bool_val x (typeof r1) Mem.empty) as [b'|] eqn:E; inv EQ3. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b' = b) by congruence. subst b'. destruct b; eapply sem_cast_match; eauto. (* comma *) auto. (* paren *) eapply sem_cast_match; eauto. (* lvalue *) induction 1; intros v' CV; simpl in CV; try (monadInv CV). (* var local *) split; auto. unfold empty_env in H. rewrite PTree.gempty in H. congruence. (* var_global *) split; auto. econstructor. unfold inj. rewrite H0. eauto. auto. (* deref *) split; eauto. (* field struct *) 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 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 (access_mode ty); discriminate || eauto. intuition eauto. Qed. (** Soundness of [constval] with respect to the reduction semantics. *) 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 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. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. Qed. (** * 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. 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. 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 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. *) 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 -> 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 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. 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 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; 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 A; inv A; auto. - (* single *) destruct ty; try discriminate. destruct f1; inv EQ0; simpl in A; inv A; auto. - (* pointer *) unfold inj in H. assert (X: data = Init_addrof b1 ofs1 /\ chunk = Mptr). { remember Archi.ptr64 as ptr64. destruct ty; inversion EQ0. - 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. (* Hypothesis ce_consistent: composite_env_consistent ge. *) (** A semantics for general initializers *) Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip. 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 -> 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 -> 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 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 -> 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 -> 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 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_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_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; lia. Qed. 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. apply exec_init_scheme. - (* single *) 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 *) intros. monadInv H2. eauto. - (* struct *) intros. monadInv H5. unfold lookup_composite in EQ. rewrite H in EQ. inv EQ. rewrite H0 in EQ0. eauto. - (* union *) 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. Qed. End SOUNDNESS. Theorem transl_init_sound: 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 -> 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 *. 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.