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

Local Open Scope option_monad_scope.

(** * Abstract syntax *)

(* 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 dreg)) (res: builtin_res dreg)  (**r built-in function (pseudo) *)
  .

Coercion PCtlFlow: cf_instruction >-> control.

(** Basic instructions *)

(* Loads waiting for (rd: dreg) (a: addressing)
 * XXX Use dreg 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 : dreg)
  | PArithPP (i : arith_pp) (rd rs : dreg)
  | PArithPPP (i : arith_ppp) (rd r1 r2 : dreg)
  | 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 : dreg)
  | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg)
  | PArithComparisonP (i : arith_comparison_p) (r1 : dreg)
  (* 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 : dreg) (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: dreg) (a: addressing)                  (**r TODO *)
  | PStore (st: store_rs_a) (r: dreg) (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 *)

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

Definition genv := Genv.t fundef unit.

Section RELSEM.

Variable lk: aarch64_linker.
Variable ge: genv.

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


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

(**  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 (fun (r: dreg) => rs r) rs#SP m args vargs ->
      external_call ef ge vargs m t vres m' ->
      rs' = incrPC size_b
              (set_res (map_builtin_res DR 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).