restore missing RISC-V fence types in sail2; ignore io bits in fences more cleanly

5 files changed, 36 insertions, 33 deletions

diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 87f1b7ca..b50c9225 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -707,19 +707,17 @@ mapping clause encdec = FENCE(pred, succ) <-> 0b0000 @ pred @ succ @ 0b00000 @ 0
 
 function clause execute (FENCE(pred, succ)) = {
   match (pred, succ) {
-    (0b0011, 0b0011) => MEM_fence_rw_rw(),
-    (0b0010, 0b0011) => MEM_fence_r_rw(),
-    (0b0010, 0b0010) => MEM_fence_r_r(),
-    (0b0011, 0b0001) => MEM_fence_rw_w(),
-    (0b0001, 0b0001) => MEM_fence_w_w(),
-
-    (0b1111, 0b1111) => MEM_fence_rw_rw(),
-    (0b1110, 0b1111) => MEM_fence_r_rw(),
-    (0b1110, 0b1110) => MEM_fence_r_r(),
-    (0b1111, 0b1101) => MEM_fence_rw_w(),
-    (0b1101, 0b1101) => MEM_fence_w_w(),
-
-    (0b0000, 0b0000) => (),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => MEM_fence_rw_rw(),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => MEM_fence_r_rw(),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => MEM_fence_r_r(),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => MEM_fence_rw_w(),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => MEM_fence_w_w(),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => MEM_fence_w_rw(),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => MEM_fence_rw_r(),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => MEM_fence_r_w(),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => MEM_fence_w_r(),
+
+    (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
     _ => { print("FIXME: unsupported fence");
            () }
@@ -1936,25 +1934,18 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
       FENCE(pred, succ) => {
              ik =
                match (pred, succ) {
-                 (0b0011, 0b0011) => IK_barrier (Barrier_RISCV_rw_rw),
-                 (0b0010, 0b0011) => IK_barrier (Barrier_RISCV_r_rw),
-                 (0b0010, 0b0010) => IK_barrier (Barrier_RISCV_r_r),
-                 (0b0011, 0b0001) => IK_barrier (Barrier_RISCV_rw_w),
-                 (0b0001, 0b0001) => IK_barrier (Barrier_RISCV_w_w),
-
-                 (0b1111, 0b1111) => IK_barrier (Barrier_RISCV_rw_rw),
-                 (0b1110, 0b1111) => IK_barrier (Barrier_RISCV_r_rw),
-                 (0b1110, 0b1110) => IK_barrier (Barrier_RISCV_r_r),
-                 (0b1111, 0b1101) => IK_barrier (Barrier_RISCV_rw_w),
-                 (0b1101, 0b1101) => IK_barrier (Barrier_RISCV_w_w),
-
-                 // (0b0001, 0b0011) => IK_barrier (Barrier_RISCV_w_rw),
-                 // (0b0011, 0b0010) => IK_barrier (Barrier_RISCV_rw_r),
-                 // (0b0010, 0b0001) => IK_barrier (Barrier_RISCV_r_w),
-                 // (0b0001, 0b0010) => IK_barrier (Barrier_RISCV_w_r),
-
-
-                 (0b0000, 0b0000) => IK_simple (),
+                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw),
+                 (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw),
+                 (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r),
+                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w),
+                 (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w),
+                 (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw),
+                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r),
+                 (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w),
+                 (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r),
+
+
+                 (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (),
 
                  _ => internal_error("barrier type not implemented in initial_analysis")
   //               case (FM_NORMAL, _, _) -> exit "not implemented"
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 601f5008..b29fe545 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -13,6 +13,10 @@ 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_w_rw  () = barrier Barrier_RISCV_w_rw
+let MEM_fence_rw_r  () = barrier Barrier_RISCV_rw_r
+let MEM_fence_r_w   () = barrier Barrier_RISCV_r_w
+let MEM_fence_w_r   () = barrier Barrier_RISCV_w_r
 let MEM_fence_i     () = barrier Barrier_RISCV_i
 
 val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index 601f5008..b29fe545 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -13,6 +13,10 @@ 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_w_rw  () = barrier Barrier_RISCV_w_rw
+let MEM_fence_rw_r  () = barrier Barrier_RISCV_rw_r
+let MEM_fence_r_w   () = barrier Barrier_RISCV_r_w
+let MEM_fence_w_r   () = barrier Barrier_RISCV_w_r
 let MEM_fence_i     () = barrier Barrier_RISCV_i
 
 val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index bdbb72bf..9ead3aeb 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -140,4 +140,8 @@ val MEM_fence_r_rw  = {ocaml: "skip", lem: "MEM_fence_r_rw"}  : unit -> unit eff
 val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit effect {barr}
 val MEM_fence_rw_w  = {ocaml: "skip", lem: "MEM_fence_rw_w"}  : unit -> unit effect {barr}
 val MEM_fence_w_w   = {ocaml: "skip", lem: "MEM_fence_w_w"}   : unit -> unit effect {barr}
+val MEM_fence_w_rw  = {ocaml: "skip", lem: "MEM_fence_w_rw"}  : unit -> unit effect {barr}
+val MEM_fence_rw_r  = {ocaml: "skip", lem: "MEM_fence_rw_r"}  : unit -> unit effect {barr}
+val MEM_fence_r_w   = {ocaml: "skip", lem: "MEM_fence_r_w"}   : unit -> unit effect {barr}
+val MEM_fence_w_r   = {ocaml: "skip", lem: "MEM_fence_w_r"}   : unit -> unit effect {barr}
 val MEM_fence_i     = {ocaml: "skip", lem: "MEM_fence_i"}     : unit -> unit effect {barr}
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 2991377d..e2341a8a 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -468,7 +468,7 @@ mapping reg_name = {
 }
 
 val sep : unit <-> string
-mapping sep = {
+mapping sep : unit <-> string = {
   () <-> opt_spc() ^ "," ^ def_spc()
 }