Interpreter, RISC-V: move memory actions to parts of the interpreter response and refactor RISC-V model accordingly

2 files changed, 19 insertions, 0 deletions

diff --git a/lib/regfp.sail b/lib/regfp.sail
index fcf10850..d69728df 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -1,3 +1,6 @@
+$ifndef _REGFP
+$define _REGFP
+
 /* iR : input registers,
  * oR : output registers,
  * aR : registers feeding into the memory address */
@@ -98,3 +101,17 @@ union instruction_kind = {
   IK_trans : trans_kind,
   IK_simple : unit
 }
+
+val __read_mem = { ocaml: "Platform.read_mem", _: "read_mem" } : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem}
+val __write_ea = { ocaml: "Platform.write_ea", _: "write_ea" } : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem}
+val __write_memv = { ocaml: "Platform.write_memv", _: "write_memv" } : forall 'n, 'n > 0. bits('n) -> bool effect {wmv}
+val __excl_res = { ocaml: "Platform.excl_res", _: "excl_res" }: unit -> bool effect {exmem}
+val __barrier = { ocaml: "Platform.barrier", _: "barrier" } : barrier_kind -> unit effect {barr}
+
+val __write_mem : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}
+function __write_mem (wk, addr, len, value) = {
+  __write_ea(wk, addr, len);
+  __write_memv(value)
+}
+
+$endif
diff --git a/lib/sail.h b/lib/sail.h
index 4ccd8b93..a1c5b270 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -329,6 +329,8 @@ void string_length(sail_int *len, sail_string s);
 void string_drop(sail_string *dst, sail_string s, sail_int len);
 void string_take(sail_string *dst, sail_string s, sail_int len);
 
+void opt_spc_matches_prefix(zoption *dst, sail_string s);
+
 /* ***** Printing ***** */
 
 void string_of_int(sail_string *str, const sail_int i);