From 82f9d1f96b30106a338e77ec83b7321c2c65f929 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 17 May 2016 15:37:56 +0200 Subject: Introduce register pairs to describe calling conventions more precisely This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly. --- backend/Allocproof.v | 302 +++++++++++++++++++++++---------------------------- 1 file changed, 138 insertions(+), 164 deletions(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index bf60a57f..154c1e2e 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -415,12 +415,10 @@ Lemma add_equations_args_satisf: satisf rs ls e' -> satisf rs ls e. Proof. intros until e'. functional induction (add_equations_args rl tyl ll e); intros. - inv H; auto. - eapply add_equation_satisf. eapply add_equation_satisf. eauto. - eapply add_equation_satisf. eauto. - eapply add_equation_satisf. eauto. - eapply add_equation_satisf. eauto. - congruence. +- inv H; auto. +- eapply add_equation_satisf; eauto. +- eapply add_equation_satisf. eapply add_equation_satisf. eauto. +- congruence. Qed. Lemma val_longofwords_eq: @@ -438,22 +436,18 @@ Lemma add_equations_args_lessdef: add_equations_args rl tyl ll e = Some e' -> satisf rs ls e' -> Val.has_type_list (rs##rl) tyl -> - Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)). + Val.lessdef_list (rs##rl) (map (fun p => Locmap.getpair p ls) ll). Proof. intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros. - inv H; auto. +- destruct H1. constructor; auto. + eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto. - destruct H1. constructor; auto. rewrite <- (val_longofwords_eq (rs#r1)); auto. apply Val.longofwords_lessdef. eapply add_equation_lessdef with (q := Eq High r1 l1). eapply add_equation_satisf. eapply add_equations_args_satisf; eauto. eapply add_equation_lessdef with (q := Eq Low r1 l2). eapply add_equations_args_satisf; eauto. -- destruct H1. constructor; auto. - eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto. -- destruct H1. constructor; auto. - eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto. -- destruct H1. constructor; auto. - eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto. - discriminate. Qed. @@ -475,13 +469,13 @@ Proof. Qed. Lemma remove_equation_res_satisf: - forall rs ls r oty ll e e', - remove_equations_res r oty ll e = Some e' -> + forall rs ls r l e e', + remove_equations_res r l e = Some e' -> satisf rs ls e -> satisf rs ls e'. Proof. intros. functional inversion H. - apply remove_equation_satisf. apply remove_equation_satisf; auto. apply remove_equation_satisf; auto. + apply remove_equation_satisf. apply remove_equation_satisf; auto. Qed. Remark select_reg_l_monotone: @@ -668,50 +662,36 @@ Proof. Qed. Lemma parallel_assignment_satisf_2: - forall rs ls res mres' oty e e' v v', - let res' := map R mres' in - remove_equations_res res oty res' e = Some e' -> + forall rs ls res res' e e' v v', + remove_equations_res res res' e = Some e' -> satisf rs ls e' -> reg_unconstrained res e' = true -> - forallb (fun l => loc_unconstrained l e') res' = true -> + forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true -> Val.lessdef v v' -> - satisf (rs#res <- v) (Locmap.setlist res' (encode_long oty v') ls) e. + satisf (rs#res <- v) (Locmap.setpair res' v' ls) e. Proof. - intros; red; intros. - assert (ISREG: forall l, In l res' -> exists mr, l = R mr). - { unfold res'; intros. exploit list_in_map_inv; eauto. intros [mr [A B]]. exists mr; auto. } - functional inversion H. + intros. functional inversion H. +- (* One location *) + subst. simpl in H2. InvBooleans. simpl. + apply parallel_assignment_satisf with Full; auto. + unfold reg_loc_unconstrained. rewrite H1, H4. auto. - (* Two 32-bit halves *) subst. - set (e' := remove_equation {| ekind := Low; ereg := res; eloc := l2 |} - (remove_equation {| ekind := High; ereg := res; eloc := l1 |} e)) in *. - rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl. - destruct (OrderedEquation.eq_dec q (Eq Low res l2)). - subst q; simpl. rewrite Regmap.gss. - destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. + set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |} + (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *. + simpl in H2. InvBooleans. simpl. + red; intros. + destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto. - destruct (OrderedEquation.eq_dec q (Eq High res l1)). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. - destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. + destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. rewrite Locmap.gss. apply Val.hiword_lessdef; auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. rewrite Regmap.gso. rewrite ! Locmap.gso. auto. eapply loc_unconstrained_sound; eauto. eapply loc_unconstrained_sound; eauto. eapply reg_unconstrained_sound; eauto. -- (* One location *) - subst. rewrite <- H5 in H2. simpl in H2. InvBooleans. - replace (encode_long oty v') with (v' :: nil). - set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *. - destruct (OrderedEquation.eq_dec q (Eq Full res l1)). - subst q; simpl. rewrite Regmap.gss. - destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. - auto. - assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. - simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto. - eapply loc_unconstrained_sound; eauto. - eapply reg_unconstrained_sound; eauto. - destruct oty as [[]|]; reflexivity || contradiction. Qed. Lemma in_subst_reg: @@ -1101,21 +1081,20 @@ Proof. Qed. Lemma add_equations_res_lessdef: - forall r oty ll e e' rs ls, - add_equations_res r oty ll e = Some e' -> + forall r oty l e e' rs ls, + add_equations_res r oty l e = Some e' -> satisf rs ls e' -> - Val.lessdef_list (encode_long oty rs#r) (map ls ll). -Proof. - intros. functional inversion H. -- subst. simpl. constructor. - eapply add_equation_lessdef with (q := Eq High r l1). + Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) -> + Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls). +Proof. + intros. functional inversion H; simpl. +- subst. eapply add_equation_lessdef with (q := Eq Full r (R mr)); eauto. +- subst. rewrite <- (val_longofwords_eq rs#r) by auto. + apply Val.longofwords_lessdef. + eapply add_equation_lessdef with (q := Eq High r (R mr1)). eapply add_equation_satisf. eauto. - constructor. - eapply add_equation_lessdef with (q := Eq Low r l2). eauto. - constructor. -- subst. replace (encode_long oty rs#r) with (rs#r :: nil). simpl. constructor; auto. - eapply add_equation_lessdef with (q := Eq Full r l1); eauto. - destruct oty as [[]|]; reflexivity || contradiction. + eapply add_equation_lessdef with (q := Eq Low r (R mr2)). + eauto. Qed. Definition callee_save_loc (l: loc) := @@ -1149,47 +1128,60 @@ Proof. lazy beta. destruct (eloc q). auto. destruct sl; congruence. Qed. +Lemma val_hiword_longofwords: + forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1. +Proof. + intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword. + rewrite Int64.hi_ofwords. auto. +Qed. + +Lemma val_loword_longofwords: + forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2. +Proof. + intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword. + rewrite Int64.lo_ofwords. auto. +Qed. + Lemma function_return_satisf: forall rs ls_before ls_after res res' sg e e' v, - res' = map R (loc_result sg) -> - remove_equations_res res (sig_res sg) res' e = Some e' -> + res' = loc_result sg -> + remove_equations_res res res' e = Some e' -> satisf rs ls_before e' -> - forallb (fun l => reg_loc_unconstrained res l e') res' = true -> + forallb (fun l => reg_loc_unconstrained res l e') (map R (regs_of_rpair res')) = true -> no_caller_saves e' = true -> - Val.lessdef_list (encode_long (sig_res sg) v) (map ls_after res') -> + Val.lessdef v (Locmap.getpair (map_rpair R res') ls_after) -> agree_callee_save ls_before ls_after -> satisf (rs#res <- v) ls_after e. Proof. intros; red; intros. functional inversion H0. -- subst. rewrite <- H11 in *. unfold encode_long in H4. rewrite <- H7 in H4. - simpl in H4. inv H4. inv H14. - set (e' := remove_equation {| ekind := Low; ereg := res; eloc := l2 |} - (remove_equation {| ekind := High; ereg := res; eloc := l1 |} e)) in *. - simpl in H2. InvBooleans. - destruct (OrderedEquation.eq_dec q (Eq Low res l2)). - subst q; simpl. rewrite Regmap.gss. auto. - destruct (OrderedEquation.eq_dec q (Eq High res l1)). - subst q; simpl. rewrite Regmap.gss. auto. - assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. - exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B]. - exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D]. - rewrite Regmap.gso; auto. - exploit no_caller_saves_sound; eauto. intros. - red in H5. rewrite <- H5; auto. -- subst. rewrite <- H11 in *. - replace (encode_long (sig_res sg) v) with (v :: nil) in H4. - simpl in H4. inv H4. - simpl in H2. InvBooleans. - set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *. - destruct (OrderedEquation.eq_dec q (Eq Full res l1)). +- (* One register *) + subst. rewrite <- H8 in *. simpl in *. InvBooleans. + set (e' := remove_equation {| ekind := Full; ereg := res; eloc := R mr |} e) in *. + destruct (OrderedEquation.eq_dec q (Eq Full res (R mr))). subst q; simpl. rewrite Regmap.gss; auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. exploit reg_loc_unconstrained_sound; eauto. intros [A B]. rewrite Regmap.gso; auto. exploit no_caller_saves_sound; eauto. intros. red in H5. rewrite <- H5; auto. - destruct (sig_res sg) as [[]|]; reflexivity || contradiction. +- (* Two 32-bit halves *) + subst. rewrite <- H9 in *. simpl in *. + set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |} + (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *. + InvBooleans. + destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). + subst q; simpl. rewrite Regmap.gss. + eapply Val.lessdef_trans. apply Val.loword_lessdef. eauto. apply val_loword_longofwords. + destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))). + subst q; simpl. rewrite Regmap.gss. + eapply Val.lessdef_trans. apply Val.hiword_lessdef. eauto. apply val_hiword_longofwords. + assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. + exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B]. + exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D]. + rewrite Regmap.gso; auto. + exploit no_caller_saves_sound; eauto. intros. + red in H5. rewrite <- H5; auto. Qed. Lemma compat_left_sound: @@ -1225,31 +1217,22 @@ Proof. exact (select_reg_h_monotone r). Qed. -Lemma val_hiword_longofwords: - forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1. -Proof. - intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword. - rewrite Int64.hi_ofwords. auto. -Qed. - -Lemma val_loword_longofwords: - forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2. -Proof. - intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword. - rewrite Int64.lo_ofwords. auto. -Qed. - Lemma compat_entry_satisf: - forall rl tyl ll e, - compat_entry rl tyl ll e = true -> + forall rl ll e, + compat_entry rl ll e = true -> forall vl ls, - Val.lessdef_list vl (decode_longs tyl (map ls ll)) -> + Val.lessdef_list vl (map (fun p => Locmap.getpair p ls) ll) -> satisf (init_regs vl rl) ls e. Proof. - intros until e. functional induction (compat_entry rl tyl ll e); intros. + intros until e. functional induction (compat_entry rl ll e); intros. - (* no params *) simpl. red; intros. rewrite Regmap.gi. destruct (ekind q); simpl; auto. -- (* a param of type Tlong *) +- (* a param in a single location *) + InvBooleans. simpl in H0. inv H0. simpl. + red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). + exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto. + eapply IHb; eauto. +- (* a param split across two locations *) InvBooleans. simpl in H0. inv H0. simpl. red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). exploit compat_left2_sound; eauto. @@ -1259,47 +1242,37 @@ Proof. apply Val.lessdef_trans with (Val.loword (Val.longofwords (ls l1) (ls l2))). apply Val.loword_lessdef; auto. apply val_loword_longofwords. eapply IHb; eauto. -- (* a param of type Tint *) - InvBooleans. simpl in H0. inv H0. simpl. - red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). - exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto. - eapply IHb; eauto. -- (* a param of type Tfloat *) - InvBooleans. simpl in H0. inv H0. simpl. - red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). - exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto. - eapply IHb; eauto. -- (* a param of type Tsingle *) - InvBooleans. simpl in H0. inv H0. simpl. - red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). - exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto. - eapply IHb; eauto. - (* error case *) discriminate. Qed. Lemma call_regs_param_values: forall sg ls, - map (call_regs ls) (loc_parameters sg) = map ls (loc_arguments sg). + map (fun p => Locmap.getpair p (call_regs ls)) (loc_parameters sg) + = map (fun p => Locmap.getpair p ls) (loc_arguments sg). Proof. intros. unfold loc_parameters. rewrite list_map_compose. - apply list_map_exten; intros. unfold call_regs, parameter_of_argument. - exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable. - destruct x; auto. destruct sl; tauto. + apply list_map_exten; intros. symmetry. + assert (A: forall l, loc_argument_acceptable l -> call_regs ls (parameter_of_argument l) = ls l). + { destruct l as [r | [] ofs ty]; simpl; auto; contradiction. } + exploit loc_arguments_acceptable; eauto. destruct x; simpl; intros. +- auto. +- destruct H0; f_equal; auto. Qed. Lemma return_regs_arg_values: forall sg ls1 ls2, tailcall_is_possible sg = true -> - map (return_regs ls1 ls2) (loc_arguments sg) = map ls2 (loc_arguments sg). -Proof. - intros. apply list_map_exten; intros. - exploit loc_arguments_acceptable; eauto. - exploit tailcall_is_possible_correct; eauto. - unfold loc_argument_acceptable, return_regs. - destruct x; intros. - rewrite H2; auto. - contradiction. + map (fun p => Locmap.getpair p (return_regs ls1 ls2)) (loc_arguments sg) + = map (fun p => Locmap.getpair p ls2) (loc_arguments sg). +Proof. + intros. + apply tailcall_is_possible_correct in H. + apply list_map_exten; intros. + apply Locmap.getpair_exten; intros. + assert (In l (regs_of_rpairs (loc_arguments sg))) by (eapply in_regs_of_rpairs; eauto). + exploit loc_arguments_acceptable_2; eauto. exploit H; eauto. + destruct l; simpl; intros; try contradiction. rewrite H4; auto. Qed. Lemma find_function_tailcall: @@ -1542,7 +1515,7 @@ Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop := wf_moves mv -> transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> track_moves env mv e1 = Some e2 -> - compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true -> + compat_entry (RTL.fn_params f) (loc_parameters (fn_sig tf)) e2 = true -> can_undef destroyed_at_function_entry e2 = true -> RTL.fn_stacksize f = LTL.fn_stacksize tf -> RTL.fn_sig f = LTL.fn_sig tf -> @@ -1702,7 +1675,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa (WTRS: wt_regset env rs) (WTRES: env res = proj_sig_res sg) (STEPS: forall v ls1 m, - Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) -> + Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) -> Val.has_type v (env res) -> agree_callee_save ls ls1 -> exists ls2, @@ -1731,7 +1704,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := forall s f args m ts tf ls m' (STACKS: match_stackframes s ts (funsig tf)) (FUN: transf_fundef f = OK tf) - (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf))))) + (ARGS: Val.lessdef_list args (map (fun p => Locmap.getpair p ls) (loc_arguments (funsig tf)))) (AG: agree_callee_save (parent_locset ts) ls) (MEM: Mem.extends m m') (WTARGS: Val.has_type_list args (sig_args (funsig tf))), @@ -1740,7 +1713,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := | match_states_return: forall s res m ts ls m' sg (STACKS: match_stackframes s ts sg) - (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg)))) + (RES: Val.lessdef res (Locmap.getpair (map_rpair R (loc_result sg)) ls)) (AG: agree_callee_save (parent_locset ts) ls) (MEM: Mem.extends m m') (WTRES: Val.has_type res (proj_sig_res sg)), @@ -2089,7 +2062,7 @@ Proof. (* call *) - set (sg := RTL.funsig fd) in *. set (args' := loc_arguments sg) in *. - set (res' := map R (loc_result sg)) in *. + set (res' := loc_result sg) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. intros [tfd [E F]]. @@ -2203,7 +2176,6 @@ Proof. eapply star_right. eexact A1. econstructor. eauto. eauto. traceEq. simpl. econstructor; eauto. - unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto. apply return_regs_agree_callee_save. constructor. + (* with an argument *) @@ -2213,11 +2185,15 @@ Proof. eapply star_right. eexact A1. econstructor. eauto. eauto. traceEq. simpl. econstructor; eauto. rewrite <- H11. - replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f)))) - with (map ls1 (map R (loc_result (RTL.fn_sig f)))). + replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) + (return_regs (parent_locset ts) ls1)) + with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). eapply add_equations_res_lessdef; eauto. - rewrite !list_map_compose. apply list_map_exten; intros. - unfold return_regs. erewrite loc_result_caller_save by eauto. auto. + rewrite H13. apply WTRS. + generalize (loc_result_caller_save (RTL.fn_sig f)). + destruct (loc_result (RTL.fn_sig f)); simpl. + intros A; rewrite A; auto. + intros [A B]; rewrite A, B; auto. apply return_regs_agree_callee_save. unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS. @@ -2230,7 +2206,7 @@ Proof. { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. } exploit (exec_moves mv). eauto. eauto. eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. - rewrite call_regs_param_values. rewrite H9. eexact ARGS. + rewrite call_regs_param_values. eexact ARGS. exact WTRS. intros [ls1 [A B]]. econstructor; split. @@ -2246,22 +2222,20 @@ Proof. simpl in FUN; inv FUN. econstructor; split. apply plus_one. econstructor; eauto. - eapply external_call_symbols_preserved' with (ge1 := ge). - econstructor; eauto. apply senv_preserved. - econstructor; eauto. simpl. - replace (map - (Locmap.setlist (map R (loc_result (ef_sig ef))) - (encode_long (sig_res (ef_sig ef)) v') ls) - (map R (loc_result (ef_sig ef)))) - with (encode_long (sig_res (ef_sig ef)) v'). - apply encode_long_lessdef; auto. - unfold encode_long, loc_result. - destruct (sig_res (ef_sig ef)) as [[]|]; simpl; symmetry; f_equal; auto. - red; intros. rewrite Locmap.gsetlisto. apply AG; auto. - apply Loc.notin_iff. intros. - exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'. - destruct l; simpl; auto. red in H0. apply loc_result_caller_save in B. congruence. - simpl. eapply external_call_well_typed; eauto. + eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved. + econstructor; eauto. + simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl. + rewrite Locmap.gss; auto. + generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D). + exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'. + rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. + rewrite val_longofwords_eq by auto. auto. + red; intros. rewrite (AG l H0). + symmetry; apply Locmap.gpo. + assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). + { intros. destruct l; simpl in *. congruence. auto. } + generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto. + eapply external_call_well_typed; eauto. (* return *) - inv STACKS. @@ -2287,7 +2261,7 @@ Proof. congruence. constructor; auto. constructor. rewrite SIG; rewrite H3; auto. - rewrite SIG; rewrite H3; simpl; auto. + rewrite SIG, H3, loc_arguments_main. auto. red; auto. apply Mem.extends_refl. rewrite SIG, H3. constructor. @@ -2297,9 +2271,9 @@ Lemma final_states_simulation: forall st1 st2 r, match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r. Proof. - intros. inv H0. inv H. inv STACKS. - econstructor. simpl; reflexivity. - unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto. + intros. inv H0. inv H. inv STACKS. + econstructor. + unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. auto. Qed. Lemma wt_prog: wt_program prog. -- cgit