From 241da496839a9101e843ce7b1da4a668f998498a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 2 Nov 2020 17:13:50 +0100 Subject: Preparation for postpass in aarch64 and refactoring --- aarch64/PostpassScheduling.v | 530 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 530 insertions(+) create mode 100644 aarch64/PostpassScheduling.v (limited to 'aarch64/PostpassScheduling.v') diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v new file mode 100644 index 00000000..485b297b --- /dev/null +++ b/aarch64/PostpassScheduling.v @@ -0,0 +1,530 @@ +(* *************************************************************) +(* *) +(* 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. *) +(* *) +(* *************************************************************) + +(** Implementation (and basic properties) of the verified postpass scheduler *) + +Require Import Coqlib Errors AST Integers. +Require Import Asmblock Axioms Memory Globalenvs. +Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. +(*Require Peephole.*) + +Local Open Scope error_monad_scope. + +(** * Oracle taking as input a basic block, + returns a scheduled basic block *) +Axiom schedule: bblock -> (list basic) * option control. + +Extract Constant schedule => "PostpassSchedulingOracle.schedule". + +(* +(** * Concat all bundles into one big basic block *) + +(* Lemmas necessary for defining concat_all *) +Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil. +Proof. + intros. destruct l; simpl. + - contradiction. + - discriminate. +Qed. + +Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil. +Proof. + destruct l. + - intros. simpl; auto. + - intros. rewrite <- app_comm_cons. discriminate. +Qed. + +Definition check_size bb := + if zlt Ptrofs.max_unsigned (size bb) + then Error (msg "PostpassSchedulingproof.check_size") + else OK tt. + +Program Definition concat2 (bb bb': bblock) : res bblock := + do ch <- check_size bb; + do ch' <- check_size bb'; + match (exit bb) with + | None => + match (header bb') with + | nil => + match (exit bb') with + | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone") + | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |} + end + | _ => Error (msg "PostpassSchedulingproof.concat2") + end + | _ => Error (msg "PostpassSchedulingproof.concat2") + end. +Next Obligation. + apply wf_bblock_refl. constructor. + - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *. + apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF. + inversion_clear WF'. inversion_clear WF. clear H1 H3. + inversion H2; inversion H0. + + left. apply app_nonil. auto. + + right. auto. + + left. apply app_nonil2. auto. + + right. auto. + - unfold builtin_alone. intros. rewrite H0 in H. + assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))). + apply (H ef args res). contradict H1. auto. +Defined. + +Lemma concat2_zlt_size: + forall a b bb, + concat2 a b = OK bb -> + size a <= Ptrofs.max_unsigned + /\ size b <= Ptrofs.max_unsigned. +Proof. + intros. monadInv H. + split. + - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega. + - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega. +Qed. + +Lemma concat2_noexit: + forall a b bb, + concat2 a b = OK bb -> + exit a = None. +Proof. + intros. destruct a as [hd bdy ex WF]; simpl in *. + destruct ex as [e|]; simpl in *; auto. + unfold concat2 in H. simpl in H. monadInv H. +Qed. + +Lemma concat2_decomp: + forall a b bb, + concat2 a b = OK bb -> + body bb = body a ++ body b + /\ exit bb = exit b. +Proof. + intros. exploit concat2_noexit; eauto. intros. + destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *. + subst exa. + unfold concat2 in H; simpl in H. + destruct hdb. + - destruct exb. + + destruct c. + * destruct i; monadInv H; split; auto. + * monadInv H. split; auto. + + monadInv H. split; auto. + - monadInv H. +Qed. + +Lemma concat2_size: + forall a b bb, concat2 a b = OK bb -> size bb = size a + size b. +Proof. + intros. unfold concat2 in H. + destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *. + destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2). + - destruct c. + + destruct i; monadInv EQ2; + unfold size; simpl; rewrite app_length; rewrite Nat.add_0_r; rewrite <- Nat2Z.inj_add; rewrite Nat.add_assoc; reflexivity. + + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity. + - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity. +Qed. + +Lemma concat2_header: + forall bb bb' tbb, + concat2 bb bb' = OK tbb -> header bb = header tbb. +Proof. + intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. + unfold concat2 in H. simpl in H. monadInv H. + destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'. + - destruct c. + + destruct i; try discriminate; congruence. + + congruence. + - congruence. +Qed. + +Lemma concat2_no_header_in_middle: + forall bb bb' tbb, + concat2 bb bb' = OK tbb -> + header bb' = nil. +Proof. + intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. + unfold concat2 in H. simpl in H. monadInv H. + destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity. +Qed. + + + +Fixpoint concat_all (lbb: list bblock) : res bblock := + match lbb with + | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list") + | bb::nil => OK bb + | bb::lbb => + do bb' <- concat_all lbb; + concat2 bb bb' + end. + +Lemma concat_all_size : + forall lbb a bb bb', + concat_all (a :: lbb) = OK bb -> + concat_all lbb = OK bb' -> + size bb = size a + size bb'. +Proof. + intros. unfold concat_all in H. fold concat_all in H. + destruct lbb; try discriminate. + monadInv H. rewrite H0 in EQ. inv EQ. + apply concat2_size. assumption. +Qed. + +Lemma concat_all_header: + forall lbb bb tbb, + concat_all (bb::lbb) = OK tbb -> header bb = header tbb. +Proof. + destruct lbb. + - intros. simpl in H. congruence. + - intros. simpl in H. destruct lbb. + + inv H. eapply concat2_header; eassumption. + + monadInv H. eapply concat2_header; eassumption. +Qed. + +Lemma concat_all_no_header_in_middle: + forall lbb tbb, + concat_all lbb = OK tbb -> + Forall (fun b => header b = nil) (tail lbb). +Proof. + induction lbb; intros; try constructor. + simpl. simpl in H. destruct lbb. + - constructor. + - monadInv H. simpl tl in IHlbb. constructor. + + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence. + + apply IHlbb in EQ. assumption. +Qed. + +Inductive is_concat : bblock -> list bblock -> Prop := + | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb. +*) +(** * Remainder of the verified scheduler *) + +(*Definition verify_schedule (bb bb' : bblock) : res unit :=*) + (*match bblock_simub bb bb' with*) + (*| true => OK tt*) + (*| false => Error (msg "PostpassScheduling.verify_schedule")*) + (*end.*) + + +(*Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").*) + +(*Lemma verify_size_size:*) + (*forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.*) +(*Proof.*) + (*intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.*) + (*apply Z.eqb_eq. assumption.*) +(*Qed.*) + +(*Lemma verify_schedule_no_header:*) + (*forall bb bb',*) + (*verify_schedule (no_header bb) bb' = verify_schedule bb bb'.*) +(*Proof.*) + (*intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv.*) + (*reflexivity.*) +(*Qed.*) + + +(*Lemma stick_header_verify_schedule:*) + (*forall hd bb' hbb' bb,*) + (*stick_header hd bb' = hbb' ->*) + (*verify_schedule bb bb' = verify_schedule bb hbb'.*) +(*Proof.*) + (*intros. unfold verify_schedule. unfold bblock_simub, pure_bblock_simu_test, bblock_simu_test.*) + (*rewrite <- H. rewrite trans_block_header_inv. reflexivity.*) +(*Qed.*) + +(*Lemma check_size_stick_header:*) + (*forall bb hd,*) + (*check_size bb = check_size (stick_header hd bb).*) +(*Proof.*) + (*intros. unfold check_size. rewrite stick_header_size. reflexivity.*) +(*Qed.*) + +(*Lemma stick_header_concat2:*) + (*forall bb bb' hd tbb,*) + (*concat2 bb bb' = OK tbb ->*) + (*concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).*) +(*Proof.*) + (*intros. monadInv H. erewrite check_size_stick_header in EQ.*) + (*unfold concat2. rewrite EQ. rewrite EQ1. simpl.*) + (*destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.*) + (*destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.*) + (*- destruct c.*) + (*+ destruct i; try discriminate; inv EQ2; unfold stick_header; simpl; reflexivity.*) + (*+ inv EQ2. unfold stick_header; simpl. reflexivity.*) + (*- inv EQ2. unfold stick_header; simpl. reflexivity.*) +(*Qed.*) + +(*Lemma stick_header_concat_all:*) + (*forall bb c tbb hd,*) + (*concat_all (bb :: c) = OK tbb ->*) + (*concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).*) +(*Proof.*) + (*intros. simpl in *. destruct c; try congruence.*) + (*monadInv H. rewrite EQ. simpl.*) + (*apply stick_header_concat2. assumption.*) +(*Qed.*) + + + +(*Definition stick_header_code (h : list label) (lbb : list bblock) :=*) + (*match (head lbb) with*) + (*| None => Error (msg "PostpassScheduling.stick_header: empty schedule")*) + (*| Some fst => OK ((stick_header h fst) :: tail lbb)*) + (*end.*) + +(*Lemma stick_header_code_no_header:*) + (*forall bb c,*) + (*stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).*) +(*Proof.*) + (*intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.*) +(*Qed.*) + +(*Lemma hd_tl_size:*) + (*forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).*) +(*Proof.*) + (*destruct lbb.*) + (*- intros. simpl in H. discriminate.*) + (*- intros. simpl in H. inv H. simpl. reflexivity.*) +(*Qed.*) + +(*Lemma stick_header_code_size:*) + (*forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.*) +(*Proof.*) + (*intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.*) + (*inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.*) +(*Qed.*) + +(*Lemma stick_header_code_no_header_in_middle:*) + (*forall c h lbb,*) + (*stick_header_code h c = OK lbb ->*) + (*Forall (fun b => header b = nil) (tl c) ->*) + (*Forall (fun b => header b = nil) (tl lbb).*) +(*Proof.*) + (*destruct c; intros.*) + (*- unfold stick_header_code in H. simpl in H. discriminate.*) + (*- unfold stick_header_code in H. simpl in H. inv H. simpl in H0.*) + (*simpl. assumption.*) +(*Qed.*) + +(*Lemma stick_header_code_concat_all:*) + (*forall hd lbb hlbb tbb,*) + (*stick_header_code hd lbb = OK hlbb ->*) + (*concat_all lbb = OK tbb ->*) + (*exists htbb,*) + (*concat_all hlbb = OK htbb*) + (*/\ stick_header hd tbb = htbb.*) +(*Proof.*) + (*intros. exists (stick_header hd tbb). split; auto.*) + (*destruct lbb.*) + (*- unfold stick_header_code in H. simpl in H. discriminate.*) + (*- unfold stick_header_code in H. simpl in H. inv H.*) + (*apply stick_header_concat_all. assumption.*) +(*Qed.*) + +Program Definition make_bblock_from_basics lb := + match lb with + | nil => Error (msg "PostpassScheduling.make_bblock_from_basics") + | b :: lb => OK {| header := nil; body := b::lb; exit := None |} + end. + +Fixpoint schedule_to_bblocks_nocontrol llb := + match llb with + | nil => OK nil + | lb :: llb => do bb <- make_bblock_from_basics lb; + do lbb <- schedule_to_bblocks_nocontrol llb; + OK (bb :: lbb) + end. + +Program Definition make_bblock_from_basics_and_control lb c := + match c with + | PCtlFlow cf => OK {| header := nil; body := lb; exit := Some (PCtlFlow cf) |} + | _ => Error (msg "PostpassScheduling.make_bblock_from_basics_and_control") + end. +Next Obligation. +Admitted. +(* TODO + apply wf_bblock_refl. constructor. + - right. discriminate. + - discriminate. +Qed.*) + +(*Fixpoint schedule_to_bblocks_wcontrol llb c :=*) + (*match llb with*) + (*| nil => OK ((bblock_single_inst (PControl c)) :: nil) [> TODO fusion avec au dessus ? <]*) + (*| lb :: nil => do bb <- make_bblock_from_basics_and_control lb c; OK (bb :: nil)*) + (*| lb :: llb => do bb <- make_bblock_from_basics lb;*) + (*do lbb <- schedule_to_bblocks_wcontrol llb c;*) + (*OK (bb :: lbb)*) + (*end.*) + +(*Definition schedule_to_bblocks (llb: list (list basic)) (oc: option control) : res (list bblock) :=*) + (*match oc with*) + (*| None => schedule_to_bblocks_nocontrol llb*) + (*| Some c => schedule_to_bblocks_wcontrol llb c*) + (*end.*) + +(*Definition do_schedule (bb: bblock) : res (list bblock) :=*) + (*if (Z.eqb (size bb) 1) then OK (bb::nil) *) + (*else match (schedule bb) with (llb, oc) => schedule_to_bblocks llb oc end. [> TODO Something here <]*) + +(*Definition verify_par_bblock (bb: bblock) : res unit :=*) + (*if (bblock_para_check bb) then OK tt else Error (msg "PostpassScheduling.verify_par_bblock").*) + +(*Fixpoint verify_par (lbb: list bblock) :=*) + (*match lbb with*) + (*| nil => OK tt*) + (*| bb :: lbb => do res <- verify_par_bblock bb; verify_par lbb*) + (*end.*) + +(*Definition verified_schedule_nob (bb : bblock) : res (list bblock) :=*) + (*let bb' := no_header bb in*) + (*[> TODO remove? let bb'' := Peephole.optimize_bblock bb' in<]*) + (*do lbb <- do_schedule bb';*) + (*do tbb <- concat_all lbb;*) + (*do sizecheck <- verify_size bb lbb;*) + (*do schedcheck <- verify_schedule bb' tbb;*) + (*do res <- stick_header_code (header bb) lbb;*) + (*do parcheck <- verify_par res;*) + (*OK res.*) + +(*Lemma verified_schedule_nob_size:*) + (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*) +(*Proof.*) + (*intros. monadInv H. erewrite <- stick_header_code_size; eauto.*) + (*apply verify_size_size.*) + (*destruct x1; try discriminate. assumption.*) +(*Qed.*) + +(*Lemma verified_schedule_nob_no_header_in_middle:*) + (*forall lbb bb,*) + (*verified_schedule_nob bb = OK lbb ->*) + (*Forall (fun b => header b = nil) (tail lbb).*) +(*Proof.*) + (*intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.*) + (*eapply concat_all_no_header_in_middle. eassumption.*) +(*Qed.*) + +(*Lemma verified_schedule_nob_header:*) + (*forall bb tbb lbb,*) + (*verified_schedule_nob bb = OK (tbb :: lbb) ->*) + (*header bb = header tbb*) + (*/\ Forall (fun b => header b = nil) lbb.*) +(*Proof.*) + (*intros. split.*) + (*- monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.*) + (*simpl. reflexivity.*) + (*- apply verified_schedule_nob_no_header_in_middle in H. assumption.*) +(*Qed.*) + + +(*Definition verified_schedule (bb : bblock) : res (list bblock) :=*) + (*verified_schedule_nob bb.*) +(* TODO Remove? + match exit bb with + | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *) + | _ => verified_schedule_nob bb + end.*) + +(*Lemma verified_schedule_size:*) + (*forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.*) +(*Proof.*) + (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) + (*all: try (apply verified_schedule_nob_size; auto; fail).*) + (*inv H. simpl. omega.*) +(*Qed.*) + +(*Lemma verified_schedule_no_header_in_middle:*) + (*forall lbb bb,*) + (*verified_schedule bb = OK lbb ->*) + (*Forall (fun b => header b = nil) (tail lbb).*) +(*Proof.*) + (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) + (*all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail).*) + (*inv H. simpl. auto.*) +(*Qed.*) + +(*Lemma verified_schedule_header:*) + (*forall bb tbb lbb,*) + (*verified_schedule bb = OK (tbb :: lbb) ->*) + (*header bb = header tbb*) + (*/\ Forall (fun b => header b = nil) lbb.*) +(*Proof.*) + (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) + (*all: try (eapply verified_schedule_nob_header; eauto; fail).*) + (*inv H. split; simpl; auto.*) +(*Qed.*) + + +(*Lemma verified_schedule_nob_correct:*) + (*forall ge f bb lbb,*) + (*verified_schedule_nob bb = OK lbb ->*) + (*exists tbb,*) + (*is_concat tbb lbb*) + (*/\ bblock_simu ge f bb tbb.*) +(*Proof.*) + (*intros. monadInv H.*) + (*exploit stick_header_code_concat_all; eauto.*) + (*intros (tbb & CONC & STH).*) + (*exists tbb. split; auto. constructor; auto.*) + (*rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto.*) + (*eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2.*) + (*destruct (bblock_simub _ _); auto; try discriminate.*) +(*Qed.*) + +(*Theorem verified_schedule_correct:*) + (*forall ge f bb lbb,*) + (*verified_schedule bb = OK lbb ->*) + (*exists tbb,*) + (*is_concat tbb lbb*) + (*/\ bblock_simu ge f bb tbb.*) +(*Proof.*) + (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) + (*all: try (eapply verified_schedule_nob_correct; eauto; fail).*) + (*inv H. eexists. split; simpl; auto. constructor; auto. simpl; auto. constructor; auto.*) +(*Qed.*) + +(*Lemma verified_schedule_builtin_idem:*) + (*forall bb ef args res lbb,*) + (*exit bb = Some (PExpand (Pbuiltin ef args res)) ->*) + (*verified_schedule bb = OK lbb ->*) + (*lbb = bb :: nil.*) +(*Proof.*) + (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*) +(*Qed.*) + + +(*Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=*) + (*match lbb with*) + (*| nil => OK nil*) + (*| (cons bb lbb) =>*) + (*do tlbb <- transf_blocks lbb;*) + (*do tbb <- verified_schedule bb;*) + (*OK (tbb ++ tlbb)*) + (*end.*) + +(*Definition transl_function (f: function) : res function :=*) + (*do lb <- transf_blocks (fn_blocks f); *) + (*OK (mkfunction (fn_sig f) lb).*) + +(*Definition transf_function (f: function) : res function :=*) + (*do tf <- transl_function f;*) + (*if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))*) + (*then Error (msg "code size exceeded")*) + (*else OK tf.*) + +(*Definition transf_fundef (f: fundef) : res fundef :=*) + (*transf_partial_fundef transf_function f.*) + +(*Definition transf_program (p: program) : res program :=*) + (*transform_partial_program transf_fundef p.*) -- cgit