[Draft] Flattened levels of binst

1 files changed, 180 insertions, 49 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 1acb3a13..1dc7ca12 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -204,59 +204,130 @@ Definition negate_decomposition (l: list (Z * Z)) :=
 
 (* 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.
+(*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)
+.
 
-Fixpoint extract_larith_pp (l: larith) :=
-  match l with
-  | nil => nil
-  | IArithPP i :: l' => i :: extract_larith_pp l'
-  | _ => nil
-  end.
+Definition code := list instruction.
+Definition bcode := list basic.
 
-Fixpoint larith_p_to_larith (l: list arith_p): larith :=
-  match l with
+Fixpoint extract_basic (c: code) :=
+  match c with
   | nil => nil
-  | ar :: l' => IArithP ar :: (larith_p_to_larith l')
+  | PBasic i :: c => i :: (extract_basic c)
+  | PControl i :: c => nil
   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')
+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: larith) : larith :=
-  larith_pp_to_larith (
+(*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 => Pmovk sz (fst np) (snd np) :: k) (extract_larith_pp k) l).
+      fun np k => (I_ArithPP (Pmovk sz (fst np) (snd np))) :: k) k l.
 
-Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z))  (k: larith) : larith :=
+Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z))  (k: bcode) : bcode :=
   match l with
-  | nil => larith_p_to_larith (Pmovz sz 0 0 :: extract_larith_p k)
-  | (n1, p1) :: l => larith_p_to_larith (Pmovz sz n1 p1 :: extract_larith_p (loadimm_k sz rd l k))
+  | nil => I_ArithP (Pmovz sz 0 0) :: k
+  | (n1, p1) :: l => I_ArithP (Pmovz sz n1 p1) :: loadimm_k sz rd l k
   end.
 
-Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: larith) : larith :=
+Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
   match l with
-  | nil => larith_p_to_larith (Pmovn sz 0 0 :: extract_larith_p k)
-  | (n1, p1) :: l => larith_p_to_larith (Pmovn sz n1 p1 :: extract_larith_p (loadimm_k sz rd (negate_decomposition l) k))
+  | 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
   end.
 
-Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: larith) : larith :=
+Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode :=
   let N := match sz with W => 2%nat | X => 4%nat end in
   let dz := decompose_int N n 0 in
   let dn := decompose_int N (Z.lnot n) 0 in
@@ -264,34 +335,34 @@ Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: larith) : larith :=
   then loadimm_z sz rd dz k
   else loadimm_n sz rd dn k.
 
-Definition loadimm32 (rd: ireg) (n: int) (k: larith) : larith :=
+Definition loadimm32 (rd: ireg) (n: int) (k: bcode) : bcode :=
   if is_logical_imm32 n
-  then IArithRR0 (Porrimm W (Int.unsigned n))
-  else loadimm W (Int.unsigned n) k.
+  then I_ArithRR0 (Porrimm W (Int.unsigned n)) :: k
+  else loadimm W rd (Int.unsigned n) k.
 
-Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code :=
+Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
   if is_logical_imm64 n
-  then Porrimm X rd XZR (Int64.unsigned n) :: k
+  then I_ArithRR0 (Porrimm X (Int64.unsigned n)) :: k
   else loadimm X rd (Int64.unsigned n) k.
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
 Definition transl_op
-              (op: operation) (args: list mreg) (res: mreg) (k: list basic) :=
+              (op: operation) (args: list mreg) (res: mreg) (k: bcode) :=
   match op, args with
   | Ointconst n, nil =>
       do rd <- ireg_of res;
       OK (loadimm32 rd n k)
-  | _ => Error(msg "Not implemented yet")
+  | _, _ => Error(msg "Not implemented yet")
   end.
 
 (** Translation of a Machblock instruction. *)
 
 Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
-                              (ep: bool) (k: list basic) :=
+                              (ep: bool) (k: bcode) :=
   match i with
-  | Mop op args res =>
+  | MBop op args res =>
       transl_op op args res k
   | _ => Error(msg "Not implemented yet")
   (*| MBgetstack ofs ty dst =>*)
@@ -311,17 +382,77 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
       (*transl_store chunk addr args src k*)
   end.
 
+(** Translation of a code sequence *)
+
+(* TODO to remove ? *)
+(*Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=*)
+  (*match i with*)
+  (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP)*)
+  (*| MBsetstack src ofs ty => before*)
+  (*| MBgetparam ofs ty dst => negb (mreg_eq dst MFP)*)
+  (*| MBop op args res => before && negb (mreg_eq res MFP)*)
+  (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP)*)
+  (*| MBstore chunk addr args res => before*)
+  (*end.*)
+
+Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
+  match i with
+  (*| Msetstack src ofs ty => before*)
+  (*| Mgetparam ofs ty dst => negb (mreg_eq dst R29)*)
+  | MBop op args res => before && negb (mreg_eq res R29)
+  | _ => false
+  end.
+
+(** 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
+  | nil => k nil
+  | i1 :: il' =>
+      transl_code_rec f il' (it1_is_parent it1p i1)
+        (fun c1 => do c2 <- transl_instr_basic f i1 it1p c1; k c2)
+  end.
+
+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) :=
   match il with
   | nil => OK nil
   | i1 :: il' =>
-      do k <- transl_basic_code f il' (fp_is_parent it1p i1);
+      do k <- transl_basic_code f il' (it1_is_parent it1p i1);
       transl_instr_basic f i1 it1p k
   end.
 
+(** Translation of a whole function.  Note that we must check
+  that the generated code contains less than [2^64] instructions,
+  otherwise the offset part of the [PC] code pointer could wrap
+  around, leading to incorrect executions. *)
+
+(* 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
+      end
+  | Some (PExpand (Pbuiltin ef args res)) =>
+      match c with
+      | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
+      | _ => {| header := hd; body := c; exit := None |} 
+              :: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
+      end
+  | 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 <- transl_instr_control f fb.(Machblock.exit);
+  do ctl <- nil; (*transl_instr_control f fb.(Machblock.exit);*)
   OK (gen_bblocks fb.(Machblock.header) c ctl)
 .