added RISC-V "fence r,r"

2 files changed, 13 insertions, 8 deletions

diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 5a0dd99e..76880dbd 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -471,10 +471,11 @@ let barrier_kindToInterpValue = function
   | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ())
   | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ())
   | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ())
-  | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ())
-  | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ())
-  | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ())
-  | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ())
+  | Barrier_RISCV_r_r -> V_ctor (Id_aux (Id "Barrier_RISCV_r_r") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ())
+  | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ())
+  | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ())
+  | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ())
+  | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 19) (toInterpValue ())
   end
 let rec barrier_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync
@@ -492,6 +493,7 @@ let rec barrier_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC
   | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw
   | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw
+  | V_ctor (Id_aux (Id "Barrier_RISCV_r_r") _) _ _ v -> Barrier_RISCV_r_r
   | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w
   | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w
   | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 4f07f574..c0ec8548 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -501,6 +501,7 @@ type barrier_kind =
   (* RISC-V barriers *)
   | Barrier_RISCV_rw_rw
   | Barrier_RISCV_r_rw
+  | Barrier_RISCV_r_r
   | Barrier_RISCV_rw_w
   | Barrier_RISCV_w_w
   | Barrier_RISCV_i
@@ -525,6 +526,7 @@ instance (Show barrier_kind)
     | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
     | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
     | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
+    | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
     | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
     | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
     | Barrier_RISCV_i     -> "Barrier_RISCV_i"
@@ -621,10 +623,11 @@ instance (EnumerationType barrier_kind)
     | Barrier_MIPS_SYNC -> 12
     | Barrier_RISCV_rw_rw -> 13
     | Barrier_RISCV_r_rw -> 14
-    | Barrier_RISCV_rw_w -> 15
-    | Barrier_RISCV_w_w -> 16
-    | Barrier_RISCV_i -> 17
-    | Barrier_x86_MFENCE -> 18
+    | Barrier_RISCV_r_r -> 15
+    | Barrier_RISCV_rw_w -> 16
+    | Barrier_RISCV_w_w -> 17
+    | Barrier_RISCV_i -> 18
+    | Barrier_x86_MFENCE -> 19
   end
 end