added RISC-V "fence r,r"

10 files changed, 23 insertions, 9 deletions

diff --git a/etc/regfp.sail b/etc/regfp.sail
index 15d1a489..cc057f2e 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -74,6 +74,7 @@ typedef barrier_kind = enumerate {
   Barrier_MIPS_SYNC;
   Barrier_RISCV_rw_rw;
   Barrier_RISCV_r_rw;
+  Barrier_RISCV_r_r;
   Barrier_RISCV_rw_w;
   Barrier_RISCV_w_w;
   Barrier_RISCV_i;
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index 82bb1d5b..cf0ca80b 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -26,10 +26,10 @@
   { match ($2, $4) with
     | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
     | (Fence_R,  Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+    | (Fence_R,  Fence_R)  -> `RISCVFENCE (0b0010, 0b0010)
     | (Fence_RW, Fence_W)  -> `RISCVFENCE (0b0011, 0b0001)
     | (Fence_W,  Fence_W)  -> `RISCVFENCE (0b0001, 0b0001)
     | (Fence_RW, Fence_R)  -> failwith "'fence rw,r' is not supported"
-    | (Fence_R,  Fence_R)  -> failwith "'fence r,r' is not supported"
     | (Fence_R,  Fence_W)  -> failwith "'fence r,w' is not supported"
     | (Fence_W,  Fence_RW) -> failwith "'fence w,rw' is not supported"
     | (Fence_W,  Fence_R)  -> failwith "'fence w,r' is not supported"
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 4938aaca..e0a6efba 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -260,6 +260,7 @@ function clause execute (FENCE(pred, succ)) = {
   switch(pred, succ) {
     case (0b0011, 0b0011) -> MEM_fence_rw_rw()
     case (0b0010, 0b0011) -> MEM_fence_r_rw()
+    case (0b0010, 0b0010) -> MEM_fence_r_r()
     case (0b0011, 0b0001) -> MEM_fence_rw_w()
     case (0b0001, 0b0001) -> MEM_fence_w_w()
     case _ -> not_implemented("unsupported fence")
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index 280095e5..30043779 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -76,6 +76,7 @@ let speculate_conditional_success : excl_res =
 let barrier_functions =
   [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
     ("MEM_fence_r_rw",  Barrier_RISCV_r_rw);
+    ("MEM_fence_r_r",   Barrier_RISCV_r_r);
     ("MEM_fence_rw_w",  Barrier_RISCV_rw_w);
     ("MEM_fence_w_w",   Barrier_RISCV_w_w);
     ("MEM_fence_i",     Barrier_RISCV_i);
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index d89dc44c..32110079 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -53,12 +53,14 @@ let speculate_conditional_success () = excl_result () >>= fun b -> return (if b
 
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_r_r   : unit -> M unit
 val MEM_fence_rw_w  : unit -> M unit
 val MEM_fence_w_w   : unit -> M unit
 val MEM_fence_i     : unit -> M unit
 
 let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
 let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
+let MEM_fence_r_r   () = barrier Barrier_RISCV_r_r
 let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
 let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
 let MEM_fence_i     () = barrier Barrier_RISCV_i
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index 1f2a0e47..3c922268 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -53,12 +53,14 @@ let speculate_conditional_success () = excl_result () >>= fun b -> return (if b
 
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_r_r   : unit -> M unit
 val MEM_fence_rw_w  : unit -> M unit
 val MEM_fence_w_w   : unit -> M unit
 val MEM_fence_i     : unit -> M unit
 
 let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
 let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
+let MEM_fence_r_r   () = barrier Barrier_RISCV_r_r
 let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
 let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
 let MEM_fence_i     () = barrier Barrier_RISCV_i
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index 602f0bec..ad341c60 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -93,6 +93,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
               switch(pred, succ) {
                 case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw)
                 case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw)
+                case (0b0010, 0b0010) -> IK_barrier (Barrier_RISCV_r_r)
                 case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w)
                 case (0b0001, 0b0001) -> IK_barrier (Barrier_RISCV_w_w)
                 case _ -> exit "not implemented"
diff --git a/risc-v/riscv_types.sail b/risc-v/riscv_types.sail
index a11d5561..a7cda963 100644
--- a/risc-v/riscv_types.sail
+++ b/risc-v/riscv_types.sail
@@ -138,6 +138,7 @@ val extern unit -> bool effect {exmem} speculate_conditional_success
 
 val extern unit -> unit effect { barr } MEM_fence_rw_rw
 val extern unit -> unit effect { barr } MEM_fence_r_rw
+val extern unit -> unit effect { barr } MEM_fence_r_r
 val extern unit -> unit effect { barr } MEM_fence_rw_w
 val extern unit -> unit effect { barr } MEM_fence_w_w
 val extern unit -> unit effect { barr } MEM_fence_i
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