added RISC-V "fence r,r"

7 files changed, 9 insertions, 1 deletions

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