Merge branch 'master-cleanup' into pmp

10 files changed, 104 insertions, 20 deletions

diff --git a/Makefile b/Makefile
index dfb699f..d7feecd 100644
--- a/Makefile
+++ b/Makefile
@@ -331,6 +331,13 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS)
 #LOC_FILES:=$(SAIL_SRCS) main.sail
 #include $(SAIL_DIR)/etc/loc.mk
 
+FORCE:
+
+SHARE_FILES:=$(wildcard model/*.sail) $(wildcard c_emulator/*.c) $(wildcard c_emulator/*.h)
+sail-riscv.install: FORCE
+	echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install
+	echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install
+
 opam-build:
 	$(MAKE) ARCH=64 c_emulator/riscv_sim_RV64
 	$(MAKE) ARCH=32 c_emulator/riscv_sim_RV32
diff --git a/c_emulator/riscv_prelude.c b/c_emulator/riscv_prelude.c
index 1621913..92f8415 100644
--- a/c_emulator/riscv_prelude.c
+++ b/c_emulator/riscv_prelude.c
@@ -30,3 +30,23 @@ unit print_platform(sail_string s)
   if (config_print_platform) printf("%s\n", s);
   return UNIT;
 }
+
+bool get_config_print_instr(unit u)
+{
+  return (config_print_instr) ? true : false;
+}
+
+bool get_config_print_reg(unit u)
+{
+  return (config_print_reg) ? true : false;
+}
+
+bool get_config_print_mem(unit u)
+{
+  return (config_print_mem_access) ? true : false;
+}
+
+bool get_config_print_platform(unit u)
+{
+  return (config_print_platform) ? true : false;
+}
diff --git a/c_emulator/riscv_prelude.h b/c_emulator/riscv_prelude.h
index a296c7e..da292fe 100644
--- a/c_emulator/riscv_prelude.h
+++ b/c_emulator/riscv_prelude.h
@@ -8,3 +8,8 @@ unit print_instr(sail_string s);
 unit print_reg(sail_string s);
 unit print_mem_access(sail_string s);
 unit print_platform(sail_string s);
+
+bool get_config_print_instr(unit u);
+bool get_config_print_reg(unit u);
+bool get_config_print_mem(unit u);
+bool get_config_print_platform(unit u);
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index af0df02..12c82ce 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -69,6 +69,26 @@ bool config_print_reg = true;
 bool config_print_mem_access = true;
 bool config_print_platform = true;
 
+void set_config_print(char *var, bool val) {
+  if (strcmp("instr", optarg) == 0) {
+    config_print_instr = val;
+  } else if (strcmp("reg", optarg) == 0) {
+    config_print_reg = val;
+  } else if (strcmp("mem", optarg) == 0) {
+    config_print_mem_access = val;
+  } else if (strcmp("platform", optarg) == 0) {
+    config_print_platform = val;
+  } else if (strcmp("all", optarg) == 0) {
+    config_print_instr = val;
+    config_print_mem_access = val;
+    config_print_reg = val;
+    config_print_platform = val;
+  } else {
+    fprintf(stderr, "Unknown trace category: %s (should be instr|reg|mem|platform|all)\n", var);
+    exit(1);
+  }
+}
+
 struct timeval init_start, init_end, run_end;
 int total_insns = 0;
 
@@ -89,6 +109,8 @@ static struct option options[] = {
   {"rvfi-dii",                    required_argument, 0, 'r'},
 #endif
   {"help",                        no_argument,       0, 'h'},
+  {"trace",                       required_argument, 0, 'v'},
+  {"no-trace",                    required_argument, 0, 'V'},
   {0, 0, 0, 0}
 };
 
@@ -172,7 +194,7 @@ char *process_args(int argc, char **argv)
   int c, idx = 1;
   uint64_t ram_size = 0;
   while(true) {
-    c = getopt_long(argc, argv, "admCIispz:b:t:v:hr:T:", options, &idx);
+    c = getopt_long(argc, argv, "admCIispz:b:t:v:hr:T:V:v:", options, &idx);
     if (c == -1) break;
     switch (c) {
     case 'a':
@@ -241,6 +263,12 @@ char *process_args(int argc, char **argv)
       fprintf(stderr, "using %d as RVFI port.\n", rvfi_dii_port);
       break;
 #endif
+    case 'V':
+      set_config_print(optarg, false);
+      break;
+    case 'v':
+      set_config_print(optarg, true);
+      break;
     }
   }
   if (do_dump_dts) dump_dts();
@@ -582,10 +610,12 @@ int compare_states(struct tv_spike_t *s)
 
 void flush_logs(void)
 {
-  fprintf(stderr, "\n");
-  fflush(stderr);
-  fprintf(stdout, "\n");
-  fflush(stdout);
+  if(config_print_instr) {
+    fprintf(stderr, "\n");
+    fflush(stderr);
+    fprintf(stdout, "\n");
+    fflush(stdout);
+  }
 }
 
 #ifdef RVFI_DII
diff --git a/model/prelude.sail b/model/prelude.sail
index 81aea14..4c232e4 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -79,7 +79,7 @@ val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", le
 /* 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
+val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat
 
 val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int
 
@@ -101,6 +101,18 @@ val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline",
 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
 
+val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
+function get_config_print_instr () -> bool = false
+
+val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
+function get_config_print_reg () -> bool = false
+
+val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
+function get_config_print_mem () -> bool = false
+
+val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
+function get_config_print_platform () -> bool = false
+
 $ifndef FEATURE_IMPLICITS
 val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
 val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
@@ -111,13 +123,10 @@ val zeros_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
 function zeros_implicit () = sail_zeros('n)
 overload zeros = {zeros_implicit, sail_zeros}
 
-val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n)
-function ones_n n = replicate_bits (0b1, n)
-
 val ones_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
-function ones_implicit () = ones_n ('n)
+function ones_implicit () = sail_ones ('n)
 
-overload ones = {ones_implicit, ones_n}
+overload ones = {ones_implicit, sail_ones}
 
 $else
 val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
@@ -130,13 +139,10 @@ val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function zeros_implicit (n) = sail_zeros(n)
 overload zeros = {zeros_implicit, sail_zeros}
 
-val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n)
-function ones_n n = replicate_bits (0b1, n)
-
 val ones_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
-function ones_implicit (n) = ones_n (n)
+function ones_implicit (n) = sail_ones (n)
 
-overload ones = {ones_implicit, ones_n}
+overload ones = {ones_implicit, sail_ones}
 
 $endif
 
diff --git a/model/prelude_mapping.sail b/model/prelude_mapping.sail
index e40edbf..070c4cb 100644
--- a/model/prelude_mapping.sail
+++ b/model/prelude_mapping.sail
@@ -1,5 +1,11 @@
 /* Some helper functions for the assembler mappings. */
 
+/* These mappings produce a lot of pattern match warnings that are not useful. 
+   The following directive suppresses them (and will be ignored by older versions of Sail 
+   with one additional warning). Would be better to fix the warnings properly but I don't
+   know how. */
+$suppress_warnings
+
 /* Python:
 f = """val hex_bits_{0} : bits({0}) <-> string
 val hex_bits_{0}_forwards = "decimal_string_of_bits" : bits({0}) -> string
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 4b5c1c5..12c8522 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -31,7 +31,9 @@ function step(step_no) = {
           /* non-error cases: */
           F_RVC(h) => {
             let ast = decodeCompressed(h);
-            print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
+            if get_config_print_instr() then {
+              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
+            };
             /* check for RVC once here instead of every RVC execute clause. */
             if haveRVC() then {
               nextPC = PC + 2;
@@ -43,7 +45,9 @@ function step(step_no) = {
           },
           F_Base(w) => {
             let ast = decode(w);
-            print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
+            if get_config_print_instr() then {
+              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
+            };
             nextPC = PC + 4;
             (execute(ext_post_decode_hook(ast)), true)
           }
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index f4a8a3c..b2a19fe 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -40,6 +40,11 @@ let print_platform s =
   then print_endline s
   else ()
 
+let get_config_print_instr () = !config_print_instr
+let get_config_print_reg () = !config_print_reg
+let get_config_print_mem () = !config_print_mem_access
+let get_config_print_platform () = !config_print_platform
+
 (* Mapping to Sail externs *)
 let cur_arch_bitwidth () =
   match !platform_arch with
diff --git a/opam b/opam
index e3b2f91..fb65f9a 100644
--- a/opam
+++ b/opam
@@ -1,6 +1,6 @@
 opam-version: "1.2"
 name: "sail-riscv"
-version: "0.2"
+version: "0.3"
 maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>"
 authors: [
   "Alasdair Armstrong"
diff --git a/sail-riscv.install b/sail-riscv.install
index 63d985a..ce50f55 100644
--- a/sail-riscv.install
+++ b/sail-riscv.install
@@ -1 +1,2 @@
-bin: ["c_emulator/riscv_sim_RV32" "c_emulator/riscv_sim_RV64"]
+bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]
+share: [ "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/prelude_mapping.sail" {"model/prelude_mapping.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/riscv_duopod.sail" {"model/riscv_duopod.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/main.sail" {"model/main.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} ]