Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import ExtValues.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Locations.
Require Stacklayout.
Require Import Conventions.
Require Import Errors.
Require Import Sorting.Permutation.
Require Import Chunks.
Require Import Lia.

Abstract syntax

General Purpose registers.

Inductive gpreg: Type :=
  | GPR0: gpreg | GPR1: gpreg | GPR2: gpreg | GPR3: gpreg | GPR4: gpreg
  | GPR5: gpreg | GPR6: gpreg | GPR7: gpreg | GPR8: gpreg | GPR9: gpreg
  | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg
  | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg
  | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg
  | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg
  | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg
  | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg
  | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg
  | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg
  | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg
  | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg
  | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg.

Definition ireg := gpreg.
Definition freg := gpreg.

Lemma gpreg_eq: forall (x y: gpreg), {x=y} + {x<>y}.

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

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

Inductive gpreg_q : Type :=
| R0R1 | R2R3 | R4R5 | R6R7 | R8R9
| R10R11 | R12R13 | R14R15 | R16R17 | R18R19
| R20R21 | R22R23 | R24R25 | R26R27 | R28R29
| R30R31 | R32R33 | R34R35 | R36R37 | R38R39
| R40R41 | R42R43 | R44R45 | R46R47 | R48R49
| R50R51 | R52R53 | R54R55 | R56R57 | R58R59
| R60R61 | R62R63.
                             
Lemma gpreg_q_eq : forall (x y : gpreg_q), {x=y} + {x<>y}.

Definition gpreg_q_expand (x : gpreg_q) : gpreg * gpreg :=
  match x with
  | R0R1 => (GPR0, GPR1)
  | R2R3 => (GPR2, GPR3)
  | R4R5 => (GPR4, GPR5)
  | R6R7 => (GPR6, GPR7)
  | R8R9 => (GPR8, GPR9)
  | R10R11 => (GPR10, GPR11)
  | R12R13 => (GPR12, GPR13)
  | R14R15 => (GPR14, GPR15)
  | R16R17 => (GPR16, GPR17)
  | R18R19 => (GPR18, GPR19)
  | R20R21 => (GPR20, GPR21)
  | R22R23 => (GPR22, GPR23)
  | R24R25 => (GPR24, GPR25)
  | R26R27 => (GPR26, GPR27)
  | R28R29 => (GPR28, GPR29)
  | R30R31 => (GPR30, GPR31)
  | R32R33 => (GPR32, GPR33)
  | R34R35 => (GPR34, GPR35)
  | R36R37 => (GPR36, GPR37)
  | R38R39 => (GPR38, GPR39)
  | R40R41 => (GPR40, GPR41)
  | R42R43 => (GPR42, GPR43)
  | R44R45 => (GPR44, GPR45)
  | R46R47 => (GPR46, GPR47)
  | R48R49 => (GPR48, GPR49)
  | R50R51 => (GPR50, GPR51)
  | R52R53 => (GPR52, GPR53)
  | R54R55 => (GPR54, GPR55)
  | R56R57 => (GPR56, GPR57)
  | R58R59 => (GPR58, GPR59)
  | R60R61 => (GPR60, GPR61)
  | R62R63 => (GPR62, GPR63)
  end.

Inductive gpreg_o : Type :=
| R0R1R2R3 | R4R5R6R7 | R8R9R10R11 | R12R13R14R15
| R16R17R18R19 | R20R21R22R23 | R24R25R26R27 | R28R29R30R31
| R32R33R34R35 | R36R37R38R39 | R40R41R42R43 | R44R45R46R47
| R48R49R50R51 | R52R53R54R55 | R56R57R58R59 | R60R61R62R63.

Definition gpreg_o_expand (x : gpreg_o) : gpreg * gpreg * gpreg * gpreg :=
  match x with
  | R0R1R2R3 => (GPR0, GPR1, GPR2, GPR3)
  | R4R5R6R7 => (GPR4, GPR5, GPR6, GPR7)
  | R8R9R10R11 => (GPR8, GPR9, GPR10, GPR11)
  | R12R13R14R15 => (GPR12, GPR13, GPR14, GPR15)
  | R16R17R18R19 => (GPR16, GPR17, GPR18, GPR19)
  | R20R21R22R23 => (GPR20, GPR21, GPR22, GPR23)
  | R24R25R26R27 => (GPR24, GPR25, GPR26, GPR27)
  | R28R29R30R31 => (GPR28, GPR29, GPR30, GPR31)
  | R32R33R34R35 => (GPR32, GPR33, GPR34, GPR35)
  | R36R37R38R39 => (GPR36, GPR37, GPR38, GPR39)
  | R40R41R42R43 => (GPR40, GPR41, GPR42, GPR43)
  | R44R45R46R47 => (GPR44, GPR45, GPR46, GPR47)
  | R48R49R50R51 => (GPR48, GPR49, GPR50, GPR51)
  | R52R53R54R55 => (GPR52, GPR53, GPR54, GPR55)
  | R56R57R58R59 => (GPR56, GPR57, GPR58, GPR59)
  | R60R61R62R63 => (GPR60, GPR61, GPR62, GPR63)
  end.

Lemma gpreg_o_eq : forall (x y : gpreg_o), {x=y} + {x<>y}.

Inductive preg: Type :=
  | IR: gpreg -> preg (* integer general purpose registers *)
  | RA: preg
  | PC: preg
  .

Coercion IR: gpreg >-> preg.

Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.

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

Definition preg_of (r: mreg) : preg :=
  match r with
  | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4
  | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9
  | R10 => GPR10 | R11 => GPR11
  | R15 => GPR15 | R17 => GPR17 | R18 => GPR18 | R19 => GPR19
  | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24
  | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29
  | R30 => GPR30 | R31 => GPR31 | R33 => GPR33 | R34 => GPR34
  | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39 => GPR39
  | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44 => GPR44
  | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49 => GPR49
  | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54 => GPR54
  | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59 => GPR59
  | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
  end.

Definition ireg_of (r: mreg) : res ireg :=
  match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.ireg_of") end.

Definition freg_of (r: mreg) : res freg :=
  match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.

Module Pregmap := EMap(PregEq).

Conventional names for stack pointer (SP), return address (RA), frame pointer (FP) and other temporaries used

Notation "'SP'" := GPR12 (only parsing) : asm.
Notation "'FP'" := GPR17 (only parsing) : asm.
Notation "'MFP'" := R17 (only parsing) : asm.
Notation "'GPRA'" := GPR16 (only parsing) : asm.
Notation "'RTMP'" := GPR32 (only parsing) : asm.

Names of tests in comparisons

Inductive btest: Type :=
  | BTdnez (* Double Not Equal to Zero *)
  | BTdeqz (* Double Equal to Zero *)
  | BTdltz (* Double Less Than Zero *)
  | BTdgez (* Double Greater Than or Equal to Zero *)
  | BTdlez (* Double Less Than or Equal to Zero *)
  | BTdgtz (* Double Greater Than Zero *)
  | BTwnez (* Word Not Equal to Zero *)
  | BTweqz (* Word Equal to Zero *)
  | BTwltz (* Word Less Than Zero *)
  | BTwgez (* Word Greater Than or Equal to Zero *)
  | BTwlez (* Word Less Than or Equal to Zero *)
  | BTwgtz (* Word Greater Than Zero *)
  .

Inductive itest: Type :=
  | ITne (* Not Equal *)
  | ITeq (* Equal *)
  | ITlt (* Less Than *)
  | ITge (* Greater Than or Equal *)
  | ITle (* Less Than or Equal *)
  | ITgt (* Greater Than *)
  | ITneu (* Unsigned Not Equal *)
  | ITequ (* Unsigned Equal *)
  | ITltu (* Less Than Unsigned *)
  | ITgeu (* Greater Than or Equal Unsigned *)
  | ITleu (* Less Than or Equal Unsigned *)
  | ITgtu (* Greater Than Unsigned *)
  .

Inductive ftest: Type :=
  | FTone (* Ordered and Not Equal *)
  | FTueq (* Unordered or Equal *)
  | FToeq (* Ordered and Equal *)
  | FTune (* Unordered or Not Equal *)
  | FTolt (* Ordered and Less Than *)
  | FTuge (* Unordered or Greater Than or Equal *)
  | FToge (* Ordered and Greater Than or Equal *)
  | FTult (* Unordered or Less Than *)
  .

Offsets for load and store instructions.

Definition offset : Type := ptrofs.

Labels for goto (in the current function)

Definition label := positive.

Instructions

Instructions to be expanded in control-flow

Inductive ex_instruction : Type :=
  | Pbuiltin: external_function -> list (builtin_arg preg)
              -> builtin_res preg -> ex_instruction (* built-in function (pseudo) *)
.

Control Flow instructions

Inductive cf_instruction : Type :=
  | Pret (* return *)
  | Pcall (l: label) (* function call *)
  | Picall (r: ireg) (* function call on register value *)
  | Pjumptable (r: ireg) (labels: list label) (* N-way branch through a jump table (pseudo) *)

  | Pgoto (l: label) (* goto *)
  | Pigoto (r: ireg) (* goto from register *)
  | Pj_l (l: label) (* jump to label *)

  | Pcb (bt: btest) (r: ireg) (l: label) (* branch based on btest *)
  | Pcbu (bt: btest) (r: ireg) (l: label) (* branch based on btest with unsigned semantics *)
.

Loads

Inductive load_name : Type :=
  | Plb (* load byte *)
  | Plbu (* load byte unsigned *)
  | Plh (* load half word *)
  | Plhu (* load half word unsigned *)
  | Plw (* load int32 *)
  | Plw_a (* load any32 *)
  | Pld (* load int64 *)
  | Pld_a (* load any64 *)
  | Pfls (* load float *)
  | Pfld (* load 64-bit float *)
.

Inductive ld_instruction : Type :=
  | PLoadRRO (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
  | PLoadRRR (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
  | PLoadRRRXS (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
  | PLoadQRRO (rd: gpreg_q) (ra: ireg) (ofs: offset)
  | PLoadORRO (rd: gpreg_o) (ra: ireg) (ofs: offset)
.

Stores

Inductive store_name : Type :=
  | Psb (* store byte *)
  | Psh (* store half byte *)
  | Psw (* store int32 *)
  | Psw_a (* store any32 *)
  | Psd (* store int64 *)
  | Psd_a (* store any64 *)
  | Pfss (* store float *)
  | Pfsd (* store 64-bit float *)
.

Inductive st_instruction : Type :=
  | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
  | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
  | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
  | PStoreQRRO (rs: gpreg_q) (ra: ireg) (ofs: offset)
  | PStoreORRO (rs: gpreg_o) (ra: ireg) (ofs: offset)
.

Arithmetic instructions

Inductive arith_name_r : Type :=
  | Ploadsymbol (id: ident) (ofs: ptrofs) (* load the address of a symbol *)
.

Inductive arith_name_rr : Type :=
  | Pmv (* register move *)
  | Pnegw (* negate word *)
  | Pnegl (* negate long *)
  | Pcvtl2w (* Convert Long to Word *)
  | Psxwd (* Sign Extend Word to Double Word *)
  | Pzxwd (* Zero Extend Word to Double Word *)
  | Pextfz (stop : Z) (start : Z) (* extract bit field, unsigned *)
  | Pextfs (stop : Z) (start : Z) (* extract bit field, signed *)
  | Pextfzl (stop : Z) (start : Z) (* extract bit field, unsigned *)
  | Pextfsl (stop : Z) (start : Z) (* extract bit field, signed *)
          
  | Pfabsd (* float absolute double *)
  | Pfabsw (* float absolute word *)
  | Pfnegd (* float negate double *)
  | Pfnegw (* float negate word *)
  | Pfinvw (* float invert word *)
  | Pfnarrowdw (* float narrow 64 -> 32 bits *)
  | Pfwidenlwd (* Floating Point widen from 32 bits to 64 bits *)
  | Pfloatwrnsz (* Floating Point conversion from integer (int -> SINGLE) *)
  | Pfloatuwrnsz (* Floating Point conversion from integer (unsigned int -> SINGLE) *)
  | Pfloatudrnsz (* Floating Point Conversion from integer (unsigned long -> float) *)
  | Pfloatdrnsz (* Floating Point Conversion from integer (long -> float) *)
  | Pfixedwrzz (* Integer conversion from floating point (single -> int) *)
  | Pfixeduwrzz (* Integer conversion from floating point (single -> unsigned int) *)
  | Pfixeddrzz (* Integer conversion from floating point (float -> long) *)
  | Pfixedudrzz (* Integer conversion from floating point (float -> unsigned long) *)
  | Pfixeddrzz_i32 (* Integer conversion from floating point (float -> int) *)
  | Pfixedudrzz_i32 (* Integer conversion from floating point (float -> unsigned int) *)
  | Pfixedwrne (* Integer conversion from floating point *)
  | Pfixeduwrne (* Integer conversion from floating point (f32 -> 32 bits unsigned *)
  | Pfixeddrne (* Integer conversion from floating point (i64 -> 64 bits) *)
  | Pfixedudrne. (* unsigned Integer conversion from floating point (u64 -> 64 bits) *)

Inductive arith_name_ri32 : Type :=
  | Pmake (* load immediate *)
.

Inductive arith_name_ri64 : Type :=
  | Pmakel (* load immediate long *)
.

Inductive arith_name_rf32 : Type :=
  | Pmakefs (* load immediate single *)
.

Inductive arith_name_rf64 : Type :=
  | Pmakef (* load immediate float *)
.

Inductive arith_name_rrr : Type :=
  | Pcompw (it: itest) (* comparison word *)
  | Pcompl (it: itest) (* comparison long *)
  | Pfcompw (ft: ftest) (* comparison float32 *)
  | Pfcompl (ft: ftest) (* comparison float64 *)

  | Paddw (* add word *)
  | Paddxw (shift : shift1_4) (* add shift *)
  | Psubw (* sub word word *)
  | Prevsubxw (shift : shift1_4) (* sub shift word *)
  | Pmulw (* mul word *)
  | Pandw (* and word *)
  | Pnandw (* nand word *)
  | Porw (* or word *)
  | Pnorw (* nor word *)
  | Pxorw (* xor word *)
  | Pnxorw (* nxor word *)
  | Pandnw (* andn word *)
  | Pornw (* orn word *)
  | Psraw (* shift right arithmetic word *)
  | Psrxw (* shift right arithmetic word round to 0 *)
  | Psrlw (* shift right logical word *)
  | Psllw (* shift left logical word *)

  | Paddl (* add long *)
  | Paddxl (shift : shift1_4) (* add shift long *)
  | Psubl (* sub long *)
  | Prevsubxl (shift : shift1_4) (* sub shift long *)
  | Pandl (* and long *)
  | Pnandl (* nand long *)
  | Porl (* or long *)
  | Pnorl (* nor long *)
  | Pxorl (* xor long *)
  | Pnxorl (* nxor long *)
  | Pandnl (* andn long *)
  | Pornl (* orn long *)
  | Pmull (* mul long (low part) *)
  | Pslll (* shift left logical long *)
  | Psrll (* shift right logical long *)
  | Psrxl (* shift right logical long round to 0 *)
  | Psral (* shift right arithmetic long *)

  | Pfaddd (* float add double *)
  | Pfaddw (* float add word *)
  | Pfsbfd (* float sub double *)
  | Pfsbfw (* float sub word *)
  | Pfmuld (* float multiply double *)
  | Pfmulw (* float multiply word *)
  | Pfmind (* float min double *)
  | Pfminw (* float min word *)
  | Pfmaxd (* float max double *)
  | Pfmaxw (* float max word *)

  | Pabdw (* absolute value of difference *)
  | Pabdl (* absolute value of difference *)
.

Inductive arith_name_rri32 : Type :=
  | Pcompiw (it: itest) (* comparison imm word *)

  | Paddiw (* add imm word *)
  | Paddxiw (shift : shift1_4)
  | Prevsubiw (* add imm word *)
  | Prevsubxiw (shift : shift1_4)
  | Pmuliw (* add imm word *)
  | Pandiw (* and imm word *)
  | Pnandiw (* nand imm word *)
  | Poriw (* or imm word *)
  | Pnoriw (* nor imm word *)
  | Pxoriw (* xor imm word *)
  | Pnxoriw (* nxor imm word *)
  | Pandniw (* andn word *)
  | Porniw (* orn word *)
  | Psraiw (* shift right arithmetic imm word *)
  | Psrxiw (* shift right arithmetic imm word round to 0 *)
  | Psrliw (* shift right logical imm word *)
  | Pslliw (* shift left logical imm word *)
  | Proriw (* rotate right imm word *)
  | Psllil (* shift left logical immediate long *)
  | Psrlil (* shift right logical immediate long *)
  | Psrail (* shift right arithmetic immediate long *)
  | Psrxil (* shift right arithmetic immediate long round to 0 *)
  | Pabdiw (* absolute value of difference *)
.

Inductive arith_name_rri64 : Type :=
  | Pcompil (it: itest) (* comparison imm long *)
  | Paddil (* add immediate long *)
  | Paddxil (shift : shift1_4)
  | Prevsubil
  | Prevsubxil (shift : shift1_4)
  | Pmulil (* mul immediate long *)
  | Pandil (* and immediate long *)
  | Pnandil (* nand immediate long *)
  | Poril (* or immediate long *)
  | Pnoril (* nor immediate long *)
  | Pxoril (* xor immediate long *)
  | Pnxoril (* nxor immediate long *)
  | Pandnil (* andn immediate long *)
  | Pornil (* orn immediate long *)
  | Pabdil (* absolute value of difference *)
.

Inductive arith_name_arrr : Type :=
  | Pmaddw (* multiply add word *)
  | Pmaddl (* multiply add long *)
  | Pmsubw (* multiply subtract word *)
  | Pmsubl (* multiply subtract long *)
  | Pcmove (bt: btest) (* conditional move *)
  | Pcmoveu (bt: btest) (* conditional move, test on unsigned semantics *)
  | Pfmaddfw (* float fused multiply add word *)
  | Pfmaddfl (* float fused multiply add long *)
  | Pfmsubfw (* float fused multiply subtract word *)
  | Pfmsubfl (* float fused multiply subtract long *)
.

Inductive arith_name_arri32 : Type :=
  | Pmaddiw (* multiply add word *)
  | Pcmoveiw (bt: btest)
  | Pcmoveuiw (bt: btest)
.

Inductive arith_name_arri64 : Type :=
  | Pmaddil (* multiply add long *)
  | Pcmoveil (bt: btest)
  | Pcmoveuil (bt: btest)
.

Inductive arith_name_arr : Type :=
  | Pinsf (stop : Z) (start : Z) (* insert bit field *)
  | Pinsfl (stop : Z) (start : Z) (* insert bit field *)
.

Inductive ar_instruction : Type :=
  | PArithR (i: arith_name_r) (rd: ireg)
  | PArithRR (i: arith_name_rr) (rd rs: ireg)
  | PArithRI32 (i: arith_name_ri32) (rd: ireg) (imm: int)
  | PArithRI64 (i: arith_name_ri64) (rd: ireg) (imm: int64)
  | PArithRF32 (i: arith_name_rf32) (rd: ireg) (imm: float32)
  | PArithRF64 (i: arith_name_rf64) (rd: ireg) (imm: float)
  | PArithRRR (i: arith_name_rrr) (rd rs1 rs2: ireg)
  | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
  | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
  | PArithARRR (i: arith_name_arrr) (rd rs1 rs2: ireg)
  | PArithARR (i: arith_name_arr) (rd rs: ireg)
  | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
  | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
.

Module PArithCoercions.

Coercion PArithR: arith_name_r >-> Funclass.
Coercion PArithRR: arith_name_rr >-> Funclass.
Coercion PArithRI32: arith_name_ri32 >-> Funclass.
Coercion PArithRI64: arith_name_ri64 >-> Funclass.
Coercion PArithRF32: arith_name_rf32 >-> Funclass.
Coercion PArithRF64: arith_name_rf64 >-> Funclass.
Coercion PArithRRR: arith_name_rrr >-> Funclass.
Coercion PArithRRI32: arith_name_rri32 >-> Funclass.
Coercion PArithRRI64: arith_name_rri64 >-> Funclass.
Coercion PArithARRR: arith_name_arrr >-> Funclass.
Coercion PArithARR: arith_name_arr >-> Funclass.
Coercion PArithARRI32: arith_name_arri32 >-> Funclass.
Coercion PArithARRI64: arith_name_arri64 >-> Funclass.

End PArithCoercions.

Basic instructions

Inductive basic : Type :=
  | PArith (i: ar_instruction)
  | PLoad (i: ld_instruction)
  | PStore (i: st_instruction)
  | Pallocframe (sz: Z) (pos: ptrofs) (* allocate new stack frame *)
  | Pfreeframe (sz: Z) (pos: ptrofs) (* deallocate stack frame and restore previous frame *)
  | Pget (rd: ireg) (rs: preg) (* get system register *)
  | Pset (rd: preg) (rs: ireg) (* set system register *)
  | Pnop (* virtual instruction that does nothing *)
.

Coercion PLoad: ld_instruction >-> basic.
Coercion PStore: st_instruction >-> basic.
Coercion PArith: ar_instruction >-> basic.

Control-flow instructions

Inductive control : Type :=
  | PExpand (i: ex_instruction)
  | PCtlFlow (i: cf_instruction)
.

Coercion PExpand: ex_instruction >-> control.
Coercion PCtlFlow: cf_instruction >-> control.

Definition of a bblock (ie a bundle)

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.


Definition builtin_aloneb (body: list basic) (exit: option control) :=
  match exit with
  | Some (PExpand (Pbuiltin _ _ _)) =>
    match body with
    | nil => true
    | _ => false
    end
  | _ => true
  end.

Definition wf_bblockb (body: list basic) (exit: option control) :=
  (non_empty_bblockb body exit) && (builtin_aloneb body exit).


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

Definition length_opt {A} (o: option A) : nat :=
  match o with
  | Some o => 1
  | None => 0
  end.

Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).

Definition bblocks := list bblock.

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

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

Parallel Semantics of bundles

Definition regset := Pregmap.t val.

Definition genv := Genv.t fundef unit.

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.

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.

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.

Local Open Scope asm.

Section RELSEM.

Variable ge: genv.


Inductive outcome: Type :=
  | Next (rs:regset) (m:mem)
  | Stuck
.

Arithmetic Expressions (including comparisons)

Inductive signedness: Type := Signed | Unsigned.

Inductive intsize: Type := Int | Long.

Definition itest_for_cmp (c: comparison) (s: signedness) :=
  match c, s with
  | Cne, Signed => ITne
  | Ceq, Signed => ITeq
  | Clt, Signed => ITlt
  | Cge, Signed => ITge
  | Cle, Signed => ITle
  | Cgt, Signed => ITgt
  | Cne, Unsigned => ITneu
  | Ceq, Unsigned => ITequ
  | Clt, Unsigned => ITltu
  | Cge, Unsigned => ITgeu
  | Cle, Unsigned => ITleu
  | Cgt, Unsigned => ITgtu
  end.

Inductive oporder_ftest :=
  | Normal (ft: ftest)
  | Reversed (ft: ftest)
.

Definition ftest_for_cmp (c: comparison) :=
  match c with
  | Ceq => Normal FToeq
  | Cne => Normal FTune
  | Clt => Normal FTolt
  | Cle => Reversed FToge
  | Cgt => Reversed FTolt
  | Cge => Normal FToge
  end.

Definition notftest_for_cmp (c: comparison) :=
  match c with
  | Ceq => Normal FTune
  | Cne => Normal FToeq
  | Clt => Normal FTuge
  | Cle => Reversed FTult
  | Cgt => Reversed FTuge
  | Cge => Normal FTult
  end.

Definition btest_for_cmpswz (c: comparison) :=
  match c with
  | Cne => BTwnez
  | Ceq => BTweqz
  | Clt => BTwltz
  | Cge => BTwgez
  | Cle => BTwlez
  | Cgt => BTwgtz
  end.

Definition btest_for_cmpsdz (c: comparison) :=
  match c with
  | Cne => BTdnez
  | Ceq => BTdeqz
  | Clt => BTdltz
  | Cge => BTdgez
  | Cle => BTdlez
  | Cgt => BTdgtz
  end.

Definition cmp_for_btest (bt: btest) :=
  match bt with
  | BTwnez => (Some Cne, Int)
  | BTweqz => (Some Ceq, Int)
  | BTwltz => (Some Clt, Int)
  | BTwgez => (Some Cge, Int)
  | BTwlez => (Some Cle, Int)
  | BTwgtz => (Some Cgt, Int)

  | BTdnez => (Some Cne, Long)
  | BTdeqz => (Some Ceq, Long)
  | BTdltz => (Some Clt, Long)
  | BTdgez => (Some Cge, Long)
  | BTdlez => (Some Cle, Long)
  | BTdgtz => (Some Cgt, Long)
  end.

Definition cmpu_for_btest (bt: btest) :=
  match bt with
  | BTwnez => (Some Cne, Int)
  | BTweqz => (Some Ceq, Int)
  | BTdnez => (Some Cne, Long)
  | BTdeqz => (Some Ceq, Long)
  | _ => (None, Int)
  end.

Comparing integers

Definition compare_int (t: itest) (v1 v2: val): val :=
  match t with
  | ITne => Val.cmp Cne v1 v2
  | ITeq => Val.cmp Ceq v1 v2
  | ITlt => Val.cmp Clt v1 v2
  | ITge => Val.cmp Cge v1 v2
  | ITle => Val.cmp Cle v1 v2
  | ITgt => Val.cmp Cgt v1 v2
  | ITneu => Val.mxcmpu Cne v1 v2
  | ITequ => Val.mxcmpu Ceq v1 v2
  | ITltu => Val.mxcmpu Clt v1 v2
  | ITgeu => Val.mxcmpu Cge v1 v2
  | ITleu => Val.mxcmpu Cle v1 v2
  | ITgtu => Val.mxcmpu Cgt v1 v2
  end.

Definition compare_long (t: itest) (v1 v2: val): val :=
  let res := match t with
  | ITne => Val.cmpl Cne v1 v2
  | ITeq => Val.cmpl Ceq v1 v2
  | ITlt => Val.cmpl Clt v1 v2
  | ITge => Val.cmpl Cge v1 v2
  | ITle => Val.cmpl Cle v1 v2
  | ITgt => Val.cmpl Cgt v1 v2
  | ITneu => Some (Val.mxcmplu Cne v1 v2)
  | ITequ => Some (Val.mxcmplu Ceq v1 v2)
  | ITltu => Some (Val.mxcmplu Clt v1 v2)
  | ITgeu => Some (Val.mxcmplu Cge v1 v2)
  | ITleu => Some (Val.mxcmplu Cle v1 v2)
  | ITgtu => Some (Val.mxcmplu Cgt v1 v2)
  end in
  match res with
  | Some v => v
  | None => Vundef
  end
  .

Definition compare_single (t: ftest) (v1 v2: val): val :=
  match t with
  | FTone | FTueq => Vundef
  | FToeq => Val.cmpfs Ceq v1 v2
  | FTune => Val.cmpfs Cne v1 v2
  | FTolt => Val.cmpfs Clt v1 v2
  | FTuge => Val.notbool (Val.cmpfs Clt v1 v2)
  | FToge => Val.cmpfs Cge v1 v2
  | FTult => Val.notbool (Val.cmpfs Cge v1 v2)
  end.

Definition compare_float (t: ftest) (v1 v2: val): val :=
  match t with
  | FTone | FTueq => Vundef
  | FToeq => Val.cmpf Ceq v1 v2
  | FTune => Val.cmpf Cne v1 v2
  | FTolt => Val.cmpf Clt v1 v2
  | FTuge => Val.notbool (Val.cmpf Clt v1 v2)
  | FToge => Val.cmpf Cge v1 v2
  | FTult => Val.notbool (Val.cmpf Cge v1 v2)
  end.

Arithmetic evaluators

Definition arith_eval_r n :=
  match n with
  | Ploadsymbol s ofs => Genv.symbol_address ge s ofs
  end
.

Definition arith_eval_rr n v :=
  match n with
  | Pmv => v
  | Pnegw => Val.neg v
  | Pnegl => Val.negl v
  | Pcvtl2w => Val.loword v
  | Psxwd => Val.longofint v
  | Pzxwd => Val.longofintu v
  | Pextfz stop start => extfz stop start v
  | Pextfs stop start => extfs stop start v
  | Pextfzl stop start => extfzl stop start v
  | Pextfsl stop start => extfsl stop start v
  | Pfnegd => Val.negf v
  | Pfnegw => Val.negfs v
  | Pfabsd => Val.absf v
  | Pfabsw => Val.absfs v
  | Pfinvw => ExtValues.invfs v
  | Pfnarrowdw => Val.singleoffloat v
  | Pfwidenlwd => Val.floatofsingle v
  | Pfloatwrnsz => Val.maketotal (Val.singleofint v)
  | Pfloatuwrnsz => Val.maketotal (Val.singleofintu v)
  | Pfloatudrnsz => Val.maketotal (Val.floatoflongu v)
  | Pfloatdrnsz => Val.maketotal (Val.floatoflong v)
  | Pfixedwrzz => Val.maketotal (Val.intofsingle v)
  | Pfixeduwrzz => Val.maketotal (Val.intuofsingle v)
  | Pfixeddrzz => Val.maketotal (Val.longoffloat v)
  | Pfixedudrzz => Val.maketotal (Val.longuoffloat v)
  | Pfixeddrzz_i32 => Val.maketotal (Val.intoffloat v)
  | Pfixedudrzz_i32 => Val.maketotal (Val.intuoffloat v)
  | Pfixedudrne => Val.maketotal (Val.longuoffloat_ne v)
  | Pfixeddrne => Val.maketotal (Val.longoffloat_ne v)
  | Pfixeduwrne => Val.maketotal (Val.intuofsingle_ne v)
  | Pfixedwrne => Val.maketotal (Val.intofsingle_ne v)
  end.

Definition arith_eval_ri32 n i :=
  match n with
  | Pmake => Vint i
  end.

Definition arith_eval_ri64 n i :=
  match n with
  | Pmakel => Vlong i
  end.

Definition arith_eval_rf32 n i :=
  match n with
  | Pmakefs => Vsingle i
  end.

Definition arith_eval_rf64 n i :=
  match n with
  | Pmakef => Vfloat i
  end.

Definition arith_eval_rrr n v1 v2 :=
  match n with
  | Pcompw c => compare_int c v1 v2
  | Pcompl c => compare_long c v1 v2
  | Pfcompw c => compare_single c v1 v2
  | Pfcompl c => compare_float c v1 v2

  | Paddw => Val.add v1 v2
  | Psubw => Val.sub v1 v2
  | Pmulw => Val.mul v1 v2
  | Pandw => Val.and v1 v2
  | Pnandw => Val.notint (Val.and v1 v2)
  | Porw => Val.or v1 v2
  | Pnorw => Val.notint (Val.or v1 v2)
  | Pxorw => Val.xor v1 v2
  | Pnxorw => Val.notint (Val.xor v1 v2)
  | Pandnw => Val.and (Val.notint v1) v2
  | Pornw => Val.or (Val.notint v1) v2
  | Psrlw => Val.shru v1 v2
  | Psraw => Val.shr v1 v2
  | Psllw => Val.shl v1 v2
  | Psrxw => ExtValues.val_shrx v1 v2

  | Paddl => Val.addl v1 v2
  | Psubl => Val.subl v1 v2
  | Pandl => Val.andl v1 v2
  | Pnandl => Val.notl (Val.andl v1 v2)
  | Porl => Val.orl v1 v2
  | Pnorl => Val.notl (Val.orl v1 v2)
  | Pxorl => Val.xorl v1 v2
  | Pnxorl => Val.notl (Val.xorl v1 v2)
  | Pandnl => Val.andl (Val.notl v1) v2
  | Pornl => Val.orl (Val.notl v1) v2
  | Pmull => Val.mull v1 v2
  | Pslll => Val.shll v1 v2
  | Psrll => Val.shrlu v1 v2
  | Psral => Val.shrl v1 v2
  | Psrxl => ExtValues.val_shrxl v1 v2

  | Pfaddd => Val.addf v1 v2
  | Pfaddw => Val.addfs v1 v2
  | Pfsbfd => Val.subf v1 v2
  | Pfsbfw => Val.subfs v1 v2
  | Pfmuld => Val.mulf v1 v2
  | Pfmulw => Val.mulfs v1 v2

  | Pfmind => ExtValues.minf v1 v2
  | Pfminw => ExtValues.minfs v1 v2
  | Pfmaxd => ExtValues.maxf v1 v2
  | Pfmaxw => ExtValues.maxfs v1 v2

  | Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2
  | Paddxl shift => ExtValues.addxl (int_of_shift1_4 shift) v1 v2

  | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2
  | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2

  | Pabdw => ExtValues.absdiff v1 v2
  | Pabdl => ExtValues.absdiffl v1 v2
  end.

Definition arith_eval_rri32 n v i :=
  match n with
  | Pcompiw c => compare_int c v (Vint i)
  | Paddiw => Val.add v (Vint i)
  | Prevsubiw => Val.sub (Vint i) v
  | Pmuliw => Val.mul v (Vint i)
  | Pandiw => Val.and v (Vint i)
  | Pnandiw => Val.notint (Val.and v (Vint i))
  | Poriw => Val.or v (Vint i)
  | Pnoriw => Val.notint (Val.or v (Vint i))
  | Pxoriw => Val.xor v (Vint i)
  | Pnxoriw => Val.notint (Val.xor v (Vint i))
  | Pandniw => Val.and (Val.notint v) (Vint i)
  | Porniw => Val.or (Val.notint v) (Vint i)
  | Psraiw => Val.shr v (Vint i)
  | Psrxiw => ExtValues.val_shrx v (Vint i)
  | Psrliw => Val.shru v (Vint i)
  | Pslliw => Val.shl v (Vint i)
  | Proriw => Val.ror v (Vint i)
  | Psllil => Val.shll v (Vint i)
  | Psrxil => ExtValues.val_shrxl v (Vint i)
  | Psrlil => Val.shrlu v (Vint i)
  | Psrail => Val.shrl v (Vint i)
  | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i)
  | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i)
  | Pabdiw => ExtValues.absdiff v (Vint i)
  end.

Definition arith_eval_rri64 n v i :=
  match n with
  | Pcompil c => compare_long c v (Vlong i)
  | Paddil => Val.addl v (Vlong i)
  | Prevsubil => Val.subl (Vlong i) v
  | Pmulil => Val.mull v (Vlong i)
  | Pandil => Val.andl v (Vlong i)
  | Pnandil => Val.notl (Val.andl v (Vlong i))
  | Poril => Val.orl v (Vlong i)
  | Pnoril => Val.notl (Val.orl v (Vlong i))
  | Pxoril => Val.xorl v (Vlong i)
  | Pnxoril => Val.notl (Val.xorl v (Vlong i))
  | Pandnil => Val.andl (Val.notl v) (Vlong i)
  | Pornil => Val.orl (Val.notl v) (Vlong i)
  | Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i)
  | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i)
  | Pabdil => ExtValues.absdiffl v (Vlong i)
  end.

Definition cmove bt v1 v2 v3 :=
  match cmp_for_btest bt with
  | (Some c, Int) =>
    match Val.cmp_bool c v2 (Vint Int.zero) with
    | None => Vundef
    | Some true => v3
    | Some false => v1
    end
  | (Some c, Long) =>
    match Val.cmpl_bool c v2 (Vlong Int64.zero) with
    | None => Vundef
    | Some true => v3
    | Some false => v1
    end
  | (None, _) => Vundef
  end.

Definition cmoveu bt v1 v2 v3 :=
  match cmpu_for_btest bt with
  | (Some c, Int) =>
    match Val.mxcmpu_bool c v2 (Vint Int.zero) with
    | None => Vundef
    | Some true => v3
    | Some false => v1
    end
  | (Some c, Long) =>
    match Val.mxcmplu_bool c v2 (Vlong Int64.zero) with
    | None => Vundef
    | Some true => v3
    | Some false => v1
    end
  | (None, _) => Vundef
  end.

Definition arith_eval_arrr n v1 v2 v3 :=
  match n with
  | Pmaddw => Val.add v1 (Val.mul v2 v3)
  | Pmaddl => Val.addl v1 (Val.mull v2 v3)
  | Pmsubw => Val.sub v1 (Val.mul v2 v3)
  | Pmsubl => Val.subl v1 (Val.mull v2 v3)
  | Pcmove bt => cmove bt v1 v2 v3
  | Pcmoveu bt => cmoveu bt v1 v2 v3
  | Pfmaddfw => ExtValues.fmaddfs v1 v2 v3
  | Pfmaddfl => ExtValues.fmaddf v1 v2 v3
  | Pfmsubfw => ExtValues.fmsubfs v1 v2 v3
  | Pfmsubfl => ExtValues.fmsubf v1 v2 v3
  end.

Definition arith_eval_arr n v1 v2 :=
  match n with
  | Pinsf stop start => ExtValues.insf stop start v1 v2
  | Pinsfl stop start => ExtValues.insfl stop start v1 v2
  end.

Definition arith_eval_arri32 n v1 v2 v3 :=
  match n with
  | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
  | Pcmoveiw bt => cmove bt v1 v2 (Vint v3)
  | Pcmoveuiw bt => cmoveu bt v1 v2 (Vint v3)
  end.

Definition arith_eval_arri64 n v1 v2 v3 :=
  match n with
  | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
  | Pcmoveil bt => cmove bt v1 v2 (Vlong v3)
  | Pcmoveuil bt => cmoveu bt v1 v2 (Vlong v3)
  end.

Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
  match ai with
  | PArithR n d => rsw#d <- (arith_eval_r n)

  | PArithRR n d s => rsw#d <- (arith_eval_rr n rsr#s)

  | PArithRI32 n d i => rsw#d <- (arith_eval_ri32 n i)
  | PArithRI64 n d i => rsw#d <- (arith_eval_ri64 n i)
  | PArithRF32 n d i => rsw#d <- (arith_eval_rf32 n i)
  | PArithRF64 n d i => rsw#d <- (arith_eval_rf64 n i)

  | PArithRRR n d s1 s2 => rsw#d <- (arith_eval_rrr n rsr#s1 rsr#s2)
  | PArithRRI32 n d s i => rsw#d <- (arith_eval_rri32 n rsr#s i)
  | PArithRRI64 n d s i => rsw#d <- (arith_eval_rri64 n rsr#s i)

  | PArithARRR n d s1 s2 => rsw#d <- (arith_eval_arrr n rsr#d rsr#s1 rsr#s2)
  | PArithARR n d s => rsw#d <- (arith_eval_arr n rsr#d rsr#s)
  | PArithARRI32 n d s i => rsw#d <- (arith_eval_arri32 n rsr#d rsr#s i)
  | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i)
  end.

Definition eval_offset (ofs: offset) : res ptrofs := OK ofs.

load/store instructions

Definition parexec_incorrect_load trap d rsw mw :=
  match trap with
  | TRAP => Stuck
  | NOTRAP => Next (rsw#d <- Vundef) mw
  end.

Definition parexec_load_offset (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
  match (eval_offset ofs) with
  | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
              | None => parexec_incorrect_load trap d rsw mw
              | Some v => Next (rsw#d <- v) mw
              end
  | _ => Stuck
  end.

Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a: ireg) (ofs: offset) :=
  let (rd0, rd1) := gpreg_q_expand d in
    match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with
    | None => Stuck
    | Some v0 =>
      match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) with
      | None => Stuck
      | Some v1 => Next (rsw#rd0 <- v0 #rd1 <- v1) mw
      end
    end.

Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a: ireg) (ofs: offset) :=
  match gpreg_o_expand d with
  | (rd0, rd1, rd2, rd3) =>
   match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with
    | None => Stuck
    | Some v0 =>
      match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) with
      | None => Stuck
      | Some v1 =>
        match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 16))) with
        | None => Stuck
        | Some v2 =>
          match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 24))) with
          | None => Stuck
          | Some v3 =>
            Next (rsw#rd0 <- v0 #rd1 <- v1 #rd2 <- v2 #rd3 <- v3) mw
          end
        end
      end
    end
  end.

Definition parexec_load_reg (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
  match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with
  | None => parexec_incorrect_load trap d rsw mw
  | Some v => Next (rsw#d <- v) mw
  end.

Definition parexec_load_regxs (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
  match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with
  | None => parexec_incorrect_load trap d rsw mw
  | Some v => Next (rsw#d <- v) mw
  end.

Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) :=
  match (eval_offset ofs) with
  | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
              | None => Stuck
              | Some m' => Next rsw m'
              end
  | _ => Stuck
  end.

Definition parexec_store_reg
           (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) :=
  match Mem.storev chunk mr (Val.addl (rsr a) (rsr ro)) (rsr s) with
  | None => Stuck
  | Some m' => Next rsw m'
  end.

Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) :=
  match Mem.storev chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) (rsr s) with
  | None => Stuck
  | Some m' => Next rsw m'
  end.

Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) (a: ireg) (ofs: offset) :=
  let (s0, s1) := gpreg_q_expand s in
  match Mem.storev Many64 mr (Val.offset_ptr (rsr a) ofs) (rsr s0) with
  | None => Stuck
  | Some m1 =>
    match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) (rsr s1) with
    | None => Stuck
    | Some m2 => Next rsw m2
    end
  end.
  
Definition parexec_store_o_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_o) (a: ireg) (ofs: offset) :=
  match gpreg_o_expand s with
  | (s0, s1, s2, s3) =>
    match Mem.storev Many64 mr (Val.offset_ptr (rsr a) ofs) (rsr s0) with
    | None => Stuck
    | Some m1 =>
      match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) (rsr s1) with
      | None => Stuck
      | Some m2 =>
        match Mem.storev Many64 m2 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 16))) (rsr s2) with
        | None => Stuck
        | Some m3 =>
          match Mem.storev Many64 m3 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 24))) (rsr s3) with
          | None => Stuck
          | Some m4 => Next rsw m4
          end
        end
      end
    end
  end.
  

Definition load_chunk n :=
  match n with
  | Plb => Mint8signed
  | Plbu => Mint8unsigned
  | Plh => Mint16signed
  | Plhu => Mint16unsigned
  | Plw => Mint32
  | Plw_a => Many32
  | Pld => Mint64
  | Pld_a => Many64
  | Pfls => Mfloat32
  | Pfld => Mfloat64
  end.
              
Definition store_chunk n :=
  match n with
  | Psb => Mint8unsigned
  | Psh => Mint16unsigned
  | Psw => Mint32
  | Psw_a => Many32
  | Psd => Mint64
  | Psd_a => Many64
  | Pfss => Mfloat32
  | Pfsd => Mfloat64
  end.

Basic (instruction) step

Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
  match bi with
  | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw

  | PLoad (PLoadRRO trap n d a ofs) => parexec_load_offset trap (load_chunk n) rsr rsw mr mw d a ofs
  | PLoad (PLoadRRR trap n d a ro) => parexec_load_reg trap (load_chunk n) rsr rsw mr mw d a ro
  | PLoad (PLoadRRRXS trap n d a ro) => parexec_load_regxs trap (load_chunk n) rsr rsw mr mw d a ro
  | PLoad (PLoadQRRO d a ofs) =>
    parexec_load_q_offset rsr rsw mr mw d a ofs
  | PLoad (PLoadORRO d a ofs) =>
    parexec_load_o_offset rsr rsw mr mw d a ofs

  | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs
  | PStoreRRR n s a ro => parexec_store_reg (store_chunk n) rsr rsw mr mw s a ro
  | PStoreRRRXS n s a ro => parexec_store_regxs (store_chunk n) rsr rsw mr mw s a ro
  | PStoreQRRO s a ofs =>
    parexec_store_q_offset rsr rsw mr mw s a ofs
  | PStoreORRO s a ofs =>
    parexec_store_o_offset rsr rsw mr mw s a ofs

  | Pallocframe sz pos =>
      let (mw, stk) := Mem.alloc mr 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      match Mem.storev Mptr mw (Val.offset_ptr sp pos) rsr#SP with
      | None => Stuck
      | Some mw => Next (rsw #FP <- (rsr SP) #SP <- sp #RTMP <- Vundef) mw
      end

  | Pfreeframe sz pos =>
      match Mem.loadv Mptr mr (Val.offset_ptr rsr#SP pos) with
      | None => Stuck
      | Some v =>
          match rsr SP with
          | Vptr stk ofs =>
              match Mem.free mr stk 0 sz with
              | None => Stuck
              | Some mw => Next (rsw#SP <- v #RTMP <- Vundef) mw
              end
          | _ => Stuck
          end
      end
  | Pget rd ra =>
    match ra with
    | RA => Next (rsw#rd <- (rsr#ra)) mw
    | _ => Stuck
    end
  | Pset ra rd =>
    match ra with
    | RA => Next (rsw#ra <- (rsr#rd)) mw
    | _ => Stuck
    end
  | Pnop => Next rsw mw
end.

parexec with writes-in-order

Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
  match body with
  | nil => Next rsw mw
  | bi::body' =>
     match bstep bi rsr rsw mr mw with
     | Next rsw mw => parexec_wio_body body' rsr rsw mr mw
     | Stuck => Stuck
     end
  end.

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.

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 par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) :=
  match label_pos lbl 0 (fn_blocks f) with
  | None => Stuck
  | Some pos =>
      match rsr#PC with
      | Vptr b ofs => Next (rsw#PC <- (Vptr b (Ptrofs.repr pos))) mw
      | _ => Stuck
      end
  end.

Parallel Evaluation of a branch

Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) :=
  match res with
    | Some true => par_goto_label f l rsr rsw mw
    | Some false => Next (rsw # PC <- (rsr PC)) mw
    | None => Stuck
  end.

Parallel execution of a control-flow instruction

Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) (mw: mem) :=
  match oc with
  | None => Next (rsw#PC <- (rsr#PC)) mw
  | Some ic => (* Branch Control Unit instructions *)
    match ic with
    | Pret =>
      Next (rsw#PC <- (rsr#RA)) mw
    | Pcall s =>
      Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
    | Picall r =>
      Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw
    | Pjumptable r tbl =>
      match rsr#r with
      | Vint n =>
        match list_nth_z tbl (Int.unsigned n) with
        | None => Stuck
        | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw
        end
      | _ => Stuck
      end
    | Pgoto s =>
      Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
    | Pigoto r =>
      Next (rsw#PC <- (rsr#r)) mw
    | Pj_l l =>
      par_goto_label f l rsr rsw mw
    | Pcb bt r l =>
      match cmp_for_btest bt with
      | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.cmp_bool c rsr#r (Vint (Int.repr 0)))
      | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.cmpl_bool c rsr#r (Vlong (Int64.repr 0)))
      | (None, _) => Stuck
      end
    | Pcbu bt r l =>
      match cmpu_for_btest bt with
      | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.mxcmpu_bool c rsr#r (Vint (Int.repr 0)))
      | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.mxcmplu_bool c rsr#r (Vlong (Int64.repr 0)))
      | (None, _) => Stuck
      end
    | Pbuiltin ef args res =>
      Stuck (* treated specially below *)
    end
  end.


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

Definition estep (f: function) ext size_b (rsr rsw: regset) (mw: mem)
  := parexec_control f ext (incrPC size_b rsr) rsw mw.

Definition parexec_wio f bdy ext size_b (rs: regset) (m: mem): outcome :=
  match parexec_wio_body bdy rs rs m m with
  | Next rsw mw => estep f ext size_b rs rsw mw
  | Stuck => Stuck
  end.

non-deterministic (out-of-order writes) parallel execution of bundles

Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
   exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\
      o=match parexec_wio f bdy1 (exit bundle) (Ptrofs.repr (size bundle)) rs m with
      | Next rsw mw => parexec_wio_body bdy2 rs rsw m mw
      | Stuck => Stuck
      end.

deterministic parallel (out-of-order writes) execution of bundles

Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' m': Prop :=
   forall o, parexec_bblock f bundle rs m o -> o = Next rs' m'.

Translation of the LTL/Linear/Mach view of machine registers to the assembly view. Note that no LTL register maps to X31. This register is reserved as temporary, to be used by the generated RV32G code.

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 assembly 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 (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 bblocks in a code sequence by position.

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 state: Type :=
  | State: regset -> mem -> state.

Definition nextblock (b:bblock) (rs: regset) :=
  incrPC (Ptrofs.repr (size b)) rs.

Inductive step: state -> trace -> state -> Prop :=
  | exec_step_internal:
      forall b ofs f bundle rs m 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 bundle ->
      det_parexec f bundle rs m 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' bi,
      rs PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      find_bblock (Ptrofs.unsigned ofs) f.(fn_blocks) = Some bi ->
      exit bi = Some (PExpand (Pbuiltin ef args res)) ->
      eval_builtin_args ge rs (rs SP) m args vargs ->
      external_call ef ge vargs m t vres m' ->
      rs' = nextblock bi
              (set_res res vres
                (undef_regs (map preg_of (destroyed_by_builtin ef))
                   (rs#RTMP <- Vundef))) ->
      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')
  .


Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
  parexec_wio f (body b) (exit b) (Ptrofs.repr (size b)) rs m.


Lemma parexec_bblock_write_in_order f b rs m:
   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).


Local Hint Resolve parexec_bblock_write_in_order: core.

Lemma det_parexec_write_in_order f b rs m rs' m':
   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.

End RELSEM.

Execution of whole programs.

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)
        # SP <- Vnullptr
        # RA <- Vnullptr 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 = Vnullptr ->
      rs GPR0 = Vint r ->
      final_state (State rs m) r.

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

Remark extcall_arguments_determ:
  forall rs m sg args1 args2,
  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.

Lemma semantics_determinate p: determinate (semantics p).