path: root/kvx/Asmblockgen.v

(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(** * Translation from Machblock to KVX assembly language (Asmblock) 
    Inspired from the Mach->Asm pass of other backends, but adapted to the block structure *)

Require Archi.
Require Import Coqlib Errors.
Require Import AST Integers Floats Memdata.
Require Import Op Locations Machblock Asmvliw Asmblock.
Require ExtValues.
Require Import Chunks.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.

Import PArithCoercions.

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

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

Definition make_immed32 (val: int) := Imm32_single val.

Inductive immed64 : Type :=
  | Imm64_single (imm: int64)
.

Definition make_immed64 (val: int64) := Imm64_single val.

Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity).
Notation "a ::i b" := (cons (A:=basic) a b) (at level 49, right associativity).
Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associativity).
Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity).
Notation "a @@ b" := (app a b) (at level 49, right associativity).

Definition loadimm32 (r: ireg) (n: int) :=
  match make_immed32 n with
  | Imm32_single imm => Pmake r imm
  end.

Definition opimm32 (op: arith_name_rrr)
                   (opimm: arith_name_rri32)
                   (rd rs: ireg) (n: int) :=
  match make_immed32 n with
  | Imm32_single imm => opimm rd rs imm
  end.

Definition addimm32 := opimm32 Paddw Paddiw.
Definition mulimm32 := opimm32 Pmulw Pmuliw.
Definition andimm32 := opimm32 Pandw Pandiw.
Definition nandimm32 := opimm32 Pnandw Pnandiw.
Definition orimm32  := opimm32 Porw Poriw.
Definition norimm32 := opimm32 Pnorw Pnoriw.
Definition xorimm32 := opimm32 Pxorw Pxoriw.
Definition nxorimm32 := opimm32 Pnxorw Pnxoriw.

Definition loadimm64 (r: ireg) (n: int64) :=
  match make_immed64 n with
  | Imm64_single imm => Pmakel r imm
  end.

Definition opimm64 (op: arith_name_rrr)
                   (opimm: arith_name_rri64)
                   (rd rs: ireg) (n: int64) :=
  match make_immed64 n with
  | Imm64_single imm => opimm rd rs imm
end.

Definition addimm64 := opimm64 Paddl Paddil.
Definition mulimm64 := opimm64 Pmull Pmulil.
Definition orimm64  := opimm64 Porl  Poril.
Definition andimm64 := opimm64 Pandl Pandil.
Definition xorimm64 := opimm64 Pxorl  Pxoril.
Definition norimm64  := opimm64 Pnorl  Pnoril.
Definition nandimm64 := opimm64 Pnandl Pnandil.
Definition nxorimm64 := opimm64 Pnxorl  Pnxoril.

Definition addptrofs (rd rs: ireg) (n: ptrofs) :=
  if Ptrofs.eq_dec n Ptrofs.zero then
    Pmv rd rs
  else
    addimm64 rd rs (Ptrofs.to_int64 n).

(** Translation of conditional branches. *)

Definition transl_comp
    (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
  Pcompw (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k.

Definition transl_compi
    (c: comparison) (s: signedness) (r: ireg) (imm: int) (lbl: label) (k: code) : list instruction :=
  Pcompiw (itest_for_cmp c s) RTMP r imm ::g Pcb BTwnez RTMP lbl ::g k.

Definition transl_compl
    (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
  Pcompl (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k.

Definition transl_compil
    (c: comparison) (s: signedness) (r: ireg) (imm: int64) (lbl: label) (k: code) : list instruction :=
  Pcompil (itest_for_cmp c s) RTMP r imm ::g Pcb BTwnez RTMP lbl ::g k.

Definition select_comp (n: int) (c: comparison) : option comparison :=
  if Int.eq n Int.zero then
    match c with
    | Ceq => Some Ceq
    | Cne => Some Cne
    | _   => None
    end
  else
    None
  .

Definition transl_opt_compuimm
    (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
  if Int.eq n Int.zero then
    match c with
    | Ceq => Pcbu BTweqz r1 lbl ::g k
    | Cne => Pcbu BTwnez r1 lbl ::g k
    | _ => transl_compi c Unsigned r1 n lbl k
    end
  else
    transl_compi c Unsigned r1 n lbl k
  .

Definition select_compl (n: int64) (c: comparison) : option comparison :=
  if Int64.eq n Int64.zero then
    match c with
    | Ceq => Some Ceq
    | Cne => Some Cne
    | _   => None
    end
  else
    None
  .

Definition transl_opt_compluimm
    (n: int64) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
  if Int64.eq n Int64.zero then
    match c with
    | Ceq => Pcbu BTdeqz r1 lbl ::g k
    | Cne => Pcbu BTdnez r1 lbl ::g k
    | _ => transl_compil c Unsigned r1 n lbl k
    end
  else
    transl_compil c Unsigned r1 n lbl k
  .

Definition transl_comp_float32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
  match ftest_for_cmp cmp with
  | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
  | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
  end.

Definition transl_comp_notfloat32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
  match notftest_for_cmp cmp with
  | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
  | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
  end.

Definition transl_comp_float64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
  match ftest_for_cmp cmp with
  | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
  | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
  end.

Definition transl_comp_notfloat64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
  match notftest_for_cmp cmp with
  | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
  | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
  end.

Definition transl_cbranch
    (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
  match cond, args with
  | Ccompuimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (transl_opt_compuimm n c r1 lbl k)
  | Ccomp c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_comp c Signed r1 r2 lbl k)
  | Ccompu c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_comp c Unsigned r1 r2 lbl k)
  | Ccompimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if Int.eq n Int.zero then
            Pcb (btest_for_cmpswz c) r1 lbl ::g k
          else
            transl_compi c Signed r1 n lbl k
         )
  | Ccompluimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (transl_opt_compluimm n c r1 lbl k)
  | Ccompl c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_compl c Signed r1 r2 lbl k)
  | Ccomplu c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_compl c Unsigned r1 r2 lbl k)
  | Ccomplimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if Int64.eq n Int64.zero then
            Pcb (btest_for_cmpsdz c) r1 lbl ::g k
          else
            transl_compil c Signed r1 n lbl k
         )
  | Ccompf c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_comp_float64 c r1 r2 lbl k)
  | Cnotcompf c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_comp_notfloat64 c r1 r2 lbl k)
  | Ccompfs c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_comp_float32 c r1 r2 lbl k)
  | Cnotcompfs c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_comp_notfloat32 c r1 r2 lbl k)
  | _, _ =>
      Error(msg "Asmgenblock.transl_cbranch")
  end.

(** Translation of a condition operator.  The generated code sets the
  [rd] target register to 0 or 1 depending on the truth value of the
  condition. *)

Definition transl_cond_int32s (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  Pcompw (itest_for_cmp cmp Signed) rd r1 r2 ::i k.

Definition transl_cond_int32u (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  Pcompw (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k.

Definition transl_cond_int64s (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  Pcompl (itest_for_cmp cmp Signed) rd r1 r2 ::i k.

Definition transl_cond_int64u (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  Pcompl (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k.

Definition transl_condimm_int32s (cmp: comparison) (rd r1: ireg) (n: int) (k: bcode) :=
  Pcompiw (itest_for_cmp cmp Signed) rd r1 n ::i k.

Definition transl_condimm_int32u (cmp: comparison) (rd r1: ireg) (n: int) (k: bcode) :=
  Pcompiw (itest_for_cmp cmp Unsigned) rd r1 n ::i k.

Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) :=
  Pcompil (itest_for_cmp cmp Signed) rd r1 n ::i k.

Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) :=
  Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k.


Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  match ftest_for_cmp cmp with
  | Normal ft => Pfcompw ft rd r1 r2 ::i k
  | Reversed ft => Pfcompw ft rd r2 r1 ::i k
  end.

Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  match notftest_for_cmp cmp with
  | Normal ft => Pfcompw ft rd r1 r2 ::i k
  | Reversed ft => Pfcompw ft rd r2 r1 ::i k
  end.

Definition transl_cond_float64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  match ftest_for_cmp cmp with
  | Normal ft => Pfcompl ft rd r1 r2 ::i k
  | Reversed ft => Pfcompl ft rd r2 r1 ::i k
  end.

Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
  match notftest_for_cmp cmp with
  | Normal ft => Pfcompl ft rd r1 r2 ::i k
  | Reversed ft => Pfcompl ft rd r2 r1 ::i k
  end.


(* CoMPare Unsigned Words to Zero *)
Definition btest_for_cmpuwz (c: comparison) :=
  match c with
  | Cne => OK BTwnez
  | Ceq => OK BTweqz
  | Clt => Error (msg "btest_for_compuwz: Clt") (* TODO reachable *)
  | Cge => Error (msg "btest_for_compuwz: Cge")
  | Cle => OK BTweqz
  | Cgt => OK BTwnez
  end.

(* CoMPare Unsigned Words to Zero *)
Definition btest_for_cmpudz (c: comparison) :=
  match c with
  | Cne => OK BTdnez
  | Ceq => OK BTdeqz
  | Clt => Error (msg "btest_for_compudz: Clt")
  | Cge => Error (msg "btest_for_compudz: Cge")
  | Cle => OK BTdeqz
  | Cgt => OK BTdnez
  end.

Definition conditional_move (cond0 : condition0) (rc rd rs : ireg) :
  res basic :=
  if ireg_eq rd rs
  then OK Pnop
  else
    (match cond0 with
     | Ccomp0 cmp =>
       OK (PArith (Pcmove (btest_for_cmpswz cmp) rd rc rs))
     | Ccompu0 cmp =>
       do bt <- btest_for_cmpuwz cmp;
         OK (PArith (Pcmoveu bt rd rc rs))
     | Ccompl0 cmp =>
       OK (PArith (Pcmove (btest_for_cmpsdz cmp) rd rc rs))
     | Ccomplu0 cmp =>
       do bt <- btest_for_cmpudz cmp;
         OK (PArith (Pcmoveu bt rd rc rs))
     end).

Definition conditional_move_imm32 (cond0 : condition0) (rc rd : ireg) (imm : int) : res basic :=
  match cond0 with
  | Ccomp0 cmp =>
    OK (PArith (Pcmoveiw (btest_for_cmpswz cmp) rd rc imm))
  | Ccompu0 cmp =>
    do bt <- btest_for_cmpuwz cmp;
      OK (PArith (Pcmoveuiw bt rd rc imm))
  | Ccompl0 cmp =>
    OK (PArith (Pcmoveiw (btest_for_cmpsdz cmp) rd rc imm))
  | Ccomplu0 cmp =>
    do bt <- btest_for_cmpudz cmp;
      OK (PArith (Pcmoveuiw bt rd rc imm))
  end.

Definition conditional_move_imm64 (cond0 : condition0) (rc rd : ireg) (imm : int64) : res basic :=
  match cond0 with
  | Ccomp0 cmp =>
    OK (PArith (Pcmoveil (btest_for_cmpswz cmp) rd rc imm))
  | Ccompu0 cmp =>
    do bt <- btest_for_cmpuwz cmp;
      OK (PArith (Pcmoveuil bt rd rc imm))
  | Ccompl0 cmp =>
    OK (PArith (Pcmoveil (btest_for_cmpsdz cmp) rd rc imm))
  | Ccomplu0 cmp =>
    do bt <- btest_for_cmpudz cmp;
      OK (PArith (Pcmoveuil bt rd rc imm))
  end.

Definition transl_cond_op
           (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) :=
  match cond, args with
  | Ccomp c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_int32s c rd r1 r2 k)
  | Ccompu c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_int32u c rd r1 r2 k)
  | Ccompimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (transl_condimm_int32s c rd r1 n k)
  | Ccompuimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (transl_condimm_int32u c rd r1 n k)
  | Ccompl c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_int64s c rd r1 r2 k)
  | Ccomplu c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_int64u c rd r1 r2 k)
  | Ccomplimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (transl_condimm_int64s c rd r1 n k)
  | Ccompluimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (transl_condimm_int64u c rd r1 n k)
  | Ccompfs c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_float32 c rd r1 r2 k)
  | Cnotcompfs c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_notfloat32 c rd r1 r2 k)
  | Ccompf c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_float64 c rd r1 r2 k)
  | Cnotcompf c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (transl_cond_notfloat64 c rd r1 r2 k)
  | _, _ =>
      Error(msg "Asmblockgen.transl_cond_op")
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: bcode) :=
  match op, args with
  | Omove, a1 :: nil =>
      match preg_of res, preg_of a1 with
      | IR r, IR a => OK (Pmv r a ::i k)
      |  _  ,  _   => Error(msg "Asmgenblock.transl_op: Omove")
      end
  | Ointconst n, nil =>
      do rd <- ireg_of res;
      OK (loadimm32 rd n ::i k)
  | Olongconst n, nil =>
      do rd <- ireg_of res;
      OK (loadimm64 rd n ::i k)
  | Ofloatconst f, nil =>
      do rd <- freg_of res;
      OK (Pmakef rd f ::i k)
  | Osingleconst f, nil =>
      do rd <- freg_of res;
      OK (Pmakefs rd f ::i k)
  | Oaddrsymbol s ofs, nil =>
      do rd <- ireg_of res;
      OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
          then Ploadsymbol s Ptrofs.zero rd ::i addptrofs rd rd ofs ::i k
          else Ploadsymbol s ofs rd ::i k)
  | Oaddrstack n, nil =>
      do rd <- ireg_of res;
      OK (addptrofs rd SP n ::i k)

  | Ocast8signed, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pslliw rd rs (Int.repr 24) ::i Psraiw rd rd (Int.repr 24) ::i k)
  | Ocast16signed, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pslliw rd rs (Int.repr 16) ::i Psraiw rd rd (Int.repr 16) ::i 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 ::i k)
  | Oaddimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (addimm32 rd rs n ::i k)
  | Oaddx shift, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Paddxw shift rd rs1 rs2 ::i k)
  | Oaddximm shift n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Paddxiw shift rd rs n ::i k)
  | Oaddxl shift, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Paddxl shift rd rs1 rs2 ::i k)
  | Oaddxlimm shift n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Paddxil shift rd rs n ::i k)
  | Oneg, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pnegw rd rs ::i 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 ::i k)
  | Orevsubimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Prevsubiw rd rs n ::i k)
  | Orevsubx shift, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Prevsubxw shift rd rs1 rs2 ::i k)
  | Orevsubximm shift n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Prevsubxiw shift rd rs n ::i 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 ::i k)
  | Omulimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1;
      OK (mulimm32 rd rs1 n ::i k)
  | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *)
  | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *)
  | Oand, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pandw rd rs1 rs2 ::i k)
  | Oandimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (andimm32 rd rs n ::i k)
  | Onand, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pnandw rd rs1 rs2 ::i k)
  | Onandimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (nandimm32 rd rs n ::i 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 ::i k)
  | Onor, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pnorw rd rs1 rs2 ::i k)
  | Oorimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (orimm32 rd rs n ::i k)
  | Onorimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (norimm32 rd rs n ::i 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 ::i k)
  | Oxorimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (xorimm32 rd rs n ::i k)
  | Onxor, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pnxorw rd rs1 rs2 ::i k)
  | Onxorimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
        OK (nxorimm32 rd rs n ::i k)
  | Onot, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
        OK (xorimm32 rd rs Int.mone ::i k)
  | Oandn, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pandnw rd rs1 rs2 ::i k)
  | Oandnimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pandniw rd rs n ::i k)
  | Oorn, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pornw rd rs1 rs2 ::i k)
  | Oornimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Porniw rd rs n ::i k)
  | Oabsdiff, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pabdw rd rs1 rs2 ::i k)
  | Oabsdiffimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pabdiw rd rs n ::i 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 ::i k)
  | Oshlimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pslliw rd rs n ::i 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 ::i k)
  | Oshrimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psraiw rd rs n ::i 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 ::i k)
  | Oshruimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrliw rd rs n ::i k)
  | Oshrximm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrxiw rd rs n ::i k)
  | Ororimm n, a1 :: nil =>
    do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Proriw rd rs n ::i k)
  | Omadd, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
      do r3 <- ireg_of a3;
        OK (Pmaddw r1 r2 r3 ::i k)
  | Omaddimm n, a1 :: a2 :: nil =>
    assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
        OK (Pmaddiw r1 r2 n ::i k)
  | Omsub, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
      do r3 <- ireg_of a3;
        OK (Pmsubw r1 r2 r3 ::i k)
  (* [Omakelong], [Ohighlong]  should not occur *)
  | Olowlong, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pcvtl2w rd rs ::i k)  
  | Ocast32signed, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psxwd rd rs ::i k)
  | Ocast32unsigned, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Pzxwd rd rs ::i k)
(*       assertion (ireg_eq rd rs);
      OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i 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 ::i k)
  | Oaddlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (addimm64 rd rs n ::i k)
  | Onegl, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pnegl rd rs ::i 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 ::i k)
  | Orevsubxl shift, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Prevsubxl shift rd rs1 rs2 ::i k)
  | Orevsublimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Prevsubil rd rs n ::i k)
  | Orevsubxlimm shift n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Prevsubxil shift rd rs n ::i 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 ::i k)
  | Omullimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1;
      OK (mulimm64 rd rs1 n ::i k)
  | Omullhs, _ => Error (msg "Asmblockgen.transl_op: Omullhs") (* Normalement pas émis *)
  | Omullhu, _ => Error (msg "Asmblockgen.transl_op: Omullhu") (* Normalement pas émis *)
  | Odivl, _ => Error (msg "Asmblockgen.transl_op: Odivl") (* Géré par fonction externe *)
  | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu") (* Géré par fonction externe *)
  | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl") (* Géré par fonction externe *)
  | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu") (* Géré par fonction externe *)
  | Onotl, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
        OK (xorimm64 rd rs Int64.mone ::i 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 ::i k)
  | Oandlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (andimm64 rd rs n ::i k)
  | Onandl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pnandl rd rs1 rs2 ::i k)
  | Onandlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (nandimm64 rd rs n ::i 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 ::i k)
  | Oorlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (orimm64 rd rs n ::i k)
  | Onorl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pnorl rd rs1 rs2 ::i k)
  | Onorlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (norimm64 rd rs n ::i 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 ::i k)
  | Oxorlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (xorimm64 rd rs n ::i k)
  | Onxorl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pnxorl rd rs1 rs2 ::i k)
  | Onxorlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (nxorimm64 rd rs n ::i k)
  | Oandnl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pandnl rd rs1 rs2 ::i k)
  | Oandnlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pandnil rd rs n ::i k)
  | Oornl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pornl rd rs1 rs2 ::i k)
  | Oornlimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pornil rd rs n ::i k)
  | Oabsdiffl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pabdl rd rs1 rs2 ::i k)
  | Oabsdifflimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pabdil rd rs n ::i 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 ::i k)
  | Oshllimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psllil rd rs n ::i 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 ::i k)
  | Oshrlimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrail rd rs n ::i 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 ::i k)
  | Oshrluimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrlil rd rs n ::i k)
  | Oshrxlimm n, a1 :: nil =>
      do rd <- ireg_of res; do rs <- ireg_of a1;
      OK (Psrxil rd rs n ::i k)
  | Omaddl, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
      do r3 <- ireg_of a3;
        OK (Pmaddl r1 r2 r3 ::i k)
  | Omaddlimm n, a1 :: a2 :: nil =>
    assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
        OK (Pmaddil r1 r2 n ::i k)
  | Omsubl, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
      do r3 <- ireg_of a3;
        OK (Pmsubl r1 r2 r3 ::i k)
  | Oabsf, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfabsd rd rs ::i k)
  | Oabsfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfabsw rd rs ::i 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 ::i k)
  | Oaddfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfaddw rd rs1 rs2 ::i k)
  | Osubf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfsbfd rd rs1 rs2 ::i k)
  | Osubfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfsbfw rd rs1 rs2 ::i 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 ::i k)
  | Omulfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmulw rd rs1 rs2 ::i k)
  | Ominf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmind rd rs1 rs2 ::i k)
  | Ominfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfminw rd rs1 rs2 ::i k)
  | Omaxf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmaxd rd rs1 rs2 ::i k)
  | Omaxfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmaxw rd rs1 rs2 ::i k)
  | Onegf, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfnegd rd rs ::i k)
  | Onegfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfnegw rd rs ::i k)
  | Oinvfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfinvw rd rs ::i k)

  | Ofmaddf, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
        do rs1 <- freg_of a1;
        do rs2 <- freg_of a2;
        do rs3 <- freg_of a3;
      OK (Pfmaddfl rs1 rs2 rs3 ::i k)
  | Ofmaddfs, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
        do rs1 <- freg_of a1;
        do rs2 <- freg_of a2;
        do rs3 <- freg_of a3;
      OK (Pfmaddfw rs1 rs2 rs3 ::i k)
  | Ofmsubf, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
        do rs1 <- freg_of a1;
        do rs2 <- freg_of a2;
        do rs3 <- freg_of a3;
      OK (Pfmsubfl rs1 rs2 rs3 ::i k)
  | Ofmsubfs, a1 :: a2 :: a3 :: nil =>
    assertion (mreg_eq a1 res);
        do rs1 <- freg_of a1;
        do rs2 <- freg_of a2;
        do rs3 <- freg_of a3;
      OK (Pfmsubfw rs1 rs2 rs3 ::i k)

  | Osingleofint, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfloatwrnsz rd rs ::i k)
  | Osingleofintu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfloatuwrnsz rd rs ::i k)
  | Ofloatoflong, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfloatdrnsz rd rs ::i k)
  | Ofloatoflongu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pfloatudrnsz rd rs ::i k)
  | Ointofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixedwrzz rd rs ::i k)
  | Ointuofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixeduwrzz rd rs ::i k)
  | Ointofsingle_ne, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixedwrne rd rs ::i k)
  | Ointuofsingle_ne, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixeduwrne rd rs ::i k)
  | Olongoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixeddrzz rd rs ::i k)
  | Ointoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixeddrzz_i32 rd rs ::i k)
  | Ointuoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixedudrzz_i32 rd rs ::i k)
  | Olonguoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixedudrzz rd rs ::i k)
  | Olongoffloat_ne, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixeddrne rd rs ::i k)
  | Olonguoffloat_ne, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfixedudrne rd rs ::i k)

  | Ofloatofsingle, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfwidenlwd rd rs ::i k)
  | Osingleoffloat, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfnarrowdw rd rs ::i k)


  | Odivf , _ => Error (msg "Asmblockgen.transl_op: Odivf")
  | Odivfs, _ => Error (msg "Asmblockgen.transl_op: Odivfs")

  (* We use the Splitlong instead for these four conversions *)
  | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") 
  | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu")
  | Olongofsingle , _ => Error (msg "Asmblockgen.transl_op: Olongofsingle")
  | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle")


  | Ocmp cmp, _ =>
      do rd <- ireg_of res;
      transl_cond_op cmp rd args k


  | Oextfz stop start, a1 :: nil =>
    assertion (ExtValues.is_bitfield stop start);
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pextfz stop start rd rs ::i k)

  | Oextfs stop start, a1 :: nil =>
    assertion (ExtValues.is_bitfield stop start);
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pextfs stop start rd rs ::i k)

  | Oextfzl stop start, a1 :: nil =>
    assertion (ExtValues.is_bitfieldl stop start);
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pextfzl stop start rd rs ::i k)

  | Oextfsl stop start, a1 :: nil =>
    assertion (ExtValues.is_bitfieldl stop start);
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pextfsl stop start rd rs ::i k)
    
  | Oinsf stop start, a0 :: a1 :: nil =>
    assertion (ExtValues.is_bitfield stop start);
    assertion (mreg_eq a0 res);
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pinsf stop start rd rs ::i k)
    
  | Oinsfl stop start, a0 :: a1 :: nil =>
    assertion (ExtValues.is_bitfieldl stop start);
    assertion (mreg_eq a0 res);
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (Pinsfl stop start rd rs ::i k)

  | Osel cond0 ty, aT :: aF :: aC :: nil =>
    assertion (mreg_eq aT res);
      do rT <- ireg_of aT;
      do rF <- ireg_of aF;
      do rC <- ireg_of aC;
      do op <- conditional_move (negate_condition0 cond0) rC rT rF;
      OK (op ::i k)

  | Oselimm cond0 imm, aT :: aC :: nil =>
    assertion (mreg_eq aT res);
      do rT <- ireg_of aT;
      do rC <- ireg_of aC;
      do op <- conditional_move_imm32 (negate_condition0 cond0) rC rT imm;
      OK (op ::i k)
      

  | Osellimm cond0 imm, aT :: aC :: nil =>
    assertion (mreg_eq aT res);
      do rT <- ireg_of aT;
      do rC <- ireg_of aC;
      do op <- conditional_move_imm64 (negate_condition0 cond0) rC rT imm;
      OK (op ::i k)
         
  | _, _ =>
      Error(msg "Asmgenblock.transl_op")
  end.

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

Definition indexed_memory_access
        (mk_instr: ireg -> offset -> basic)
        (base: ireg) (ofs: ptrofs) :=
  match make_immed64 (Ptrofs.to_int64 ofs) with
  | Imm64_single imm =>
      mk_instr base (Ptrofs.of_int64 imm)
end.

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

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

Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) :=
  indexed_memory_access (PLoadRRO TRAP Pld dst) base ofs.

Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) :=
  indexed_memory_access (PStoreRRO Psd src) base ofs.

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

Definition transl_memory_access2
     (mk_instr: ireg -> ireg -> basic)
     (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
  match addr, args with
  | Aindexed2, a1 :: a2 :: nil =>
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      OK (mk_instr rs1 rs2 ::i k)
  | _, _ => Error (msg "Asmblockgen.transl_memory_access2")
  end.

Definition transl_memory_access2XS
     (chunk: memory_chunk)
     (mk_instr: ireg -> ireg -> basic)
     scale (args: list mreg) (k: bcode) : res bcode :=
  match args with
  | (a1 :: a2 :: nil) =>
      assertion (Z.eqb (zscale_of_chunk chunk) scale);
      do rs1 <- ireg_of a1;
      do rs2 <- ireg_of a2;
      OK (mk_instr rs1 rs2 ::i k)
  | _ => Error (msg "Asmblockgen.transl_memory_access2XS")
  end.

Definition transl_memory_access
     (mk_instr: ireg -> offset -> basic)
     (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
  match addr, args with
  | Aindexed ofs, a1 :: nil =>
      do rs <- ireg_of a1;
      OK (indexed_memory_access mk_instr rs ofs ::i k)
  | Aglobal id ofs, nil =>
      OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP Ptrofs.zero ::i k))
  | Ainstack ofs, nil =>
      OK (indexed_memory_access mk_instr SP ofs ::i k)
  | _, _ =>
      Error(msg "Asmblockgen.transl_memory_access")
  end.

Definition chunk2load (chunk: memory_chunk) :=
  match chunk with
  | Mint8signed => Plb
  | Mint8unsigned => Plbu
  | Mint16signed => Plh
  | Mint16unsigned => Plhu
  | Mint32 => Plw
  | Mint64 => Pld
  | Mfloat32 => Pfls
  | Mfloat64 => Pfld
  | Many32 => Plw_a
  | Many64 => Pld_a
  end.

Definition transl_load_rro (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
  do r <- ireg_of dst;
  transl_memory_access (PLoadRRO trap (chunk2load chunk) r) addr args k.

Definition transl_load_rrr (trap: trapping_mode)  (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
  do r <- ireg_of dst;
  transl_memory_access2 (PLoadRRR trap (chunk2load chunk) r) addr args k.

Definition transl_load_rrrXS (trap: trapping_mode) (chunk: memory_chunk) (scale : Z)
           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
  do r <- ireg_of dst;
  transl_memory_access2XS chunk (PLoadRRRXS trap (chunk2load chunk) r) scale args k.

Definition transl_load (trap : trapping_mode)
           (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
  match addr with
    | Aindexed2XS scale => transl_load_rrrXS trap chunk scale args dst k
    | Aindexed2 => transl_load_rrr trap chunk addr args dst k
    | _ => transl_load_rro trap chunk addr args dst k
  end.

Definition chunk2store (chunk: memory_chunk) :=
  match chunk with
  | Mint8signed | Mint8unsigned => Psb
  | Mint16signed | Mint16unsigned => Psh
  | Mint32 => Psw
  | Mint64 => Psd
  | Mfloat32 => Pfss
  | Mfloat64 => Pfsd
  | Many32 => Psw_a
  | Many64 => Psd_a
  end.

Definition transl_store_rro (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
  do r <- ireg_of src;
  transl_memory_access (PStoreRRO (chunk2store chunk) r) addr args k.

Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
  do r <- ireg_of src;
  transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k.

Definition transl_store_rrrxs (chunk: memory_chunk) (scale: Z)
           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
  do r <- ireg_of src;
  transl_memory_access2XS chunk (PStoreRRRXS (chunk2store chunk) r) scale args k.

Definition transl_store (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
  match addr with
  | Aindexed2 => transl_store_rrr chunk addr args src k
  | Aindexed2XS scale => transl_store_rrrxs chunk scale args src k
  | _ => transl_store_rro chunk addr args src k
  end.

(** Function epilogue *)

Definition make_epilogue (f: Machblock.function) (k: code) :=
  (loadind_ptr SP f.(fn_retaddr_ofs) GPRA) 
  ::g Pset RA GPRA ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k.

(** Translation of a Machblock instruction. *)

Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                              (ep: bool) (k: bcode) :=
  match i with
  | MBgetstack ofs ty dst =>
      loadind SP ofs ty dst k
  | MBsetstack src ofs ty =>
      storeind src SP ofs ty k
  | MBgetparam ofs ty dst =>
      (* load via the frame pointer if it is valid *)
      do c <- loadind FP ofs ty dst k;
      OK (if ep then c
                else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)
  | MBop op args res =>
      transl_op op args res k
  | MBload trap chunk addr args dst =>
      transl_load trap chunk addr args dst k
  | MBstore chunk addr args src =>
      transl_store chunk addr args src k
  end.

Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.control_flow_inst)
                                : res code :=
  match oi with
  | None => OK nil
  | Some i =>
    match i with
    | MBcall sig (inl r) =>
        do r1 <- ireg_of r; OK ((Picall r1) ::g nil)
    | MBcall sig (inr symb) =>
        OK ((Pcall symb) ::g nil)
    | MBtailcall sig (inr symb) =>
        OK (make_epilogue f ((Pgoto symb) ::g nil))
    | MBtailcall sig (inl r) =>
        do r1 <- ireg_of r; OK (make_epilogue f ((Pigoto r1) ::g nil))
    | MBbuiltin ef args res =>
        OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) ::g nil)
    | MBgoto lbl =>
        OK (Pj_l lbl ::g nil)
    | MBcond cond args lbl =>
        transl_cbranch cond args lbl nil
    | MBreturn =>
        OK (make_epilogue f (Pret ::g nil))
    | MBjumptable arg tbl =>
      do r <- ireg_of arg;
      OK (Pjumptable r tbl ::g nil)
    end
  end.

(** Translation of a code sequence *)

Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
  match i with
  | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP)
  | MBsetstack src ofs ty => before
  | MBgetparam ofs ty dst => negb (mreg_eq dst MFP)
  | MBop op args res => before && negb (mreg_eq res MFP)
  | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP)
  | MBstore chunk addr args res => before
  end.

(** This is the naive definition, which is not tail-recursive unlike the other backends *)

Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
  match il with
  | nil => OK nil
  | i1 :: il' =>
      do k <- transl_basic_code f il' (fp_is_parent it1p i1);
      transl_instr_basic f i1 it1p k
  end.

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

Fixpoint transl_basic_rec (f: Machblock.function) (il: list Machblock.basic_inst)
                          (it1p: bool) (k: bcode -> res bcode) :=
  match il with
  | nil => k nil
  | i1 :: il' =>
      transl_basic_rec f il' (fp_is_parent it1p i1)
        (fun c1 => do c2 <- transl_instr_basic f i1 it1p c1; k c2)
  end.

Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
  transl_basic_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^64] instructions,
  otherwise the offset part of the [PC] code pointer could wrap
  around, leading to incorrect executions. *)

(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instruction) :=
  match (extract_ctl ctl) with
  | None => 
      match c with
      | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
      | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil
      end
  | Some (PExpand (Pbuiltin ef args res)) =>
      match c with
      | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
      | _ => {| header := hd; body := c; exit := None |} 
              :: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
      end
  | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil
  end
.
Next Obligation.
  apply wf_bblock_refl. constructor.
    left. auto.
    discriminate.
Qed. Next Obligation.
  apply wf_bblock_refl. constructor.
    right. discriminate.
    unfold builtin_alone. intros. pose (H ef args res). rewrite H0 in n. contradiction.
Qed.

Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
  do c <- transl_basic_code f fb.(Machblock.body) ep;
  do ctl <- transl_instr_control f fb.(Machblock.exit);
  OK (gen_bblocks fb.(Machblock.header) c ctl)
.

Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=
  match lmb with
  | nil => OK nil
  | mb :: lmb => 
      do lb <- transl_block f mb (if Machblock.header mb then ep else false);
      do lb' <- transl_blocks f lmb false;
      OK (lb @@ lb')
  end
.

Program Definition make_prologue (f:  Machblock.function) lb :=
  ({| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::i
         Pget GPRA RA ::i
         storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::i nil;
      exit := None |} :: lb).

Definition transl_function (f: Machblock.function) :=
  do lb <- transl_blocks f f.(Machblock.fn_code) true;
  OK (mkfunction f.(Machblock.fn_sig)
        (make_prologue f lb)).

Definition transf_function (f: Machblock.function) : res Asmvliw.function :=
  do tf <- transl_function f;
  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
  then Error (msg "code size exceeded")
  else OK tf.

Definition transf_fundef (f: Machblock.fundef) : res Asmvliw.fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: Machblock.program) : res Asmvliw.program :=
  transform_partial_program transf_fundef p.