From bb3f0926265ef44485d065aa44a91d9932df93bf Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 26 Oct 2020 17:40:30 +0100 Subject: [Draft] Problems with coercions --- aarch64/Asmblockgen.v | 1244 +++++++------------------------------------------ 1 file changed, 166 insertions(+), 1078 deletions(-) diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 66db0f5f..1acb3a13 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -25,116 +25,19 @@ Local Open Scope string_scope. Local Open Scope list_scope. Local Open Scope error_monad_scope. -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). - -(* insert [ctl] at the head of [k] *) -Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks := - {| header := nil; body := nil; exit := Some ctl |}::k. - -Notation "ctl ::c k" := (insert_ctl ctl k) (at level 49, right associativity). - - -(** Alignment check for symbols *) - -Parameter symbol_is_aligned : ident -> Z -> bool. -(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) - -(***************************************************************************************) -(* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *) - -Definition indexed_memory_access (insn: addressing -> basic) - (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks := - let ofs := Ptrofs.to_int64 ofs in - insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *) - - -Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks := - indexed_memory_access (PLoad Pldrx dst) 8 base ofs k. - -Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks := - indexed_memory_access (PStore Pstrx src) 8 base ofs k. - -(** Function epilogue *) - -Definition make_epilogue (f: Machblock.function) (k: bblocks) : bblocks := - (* FIXME - Cannot be used because memcpy destroys X30; - issue being discussed with X. Leroy *) - (* if is_leaf_function f - then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k - else*) loadptr XSP f.(fn_retaddr_ofs) RA - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::b k). - - -Program Definition transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks := - OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *) - -(* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *) -Program Definition make_prologue (f: Machblock.function) (k:bblocks) := - Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b - storeptr RA XSP f.(fn_retaddr_ofs) 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_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) - -Definition transf_program (p: Machblock.program) : res Asmblock.program := - transform_partial_program transf_fundef p. - -(* ORIGINAL aarch64/Asmgen file that needs to be adapted - -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Translation from Mach to AArch64. *) - -Require Import Recdef Coqlib Zwf Zbits. -Require Import Errors AST Integers Floats Op. -Require Import Locations Mach Asm. - -Local Open Scope string_scope. -Local Open Scope list_scope. -Local Open Scope error_monad_scope. - -(** Alignment check for symbols *) - -Parameter symbol_is_aligned : ident -> Z -> bool. -(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) - (** Extracting integer or float registers. *) Definition ireg_of (r: mreg) : res ireg := - match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. + 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 "Asmgen.freg_of") end. + match preg_of r with FR' mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. (** Recognition of immediate arguments for logical integer operations.*) @@ -226,15 +129,59 @@ Definition is_logical_imm64 (x: int64) : bool := 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 *) +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). + +(* insert [ctl] at the head of [k] *) +Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks := + {| header := nil; body := nil; exit := Some ctl |}::k. + +Notation "ctl ::c k" := (insert_ctl ctl k) (at level 49, right associativity). + + +(** Alignment check for symbols *) + +Parameter symbol_is_aligned : ident -> Z -> bool. +(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) + +(***************************************************************************************) +(* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *) + +Definition indexed_memory_access (insn: addressing -> basic) + (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks := + let ofs := Ptrofs.to_int64 ofs in + insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *) + -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 loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks := + indexed_memory_access (PLoad Pldrx dst) 8 base ofs k. + +Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks := + indexed_memory_access (PStore Pstrx src) 8 base ofs k. + +(** Function epilogue *) -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 make_epilogue (f: Machblock.function) (k: bblocks) : bblocks := + (* FIXME + Cannot be used because memcpy destroys X30; + issue being discussed with X. Leroy *) + (* if is_leaf_function f + then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k + else*) loadptr XSP f.(fn_retaddr_ofs) RA + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::b k). (** Decompose integer literals into 16-bit fragments *) @@ -252,22 +199,64 @@ 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. -Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := - List.fold_right (fun np k => Pmovk sz rd (fst np) (snd np) :: k) k l. +(* XXX Que faire des rd ici ? inutiles ? *) +(* XXX Faudra-t-il remplacer arith_pp par un type abstrait ? *) -Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := +(* 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 => Pmovz sz rd 0 0 :: k - | (n1, p1) :: l => Pmovz sz rd n1 p1 :: loadimm_k sz rd l k + | nil => nil + | IArithP i :: l' => i :: extract_larith_p l' + | _ => nil end. -Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := +Fixpoint extract_larith_pp (l: larith) := match l with - | nil => Pmovn sz rd 0 0 :: k - | (n1, p1) :: l => Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k + | nil => nil + | IArithPP i :: l' => i :: extract_larith_pp l' + | _ => nil end. -Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code := +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. + +Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: larith) : larith := + larith_pp_to_larith ( + List.fold_right ( + fun np k => Pmovk sz (fst np) (snd np) :: k) (extract_larith_pp k) l). + +Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: larith) : larith := + 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)) + end. + +Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: larith) : larith := + 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)) + end. + +Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: larith) : larith := 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 @@ -275,991 +264,90 @@ Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code := then loadimm_z sz rd dz k else loadimm_n sz rd dn k. -Definition loadimm32 (rd: ireg) (n: int) (k: code) : code := +Definition loadimm32 (rd: ireg) (n: int) (k: larith) : larith := if is_logical_imm32 n - then Porrimm W rd XZR (Int.unsigned n) :: k - else loadimm W rd (Int.unsigned n) k. + then IArithRR0 (Porrimm W (Int.unsigned n)) + else loadimm W (Int.unsigned n) k. Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code := if is_logical_imm64 n then Porrimm X rd XZR (Int64.unsigned n) :: k else loadimm X rd (Int64.unsigned n) k. -(** Add immediate *) - -Definition addimm_aux (insn: iregsp -> iregsp -> Z -> instruction) - (rd r1: iregsp) (n: Z) (k: code) := - let nlo := Zzero_ext 12 n in - let nhi := n - nlo in - if Z.eqb nhi 0 then - insn rd r1 nlo :: k - else if Z.eqb nlo 0 then - insn rd r1 nhi :: k - else - insn rd r1 nhi :: insn rd rd nlo :: k. - -Definition addimm32 (rd r1: ireg) (n: int) (k: code) : code := - 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 rd r1 X16 SOnone :: k) - else - loadimm32 X16 n (Padd W rd r1 X16 SOnone :: k). - -Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code := - 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 rd r1 X16 (EOuxtx Int.zero) :: k) - else - loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k). - -(** Logical immediate *) - -Definition logicalimm32 - (insn1: ireg -> ireg0 -> Z -> instruction) - (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (rd r1: ireg) (n: int) (k: code) : code := - if is_logical_imm32 n - then insn1 rd r1 (Int.unsigned n) :: k - else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k). - -Definition logicalimm64 - (insn1: ireg -> ireg0 -> Z -> instruction) - (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (rd r1: ireg) (n: int64) (k: code) : code := - if is_logical_imm64 n - then insn1 rd r1 (Int64.unsigned n) :: k - else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: 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: code) : code := - match ex with - | Xsgn32 => Pcvtsw2x rd r1 :: k - | Xuns32 => Pcvtuw2x rd r1 :: k - end. - -Definition move_extended - (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code := - if Int.eq a Int.zero then - move_extended_base rd r1 ex k - else - move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k). - -Definition arith_extended - (insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction) - (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code := - if Int.ltu a (Int.repr 5) then - insnX rd r1 r2 (transl_extension ex a) :: k - else - move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k). - -(** Extended right shift *) - -Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code := - if Int.eq n Int.zero then - Pmov rd r1 :: k - else if Int.eq n Int.one then - Padd W X16 r1 r1 (SOlsr (Int.repr 31)) :: - Porr W rd XZR X16 (SOasr n) :: k - else - Porr W X16 XZR r1 (SOasr (Int.repr 31)) :: - Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) :: - Porr W rd XZR X16 (SOasr n) :: k. - -Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code := - if Int.eq n Int.zero then - Pmov rd r1 :: k - else if Int.eq n Int.one then - Padd X X16 r1 r1 (SOlsr (Int.repr 63)) :: - Porr X rd XZR X16 (SOasr n) :: k - else - Porr X X16 XZR r1 (SOasr (Int.repr 63)) :: - Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) :: - Porr X rd XZR X16 (SOasr n) :: k. - -(** Load the address [id + ofs] in [rd] *) - -Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code := - if Archi.pic_code tt then - if Ptrofs.eq ofs Ptrofs.zero then - Ploadsymbol rd id :: k - else - Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k - else - Padrp rd id ofs :: Paddadr rd rd id ofs :: 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: code) := - match cond, args with - | (Ccomp c | Ccompu c), a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pcmp W r1 r2 SOnone :: 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 r1 r2 (transl_shift s a) :: k) - | (Ccompimm c n | Ccompuimm c n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_arith_imm32 n then - Pcmpimm W r1 (Int.unsigned n) :: k - else if is_arith_imm32 (Int.neg n) then - Pcmnimm W r1 (Int.unsigned (Int.neg n)) :: k - else - loadimm32 X16 n (Pcmp W r1 X16 SOnone :: k)) - | (Cmaskzero n | Cmasknotzero n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_logical_imm32 n then - Ptstimm W r1 (Int.unsigned n) :: k - else - loadimm32 X16 n (Ptst W r1 X16 SOnone :: k)) - | (Ccompl c | Ccomplu c), a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pcmp X r1 r2 SOnone :: 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 r1 r2 (transl_shift s a) :: k) - | (Ccomplimm c n | Ccompluimm c n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_arith_imm64 n then - Pcmpimm X r1 (Int64.unsigned n) :: k - else if is_arith_imm64 (Int64.neg n) then - Pcmnimm X r1 (Int64.unsigned (Int64.neg n)) :: k - else - loadimm64 X16 n (Pcmp X r1 X16 SOnone :: k)) - | (Cmasklzero n | Cmasklnotzero n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_logical_imm64 n then - Ptstimm X r1 (Int64.unsigned n) :: k - else - loadimm64 X16 n (Ptst X r1 X16 SOnone :: k)) - | Ccompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp D r1 r2 :: k) - | Cnotcompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp D r1 r2 :: k) - | Ccompfzero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 D r1 :: k) - | Cnotcompfzero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 D r1 :: k) - | Ccompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp S r1 r2 :: k) - | Cnotcompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp S r1 r2 :: k) - | Ccompfszero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 S r1 :: k) - | Cnotcompfszero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 S r1 :: k) - | _, _ => - Error(msg "Asmgen.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: code) := - transl_cond c args (Pbc (cond_for_cond c) lbl :: k). - -Definition transl_cond_branch - (c: condition) (args: list mreg) (lbl: label) (k: code) := - 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 (Pcbnz W r1 lbl :: k)) - 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 (Pcbz W r1 lbl :: k)) - 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 (Pcbnz X r1 lbl :: k)) - 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 (Pcbz X r1 lbl :: k)) - 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 (Ptbz W r1 bit lbl :: k) - | 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 (Ptbnz W r1 bit lbl :: k) - | 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 (Ptbz X r1 bit lbl :: k) - | 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 (Ptbnz X r1 bit lbl :: k) - | None => transl_cond_branch_default c args lbl k - end - | _, _ => - transl_cond_branch_default c args lbl k - end. - -(** Translation of the arithmetic operation [res <- op(args)]. - The corresponding instructions are prepended to [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: code) := + (op: operation) (args: list mreg) (res: mreg) (k: list basic) := match op, args with - | Omove, a1 :: nil => - match preg_of res, preg_of a1 with - | IR r, IR a => OK (Pmov r a :: k) - | FR r, FR a => OK (Pfmov r a :: k) - | _ , _ => Error(msg "Asmgen.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 :: k - else Pfmovimmd rd f :: k) - | Osingleconst f, nil => - do rd <- freg_of res; - OK (if Float32.eq_dec f Float32.zero - then Pfmovi S rd XZR :: k - else Pfmovimms rd f :: 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 rd XZR r1 (transl_shift s a) :: k) - | Oadd, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Padd W rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: k) - | Oaddimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (addimm32 rd r1 n k) - | Oneg, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub W rd XZR r1 SOnone :: k) - | Onegshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub W rd XZR r1 (transl_shift s a) :: k) - | Osub, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psub W rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: k) - | Omul, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pmadd W rd r1 r2 XZR :: 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 :: 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 :: 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 :: 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 :: k) - | Oand, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pand W rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd XZR r1 SOnone :: k) - | Onotshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porn W rd XZR r1 (transl_shift s a) :: k) - | Obic, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pbic W rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: k) - | Oorn, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porn W rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: k) - | Oeqv, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peon W rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 :: 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 :: 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 :: 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 rd r1 Int.zero s :: k) - | Osext s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz W rd r1 Int.zero s :: k) - | Oshlzext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) - | Oshlsext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) - | Ozextshr a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) - | Osextshr a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) -(** 64-bit integer arithmetic *) - | Oshiftl s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porr X rd XZR r1 (transl_shift s a) :: 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 :: k) - | Oaddl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Padd X rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd XZR r1 SOnone :: k) - | Oneglshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub X rd XZR r1 (transl_shift s a) :: k) - | Osubl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psub X rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: k) - | Oandl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pand X rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 rd XZR r1 SOnone :: k) - | Onotlshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porn X rd XZR r1 (transl_shift s a) :: k) - | Obicl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pbic X rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: k) - | Oornl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porn X rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: k) - | Oeqvl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peon X rd r1 r2 SOnone :: 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 rd r1 r2 (transl_shift s a) :: 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 :: 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 :: 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 :: 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 rd r1 Int.zero s :: k) - | Osextl s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz X rd r1 Int.zero s :: k) - | Oshllzext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) - | Oshllsext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) - | Ozextshrl a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) - | Osextshrl a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) -(** 64-bit floating-point arithmetic *) - | Onegf, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfneg D rd rs :: k) - | Oabsf, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfabs D rd rs :: 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 :: 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 :: 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 :: 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 :: k) -(** 32-bit floating-point arithmetic *) - | Onegfs, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfneg S rd rs :: k) - | Oabsfs, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfabs S rd rs :: 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 :: 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 :: 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 :: 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 :: k) - | Osingleoffloat, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfcvtsd rd rs :: k) - | Ofloatofsingle, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfcvtds rd rs :: 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 :: k) - | Ointuoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu W D rd rs :: k) - | Ofloatofint, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf D W rd rs :: k) - | Ofloatofintu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf D W rd rs :: k) - | Ointofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs W S rd rs :: k) - | Ointuofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu W S rd rs :: k) - | Osingleofint, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf S W rd rs :: k) - | Osingleofintu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf S W rd rs :: k) - | Olongoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs X D rd rs :: k) - | Olonguoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu X D rd rs :: k) - | Ofloatoflong, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf D X rd rs :: k) - | Ofloatoflongu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf D X rd rs :: k) - | Olongofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs X S rd rs :: k) - | Olonguofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu X S rd rs :: k) - | Osingleoflong, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf S X rd rs :: k) - | Osingleoflongu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf S X rd rs :: k) -(** Boolean tests *) - | Ocmp c, _ => - do rd <- ireg_of res; - transl_cond c args (Pcset rd (cond_for_cond c) :: 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) :: k) - | FR r => - do r1 <- freg_of a1; do r2 <- freg_of a2; - transl_cond cmp args (Pfsel r r1 r2 (cond_for_cond cmp) :: k) - | _ => - Error(msg "Asmgen.Osel") - end - | _, _ => - Error(msg "Asmgen.transl_op") + | _ => Error(msg "Not implemented yet") end. -(** Translation of addressing modes *) - -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 transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) - (insn: Asm.addressing -> instruction) (k: code) : res code := - match addr, args with - | Aindexed ofs, a1 :: nil => - do r1 <- ireg_of a1; - if offset_representable sz ofs then - OK (insn (ADimm r1 ofs) :: k) - else - OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k)) - | Aindexed2, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (insn (ADreg r1 r2) :: 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) :: k) - else if Int.eq (Int.shl Int.one a) (Int.repr sz) then - OK (insn (ADlsl r1 r2 a) :: k) - else - OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: 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) :: k) - else - OK (arith_extended Paddext (Padd X) X16 r1 r2 x a - (insn (ADimm X16 Int64.zero) :: 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 X16 id ofs :: insn (ADadr X16 id ofs) :: k) - else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k)) - | Ainstack ofs, nil => - let ofs := Ptrofs.to_int64 ofs in - if offset_representable sz ofs then - OK (insn (ADimm XSP ofs) :: k) - else - OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k)) - | _, _ => - Error(msg "Asmgen.transl_addressing") - end. - -(** Translation of loads and stores *) - -Definition transl_load (trap: trapping_mode) - (chunk: memory_chunk) (addr: Op.addressing) - (args: list mreg) (dst: mreg) (k: code) : res code := - match trap with - | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64") - | TRAP => - match chunk with - | Mint8unsigned => - do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k - | Mint8signed => - do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrsb W rd) k - | Mint16unsigned => - do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrh W rd) k - | Mint16signed => - do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrsh W rd) k - | Mint32 => - do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw rd) k - | Mint64 => - do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx rd) k - | Mfloat32 => - do rd <- freg_of dst; transl_addressing 4 addr args (Pldrs rd) k - | Mfloat64 => - do rd <- freg_of dst; transl_addressing 8 addr args (Pldrd rd) k - | Many32 => - do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k - | Many64 => - do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k - end - end. - -Definition transl_store (chunk: memory_chunk) (addr: Op.addressing) - (args: list mreg) (src: mreg) (k: code) : res code := - match chunk with - | Mint8unsigned | Mint8signed => - do r1 <- ireg_of src; transl_addressing 1 addr args (Pstrb r1) k - | Mint16unsigned | Mint16signed => - do r1 <- ireg_of src; transl_addressing 2 addr args (Pstrh r1) k - | Mint32 => - do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw r1) k - | Mint64 => - do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx r1) k - | Mfloat32 => - do r1 <- freg_of src; transl_addressing 4 addr args (Pstrs r1) k - | Mfloat64 => - do r1 <- freg_of src; transl_addressing 8 addr args (Pstrd r1) k - | Many32 => - do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw_a r1) k - | Many64 => - do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx_a r1) k - end. - -(** Register-indexed loads and stores *) - -Definition indexed_memory_access (insn: Asm.addressing -> instruction) - (sz: Z) (base: iregsp) (ofs: ptrofs) (k: code) := - 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: code) := - match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (Pldrw rd) 4 base ofs k) - | Tlong, IR rd => OK (indexed_memory_access (Pldrx rd) 8 base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pldrs rd) 4 base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pldrd rd) 8 base ofs k) - | Tany32, IR rd => OK (indexed_memory_access (Pldrw_a rd) 4 base ofs k) - | Tany64, IR rd => OK (indexed_memory_access (Pldrx_a rd) 8 base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pldrd_a rd) 8 base ofs k) - | _, _ => Error (msg "Asmgen.loadind") - end. - -Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: code) := - match ty, preg_of src with - | Tint, IR rd => OK (indexed_memory_access (Pstrw rd) 4 base ofs k) - | Tlong, IR rd => OK (indexed_memory_access (Pstrx rd) 8 base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pstrs rd) 4 base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pstrd rd) 8 base ofs k) - | Tany32, IR rd => OK (indexed_memory_access (Pstrw_a rd) 4 base ofs k) - | Tany64, IR rd => OK (indexed_memory_access (Pstrx_a rd) 8 base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pstrd_a rd) 8 base ofs k) - | _, _ => Error (msg "Asmgen.storeind") - end. - -Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: code) := - indexed_memory_access (Pldrx dst) 8 base ofs k. - -Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := - indexed_memory_access (Pstrx src) 8 base ofs k. - -(** Function epilogue *) - -Definition make_epilogue (f: Mach.function) (k: code) := - (* FIXME - Cannot be used because memcpy destroys X30; - issue being discussed with X. Leroy *) - (* if is_leaf_function f - then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k - else*) loadptr XSP f.(fn_retaddr_ofs) RA - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). - -(** Translation of a Mach instruction. *) +(** Translation of a Machblock instruction. *) -Definition transl_instr (f: Mach.function) (i: Mach.instruction) - (r29_is_parent: bool) (k: code) : res code := +Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) + (ep: bool) (k: list basic) := match i with - | Mgetstack ofs ty dst => - loadind XSP ofs ty dst k - | Msetstack src ofs ty => - storeind src XSP ofs ty k - | Mgetparam ofs ty dst => - (* load via the frame pointer if it is valid *) - do c <- loadind X29 ofs ty dst k; - OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c) | Mop op args res => transl_op op args res k - | Mload trap chunk addr args dst => - transl_load trap chunk addr args dst k - | Mstore chunk addr args src => - transl_store chunk addr args src k - | Mcall sig (inl r) => - do r1 <- ireg_of r; OK (Pblr r1 sig :: k) - | Mcall sig (inr symb) => - OK (Pbl symb sig :: k) - | Mtailcall sig (inl r) => - do r1 <- ireg_of r; - OK (make_epilogue f (Pbr r1 sig :: k)) - | Mtailcall sig (inr symb) => - OK (make_epilogue f (Pbs symb sig :: k)) - | Mbuiltin ef args res => - OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) - | Mlabel lbl => - OK (Plabel lbl :: k) - | Mgoto lbl => - OK (Pb lbl :: k) - | Mcond cond args lbl => - transl_cond_branch cond args lbl k - | Mjumptable arg tbl => - do r <- ireg_of arg; - OK (Pbtbl r tbl :: k) - | Mreturn => - OK (make_epilogue f (Pret RA :: k)) + | _ => Error(msg "Not implemented yet") + (*| MBgetstack ofs ty dst =>*) + (*loadind SP ofs ty dst k*) + (*| MBsetstack src ofs ty =>*) + (*storeind src SP ofs ty k*) + (*| MBgetparam ofs ty dst =>*) + (*[> load via the frame pointer if it is valid <]*) + (*do c <- loadind FP ofs ty dst k;*) + (*OK (if ep then c*) + (*else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)*) + (*| MBop op args res =>*) + (*transl_op op args res k*) + (*| MBload trap chunk addr args dst =>*) + (*transl_load trap chunk addr args dst k*) + (*| 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: Mach.instruction) : bool := - match i with - | Msetstack src ofs ty => before - | Mgetparam ofs ty dst => negb (mreg_eq dst R29) - | Mop op args res => before && negb (mreg_eq res R29) - | _ => false - end. - -(** This is the naive definition that we no longer use because it - is not tail-recursive. It is kept as specification. *) - -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := +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_code f il' (it1_is_parent it1p i1); - transl_instr f i1 it1p k + do k <- transl_basic_code f il' (fp_is_parent it1p i1); + transl_instr_basic f i1 it1p k end. -(** This is an equivalent definition in continuation-passing style - that runs in constant stack space. *) +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); + OK (gen_bblocks fb.(Machblock.header) c ctl) +. -Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) - (it1p: bool) (k: code -> res code) := - match il with - | nil => k nil - | i1 :: il' => - transl_code_rec f il' (it1_is_parent it1p i1) - (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2) - end. +Program Definition 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 + (* OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)*) -Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := - transl_code_rec f il it1p (fun c => OK c). +(* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *) +Program Definition make_prologue (f: Machblock.function) (k:bblocks) := + Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b + storeptr RA XSP f.(fn_retaddr_ofs) 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)). -(** Translation of a whole function. Note that we must check - that the generated code contains less than [2^32] instructions, - otherwise the offset part of the [PC] code pointer could wrap - around, leading to incorrect executions. *) +Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := + transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) -Definition transl_function (f: Mach.function) := - do c <- transl_code' f f.(Mach.fn_code) true; - OK (mkfunction f.(Mach.fn_sig) - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - storeptr RA XSP f.(fn_retaddr_ofs) c)). +Definition transf_program (p: Machblock.program) : res Asmblock.program := + transform_partial_program transf_fundef p. -*) \ No newline at end of file -- cgit