path: root/aarch64/TO_MERGE/Asmgen.v

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