diff options
-rw-r--r-- | aarch64/Asmblockgen.v | 229 |
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) . |