Merge pull request #458 from Alasdair/interface

RVWMO support via Sail concurrency interface

8 files changed, 194 insertions, 454 deletions

diff --git a/Makefile b/Makefile
index 8004a56..ea6244a 100644
--- a/Makefile
+++ b/Makefile
@@ -109,16 +109,13 @@ SAIL_ARCH_SRCS += riscv_types_kext.sail    # Shared/common code for the cryptogr
 SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
 RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail
 
-# Control inclusion of 64-bit only riscv_analysis
-ifeq ($(ARCH),RV32)
 SAIL_OTHER_SRCS     = $(SAIL_STEP_SRCS)
+ifeq ($(ARCH),RV32)
 SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv32.sail
 else
-SAIL_OTHER_SRCS     = $(SAIL_STEP_SRCS) riscv_analysis.sail
-SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail riscv_analysis.sail
+SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail
 endif
 
-
 PRELUDE_SRCS   = $(addprefix model/,$(PRELUDE))
 SAIL_SRCS      = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS)  $(SAIL_OTHER_SRCS))
 SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS))
diff --git a/model/main.sail b/model/main.sail
index c545e27..1422635 100644
--- a/model/main.sail
+++ b/model/main.sail
@@ -6,19 +6,74 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-function main () : unit -> unit = {
+// When the symbolic execution is running a litmus test, it sets a
+// different entry point for each thread in the compiled litmus test.
+
+val get_entry_point : unit -> xlenbits
+
+$ifdef SYMBOLIC
+
+$include <elf.sail>
+
+function get_entry_point() = to_bits(sizeof(xlen), elf_entry())
+
+$else
+
+function get_entry_point() = zero_extend(0x1000)
+
+$endif
+
+function main() : unit -> unit = {
   // initialize extensions
-  ext_init ();
+  ext_init();
 
-  // PC = __GetSlice_int(64, elf_entry(), 0);
-  PC = sail_zero_extend(0x1000, sizeof(xlen));
+  PC = get_entry_point();
   print_bits("PC = ", PC);
 
   try {
     init_model();
+    sail_end_cycle();
     loop()
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
     Error_internal_error() => print("Error: internal error")
   }
 }
+
+// For symbolic execution using Isla, we need an entry point that
+// allows us to execute a single instruction.
+$ifdef SYMBOLIC
+
+$include <isla.sail>
+
+val isla_footprint_no_init : forall 'n, 'n in {16, 32}. bits('n) -> bool
+
+function isla_footprint_no_init(opcode) = {
+  try {
+    isla_reset_registers();
+    sail_end_cycle();
+
+    let instr = if length(opcode) == 16 then {
+      ext_decode_compressed(opcode)
+    } else {
+      ext_decode(opcode)
+    };
+    let _ = execute(instr);
+    true
+  } catch {
+    _ => false
+  }
+}
+
+val isla_footprint : forall 'n, 'n in {16, 32}. bits('n) -> bool
+
+function isla_footprint(opcode) = {
+  try {
+    init_model();
+    isla_footprint_no_init(opcode)
+  } catch {
+    _ => false
+  }
+}
+
+$endif
diff --git a/model/prelude.sail b/model/prelude.sail
index 028af21..b876b4f 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -14,11 +14,9 @@ $include <arith.sail>
 $include <string.sail>
 $include "mapping.sail"
 $include <vector_dec.sail>
-$include <regfp.sail>
 $include <generic_equality.sail>
 $include "hex_bits.sail"
 
-
 val not_bit : bit -> bit
 function not_bit(b) = if b == bitone then bitzero else bitone
 
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index c4f3d07..345e78c 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -12,12 +12,68 @@
  * They also depend on the type of metadata that is read and written
  * to physical memory.  For models that do not require this metadata,
  * a unit type can be used.
- *
- * The underlying __read_mem and __write_mem functions are from the
- * Sail library.  The metadata primitives __{Read,Write}RAM_Meta are
- * in prelude_mem_metadata.
  */
 
+$include <concurrency_interface.sail>
+
+enum write_kind = {
+  Write_plain,
+  Write_RISCV_release,
+  Write_RISCV_strong_release,
+  Write_RISCV_conditional,
+  Write_RISCV_conditional_release,
+  Write_RISCV_conditional_strong_release,
+}
+
+enum read_kind = {
+  Read_plain,
+  Read_ifetch,
+  Read_RISCV_acquire,
+  Read_RISCV_strong_acquire,
+  Read_RISCV_reserved,
+  Read_RISCV_reserved_acquire,
+  Read_RISCV_reserved_strong_acquire,
+}
+
+enum barrier_kind = {
+  Barrier_RISCV_rw_rw,
+  Barrier_RISCV_r_rw,
+  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_tso,
+  Barrier_RISCV_i,
+}
+
+/* Most of the above read/write_kinds are understood natively by the
+   Sail concurrency interface, except for the strong acquire release
+   variants which require an architecture specific access kind. */
+struct RISCV_strong_access = {
+  variety : Access_variety,
+}
+
+/* The Sail concurrency interface lets us have a physical address type
+   with additional information, provided we can supply a function that
+   converts it into a bitvector.  Since we are just using xlenbits as a
+   physical address, we need the identity function for xlenbits. */
+val xlenbits_identity : xlenbits -> xlenbits
+
+function xlenbits_identity xs = xs
+
+instantiation sail_mem_write with
+  'pa = xlenbits,
+  pa_bits = xlenbits_identity,
+  /* We don't have a relaxed-memory translation model for RISC-V, so
+     we just use unit as a dummy type. */
+  'translation_summary = unit,
+  'arch_ak = RISCV_strong_access,
+  /* Similarly to translation_summary, we don't have a defined type for external
+     aborts, so just use unit here too */
+  'abort = unit
 
 /* This is a slightly arbitrary limit on the maximum number of bytes
    in a memory access.  It helps to generate slightly better C code
@@ -27,8 +83,25 @@
    capabilities and SIMD / vector instructions will also need more. */
 type max_mem_access : Int = 16
 
-val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool
+val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool
+
 function write_ram(wk, addr, width, data, meta) = {
+  let request : Mem_write_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct {
+    access_kind = match wk {
+      Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }),
+      Write_RISCV_release => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }),
+      Write_RISCV_strong_release => AK_arch(struct { variety = AV_plain }),
+      Write_RISCV_conditional => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }),
+      Write_RISCV_conditional_release => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }),
+      Write_RISCV_conditional_strong_release => AK_arch(struct { variety = AV_exclusive }),
+    },
+    va = None(),
+    pa = addr,
+    translation = (),
+    size = width,
+    value = Some(data),
+    tag = None(),
+  };
   /* Write out metadata only if the value write succeeds.
    * It is assumed for now that this write always succeeds;
    * there is currently no return value.
@@ -36,19 +109,47 @@ function write_ram(wk, addr, width, data, meta) = {
    * (not just for Lem) to consume the value along with the
    * metadata to ensure atomicity.
    */
-  let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data);
-  if ret then __WriteRAM_Meta(addr, width, meta);
-  ret
+  match sail_mem_write(request) {
+    Ok(_) => {
+      __WriteRAM_Meta(addr, width, meta);
+      true
+    },
+    Err() => false,
+  }
 }
 
-val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n)) -> unit
-function write_ram_ea(wk, addr, width) =
-  __write_mem_ea(wk, sizeof(xlen), addr, width)
+val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n)) -> unit
+function write_ram_ea(wk, addr, width) = ()
+
+instantiation sail_mem_read with
+  pa_bits = xlenbits_identity
+
+val read_ram : forall 'n, 0 < 'n <= max_mem_access.  (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta)
+function read_ram(rk, addr, width, read_meta) = {
+  let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta;
+  let request : Mem_read_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct {
+    access_kind = match rk {
+      Read_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }),
+      Read_ifetch => AK_ifetch(),
+      Read_RISCV_acquire => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }),
+      Read_RISCV_strong_acquire => AK_arch(struct { variety = AV_plain }),
+      Read_RISCV_reserved => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }),
+      Read_RISCV_reserved_acquire => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }),
+      Read_RISCV_reserved_strong_acquire => AK_arch(struct { variety = AV_exclusive }),
+    },
+    va = None(),
+    pa = addr,
+    translation = (),
+    size = width,
+    tag = false,
+  };
+  match sail_mem_read(request) {
+    Ok((value, _)) => (value, meta),
+    Err() => exit(),
+  }
+}
 
-val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta)
-function read_ram(rk, addr, width, read_meta) =
-  let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
-  (__read_mem(rk, sizeof(xlen), addr, width), meta)
+instantiation sail_barrier with 'barrier = barrier_kind
 
 val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
 val __TraceMemoryRead  : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
deleted file mode 100644
index 0d72bed..0000000
--- a/model/riscv_analysis.sail
+++ /dev/null
@@ -1,367 +0,0 @@
-/*=======================================================================================*/
-/*  This Sail RISC-V architecture model, comprising all files and                        */
-/*  directories except where otherwise noted is subject the BSD                          */
-/*  two-clause license in the LICENSE file.                                              */
-/*                                                                                       */
-/*  SPDX-License-Identifier: BSD-2-Clause                                                */
-/*=======================================================================================*/
-
-$include <regfp.sail>
-
-/* in reverse order because inc vectors don't seem to work (bug) */
-let GPRstrs : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21",
-  "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x11",
-  "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0"
-  ]
-
-function GPRstr(i: bits(5)) -> string = GPRstrs[unsigned(i)]
-
-let CIA_fp = RFull("CIA")
-let NIA_fp = RFull("NIA")
-
-$ifndef FEATURE_UNION_BARRIER
-
-function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = {
-  iR = [| |] : regfps;
-  oR = [| |] : regfps;
-  aR = [| |] : regfps;
-  ik = IK_simple() : instruction_kind;
-  Nias = [| NIAFP_successor() |] : niafps;
-  Dia = DIAFP_none() : diafp;
-
-  match instr {
-     EBREAK() => (),
-     UTYPE(imm, rd, op) => {
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-     },
-     RISCV_JAL(imm, rd) => {
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address (PC + offset) |];
-            ik = IK_branch();
-     },
-     RISCV_JALR(imm, rs, rd) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_indirect_address() |];
-            ik = IK_branch();
-     },
-     BTYPE(imm, rs2, rs1, op) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            ik = IK_branch();
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
-      },
-      ITYPE(imm, rs, rd, op) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPE(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      CSR(csr, rs1, rd, is_imm, op) => {
-               let isWrite : bool = match op {
-                   CSRRW  => true,
-                   _      => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0
-               };
-               iR = RFull(csr_name(csr)) :: iR;
-               if not(is_imm) then {
-                  iR = RFull(GPRstr(rs1)) :: iR;
-               };
-               if isWrite then {
-                  oR = RFull(csr_name(csr)) :: oR;
-               };
-               oR = RFull(GPRstr(rd)) :: oR;
-      },
-      LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-             aR = iR;
-             ik =
-               match (aq, rl) {
-                 (false, false) => IK_mem_read (Read_plain),
-                 (true,  false) => IK_mem_read (Read_RISCV_acquire),
-                 (true,  true)  => IK_mem_read (Read_RISCV_strong_acquire),
-
-                 _  => internal_error(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis")
-               }
-      },
-      STORE(imm, rs2, rs1, width, aq, rl) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-             ik =
-               match (aq, rl) {
-                 (false, false) => IK_mem_write (Write_plain),
-                 (false, true)  => IK_mem_write (Write_RISCV_release),
-                 (true,  true)  => IK_mem_write (Write_RISCV_strong_release),
-
-                 _ => internal_error(__FILE__, __LINE__, "STORE type not implemented in initial_analysis")
-               }
-      },
-      ADDIW(imm, rs, rd) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIWOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPEW(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      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) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (),
-
-                 _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-      FENCE_TSO(pred, succ) => {
-             ik =
-               match (pred, succ) {
-                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso),
-                 _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-     FENCEI() => {
-              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
-     },
-     LOADRES(aq, rl, rs1, width, rd) => {
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            aR = iR;
-            ik = match (aq, rl) {
-              (false, false) => IK_mem_read (Read_RISCV_reserved),
-              (true,  false) => IK_mem_read (Read_RISCV_reserved_acquire),
-              (true,  true)  => IK_mem_read (Read_RISCV_reserved_strong_acquire),
-              (false, true)  => internal_error(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis")
-            };
-     },
-     STORECON(aq, rl, rs2, rs1, width, rd) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-             ik = match (aq, rl) {
-               (false, false) => IK_mem_write (Write_RISCV_conditional),
-               (false, true)  => IK_mem_write (Write_RISCV_conditional_release),
-               (true,  true)  => IK_mem_write (Write_RISCV_conditional_strong_release),
-
-               (true,  false) => internal_error(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis")
-             };
-      },
-      AMO(op, aq, rl, rs2, rs1, width, rd) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-             ik = match (aq, rl) {
-               (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional),
-               (false, true)  => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release),
-               (true,  false) => IK_mem_rmw (Read_RISCV_reserved_acquire,
-                                                                       Write_RISCV_conditional),
-               (true,  true)  => IK_mem_rmw (Read_RISCV_reserved_acquire,
-                                                                       Write_RISCV_conditional_release)
-             };
-      },
-        _ => ()
-  };
-  (iR,oR,aR,Nias,Dia,ik)
-}
-
-$else
-
-function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = {
-  iR = [| |] : regfps;
-  oR = [| |] : regfps;
-  aR = [| |] : regfps;
-  ik = IK_simple() : instruction_kind;
-  Nias = [| NIAFP_successor() |] : niafps;
-  Dia = DIAFP_none() : diafp;
-
-  match instr {
-     EBREAK() => (),
-     UTYPE(imm, rd, op) => {
-	    if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-     },
-     RISCV_JAL(imm, rd) => {
-	    if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address (PC + offset) |];
-            ik = IK_branch();
-     },
-     RISCV_JALR(imm, rs, rd) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_indirect_address() |];
-            ik = IK_branch();
-     },
-     BTYPE(imm, rs2, rs1, op) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            ik = IK_branch();
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
-      },
-      ITYPE(imm, rs, rd, op) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPE(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      CSR(csr, rs1, rd, is_imm, op) => {
-               let isWrite : bool = match op {
-                   CSRRW  => true,
-                   _      => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0
-               };
-               iR = RFull(csr_name(csr)) :: iR;
-               if not(is_imm) then {
-                  iR = RFull(GPRstr(rs1)) :: iR;
-               };
-               if isWrite then {
-                  oR = RFull(csr_name(csr)) :: oR;
-               };
-               oR = RFull(GPRstr(rd)) :: oR;
-      },
-      LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-             aR = iR;
-             ik =
-               match (aq, rl) {
-                 (false, false) => IK_mem_read (Read_plain),
-                 (true,  false) => IK_mem_read (Read_RISCV_acquire),
-                 (true,  true)  => IK_mem_read (Read_RISCV_strong_acquire),
-
-                 _  => internal_error(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis")
-               }
-      },
-      STORE(imm, rs2, rs1, width, aq, rl) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-             ik =
-               match (aq, rl) {
-                 (false, false) => IK_mem_write (Write_plain),
-                 (false, true)  => IK_mem_write (Write_RISCV_release),
-                 (true,  true)  => IK_mem_write (Write_RISCV_strong_release),
-
-                 _ => internal_error(__FILE__, __LINE__, "STORE type not implemented in initial_analysis")
-               }
-      },
-      ADDIW(imm, rs, rd) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIWOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPEW(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      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) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (),
-
-                 _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-      FENCE_TSO(pred, succ) => {
-             ik =
-               match (pred, succ) {
-		 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()),
-                 _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-     FENCEI() => {
-              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
-     },
-     LOADRES(aq, rl, rs1, width, rd) => {
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            aR = iR;
-            ik = match (aq, rl) {
-              (false, false) => IK_mem_read (Read_RISCV_reserved),
-              (true,  false) => IK_mem_read (Read_RISCV_reserved_acquire),
-              (true,  true)  => IK_mem_read (Read_RISCV_reserved_strong_acquire),
-              (false, true)  => internal_error(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis")
-            };
-     },
-     STORECON(aq, rl, rs2, rs1, width, rd) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-             ik = match (aq, rl) {
-               (false, false) => IK_mem_write (Write_RISCV_conditional),
-               (false, true)  => IK_mem_write (Write_RISCV_conditional_release),
-               (true,  true)  => IK_mem_write (Write_RISCV_conditional_strong_release),
-
-               (true,  false) => internal_error(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis")
-             };
-      },
-      AMO(op, aq, rl, rs2, rs1, width, rd) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-             ik = match (aq, rl) {
-               (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional),
-               (false, true)  => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release),
-               (true,  false) => IK_mem_rmw (Read_RISCV_reserved_acquire,
-                                                                       Write_RISCV_conditional),
-               (true,  true)  => IK_mem_rmw (Read_RISCV_reserved_acquire,
-                                                                       Write_RISCV_conditional_release)
-             };
-      },
-        _ => ()
-  };
-  (iR,oR,aR,Nias,Dia,ik)
-}
-
-$endif
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 9c4630b..25891c9 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -544,9 +544,6 @@ function effective_fence_set(set : bits(4), fiom : bool) -> bits(4) = {
   } else set
 }
 
-/* For future versions of Sail where barriers can be parameterised */
-$ifdef FEATURE_UNION_BARRIER
-
 function clause execute (FENCE(pred, succ)) = {
   // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W.
   let fiom = is_fiom_active();
@@ -554,15 +551,15 @@ function clause execute (FENCE(pred, succ)) = {
   let succ = effective_fence_set(succ, fiom);
 
   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) => sail_barrier(Barrier_RISCV_rw_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_r_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_r_r),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_rw_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_w_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_w_rw),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_rw_r),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_r_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_w_r),
 
     (_ : bits(4)       , _ : bits(2) @ 0b00) => (),
     (_ : bits(2) @ 0b00, _ : bits(4)       ) => (),
@@ -573,36 +570,6 @@ function clause execute (FENCE(pred, succ)) = {
   RETIRE_SUCCESS
 }
 
-$else
-
-function clause execute (FENCE(pred, succ)) = {
-  // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W.
-  let fiom = is_fiom_active();
-  let pred = effective_fence_set(pred, fiom);
-  let succ = effective_fence_set(succ, fiom);
-
-  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(4)       , _ : bits(2) @ 0b00) => (),
-    (_ : bits(2) @ 0b00, _ : bits(4)       ) => (),
-
-    _ => { print("FIXME: unsupported fence");
-           () }
-  };
-  RETIRE_SUCCESS
-}
-
-$endif
-
 mapping bit_maybe_r : bits(1) <-> string = {
   0b1 <-> "r",
   0b0 <-> ""
@@ -636,24 +603,9 @@ union clause ast = FENCE_TSO : (bits(4), bits(4))
 mapping clause encdec = FENCE_TSO(pred, succ)
   <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
-$ifdef FEATURE_UNION_BARRIER
-
-function clause execute (FENCE_TSO(pred, succ)) = {
-  match (pred, succ) {
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso()),
-    (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
-
-    _ => { print("FIXME: unsupported fence");
-           () }
-  };
-  RETIRE_SUCCESS
-}
-
-$else
-
 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) => sail_barrier(Barrier_RISCV_tso),
     (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
     _ => { print("FIXME: unsupported fence");
@@ -662,8 +614,6 @@ function clause execute (FENCE_TSO(pred, succ)) = {
   RETIRE_SUCCESS
 }
 
-$endif
-
 mapping clause assembly = FENCE_TSO(pred, succ)
   <-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)
 
diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail
index d3e54e5..a17e86d 100644
--- a/model/riscv_pc_access.sail
+++ b/model/riscv_pc_access.sail
@@ -22,6 +22,7 @@ function get_next_pc() = nextPC
 
 val set_next_pc : xlenbits -> unit
 function set_next_pc(pc) = {
+  sail_branch_announce(sizeof(xlen), pc);
   nextPC = pc
 }
 
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 012f63b..69d2b8c 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -47,6 +47,7 @@ function step(step_no : int) -> bool = {
           },
           /* non-error cases: */
           F_RVC(h) => {
+            sail_instr_announce(h);
             instbits = zero_extend(h);
             let ast = ext_decode_compressed(h);
             if   get_config_print_instr()
@@ -63,6 +64,7 @@ function step(step_no : int) -> bool = {
              }
           },
           F_Base(w) => {
+            sail_instr_announce(w);
             instbits = zero_extend(w);
             let ast = ext_decode(w);
             if   get_config_print_instr()
@@ -96,7 +98,10 @@ function loop () : unit -> unit = {
   step_no : int = 0;
   while not(htif_done) do {
     let stepped = step(step_no);
-    if stepped then step_no = step_no + 1;
+    if stepped then {
+      step_no = step_no + 1;
+      sail_end_cycle()
+    };
 
     /* check htif exit */
     if htif_done then {