another start for Asmblockgen

1 files changed, 52 insertions, 131 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 1dc7ca12..fc07bbb9 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -199,132 +199,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 iar: Type :=*)
-  (*| IArithP (i: arith_p)*)
-  (*| IArithPP (i: arith_pp)*)
-  (*| IArithRR0 (i: arith_rr0).*)
-
-(*Coercion IArithP: arith_p >-> iar.*)
-(*Coercion IArithPP: arith_pp >-> iar.*)
-(*Definition larith := list iar.*)
-
-(*Fixpoint extract_larith_p (l: larith) :=*)
-  (*match l with*)
-  (*| nil => nil*)
-  (*| IArithP i :: l' => i :: extract_larith_p l'*)
-  (*| _ => nil*)
-  (*end.*)
-
-(*Fixpoint extract_larith_pp (l: larith) :=*)
-  (*match l with*)
-  (*| nil => nil*)
-  (*| IArithPP i :: l' => i :: extract_larith_pp l'*)
-  (*| _ => nil*)
-  (*end.*)
-
-(*Fixpoint larith_p_to_larith (l: list arith_p): larith :=*)
-  (*match l with*)
-  (*| nil => nil*)
-  (*| ar :: l' => IArithP ar :: (larith_p_to_larith l')*)
-  (*end.*)
-
-(*Fixpoint larith_pp_to_larith (l: list arith_pp): larith :=*)
-  (*match l with*)
-  (*| nil => nil*)
-  (*| ar :: l' => IArithPP ar :: (larith_pp_to_larith l')*)
-  (*end.*)
-
-(*Coercion PArithP: arith_p >-> Funclass.*)
-(*Coercion PArithPP: arith_pp >-> Funclass.*)
-(*Coercion PArithRR0: arith_rr0 >-> Funclass.*)
-
-(*Definition bcode := list basic.*)
-(*Definition larith := list ar_instruction.*)
-(*Definition larith_p := list arith_p.*)
-(*Definition larith_pp := list arith_pp.*)
-(*Definition larith_rr0 := list arith_rr0.*)
-
-(*Coercion PBasic:    basic >-> instruction.*)
-(*Coercion PControl:  control >-> instruction.*)
-(*Coercion PArith:    ar_instruction >-> basic.*)
-
-Inductive basic : Type :=
-  | I_BI (i: basic)
-  | I_Arith (i: ar_instruction)
-  | I_ArithP (i : arith_p)
-  | I_ArithPP (i : arith_pp)
-  | I_ArithRR0 (i : arith_rr0).
-
-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 code := list instruction.*)
-
-(*Coercion PArith: ar_instruction >-> basic.*)
-(*Coercion I_bi: bcode >-> code.*)
-(*Coercion I_larith: larith >-> code.*)
-(*Coercion I_larith_p: larith_p >-> code.*)
-(*Coercion I_larith_pp: larith_pp >-> code.*)
-(*Coercion I_larith_rr0: larith_rr0 >-> code.*)
-
-(*Fixpoint extract_larith (c: code) :=*)
-  (*match c with*)
-  (*| nil => nil*)
-  (*| PArith i :: l' => i :: extract_larith l'*)
-  (*| _ => nil*)
-  (*end.*)
-
-(*Fixpoint extract_larith_p (c: code) :=*)
-  (*match c with*)
-  (*| I_larith_p i :: l => i :: extract_larith_p l*)
-  (*| _ => nil*)
-  (*end.*)
-
-(*Fixpoint extract_arith_pp (ar: arith_pp) :=*)
-  (*match ar with*)
-  (*| Pmovk i  => i :: extract_larith_pp l*)
-  (*| _ => nil*)
-  (*end.*)
 
 Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
-    List.fold_right (
-      fun np k => (I_ArithPP (Pmovk sz (fst np) (snd np))) :: 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 => I_ArithP (Pmovz sz 0 0) :: k
-  | (n1, p1) :: l => I_ArithP (Pmovz sz n1 p1) :: 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 => I_ArithP (Pmovn sz 0 0) :: k
-  | (n1, p1) :: l => I_ArithP (Pmovn sz n1 p1) :: 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 :=
@@ -337,12 +236,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 I_ArithRR0 (Porrimm W (Int.unsigned n)) :: 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 I_ArithRR0 (Porrimm X (Int64.unsigned n)) :: 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)].
@@ -405,7 +304,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
@@ -417,14 +316,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
@@ -432,13 +331,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 => 
       match c with
       | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
-      | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil
+      | i :: c => {| header := hd; body := ((i :: c) ++ extract_basic ctl); exit := None |} :: nil
       end
   | Some (PExpand (Pbuiltin ef args res)) =>
       match c with
@@ -449,21 +350,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... *)