path: root/riscV/Asmgen.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*           Prashanth Mundkur, SRI International                      *)
(*                                                                     *)
(*  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.     *)
(*                                                                     *)
(*  The contributions by Prashanth Mundkur are reused and adapted      *)
(*  under the terms of a Contributor License Agreement between         *)
(*  SRI International and INRIA.                                       *)
(*                                                                     *)
(* *********************************************************************)

(** Translation from Mach to RISC-V assembly language *)

Require Archi.
Require Import Coqlib Errors.
Require Import AST Integers Floats Memdata.
Require Import Op Locations Mach Asm.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.

Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.

(** The code generation functions take advantage of several
  characteristics of the [Mach] code generated by earlier passes of the
  compiler, mostly that argument and result registers are of the correct
  types.  These properties are true by construction, but it's easier to
  recheck them during code generation and fail if they do not hold. *)

(** 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.

(** Decomposition of 32-bit integer constants.  They are split into either
  small signed immediates that fit in 12-bits, or, if they do not fit,
  into a (20-bit hi, 12-bit lo) pair where lo is sign-extended. *)

Inductive immed32 : Type :=
  | Imm32_single (imm: int)
  | Imm32_pair   (hi: int) (lo: int).

Definition make_immed32 (val: int) :=
  let lo := Int.sign_ext 12 val in
  if Int.eq val lo
  then Imm32_single val
  else Imm32_pair (Int.shru (Int.sub val lo) (Int.repr 12)) lo.
(*
  let discr := Int.shr val (Int.repr 11) in
  let hi    := Int.shru val (Int.repr 12) in
  if Int.eq discr Int.zero || Int.eq discr Int.mone
  then Imm32_single val
  else Imm32_pair (Int.add hi (Int.and discr Int.one)) (Int.sign_ext 12 val).
*)

(** Likewise, for 64-bit integer constants. *)

Inductive immed64 : Type :=
  | Imm64_single (imm: int64)
  | Imm64_pair   (hi: int64) (lo: int64)
  | Imm64_large  (imm: int64).

Definition make_immed64 (val: int64) :=
  let lo := Int64.sign_ext 12 val in
  if Int64.eq val lo then Imm64_single lo else
  let hi := Int64.zero_ext 20 (Int64.shru (Int64.sub val lo) (Int64.repr 12)) in
  if Int64.eq val (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)
  then Imm64_pair hi lo
  else Imm64_large val.

(** Smart constructors for arithmetic operations involving
  a 32-bit or 64-bit integer constant.  Depending on whether the
  constant fits in 12 bits or not, one or several instructions
  are generated as required to perform the operation
  and prepended to the given instruction sequence [k]. *)

Definition load_hilo32 (r: ireg) (hi lo: int) k :=
  if Int.eq lo Int.zero then Pluiw r hi :: k
  else Pluiw r hi :: Paddiw r r lo :: k.

Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
                   (opimm: ireg -> ireg0 -> int -> instruction)
                   (rd rs: ireg) (n: int) (k: code) :=
  match make_immed32 n with
  | Imm32_single imm => opimm rd rs imm :: k
  | Imm32_pair hi lo => load_hilo32 X31 hi lo (op rd rs X31 :: k)
  end.

Definition addimm32 := opimm32 Paddw Paddiw.
  
Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
  if Int64.eq lo Int64.zero then Pluil r hi :: k
  else Pluil r hi :: Paddil r r lo :: k.

Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
                   (opimm: ireg -> ireg0 -> int64 -> instruction)
                   (rd rs: ireg) (n: int64) (k: code) :=
  match make_immed64 n with
  | Imm64_single imm => opimm rd rs imm :: k
  | Imm64_pair hi lo => load_hilo64 X31 hi lo (op rd rs X31 :: k)
  | Imm64_large imm  => Ploadli X31 imm :: op rd rs X31 :: k
  end.

Definition addimm64 := opimm64 Paddl Paddil.

Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
  if Ptrofs.eq_dec n Ptrofs.zero then
    Pmv rd rs :: k
  else
    if Archi.ptr64
    then addimm64 rd rs (Ptrofs.to_int64 n) k
    else addimm32 rd rs (Ptrofs.to_int n) k.
  
(** Functions to select a special register according to the op "oreg" argument from RTL *)

Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
  match optR with
  | None => (r1, r2)
  | Some X0_L => (X0, r1)
  | Some X0_R => (r1, X0)
  end. 

Definition get_oreg (optR: option oreg) (r: ireg0) :=
  match optR with
  | Some X0_L | Some X0_R => X0
  | _ => r
  end. 

Definition transl_cbranch
           (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
  match cond, args with
  | CEbeqw optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbeqw r1' r2' lbl :: k)
  | CEbnew optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbnew r1' r2' lbl :: k)
  | CEbequw optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbeqw r1' r2' lbl :: k)
  | CEbneuw optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbnew r1' r2' lbl :: k)
  | CEbltw optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbltw r1' r2' lbl :: k)
  | CEbltuw optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbltuw r1' r2' lbl :: k)
  | CEbgew optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbgew r1' r2' lbl :: k)
  | CEbgeuw optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbgeuw r1' r2' lbl :: k)
  | CEbeql optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbeql r1' r2' lbl :: k)
  | CEbnel optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbnel r1' r2' lbl :: k)
  | CEbequl optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbeql r1' r2' lbl :: k)
  | CEbneul optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbnel r1' r2' lbl :: k)
  | CEbltl optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbltl r1' r2' lbl :: k)
  | CEbltul optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbltul r1' r2' lbl :: k)
  | CEbgel optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbgel r1' r2' lbl :: k)
  | CEbgeul optR, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
      OK (Pbgeul r1' r2' lbl :: k)
  | _, _ =>
      Error(msg "Asmgen.transl_cond_branch")
  end.

(** Translation of the arithmetic operation [r <- op(args)].
  The corresponding instructions are prepended to [k]. *)
  
Definition transl_op
              (op: operation) (args: list mreg) (res: mreg) (k: code) :=
  match op, args with
  | Omove, a1 :: nil =>
      match preg_of res, preg_of a1 with
      | IR r, IR a => OK (Pmv r a :: k)
      | FR r, FR a => OK (Pfmv r a :: k)
      |  _  ,  _   => Error(msg "Asmgen.Omove")
      end
  | Oaddrsymbol s ofs, nil =>
      do rd <- ireg_of res;
      OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
          then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k
          else Ploadsymbol rd s ofs :: k)
  | Oaddrstack n, nil =>
      do rd <- ireg_of res;
      OK (addptrofs rd SP n k)

  | Oadd, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Paddw rd rs1 rs2 :: k)
  | Oneg, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Psubw rd X0 rs :: k)
  | Osub, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psubw rd rs1 rs2 :: k)
  | Omul, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmulw rd rs1 rs2 :: k)
  | Omulhs, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmulhw rd rs1 rs2 :: k)
  | Omulhu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmulhuw rd rs1 rs2 :: k)
  | Odiv, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pdivw rd rs1 rs2 :: k)
  | Odivu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pdivuw rd rs1 rs2 :: k)
  | Omod, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Premw rd rs1 rs2 :: k)
  | Omodu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Premuw rd rs1 rs2 :: k)
  | Oand, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pandw rd rs1 rs2 :: k)
  | Oor, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Porw rd rs1 rs2 :: k)
  | Oxor, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pxorw rd rs1 rs2 :: k)
  | Oshl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psllw rd rs1 rs2 :: k)
  | Oshlimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pslliw rd rs n :: k)
  | Oshr, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psraw rd rs1 rs2 :: k)
  | Oshrimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psraiw rd rs n :: k)
  | Oshru, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psrlw rd rs1 rs2 :: k)
  | Oshruimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrliw rd rs n :: k)
  (* [Omakelong], [Ohighlong]  should not occur *)
  | Olowlong, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pcvtl2w rd rs :: k)  
  | Ocast32signed, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      assertion (ireg_eq rd rs);
      OK (Pcvtw2l rd :: k)
  | Oaddl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Paddl rd rs1 rs2 :: k)
  | Onegl, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Psubl rd X0 rs :: k)
  | Osubl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psubl rd rs1 rs2 :: k)
  | Omull, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmull rd rs1 rs2 :: k)
  | Omullhs, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmulhl rd rs1 rs2 :: k)
  | Omullhu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmulhul rd rs1 rs2 :: k)
  | Odivl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pdivl rd rs1 rs2 :: k)
  | Odivlu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pdivul rd rs1 rs2 :: k)
  | Omodl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Preml rd rs1 rs2 :: k)
  | Omodlu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Premul rd rs1 rs2 :: k)
  | Oandl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pandl rd rs1 rs2 :: k)
  | Oorl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Porl rd rs1 rs2 :: k)
  | Oxorl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pxorl rd rs1 rs2 :: k)
  | Oshll, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pslll rd rs1 rs2 :: k)
  | Oshllimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psllil rd rs n :: k)
  | Oshrl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psral rd rs1 rs2 :: k)
  | Oshrlimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrail rd rs n :: k)
  | Oshrlu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Psrll rd rs1 rs2 :: k)
  | Oshrluimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrlil rd rs n :: k)
  | Onegf, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfnegd rd rs :: k)
  | Oabsf, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfabsd rd rs :: k)
  | Oaddf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfaddd rd rs1 rs2 :: k)
  | Osubf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfsubd rd rs1 rs2 :: k)
  | Omulf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmuld rd rs1 rs2 :: k)
  | Odivf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfdivd rd rs1 rs2 :: k)

  | Onegfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfnegs rd rs :: k)
  | Oabsfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfabss rd rs :: k)
  | Oaddfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfadds rd rs1 rs2 :: k)
  | Osubfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfsubs rd rs1 rs2 :: k)
  | Omulfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmuls rd rs1 rs2 :: k)
  | Odivfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfdivs 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)

  | Ointoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtwd rd rs :: k)
  | Ointuoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtwud rd rs :: k)
  | Ofloatofint, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtdw rd rs :: k)
  | Ofloatofintu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtdwu rd rs :: k)
  | Ointofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtws rd rs :: k)
  | Ointuofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtwus rd rs :: k)
  | Osingleofint, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtsw rd rs :: k)
  | Osingleofintu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtswu rd rs :: k)

  | Olongoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtld rd rs :: k)
  | Olonguoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtlud rd rs :: k)
  | Ofloatoflong, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtdl rd rs :: k)
  | Ofloatoflongu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtdlu rd rs :: k)
  | Olongofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtls rd rs :: k)
  | Olonguofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtlus rd rs :: k)
  | Osingleoflong, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtsl rd rs :: k)
  | Osingleoflongu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfcvtslu rd rs :: k)

  (* Instructions expanded in RTL *)
  | OEseqw optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Pseqw rd rs1' rs2' :: k)
  | OEsnew optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psnew rd rs1' rs2' :: k)
  | OEsequw optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Pseqw rd rs1' rs2' :: k)
  | OEsneuw optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psnew rd rs1' rs2' :: k)
  | OEsltw optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psltw rd rs1' rs2' :: k)
  | OEsltuw optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psltuw rd rs1' rs2' :: k)
  | OEsltiw n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Psltiw rd rs n :: k)
  | OEsltiuw n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Psltiuw rd rs n :: k)
  | OExoriw n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Pxoriw rd rs n :: k)
  | OEluiw n, nil =>
      do rd <- ireg_of res;
      OK (Pluiw rd n :: k)
  | OEaddiw optR n, nil =>
      do rd <- ireg_of res;
      let rs := get_oreg optR X0 in
      OK (Paddiw rd rs n :: k)
  | OEaddiw optR n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      let rs' := get_oreg optR rs in
      OK (Paddiw rd rs' n :: k)
  | OEandiw n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Pandiw rd rs n :: k)
  | OEoriw n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Poriw rd rs n :: k)
  | OEseql optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Pseql rd rs1' rs2' :: k)
  | OEsnel optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psnel rd rs1' rs2' :: k)
  | OEsequl optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Pseql rd rs1' rs2' :: k)
  | OEsneul optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psnel rd rs1' rs2' :: k)
  | OEsltl optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psltl rd rs1' rs2' :: k)
  | OEsltul optR, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
      OK (Psltul rd rs1' rs2' :: k)
  | OEsltil n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Psltil rd rs n :: k)
  | OEsltiul n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Psltiul rd rs n :: k)
  | OExoril n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Pxoril rd rs n :: k)
  | OEluil n, nil =>
      do rd <- ireg_of res;
      OK (Pluil rd n :: k)
  | OEaddil optR n, nil =>
      do rd <- ireg_of res;
      let rs := get_oreg optR X0 in
      OK (Paddil rd rs n :: k)
  | OEaddil optR n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      let rs' := get_oreg optR rs in
      OK (Paddil rd rs' n :: k)
  | OEandil n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Pandil rd rs n :: k)
  | OEoril n, a1 :: nil =>
      do rd <- ireg_of res;
      do rs <- ireg_of a1;
      OK (Poril rd rs n :: k)
  | OEloadli n, nil =>
      do rd <- ireg_of res;
      OK (Ploadli rd n :: k)
  | OEfeqd, f1 :: f2 :: nil =>
      do rd <- ireg_of res;
      do r1 <- freg_of f1;
      do r2 <- freg_of f2;
      OK (Pfeqd rd r1 r2 :: k)
  | OEfltd, f1 :: f2 :: nil =>
      do rd <- ireg_of res;
      do r1 <- freg_of f1;
      do r2 <- freg_of f2;
      OK (Pfltd rd r1 r2 :: k)
  | OEfled, f1 :: f2 :: nil =>
      do rd <- ireg_of res;
      do r1 <- freg_of f1;
      do r2 <- freg_of f2;
      OK (Pfled rd r1 r2 :: k)
  | OEfeqs, f1 :: f2 :: nil =>
      do rd <- ireg_of res;
      do r1 <- freg_of f1;
      do r2 <- freg_of f2;
      OK (Pfeqs rd r1 r2 :: k)
  | OEflts, f1 :: f2 :: nil =>
      do rd <- ireg_of res;
      do r1 <- freg_of f1;
      do r2 <- freg_of f2;
      OK (Pflts rd r1 r2 :: k)
  | OEfles, f1 :: f2 :: nil =>
      do rd <- ireg_of res;
      do r1 <- freg_of f1;
      do r2 <- freg_of f2;
      OK (Pfles rd r1 r2 :: k)
  | OEmayundef _, a1 :: a2 :: nil =>
      do rd <- ireg_of res;
      do r2 <- ireg_of a2;
      if ireg_eq rd r2 then
        OK (Pnop :: k)
      else
        OK (Pmv rd r2 :: k)

  | Obits_of_single, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfmvxs rd rs :: k)
  | Obits_of_float, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfmvxd rd rs :: k)
  | Osingle_of_bits, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfmvsx rd rs :: k)
  | Ofloat_of_bits, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfmvdx rd rs :: k)
  | Oselectl, b::t::f::nil =>
      do rd <- ireg_of res;
      do rb <- ireg_of b;
      do rt <- ireg_of t;
      do rf <- ireg_of f;
      OK (Pselectl rd rb rt rf :: k)
  | _, _ =>
      Error(msg "Asmgen.transl_op")
  end.

(** Accessing data in the stack frame. *)

Definition indexed_memory_access
        (mk_instr: ireg -> offset -> instruction)
        (base: ireg) (ofs: ptrofs) (k: code) :=
  if Archi.ptr64 then
    match make_immed64 (Ptrofs.to_int64 ofs) with
    | Imm64_single imm =>
        mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k
    | Imm64_pair hi lo =>
        Pluil X31 hi :: Paddl X31 base X31 :: mk_instr X31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
    | Imm64_large imm =>
        Ploadli X31 imm :: Paddl X31 base X31 :: mk_instr X31 (Ofsimm Ptrofs.zero) :: k
    end
  else
    match make_immed32 (Ptrofs.to_int ofs) with
    | Imm32_single imm =>
        mk_instr base (Ofsimm (Ptrofs.of_int imm)) :: k
    | Imm32_pair hi lo =>
        Pluiw X31 hi :: Paddw X31 base X31 :: mk_instr X31 (Ofsimm (Ptrofs.of_int lo)) :: k
    end.

Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
  match ty, preg_of dst with
  | Tint,    IR rd => OK (indexed_memory_access (Plw rd) base ofs k)
  | Tlong,   IR rd => OK (indexed_memory_access (Pld rd) base ofs k)
  | Tsingle, FR rd => OK (indexed_memory_access (Pfls rd) base ofs k)
  | Tfloat,  FR rd => OK (indexed_memory_access (Pfld rd) base ofs k)
  | Tany32,  IR rd => OK (indexed_memory_access (Plw_a rd) base ofs k)
  | Tany64,  IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k)
  | Tany64,  FR rd => OK (indexed_memory_access (Pfld_a rd) base ofs k)
  | _, _           => Error (msg "Asmgen.loadind")
  end.

Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :=
  match ty, preg_of src with
  | Tint,    IR rd => OK (indexed_memory_access (Psw rd) base ofs k)
  | Tlong,   IR rd => OK (indexed_memory_access (Psd rd) base ofs k)
  | Tsingle, FR rd => OK (indexed_memory_access (Pfss rd) base ofs k)
  | Tfloat,  FR rd => OK (indexed_memory_access (Pfsd rd) base ofs k)
  | Tany32,  IR rd => OK (indexed_memory_access (Psw_a rd) base ofs k)
  | Tany64,  IR rd => OK (indexed_memory_access (Psd_a rd) base ofs k)
  | Tany64,  FR rd => OK (indexed_memory_access (Pfsd_a rd) base ofs k)
  | _, _           => Error (msg "Asmgen.storeind")
  end.

Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) :=
  indexed_memory_access (if Archi.ptr64 then Pld dst else Plw dst) base ofs k.

Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) (k: code) :=
  indexed_memory_access (if Archi.ptr64 then Psd src else Psw src) base ofs k.

(** Translation of memory accesses: loads, and stores. *)

Definition transl_memory_access
     (mk_instr: ireg -> offset -> instruction)
     (addr: addressing) (args: list mreg) (k: code) :=
  match addr, args with
  | Aindexed ofs, a1 :: nil =>
      do rs <- ireg_of a1;
      OK (indexed_memory_access mk_instr rs ofs k)
  | Aglobal id ofs, nil =>
      OK (Ploadsymbol_high X31 id ofs :: mk_instr X31 (Ofslow id ofs) :: k)
  | Ainstack ofs, nil =>
      OK (indexed_memory_access mk_instr SP ofs k)
  | _, _ =>
      Error(msg "Asmgen.transl_memory_access")
  end.

Definition transl_load (trap : trapping_mode)
           (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (dst: mreg) (k: code) :=
  match trap with
  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm")
  | TRAP =>
    match chunk with
  | Mint8signed =>
      do r <- ireg_of dst;
      transl_memory_access (Plb r)  addr args k
  | Mint8unsigned =>
      do r <- ireg_of dst;
      transl_memory_access (Plbu r) addr args k
  | Mint16signed =>
      do r <- ireg_of dst;
      transl_memory_access (Plh r)  addr args k
  | Mint16unsigned =>
      do r <- ireg_of dst;
      transl_memory_access (Plhu r) addr args k
  | Mint32 =>
      do r <- ireg_of dst;
      transl_memory_access (Plw r)  addr args k
  | Mint64 =>
      do r <- ireg_of dst;
      transl_memory_access (Pld r)  addr args k
  | Mfloat32 =>
      do r <- freg_of dst;
      transl_memory_access (Pfls r) addr args k
  | Mfloat64 =>
      do r <- freg_of dst;
      transl_memory_access (Pfld r) addr args k
  | _ =>
      Error (msg "Asmgen.transl_load")
    end
  end.

Definition transl_store (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (src: mreg) (k: code) :=
  match chunk with
  | Mint8signed | Mint8unsigned =>
      do r <- ireg_of src;
      transl_memory_access (Psb r)  addr args k
  | Mint16signed | Mint16unsigned =>
      do r <- ireg_of src;
      transl_memory_access (Psh r)  addr args k
  | Mint32 =>
      do r <- ireg_of src;
      transl_memory_access (Psw r)  addr args k
  | Mint64 =>
      do r <- ireg_of src;
      transl_memory_access (Psd r)  addr args k
  | Mfloat32 =>
      do r <- freg_of src;
      transl_memory_access (Pfss r) addr args k
  | Mfloat64 =>
      do r <- freg_of src;
      transl_memory_access (Pfsd r) addr args k
  | _ =>
      Error (msg "Asmgen.transl_store")
  end.

(** Function epilogue *)

Definition make_epilogue (f: Mach.function) (k: code) :=
  loadind_ptr SP f.(fn_retaddr_ofs) RA
    (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).

(** Translation of a Mach instruction. *)

Definition transl_instr (f: Mach.function) (i: Mach.instruction)
                        (ep: bool) (k: code) :=
  match i with
  | Mgetstack ofs ty dst =>
      loadind SP ofs ty dst k
  | Msetstack src ofs ty =>
      storeind src SP ofs ty k
  | Mgetparam ofs ty dst =>
      (* load via the frame pointer if it is valid *)
      do c <- loadind X30 ofs ty dst k;
      OK (if ep then c
                else loadind_ptr SP f.(fn_link_ofs) X30 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 (Pjal_r r1 sig :: k)
  | Mcall sig (inr symb) =>
      OK (Pjal_s symb sig :: k)
  | Mtailcall sig (inl r) =>
      do r1 <- ireg_of r;
      OK (make_epilogue f (Pj_r r1 sig :: k))
  | Mtailcall sig (inr symb) =>
      OK (make_epilogue f (Pj_s 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 (Pj_l lbl :: k)
  | Mcond cond args lbl =>
      transl_cbranch cond args lbl k
  | Mjumptable arg tbl =>
      do r <- ireg_of arg;
      OK (Pbtbl r tbl :: k)
  | Mreturn =>
      OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: 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 R30)
  | Mop op args res => before && negb (mreg_eq res R30)
  | _ => 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) :=
  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
  end.

(** This is an equivalent definition in continuation-passing style
  that runs in constant stack space. *)

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.

Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) :=
  transl_code_rec f il it1p (fun c => OK c).

(** 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) :=
  do c <- transl_code' f f.(Mach.fn_code) true;
  OK (mkfunction f.(Mach.fn_sig)
        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
         storeind_ptr RA SP f.(fn_retaddr_ofs) c)).

Definition transf_function (f: Mach.function) : res Asm.function :=
  do tf <- transl_function f;
  if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code))
  then Error (msg "code size exceeded")
  else OK tf.

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.