diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 86 |
1 files changed, 10 insertions, 76 deletions
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 89d41017..decc3e2e 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -1,3 +1,9 @@ +(** * "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. @@ -31,19 +37,13 @@ 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. -(* destruct b. all: try discriminate. - inv H1. auto. - *)Qed. +Qed. -(* FIXME - Replaced FR by IR for MPPA *) 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. -(* destruct b. all: try discriminate. - inv H1. auto. - *)Qed. - +Qed. Lemma preg_of_injective: forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. @@ -277,24 +277,6 @@ Proof. exploit preg_of_injective; eauto. congruence. Qed. -(* Lemma agree_undef_regs2: - forall ms sp rl rs rs', - agree (Mach.undef_regs rl 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 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 -> @@ -607,15 +589,13 @@ Hypothesis transf_function_len: forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned. -(* NB: the hypothesis in comment on [b] is not needed in the proof ! *) Lemma return_address_exists: - forall b f (* sg ros *) c, (* b.(MB.exit) = Some (MBcall sg ros) -> *) is_tail (b :: c) f.(MB.fn_code) -> + 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). -(* unfold return_address_offset. *) monadInv TR2. assert (TL3: is_tail x0 (fn_blocks tf)). { apply is_tail_trans with tc1; auto. @@ -632,7 +612,7 @@ Qed. End RETADDR_EXISTS. (** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points - within the Asm code generated by translating Mach function [f], + 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]. *) @@ -850,18 +830,6 @@ Proof. apply exec_straight_step with rs2 m2; auto. Qed. -(* Theorem exec_straight_bblock: - forall rs1 m1 rs2 m2 rs3 m3 b, - exec_straight (body b) rs1 m1 nil rs2 m2 -> - exec_control_rel (exit b) b rs2 m2 rs3 m3 -> - exec_bblock_rel b rs1 m1 rs3 m3. -Proof. - intros. - econstructor; eauto. unfold exec_bblock. erewrite exec_straight_body; eauto. - inv H0. 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 -> @@ -973,18 +941,6 @@ Proof. - reflexivity. Qed. -(* Lemma exec_straight_pc': - forall c rs1 m1 rs2 m2, - exec_straight c rs1 m1 nil rs2 m2 -> - rs2 PC = rs1 PC. -Proof. - induction c; intros; try (inv H; fail). - inv H. - - erewrite exec_basic_instr_pc; eauto. - - rewrite (IHc rs3 m3 rs2 m2); auto. - erewrite exec_basic_instr_pc; eauto. -Qed. *) - Lemma exec_straight_pc: forall c c' rs1 m1 rs2 m2, exec_straight c rs1 m1 c' rs2 m2 -> @@ -997,25 +953,6 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. -(* Lemma exec_straight_through: - forall c i b lb rs1 m1 rs2 m2 rs2' m2', - bblock_basic_ctl c i = b -> - exec_straight c rs1 m1 nil rs2 m2 -> - nextblock b rs2 = rs2' -> m2 = m2' -> - exec_control ge fn i rs2' m2' = Next rs2' m2' -> (* if the control does not jump *) - exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'. -Proof. - intros. subst. destruct i. - - constructor 1. - + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - + rewrite <- (exec_straight_pc c nil rs1 m1 rs2 m2'); auto. - - destruct c as [|i c]; try (inv H0; fail). - constructor 1. - + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto. -Qed. - *) - Lemma regset_same_assign (rs: regset) r: rs # r <- (rs r) = rs. Proof. @@ -1034,8 +971,6 @@ Proof. 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. *) @@ -1086,7 +1021,6 @@ Qed. End STRAIGHTLINE. - (** * Properties of the Machblock call stack *) Section MATCH_STACK. |