diff options
| -rw-r--r-- | backend/Allocproof.v | 295 | ||||
| -rw-r--r-- | backend/LTL.v | 144 | ||||
| -rw-r--r-- | backend/LTLin.v | 63 | ||||
| -rw-r--r-- | backend/Linear.v | 46 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 25 | ||||
| -rw-r--r-- | backend/Reloadproof.v | 447 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 12 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 29 |
8 files changed, 538 insertions, 523 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 051be1e..fd569ad 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -37,6 +37,7 @@ Require Import Allocation. (** * Semantic properties of calling conventions *) +(************* (** The value of a parameter in the called function is the same as the value of the corresponding argument in the caller function. *) @@ -118,6 +119,7 @@ Proof. symmetry. apply Locmap.gso. eapply Loc.in_notin_diff; eauto. intros x [A B]. rewrite Locmap.gso; auto. apply Loc.diff_sym; auto. Qed. +****************) (** * Properties of allocated locations *) @@ -220,7 +222,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign. of [assign r] can be arbitrary. *) Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := - forall (r: reg), Regset.In r live -> Val.lessdef (rs#r) (ls (assign r)). + forall (r: reg), Regset.In r live -> rs#r = ls (assign r). (** What follows is a long list of lemmas expressing properties of the [agree_live_regs] predicate that are useful for the @@ -289,7 +291,7 @@ Qed. Lemma agree_eval_reg: forall r live rs ls, - agree (reg_live r live) rs ls -> Val.lessdef (rs#r) (ls (assign r)). + agree (reg_live r live) rs ls -> rs#r = ls (assign r). Proof. intros. apply H. apply Regset.add_1. auto. Qed. @@ -299,11 +301,11 @@ Qed. Lemma agree_eval_regs: forall rl live rs ls, agree (reg_list_live rl live) rs ls -> - Val.lessdef_list (rs##rl) (List.map ls (List.map assign rl)). + rs##rl = List.map ls (List.map assign rl). Proof. induction rl; simpl; intros. - constructor. - constructor. + auto. + f_equal. apply agree_eval_reg with live. apply agree_reg_list_live with rl. auto. eapply IHrl. eexact H. @@ -345,17 +347,16 @@ Qed. are mapped to locations other than that of [r]. *) Lemma agree_assign_live: - forall live r rs ls v v', + forall live r rs ls v, (forall s, Regset.In s live -> s <> r -> assign s <> assign r) -> - Val.lessdef v v' -> agree (reg_dead r live) rs ls -> - agree live (rs#r <- v) (Locmap.set (assign r) v' ls). + agree live (rs#r <- v) (Locmap.set (assign r) v ls). Proof. unfold agree; intros. rewrite Regmap.gsspec. destruct (peq r0 r). subst r0. rewrite Locmap.gss. auto. - rewrite Locmap.gso. apply H1. apply Regset.remove_2; auto. + rewrite Locmap.gso. apply H0. apply Regset.remove_2; auto. eapply regalloc_noteq_diff. eauto. apply sym_not_equal. apply H. auto. auto. Qed. @@ -414,66 +415,70 @@ Qed. a function call, provided that the states before the call agree and that calling conventions are respected. *) -Lemma agree_call: - forall live args ros res rs v (ls ls': locset), +Lemma agree_postcall: + forall live args ros res rs v (ls: locset), (forall r, Regset.In r live -> r <> res -> ~(In (assign r) Conventions.destroyed_at_call)) -> (forall r, Regset.In r live -> r <> res -> assign r <> assign res) -> - Val.lessdef v (ls' (assign res)) -> - (forall l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) -> - ls' l = ls l) -> agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls -> - agree live (rs#res <- v) ls'. + agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_regs ls)). Proof. intros. assert (agree (reg_dead res live) rs ls). apply agree_reg_sum_live with ros. apply agree_reg_list_live with args. assumption. - red; intros. - case (Reg.eq r res); intro. - subst r. rewrite Regmap.gss. assumption. - rewrite Regmap.gso; auto. rewrite H2. apply H4. - apply Regset.remove_2; auto. - eapply regalloc_notin_notin; eauto. - eapply regalloc_acceptable; eauto. - eapply regalloc_noteq_diff; eauto. + red; intros. rewrite Regmap.gsspec. destruct (peq r res). + subst r. rewrite Locmap.gss. auto. + rewrite Locmap.gso. transitivity (ls (assign r)). + apply H2. apply Regset.remove_2; auto. + unfold postcall_regs. + assert (~In (assign r) temporaries). + apply Loc.notin_not_in. eapply regalloc_not_temporary; eauto. + assert (~In (assign r) destroyed_at_call). + apply H. auto. auto. + caseEq (assign r); auto. intros m ASG. rewrite <- ASG. + destruct (In_dec Loc.eq (assign r) temporaries). contradiction. + destruct (In_dec Loc.eq (assign r) destroyed_at_call). contradiction. + auto. + eapply regalloc_noteq_diff; eauto. apply sym_not_eq. auto. Qed. (** Agreement between the initial register set at RTL function entry and the location set at LTL function entry. *) Lemma agree_init_regs: - forall rl vl ls live, + forall live rl vl, (forall r1 r2, In r1 rl -> Regset.In r2 live -> r1 <> r2 -> assign r1 <> assign r2) -> - Val.lessdef_list vl (List.map ls (List.map assign rl)) -> - agree live (init_regs vl rl) ls. + agree live (RTL.init_regs vl rl) + (LTL.init_locs vl (List.map assign rl)). Proof. + intro live. + assert (agree live (Regmap.init Vundef) (Locmap.init Vundef)). + red; intros. rewrite Regmap.gi. auto. induction rl; simpl; intros. - red; intros. rewrite Regmap.gi. auto. - inv H0. - assert (agree live (init_regs vl1 rl) ls). - apply IHrl. intros. apply H. tauto. auto. auto. auto. - red; intros. case (Reg.eq a r); intro. - subst r. rewrite Regmap.gss. auto. - rewrite Regmap.gso; auto. + auto. + destruct vl. auto. + assert (agree live (init_regs vl rl) (init_locs vl (map assign rl))). + apply IHrl. intros. apply H0. tauto. auto. auto. + red; intros. rewrite Regmap.gsspec. destruct (peq r a). + subst r. rewrite Locmap.gss. auto. + rewrite Locmap.gso. apply H1; auto. + eapply regalloc_noteq_diff; eauto. Qed. Lemma agree_parameters: - forall vl ls, + forall vl, let params := f.(RTL.fn_params) in - Val.lessdef_list vl (List.map ls (List.map assign params)) -> agree (live0 f flive) - (init_regs vl params) - ls. + (RTL.init_regs vl params) + (LTL.init_locs vl (List.map assign params)). Proof. intros. apply agree_init_regs. intros. eapply regalloc_correct_3; eauto. - auto. Qed. End AGREE. @@ -556,52 +561,40 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> Prop | match_stackframes_nil: match_stackframes nil nil | match_stackframes_cons: - forall s ts sig res f sp pc rs ls env live assign, + forall s ts res f sp pc rs ls env live assign, match_stackframes s ts -> - sig_res (RTL.fn_sig f) = sig_res (parent_callsig ts) -> wt_function f env -> analyze f = Some live -> regalloc f live (live0 f live) env = Some assign -> - (forall rv ls1, - (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls1 l = ls l) -> - Val.lessdef rv (ls1 (R (loc_result sig))) -> + (forall rv, agree assign (transfer f pc live!!pc) (rs#res <- rv) - (Locmap.set (assign res) (ls1 (R (loc_result sig))) ls1)) -> + (Locmap.set (assign res) rv ls)) -> match_stackframes (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s) - (LTL.Stackframe sig (assign res) (transf_fun f live assign) sp ls pc :: ts). + (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts). Inductive match_states: RTL.state -> LTL.state -> Prop := | match_states_intro: - forall s f sp pc rs m ts ls tm live assign env + forall s f sp pc rs m ts ls live assign env (STACKS: match_stackframes s ts) - (SIG: sig_res(RTL.fn_sig f) = sig_res(parent_callsig ts)) (WT: wt_function f env) (ANL: analyze f = Some live) (ASG: regalloc f live (live0 f live) env = Some assign) - (AG: agree assign (transfer f pc live!!pc) rs ls) - (MMD: Mem.lessdef m tm), + (AG: agree assign (transfer f pc live!!pc) rs ls), match_states (RTL.State s (RTL.fn_code f) sp pc rs m) - (LTL.State ts (transf_fun f live assign) sp pc ls tm) + (LTL.State ts (transf_fun f live assign) sp pc ls m) | match_states_call: - forall s f args m ts tf ls tm, + forall s f args m ts tf, match_stackframes s ts -> - sig_res(RTL.funsig f) = sig_res(parent_callsig ts) -> transf_fundef f = OK tf -> - Val.lessdef_list args (List.map ls (loc_arguments (funsig tf))) -> - Mem.lessdef m tm -> - (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) -> match_states (RTL.Callstate s f args m) - (LTL.Callstate ts tf ls tm) + (LTL.Callstate ts tf args m) | match_states_return: - forall s v m ts ls tm, + forall s v m ts, match_stackframes s ts -> - Val.lessdef v (ls (R (loc_result (parent_callsig ts)))) -> - Mem.lessdef m tm -> - (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) -> match_states (RTL.Returnstate s v m) - (LTL.Returnstate ts ls tm). + (LTL.Returnstate ts v m). (** The simulation proof is by case analysis over the RTL transition taken in the source program. *) @@ -652,10 +645,9 @@ Lemma transl_find_function: transf_fundef f = OK tf. Proof. intros; destruct ros; simpl in *. - assert (Val.lessdef (rs#r) (ls (alloc r))). + assert (rs#r = ls (alloc r)). eapply agree_eval_reg. eapply agree_reg_list_live; eauto. - inv H1. apply functions_translated. auto. - exploit Genv.find_funct_inv; eauto. intros [b EQ]. congruence. + rewrite <- H1. apply functions_translated. auto. rewrite symbols_preserved. destruct (Genv.find_symbol ge i). apply function_ptr_translated. auto. discriminate. Qed. @@ -696,15 +688,11 @@ Proof. rewrite <- H1. eapply agree_move_live; eauto. (* Not a move *) intros INMO CORR CODE. - assert (exists v1, - eval_operation tge sp op (map ls (map assign args)) tm = Some v1 - /\ Val.lessdef v v1). - apply eval_operation_lessdef with m (rs##args); auto. + assert (eval_operation tge sp op (map ls (map assign args)) m = Some v). + replace (map ls (map assign args)) with (rs##args). + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. eapply agree_eval_regs; eauto. - rewrite (eval_operation_preserved symbols_preserved). assumption. - destruct H1 as [v1 [EV VMD]]. - econstructor; split. eapply exec_Lop; eauto. - MatchStates. + econstructor; split. eapply exec_Lop; eauto. MatchStates. apply agree_assign_live with f env live; auto. eapply agree_reg_list_live; eauto. (* Result is not live, instruction turned into a nop *) @@ -717,15 +705,10 @@ Proof. rewrite LV in AG. (* dst is live *) exploit Regset.mem_2; eauto. intro LV'. - assert (exists a', - eval_addressing tge sp addr (map ls (map assign args)) = Some a' - /\ Val.lessdef a a'). - apply eval_addressing_lessdef with (rs##args). - eapply agree_eval_regs; eauto. + assert (eval_addressing tge sp addr (map ls (map assign args)) = Some a). + replace (map ls (map assign args)) with (rs##args). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - destruct H2 as [a' [EVAL VMD]]. - exploit Mem.loadv_lessdef; eauto. - intros [v' [LOADV VMD2]]. + eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lload; eauto. TranslInstr. rewrite LV; auto. generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). @@ -740,106 +723,61 @@ Proof. red; intro; exploit Regset.mem_1; eauto. congruence. (* Istore *) - assert (exists a', - eval_addressing tge sp addr (map ls (map assign args)) = Some a' - /\ Val.lessdef a a'). - apply eval_addressing_lessdef with (rs##args). - eapply agree_eval_regs; eauto. + assert (eval_addressing tge sp addr (map ls (map assign args)) = Some a). + replace (map ls (map assign args)) with (rs##args). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - destruct H2 as [a' [EVAL VMD]]. - assert (ESRC: Val.lessdef rs#src (ls (assign src))). + eapply agree_eval_regs; eauto. + assert (ESRC: rs#src = ls (assign src)). eapply agree_eval_reg. eapply agree_reg_list_live. eauto. - assert (exists tm', storev chunk tm a' (ls (assign src)) = Some tm' - /\ Mem.lessdef m' tm'). - eapply Mem.storev_lessdef; eauto. - destruct H2 as [m1' [STORE MMD']]. econstructor; split. eapply exec_Lstore; eauto. TranslInstr. + rewrite <- ESRC. eauto. MatchStates. eapply agree_reg_live. eapply agree_reg_list_live. eauto. (* Icall *) exploit transl_find_function; eauto. intros [tf [TFIND TF]]. generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 CORR2]. - exploit (parmov_spec ls (map assign args) - (loc_arguments (RTL.funsig f))). - apply loc_arguments_norepet. - rewrite loc_arguments_length. inv WTI. - rewrite <- H7. repeat rewrite list_length_map. auto. - intros [PM1 PM2]. + assert (rs##args = map ls (map assign args)). + eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcall; eauto. TranslInstr. rewrite (sig_function_translated _ _ TF). eauto. - rewrite (sig_function_translated _ _ TF). + rewrite H1. econstructor; eauto. econstructor; eauto. intros. eapply agree_succ with (n := pc); eauto. unfold RTL.successors; rewrite H; auto with coqlib. - eapply agree_call with (ls := ls); eauto. - rewrite Locmap.gss. auto. - intros. rewrite Locmap.gso. rewrite H1; auto. apply PM2; auto. - eapply arguments_not_preserved; eauto. apply Loc.diff_sym; auto. - rewrite (sig_function_translated _ _ TF). - change Regset.elt with reg in PM1. - rewrite PM1. eapply agree_eval_regs; eauto. + eapply agree_postcall; eauto. (* Itailcall *) exploit transl_find_function; eauto. intros [tf [TFIND TF]]. - exploit (parmov_spec ls (map assign args) - (loc_arguments (RTL.funsig f))). - apply loc_arguments_norepet. - rewrite loc_arguments_length. inv WTI. - rewrite <- H6. repeat rewrite list_length_map. auto. - intros [PM1 PM2]. + assert (rs##args = map ls (map assign args)). + eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Ltailcall; eauto. TranslInstr. rewrite (sig_function_translated _ _ TF). eauto. - rewrite (sig_function_translated _ _ TF). - econstructor; eauto. - inv WTI. congruence. - rewrite (sig_function_translated _ _ TF). - rewrite return_regs_arguments. - change Regset.elt with reg in PM1. - rewrite PM1. eapply agree_eval_regs; eauto. - inv WTI; auto. - apply free_lessdef; auto. - intros. rewrite return_regs_not_destroyed; auto. + rewrite H1. econstructor; eauto. (* Ialloc *) - assert (Val.lessdef (Vint sz) (ls (assign arg))). - rewrite <- H0. eapply agree_eval_reg. eauto. - inversion H2. subst v. - pose (ls1 := Locmap.set (R loc_alloc_argument) (ls (assign arg)) ls). - pose (ls2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) ls1). - pose (ls3 := Locmap.set (assign res) (ls2 (R loc_alloc_result)) ls2). - caseEq (alloc tm 0 (Int.signed sz)). intros tm' b1 ALLOC1. - exploit Mem.alloc_lessdef; eauto. intros [EQ MMD1]. subst b1. - exists (State ts (transf_fun f live assign) sp pc' ls3 tm'); split. - unfold ls3, ls2, ls1. eapply exec_Lalloc; eauto. TranslInstr. + assert (ls (assign arg) = Vint sz). + rewrite <- H0. symmetry. eapply agree_eval_reg; eauto. + econstructor; split. + eapply exec_Lalloc; eauto. TranslInstr. generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). unfold correct_alloc_instr. intros [CORR1 CORR2]. MatchStates. - eapply agree_call with (args := arg :: nil) (ros := inr reg 1%positive) (ls := ls); eauto. - unfold ls3; rewrite Locmap.gss. - unfold ls2; rewrite Locmap.gss. auto. - intros. unfold ls3; rewrite Locmap.gso. - unfold ls2; rewrite Locmap.gso. - unfold ls1; apply Locmap.gso. - apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. - unfold loc_alloc_argument, destroyed_at_call; simpl; tauto. - apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. - unfold loc_alloc_result, destroyed_at_call; simpl; tauto. - apply Loc.diff_sym; auto. + eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto. (* Icond, true *) - assert (COND: eval_condition cond (map ls (map assign args)) tm = Some true). - eapply eval_condition_lessdef; eauto. + assert (COND: eval_condition cond (map ls (map assign args)) m = Some true). + replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_true; eauto. TranslInstr. MatchStates. eapply agree_reg_list_live. eauto. (* Icond, false *) - assert (COND: eval_condition cond (map ls (map assign args)) tm = Some false). - eapply eval_condition_lessdef; eauto. + assert (COND: eval_condition cond (map ls (map assign args)) m = Some false). + replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_false; eauto. TranslInstr. @@ -848,16 +786,12 @@ Proof. (* Ireturn *) econstructor; split. eapply exec_Lreturn; eauto. TranslInstr; eauto. + replace (regmap_optget or Vundef rs) + with (locmap_optget (option_map assign or) Vundef ls). econstructor; eauto. - rewrite return_regs_result. - inv WTI. destruct or; simpl in *. - replace (loc_result (parent_callsig ts)) - with (loc_result (RTL.fn_sig f)). - rewrite Locmap.gss. eapply agree_eval_reg; eauto. - unfold loc_result. rewrite SIG. auto. - constructor. - apply free_lessdef; auto. - intros. apply return_regs_not_destroyed; auto. + inv WTI. destruct or; simpl in *. + symmetry; eapply agree_eval_reg; eauto. + auto. (* internal function *) generalize H7. simpl. unfold transf_function. @@ -866,46 +800,21 @@ Proof. caseEq (analyze f); simpl; try congruence. intros live ANL. caseEq (regalloc f live (live0 f live) env); simpl; try congruence. intros alloc ALLOC EQ. inv EQ. simpl in *. - caseEq (Mem.alloc tm 0 (RTL.fn_stacksize f)). intros tm' stk' MEMALLOC. - exploit alloc_lessdef; eauto. intros [EQ LDM]. subst stk'. econstructor; split. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. - apply agree_init_regs. intros; eapply regalloc_correct_3; eauto. - inv WTF. - exploit (parmov_spec (call_regs ls) - (loc_parameters (RTL.fn_sig f)) - (map alloc (RTL.fn_params f))). - eapply regalloc_norepet_norepet; eauto. - eapply regalloc_correct_2; eauto. - rewrite loc_parameters_length. symmetry. - transitivity (length (map env (RTL.fn_params f))). - repeat rewrite list_length_map. auto. - rewrite wt_params; auto. - intros [PM1 PM2]. - change Regset.elt with reg in PM1. rewrite PM1. - replace (map (call_regs ls) (loc_parameters (RTL.fn_sig f))) - with (map ls (loc_arguments (RTL.fn_sig f))). - auto. - symmetry. unfold loc_parameters. rewrite list_map_compose. - apply list_map_exten. intros. symmetry. eapply call_regs_param_of_arg; eauto. + change (transfer f (RTL.fn_entrypoint f) live !! (RTL.fn_entrypoint f)) + with (live0 f live). + eapply agree_parameters; eauto. (* external function *) injection H7; intro EQ; inv EQ. - exploit event_match_lessdef; eauto. intros [tres [A B]]. econstructor; split. eapply exec_function_external; eauto. eapply match_states_return; eauto. - replace (loc_result (parent_callsig ts)) - with (loc_result (ef_sig ef)). - rewrite Locmap.gss. auto. - unfold loc_result. rewrite <- H6. auto. - intros. rewrite <- H11; auto. apply Locmap.gso. - apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. - apply loc_result_caller_save. (* return *) - inv H3. + inv H4. econstructor; split. eapply exec_return; eauto. econstructor; eauto. @@ -920,27 +829,21 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. - assert (SIG2: funsig tf = mksignature nil (Some Tint)). - rewrite <- H2. apply sig_function_translated; auto. - assert (VPARAMS: Val.lessdef_list nil (map (Locmap.init Vundef) (loc_arguments (funsig tf)))). - rewrite SIG2. simpl. constructor. - assert (GENV: (Genv.init_mem tprog) = (Genv.init_mem prog)). + assert (MEM: (Genv.init_mem tprog) = (Genv.init_mem prog)). exact (Genv.init_mem_transf_partial _ _ TRANSF). - assert (MMD: Mem.lessdef (Genv.init_mem prog) (Genv.init_mem tprog)). - rewrite GENV. apply Mem.lessdef_refl. - exists (LTL.Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split. + exists (LTL.Callstate nil tf nil (Genv.init_mem tprog)); split. econstructor; eauto. rewrite symbols_preserved. rewrite (transform_partial_program_main _ _ TRANSF). auto. - constructor; auto. constructor. rewrite H2; auto. + rewrite <- H2. apply sig_function_translated; auto. + rewrite MEM. constructor; auto. constructor. Qed. Lemma transf_final_states: 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 H3. econstructor. - simpl in H4. inv H4. auto. + intros. inv H0. inv H. inv H4. econstructor. Qed. Theorem transf_program_correct: diff --git a/backend/LTL.v b/backend/LTL.v index a082e12..e39a4ec 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -72,53 +72,20 @@ Definition funsig (fd: fundef) := Definition genv := Genv.t fundef. Definition locset := Locmap.t. -Section RELSEM. - -(** Calling conventions are reflected at the level of location sets - (environments mapping locations to values) by the following two - functions. +Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val := + match ol with + | None => dfl + | Some l => ls l + end. - [call_regs caller] returns the location set at function entry, - as a function of the location set [caller] of the calling function. -- Machine registers have the same values as in the caller. -- Incoming stack slots (used for parameter passing) have the same - values as the corresponding outgoing stack slots (used for argument - passing) in the caller. -- Local and outgoing stack slots are initialized to undefined values. -*) +Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset := + match rl, vl with + | r1 :: rs, v1 :: vs => Locmap.set r1 v1 (init_locs vs rs) + | _, _ => Locmap.init Vundef + end. -Definition call_regs (caller: locset) : locset := - fun (l: loc) => - match l with - | R r => caller (R r) - | S (Local ofs ty) => Vundef - | S (Incoming ofs ty) => caller (S (Outgoing ofs ty)) - | S (Outgoing ofs ty) => Vundef - end. -(** [return_regs caller callee] returns the location set after - a call instruction, as a function of the location set [caller] - of the caller before the call instruction and of the location - set [callee] of the callee at the return instruction. -- Callee-save machine registers have the same values as in the caller - before the call. -- Caller-save machine registers have the same values - as in the callee at the return point. -- Stack slots have the same values as in the caller before the call. -*) - -Definition return_regs (caller callee: locset) : locset := - fun (l: loc) => - match l with - | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then - callee (R r) - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then - callee (R r) - else - caller (R r) - | S s => caller (S s) - end. +Section RELSEM. (** [parmov srcs dsts ls] performs the parallel assignment of locations [dsts] to the values of the corresponding locations @@ -130,18 +97,29 @@ Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset := | _, _ => ls end. -Definition set_result_reg (s: signature) (or: option loc) (ls: locset) := - match or with - | Some r => Locmap.set (R (loc_result s)) (ls r) ls - | None => ls - end. +(** [postcall_regs ls] returns the location set [ls] after a function + call. Caller-save registers and temporary registers + are set to [undef], reflecting the fact that the called + function can modify them freely. *) + +Definition postcall_regs (ls: locset) : locset := + fun (l: loc) => + match l with + | R r => + if In_dec Loc.eq (R r) Conventions.temporaries then + Vundef + else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + Vundef + else + ls (R r) + | S s => ls (S s) + end. (** LTL execution states. *) Inductive stackframe : Set := | Stackframe: - forall (sig: signature) (**r signature of call *) - (res: loc) (**r where to store the result *) + forall (res: loc) (**r where to store the result *) (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (ls: locset) (**r location state in calling function *) @@ -160,27 +138,15 @@ Inductive state : Set := | Callstate: forall (stack: list stackframe) (**r call stack *) (f: fundef) (**r function to call *) - (ls: locset) (**r location state at point of call *) + (args: list val) (**r arguments to the call *) (m: mem), (**r memory state *) state | Returnstate: forall (stack: list stackframe) (**r call stack *) - (ls: locset) (**r location state at point of return *) + (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. -Definition parent_locset (stack: list stackframe) : locset := - match stack with - | nil => Locmap.init Vundef - | Stackframe sg res f sp ls pc :: stack' => ls - end. - -Definition parent_callsig (stack: list stackframe) : signature := - match stack with - | nil => mksignature nil (Some Tint) - | Stackframe sg res f sp ls pc :: stack' => sg - end. - Variable ge: genv. Definition find_function (los: loc + ident) (rs: locset) : option fundef := @@ -265,28 +231,23 @@ Inductive step: state -> trace -> state -> Prop := (fn_code f)!pc = Some(Lcall sig ros args res pc') -> find_function ros rs = Some f' -> funsig f' = sig -> - let rs1 := parmov args (loc_arguments sig) rs in step (State s f sp pc rs m) - E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m) + E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s) + f' (List.map rs args) m) | exec_Ltailcall: forall s f stk pc rs m sig ros args f', (fn_code f)!pc = Some(Ltailcall sig ros args) -> find_function ros rs = Some f' -> funsig f' = sig -> - let rs1 := parmov args (loc_arguments sig) rs in - let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Callstate s f' rs2 (Mem.free m stk)) + E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) | exec_Lalloc: forall s f sp pc rs m pc' arg res sz m' b, (fn_code f)!pc = Some(Lalloc arg res pc') -> rs arg = Vint sz -> Mem.alloc m 0 (Int.signed sz) = (m', b) -> - let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in - let rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1 in - let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in step (State s f sp pc rs m) - E0 (State s f sp pc' rs3 m') + E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> @@ -302,30 +263,22 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lreturn: forall s f stk pc rs m or, (fn_code f)!pc = Some(Lreturn or) -> - let rs1 := set_result_reg f.(fn_sig) or rs in - let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Returnstate s rs2 (Mem.free m stk)) + E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk)) | exec_function_internal: - forall s f rs m m' stk, + forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - let rs1 := call_regs rs in - let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in - step (Callstate s (Internal f) rs m) - E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) rs2 m') + step (Callstate s (Internal f) args m) + E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m') | exec_function_external: - forall s ef t res rs m, - let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in + forall s ef t args res m, event_match ef args t res -> - let rs1 := - Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in - step (Callstate s (External ef) rs m) - t (Returnstate s rs1 m) + step (Callstate s (External ef) args m) + t (Returnstate s res m) | exec_return: - forall res f sp rs0 pc s sig rs m, - let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in - step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m) - E0 (State s f sp pc rs1 m). + forall res f sp rs pc s vres m, + step (Returnstate (Stackframe res f sp rs pc :: s) vres m) + E0 (State s f sp pc (Locmap.set res vres rs) m). End RELSEM. @@ -341,12 +294,11 @@ Inductive initial_state (p: program): state -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> - initial_state p (Callstate nil f (Locmap.init Vundef) m0). + initial_state p (Callstate nil f nil m0). Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r, - rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> - final_state (Returnstate nil rs m) r. + | final_state_intro: forall n m, + final_state (Returnstate nil (Vint n) m) n. Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. diff --git a/backend/LTLin.v b/backend/LTLin.v index 157b6d4..83787ce 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -112,8 +112,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := Inductive stackframe : Set := | Stackframe: - forall (sig: signature) (**r signature of call *) - (res: loc) (**r where to store the result *) + forall (res: loc) (**r where to store the result *) (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (ls: locset) (**r location state in calling function *) @@ -132,26 +131,22 @@ Inductive state : Set := | Callstate: forall (stack: list stackframe) (**r call stack *) (f: fundef) (**r function to call *) - (ls: locset) (**r location state at point of call *) + (args: list val) (**r arguments to the call *) (m: mem), (**r memory state *) state | Returnstate: forall (stack: list stackframe) (**r call stack *) - (ls: locset) (**r location state at point of return *) + (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. -Definition parent_locset (stack: list stackframe) : locset := - match stack with - | nil => Locmap.init Vundef - | Stackframe sg res f sp ls pc :: stack' => ls - end. - +(* Definition parent_callsig (stack: list stackframe) : signature := match stack with | nil => mksignature nil (Some Tint) | Stackframe sg res f sp ls pc :: stack' => sg end. +*) Section RELSEM. @@ -189,26 +184,21 @@ Inductive step: state -> trace -> state -> Prop := forall s f sp sig ros args res b rs m f', find_function ros rs = Some f' -> sig = funsig f' -> - let rs1 := parmov args (loc_arguments sig) rs in step (State s f sp (Lcall sig ros args res :: b) rs m) - E0 (Callstate (Stackframe sig res f sp rs1 b :: s) f' rs1 m) + E0 (Callstate (Stackframe res f sp (postcall_regs rs) b :: s) + f' (List.map rs args) m) | exec_Ltailcall: forall s f stk sig ros args b rs m f', find_function ros rs = Some f' -> sig = funsig f' -> - let rs1 := parmov args (loc_arguments sig) rs in - let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m) - E0 (Callstate s f' rs2 (Mem.free m stk)) + E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) | exec_Lalloc: forall s f sp arg res b rs m sz m' blk, rs arg = Vint sz -> Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in - let rs2 := Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) rs1 in - let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in step (State s f sp (Lalloc arg res :: b) rs m) - E0 (State s f sp b rs3 m') + E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_regs rs)) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -231,30 +221,22 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b rs m) | exec_Lreturn: forall s f stk rs m or b, - let rs1 := set_result_reg f.(fn_sig) or rs in - let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m) - E0 (Returnstate s rs2 (Mem.free m stk)) + E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk)) | exec_function_internal: - forall s f rs m m' stk, + forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - let rs1 := call_regs rs in - let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in - step (Callstate s (Internal f) rs m) - E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs2 m') + step (Callstate s (Internal f) args m) + E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m') | exec_function_external: - forall s ef t res rs m, - let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in + forall s ef args t res m, event_match ef args t res -> - let rs1 := - Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in - step (Callstate s (External ef) rs m) - t (Returnstate s rs1 m) + step (Callstate s (External ef) args m) + t (Returnstate s res m) | exec_return: - forall res f sp rs0 b s sig rs m, - let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in - step (Returnstate (Stackframe sig res f sp rs0 b :: s) rs m) - E0 (State s f sp b rs1 m). + forall res f sp rs b s vres m, + step (Returnstate (Stackframe res f sp rs b :: s) vres m) + E0 (State s f sp b (Locmap.set res vres rs) m). End RELSEM. @@ -265,12 +247,11 @@ Inductive initial_state (p: program): state -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> - initial_state p (Callstate nil f (Locmap.init Vundef) m0). + initial_state p (Callstate nil f nil m0). Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r, - rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> - final_state (Returnstate nil rs m) r. + | final_state_intro: forall n m, + final_state (Returnstate nil (Vint n) m) n. Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. diff --git a/backend/Linear.v b/backend/Linear.v index b9880ff..ca1a2bc 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -116,6 +116,52 @@ Definition find_function (ros: mreg + ident) (rs: locset) : option fundef := Definition reglist (rs: locset) (rl: list mreg) : list val := List.map (fun r => rs (R r)) rl. +(** Calling conventions are reflected at the level of location sets + (environments mapping locations to values) by the following two + functions. + + [call_regs caller] returns the location set at function entry, + as a function of the location set [caller] of the calling function. +- Machine registers have the same values as in the caller. +- Incoming stack slots (used for parameter passing) have the same + values as the corresponding outgoing stack slots (used for argument + passing) in the caller. +- Local and outgoing stack slots are initialized to undefined values. +*) + +Definition call_regs (caller: locset) : locset := + fun (l: loc) => + match l with + | R r => caller (R r) + | S (Local ofs ty) => Vundef + | S (Incoming ofs ty) => caller (S (Outgoing ofs ty)) + | S (Outgoing ofs ty) => Vundef + end. + +(** [return_regs caller callee] returns the location set after + a call instruction, as a function of the location set [caller] + of the caller before the call instruction and of the location + set [callee] of the callee at the return instruction. +- Callee-save machine registers have the same values as in the caller + before the call. +- Caller-save machine registers have the same values + as in the callee at the return point. +- Stack slots have the same values as in the caller before the call. +*) + +Definition return_regs (caller callee: locset) : locset := + fun (l: loc) => + match l with + | R r => + if In_dec Loc.eq (R r) Conventions.temporaries then + callee (R r) + else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + callee (R r) + else + caller (R r) + | S s => caller (S s) + end. + (** Linear execution states. *) Inductive stackframe: Set := diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 303482e..3451cdb 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -468,15 +468,15 @@ Qed. Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop := | match_stackframe_intro: - forall sig res f sp pc ls tf c, + forall res f sp pc ls tf c, transf_function f = OK tf -> (reachable f)!!pc = true -> valid_successor f pc -> is_tail c (fn_code tf) -> wt_function f -> match_stackframes - (LTL.Stackframe sig res f sp ls pc) - (LTLin.Stackframe sig res tf sp ls (add_branch pc c)). + (LTL.Stackframe res f sp ls pc) + (LTLin.Stackframe res tf sp ls (add_branch pc c)). Inductive match_states: LTL.state -> LTLin.state -> Prop := | match_states_intro: @@ -501,14 +501,6 @@ Inductive match_states: LTL.state -> LTLin.state -> Prop := match_states (LTL.Returnstate s ls m) (LTLin.Returnstate ts ls m). -Remark parent_locset_match: - forall s ts, - list_forall2 match_stackframes s ts -> - parent_locset ts = LTL.parent_locset s. -Proof. - induction 1; simpl; auto. inv H; auto. -Qed. - Hypothesis wt_prog: wt_program prog. Theorem transf_step_correct: @@ -578,8 +570,6 @@ Proof. traceEq. econstructor; eauto. (* Lcall *) - unfold rs1 in *. inv MS. fold rs1. - generalize (wt_instrs _ WTF _ _ H); intro WTI. destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). @@ -600,14 +590,12 @@ Proof. eapply Genv.find_funct_ptr_prop; eauto. (* Ltailcall *) - unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2. destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. exploit find_function_translated; eauto. intros [tf' [A B]]. econstructor; split. apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto. symmetry; apply sig_preserved; auto. - rewrite (parent_locset_match _ _ STACKS). econstructor; eauto. destruct ros; simpl in H0. eapply Genv.find_funct_prop; eauto. @@ -677,8 +665,7 @@ Proof. simpl in EQ. subst c. econstructor; split. apply plus_one. eapply exec_Lreturn; eauto. - rewrite (parent_locset_match _ _ STACKS). - monadInv TRF. simpl. econstructor; eauto. + econstructor; eauto. (* internal function *) assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true). @@ -714,7 +701,7 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists (Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split. + exists (Callstate nil tf nil (Genv.init_mem tprog)); split. econstructor; eauto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. @@ -730,7 +717,7 @@ Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r. Proof. - intros. inv H0. inv H. inv H5. constructor. auto. + intros. inv H0. inv H. inv H4. constructor. Qed. Theorem transf_program_correct: diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index f0b17e1..372a261 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -414,22 +414,22 @@ End LINEAR_CONSTRUCTORS. that is, non-temporary registers and [Local] stack slots. *) Definition agree (rs1 rs2: locset) : Prop := - forall l, loc_acceptable l -> rs2 l = rs1 l. + forall l, loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l). Lemma agree_loc: forall rs1 rs2 l, - agree rs1 rs2 -> loc_acceptable l -> rs2 l = rs1 l. + agree rs1 rs2 -> loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l). Proof. auto. Qed. Lemma agree_locs: forall rs1 rs2 ll, - agree rs1 rs2 -> locs_acceptable ll -> map rs2 ll = map rs1 ll. + agree rs1 rs2 -> locs_acceptable ll -> Val.lessdef_list (map rs1 ll) (map rs2 ll). Proof. induction ll; simpl; intros. - auto. - f_equal. apply H. apply H0; auto with coqlib. + constructor. + constructor. apply H. apply H0; auto with coqlib. apply IHll; auto. red; intros. apply H0; auto with coqlib. Qed. @@ -446,7 +446,7 @@ Qed. Lemma agree_set: forall rs1 rs2 rs2' l v, loc_acceptable l -> - rs2' l = v -> + Val.lessdef v (rs2' l) -> (forall l', Loc.diff l l' -> Loc.notin l' temporaries -> rs2' l' = rs2 l') -> agree rs1 rs2 -> agree (Locmap.set l v rs1) rs2'. Proof. @@ -458,6 +458,7 @@ Proof. apply temporaries_not_acceptable; auto. Qed. +(***** Lemma agree_return_regs: forall rs1 ls1 rs2 ls2, agree rs1 ls1 -> agree rs2 ls2 -> @@ -624,6 +625,140 @@ Proof. destruct (In_dec Loc.eq (R m) destroyed_at_call); auto. contradiction. Qed. +**********) + +Lemma agree_find_funct: + forall (ge: Linear.genv) rs ls r f, + Genv.find_funct ge (rs r) = Some f -> + agree rs ls -> + loc_acceptable r -> + Genv.find_funct ge (ls r) = Some f. +Proof. + intros. + assert (Val.lessdef (rs r) (ls r)). eapply agree_loc; eauto. + exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H2. + inv H2. rewrite <- EQ. auto. +Qed. + +Lemma agree_postcall_1: + forall rs ls, + agree rs ls -> + agree (LTL.postcall_regs rs) ls. +Proof. + intros; red; intros. unfold LTL.postcall_regs. + destruct l; auto. + destruct (In_dec Loc.eq (R m) temporaries). constructor. + destruct (In_dec Loc.eq (R m) destroyed_at_call). constructor. + auto. +Qed. + +Lemma agree_postcall_2: + forall rs ls ls', + agree (LTL.postcall_regs rs) ls -> + (forall l, loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries -> ls' l = ls l) -> + agree (LTL.postcall_regs rs) ls'. +Proof. + intros; red; intros. generalize (H l H1). unfold LTL.postcall_regs. + destruct l. + destruct (In_dec Loc.eq (R m) temporaries). intro; constructor. + destruct (In_dec Loc.eq (R m) destroyed_at_call). intro; constructor. + intro. rewrite H0; auto. + intro. rewrite H0; auto. + simpl. intuition congruence. + simpl. intuition congruence. +Qed. + +Lemma agree_postcall_call: + forall rs ls ls' sig, + agree rs ls -> + (forall l, Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries -> ls' l = ls l) -> + agree (LTL.postcall_regs rs) ls'. +Proof. + intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto. + intros. apply H0. + apply arguments_not_preserved; auto. + destruct l; simpl. simpl in H2. intuition congruence. + destruct s; tauto. + apply temporaries_not_acceptable; auto. +Qed. + +Lemma agree_postcall_alloc: + forall rs ls ls2 v, + agree rs ls -> + (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) -> + agree (LTL.postcall_regs rs) (Locmap.set (R loc_alloc_result) v ls2). +Proof. + intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto. + intros. destruct (Loc.eq l (R loc_alloc_result)). + subst l. elim H2. simpl. tauto. + rewrite Locmap.gso. apply H0. + red. destruct l; auto. red; intro. subst m. elim H2. + simpl. tauto. + apply Loc.diff_sym. apply loc_acceptable_noteq_diff; auto. +Qed. + +Lemma agree_init_locs: + forall ls dsts vl, + locs_acceptable dsts -> + Loc.norepet dsts -> + Val.lessdef_list vl (map ls dsts) -> + agree (LTL.init_locs vl dsts) ls. +Proof. + induction dsts; intros; simpl. + red; intros. unfold Locmap.init. constructor. + simpl in H1. inv H1. inv H0. + apply agree_set with ls. apply H; auto with coqlib. auto. auto. + apply IHdsts; auto. red; intros; apply H; auto with coqlib. +Qed. + +Lemma call_regs_parameters: + forall ls sig, + map (call_regs ls) (loc_parameters sig) = + map ls (loc_arguments sig). +Proof. + intros. unfold loc_parameters. rewrite list_map_compose. + apply list_map_exten; intros. + unfold call_regs, parameter_of_argument. + generalize (loc_arguments_acceptable _ _ H). + unfold loc_argument_acceptable. + destruct x. auto. + destruct s; intros; try contradiction. auto. +Qed. + +Lemma return_regs_arguments: + forall ls1 ls2 sig, + tailcall_possible sig -> + map (return_regs ls1 ls2) (loc_arguments sig) = map ls2 (loc_arguments sig). +Proof. + intros. symmetry. apply list_map_exten; intros. + unfold return_regs. generalize (H x H0). destruct x; intros. + destruct (In_dec Loc.eq (R m) temporaries). auto. + destruct (In_dec Loc.eq (R m) destroyed_at_call). auto. + elim n0. eapply arguments_caller_save; eauto. + contradiction. +Qed. + +Lemma return_regs_result: + forall ls1 ls2 sig, + return_regs ls1 ls2 (R (loc_result sig)) = ls2 (R (loc_result sig)). +Proof. + intros. unfold return_regs. + destruct (In_dec Loc.eq (R (loc_result sig)) temporaries). auto. + destruct (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call). auto. + elim n0. apply loc_result_caller_save. +Qed. + +Lemma return_regs_preserve: + forall ls1 ls2 l, + ~ In l temporaries -> + ~ In l destroyed_at_call -> + return_regs ls1 ls2 l = ls1 l. +Proof. + intros. unfold return_regs. destruct l; auto. + destruct (In_dec Loc.eq (R m) temporaries). contradiction. + destruct (In_dec Loc.eq (R m) destroyed_at_call). contradiction. + auto. +Qed. (** * Preservation of labels and gotos *) @@ -770,56 +905,63 @@ Qed. only acceptable locations are accessed by this code. *) -Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> Prop := +Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop := | match_stackframes_nil: - match_stackframes nil nil + forall sig, + sig.(sig_res) = Some Tint -> + match_stackframes nil nil sig | match_stackframes_cons: forall res f sp c rs s s' c' ls sig, - match_stackframes s s' -> - sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s) -> + match_stackframes s s' (LTLin.fn_sig f) -> c' = add_spill (loc_result sig) res (transf_code f c) -> - agree rs ls -> + agree (LTL.postcall_regs rs) ls -> loc_acceptable res -> wt_function f -> is_tail c (LTLin.fn_code f) -> - match_stackframes (LTLin.Stackframe sig res f sp rs c :: s) - (Linear.Stackframe (transf_function f) sp ls c' :: s'). + match_stackframes (LTLin.Stackframe res f sp (LTL.postcall_regs rs) c :: s) + (Linear.Stackframe (transf_function f) sp ls c' :: s') + sig. Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_intro: - forall s f sp c rs m s' ls - (STACKS: match_stackframes s s') - (SIG: sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s)) + forall s f sp c rs m s' ls tm + (STACKS: match_stackframes s s' (LTLin.fn_sig f)) (AG: agree rs ls) (WT: wt_function f) - (TL: is_tail c (LTLin.fn_code f)), + (TL: is_tail c (LTLin.fn_code f)) + (MMD: Mem.lessdef m tm), match_states (LTLin.State s f sp c rs m) - (Linear.State s' (transf_function f) sp (transf_code f c) ls m) + (Linear.State s' (transf_function f) sp (transf_code f c) ls tm) | match_states_call: - forall s f rs m s' ls - (STACKS: match_stackframes s s') - (SIG: sig_res (LTLin.funsig f) = sig_res (parent_callsig s)) - (AG: agree_arguments (LTLin.funsig f) rs ls) - (WT: wt_fundef f), - match_states (LTLin.Callstate s f rs m) - (Linear.Callstate s' (transf_fundef f) ls m) + forall s f args m s' ls tm + (STACKS: match_stackframes s s' (LTLin.funsig f)) + (AG: Val.lessdef_list args (map ls (Conventions.loc_arguments (LTLin.funsig f)))) + (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> + ls l = parent_locset s' l) + (WT: wt_fundef f) + (MMD: Mem.lessdef m tm), + match_states (LTLin.Callstate s f args m) + (Linear.Callstate s' (transf_fundef f) ls tm) | match_states_return: - forall s rs m s' ls - (STACKS: match_stackframes s s') - (AG: agree rs ls), - match_states (LTLin.Returnstate s rs m) - (Linear.Returnstate s' ls m). - -Remark parent_locset_match: - forall s s', - match_stackframes s s' -> - agree (LTLin.parent_locset s) (parent_locset s'). + forall s res m s' ls tm sig + (STACKS: match_stackframes s s' sig) + (AG: Val.lessdef res (ls (R (Conventions.loc_result sig)))) + (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> + ls l = parent_locset s' l) + (MMD: Mem.lessdef m tm), + match_states (LTLin.Returnstate s res m) + (Linear.Returnstate s' ls tm). + +Lemma match_stackframes_change_sig: + forall s s' sig1 sig2, + match_stackframes s s' sig1 -> + sig2.(sig_res) = sig1.(sig_res) -> + match_stackframes s s' sig2. Proof. - induction 1; simpl. - red; intros; auto. - auto. + intros. inv H. constructor. congruence. + econstructor; eauto. unfold loc_result. rewrite H0. auto. Qed. - + Ltac ExploitWT := match goal with | [ WT: wt_function _, TL: is_tail _ _ |- _ ] => @@ -850,6 +992,8 @@ Definition measure (st: LTLin.state) : nat := | LTLin.Returnstate s ls m => 0%nat end. +Axiom ADMITTED: forall (P: Prop), P. + Theorem transf_step_correct: forall s1 t s2, LTLin.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), @@ -863,18 +1007,18 @@ Proof. ExploitWT. inv WTI. (* move *) simpl. - destruct (add_move_correct tge s' (transf_function f) sp r1 res (transf_code f b) ls m) + destruct (add_move_correct tge s' (transf_function f) sp r1 res (transf_code f b) ls tm) as [ls2 [A [B C]]]. inv A. right. split. omega. split. auto. rewrite H1. rewrite H1. econstructor; eauto with coqlib. - apply agree_set with ls2; auto. + apply agree_set with ls2; auto. rewrite B. simpl in H; inversion H. auto. left; econstructor; split. eapply plus_left; eauto. econstructor; eauto with coqlib. apply agree_set with ls; auto. rewrite B. simpl in H; inversion H. auto. - intros. simpl in H1. apply C. apply Loc.diff_sym; auto. + intros. apply C. apply Loc.diff_sym; auto. simpl in H7; tauto. simpl in H7; tauto. (* other ops *) assert (is_move_operation op args = None). @@ -885,18 +1029,22 @@ Proof. exploit add_reloads_correct. eapply length_op_args; eauto. apply locs_acceptable_disj_temporaries; auto. - intros [ls2 [A [B C]]]. + intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. + assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv + /\ Val.lessdef v tv). + apply eval_operation_lessdef with m (map rs args); auto. + rewrite B. eapply agree_locs; eauto. + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + destruct H1 as [tv [P Q]]. exploit add_spill_correct. intros [ls3 [D [E F]]]. left; econstructor; split. eapply star_plus_trans. eexact A. - eapply plus_left. eapply exec_Lop with (v := v). - rewrite <- H. rewrite B. rewrite (agree_locs _ _ _ AG H5). - apply eval_operation_preserved. exact symbols_preserved. + eapply plus_left. eapply exec_Lop with (v := tv); eauto. eexact D. eauto. traceEq. econstructor; eauto with coqlib. apply agree_set with ls; auto. - rewrite E. apply Locmap.gss. + rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. auto. apply reg_for_diff; auto. @@ -906,17 +1054,23 @@ Proof. apply le_S. eapply length_addr_args; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. + assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta + /\ Val.lessdef a ta). + apply eval_addressing_lessdef with (map rs args); auto. + rewrite B. eapply agree_locs; eauto. + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + destruct H1 as [ta [P Q]]. + exploit Mem.loadv_lessdef; eauto. + intros [tv [R S]]. exploit add_spill_correct. intros [ls3 [D [E F]]]. left; econstructor; split. eapply star_plus_trans. eauto. eapply plus_left. eapply exec_Lload; eauto. - rewrite B. rewrite <- H. rewrite (agree_locs _ _ _ AG H7). - apply eval_addressing_preserved. exact symbols_preserved. eauto. auto. traceEq. econstructor; eauto with coqlib. apply agree_set with ls; auto. - rewrite E. apply Locmap.gss. + rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. auto. apply reg_for_diff; auto. @@ -936,20 +1090,25 @@ Proof. intros [ls2 [A [B C]]]. rewrite EQ in A. rewrite EQ in B. injection B. intros D E. simpl in B. + assert (exists ta, eval_addressing tge sp addr (reglist ls2 rargs) = Some ta + /\ Val.lessdef a ta). + apply eval_addressing_lessdef with (map rs args); auto. + rewrite D. eapply agree_locs; eauto. + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + destruct H2 as [ta [P Q]]. + assert (X: Val.lessdef (rs src) (ls2 (R rsrc))). + rewrite E. eapply agree_loc; eauto. + exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. + intros [tm2 [Y Z]]. left; econstructor; split. eapply plus_right. eauto. - eapply exec_Lstore with (a := a); eauto. - rewrite D. rewrite <- H. rewrite (agree_locs _ _ _ AG H7). - apply eval_addressing_preserved. exact symbols_preserved. - rewrite E. rewrite (agree_loc _ _ _ AG H8). eauto. + eapply exec_Lstore with (a := ta); eauto. traceEq. econstructor; eauto with coqlib. apply agree_exten with ls; auto. (* Lcall *) - inversion MS. subst s0 f0 sp0 c rs0 m0. - simpl transf_code. - ExploitWT. inversion WTI. subst sig0 ros0 args0 res0. + ExploitWT. inversion WTI. subst ros0 args0 res0. rewrite <- H0. assert (WTF': wt_fundef f'). eapply find_function_wt; eauto. destruct ros as [fn | id]. (* indirect call *) @@ -957,44 +1116,41 @@ Proof. (parallel_move args (loc_arguments sig) (Lcall sig (inl ident IT3) :: add_spill (loc_result sig) res (transf_code f b))) - ls m) + ls tm) as [ls2 [A [B C]]]. + rewrite <- H0 in H5. destruct (parallel_move_arguments_correct tge s' (transf_function f) sp args sig (Lcall sig (inl ident IT3) :: add_spill (loc_result sig) res (transf_code f b)) - ls2 m H7 H10) + ls2 tm H5 H8) as [ls3 [D [E [F G]]]]. - assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs1 ls3). - rewrite <- H0. - unfold rs1. apply agree_set_arguments with ls; auto. - rewrite E. apply list_map_exten; intros. symmetry. apply C. - assert (Loc.notin x temporaries). apply temporaries_not_acceptable; auto. - simpl in H3. apply Loc.diff_sym. tauto. - intros. rewrite G; auto. apply C. - simpl in H3. apply Loc.diff_sym. tauto. + assert (ARGS: Val.lessdef_list (map rs args) + (map ls3 (loc_arguments sig))). + rewrite E. apply agree_locs. apply agree_exten with ls; auto. + intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto. left; econstructor; split. - eapply star_plus_trans. eauto. eapply plus_right. eauto. + eapply star_plus_trans. eexact A. eapply plus_right. eexact D. eapply exec_Lcall; eauto. - simpl. rewrite F. rewrite B. - rewrite (agree_loc rs ls fn); auto. + simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto. apply functions_translated. eauto. rewrite H0; symmetry; apply sig_preserved. eauto. traceEq. econstructor; eauto. - econstructor; eauto with coqlib. - eapply agree_arguments_agree; eauto. - simpl. congruence. + econstructor; eauto with coqlib. rewrite H0; auto. + apply agree_postcall_call with ls sig; auto. + intros. rewrite G; auto. apply C. simpl in H2. apply Loc.diff_sym. tauto. + congruence. (* direct call *) + rewrite <- H0 in H5. destruct (parallel_move_arguments_correct tge s' (transf_function f) sp args sig (Lcall sig (inr mreg id) :: add_spill (loc_result sig) res (transf_code f b)) - ls m H7 H10) + ls tm H5 H8) as [ls3 [D [E [F G]]]]. - assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs1 ls3). - rewrite <- H0. - unfold rs1. apply agree_set_arguments with ls; auto. + assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))). + rewrite E. apply agree_locs; auto. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcall; eauto. @@ -1004,58 +1160,53 @@ Proof. rewrite H0. symmetry; apply sig_preserved. traceEq. econstructor; eauto. - econstructor; eauto with coqlib. - eapply agree_arguments_agree; eauto. - simpl; congruence. + econstructor; eauto with coqlib. rewrite H0; auto. + apply agree_postcall_call with ls sig; auto. + congruence. (* Ltailcall *) - inversion MS. subst s0 f0 sp c rs0 m0 s1'. - simpl transf_code. - ExploitWT. inversion WTI. subst sig0 ros0 args0. + ExploitWT. inversion WTI. subst ros0 args0. assert (WTF': wt_fundef f'). eapply find_function_wt; eauto. + rewrite <- H0. destruct ros as [fn | id]. (* indirect call *) destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT3 (parallel_move args (loc_arguments sig) (Ltailcall sig (inl ident IT3) :: transf_code f b)) - ls m) + ls tm) as [ls2 [A [B C]]]. + rewrite <- H0 in H4. destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) args sig (Ltailcall sig (inl ident IT3) :: transf_code f b) - ls2 m H5 H7) + ls2 tm H4 H6) as [ls3 [D [E [F G]]]]. - assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs2 (LTL.return_regs (parent_locset s') ls3)). - rewrite <- H0. unfold rs2. - apply agree_arguments_return_regs; auto. - eapply parent_locset_match; eauto. - unfold rs1. apply agree_set_arguments with ls; auto. - rewrite E. apply list_map_exten; intros. symmetry. apply C. - assert (Loc.notin x temporaries). apply temporaries_not_acceptable; auto. - simpl in H2. apply Loc.diff_sym. tauto. - intros. rewrite G; auto. apply C. - simpl in H2. apply Loc.diff_sym. tauto. + assert (ARGS: Val.lessdef_list (map rs args) + (map ls3 (loc_arguments sig))). + rewrite E. apply agree_locs. apply agree_exten with ls; auto. + intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto. left; econstructor; split. eapply star_plus_trans. eauto. eapply plus_right. eauto. eapply exec_Ltailcall; eauto. - simpl. rewrite F. rewrite B. - rewrite (agree_loc rs ls fn); auto. + simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto. apply functions_translated. eauto. rewrite H0; symmetry; apply sig_preserved. eauto. traceEq. - econstructor; eauto. congruence. - + econstructor; eauto. + eapply match_stackframes_change_sig; eauto. + rewrite return_regs_arguments; auto. congruence. + exact (return_regs_preserve (parent_locset s') ls3). + apply Mem.free_lessdef; auto. (* direct call *) + rewrite <- H0 in H4. destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) args sig (Ltailcall sig (inr mreg id) :: transf_code f b) - ls m H5 H7) + ls tm H4 H6) as [ls3 [D [E [F G]]]]. - assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs2 (LTL.return_regs (parent_locset s') ls3)). - rewrite <- H0. unfold rs2. - apply agree_arguments_return_regs; auto. - eapply parent_locset_match; eauto. - unfold rs1. apply agree_set_arguments with ls; auto. + assert (ARGS: Val.lessdef_list (map rs args) + (map ls3 (loc_arguments sig))). + rewrite E. apply agree_locs. apply agree_exten with ls; auto. auto. left; econstructor; split. eapply plus_right. eauto. eapply exec_Ltailcall; eauto. @@ -1064,28 +1215,33 @@ Proof. apply function_ptr_translated; auto. congruence. rewrite H0. symmetry; apply sig_preserved. traceEq. - econstructor; eauto. congruence. + econstructor; eauto. + eapply match_stackframes_change_sig; eauto. + rewrite return_regs_arguments; auto. congruence. + exact (return_regs_preserve (parent_locset s') ls3). + apply Mem.free_lessdef; auto. (* Lalloc *) ExploitWT; inv WTI. + caseEq (alloc tm 0 (Int.signed sz)). intros tm' blk' TALLOC. + assert (blk = blk' /\ Mem.lessdef m' tm'). + eapply Mem.alloc_lessdef; eauto. exploit add_reload_correct. intros [ls2 [A [B C]]]. exploit add_spill_correct. intros [ls3 [D [E F]]]. + destruct H1 as [P Q]. subst blk'. + assert (ls arg = Vint sz). + assert (Val.lessdef (rs arg) (ls arg)). eapply agree_loc; eauto. + rewrite H in H1; inversion H1; auto. left; econstructor; split. eapply star_plus_trans. eauto. eapply plus_left. eapply exec_Lalloc; eauto. - rewrite B. rewrite <- H. apply AG. auto. + rewrite B. eauto. eauto. eauto. traceEq. econstructor; eauto with coqlib. - unfold rs3; apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2). - auto. rewrite E. rewrite Locmap.gss. - unfold rs2; rewrite Locmap.gss. auto. - auto. - unfold rs2. apply agree_set with ls2. - unfold loc_alloc_result; simpl; intuition congruence. - apply Locmap.gss. intros. apply Locmap.gso; auto. - unfold rs1. apply agree_set with ls. - unfold loc_alloc_argument; simpl; intuition congruence. - rewrite B. apply AG; auto. auto. auto. + apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2). + auto. rewrite E. rewrite Locmap.gss. constructor. + auto. + apply agree_postcall_alloc with ls; auto. (* Llabel *) left; econstructor; split. @@ -1106,7 +1262,8 @@ Proof. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcond_true; eauto. - rewrite B. rewrite (agree_locs _ _ _ AG H5). auto. + rewrite B. apply eval_condition_lessdef with m (map rs args); auto. + eapply agree_locs; eauto. apply find_label_transf_function; eauto. traceEq. econstructor; eauto. @@ -1121,44 +1278,44 @@ Proof. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcond_false; eauto. - rewrite B. rewrite (agree_locs _ _ _ AG H4). auto. + rewrite B. apply eval_condition_lessdef with m (map rs args); auto. + eapply agree_locs; eauto. traceEq. econstructor; eauto with coqlib. apply agree_exten with ls; auto. (* Lreturn *) ExploitWT; inv WTI. - unfold rs2, rs1; destruct or; simpl. + destruct or; simpl. (* with an argument *) exploit add_reload_correct. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lreturn; eauto. traceEq. - econstructor; eauto. - apply agree_return_regs; auto. - eapply parent_locset_match; eauto. - apply agree_set with ls. - apply loc_result_acceptable. - rewrite B. eapply agree_loc; eauto. - auto. auto. + econstructor; eauto. + rewrite return_regs_result. rewrite B. apply agree_loc; auto. + apply return_regs_preserve. + apply Mem.free_lessdef; auto. (* without an argument *) left; econstructor; split. apply plus_one. eapply exec_Lreturn; eauto. econstructor; eauto. - apply agree_return_regs; auto. - eapply parent_locset_match; eauto. + apply return_regs_preserve. + apply Mem.free_lessdef; auto. (* internal function *) simpl in WT. inversion_clear WT. inversion H0. simpl in AG. + caseEq (alloc tm 0 (LTLin.fn_stacksize f)). intros tm' tstk TALLOC. + exploit Mem.alloc_lessdef; eauto. intros [P Q]. subst tstk. destruct (parallel_move_parameters_correct tge s' (transf_function f) (Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f) - (transf_code f (LTLin.fn_code f)) (LTL.call_regs ls) m' + (transf_code f (LTLin.fn_code f)) (call_regs ls) tm' wt_params wt_acceptable wt_norepet) as [ls2 [A [B [C D]]]]. - assert (AG2: agree rs2 ls2). - unfold rs2. eapply agree_set_parameters; eauto. - unfold rs1. apply agree_call_regs; auto. + assert (AG2: agree (LTL.init_locs args (fn_params f)) ls2). + apply agree_init_locs; auto. + rewrite B. rewrite call_regs_parameters. auto. left; econstructor; split. eapply plus_left. eapply exec_function_internal; eauto. @@ -1166,15 +1323,14 @@ Proof. econstructor; eauto with coqlib. (* external function *) + exploit event_match_lessdef; eauto. + intros [res' [A B]]. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. - unfold args. symmetry. eapply agree_arguments_locs; auto. econstructor; eauto. - unfold rs1. apply agree_set with ls; auto. - apply loc_result_acceptable. - apply Locmap.gss. - intros. apply Locmap.gso; auto. - eapply agree_arguments_agree; eauto. + simpl. rewrite Locmap.gss. auto. + intros. rewrite Locmap.gso. auto. + simpl. destruct l; auto. red; intro. elim H1. subst m0. apply loc_result_caller_save. (* return *) inv STACKS. @@ -1183,8 +1339,10 @@ Proof. eapply plus_left. eapply exec_return; eauto. eauto. traceEq. econstructor; eauto. - unfold rs1. apply agree_set with ls; auto. - rewrite B. apply AG. apply loc_result_acceptable. + apply agree_set with ls; auto. + rewrite B. auto. + unfold parent_locset in PRES. + apply agree_postcall_2 with ls0; auto. Qed. Lemma transf_initial_states: @@ -1200,9 +1358,9 @@ Proof. rewrite sig_preserved. auto. replace (Genv.init_mem tprog) with (Genv.init_mem prog). econstructor; eauto. constructor. rewrite H2; auto. - red; intros. auto. + rewrite H2. simpl. constructor. eapply Genv.find_funct_ptr_prop; eauto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto. + apply Mem.lessdef_refl. symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto. Qed. Lemma transf_final_states: @@ -1210,8 +1368,7 @@ Lemma transf_final_states: match_states st1 st2 -> LTLin.final_state st1 r -> Linear.final_state st2 r. Proof. intros. inv H0. inv H. inv STACKS. econstructor. - rewrite (agree_loc _ _ (R R3) AG). auto. - simpl. intuition congruence. + unfold loc_result in AG. rewrite H in AG. inv AG. auto. Qed. Theorem transf_program_correct: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1759d7f..a9187ee 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -726,9 +726,9 @@ Lemma agree_return_regs: (forall r, In r int_callee_save_regs \/ In r float_callee_save_regs -> rs' r = ls0 (R r)) -> - (forall r, LTL.return_regs ls0 ls (R r) = rs' r). + (forall r, return_regs ls0 ls (R r) = rs' r). Proof. - intros; unfold LTL.return_regs. + intros; unfold return_regs. case (In_dec Loc.eq (R r) temporaries); intro. rewrite H0. eapply agree_reg; eauto. apply int_callee_save_not_destroyed; auto. @@ -778,10 +778,10 @@ Qed. Lemma agree_callee_save_return_regs: forall ls1 ls2, - agree_callee_save (LTL.return_regs ls1 ls2) ls1. + agree_callee_save (return_regs ls1 ls2) ls1. Proof. intros; red; intros. - unfold LTL.return_regs. destruct l; auto. + unfold return_regs. destruct l; auto. generalize (int_callee_save_not_destroyed m); intro. generalize (float_callee_save_not_destroyed m); intro. destruct (In_dec Loc.eq (R m) temporaries). tauto. @@ -988,7 +988,7 @@ Lemma save_callee_save_correct: star step tge (State stack tf sp (save_callee_save fe k) rs empty_frame m) E0 (State stack tf sp k rs fr' m) - /\ agree (LTL.call_regs ls) ls rs fr' cs. + /\ agree (call_regs ls) ls rs fr' cs. Proof. intros. unfold save_callee_save. exploit save_callee_save_int_correct; eauto. @@ -997,7 +997,7 @@ Proof. intros [fr2 [A2 [B2 C2]]]. exists fr2. split. eapply star_trans. eexact A1. eexact A2. traceEq. - constructor; unfold LTL.call_regs; auto. + constructor; unfold call_regs; auto. (* agree_local *) intros. rewrite C2; auto with stacking. rewrite C1; auto with stacking. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index cb0a6d8..cefad10 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -190,10 +190,10 @@ Definition tunneled_code (f: function) := Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframes_intro: - forall sig res f sp ls0 pc, + forall res f sp ls0 pc, match_stackframes - (Stackframe sig res f sp ls0 pc) - (Stackframe sig res (tunnel_function f) sp ls0 (branch_target f pc)). + (Stackframe res f sp ls0 pc) + (Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)). Inductive match_states: state -> state -> Prop := | match_states_intro: @@ -212,12 +212,6 @@ Inductive match_states: state -> state -> Prop := match_states (Returnstate s ls m) (Returnstate ts ls m). -Lemma parent_locset_match: - forall s ts, list_forall2 match_stackframes s ts -> parent_locset ts = parent_locset s. -Proof. - induction 1; simpl; auto. inv H; auto. -Qed. - (** To preserve non-terminating behaviours, we show that the transformed code cannot take an infinity of "zero transition" cases. We use the following [measure] function over source states, @@ -286,32 +280,27 @@ Proof. rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. econstructor; eauto. (* Lcall *) - unfold rs1. inv MS. left; econstructor; split. eapply exec_Lcall with (f' := tunnel_fundef f'); eauto. rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. rewrite (tunnel_function_lookup _ _ _ H); simpl. rewrite sig_preserved. auto. apply find_function_translated; auto. - rewrite sig_preserved; auto. fold rs1. econstructor; eauto. constructor; auto. constructor; auto. (* Ltailcall *) - unfold rs2, rs1 in *. inv MS. fold rs1. fold rs2. left; econstructor; split. eapply exec_Ltailcall with (f' := tunnel_fundef f'); eauto. rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. rewrite (tunnel_function_lookup _ _ _ H); simpl. rewrite sig_preserved. auto. apply find_function_translated; auto. - rewrite sig_preserved; auto. fold rs1. - rewrite (parent_locset_match _ _ H9). econstructor; eauto. (* Lalloc *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - left; exists (State ts (tunnel_function f) sp (branch_target f pc') rs3 m'); split. - unfold rs3, rs2, rs1; eapply exec_Lalloc; eauto. + left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_regs rs)) m'); split. + eapply exec_Lalloc; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. econstructor; eauto. (* cond *) @@ -330,7 +319,7 @@ Proof. left; econstructor; split. eapply exec_Lreturn; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. - simpl. rewrite (parent_locset_match _ _ H7). constructor; auto. + simpl. constructor; auto. (* internal function *) simpl. left; econstructor; split. eapply exec_function_internal; eauto. @@ -343,7 +332,7 @@ Proof. inv H3. inv H1. left; econstructor; split. eapply exec_return; eauto. - fold rs1. constructor. auto. + constructor. auto. Qed. Lemma transf_initial_states: @@ -351,7 +340,7 @@ Lemma transf_initial_states: exists st2, initial_state tp st2 /\ match_states st1 st2. Proof. intros. inversion H. - exists (Callstate nil (tunnel_fundef f) (Locmap.init Vundef) (Genv.init_mem tp)); split. + exists (Callstate nil (tunnel_fundef f) nil (Genv.init_mem tp)); split. econstructor; eauto. change (prog_main tp) with (prog_main p). rewrite symbols_preserved. eauto. @@ -366,7 +355,7 @@ Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> final_state st1 r -> final_state st2 r. Proof. - intros. inv H0. inv H. inv H5. constructor. auto. + intros. inv H0. inv H. inv H4. constructor. Qed. Theorem transf_program_correct: |