diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-07-09 15:47:38 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-07-09 15:47:38 -0700 |
| commit | b6b1b31e48706adfa4795a84519df0aa792f4474 (patch) | |
| tree | e78fb3c2e2395c5019d2f7bcc67d52e0fa853798 | |
| parent | 9ccecb30e1412566cfae99747945ae88d5cd433b (diff) | |
| download | sail-riscv-b6b1b31e48706adfa4795a84519df0aa792f4474.zip sail-riscv-b6b1b31e48706adfa4795a84519df0aa792f4474.tar.gz sail-riscv-b6b1b31e48706adfa4795a84519df0aa792f4474.tar.bz2 | |
Move the get_config_ print defaults to the backend preludes, since it seems to get optimized out by sail, making the emulator the command-line options ineffective.
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 12 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 12 | ||||
| -rw-r--r-- | model/prelude.sail | 7 |
3 files changed, 24 insertions, 7 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index da6106d..e6991fd 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -71,6 +71,18 @@ let speculate_conditional_success () = excl_result () let match_reservation _ = true let cancel_reservation () = () +val get_config_print_instr : unit -> bool +let get_config_print_instr () = true + +val get_config_print_reg : unit -> bool +let get_config_print_reg () = true + +val get_config_print_mem : unit -> bool +let get_config_print_mem () = true + +val get_config_print_platform : unit -> bool +let get_config_print_platform () = true + val sys_enable_writable_misa : unit -> bool let sys_enable_writable_misa () = true declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 7715614..1391d47 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -67,6 +67,18 @@ let speculate_conditional_success () = excl_result () let match_reservation _ = true let cancel_reservation () = () +val get_config_print_instr : unit -> bool +let get_config_print_instr () = true + +val get_config_print_reg : unit -> bool +let get_config_print_reg () = true + +val get_config_print_mem : unit -> bool +let get_config_print_mem () = true + +val get_config_print_platform : unit -> bool +let get_config_print_platform () = true + val sys_enable_writable_misa : unit -> bool let sys_enable_writable_misa () = true declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` diff --git a/model/prelude.sail b/model/prelude.sail index 22d050f..5ec0b92 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -102,16 +102,9 @@ val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_en 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) |