diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-28 14:20:03 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-28 14:20:03 +0200 |
| commit | cb3dc9a89d66741f4452becaf51d03a656e8e150 (patch) | |
| tree | dcfaeb8ab12b5539609d58d22ef88592ed8728cf /mppa_k1c/Asm.v | |
| parent | 087335c6b4a80aedb65562ce7c9cda30ebb13f37 (diff) | |
| parent | ac205c117a809aa40132f4184d04371e0e467b6c (diff) | |
| download | compcert-kvx-cb3dc9a89d66741f4452becaf51d03a656e8e150.tar.gz compcert-kvx-cb3dc9a89d66741f4452becaf51d03a656e8e150.zip | |
Merge remote-tracking branch 'origin/mppa-bitfields' into mppa-work
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 609bf93e..f1ccc126 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -137,6 +137,9 @@ Inductive instruction : Type := | Pextfzl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)
| Pextfsl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)
+ | Pinsf (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r insert bitfield *)
+ | Pinsfl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r insert bitfield *)
+
| Pfabsd (rd rs: ireg) (**r float absolute double *)
| Pfabsw (rd rs: ireg) (**r float absolute word *)
| Pfnegd (rd rs: ireg) (**r float negate double *)
@@ -404,6 +407,10 @@ Definition basic_to_instruction (b: basic) := | 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
|