diff options
-rw-r--r-- | aarch64/Asmblock.v | 11 | ||||
-rw-r--r-- | aarch64/PostpassScheduling.v | 107 |
2 files changed, 47 insertions, 71 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index ddd58223..27292234 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -7,6 +7,7 @@ (* Xavier Leroy INRIA Paris-Rocquencourt *) (* 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 *) @@ -373,6 +374,16 @@ Definition length_opt {A} (o: option A) : nat := | None => 0 end. +Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; cbn. assumption. +Defined. + +Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; cbn. assumption. +Defined. + (* This notion of size induces the notion of "valid" code address given by [find_bblock] The result is in Z to be compatible with operations on PC. diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index 485b297b..eeca4e54 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.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 *) @@ -275,14 +276,6 @@ Inductive is_concat : bblock -> list bblock -> Prop := (*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).*) @@ -338,65 +331,37 @@ Program Definition make_bblock_from_basics lb := | 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") +Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : res bblock := + match oc with + | None => make_bblock_from_basics lb + | Some c => OK {| header := nil; body := lb; exit := Some c |} end. Next Obligation. + (* TODO *) 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 do_schedule (bb: bblock) : res bblock := + if (Z.eqb (size bb) 1) then OK (bb) + else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. (* TODO Something here *) +(* TODO to remove ? *) (*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';*) +Definition verified_schedule (bb : bblock) : res bblock := + let bb' := no_header bb in + (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *) + do lb <- 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 schedcheck <- verify_schedule bb' tbb;*) (* TODO Keep this one *) (*do parcheck <- verify_par res;*) - (*OK res.*) + OK (stick_header (header bb) lb). (*Lemma verified_schedule_nob_size:*) (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*) @@ -504,27 +469,27 @@ Qed.*) (*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.*) +Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) := + match lbb with + | nil => OK nil + | 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 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_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_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. -(*Definition transf_program (p: program) : res program :=*) - (*transform_partial_program transf_fundef p.*) +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. |