Require Import Coqlib Zbits Maps.
Require Import AST Integers Floats.
Require Import Op Values Memory Events Globalenvs Smallstep.
Require Import Locations Conventions.
Require Stacklayout.
Require Import OptionMonad Asm.
Require Import Lia.
Require Export Asm.
Require Import Decidableplus.
Require Import Compopts.

Local Open Scope option_monad_scope.

Notation regset := Asm.regset.

Inductive cf_instruction: Type :=
  | Pb (lbl: label) (* branch to label *)
  | Pbc (c: testcond) (lbl: label) (* conditional branch to label *)
  | Pcbz (r: ireg) (lbl: label) (* branch if zero *)
  | Pcbnz (r: ireg) (lbl: label) (* branch if not zero *)
  | Pbsymb (id: qualident) (sg: signature) (* branch to symbol *)
  | Pblsymb (id: qualident) (sg: signature) (* branch and link to symbol *)
  | Pbreg (r: ireg) (sg: signature) (* computed branch *)
  | Pblreg (r: ireg) (sg: signature) (* computed branch and link *)
  | Pbtbl (r: ireg) (tbl: list label) (* N-way branch through a jump table *)
  .


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


Inductive ldi: Type :=
  | Pldr (* int32 load *)
  | Pldr_a (* any32 load to int register *)
  | Pldr_u (* int32 unaligned load *)
  | Pldrb (* unsigned int8 load *)
  | Pldrh (* unsigned int16 load *)
  | Pldrsb (* signed int8 load *)
  | Pldrsh (* unsigned int16 load *)
  .

Inductive ldipi: Type :=
  | Pldr_pi (* int32 post-incremented load *)
  | Pldr_api (* any32 post-incremented load *)
  | Pldrb_pi (* unsigned int8 post-incremented load *)
  | Pldrh_pi (* unsigned int16 post-incremented load *)
  | Pldrsb_pi (* signed int8 post-incremented load *)
  | Pldrsh_pi (* signed int16 post-incremented load *)
  .

Inductive ldipd: Type :=
  | Pldr_pd (* int32 pre-decremented load *)
  | Pldr_apd (* any32 pre-decremented load *)
  | Pldrb_pd (* unsigned int8 pre-decremented load *)
  | Pldrh_pd (* unsigned int16 pre-decremented load *)
  | Pldrsb_pd (* signed int8 pre-decremented load *)
  | Pldrsh_pd (* signed int16 pre-decremented load *)
  .

Inductive ldf: Type :=
  | Pfldd (* float64 load *)
  | Pfldd_a (* any64 load to FP reg *)
  | Pflds (* float32 load *)
  .

Inductive ld_instruction: Type :=
  | Pcldi (ld: ldi) (rd ra: ireg) (o: shift_op)
  | Pcldf (ld: ldf) (rd: freg) (ra: ireg) (i: int)
  | Pcldipi (ld: ldipi) (rd ra: ireg) (o: shift_op) (* post-incremented load *)
  | Pcldipd (ld: ldipd) (rd ra: ireg) (o: shift_op) (* pre-decremented load *)
  | Pclddi (rd1 rd2 ra: ireg) (chk1 chk2: memory_chunk) (i1 i2: int) (* load double *)
  | Pclddi_pi (rd1 rd2 ra: ireg) (chk1 chk2: memory_chunk) (i: int) (* post-incremented load double *)
  | Pcldm (ra: ireg) (l: list (ireg * memory_chunk)) (* load multiple int *)
  | Pcvldm (ra: ireg) (l: list (freg * memory_chunk)) (* load multiple VFP-d *)
  .

Inductive sti: Type :=
  | Pstr (* int32 store *)
  | Pstr_a (* any32 store from int register *)
  | Pstr_u (* int32 unaligned store *)
  | Pstrb (* int8 store *)
  | Pstrh (* int16 store *)
  .

Inductive stipi: Type :=
  | Pstr_pi (* int32 post-incremented store *)
  | Pstr_api (* any32 post-incremented store *)
  | Pstrb_pi (* unsigned int8 post-incremented store *)
  | Pstrh_pi (* unsigned int16 post-incremented store *)
  .

Inductive stipd: Type :=
  | Pstr_pd (* int32 pre-decremented store *)
  | Pstr_apd (* any32 pre-decremented store *)
  | Pstrb_pd (* unsigned int8 pre-decremented store *)
  | Pstrh_pd (* unsigned int16 pre-decremented store *)
  .

Inductive stf: Type :=
  | Pfstd (* float64 store *)
  | Pfstd_a (* any64 store from FP reg *)
  | Pfsts (* float32 store *)
  .

Inductive st_instruction: Type :=
  | Pcsti (st: sti) (rs ra: ireg) (o: shift_op)
  | Pcstf (st: stf) (rs: freg) (ra: ireg) (i: int)
  | Pcstipi (st: stipi) (rs ra: ireg) (o: shift_op) (* post-incremented store *)
  | Pcstipd (st: stipd) (rs ra: ireg) (o: shift_op) (* pre-decremented store *)
  | Pcstdi (rs1 rs2 ra: ireg) (chk1 chk2: memory_chunk) (i1 i2: int)
  | Pcstdi_pi (rs1 rs2 ra: ireg) (chk1 chk2: memory_chunk) (i: int) (* post-incremented store double *)
  | Pcstm (ra: ireg) (l: list (ireg * memory_chunk)) (* store multiple int *)
  | Pcvstm (ra: ireg) (l: list (freg * memory_chunk)) (* store multiple VFP-d *)
  .

Inductive memcpy_instruction: Type :=
  | Pmemcpy8 (tr: ireg)
  | Pmemcpy16 (tr: ireg)
  | Pmemcpy32 (tr: ireg)
  | Pmemcpy64 (tr1 tr2: ireg)
  .

Inductive arith_p: Type :=
  | Pgetcanary
  | Pflis (f: float32) (* load float constant *)
  | Pmovw (i: int) (* move 16-bit immediate *)
  .

Inductive arith_pp: Type :=
  | Pubfx (i1 i2: int) (* unsigned bitfield extract *)
  | Psbfx (i1 i2: int) (* signed bitfield extract *)
  | Puxtb (* unsigned extend byte *)
  | Psxtb (* signed extend byte *)
  | Puxth (* unsigned extend halfword *)
  | Psxth (* signed extend halfword *)
  | Pclz (* count leading zeros *)
  | Prbit (* reverse bits *)
  | Prev (* reverse bytes (32-bit) *)
  | Pfcpyd (* float move *)
  | Pfabsd (* float absolute value *)
  | Pfnegd (* float opposite *)
  | Pfabss (* float absolute value *)
  | Pfnegs (* float opposite *)
  | Pfcvtsd (* round to single precision *)
  | Pfcvtds (* expand to double precision *)
  | Pfsqrtd (* double-precision floating-point square root. *)
  | Pfsqrts (* single-precision floating-point square root. *)
  | Pfsitod (* signed int to float *)
  | Pfuitod (* unsigned int to float *)
  | Pfsitos (* signed int to float *)
  | Pfuitos (* unsigned int to float *)
  | Psingle_of_bits
  | Pbits_of_single
  | Phibits_of_float
 .

Inductive arith_ro: Type :=
  | Pmov (* integer move *)
  | Pmvn (* integer complement *)
  .

Inductive arith_app: Type :=
  | Pmovt (i: int) (* set high 16 bits *)
  | Pbfc (i1 i2: int) (* bitfield clear *)
  .

Inductive arith_ppp: Type :=
  | Pasr (* arithmetic shift right *)
  | Plsl (* shift left *)
  | Plsr (* logical shift right *)
  | Pror (* rotate right by register *)
  | Pmul (* integer multiplication *)
  | Pfaddd (* float addition *)
  | Pfdivd (* float division *)
  | Pfmuld (* float multiplication *)
  | Pfsubd (* float subtraction *)
  | Pfadds (* float addition *)
  | Pfdivs (* float division *)
  | Pfmuls (* float multiplication *)
  | Pfsubs (* float subtraction *)
  | Pdouble_of_iibits
  | Pbfi (i1 i2: int) (* bitfield clear *)
  .

Inductive arith_rro: Type :=
  | Padd (* integer addition *)
  | Pand (* bitwise and *)
  | Pbic (* bitwise bit-clear *)
  | Peor (* bitwise exclusive or *)
  | Porr (* bitwise or *)
  | Prsb (* integer reverse subtraction *)
  | Psub (* integer subtraction *)
  .

Inductive arith_afff: Type :=
  | Pfmlad (* float multiplication-add *)
  | Pfmlsd (* float multiplication-subtract *)
  | Pfmlas (* float multiplication-add *)
  | Pfmlss (* float multiplication-subtract *)
  .

Inductive arith_rrrr: Type :=
  | Pmla (* integer multiply-add *)
  | Pmls (* integer multiply-subtract *)
  .

Inductive arith_drrrr: Type :=
  | Psmull (* signed multiply long *)
  | Pumull (* unsigned multiply long *)
  .

Inductive arith_comparison_f: Type :=
  | Pfcmpzd (* float comparison with 0.0 *)
  | Pfcmpzs (* float comparison with 0.0 *)
  .

Inductive arith_comparison_ff: Type :=
  | Pfcmpd (* float comparison *)
  | Pfcmps (* float comparison *)
  .

Inductive arith_comparison_ro: Type :=
  | Pcmp (* integer comparison *)
  | Pcmn (* integer comparison with opposite *)
  | Ptst (* bitwise and, set flags only *)
  .

Inductive ar_instruction: Type :=
  | PArithP (i: arith_p) (rd: dreg)
  | PArithPP (i: arith_pp) (rd rs: dreg)
  | PArithRO (i: arith_ro) (rd : ireg) (o: shift_op)
  | PArithAPP (i: arith_app) (rd: dreg) (rs: dreg)
  | PArithPPP (i: arith_ppp) (rd r1 r2: dreg)
  | PArithRRO (i: arith_rro) (rd rs: ireg) (o: shift_op)
  | PArithAFFF (i: arith_afff) (rd r1 r2: freg)
  | PArithRRRR (i: arith_rrrr) (rd r1 r2 r3: ireg)
  | PArithDRRRR (i: arith_drrrr) (rd1 rd2 r1 r2: ireg)
  | PArithComparisonF (i: arith_comparison_f) (r1: freg)
  | PArithComparisonFF (i: arith_comparison_ff) (r1 r2: freg)
  | PArithComparisonRO (i: arith_comparison_ro) (r1: ireg) (o: shift_op)
  | Pflid (rd: freg) (f: float) (* load float constant *)
  | Pftosizd (rd: ireg) (rs: freg) (* float to signed int *)
  | Pftouizd (rd: ireg) (rs: freg) (* float to unsigned int *)
  | Pftosizs (rd: ireg) (rs: freg) (* float to signed int *)
  | Pftouizs (rd: ireg) (rs: freg) (* float to unsigned int *)
  | Pmovite (c: testcond) (rd: ireg) (o1 o2: shift_op) (* integer conditional move *)
  | Pfmovite (c: testcond) (rd r1 r2: freg) (* FP conditional move *)
  | Psubs (rd r1: ireg) (so: shift_op) (* integer subtraction with flag update *)
  | Padds (rd r1: ireg) (so: shift_op) (* integer addition with flag update *)
  | Psbcs (rd r1: ireg) (so: shift_op) (* subtract-with-carry, set flags *)
  .

Inductive basic: Type :=
  | PArith (i: ar_instruction)
  | PLoad (ld: ld_instruction)
  | PStore (st: st_instruction)
  | PMemcpy (cp: memcpy_instruction) (ras rad: ireg) (mas mad: mcpy_addr)
  | Pallocframe (sz: Z) (linkofs: ptrofs) (* allocate new stack frame *)
  | Pfreeframe (sz: Z) (linkofs: ptrofs) (* deallocate stack frame and restore previous frame *)
  | Ploadsymbol (rd: ireg) (id: qualident) (p: ptrofs) (* load the address of a symbol *)
  | Pnop (real: bool) (* nop instruction *)
  | Pcfi_rel_offset (ofs: int) (* .cfi_rel_offset debug directive *)
  | Psdiv (rd r1 r2: ireg) (* signed division *)
  | Pudiv (rd r1 r2: ireg) (* unsigned division *)
  | Pmemcpyf64 (ras rad: ireg) (tr: freg) (ofs1 ofs2: int) (* 8-byte FPU memcpy operation *)
  .

Coercion PCtlFlow: cf_instruction >-> control.
Coercion Pcldi: ldi >-> Funclass.
Coercion Pcldf: ldf >-> Funclass.
Coercion Pcsti: sti >-> Funclass.
Coercion Pcstf: stf >-> Funclass.
Coercion PLoad: ld_instruction >-> basic.
Coercion PStore: st_instruction >-> basic.
Coercion PArithP: arith_p >-> Funclass.
Coercion PArithPP: arith_pp >-> Funclass.
Coercion PArithRO: arith_ro >-> Funclass.
Coercion PArithAPP: arith_app >-> Funclass.
Coercion PArithPPP: arith_ppp >-> Funclass.
Coercion PArithRRO: arith_rro >-> Funclass.
Coercion PArithAFFF: arith_afff >-> Funclass.
Coercion PArithRRRR: arith_rrrr >-> Funclass.
Coercion PArithDRRRR: arith_drrrr >-> Funclass.
Coercion PArithComparisonF: arith_comparison_f >-> Funclass.
Coercion PArithComparisonFF: arith_comparison_ff >-> Funclass.
Coercion PArithComparisonRO: arith_comparison_ro >-> Funclass.
Coercion PArith: ar_instruction >-> basic.

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.


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

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

Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.

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.

Lemma size_positive (b:bblock): size b > 0.

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

Definition genv := Genv.t fundef unit.

Operational semantics

Section RELSEM.

Variable ge: genv.

Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }.

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.

Lemma is_label_correct_false lbl bb:
  ~(List.In lbl (header bb)) <-> is_label lbl bb = false.

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) :=
  match label_pos lbl 0 (fn_blocks 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.


Definition eval_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
  match ores with
  | None => Stuck
  | Some res => if res then goto_label f lbl rs m else Next rs m
  end.

Definition eval_neg_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
  match ores with
  | None => Stuck
  | Some res => if res then Next rs m else goto_label f lbl rs m
  end.

Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) :=
  match cfi with
  | Pb lbl =>
      goto_label f lbl rs m
  | Pbc c lbl =>
      eval_branch f lbl rs m (eval_testcond c rs)
  | Pcbz r lbl =>
      eval_branch f lbl rs m (eval_testzero rs#r)
  | Pcbnz r lbl =>
      eval_neg_branch f lbl rs m (eval_testzero rs#r)
  | Pbsymb id sg =>
      Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pblsymb id sg =>
      Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
  | Pbreg r sg =>
      Next (rs#PC <- (rs#r)) m
  | Pblreg r sg =>
      Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m
  | Pbtbl r tbl =>
      match rs#r with
      | Vint n =>
          match list_nth_z tbl (Int.unsigned n) with
          | None => Stuck
          | Some lbl => goto_label f lbl (rs#RA <- Vundef) m
          end
      | _ => Stuck
      end
  end.

Definition exec_load_aux (chunk: memory_chunk) (addr: val) (rd: preg)
                         (rs: regset) (m: mem) :=
  match Mem.loadv chunk m addr with
  | Some v => Next (rs#rd <- v) m
  | None => Stuck
  end.

Definition exec_load_pi_aux (chunk: memory_chunk) (addr: val) (rd ra: preg)
                            (rs: regset) (m: mem) :=
  match Mem.loadv chunk m rs#ra with
  | Some v => Next (undef_flags (rs#ra <- addr #rd <- v)) m
  | None => Stuck
  end.

Definition exec_load_pd_aux (chunk: memory_chunk) (addr: val) (rd ra: preg)
                            (rs: regset) (m: mem) :=
  match Mem.loadv chunk m addr with
  | Some v => Next (undef_flags (rs#ra <- addr #rd <- v)) m
  | None => Stuck
  end.

Definition exec_load_double_aux (chk1 chk2: memory_chunk) (addr1 addr2: val) (rd1 rd2: preg) (rs: regset) (m: mem) :=
  match Mem.loadv chk1 m addr1, Mem.loadv chk2 m addr2 with
  | Some v1, Some v2 => Next (rs#rd1 <- v1 #rd2 <- v2) m
  | _, _ => Stuck
  end.

Definition exec_load_pi_double_aux (chk1 chk2: memory_chunk) (addr_new: val)
                                   (rd1 rd2 ra: preg) (rs: regset) (m: mem) :=
  let addr := rs#ra in
  let addr' := Val.add addr (Vint (Int.repr 4)) in
  match Mem.loadv chk1 m addr, Mem.loadv chk2 m addr' with
  | Some v1, Some v2 =>
      Next (undef_flags (rs#ra <- addr_new #rd1 <- v1 #rd2 <- v2)) m
  | _, _ => Stuck
  end.

Definition exec_store_aux (chunk: memory_chunk) (addr: val) (rf: preg)
                          (rs: regset) (m: mem) :=
  match Mem.storev chunk m addr rs#rf with
  | Some m' => Next rs m'
  | None => Stuck
  end.

Definition exec_store_pi_aux (chunk: memory_chunk) (addr: val) (rf ra: preg)
                             (rs: regset) (m: mem) :=
  match Mem.storev chunk m rs#ra rs#rf with
  | Some m' => Next (undef_flags (rs#ra <- addr)) m'
  | None => Stuck
  end.

Definition exec_store_pd_aux (chunk: memory_chunk) (addr: val) (rf ra: preg)
                             (rs: regset) (m: mem) :=
  match Mem.storev chunk m addr rs#rf with
  | Some m' => Next (undef_flags (rs#ra <- addr)) m'
  | None => Stuck
  end.

Definition exec_store_double_aux (chk1 chk2: memory_chunk) (addr1 addr2: val) (rf1 rf2: preg) (rs: regset) (m: mem) :=
  match Mem.storev chk1 m addr1 rs#rf1 with
  | Some m' =>
      match Mem.storev chk2 m' addr2 rs#rf2 with
      | Some m'' => Next rs m''
      | None => Stuck
      end
  | None => Stuck
  end.

Definition exec_store_pi_double_aux (chk1 chk2: memory_chunk) (addr_new: val)
                                    (rf1 rf2 ra: preg) (rs: regset) (m: mem) :=
  let addr := rs#ra in
  let addr' := Val.add addr (Vint (Int.repr 4)) in
  match Mem.storev chk1 m addr rs#rf1 with
  | Some m' =>
      match Mem.storev chk2 m' addr' rs#rf2 with
      | Some m'' => Next (undef_flags (rs#ra <- addr_new)) m''
      | None => Stuck
      end
  | None => Stuck
  end.

Definition chunk_ldi (ld: ldi) :=
  match ld with
  | Pldr => Mint32
  | Pldr_a => Many32
  | Pldr_u => Mint32al1
  | Pldrb => Mint8unsigned
  | Pldrh => Mint16unsigned
  | Pldrsb => Mint8signed
  | Pldrsh => Mint16signed
  end.

Definition chunk_ldipi (ld: ldipi) :=
  match ld with
  | Pldr_pi => Mint32
  | Pldr_api => Many32
  | Pldrb_pi => Mint8unsigned
  | Pldrh_pi => Mint16unsigned
  | Pldrsb_pi => Mint8signed
  | Pldrsh_pi => Mint16signed
  end.

Definition chunk_ldipd (ld: ldipd) :=
  match ld with
  | Pldr_pd => Mint32
  | Pldr_apd => Many32
  | Pldrb_pd => Mint8unsigned
  | Pldrh_pd => Mint16unsigned
  | Pldrsb_pd => Mint8signed
  | Pldrsh_pd => Mint16signed
  end.

Definition chunk_ldf (ld: ldf) :=
  match ld with
  | Pfldd => Mfloat64
  | Pfldd_a => Many64
  | Pflds => Mfloat32
  end.

Definition chunk_sti (st: sti) :=
  match st with
  | Pstr => Mint32
  | Pstr_a => Many32
  | Pstr_u => Mint32al1
  | Pstrb => Mint8unsigned
  | Pstrh => Mint16unsigned
  end.

Definition chunk_stipi (st: stipi) :=
  match st with
  | Pstr_pi => Mint32
  | Pstr_api => Many32
  | Pstrb_pi => Mint8unsigned
  | Pstrh_pi => Mint16unsigned
  end.

Definition chunk_stipd (st: stipd) :=
  match st with
  | Pstr_pd => Mint32
  | Pstr_apd => Many32
  | Pstrb_pd => Mint8unsigned
  | Pstrh_pd => Mint16unsigned
  end.

Definition chunk_stf (st: stf) :=
  match st with
  | Pfstd => Mfloat64
  | Pfstd_a => Many64
  | Pfsts => Mfloat32
  end.

Definition exec_load (ld: ld_instruction) (rs: regset) (m: mem) :=
  match ld with
  | Pcldi ldi rd ra o =>
      exec_load_aux (chunk_ldi ldi) (Val.add rs#ra (eval_shift_op o rs)) rd rs m
  | Pcldipi ldi rd ra o =>
      exec_load_pi_aux (chunk_ldipi ldi) (Val.add rs#ra (eval_shift_op o rs)) rd ra rs m
  | Pcldipd ldi rd ra o =>
      exec_load_pd_aux (chunk_ldipd ldi) (Val.sub rs#ra (eval_shift_op o rs)) rd ra rs m
  | Pclddi rd1 rd2 ra chk1 chk2 i1 i2 =>
      exec_load_double_aux chk1 chk2 (Val.add rs#ra (Vint i1)) (Val.add rs#ra (Vint i2)) rd1 rd2 rs m
  | Pclddi_pi rd1 rd2 ra chk1 chk2 i =>
      exec_load_pi_double_aux chk1 chk2 (Val.add rs#ra (Vint i)) rd1 rd2 ra rs m
  | Pcldf ldf rd ra i =>
      exec_load_aux (chunk_ldf ldf) (Val.add rs#ra (Vint i)) rd rs m
  | Pcldm ra l =>
      if ldm_iregs_wf ra l then
        match exec_load_multi_i rs#ra 0 l rs m with
        | Some rs' => Next rs' m
        | None => Stuck
        end
      else Stuck
  | Pcvldm ra l =>
      if vldm_fregs_wf l then
        match exec_load_multi_f rs#ra 0 l rs m with
        | Some rs' => Next rs' m
        | None => Stuck
        end
      else Stuck
  end.

Definition exec_store (st: st_instruction) (rs: regset) (m: mem) :=
  match st with
  | Pcsti sti rf ra o =>
      exec_store_aux (chunk_sti sti) (Val.add rs#ra (eval_shift_op o rs)) rf rs m
  | Pcstipi sti rd ra o =>
      exec_store_pi_aux (chunk_stipi sti) (Val.add rs#ra (eval_shift_op o rs)) rd ra rs m
  | Pcstipd sti rd ra o =>
      exec_store_pd_aux (chunk_stipd sti) (Val.sub rs#ra (eval_shift_op o rs)) rd ra rs m
  | Pcstdi rf1 rf2 ra chk1 chk2 i1 i2 =>
      exec_store_double_aux chk1 chk2 (Val.add rs#ra (Vint i1)) (Val.add rs#ra (Vint i2)) rf1 rf2 rs m
  | Pcstdi_pi rf1 rf2 ra chk1 chk2 i =>
      exec_store_pi_double_aux chk1 chk2 (Val.add rs#ra (Vint i)) rf1 rf2 ra rs m
  | Pcstf stf rf ra i =>
      exec_store_aux (chunk_stf stf) (Val.add rs#ra (Vint i)) rf rs m
  | Pcstm ra l =>
      if stm_iregs_wf ra l then
        match exec_store_multi_i rs#ra 0 l rs m with
        | Some m' => Next rs m'
        | None => Stuck
        end
      else Stuck
  | Pcvstm ra l =>
      if vstm_fregs_wf l then
        match exec_store_multi_f rs#ra 0 l rs m with
        | Some m' => Next rs m'
        | None => Stuck
        end
      else Stuck
  end.

Definition exec_memcpy_aux (tr: list dreg) (ras rad: ireg) (mas mad: mcpy_addr)
                           (sz: Z) (rs: regset) (m: mem) :=
  let rss := mcpy_rs_use_src tr ras mas rs in
  let rsd := mcpy_rs tr ras rad mas mad rs mcpy_rs_use_addr in
  let rsr := mcpy_rs tr ras rad mas mad rs mcpy_rs_ret_addr in
  match rss#ras, rsd#rad with
  | Vptr bsrc osrc, Vptr bdst odst =>
      match Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz with
      | Some bytes =>
          match Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes with
          | Some m' => Next rsr m'
          | None => Stuck
          end
      | None => Stuck
      end
  | _, _ => Stuck
  end.

Definition exec_memcpy (cp: memcpy_instruction) (ras rad: ireg) (mas mad: mcpy_addr)
                       (rs: regset) (m: mem) :=
  match cp with
  | Pmemcpy8 tr =>
      if PregEq.eq rad tr || negb (mcpy_valid_reg ras rad mas mad)
      then Stuck
      else exec_memcpy_aux (IR tr :: nil) ras rad mas mad 1 rs m
  | Pmemcpy16 tr =>
      if PregEq.eq rad tr || negb (mcpy_valid_reg ras rad mas mad)
      then Stuck
      else exec_memcpy_aux (IR tr :: nil) ras rad mas mad 2 rs m
  | Pmemcpy32 tr =>
      if PregEq.eq rad tr || negb (mcpy_valid_reg ras rad mas mad)
      then Stuck
      else exec_memcpy_aux (IR tr :: nil) ras rad mas mad 4 rs m
  | Pmemcpy64 tr1 tr2 =>
      if PregEq.eq rad tr1 || PregEq.eq rad tr2 ||
         negb (mcpy_valid_reg ras rad mas mad) ||
         negb (thumb tt || ls_double_valid_regs tr1 tr2)
      then Stuck
      else exec_memcpy_aux (IR tr1 :: IR tr2 :: nil) ras rad mas mad 8 rs m
  end.

Definition arith_undef_flags ai :=
  match ai with
  | PArithRO Pmov _ _ | PArithRO Pmvn _ _
  | PArithPPP Pasr _ _ _ | PArithPPP Plsl _ _ _
  | PArithPPP Plsr _ _ _ | PArithPPP Pror _ _ _
  | PArithRRO Padd _ _ _
  | PArithRRO Pand _ _ _ | PArithRRO Pbic _ _ _
  | PArithRRO Peor _ _ _ | PArithRRO Porr _ _ _
  | PArithRRO Prsb _ _ _ | PArithRRO Psub _ _ _
      => true
  | _ => false
  end.

Definition arith_uf_fn ai :=
  if arith_undef_flags ai then undef_flags
  else (fun x => x).

Definition arith_eval_p i :=
  match i with
  | Pgetcanary => (canary_val tt)
  | Pflis f => (Vsingle f)
  | Pmovw i => Vint i
  end.

Definition arith_eval_pp i v :=
  match i with
  | Pubfx lsb sz => Val.zero_ext (Int.unsigned sz) (Val.shru v (Vint (lsb)))
  | Psbfx lsb sz => Val.sign_ext (Int.unsigned sz) (Val.shru v (Vint (lsb)))
  | Puxtb => Val.zero_ext 8 v
  | Psxtb => Val.sign_ext 8 v
  | Puxth => Val.zero_ext 16 v
  | Psxth => Val.sign_ext 16 v
  | Pfcpyd => v
  | Pfabsd => Val.absf v
  | Pfnegd => Val.negf v
  | Pfabss => Val.absfs v
  | Pfnegs => Val.negfs v
  | Pfcvtsd => Val.singleoffloat v
  | Pfcvtds => Val.floatofsingle v
  | Pfsitod => Val.maketotal (Val.floatofint v)
  | Pfuitod => Val.maketotal (Val.floatofintu v)
  | Pfsitos => Val.maketotal (Val.singleofint v)
  | Pfuitos => Val.maketotal (Val.singleofintu v)
  | Pclz => match v with Vint n => Vint (Int.clz n) | _ => Vundef end
  | Prbit => match v with Vint n => Vint (Int.reverse_bits n) | _ => Vundef end
  | Prev => ExtValues.val_bswap32 v
  | Psingle_of_bits => Val.single_of_bits v
  | Pbits_of_single => Val.bits_of_single v
  | Phibits_of_float => Val.hiword (Val.bits_of_float v)
  | Pfsqrtd => Val.sqrtf v
  | Pfsqrts => Val.sqrtfs v
  end.

Definition arith_eval_ro i v :=
  match i with
  | Pmov => v
  | Pmvn => Val.notint v
  end.

Definition arith_eval_app i v :=
  match i with
  | Pmovt i => Val.or (Val.and v (Vint (Int.repr 65535)))
      (Vint (Int.shl i (Int.repr 16)))
  | Pbfc lsb sz => ExtValues.clearf lsb sz v
  end.

Definition arith_eval_ppp i v1 v2 :=
  match i with
  | Pasr => Val.shr v1 v2
  | Plsl => Val.shl v1 v2
  | Plsr => Val.shru v1 v2
  | Pror => Val.ror v1 v2
  | Pmul => Val.mul v1 v2
  | Pfaddd => Val.addf v1 v2
  | Pfdivd => Val.divf v1 v2
  | Pfmuld => Val.mulf v1 v2
  | Pfsubd => Val.subf v1 v2
  | Pfadds => Val.addfs v1 v2
  | Pfdivs => Val.divfs v1 v2
  | Pfmuls => Val.mulfs v1 v2
  | Pfsubs => Val.subfs v1 v2
  | Pdouble_of_iibits => Val.floatofwords v2 v1
  | Pbfi lsb sz => ExtValues.insf lsb sz v1 v2
  end.

Definition arith_eval_rro i v1 v2 :=
  match i with
  | Padd => Val.add v1 v2
  | Pand => Val.and v1 v2
  | Pbic => Val.and v1 (Val.notint v2)
  | Peor => Val.xor v1 v2
  | Porr => Val.or v1 v2
  | Prsb => Val.sub v2 v1
  | Psub => Val.sub v1 v2
  end.

Definition arith_eval_afff i vd v1 v2 :=
  match i with
  | Pfmlad => Val.addf vd (Val.mulf v1 v2)
  | Pfmlsd => Val.subf vd (Val.mulf v1 v2)
  | Pfmlas => Val.addfs vd (Val.mulfs v1 v2)
  | Pfmlss => Val.subfs vd (Val.mulfs v1 v2)
  end.

Definition arith_eval_rrrr i v1 v2 v3 :=
  match i with
  | Pmla => Val.add (Val.mul v1 v2) v3
  | Pmls => Val.sub v3 (Val.mul v1 v2)
  end.

Definition arith_eval_drrrr1 i v1 v2 :=
  match i with
  | Psmull => Val.mul v1 v2
  | Pumull => Val.mul v1 v2
  end.

Definition arith_eval_drrrr2 i v1 v2 :=
  match i with
  | Psmull => Val.mulhs v1 v2
  | Pumull => Val.mulhu v1 v2
  end.

Definition arith_prepare_comparison_f i (v: val) :=
  match i with
  | Pfcmpzd => (v, Vfloat Float.zero)
  | Pfcmpzs => (v, Vsingle Float32.zero)
  end.

Definition arith_prepare_comparison_ff i (v1 v2: val) :=
  match i with
  | Pfcmpd | Pfcmps => (v1, v2)
  end.

Definition arith_prepare_comparison_ro i (v vo: val) :=
  match i with
  | Pcmp => (v, vo)
  | Pcmn => (v, Val.neg vo)
  | Ptst => (v, vo)
  end.

Definition arith_comparison_f_compare i :=
  match i with
  | Pfcmpzd => compare_float
  | Pfcmpzs => compare_float32
  end.

Definition arith_comparison_ff_compare i :=
  match i with
  | Pfcmpd => compare_float
  | Pfcmps => compare_float32
  end.

Definition arith_comparison_ro_compare i (rs: regset) (v1 v2: val) (m: mem) : regset :=
  match i with
  | Pcmp | Pcmn => compare_int rs v1 v2 m
  | Ptst => compare_int_test rs v1 v2
  end.

Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem): regset :=
  match ai with
  | PArithP i d => rs#d <- (arith_eval_p i)
  | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s)
  | PArithRO i d o => (arith_uf_fn ai) rs#d <- (arith_eval_ro i (eval_shift_op o rs))
  | PArithAPP i d s => rs#d <- (arith_eval_app i rs#s)
  | PArithPPP i d s1 s2 => (arith_uf_fn ai) rs#d <- (arith_eval_ppp i rs#s1 rs#s2)
  | PArithRRO i d s o => (arith_uf_fn ai) rs#d <- (arith_eval_rro i rs#s (eval_shift_op o rs))
  | PArithAFFF i d s1 s2 => rs#d <- (arith_eval_afff i rs#d rs#s1 rs#s2)
  | PArithRRRR i d s1 s2 s3 => rs#d <- (arith_eval_rrrr i rs#s1 rs#s2 rs#s3)
  | PArithDRRRR i d1 d2 s1 s2 => rs#d1 <- (arith_eval_drrrr1 i rs#s1 rs#s2)
                                   #d2 <- (arith_eval_drrrr2 i rs#s1 rs#s2)
  | PArithComparisonF i s =>
      let (v1, v2) := arith_prepare_comparison_f i rs#s in
      arith_comparison_f_compare i rs v1 v2
  | PArithComparisonFF i s1 s2 =>
      let (v1, v2) := arith_prepare_comparison_ff i rs#s1 rs#s2 in
      arith_comparison_ff_compare i rs v1 v2
  | PArithComparisonRO i s o =>
      let (v1, v2) := arith_prepare_comparison_ro i rs#s (eval_shift_op o rs) in
      arith_comparison_ro_compare i rs v1 v2 m
  | Pflid d f => rs#IR14 <- Vundef #d <- (Vfloat f)
  | Pftosizd d s => rs #FR6 <- Vundef #d <- (Val.maketotal (Val.intoffloat rs#s))
  | Pftouizd d s => rs #FR6 <- Vundef #d <- (Val.maketotal (Val.intuoffloat rs#s))
  | Pftosizs d s => rs #FR6 <- Vundef #d <- (Val.maketotal (Val.intofsingle rs#s))
  | Pftouizs d s => rs #FR6 <- Vundef #d <- (Val.maketotal (Val.intuofsingle rs#s))
  | Pmovite c d ifso ifnot =>
      rs #d <- match eval_testcond c rs with
               | Some true => eval_shift_op ifso rs
               | Some false => eval_shift_op ifnot rs
               | None => Vundef
               end
  | Pfmovite c d ifso ifnot =>
      rs #d <- match eval_testcond c rs with
        | Some true => rs#ifso
        | Some false => rs#ifnot
        | None => Vundef
        end
  | Psubs r1 r2 so =>
      let v2 := eval_shift_op so rs in
      (compare_int rs rs#r2 v2 m) #r1 <- (Val.sub rs#r2 v2)
  | Padds r1 r2 so =>
      let v2 := eval_shift_op so rs in
      (compare_int_add rs rs#r2 v2 m) #r1 <- (Val.add rs#r2 v2)
  | Psbcs r1 r2 so =>
      let v2 := eval_shift_op so rs in
      let cin := rs#CC in
      let bin := Val.sub (Vint Int.one) cin in
      (compare_int_sbc rs rs#r2 v2 cin m) #r1 <- (Val.sub (Val.sub rs#r2 v2) bin)
  end.

Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
  match b with
  | PArith ai => Next (exec_arith_instr ai rs m) m
  | PLoad ldi => exec_load ldi rs m
  | PStore sti => exec_store sti rs m
  | PMemcpy cp ras rad mas mad => exec_memcpy cp ras rad mas mad rs m
  | Pallocframe sz pos =>
      let (m1, stk) := Mem.alloc m 0 sz 8 in
      let sp := (Vptr stk Ptrofs.zero) in
      match Mem.storev Mint32 m1 (Val.offset_ptr sp pos) rs#IR13 with
      | None => Stuck
      | Some m2 => Next (rs #IR12 <- (rs#IR13) #IR13 <- sp) m2
      end
  | Pfreeframe sz pos =>
      match Mem.loadv Mint32 m (Val.offset_ptr rs#IR13 pos) with
      | None => Stuck
      | Some v =>
          match rs#IR13 with
          | Vptr stk ofs =>
              match Mem.free m stk 0 sz with
              | None => Stuck
              | Some m' => Next (rs#IR13 <- v) m'
              end
          | _ => Stuck
          end
      end
  | Ploadsymbol rd id pos =>
      Next (rs#rd <- (Genv.symbol_address ge id pos)) m
  | Psdiv rd r1 r2 =>
      match Val.divs rs#r1 rs#r2 with
      | Some v => if Archi.hardware_idiv tt then
                    Next (rs#rd <- v) m
                  else
                    let rs := undef_regs
                       (DR IR0 :: DR IR1 :: DR IR2 :: DR IR3 :: DR IR12
                        :: DR FR0 :: DR FR1 :: DR FR2 :: DR FR3
                        :: DR FR4 :: DR FR5 :: DR FR6 :: DR FR7 :: nil) rs in
                    Next (rs#rd <- v) m
      | None => Stuck
      end
  | Pudiv rd r1 r2 =>
      match Val.divu rs#r1 rs#r2 with
      | Some v => if Archi.hardware_idiv tt then
                    Next (rs#rd <- v) m
                  else
                    let rs := undef_regs
                       (DR IR0 :: DR IR1 :: DR IR2 :: DR IR3 :: DR IR12
                        :: DR FR0 :: DR FR1 :: DR FR2 :: DR FR3
                        :: DR FR4 :: DR FR5 :: DR FR6 :: DR FR7 :: nil) rs in
                    Next (rs#rd <- v) m
      | None => Stuck
      end
  | Pmemcpyf64 ras rad tr ofs1 ofs2 =>
      exec_memcpy_aux (FR tr :: nil) ras rad (Ofs ofs1) (Ofs ofs2) 8 rs m
  | Pnop _ | Pcfi_rel_offset _ => Next rs m
  end.


Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
  match body with
  | nil => Next rs m
  | bi :: body' =>
      match exec_basic bi rs m with
      | Next rs' m' => exec_body body' rs' m'
      | Stuck => Stuck
      end
  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.

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 IR14) :: 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 bb rs m :=
  match exec_body (body bb) rs m with
  | Next 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
    else if zeq pos 0 then Some b
    else find_bblock (pos - (size b)) il
  end.


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.



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

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

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