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


(* 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.
Require Import Lia.
Require Export Asm.

Local Open Scope option_monad_scope.

Notation regset := Asm.regset.

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

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

Inductive load_rd1_rd2_a: Type :=
  | Pldpw
  | Pldpx
  | Pldps
  | Pldpd
  .

Inductive ld_instruction: Type :=
  | PLd_rd_a (ld: load_rd_a) (rd: dreg) (a: addressing)
  | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: dreg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two int64 *)
  .

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

Inductive store_rs1_rs2_a : Type :=
  | Pstpw
  | Pstpx
  | Pstps
  | Pstpd
  .

Inductive st_instruction : Type :=
  | PSt_rs_a (st: store_rs_a) (rs: dreg) (a: addressing)
  | Pstp (st: store_rs1_rs2_a) (rs1 rs2: dreg) (chk1 chk2: memory_chunk) (a: addressing)  (**r store two int64 *)
  .

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)
  | PLoad (ld: ld_instruction)
  | PStore (st: st_instruction)
  | 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 *)
  | Pnop                                                              (**r no operation *)
(* NOT USED IN THE SEMANTICS !
  | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
  | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
*)
.

Coercion PCtlFlow: cf_instruction >-> control.
Coercion PLoad: ld_instruction >-> basic.
Coercion PStore : st_instruction >-> basic.
Coercion PArithP: arith_p >-> Funclass.
Coercion PArithPP: arith_pp >-> Funclass.
Coercion PArithPPP: arith_ppp >-> Funclass.
Coercion PArithRR0: arith_rr0 >-> Funclass.
Coercion PArithRR0R: arith_rr0r >-> Funclass.
Coercion PArithARRRR0: arith_arrrr0 >-> Funclass.
Coercion PArithComparisonP: arith_comparison_p >-> Funclass.
Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass.
Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass.
Coercion PArith: ar_instruction >-> basic.


(* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml
Inductive instruction : Type :=
  | PBasic    (i: basic)
  | PControl  (i: control).

Coercion PBasic:    basic >-> instruction.
Coercion PControl:  control >-> instruction. *)

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

Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
Next Obligation.
  destruct bb; cbn. assumption.
Defined.

Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
Next Obligation.
  destruct bb; cbn. assumption.
Defined.

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

Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
Proof.
  intros. destruct z; auto.
  - contradict H. cbn. apply gt_irrefl.
  - apply Zgt_pos_0.
  - contradict H. cbn. apply gt_irrefl.
Qed.

Lemma size_positive (b:bblock): size b > 0.
Proof.
  unfold size. destruct b as [hd bdy ex cor]. cbn.
  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia);
  unfold non_empty_bblockb in cor; simpl in cor.
  inversion cor.
Qed.

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

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

(** Auxiliaries for memory accesses *)

Definition exec_load_rd_a (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_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
                     (a: addressing) (rd1 rd2: dreg) (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 ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m
            end
        end
  else Stuck.

Definition exec_store_rs_a (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'.

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 rs m''
                   end
      end
  else Stuck.

(** execution of loads
*)

Definition chunk_load (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 (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 (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.

Definition exec_load (ldi: ld_instruction) (rs: regset) (m: mem) :=
  match ldi with
  | PLd_rd_a ld rd a => exec_load_rd_a (chunk_load ld) (interp_load ld) a rd rs m
  | Pldp ld rd1 rd2 chk1 chk2 a => exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
  end.

Definition exec_store (sti: st_instruction) (rs: regset) (m: mem) :=
  match sti with
  | PSt_rs_a st rsr a => exec_store_rs_a (chunk_store st) a rs#rsr rs m
  | Pstp st rs1 rs2 chk1 chk2 a => exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
  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) 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 destroy_X16 (i : arith_p) : bool :=
  match i with
  | Pfmovimms d => negb (is_immediate_float32 d)
  | Pfmovimmd d => negb (is_immediate_float64 d)
  | _ => false
  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 =>
     let rs' := rs#d <- (arith_eval_p i) in
     if destroy_X16 i then rs'#X16 <- Vundef else rs'
  | 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 ldi => exec_load ldi rs m
  | PStore sti => exec_store sti 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
  | Pnop => Next rs m
  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).

Definition estep (f: function) oc size_b (rs: regset) (m: mem) :=
  match oc with
  | Some (PCtlFlow cfi) => exec_cfi f cfi (incrPC size_b rs) m
  | Some (Pbuiltin ef args res) => Next (incrPC size_b rs) m
  | None => Next (incrPC size_b rs) m
  end.

(**  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 (DR (IR X16) :: DR (IR X30) :: map preg_of (destroyed_by_builtin ef)) rs)) ->
      exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m'
      .

(*Definition bbstep f cfi size_b bdy rs m :=*)
  (*match exec_body bdy rs m with*)
  (*| Some (State rs' m') => estep f cfi size_b rs' m'*)
  (*| Stuck => Stuck*)
  (*end.*)

Definition bbstep f bb rs m :=
  match exec_body (body bb) rs m with
  | Some (State rs' m') => estep f (exit bb) (Ptrofs.repr (size bb)) rs' m'
  | Stuck => Stuck
  end.

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