Add memory kind for concurrent tag reads and writes

2 files changed, 4 insertions, 53 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 0f9dff80..6b04abed 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -395,66 +395,27 @@ end
 type read_kind =
   (* common reads *)
   Read_plain
-  | Read_tag (*For reading the tag of tagged memory*)
+  | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*)
   (* Power reads *)
   | Read_reserve
   (* AArch64 reads *)
   | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
 
-instance (Show read_kind)
-  let show = function
-    | Read_plain -> "Read_plain"
-    | Read_tag -> "Read_tag"
-    | Read_reserve -> "Read_reserve"
-    | Read_acquire -> "Read_acquire"
-    | Read_exclusive_acquire -> "Read_exclusive_acquire"
-    | Read_stream -> "Read_stream"
-  end
-end
-
 type write_kind =
   (* common writes *)
     Write_plain
-  | Write_tag (*For writing the tag of tagged memory*)
+  | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*)
   (* Power writes *)
   | Write_conditional
   (* AArch64 writes *)
   | Write_release | Write_exclusive | Write_exclusive_release
 
-instance (Show write_kind)
-  let show = function
-    | Write_plain -> "Write_plain"
-    | Write_tag -> "Write_tag"
-    | Write_conditional -> "Write_conditional"
-    | Write_release -> "Write_release"
-    | Write_exclusive -> "Write_exclusive"
-    | Write_exclusive_release -> "Write_exclusive_release"
-  end
-end
-
 type barrier_kind =
   (* Power barriers *)
   Sync | LwSync | Eieio | Isync
   (* AArch64 barriers *)
   | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
 
-instance (Show barrier_kind)
-  let show = function
-    | Sync -> "Sync"
-    | LwSync -> "LwSync"
-    | Eieio -> "Eieio"
-    | Isync -> "Isync"
-    | DMB -> "DMB"
-    | DMB_ST -> "DMB_ST"
-    | DMB_LD -> "DMB_LD"
-    | DSB -> "DSB"
-    | DSB_ST -> "DSB_ST"
-    | DSB_LD -> "DSB_LD"
-    | ISB -> "ISB"
-  end
-end
-
-
 type instruction_kind = 
   | IK_barrier of barrier_kind 
   | IK_mem_read of read_kind 
@@ -466,16 +427,6 @@ they just have particular nias (and will be IK_simple *)
 (*  | IK_uncond_branch *)
   | IK_simple
 
-instance (Show instruction_kind)
-  let show = function
-    | IK_barrier bk -> "IK_barrier " ^ show bk
-    | IK_mem_read m -> "IK_mem_read " ^ show m
-    | IK_mem_write w -> "IK_mem_write " ^ show w
-    | IK_cond_branch -> "IK_cond_branch"
-    | IK_simple -> "IK_simple"
-  end
-end
-
 (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
 type external_functions = list (string * (Interp.value -> Interp.value))
 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index aca33e96..eec87f4f 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -128,7 +128,7 @@ let rec perform_action ((reg, mem, tagmem) as env) = function
      | None -> assert false (*TODO remember how to report an error *)in
    let naddress = integer_of_address address in
    (match kind with
-    | Read_tag ->
+    | Read_tag | Read_tag_reserve ->
       let tag = Mem.find naddress tagmem in
       let rec reading (n : num) length = 
         if length = 0 
@@ -147,7 +147,7 @@ let rec perform_action ((reg, mem, tagmem) as env) = function
      | None -> assert false (*TODO remember how to report an error *)in
    let naddress = integer_of_address address in
    (match kind with
-    | Write_tag ->
+    | Write_tag | Write_tag_conditional ->
       (match bytes with
        | [b] -> (None,(reg,mem,Mem.add naddress b tagmem))
        | _ -> assert false)