diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 08:01:15 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 08:01:15 +0200 |
| commit | 10963816f7f909e58afb0b12cc77c84f7f9c8b94 (patch) | |
| tree | b4a23165cf7b2eb92300f0da7b41f0e446a2b911 /mppa_k1c/Asm.v | |
| parent | 36d9f605478abac2f2fa15ecace6722863263bf3 (diff) | |
| download | compcert-kvx-10963816f7f909e58afb0b12cc77c84f7f9c8b94.tar.gz compcert-kvx-10963816f7f909e58afb0b12cc77c84f7f9c8b94.zip | |
big proofs for so / lo
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 70d39168..b928a48e 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -113,7 +113,8 @@ Inductive instruction : Type := | Pld_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any64 *)
| Pfls (rd: freg) (ra: ireg) (ofs: addressing) (**r load float *)
| Pfld (rd: freg) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
- | Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
+ | Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r load 2*64-bit *)
+ | Plo (rs: gpreg_o) (ra: ireg) (ofs: addressing) (**r load 4*64-bit *)
(** Stores **)
| Psb (rs: ireg) (ra: ireg) (ofs: addressing) (**r store byte *)
@@ -125,7 +126,8 @@ Inductive instruction : Type := | Pfss (rs: freg) (ra: ireg) (ofs: addressing) (**r store float *)
| Pfsd (rs: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
- | Psq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
+ | Psq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r store 2*64-bit *)
+ | Pso (rs: gpreg_o) (ra: ireg) (ofs: addressing) (**r store 2*64-bit *)
(** Arith RR *)
| Pmv (rd rs: ireg) (**r register move *)
@@ -438,6 +440,7 @@ Definition basic_to_instruction (b: basic) := | PLoadRRO Asmvliw.Pfld rd ra ofs => Pfld rd ra (AOff ofs)
| PLoadQRRO qrs ra ofs => Plq qrs ra (AOff ofs)
+ | PLoadORRO qrs ra ofs => Plo qrs ra (AOff ofs)
| PLoadRRR Asmvliw.Plb rd ra ro => Plb rd ra (AReg ro)
| PLoadRRR Asmvliw.Plbu rd ra ro => Plbu rd ra (AReg ro)
@@ -490,6 +493,7 @@ Definition basic_to_instruction (b: basic) := | 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.
Section RELSEM.
|