(* *************************************************************)
(*                                                             *)
(*             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                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)


(* Asmblock language for aarch64

WORK IN PROGRESS: we want to define an Asmblock syntax, with an Asmblock semantics
(e.g. we don't need the parallel semantics of Asmvliw)


NOTE: this file is inspired from 
   - aarch64/Asm.v
   - kvx/Asmvliw.v (only the Asmblock syntax)
   - kvx/Asmblock.v
*)


(** Abstract syntax and semantics for AArch64 assembly language *)

Require Import Coqlib Zbits Maps.
Require Import AST Integers Floats.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Locations Conventions.
Require Stacklayout.
Require Import OptionMonad.

(** * Abstract syntax *)

(** Integer registers, floating-point registers. *)

(** In assembly files, [Xn] denotes the full 64-bit register
    and [Wn] the low 32 bits of [Xn]. *)

Inductive ireg: Type :=
  | X0  | X1  | X2  | X3  | X4  | X5  |  X6  | X7
  | X8  | X9  | X10 | X11 | X12 | X13 |  X14 | X15
  | X16 | X17 | X18 | X19 | X20 | X21 |  X22 | X23
  | X24 | X25 | X26 | X27 | X28 | X29 |  X30.

Inductive ireg0: Type :=
  | RR0 (r: ireg) | XZR.

Inductive iregsp: Type :=
  | RR1 (r: ireg) | XSP.

Coercion RR0: ireg >-> ireg0.
Coercion RR1: ireg >-> iregsp.

Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
Proof. decide equality. Defined.

Lemma iregsp_eq: forall (x y: iregsp), {x=y} + {x<>y}.
Proof. decide equality; apply ireg_eq. Defined.

(** In assembly files, [Dn] denotes the low 64-bit of a vector register,
    and [Sn] the low 32 bits. *)

Inductive freg: Type :=
  | D0  | D1  | D2  | D3  | D4  | D5  |  D6  | D7
  | D8  | D9  | D10 | D11 | D12 | D13 |  D14 | D15
  | D16 | D17 | D18 | D19 | D20 | D21 |  D22 | D23
  | D24 | D25 | D26 | D27 | D28 | D29 |  D30 | D31.

Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
Proof. decide equality. Defined.

(** Bits in the condition register. *)

Inductive crbit: Type :=
  | CN: crbit    (**r negative *)
  | CZ: crbit    (**r zero *)
  | CC: crbit    (**r carry *)
  | CV: crbit.   (**r overflow *)

Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
Proof. decide equality. Defined.

(** We model the following registers of the ARM architecture. *)

Inductive preg: Type :=
  | IR: iregsp -> preg   (**r 64- or 32-bit integer registers *)
  | FR: freg -> preg     (**r double- or single-precision float registers *)
  | CR: crbit -> preg    (**r bits in the condition register *)
  | PC: preg.            (**r program counter *)

(* XXX: ireg no longer coerces to preg *)
Coercion IR: iregsp >-> preg.
Definition SP:preg := XSP.
Coercion FR: freg >-> preg.
Coercion CR: crbit >-> preg.

Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
Proof. decide equality. apply iregsp_eq. apply freg_eq. apply crbit_eq. Defined.

Module PregEq.
  Definition t := preg.
  Definition eq := preg_eq.
End PregEq.

Module Pregmap := EMap(PregEq).

Definition preg_of_iregsp (r: iregsp) : preg :=
  match r with RR1 r => IR r | XSP => SP end.

(** Conventional name for return address ([RA]) *)

Notation "'RA'" := X30 (only parsing) : asm.

(** The instruction set.  Most instructions correspond exactly to
  actual AArch64 instructions. See the ARM reference manuals for more
  details.  Some instructions, described below, are
  pseudo-instructions: they expand to canned instruction sequences
  during the printing of the assembly code.  *)

Definition label := positive.

Inductive isize: Type :=
  | W                                                (**r 32-bit integer operation *)
  | X.                                               (**r 64-bit integer operation *)

Inductive fsize: Type :=
  | S                                                (**r 32-bit, single-precision FP operation *)
  | D.                                               (**r 64-bit, double-precision FP operation *)

Inductive testcond : Type :=
  | TCeq: testcond    (**r equal *)
  | TCne: testcond    (**r not equal *)
  | TChs: testcond    (**r unsigned higher or same *)
  | TClo: testcond    (**r unsigned lower *)
  | TCmi: testcond    (**r negative *)
  | TCpl: testcond    (**r positive *)
  | TChi: testcond    (**r unsigned higher *)
  | TCls: testcond    (**r unsigned lower or same *)
  | TCge: testcond    (**r signed greater or equal *)
  | TClt: testcond    (**r signed less than *)
  | TCgt: testcond    (**r signed greater *)
  | TCle: testcond.   (**r signed less than or equal *)

Inductive addressing: Type :=
  | ADimm (base: iregsp) (n: int64)                  (**r base plus immediate offset *)
  | ADreg (base: iregsp) (r: ireg)                   (**r base plus reg *)
  | ADlsl (base: iregsp) (r: ireg) (n: int)          (**r base plus reg LSL n *)
  | ADsxt (base: iregsp) (r: ireg) (n: int)          (**r base plus SIGN-EXT(reg) LSL n *)
  | ADuxt (base: iregsp) (r: ireg) (n: int)          (**r base plus ZERO-EXT(reg) LSL n *)
  | ADadr (base: iregsp) (id: ident) (ofs: ptrofs)   (**r base plus low address of [id + ofs] *)
  | ADpostincr (base: iregsp) (n: int64).            (**r base plus offset; base is updated after *)

Inductive shift_op: Type :=
  | SOnone
  | SOlsl (n: int)
  | SOlsr (n: int)
  | SOasr (n: int)
  | SOror (n: int).

Inductive extend_op: Type :=
  | EOsxtb (n: int)
  | EOsxth (n: int)
  | EOsxtw (n: int)
  | EOuxtb (n: int)
  | EOuxth (n: int)
  | EOuxtw (n: int)
  | EOuxtx (n: int).

(* First task: splitting the big [instruction] type below into CFI and basic instructions.
   Actually a finer splitting in order to regroup "similar" instructions could be much better for automation of the scheduler proof!
   e.g. "similar" means identical "interface" w.r.t. pseudo-registers when translated to AbstractBB,
   or with a "similar" semantics.

   see example of loads below.
*)

(** Control Flow instructions 

*)
Inductive cf_instruction : Type :=
  | Pb (lbl: label)                                                   (**r branch *)
  | Pbc (c: testcond) (lbl: label)                                    (**r conditional branch *)
  | Pbl (id: ident) (sg: signature)                                   (**r jump to function and link *)
  | Pbs (id: ident) (sg: signature)                                   (**r jump to function *)
  | Pblr (r: ireg) (sg: signature)                                    (**r indirect jump and link *)
  | Pbr (r: ireg) (sg: signature)                                     (**r indirect jump *)
  | Pret (r: ireg)                                                    (**r return *)
  | Pcbnz (sz: isize) (r: ireg) (lbl: label)                          (**r branch if not zero *)
  | Pcbz (sz: isize) (r: ireg) (lbl: label)                           (**r branch if zero *)
  | Ptbnz (sz: isize) (r: ireg) (n: int) (lbl: label)                 (**r branch if bit n is not zero *)
  | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label)                  (**r branch if bit n is zero *)
  (** Pseudo-instructions *)
  | Pbtbl (r1: ireg) (tbl: list label)                                (**r N-way branch through a jump table *)
  . 

(*
A builtin is considered as a control-flow instruction, because it could emit a trace (cf. Machblock semantics).
Here, we do not need to have builtins alone in basic-blocks (on the contrary to KVX bundles).
*)

Inductive control: Type :=
  | PCtlFlow  (i: cf_instruction)
  (** Pseudo-instructions *)
  | Pbuiltin (ef: external_function)
             (args: list (builtin_arg preg)) (res: builtin_res preg)  (**r built-in function (pseudo) *)
  .

Coercion PCtlFlow: cf_instruction >-> control.

(** Basic instructions *)

(* Loads waiting for (rd: preg) (a: addressing) 
 * XXX Use preg because exec_load is defined in terms of it, thus allowing us to
 * treat integer and floating point loads the same. *)
Inductive load_rd_a: Type :=
  (* Integer load *)
  | Pldrw                                   (**r load int32 *)
  | Pldrw_a                                 (**r load int32 as any32 *)
  | Pldrx                                   (**r load int64 *)
  | Pldrx_a                                 (**r load int64 as any64 *)
  | Pldrb (sz: isize)                       (**r load int8, zero-extend *)
  | Pldrsb (sz: isize)                      (**r load int8, sign-extend *)
  | Pldrh (sz: isize)                       (**r load int16, zero-extend *)
  | Pldrsh (sz: isize)                      (**r load int16, sign-extend *)
  | Pldrzw                                  (**r load int32, zero-extend to int64 *)
  | Pldrsw                                  (**r load int32, sign-extend to int64 *)
  (* Floating-point load *)
  | Pldrs                                   (**r load float32 (single precision) *)
  | Pldrd                                   (**r load float64 (double precision) *)
  | Pldrd_a                                 (**r load float64 as any64 *)
  .

(* Actually, Pldp is not used in the aarch64/Asm semantics!
 
Thus we skip this particular case:

Inductive ld_instruction: Type :=
  | PLd_rd_a (ld: load_rd_a) (rd: ireg) (a: addressing)
  | Pldp (rd1 rd2: ireg) (a: addressing)   (**r load two int64 *)
  .

Coercion PLoad: ld_instruction >-> basic.

*)

Inductive store_rs_a : Type :=
  (* Integer store *)
  | Pstrw                                   (**r store int32 *)
  | Pstrw_a                                 (**r store int32 as any32 *)
  | Pstrx                                   (**r store int64 *)
  | Pstrx_a                                 (**r store int64 as any64 *)
  | Pstrb                                   (**r store int8 *)
  | Pstrh                                   (**r store int16 *)
  (* Floating-point store *)
  | Pstrs                                   (**r store float32 *)
  | Pstrd                                   (**r store float64 *)
  | Pstrd_a                                 (**r store float64 as any64 *)
  .
(* Actually, Pstp is not used in the aarch64/Asm semantics!
 * Thus we skip this particular case:
 *   Inductive st_instruction : Type :=
 *     | PSt_rs_a (st : store_rs_a) (rs : ireg) (a : addressing)
 *     | Pstp (rs1 rs2: ireg) (a: addressing)  (**r store two int64 *)
 *     .
 *   Coercion PStore : st_instruction >-> basic.
 *)

Inductive arith_p : Type :=
  (** PC-relative addressing *)
  | Padrp (id: ident) (ofs: ptrofs)                        (**r set [rd] to high address of [id + ofs] *)
  (** Move wide immediate *)
  | Pmovz (sz: isize) (n: Z) (pos: Z)                      (**r move [n << pos] to [rd] *)
  | Pmovn (sz: isize) (n: Z) (pos: Z)                      (**r move [NOT(n << pos)] to [rd] *)
  (** Floating-point move *)
  | Pfmovimms (f: float32)                                 (**r load float32 constant *)
  | Pfmovimmd (f: float)                                   (**r load float64 constant *)
.

Inductive arith_comparison_p : Type :=
  (** Floating-point comparison *)
  | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
  (** Integer arithmetic, immediate *)
  | Pcmpimm (sz: isize) (n: Z)                        (**r compare *)
  | Pcmnimm (sz: isize) (n: Z)                        (**r compare negative *)
  (** Logical, immediate *)
  | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
.

Inductive arith_pp : Type :=
  (** Move integer register *)
  | Pmov
  (** Move wide immediate *)
  (* XXX: has to have the same register supplied both times *)
  | Pmovk (sz: isize) (n: Z) (pos: Z)           (**r insert 16 bits of [n] at [pos] in rd *)
  (** PC-relative addressing *)
  | Paddadr (id: ident) (ofs: ptrofs)           (**r add the low address of [id + ofs] *)
  (** Bit-field operations *)
  | Psbfiz (sz: isize) (r: int) (s: Z)          (**r sign extend and shift left *)
  | Psbfx (sz: isize) (r: int) (s: Z)           (**r shift right and sign extend *)
  | Pubfiz (sz: isize) (r: int) (s: Z)          (**r zero extend and shift left *)
  | Pubfx (sz: isize) (r: int) (s: Z)           (**r shift right and zero extend *)
(* Bit operations are not used in the aarch64/asm semantics
  (** Bit operations *)
  | Pcls (sz: isize)                            (**r count leading sign bits *)
  | Pclz (sz: isize)                            (**r count leading zero bits *)
  | Prev (sz: isize)                            (**r reverse bytes *)
  | Prev16 (sz: isize)                          (**r reverse bytes in each 16-bit word *)
*)
  (** Floating-point move *)
  | Pfmov
  (** Floating-point conversions *)
  | Pfcvtds                                           (**r convert float32 to float64 *)
  | Pfcvtsd                                           (**r convert float64 to float32 *)
  (** Floating-point arithmetic *)
  | Pfabs (sz: fsize)                                 (**r absolute value *)
  | Pfneg (sz: fsize)                                 (**r negation *)
  (* Pfsqrt is not used in the semantics of aarch64/asm
  | Pfsqrt (sz: fsize)                                (**r square root *) *)
  (** Floating-point conversions *)
  | Pscvtf (fsz: fsize) (isz: isize)                  (**r convert signed int to float *)
  | Pucvtf (fsz: fsize) (isz: isize)                  (**r convert unsigned int to float *)
  | Pfcvtzs (isz: isize) (fsz: fsize)                 (**r convert float to signed int *)
  | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
  (** Integer arithmetic, immediate *)
  | Paddimm (sz: isize) (n: Z)                        (**r addition *)
  | Psubimm (sz: isize) (n: Z)                        (**r subtraction *)
.

Inductive arith_comparison_r0r : Type :=
  (** Integer arithmetic, shifted register *)
  | Pcmp (is:isize) (s: shift_op)             (**r compare *)
  | Pcmn (is:isize) (s: shift_op)             (**r compare negative *)
  (** Logical, shifted register *)
  | Ptst (is:isize) (s: shift_op)             (**r and, then set flags *)
.

Inductive arith_comparison_pp : Type :=
  (** Integer arithmetic, extending register *)
  | Pcmpext (x: extend_op)                      (**r int64-int32 cmp *)
  | Pcmnext (x: extend_op)                      (**r int64-int32 cmn *)
  (** Floating-point comparison *)
  | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
.

Inductive arith_ppp : Type :=
  (** Variable shifts *)
  | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
  | Plslv (sz: isize)                                 (**r left shift *)
  | Plsrv (sz: isize)                                 (**r logical right shift *)
  | Prorv (sz: isize)                                 (**r rotate right *)
  (** Integer multiply/divide *)
  | Psmulh                                            (**r signed multiply high *)
  | Pumulh                                            (**r unsigned multiply high *)
  | Psdiv (sz: isize)                                 (**r signed division *)
  | Pudiv (sz: isize)                                 (**r unsigned division *)
  (** Integer arithmetic, extending register *)
  | Paddext (x: extend_op)                            (**r int64-int32 add *)
  | Psubext (x: extend_op)                            (**r int64-int32 sub *)
  (** Floating-point arithmetic *)
  | Pfadd (sz: fsize)                                (**r addition *)
  | Pfdiv (sz: fsize)                                (**r division *)
  | Pfmul (sz: fsize)                                (**r multiplication *)
  | Pfsub (sz: fsize)                                (**r subtraction *)
.

Inductive arith_rr0r : Type :=
  (** Integer arithmetic, shifted register *)
  | Padd (sz:isize) (s: shift_op)                               (**r addition *)
  | Psub (sz:isize) (s: shift_op)                               (**r subtraction *)
  (** Logical, shifted register *)
  | Pand (sz:isize) (s: shift_op)                               (**r and *)
  | Pbic (sz:isize) (s: shift_op)                               (**r and-not *)
  | Peon (sz:isize) (s: shift_op)                               (**r xor-not *)
  | Peor (sz:isize) (s: shift_op)                               (**r xor *)
  | Porr (sz:isize) (s: shift_op)                               (**r or *)
  | Porn (sz:isize) (s: shift_op)                               (**r or-not *)
.


Inductive arith_rr0 : Type :=
  (** Logical, immediate *)
  | Pandimm (sz: isize) (n: Z)                     (**r and *)
  | Peorimm (sz: isize) (n: Z)                     (**r xor *)
  | Porrimm (sz: isize) (n: Z)                     (**r or *)
.

Inductive arith_arrrr0 : Type :=
  (** Integer multiply/divide *)
  | Pmadd (sz: isize)                               (**r multiply-add *)
  | Pmsub (sz: isize)                               (**r multiply-sub *)
.

(* Currently not used by the semantics of aarch64/Asm
 * Inductive arith_apppp : Type :=
 *   (** Floating-point arithmetic *)
 *   | Pfmadd (sz: fsize)                              (**r [rd = r3 + r1 * r2] *)
 *   | Pfmsub (sz: fsize)                              (**r [rd = r3 - r1 * r2] *)
 * .

 * Inductive arith_aapppp : Type :=
 *   (** Floating-point arithmetic *)
 *   | Pfnmadd (sz: fsize)                             (**r [rd = - r3 - r1 * r2] *)
 *   | Pfnmsub (sz: fsize)                             (**r [rd = - r3 + r1 * r2] *)
 * . *)

(* Notes on the naming scheme used here:
 * R: ireg
 * R0: ireg0
 * Rsp: iregsp
 * F: freg
 * W/X: Occur in conjunction with R0, says whether an ireg0 should be evaluated
 *      as W regsiter (32 bit) or X register (64 bit)
 * S/D: Used for completeness sake. Only used for copying an integer register
 *      to a floating point register. Could be removed.
 * A: These instructions perform an additional arithmetic operation
      XXX Does this interpretation match the use in kvx/Asmvliw?
 * Comparison: For these instructions the first register is not the target.
 *             Instead, the condition register is mutated.
 *)
Inductive ar_instruction : Type :=
  | PArithP (i : arith_p) (rd : preg)
  | PArithPP (i : arith_pp) (rd rs : preg)
  | PArithPPP (i : arith_ppp) (rd r1 r2 : preg)
  | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
  | PArithRR0 (i : arith_rr0) (rd : ireg) (r1 : ireg0)
  | PArithARRRR0 (i : arith_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
  (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
  | PArithAPPPP (i : arith_apppp) (rd r1 r2 r3 : preg) *)
  (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
  | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *)
  | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg)
  | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg)
  | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
  (* Instructions without indirection sine they would be the only ones *)
  (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *)
  | Pcset (rd : ireg) (c : testcond)                                  (**r set to 1/0 if cond is true/false *)
  (* PArithFR0 *)
  | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0)                     (**r copy int reg to FP reg *)
  (* PArithCPPP *)
  | Pcsel (rd r1 r2 : preg) (c : testcond)                            (**r int/float conditional move *)
  (* PArithAFFF *)
  | Pfnmul (fsz : fsize) (rd r1 r2 : freg)                            (**r multiply-negate *)
.

Inductive basic : Type :=
  | PArith (i: ar_instruction)                                        (**r TODO *)
  | PLoad (ld: load_rd_a) (rd: preg) (a: addressing)                  (**r TODO *)
  | PStore (st: store_rs_a) (r: preg) (a: addressing)                 (**r TODO *)
  | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
  | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
  | Ploadsymbol (rd: ireg) (id: ident)                                (**r load the address of [id] *)
  | Pcvtsw2x (rd: ireg) (r1: ireg)                                    (**r sign-extend 32-bit int to 64-bit *)
  | Pcvtuw2x (rd: ireg) (r1: ireg)                                    (**r zero-extend 32-bit int to 64-bit *)
  | Pcvtx2w (rd: ireg)                                                (**r retype a 64-bit int as a 32-bit int *)
(* NOT USED IN THE SEMANTICS !
  | Pnop                                                              (**r no operation *)
  | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
  | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
*)
.

(** * Definition of a bblock

A bblock must contain at least one instruction.

This choice simplifies the definition of [find_bblock] below:
indeed, each address of a code block identifies at most one bblock.
*)

Definition non_empty_body (body: list basic): bool :=
  match body with
  | nil => false
  | _ => true
  end.

Definition non_empty_exit (exit: option control): bool :=
  match exit with
  | None => false
  | _ => true
  end.

Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit.

(** A bblock is well-formed if he contains at least one instruction. *)

Record bblock := mk_bblock {
  header: list label;
  body: list basic;
  exit: option control;
  correct: Is_true (non_empty_bblockb body exit)
}.

(* FIXME? redundant with definition in Machblock *)
Definition length_opt {A} (o: option A) : nat :=
  match o with
  | Some o => 1
  | None => 0
  end.

(* This notion of size induces the notion of "valid" code address given by [find_bblock]

   The result is in Z to be compatible with operations on PC.
*)
Definition size (b:bblock): Z := Z.of_nat (length (header b) + length (body b) + length_opt (exit b)).

Definition bblocks := list bblock.

Fixpoint size_blocks (l: bblocks): Z :=
  match l with
  | nil => 0
  | b :: l =>
     (size b) + (size_blocks l)
  end
  .

Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.

(* TODO: ORIGINAL ABSTRACT SYNTAX OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !

Inductive instruction: Type :=
  (** Branches *)
  | Pb (lbl: label)                                                   (**r branch *)
  | Pbc (c: testcond) (lbl: label)                                    (**r conditional branch *)
  | Pbl (id: ident) (sg: signature)                                   (**r jump to function and link *)
  | Pbs (id: ident) (sg: signature)                                   (**r jump to function *)
  | Pblr (r: ireg) (sg: signature)                                    (**r indirect jump and link *)
  | Pbr (r: ireg) (sg: signature)                                     (**r indirect jump *)
  | Pret (r: ireg)                                                    (**r return *)
  | Pcbnz (sz: isize) (r: ireg) (lbl: label)                          (**r branch if not zero *)
  | Pcbz (sz: isize) (r: ireg) (lbl: label)                           (**r branch if zero *)
  | Ptbnz (sz: isize) (r: ireg) (n: int) (lbl: label)                 (**r branch if bit n is not zero *)
  | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label)                  (**r branch if bit n is zero *)
  (** Memory loads and stores *)
  | Pldrw (rd: ireg) (a: addressing)                                  (**r load int32 *)
  | Pldrw_a (rd: ireg) (a: addressing)                                (**r load int32 as any32 *)
  | Pldrx (rd: ireg) (a: addressing)                                  (**r load int64 *)
  | Pldrx_a (rd: ireg) (a: addressing)                                (**r load int64 as any64 *)
  | Pldrb (sz: isize) (rd: ireg) (a: addressing)                      (**r load int8, zero-extend *)
  | Pldrsb (sz: isize) (rd: ireg) (a: addressing)                     (**r load int8, sign-extend *)
  | Pldrh (sz: isize) (rd: ireg) (a: addressing)                      (**r load int16, zero-extend *)
  | Pldrsh (sz: isize) (rd: ireg) (a: addressing)                     (**r load int16, sign-extend *)
  | Pldrzw (rd: ireg) (a: addressing)                                 (**r load int32, zero-extend to int64 *)
  | Pldrsw (rd: ireg) (a: addressing)                                 (**r load int32, sign-extend to int64 *)
  | Pldp (rd1 rd2: ireg) (a: addressing)                              (**r load two int64 *)
  | Pstrw (rs: ireg) (a: addressing)                                  (**r store int32 *)
  | Pstrw_a (rs: ireg) (a: addressing)                                (**r store int32 as any32 *)
  | Pstrx (rs: ireg) (a: addressing)                                  (**r store int64 *)
  | Pstrx_a (rs: ireg) (a: addressing)                                (**r store int64 as any64 *)
  | Pstrb (rs: ireg) (a: addressing)                                  (**r store int8 *)
  | Pstrh (rs: ireg) (a: addressing)                                  (**r store int16 *)
  | Pstp (rs1 rs2: ireg) (a: addressing)                              (**r store two int64 *)
  (** Integer arithmetic, immediate *)
  | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r addition *)
  | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r subtraction *)
  | Pcmpimm (sz: isize) (r1: ireg) (n: Z)                             (**r compare *)
  | Pcmnimm (sz: isize) (r1: ireg) (n: Z)                             (**r compare negative *)
  (** Move integer register *)
  | Pmov (rd: iregsp) (r1: iregsp)
  (** Logical, immediate *)
  | Pandimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z)                 (**r and *)
  | Peorimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z)                 (**r xor *)
  | Porrimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z)                 (**r or *)
  | Ptstimm (sz: isize) (r1: ireg) (n: Z)                             (**r and, then set flags *)
  (** Move wide immediate *)
  | Pmovz (sz: isize) (rd: ireg) (n: Z) (pos: Z)                      (**r move [n << pos] to [rd] *)
  | Pmovn (sz: isize) (rd: ireg) (n: Z) (pos: Z)                      (**r move [NOT(n << pos)] to [rd] *)
  | Pmovk (sz: isize) (rd: ireg) (n: Z) (pos: Z)                      (**r insert 16 bits of [n] at [pos] in rd *)
  (** PC-relative addressing *)
  | Padrp (rd: ireg) (id: ident) (ofs: ptrofs)                        (**r set [rd] to high address of [id + ofs] *)
  | Paddadr (rd: ireg) (r1: ireg) (id: ident) (ofs: ptrofs)           (**r add the low address of [id + ofs] *)
  (** Bit-field operations *)
  | Psbfiz (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)          (**r sign extend and shift left *)
  | Psbfx (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)           (**r shift right and sign extend *)
  | Pubfiz (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)          (**r zero extend and shift left *)
  | Pubfx (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)           (**r shift right and zero extend *)
  (** Integer arithmetic, shifted register *)
  | Padd (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r addition *)
  | Psub (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r subtraction *)
  | Pcmp (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op)             (**r compare *)
  | Pcmn (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op)             (**r compare negative *)
  (** Integer arithmetic, extending register *)
  | Paddext (rd: iregsp) (r1: iregsp) (r2: ireg) (x: extend_op)       (**r int64-int32 add *)
  | Psubext (rd: iregsp) (r1: iregsp) (r2: ireg) (x: extend_op)       (**r int64-int32 sub *)
  | Pcmpext (r1: ireg) (r2: ireg) (x: extend_op)                      (**r int64-int32 cmp *)
  | Pcmnext (r1: ireg) (r2: ireg) (x: extend_op)                      (**r int64-int32 cmn *)
  (** Logical, shifted register *)
  | Pand (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r and *)
  | Pbic (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r and-not *)
  | Peon (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r xor-not *)
  | Peor (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r xor *)
  | Porr (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r or *)
  | Porn (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r or-not *)
  | Ptst (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op)             (**r and, then set flags *)
  (** Variable shifts *)
  | Pasrv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r arithmetic right shift *)
  | Plslv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r left shift *)
  | Plsrv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r logical right shift *)
  | Prorv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r rotate right *)
  (** Bit operations *)
  | Pcls (sz: isize) (rd r1: ireg)                                    (**r count leading sign bits *)
  | Pclz (sz: isize) (rd r1: ireg)                                    (**r count leading zero bits *)
  | Prev (sz: isize) (rd r1: ireg)                                    (**r reverse bytes *)
  | Prev16 (sz: isize) (rd r1: ireg)                                  (**r reverse bytes in each 16-bit word *)
  (** Conditional data processing *)
  | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond)                      (**r int conditional move *)
  | Pcset (rd: ireg) (c: testcond)                                    (**r set to 1/0 if cond is true/false *)
(*
  | Pcsetm (rd: ireg) (c: testcond)                                   (**r set to -1/0 if cond is true/false *)
*)
  (** Integer multiply/divide *)
  | Pmadd (sz: isize) (rd: ireg) (r1 r2: ireg) (r3: ireg0)            (**r multiply-add *)
  | Pmsub (sz: isize) (rd: ireg) (r1 r2: ireg) (r3: ireg0)            (**r multiply-sub *)
  | Psmulh (rd: ireg) (r1 r2: ireg)                                   (**r signed multiply high *)
  | Pumulh (rd: ireg) (r1 r2: ireg)                                   (**r unsigned multiply high *)
  | Psdiv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r signed division *)
  | Pudiv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r unsigned division *)
  (** Floating-point loads and stores *)
  | Pldrs (rd: freg) (a: addressing)                                  (**r load float32 (single precision) *)
  | Pldrd (rd: freg) (a: addressing)                                  (**r load float64 (double precision) *)
  | Pldrd_a (rd: freg) (a: addressing)                                (**r load float64 as any64 *)
  | Pstrs (rs: freg) (a: addressing)                                  (**r store float32 *)
  | Pstrd (rs: freg) (a: addressing)                                  (**r store float64 *)
  | Pstrd_a (rs: freg) (a: addressing)                                (**r store float64 as any64 *)
  (** Floating-point move *)
  | Pfmov (rd r1: freg)
  | Pfmovimms (rd: freg) (f: float32)                                 (**r load float32 constant *)
  | Pfmovimmd (rd: freg) (f: float)                                   (**r load float64 constant *)
  | Pfmovi (fsz: fsize) (rd: freg) (r1: ireg0)                        (**r copy int reg to FP reg *)
  (** Floating-point conversions *)
  | Pfcvtds (rd r1: freg)                                             (**r convert float32 to float64 *)
  | Pfcvtsd (rd r1: freg)                                             (**r convert float64 to float32 *)
  | Pfcvtzs (isz: isize) (fsz: fsize) (rd: ireg) (r1: freg)           (**r convert float to signed int *)
  | Pfcvtzu (isz: isize) (fsz: fsize) (rd: ireg) (r1: freg)           (**r convert float to unsigned int *)
  | Pscvtf (fsz: fsize) (isz: isize) (rd: freg) (r1: ireg)            (**r convert signed int to float *)
  | Pucvtf (fsz: fsize) (isz: isize) (rd: freg) (r1: ireg)            (**r convert unsigned int to float *)
  (** Floating-point arithmetic *)
  | Pfabs (sz: fsize) (rd r1: freg)                                   (**r absolute value *)
  | Pfneg (sz: fsize) (rd r1: freg)                                   (**r negation *)
  | Pfsqrt (sz: fsize) (rd r1: freg)                                  (**r square root *)
  | Pfadd (sz: fsize) (rd r1 r2: freg)                                (**r addition *)
  | Pfdiv (sz: fsize) (rd r1 r2: freg)                                (**r division *)
  | Pfmul (sz: fsize) (rd r1 r2: freg)                                (**r multiplication *)
  | Pfnmul (sz: fsize) (rd r1 r2: freg)                               (**r multiply-negate *)
  | Pfsub (sz: fsize) (rd r1 r2: freg)                                (**r subtraction *)
  | Pfmadd (sz: fsize) (rd r1 r2 r3: freg)                            (**r [rd = r3 + r1 * r2] *)
  | Pfmsub (sz: fsize) (rd r1 r2 r3: freg)                            (**r [rd = r3 - r1 * r2] *)
  | Pfnmadd (sz: fsize) (rd r1 r2 r3: freg)                           (**r [rd = - r3 - r1 * r2] *)
  | Pfnmsub (sz: fsize) (rd r1 r2 r3: freg)                           (**r [rd = - r3 + r1 * r2] *)
  (** Floating-point comparison *)
  | Pfcmp (sz: fsize) (r1 r2: freg)                                   (**r compare [r1] and [r2] *)
  | Pfcmp0 (sz: fsize) (r1: freg)                                     (**r compare [r1] and [+0.0] *)
  (** Floating-point conditional select *)
  | Pfsel (rd r1 r2: freg) (cond: testcond)
  (** Pseudo-instructions *)
  | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
  | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
  | Plabel (lbl: label)                                               (**r define a code label *)
  | Ploadsymbol (rd: ireg) (id: ident)                                (**r load the address of [id] *)
  | Pcvtsw2x (rd: ireg) (r1: ireg)                                    (**r sign-extend 32-bit int to 64-bit *)
  | Pcvtuw2x (rd: ireg) (r1: ireg)                                    (**r zero-extend 32-bit int to 64-bit *)
  | Pcvtx2w (rd: ireg)                                                (**r retype a 64-bit int as a 32-bit int *)
  | Pbtbl (r1: ireg) (tbl: list label)                                (**r N-way branch through a jump table *)
  | Pbuiltin (ef: external_function)
             (args: list (builtin_arg preg)) (res: builtin_res preg)  (**r built-in function (pseudo) *)
  | Pnop                                                              (**r no operation *)
  | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
  | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
.
*)


(** * Operational semantics *)

(** The semantics operates over a single mapping from registers
  (type [preg]) to values.  We maintain (but do not enforce)
  the convention that integer registers are mapped to values of
  type [Tint], float registers to values of type [Tfloat],
  and condition bits to either [Vzero] or [Vone]. *)

Definition regset := Pregmap.t val.
Definition genv := Genv.t fundef unit.

(** The value of an [ireg0] is either the value of the integer register,
    or 0. *)

Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val :=
  match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end.

(** Concise notations for accessing and updating the values of registers. *)

Notation "a # b" := (a b) (at level 1, only parsing) : asm.
Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm.
Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm.

Open Scope asm.

(** Undefining some registers *)

Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
  match l with
  | nil => rs
  | r :: l' => undef_regs l' (rs#r <- Vundef)
  end.

(** Undefining the condition codes *)

Definition undef_flags (rs: regset) : regset :=
  fun r => match r with CR _ => Vundef | _ => rs r end.

(** Assigning a register pair *)

Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
  match p with
  | One r => rs#r <- v
  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
  end.

(** Assigning the result of a builtin *)

Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
  match res with
  | BR r => rs#r <- v
  | BR_none => rs
  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
  end.

(** See "Parameters" of the same names in Asm.v *) 
Record aarch64_linker: Type := {
  symbol_low: ident -> ptrofs -> val;
  symbol_high: ident -> ptrofs -> val
}.

Section RELSEM.

Variable lk: aarch64_linker.
Variable ge: genv.


(** The semantics is purely small-step and defined as a function
  from the current state (a register set + a memory state)
  to either [Next rs' m'] where [rs'] and [m'] are the updated register
  set and memory state after execution of the instruction at [rs#PC],
  or [Stuck] if the processor is stuck. *)

Record state: Type := State { _rs: regset; _m: mem }.
Definition outcome := option state.
Definition Next rs m: outcome := Some (State rs m).
Definition Stuck: outcome := None.
Local Open Scope option_monad_scope.

(* a few lemma on comparisons of unsigned (e.g. pointers) 

TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
*)

Definition Val_cmpu_bool cmp v1 v2: option bool :=
  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.

Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
   -> (Val_cmpu_bool cmp v1 v2) = Some b.
Proof.
  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
Qed.

Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).

Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
               (Val_cmpu cmp v1 v2).
Proof.
  unfold Val.cmpu, Val_cmpu.
  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
  destruct ob; simpl.
  - erewrite Val_cmpu_bool_correct; eauto.
    econstructor.
  - econstructor.
Qed.

Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
 := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).

Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
   -> (Val_cmplu_bool cmp v1 v2) = Some b.
Proof.
  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
Qed.

Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).

Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
               (Val_cmplu cmp v1 v2).
Proof.
  unfold Val.cmplu, Val_cmplu.
  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
  destruct ob as [b|]; simpl.
  - erewrite Val_cmplu_bool_correct; eauto.
    simpl. econstructor.
  - econstructor.
Qed.

(** Testing a condition *)

Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
  match c with
  | TCeq =>                             (**r equal *)
      match rs#CZ with
      | Vint n => Some (Int.eq n Int.one)
      | _ => None
      end
  | TCne =>                             (**r not equal *)
      match rs#CZ with
      | Vint n => Some (Int.eq n Int.zero)
      | _ => None
      end
  | TClo =>                             (**r unsigned less than  *)
      match rs#CC with
      | Vint n => Some (Int.eq n Int.zero)
      | _ => None
      end
  | TCls =>                             (**r unsigned less or equal *)
      match rs#CC, rs#CZ with
      | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
      | _, _ => None
      end
  | TChs =>                             (**r unsigned greater or equal *)
      match rs#CC with
      | Vint n => Some (Int.eq n Int.one)
      | _ => None
      end
  | TChi =>                             (**r unsigned greater *)
      match rs#CC, rs#CZ with
      | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
      | _, _ => None
      end
  | TClt =>                             (**r signed less than *)
      match rs#CV, rs#CN with
      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
      | _, _ => None
      end
  | TCle =>                             (**r signed less or equal *)
      match rs#CV, rs#CN, rs#CZ with
      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
      | _, _, _ => None
      end
  | TCge =>                             (**r signed greater or equal *)
      match rs#CV, rs#CN with
      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
      | _, _ => None
      end
  | TCgt =>                             (**r signed greater *)
      match rs#CV, rs#CN, rs#CZ with
      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
      | _, _, _ => None
      end
  | TCpl =>                             (**r positive *)
      match rs#CN with
      | Vint n => Some (Int.eq n Int.zero)
      | _ => None
      end
  | TCmi =>                             (**r negative *)
      match rs#CN with
      | Vint n => Some (Int.eq n Int.one)
      | _ => None
      end
  end.

(** Integer "is zero?" test *)

Definition eval_testzero (sz: isize) (v: val): option bool :=
  match sz with
  | W => Val_cmpu_bool Ceq v (Vint Int.zero)
  | X => Val_cmplu_bool Ceq v (Vlong Int64.zero)
  end.

(** Integer "bit is set?" test *)

Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
  match sz with
  | W => Val.cmp_bool Cne (Val.and v (Vint (Int.shl Int.one n))) (Vint Int.zero)
  | X => Val.cmpl_bool Cne (Val.andl v (Vlong (Int64.shl' Int64.one n))) (Vlong Int64.zero)
  end.


(** Comparisons *)

Definition compare_int (rs: regset) (v1 v2: val) :=
  rs#CN <- (Val.negative (Val.sub v1 v2))
    #CZ <- (Val_cmpu Ceq v1 v2)
    #CC <- (Val_cmpu Cge v1 v2)
    #CV <- (Val.sub_overflow v1 v2).

Definition compare_long (rs: regset) (v1 v2: val) :=
  rs#CN <- (Val.negativel (Val.subl v1 v2))
    #CZ <- (Val_cmplu Ceq v1 v2)
    #CC <- (Val_cmplu Cge v1 v2)
    #CV <- (Val.subl_overflow v1 v2).

(** Semantics of [fcmp] instructions:
<<
==	N=0 Z=1 C=1 V=0
<	N=1 Z=0 C=0 V=0
>	N=0 Z=0 C=1 V=0
unord	N=0 Z=0 C=1 V=1
>>
*)

Definition compare_float (rs: regset) (v1 v2: val) :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 =>
      rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2))
        #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2))
        #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2)))
        #CV <- (Val.of_bool (negb (Float.ordered f1 f2)))
  | _, _ =>
      rs#CN <- Vundef
        #CZ <- Vundef
        #CC <- Vundef
        #CV <- Vundef
  end.

Definition compare_single (rs: regset) (v1 v2: val) :=
  match v1, v2 with
  | Vsingle f1, Vsingle f2 =>
      rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2))
        #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2))
        #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2)))
        #CV <- (Val.of_bool (negb (Float32.ordered f1 f2)))
  | _, _ =>
      rs#CN <- Vundef
        #CZ <- Vundef
        #CC <- Vundef
        #CV <- Vundef
  end.


(** Evaluating an addressing mode *)

Definition eval_addressing (a: addressing) (rs: regset): val :=
  match a with
  | ADimm base n => Val.addl rs#base (Vlong n)
  | ADreg base r => Val.addl rs#base rs#r
  | ADlsl base r n => Val.addl rs#base (Val.shll rs#r (Vint n))
  | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n))
  | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n))
  | ADadr base id ofs => Val.addl rs#base (symbol_low lk id ofs)
  | ADpostincr base n => Vundef (* not modeled yet *)
  end.

(** Auxiliaries for memory accesses *)

Definition exec_load (chunk: memory_chunk) (transf: val -> val)
                     (a: addressing) (r: preg) (rs: regset) (m: mem) :=
  SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN
  Next (rs#r <- (transf v)) m.

Definition exec_store (chunk: memory_chunk)
                      (a: addressing) (v: val)
                      (rs: regset) (m: mem) :=
  SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN
  Next rs m'.

(** Insertion of bits into an integer *)

Definition insert_in_int (x: val) (y: Z) (pos: Z) (len: Z) : val :=
  match x with
  | Vint n => Vint (Int.repr (Zinsert (Int.unsigned n) y pos len))
  | _ => Vundef
  end.

Definition insert_in_long (x: val) (y: Z) (pos: Z) (len: Z) : val :=
  match x with
  | Vlong n => Vlong (Int64.repr (Zinsert (Int64.unsigned n) y pos len))
  | _ => Vundef
  end.

(** Evaluation of shifted operands *)

Definition eval_shift_op_int (v: val) (s: shift_op): val :=
  match s with
  | SOnone => v
  | SOlsl n => Val.shl v (Vint n)
  | SOlsr n => Val.shru v (Vint n)
  | SOasr n => Val.shr v (Vint n)
  | SOror n => Val.ror v (Vint n)
  end.

Definition eval_shift_op_long (v: val) (s: shift_op): val :=
  match s with
  | SOnone => v
  | SOlsl n => Val.shll v (Vint n)
  | SOlsr n => Val.shrlu v (Vint n)
  | SOasr n => Val.shrl v (Vint n)
  | SOror n => Val.rorl v (Vint n)
  end.

(** Evaluation of sign- or zero- extended operands *)

Definition eval_extend (v: val) (x: extend_op): val :=
  match x with
  | EOsxtb n => Val.shll (Val.longofint (Val.sign_ext 8 v)) (Vint n)
  | EOsxth n => Val.shll (Val.longofint (Val.sign_ext 16 v)) (Vint n)
  | EOsxtw n => Val.shll (Val.longofint v) (Vint n)
  | EOuxtb n => Val.shll (Val.longofintu (Val.zero_ext 8 v)) (Vint n)
  | EOuxth n => Val.shll (Val.longofintu (Val.zero_ext 16 v)) (Vint n)
  | EOuxtw n => Val.shll (Val.longofintu v) (Vint n)
  | EOuxtx n => Val.shll v (Vint n)
  end.

(** Bit-level conversion from integers to FP numbers *)

Definition float32_of_bits (v: val): val :=
  match v with
  | Vint n => Vsingle (Float32.of_bits n)
  | _ => Vundef
  end.

Definition float64_of_bits (v: val): val :=
  match v with
  | Vlong n => Vfloat (Float.of_bits n)
  | _ => Vundef
  end.

(** execution of loads 
*)

Definition chunk_load_rd_a (ld: load_rd_a): memory_chunk :=
  match ld with
  | Pldrw => Mint32 
  | Pldrw_a => Many32
  | Pldrx => Mint64
  | Pldrx_a => Many64
  | Pldrb _ => Mint8unsigned
  | Pldrsb _ => Mint8signed
  | Pldrh _ => Mint16unsigned
  | Pldrsh _ => Mint16signed
  | Pldrzw => Mint32
  | Pldrsw => Mint32
  | Pldrs => Mfloat32
  | Pldrd => Mfloat64
  | Pldrd_a =>  Many64
  end.

Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk :=
  match st with
  | Pstrw   => Mint32
  | Pstrw_a => Many32
  | Pstrx   => Mint64
  | Pstrx_a => Many64
  | Pstrb   => Mint8unsigned
  | Pstrh   => Mint16unsigned
  | Pstrs   => Mfloat32
  | Pstrd   => Mfloat64
  | Pstrd_a => Many64
  end.

Definition interp_load_rd_a (ld: load_rd_a): val -> val :=
  match ld with
  | Pldrb X => Val.longofintu
  | Pldrsb X => Val.longofint
  | Pldrh X => Val.longofintu
  | Pldrsh X => Val.longofint
  | Pldrzw => Val.longofintu
  | Pldrsw => Val.longofint
  (* Changed to exhaustive list because I tend to forgot all the places I need
   * to check when changing things. *)
  | Pldrb W | Pldrsb W | Pldrh W | Pldrsh W
  | Pldrw   | Pldrw_a  | Pldrx   | Pldrx_a
  | Pldrs   | Pldrd    | Pldrd_a => fun v => v
  end.

(** TODO: redundant w.r.t Machblock ?? *)
Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
Proof.
  apply List.in_dec.
  apply Pos.eq_dec.
Qed.

(** Note: copy-paste from Machblock *)
Definition is_label (lbl: label) (bb: bblock) : bool :=
  if in_dec lbl (header bb) then true else false.

Lemma is_label_correct_true lbl bb:
  List.In lbl (header bb) <-> is_label lbl bb = true. 
Proof.
  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
Qed.

Lemma is_label_correct_false lbl bb:
  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
Proof.
  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
Qed.

(** convert a label into a position in the code *)
Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
  match lb with
  | nil => None
  | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
  end.

Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
  SOME pos <- label_pos lbl 0 (fn_blocks f) IN
  match rs#PC with
  | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
  | _ => Stuck
  end.

(** Evaluating a branch 

Warning: PC is assumed to be already pointing on the next instruction !

*)

Definition eval_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
  SOME res <- ores IN
  if res then goto_label f lbl rs m else Next rs m.

Definition  eval_neg_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
  SOME res <- ores IN
  if res then Next rs m else goto_label f lbl rs m.

Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) : outcome :=
  match cfi with
  (** Branches *)
  | Pb lbl =>
      goto_label f lbl rs m
  | Pbc cond lbl =>
      eval_branch f lbl rs m (eval_testcond cond rs)
  | Pbl id sg =>
      Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pbs id sg =>
      Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pblr r sg =>
      Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m
  | Pbr r sg =>
      Next (rs#PC <- (rs#r)) m
  | Pret r =>
      Next (rs#PC <- (rs#r)) m
  | Pcbnz sz r lbl =>
      eval_neg_branch f lbl rs m (eval_testzero sz rs#r)
  | Pcbz sz r lbl =>
      eval_branch f lbl rs m (eval_testzero sz rs#r)
  | Ptbnz sz r n lbl =>
      eval_branch f lbl rs m (eval_testbit sz rs#r n)
  | Ptbz sz r n lbl =>
      eval_neg_branch f lbl rs m (eval_testbit sz rs#r n)
  (** Pseudo-instructions *)
  | Pbtbl r tbl =>
      match (rs#X16 <- Vundef)#r with
      | Vint n =>
          SOME lbl <- list_nth_z tbl (Int.unsigned n) IN
          goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
      | _ => Stuck
      end
  end.

Definition arith_eval_p (i : arith_p) : val :=
  match i with
  | Padrp id ofs => symbol_high lk id ofs
  (** Move wide immediate *)
  | Pmovz W n pos => Vint (Int.repr (Z.shiftl n pos))
  | Pmovz X n pos => Vlong (Int64.repr (Z.shiftl n pos))
  | Pmovn W n pos => Vint (Int.repr (Z.lnot (Z.shiftl n pos)))
  | Pmovn X n pos => Vlong (Int64.repr (Z.lnot (Z.shiftl n pos)))
  (** Floating-point move *)
  | Pfmovimms f => Vsingle f
  | Pfmovimmd f => Vfloat f
  end.

Definition if_opt_bool_val (c: option bool) v1 v2: val :=
   match c with
   | Some true => v1
   | Some false =>  v2
   | None => Vundef
   end.

Definition arith_eval_pp i v :=
  match i with
  | Pmov => v
  | Pmovk W n pos => insert_in_int v n pos 16
  | Pmovk X n pos => insert_in_long v n pos 16
  | Paddadr id ofs => Val.addl v (symbol_low lk id ofs)
  | Psbfiz W r s => Val.shl (Val.sign_ext s v) (Vint r)
  | Psbfiz X r s => Val.shll (Val.sign_ext_l s v) (Vint r)
  | Psbfx W r s => Val.sign_ext s (Val.shr v (Vint r))
  | Psbfx X r s => Val.sign_ext_l s (Val.shrl v (Vint r))
  | Pubfiz W r s => Val.shl (Val.zero_ext s v) (Vint r)
  | Pubfiz X r s => Val.shll (Val.zero_ext_l s v) (Vint r)
  | Pubfx W r s => Val.zero_ext s (Val.shru v (Vint r))
  | Pubfx X r s => Val.zero_ext_l s (Val.shrlu v (Vint r))
  | Pfmov => v
  | Pfcvtds => Val.floatofsingle v
  | Pfcvtsd => Val.singleoffloat v
  | Pfabs S => Val.absfs v
  | Pfabs D => Val.absf v
  | Pfneg S => Val.negfs v
  | Pfneg D => Val.negf v
  | Pfcvtzs W S => Val.maketotal (Val.intofsingle v)
  | Pfcvtzs W D => Val.maketotal (Val.intoffloat v)
  | Pfcvtzs X S => Val.maketotal (Val.longofsingle v)
  | Pfcvtzs X D => Val.maketotal (Val.longoffloat v)
  | Pfcvtzu W S => Val.maketotal (Val.intuofsingle v)
  | Pfcvtzu W D => Val.maketotal (Val.intuoffloat v)
  | Pfcvtzu X S => Val.maketotal (Val.longuofsingle v)
  | Pfcvtzu X D => Val.maketotal (Val.longuoffloat v)
  | Paddimm W n => Val.add v (Vint (Int.repr n))
  | Paddimm X n => Val.addl v (Vlong (Int64.repr n))
  | Psubimm W n => Val.sub v (Vint (Int.repr n))
  | Psubimm X n => Val.subl v (Vlong (Int64.repr n))
  | Pscvtf S W => Val.maketotal (Val.singleofint v)
  | Pscvtf D W => Val.maketotal (Val.floatofint v)
  | Pscvtf S X => Val.maketotal (Val.singleoflong v)
  | Pscvtf D X => Val.maketotal (Val.floatoflong v)
  | Pucvtf S W => Val.maketotal (Val.singleofintu v)
  | Pucvtf D W => Val.maketotal (Val.floatofintu v)
  | Pucvtf S X => Val.maketotal (Val.singleoflongu v)
  | Pucvtf D X => Val.maketotal (Val.floatoflongu v)
  end.

Definition arith_eval_ppp i v1 v2 :=
  match i with
  | Pasrv W => Val.shr v1 v2
  | Pasrv X => Val.shrl v1 v2
  | Plslv W => Val.shl v1 v2
  | Plslv X => Val.shll v1 v2
  | Plsrv W => Val.shru v1 v2
  | Plsrv X => Val.shrlu v1 v2
  | Prorv W => Val.ror v1 v2
  | Prorv X => Val.rorl v1 v2
  | Psmulh => Val.mullhs v1 v2
  | Pumulh => Val.mullhu v1 v2
  | Psdiv W => Val.maketotal (Val.divs v1 v2)
  | Psdiv X => Val.maketotal (Val.divls v1 v2)
  | Pudiv W => Val.maketotal (Val.divu v1 v2)
  | Pudiv X => Val.maketotal (Val.divlu v1 v2)
  | Paddext x => Val.addl v1 (eval_extend v2 x)
  | Psubext x => Val.subl v2 (eval_extend v2 x)
  | Pfadd S => Val.addfs v1 v2
  | Pfadd D => Val.addf v1 v2
  | Pfdiv S => Val.divfs v1 v2
  | Pfdiv D => Val.divf v1 v2
  | Pfmul S => Val.mulfs v1 v2
  | Pfmul D => Val.mulf v1 v2
  | Pfsub S => Val.subfs v1 v2
  | Pfsub D => Val.subf v1 v2
  end.

Definition arith_rr0r_isize (i: arith_rr0r) :=
  match i with
  | Padd is _ => is
  | Psub is _ => is
  | Pand is _ => is
  | Pbic is _ => is
  | Peon is _ => is
  | Peor is _ => is
  | Porr is _ => is
  | Porn is _ => is
  end.

(* obtain v1 by [ir0 (arith_rr0r_isize i) rs s1] *)
Definition arith_eval_rr0r i v1 v2 :=
  match i with
  | Padd W s => Val.add v1 (eval_shift_op_int v2 s)
  | Padd X s => Val.addl v1 (eval_shift_op_long v2 s)
  | Psub W s => Val.sub v1 (eval_shift_op_int v2 s)
  | Psub X s => Val.subl v1 (eval_shift_op_long v2 s)
  | Pand W s => Val.and v1 (eval_shift_op_int v2 s)
  | Pand X s => Val.andl v1 (eval_shift_op_long v2 s)
  | Pbic W s => Val.and v1 (Val.notint (eval_shift_op_int v2 s))
  | Pbic X s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s))
  | Peon W s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s))
  | Peon X s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s))
  | Peor W s => Val.xor v1 (eval_shift_op_int v2 s)
  | Peor X s => Val.xorl v1 (eval_shift_op_long v2 s)
  | Porr W s => Val.or v1 (eval_shift_op_int v2 s)
  | Porr X s => Val.orl v1 (eval_shift_op_long v2 s)
  | Porn W s => Val.or v1 (Val.notint (eval_shift_op_int v2 s))
  | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
  end.

Definition arith_rr0_isize (i : arith_rr0) :=
  match i with
  | Pandimm is _ | Peorimm is _ | Porrimm is _ => is
  end.

(* obtain v by [ir0 (arith_rr0_isize i) rs s] *)
Definition arith_eval_rr0 i v :=
  match i with
  | Pandimm W n => Val.and v (Vint (Int.repr n))
  | Pandimm X n => Val.andl v (Vlong (Int64.repr n))
  | Peorimm W n => Val.xor v (Vint (Int.repr n))
  | Peorimm X n => Val.xorl v (Vlong (Int64.repr n))
  | Porrimm W n => Val.or v (Vint (Int.repr n))
  | Porrimm X n => Val.orl v (Vlong (Int64.repr n))
  end.

Definition arith_arrrr0_isize (i : arith_arrrr0) :=
  match i with
  | Pmadd is | Pmsub is => is
  end.

(* obtain v3 by [ir0 (arith_arrrr0_isize i) rs s3] *)
Definition arith_eval_arrrr0 i v1 v2 v3 :=
  match i with
  | Pmadd W => Val.add v3 (Val.mul v1 v2)
  | Pmadd X => Val.addl v3 (Val.mull v1 v2)
  | Pmsub W => Val.sub v3 (Val.mul v1 v2)
  | Pmsub X => Val.subl v3 (Val.mull v1 v2)
  end.

Definition arith_prepare_comparison_pp i (v1 v2 : val) :=
  match i with
  | Pcmpext x => (v1, (eval_extend v2 x))
  | Pcmnext x => (v1, (Val.negl (eval_extend v2 x)))
  | Pfcmp _ => (v1, v2)
  end.

Definition arith_comparison_r0r_isize i :=
  match i with
  | Pcmp is _ => is
  | Pcmn is _ => is
  | Ptst is _ => is
  end.

Definition arith_prepare_comparison_r0r i v1 v2 :=
  match i with
  | Pcmp W s => (v1, (eval_shift_op_int v2 s))
  | Pcmp X s => (v1, (eval_shift_op_long v2 s))
  | Pcmn W s => (v1, (Val.neg (eval_shift_op_int v2 s)))
  | Pcmn X s => (v1, (Val.negl (eval_shift_op_long v2 s)))
  | Ptst W s => ((Val.and v1 (eval_shift_op_int v2 s)), (Vint Int.zero))
  | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
  end.

Definition arith_prepare_comparison_p i v :=
  match i with
  | Pcmpimm W n => (v, (Vint (Int.repr n)))
  | Pcmpimm X n => (v, (Vlong (Int64.repr n)))
  | Pcmnimm W n => (v, (Vint (Int.neg (Int.repr n))))
  | Pcmnimm X n => (v, (Vlong (Int64.neg (Int64.repr n))))
  | Ptstimm W n => ((Val.and v (Vint (Int.repr n))), (Vint Int.zero))
  | Ptstimm X n => ((Val.andl v (Vlong (Int64.repr n))), (Vlong Int64.zero))
  | Pfcmp0 S => (v, (Vsingle Float32.zero))
  | Pfcmp0 D => (v, (Vfloat Float.zero))
  end.

Definition arith_comparison_pp_compare i :=
  match i with
  | Pcmpext _ | Pcmnext _ => compare_long
  | Pfcmp S => compare_single
  | Pfcmp D => compare_float
  end.

Definition arith_comparison_p_compare i :=
   match i with
   | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int
   | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long
   | Pfcmp0 S => compare_single
   | Pfcmp0 D => compare_float
   end.

Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
  match ai with
  | PArithP i d => rs#d <- (arith_eval_p i)
  | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s)
  | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2)

  | PArithRR0R i d s1 s2 => rs#d <- (arith_eval_rr0r i (ir0 (arith_rr0r_isize i) rs s1) rs#s2)

  | PArithRR0 i d s => rs#d <- (arith_eval_rr0 i (ir0 (arith_rr0_isize i) rs s))

  | PArithARRRR0 i d s1 s2 s3 =>
    rs#d <- (arith_eval_arrrr0 i rs#s1 rs#s2 (ir0 (arith_arrrr0_isize i) rs s3))

  | PArithComparisonPP i s1 s2 =>
    let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in
    arith_comparison_pp_compare i rs v1 v2
  | PArithComparisonR0R i s1 s2 =>
    let is := arith_comparison_r0r_isize i in
    let (v1, v2) := arith_prepare_comparison_r0r i (ir0 is rs s1) rs#s2 in
    (if is (* is W *) then compare_int else compare_long) rs v1 v2
  | PArithComparisonP i s =>
    let (v1, v2) := arith_prepare_comparison_p i rs#s in
    arith_comparison_p_compare i rs v1 v2
  | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero))
  | Pfmovi S d s => rs#d <- (float32_of_bits rs##s)
  | Pfmovi D d s => rs#d <- (float64_of_bits rs###s)
  | Pcsel d s1 s2 c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (rs#s1) (rs#s2))
  | Pfnmul S d s1 s2 => rs#d <- (Val.negfs (Val.mulfs rs#s1 rs#s2))
  | Pfnmul D d s1 s2 => rs#d <- (Val.negf (Val.mulf rs#s1 rs#s2))
  end.

(* basic exec *)
Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
  match b with
  | PArith ai => Next (exec_arith_instr ai rs) m
  | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd rs m
  | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m
  | Pallocframe sz pos =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      SOME m2 <- Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP IN
      Next (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef) m2
  | Pfreeframe sz pos =>
      SOME v <- Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) IN
      match rs#SP with
      | Vptr stk ofs =>
        SOME m' <- Mem.free m stk 0 sz IN
        Next (rs#SP <- v #X16 <- Vundef) m'
      | _ => Stuck
      end
  | Ploadsymbol rd id =>
      Next (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pcvtsw2x rd r1 =>
      Next (rs#rd <- (Val.longofint rs#r1)) m
  | Pcvtuw2x rd r1 =>
      Next (rs#rd <- (Val.longofintu rs#r1)) m
  | Pcvtx2w rd =>
      Next (rs#rd <- (Val.loword rs#rd)) m
  end.

(* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !

(** Execution of a single instruction [i] in initial state
    [rs] and [m].  Return updated state.  For instructions
    that correspond to actual AArch64 instructions, the cases are
    straightforward transliterations of the informal descriptions
    given in the ARMv8 reference manuals.  For pseudo-instructions,
    refer to the informal descriptions given above.

    Note that we set to [Vundef] the registers used as temporaries by
    the expansions of the pseudo-instructions, so that the code we
    generate cannot use those registers to hold values that must
    survive the execution of the pseudo-instruction.
*)

Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
  match i with
  (** Branches *)
  | Pb lbl =>
      goto_label f lbl rs m
  | Pbc cond lbl =>
      match eval_testcond cond rs with
      | Some true => goto_label f lbl rs m
      | Some false => Next (nextinstr rs) m
      | None => Stuck
      end
  | Pbl id sg =>
      Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pbs id sg =>
      Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pblr r sg =>
      Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (rs#r)) m
  | Pbr r sg =>
      Next (rs#PC <- (rs#r)) m
  | Pret r =>
      Next (rs#PC <- (rs#r)) m
  | Pcbnz sz r lbl =>
      match eval_testzero sz rs#r m with
      | Some true => Next (nextinstr rs) m
      | Some false => goto_label f lbl rs m
      | None => Stuck
      end
  | Pcbz sz r lbl =>
      match eval_testzero sz rs#r m with
      | Some true => goto_label f lbl rs m
      | Some false => Next (nextinstr rs) m
      | None => Stuck
      end
  | Ptbnz sz r n lbl =>
      match eval_testbit sz rs#r n with
      | Some true => goto_label f lbl rs m
      | Some false => Next (nextinstr rs) m
      | None => Stuck
      end
  | Ptbz sz r n lbl =>
      match eval_testbit sz rs#r n with
      | Some true => Next (nextinstr rs) m
      | Some false => goto_label f lbl rs m
      | None => Stuck
      end
  (** Memory loads and stores *)
  | Pldrw rd a =>
      exec_load Mint32 (fun v => v) a rd rs m
  | Pldrw_a rd a =>
      exec_load Many32 (fun v => v) a rd rs m
  | Pldrx rd a =>
      exec_load Mint64 (fun v => v) a rd rs m
  | Pldrx_a rd a =>
      exec_load Many64 (fun v => v) a rd rs m
  | Pldrb W rd a =>
      exec_load Mint8unsigned (fun v => v) a rd rs m
  | Pldrb X rd a =>
      exec_load Mint8unsigned Val.longofintu a rd rs m
  | Pldrsb W rd a =>
      exec_load Mint8signed (fun v => v) a rd rs m
  | Pldrsb X rd a =>
      exec_load Mint8signed Val.longofint a rd rs m
  | Pldrh W rd a =>
      exec_load Mint16unsigned (fun v => v) a rd rs m
  | Pldrh X rd a =>
      exec_load Mint16unsigned Val.longofintu a rd rs m
  | Pldrsh W rd a =>
      exec_load Mint16signed (fun v => v) a rd rs m
  | Pldrsh X rd a =>
      exec_load Mint16signed Val.longofint a rd rs m
  | Pldrzw rd a =>
      exec_load Mint32 Val.longofintu a rd rs m
  | Pldrsw rd a =>
      exec_load Mint32 Val.longofint a rd rs m
  | Pstrw r a =>
      exec_store Mint32 a rs#r rs m
  | Pstrw_a r a =>
      exec_store Many32 a rs#r rs m
  | Pstrx r a =>
      exec_store Mint64 a rs#r rs m
  | Pstrx_a r a =>
      exec_store Many64 a rs#r rs m
  | Pstrb r a =>
      exec_store Mint8unsigned a rs#r rs m
  | Pstrh r a =>
      exec_store Mint16unsigned a rs#r rs m
  (** Integer arithmetic, immediate *)
  | Paddimm W rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.add rs#r1 (Vint (Int.repr n))))) m
  | Paddimm X rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.addl rs#r1 (Vlong (Int64.repr n))))) m
  | Psubimm W rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.sub rs#r1 (Vint (Int.repr n))))) m
  | Psubimm X rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.subl rs#r1 (Vlong (Int64.repr n))))) m
  | Pcmpimm W r1 n =>
      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.repr n)) m)) m
  | Pcmpimm X r1 n =>
      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)) m)) m
  | Pcmnimm W r1 n =>
      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))) m)) m
  | Pcmnimm X r1 n =>
      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))) m)) m
  (** Move integer register *)
  | Pmov rd r1 =>
      Next (nextinstr (rs#rd <- (rs#r1))) m
  (** Logical, immediate *)
  | Pandimm W rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.and rs##r1 (Vint (Int.repr n))))) m
  | Pandimm X rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.andl rs###r1 (Vlong (Int64.repr n))))) m
  | Peorimm W rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.xor rs##r1 (Vint (Int.repr n))))) m
  | Peorimm X rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (Vlong (Int64.repr n))))) m
  | Porrimm W rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.or rs##r1 (Vint (Int.repr n))))) m
  | Porrimm X rd r1 n =>
      Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Vlong (Int64.repr n))))) m
  | Ptstimm W r1 n =>
      Next (nextinstr (compare_int rs (Val.and rs#r1 (Vint (Int.repr n))) (Vint Int.zero) m)) m
  | Ptstimm X r1 n =>
      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero) m)) m
  (** Move wide immediate *)
  | Pmovz W rd n pos =>
      Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.shiftl n pos))))) m
  | Pmovz X rd n pos =>
      Next (nextinstr (rs#rd <- (Vlong (Int64.repr (Z.shiftl n pos))))) m
  | Pmovn W rd n pos =>
      Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.lnot (Z.shiftl n pos)))))) m
  | Pmovn X rd n pos =>
      Next (nextinstr (rs#rd <- (Vlong (Int64.repr (Z.lnot (Z.shiftl n pos)))))) m
  | Pmovk W rd n pos =>
      Next (nextinstr (rs#rd <- (insert_in_int rs#rd n pos 16))) m
  | Pmovk X rd n pos =>
      Next (nextinstr (rs#rd <- (insert_in_long rs#rd n pos 16))) m
  (** PC-relative addressing *)
  | Padrp rd id ofs =>
      Next (nextinstr (rs#rd <- (symbol_high ge id ofs))) m
  | Paddadr rd r1 id ofs =>
      Next (nextinstr (rs#rd <- (Val.addl rs#r1 (symbol_low ge id ofs)))) m
  (** Bit-field operations *)
  | Psbfiz W rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.shl (Val.sign_ext s rs#r1) (Vint r)))) m
  | Psbfiz X rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.shll (Val.sign_ext_l s rs#r1) (Vint r)))) m
  | Psbfx W rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.sign_ext s (Val.shr rs#r1 (Vint r))))) m
  | Psbfx X rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.sign_ext_l s (Val.shrl rs#r1 (Vint r))))) m
  | Pubfiz W rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.shl (Val.zero_ext s rs#r1) (Vint r)))) m
  | Pubfiz X rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.shll (Val.zero_ext_l s rs#r1) (Vint r)))) m
  | Pubfx W rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.zero_ext s (Val.shru rs#r1 (Vint r))))) m
  | Pubfx X rd r1 r s =>
      Next (nextinstr (rs#rd <- (Val.zero_ext_l s (Val.shrlu rs#r1 (Vint r))))) m
  (** Integer arithmetic, shifted register *)
  | Padd W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.add rs##r1 (eval_shift_op_int rs#r2 s)))) m
  | Padd X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.addl rs###r1 (eval_shift_op_long rs#r2 s)))) m
  | Psub W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.sub rs##r1 (eval_shift_op_int rs#r2 s)))) m
  | Psub X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.subl rs###r1 (eval_shift_op_long rs#r2 s)))) m
  | Pcmp W r1 r2 s =>
      Next (nextinstr (compare_int rs rs##r1 (eval_shift_op_int rs#r2 s) m)) m
  | Pcmp X r1 r2 s =>
      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s) m)) m
  | Pcmn W r1 r2 s =>
      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)) m)) m
  | Pcmn X r1 r2 s =>
      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)) m)) m
  (** Integer arithmetic, extending register *)
  | Paddext rd r1 r2 x =>
      Next (nextinstr (rs#rd <- (Val.addl rs#r1 (eval_extend rs#r2 x)))) m
  | Psubext rd r1 r2 x =>
      Next (nextinstr (rs#rd <- (Val.subl rs#r1 (eval_extend rs#r2 x)))) m
  | Pcmpext r1 r2 x =>
      Next (nextinstr (compare_long rs rs#r1 (eval_extend rs#r2 x) m)) m
  | Pcmnext r1 r2 x =>
      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)) m)) m
  (** Logical, shifted register *)
  | Pand W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.and rs##r1 (eval_shift_op_int rs#r2 s)))) m
  | Pand X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)))) m
  | Pbic W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.and rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m
  | Pbic X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.andl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
  | Peon W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.xor rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m
  | Peon X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
  | Peor W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.xor rs##r1 (eval_shift_op_int rs#r2 s)))) m
  | Peor X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (eval_shift_op_long rs#r2 s)))) m
  | Porr W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.or rs##r1 (eval_shift_op_int rs#r2 s)))) m
  | Porr X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.orl rs###r1 (eval_shift_op_long rs#r2 s)))) m
  | Porn W rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.or rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m
  | Porn X rd r1 r2 s =>
      Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
  | Ptst W r1 r2 s =>
      Next (nextinstr (compare_int rs (Val.and rs##r1 (eval_shift_op_int rs#r2 s)) (Vint Int.zero) m)) m
  | Ptst X r1 r2 s =>
      Next (nextinstr (compare_long rs (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)) (Vlong Int64.zero) m)) m
  (** Variable shifts *)
  | Pasrv W rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2))) m
  | Pasrv X rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.shrl rs#r1 rs#r2))) m
  | Plslv W rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m
  | Plslv X rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.shll rs#r1 rs#r2))) m
  | Plsrv W rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m
  | Plsrv X rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.shrlu rs#r1 rs#r2))) m
  | Prorv W rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.ror rs#r1 rs#r2))) m
  | Prorv X rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.rorl rs#r1 rs#r2))) m
  (** Conditional data processing *)
  | Pcsel rd r1 r2 cond =>
      let v :=
        match eval_testcond cond rs with
        | Some true => rs#r1
        | Some false => rs#r2
        | None => Vundef
        end in
      Next (nextinstr (rs#rd <- v)) m
  | Pcset rd cond =>
      let v :=
        match cond rs with
        | Some true => Vint Int.one
        | Some false => Vint Int.zero
        | None => Vundef
        end in
      Next (nextinstr (rs#rd <- v)) m
  (** Integer multiply/divide *)
  | Pmadd W rd r1 r2 r3 =>
      Next (nextinstr (rs#rd <- (Val.add rs##r3 (Val.mul rs#r1 rs#r2)))) m
  | Pmadd X rd r1 r2 r3 =>
      Next (nextinstr (rs#rd <- (Val.addl rs###r3 (Val.mull rs#r1 rs#r2)))) m
  | Pmsub W rd r1 r2 r3 =>
      Next (nextinstr (rs#rd <- (Val.sub rs##r3 (Val.mul rs#r1 rs#r2)))) m
  | Pmsub X rd r1 r2 r3 =>
      Next (nextinstr (rs#rd <- (Val.subl rs###r3 (Val.mull rs#r1 rs#r2)))) m
  | Psmulh rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.mullhs rs#r1 rs#r2))) m
  | Pumulh rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.mullhu rs#r1 rs#r2))) m
  | Psdiv W rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m
  | Psdiv X rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divls rs#r1 rs#r2)))) m
  | Pudiv W rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m
  | Pudiv X rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divlu rs#r1 rs#r2)))) m
  (** Floating-point loads and stores *)
  | Pldrs rd a =>
      exec_load Mfloat32 (fun v => v) a rd rs m
  | Pldrd rd a =>
      exec_load Mfloat64 (fun v => v) a rd rs m
  | Pldrd_a rd a =>
      exec_load Many64 (fun v => v) a rd rs m
  | Pstrs r a =>
      exec_store Mfloat32 a rs#r rs m
  | Pstrd r a =>
      exec_store Mfloat64 a rs#r rs m
  | Pstrd_a r a =>
      exec_store Many64 a rs#r rs m
  (** Floating-point move *)
  | Pfmov rd r1 =>
      Next (nextinstr (rs#rd <- (rs#r1))) m
  | Pfmovimms rd f =>
      Next (nextinstr (rs#rd <- (Vsingle f))) m
  | Pfmovimmd rd f =>
      Next (nextinstr (rs#rd <- (Vfloat f))) m
  | Pfmovi S rd r1 =>
      Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
  | Pfmovi D rd r1 =>
      Next (nextinstr (rs#rd <- (float64_of_bits rs###r1))) m
  (** Floating-point conversions *)
  | Pfcvtds rd r1 =>
      Next (nextinstr (rs#rd <- (Val.floatofsingle rs#r1))) m
  | Pfcvtsd rd r1 =>
      Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m
  | Pfcvtzs W S rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intofsingle rs#r1)))) m
  | Pfcvtzs W D rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
  | Pfcvtzs X S rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longofsingle rs#r1)))) m
  | Pfcvtzs X D rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m
  | Pfcvtzu W S rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intuofsingle rs#r1)))) m
  | Pfcvtzu W D rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m
  | Pfcvtzu X S rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longuofsingle rs#r1)))) m
  | Pfcvtzu X D rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longuoffloat rs#r1)))) m
  | Pscvtf S W rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofint rs#r1)))) m
  | Pscvtf D W rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m
  | Pscvtf S X rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflong rs#r1)))) m
  | Pscvtf D X rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m
  | Pucvtf S W rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofintu rs#r1)))) m
  | Pucvtf D W rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m
  | Pucvtf S X rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflongu rs#r1)))) m
  | Pucvtf D X rd r1 =>
      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflongu rs#r1)))) m
  (** Floating-point arithmetic *)
  | Pfabs S rd r1 =>
      Next (nextinstr (rs#rd <- (Val.absfs rs#r1))) m
  | Pfabs D rd r1 =>
      Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m
  | Pfneg S rd r1 =>
      Next (nextinstr (rs#rd <- (Val.negfs rs#r1))) m
  | Pfneg D rd r1 =>
      Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m
  | Pfadd S rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
  | Pfadd D rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m
  | Pfdiv S rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.divfs rs#r1 rs#r2))) m
  | Pfdiv D rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
  | Pfmul S rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.mulfs rs#r1 rs#r2))) m
  | Pfmul D rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m
  | Pfnmul S rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.negfs (Val.mulfs rs#r1 rs#r2)))) m
  | Pfnmul D rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.negf (Val.mulf rs#r1 rs#r2)))) m
  | Pfsub S rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.subfs rs#r1 rs#r2))) m
  | Pfsub D rd r1 r2 =>
      Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
  (** Floating-point comparison *)
  | Pfcmp S r1 r2 =>
      Next (nextinstr (compare_single rs rs#r1 rs#r2)) m
  | Pfcmp D r1 r2 =>
      Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
  | Pfcmp0 S r1 =>
      Next (nextinstr (compare_single rs rs#r1 (Vsingle Float32.zero))) m
  | Pfcmp0 D r1 =>
      Next (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m
  (** Floating-point conditional select *)
  | Pfsel rd r1 r2 cond =>
      let v :=
        match eval_testcond cond rs with
        | Some true => rs#r1
        | Some false => rs#r2
        | None => Vundef
        end in
      Next (nextinstr (rs#rd <- v)) m
  (** Pseudo-instructions *)
  | Pallocframe sz pos =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with
      | None => Stuck
      | Some m2 => Next (nextinstr (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2
      end
  | Pfreeframe sz pos =>
      match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with
      | None => Stuck
      | Some v =>
          match rs#SP with
          | Vptr stk ofs =>
              match Mem.free m stk 0 sz with
              | None => Stuck
              | Some m' => Next (nextinstr (rs#SP <- v #X16 <- Vundef)) m'
              end
          | _ => Stuck
          end
      end
  | Plabel lbl =>
      Next (nextinstr rs) m
  | Ploadsymbol rd id =>
      Next (nextinstr (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero))) m
  | Pcvtsw2x rd r1 =>
      Next (nextinstr (rs#rd <- (Val.longofint rs#r1))) m
  | Pcvtuw2x rd r1 =>
      Next (nextinstr (rs#rd <- (Val.longofintu rs#r1))) m
  | Pcvtx2w rd =>
      Next (nextinstr (rs#rd <- (Val.loword rs#rd))) m
  | Pbtbl r tbl =>
      match (rs#X16 <- Vundef)#r with
      | Vint n =>
          match list_nth_z tbl (Int.unsigned n) with
          | None => Stuck
          | Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
          end
      | _ => Stuck
      end
  | Pbuiltin ef args res => Stuck    (**r treated specially below *)
  (** The following instructions and directives are not generated directly
      by Asmgen, so we do not model them. *)
  | Pldp _ _ _
  | Pstp _ _ _
  | Pcls _ _ _
  | Pclz _ _ _
  | Prev _ _ _
  | Prev16 _ _ _
  | Pfsqrt _ _ _
  | Pfmadd _ _ _ _ _
  | Pfmsub _ _ _ _ _
  | Pfnmadd _ _ _ _ _
  | Pfnmsub _ _ _ _ _
  | Pnop
  | Pcfi_adjust _ 
  | Pcfi_rel_offset _ =>
      Stuck
  end.
*)

(** Translation of the LTL/Linear/Mach view of machine registers
  to the AArch64 view.  Note that no LTL register maps to [X16],
  [X18], nor [X30].
  [X18] is reserved as the platform register and never used by the
  code generated by CompCert.
  [X30] is used for the return address, and can also be used as temporary.
  [X16] can be used as temporary. *)

Definition preg_of (r: mreg) : preg :=
  match r with
  | R0 => X0   | R1 => X1   | R2 => X2   | R3 => X3
  | R4 => X4   | R5 => X5   | R6 => X6   | R7 => X7
  | R8 => X8   | R9 => X9   | R10 => X10 | R11 => X11
  | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15
  | R17 => X17 | R19 => X19
  | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23
  | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27
  | R28 => X28 | R29 => X29
  | F0 => D0   | F1 => D1   | F2 => D2   | F3 => D3
  | F4 => D4   | F5 => D5   | F6 => D6   | F7 => D7
  | F8 => D8   | F9 => D9   | F10 => D10 | F11 => D11
  | F12 => D12 | F13 => D13 | F14 => D14 | F15 => D15
  | F16 => D16 | F17 => D17 | F18 => D18 | F19 => D19
  | F20 => D20 | F21 => D21 | F22 => D22 | F23 => D23
  | F24 => D24 | F25 => D25 | F26 => D26 | F27 => D27
  | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31
  end.

(** Undefine all registers except SP and callee-save registers *)

Definition undef_caller_save_regs (rs: regset) : regset :=
  fun r =>
    if preg_eq r SP
    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
    then rs r
    else Vundef.

(** Extract the values of the arguments of an external call.
    We exploit the calling conventions from module [Conventions], except that
    we use AArch64 registers instead of locations. *)

Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
  | extcall_arg_reg: forall r,
      extcall_arg rs m (R r) (rs (preg_of r))
  | extcall_arg_stack: forall ofs ty bofs v,
      bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
      Mem.loadv (chunk_of_type ty) m
                (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v ->
      extcall_arg rs m (Locations.S Outgoing ofs ty) v.

Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
  | extcall_arg_one: forall l v,
      extcall_arg rs m l v ->
      extcall_arg_pair rs m (One l) v
  | extcall_arg_twolong: forall hi lo vhi vlo,
      extcall_arg rs m hi vhi ->
      extcall_arg rs m lo vlo ->
      extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).

Definition extcall_arguments
    (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
  list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.

Definition loc_external_result (sg: signature) : rpair preg :=
  map_rpair preg_of (loc_result sg).


(**  execution of the body of a bblock *)
Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
  match body with
  | nil => Next rs m
  | bi::body' => 
     SOME o <- exec_basic bi rs m IN
     exec_body body' (_rs o) (_m o)
  end.

Definition incrPC size_b (rs: regset) :=
  rs#PC <- (Val.offset_ptr rs#PC size_b).

(**  execution of the exit instruction of a bblock *)
Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) -> trace -> regset -> mem -> Prop :=
  | none_step:
      exec_exit f size_b rs m None E0 (incrPC size_b rs) m
  | cfi_step (cfi: cf_instruction) rs' m':
      exec_cfi f cfi (incrPC size_b rs) m = Next rs' m' ->
      exec_exit f size_b rs m (Some (PCtlFlow cfi)) E0 rs' m'
  | builtin_step ef args res vargs t vres rs' m':
      eval_builtin_args ge rs rs#SP m args vargs ->
      external_call ef ge vargs m t vres m' ->
      rs' = incrPC size_b
              (set_res res vres
                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
      exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m'
      .

Definition exec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (t:trace) (rs':regset) (m':mem): Prop
  := exists rs1 m1, exec_body (body b) rs m = Next rs1 m1 /\  exec_exit f (Ptrofs.repr (size b)) rs1 m1 (exit b) t rs' m'.

Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
  match lb with
  | nil => None
  | b :: il => 
    if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
    else if zeq pos 0 then Some b
    else find_bblock (pos - (size b)) il
  end.

(** Execution of the instruction at [rs PC]. *)

Inductive step: state -> trace -> state -> Prop :=
  | exec_step_internal:
      forall b ofs f bi rs m t rs' m',
      rs PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi ->
      exec_bblock f bi rs m t rs' m' ->
      step (State rs m) t (State rs' m')
  | exec_step_external:
      forall b ef args res rs m t rs' m',
      rs PC = Vptr b Ptrofs.zero ->
      Genv.find_funct_ptr ge b = Some (External ef) ->
      external_call ef ge args m t res m' ->
      extcall_arguments rs m (ef_sig ef) args ->
      rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) ->
      step (State rs m) t (State rs' m')
  .


End RELSEM.


(** Execution of whole programs. *)

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall m0,
      Genv.init_mem p = Some m0 ->
      let ge := Genv.globalenv p in
      let rs0 :=
        (Pregmap.init Vundef)
        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
        # RA <- Vnullptr
        # SP <- Vnullptr in
      initial_state p (State rs0 m0).

Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall rs m r,
      rs#PC = Vnullptr ->
      rs#X0 = Vint r ->
      final_state (State rs m) r.

Definition semantics (lk: aarch64_linker) (p: program) :=
  Semantics (step lk) (initial_state p) final_state (Genv.globalenv p).