diff options
Diffstat (limited to 'backend/Allocproof.v')
| -rw-r--r-- | backend/Allocproof.v | 336 |
1 files changed, 218 insertions, 118 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 138e6d7..07c0f58 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -8,6 +8,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Mem. +Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Registers. @@ -17,8 +18,8 @@ Require Import Locations. Require Import Conventions. Require Import Coloring. Require Import Coloringproof. +Require Import Parallelmove. Require Import Allocation. -Require Import Allocproof_aux. (** * Semantic properties of calling conventions *) @@ -473,7 +474,7 @@ Qed. Lemma add_reload_correct: forall src dst k rs m, exists rs', - exec_instrs ge sp (add_reload src dst k) rs m k rs' m /\ + exec_instrs ge sp (add_reload src dst k) rs m E0 k rs' m /\ rs' (R dst) = rs src /\ forall l, Loc.diff (R dst) l -> rs' l = rs l. Proof. @@ -493,7 +494,7 @@ Qed. Lemma add_spill_correct: forall src dst k rs m, exists rs', - exec_instrs ge sp (add_spill src dst k) rs m k rs' m /\ + exec_instrs ge sp (add_spill src dst k) rs m E0 k rs' m /\ rs' dst = rs (R src) /\ forall l, Loc.diff dst l -> rs' l = rs l. Proof. @@ -520,7 +521,7 @@ Lemma add_reloads_correct_rec: list_norepet itmps -> list_norepet ftmps -> exists rs', - exec_instrs ge sp (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m k rs' m /\ + exec_instrs ge sp (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m E0 k rs' m /\ reglist (regs_for_rec srcs itmps ftmps) rs' = map rs srcs /\ (forall r, ~(In r itmps) -> ~(In r ftmps) -> rs' (R r) = rs (R r)) /\ (forall s, rs' (S s) = rs (S s)). @@ -578,7 +579,7 @@ Proof. generalize (IHsrcs itmps ftmps k rs1 m R1 R2 R3 R4 R5 R6 R7). intros [rs' [EX [RES [OTH1 OTH2]]]]. exists rs'. - split. eapply exec_trans; eauto. + split. eapply exec_trans; eauto. traceEq. split. simpl. apply (f_equal2 (@cons val)). rewrite OTH1; auto. rewrite RES. apply list_map_exten. intros. @@ -599,7 +600,7 @@ Lemma add_reloads_correct: (List.length srcs <= 3)%nat -> Loc.disjoint srcs temporaries -> exists rs', - exec_instrs ge sp (add_reloads srcs (regs_for srcs) k) rs m k rs' m /\ + exec_instrs ge sp (add_reloads srcs (regs_for srcs) k) rs m E0 k rs' m /\ reglist (regs_for srcs) rs' = List.map rs srcs /\ forall l, Loc.notin l temporaries -> rs' l = rs l. Proof. @@ -638,7 +639,7 @@ Qed. Lemma add_move_correct: forall src dst k rs m, exists rs', - exec_instrs ge sp (add_move src dst k) rs m k rs' m /\ + exec_instrs ge sp (add_move src dst k) rs m E0 k rs' m /\ rs' dst = rs src /\ forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> rs' l = rs l. Proof. @@ -660,13 +661,33 @@ Proof. generalize (add_spill_correct tmp (S s0) k rs1 m); intros [rs2 [EX2 [RES2 OTH2]]]. exists rs2. split. - eapply exec_trans; eauto. + eapply exec_trans; eauto. traceEq. split. congruence. intros. rewrite OTH2. apply OTH1. apply Loc.diff_sym. unfold tmp; case (slot_type s); auto. apply Loc.diff_sym; auto. Qed. +Lemma effect_move_sequence: + forall k moves rs m, + let k' := List.fold_right (fun p k => add_move (fst p) (snd p) k) k moves in + exists rs', + exec_instrs ge sp k' rs m E0 k rs' m /\ + effect_seqmove moves rs rs'. +Proof. + induction moves; intros until m; simpl. + exists rs; split. constructor. constructor. + destruct a as [src dst]; simpl. + set (k1 := fold_right + (fun (p : loc * loc) (k : block) => add_move (fst p) (snd p) k) + k moves) in *. + destruct (add_move_correct src dst k1 rs m) as [rs1 [A [B C]]]. + destruct (IHmoves rs1 m) as [rs' [D E]]. + exists rs'; split. + eapply exec_trans; eauto. traceEq. + econstructor; eauto. red. tauto. +Qed. + Theorem parallel_move_correct: forall srcs dsts k rs m, List.length srcs = List.length dsts -> @@ -675,13 +696,16 @@ Theorem parallel_move_correct: Loc.disjoint srcs temporaries -> Loc.disjoint dsts temporaries -> exists rs', - exec_instrs ge sp (parallel_move srcs dsts k) rs m k rs' m /\ + exec_instrs ge sp (parallel_move srcs dsts k) rs m E0 k rs' m /\ List.map rs' dsts = List.map rs srcs /\ rs' (R IT3) = rs (R IT3) /\ forall l, Loc.notin l dsts -> Loc.notin l temporaries -> rs' l = rs l. Proof. - apply (parallel_move_correctX ge sp). - apply add_move_correct. + intros. + generalize (effect_move_sequence k (parmove srcs dsts) rs m). + intros [rs' [EXEC EFFECT]]. + exists rs'. split. exact EXEC. + apply effect_parmove; auto. Qed. Lemma add_op_correct: @@ -690,7 +714,7 @@ Lemma add_op_correct: Loc.disjoint args temporaries -> eval_operation ge sp op (List.map rs args) = Some v -> exists rs', - exec_block ge sp (add_op op args res s) rs m (Cont s) rs' m /\ + exec_block ge sp (add_op op args res s) rs m E0 (Cont s) rs' m /\ rs' res = v /\ forall l, Loc.diff l res -> Loc.notin l temporaries -> rs' l = rs l. Proof. @@ -721,7 +745,7 @@ Proof. split. apply exec_Bgoto. eapply exec_trans. eexact EX1. eapply exec_trans; eauto. apply exec_one. unfold rs2. apply exec_Bop. - unfold rargs. rewrite RES1. auto. + unfold rargs. rewrite RES1. auto. traceEq. split. rewrite RES3. unfold rs2; apply Locmap.gss. intros. rewrite OTHER3. unfold rs2. rewrite Locmap.gso. apply OTHER1. assumption. @@ -737,7 +761,7 @@ Lemma add_load_correct: eval_addressing ge sp addr (List.map rs args) = Some a -> loadv chunk m a = Some v -> exists rs', - exec_block ge sp (add_load chunk addr args res s) rs m (Cont s) rs' m /\ + exec_block ge sp (add_load chunk addr args res s) rs m E0 (Cont s) rs' m /\ rs' res = v /\ forall l, Loc.diff l res -> Loc.notin l temporaries -> rs' l = rs l. Proof. @@ -755,7 +779,7 @@ Proof. split. apply exec_Bgoto. eapply exec_trans; eauto. eapply exec_trans; eauto. apply exec_one. unfold rs2. apply exec_Bload with a. - unfold rargs; rewrite RES1. assumption. assumption. + unfold rargs; rewrite RES1. assumption. assumption. traceEq. split. rewrite RES3. unfold rs2; apply Locmap.gss. intros. rewrite OTHER3. unfold rs2. rewrite Locmap.gso. apply OTHER1. assumption. @@ -772,7 +796,7 @@ Lemma add_store_correct: eval_addressing ge sp addr (List.map rs args) = Some a -> storev chunk m a (rs src) = Some m' -> exists rs', - exec_block ge sp (add_store chunk addr args src s) rs m (Cont s) rs' m' /\ + exec_block ge sp (add_store chunk addr args src s) rs m E0 (Cont s) rs' m' /\ forall l, Loc.notin l temporaries -> rs' l = rs l. Proof. intros. @@ -795,10 +819,42 @@ Proof. split. apply exec_Bgoto. eapply exec_trans. rewrite <- EQ. eexact EX1. apply exec_one. apply exec_Bstore with a. - rewrite RES2. assumption. rewrite RES3. assumption. + rewrite RES2. assumption. rewrite RES3. assumption. traceEq. exact OTHER1. Qed. +Lemma add_alloc_correct: + forall arg res s rs m m' sz b, + rs arg = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', b) -> + exists rs', + exec_block ge sp (add_alloc arg res s) rs m E0 (Cont s) rs' m' /\ + rs' res = Vptr b Int.zero /\ + forall l, + Loc.diff l (R Conventions.loc_alloc_argument) -> + Loc.diff l (R Conventions.loc_alloc_result) -> + Loc.diff l res -> + rs' l = rs l. +Proof. + intros; unfold add_alloc. + generalize (add_reload_correct arg loc_alloc_argument + (Balloc (add_spill loc_alloc_result res (Bgoto s))) + rs m). + intros [rs1 [EX1 [RES1 OTHER1]]]. + pose (rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1). + generalize (add_spill_correct loc_alloc_result res (Bgoto s) rs2 m'). + intros [rs3 [EX3 [RES3 OTHER3]]]. + exists rs3. + split. apply exec_Bgoto. eapply exec_trans. eexact EX1. + eapply exec_trans. apply exec_one. eapply exec_Balloc; eauto. congruence. + fold rs2. eexact EX3. reflexivity. traceEq. + split. rewrite RES3; unfold rs2. apply Locmap.gss. + intros. rewrite OTHER3. unfold rs2. rewrite Locmap.gso. + apply OTHER1. apply Loc.diff_sym; auto. + apply Loc.diff_sym; auto. + apply Loc.diff_sym; auto. +Qed. + Lemma add_cond_correct: forall cond args ifso ifnot rs m b s, (List.length args <= 3)%nat -> @@ -806,7 +862,7 @@ Lemma add_cond_correct: eval_condition cond (List.map rs args) = Some b -> s = (if b then ifso else ifnot) -> exists rs', - exec_block ge sp (add_cond cond args ifso ifnot) rs m (Cont s) rs' m /\ + exec_block ge sp (add_cond cond args ifso ifnot) rs m E0 (Cont s) rs' m /\ forall l, Loc.notin l temporaries -> rs' l = rs l. Proof. intros. unfold add_cond. @@ -825,7 +881,7 @@ Proof. exact OTHER1. Qed. -Definition find_function2 (los: loc + ident) (ls: locset) : option function := +Definition find_function2 (los: loc + ident) (ls: locset) : option fundef := match los with | inl l => Genv.find_funct ge (ls l) | inr symb => @@ -836,21 +892,21 @@ Definition find_function2 (los: loc + ident) (ls: locset) : option function := end. Lemma add_call_correct: - forall f vargs m vres m' sig los args res s ls + forall f vargs m t vres m' sig los args res s ls (EXECF: forall lsi, - List.map lsi (loc_arguments f.(fn_sig)) = vargs -> + List.map lsi (loc_arguments (funsig f)) = vargs -> exists lso, - exec_function ge f lsi m lso m' - /\ lso (R (loc_result f.(fn_sig))) = vres) + exec_function ge f lsi m t lso m' + /\ lso (R (loc_result (funsig f))) = vres) (FIND: find_function2 los ls = Some f) - (SIG: sig = f.(fn_sig)) + (SIG: sig = funsig f) (VARGS: List.map ls args = vargs) (LARGS: List.length args = List.length sig.(sig_args)) (AARGS: locs_acceptable args) (RES: loc_acceptable res), exists ls', - exec_block ge sp (add_call sig los args res s) ls m (Cont s) ls' m' /\ + exec_block ge sp (add_call sig los args res s) ls m t (Cont s) ls' m' /\ ls' res = vres /\ forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l res -> @@ -896,7 +952,7 @@ Proof. eapply exec_trans. apply exec_one. apply exec_Bcall with f. unfold find_function. rewrite TMP2. rewrite RES1. assumption. assumption. eexact EX3. - exact EX5. + eexact EX5. reflexivity. reflexivity. traceEq. (* Result *) split. rewrite RES5. unfold ls4. rewrite return_regs_result. assumption. @@ -936,7 +992,7 @@ Proof. eapply exec_trans. eexact EX2. eapply exec_trans. apply exec_one. apply exec_Bcall with f. unfold find_function. assumption. assumption. eexact EX3. - exact EX5. + eexact EX5. reflexivity. traceEq. (* Result *) split. rewrite RES5. unfold ls4. rewrite return_regs_result. @@ -955,7 +1011,7 @@ Lemma add_undefs_correct: (forall l, In l res -> loc_acceptable l) -> (forall ofs ty, In (S (Local ofs ty)) res -> ls (S (Local ofs ty)) = Vundef) -> exists ls', - exec_instrs ge sp (add_undefs res b) ls m b ls' m /\ + exec_instrs ge sp (add_undefs res b) ls m E0 b ls' m /\ (forall l, In l res -> ls' l = Vundef) /\ (forall l, Loc.notin l res -> ls' l = ls l). Proof. @@ -972,7 +1028,7 @@ Proof. intros [ls2 [EX2 [RES2 OTHER2]]]. exists ls2. split. eapply exec_trans. apply exec_one. apply exec_Bop. - simpl; reflexivity. exact EX2. + simpl; reflexivity. eexact EX2. traceEq. split. intros. case (In_dec Loc.eq l res); intro. apply RES2; auto. rewrite OTHER2. elim H1; intro. @@ -1006,7 +1062,7 @@ Lemma add_entry_correct: locs_acceptable undefs -> (forall ofs ty, ls (S (Local ofs ty)) = Vundef) -> exists ls', - exec_block ge sp (add_entry sig params undefs s) ls m (Cont s) ls' m /\ + exec_block ge sp (add_entry sig params undefs s) ls m E0 (Cont s) ls' m /\ List.map ls' params = List.map ls (loc_parameters sig) /\ (forall l, In l undefs -> ls' l = Vundef). Proof. @@ -1029,7 +1085,7 @@ Proof. intros [ls2 [EX2 [RES2 OTHER2]]]. exists ls2. split. apply exec_Bgoto. unfold add_entry. - eapply exec_trans. eexact EX1. eexact EX2. + eapply exec_trans. eexact EX1. eexact EX2. traceEq. split. rewrite <- RES1. apply list_map_exten. intros. symmetry. apply OTHER2. eapply Loc.disjoint_notin; eauto. exact RES2. @@ -1038,7 +1094,7 @@ Qed. Lemma add_return_correct: forall sig optarg ls m, exists ls', - exec_block ge sp (add_return sig optarg) ls m Return ls' m /\ + exec_block ge sp (add_return sig optarg) ls m E0 Return ls' m /\ match optarg with | Some arg => ls' (R (loc_result sig)) = ls arg | None => ls' (R (loc_result sig)) = Vundef @@ -1131,51 +1187,53 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intro. unfold ge, tge. - apply Genv.find_symbol_transf_partial with transf_function. + apply Genv.find_symbol_transf_partial with transf_fundef. exact TRANSF. Qed. Lemma functions_translated: - forall (v: val) (f: RTL.function), + forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transf_function f = Some tf. + Genv.find_funct tge v = Some tf /\ transf_fundef f = Some tf. Proof. intros. generalize - (Genv.find_funct_transf_partial transf_function TRANSF H). - case (transf_function f). + (Genv.find_funct_transf_partial transf_fundef TRANSF H). + case (transf_fundef f). intros tf [A B]. exists tf. tauto. intros [A B]. elim B. reflexivity. Qed. Lemma function_ptr_translated: - forall (b: Values.block) (f: RTL.function), + forall (b: Values.block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_function f = Some tf. + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Some tf. Proof. intros. generalize - (Genv.find_funct_ptr_transf_partial transf_function TRANSF H). - case (transf_function f). + (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF H). + case (transf_fundef f). intros tf [A B]. exists tf. tauto. intros [A B]. elim B. reflexivity. Qed. Lemma sig_function_translated: forall f tf, - transf_function f = Some tf -> - tf.(LTL.fn_sig) = f.(RTL.fn_sig). + transf_fundef f = Some tf -> + LTL.funsig tf = RTL.funsig f. Proof. - intros f tf. unfold transf_function. - destruct (type_rtl_function f). + intros f tf. destruct f; simpl. + unfold transf_function. + destruct (type_function f). destruct (analyze f). - destruct (regalloc f t0). + destruct (regalloc f t). intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto. - intros; discriminate. - intros; discriminate. - intros; discriminate. + congruence. congruence. congruence. + destruct (type_external_function e). + intro EQ; inversion EQ; subst tf. reflexivity. + congruence. Qed. Lemma entrypoint_function_translated: @@ -1184,9 +1242,9 @@ Lemma entrypoint_function_translated: tf.(LTL.fn_entrypoint) = f.(RTL.fn_nextpc). Proof. intros f tf. unfold transf_function. - destruct (type_rtl_function f). + destruct (type_function f). destruct (analyze f). - destruct (regalloc f t0). + destruct (regalloc f t). intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto. intros; discriminate. intros; discriminate. @@ -1220,43 +1278,43 @@ Qed. Definition exec_instr_prop (c: RTL.code) (sp: val) - (pc: node) (rs: regset) (m: mem) + (pc: node) (rs: regset) (m: mem) (t: trace) (pc': node) (rs': regset) (m': mem) : Prop := forall f env live assign ls (CF: c = f.(RTL.fn_code)) - (WT: wt_function env f) + (WT: wt_function f env) (ASG: regalloc f live (live0 f live) env = Some assign) (AG: agree assign (transfer f pc live!!pc) rs ls), let tc := PTree.map (transf_instr f live assign) c in exists ls', - exec_blocks tge tc sp pc ls m (Cont pc') ls' m' /\ + exec_blocks tge tc sp pc ls m t (Cont pc') ls' m' /\ agree assign live!!pc rs' ls'. Definition exec_instrs_prop (c: RTL.code) (sp: val) - (pc: node) (rs: regset) (m: mem) + (pc: node) (rs: regset) (m: mem) (t: trace) (pc': node) (rs': regset) (m': mem) : Prop := forall f env live assign ls, forall (CF: c = f.(RTL.fn_code)) - (WT: wt_function env f) + (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) (VALIDPC': c!pc' <> None), let tc := PTree.map (transf_instr f live assign) c in exists ls', - exec_blocks tge tc sp pc ls m (Cont pc') ls' m' /\ + exec_blocks tge tc sp pc ls m t (Cont pc') ls' m' /\ agree assign (transfer f pc' live!!pc') rs' ls'. Definition exec_function_prop - (f: RTL.function) (args: list val) (m: mem) - (res: val) (m': mem) : Prop := + (f: RTL.fundef) (args: list val) (m: mem) + (t: trace) (res: val) (m': mem) : Prop := forall ls tf, - transf_function f = Some tf -> - List.map ls (Conventions.loc_arguments tf.(fn_sig)) = args -> + transf_fundef f = Some tf -> + List.map ls (Conventions.loc_arguments (funsig tf)) = args -> exists ls', - LTL.exec_function tge tf ls m ls' m' /\ - ls' (R (Conventions.loc_result tf.(fn_sig))) = res. + LTL.exec_function tge tf ls m t ls' m' /\ + ls' (R (Conventions.loc_result (funsig tf))) = res. (** The simulation proof is by structural induction over the RTL evaluation derivation. We prove each case of the proof as a separate lemma. @@ -1298,7 +1356,7 @@ Lemma transl_Inop_correct: forall (c : PTree.t instruction) (sp: val) (pc : positive) (rs : regset) (m : mem) (pc' : RTL.node), c ! pc = Some (Inop pc') -> - exec_instr_prop c sp pc rs m pc' rs m. + exec_instr_prop c sp pc rs m E0 pc' rs m. Proof. intros; red; intros; CleanupHyps. exists ls. split. @@ -1312,7 +1370,7 @@ Lemma transl_Iop_correct: (res : reg) (pc' : RTL.node) (v: val), c ! pc = Some (Iop op args res pc') -> eval_operation ge sp op (rs ## args) = Some v -> - exec_instr_prop c sp pc rs m pc' (rs # res <- v) m. + exec_instr_prop c sp pc rs m E0 pc' (rs # res <- v) m. Proof. intros; red; intros; CleanupHyps. caseEq (Regset.mem res live!!pc); intro LV; @@ -1364,7 +1422,7 @@ Lemma transl_Iload_correct: c ! pc = Some (Iload chunk addr args dst pc') -> eval_addressing ge sp addr rs ## args = Some a -> loadv chunk m a = Some v -> - exec_instr_prop c sp pc rs m pc' rs # dst <- v m. + exec_instr_prop c sp pc rs m E0 pc' rs # dst <- v m. Proof. intros; red; intros; CleanupHyps. caseEq (Regset.mem dst live!!pc); intro LV; @@ -1407,7 +1465,7 @@ Lemma transl_Istore_correct: c ! pc = Some (Istore chunk addr args src pc') -> eval_addressing ge sp addr rs ## args = Some a -> storev chunk m a rs # src = Some m' -> - exec_instr_prop c sp pc rs m pc' rs m'. + exec_instr_prop c sp pc rs m E0 pc' rs m'. Proof. intros; red; intros; CleanupHyps. assert (LL: (List.length (List.map assign args) <= 2)%nat). @@ -1444,19 +1502,19 @@ Lemma transl_Icall_correct: forall (c : PTree.t instruction) (sp: val) (pc : positive) (rs : regset) (m : mem) (sig : signature) (ros : reg + ident) (args : list reg) (res : reg) (pc' : RTL.node) - (f : RTL.function) (vres : val) (m' : mem), + (f : RTL.fundef) (vres : val) (m' : mem) (t: trace), c ! pc = Some (Icall sig ros args res pc') -> RTL.find_function ge ros rs = Some f -> - sig = RTL.fn_sig f -> - RTL.exec_function ge f (rs##args) m vres m' -> - exec_function_prop f (rs##args) m vres m' -> - exec_instr_prop c sp pc rs m pc' (rs#res <- vres) m'. + RTL.funsig f = sig -> + RTL.exec_function ge f (rs##args) m t vres m' -> + exec_function_prop f (rs##args) m t vres m' -> + exec_instr_prop c sp pc rs m t pc' (rs#res <- vres) m'. Proof. intros; red; intros; CleanupHyps. set (los := sum_left_map assign ros). assert (FIND: exists tf, find_function2 tge los ls = Some tf /\ - transf_function f = Some tf). + transf_fundef f = Some tf). unfold los. destruct ros; simpl; simpl in H0. apply functions_translated. replace (ls (assign r)) with rs#r. assumption. @@ -1466,7 +1524,7 @@ Proof. apply function_ptr_translated. auto. discriminate. elim FIND; intros tf [AFIND TRF]; clear FIND. - assert (ASIG: sig = fn_sig tf). + assert (ASIG: sig = funsig tf). rewrite (sig_function_translated _ _ TRF). auto. generalize (fun ls => H3 ls tf TRF); intro AEXECF. assert (AVARGS: List.map ls (List.map assign args) = rs##args). @@ -1482,7 +1540,7 @@ Proof. unfold correct_alloc_instr. intros [CORR1 CORR2]. assert (ARES: loc_acceptable (assign res)). eapply regalloc_acceptable; eauto. - generalize (add_call_correct tge sp tf _ _ _ _ _ _ _ _ pc' _ + generalize (add_call_correct tge sp tf _ _ _ _ _ _ _ _ _ pc' _ AEXECF AFIND ASIG AVARGS ALARGS AACCEPT ARES). intros [ls' [EX [RES OTHER]]]. @@ -1491,13 +1549,42 @@ Proof. simpl. eapply agree_call; eauto. Qed. +Lemma transl_Ialloc_correct: + forall (c : PTree.t instruction) (sp: val) (pc : positive) + (rs : Regmap.t val) (m : mem) (pc': RTL.node) (arg res: reg) + (sz: int) (m': mem) (b: Values.block), + c ! pc = Some (Ialloc arg res pc') -> + rs#arg = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', b) -> + exec_instr_prop c sp pc rs m E0 pc' (rs # res <- (Vptr b Int.zero)) m'. +Proof. + intros; red; intros; CleanupHyps. + assert (SZ: ls (assign arg) = Vint sz). + rewrite <- H0. eapply agree_eval_reg. eauto. + generalize (add_alloc_correct tge sp (assign arg) (assign res) + pc' ls m m' sz b SZ H1). + intros [ls' [EX [RES OTHER]]]. + exists ls'. + split. CleanupGoal. exact EX. + rewrite CF in H. + generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). + unfold correct_alloc_instr. intros [CORR1 CORR2]. + eapply agree_call with (args := arg :: nil) (ros := inr reg 1%positive) (ls := ls) (ls' := ls'); eauto. + intros. apply OTHER. + eapply Loc.in_notin_diff; eauto. + unfold loc_alloc_argument, destroyed_at_call; simpl; tauto. + eapply Loc.in_notin_diff; eauto. + unfold loc_alloc_argument, destroyed_at_call; simpl; tauto. + auto. +Qed. + Lemma transl_Icond_true_correct: forall (c : PTree.t instruction) (sp: val) (pc : positive) (rs : Regmap.t val) (m : mem) (cond : condition) (args : list reg) (ifso ifnot : RTL.node), c ! pc = Some (Icond cond args ifso ifnot) -> eval_condition cond rs ## args = Some true -> - exec_instr_prop c sp pc rs m ifso rs m. + exec_instr_prop c sp pc rs m E0 ifso rs m. Proof. intros; red; intros; CleanupHyps. assert (LL: (List.length (map assign args) <= 3)%nat). @@ -1523,7 +1610,7 @@ Lemma transl_Icond_false_correct: (ifso ifnot : RTL.node), c ! pc = Some (Icond cond args ifso ifnot) -> eval_condition cond rs ## args = Some false -> - exec_instr_prop c sp pc rs m ifnot rs m. + exec_instr_prop c sp pc rs m E0 ifnot rs m. Proof. intros; red; intros; CleanupHyps. assert (LL: (List.length (map assign args) <= 3)%nat). @@ -1545,7 +1632,7 @@ Qed. Lemma transl_refl_correct: forall (c : RTL.code) (sp: val) (pc : RTL.node) (rs : regset) - (m : mem), exec_instrs_prop c sp pc rs m pc rs m. + (m : mem), exec_instrs_prop c sp pc rs m E0 pc rs m. Proof. intros; red; intros. exists ls. split. apply exec_blocks_refl. assumption. @@ -1553,10 +1640,10 @@ Qed. Lemma transl_one_correct: forall (c : RTL.code) (sp: val) (pc : RTL.node) (rs : regset) - (m : mem) (pc' : RTL.node) (rs' : regset) (m' : mem), - RTL.exec_instr ge c sp pc rs m pc' rs' m' -> - exec_instr_prop c sp pc rs m pc' rs' m' -> - exec_instrs_prop c sp pc rs m pc' rs' m'. + (m : mem) (t: trace) (pc' : RTL.node) (rs' : regset) (m' : mem), + RTL.exec_instr ge c sp pc rs m t pc' rs' m' -> + exec_instr_prop c sp pc rs m t pc' rs' m' -> + exec_instrs_prop c sp pc rs m t pc' rs' m'. Proof. intros; red; intros. generalize (H0 f env live assign ls CF WT ASG AG). @@ -1573,13 +1660,14 @@ Qed. Lemma transl_trans_correct: forall (c : RTL.code) (sp: val) (pc1 : RTL.node) (rs1 : regset) - (m1 : mem) (pc2 : RTL.node) (rs2 : regset) (m2 : mem) - (pc3 : RTL.node) (rs3 : regset) (m3 : mem), - RTL.exec_instrs ge c sp pc1 rs1 m1 pc2 rs2 m2 -> - exec_instrs_prop c sp pc1 rs1 m1 pc2 rs2 m2 -> - RTL.exec_instrs ge c sp pc2 rs2 m2 pc3 rs3 m3 -> - exec_instrs_prop c sp pc2 rs2 m2 pc3 rs3 m3 -> - exec_instrs_prop c sp pc1 rs1 m1 pc3 rs3 m3. + (m1 : mem) (t1: trace) (pc2 : RTL.node) (rs2 : regset) (m2 : mem) + (t2: trace) (pc3 : RTL.node) (rs3 : regset) (m3 : mem) (t3: trace), + RTL.exec_instrs ge c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + exec_instrs_prop c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + RTL.exec_instrs ge c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> + exec_instrs_prop c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> + t3 = t1 ** t2 -> + exec_instrs_prop c sp pc1 rs1 m1 t3 pc3 rs3 m3. Proof. intros; red; intros. assert (VALIDPC2: c!pc2 <> None). @@ -1589,7 +1677,7 @@ Proof. generalize (H2 f env live assign ls1 CF WT ANL ASG AG1 VALIDPC'). intros [ls2 [EX2 AG2]]. exists ls2. split. - eapply exec_blocks_trans. eexact EX1. exact EX2. + eapply exec_blocks_trans. eexact EX1. eexact EX2. auto. exact AG2. Qed. @@ -1609,14 +1697,14 @@ Qed. Lemma transf_entrypoint_correct: forall f env live assign c ls args sp m, - wt_function env f -> + wt_function f env -> regalloc f live (live0 f live) env = Some assign -> c!(RTL.fn_nextpc f) = None -> List.map ls (loc_parameters (RTL.fn_sig f)) = args -> (forall ofs ty, ls (S (Local ofs ty)) = Vundef) -> let tc := transf_entrypoint f live assign c in exists ls', - exec_blocks tge tc sp (RTL.fn_nextpc f) ls m + exec_blocks tge tc sp (RTL.fn_nextpc f) ls m E0 (Cont (RTL.fn_entrypoint f)) ls' m /\ agree assign (transfer f (RTL.fn_entrypoint f) live!!(RTL.fn_entrypoint f)) (init_regs args (RTL.fn_params f)) ls'. @@ -1680,20 +1768,20 @@ Qed. Lemma transl_function_correct: forall (f : RTL.function) (m m1 : mem) (stk : Values.block) - (args : list val) (pc : RTL.node) (rs : regset) (m2 : mem) + (args : list val) (t: trace) (pc : RTL.node) (rs : regset) (m2 : mem) (or : option reg) (vres : val), alloc m 0 (RTL.fn_stacksize f) = (m1, stk) -> RTL.exec_instrs ge (RTL.fn_code f) (Vptr stk Int.zero) - (RTL.fn_entrypoint f) (init_regs args (fn_params f)) m1 pc rs m2 -> + (RTL.fn_entrypoint f) (init_regs args (fn_params f)) m1 t pc rs m2 -> exec_instrs_prop (RTL.fn_code f) (Vptr stk Int.zero) - (RTL.fn_entrypoint f) (init_regs args (fn_params f)) m1 pc rs m2 -> + (RTL.fn_entrypoint f) (init_regs args (fn_params f)) m1 t pc rs m2 -> (RTL.fn_code f) ! pc = Some (Ireturn or) -> vres = regmap_optget or Vundef rs -> - exec_function_prop f args m vres (free m2 stk). + exec_function_prop (Internal f) args m t vres (free m2 stk). Proof. intros; red; intros until tf. - unfold transf_function. - caseEq (type_rtl_function f). + unfold transf_fundef, transf_function. + caseEq (type_function f). intros env TRF. caseEq (analyze f). intros live ANL. @@ -1704,7 +1792,7 @@ Proof. set (tc1 := PTree.map (transf_instr f live alloc) (RTL.fn_code f)). set (tc2 := transf_entrypoint f live alloc tc1). intro EQ; injection EQ; intro TF; clear EQ. intro VARGS. - generalize (type_rtl_function_correct _ _ TRF); intro WTF. + generalize (type_function_correct _ _ TRF); intro WTF. assert (NEWINSTR: tc1!(RTL.fn_nextpc f) = None). unfold tc1; rewrite PTree.gmap. unfold option_map. elim (RTL.fn_code_wf f (fn_nextpc f)); intro. @@ -1712,7 +1800,7 @@ Proof. rewrite H4. auto. pose (ls1 := call_regs ls). assert (VARGS1: List.map ls1 (loc_parameters (RTL.fn_sig f)) = args). - replace (RTL.fn_sig f) with (fn_sig tf). + replace (RTL.fn_sig f) with (funsig tf). rewrite <- VARGS. unfold loc_parameters. rewrite list_map_compose. apply list_map_exten. intros. symmetry. unfold ls1. eapply call_regs_param_of_arg; eauto. @@ -1732,9 +1820,9 @@ Proof. intros [ls4 [EX4 RES4]]. exists ls4. (* Execution *) - split. apply exec_funct with m1. - rewrite <- TF; simpl; assumption. - rewrite <- TF; simpl. fold ls1. + split. rewrite <- TF; apply exec_funct_internal with m1; simpl. + assumption. + fold ls1. eapply exec_blocks_trans. eexact EX2. apply exec_blocks_extends with tc1. intro p. unfold tc2. unfold transf_entrypoint. @@ -1746,7 +1834,7 @@ Proof. eapply exec_blocks_trans. eexact EX3. eapply exec_blocks_one. unfold tc1. rewrite PTree.gmap. rewrite H2. simpl. reflexivity. - exact EX4. + eexact EX4. reflexivity. traceEq. destruct or. simpl in RES4. simpl in H3. rewrite H3. rewrite <- TF; simpl. rewrite RES4. @@ -1760,6 +1848,20 @@ Proof. intros; discriminate. Qed. +Lemma transl_external_function_correct: + forall (ef : external_function) (args : list val) (m : mem) + (t: trace) (res: val), + event_match ef args t res -> + exec_function_prop (External ef) args m t res m. +Proof. + intros; red; intros. + simpl in H0. + destruct (type_external_function ef); simplify_eq H0; intro. + exists (Locmap.set (R (loc_result (funsig tf))) res ls); split. + subst tf. eapply exec_funct_external; eauto. + apply Locmap.gss. +Qed. + (** The correctness of the code transformation is obtained by structural induction (and case analysis on the last rule used) on the RTL evaluation derivation. @@ -1767,14 +1869,10 @@ Qed. [exec_instrs_prop] and [exec_function_prop] as the induction hypotheses, and the lemmas above as cases for the induction. *) -Scheme exec_instr_ind_3 := Minimality for RTL.exec_instr Sort Prop - with exec_instrs_ind_3 := Minimality for RTL.exec_instrs Sort Prop - with exec_function_ind_3 := Minimality for RTL.exec_function Sort Prop. - Theorem transl_function_correctness: - forall f args m res m', - RTL.exec_function ge f args m res m' -> - exec_function_prop f args m res m'. + forall f args m t res m', + RTL.exec_function ge f args m t res m' -> + exec_function_prop f args m t res m'. Proof (exec_function_ind_3 ge exec_instr_prop @@ -1786,6 +1884,7 @@ Proof transl_Iload_correct transl_Istore_correct transl_Icall_correct + transl_Ialloc_correct transl_Icond_true_correct transl_Icond_false_correct @@ -1793,23 +1892,24 @@ Proof transl_one_correct transl_trans_correct - transl_function_correct). + transl_function_correct + transl_external_function_correct). (** The semantic equivalence between the original and transformed programs follows easily. *) Theorem transl_program_correct: - forall (r: val), - RTL.exec_program prog r -> LTL.exec_program tprog r. + forall (t: trace) (r: val), + RTL.exec_program prog t r -> LTL.exec_program tprog t r. Proof. - intros r [b [f [m [FIND1 [FIND2 [SIG EXEC]]]]]]. + intros t r [b [f [m [FIND1 [FIND2 [SIG EXEC]]]]]]. generalize (function_ptr_translated _ _ FIND2). intros [tf [TFIND TRF]]. - assert (SIG2: tf.(fn_sig) = mksignature nil (Some Tint)). + assert (SIG2: funsig tf = mksignature nil (Some Tint)). rewrite <- SIG. apply sig_function_translated; auto. - assert (VPARAMS: map (Locmap.init Vundef) (loc_arguments (fn_sig tf)) = nil). + assert (VPARAMS: map (Locmap.init Vundef) (loc_arguments (funsig tf)) = nil). rewrite SIG2. reflexivity. - generalize (transl_function_correctness _ _ _ _ _ EXEC + generalize (transl_function_correctness _ _ _ _ _ _ EXEC (Locmap.init Vundef) tf TRF VPARAMS). intros [ls' [TEXEC RES]]. red. exists b; exists tf; exists ls'; exists m. |