Module Asm


Abstract syntax for KVX textual assembly language. Each emittable instruction is defined here. ';;' is also defined as an instruction. The goal of this representation is to stay compatible with the rest of the generic backend of CompCert We define unfold : list bblock -> list instruction An Asm function is then defined as : fn_sig, fn_blocks, fn_code, and a proof of unfold fn_blocks = fn_code fn_code has no semantic. Instead, the semantic of Asm is given by using the AsmVLIW semantic on fn_blocks

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 Export Asmvliw.
Require Import Linking.
Require Import Errors.

Definitions for OCaml code
Definition label := positive.

Definition preg := preg.

Inductive addressing : Type :=
  | AOff (ofs: offset)
  | AReg (ro: ireg)
  | ARegXS (ro: ireg)
.

Syntax

Inductive instruction : Type :=
pseudo instructions
  | Pallocframe (sz: Z) (pos: ptrofs) (* allocate new stack frame *)
  | Pfreeframe (sz: Z) (pos: ptrofs) (* deallocate stack frame and restore previous frame *)
  | Plabel (lbl: label) (* define a code label *)
  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (* load the address of a symbol *)
  | Pbuiltin: external_function -> list (builtin_arg preg)
              -> builtin_res preg -> instruction (* built-in function (pseudo) *)
  | Psemi (* semi colon separating bundles *)
  | Pnop (* instruction that does nothing *)

Control flow instructions
  | Pget (rd: ireg) (rs: preg) (* get system register *)
  | Pset (rd: preg) (rs: ireg) (* set system register *)
  | Pret (* return *)
  | Pcall (l: label) (* function call *)
  | Picall (rs: ireg) (* function call on register *)
  | Pgoto (l: label) (* goto *)
  | Pigoto (rs: 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 *)
  | Pjumptable (r: ireg) (labels: list label)

  | Ploopdo (count: ireg) (loopend: label)
  | Pgetn (n: int) (dst: ireg)
  | Psetn (n: int) (src: ireg)
  | Pwfxl (n: int) (src: ireg)
  | Pwfxm (n: int) (src: ireg)
  | Pldu (dst: ireg) (addr: ireg)
  | Plbzu (dst: ireg) (addr: ireg)
  | Plhzu (dst: ireg) (addr: ireg)
  | Plwzu (dst: ireg) (addr: ireg)
  | Pawait
  | Psleep
  | Pstop
  | Pbarrier
  | Pfence
  | Pdinval
  | Pdinvall (addr: ireg)
  | Pdtouchl (addr: ireg)
  | Piinval
  | Piinvals (addr: ireg)
  | Pitouchl (addr: ireg)
  | Pdzerol (addr: ireg)

  | Palclrd (dst: ireg) (addr: ireg)
  | Palclrw (dst: ireg) (addr: ireg)
  | Pclzll (rd rs: ireg)
  | Pclzw (rd rs: ireg)
  | Pctzll (rd rs: ireg)
  | Pctzw (rd rs: ireg)
  | Pstsud (rd rs1 rs2: ireg)
            
Loads
  | Plb (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load byte *)
  | Plbu (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load byte unsigned *)
  | Plh (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load half word *)
  | Plhu (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load half word unsigned *)
  | Plw (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load int32 *)
  | Plw_a (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load any32 *)
  | Pld (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load int64 *)
  | Pld_a (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (* load any64 *)
  | Pfls (trap: trapping_mode) (rd: freg) (ra: ireg) (ofs: addressing) (* load float *)
  | Pfld (trap: trapping_mode) (rd: freg) (ra: ireg) (ofs: addressing) (* load 64-bit float *)
  | Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (* load 2*64-bit *)
  | Plo (rs: gpreg_o) (ra: ireg) (ofs: addressing) (* load 4*64-bit *)

Stores
  | Psb (rs: ireg) (ra: ireg) (ofs: addressing) (* store byte *)
  | Psh (rs: ireg) (ra: ireg) (ofs: addressing) (* store half byte *)
  | Psw (rs: ireg) (ra: ireg) (ofs: addressing) (* store int32 *)
  | Psw_a (rs: ireg) (ra: ireg) (ofs: addressing) (* store any32 *)
  | Psd (rs: ireg) (ra: ireg) (ofs: addressing) (* store int64 *)
  | Psd_a (rs: ireg) (ra: ireg) (ofs: addressing) (* store any64 *)
  | Pfss (rs: freg) (ra: ireg) (ofs: addressing) (* store float *)
  | Pfsd (rs: freg) (ra: ireg) (ofs: addressing) (* store 64-bit float *)

  | Psq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (* store 2*64-bit *)
  | Pso (rs: gpreg_o) (ra: ireg) (ofs: addressing) (* store 2*64-bit *)

Arith RR
  | Pmv (rd rs: ireg) (* register move *)
  | Pnegw (rd rs: ireg) (* negate word *)
  | Pnegl (rd rs: ireg) (* negate long *)
  | Pcvtl2w (rd rs: ireg) (* Convert Long to Word *)
  | Psxwd (rd rs: ireg) (* Sign Extend Word to Double Word *)
  | Pzxwd (rd rs: ireg) (* Zero Extend Word to Double Word *)

  | Pextfz (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (* extract bitfields unsigned *)
  | Pextfs (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (* extract bitfields signed *)

  | Pextfzl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (* extract bitfields unsigned *)
  | Pextfsl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (* extract bitfields signed *)

  | Pinsf (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (* insert bitfield *)
  | Pinsfl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (* insert bitfield *)

  | Pfabsd (rd rs: ireg) (* float absolute double *)
  | Pfabsw (rd rs: ireg) (* float absolute word *)
  | Pfnegd (rd rs: ireg) (* float negate double *)
  | Pfnegw (rd rs: ireg) (* float negate word *)
  | Pfnarrowdw (rd rs: ireg) (* float narrow 64 -> 32 bits *)
  | Pfwidenlwd (rd rs: ireg) (* float widen 32 -> 64 bits *)
  | Pfloatwrnsz (rd rs: ireg) (* Floating Point Conversion from integer (32 -> 32) *)
  | Pfloatuwrnsz (rd rs: ireg) (* Floating Point Conversion from integer (u32 -> 32) *)
  | Pfloatudrnsz (rd rs: ireg) (* Floating Point Conversion from unsigned integer (64 bits) *)
  | Pfloatdrnsz (rd rs: ireg) (* Floating Point Conversion from integer (64 bits) *)

  | Pfixedwrzz (rd rs: ireg) (* Integer conversion from floating point *)
  | Pfixeduwrzz (rd rs: ireg) (* Integer conversion from floating point (f32 -> 32 bits unsigned *)
  | Pfixeddrzz (rd rs: ireg) (* Integer conversion from floating point (i64 -> 64 bits) *)
  | Pfixeddrzz_i32 (rd rs: ireg) (* Integer conversion from floating point (i32 -> f64) *)
  | Pfixedudrzz (rd rs: ireg) (* unsigned Integer conversion from floating point (u64 -> 64 bits) *)
  | Pfixedudrzz_i32 (rd rs: ireg) (* unsigned Integer conversion from floating point (u32 -> 64 bits) *)

  | Pfixedwrne (rd rs: ireg) (* Integer conversion from floating point *)
  | Pfixeduwrne (rd rs: ireg) (* Integer conversion from floating point (f32 -> 32 bits unsigned *)
  | Pfixeddrne (rd rs: ireg) (* Integer conversion from floating point (i64 -> 64 bits) *)
  | Pfixedudrne (rd rs: ireg) (* unsigned Integer conversion from floating point (u64 -> 64 bits) *)

Arith RI32
  | Pmake (rd: ireg) (imm: int) (* load immediate *)

Arith RI64
  | Pmakel (rd: ireg) (imm: int64) (* load immediate long *)

Arith RF32
  | Pmakefs (rd: ireg) (imm: float32)

Arith RF64
  | Pmakef (rd: ireg) (imm: float)

Arith RRR
  | Pcompw (it: itest) (rd rs1 rs2: ireg) (* comparison word *)
  | Pcompl (it: itest) (rd rs1 rs2: ireg) (* comparison long *)
  | Pfcompw (ft: ftest) (rd rs1 rs2: ireg) (* comparison float *)
  | Pfcompl (ft: ftest) (rd rs1 rs2: ireg) (* comparison float64 *)

  | Paddw (rd rs1 rs2: ireg) (* add word *)
  | Paddxw (shift : shift1_4) (rd rs1 rs2: ireg) (* add word *)
  | Psubw (rd rs1 rs2: ireg) (* sub word *)
  | Prevsubxw (shift : shift1_4) (rd rs1 rs2: ireg) (* add word *)
  | Pmulw (rd rs1 rs2: ireg) (* mul word *)
  | Pandw (rd rs1 rs2: ireg) (* and word *)
  | Pnandw (rd rs1 rs2: ireg) (* nand word *)
  | Porw (rd rs1 rs2: ireg) (* or word *)
  | Pnorw (rd rs1 rs2: ireg) (* nor word *)
  | Pxorw (rd rs1 rs2: ireg) (* xor word *)
  | Pnxorw (rd rs1 rs2: ireg) (* xor word *)
  | Pandnw (rd rs1 rs2: ireg) (* andn word *)
  | Pornw (rd rs1 rs2: ireg) (* orn word *)
  | Psraw (rd rs1 rs2: ireg) (* shift right arithmetic word *)
  | Psrxw (rd rs1 rs2: ireg) (* shift right arithmetic word round to 0 *)
  | Psrlw (rd rs1 rs2: ireg) (* shift right logical word *)
  | Psllw (rd rs1 rs2: ireg) (* shift left logical word *)
  | Pmaddw (rd rs1 rs2: ireg) (* multiply-add words *)
  | Pmsubw (rd rs1 rs2: ireg) (* multiply-add words *)
  | Pfmaddfw (rd rs1 rs2: ireg) (* float fused multiply-add words *)
  | Pfmsubfw (rd rs1 rs2: ireg) (* float fused multiply-subtract words *)
  | Pfmaddfl (rd rs1 rs2: ireg) (* float fused multiply-add longs *)
  | Pfmsubfl (rd rs1 rs2: ireg) (* float fused multiply-subtract longs *)

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

  | Pfaddd (rd rs1 rs2: ireg) (* Float addition double *)
  | Pfaddw (rd rs1 rs2: ireg) (* Float addition word *)
  | Pfsbfd (rd rs1 rs2: ireg) (* Float sub double *)
  | Pfsbfw (rd rs1 rs2: ireg) (* Float sub word *)
  | Pfmuld (rd rs1 rs2: ireg) (* Float mul double *)
  | Pfmulw (rd rs1 rs2: ireg) (* Float mul word *)
  | Pfmind (rd rs1 rs2: ireg) (* Float min double *)
  | Pfminw (rd rs1 rs2: ireg) (* Float min word *)
  | Pfmaxd (rd rs1 rs2: ireg) (* Float max double *)
  | Pfmaxw (rd rs1 rs2: ireg) (* Float max word *)
  | Pfinvw (rd rs1: ireg) (* Float invert word *)

  | Pabdw (rd rs1 rs2: ireg) (* Absolute difference word *)
  | Pabdl (rd rs1 rs2: ireg) (* Absolute difference long *)
                        
Arith RRI32
  | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (* comparison imm word *)

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

Arith RRI64
  | Pcompil (it: itest) (rd rs: ireg) (imm: int64) (* comparison imm long *)
  | Paddil (rd rs: ireg) (imm: int64) (* add immediate long *)
  | Paddxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (* add immediate long *)
  | Prevsubil (rd rs: ireg) (imm: int64) (* subtract imm long *)
  | Prevsubxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (* subtract imm long *)
  | Pmulil (rd rs: ireg) (imm: int64) (* add immediate long *)
  | Pandil (rd rs: ireg) (imm: int64) (* and immediate long *)
  | Pnandil (rd rs: ireg) (imm: int64) (* and immediate long *)
  | Poril (rd rs: ireg) (imm: int64) (* or immediate long *)
  | Pnoril (rd rs: ireg) (imm: int64) (* and immediate long *)
  | Pxoril (rd rs: ireg) (imm: int64) (* xor immediate long *)
  | Pnxoril (rd rs: ireg) (imm: int64) (* xor immediate long *)
  | Pandnil (rd rs: ireg) (imm: int64) (* andn long *)
  | Pornil (rd rs: ireg) (imm: int64) (* orn long *)
  | Pmaddil (rd rs: ireg) (imm: int64) (* multiply add imm long *)
  | Pcmove (bt: btest) (rcond rd rs : ireg)
  | Pcmoveu (bt: btest) (rcond rd rs : ireg)
  | Pcmoveiw (bt: btest) (rcond rd : ireg) (imm: int)
  | Pcmoveuiw (bt: btest) (rcond rd : ireg) (imm: int)
  | Pcmoveil (bt: btest) (rcond rd : ireg) (imm: int64)
  | Pcmoveuil (bt: btest) (rcond rd : ireg) (imm: int64)
  | Pabdil (rd rs : ireg) (imm: int64) (* Absolute difference long *)
.

Correspondance between Asmblock and Asm

Definition control_to_instruction (c: control) :=
  match c with
  | PExpand (Asmvliw.Pbuiltin ef args res) => Pbuiltin ef args res
  | PCtlFlow Asmvliw.Pret => Pret
  | PCtlFlow (Asmvliw.Pcall l) => Pcall l
  | PCtlFlow (Asmvliw.Picall r) => Picall r
  | PCtlFlow (Asmvliw.Pgoto l) => Pgoto l
  | PCtlFlow (Asmvliw.Pigoto l) => Pigoto l
  | PCtlFlow (Asmvliw.Pj_l l) => Pj_l l
  | PCtlFlow (Asmvliw.Pcb bt r l) => Pcb bt r l
  | PCtlFlow (Asmvliw.Pcbu bt r l) => Pcbu bt r l
  | PCtlFlow (Asmvliw.Pjumptable r label) => Pjumptable r label
  end.

Definition basic_to_instruction (b: basic) :=
  match b with
Special basics
  | Asmvliw.Pget rd rs => Pget rd rs
  | Asmvliw.Pset rd rs => Pset rd rs
  | Asmvliw.Pnop => Pnop
  | Asmvliw.Pallocframe sz pos => Pallocframe sz pos
  | Asmvliw.Pfreeframe sz pos => Pfreeframe sz pos

PArith basics
  | PArithR (Asmvliw.Ploadsymbol id ofs) r => Ploadsymbol r id ofs

  | PArithRR Asmvliw.Pmv rd rs => Pmv rd rs
  | PArithRR Asmvliw.Pnegw rd rs => Pnegw rd rs
  | PArithRR Asmvliw.Pnegl rd rs => Pnegl rd rs
  | PArithRR Asmvliw.Pcvtl2w rd rs => Pcvtl2w rd rs
  | PArithRR Asmvliw.Psxwd rd rs => Psxwd rd rs
  | PArithRR Asmvliw.Pzxwd rd rs => Pzxwd rd rs
  | PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start
  | PArithRR (Asmvliw.Pextfs stop start) rd rs => Pextfs rd rs stop start
  | PArithRR (Asmvliw.Pextfzl stop start) rd rs => Pextfzl rd rs stop start
  | PArithRR (Asmvliw.Pextfsl stop start) rd rs => Pextfsl rd rs stop start
  | PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs
  | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs
  | PArithRR Asmvliw.Pfnegd rd rs => Pfnegd rd rs
  | PArithRR Asmvliw.Pfnegw rd rs => Pfnegw rd rs
  | PArithRR Asmvliw.Pfinvw rd rs => Pfinvw rd rs
  | PArithRR Asmvliw.Pfnarrowdw rd rs => Pfnarrowdw rd rs
  | PArithRR Asmvliw.Pfwidenlwd rd rs => Pfwidenlwd rd rs
  | PArithRR Asmvliw.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs
  | PArithRR Asmvliw.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
  | PArithRR Asmvliw.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
  | PArithRR Asmvliw.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
  | PArithRR Asmvliw.Pfixedwrzz rd rs => Pfixedwrzz rd rs
  | PArithRR Asmvliw.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
  | PArithRR Asmvliw.Pfixeddrzz rd rs => Pfixeddrzz rd rs
  | PArithRR Asmvliw.Pfixedudrzz rd rs => Pfixedudrzz rd rs
  | PArithRR Asmvliw.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs
  | PArithRR Asmvliw.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs
  | PArithRR Asmvliw.Pfixedwrne rd rs => Pfixedwrne rd rs
  | PArithRR Asmvliw.Pfixeduwrne rd rs => Pfixeduwrne rd rs
  | PArithRR Asmvliw.Pfixeddrne rd rs => Pfixeddrne rd rs
  | PArithRR Asmvliw.Pfixedudrne rd rs => Pfixedudrne rd rs

  | PArithRI32 Asmvliw.Pmake rd imm => Pmake rd imm

  | PArithRI64 Asmvliw.Pmakel rd imm => Pmakel rd imm

  | PArithRF32 Asmvliw.Pmakefs rd imm => Pmakefs rd imm

  | PArithRF64 Asmvliw.Pmakef rd imm => Pmakef rd imm

  | PArithRRR (Asmvliw.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2
  | PArithRRR (Asmvliw.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2
  | PArithRRR (Asmvliw.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2
  | PArithRRR (Asmvliw.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2
  | PArithRRR Asmvliw.Paddw rd rs1 rs2 => Paddw rd rs1 rs2
  | PArithRRR (Asmvliw.Paddxw shift) rd rs1 rs2 => Paddxw shift rd rs1 rs2
  | PArithRRR Asmvliw.Psubw rd rs1 rs2 => Psubw rd rs1 rs2
  | PArithRRR (Asmvliw.Prevsubxw shift) rd rs1 rs2 => Prevsubxw shift rd rs1 rs2
  | PArithRRR Asmvliw.Pmulw rd rs1 rs2 => Pmulw rd rs1 rs2
  | PArithRRR Asmvliw.Pandw rd rs1 rs2 => Pandw rd rs1 rs2
  | PArithRRR Asmvliw.Pnandw rd rs1 rs2 => Pnandw rd rs1 rs2
  | PArithRRR Asmvliw.Porw rd rs1 rs2 => Porw rd rs1 rs2
  | PArithRRR Asmvliw.Pnorw rd rs1 rs2 => Pnorw rd rs1 rs2
  | PArithRRR Asmvliw.Pxorw rd rs1 rs2 => Pxorw rd rs1 rs2
  | PArithRRR Asmvliw.Pnxorw rd rs1 rs2 => Pnxorw rd rs1 rs2
  | PArithRRR Asmvliw.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
  | PArithRRR Asmvliw.Pornw rd rs1 rs2 => Pornw rd rs1 rs2
  | PArithRRR Asmvliw.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
  | PArithRRR Asmvliw.Psrxw rd rs1 rs2 => Psrxw rd rs1 rs2
  | PArithRRR Asmvliw.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
  | PArithRRR Asmvliw.Psllw rd rs1 rs2 => Psllw rd rs1 rs2

  | PArithRRR Asmvliw.Paddl rd rs1 rs2 => Paddl rd rs1 rs2
  | PArithRRR (Asmvliw.Paddxl shift) rd rs1 rs2 => Paddxl shift rd rs1 rs2
  | PArithRRR Asmvliw.Psubl rd rs1 rs2 => Psubl rd rs1 rs2
  | PArithRRR (Asmvliw.Prevsubxl shift) rd rs1 rs2 => Prevsubxl shift rd rs1 rs2
  | PArithRRR Asmvliw.Pandl rd rs1 rs2 => Pandl rd rs1 rs2
  | PArithRRR Asmvliw.Pnandl rd rs1 rs2 => Pnandl rd rs1 rs2
  | PArithRRR Asmvliw.Porl rd rs1 rs2 => Porl rd rs1 rs2
  | PArithRRR Asmvliw.Pnorl rd rs1 rs2 => Pnorl rd rs1 rs2
  | PArithRRR Asmvliw.Pxorl rd rs1 rs2 => Pxorl rd rs1 rs2
  | PArithRRR Asmvliw.Pnxorl rd rs1 rs2 => Pnxorl rd rs1 rs2
  | PArithRRR Asmvliw.Pandnl rd rs1 rs2 => Pandnl rd rs1 rs2
  | PArithRRR Asmvliw.Pornl rd rs1 rs2 => Pornl rd rs1 rs2
  | PArithRRR Asmvliw.Pmull rd rs1 rs2 => Pmull rd rs1 rs2
  | PArithRRR Asmvliw.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
  | PArithRRR Asmvliw.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
  | PArithRRR Asmvliw.Psral rd rs1 rs2 => Psral rd rs1 rs2
  | PArithRRR Asmvliw.Psrxl rd rs1 rs2 => Psrxl rd rs1 rs2

  | PArithRRR Asmvliw.Pfaddd rd rs1 rs2 => Pfaddd rd rs1 rs2
  | PArithRRR Asmvliw.Pfaddw rd rs1 rs2 => Pfaddw rd rs1 rs2
  | PArithRRR Asmvliw.Pfsbfd rd rs1 rs2 => Pfsbfd rd rs1 rs2
  | PArithRRR Asmvliw.Pfsbfw rd rs1 rs2 => Pfsbfw rd rs1 rs2
  | PArithRRR Asmvliw.Pfmuld rd rs1 rs2 => Pfmuld rd rs1 rs2
  | PArithRRR Asmvliw.Pfmulw rd rs1 rs2 => Pfmulw rd rs1 rs2
  | PArithRRR Asmvliw.Pfmind rd rs1 rs2 => Pfmind rd rs1 rs2
  | PArithRRR Asmvliw.Pfminw rd rs1 rs2 => Pfminw rd rs1 rs2
  | PArithRRR Asmvliw.Pfmaxd rd rs1 rs2 => Pfmaxd rd rs1 rs2
  | PArithRRR Asmvliw.Pfmaxw rd rs1 rs2 => Pfmaxw rd rs1 rs2

  | PArithRRR Asmvliw.Pabdw rd rs1 rs2 => Pabdw rd rs1 rs2
  | PArithRRR Asmvliw.Pabdl rd rs1 rs2 => Pabdl rd rs1 rs2

  | PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
  | PArithRRI32 Asmvliw.Paddiw rd rs imm => Paddiw rd rs imm
  | PArithRRI32 (Asmvliw.Paddxiw shift) rd rs imm => Paddxiw shift rd rs imm
  | PArithRRI32 Asmvliw.Prevsubiw rd rs imm => Prevsubiw rd rs imm
  | PArithRRI32 (Asmvliw.Prevsubxiw shift) rd rs imm => Prevsubxiw shift rd rs imm
  | PArithRRI32 Asmvliw.Pmuliw rd rs imm => Pmuliw rd rs imm
  | PArithRRI32 Asmvliw.Pandiw rd rs imm => Pandiw rd rs imm
  | PArithRRI32 Asmvliw.Pnandiw rd rs imm => Pnandiw rd rs imm
  | PArithRRI32 Asmvliw.Poriw rd rs imm => Poriw rd rs imm
  | PArithRRI32 Asmvliw.Pnoriw rd rs imm => Pnoriw rd rs imm
  | PArithRRI32 Asmvliw.Pxoriw rd rs imm => Pxoriw rd rs imm
  | PArithRRI32 Asmvliw.Pnxoriw rd rs imm => Pnxoriw rd rs imm
  | PArithRRI32 Asmvliw.Pandniw rd rs imm => Pandniw rd rs imm
  | PArithRRI32 Asmvliw.Porniw rd rs imm => Porniw rd rs imm
  | PArithRRI32 Asmvliw.Psraiw rd rs imm => Psraiw rd rs imm
  | PArithRRI32 Asmvliw.Psrxiw rd rs imm => Psrxiw rd rs imm
  | PArithRRI32 Asmvliw.Psrliw rd rs imm => Psrliw rd rs imm
  | PArithRRI32 Asmvliw.Pslliw rd rs imm => Pslliw rd rs imm
  | PArithRRI32 Asmvliw.Proriw rd rs imm => Proriw rd rs imm
  | PArithRRI32 Asmvliw.Psllil rd rs imm => Psllil rd rs imm
  | PArithRRI32 Asmvliw.Psrlil rd rs imm => Psrlil rd rs imm
  | PArithRRI32 Asmvliw.Psrxil rd rs imm => Psrxil rd rs imm
  | PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm

  | PArithRRI32 Asmvliw.Pabdiw rd rs imm => Pabdiw rd rs imm

  | PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm
  | PArithRRI64 Asmvliw.Paddil rd rs imm => Paddil rd rs imm
  | PArithRRI64 (Asmvliw.Paddxil shift) rd rs imm => Paddxil shift rd rs imm
  | PArithRRI64 Asmvliw.Prevsubil rd rs imm => Prevsubil rd rs imm
  | PArithRRI64 (Asmvliw.Prevsubxil shift) rd rs imm => Prevsubxil shift rd rs imm
  | PArithRRI64 Asmvliw.Pmulil rd rs imm => Pmulil rd rs imm
  | PArithRRI64 Asmvliw.Pandil rd rs imm => Pandil rd rs imm
  | PArithRRI64 Asmvliw.Pnandil rd rs imm => Pnandil rd rs imm
  | PArithRRI64 Asmvliw.Poril rd rs imm => Poril rd rs imm
  | PArithRRI64 Asmvliw.Pnoril rd rs imm => Pnoril rd rs imm
  | PArithRRI64 Asmvliw.Pxoril rd rs imm => Pxoril rd rs imm
  | PArithRRI64 Asmvliw.Pnxoril rd rs imm => Pnxoril rd rs imm
  | PArithRRI64 Asmvliw.Pandnil rd rs imm => Pandnil rd rs imm
  | PArithRRI64 Asmvliw.Pornil rd rs imm => Pornil rd rs imm

  | PArithRRI64 Asmvliw.Pabdil rd rs imm => Pabdil rd rs imm

ARRR
  | PArithARRR Asmvliw.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
  | PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
  | PArithARRR Asmvliw.Pmsubw rd rs1 rs2 => Pmsubw rd rs1 rs2
  | PArithARRR Asmvliw.Pmsubl rd rs1 rs2 => Pmsubl rd rs1 rs2
  | PArithARRR Asmvliw.Pfmaddfw rd rs1 rs2 => Pfmaddfw rd rs1 rs2
  | PArithARRR Asmvliw.Pfmaddfl rd rs1 rs2 => Pfmaddfl rd rs1 rs2
  | PArithARRR Asmvliw.Pfmsubfw rd rs1 rs2 => Pfmsubfw rd rs1 rs2
  | PArithARRR Asmvliw.Pfmsubfl rd rs1 rs2 => Pfmsubfl rd rs1 rs2
  | PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
  | PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2

ARR
  | PArithARR (Asmvliw.Pinsf stop start) rd rs => Pinsf rd rs stop start
  | PArithARR (Asmvliw.Pinsfl stop start) rd rs => Pinsfl rd rs stop start

ARRI32
  | PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
  | PArithARRI32 (Asmvliw.Pcmoveiw cond) rd rs1 imm => Pcmoveiw cond rd rs1 imm
  | PArithARRI32 (Asmvliw.Pcmoveuiw cond) rd rs1 imm => Pcmoveuiw cond rd rs1 imm

ARRI64
  | PArithARRI64 Asmvliw.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
  | PArithARRI64 (Asmvliw.Pcmoveil cond) rd rs1 imm => Pcmoveil cond rd rs1 imm
  | PArithARRI64 (Asmvliw.Pcmoveuil cond) rd rs1 imm => Pcmoveuil cond rd rs1 imm
Load
  | PLoadRRO trap Asmvliw.Plb rd ra ofs => Plb trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Plbu rd ra ofs => Plbu trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Plh rd ra ofs => Plh trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Plhu rd ra ofs => Plhu trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Plw rd ra ofs => Plw trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Plw_a rd ra ofs => Plw_a trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Pld rd ra ofs => Pld trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Pld_a rd ra ofs => Pld_a trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Pfls rd ra ofs => Pfls trap rd ra (AOff ofs)
  | PLoadRRO trap Asmvliw.Pfld rd ra ofs => Pfld trap rd ra (AOff ofs)

  | PLoadQRRO qrs ra ofs => Plq qrs ra (AOff ofs)
  | PLoadORRO qrs ra ofs => Plo qrs ra (AOff ofs)

  | PLoadRRR trap Asmvliw.Plb rd ra ro => Plb trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Plbu rd ra ro => Plbu trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Plh rd ra ro => Plh trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Plhu rd ra ro => Plhu trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Plw rd ra ro => Plw trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Plw_a rd ra ro => Plw_a trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Pld rd ra ro => Pld trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Pld_a rd ra ro => Pld_a trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Pfls rd ra ro => Pfls trap rd ra (AReg ro)
  | PLoadRRR trap Asmvliw.Pfld rd ra ro => Pfld trap rd ra (AReg ro)

  | PLoadRRRXS trap Asmvliw.Plb rd ra ro => Plb trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Plbu rd ra ro => Plbu trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Plh rd ra ro => Plh trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Plhu rd ra ro => Plhu trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Plw rd ra ro => Plw trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Plw_a rd ra ro => Plw_a trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Pld rd ra ro => Pld trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Pld_a rd ra ro => Pld_a trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Pfls rd ra ro => Pfls trap rd ra (ARegXS ro)
  | PLoadRRRXS trap Asmvliw.Pfld rd ra ro => Pfld trap rd ra (ARegXS ro)

Store
  | PStoreRRO Asmvliw.Psb rd ra ofs => Psb rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Psh rd ra ofs => Psh rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Psw rd ra ofs => Psw rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Psw_a rd ra ofs => Psw_a rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Psd rd ra ofs => Psd rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Psd_a rd ra ofs => Psd_a rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Pfss rd ra ofs => Pfss rd ra (AOff ofs)
  | PStoreRRO Asmvliw.Pfsd rd ra ofs => Pfsd rd ra (AOff ofs)

  | PStoreRRR Asmvliw.Psb rd ra ro => Psb rd ra (AReg ro)
  | PStoreRRR Asmvliw.Psh rd ra ro => Psh rd ra (AReg ro)
  | PStoreRRR Asmvliw.Psw rd ra ro => Psw rd ra (AReg ro)
  | PStoreRRR Asmvliw.Psw_a rd ra ro => Psw_a rd ra (AReg ro)
  | PStoreRRR Asmvliw.Psd rd ra ro => Psd rd ra (AReg ro)
  | PStoreRRR Asmvliw.Psd_a rd ra ro => Psd_a rd ra (AReg ro)
  | PStoreRRR Asmvliw.Pfss rd ra ro => Pfss rd ra (AReg ro)
  | PStoreRRR Asmvliw.Pfsd rd ra ro => Pfsd rd ra (AReg ro)

  | PStoreRRRXS Asmvliw.Psb rd ra ro => Psb rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Psh rd ra ro => Psh rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Psw rd ra ro => Psw rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Psw_a rd ra ro => Psw_a rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Psd rd ra ro => Psd rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Psd_a rd ra ro => Psd_a rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro)
  | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro)

  | PStoreQRRO qrs ra ofs => Psq qrs ra (AOff ofs)
  | PStoreORRO qrs ra ofs => Pso qrs ra (AOff ofs)
  end.

Semantics (given through the existence of well-formed VLIW program)


Section RELSEM.

Definition code := list instruction.

Fixpoint unfold_label (ll: list label) :=
  match ll with
  | nil => nil
  | l :: ll => Plabel l :: unfold_label ll
  end.

Fixpoint unfold_body (lb: list basic) :=
  match lb with
  | nil => nil
  | b :: lb => basic_to_instruction b :: unfold_body lb
  end.

Definition unfold_exit (oc: option control) :=
  match oc with
  | None => nil
  | Some c => control_to_instruction c :: nil
  end.

Definition unfold_bblock (b: bblock) := unfold_label (header b) ++
  (match (body b), (exit b) with
   | (((Asmvliw.Pfreeframe _ _ | Asmvliw.Pallocframe _ _)::nil) as bo), None =>
     unfold_body bo
   | bo, ex => unfold_body bo ++ unfold_exit ex ++ Psemi :: nil
  end).

Fixpoint unfold (lb: bblocks) :=
  match lb with
  | nil => nil
  | b :: lb => (unfold_bblock b) ++ unfold lb
  end.

Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks; fn_code: code;
                                       correct: unfold fn_blocks = fn_code }.

Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
Definition genv := Genv.t fundef unit.

Definition function_proj (f: function) := Asmvliw.mkfunction (fn_sig f) (fn_blocks f).

Definition fundef_proj (fu: fundef) : Asmvliw.fundef :=
  match fu with
  | Internal f => Internal (function_proj f)
  | External ef => External ef
  end.

Definition globdef_proj (gd: globdef fundef unit) : globdef Asmvliw.fundef unit :=
  match gd with
  | Gfun f => Gfun (fundef_proj f)
  | Gvar gu => Gvar gu
  end.

Program Definition genv_trans (ge: genv) : Asmvliw.genv :=
  {| Genv.genv_public := Genv.genv_public ge;
      Genv.genv_symb := Genv.genv_symb ge;
      Genv.genv_defs := PTree.map1 globdef_proj (Genv.genv_defs ge);
      Genv.genv_next := Genv.genv_next ge |}.
Next Obligation.
  destruct ge. cbn in *. eauto.
Qed.
Next Obligation.
  destruct ge; cbn in *.
  rewrite PTree.gmap1 in H.
  destruct (genv_defs ! b) eqn:GEN.
  - eauto.
  - discriminate.
Qed.
Next Obligation.
  destruct ge; cbn in *.
  eauto.
Qed.
Fixpoint prog_defs_proj (l: list (ident * globdef fundef unit))
                          : list (ident * globdef Asmvliw.fundef unit) :=
  match l with
  | nil => nil
  | (i, gd) :: l => (i, globdef_proj gd) :: prog_defs_proj l
  end.

Definition program_proj (p: program) : Asmvliw.program :=
  {| prog_defs := prog_defs_proj (prog_defs p);
      prog_public := prog_public p;
      prog_main := prog_main p
  |}.

End RELSEM.

Definition semantics (p: program) := Asmvliw.semantics (program_proj p).

Determinacy of the Asm semantics.

Lemma semantics_determinate: forall p, determinate (semantics p).
Proof.
  intros. apply semantics_determinate.
Qed.

transf_program

Program Definition transf_function (f: Asmvliw.function) : function :=
     {| fn_sig := Asmvliw.fn_sig f; fn_blocks := Asmvliw.fn_blocks f;
        fn_code := unfold (Asmvliw.fn_blocks f) |}.

Lemma transf_function_proj: forall f, function_proj (transf_function f) = f.
Proof.
  intros f. destruct f as [sig blks]. unfold function_proj. cbn. auto.
Qed.

Definition transf_fundef : Asmvliw.fundef -> fundef := AST.transf_fundef transf_function.

Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f.
Proof.
  intros f. destruct f as [f|e]; cbn; auto.
  rewrite transf_function_proj. auto.
Qed.

Definition transf_program : Asmvliw.program -> program := transform_program transf_fundef.

Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
  prog_defs p1 = prog_defs p2 ->
  prog_public p1 = prog_public p2 ->
  prog_main p1 = prog_main p2 ->
  p1 = p2.
Proof.
  intros. destruct p1. destruct p2. cbn in *. subst. auto.
Qed.

Lemma transf_program_proj: forall p, program_proj (transf_program p) = p.
Proof.
  intros p. destruct p as [defs pub main]. unfold program_proj. cbn.
  apply program_equals; cbn; auto.
  induction defs.
  - cbn; auto.
  - cbn. rewrite IHdefs.
    destruct a as [id gd]; cbn.
    destruct gd as [f|v]; cbn; auto.
    rewrite transf_fundef_proj. auto.
Qed.

Definition match_prog (p: Asmvliw.program) (tp: program) :=
  match_program (fun _ f tf => tf = transf_fundef f) eq p tp.

Lemma transf_program_match:
  forall p tp, transf_program p = tp -> match_prog p tp.
Proof.
  intros. rewrite <- H. eapply match_transform_program; eauto.
Qed.

Lemma cons_extract {A: Type} : forall (l: list A) a b, a = b -> a::l = b::l.
Proof.
  intros. congruence.
Qed.

Lemma match_program_transf:
  forall p tp, match_prog p tp -> transf_program p = tp.
Proof.
  intros p tp H. inversion_clear H. inv H1.
  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. cbn in *.
  subst. unfold transf_program. unfold transform_program. cbn.
  apply program_equals; cbn; auto.
  induction H0; cbn; auto.
  rewrite IHlist_forall2. apply cons_extract.
  destruct a1 as [ida gda]. destruct b1 as [idb gdb].
  cbn in *.
  inv H. inv H2.
  - cbn in *. subst. auto.
  - cbn in *. subst. inv H. auto.
Qed.

Section PRESERVATION.

Variable prog: Asmvliw.program.
Variable tprog: program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Definition match_states (s1 s2: state) := s1 = s2.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).


Theorem transf_program_correct:
  forward_simulation (Asmvliw.semantics prog) (semantics tprog).
Proof.
  pose proof (match_program_transf prog tprog TRANSF) as TR.
  subst. unfold semantics. rewrite transf_program_proj.

  eapply forward_simulation_step with (match_states := match_states); cbn; auto.
  - intros. exists s1. split; auto. congruence.
  - intros. inv H. auto.
  - intros. exists s1'. inv H0. split; auto. congruence.
Qed.

End PRESERVATION.