added RISC-V AMOs

2 files changed, 51 insertions, 13 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 6a9a77a1..411ad3fc 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1416,6 +1416,41 @@ let interp_instruction_analysis
 
           if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
             inst_kind
+
+          else if
+            (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | IK_mem_write _ -> true
+                | IK_mem_rmw _   -> false
+                | IK_barrier _   -> false
+                | IK_cond_branch -> false
+                | IK_trans _     -> false
+                | IK_simple      -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | _              -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_write _ -> true
+                | _              -> false
+                end)
+          then
+            match
+              List.partition
+                (function IK_mem_read _ -> true | _ -> false end)
+                (inst_kind :: inst_kinds)
+            with
+            | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) ->
+                let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in
+                let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in
+                IK_mem_rmw (r, w)
+            | _ -> fail
+            end
+
           (* the TSTART instruction can also be aborted so it will have two kinds of events *)
           else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
                         inst_kind' = IK_trans Transaction_start) &&
@@ -1424,7 +1459,9 @@ let interp_instruction_analysis
                         || inst_kind' = IK_trans Transaction_abort)
           then
             IK_trans Transaction_start
-          else failwith "multiple instruction kinds"
+
+          else
+            failwith "multiple instruction kinds"
     end in
 
   (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 3886f919..721c0226 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -552,26 +552,27 @@ instance (Show trans_kind)
 end
 
 type instruction_kind = 
-  | IK_barrier of barrier_kind 
-  | IK_mem_read of read_kind 
+  | IK_barrier   of barrier_kind
+  | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
-(* SS reinstating cond_branches
-at present branches are not distinguished in the instruction_kind;
-they just have particular nias (and will be IK_simple *)
-  | IK_cond_branch 
-(*  | IK_uncond_branch *)
-  | IK_trans of trans_kind
+  | IK_mem_rmw   of (read_kind * write_kind)
+  | IK_cond_branch
+  (* unconditional branches are not distinguished in the instruction_kind;
+  they just have particular nias (and will be IK_simple *)
+  (* | IK_uncond_branch *)
+  | IK_trans     of trans_kind
   | IK_simple
 
 
 instance (Show instruction_kind)
   let show = function
     | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
-    | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind)
+    | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_cond_branch -> "IK_cond_branch"
-    | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind)
-    | IK_simple -> "IK_simple"
+    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
+    | IK_cond_branch          -> "IK_cond_branch"
+    | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
+    | IK_simple               -> "IK_simple"
   end
 end