Merge branch 'master' into rmem_interpreterrmem_interpreter

5 files changed, 48 insertions, 43 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index 73f96b0..457c4d4 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -1,5 +1,6 @@
 default Order dec
 
+$include <smt.sail>
 $include <option.sail>
 $include <arith.sail>
 $include <string.sail>
@@ -84,9 +85,8 @@ overload operator - = {sub_vec, sub_vec_int}
 val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int
 val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
 
-val modulus = {lem: "hardware_mod"} : (int, int) -> int
-
-overload operator % = {modulus}
+/* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */
+overload operator % = {emod_int, mod}
 
 val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat
 
@@ -105,10 +105,10 @@ val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
 val print = "print_endline" : string -> unit
 val print_string = "print_string" : (string, string) -> unit
 
-val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", _: "print_endline"} : string -> unit
-val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline",   c: "print_reg", _: "print_endline"} : string -> unit
-val print_mem      = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", _: "print_endline"} : string -> unit
-val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", _: "print_endline"} : string -> unit
+val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_mem      = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
 
 $ifndef FEATURE_IMPLICITS
 val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 8e483f8..b6fa0bc 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -2,22 +2,22 @@
  * They depend on the XLEN of the architecture.
  */
 
-val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM = {lem: "MEMw", coq: "MEMw", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_release = {lem: "MEMw_release", coq: "MEMw_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_strong_release = {lem: "MEMw_strong_release", coq: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional = {lem: "MEMw_conditional", coq: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", coq: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", coq: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
 val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
@@ -36,22 +36,22 @@ function __RISCV_write (addr, width, data, aq, rl, con) =
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
 
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM = { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_acquire = { lem: "MEMr_acquire", coq: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", coq: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved = { lem: "MEMr_reserved", coq: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", coq: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", coq: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
 val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index 70d4978..4986278 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -150,13 +150,8 @@ mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
   <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
       if rsd != zreg & sizeof(xlen) == 64
 
-function clause execute (C_ADDIW(imm, rsd)) = {
-  let imm : bits(32) = EXTS(imm);
-  let rs_val = X(rsd);
-  let res : bits(32) = rs_val[31..0] + imm;
-  X(rsd) = EXTS(res);
-  true
-}
+function clause execute (C_ADDIW(imm, rsd)) =
+  execute(ADDIW(EXTS(imm), rsd, rsd))
 
 mapping clause assembly = C_ADDIW(imm, rsd)
       if sizeof(xlen) == 64
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 2f02839..4155d66 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -415,18 +415,19 @@ function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
 
 /* state state initialization */
 
+val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
 function init_sys() -> unit = {
   cur_privilege = Machine;
 
   mhartid     = EXTZ(0b0);
 
   misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64);
-  misa->A()   = true; /* atomics */
-  misa->C()   = true; /* RVC */
-  misa->I()   = true; /* base integer ISA */
-  misa->M()   = true; /* integer multiply/divide */
-  misa->U()   = true; /* user-mode */
-  misa->S()   = true; /* supervisor-mode */
+  misa->A()   = true;               /* atomics */
+  misa->C()   = sys_enable_rvc ();  /* RVC */
+  misa->I()   = true;               /* base integer ISA */
+  misa->M()   = true;               /* integer multiply/divide */
+  misa->U()   = true;               /* user-mode */
+  misa->S()   = true;               /* supervisor-mode */
 
   mstatus = set_mstatus_SXL(mstatus, misa.MXL());
   mstatus = set_mstatus_UXL(mstatus, misa.MXL());
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 439d12d..fb8a994 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -70,13 +70,19 @@ bitfield Misa : xlenbits = {
 }
 register misa : Misa
 
+val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
+
+/* We currently only support dynamic changes for the C extension. */
 function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
-  /* Allow modifications to C. */
-  let v = Mk_Misa(v);
-  // Suppress changing C if nextPC would become misaligned.
-  if   v.C() == false & nextPC[1] == true
-  then m
-  else update_C(m, v.C())
+  if   sys_enable_writable_misa ()
+  then { /* Allow modifications to C only for now. */
+         let  v = Mk_Misa(v);
+         /* Suppress changing C if nextPC would become misaligned. */
+         if   v.C() == false & nextPC[1] == true
+         then m
+         else update_C(m, v.C())
+       }
+  else m
 }
 
 /* helpers to check support for various extensions. */
@@ -319,12 +325,15 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
 
 register mepc : xlenbits
 
-// legalizing writes to xepc
-function legalize_xepc(v : xlenbits) -> xlenbits = {
-  v & EXTS(if haveRVC() then 0b110 else 0b100)
-}
+/* The xepc legalization zeroes xepc[1:0] when misa.C is hardwired to 0.
+ * When misa.C is writable, it zeroes only xepc[0].
+ */
+function legalize_xepc(v : xlenbits) -> xlenbits =
+  if   sys_enable_writable_misa () | misa.C() == true
+  then [v with 0 = bitzero]
+  else v & EXTS(0b100)
 
-// masking for reads to xepc
+/* masking for reads to xepc */
 function pc_alignment_mask() -> xlenbits =
   ~(EXTZ(if misa.C() == true then 0b00 else 0b10))