Asmblock: Add floating-point load and stores

Since exec_load and exec_store are defined with preg (not ireg or freg)
I simply appended the floating point instructions to the already defined
types and functions.

1 files changed, 24 insertions, 4 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 50c1a387..66a8f14e 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -215,8 +215,11 @@ Coercion PCtlFlow: cf_instruction >-> control.
 
 (** Basic instructions *)
 
-(* Loads waiting for (rd: ireg) (a: addressing) *)
+(* Loads waiting for (rd: preg) (a: addressing) 
+ * XXX Use preg because exec_load is defined in terms of it, thus allowing us to
+ * treat integer and floating point loads the same. *)
 Inductive load_rd_a: Type :=
+  (* Integer load *)
   | Pldrw                                   (**r load int32 *)
   | Pldrw_a                                 (**r load int32 as any32 *)
   | Pldrx                                   (**r load int64 *)
@@ -227,7 +230,10 @@ Inductive load_rd_a: Type :=
   | Pldrsh (sz: isize)                      (**r load int16, sign-extend *)
   | Pldrzw                                  (**r load int32, zero-extend to int64 *)
   | Pldrsw                                  (**r load int32, sign-extend to int64 *)
-  (* TODO floating point loads *)
+  (* Floating-point load *)
+  | Pldrs                                   (**r load float32 (single precision) *)
+  | Pldrd                                   (**r load float64 (double precision) *)
+  | Pldrd_a                                 (**r load float64 as any64 *)
   .
 
 (* Actually, Pldp is not used in the aarch64/Asm semantics!
@@ -244,13 +250,17 @@ Coercion PLoad: ld_instruction >-> basic.
 *)
 
 Inductive store_rs_a : Type :=
+  (* Integer store *)
   | Pstrw                                   (**r store int32 *)
   | Pstrw_a                                 (**r store int32 as any32 *)
   | Pstrx                                   (**r store int64 *)
   | Pstrx_a                                 (**r store int64 as any64 *)
   | Pstrb                                   (**r store int8 *)
   | Pstrh                                   (**r store int16 *)
-  (* TODO: floating stores *)
+  (* Floating-point store *)
+  | Pstrs                                   (**r store float32 *)
+  | Pstrd                                   (**r store float64 *)
+  | Pstrd_a                                 (**r store float64 as any64 *)
   .
 (* Actually, Pstp is not used in the aarch64/Asm semantics!
  * Thus we skip this particular case:
@@ -1157,6 +1167,9 @@ Definition chunk_load_rd_a (ld: load_rd_a): memory_chunk :=
   | Pldrsh _ => Mint16signed
   | Pldrzw => Mint32
   | Pldrsw => Mint32
+  | Pldrs => Mfloat32
+  | Pldrd => Mfloat64
+  | Pldrd_a =>  Many64
   end.
 
 Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk :=
@@ -1167,6 +1180,9 @@ Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk :=
   | Pstrx_a => Many64
   | Pstrb   => Mint8unsigned
   | Pstrh   => Mint16unsigned
+  | Pstrs   => Mfloat32
+  | Pstrd   => Mfloat64
+  | Pstrd_a => Many64
   end.
 
 Definition interp_load_rd_a (ld: load_rd_a): val -> val :=
@@ -1177,7 +1193,11 @@ Definition interp_load_rd_a (ld: load_rd_a): val -> val :=
   | Pldrsh X => Val.longofint
   | Pldrzw => Val.longofintu
   | Pldrsw => Val.longofint
-  | _ => fun v => v
+  (* Changed to exhaustive list because I tend to forgot all the places I need
+   * to check when changing things. *)
+  | Pldrb W | Pldrsb W | Pldrh W | Pldrsh W
+  | Pldrw   | Pldrw_a  | Pldrx   | Pldrx_a
+  | Pldrs   | Pldrd    | Pldrd_a => fun v => v
   end.
 
 (** TODO: redundant w.r.t Machblock ?? *)