diff options
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 85e5ed3a..5f109224 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -278,7 +278,8 @@ Inductive instruction: Type := | Pstrs (rs: freg) (a: addressing) (**r store float32 *) | Pstrd (rs: freg) (a: addressing) (**r store float64 *) | Pstrd_a (rs: freg) (a: addressing) (**r store float64 as any64 *) - (* TODO *) + | Pstps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float32 *) + | Pstpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float64 *) (** Floating-point move *) | Pfmov (rd r1: freg) | Pfmovimms (rd: freg) (f: float32) (**r load float32 constant *) @@ -1275,10 +1276,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m | Pldpd rd1 rd2 chk1 chk2 a => exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m - (* TODO | Pstps rs1 rs2 chk1 chk2 a => + | Pstps rs1 rs2 chk1 chk2 a => exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m | Pstpd rs1 rs2 chk1 chk2 a => - exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m *) + exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m | Pnop => Next (nextinstr rs) m (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) |