Module Asmvliw


Abstract syntax and semantics for VLIW semantics of KVX assembly language.

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.

Abstract syntax


A KVX program is syntactically given as a list of functions. Each function is associated to a list of bundles of type bblock below. Hence, syntactically, we view each bundle as a basic block: this view induces our sequential semantics of bundles defined in Asmblock.

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}.
Proof.
decide equality. Defined.

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

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

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}.
Proof.
decide equality. Defined.

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}.
Proof.
decide equality. Defined.

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}.
Proof.
decide equality. apply ireg_eq. Defined.

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


We model a subset of the KVX instruction set.

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

Similarly to other CompCert assembly languages, the pseudo-instructions are the following: This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline.

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

Definition concrete_default_notrap_load_value (chunk : memory_chunk) :=
  match chunk with
  | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned
  | Mint32 => Vint Int.zero
  | Mint64 => Vlong Int64.zero
  | Many32 | Many64 => Vundef
  | Mfloat32 => Vsingle Float32.zero
  | Mfloat64 => Vfloat Float.zero
  end.

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

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

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

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

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)


A bundle/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 bundle (which depends on the number of instructions in the bundles of lower addresses).

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.


For now, we consider a builtin is alone in a bundle (and a basic block). Is there a way to avoid that ? (TODO)
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).

A bblock is well-formed if he contains at least one instruction, and if there is a builtin then it must be alone in this bblock.

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.

The 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. WARNING: this notion of size is not the same than in Machblock ! We ignore labels here...
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


The semantics operates over a single mapping from registers (type preg) to values. We maintain the convention that integer registers are mapped to values of type Tint or Tlong (in 64 bit mode), and float registers to values of type Tsingle or Tfloat.

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.

The parallel semantics on bundles is purely small-step and defined as a relation from the current state (a register set + a memory state) to either Next rs' m' where rs' and m' are the updated register set and memory state after execution of the instruction at rs#PC, or Stuck if the processor is stuck. The parallel semantics of each instructions handles two states in input: - the actual input state of the bundle which is only read - and the other on which every "write" is performed: it represents a temporary "writes" buffer, from which the final state of the bundle is computed. NB: the sequential semantics defined in Asmblock is derived from the parallel semantics of each instruction by identifying the read state and the write state.

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)
  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
  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)
  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)
  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 chunk d rsw mw :=
  match trap with
  | TRAP => Stuck
  | NOTRAP => Next (rsw#d <- (concrete_default_notrap_load_value chunk)) 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 chunk 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 chunk 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 chunk 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) }.
Proof.
  apply List.in_dec.
  apply Pos.eq_dec.
Qed.



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)); cbn; 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)); cbn; 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 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


Warning: PC is assumed to be already pointing on the next bundle !

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


As above: PC is assumed to be incremented on the next block before the 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).

parallel execution of the exit instruction of a bundle
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')
  .


parallel in-order writes execution of bundles
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).
Proof.
   exists (body b). exists nil.
   constructor 1.
   - rewrite app_nil_r; auto.
   - unfold parexec_wio_bblock.
     destruct (parexec_wio f _ _ _); cbn; auto.
Qed.


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'.
Proof.
   unfold det_parexec; auto.
Qed.

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.
Proof.
  intros until m.
  assert (A: forall l v1 v2,
             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
  { intros. inv H; inv H0; congruence. }
  assert (B: forall p v1 v2,
             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
  { intros. inv H; inv H0.
    eapply A; eauto.
    f_equal; eapply A; eauto. }
  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
  {
    induction 1; intros vl2 EA; inv EA.
    auto.
    f_equal; eauto. }
  intros. eapply C; eauto.
Qed.

Lemma semantics_determinate p: determinate (semantics p).
Proof.
Ltac Equalities :=
  match goal with
  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
      rewrite H1 in H2; inv H2; Equalities
  | _ => idtac
  end.
Ltac Det_WIO X :=
  match goal with
  | [ H: det_parexec _ _ _ _ _ _ _ |- _ ] =>
      exploit det_parexec_write_in_order; [ eapply H | idtac]; clear H; intro X
  | _ => idtac
  end.
  intros; constructor; cbn.
- (* determ *) intros s t1 s1 t2 s2 H H0. inv H; Det_WIO X1;
  inv H0; Det_WIO X2; Equalities.
  + split. constructor. auto.
  + unfold parexec_wio_bblock, parexec_wio in X1. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
    rewrite H8 in X1. discriminate.
  + unfold parexec_wio_bblock, parexec_wio in X2. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
    rewrite H4 in X2. discriminate.
  + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
    exploit external_call_determ. eexact H6. eexact H13. intros [A B].
    split. auto. intros. destruct B; auto. subst. auto.
  + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
    exploit external_call_determ. eexact H3. eexact H8. intros [A B].
    split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
  red; intros. inv H; cbn.
  omega.
  eapply external_call_trace_length; eauto.
  eapply external_call_trace_length; eauto.
- (* initial states *)
  intros s1 s2 H H0; inv H; inv H0; f_equal; congruence.
- (* final no step *)
  intros s r H; assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
  inv H. red; intros; red; intros.
  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
- (* final states *)
  intros s r1 r2 H H0; inv H; inv H0. congruence.
Qed.