From 8781c27a16463fd8f83a9c6eaba7b76846bd296c Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 20 Jan 2021 16:46:52 +0100
Subject: Adding fp loads pair

---
 aarch64/Asm.v | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

(limited to 'aarch64/Asm.v')

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index dc1f025f..85e5ed3a 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -201,8 +201,8 @@ Inductive instruction: Type :=
   | Pstrx_a (rs: ireg) (a: addressing)                                (**r store int64 as any64 *)
   | Pstrb (rs: ireg) (a: addressing)                                  (**r store int8 *)
   | Pstrh (rs: ireg) (a: addressing)                                  (**r store int16 *)
-  | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)                              (**r store two int64 *)
-  | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)                              (**r store two int64 *)
+  | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two int64 *)
+  | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing)   (**r store two int64 *)
   (** Integer arithmetic, immediate *)
   | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r addition *)
   | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r subtraction *)
@@ -273,9 +273,12 @@ Inductive instruction: Type :=
   | Pldrs (rd: freg) (a: addressing)                                  (**r load float32 (single precision) *)
   | Pldrd (rd: freg) (a: addressing)                                  (**r load float64 (double precision) *)
   | Pldrd_a (rd: freg) (a: addressing)                                (**r load float64 as any64 *)
+  | Pldps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two float32 *)
+  | Pldpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing)   (**r load two float64 *)
   | 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 *)
   (** Floating-point move *)
   | Pfmov (rd r1: freg)
   | Pfmovimms (rd: freg) (f: float32)                                 (**r load float32 constant *)
@@ -798,7 +801,7 @@ Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
                      (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
-    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
+    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
         match Mem.loadv chk1 m addr with
         | None => Stuck
@@ -824,7 +827,7 @@ Definition exec_store_double (chk1 chk2: memory_chunk)
                       (rs: regset) (m: mem) :=
   if is_pair_addressing_mode_correct a then
     let addr := (eval_addressing a rs) in
-    let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
+    let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in
     let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
       match Mem.storev chk1 m addr v1 with
       | None => Stuck
@@ -1258,17 +1261,27 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | _ => Stuck
       end
   | Pbuiltin ef args res => Stuck    (**r treated specially below *)
-  (** The following instructions and directives are not generated directly
-      by Asmgen, so we do not model them. *)
+  (** loads and stores pairs int/int64 *)
   | Pldpw rd1 rd2 chk1 chk2 a =>
       exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
   | Pldpx rd1 rd2 chk1 chk2 a =>
       exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
-  | Pnop => Next (nextinstr rs) m
   | Pstpw rs1 rs2 chk1 chk2 a =>
       exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
   | Pstpx rs1 rs2 chk1 chk2 a =>
       exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
+  (** loads and stores pairs floating-point *)
+  | Pldps rd1 rd2 chk1 chk2 a =>
+      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 =>
+      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 *)
+  | Pnop => Next (nextinstr rs) m
+  (** The following instructions and directives are not generated directly
+      by Asmgen, so we do not model them. *)
   | Pcls _ _ _
   | Pclz _ _ _
   | Prev _ _ _
-- 
cgit