A more convenient way to handle basic inst

1 files changed, 18 insertions, 99 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 1dc7ca12..0e8d30fd 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -25,6 +25,8 @@ Local Open Scope string_scope.
 Local Open Scope list_scope.
 Local Open Scope error_monad_scope.
 
+Import PArithCoercions.
+
 (** Extracting integer or float registers. *)
 
 Definition ireg_of (r: mreg) : res ireg :=
@@ -204,62 +206,6 @@ 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.*)
-
-(*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)
@@ -283,48 +229,20 @@ Fixpoint extract_ctl (c: code) :=
   | 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.
+      fun np k => (PArith (PArithPP (Pmovk sz (fst np) (snd np)) rd rd)) :: 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 => PArith (PArithP (Pmovz sz 0 0) rd) :: k
+  | (n1, p1) :: l => PArith (PArithP (Pmovz sz n1 p1) rd) :: 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 => 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
   end.
 
 Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode :=
@@ -337,12 +255,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 PArith (PArithRR0 (Porrimm W (Int.unsigned n)) rd XZR) :: 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 PArith (PArithRR0 (Porrimm X (Int64.unsigned n)) rd XZR) :: k
   else loadimm X rd (Int64.unsigned n) k.
 
 (** Translation of the arithmetic operation [r <- op(args)].
@@ -436,16 +354,17 @@ Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_ins
 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
-      | 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
+      | 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) =>*)
+      (*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
 .