(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*         Xavier Leroy, Collège de France and INRIA Paris             *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Abstract syntax and semantics for AArch64 assembly language 

W.r.t Asmblock, this is a "flat" syntax and semantics of "aarch64" assembly:
  - without the basic block structure
  - without the hierarchy of instructions.

*)

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.

Inductive dreg : Type :=
  | IR: iregsp -> dreg  (**r 64- or 32-bit integer registers *)
  | FR: freg -> dreg.   (**r double- or single-precision float registers *)

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

Inductive preg: Type :=
  | DR: dreg -> preg     (** see dreg **)
  | CR: crbit -> preg    (**r bits in the condition register *)
  | PC: preg.            (**r program counter *)

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

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

Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
Proof. decide equality. apply dreg_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).

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 *)
  | Pldpw (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int32 *)
  | Pldpx (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (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 *)
  | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two int32 *)
  | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (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 *)
  | Prbit (sz: isize) (rd r1: ireg)                                   (**r reverse bits *)
  (** 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 *)
  | Pldps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two float32 *)
  | Pldpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two float64 *)
  | 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 *)
  | Pstps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two float32 *)
  | Pstpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two float64 *)
  (** 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] *)
  | Pfmax (sz: fsize) (rd r1 r2: freg)                                (**r maximum *)
  | Pfmin (sz: fsize) (rd r1 r2: freg)                                (**r minimum *)
  (** 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 *)
.

Definition code := list instruction.
Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
Definition genv := Genv.t fundef unit.

(** The two functions below axiomatize how the linker processes
  symbolic references [symbol + offset].  It computes the
  difference between the address and the PC, and splits it into:
  - 12 low bits usable as an offset in an addressing mode;
  - 21 high bits usable as argument to the ADRP instruction.

  In CompCert's model, we cannot really describe PC-relative addressing,
  but we can claim that the address of [symbol + offset] decomposes
  as the sum of
  - a low part, usable as an offset in an addressing mode;
  - a high part, usable as argument to the ADRP instruction. *)

Parameter symbol_low: genv -> ident -> ptrofs -> val.
Parameter symbol_high: genv -> ident -> ptrofs -> val.

Axiom symbol_high_low:
  forall (ge: genv) (id: ident) (ofs: ptrofs),
  Val.addl (symbol_high ge id ofs) (symbol_low ge id ofs) = Genv.symbol_address ge id ofs.

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

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

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

(** 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.mxcmpu_bool Ceq v (Vint Int.zero)
  | X => Val.mxcmplu_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.mxcmpu Ceq v1 v2)
    #CC <- (Val.mxcmpu 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.mxcmplu Ceq v1 v2)
    #CC <- (Val.mxcmplu 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.

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

(* Recognition of FP numbers that are supported by the fmov #imm instructions:
   "a normalized binary floating point encoding with 1 sign bit,
    4 bits of fraction and a 3-bit exponent"
*)

Definition is_immediate_float64 (f: float): bool :=
  let bits := Float.to_bits f in
  let exp :=
    Int64.sub
      (Int64.and (Int64.shr' bits (Int.repr 52))
        (Int64.repr 2047)) (Int64.repr 1023) in
  let mant :=
    Int64.and bits (Int64.repr 4503599627370495) in
    andb (Int64.cmp Cge exp (Int64.repr (-3)))
    (andb (Int64.cmp Cle exp (Int64.repr 4))
      (Int64.eq
        (Int64.and mant
          (Int64.repr 4222124650659840)) mant)).

Definition is_immediate_float32 (f: float32): bool :=
  let bits := Float32.to_bits f in
  let exp :=
    Int.sub
      (Int.and (Int.shr bits (Int.repr 23))
        (Int.repr 255)) (Int.repr 127) in
  let mant :=
    Int.and bits (Int.repr 8388607) in
    andb (Int.cmp Cge exp (Int.repr (-3)))
    (andb (Int.cmp Cle exp (Int.repr 4))
      (Int.eq
        (Int.and mant
          (Int.repr 7864320)) mant)).

(** 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 dreg_of (r: mreg) : dreg :=
  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.

Definition preg_of (r: mreg) : preg :=
  dreg_of r.

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

(** Looking up instructions in a code sequence by position. *)

Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction :=
  match c with
  | nil => None
  | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il
  end.

(** Position corresponding to a label *)

Definition is_label (lbl: label) (instr: instruction) : bool :=
  match instr with
  | Plabel lbl' => if peq lbl lbl' then true else false
  | _ => false
  end.

Lemma is_label_correct:
  forall lbl instr,
  if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl.
Proof.
  intros.  destruct instr; simpl; try discriminate. destruct (peq lbl lbl0); congruence.
Qed.

Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
  match c with
  | nil => None
  | instr :: c' =>
      if is_label lbl instr then Some pos else label_pos lbl (pos + 1) c'
  end.

Definition nextinstr (rs: regset) :=
  rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one).

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

Section RELSEM.

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 ge id ofs)
  | ADpostincr base n => Vundef
  end.

Definition is_pair_addressing_mode_correct (a: addressing): bool :=
  match a with
  | ADimm _ _ => true
  | _ => false
  end.

Definition get_offset_addr (a: addressing) (ofs: Z) : addressing :=
  match a with
  | ADimm base n => (ADimm base (Int64.add n (Int64.repr ofs)))
  | _ => a
  end.

(** Auxiliaries for memory accesses *)

Definition exec_load (chunk: memory_chunk) (transf: val -> val)
                     (a: addressing) (r: preg) (rs: regset) (m: mem) :=
  match Mem.loadv chunk m (eval_addressing a rs) with
  | None => Stuck
  | Some v => Next (nextinstr (rs#r <- (transf v))) m
  end.

Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
                     (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) :=
  if is_pair_addressing_mode_correct a then
    let addr := (eval_addressing a rs) in
    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
    let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
        match Mem.loadv chk1 m addr with
        | None => Stuck
        | Some v1 =>
            match Mem.loadv chk2 m addr' with
            | None => Stuck
            | Some v2 =>
                Next (nextinstr ((rs#rd1 <- (transf v1))#rd2 <- (transf v2))) m
            end
        end
  else Stuck.

Definition exec_store (chunk: memory_chunk)
                      (a: addressing) (v: val)
                      (rs: regset) (m: mem) :=
  match Mem.storev chunk m (eval_addressing a rs) v with
  | None => Stuck
  | Some m' => Next (nextinstr rs) m'
  end.

Definition exec_store_double (chk1 chk2: memory_chunk)
                      (a: addressing) (v1 v2: val)
                      (rs: regset) (m: mem) :=
  if is_pair_addressing_mode_correct a then
    let addr := (eval_addressing a rs) in
    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
    let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
      match Mem.storev chk1 m addr v1 with
      | None => Stuck
      | Some m' => match Mem.storev chk2 m' addr' v2 with
                   | None => Stuck
                   | Some m'' => Next (nextinstr rs) m''
                   end
      end
  else Stuck.

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 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 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
  | Pcmpimm X r1 n =>
      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)))) m
  | Pcmnimm W r1 n =>
      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))))) m
  | Pcmnimm X r1 n =>
      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))))) 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
  | Ptstimm X r1 n =>
      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero))) 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
  | Pcmp X r1 r2 s =>
      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s))) m
  | Pcmn W r1 r2 s =>
      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)))) m
  | Pcmn X r1 r2 s =>
      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)))) 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
  | Pcmnext r1 r2 x =>
      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)))) 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
  | 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
  (** 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 eval_testcond 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 => 
      if is_immediate_float32 f then
        Next (nextinstr (rs#rd <- (Vsingle f))) m
      else
        Next (nextinstr ((rs#rd <- (Vsingle f))#X16 <- Vundef)) m
  | Pfmovimmd rd f =>
      if is_immediate_float64 f then
        Next (nextinstr (rs#rd <- (Vfloat f))) m
      else
        Next (nextinstr ((rs#rd <- (Vfloat f))#X16 <- Vundef)) 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) m
          end
      | _ => Stuck
      end
  | Pbuiltin ef args res => Stuck    (**r treated specially below *)
  (** loads and stores pairs int/int64 *)
  | Pldpw rd1 rd2 chk1 chk2 a =>
      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
  | Pldpx rd1 rd2 chk1 chk2 a =>
      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
  | Pstpw rs1 rs2 chk1 chk2 a =>
      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
  | Pstpx rs1 rs2 chk1 chk2 a =>
      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
  (** loads and stores pairs floating-point *)
  | Pldps rd1 rd2 chk1 chk2 a =>
      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
  | Pldpd rd1 rd2 chk1 chk2 a =>
      exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
  | Pstps rs1 rs2 chk1 chk2 a =>
      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
  | Pstpd rs1 rs2 chk1 chk2 a =>
      exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
  | Pnop => Next (nextinstr rs) m
  (** The following instructions and directives are not generated directly
      by Asmgen, so we do not model them. *)
  | Pcls _ _ _
  | Pclz _ _ _
  | Prev _ _ _
  | Prev16 _ _ _
  | Prbit _ _ _
  | Pfsqrt _ _ _
  | Pfmadd _ _ _ _ _
  | Pfmsub _ _ _ _ _
  | Pfnmadd _ _ _ _ _
  | Pfnmsub _ _ _ _ _
  | Pfmax _ _ _ _
  | Pfmin _ _ _ _
  | Pcfi_adjust _ 
  | Pcfi_rel_offset _ =>
      Stuck
  end.

Inductive step: state -> trace -> state -> Prop :=
  | exec_step_internal:
      forall b ofs (f:function) i rs m rs' m',
      rs PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some i ->
      exec_instr f i rs m = Next rs' m' ->
      step (State rs m) E0 (State rs' m')
  | exec_step_builtin:
      forall b ofs f ef args res rs m vargs t vres rs' m',
      rs PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
      eval_builtin_args ge rs rs#SP m args vargs ->
      external_call ef ge vargs m t vres m' ->
      rs' = nextinstr
              (set_res res vres
                (undef_regs (DR X16 :: DR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
      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 (p: program) :=
  Semantics step (initial_state p) final_state (Genv.globalenv p).

(** Determinacy of the [Asm] semantics. *)

Remark extcall_arguments_determ:
  forall rs m sg args1 args2,
  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
Proof.
  intros until m.
  assert (A: forall l v1 v2,
             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
  { intros. inv H; inv H0; congruence. }
  assert (B: forall p v1 v2,
             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
  { intros. inv H; inv H0.
    eapply A; eauto.
    f_equal; eapply A; eauto. }
  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
  {
    induction 1; intros vl2 EA; inv EA.
    auto.
    f_equal; eauto. }
  intros. eapply C; eauto.
Qed.

Lemma semantics_determinate: forall p, determinate (semantics p).
Proof.
Ltac Equalities :=
  match goal with
  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
      rewrite H1 in H2; inv H2; Equalities
  | _ => idtac
  end.
  intros; constructor; simpl; intros.
- (* determ *)
  inv H; inv H0; Equalities.
  split. constructor. auto.
  discriminate.
  discriminate.
  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
  exploit external_call_determ. eexact H5. eexact H11. intros [A B].
  split. auto. intros. destruct B; auto. subst. auto.
  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
  split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
  red; intros. inv H; simpl.
  lia.
  eapply external_call_trace_length; eauto.
  eapply external_call_trace_length; eauto.
- (* initial states *)
  inv H; inv H0. f_equal. congruence.
- (* final no step *)
  inv H. red; intros; red; intros. inv H; rewrite H0 in *; discriminate.
- (* final states *)
  inv H; inv H0. congruence.
Qed.

(** Classification functions for processor registers (used in Asmgenproof). *)

Definition data_preg (r: preg) : bool :=
  match r with
  | DR (IR X16) => false
  | DR (IR X30) => false
  | DR (IR _) => true
  | DR (FR _) => true
  | CR _ => false
  (* | SP => true; subsumed by IR (iregsp) *)
  | PC => false
  end.