From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 311 +++++++++++++++++++++++++++++++++------------ 1 file changed, 232 insertions(+), 79 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a6656e0b..1a66ec90 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -61,6 +61,18 @@ Lemma functions_translated: Genv.find_funct tge v = Some tf /\ transl_fundef gce f = OK tf. Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). +Lemma var_info_translated: + forall b v, + Genv.find_var_info ge b = Some v -> + exists tv, Genv.find_var_info tge b = Some tv /\ transf_globvar transl_globvar v = OK tv. +Proof (Genv.find_var_info_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). + +Lemma var_info_rev_translated: + forall b tv, + Genv.find_var_info tge b = Some tv -> + exists v, Genv.find_var_info ge b = Some v /\ transf_globvar transl_globvar v = OK tv. +Proof (Genv.find_var_info_rev_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). + Lemma sig_preserved_body: forall f tf cenv size, transl_funbody cenv size f = OK tf -> @@ -245,10 +257,10 @@ Inductive match_var (f: meminj) (id: ident) val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> match_var f id e m te sp (Var_stack_scalar chunk ofs) | match_var_stack_array: - forall ofs sz b, - PTree.get id e = Some (b, Varray sz) -> + forall ofs sz al b, + PTree.get id e = Some (b, Varray sz al) -> val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> - match_var f id e m te sp (Var_stack_array ofs) + match_var f id e m te sp (Var_stack_array ofs sz al) | match_var_global_scalar: forall chunk, PTree.get id e = None -> @@ -463,8 +475,8 @@ Inductive alloc_condition: var_info -> var_kind -> block -> option (block * Z) - alloc_condition (Var_local chunk) (Vscalar chunk) sp None | alloc_cond_stack_scalar: forall chunk pos sp, alloc_condition (Var_stack_scalar chunk pos) (Vscalar chunk) sp (Some(sp, pos)) - | alloc_cond_stack_array: forall pos sz sp, - alloc_condition (Var_stack_array pos) (Varray sz) sp (Some(sp, pos)). + | alloc_cond_stack_array: forall pos sz al sp, + alloc_condition (Var_stack_array pos sz al) (Varray sz al) sp (Some(sp, pos)). Lemma match_env_alloc_same: forall f1 cenv e le m1 te sp lo lv m2 b f2 id info tv, @@ -1156,6 +1168,7 @@ Qed. Definition val_match_approx (a: approx) (v: val) : Prop := match a with + | Int1 => v = Val.zero_ext 1 v | Int7 => v = Val.zero_ext 8 v /\ v = Val.sign_ext 8 v | Int8u => v = Val.zero_ext 8 v | Int8s => v = Val.sign_ext 8 v @@ -1187,8 +1200,16 @@ Proof. intros. rewrite H. destruct v; simpl; auto. decEq. symmetry. apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto. + assert (D: forall v, v = Val.zero_ext 1 v -> v = Val.zero_ext 8 v). + intros. rewrite H. + destruct v; simpl; auto. decEq. symmetry. + apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. + assert (E: forall v, v = Val.zero_ext 1 v -> v = Val.sign_ext 8 v). + intros. rewrite H. + destruct v; simpl; auto. decEq. symmetry. + apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto. intros. - unfold Approx.bge in H; destruct a1; try discriminate; destruct a2; simpl in *; try discriminate; intuition; auto. + unfold Approx.bge in H; destruct a1; try discriminate; destruct a2; simpl in *; try discriminate; intuition. Qed. Lemma approx_lub_ge_left: @@ -1206,7 +1227,9 @@ Qed. Lemma approx_of_int_sound: forall n, val_match_approx (Approx.of_int n) (Vint n). Proof. - unfold Approx.of_int; intros. + unfold Approx.of_int; intros. + destruct (Int.eq_dec n Int.zero); simpl. subst; auto. + destruct (Int.eq_dec n Int.one); simpl. subst; auto. destruct (Int.eq_dec n (Int.zero_ext 7 n)). simpl. split. decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. @@ -1249,7 +1272,8 @@ Proof. destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto. destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto. destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto. - destruct v1; simpl; auto. destruct (Int.eq i Int.zero); auto. + destruct v1; simpl; auto. destruct (Int.eq i Int.zero); simpl; auto. + destruct v1; simpl; auto. destruct (Int.eq i Int.zero); simpl; auto. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem; auto. Qed. @@ -1273,7 +1297,13 @@ Proof. assert (Q: forall a v, val_match_approx a v -> Approx.bge Int16u a = true -> v = Val.zero_ext 16 v). intros. apply (val_match_approx_increasing Int16u a v); auto. + assert (R: forall a v, val_match_approx a v -> Approx.bge Int1 a = true -> + v = Val.zero_ext 1 v). + intros. apply (val_match_approx_increasing Int1 a v); auto. + intros; unfold Approx.bitwise_and. + destruct (Approx.bge Int1 a1) as []_eqn. simpl. apply Y; eauto. compute; auto. + destruct (Approx.bge Int1 a2) as []_eqn. simpl. apply X; eauto. compute; auto. destruct (Approx.bge Int8u a1) as []_eqn. simpl. apply Y; eauto. compute; auto. destruct (Approx.bge Int8u a2) as []_eqn. simpl. apply X; eauto. compute; auto. destruct (Approx.bge Int16u a1) as []_eqn. simpl. apply Y; eauto. compute; auto. @@ -1298,14 +1328,21 @@ Proof. simpl. rewrite Int.and_idem. auto. unfold Approx.bitwise_or. - destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) as []_eqn. + + destruct (Approx.bge Int1 a1 && Approx.bge Int1 a2) as []_eqn. destruct (andb_prop _ _ Heqb). simpl. apply X. compute; auto. + apply (val_match_approx_increasing Int1 a1 v1); auto. + apply (val_match_approx_increasing Int1 a2 v2); auto. + + destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) as []_eqn. + destruct (andb_prop _ _ Heqb0). + simpl. apply X. compute; auto. apply (val_match_approx_increasing Int8u a1 v1); auto. apply (val_match_approx_increasing Int8u a2 v2); auto. destruct (Approx.bge Int16u a1 && Approx.bge Int16u a2) as []_eqn. - destruct (andb_prop _ _ Heqb0). + destruct (andb_prop _ _ Heqb1). simpl. apply X. compute; auto. apply (val_match_approx_increasing Int16u a1 v1); auto. apply (val_match_approx_increasing Int16u a2 v2); auto. @@ -1319,7 +1356,7 @@ Lemma approx_of_binop_sound: val_match_approx a1 v1 -> val_match_approx a2 v2 -> val_match_approx (Approx.binop op a1 a2) v. Proof. - assert (OB: forall ob, val_match_approx Int7 (Val.of_optbool ob)). + assert (OB: forall ob, val_match_approx Int1 (Val.of_optbool ob)). destruct ob; simpl. destruct b; auto. auto. destruct op; intros; simpl Approx.binop; simpl in H; try (exact I); inv H. @@ -1356,6 +1393,20 @@ Proof. (* cast16signed *) assert (V: val_match_approx Int16s v) by (eapply val_match_approx_increasing; eauto). simpl in *. congruence. +(* boolval *) + assert (V: val_match_approx Int1 v) by (eapply val_match_approx_increasing; eauto). + simpl in *. + assert (v = Vundef \/ v = Vzero \/ v = Vone). + rewrite V. destruct v; simpl; auto. + assert (0 <= Int.unsigned (Int.zero_ext 1 i) < 2). + apply Int.zero_ext_range. compute; auto. + assert (Int.unsigned(Int.zero_ext 1 i) = 0 \/ Int.unsigned(Int.zero_ext 1 i) = 1) by omega. + destruct H2. + assert (Int.repr (Int.unsigned (Int.zero_ext 1 i)) = Int.repr 0) by congruence. + rewrite Int.repr_unsigned in H3. rewrite H3; auto. + assert (Int.repr (Int.unsigned (Int.zero_ext 1 i)) = Int.repr 1) by congruence. + rewrite Int.repr_unsigned in H3. rewrite H3; auto. + intuition; subst v; auto. (* singleoffloat *) assert (V: val_match_approx Float32 v) by (eapply val_match_approx_increasing; eauto). simpl in *. congruence. @@ -1401,6 +1452,7 @@ Proof. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. apply val_inject_val_of_bool. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. apply val_inject_val_of_bool. inv H; inv H0; simpl; TrivialExists. @@ -1946,9 +1998,9 @@ Proof. apply match_env_extensional with te1; auto. Qed. -Lemma var_set_self_correct: - forall cenv id ty s a f tf e le te sp lo hi m cs tm tv v m' fn k, - var_set_self cenv id ty s = OK a -> +Lemma var_set_self_correct_scalar: + forall cenv id s a f tf e le te sp lo hi m cs tm tv v m' fn k, + var_set_self cenv id s = OK a -> match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> val_inject f v tv -> Mem.inject f m tm -> @@ -1995,20 +2047,55 @@ Proof. split. auto. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). eapply match_callstack_storev_mapped; eauto. - (* var_global_scalar *) - simpl in *. - assert (chunk0 = chunk). exploit H4; eauto. congruence. subst chunk0. - assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. - exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. - exploit make_store_correct. - eapply make_globaladdr_correct; eauto. - rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. eauto. - intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]]. - exists tm'. - split. eapply star_three. constructor. eauto. constructor. traceEq. - split. auto. - rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). - eapply match_callstack_store_mapped; eauto. +Qed. + +Lemma var_set_self_correct_array: + forall cenv id s a f tf e le te sp lo hi m cs tm tv b v sz al m' fn k, + var_set_self cenv id s = OK a -> + match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> + val_inject f v tv -> + Mem.inject f m tm -> + PTree.get id e = Some(b, Varray sz al) -> + extcall_memcpy_sem sz (Zmin al 4) ge + (Vptr b Int.zero :: v :: nil) m E0 Vundef m' -> + te!(for_var id) = Some tv -> + exists f', exists tm', + star step tge (State fn a k (Vptr sp Int.zero) te tm) + E0 (State fn s k (Vptr sp Int.zero) te tm') /\ + Mem.inject f' m' tm' /\ + match_callstack f' m' tm' (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\ + inject_incr f f'. +Proof. + intros until k. + intros VS MCS VINJ MINJ KIND MEMCPY VAL. + assert (MV: match_var f id e m te sp cenv!!id). + inv MCS. inv MENV. auto. + inv MV; try congruence. rewrite KIND in H0; inv H0. + (* var_stack_array *) + unfold var_set_self in VS. rewrite <- H in VS. inv VS. + exploit match_callstack_match_globalenvs; eauto. intros [hi' MG]. + assert (external_call (EF_memcpy sz0 (Zmin al0 4)) ge (Vptr b0 Int.zero :: v :: nil) m E0 Vundef m'). + assumption. + exploit external_call_mem_inject; eauto. + eapply inj_preserves_globals; eauto. + intros [f' [vres' [tm' [EC' [VINJ' [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. + exists f'; exists tm'. + split. eapply star_step. constructor. + eapply star_step. econstructor; eauto. + constructor. apply make_stackaddr_correct. constructor. constructor. eauto. constructor. + eapply external_call_symbols_preserved_2; eauto. + exact symbols_preserved. + eexact var_info_translated. + eexact var_info_rev_translated. + apply star_one. constructor. reflexivity. traceEq. + split. auto. + split. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). + eapply match_callstack_external_call; eauto. + intros. eapply external_call_bounds; eauto. + omega. omega. + eapply external_call_nextblock_incr; eauto. + eapply external_call_nextblock_incr; eauto. + auto. Qed. (** * Correctness of stack allocation of local variables *) @@ -2032,16 +2119,15 @@ Remark assign_variable_incr: Proof. intros until sz'; simpl. destruct lv. case (Identset.mem id atk); intros. - inv H. generalize (size_chunk_pos m). intro. - generalize (align_le sz (size_chunk m) H). omega. + inv H. generalize (size_chunk_pos chunk). intro. + generalize (align_le sz (size_chunk chunk) H). omega. inv H. omega. intros. inv H. - generalize (align_le sz (array_alignment z) (array_alignment_pos z)). - assert (0 <= Zmax 0 z). apply Zmax_bound_l. omega. + generalize (align_le sz (array_alignment sz0) (array_alignment_pos sz0)). + assert (0 <= Zmax 0 sz0). apply Zmax_bound_l. omega. omega. Qed. - Remark assign_variables_incr: forall atk vars cenv sz cenv' sz', assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'. @@ -2166,7 +2252,7 @@ Proof. subst b0. congruence. rewrite OTHER in H; eauto. (* 2 info = Var_stack_array ofs *) - intros dim LV EQ. injection EQ; clear EQ; intros. rewrite <- H0. + intros dim al LV EQ. injection EQ; clear EQ; intros. rewrite <- H. assert (0 <= Zmax 0 dim). apply Zmax1. generalize (align_le sz (array_alignment dim) (array_alignment_pos dim)). intro. set (ofs := align sz (array_alignment dim)) in *. @@ -2181,7 +2267,7 @@ Proof. intros. generalize (RANGE _ _ H3). omega. intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]]. exists f1; split. auto. split. auto. split. - eapply match_callstack_alloc_left; eauto. + subst cenv'. eapply match_callstack_alloc_left; eauto. rewrite <- LV; auto. rewrite SAME; constructor. intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). @@ -2317,14 +2403,12 @@ Proof. eapply Mem.valid_block_inject_2; eauto. intros. unfold te. apply set_locals_params_defined. elim (in_app_or _ _ _ H6); intros. - elim (list_in_map_inv _ _ _ H7). intros x [A B]. - apply in_or_app; left. unfold tparams. apply List.in_map. inversion A. apply List.in_map. auto. + apply in_or_app; left. unfold tparams. apply List.in_map. + change id with (fst (id, lv)). apply List.in_map. auto. apply in_or_app; right. apply in_or_app; left. unfold tvars. apply List.in_map. change id with (fst (id, lv)). apply List.in_map; auto. (* norepet *) - unfold fn_variables. - rewrite List.map_app. rewrite list_map_compose. simpl. - assumption. + unfold fn_variables. rewrite List.map_app. assumption. (* undef *) intros. unfold empty_env. apply PTree.gempty. Qed. @@ -2333,17 +2417,23 @@ Qed. to store in memory the values of parameters that are stack-allocated. *) Inductive vars_vals_match (f:meminj): - list (ident * memory_chunk) -> list val -> env -> Prop := + list (ident * var_kind) -> list val -> env -> Prop := | vars_vals_nil: forall te, vars_vals_match f nil nil te - | vars_vals_cons: + | vars_vals_scalar: forall te id chunk vars v vals tv, te!(for_var id) = Some tv -> val_inject f v tv -> val_normalized v chunk -> vars_vals_match f vars vals te -> - vars_vals_match f ((id, chunk) :: vars) (v :: vals) te. + vars_vals_match f ((id, Vscalar chunk) :: vars) (v :: vals) te + | vars_vals_array: + forall te id sz al vars v vals tv, + te!(for_var id) = Some tv -> + val_inject f v tv -> + vars_vals_match f vars vals te -> + vars_vals_match f ((id, Varray sz al) :: vars) (v :: vals) te. Lemma vars_vals_match_extensional: forall f vars vals te, @@ -2357,88 +2447,120 @@ Proof. econstructor; eauto. rewrite <- H. eauto with coqlib. apply IHvars_vals_match. intros. eapply H3; eauto with coqlib. + econstructor; eauto. + rewrite <- H. eauto with coqlib. + apply IHvars_vals_match. intros. eapply H2; eauto with coqlib. +Qed. + +Lemma vars_vals_match_incr: + forall f f', inject_incr f f' -> + forall vars vals te, + vars_vals_match f vars vals te -> + vars_vals_match f' vars vals te. +Proof. + induction 2; intros; econstructor; eauto. Qed. Lemma store_parameters_correct: forall e le te m1 params vl m2, - bind_parameters e m1 params vl m2 -> + bind_parameters ge e m1 params vl m2 -> forall s f cenv tf sp lo hi cs tm1 fn k, vars_vals_match f params vl te -> - list_norepet (List.map param_name params) -> + list_norepet (List.map variable_name params) -> Mem.inject f m1 tm1 -> match_callstack f m1 tm1 (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m1) (Mem.nextblock tm1) -> store_parameters cenv params = OK s -> - exists tm2, + exists f', exists tm2, star step tge (State fn s k (Vptr sp Int.zero) te tm1) E0 (State fn Sskip k (Vptr sp Int.zero) te tm2) - /\ Mem.inject f m2 tm2 - /\ match_callstack f m2 tm2 (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m2) (Mem.nextblock tm2). + /\ Mem.inject f' m2 tm2 + /\ match_callstack f' m2 tm2 (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m2) (Mem.nextblock tm2) + /\ inject_incr f f'. Proof. induction 1. (* base case *) intros; simpl. monadInv H3. - exists tm1. split. constructor. tauto. - (* inductive case *) + exists f; exists tm1. split. constructor. auto. + (* scalar case *) intros until k. intros VVM NOREPET MINJ MATCH STOREP. - monadInv STOREP. - inv VVM. - inv NOREPET. - exploit var_set_self_correct; eauto. + monadInv STOREP. inv VVM. inv NOREPET. + exploit var_set_self_correct_scalar; eauto. econstructor; eauto. econstructor; eauto. intros [tm2 [EXEC1 [MINJ1 MATCH1]]]. exploit IHbind_parameters; eauto. - intros [tm3 [EXEC2 [MINJ2 MATCH2]]]. - exists tm3. + intros [f' [tm3 [EXEC2 [MINJ2 [MATCH2 INCR2]]]]]. + exists f'; exists tm3. split. eapply star_trans; eauto. auto. -Qed. + (* array case *) + intros until k. intros VVM NOREPET MINJ MATCH STOREP. + monadInv STOREP. inv VVM. inv NOREPET. + exploit var_set_self_correct_array; eauto. + intros [f2 [tm2 [EXEC1 [MINJ1 [MATCH1 INCR1]]]]]. + exploit IHbind_parameters. eapply vars_vals_match_incr; eauto. auto. eauto. eauto. eauto. + intros [f3 [tm3 [EXEC2 [MINJ2 [MATCH2 INCR2]]]]]. + exists f3; exists tm3. + split. eapply star_trans; eauto. + split. auto. split. auto. eapply inject_incr_trans; eauto. +Qed. + +Definition val_normalized' (v: val) (vk: var_kind) : Prop := + match vk with + | Vscalar chunk => val_normalized v chunk + | Varray _ _ => True + end. Lemma vars_vals_match_holds_1: forall f params args targs, - list_norepet (List.map param_name params) -> + list_norepet (List.map variable_name params) -> val_list_inject f args targs -> - list_forall2 val_normalized args (List.map param_chunk params) -> + list_forall2 val_normalized' args (List.map variable_kind params) -> vars_vals_match f params args - (set_params targs (List.map for_var (List.map param_name params))). + (set_params targs (List.map for_var (List.map variable_name params))). Proof. Opaque for_var. induction params; simpl; intros. inv H1. constructor. inv H. inv H1. inv H0. - destruct a as [id chunk]; simpl in *. econstructor. - rewrite PTree.gss. reflexivity. - auto. auto. + destruct a as [id vk]; simpl in *. + assert (R: vars_vals_match f params al + (PTree.set (for_var id) v' + (set_params vl' (map for_var (map variable_name params))))). apply vars_vals_match_extensional - with (set_params vl' (map for_var (map param_name params))). + with (set_params vl' (map for_var (map variable_name params))). eapply IHparams; eauto. Transparent for_var. intros. apply PTree.gso. unfold for_var; red; intros. inv H0. - elim H4. change id with (param_name (id, lv)). apply List.in_map; auto. + elim H4. change id with (variable_name (id, lv)). apply List.in_map; auto. + + destruct vk; red in H6. + econstructor. rewrite PTree.gss. reflexivity. auto. auto. auto. + econstructor. rewrite PTree.gss. reflexivity. auto. auto. Qed. Lemma vars_vals_match_holds_2: forall f params args e, vars_vals_match f params args e -> forall vl, - (forall id1 id2, In id1 (List.map param_name params) -> In id2 vl -> for_var id1 <> id2) -> + (forall id1 id2, In id1 (List.map variable_name params) -> In id2 vl -> for_var id1 <> id2) -> vars_vals_match f params args (set_locals vl e). Proof. induction vl; simpl; intros. auto. apply vars_vals_match_extensional with (set_locals vl e); auto. intros. apply PTree.gso. apply H0. - change id with (param_name (id, lv)). apply List.in_map. auto. + change id with (variable_name (id, lv)). apply List.in_map. auto. auto. Qed. Lemma vars_vals_match_holds: forall f params args targs vars temps, - list_norepet (List.map param_name params ++ vars) -> + list_norepet (List.map variable_name params ++ vars) -> val_list_inject f args targs -> - list_forall2 val_normalized args (List.map param_chunk params) -> + list_forall2 val_normalized' args (List.map variable_kind params) -> vars_vals_match f params args (set_locals (List.map for_var vars ++ List.map for_temp temps) - (set_params targs (List.map for_var (List.map param_name params)))). + (set_params targs (List.map for_var (List.map variable_name params)))). Proof. intros. rewrite list_norepet_app in H. destruct H as [A [B C]]. apply vars_vals_match_holds_2; auto. apply vars_vals_match_holds_1; auto. @@ -2452,12 +2574,13 @@ Qed. Remark bind_parameters_normalized: forall e m params args m', - bind_parameters e m params args m' -> - list_forall2 val_normalized args (List.map param_chunk params). + bind_parameters ge e m params args m' -> + list_forall2 val_normalized' args (List.map variable_kind params). Proof. induction 1; simpl. constructor. constructor; auto. + constructor; auto. red; auto. Qed. (** The main result in this section: the behaviour of function entry @@ -2470,7 +2593,7 @@ Lemma function_entry_ok: forall fn m e m1 vargs m2 f cs tm cenv tf tm1 sp tvargs s fn' k, list_norepet (fn_params_names fn ++ fn_vars_names fn) -> alloc_variables empty_env m (fn_variables fn) e m1 -> - bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> + bind_parameters ge e m1 fn.(Csharpminor.fn_params) vargs m2 -> match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> build_compilenv gce fn = (cenv, tf.(fn_stackspace)) -> tf.(fn_stackspace) <= Int.max_unsigned -> @@ -2504,8 +2627,9 @@ Proof. exploit store_parameters_correct. eauto. eauto. eapply list_norepet_append_left; eauto. eexact MINJ1. eexact MATCH1. eauto. - intros [tm2 [EXEC [MINJ2 MATCH2]]]. - exists f1; exists tm2. eauto. + intros [f2 [tm2 [EXEC [MINJ2 [MATCH2 INCR2]]]]]. + exists f2; exists tm2. + split; eauto. split; auto. split; auto. eapply inject_incr_trans; eauto. Qed. (** * Semantic preservation for the translation *) @@ -2888,8 +3012,8 @@ Proof. Qed. Remark find_label_var_set_self: - forall id ty s0 s k, - var_set_self cenv id ty s0 = OK s -> + forall id s0 s k, + var_set_self cenv id s0 = OK s -> find_label lbl s k = find_label lbl s0 k. Proof. intros. unfold var_set_self in H. @@ -3114,6 +3238,35 @@ Proof. eapply match_Kcall with (cenv' := cenv); eauto. red; auto. +(* builtin *) + monadInv TR. + exploit transl_exprlist_correct; eauto. + intros [tvargs [EVAL2 VINJ2]]. + exploit match_callstack_match_globalenvs; eauto. intros [hi' MG]. + exploit external_call_mem_inject; eauto. + eapply inj_preserves_globals; eauto. + intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. + left; econstructor; split. + apply plus_one. econstructor. eauto. + eapply external_call_symbols_preserved_2; eauto. + exact symbols_preserved. + eexact var_info_translated. + eexact var_info_rev_translated. + assert (MCS': match_callstack f' m' tm' + (Frame cenv tfn e le te sp lo hi :: cs) + (Mem.nextblock m') (Mem.nextblock tm')). + apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). + eapply match_callstack_external_call; eauto. + intros. eapply external_call_bounds; eauto. + omega. omega. + eapply external_call_nextblock_incr; eauto. + eapply external_call_nextblock_incr; eauto. + econstructor; eauto. +Opaque PTree.set. + unfold set_optvar. destruct optid; simpl. + eapply match_callstack_set_temp; eauto. + auto. + (* seq *) monadInv TR. left; econstructor; split. @@ -3256,8 +3409,8 @@ Proof. apply plus_one. econstructor. eapply external_call_symbols_preserved_2; eauto. exact symbols_preserved. - eexact (Genv.find_var_info_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). - eexact (Genv.find_var_info_rev_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). + eexact var_info_translated. + eexact var_info_rev_translated. econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. -- cgit