diff options
Diffstat (limited to 'aarch64/Asmblockgen.v')
-rw-r--r-- | aarch64/Asmblockgen.v | 1252 |
1 files changed, 1252 insertions, 0 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v new file mode 100644 index 00000000..acb5a1e6 --- /dev/null +++ b/aarch64/Asmblockgen.v @@ -0,0 +1,1252 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Léo Gourdin UGA, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** * Translation from Machblock to AArch64 assembly block language (Asmblock) + Inspired from the Mach->Asm pass of original Leroy's backend, but adapted to the block structure like the KVX backend. *) + +Require Import Recdef Coqlib Zwf Zbits. +Require Import Errors AST Integers Floats Op. +Require Import Locations Machblock Asm Asmblock. + +Local Open Scope string_scope. +Local Open Scope list_scope. +Local Open Scope error_monad_scope. + +(** Extracting integer or float registers. *) + +Definition ireg_of (r: mreg) : res ireg := + match preg_of r with + | IR irs => match irs with + | RR1 mr => OK mr + | _ => Error(msg "Asmgenblock.ireg_of") + end + | _ => Error(msg "Asmgenblock.iregsp_of") + end. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. + +(** Recognition of immediate arguments for logical integer operations.*) + +(** Valid immediate arguments are repetitions of a bit pattern [B] + of length [e] = 2, 4, 8, 16, 32 or 64. + The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*] + but must not be all zeros or all ones. *) + +(** The following automaton recognizes [0*1*0*|1*0*1*]. +<< + 0 1 0 + / \ / \ / \ + \ / \ / \ / + -0--> [B] --1--> [D] --0--> [F] + / + [A] + \ + -1--> [C] --0--> [E] --1--> [G] + / \ / \ / \ + \ / \ / \ / + 1 0 1 +>> +*) + +Module Automaton. + +Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad. + +Definition start := SA. + +Definition next (s: state) (b: bool) := + match s, b with + | SA,false => SB | SA,true => SC + | SB,false => SB | SB,true => SD + | SC,false => SE | SC,true => SC + | SD,false => SF | SD,true => SD + | SE,false => SE | SE,true => SG + | SF,false => SF | SF,true => Sbad + | SG,false => Sbad | SG,true => SG + | Sbad,_ => Sbad + end. + +Definition accepting (s: state) := + match s with + | SA | SB | SC | SD | SE | SF | SG => true + | Sbad => false + end. + +Fixpoint run (len: nat) (s: state) (x: Z) : bool := + match len with + | Datatypes.O => accepting s + | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x) + end. + +End Automaton. + +(** The following function determines the candidate length [e], + ensuring that [x] is a repetition [BB...B] + of a bit pattern [B] of length [e]. *) + +Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat := + (** [test n] checks that the low [2n] bits of [x] are of the + form [BB], that is, two occurrences of the same [n] bits *) + let test (n: Z) : bool := + Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in + (** If [test n] fails, we know that the candidate length [e] is + at least [2n]. Hence we test with decreasing values of [n]: + 32, 16, 8, 4, 2. *) + if sixtyfour && negb (test 32) then 64%nat + else if negb (test 16) then 32%nat + else if negb (test 8) then 16%nat + else if negb (test 4) then 8%nat + else if negb (test 2) then 4%nat + else 2%nat. + +(** A valid logical immediate is +- neither [0] nor [-1]; +- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e] +- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*]. +*) + +Definition is_logical_imm32 (x: int) : bool := + negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) && + Automaton.run (logical_imm_length (Int.unsigned x) false) + Automaton.start (Int.unsigned x). + +Definition is_logical_imm64 (x: int64) : bool := + negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) && + Automaton.run (logical_imm_length (Int64.unsigned x) true) + Automaton.start (Int64.unsigned x). + +(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *) + +Definition is_arith_imm32 (x: int) : bool := + Int.eq x (Int.zero_ext 12 x) + || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)). + +Definition is_arith_imm64 (x: int64) : bool := + Int64.eq x (Int64.zero_ext 12 x) + || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)). + +Definition bcode := list basic. + +Program Definition single_basic (bi: basic): bblock := + {| header := nil; body:= bi::nil; exit := None |}. + +(* insert [bi] at the head of [k] *) +Program Definition insert_basic (bi: basic) (k:bblocks): bblocks := + match k with + | bb::k' => + match bb.(header) with + | nil => {| header := nil; body := bi :: (body bb); exit := exit bb |}::k' + | _ => (single_basic bi)::k + end + | _ => (single_basic bi)::k + end. + +Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity). + +(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *) +(** Alignment check for symbols *) +Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). +Notation "a @@ b" := (app a b) (at level 49, right associativity). + +(* The pop_bc and push_bc functions are used to adapt the output of some definitions + in bblocks format and avoid some redefinitions. *) + +(* pop_bc takes the body of the first bblock in the list if it does not have a header. *) +Definition pop_bc (k: bblocks): bcode := + match k with + | bb :: k' => match bb.(header) with + | nil => (body bb) + | _ => nil + end + | _ => nil + end. + +(* push_bc tries to overwrite code in the first bblock if it does not have a header, + otherwise, a new bblock is created and appended to the list. *) +Program Definition push_bc (bc: bcode) (k:bblocks): bblocks := + match bc with + | bi :: bc' => match k with + | bb :: k' => match bb.(header) with + | nil => {| header := nil; body := bc; exit := exit bb |} :: k' + | _ => {| header := nil; body := bc; exit := None |} :: k + end + | _ => {| header := nil; body := bc; exit := None |} :: nil + end + | nil => k + end. +Next Obligation. + simpl; auto. +Qed. +Next Obligation. + simpl; auto. +Qed. +Next Obligation. + simpl; auto. +Qed. + +Parameter symbol_is_aligned : ident -> Z -> bool. +(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) + +(***************************************************************************************) + +(** Decompose integer literals into 16-bit fragments *) + +Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) := + match N with + | Datatypes.O => nil + | Datatypes.S N => + let frag := Zzero_ext 16 (Z.shiftr n p) in + if Z.eqb frag 0 then + decompose_int N n (p + 16) + else + (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16) + end. + +Definition negate_decomposition (l: list (Z * Z)) := + List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l. + +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) rd rd ::bi k) k l. + +Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode := + match l with + | 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 => 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 := + 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 + if Nat.leb (List.length dz) (List.length dn) + then loadimm_z sz rd dz k + else loadimm_n sz rd dn k. + +Definition loadimm32 (rd: ireg) (n: int) (k: bcode) : bcode := + if is_logical_imm32 n + 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 Porrimm X (Int64.unsigned n) rd XZR ::bi k + else loadimm X rd (Int64.unsigned n) k. + +Definition offset_representable (sz: Z) (ofs: int64) : bool := + let isz := Int64.repr sz in + (** either unscaled 9-bit signed *) + Int64.eq ofs (Int64.sign_ext 9 ofs) || + (** or scaled 12-bit unsigned *) + (Int64.eq (Int64.modu ofs isz) Int64.zero + && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))). + +Definition indexed_memory_access_bc (insn: addressing -> basic) + (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bcode) : bcode := + let ofs := Ptrofs.to_int64 ofs in + if offset_representable sz ofs + then insn (ADimm base ofs) :: k + else loadimm64 X16 ofs (insn (ADreg base X16) :: k). + +Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := + match ty, preg_of dst with + | Tint, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd_a rd) 8 base ofs k) + | _, _ => Error (msg "Asmgen.loadind") + end. + +Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) := + match ty, preg_of src with + | Tint, IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrd_a rd) 8 base ofs k) + | _, _ => Error (msg "Asmgen.storeind") + end. + +Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode := + indexed_memory_access_bc (PLd_rd_a Pldrx dst) 8 base ofs k. + +Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode := + indexed_memory_access_bc (PSt_rs_a Pstrx src) 8 base ofs k. + +(** Function epilogue *) + +Definition make_epilogue (f: Machblock.function) : bcode := + loadptr_bc XSP f.(fn_retaddr_ofs) RA + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs)::nil). + +(** Add immediate *) + +Definition addimm_aux (insn: Z -> arith_pp) + (rd r1: iregsp) (n: Z) (k: bcode) := + let nlo := Zzero_ext 12 n in + let nhi := n - nlo in + if Z.eqb nhi 0 then + insn nlo rd r1 ::bi k + else if Z.eqb nlo 0 then + insn nhi rd r1 ::bi k + else + insn nhi rd r1 ::bi insn nlo rd rd ::bi k. + +Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode := + let m := Int.neg n in + if Int.eq n (Int.zero_ext 24 n) then + addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k + else if Int.eq m (Int.zero_ext 24 m) then + addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k + else if Int.lt n Int.zero then + loadimm32 X16 m (Psub W SOnone rd r1 X16 ::bi k) + else + loadimm32 X16 n (Padd W SOnone rd r1 X16 ::bi k). + +Definition addimm64 (rd r1: iregsp) (n: int64) (k: bcode) : bcode := + let m := Int64.neg n in + if Int64.eq n (Int64.zero_ext 24 n) then + addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k + else if Int64.eq m (Int64.zero_ext 24 m) then + addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k + else if Int64.lt n Int64.zero then + loadimm64 X16 m (Psubext (EOuxtx Int.zero) rd r1 X16 ::bi k) + else + loadimm64 X16 n (Paddext (EOuxtx Int.zero) rd r1 X16 ::bi k). + +(** Logical immediate *) + +Definition logicalimm32 + (insn1: Z -> arith_rr0) + (insn2: shift_op -> arith_rr0r) + (rd r1: ireg) (n: int) (k: bcode) : bcode := + if is_logical_imm32 n + then insn1 (Int.unsigned n) rd r1 ::bi k + else loadimm32 X16 n (insn2 SOnone rd r1 X16 ::bi k). + +Definition logicalimm64 + (insn1: Z -> arith_rr0) + (insn2: shift_op -> arith_rr0r) + (rd r1: ireg) (n: int64) (k: bcode) : bcode := + if is_logical_imm64 n + then insn1 (Int64.unsigned n) rd r1 ::bi k + else loadimm64 X16 n (insn2 SOnone rd r1 X16 ::bi k). + +(** Sign- or zero-extended arithmetic *) + +Definition transl_extension (ex: extension) (a: int) : extend_op := + match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end. + +Definition move_extended_base + (rd: ireg) (r1: ireg) (ex: extension) (k: bcode) : bcode := + match ex with + | Xsgn32 => Pcvtsw2x rd r1 ::bi k + | Xuns32 => Pcvtuw2x rd r1 ::bi k + end. + +Definition move_extended + (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: bcode) : bcode := + if Int.eq a Int.zero then + move_extended_base rd r1 ex k + else + move_extended_base rd r1 ex (Padd X (SOlsl a) rd XZR rd ::bi k). + +Definition arith_extended + (insnX: extend_op -> arith_ppp) + (insnS: shift_op -> arith_rr0r) + (rd r1 r2: ireg) (ex: extension) (a: int) (k: bcode) : bcode := + if Int.ltu a (Int.repr 5) then + insnX (transl_extension ex a) rd r1 r2 ::bi k + else + move_extended_base X16 r2 ex (insnS (SOlsl a) rd r1 X16 ::bi k). + +(** Extended right shift *) + +Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := + if Int.eq n Int.zero then + Pmov rd r1 ::bi k + else + Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi + Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi + Porr W (SOasr n) rd XZR X16 ::bi k. + +Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode := + if Int.eq n Int.zero then + Pmov rd r1 ::bi k + else + Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi + Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi + Porr X (SOasr n) rd XZR X16 ::bi k. + +(** Load the address [id + ofs] in [rd] *) + +Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: bcode) : bcode := + if Archi.pic_code tt then + if Ptrofs.eq ofs Ptrofs.zero then + Ploadsymbol rd id ::bi k + else + Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k + else + Padrp id ofs rd ::bi Paddadr id ofs rd rd ::bi k. + +(** Translate a shifted operand *) + +Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op := + match s with + | Slsl => SOlsl a + | Slsr => SOlsr a + | Sasr => SOasr a + | Sror => SOror a + end. + +(** Translation of a condition. Prepends to [k] the instructions + that evaluate the condition and leave its boolean result in one of + the bits of the condition register. The bit in question is + determined by the [crbit_for_cond] function. *) + +Definition transl_cond + (cond: condition) (args: list mreg) (k: bcode) := + match cond, args with + | (Ccomp c | Ccompu c), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp W SOnone r1 r2 ::bi k) + | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp W (transl_shift s a) r1 r2 ::bi k) + | (Ccompimm c n | Ccompuimm c n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_arith_imm32 n then + Pcmpimm W (Int.unsigned n) r1 ::bi k + else if is_arith_imm32 (Int.neg n) then + Pcmnimm W (Int.unsigned (Int.neg n)) r1 ::bi k + else + loadimm32 X16 n (Pcmp W SOnone r1 X16 ::bi k)) + | (Cmaskzero n | Cmasknotzero n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_logical_imm32 n then + Ptstimm W (Int.unsigned n) r1 ::bi k + else + loadimm32 X16 n (Ptst W SOnone r1 X16 ::bi k)) + | (Ccompl c | Ccomplu c), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp X SOnone r1 r2 ::bi k) + | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp X (transl_shift s a) r1 r2 ::bi k) + | (Ccomplimm c n | Ccompluimm c n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_arith_imm64 n then + Pcmpimm X (Int64.unsigned n) r1 ::bi k + else if is_arith_imm64 (Int64.neg n) then + Pcmnimm X (Int64.unsigned (Int64.neg n)) r1 ::bi k + else + loadimm64 X16 n (Pcmp X SOnone r1 X16 ::bi k)) + | (Cmasklzero n | Cmasklnotzero n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_logical_imm64 n then + Ptstimm X (Int64.unsigned n) r1 ::bi k + else + loadimm64 X16 n (Ptst X SOnone r1 X16 ::bi k)) + | Ccompf cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp D r1 r2 ::bi k) + | Cnotcompf cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp D r1 r2 ::bi k) + | Ccompfzero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 D r1 ::bi k) + | Cnotcompfzero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 D r1 ::bi k) + | Ccompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp S r1 r2 ::bi k) + | Cnotcompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp S r1 r2 ::bi k) + | Ccompfszero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 S r1 ::bi k) + | Cnotcompfszero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 S r1 ::bi k) + | _, _ => + Error(msg "Asmgenblock.transl_cond") + end. + +Definition cond_for_signed_cmp (cmp: comparison) := + match cmp with + | Ceq => TCeq + | Cne => TCne + | Clt => TClt + | Cle => TCle + | Cgt => TCgt + | Cge => TCge + end. + +Definition cond_for_unsigned_cmp (cmp: comparison) := + match cmp with + | Ceq => TCeq + | Cne => TCne + | Clt => TClo + | Cle => TCls + | Cgt => TChi + | Cge => TChs + end. + +Definition cond_for_float_cmp (cmp: comparison) := + match cmp with + | Ceq => TCeq + | Cne => TCne + | Clt => TCmi + | Cle => TCls + | Cgt => TCgt + | Cge => TCge + end. + +Definition cond_for_float_not_cmp (cmp: comparison) := + match cmp with + | Ceq => TCne + | Cne => TCeq + | Clt => TCpl + | Cle => TChi + | Cgt => TCle + | Cge => TClt + end. + +Definition cond_for_cond (cond: condition) := + match cond with + | Ccomp cmp => cond_for_signed_cmp cmp + | Ccompu cmp => cond_for_unsigned_cmp cmp + | Ccompshift cmp s a => cond_for_signed_cmp cmp + | Ccompushift cmp s a => cond_for_unsigned_cmp cmp + | Ccompimm cmp n => cond_for_signed_cmp cmp + | Ccompuimm cmp n => cond_for_unsigned_cmp cmp + | Cmaskzero n => TCeq + | Cmasknotzero n => TCne + | Ccompl cmp => cond_for_signed_cmp cmp + | Ccomplu cmp => cond_for_unsigned_cmp cmp + | Ccomplshift cmp s a => cond_for_signed_cmp cmp + | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp + | Ccomplimm cmp n => cond_for_signed_cmp cmp + | Ccompluimm cmp n => cond_for_unsigned_cmp cmp + | Cmasklzero n => TCeq + | Cmasklnotzero n => TCne + | Ccompf cmp => cond_for_float_cmp cmp + | Cnotcompf cmp => cond_for_float_not_cmp cmp + | Ccompfzero cmp => cond_for_float_cmp cmp + | Cnotcompfzero cmp => cond_for_float_not_cmp cmp + | Ccompfs cmp => cond_for_float_cmp cmp + | Cnotcompfs cmp => cond_for_float_not_cmp cmp + | Ccompfszero cmp => cond_for_float_cmp cmp + | Cnotcompfszero cmp => cond_for_float_not_cmp cmp + end. + +(** Translation of a conditional branch. Prepends to [k] the instructions + that evaluate the condition and ranch to [lbl] if it holds. + We recognize some conditional branches that can be implemented + without setting then testing condition flags. *) + +Definition transl_cond_branch_default + (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) := + do ccode <- transl_cond c args k; + OK(ccode, Pbc (cond_for_cond c) lbl). + +Definition transl_cond_branch + (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) := + match args, c with + | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) => + if Int.eq n Int.zero + then (do r1 <- ireg_of a1; OK (k, Pcbnz W r1 lbl)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) => + if Int.eq n Int.zero + then (do r1 <- ireg_of a1; OK (k, Pcbz W r1 lbl)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) => + if Int64.eq n Int64.zero + then (do r1 <- ireg_of a1; OK (k, Pcbnz X r1 lbl)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) => + if Int64.eq n Int64.zero + then (do r1 <- ireg_of a1; OK (k, Pcbz X r1 lbl)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, Cmaskzero n => + match Int.is_power2 n with + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz W r1 bit lbl) + | None => transl_cond_branch_default c args lbl k + end + | a1 :: nil, Cmasknotzero n => + match Int.is_power2 n with + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz W r1 bit lbl) + | None => transl_cond_branch_default c args lbl k + end + | a1 :: nil, Cmasklzero n => + match Int64.is_power2' n with + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz X r1 bit lbl) + | None => transl_cond_branch_default c args lbl k + end + | a1 :: nil, Cmasklnotzero n => + match Int64.is_power2' n with + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz X r1 bit lbl) + | None => transl_cond_branch_default c args lbl k + end + | _, _ => + transl_cond_branch_default c args lbl k + end. + +(** 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: bcode) := + match op, args with + | Omove, a1 :: nil => + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmov r a ::bi k) + | FR r, FR a => OK (Pfmov r a ::bi k) + | _ , _ => Error(msg "Asmgenblock.Omove") + end + | Ointconst n, nil => + do rd <- ireg_of res; + OK (loadimm32 rd n k) + | Olongconst n, nil => + do rd <- ireg_of res; + OK (loadimm64 rd n k) + | Ofloatconst f, nil => + do rd <- freg_of res; + OK (if Float.eq_dec f Float.zero + then Pfmovi D rd XZR ::bi k + else Pfmovimmd f rd ::bi k) + | Osingleconst f, nil => + do rd <- freg_of res; + OK (if Float32.eq_dec f Float32.zero + then Pfmovi S rd XZR ::bi k + else Pfmovimms f rd ::bi k) + | Oaddrsymbol id ofs, nil => + do rd <- ireg_of res; + OK (loadsymbol rd id ofs k) + | Oaddrstack ofs, nil => + do rd <- ireg_of res; + OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k) + (** 32-bit integer arithmetic *) + | Oshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porr W (transl_shift s a) rd XZR r1 ::bi k) + | Oadd, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd W SOnone rd r1 r2 ::bi k) + | Oaddshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd W (transl_shift s a) rd r1 r2 ::bi k) + | Oaddimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (addimm32 rd rs n k) + | Oneg, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub W SOnone rd XZR r1 ::bi k) + | Onegshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub W (transl_shift s a) rd XZR r1 ::bi k) + | Osub, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub W SOnone rd r1 r2 ::bi k) + | Osubshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub W (transl_shift s a) rd r1 r2 ::bi k) + | Omul, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pmadd W rd rs1 rs2 XZR ::bi k) + | Omuladd, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmadd W rd r2 r3 r1 ::bi k) + | Omulsub, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmsub W rd r2 r3 r1 ::bi k) + | Odiv, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psdiv W rd r1 r2 ::bi k) + | Odivu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pudiv W rd r1 r2 ::bi k) + | Oand, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand W SOnone rd r1 r2 ::bi k) + | Oandshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand W (transl_shift s a) rd r1 r2 ::bi k) + | Oandimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k) + | Oor, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr W SOnone rd r1 r2 ::bi k) + | Oorshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr W (transl_shift s a) rd r1 r2 ::bi k) + | Oorimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k) + | Oxor, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor W SOnone rd r1 r2 ::bi k) + | Oxorshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor W (transl_shift s a) rd r1 r2 ::bi k) + | Oxorimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k) + | Onot, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn W SOnone rd XZR r1 ::bi k) + | Onotshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn W (transl_shift s a) rd XZR r1 ::bi k) + | Obic, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic W SOnone rd r1 r2 ::bi k) + | Obicshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic W (transl_shift s a) rd r1 r2 ::bi k) + | Oorn, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn W SOnone rd r1 r2 ::bi k) + | Oornshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn W (transl_shift s a) rd r1 r2 ::bi k) + | Oeqv, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon W SOnone rd r1 r2 ::bi k) + | Oeqvshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon W (transl_shift s a) rd r1 r2 ::bi k) + | Oshl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plslv W rd r1 r2 ::bi k) + | Oshr, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pasrv W rd r1 r2 ::bi k) + | Oshru, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plsrv W rd r1 r2 ::bi k) + | Oshrximm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (shrx32 rd r1 n k) + | Ozext s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz W Int.zero s rd r1 ::bi k) + | Osext s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz W Int.zero s rd r1 ::bi k) + | Oshlzext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k) + | Oshlsext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k) + | Ozextshr a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfx W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k) + | Osextshr a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfx W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k) + (** 64-bit integer arithmetic *) + | Oshiftl s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porr X (transl_shift s a) rd XZR r1 ::bi k) + | Oextend x a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (move_extended rd r1 x a k) + (* [Omakelong] and [Ohighlong] should not occur *) + | Olowlong, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + assertion (ireg_eq rd r1); + OK (Pcvtx2w rd ::bi k) + | Oaddl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd X SOnone rd r1 r2 ::bi k) + | Oaddlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd X (transl_shift s a) rd r1 r2 ::bi k) + | Oaddlext x a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (arith_extended Paddext (Padd X) rd r1 r2 x a k) + | Oaddlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (addimm64 rd r1 n k) + | Onegl, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub X SOnone rd XZR r1 ::bi k) + | Oneglshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub X (transl_shift s a) rd XZR r1 ::bi k) + | Osubl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub X SOnone rd r1 r2 ::bi k) + | Osublshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub X (transl_shift s a) rd r1 r2 ::bi k) + | Osublext x a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (arith_extended Psubext (Psub X) rd r1 r2 x a k) + | Omull, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmadd X rd r1 r2 XZR ::bi k) + | Omulladd, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmadd X rd r2 r3 r1 ::bi k) + | Omullsub, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmsub X rd r2 r3 r1 ::bi k) + | Omullhs, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psmulh rd r1 r2 ::bi k) + | Omullhu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pumulh rd r1 r2 ::bi k) + | Odivl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psdiv X rd r1 r2 ::bi k) + | Odivlu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pudiv X rd r1 r2 ::bi k) + | Oandl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand X SOnone rd r1 r2 ::bi k) + | Oandlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand X (transl_shift s a) rd r1 r2 ::bi k) + | Oandlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k) + | Oorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr X SOnone rd r1 r2 ::bi k) + | Oorlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr X (transl_shift s a) rd r1 r2 ::bi k) + | Oorlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k) + | Oxorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor X SOnone rd r1 r2 ::bi k) + | Oxorlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor X (transl_shift s a) rd r1 r2 ::bi k) + | Oxorlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k) + | Onotl, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn X SOnone rd XZR r1 ::bi k) + | Onotlshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn X (transl_shift s a) rd XZR r1 ::bi k) + | Obicl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic X SOnone rd r1 r2 ::bi k) + | Obiclshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic X (transl_shift s a) rd r1 r2 ::bi k) + | Oornl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn X SOnone rd r1 r2 ::bi k) + | Oornlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn X (transl_shift s a) rd r1 r2 ::bi k) + | Oeqvl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon X SOnone rd r1 r2 ::bi k) + | Oeqvlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon X (transl_shift s a) rd r1 r2 ::bi k) + | Oshll, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plslv X rd r1 r2 ::bi k) + | Oshrl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pasrv X rd r1 r2 ::bi k) + | Oshrlu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plsrv X rd r1 r2 ::bi k) + | Oshrlximm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (shrx64 rd r1 n k) + | Ozextl s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz X Int.zero s rd r1 ::bi k) + | Osextl s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz X Int.zero s rd r1 ::bi k) + | Oshllzext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k) + | Oshllsext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k) + | Ozextshrl a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfx X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k) + | Osextshrl a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfx X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k) + (** 64-bit floating-point arithmetic *) + | Onegf, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfneg D rd rs ::bi k) + | Oabsf, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfabs D rd rs ::bi k) + | Oaddf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfadd D rd rs1 rs2 ::bi k) + | Osubf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfsub D rd rs1 rs2 ::bi k) + | Omulf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmul D rd rs1 rs2 ::bi k) + | Odivf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfdiv D rd rs1 rs2 ::bi k) + (** 32-bit floating-point arithmetic *) + | Onegfs, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfneg S rd rs ::bi k) + | Oabsfs, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfabs S rd rs ::bi k) + | Oaddfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfadd S rd rs1 rs2 ::bi k) + | Osubfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfsub S rd rs1 rs2 ::bi k) + | Omulfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmul S rd rs1 rs2 ::bi k) + | Odivfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfdiv S rd rs1 rs2 ::bi k) + | Osingleoffloat, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfcvtsd rd rs ::bi k) + | Ofloatofsingle, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfcvtds rd rs ::bi k) + (** Conversions between int and float *) + | Ointoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs W D rd rs ::bi k) + | Ointuoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu W D rd rs ::bi k) + | Ofloatofint, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf D W rd rs ::bi k) + | Ofloatofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf D W rd rs ::bi k) + | Ointofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs W S rd rs ::bi k) + | Ointuofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu W S rd rs ::bi k) + | Osingleofint, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf S W rd rs ::bi k) + | Osingleofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf S W rd rs ::bi k) + | Olongoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs X D rd rs ::bi k) + | Olonguoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu X D rd rs ::bi k) + | Ofloatoflong, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf D X rd rs ::bi k) + | Ofloatoflongu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf D X rd rs ::bi k) + | Olongofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs X S rd rs ::bi k) + | Olonguofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu X S rd rs ::bi k) + | Osingleoflong, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf S X rd rs ::bi k) + | Osingleoflongu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf S X rd rs ::bi k) + (** Boolean tests *) + | Ocmp c, _ => + do rd <- ireg_of res; + transl_cond c args (Pcset rd (cond_for_cond c) ::bi k) + (** Conditional move *) + | Osel cmp ty, a1 :: a2 :: args => + match preg_of res with + | IR r => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k) + | FR r => + do r1 <- freg_of a1; do r2 <- freg_of a2; + transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k) + | _ => + Error(msg "Asmgenblock.Osel") + end + | _, _ => Error(msg "Asmgenblock.transl_op") + end. + +(** Translation of addressing modes *) + +Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) + (insn: Asm.addressing -> basic) (k: bcode) : res bcode := + match addr, args with + | Aindexed ofs, a1 :: nil => + do r1 <- ireg_of a1; + if offset_representable sz ofs then + OK (insn (ADimm r1 ofs) ::bi k) + else + OK (loadimm64 X16 ofs (insn (ADreg r1 X16) ::bi k)) + | Aindexed2, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (insn (ADreg r1 r2) ::bi k) + | Aindexed2shift a, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + if Int.eq a Int.zero then + OK (insn (ADreg r1 r2) ::bi k) + else if Int.eq (Int.shl Int.one a) (Int.repr sz) then + OK (insn (ADlsl r1 r2 a) ::bi k) + else + OK (Padd X (SOlsl a) X16 r1 r2 ::bi insn (ADimm X16 Int64.zero) ::bi k) + | Aindexed2ext x a, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then + OK (insn (match x with Xsgn32 => ADsxt r1 r2 a + | Xuns32 => ADuxt r1 r2 a end) ::bi k) + else + OK (arith_extended Paddext (Padd X) X16 r1 r2 x a + (insn (ADimm X16 Int64.zero) ::bi k)) + | Aglobal id ofs, nil => + assertion (negb (Archi.pic_code tt)); + if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz + then OK (Padrp id ofs X16 ::bi insn (ADadr X16 id ofs) ::bi k) + else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) ::bi k)) + | Ainstack ofs, nil => + let ofs := Ptrofs.to_int64 ofs in + if offset_representable sz ofs then + OK (insn (ADimm XSP ofs) ::bi k) + else + OK (loadimm64 X16 ofs (insn (ADreg XSP X16) ::bi k)) + | _, _ => + Error(msg "Asmgen.transl_addressing") + end. + +(** Translation of loads and stores *) + +Definition transl_load (chunk: memory_chunk) (addr: Op.addressing) + (args: list mreg) (dst: mreg) (k: bcode) : res bcode := + match chunk with + | Mint8unsigned => + do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrb W) rd) k + | Mint8signed => + do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrsb W) rd) k + | Mint16unsigned => + do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrh W) rd) k + | Mint16signed => + do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrsh W) rd) k + | Mint32 => + do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw rd) k + | Mint64 => + do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx rd) k + | Mfloat32 => + do rd <- freg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrs rd) k + | Mfloat64 => + do rd <- freg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrd rd) k + | Many32 => + do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw_a rd) k + | Many64 => + do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx_a rd) k + end. + +Definition transl_store (chunk: memory_chunk) (addr: Op.addressing) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + match chunk with + | Mint8unsigned | Mint8signed => + do r1 <- ireg_of src; transl_addressing 1 addr args (PSt_rs_a Pstrb r1) k + | Mint16unsigned | Mint16signed => + do r1 <- ireg_of src; transl_addressing 2 addr args (PSt_rs_a Pstrh r1) k + | Mint32 => + do r1 <- ireg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrw r1) k + | Mint64 => + do r1 <- ireg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrx r1) k + | Mfloat32 => + do r1 <- freg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrs r1) k + | Mfloat64 => + do r1 <- freg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrd r1) k + | Many32 => + do r1 <- ireg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrw_a r1) k + | Many64 => + do r1 <- ireg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrx_a r1) k + end. + +(** Translation of a Machblock instruction. *) + +Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) + (ep: bool) (k: bcode) := + match i with + | MBgetstack ofs ty dst => + loadind XSP ofs ty dst k + | MBsetstack src ofs ty => + storeind src XSP ofs ty k + | MBgetparam ofs ty dst => + do c <- loadind X29 ofs ty dst k; + OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c) + | MBop op args res => + transl_op op args res k + | MBload t chunk addr args dst => + match t with + | TRAP => transl_load chunk addr args dst k + | NOTRAP => Error(msg "Asmgenblock.transl_instr_basic: NOTRAP load not supported in aarch64.") + end + | MBstore chunk addr args src => + transl_store chunk addr args src k + end. + +(** Translation of a code sequence *) + +Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool := + match i with + (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)*) + | MBsetstack src ofs ty => before + | MBgetparam ofs ty dst => negb (mreg_eq dst R29) + | MBop op args res => before && negb (mreg_eq res R29) + (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)*) + | _ => false + end. + +Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := + match il with + | nil => OK (nil) + | i1 :: il' => + do k1 <- transl_basic_code f il' (it1_is_parent it1p i1); + transl_instr_basic f i1 it1p k1 + end. + +Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks := + match ex with + | None => + match bdy with + | nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil + | _ => {| header := ll; body:= bdy; exit := None |} :: nil + end + | _ => + match bdy with + | nil => {| header := ll; body:= nil; exit := ex |} :: nil + | _ => {| header := ll; body:= bdy; exit := ex |} :: nil + end + end. +Next Obligation. + induction bdy. congruence. + simpl. auto. +Qed. +Next Obligation. + destruct ex. simpl. auto. + congruence. +Qed. +Next Obligation. + induction bdy. congruence. + simpl. auto. +Qed. + +Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) := + match ctl with + | MBcall sig (inl r) => do r1 <- ireg_of r; + OK (nil, PCtlFlow (Pblr r1 sig)) + | MBcall sig (inr symb) => OK (nil, PCtlFlow (Pbl symb sig)) + | MBtailcall sig (inr symb) => OK(make_epilogue f, PCtlFlow (Pbs symb sig)) + | MBtailcall sig (inl r) => do r1 <- ireg_of r; + OK (make_epilogue f, PCtlFlow (Pbr r1 sig)) + | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of res)) + | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl)) + | MBcond cond args lbl => do (bc, c) <- transl_cond_branch cond args lbl nil; OK (bc, PCtlFlow c) + | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA)) + | MBjumptable arg tbl => do r <- ireg_of arg; + OK (nil, PCtlFlow (Pbtbl r tbl)) + end. + +Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : res (bcode*option control) := + match ext with + Some ctl => do (b,c) <- transl_control f ctl; OK (b, Some c) + | None => OK (nil, None) + end. + +Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := + do (bdy2, ex) <- transl_exit f fb.(Machblock.exit); + do bdy1 <- transl_basic_code f fb.(Machblock.body) ep; + OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex) + . + +Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) := + 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 +. + +Program Definition make_prologue (f: Machblock.function) (k:bblocks) := + {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi + ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil; + exit := None |} :: k. + +Definition transl_function (f: Machblock.function) : res Asmblock.function := + do lb <- transl_blocks f f.(Machblock.fn_code) true; + OK (mkfunction f.(Machblock.fn_sig) + (make_prologue f lb)). + +Definition transf_function (f: Machblock.function) : res Asmblock.function := + do tf <- transl_function f; + if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks)) + then Error (msg "code size exceeded") + else OK tf. + +Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Machblock.program) : res Asmblock.program := + transform_partial_program transf_fundef p. + |