Revert "Support DMB/DSB domains"

Move this commit to new_barriers branch until we can update C/SMT/etc
and make a new release of Sail for backwards compatability with the
opam package

This reverts commit 273ec8b0715b39844101c8081114f2697f291312.

4 files changed, 44 insertions, 44 deletions

diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index f4ade26..da6106d 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -8,17 +8,17 @@ open import Sail2_prompt
 
 type bitvector 'a = mword 'a
 
-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_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_tso   () = barrier (Barrier_RISCV_tso ())
-let MEM_fence_i     () = barrier (Barrier_RISCV_i ())
+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_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_tso   () = barrier Barrier_RISCV_tso
+let MEM_fence_i     () = barrier Barrier_RISCV_i
 
 val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
 val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
index ac70ee5..7715614 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -8,17 +8,17 @@ open import Sail2_prompt
 
 type bitvector 'a = mword 'a
 
-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_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_tso   () = barrier (Barrier_RISCV_tso ())
-let MEM_fence_i     () = barrier (Barrier_RISCV_i ())
+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_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_tso   () = barrier Barrier_RISCV_tso
+let MEM_fence_i     () = barrier Barrier_RISCV_i
 
 val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
 val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index 1f0f59b..34572f8 100644
--- a/model/riscv_analysis.sail
+++ b/model/riscv_analysis.sail
@@ -112,15 +112,15 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
       FENCE(pred, succ) => {
              ik =
                match (pred, succ) {
-                 (_ : 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) @ 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 (),
@@ -131,12 +131,12 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
       FENCE_TSO(pred, succ) => {
              ik =
                match (pred, succ) {
-                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()),
+                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso),
                  _ => internal_error("barrier type not implemented in initial_analysis")
                };
       },
      FENCEI() => {
-              ik = IK_simple (); // for RMEM, should morally be (Barrier_RISCV_i ())
+              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
      },
      LOADRES(aq, rl, rs1, width, rd) => {
             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index eab4bfc..14a626e 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -566,15 +566,15 @@ mapping clause encdec = FENCE(pred, succ)
 
 function clause execute (FENCE(pred, succ)) = {
   match (pred, succ) {
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw ()),
-    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw ()),
-    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r ()),
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w ()),
-    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w ()),
-    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw ()),
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r ()),
-    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w ()),
-    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r ()),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r),
 
     (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
@@ -619,7 +619,7 @@ mapping clause encdec = FENCE_TSO(pred, succ)
 
 function clause execute (FENCE_TSO(pred, succ)) = {
   match (pred, succ) {
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso ()),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso),
     (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
     _ => { print("FIXME: unsupported fence");
@@ -638,7 +638,7 @@ mapping clause encdec = FENCEI()
   <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111
 
 /* fence.i is a nop for the memory model */
-function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i ()); */ RETIRE_SUCCESS }
+function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SUCCESS }
 
 mapping clause assembly = FENCEI() <-> "fence.i"