diff options
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 260 |
1 files changed, 6 insertions, 254 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 21af276b..8cc7f0ab 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. -Require Import Asmblockgenproof0. +Require Import Asmblockgenproof0 Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. @@ -30,62 +30,6 @@ Proof. intros. eapply match_transform_partial_program; eauto. Qed. -Remark builtin_body_nil: - forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil. -Proof. - intros. destruct bb as [hd bdy ex WF]. simpl in *. - apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1. - eapply H1; eauto. -Qed. - -Lemma exec_body_app: - forall l l' ge rs m rs'' m'', - exec_body ge (l ++ l') rs m = Next rs'' m'' -> - exists rs' m', - exec_body ge l rs m = Next rs' m' - /\ exec_body ge l' rs' m' = Next rs'' m''. -Proof. - induction l. - - intros. simpl in H. repeat eexists. auto. - - intros. rewrite <- app_comm_cons in H. simpl in H. - destruct (exec_basic_instr ge a rs m) eqn:EXEBI. - + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2). - repeat eexists. simpl. rewrite EXEBI. eauto. auto. - + discriminate. -Qed. - -Lemma exec_body_pc: - forall l ge 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. - -Lemma next_eq: - forall (rs rs': regset) m m', - rs = rs' -> m = m' -> Next rs m = Next rs' m'. -Proof. - intros; apply f_equal2; auto. -Qed. - -Lemma regset_double_set: - forall r1 r2 (rs: regset) v1 v2, - r1 <> r2 -> - (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1). -Proof. - intros. apply functional_extensionality. intros r. destruct (preg_eq r r1). - - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto. - - destruct (preg_eq r r2). - + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto. - + repeat (rewrite Pregmap.gso; auto). -Qed. - Lemma regset_double_set_id: forall r (rs: regset) v1 v2, (rs # r <- v1 # r <- v2) = (rs # r <- v2). @@ -95,191 +39,6 @@ Proof. - repeat (rewrite Pregmap.gso); auto. Qed. -Lemma exec_load_offset_pc_var: - forall t rs m rd ra ofs rs' m' v, - exec_load_offset t rs m rd ra ofs = Next rs' m' -> - exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. - destruct (Mem.loadv _ _ _). - - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. -Qed. - -Lemma exec_load_reg_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_reg t rs m rd ra ro = Next rs' m' -> - exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.loadv _ _ _). - - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. -Qed. - -Lemma exec_load_regxs_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_regxs t rs m rd ra ro = Next rs' m' -> - exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.loadv _ _ _). - - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. -Qed. - -Lemma exec_load_offset_q_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_load_q_offset rs m rd ra ofs = Next rs' m' -> - exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *. - destruct (gpreg_q_expand rd) as [rd0 rd1]. - (* destruct (ireg_eq rd0 ra); try discriminate. *) - rewrite Pregmap.gso; try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - inv H. - destruct (Mem.loadv _ _ _); try discriminate. - inv H1. f_equal. - rewrite (regset_double_set PC rd0) by discriminate. - rewrite (regset_double_set PC rd1) by discriminate. - reflexivity. -Qed. - -Lemma exec_load_offset_o_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_load_o_offset rs m rd ra ofs = Next rs' m' -> - exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *. - destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]. -(* - destruct (ireg_eq rd0 ra); try discriminate. - destruct (ireg_eq rd1 ra); try discriminate. - destruct (ireg_eq rd2 ra); try discriminate. -*) - rewrite Pregmap.gso; try discriminate. - simpl in *. - destruct (Mem.loadv _ _ _); try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - rewrite (regset_double_set PC rd0) by discriminate. - rewrite (regset_double_set PC rd1) by discriminate. - rewrite (regset_double_set PC rd2) by discriminate. - rewrite (regset_double_set PC rd3) by discriminate. - inv H. - trivial. -Qed. - -Lemma exec_store_offset_pc_var: - forall t rs m rd ra ofs rs' m' v, - exec_store_offset t rs m rd ra ofs = Next rs' m' -> - exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate. - destruct (eval_offset ofs); try discriminate. - destruct (Mem.storev _ _ _). - - inv H. apply next_eq; auto. - - discriminate. -Qed. - -Lemma exec_store_q_offset_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_store_q_offset rs m rd ra ofs = Next rs' m' -> - exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. - simpl in *. - destruct (gpreg_q_expand _) as [s0 s1]. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - inv H. apply next_eq; auto. -Qed. - -Lemma exec_store_o_offset_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_store_o_offset rs m rd ra ofs = Next rs' m' -> - exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. - unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *. - destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3]. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - inv H. - trivial. -Qed. - -Lemma exec_store_reg_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_store_reg t rs m rd ra ro = Next rs' m' -> - exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.storev _ _ _). - - inv H. apply next_eq; auto. - - discriminate. -Qed. - -Lemma exec_store_regxs_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_store_regxs t rs m rd ra ro = Next rs' m' -> - exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.storev _ _ _). - - inv H. apply next_eq; auto. - - discriminate. -Qed. - -Lemma exec_basic_instr_pc_var: - forall ge i rs m rs' m' v, - exec_basic_instr ge i rs m = Next rs' m' -> - exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'. -Proof. - intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i. - - unfold exec_arith_instr in *. destruct i; destruct i. - all: try (exploreInst; inv H; apply next_eq; auto; - apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). -(* - (* Some cases treated seperately because exploreInst destructs too much *) - all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *) - - destruct i. - + exploreInst; apply exec_load_offset_pc_var; auto. - + exploreInst; apply exec_load_reg_pc_var; auto. - + exploreInst; apply exec_load_regxs_pc_var; auto. - + apply exec_load_offset_q_pc_var; auto. - + apply exec_load_offset_o_pc_var; auto. - - destruct i. - + exploreInst; apply exec_store_offset_pc_var; auto. - + exploreInst; apply exec_store_reg_pc_var; auto. - + exploreInst; apply exec_store_regxs_pc_var; auto. - + apply exec_store_q_offset_pc_var; auto. - + apply exec_store_o_offset_pc_var; auto. - - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). - destruct (Mem.storev _ _ _ _); try discriminate. - inv H. apply next_eq; auto. apply functional_extensionality. intros. - rewrite (regset_double_set GPR32 PC); try discriminate. - rewrite (regset_double_set GPR12 PC); try discriminate. - rewrite (regset_double_set FP PC); try discriminate. reflexivity. - - repeat (rewrite Pregmap.gso; try discriminate). - destruct (Mem.loadv _ _ _); try discriminate. - destruct (rs GPR12); try discriminate. - destruct (Mem.free _ _ _ _); try discriminate. - inv H. apply next_eq; auto. - rewrite (regset_double_set GPR32 PC). - rewrite (regset_double_set GPR12 PC). reflexivity. - all: discriminate. - - destruct rs0; try discriminate. inv H. apply next_eq; auto. - repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. - - destruct rd; try discriminate. inv H. apply next_eq; auto. - repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. - - inv H. apply next_eq; auto. -Qed. - Lemma exec_body_pc_var: forall l ge rs m rs' m' v, exec_body ge l rs m = Next rs' m' -> @@ -302,9 +61,9 @@ Proof. - subst. repeat (rewrite Pregmap.gss); auto. destruct v; simpl; auto. rewrite Ptrofs.add_assoc. - cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto. + enough (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)) as ->; auto. unfold Ptrofs.add. - cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto. + enough (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)) as ->; auto. repeat (rewrite Ptrofs.unsigned_repr); auto. - repeat (rewrite Pregmap.gso; auto). Qed. @@ -461,7 +220,8 @@ Proof. destruct (zeq pos 0). + inv H. exists lbb. constructor; auto. + apply IHlbb in H. destruct H as (c & TAIL). exists c. - cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto. + enough (pos = pos - size a + size a) as ->. + apply code_tail_S; auto. omega. Qed. @@ -776,12 +536,8 @@ Qed. End PRESERVATION_ASMBLOCK. - - - Require Import Asmvliw. - Lemma verified_par_checks_alls_bundles lb x: forall bundle, verify_par lb = OK x -> List.In bundle lb -> verify_par_bblock bundle = OK tt. @@ -792,7 +548,6 @@ Proof. destruct x0; auto. Qed. - Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle: verified_schedule_nob bb = OK lb -> List.In bundle lb -> verify_par_bblock bundle = OK tt. @@ -813,7 +568,7 @@ Proof. unfold builtin_alone in H0. erewrite H0; eauto. Qed. -Local Hint Resolve verified_schedule_nob_checks_alls_bundles. +Local Hint Resolve verified_schedule_nob_checks_alls_bundles: core. Lemma verified_schedule_checks_alls_bundles bb lb bundle: verified_schedule bb = OK lb -> @@ -914,9 +669,6 @@ Qed. End PRESERVATION_ASMVLIW. - - - Section PRESERVATION. Variables prog tprog: program. |