diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-07-11 11:33:24 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-07-11 11:33:24 -0700 |
| commit | e2c413be2bbbb6745978bb4437d23279262ddeeb (patch) | |
| tree | ff7d136948f295cdae0517fd770518ddeceeb0f8 | |
| parent | c01474489b68fc9e6aa4a96295db03df3dcc99a6 (diff) | |
| download | sail-riscv-e2c413be2bbbb6745978bb4437d23279262ddeeb.zip sail-riscv-e2c413be2bbbb6745978bb4437d23279262ddeeb.tar.gz sail-riscv-e2c413be2bbbb6745978bb4437d23279262ddeeb.tar.bz2 | |
Undo get_config workarounds.
| -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 | 14 |
3 files changed, 10 insertions, 28 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index e6991fd..da6106d 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -71,18 +71,6 @@ 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 1391d47..7715614 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -67,18 +67,6 @@ 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 63c896c..c67ec3c 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -101,10 +101,16 @@ 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", _:"get_config_print_instr"} : unit -> bool -val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", _:"get_config_print_reg"} : unit -> bool -val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", _:"get_config_print_mem"} : unit -> bool -val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", _:"get_config_print_platform"} : unit -> bool +val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool +val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool +val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool + +val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool +// defaults for other backends +function get_config_print_instr () = false +function get_config_print_reg () = false +function get_config_print_mem () = false +function get_config_print_platform () = false val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) |