Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed

1 files changed, 0 insertions, 467 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
deleted file mode 100644
index 45205158..00000000
--- a/aarch64/Asmgen.v
+++ /dev/null
@@ -1,467 +0,0 @@
-(* *************************************************************)
-(*                                                             *)
-(*             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.
-Require Import Locations Compopts.
-Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling.
-
-
-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
-    loadimm64 X16 m (Asm.Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
-  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.
-
-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
-  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'.