diff options
Diffstat (limited to 'aarch64/PostpassSchedulingproof.v')
-rw-r--r-- | aarch64/PostpassSchedulingproof.v | 429 |
1 files changed, 91 insertions, 338 deletions
diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 22daede9..c32579a2 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -5,6 +5,7 @@ (* Sylvain Boulmé Grenoble-INP, VERIMAG *) (* David Monniaux CNRS, VERIMAG *) (* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) (* *) (* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) (* This file is distributed under the terms of the INRIA *) @@ -16,7 +17,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 Asmblockprops. +Require Import Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. @@ -32,103 +33,6 @@ Proof. intros. eapply match_transform_partial_program; eauto. Qed. -(* -Lemma regset_double_set_id: - forall r (rs: regset) v1 v2, - (rs # r <- v1 # r <- v2) = (rs # r <- v2). -Proof. - intros. apply functional_extensionality. intros. destruct (preg_eq r x). - - subst r. repeat (rewrite Pregmap.gss; auto). - - repeat (rewrite Pregmap.gso); auto. -Qed. - -Lemma exec_body_pc_var: - forall l ge rs m rs' m' v, - exec_body ge l rs m = Next rs' m' -> - exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'. -Proof. - induction l. - - intros. simpl. simpl in H. inv H. auto. - - intros. simpl in *. - destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate. - erewrite exec_basic_instr_pc_var; eauto. -Qed. - -Lemma pc_set_add: - forall rs v r x y, - 0 <= x <= Ptrofs.max_unsigned -> - 0 <= y <= Ptrofs.max_unsigned -> - rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)). -Proof. - intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0). - - subst. repeat (rewrite Pregmap.gss); auto. - destruct v; simpl; auto. - rewrite Ptrofs.add_assoc. - enough (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)) as ->; auto. - unfold Ptrofs.add. - 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. - -Lemma concat2_straight: - forall a b bb rs m rs'' m'' f ge, - concat2 a b = OK bb -> - exec_bblock ge f bb rs m = Next rs'' m'' -> - exists rs' m', - exec_bblock ge f a rs m = Next rs' m' - /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) - /\ exec_bblock ge f b rs' m' = Next rs'' m''. -Proof. - intros until ge. intros CONC2 EXEB. - exploit concat2_zlt_size; eauto. intros (LTA & LTB). - exploit concat2_noexit; eauto. intros EXA. - exploit concat2_decomp; eauto. intros. inv H. - unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate. - rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2). - eexists; eexists. split. - unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto. - split. - exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto. - unfold exec_bblock. unfold nextblock, incrPC. rewrite regset_same_assign. erewrite exec_body_pc_var; eauto. - rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. - assert (size bb = size a + size b). - { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. - repeat (rewrite Nat2Z.inj_add). omega. } - clear EXA H0 H1. rewrite H in EXEB. - assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } - rewrite H0. rewrite <- pc_set_add; auto. - exploit size_positive. instantiate (1 := a). intro. omega. - exploit size_positive. instantiate (1 := b). intro. omega. -Qed. - -Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : - forall a bb rs m lbb rs'' m'', - lbb <> nil -> - concat_all (a :: lbb) = OK bb -> - exec_bblock ge f bb rs m = Next rs'' m'' -> - exists bb' rs' m', - concat_all lbb = OK bb' - /\ exec_bblock ge f a rs m = Next rs' m' - /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) - /\ exec_bblock ge f bb' rs' m' = Next rs'' m''. -Proof. - intros until m''. intros Hnonil CONC EXEB. - simpl in CONC. - destruct lbb as [|b lbb]; try contradiction. clear Hnonil. - monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2). - exists x. repeat econstructor. all: eauto. -Qed. - -Lemma ptrofs_add_repr : - forall a b, - Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)). -Proof. - intros a b. - rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq). - rewrite <- Zplus_mod. auto. -Qed. -*) Section PRESERVATION_ASMBLOCK. Variables prog tprog: program. @@ -136,15 +40,7 @@ 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. -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. @@ -153,31 +49,14 @@ 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) -> - transf_function f = OK tf -> - Genv.find_funct_ptr tge fb = Some (Internal tf). -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. @@ -212,48 +91,6 @@ Proof. intros. inv H0. inv H. econstructor; eauto. Qed. -(* Lemma tail_find_bblock: - forall lbb pos bb, - find_bblock pos lbb = Some bb -> - exists c, code_tail pos lbb (bb::c). -Proof. - induction lbb. - - intros. simpl in H. inv H. - - intros. simpl in H. - destruct (zlt pos 0); try (inv H; fail). - destruct (zeq pos 0). - + inv H. exists lbb. constructor; auto. - + apply IHlbb in H. destruct H as (c & TAIL). exists c. - enough (pos = pos - size a + size a) as ->. - apply code_tail_S; auto. - omega. -Qed. *) - -(* Lemma code_tail_head_app: - forall l pos c1 c2, - code_tail pos c1 c2 -> - code_tail (pos + size_blocks l) (l++c1) c2. -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. *) - -(* 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. -Proof. - induction c; intros. - - simpl in H. inv H. inv H0. - - inv H0. - + monadInv H. exists x0; eauto. - + unfold transf_blocks in H. fold transf_blocks in H. monadInv H. - exploit IHc; eauto. -Qed. *) - Lemma transf_find_bblock: forall ofs f bb tf, find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> @@ -269,97 +106,43 @@ Proof. 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. + 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 stick_header_neutral: forall a, + a = (stick_header (header a) (no_header a)). 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. + intros. + unfold stick_header. unfold Asmblock.stick_header_obligation_1. simpl. destruct a. + simpl. reflexivity. +Qed. 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. - intros. simpl. auto. -Qed. - -Lemma verified_schedule_not_empty: - forall bb lbb, - verified_schedule bb = OK lbb -> lbb <> nil. -Proof. - intros. apply verified_schedule_size in H. - pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. - destruct lbb; simpl in *; discriminate. -Qed. - -Lemma header_nil_label_pos_none: - forall lbb l p, - Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None. -Proof. - induction lbb. - - intros. simpl. auto. - - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. } - auto. -Qed. Lemma verified_schedule_label: - forall bb tbb lbb l, - verified_schedule bb = OK (tbb :: lbb) -> - is_label l bb = is_label l tbb - /\ label_pos l 0 lbb = None. -Proof. - intros. exploit verified_schedule_header; eauto. - intros (HdrEq & HdrNil). - split. - - unfold is_label. rewrite HdrEq. reflexivity. - - apply header_nil_label_pos_none. assumption. -Qed. - -Lemma label_pos_app_none: - forall c c' l p p', - label_pos l p c = None -> - label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c'). + forall bb tbb l, + verified_schedule bb = OK (tbb) -> + is_label l bb = is_label l tbb. Proof. - induction c. - - intros. simpl in *. rewrite Z.add_0_r. reflexivity. - - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL. - + discriminate. - + eapply IHc in H. rewrite Z.add_assoc. eauto. + intros. + unfold is_label. + monadInv H. simpl. auto. Qed. Remark label_pos_pvar_none_add: @@ -422,20 +205,18 @@ Proof. eapply label_pos_pvar_add; eauto. Qed. -Lemma label_pos_head_app: - forall c bb lbb l tc p, - verified_schedule bb = OK lbb -> +Lemma label_pos_head_cons: + forall c bb tbb l tc p, + verified_schedule bb = OK tbb -> label_pos l p c = label_pos l p tc -> - label_pos l p (bb :: c) = label_pos l p (lbb ++ tc). + label_pos l p (bb :: c) = label_pos l p (tbb :: tc). Proof. - intros. simpl. destruct lbb as [|tbb lbb]. - - apply verified_schedule_not_empty in H. contradiction. - - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS). - rewrite ISLBL. - destruct (is_label l tbb) eqn:ISLBL'; simpl; auto. - eapply label_pos_pvar in H0. erewrite H0. - erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc. - erewrite label_pos_app_none; eauto. + intros. simpl. + exploit verified_schedule_label; eauto. intros ISLBL. + rewrite ISLBL. + destruct (is_label l tbb) eqn:ISLBL'; simpl; auto. + eapply label_pos_pvar in H0. erewrite H0. + erewrite verified_schedule_size; eauto. Qed. Lemma label_pos_preserved: @@ -444,8 +225,8 @@ Lemma label_pos_preserved: Proof. induction c. - intros. simpl in *. inv H. reflexivity. - - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ. - eapply label_pos_head_app; eauto. + - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. + eapply IHc in EQ. eapply label_pos_head_cons; eauto. Qed. Lemma label_pos_preserved_blocks: @@ -458,38 +239,6 @@ Proof. monadInv EQ0. simpl. eapply label_pos_preserved; eauto. Qed. -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 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: forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m. Proof. @@ -507,55 +256,59 @@ Proof. destruct (exec_basic _ _ _); auto. Qed. -(* Lemma transf_exec_bblock: - forall f tf bb b ofs t rs m rs' m', - rs PC = Vptr b ofs -> +Lemma transf_exec_cfi: forall f tf cfi rs m, transf_function f = OK tf -> - 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 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 -> *) - rs PC = Vptr b ofs -> - 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 bb'. - - intros until m'. simpl. intros. discriminate. - - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB. - destruct lbb. - + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto. - + exploit concat_all_exec_bblock; eauto; try discriminate. - intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1). - eapply plus_left. - econstructor. - 3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto. - all: eauto. - eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto. - eapply code_tail_next_int; eauto. -Qed. -*) + exec_cfi ge f cfi rs m = exec_cfi tge tf cfi rs m. +Proof. + intros. destruct cfi; simpl; auto; + assert (ge = Genv.globalenv prog); auto; + assert (tge = Genv.globalenv tprog); auto; + pose symbol_address_preserved. + all: try unfold eval_branch; try unfold eval_neg_branch; try unfold goto_label; + try erewrite label_pos_preserved_blocks; try rewrite e; eauto. + destruct (rs # X16 <- Vundef r1); auto. + destruct (list_nth_z tbl (Int.unsigned i)); auto. + erewrite label_pos_preserved_blocks; eauto. +Qed. + +Lemma transf_exec_exit: + forall f tf sz ex t rs m rs' m', + transf_function f = OK tf -> + exec_exit ge f sz rs m ex t rs' m' -> + exec_exit tge tf sz rs m ex t rs' m'. +Proof. + intros. induction H0. + - econstructor. + - econstructor. erewrite <- transf_exec_cfi; eauto. + - econstructor; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. +Qed. + +Lemma transf_exec_bblock: + forall f tf bb t rs m rs' m', + transf_function f = OK tf -> + exec_bblock lk ge f bb rs m t rs' m' -> + exec_bblock lk tge tf bb rs m t rs' m'. +Proof. + intros. + destruct H0 as [rs1[m1[BDY EXIT]]]. + unfold exec_bblock. + eexists; eexists; split. + rewrite <- transf_exec_body; eauto. + eapply transf_exec_exit; eauto. +Qed. + Theorem transf_step_correct: forall s1 t s2, step lk ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), (exists s2', step lk tge s1' t s2' /\ match_states s2 s2'). Proof. induction 1; intros; inv MS. - - inversion H2. - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. - exploit transf_exec_bblock; eauto. intros (lbb & EBB & FIND). + - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + exploit transf_find_bblock; eauto. intros (tbb & VES & FIND). + exploit verified_schedule_correct; eauto. intros EBB. + eapply transf_exec_bblock in EBB; eauto. exists (State rs' m'). split; try (econstructor; eauto). - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. @@ -576,9 +329,9 @@ Qed. End PRESERVATION_ASMBLOCK. +(* 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. |