From 1685bfd6d017a487368ceb3c71cfaf03c9d42c9b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 23 Nov 2020 23:53:22 +0100 Subject: Start of the postpasschedproof, redefining verify schedule lemmas --- aarch64/PostpassSchedulingproof.v | 219 ++++++++++++++++++++++---------------- 1 file changed, 129 insertions(+), 90 deletions(-) (limited to 'aarch64/PostpassSchedulingproof.v') diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 86a160bd..22daede9 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -128,14 +128,15 @@ Proof. rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq). rewrite <- Zplus_mod. auto. Qed. - +*) Section PRESERVATION_ASMBLOCK. Variables prog tprog: program. +Variable lk: aarch64_linker. Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. - +(* Lemma transf_function_no_overflow: forall f tf, transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. @@ -143,7 +144,7 @@ Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. omega. Qed. - +*) Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. @@ -152,21 +153,21 @@ Proof (Genv.find_symbol_match TRANSL). Lemma senv_preserved: Senv.equiv ge tge. Proof (Genv.senv_match TRANSL). - +(* Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_transf_partial TRANSL). - +*) Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSL). - +(* Lemma functions_transl: forall fb f tf, Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -176,7 +177,7 @@ Proof. intros. exploit function_ptr_translated; eauto. intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto. Qed. - +*) Inductive match_states: state -> state -> Prop := | match_states_intro: forall s1 s2, s1 = s2 -> match_states s1 s2. @@ -211,7 +212,7 @@ Proof. intros. inv H0. inv H. econstructor; eauto. Qed. -Lemma tail_find_bblock: +(* Lemma tail_find_bblock: forall lbb pos bb, find_bblock pos lbb = Some bb -> exists c, code_tail pos lbb (bb::c). @@ -226,9 +227,9 @@ Proof. enough (pos = pos - size a + size a) as ->. apply code_tail_S; auto. omega. -Qed. +Qed. *) -Lemma code_tail_head_app: +(* Lemma code_tail_head_app: forall l pos c1 c2, code_tail pos c1 c2 -> code_tail (pos + size_blocks l) (l++c1) c2. @@ -236,51 +237,81 @@ Proof. induction l. - intros. simpl. rewrite Z.add_0_r. auto. - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption. -Qed. +Qed. *) -Lemma transf_blocks_verified: +(* Lemma transf_blocks_verified: forall c tc pos bb c', transf_blocks c = OK tc -> code_tail pos c (bb::c') -> exists lbb, - verified_schedule bb = OK lbb - /\ exists tc', code_tail pos tc (lbb ++ tc'). + verified_schedule bb = OK lbb. Proof. induction c; intros. - simpl in H. inv H. inv H0. - inv H0. - + monadInv H. exists x0. - split; simpl; auto. eexists; eauto. econstructor; eauto. + + monadInv H. exists x0; eauto. + unfold transf_blocks in H. fold transf_blocks in H. monadInv H. exploit IHc; eauto. - intros (lbb & TRANS & tc' & TAIL). -(* monadInv TRANS. *) - repeat eexists; eauto. - erewrite verified_schedule_size; eauto. - apply code_tail_head_app. - eauto. -Qed. +Qed. *) Lemma transf_find_bblock: forall ofs f bb tf, find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> transf_function f = OK tf -> - exists lbb, - verified_schedule bb = OK lbb - /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c). + exists tbb, + verified_schedule bb = OK tbb + /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. Proof. intros. monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0. - monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL). - eapply transf_blocks_verified; eauto. + monadInv EQ. simpl in *. + generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0. + induction (fn_blocks f). + - intros. simpl in *. discriminate. + - intros. simpl in *. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. eauto. + + monadInv EQ0. + exploit IHb; eauto. + intros (tbb & SCH & FIND). + eexists; split; eauto. + inv FIND. + unfold verify_size in EQ0. + destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. + rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. + reflexivity. Qed. +Lemma transf_exec_bblock: + forall f tf bb ofs t rs m rs' m', + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> + transf_function f = OK tf -> + exec_bblock lk ge f bb rs m t rs' m' -> + exists tbb, + exec_bblock lk tge tf tbb rs m t rs' m' + /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. +Proof. + intros. inv H1. + monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try (inv EQ0; fail). inv EQ0. + monadInv EQ. simpl in *. + generalize (Ptrofs.unsigned ofs) H x0 g EQ0; clear ofs H x0 g EQ0. + induction (fn_blocks f). + - intros. simpl in *. discriminate. + - intros. simpl in *. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. +Admitted. + Lemma symbol_address_preserved: forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs. Proof. intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity. Qed. - +(* Lemma head_tail {A: Type}: forall (l: list A) hd, hd::l = hd :: (tail (hd::l)). Proof. @@ -427,56 +458,81 @@ Proof. monadInv EQ0. simpl. eapply label_pos_preserved; eauto. Qed. -Lemma transf_exec_control: - forall f tf ex rs m, - transf_function f = OK tf -> - exec_control ge f ex rs m = exec_control tge tf ex rs m. +Lemma transf_exec_exit: + forall f sz cfi t rs m rs' m', + (exec_cfi ge f cfi (incrPC sz rs) m = Next rs' m') -> + exec_exit ge f sz rs m (Some (PCtlFlow cfi)) t rs' m'. Proof. - intros. destruct ex; simpl; auto. - assert (ge = Genv.globalenv prog). auto. + intros. + destruct t. + - constructor; auto. + - congruence. + destruct ex; try destruct c; simpl. + - generalize cfi_step. intros. apply H0. + + monadInv H. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned _); try discriminate. + monadInv EQ0. simpl. + assert (ge = Genv.globalenv prog). auto. assert (tge = Genv.globalenv tprog). auto. pose symbol_address_preserved. + + + exists rs; exists m. apply cfi_step. inv H. + destruct cfi; simpl; eauto. + assert (ge = Genv.globalenv prog); auto; + assert (tge = Genv.globalenv tprog); auto; + pose symbol_address_preserved; simpl. + - + constructor. + unfold exec_exit. exploreInst; simpl; auto; try congruence; unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto. Qed. - -Lemma transf_exec_basic_instr: - forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. +*) +Lemma transf_exec_basic: + forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m. Proof. intros. pose symbol_address_preserved. - unfold exec_basic_instr. unfold bstep. exploreInst; simpl; auto; try congruence. - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. + unfold exec_basic. + destruct i; simpl; auto; try congruence. Qed. Lemma transf_exec_body: - forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m. + forall bdy rs m, exec_body lk ge bdy rs m = exec_body lk tge bdy rs m. Proof. induction bdy; intros. - simpl. reflexivity. - - simpl. rewrite transf_exec_basic_instr. - destruct (exec_basic_instr _ _ _); auto. + - simpl. rewrite transf_exec_basic. + destruct (exec_basic _ _ _); auto. Qed. -Lemma transf_exec_bblock: - forall f tf bb rs m, +(* Lemma transf_exec_bblock: + forall f tf bb b ofs t rs m rs' m', + rs PC = Vptr b ofs -> transf_function f = OK tf -> - exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m. -Proof. - intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto. - eapply transf_exec_control; eauto. -Qed. - + exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk tge tf bb rs m t rs' m'. +Proof. + intros. monadInv H. monadInv EQ. pose symbol_address_preserved. + simpl in *. + destruct (zlt Ptrofs.max_unsigned (size_blocks x0)); try discriminate. + monadInv EQ0. unfold transf_blocks in *. destruct f. simpl in *. + generalize H0 EQ1; clear H0 EQ1. + induction (fn_blocks). + - intros. monadInv EQ1. auto. admit. + - intros. apply IHb. +Qed. *) +(* Lemma transf_step_simu: - forall tf b lbb ofs c tbb rs m rs' m', + forall f b bb ofs c rs m t rs' m' rs1 m1, Genv.find_funct_ptr tge b = Some (Internal tf) -> - size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> + (* size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> *) rs PC = Vptr b ofs -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) -> - concat_all lbb = OK tbb -> - exec_bblock tge tf tbb rs m = Next rs' m' -> - plus step tge (State rs m) E0 (State rs' m'). + exec_body lk ge (body bi) rs m = Next rs1 m1 -> + exec_exit ge f (Ptrofs.repr (size bb)) rs1 m1 (exit bb) t rs' m' -> + plus (step lk) tge (State rs m) t (State rs' m'). Proof. - induction lbb. + induction bb'. - intros until m'. simpl. intros. discriminate. - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB. destruct lbb. @@ -490,47 +546,28 @@ Proof. eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto. eapply code_tail_next_int; eauto. Qed. - +*) Theorem transf_step_correct: - forall s1 t s2, step ge s1 t s2 -> + forall s1 t s2, step lk ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), - (exists s2', plus step tge s1' t s2' /\ match_states s2 s2'). + (exists s2', step lk tge s1' t s2' /\ match_states s2 s2'). Proof. induction 1; intros; inv MS. - - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. - exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC. - assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). - eapply transf_function_no_overflow; eauto. - - erewrite transf_exec_bblock in H2; eauto. - unfold bblock_simu in BBEQ. rewrite BBEQ in H2; try congruence. - exists (State rs' m'). split; try (constructor; auto). - eapply transf_step_simu; eauto. - - - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. - exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_builtin_idem; eauto. intros. subst lbb. - - remember (State (nextblock _ _) _) as s'. exists s'. - split; try constructor; auto. - eapply plus_one. subst s'. - eapply exec_step_builtin. - 3: eapply find_bblock_tail. simpl in TAIL. 3: eauto. - all: eauto. - eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - + - inversion H2. + exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + exploit transf_exec_bblock; eauto. intros (lbb & EBB & FIND). + exists (State rs' m'). + split; try (econstructor; eauto). - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. remember (State _ m') as s'. exists s'. split; try constructor; auto. - subst s'. eapply plus_one. eapply exec_step_external; eauto. + subst s'. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. Qed. Theorem transf_program_correct_Asmblock: - forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). + forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog). Proof. - eapply forward_simulation_plus. + eapply forward_simulation_step. - apply senv_preserved. - apply transf_initial_states. - apply transf_final_states. @@ -539,8 +576,9 @@ Qed. End PRESERVATION_ASMBLOCK. -Require Import Asmvliw. +Require Import Asm. +(* 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. @@ -605,8 +643,9 @@ Proof. destruct (zlt ofs 0); try congruence. destruct (zeq ofs 0); eauto. intros X; inversion X; eauto. -Qed. +Qed.*) +(* Section PRESERVATION_ASMVLIW. Variables prog tprog: program. -- cgit