diff options
Diffstat (limited to 'backend/Allocproof.v')
| -rw-r--r-- | backend/Allocproof.v | 295 |
1 files changed, 99 insertions, 196 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: |