From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgen.v | 510 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 510 insertions(+) create mode 100644 powerpc/Asmgen.v (limited to 'powerpc/Asmgen.v') diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v new file mode 100644 index 00000000..2ddaa6d0 --- /dev/null +++ b/powerpc/Asmgen.v @@ -0,0 +1,510 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* 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 PPC. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Errors. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import Mach. +Require Import Asm. + +(** Decomposition of integer constants. As noted in file [Asm], + immediate arguments to PowerPC instructions must fit into 16 bits, + and are interpreted after zero extension, sign extension, or + left shift by 16 bits, depending on the instruction. Integer + constants that do not fit must be synthesized using two + processor instructions. The following functions decompose + arbitrary 32-bit integers into two 16-bit halves (high and low + halves). They satisfy the following properties: +- [low_u n] is an unsigned 16-bit integer; +- [low_s n] is a signed 16-bit integer; +- [(high_u n) << 16 | low_u n] equals [n]; +- [(high_s n) << 16 + low_s n] equals [n]. +*) + +Definition low_u (n: int) := Int.and n (Int.repr 65535). +Definition high_u (n: int) := Int.shru n (Int.repr 16). +Definition low_s (n: int) := Int.sign_ext 16 n. +Definition high_s (n: int) := Int.shru (Int.sub n (low_s n)) (Int.repr 16). + +(** Smart constructors for arithmetic operations involving + a 32-bit integer constant. Depending on whether the + constant fits in 16 bits or not, one or several instructions + are generated as required to perform the operation + and prepended to the given instruction sequence [k]. *) + +Definition loadimm (r: ireg) (n: int) (k: code) := + if Int.eq (high_s n) Int.zero then + Paddi r GPR0 (Cint n) :: k + else if Int.eq (low_s n) Int.zero then + Paddis r GPR0 (Cint (high_s n)) :: k + else + Paddis r GPR0 (Cint (high_u n)) :: + Pori r r (Cint (low_u n)) :: k. + +Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) := + if Int.eq (high_s n) Int.zero then + Paddi r1 r2 (Cint n) :: k + else if Int.eq (low_s n) Int.zero then + Paddis r1 r2 (Cint (high_s n)) :: k + else + Paddis r1 r2 (Cint (high_s n)) :: + Paddi r1 r1 (Cint (low_s n)) :: k. + +Definition addimm_2 (r1 r2: ireg) (n: int) (k: code) := + loadimm GPR12 n (Padd r1 r2 GPR12 :: k). + +Definition addimm (r1 r2: ireg) (n: int) (k: code) := + if ireg_eq r1 GPR0 then + addimm_2 r1 r2 n k + else if ireg_eq r2 GPR0 then + addimm_2 r1 r2 n k + else + addimm_1 r1 r2 n k. + +Definition andimm (r1 r2: ireg) (n: int) (k: code) := + if Int.eq (high_u n) Int.zero then + Pandi_ r1 r2 (Cint n) :: k + else if Int.eq (low_u n) Int.zero then + Pandis_ r1 r2 (Cint (high_u n)) :: k + else + loadimm GPR12 n (Pand_ r1 r2 GPR12 :: k). + +Definition orimm (r1 r2: ireg) (n: int) (k: code) := + if Int.eq (high_u n) Int.zero then + Pori r1 r2 (Cint n) :: k + else if Int.eq (low_u n) Int.zero then + Poris r1 r2 (Cint (high_u n)) :: k + else + Poris r1 r2 (Cint (high_u n)) :: + Pori r1 r1 (Cint (low_u n)) :: k. + +Definition xorimm (r1 r2: ireg) (n: int) (k: code) := + if Int.eq (high_u n) Int.zero then + Pxori r1 r2 (Cint n) :: k + else if Int.eq (low_u n) Int.zero then + Pxoris r1 r2 (Cint (high_u n)) :: k + else + Pxoris r1 r2 (Cint (high_u n)) :: + Pxori r1 r1 (Cint (low_u n)) :: k. + +(** Smart constructors for indexed loads and stores, + where the address is the contents of a register plus + an integer literal. *) + +Definition loadind_aux (base: ireg) (ofs: int) (ty: typ) (dst: mreg) := + match ty with + | Tint => Plwz (ireg_of dst) (Cint ofs) base + | Tfloat => Plfd (freg_of dst) (Cint ofs) base + end. + +Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := + if Int.eq (high_s ofs) Int.zero then + loadind_aux base ofs ty dst :: k + else + Paddis GPR12 base (Cint (high_s ofs)) :: + loadind_aux GPR12 (low_s ofs) ty dst :: k. + +Definition storeind_aux (src: mreg) (base: ireg) (ofs: int) (ty: typ) := + match ty with + | Tint => Pstw (ireg_of src) (Cint ofs) base + | Tfloat => Pstfd (freg_of src) (Cint ofs) base + end. + +Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := + if Int.eq (high_s ofs) Int.zero then + storeind_aux src base ofs ty :: k + else + Paddis GPR12 base (Cint (high_s ofs)) :: + storeind_aux src GPR12 (low_s ofs) ty :: k. + +(** Constructor for a floating-point comparison. The PowerPC has + a single [fcmpu] instruction to compare floats, which sets + bits 0, 1 and 2 of the condition register to reflect ``less'', + ``greater'' and ``equal'' conditions, respectively. + The ``less or equal'' and ``greater or equal'' conditions must be + synthesized by a [cror] instruction that computes the logical ``or'' + of the corresponding two conditions. *) + +Definition floatcomp (cmp: comparison) (r1 r2: freg) (k: code) := + Pfcmpu r1 r2 :: + match cmp with + | Cle => Pcror CRbit_3 CRbit_2 CRbit_0 :: k + | Cge => Pcror CRbit_3 CRbit_2 CRbit_1 :: k + | _ => k + 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, a1 :: a2 :: nil => + Pcmpw (ireg_of a1) (ireg_of a2) :: k + | Ccompu c, a1 :: a2 :: nil => + Pcmplw (ireg_of a1) (ireg_of a2) :: k + | Ccompimm c n, a1 :: nil => + if Int.eq (high_s n) Int.zero then + Pcmpwi (ireg_of a1) (Cint n) :: k + else + loadimm GPR12 n (Pcmpw (ireg_of a1) GPR12 :: k) + | Ccompuimm c n, a1 :: nil => + if Int.eq (high_u n) Int.zero then + Pcmplwi (ireg_of a1) (Cint n) :: k + else + loadimm GPR12 n (Pcmplw (ireg_of a1) GPR12 :: k) + | Ccompf cmp, a1 :: a2 :: nil => + floatcomp cmp (freg_of a1) (freg_of a2) k + | Cnotcompf cmp, a1 :: a2 :: nil => + floatcomp cmp (freg_of a1) (freg_of a2) k + | Cmaskzero n, a1 :: nil => + andimm GPR12 (ireg_of a1) n k + | Cmasknotzero n, a1 :: nil => + andimm GPR12 (ireg_of a1) n k + | _, _ => + k (**r never happens for well-typed code *) + end. + +(* CRbit_0 = Less + CRbit_1 = Greater + CRbit_2 = Equal + CRbit_3 = Other *) + +Definition crbit_for_icmp (cmp: comparison) := + match cmp with + | Ceq => (CRbit_2, true) + | Cne => (CRbit_2, false) + | Clt => (CRbit_0, true) + | Cle => (CRbit_1, false) + | Cgt => (CRbit_1, true) + | Cge => (CRbit_0, false) + end. + +Definition crbit_for_fcmp (cmp: comparison) := + match cmp with + | Ceq => (CRbit_2, true) + | Cne => (CRbit_2, false) + | Clt => (CRbit_0, true) + | Cle => (CRbit_3, true) + | Cgt => (CRbit_1, true) + | Cge => (CRbit_3, true) + end. + +Definition crbit_for_cond (cond: condition) := + match cond with + | Ccomp cmp => crbit_for_icmp cmp + | Ccompu cmp => crbit_for_icmp cmp + | Ccompimm cmp n => crbit_for_icmp cmp + | Ccompuimm cmp n => crbit_for_icmp cmp + | Ccompf cmp => crbit_for_fcmp cmp + | Cnotcompf cmp => let p := crbit_for_fcmp cmp in (fst p, negb (snd p)) + | Cmaskzero n => (CRbit_2, true) + | Cmasknotzero n => (CRbit_2, false) + end. + +(** Translation of the arithmetic operation [r <- op(args)]. + The corresponding instructions are prepended to [k]. *) + +Definition transl_op + (op: operation) (args: list mreg) (r: mreg) (k: code) := + match op, args with + | Omove, a1 :: nil => + match mreg_type a1 with + | Tint => Pmr (ireg_of r) (ireg_of a1) :: k + | Tfloat => Pfmr (freg_of r) (freg_of a1) :: k + end + | Ointconst n, nil => + loadimm (ireg_of r) n k + | Ofloatconst f, nil => + Plfi (freg_of r) f :: k + | Oaddrsymbol s ofs, nil => + Paddis GPR12 GPR0 (Csymbol_high s ofs) :: + Paddi (ireg_of r) GPR12 (Csymbol_low s ofs) :: k + | Oaddrstack n, nil => + addimm (ireg_of r) GPR1 n k + | Ocast8signed, a1 :: nil => + Pextsb (ireg_of r) (ireg_of a1) :: k + | Ocast8unsigned, a1 :: nil => + Prlwinm (ireg_of r) (ireg_of a1) Int.zero (Int.repr 255) :: k + | Ocast16signed, a1 :: nil => + Pextsh (ireg_of r) (ireg_of a1) :: k + | Ocast16unsigned, a1 :: nil => + Prlwinm (ireg_of r) (ireg_of a1) Int.zero (Int.repr 65535) :: k + | Oadd, a1 :: a2 :: nil => + Padd (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oaddimm n, a1 :: nil => + addimm (ireg_of r) (ireg_of a1) n k + | Osub, a1 :: a2 :: nil => + Psubfc (ireg_of r) (ireg_of a2) (ireg_of a1) :: k + | Osubimm n, a1 :: nil => + if Int.eq (high_s n) Int.zero then + Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k + else + loadimm GPR12 n (Psubfc (ireg_of r) (ireg_of a1) GPR12 :: k) + | Omul, a1 :: a2 :: nil => + Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Omulimm n, a1 :: nil => + if Int.eq (high_s n) Int.zero then + Pmulli (ireg_of r) (ireg_of a1) (Cint n) :: k + else + loadimm GPR12 n (Pmullw (ireg_of r) (ireg_of a1) GPR12 :: k) + | Odiv, a1 :: a2 :: nil => + Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Odivu, a1 :: a2 :: nil => + Pdivwu (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oand, a1 :: a2 :: nil => + Pand_ (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oandimm n, a1 :: nil => + andimm (ireg_of r) (ireg_of a1) n k + | Oor, a1 :: a2 :: nil => + Por (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oorimm n, a1 :: nil => + orimm (ireg_of r) (ireg_of a1) n k + | Oxor, a1 :: a2 :: nil => + Pxor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oxorimm n, a1 :: nil => + xorimm (ireg_of r) (ireg_of a1) n k + | Onand, a1 :: a2 :: nil => + Pnand (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Onor, a1 :: a2 :: nil => + Pnor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Onxor, a1 :: a2 :: nil => + Peqv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oshl, a1 :: a2 :: nil => + Pslw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oshr, a1 :: a2 :: nil => + Psraw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oshrimm n, a1 :: nil => + Psrawi (ireg_of r) (ireg_of a1) n :: k + | Oshrximm n, a1 :: nil => + Psrawi (ireg_of r) (ireg_of a1) n :: + Paddze (ireg_of r) (ireg_of r) :: k + | Oshru, a1 :: a2 :: nil => + Psrw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Orolm amount mask, a1 :: nil => + Prlwinm (ireg_of r) (ireg_of a1) amount mask :: k + | Onegf, a1 :: nil => + Pfneg (freg_of r) (freg_of a1) :: k + | Oabsf, a1 :: nil => + Pfabs (freg_of r) (freg_of a1) :: k + | Oaddf, a1 :: a2 :: nil => + Pfadd (freg_of r) (freg_of a1) (freg_of a2) :: k + | Osubf, a1 :: a2 :: nil => + Pfsub (freg_of r) (freg_of a1) (freg_of a2) :: k + | Omulf, a1 :: a2 :: nil => + Pfmul (freg_of r) (freg_of a1) (freg_of a2) :: k + | Odivf, a1 :: a2 :: nil => + Pfdiv (freg_of r) (freg_of a1) (freg_of a2) :: k + | Omuladdf, a1 :: a2 :: a3 :: nil => + Pfmadd (freg_of r) (freg_of a1) (freg_of a2) (freg_of a3) :: k + | Omulsubf, a1 :: a2 :: a3 :: nil => + Pfmsub (freg_of r) (freg_of a1) (freg_of a2) (freg_of a3) :: k + | Osingleoffloat, a1 :: nil => + Pfrsp (freg_of r) (freg_of a1) :: k + | Ointoffloat, a1 :: nil => + Pfcti (ireg_of r) (freg_of a1) :: k + | Ointuoffloat, a1 :: nil => + Pfctiu (ireg_of r) (freg_of a1) :: k + | Ofloatofint, a1 :: nil => + Pictf (freg_of r) (ireg_of a1) :: k + | Ofloatofintu, a1 :: nil => + Piuctf (freg_of r) (ireg_of a1) :: k + | Ocmp cmp, _ => + let p := crbit_for_cond cmp in + transl_cond cmp args + (Pmfcrbit (ireg_of r) (fst p) :: + if snd p + then k + else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k) + | _, _ => + k (**r never happens for well-typed code *) + end. + +(** Common code to translate [Mload] and [Mstore] instructions. *) + +Definition transl_load_store + (mk1: constant -> ireg -> instruction) + (mk2: ireg -> ireg -> instruction) + (addr: addressing) (args: list mreg) (k: code) := + match addr, args with + | Aindexed ofs, a1 :: nil => + if ireg_eq (ireg_of a1) GPR0 then + Pmr GPR12 (ireg_of a1) :: + Paddis GPR12 GPR12 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) GPR12 :: k + else if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) (ireg_of a1) :: k + else + Paddis GPR12 (ireg_of a1) (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) GPR12 :: k + | Aindexed2, a1 :: a2 :: nil => + mk2 (ireg_of a1) (ireg_of a2) :: k + | Aglobal symb ofs, nil => + Paddis GPR12 GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR12 :: k + | Abased symb ofs, a1 :: nil => + if ireg_eq (ireg_of a1) GPR0 then + Pmr GPR12 (ireg_of a1) :: + Paddis GPR12 GPR12 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR12 :: k + else + Paddis GPR12 (ireg_of a1) (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR12 :: k + | Ainstack ofs, nil => + if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) GPR1 :: k + else + Paddis GPR12 GPR1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) GPR12 :: k + | _, _ => + (* should not happen *) k + end. + +(** Translation of a Mach instruction. *) + +Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := + match i with + | Mgetstack ofs ty dst => + loadind GPR1 ofs ty dst k + | Msetstack src ofs ty => + storeind src GPR1 ofs ty k + | Mgetparam ofs ty dst => + Plwz GPR12 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR12 ofs ty dst k + | Mop op args res => + transl_op op args res k + | Mload chunk addr args dst => + match chunk with + | Mint8signed => + transl_load_store + (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args + (Pextsb (ireg_of dst) (ireg_of dst) :: k) + | Mint8unsigned => + transl_load_store + (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args k + | Mint16signed => + transl_load_store + (Plha (ireg_of dst)) (Plhax (ireg_of dst)) addr args k + | Mint16unsigned => + transl_load_store + (Plhz (ireg_of dst)) (Plhzx (ireg_of dst)) addr args k + | Mint32 => + transl_load_store + (Plwz (ireg_of dst)) (Plwzx (ireg_of dst)) addr args k + | Mfloat32 => + transl_load_store + (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args k + | Mfloat64 => + transl_load_store + (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args k + end + | Mstore chunk addr args src => + match chunk with + | Mint8signed => + transl_load_store + (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args k + | Mint8unsigned => + transl_load_store + (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args k + | Mint16signed => + transl_load_store + (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args k + | Mint16unsigned => + transl_load_store + (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args k + | Mint32 => + transl_load_store + (Pstw (ireg_of src)) (Pstwx (ireg_of src)) addr args k + | Mfloat32 => + transl_load_store + (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args k + | Mfloat64 => + transl_load_store + (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args k + end + | Mcall sig (inl r) => + Pmtctr (ireg_of r) :: Pbctrl :: k + | Mcall sig (inr symb) => + Pbl symb :: k + | Mtailcall sig (inl r) => + Pmtctr (ireg_of r) :: + Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR12 :: + Pfreeframe f.(fn_link_ofs) :: + Pbctr :: k + | Mtailcall sig (inr symb) => + Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR12 :: + Pfreeframe f.(fn_link_ofs) :: + Pbs symb :: k + | Malloc => + Pallocblock :: k + | Mlabel lbl => + Plabel lbl :: k + | Mgoto lbl => + Pb lbl :: k + | Mcond cond args lbl => + let p := crbit_for_cond cond in + transl_cond cond args + (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) + | Mreturn => + Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR12 :: + Pfreeframe f.(fn_link_ofs) :: + Pblr :: k + end. + +Definition transl_code (f: Mach.function) (il: list Mach.instruction) := + List.fold_right (transl_instr f) nil il. + +(** 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 transl_function (f: Mach.function) := + Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pmflr GPR12 :: + Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + transl_code f f.(fn_code). + +Fixpoint code_size (c: code) : Z := + match c with + | nil => 0 + | instr :: c' => code_size c' + 1 + end. + +Open Local Scope string_scope. + +Definition transf_function (f: Mach.function) : res Asm.code := + let c := transl_function f in + if zlt Int.max_unsigned (code_size c) + then Errors.Error (msg "code size exceeded") + else Errors.OK c. + +Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Mach.program) : res Asm.program := + transform_partial_program transf_fundef p. + -- cgit