Some adaptations on PostpassScheduling for aarch64, and defs in Asmblock

1 files changed, 36 insertions, 71 deletions

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.