RVWMO support via Sail concurrency interface

Makefile

@@ -107,16 +107,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))

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

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
 

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,28 +83,73 @@
    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.
    * FIXME: We should convert the external API for all backends
    * (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