Merge remote-tracking branch 'origin/aarch64_asmblockgen' into aarch64_block

1 files changed, 52 insertions, 47 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 0e8d30fd..2bab1927 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -201,48 +201,31 @@ Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) :=
 Definition negate_decomposition (l: list (Z * Z)) :=
   List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l.
 
-(* XXX Que faire des rd ici ? inutiles ? *)
-(* XXX Faudra-t-il remplacer arith_pp par un type abstrait ? *)
+(* TODO: Coercions to move in Asmblock ? *)
+Coercion PArithP: arith_p >-> Funclass.
+Coercion PArithPP: arith_pp >-> Funclass.
+Coercion PArithRR0: arith_rr0 >-> Funclass.
+Coercion PArith: ar_instruction >-> basic.
 
-(* XXX Move this in Asmblock.v ? *)
-
-Inductive instruction : Type :=
-  | PBasic    (i: basic)
-  | PControl  (i: control)
-.
-
-Definition code := list instruction.
 Definition bcode := list basic.
 
-Fixpoint extract_basic (c: code) :=
-  match c with
-  | nil => nil
-  | PBasic i :: c => i :: (extract_basic c)
-  | PControl i :: c => nil
-  end.
+Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
+(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *)
 
-Fixpoint extract_ctl (c: code) :=
-  match c with
-  | nil => None
-  | PBasic i :: c => extract_ctl c
-  | PControl i :: nil => Some i
-  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
-  end.
 
 Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
-    List.fold_right (
-      fun np k => (PArith (PArithPP (Pmovk sz (fst np) (snd np)) rd rd)) :: k) k l.
+    List.fold_right (fun np k => Pmovk sz (fst np) (snd np) rd rd ::bi k) k l.
 
 Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z))  (k: bcode) : bcode :=
   match l with
-  | nil => PArith (PArithP (Pmovz sz 0 0) rd) :: k
-  | (n1, p1) :: l => PArith (PArithP (Pmovz sz n1 p1) rd) :: loadimm_k sz rd l k
+  | nil => Pmovz sz 0 0 rd ::bi k
+  | (n1, p1) :: l => (Pmovz sz n1 p1 rd) ::bi loadimm_k sz rd l k
   end.
 
 Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
   match l with
-  | nil => PArith (PArithP (Pmovn sz 0 0) rd) :: k
-  | (n1, p1) :: l => PArith (PArithP (Pmovn sz n1 p1) rd) :: loadimm_k sz rd (negate_decomposition l) k
+  | nil => Pmovn sz 0 0 rd ::bi k
+  | (n1, p1) :: l => Pmovn sz n1 p1 rd ::bi loadimm_k sz rd (negate_decomposition l) k
   end.
 
 Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode :=
@@ -255,12 +238,12 @@ Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode :=
 
 Definition loadimm32 (rd: ireg) (n: int) (k: bcode) : bcode :=
   if is_logical_imm32 n
-  then PArith (PArithRR0 (Porrimm W (Int.unsigned n)) rd XZR) :: k
+  then Porrimm W (Int.unsigned n) rd XZR ::bi k
   else loadimm W rd (Int.unsigned n) k.
 
 Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
   if is_logical_imm64 n
-  then PArith (PArithRR0 (Porrimm X (Int64.unsigned n)) rd XZR) :: k
+  then Porrimm X (Int64.unsigned n) rd XZR ::bi k
   else loadimm X rd (Int64.unsigned n) k.
 
 (** Translation of the arithmetic operation [r <- op(args)].
@@ -323,7 +306,7 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
 
 (** This is an equivalent definition in continuation-passing style
   that runs in constant stack space. *)
-
+(*
 Fixpoint transl_code_rec (f: Machblock.function) (il: list Machblock.basic_inst)
                          (it1p: bool) (k: bcode -> res bcode) :=
   match il with
@@ -335,14 +318,14 @@ Fixpoint transl_code_rec (f: Machblock.function) (il: list Machblock.basic_inst)
 
 Definition transl_code' (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
   transl_code_rec f il it1p (fun c => OK c).
+*)
 
-
-Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
+Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):=
   match il with
   | nil => OK nil
   | i1 :: il' =>
-      do k <- transl_basic_code f il' (it1_is_parent it1p i1);
-      transl_instr_basic f i1 it1p k
+      do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k;
+      transl_instr_basic f i1 it1p k1
   end.
 
 (** Translation of a whole function.  Note that we must check
@@ -350,13 +333,15 @@ Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_ins
   otherwise the offset part of the [PC] code pointer could wrap
   around, leading to incorrect executions. *)
 
+(* NB Sylvain: this issue with PExpand seems specific to kvx -- and not necessary here *)
 (* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
+(*
 Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instruction) :=
   match (extract_ctl ctl) with
   | None => 
       (* XXX Que faire du Pnop ? *)
       match c with
-      | nil => {| header := hd; body := (*Pnop::*)nil; exit := None |} :: nil
+      | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
       | i :: c => {| header := hd; body := ((i :: c) ++ extract_basic ctl); exit := None |} :: nil
       end
   (*| Some (i) =>*)
@@ -368,21 +353,41 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio
   | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil
   end
 .
+*)
 
-Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
-  do c <- transl_basic_code f fb.(Machblock.body) ep;
-  do ctl <- nil; (*transl_instr_control f fb.(Machblock.exit);*)
-  OK (gen_bblocks fb.(Machblock.header) c ctl)
-.
+(* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
+Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control) (k:bblocks): bblocks :=
+  match non_empty_bblockb bdy ex with
+  | true => {| header := ll; body:= bdy; exit := ex |}::k
+  | false => k
+  end.
+Obligation 1.
+  rewrite <- Heq_anonymous. constructor.
+Qed.
+
+Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) :=
+  Error (msg ("not yet implemented")).
+
+Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) (ep: bool) : res (bcode*option control) :=
+  match ext with
+    Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, Some c)
+  | None => OK (nil, None)
+  end.
+
+Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) :=
+  let stub := false in (* TODO: FIXME *) 
+  do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub;
+  do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
+  OK (cons_bblocks fb.(Machblock.header) bdy' ex k) 
+  .
 
-Program Definition transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
+Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
   match lmb with
   | nil => OK nil
   | mb :: lmb => 
-      do lb <- transl_block f mb (if Machblock.header mb then ep else false);
-      do lb' <- transl_blocks f lmb false;
-      OK (lb @@ lb')
-  end
+      do lb <- transl_blocks f lmb false; (* TODO: check [false] here *)
+      transl_block f mb (if Machblock.header mb then ep else false) lb  (* TODO: check this *)
+  end.
   (* OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)*)
 
 (* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *)