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

7 files changed, 54 insertions, 35 deletions

diff --git a/lib/regfp.sail b/lib/regfp.sail
index b8cffb98..fcf10850 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -75,6 +75,10 @@ enum barrier_kind = {
   Barrier_RISCV_r_r,
   Barrier_RISCV_rw_w,
   Barrier_RISCV_w_w,
+  Barrier_RISCV_w_rw,
+  Barrier_RISCV_rw_r,
+  Barrier_RISCV_r_w,
+  Barrier_RISCV_w_r,
   Barrier_RISCV_i,
   Barrier_x86_MFENCE
 }
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()
 }
 
diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index 13e5304e..938b693d 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -151,6 +151,10 @@ type barrier_kind =
   | Barrier_RISCV_r_r
   | Barrier_RISCV_rw_w
   | Barrier_RISCV_w_w
+  | Barrier_RISCV_w_rw
+  | Barrier_RISCV_rw_r
+  | Barrier_RISCV_r_w
+  | Barrier_RISCV_w_r
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE
@@ -176,6 +180,10 @@ instance (Show barrier_kind)
     | 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_w_rw  -> "Barrier_RISCV_w_rw"
+    | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
+    | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
+    | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
     | Barrier_RISCV_i     -> "Barrier_RISCV_i"
     | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
   end
@@ -288,7 +296,11 @@ instance (EnumerationType barrier_kind)
     | Barrier_RISCV_r_r -> 15
     | Barrier_RISCV_rw_w -> 16
     | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_i -> 18
-    | Barrier_x86_MFENCE -> 19
+    | Barrier_RISCV_w_rw -> 18
+    | Barrier_RISCV_rw_r -> 19
+    | Barrier_RISCV_r_w -> 20
+    | Barrier_RISCV_w_r -> 21
+    | Barrier_RISCV_i -> 22
+    | Barrier_x86_MFENCE -> 23
   end
 end