diff options
Diffstat (limited to 'riscV/Asm.v')
| -rw-r--r-- | riscV/Asm.v | 36 |
1 files changed, 24 insertions, 12 deletions
diff --git a/riscV/Asm.v b/riscV/Asm.v index a47573a2..c80c6cc2 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -30,6 +30,7 @@ Require Import Smallstep. Require Import Locations. Require Stacklayout. Require Import Conventions. +Require ExtValues. (** * Abstract syntax *) @@ -62,10 +63,10 @@ Inductive freg: Type := | F24: freg | F25: freg | F26: freg | F27: freg | F28: freg | F29: freg | F30: freg | F31: freg. -Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. +Definition ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. -Lemma ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}. +Definition ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}. Proof. decide equality. apply ireg_eq. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. @@ -255,10 +256,10 @@ Inductive instruction : Type := (* floating point register move *) | Pfmv (rd: freg) (rs: freg) (**r move *) - | Pfmvxs (rd: ireg) (rs: freg) (**r move FP single to integer register *) - | Pfmvsx (rd: freg) (rs: ireg) (**r move integer register to FP single *) - | Pfmvxd (rd: ireg) (rs: freg) (**r move FP double to integer register *) - | Pfmvdx (rd: freg) (rs: ireg) (**r move integer register to FP double *) + | Pfmvxs (rd: ireg) (rs: freg) (**r bitwise move FP single to integer register *) + | Pfmvxd (rd: ireg) (rs: freg) (**r bitwise move FP double to integer register *) + | Pfmvsx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP single *) + | Pfmvdx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP double*) (* 32-bit (single-precision) floating point *) | Pfls (rd: freg) (ra: ireg) (ofs: offset) (**r load float *) @@ -347,6 +348,7 @@ Inductive instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) + | Pselectl (rd: ireg) (rb: ireg0) (rt: ireg0) (rf: ireg0) | Pnop : instruction. (**r nop instruction *) @@ -920,6 +922,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.floatofsingle rs#s))) m | Pfcvtsd d s => Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) m + + | Pfmvxs d s => + Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m + | Pfmvxd d s => + Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m + + | Pfmvsx d s => + Next (nextinstr (rs#d <- (ExtValues.single_of_bits rs#s))) m + | Pfmvdx d s => + Next (nextinstr (rs#d <- (ExtValues.float_of_bits rs#s))) m + (** Pseudo-instructions *) | Pallocframe sz pos => @@ -942,6 +955,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end end + | Pselectl rd rb rt rf => + Next (nextinstr (rs#rd <- (ExtValues.select01_long + (rs###rb) (rs###rt) (rs###rf))) + #X31 <- Vundef) m | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol rd s ofs => @@ -965,16 +982,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pbuiltin ef args res => Stuck (**r treated specially below *) + | Pnop => Next (nextinstr rs) m (**r Pnop is used by an oracle during expansion *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) | Pfence - | Pfmvxs _ _ - | Pfmvsx _ _ - | Pfmvxd _ _ - | Pfmvdx _ _ - | Pfmins _ _ _ | Pfmaxs _ _ _ | Pfsqrts _ _ @@ -990,7 +1003,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfmsubd _ _ _ _ | Pfnmaddd _ _ _ _ | Pfnmsubd _ _ _ _ - | Pnop => Stuck end. |