diff options
Diffstat (limited to 'aarch64/TO_MERGE/Asmgen.v')
| -rw-r--r-- | aarch64/TO_MERGE/Asmgen.v | 712 |
1 files changed, 712 insertions, 0 deletions
diff --git a/aarch64/TO_MERGE/Asmgen.v b/aarch64/TO_MERGE/Asmgen.v new file mode 100644 index 00000000..c8e48b40 --- /dev/null +++ b/aarch64/TO_MERGE/Asmgen.v @@ -0,0 +1,712 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Justus Fasse UGA, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Recdef Coqlib Zwf Zbits. +Require Import Errors AST Integers Floats Op. +<<<<<<< HEAD +Require Import Locations Compopts. +Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling. +======= +Require Import Locations Mach Asm. +Require SelectOp. + +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. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.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). +>>>>>>> master + + +Local Open Scope error_monad_scope. + +(** Functions called by the Asmexpand ocaml file, inspired and adapted from Asmblockgen.v *) + +Module Asmgen_expand. + +(* Load immediate *) + +Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := + List.fold_right (fun np k => Asm.Pmovk sz rd (fst np) (snd np) :: k) k l. + +Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := + match l with + | nil => Asm.Pmovz sz rd 0 0 :: k + | (n1, p1) :: l => Asm.Pmovz sz rd n1 p1 :: loadimm_k sz rd l k + end. + +Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := + match l with + | nil => Asm.Pmovn sz rd 0 0 :: k + | (n1, p1) :: l => Asm.Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k + end. + +Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code := + 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: code) : code := + if is_logical_imm32 n + then Asm.Porrimm W rd XZR (Int.unsigned n) :: k + else loadimm W rd (Int.unsigned n) k. + +Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code := + if is_logical_imm64 n + then Asm.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 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 (Asm.Paddimm X) rd r1 (Int64.unsigned n) k + else if Int64.eq m (Int64.zero_ext 24 m) then + addimm_aux (Asm.Psubimm X) rd r1 (Int64.unsigned m) k + else if Int64.lt n Int64.zero then +<<<<<<< HEAD + loadimm64 X16 m (Asm.Psubext rd r1 X16 (EOuxtx Int.zero) :: k) +======= + 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 + 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 + 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 SelectOp.symbol_is_relocatable id then + if Ptrofs.eq ofs Ptrofs.zero then + Ploadsymbol rd id :: k + else + Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k +>>>>>>> master + else + loadimm64 X16 n (Asm.Paddext rd r1 X16 (EOuxtx Int.zero) :: k). + +(** Register-indexed 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 storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := + indexed_memory_access (Asm.Pstrx src) 8 base ofs k. + +End Asmgen_expand. + +(** * Translation from Asmblock to assembly language + Inspired from the KVX backend (see kvx/Asm.v and kvx/Asmgen.v) *) + +Module Asmblock_TRANSF. +(* STUB *) + +Definition ireg_of_preg (p : Asm.preg) : res ireg := + match p with + | DR (IR (RR1 r)) => OK r + | _ => Error (msg "Asmgen.ireg_of_preg") + end. + +Definition freg_of_preg (p : Asm.preg) : res freg := + match p with + | DR (FR r) => OK r + | _ => Error (msg "Asmgen.freg_of_preg") + end. + +Definition iregsp_of_preg (p : Asm.preg) : res iregsp := + match p with + | DR (IR r) => OK r + | _ => Error (msg "Asmgen.iregsp_of_preg") + end. + +Definition basic_to_instruction (b: basic) : res Asm.instruction := + match b with + (* Aithmetic instructions *) + | PArith (PArithP (Padrp id ofs) rd) => do rd' <- ireg_of_preg rd; + OK (Asm.Padrp rd' id ofs) + | PArith (PArithP (Pmovz sz n pos) rd) => do rd' <- ireg_of_preg rd; + OK (Asm.Pmovz sz rd' n pos) + | PArith (PArithP (Pmovn sz n pos) rd) => do rd' <- ireg_of_preg rd; + OK (Asm.Pmovn sz rd' n pos) + | PArith (PArithP (Pfmovimms f) rd) => do rd' <- freg_of_preg rd; + OK (Asm.Pfmovimms rd' f) + | PArith (PArithP (Pfmovimmd f) rd) => do rd' <- freg_of_preg rd; + OK (Asm.Pfmovimmd rd' f) + + | PArith (PArithPP (Pmovk sz n pos) rd rs) => + if (Asm.preg_eq rd rs) then ( + do rd' <- ireg_of_preg rd; + OK (Asm.Pmovk sz rd' n pos) + ) else + Error (msg "Asmgen.basic_to_instruction: Pmovk uses a single register as both source and target") + | PArith (PArithPP Pmov rd rs) => do rd' <- iregsp_of_preg rd; + do rs' <- iregsp_of_preg rs; + OK (Asm.Pmov rd' rs') + | PArith (PArithPP (Paddadr id ofs) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Paddadr rd' rs' id ofs) + | PArith (PArithPP (Psbfiz sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Psbfiz sz rd' rs' r s) + | PArith (PArithPP (Psbfx sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Psbfx sz rd' rs' r s) + | PArith (PArithPP (Pubfiz sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pubfiz sz rd' rs' r s) + | PArith (PArithPP (Pubfx sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pubfx sz rd' rs' r s) + | PArith (PArithPP Pfmov rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfmov rd' rs') + | PArith (PArithPP Pfcvtds rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtds rd' rs') + | PArith (PArithPP Pfcvtsd rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtsd rd' rs') + | PArith (PArithPP (Pfabs sz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfabs sz rd' rs') + | PArith (PArithPP (Pfneg sz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfneg sz rd' rs') + | PArith (PArithPP (Pscvtf fsz isz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pscvtf fsz isz rd' rs') + | PArith (PArithPP (Pucvtf fsz isz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pucvtf fsz isz rd' rs') + | PArith (PArithPP (Pfcvtzs isz fsz) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtzs isz fsz rd' rs') + | PArith (PArithPP (Pfcvtzu isz fsz) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtzu isz fsz rd' rs') + | PArith (PArithPP (Paddimm sz n) rd rs) => do rd' <- iregsp_of_preg rd; + do rs' <- iregsp_of_preg rs; + OK (Asm.Paddimm sz rd' rs' n) + | PArith (PArithPP (Psubimm sz n) rd rs) => do rd' <- iregsp_of_preg rd; + do rs' <- iregsp_of_preg rs; + OK (Asm.Psubimm sz rd' rs' n) + + | PArith (PArithPPP (Pasrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pasrv sz rd' r1' r2') + | PArith (PArithPPP (Plslv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Plslv sz rd' r1' r2') + | PArith (PArithPPP (Plsrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Plsrv sz rd' r1' r2') + | PArith (PArithPPP (Prorv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Prorv sz rd' r1' r2') + | PArith (PArithPPP Psmulh rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Psmulh rd' r1' r2') + | PArith (PArithPPP Pumulh rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pumulh rd' r1' r2') + | PArith (PArithPPP (Psdiv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Psdiv sz rd' r1' r2') + | PArith (PArithPPP (Pudiv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pudiv sz rd' r1' r2') + | PArith (PArithPPP (Paddext x) rd r1 r2) => do rd' <- iregsp_of_preg rd; + do r1' <- iregsp_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Paddext rd' r1' r2' x) + | PArith (PArithPPP (Psubext x) rd r1 r2) => do rd' <- iregsp_of_preg rd; + do r1' <- iregsp_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Psubext rd' r1' r2' x) + | PArith (PArithPPP (Pfadd sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfadd sz rd' r1' r2') + | PArith (PArithPPP (Pfdiv sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfdiv sz rd' r1' r2') + | PArith (PArithPPP (Pfmul sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfmul sz rd' r1' r2') + | PArith (PArithPPP (Pfsub sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfsub sz rd' r1' r2') + + | PArith (PArithRR0 (Pandimm sz n) rd r1) => OK (Asm.Pandimm sz rd r1 n) + | PArith (PArithRR0 (Peorimm sz n) rd r1) => OK (Asm.Peorimm sz rd r1 n) + | PArith (PArithRR0 (Porrimm sz n) rd r1) => OK (Asm.Porrimm sz rd r1 n) + + + | PArith (PArithRR0R (Padd sz s) rd r1 r2) => OK (Asm.Padd sz rd r1 r2 s) + | PArith (PArithRR0R (Psub sz s) rd r1 r2) => OK (Asm.Psub sz rd r1 r2 s) + | PArith (PArithRR0R (Pand sz s) rd r1 r2) => OK (Asm.Pand sz rd r1 r2 s) + | PArith (PArithRR0R (Pbic sz s) rd r1 r2) => OK (Asm.Pbic sz rd r1 r2 s) + | PArith (PArithRR0R (Peon sz s) rd r1 r2) => OK (Asm.Peon sz rd r1 r2 s) + | PArith (PArithRR0R (Peor sz s) rd r1 r2) => OK (Asm.Peor sz rd r1 r2 s) + | PArith (PArithRR0R (Porr sz s) rd r1 r2) => OK (Asm.Porr sz rd r1 r2 s) + | PArith (PArithRR0R (Porn sz s) rd r1 r2) => OK (Asm.Porn sz rd r1 r2 s) + + | PArith (PArithARRRR0 (Pmadd sz) rd r1 r2 r3) => OK (Asm.Pmadd sz rd r1 r2 r3) + | PArith (PArithARRRR0 (Pmsub sz) rd r1 r2 r3) => OK (Asm.Pmsub sz rd r1 r2 r3) + + | PArith (PArithComparisonPP (Pcmpext x) r1 r2) => do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pcmpext r1' r2' x) + | PArith (PArithComparisonPP (Pcmnext x) r1 r2) => do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pcmnext r1' r2' x) + | PArith (PArithComparisonPP (Pfcmp sz) r1 r2) => do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfcmp sz r1' r2') + + | PArith (PArithComparisonR0R (Pcmp is s) r1 r2) => OK (Asm.Pcmp is r1 r2 s) + | PArith (PArithComparisonR0R (Pcmn is s) r1 r2) => OK (Asm.Pcmn is r1 r2 s) + | PArith (PArithComparisonR0R (Ptst is s) r1 r2) => OK (Asm.Ptst is r1 r2 s) + + | PArith (PArithComparisonP (Pcmpimm sz n) r1) => do r1' <- ireg_of_preg r1; + OK (Asm.Pcmpimm sz r1' n) + | PArith (PArithComparisonP (Pcmnimm sz n) r1) => do r1' <- ireg_of_preg r1; + OK (Asm.Pcmnimm sz r1' n) + | PArith (PArithComparisonP (Ptstimm sz n) r1) => do r1' <- ireg_of_preg r1; + OK (Asm.Ptstimm sz r1' n) + | PArith (PArithComparisonP (Pfcmp0 sz) r1) => do r1' <- freg_of_preg r1; + OK (Asm.Pfcmp0 sz r1') + + | PArith (Pcset rd c) => OK (Asm.Pcset rd c) + | PArith (Pfmovi fsz rd r1) => OK (Asm.Pfmovi fsz rd r1) + | PArith (Pcsel rd r1 r2 c) => + match r1, r2 with + | IR r1', IR r2' => do rd' <- ireg_of_preg rd; + do r1'' <- ireg_of_preg r1'; + do r2'' <- ireg_of_preg r2'; + OK (Asm.Pcsel rd' r1'' r2'' c) + | FR r1', FR r2' => do rd' <- freg_of_preg rd; + do r1'' <- freg_of_preg r1'; + do r2'' <- freg_of_preg r2'; + OK (Asm.Pfsel rd' r1'' r2'' c) + | _, _ => Error (msg "Asmgen.basic_to_instruction: Pcsel is only defind on iregs and fregs.") + end + | PArith (Pfnmul fsz rd r1 r2) => OK (Asm.Pfnmul fsz rd r1 r2) + + | PLoad (PLd_rd_a Pldrw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw rd' a) + | PLoad (PLd_rd_a Pldrw_a rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw_a rd' a) + | PLoad (PLd_rd_a Pldrx rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx rd' a) + | PLoad (PLd_rd_a Pldrx_a rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx_a rd' a) + | PLoad (PLd_rd_a (Pldrb sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrb sz rd' a) + | PLoad (PLd_rd_a (Pldrsb sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsb sz rd' a) + | PLoad (PLd_rd_a (Pldrh sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrh sz rd' a) + | PLoad (PLd_rd_a (Pldrsh sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsh sz rd' a) + | PLoad (PLd_rd_a Pldrzw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrzw rd' a) + | PLoad (PLd_rd_a Pldrsw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsw rd' a) + + | PLoad (PLd_rd_a Pldrs rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrs rd' a) + | PLoad (PLd_rd_a Pldrd rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrd rd' a) + | PLoad (PLd_rd_a Pldrd_a rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrd_a rd' a) + + | PLoad (Pldp Pldpw rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1; + do rd2' <- ireg_of_preg rd2; + OK (Asm.Pldpw rd1' rd2' chk1 chk2 a) + | PLoad (Pldp Pldpx rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1; + do rd2' <- ireg_of_preg rd2; + OK (Asm.Pldpx rd1' rd2' chk1 chk2 a) + | PLoad (Pldp Pldps rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1; + do rd2' <- freg_of_preg rd2; + OK (Asm.Pldps rd1' rd2' chk1 chk2 a) + | PLoad (Pldp Pldpd rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1; + do rd2' <- freg_of_preg rd2; + OK (Asm.Pldpd rd1' rd2' chk1 chk2 a) + + | PStore (PSt_rs_a Pstrw r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw r' a) + | PStore (PSt_rs_a Pstrw_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw_a r' a) + | PStore (PSt_rs_a Pstrx r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrx r' a) + | PStore (PSt_rs_a Pstrx_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrx_a r' a) + | PStore (PSt_rs_a Pstrb r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrb r' a) + | PStore (PSt_rs_a Pstrh r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrh r' a) + + | PStore (PSt_rs_a Pstrs r a) => do r' <- freg_of_preg r; OK (Asm.Pstrs r' a) + | PStore (PSt_rs_a Pstrd r a) => do r' <- freg_of_preg r; OK (Asm.Pstrd r' a) + | PStore (PSt_rs_a Pstrd_a r a) => do r' <- freg_of_preg r; OK (Asm.Pstrd_a r' a) + + | PStore (Pstp Pstpw rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1; + do rs2' <- ireg_of_preg rs2; + OK (Asm.Pstpw rs1' rs2' chk1 chk2 a) + | PStore (Pstp Pstpx rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1; + do rs2' <- ireg_of_preg rs2; + OK (Asm.Pstpx rs1' rs2' chk1 chk2 a) + | PStore (Pstp Pstps rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1; + do rs2' <- freg_of_preg rs2; + OK (Asm.Pstps rs1' rs2' chk1 chk2 a) + | PStore (Pstp Pstpd rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1; + do rs2' <- freg_of_preg rs2; + OK (Asm.Pstpd rs1' rs2' chk1 chk2 a) + + | Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs) + | Pfreeframe sz linkofs => OK (Asm.Pfreeframe sz linkofs) + + | Ploadsymbol rd id => OK (Asm.Ploadsymbol rd id) + + | Pcvtsw2x rd r1 => OK (Asm.Pcvtsw2x rd r1) + + | Pcvtuw2x rd r1 => OK (Asm.Pcvtuw2x rd r1) + + | Pcvtx2w rd => OK (Asm.Pcvtx2w rd) + | Pnop => OK (Asm.Pnop) + end. + +<<<<<<< HEAD +Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction := + match cfi with + | Pb l => Asm.Pb l + | Pbc c lbl => Asm.Pbc c lbl + | Pbl id sg => Asm.Pbl id sg + | Pbs id sg => Asm.Pbs id sg + | Pblr r sg => Asm.Pblr r sg + | Pbr r sg => Asm.Pbr r sg + | Pret r => Asm.Pret r + | Pcbnz sz r lbl => Asm.Pcbnz sz r lbl + | Pcbz sz r lbl => Asm.Pcbz sz r lbl + | Ptbnz sz r n lbl => Asm.Ptbnz sz r n lbl + | Ptbz sz r n lbl => Asm.Ptbz sz r n lbl + | Pbtbl r1 tbl => Asm.Pbtbl r1 tbl +======= +(** 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 (SelectOp.symbol_is_relocatable id)); + 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") +>>>>>>> master + end. + +Definition control_to_instruction (c: control) := + match c with + | PCtlFlow i => cf_instruction_to_instruction i + | Pbuiltin ef args res => Asm.Pbuiltin ef (List.map (map_builtin_arg DR) args) (map_builtin_res DR res) + end. + +Fixpoint unfold_label (ll: list label) := + match ll with + | nil => nil + | l :: ll => Plabel l :: unfold_label ll + end. + +Fixpoint unfold_body (lb: list basic) : res Asm.code := + match lb with + | nil => OK nil + | b :: lb => + (* x_is: x's instructions *) + do b_is <- basic_to_instruction b; + do lb_is <- unfold_body lb; + OK (b_is :: lb_is) + end. + +Definition unfold_exit (oc: option control) := + match oc with + | None => nil + | Some c => control_to_instruction c :: nil + end. + +Definition unfold_bblock (bb: bblock) := + let lbl := unfold_label (header bb) in + (* + * With this dynamically checked assumption on a previous optimization we + * can show that [Asmblock.label_pos] and [Asm.label_pos] retrieve the same + * exact address. Maintaining this property allows us to use the simple + * formulation of match_states defined as equality. + * Otherwise we would have to deal with the case of a basic block header + * that has multiple labels. Asmblock.label_pos will, for all labels, point + * to the same location at the beginning of the basic block. Asm.label_pos + * on the other hand could return a position pointing into the original + * basic block. + *) + if zle (list_length_z (header bb)) 1 then + do bo_is <- unfold_body (body bb); + OK (lbl ++ bo_is ++ unfold_exit (exit bb)) + else + Error (msg "Asmgen.unfold_bblock: Multiple labels were generated."). + +Fixpoint unfold (bbs: Asmblock.bblocks) : res Asm.code := + match bbs with + | nil => OK (nil) + | bb :: bbs' => + do bb_is <- unfold_bblock bb; + do bbs'_is <- unfold bbs'; + OK (bb_is ++ bbs'_is) + end. + +Definition transf_function (f: Asmblock.function) : res Asm.function := + do c <- unfold (Asmblock.fn_blocks f); + if zlt Ptrofs.max_unsigned (list_length_z c) + then Error (msg "Asmgen.trans_function: code size exceeded") + else OK {| Asm.fn_sig := Asmblock.fn_sig f; Asm.fn_code := c |}. + +Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Asmblock.program) : res Asm.program := + transform_partial_program transf_fundef p. + +End Asmblock_TRANSF. + +Definition transf_program (p: Mach.program) : res Asm.program := + let mbp := Machblockgen.transf_program p in + do abp <- Asmblockgen.transf_program mbp; + do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp; + Asmblock_TRANSF.transf_program abp'. |