diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 10:21:17 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 10:21:17 +0100 |
| commit | d2159e300b2d5e017a3144c747d34949b2ff2769 (patch) | |
| tree | 2186636bc3f2e85b5effd19f9e7c23f4183545aa /riscV/Asm.v | |
| parent | e0f1a90c2dcf7c43137064470ce4b12368b8435d (diff) | |
| download | compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.tar.gz compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.zip | |
begin implementing select
Diffstat (limited to 'riscV/Asm.v')
| -rw-r--r-- | riscV/Asm.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/riscV/Asm.v b/riscV/Asm.v index d1946a06..9a4b2a57 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -63,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}. @@ -348,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 *) @@ -954,6 +955,9 @@ 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)))) m | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol rd s ofs => |