diff options
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 982 | ||||
| -rw-r--r-- | mppa_k1c/lib/ForwardSimulationBlock.v | 387 | ||||
| -rw-r--r-- | mppa_k1c/lib/Machblock.v | 380 | ||||
| -rw-r--r-- | mppa_k1c/lib/Machblockgen.v | 216 | ||||
| -rw-r--r-- | mppa_k1c/lib/Machblockgenproof.v | 824 |
5 files changed, 0 insertions, 2789 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v deleted file mode 100644 index 1af59238..00000000 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ /dev/null @@ -1,982 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* Xavier Leroy INRIA Paris-Rocquencourt *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -(** * "block" version of Asmgenproof0 - - This module is largely adapted from Asmgenproof0.v of the other backends - It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends - It has similar definitions than Asmgenproof0, but adapted to this new structure *) - -Require Import Coqlib. -Require Intv. -Require Import AST. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Locations. -Require Import Machblock. -Require Import Asmblock. -Require Import Asmblockgen. -Require Import Conventions1. -Require Import Axioms. -Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) -Require Import Asmblockprops. - -Module MB:=Machblock. -Module AB:=Asmblock. - -Lemma ireg_of_eq: - forall r r', ireg_of r = OK r' -> preg_of r = IR r'. -Proof. - unfold ireg_of; intros. destruct (preg_of r); inv H; auto. -Qed. - -Lemma freg_of_eq: - forall r r', freg_of r = OK r' -> preg_of r = IR r'. -Proof. - unfold freg_of; intros. destruct (preg_of r); inv H; auto. -Qed. - -Lemma preg_of_injective: - forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. -Proof. - destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. -Qed. - -Lemma undef_regs_other: - forall r rl rs, - (forall r', In r' rl -> r <> r') -> - undef_regs rl rs r = rs r. -Proof. - induction rl; simpl; intros. auto. - rewrite IHrl by auto. rewrite Pregmap.gso; auto. -Qed. - -Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop := - match rl with - | nil => True - | r1 :: nil => r <> preg_of r1 - | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl - end. - -Remark preg_notin_charact: - forall r rl, - preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr). -Proof. - induction rl; simpl; intros. - tauto. - destruct rl. - simpl. split. intros. intuition congruence. auto. - rewrite IHrl. split. - intros [A B]. intros. destruct H. congruence. auto. - auto. -Qed. - -Lemma undef_regs_other_2: - forall r rl rs, - preg_notin r rl -> - undef_regs (map preg_of rl) rs r = rs r. -Proof. - intros. apply undef_regs_other. intros. - exploit list_in_map_inv; eauto. intros [mr [A B]]. subst. - rewrite preg_notin_charact in H. auto. -Qed. - -(** * Agreement between Mach registers and processor registers *) - -Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree { - agree_sp: rs#SP = sp; - agree_sp_def: sp <> Vundef; - agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) -}. - -Lemma preg_val: - forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). -Proof. - intros. destruct H. auto. -Qed. - -Lemma preg_vals: - forall ms sp rs, agree ms sp rs -> - forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)). -Proof. - induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto. -Qed. - -Lemma sp_val: - forall ms sp rs, agree ms sp rs -> sp = rs#SP. -Proof. - intros. destruct H; auto. -Qed. - -Lemma ireg_val: - forall ms sp rs r r', - agree ms sp rs -> - ireg_of r = OK r' -> - Val.lessdef (ms r) rs#r'. -Proof. - intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto. -Qed. - -Lemma freg_val: - forall ms sp rs r r', - agree ms sp rs -> - freg_of r = OK r' -> - Val.lessdef (ms r) (rs#r'). -Proof. - intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto. -Qed. - -Lemma agree_exten: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, data_preg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. destruct H. split; auto. - rewrite H0; auto. auto. - intros. rewrite H0; auto. apply preg_of_data. -Qed. - -(** Preservation of register agreement under various assignments. *) - -Lemma agree_set_mreg: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Mach.Regmap.set r v ms) sp rs'. -Proof. - intros. destruct H. split; auto. - rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP. - intros. unfold Mach.Regmap.set. destruct (Mach.RegEq.eq r0 r). congruence. - rewrite H1. auto. apply preg_of_data. - red; intros; elim n. eapply preg_of_injective; eauto. -Qed. - -Corollary agree_set_mreg_parallel: - forall ms sp rs r v v', - agree ms sp rs -> - Val.lessdef v v' -> - agree (Mach.Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs). -Proof. - intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto. -Qed. - -Lemma agree_set_other: - forall ms sp rs r v, - agree ms sp rs -> - data_preg r = false -> - agree ms sp (rs#r <- v). -Proof. - intros. apply agree_exten with rs. auto. - intros. apply Pregmap.gso. congruence. -Qed. - -Lemma agree_nextblock: - forall ms sp rs b, - agree ms sp rs -> agree ms sp (nextblock b rs). -Proof. - intros. unfold nextblock. apply agree_set_other. auto. auto. -Qed. - -Lemma agree_set_pair: - forall sp p v v' ms rs, - agree ms sp rs -> - Val.lessdef v v' -> - agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs). -Proof. - intros. destruct p; simpl. -- apply agree_set_mreg_parallel; auto. -- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. - apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. -Qed. - -Lemma agree_undef_nondata_regs: - forall ms sp rl rs, - agree ms sp rs -> - (forall r, In r rl -> data_preg r = false) -> - agree ms sp (undef_regs rl rs). -Proof. - induction rl; simpl; intros. auto. - apply IHrl. apply agree_exten with rs; auto. - intros. apply Pregmap.gso. red; intros; subst. - assert (data_preg a = false) by auto. congruence. - intros. apply H0; auto. -Qed. - -Lemma agree_undef_regs: - forall ms sp rl rs rs', - agree ms sp rs -> - (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') -> - agree (Mach.undef_regs rl ms) sp rs'. -Proof. - intros. destruct H. split; auto. - rewrite <- agree_sp0. apply H0; auto. - rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP. - intros. destruct (In_dec mreg_eq r rl). - rewrite Mach.undef_regs_same; auto. - rewrite Mach.undef_regs_other; auto. rewrite H0; auto. - apply preg_of_data. - rewrite preg_notin_charact. intros; red; intros. elim n. - exploit preg_of_injective; eauto. congruence. -Qed. - -Lemma agree_set_undef_mreg: - forall ms sp rs r v rl rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') -> - agree (Mach.Regmap.set r v (Mach.undef_regs rl ms)) sp rs'. -Proof. - intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. - apply agree_undef_regs with rs; auto. - intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)). - congruence. auto. - intros. rewrite Pregmap.gso; auto. -Qed. - -Lemma agree_undef_caller_save_regs: - forall ms sp rs, - agree ms sp rs -> - agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). -Proof. - intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. -- unfold proj_sumbool; rewrite dec_eq_true. auto. -- auto. -- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). - destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. -+ apply list_in_map_inv in i. destruct i as (mr & A & B). - assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. - apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. -+ destruct (is_callee_save r) eqn:CS; auto. - elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. -Qed. - -Lemma agree_change_sp: - forall ms sp rs sp', - agree ms sp rs -> sp' <> Vundef -> - agree ms sp' (rs#SP <- sp'). -Proof. - intros. inv H. split; auto. - intros. rewrite Pregmap.gso; auto with asmgen. -Qed. - -(** Connection between Mach and Asm calling conventions for external - functions. *) - -Lemma extcall_arg_match: - forall ms sp rs m m' l v, - agree ms sp rs -> - Mem.extends m m' -> - Mach.extcall_arg ms m sp l v -> - exists v', AB.extcall_arg rs m' l v' /\ Val.lessdef v v'. -Proof. - intros. inv H1. - exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. - unfold Mach.load_stack in H2. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ H) in A. - exists v'; split; auto. - econstructor. eauto. assumption. -Qed. - -Lemma extcall_arg_pair_match: - forall ms sp rs m m' p v, - agree ms sp rs -> - Mem.extends m m' -> - Mach.extcall_arg_pair ms m sp p v -> - exists v', AB.extcall_arg_pair rs m' p v' /\ Val.lessdef v v'. -Proof. - intros. inv H1. -- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. -- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). - exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). - exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. -Qed. - - -Lemma extcall_args_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall ll vl, - list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl -> - exists vl', list_forall2 (AB.extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'. -Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit extcall_arg_pair_match; eauto. intros [v1' [A B]]. - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. -Qed. - -Lemma extcall_arguments_match: - forall ms m m' sp rs sg args, - agree ms sp rs -> Mem.extends m m' -> - Mach.extcall_arguments ms m sp sg args -> - exists args', AB.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. -Proof. - unfold Mach.extcall_arguments, AB.extcall_arguments; intros. - eapply extcall_args_match; eauto. -Qed. - -Remark builtin_arg_match: - forall ge (rs: regset) sp m a v, - eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v -> - eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v. -Proof. - induction 1; simpl; eauto with barg. -Qed. - -Lemma builtin_args_match: - forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall al vl, eval_builtin_args ge ms sp m al vl -> - exists vl', eval_builtin_args ge rs sp m' (map (map_builtin_arg preg_of) al) vl' - /\ Val.lessdef_list vl vl'. -Proof. - induction 3; intros; simpl. - exists (@nil val); split; constructor. - exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. - intros; eapply preg_val; eauto. - intros (v1' & A & B). - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto. -Qed. - -Lemma agree_set_res: - forall res ms sp rs v v', - agree ms sp rs -> - Val.lessdef v v' -> - agree (Mach.set_res res v ms) sp (AB.set_res (map_builtin_res preg_of res) v' rs). -Proof. - induction res; simpl; intros. -- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. - intros. apply Pregmap.gso; auto. -- auto. -- apply IHres2. apply IHres1. auto. - apply Val.hiword_lessdef; auto. - apply Val.loword_lessdef; auto. -Qed. - -Lemma set_res_other: - forall r res v rs, - data_preg r = false -> - set_res (map_builtin_res preg_of res) v rs r = rs r. -Proof. - induction res; simpl; intros. -- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate. -- auto. -- rewrite IHres2, IHres1; auto. -Qed. - -(* inspired from Mach *) - -Lemma find_label_tail: - forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c. -Proof. - induction c; simpl; intros. discriminate. - destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib. -Qed. - -(* inspired from Asmgenproof0 *) - -(* ... skip ... *) - -(** The ``code tail'' of an instruction list [c] is the list of instructions - starting at PC [pos]. *) - -Inductive code_tail: Z -> bblocks -> bblocks -> Prop := - | code_tail_0: forall c, - code_tail 0 c c - | code_tail_S: forall pos bi c1 c2, - code_tail pos c1 c2 -> - code_tail (pos + (size bi)) (bi :: c1) c2. - -Lemma code_tail_pos: - forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. -Proof. - induction 1. omega. generalize (size_positive bi); intros; omega. -Qed. - -Lemma find_bblock_tail: - forall c1 bi c2 pos, - code_tail pos c1 (bi :: c2) -> - find_bblock pos c1 = Some bi. -Proof. - induction c1; simpl; intros. - inversion H. - destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega. - destruct (zeq pos 0). subst pos. - inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. - inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega. - eauto. -Qed. - - -Local Hint Resolve code_tail_0 code_tail_S: core. - -Lemma code_tail_next: - forall fn ofs c0, - code_tail ofs fn c0 -> - forall bi c1, c0 = bi :: c1 -> code_tail (ofs + (size bi)) fn c1. -Proof. - induction 1; intros. - - subst; eauto. - - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto. - omega. -Qed. - -Lemma size_blocks_pos c: 0 <= size_blocks c. -Proof. - induction c as [| a l ]; simpl; try omega. - generalize (size_positive a); omega. -Qed. - -Remark code_tail_positive: - forall fn ofs c, - code_tail ofs fn c -> 0 <= ofs. -Proof. - induction 1; intros; simpl. - - omega. - - generalize (size_positive bi). omega. -Qed. - -Remark code_tail_size: - forall fn ofs c, - code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c. -Proof. - induction 1; intros; simpl; try omega. -Qed. - -Remark code_tail_bounds fn ofs c: - code_tail ofs fn c -> 0 <= ofs <= size_blocks fn. -Proof. - intro H; - exploit code_tail_size; eauto. - generalize (code_tail_positive _ _ _ H), (size_blocks_pos c). - omega. -Qed. - -Local Hint Resolve code_tail_next: core. - -Lemma code_tail_next_int: - forall fn ofs bi c, - size_blocks fn <= Ptrofs.max_unsigned -> - code_tail (Ptrofs.unsigned ofs) fn (bi :: c) -> - code_tail (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bi)))) fn c. -Proof. - intros. - exploit code_tail_size; eauto. - simpl; generalize (code_tail_positive _ _ _ H0), (size_positive bi), (size_blocks_pos c). - intros. - rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr. - - rewrite Ptrofs.unsigned_repr; eauto. - omega. - - rewrite Ptrofs.unsigned_repr; omega. -Qed. - -(** Predictor for return addresses in generated Asm code. - - The [return_address_offset] predicate defined here is used in the - semantics for Mach to determine the return addresses that are - stored in activation records. *) - -(** Consider a Mach function [f] and a sequence [c] of Mach instructions - representing the Mach code that remains to be executed after a - function call returns. The predicate [return_address_offset f c ofs] - holds if [ofs] is the integer offset of the PPC instruction - following the call in the Asm code obtained by translating the - code of [f]. Graphically: -<< - Mach function f |--------- Mcall ---------| - Mach code c | |--------| - | \ \ - | \ \ - | \ \ - Asm code | |--------| - Asm function |------------- Pcall ---------| - - <-------- ofs -------> ->> -*) - -Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : Prop := - forall tf tc, - transf_function f = OK tf -> - transl_blocks f c false = OK tc -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc. - -Lemma transl_blocks_tail: - forall f c1 c2, is_tail c1 c2 -> - forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 -> - exists tc1, exists ep1, transl_blocks f c1 ep1 = OK tc1 /\ is_tail tc1 tc2. -Proof. - induction 1; simpl; intros. - exists tc2; exists ep2; split; auto with coqlib. - monadInv H0. exploit IHis_tail; eauto. intros (tc1 & ep1 & A & B). - exists tc1; exists ep1; split. auto. - eapply is_tail_trans with x0; eauto with coqlib. -Qed. - -Lemma is_tail_code_tail: - forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1. -Proof. - induction 1; eauto. - destruct IHis_tail; eauto. -Qed. - -Section RETADDR_EXISTS. - -Hypothesis transf_function_inv: - forall f tf, transf_function f = OK tf -> - exists tc ep, transl_blocks f (Machblock.fn_code f) ep = OK tc /\ is_tail tc (fn_blocks tf). - -Hypothesis transf_function_len: - forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned. - - -Lemma return_address_exists: - forall b f c, is_tail (b :: c) f.(MB.fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. destruct (transf_function f) as [tf|] eqn:TF. - + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1). - exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2). - monadInv TR2. - assert (TL3: is_tail x0 (fn_blocks tf)). - { apply is_tail_trans with tc1; auto. - apply is_tail_trans with (x++x0); auto. eapply is_tail_app. - } - exploit is_tail_code_tail. eexact TL3. intros [ofs CT]. - exists (Ptrofs.repr ofs). red; intros. - rewrite Ptrofs.unsigned_repr. congruence. - exploit code_tail_bounds; eauto. - intros; apply transf_function_len in TF. omega. - + exists Ptrofs.zero; red; intros. congruence. -Qed. - -End RETADDR_EXISTS. - -(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points - within the Asmblock code generated by translating Machblock function [f], - and [tc] is the tail of the generated code at the position corresponding - to the code pointer [pc]. *) - -Inductive transl_code_at_pc (ge: MB.genv): - val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop := - transl_code_at_pc_intro: - forall b ofs f c ep tf tc, - Genv.find_funct_ptr ge b = Some(Internal f) -> - transf_function f = Errors.OK tf -> - transl_blocks f c ep = OK tc -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc -> - transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. - -Remark code_tail_no_bigger: - forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. -Proof. - induction 1; simpl; omega. -Qed. - -Remark code_tail_unique: - forall fn c pos pos', - code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. -Proof. - induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - f_equal. eauto. -Qed. - -Lemma return_address_offset_correct: - forall ge b ofs fb f c tf tc ofs', - transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc -> - return_address_offset f c ofs' -> - ofs' = ofs. -Proof. - intros. inv H. red in H0. - exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. - rewrite <- (Ptrofs.repr_unsigned ofs). - rewrite <- (Ptrofs.repr_unsigned ofs'). - congruence. -Qed. - -(** The [find_label] function returns the code tail starting at the - given label. A connection with [code_tail] is then established. *) - -Fixpoint find_label (lbl: label) (c: bblocks) {struct c} : option bblocks := - match c with - | nil => None - | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl - end. - -Lemma label_pos_code_tail: - forall lbl c pos c', - find_label lbl c = Some c' -> - exists pos', - label_pos lbl pos c = Some pos' - /\ code_tail (pos' - pos) c c' - /\ pos <= pos' <= pos + size_blocks c. -Proof. - induction c. - simpl; intros. discriminate. - simpl; intros until c'. - case (is_label lbl a). - - intros. inv H. exists pos. split; auto. split. - replace (pos - pos) with 0 by omega. constructor. constructor; try omega. - generalize (size_blocks_pos c). generalize (size_positive a). omega. - - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]]. - exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega. - constructor. auto. generalize (size_positive a). omega. -Qed. - -(** Helper lemmas to reason about -- the "code is tail of" property -- correct translation of labels. *) - -Definition tail_nolabel (k c: bblocks) : Prop := - is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. - -Lemma tail_nolabel_refl: - forall c, tail_nolabel c c. -Proof. - intros; split. apply is_tail_refl. auto. -Qed. - -Lemma tail_nolabel_trans: - forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3. -Proof. - intros. destruct H; destruct H0; split. - eapply is_tail_trans; eauto. - intros. rewrite H1; auto. -Qed. - -Definition nolabel (b: bblock) := - match (header b) with nil => True | _ => False end. - -Hint Extern 1 (nolabel _) => exact I : labels. - -Lemma tail_nolabel_cons: - forall b c k, - nolabel b -> tail_nolabel k c -> tail_nolabel k (b :: c). -Proof. - intros. destruct H0. split. - constructor; auto. - intros. simpl. rewrite <- H1. destruct b as [hd bdy ex]; simpl in *. - destruct hd as [|l hd]; simpl in *. - - assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false). - { apply is_label_correct_false. simpl header. apply in_nil. } - rewrite H2. auto. - - contradiction. -Qed. - -Hint Resolve tail_nolabel_refl: labels. - -Ltac TailNoLabel := - eauto with labels; - match goal with - | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: assertion_failed = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel - | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel - | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel - | _ => idtac - end. - -Remark tail_nolabel_find_label: - forall lbl k c, tail_nolabel k c -> find_label lbl c = find_label lbl k. -Proof. - intros. destruct H. auto. -Qed. - -Remark tail_nolabel_is_tail: - forall k c, tail_nolabel k c -> is_tail k c. -Proof. - intros. destruct H. auto. -Qed. - -Lemma exec_body_pc: - forall ge l rs1 m1 rs2 m2, - exec_body ge l rs1 m1 = Next rs2 m2 -> - rs2 PC = rs1 PC. -Proof. - induction l. - - intros. inv H. auto. - - intros until m2. intro EXEB. - inv EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate. - eapply IHl in H0. rewrite H0. - erewrite exec_basic_instr_pc; eauto. -Qed. - -Section STRAIGHTLINE. - -Variable ge: genv. -Variable fn: function. - -(** Straight-line code is composed of processor instructions that execute - in sequence (no branches, no function calls and returns). - The following inductive predicate relates the machine states - before and after executing a straight-line sequence of instructions. - Instructions are taken from the first list instead of being fetched - from memory. *) - -Inductive exec_straight: list instruction -> regset -> mem -> - list instruction -> regset -> mem -> Prop := - | exec_straight_one: - forall i1 c rs1 m1 rs2 m2, - exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_straight ((PBasic i1) ::g c) rs1 m1 c rs2 m2 - | exec_straight_step: - forall i c rs1 m1 rs2 m2 c' rs3 m3, - exec_basic_instr ge i rs1 m1 = Next rs2 m2 -> - exec_straight c rs2 m2 c' rs3 m3 -> - exec_straight ((PBasic i) :: c) rs1 m1 c' rs3 m3. - -Inductive exec_control_rel: option control -> bblock -> regset -> mem -> - regset -> mem -> Prop := - | exec_control_rel_intro: - forall rs1 m1 b rs1' ctl rs2 m2, - rs1' = nextblock b rs1 -> - exec_control ge fn ctl rs1' m1 = Next rs2 m2 -> - exec_control_rel ctl b rs1 m1 rs2 m2. - -Inductive exec_bblock_rel: bblock -> regset -> mem -> regset -> mem -> Prop := - | exec_bblock_rel_intro: - forall rs1 m1 b rs2 m2, - exec_bblock ge fn b rs1 m1 = Next rs2 m2 -> - exec_bblock_rel b rs1 m1 rs2 m2. - -Lemma exec_straight_body: - forall c l rs1 m1 rs2 m2, - exec_straight c rs1 m1 nil rs2 m2 -> - code_to_basics c = Some l -> - exec_body ge l rs1 m1 = Next rs2 m2. -Proof. - induction c as [|i c]. - - intros until m2. intros EXES CTB. inv EXES. - - intros until m2. intros EXES CTB. inv EXES. - + inv CTB. simpl. rewrite H6. auto. - + inv CTB. destruct (code_to_basics c); try discriminate. inv H0. eapply IHc in H7; eauto. - rewrite <- H7. simpl. rewrite H1. auto. -Qed. - -Lemma exec_straight_body2: - forall c rs1 m1 c' rs2 m2, - exec_straight c rs1 m1 c' rs2 m2 -> - exists body, - exec_body ge body rs1 m1 = Next rs2 m2 - /\ (basics_to_code body) ++g c' = c. -Proof. - intros until m2. induction 1. - - exists (i1::nil). split; auto. simpl. rewrite H. auto. - - destruct IHexec_straight as (bdy & EXEB & BTC). - exists (i:: bdy). split; simpl. - + rewrite H. auto. - + congruence. -Qed. - -Lemma exec_straight_trans: - forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, - exec_straight c1 rs1 m1 c2 rs2 m2 -> - exec_straight c2 rs2 m2 c3 rs3 m3 -> - exec_straight c1 rs1 m1 c3 rs3 m3. -Proof. - induction 1; intros. - apply exec_straight_step with rs2 m2; auto. - apply exec_straight_step with rs2 m2; auto. -Qed. - -Lemma exec_straight_two: - forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, - exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> - exec_straight (i1 ::g i2 ::g c) rs1 m1 c rs3 m3. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - apply exec_straight_one; auto. -Qed. - -Lemma exec_straight_three: - forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, - exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> - exec_basic_instr ge i3 rs3 m3 = Next rs4 m4 -> - exec_straight (i1 ::g i2 ::g i3 ::g c) rs1 m1 c rs4 m4. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - eapply exec_straight_two; eauto. -Qed. - -(** Like exec_straight predicate, but on blocks *) - -Inductive exec_straight_blocks: bblocks -> regset -> mem -> - bblocks -> regset -> mem -> Prop := - | exec_straight_blocks_one: - forall b1 c rs1 m1 rs2 m2, - exec_bblock ge fn b1 rs1 m1 = Next rs2 m2 -> - rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) -> - exec_straight_blocks (b1 :: c) rs1 m1 c rs2 m2 - | exec_straight_blocks_step: - forall b c rs1 m1 rs2 m2 c' rs3 m3, - exec_bblock ge fn b rs1 m1 = Next rs2 m2 -> - rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b)) -> - exec_straight_blocks c rs2 m2 c' rs3 m3 -> - exec_straight_blocks (b :: c) rs1 m1 c' rs3 m3. - -Lemma exec_straight_blocks_trans: - forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, - exec_straight_blocks c1 rs1 m1 c2 rs2 m2 -> - exec_straight_blocks c2 rs2 m2 c3 rs3 m3 -> - exec_straight_blocks c1 rs1 m1 c3 rs3 m3. -Proof. - induction 1; intros. - apply exec_straight_blocks_step with rs2 m2; auto. - apply exec_straight_blocks_step with rs2 m2; auto. -Qed. - -(** Linking exec_straight with exec_straight_blocks *) - -Lemma exec_straight_pc: - forall c c' rs1 m1 rs2 m2, - exec_straight c rs1 m1 c' rs2 m2 -> - rs2 PC = rs1 PC. -Proof. - induction c; intros; try (inv H; fail). - inv H. - - eapply exec_basic_instr_pc; eauto. - - rewrite (IHc c' rs3 m3 rs2 m2); auto. - erewrite exec_basic_instr_pc; eauto. -Qed. - -Lemma regset_same_assign (rs: regset) r: - rs # r <- (rs r) = rs. -Proof. - apply functional_extensionality. intros x. destruct (preg_eq x r); subst; Simpl. -Qed. - -Lemma exec_straight_through_singleinst: - forall a b rs1 m1 rs2 m2 rs2' m2' lb, - bblock_single_inst (PBasic a) = b -> - exec_straight (a ::g nil) rs1 m1 nil rs2 m2 -> - nextblock b rs2 = rs2' -> m2 = m2' -> - exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'. -Proof. - intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - simpl. rewrite regset_same_assign. auto. - simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto. -Qed. - -(** The following lemmas show that straight-line executions - (predicate [exec_straight_blocks]) correspond to correct Asm executions. *) - -Lemma exec_straight_steps_1: - forall c rs m c' rs' m', - exec_straight_blocks c rs m c' rs' m' -> - size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal fn) -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c -> - plus step ge (State rs m) E0 (State rs' m'). -Proof. - induction 1; intros. - apply plus_one. - econstructor; eauto. - eapply find_bblock_tail. eauto. - eapply plus_left'. - econstructor; eauto. - eapply find_bblock_tail. eauto. - apply IHexec_straight_blocks with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))). - auto. rewrite H0. rewrite H3. reflexivity. - auto. - apply code_tail_next_int; auto. - traceEq. -Qed. - -Lemma exec_straight_steps_2: - forall c rs m c' rs' m', - exec_straight_blocks c rs m c' rs' m' -> - size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal fn) -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c -> - exists ofs', - rs'#PC = Vptr b ofs' - /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'. -Proof. - induction 1; intros. - exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split. - rewrite H0. rewrite H2. auto. - apply code_tail_next_int; auto. - apply IHexec_straight_blocks with (Ptrofs.add ofs (Ptrofs.repr (size b))). - auto. rewrite H0. rewrite H3. reflexivity. auto. - apply code_tail_next_int; auto. -Qed. - -End STRAIGHTLINE. - -(** * Properties of the Machblock call stack *) - -Section MATCH_STACK. - -Variable ge: MB.genv. - -Inductive match_stack: list MB.stackframe -> Prop := - | match_stack_nil: - match_stack nil - | match_stack_cons: forall fb sp ra c s f tf tc, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc ge ra fb f c false tf tc -> - sp <> Vundef -> - match_stack s -> - match_stack (Stackframe fb sp ra c :: s). - -Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. -Proof. - induction 1; simpl. - unfold Vnullptr; destruct Archi.ptr64; congruence. - auto. -Qed. - -Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. -Proof. - induction 1; simpl. - unfold Vnullptr; destruct Archi.ptr64; congruence. - inv H0. congruence. -Qed. - -Lemma lessdef_parent_sp: - forall s v, - match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. -Proof. - intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. -Qed. - -Lemma lessdef_parent_ra: - forall s v, - match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. -Proof. - intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. -Qed. - -End MATCH_STACK. diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v deleted file mode 100644 index f79814f2..00000000 --- a/mppa_k1c/lib/ForwardSimulationBlock.v +++ /dev/null @@ -1,387 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -(*** - -Auxiliary lemmas on starN and forward_simulation -in order to prove the forward simulation of Mach -> Machblock. - -***) - -Require Import Relations. -Require Import Wellfounded. -Require Import Coqlib. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. - - -Local Open Scope nat_scope. - - -(** Auxiliary lemma on starN *) -Section starN_lemma. - -Variable L: semantics. - -Local Hint Resolve starN_refl starN_step Eapp_assoc: core. - -Lemma starN_split n s t s': - starN (step L) (globalenv L) n s t s' -> - forall m k, n=m+k -> - exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. -Proof. - induction 1; simpl. - + intros m k H; assert (X: m=0); try omega. - assert (X0: k=0); try omega. - subst; repeat (eapply ex_intro); intuition eauto. - + intros m; destruct m as [| m']; simpl. - - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. - - intros k H2. inversion H2. - exploit (IHstarN m' k); eauto. intro. - destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). - repeat (eapply ex_intro). - instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). - intuition eauto. subst. auto. -Qed. - -Lemma starN_tailstep n s t1 s': - starN (step L) (globalenv L) n s t1 s' -> - forall (t t2:trace) s'', - Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. -Proof. - induction 1; simpl. - + intros t t1 s0; autorewrite with trace_rewrite. - intros; subst; eapply starN_step; eauto. - autorewrite with trace_rewrite; auto. - + intros. eapply starN_step; eauto. - intros; subst; autorewrite with trace_rewrite; auto. -Qed. - -End starN_lemma. - - - -(** General scheme from a "match_states" relation *) - -Section ForwardSimuBlock_REL. - -Variable L1 L2: semantics. - - -(** Hypothèses de la preuve *) - -Variable dist_end_block: state L1 -> nat. - -Hypothesis simu_mid_block: - forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). - -Hypothesis public_preserved: - forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. - -Variable match_states: state L1 -> state L2 -> Prop. - -Hypothesis match_initial_states: - forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. - -Hypothesis match_final_states: - forall s1 s2 r, final_state L1 s1 r -> match_states s1 s2 -> final_state L2 s2 r. - -Hypothesis final_states_end_block: - forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. - -Hypothesis simu_end_block: - forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> match_states s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states s1' s2'. - - -(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) - -Local Hint Resolve starN_refl starN_step: core. - -Definition follows_in_block (head current: state L1): Prop := - dist_end_block head >= dist_end_block current - /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. - -Lemma follows_in_block_step (head previous next: state L1): - forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next. -Proof. - intros t [H1 H2] H3 H4. - destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. - constructor 1. - + omega. - + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). - - eapply starN_tailstep; eauto. - - omega. -Qed. - -Lemma follows_in_block_init (head current: state L1): - forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current. -Proof. - intros t H3 H4. - destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. - constructor 1. - + omega. - + cutrewrite (dist_end_block head - dist_end_block current = 1). - - eapply starN_tailstep; eauto. - - omega. -Qed. - - -Record memostate := { - real: state L1; - memorized: option (state L1); - memo_star: forall head, memorized = Some head -> follows_in_block head real; - memo_final: forall r, final_state L1 real r -> memorized = None -}. - -Definition head (s: memostate): state L1 := - match memorized s with - | None => real s - | Some s' => s' - end. - -Lemma head_followed (s: memostate): follows_in_block (head s) (real s). -Proof. - destruct s as [rs ms Hs]. simpl. - destruct ms as [ms|]; unfold head; simpl; auto. - constructor 1. - omega. - cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). - + apply starN_refl; auto. - + omega. -Qed. - -Inductive is_well_memorized (s s': memostate): Prop := - | StartBloc: - dist_end_block (real s) <> O -> - memorized s = None -> - memorized s' = Some (real s) -> - is_well_memorized s s' - | MidBloc: - dist_end_block (real s) <> O -> - memorized s <> None -> - memorized s' = memorized s -> - is_well_memorized s s' - | ExitBloc: - dist_end_block (real s) = O -> - memorized s' = None -> - is_well_memorized s s'. - -Local Hint Resolve StartBloc MidBloc ExitBloc: core. - -Definition memoL1 := {| - state := memostate; - genvtype := genvtype L1; - step := fun ge s t s' => - step L1 ge (real s) t (real s') - /\ is_well_memorized s s' ; - initial_state := fun s => initial_state L1 (real s) /\ memorized s = None; - final_state := fun s r => final_state L1 (real s) r; - globalenv:= globalenv L1; - symbolenv:= symbolenv L1 -|}. - - -(** Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2 *) - -Lemma discr_dist_end s: - {dist_end_block s = O} + {dist_end_block s <> O}. -Proof. - destruct (dist_end_block s); simpl; intuition. -Qed. - -Lemma memo_simulation_step: - forall s1 t s1', Step L1 s1 t s1' -> - forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). -Proof. - intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. - destruct (discr_dist_end rs2) as [H3 | H3]. - + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. - intuition. - + destruct ms2 as [s|]. - - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. - intuition. - - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. - intuition. - Unshelve. - * intros; discriminate. - * intros; auto. - * intros head X; injection X; clear X; intros; subst. - eapply follows_in_block_step; eauto. - * intros r X; erewrite final_states_end_block in H3; intuition eauto. - * intros head X; injection X; clear X; intros; subst. - eapply follows_in_block_init; eauto. - * intros r X; erewrite final_states_end_block in H3; intuition eauto. -Qed. - -Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. -Proof. - apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. - + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. - intuition. - + intros; subst; auto. - + intros; exploit memo_simulation_step; eauto. - Unshelve. - * intros; discriminate. - * auto. -Qed. - -Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. -Proof. - unfold memoL1; simpl. - apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; auto. - + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). - unfold head; rewrite H1. - intuition eauto. - + intros s1 s2 r X H0; unfold head in X. - erewrite memo_final in X; eauto. - + intros s1 t s1' [H1 H2] s2 H; subst. - destruct H2 as [ H0 H2 H3 | H0 H2 H3 | H0 H2]. - - (* StartBloc *) - constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. - unfold head in * |- *. rewrite H2 in H. rewrite H3. rewrite H4. intuition. - - (* MidBloc *) - constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. - unfold head in * |- *. rewrite H3. rewrite H4. intuition. - destruct (memorized s1); simpl; auto. tauto. - - (* EndBloc *) - constructor 1. - destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. - * destruct (head_followed s1) as [H4 H3]. - cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. - eapply starN_tailstep; eauto. - * unfold head; rewrite H2; simpl. intuition eauto. -Qed. - -Lemma forward_simulation_block_rel: forward_simulation L1 L2. -Proof. - eapply compose_forward_simulations. - eapply forward_memo_simulation_1. - apply forward_memo_simulation_2. -Qed. - - -End ForwardSimuBlock_REL. - - - -(* An instance of the previous scheme, when there is a translation from L1 states to L2 states - -Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state. -This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label). - -However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below... - -*) - - -Section ForwardSimuBlock_TRANS. - -Variable L1 L2: semantics. - -Variable trans_state: state L1 -> state L2. - -Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := - (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))). - -Definition match_states s1 s2: Prop := - equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1). - -Lemma match_states_trans_state s1: match_states s1 (trans_state s1). -Proof. - unfold match_states, equiv_on_next_step. intuition. -Qed. - -Variable dist_end_block: state L1 -> nat. - -Hypothesis simu_mid_block: - forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). - -Hypothesis public_preserved: - forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. - -Hypothesis match_initial_states: - forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. - -Hypothesis match_final_states: - forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) r. - -Hypothesis final_states_end_block: - forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. - -Hypothesis simu_end_block: - forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'. - -Lemma forward_simulation_block_trans: forward_simulation L1 L2. -Proof. - eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto. - + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto. - + (* simu_end_block *) - intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto. - intros (s2' & H3 & H4); econstructor 1; intuition eauto. - rewrite H2a; auto. - inversion_clear H1. eauto. -Qed. - -End ForwardSimuBlock_TRANS. - - -(* another version with a relation [trans_state_R] instead of a function [trans_state] *) -Section ForwardSimuBlock_TRANS_R. - -Variable L1 L2: semantics. - -Variable trans_state_R: state L1 -> state L2 -> Prop. - -Definition match_states_R s1 s2: Prop := - exists s2', trans_state_R s1 s2' /\ equiv_on_next_step _ (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 s2'. - -Lemma match_states_trans_state_R s1 s2: trans_state_R s1 s2 -> match_states_R s1 s2. -Proof. - unfold match_states, equiv_on_next_step. firstorder. -Qed. - -Variable dist_end_block: state L1 -> nat. - -Hypothesis simu_mid_block: - forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). - -Hypothesis public_preserved: - forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. - -Hypothesis match_initial_states: - forall s1, initial_state L1 s1 -> exists s2, match_states_R s1 s2 /\ initial_state L2 s2. - -Hypothesis match_final_states: - forall s1 s2 r, final_state L1 s1 r -> trans_state_R s1 s2 -> final_state L2 s2 r. - -Hypothesis final_states_end_block: - forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. - -Hypothesis simu_end_block: - forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> trans_state_R s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states_R s1' s2'. - -Lemma forward_simulation_block_trans_R: forward_simulation L1 L2. -Proof. - eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states_R); try tauto. - + (* final_states *) intros s1 s2 r H1 (s2' & H2 & H3 & H4). rewrite H4; eauto. - + (* simu_end_block *) - intros s1 t s1' s2 H1 (s2' & H2 & H2a & H2b). exploit simu_end_block; eauto. - intros (x & Hx & (y & H3 & H4 & H5)). repeat (econstructor; eauto). - rewrite H2a; eauto. - inversion_clear H1. eauto. -Qed. - -End ForwardSimuBlock_TRANS_R. - diff --git a/mppa_k1c/lib/Machblock.v b/mppa_k1c/lib/Machblock.v deleted file mode 100644 index 08e0eba2..00000000 --- a/mppa_k1c/lib/Machblock.v +++ /dev/null @@ -1,380 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import Conventions. -Require Stacklayout. -Require Import Mach. -Require Import Linking. - -(** basic instructions (ie no control-flow) *) -Inductive basic_inst: Type := - | MBgetstack: ptrofs -> typ -> mreg -> basic_inst - | MBsetstack: mreg -> ptrofs -> typ -> basic_inst - | MBgetparam: ptrofs -> typ -> mreg -> basic_inst - | MBop: operation -> list mreg -> mreg -> basic_inst - | MBload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> basic_inst - | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst - . - -Definition bblock_body := list basic_inst. - -(** control flow instructions *) -Inductive control_flow_inst: Type := - | MBcall: signature -> mreg + ident -> control_flow_inst - | MBtailcall: signature -> mreg + ident -> control_flow_inst - | MBbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> control_flow_inst - | MBgoto: label -> control_flow_inst - | MBcond: condition -> list mreg -> label -> control_flow_inst - | MBjumptable: mreg -> list label -> control_flow_inst - | MBreturn: control_flow_inst - . - -Record bblock := mk_bblock { - header: list label; - body: bblock_body; - exit: option control_flow_inst -}. - -Lemma bblock_eq: - forall b1 b2, - header b1 = header b2 -> - body b1 = body b2 -> - exit b1 = exit b2 -> - b1 = b2. -Proof. - intros. destruct b1. destruct b2. - simpl in *. subst. auto. -Qed. - -Definition length_opt {A} (o: option A) : nat := - match o with - | Some o => 1 - | None => 0 - end. - -Definition size (b:bblock): nat := (length (header b))+(length (body b))+(length_opt (exit b)). - -Lemma size_null b: - size b = 0%nat -> - header b = nil /\ body b = nil /\ exit b = None. -Proof. - destruct b as [h b e]. simpl. unfold size. simpl. - intros H. - assert (length h = 0%nat) as Hh; [ omega |]. - assert (length b = 0%nat) as Hb; [ omega |]. - assert (length_opt e = 0%nat) as He; [ omega|]. - repeat split. - destruct h; try (simpl in Hh; discriminate); auto. - destruct b; try (simpl in Hb; discriminate); auto. - destruct e; try (simpl in He; discriminate); auto. -Qed. - -Definition code := list bblock. - -Record function: Type := mkfunction - { fn_sig: signature; - fn_code: code; - fn_stacksize: Z; - fn_link_ofs: ptrofs; - fn_retaddr_ofs: ptrofs }. - -Definition fundef := AST.fundef function. - -Definition program := AST.program fundef unit. - -Definition genv := Genv.t fundef unit. - -(*** sémantique ***) - -Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. -Proof. - apply List.in_dec. - apply Pos.eq_dec. -Qed. - -Definition is_label (lbl: label) (bb: bblock) : bool := - if in_dec lbl (header bb) then true else false. - -Lemma is_label_correct_true lbl bb: - List.In lbl (header bb) <-> is_label lbl bb = true. -Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. -Qed. - -Lemma is_label_correct_false lbl bb: - ~(List.In lbl (header bb)) <-> is_label lbl bb = false. -Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. -Qed. - - -Local Open Scope nat_scope. - -Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := - match c with - | nil => None - | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl - end. - -Section RELSEM. - -Variable rao:function -> code -> ptrofs -> Prop. -Variable ge:genv. - -Definition find_function_ptr - (ge: genv) (ros: mreg + ident) (rs: regset) : option block := - match ros with - | inl r => - match rs r with - | Vptr b ofs => if Ptrofs.eq ofs Ptrofs.zero then Some b else None - | _ => None - end - | inr symb => - Genv.find_symbol ge symb - end. - -(** Machblock execution states. *) - -Inductive stackframe: Type := - | Stackframe: - forall (f: block) (**r pointer to calling function *) - (sp: val) (**r stack pointer in calling function *) - (retaddr: val) (**r Asm return address in calling function *) - (c: code), (**r program point in calling function *) - stackframe. - -Inductive state: Type := - | State: - forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to current function *) - (sp: val) (**r stack pointer *) - (c: code) (**r current program point *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state - | Callstate: - forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to function to call *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state - | Returnstate: - forall (stack: list stackframe) (**r call stack *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state. - -Definition parent_sp (s: list stackframe) : val := - match s with - | nil => Vnullptr - | Stackframe f sp ra c :: s' => sp - end. - -Definition parent_ra (s: list stackframe) : val := - match s with - | nil => Vnullptr - | Stackframe f sp ra c :: s' => ra - end. - -Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop := - | exec_MBgetstack: - forall ofs ty dst v, - load_stack m sp ty ofs = Some v -> - basic_step s fb sp rs m (MBgetstack ofs ty dst) (rs#dst <- v) m - | exec_MBsetstack: - forall src ofs ty m' rs', - store_stack m sp ty ofs (rs src) = Some m' -> - rs' = undef_regs (destroyed_by_setstack ty) rs -> - basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m' - | exec_MBgetparam: - forall ofs ty dst v rs' f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m sp Tptr f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (parent_sp s) ty ofs = Some v -> - rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) -> - basic_step s fb sp rs m (MBgetparam ofs ty dst) rs' m - | exec_MBop: - forall op args v rs' res, - eval_operation ge sp op rs##args m = Some v -> - rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) -> - basic_step s fb sp rs m (MBop op args res) rs' m - | exec_MBload: - forall addr args a v rs' trap chunk dst, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) -> - basic_step s fb sp rs m (MBload trap chunk addr args dst) rs' m - | exec_MBload_notrap1: - forall addr args rs' chunk dst, - eval_addressing ge sp addr rs##args = None -> - rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> - basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m - | exec_MBload_notrap2: - forall addr args a rs' chunk dst, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = None -> - rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> - basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m - | exec_MBstore: - forall chunk addr args src m' a rs', - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a (rs src) = Some m' -> - rs' = undef_regs (destroyed_by_store chunk addr) rs -> - basic_step s fb sp rs m (MBstore chunk addr args src) rs' m' - . - - -Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> regset -> mem -> regset -> mem -> Prop := - | exec_nil_body: - forall rs m, - body_step s f sp nil rs m rs m - | exec_cons_body: - forall rs m bi p rs' m' rs'' m'', - basic_step s f sp rs m bi rs' m' -> - body_step s f sp p rs' m' rs'' m'' -> - body_step s f sp (bi::p) rs m rs'' m'' - . - -Inductive cfi_step: control_flow_inst -> state -> trace -> state -> Prop := - | exec_MBcall: - forall s fb sp sig ros c b rs m f f' ra, - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - rao f c ra -> - cfi_step (MBcall sig ros) (State s fb sp (b::c) rs m) - E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) - f' rs m) - | exec_MBtailcall: - forall s fb stk soff sig ros c rs m f f' m', - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - cfi_step (MBtailcall sig ros) (State s fb (Vptr stk soff) c rs m) - E0 (Callstate s f' rs m') - | exec_MBbuiltin: - forall s f sp rs m ef args res b c vargs t vres rs' m', - eval_builtin_args ge rs sp m args vargs -> - external_call ef ge vargs m t vres m' -> - rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) -> - cfi_step (MBbuiltin ef args res) (State s f sp (b :: c) rs m) - t (State s f sp c rs' m') - | exec_MBgoto: - forall s fb f sp lbl c rs m c', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - cfi_step (MBgoto lbl) (State s fb sp c rs m) - E0 (State s fb sp c' rs m) - | exec_MBcond_true: - forall s fb f sp cond args lbl c rs m c' rs', - eval_condition cond rs##args m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - rs' = undef_regs (destroyed_by_cond cond) rs -> - cfi_step (MBcond cond args lbl) (State s fb sp c rs m) - E0 (State s fb sp c' rs' m) - | exec_MBcond_false: - forall s f sp cond args lbl b c rs m rs', - eval_condition cond rs##args m = Some false -> - rs' = undef_regs (destroyed_by_cond cond) rs -> - cfi_step (MBcond cond args lbl) (State s f sp (b :: c) rs m) - E0 (State s f sp c rs' m) - | exec_MBjumptable: - forall s fb f sp arg tbl c rs m n lbl c' rs', - rs arg = Vint n -> - list_nth_z tbl (Int.unsigned n) = Some lbl -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - rs' = undef_regs destroyed_by_jumptable rs -> - cfi_step (MBjumptable arg tbl) (State s fb sp c rs m) - E0 (State s fb sp c' rs' m) - | exec_MBreturn: - forall s fb stk soff c rs m f m', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - cfi_step MBreturn (State s fb (Vptr stk soff) c rs m) - E0 (Returnstate s rs m') - . - -Inductive exit_step: option control_flow_inst -> state -> trace -> state -> Prop := - | exec_Some_exit: - forall ctl s t s', - cfi_step ctl s t s' -> - exit_step (Some ctl) s t s' - | exec_None_exit: - forall stk f sp b lb rs m, - exit_step None (State stk f sp (b::lb) rs m) E0 (State stk f sp lb rs m) - . - -Inductive step: state -> trace -> state -> Prop := - | exec_bblock: - forall sf f sp bb c rs m rs' m' t s', - body_step sf f sp (body bb) rs m rs' m' -> - exit_step (exit bb) (State sf f sp (bb::c) rs' m') t s' -> - step (State sf f sp (bb::c) rs m) t s' - | exec_function_internal: - forall s fb rs m f m1 m2 m3 stk rs', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - let sp := Vptr stk Ptrofs.zero in - store_stack m1 sp Tptr f.(fn_link_ofs) (parent_sp s) = Some m2 -> - store_stack m2 sp Tptr f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> - rs' = undef_regs destroyed_at_function_entry rs -> - step (Callstate s fb rs m) - E0 (State s fb sp f.(fn_code) rs' m3) - | exec_function_external: - forall s fb rs m t rs' ef args res m', - Genv.find_funct_ptr ge fb = Some (External ef) -> - extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> - external_call ef ge args m t res m' -> - rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> - step (Callstate s fb rs m) - t (Returnstate s rs' m') - | exec_return: - forall s f sp ra c rs m, - step (Returnstate (Stackframe f sp ra c :: s) rs m) - E0 (State s f sp c rs m) - . - -End RELSEM. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall fb m0, - let ge := Genv.globalenv p in - Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some fb -> - initial_state p (Callstate nil fb (Regmap.init Vundef) m0). - -Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r retcode, - loc_result signature_main = One r -> - rs r = Vint retcode -> - final_state (Returnstate nil rs m) retcode. - -Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) := - Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v deleted file mode 100644 index 287e4f7b..00000000 --- a/mppa_k1c/lib/Machblockgen.v +++ /dev/null @@ -1,216 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import Conventions. -Require Stacklayout. -Require Import Mach. -Require Import Linking. -Require Import Machblock. - -Inductive Machblock_inst: Type := -| MB_label (lbl: label) -| MB_basic (bi: basic_inst) -| MB_cfi (cfi: control_flow_inst). - -Definition trans_inst (i:Mach.instruction) : Machblock_inst := - match i with - | Mcall sig ros => MB_cfi (MBcall sig ros) - | Mtailcall sig ros => MB_cfi (MBtailcall sig ros) - | Mbuiltin ef args res => MB_cfi (MBbuiltin ef args res) - | Mgoto lbl => MB_cfi (MBgoto lbl) - | Mcond cond args lbl => MB_cfi (MBcond cond args lbl) - | Mjumptable arg tbl => MB_cfi (MBjumptable arg tbl) - | Mreturn => MB_cfi (MBreturn) - | Mgetstack ofs ty dst => MB_basic (MBgetstack ofs ty dst) - | Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty) - | Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst) - | Mop op args res => MB_basic (MBop op args res) - | Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst) - | Mstore chunk addr args src => MB_basic (MBstore chunk addr args src) - | Mlabel l => MB_label l - end. - -Definition empty_bblock:={| header := nil; body := nil; exit := None |}. -Extraction Inline empty_bblock. - -Definition add_label l bb:={| header := l::(header bb); body := (body bb); exit := (exit bb) |}. -Extraction Inline add_label. - -Definition add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}. -Extraction Inline add_basic. - -Definition cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}. -Extraction Inline cfi_bblock. - -Definition add_to_new_bblock (i:Machblock_inst) : bblock := - match i with - | MB_label l => add_label l empty_bblock - | MB_basic i => add_basic i empty_bblock - | MB_cfi i => cfi_bblock i - end. - -(** Adding an instruction to the beginning of a bblock list - * Either adding the instruction to the head of the list, - * or create a new bblock with the instruction *) -Definition add_to_code (i:Machblock_inst) (bl:code) : code := - match bl with - | bh::bl0 => match i with - | MB_label l => add_label l bh::bl0 - | MB_cfi i0 => cfi_bblock i0::bl - | MB_basic i0 => match header bh with - |_::_ => add_basic i0 empty_bblock::bl - | nil => add_basic i0 bh::bl0 - end - end - | _ => add_to_new_bblock i::nil - end. - -Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := - match c with - | nil => bl - | i::c0 => - trans_code_rev c0 (add_to_code (trans_inst i) bl) - end. - -Function trans_code (c: Mach.code) : code := - trans_code_rev (List.rev_append c nil) nil. - -Definition transf_function (f: Mach.function) : function := - {| fn_sig:=Mach.fn_sig f; - fn_code:=trans_code (Mach.fn_code f); - fn_stacksize := Mach.fn_stacksize f; - fn_link_ofs := Mach.fn_link_ofs f; - fn_retaddr_ofs := Mach.fn_retaddr_ofs f - |}. - -Definition transf_fundef (f: Mach.fundef) : fundef := - transf_fundef transf_function f. - -Definition transf_program (src: Mach.program) : program := - transform_program transf_fundef src. - - -(** Abstracting trans_code *) - -Inductive is_end_block: Machblock_inst -> code -> Prop := - | End_empty mbi: is_end_block mbi nil - | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl) - | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. - -Local Hint Resolve End_empty End_basic End_cfi: core. - -Inductive is_trans_code: Mach.code -> code -> Prop := - | Tr_nil: is_trans_code nil nil - | Tr_end_block i c bl: - is_trans_code c bl -> - is_end_block (trans_inst i) bl -> - is_trans_code (i::c) (add_to_new_bblock (trans_inst i)::bl) - | Tr_add_label i l bh c bl: - is_trans_code c (bh::bl) -> - i = Mlabel l -> - is_trans_code (i::c) (add_label l bh::bl) - | Tr_add_basic i bi bh c bl: - is_trans_code c (bh::bl) -> - trans_inst i = MB_basic bi -> - header bh = nil -> - is_trans_code (i::c) (add_basic bi bh::bl). - -Local Hint Resolve Tr_nil Tr_end_block: core. - -Lemma add_to_code_is_trans_code i c bl: - is_trans_code c bl -> - is_trans_code (i::c) (add_to_code (trans_inst i) bl). -Proof. - destruct bl as [|bh0 bl]; simpl. - - intro H. inversion H. subst. eauto. - - remember (trans_inst i) as ti. - destruct ti as [l|bi|cfi]. - + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence. - + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. - * eapply Tr_add_basic; eauto. - * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. - rewrite Heqti; eapply Tr_end_block; eauto. - rewrite <- Heqti. eapply End_basic. congruence. - + intros. - cutrewrite (cfi_bblock cfi = add_to_new_bblock (MB_cfi cfi)); auto. - rewrite Heqti. eapply Tr_end_block; eauto. - rewrite <- Heqti. eapply End_cfi. congruence. -Qed. - -Local Hint Resolve add_to_code_is_trans_code: core. - -Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, - is_trans_code c2 mbi -> - is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi). -Proof. - induction c1 as [| i c1]; simpl; auto. -Qed. - -Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c). -Proof. - unfold trans_code. - rewrite <- rev_alt. - rewrite <- (rev_involutive c) at 1. - rewrite rev_alt at 1. - apply trans_code_is_trans_code_rev; auto. -Qed. - -Lemma add_to_code_is_trans_code_inv i c bl: - is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0. -Proof. - intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto. - + (* case Tr_end_block *) inversion H3; subst; simpl; auto. - * destruct (header bh); congruence. - * destruct bl0; simpl; congruence. - + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence. -Qed. - -Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, - is_trans_code (rev_append c1 c2) mbi -> - exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0. -Proof. - induction c1 as [| i c1]; simpl; eauto. - intros; exploit IHc1; eauto. - intros (mbi0 & H1 & H2); subst. - exploit add_to_code_is_trans_code_inv; eauto. - intros. destruct H0 as [mbi1 [H2 H3]]. - exists mbi1. split; congruence. -Qed. - -Local Hint Resolve trans_code_is_trans_code: core. - -Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c). -Proof. - constructor; intros; subst; auto. - unfold trans_code. - exploit (trans_code_is_trans_code_rev_inv (rev_append c nil) nil bl); eauto. - * rewrite <- rev_alt. - rewrite <- rev_alt. - rewrite (rev_involutive c). - apply H. - * intros. - destruct H0 as [mbi [H0 H1]]. - inversion H0. subst. reflexivity. -Qed. diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v deleted file mode 100644 index dfb97bfe..00000000 --- a/mppa_k1c/lib/Machblockgenproof.v +++ /dev/null @@ -1,824 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import Conventions. -Require Stacklayout. -Require Import Mach. -Require Import Linking. -Require Import Machblock. -Require Import Machblockgen. -Require Import ForwardSimulationBlock. - -Ltac subst_is_trans_code H := - rewrite is_trans_code_inv in H; - rewrite <- H in * |- *; - rewrite <- is_trans_code_inv in H. - -Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) := - rao (transf_function f) (trans_code c). - -Definition match_prog (p: Mach.program) (tp: Machblock.program) := - match_program (fun _ f tf => tf = transf_fundef f) eq p tp. - -Lemma transf_program_match: forall p tp, transf_program p = tp -> match_prog p tp. -Proof. - intros. rewrite <- H. eapply match_transform_program; eauto. -Qed. - -Definition trans_stackframe (msf: Mach.stackframe) : stackframe := - match msf with - | Mach.Stackframe f sp retaddr c => Stackframe f sp retaddr (trans_code c) - end. - -Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe := - match mst with - | nil => nil - | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0) - end. - -Definition trans_state (ms: Mach.state): state := - match ms with - | Mach.State s f sp c rs m => State (trans_stack s) f sp (trans_code c) rs m - | Mach.Callstate s f rs m => Callstate (trans_stack s) f rs m - | Mach.Returnstate s rs m => Returnstate (trans_stack s) rs m - end. - -Section PRESERVATION. - -Local Open Scope nat_scope. - -Variable prog: Mach.program. -Variable tprog: Machblock.program. -Hypothesis TRANSF: match_prog prog tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - - -Variable rao: function -> code -> ptrofs -> Prop. - -Definition match_states: Mach.state -> state -> Prop - := ForwardSimulationBlock.match_states (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog) trans_state. - -Lemma match_states_trans_state s1: match_states s1 (trans_state s1). -Proof. - apply match_states_trans_state. -Qed. - -Local Hint Resolve match_states_trans_state: core. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_match TRANSF). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_match TRANSF). - -Lemma init_mem_preserved: - forall m, - Genv.init_mem prog = Some m -> - Genv.init_mem tprog = Some m. -Proof (Genv.init_mem_transf TRANSF). - -Lemma prog_main_preserved: - prog_main tprog = prog_main prog. -Proof (match_program_main TRANSF). - -Lemma functions_translated: - forall b f, - Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = tf. -Proof. - intros. - exploit (Genv.find_funct_ptr_match TRANSF); eauto. intro. - destruct H0 as (cunit & tf & A & B & C). - eapply ex_intro. intuition; eauto. subst. eapply A. -Qed. - -Lemma find_function_ptr_same: - forall s rs, - Mach.find_function_ptr ge s rs = find_function_ptr tge s rs. -Proof. - intros. unfold Mach.find_function_ptr. unfold find_function_ptr. - destruct s; auto. - rewrite symbols_preserved; auto. -Qed. - -Lemma find_funct_ptr_same: - forall f f0, - Genv.find_funct_ptr ge f = Some (Internal f0) -> - Genv.find_funct_ptr tge f = Some (Internal (transf_function f0)). -Proof. - intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. -Qed. - -Lemma find_funct_ptr_same_external: - forall f f0, - Genv.find_funct_ptr ge f = Some (External f0) -> - Genv.find_funct_ptr tge f = Some (External f0). -Proof. - intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. -Qed. - -Lemma parent_sp_preserved: - forall s, - Mach.parent_sp s = parent_sp (trans_stack s). -Proof. - unfold parent_sp. unfold Mach.parent_sp. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. -Qed. - -Lemma parent_ra_preserved: - forall s, - Mach.parent_ra s = parent_ra (trans_stack s). -Proof. - unfold parent_ra. unfold Mach.parent_ra. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. -Qed. - -Lemma external_call_preserved: - forall ef args m t res m', - external_call ef ge args m t res m' -> - external_call ef tge args m t res m'. -Proof. - intros. eapply external_call_symbols_preserved; eauto. - apply senv_preserved. -Qed. - -Lemma Mach_find_label_split l i c c': - Mach.find_label l (i :: c) = Some c' -> - (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c'). -Proof. - intros H. - destruct i; try (constructor 2; split; auto; discriminate ). - destruct (peq l0 l) as [P|P]. - - constructor. subst l0; split; auto. - revert H. unfold Mach.find_label. simpl. rewrite peq_true. - intros H; injection H; auto. - - constructor 2. split. - + intro F. injection F. intros. contradict P; auto. - + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto. -Qed. - -Lemma find_label_is_end_block_not_label i l c bl: - is_end_block (trans_inst i) bl -> - is_trans_code c bl -> - i <> Mlabel l -> find_label l (add_to_new_bblock (trans_inst i) :: bl) = find_label l bl. -Proof. - intros H H0 H1. - unfold find_label. - remember (is_label l _) as b. - cutrewrite (b = false); auto. - subst; unfold is_label. - destruct i; simpl in * |- *; try (destruct (in_dec l nil); intuition). - inversion H. - destruct (in_dec l (l0::nil)) as [H6|H6]; auto. - simpl in H6; intuition try congruence. -Qed. - -Lemma find_label_at_begin l bh bl: - In l (header bh) - -> find_label l (bh :: bl) = Some (bh::bl). -Proof. - unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; simpl; auto. -Qed. - -Lemma find_label_add_label_diff l bh bl: - ~(In l (header bh)) -> - find_label l (bh::bl) = find_label l bl. -Proof. - unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; simpl; auto. -Qed. - -Definition concat (h: list label) (c: code): code := - match c with - | nil => {| header := h; body := nil; exit := None |}::nil - | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c' - end. - -Lemma find_label_transcode_preserved: - forall l c c', - Mach.find_label l c = Some c' -> - exists h, In l h /\ find_label l (trans_code c) = Some (concat h (trans_code c')). -Proof. - intros l c. remember (trans_code _) as bl. - rewrite <- is_trans_code_inv in * |-. - induction Heqbl. - + (* Tr_nil *) - intros; exists (l::nil); simpl in * |- *; intuition. - discriminate. - + (* Tr_end_block *) - intros. - exploit Mach_find_label_split; eauto. - clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. - - subst. rewrite find_label_at_begin; simpl; auto. - inversion H as [mbi H1 H2| | ]. - subst. - inversion Heqbl. - subst. - exists (l :: nil); simpl; eauto. - - exploit IHHeqbl; eauto. - destruct 1 as (h & H3 & H4). - exists h. - split; auto. - erewrite find_label_is_end_block_not_label;eauto. - + (* Tr_add_label *) - intros. - exploit Mach_find_label_split; eauto. - clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. - - subst. - inversion H0 as [H1]. - clear H0. - erewrite find_label_at_begin; simpl; eauto. - subst_is_trans_code Heqbl. - exists (l :: nil); simpl; eauto. - - subst; assert (H: l0 <> l); try congruence; clear H0. - exploit IHHeqbl; eauto. - clear IHHeqbl Heqbl. - intros (h & H3 & H4). - simpl; unfold is_label, add_label; simpl. - destruct (in_dec l (l0::header bh)) as [H5|H5]; simpl in H5. - * destruct H5; try congruence. - exists (l0::h); simpl; intuition. - rewrite find_label_at_begin in H4; auto. - apply f_equal. inversion H4 as [H5]. clear H4. - destruct (trans_code c'); simpl in * |- *; - inversion H5; subst; simpl; auto. - * exists h. intuition. - erewrite <- find_label_add_label_diff; eauto. - + (* Tr_add_basic *) - intros. - exploit Mach_find_label_split; eauto. - destruct 1 as [(H2&H3)|(H2&H3)]. - rewrite H2 in H. unfold trans_inst in H. congruence. - exploit IHHeqbl; eauto. - clear IHHeqbl Heqbl. - intros (h & H4 & H5). - rewrite find_label_add_label_diff; auto. - rewrite find_label_add_label_diff in H5; eauto. - rewrite H0; auto. -Qed. - -Lemma find_label_preserved: - forall l f c, - Mach.find_label l (Mach.fn_code f) = Some c -> - exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)). -Proof. - intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto. - apply find_label_transcode_preserved; auto. -Qed. - -Lemma mem_free_preserved: - forall m stk f, - Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (transf_function f)). -Proof. - intros. auto. -Qed. - -Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated - parent_sp_preserved: core. - - -Definition dist_end_block_code (c: Mach.code) := - match trans_code c with - | nil => 0 - | bh::_ => (size bh-1)%nat - end. - -Definition dist_end_block (s: Mach.state): nat := - match s with - | Mach.State _ _ _ c _ _ => dist_end_block_code c - | _ => 0 - end. - -Local Hint Resolve exec_nil_body exec_cons_body: core. -Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore: core. - -Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. -Proof. - unfold add_label, size; simpl; omega. -Qed. - -Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. -Proof. - intro H. unfold add_basic, size; rewrite H; simpl. omega. -Qed. - - -Lemma size_add_to_newblock i: size (add_to_new_bblock i) = 1. -Proof. - destruct i; auto. -Qed. - - -Lemma dist_end_block_code_simu_mid_block i c: - dist_end_block_code (i::c) <> 0 -> - (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)). -Proof. - unfold dist_end_block_code. - remember (trans_code (i::c)) as bl. - rewrite <- is_trans_code_inv in Heqbl. - inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl. - - rewrite size_add_to_newblock; omega. - - rewrite size_add_label; - subst_is_trans_code H. - omega. - - rewrite size_add_basic; auto. - subst_is_trans_code H. - omega. -Qed. - -Local Hint Resolve dist_end_block_code_simu_mid_block: core. - - -Lemma size_nonzero c b bl: - is_trans_code c (b :: bl) -> size b <> 0. -Proof. - intros H; inversion H; subst. - - rewrite size_add_to_newblock; omega. - - rewrite size_add_label; omega. - - rewrite size_add_basic; auto; omega. -Qed. - -Inductive is_header: list label -> Mach.code -> Mach.code -> Prop := - | header_empty : is_header nil nil nil - | header_not_label i c: (forall l, i <> Mlabel l) -> is_header nil (i::c) (i::c) - | header_is_label l h c c0: is_header h c c0 -> is_header (l::h) ((Mlabel l)::c) c0 - . - -Inductive is_body: list basic_inst -> Mach.code -> Mach.code -> Prop := - | body_empty : is_body nil nil nil - | body_not_bi i c: (forall bi, (trans_inst i) <> (MB_basic bi)) -> is_body nil (i::c) (i::c) - | body_is_bi i lbi c0 c1 bi: (trans_inst i) = MB_basic bi -> is_body lbi c0 c1 -> is_body (bi::lbi) (i::c0) c1 - . - -Inductive is_exit: option control_flow_inst -> Mach.code -> Mach.code -> Prop := - | exit_empty: is_exit None nil nil - | exit_not_cfi i c: (forall cfi, (trans_inst i) <> MB_cfi cfi) -> is_exit None (i::c) (i::c) - | exit_is_cfi i c cfi: (trans_inst i) = MB_cfi cfi -> is_exit (Some cfi) (i::c) c - . - -Lemma Mlabel_is_not_basic i: - forall bi, trans_inst i = MB_basic bi -> forall l, i <> Mlabel l. -Proof. -intros. -unfold trans_inst in H. -destruct i; congruence. -Qed. - -Lemma Mlabel_is_not_cfi i: - forall cfi, trans_inst i = MB_cfi cfi -> forall l, i <> Mlabel l. -Proof. -intros. -unfold trans_inst in H. -destruct i; congruence. -Qed. - -Lemma MBbasic_is_not_cfi i: - forall cfi, trans_inst i = MB_cfi cfi -> forall bi, trans_inst i <> MB_basic bi. -Proof. -intros. -unfold trans_inst in H. -unfold trans_inst. -destruct i; congruence. -Qed. - - -Local Hint Resolve Mlabel_is_not_cfi: core. -Local Hint Resolve MBbasic_is_not_cfi: core. - -Lemma add_to_new_block_is_label i: - header (add_to_new_bblock (trans_inst i)) <> nil -> exists l, i = Mlabel l. -Proof. - intros. - unfold add_to_new_bblock in H. - destruct (trans_inst i) eqn : H1. - + exists lbl. - unfold trans_inst in H1. - destruct i; congruence. - + unfold add_basic in H; simpl in H; congruence. - + unfold cfi_bblock in H; simpl in H; congruence. -Qed. - -Local Hint Resolve Mlabel_is_not_basic: core. - -Lemma trans_code_decompose c: forall b bl, - is_trans_code c (b::bl) -> - exists c0 c1 c2, is_header (header b) c c0 /\ is_body (body b) c0 c1 /\ is_exit (exit b) c1 c2 /\ is_trans_code c2 bl. -Proof. - induction c as [|i c]. - { (* nil => absurd *) intros b bl H; inversion H. } - intros b bl H; remember (trans_inst i) as ti. - destruct ti as [lbl|bi|cfi]; - inversion H as [|d0 d1 d2 H0 H1| |]; subst; - try (rewrite <- Heqti in * |- *); simpl in * |- *; - try congruence. - + (* label at end block *) - inversion H1; subst. inversion H0; subst. - assert (X:i=Mlabel lbl). { destruct i; simpl in Heqti; congruence. } - subst. repeat econstructor; eauto. - + (* label at mid block *) - exploit IHc; eauto. - intros (c0 & c1 & c2 & H1 & H2 & H3 & H4). - repeat econstructor; eauto. - + (* basic at end block *) - inversion H1; subst. - lapply (Mlabel_is_not_basic i bi); auto. - intro H2. - - inversion H0; subst. - assert (X:(trans_inst i) = MB_basic bi ). { repeat econstructor; congruence. } - repeat econstructor; congruence. - - exists (i::c), c, c. - repeat econstructor; eauto; inversion H0; subst; repeat econstructor; simpl; try congruence. - * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. - * exploit H3; eauto. - * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. - + (* basic at mid block *) - inversion H1; subst. - exploit IHc; eauto. - intros (c0 & c1 & c2 & H3 & H4 & H5 & H6). - exists (i::c0), c1, c2. - repeat econstructor; eauto. - rewrite H2 in H3. - inversion H3; econstructor; eauto. - + (* cfi at end block *) - inversion H1; subst; - repeat econstructor; eauto. -Qed. - - -Lemma step_simu_header st f sp rs m s c h c' t: - is_header h c c' -> - starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> - s = Mach.State st f sp c' rs m /\ t = E0. -Proof. - induction 1; simpl; intros hs; try (inversion hs; tauto). - inversion hs as [|n1 s1 t1 t2 s2 t3 s3 H1]. inversion H1. subst. auto. -Qed. - - - -Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state): - trans_inst i = MB_basic bi -> - Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> - exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. -Proof. - destruct i; simpl in * |-; - (discriminate - || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). - - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. - destruct H3 as (tf & A & B). subst. eapply A. - all: simpl; rewrite <- parent_sp_preserved; auto. - - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto. - unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; - unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; - unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; - unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; - unfold Genv.symbol_address; rewrite symbols_preserved; auto. -Qed. - - -Lemma star_step_simu_body_step s f sp c bdy c': - is_body bdy c c' -> forall rs m t s', - starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' -> - exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'. -Proof. - induction 1; simpl. - + intros. inversion H. exists rs. exists m. auto. - + intros. inversion H0. exists rs. exists m. auto. - + intros. inversion H1; subst. - exploit (step_simu_basic_step ); eauto. - destruct 1 as [ rs1 [ m1 Hs]]. - destruct Hs as [Hs1 [Hs2 Hs3]]. - destruct (IHis_body rs1 m1 t2 s') as [rs2 Hb]. rewrite <- Hs1; eauto. - destruct Hb as [m2 [Hb1 [Hb2 Hb3]]]. - exists rs2, m2. - rewrite Hs2, Hb2; eauto. - Qed. - -Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit: core. -Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same: core. - - -Lemma match_states_concat_trans_code st f sp c rs m h: - match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). -Proof. - intros; constructor 1; simpl. - + intros (t0 & s1' & H0) t s'. - remember (trans_code _) as bl. - destruct bl as [|bh bl]. - { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } - clear H0. - simpl; constructor 1; - intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; simpl in * |- *; - eapply exec_bblock; eauto; simpl; - inversion X2 as [cfi d1 d2 d3 H1|]; subst; eauto; - inversion H1; subst; eauto. - + intros H r; constructor 1; intro X; inversion X. -Qed. - -Lemma step_simu_cfi_step (i: Mach.instruction) (cfi: control_flow_inst) (c: Mach.code) (blc:code) stk f sp rs m (t:trace) (s':Mach.state) b: - trans_inst i = MB_cfi cfi -> - is_trans_code c blc -> - Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp (i::c) rs m) t s' -> - exists s2, cfi_step rao tge cfi (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s' s2. -Proof. - destruct i; simpl in * |-; - (intro H; intro Htc;apply is_trans_code_inv in Htc;rewrite Htc;inversion_clear H;intro X; inversion_clear X). - * eapply ex_intro. - intuition auto. - eapply exec_MBcall;eauto. - rewrite <-H; exploit (find_function_ptr_same); eauto. - * eapply ex_intro. - intuition auto. - eapply exec_MBtailcall;eauto. - - rewrite <-H; exploit (find_function_ptr_same); eauto. - - simpl; rewrite <- parent_sp_preserved; auto. - - simpl; rewrite <- parent_ra_preserved; auto. - * eapply ex_intro. - intuition auto. - eapply exec_MBbuiltin ;eauto. - * exploit find_label_transcode_preserved; eauto. - intros (x & X1 & X2). - eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. - * exploit find_label_transcode_preserved; eauto. - intros (x & X1 & X2). - eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. - * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. - eapply exec_MBcond_false; eauto. - * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2). - eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. - * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. - eapply exec_MBreturn; eauto. - rewrite parent_sp_preserved in H0; subst; auto. - rewrite parent_ra_preserved in H1; subst; auto. -Qed. - -Lemma step_simu_exit_step stk f sp rs m t s1 e c c' b blc: - is_exit e c c' -> is_trans_code c' blc -> - starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s1 -> - exists s2, exit_step rao tge e (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s1 s2. -Proof. - destruct 1. - - (* None *) - intros H0 H1. inversion H1. exists (State (trans_stack stk) f sp blc rs m). - split; eauto. - apply is_trans_code_inv in H0. - rewrite H0. - apply match_states_trans_state. - - (* None *) - intros H0 H1. inversion H1. exists (State (trans_stack stk) f sp blc rs m). - split; eauto. - apply is_trans_code_inv in H0. - rewrite H0. - apply match_states_trans_state. - - (* Some *) - intros H0 H1. - inversion H1; subst. - exploit (step_simu_cfi_step); eauto. - intros [s2 [Hcfi1 Hcfi3]]. - inversion H4. subst; simpl. - autorewrite with trace_rewrite. - exists s2. - split;eauto. -Qed. - -Lemma simu_end_block: - forall s1 t s1', - starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> - exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'. -Proof. - destruct s1; simpl. - + (* State *) - remember (trans_code _) as tc. - rewrite <- is_trans_code_inv in Heqtc. - intros t s1 H. - destruct tc as [|b bl]. - { (* nil => absurd *) - inversion Heqtc. subst. - unfold dist_end_block_code; simpl. - inversion_clear H; - inversion_clear H0. - } - assert (X: Datatypes.S (dist_end_block_code c) = (size b)). - { - unfold dist_end_block_code. - subst_is_trans_code Heqtc. - lapply (size_nonzero c b bl); auto. - omega. - } - rewrite X in H; unfold size in H. - (* decomposition of starN in 3 parts: header + body + exit *) - destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as (t3&t4&s1'&H0&H3&H4). - subst t; clear X H. - destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as (t1&t2&s1''&H&H1&H2). - subst t3; clear H0. - exploit trans_code_decompose; eauto. clear Heqtc. - intros (c0&c1&c2&Hc0&Hc1&Hc2&Heqtc). - (* header steps *) - exploit step_simu_header; eauto. - clear H; intros [X1 X2]; subst. - (* body steps *) - exploit (star_step_simu_body_step); eauto. - clear H1; intros (rs'&m'&H0&H1&H2). subst. - autorewrite with trace_rewrite. - (* exit step *) - exploit step_simu_exit_step; eauto. - clear H3; intros (s2' & H3 & H4). - eapply ex_intro; intuition eauto. - eapply exec_bblock; eauto. - + (* Callstate *) - intros t s1' H; inversion_clear H. - eapply ex_intro; constructor 1; eauto. - inversion H1; subst; clear H1. - inversion_clear H0; simpl. - - (* function_internal*) - cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. - eapply exec_function_internal; eauto. - rewrite <- parent_sp_preserved; eauto. - rewrite <- parent_ra_preserved; eauto. - - (* function_external *) - autorewrite with trace_rewrite. - eapply exec_function_external; eauto. - apply find_funct_ptr_same_external; auto. - rewrite <- parent_sp_preserved; eauto. - + (* Returnstate *) - intros t s1' H; inversion_clear H. - eapply ex_intro; constructor 1; eauto. - inversion H1; subst; clear H1. - inversion_clear H0; simpl. - eapply exec_return. -Qed. - - -Lemma cfi_dist_end_block i c: -(exists cfi, trans_inst i = MB_cfi cfi) -> -dist_end_block_code (i :: c) = 0. -Proof. - unfold dist_end_block_code. - intro H. destruct H as [cfi H]. - destruct i;simpl in H;try(congruence); ( - remember (trans_code _) as bl; - rewrite <- is_trans_code_inv in Heqbl; - inversion Heqbl; subst; simpl in * |- *; try (congruence)). -Qed. - -Theorem transf_program_correct: - forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). -Proof. - apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state). -(* simu_mid_block *) - - intros s1 t s1' H1 H2. - destruct H1; simpl in * |- *; omega || (intuition auto); - destruct H2; eapply cfi_dist_end_block; simpl; eauto. -(* public_preserved *) - - apply senv_preserved. -(* match_initial_states *) - - intros. simpl. - eapply ex_intro; constructor 1. - eapply match_states_trans_state. - destruct H. split. - apply init_mem_preserved; auto. - rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. -(* match_final_states *) - - intros. simpl. destruct H. split with (r := r); auto. -(* final_states_end_block *) - - intros. simpl in H0. - inversion H0. - inversion H; simpl; auto. - all: try (subst; discriminate). - apply cfi_dist_end_block; exists MBreturn; eauto. -(* simu_end_block *) - - apply simu_end_block. -Qed. - -End PRESERVATION. - -(** Auxiliary lemmas used to prove existence of a Mach return adress from a Machblock return address. *) - - - -Lemma is_trans_code_monotonic i c b l: - is_trans_code c (b::l) -> - exists l' b', is_trans_code (i::c) (l' ++ (b'::l)). -Proof. - intro H; destruct c as [|i' c]. { inversion H. } - remember (trans_inst i) as ti. - destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; simpl in * |- *; try congruence ). - exists nil; simpl; eexists. eapply Tr_add_label; eauto. - - (*i=basic*) - destruct i'. - 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. - cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. - rewrite Heqti. - eapply Tr_end_block; eauto. - rewrite <-Heqti. - eapply End_basic. inversion H; try(simpl; congruence). - simpl in H5; congruence. } - all: try(exists nil; simpl; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). - - (*i=cfi*) - destruct i; try(simpl in Heqti; congruence). - all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; - cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; - rewrite Heqti; - eapply Tr_end_block; eauto; - rewrite <-Heqti; - eapply End_cfi; congruence. -Qed. - -Lemma trans_code_monotonic i c b l: - (b::l) = trans_code c -> - exists l' b', trans_code (i::c) = (l' ++ (b'::l)). -Proof. - intro H; rewrite <- is_trans_code_inv in H. - destruct (is_trans_code_monotonic i c b l H) as (l' & b' & H0). - subst_is_trans_code H0. - eauto. -Qed. - -(* FIXME: these two lemma should go into [Coqlib.v] *) -Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). -Proof. - induction l1; simpl; auto with coqlib. -Qed. -Hint Resolve is_tail_app: coqlib. - -Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. -Proof. - induction l1; simpl; auto with coqlib. - intros l2 l3 H; inversion H; eauto with coqlib. -Qed. -Hint Resolve is_tail_app_inv: coqlib. - - -Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> - exists b, is_tail (b :: trans_code c) (trans_code c2). -Proof. - intros H; induction 1. - - intros; subst. - remember (trans_code (Mcall _ _::c)) as tc2. - rewrite <- is_trans_code_inv in Heqtc2. - inversion Heqtc2; simpl in * |- *; subst; try congruence. - subst_is_trans_code H1. - eapply ex_intro; eauto with coqlib. - - intros; exploit IHis_tail; eauto. clear IHis_tail. - intros (b & Hb). inversion Hb; clear Hb. - * exploit (trans_code_monotonic i c2); eauto. - intros (l' & b' & Hl'); rewrite Hl'. - exists b'; simpl; eauto with coqlib. - * exploit (trans_code_monotonic i c2); eauto. - intros (l' & b' & Hl'); rewrite Hl'. - simpl; eapply ex_intro. - eapply is_tail_trans; eauto with coqlib. -Qed. - -Section Mach_Return_Address. - -Variable return_address_offset: function -> code -> ptrofs -> Prop. - -Hypothesis ra_exists: forall (b: bblock) (f: function) (c : list bblock), - is_tail (b :: c) (fn_code f) -> exists ra : ptrofs, return_address_offset f c ra. - -Definition Mach_return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := - return_address_offset (transf_function f) (trans_code c) ofs. - -Lemma Mach_return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> - exists ra, Mach_return_address_offset f c ra. -Proof. - intros. - exploit Mach_Machblock_tail; eauto. - destruct 1. - eapply ra_exists; eauto. -Qed. - -End Mach_Return_Address. |