Remove the OCaml emulator

This has the following benefits:

* Reduces the maintenance burden for making changes to the emulator. They don't have to be done in two places and you don't need to learn OCaml.
* Removes the dependency on OCaml and OPAM, which is a weirdly bug-prone tool.
* Removes confusion for new users about which emulator to use.
* Shorter CI time.

It removed two capabilities which were deemed to be acceptable for now:

* Unlike the OCaml emulator the C emulator cannot dynamically generate a Device Tree Blob based on the options you give it. However this would be relatively easy to add back if anyone needs it - it just involves making a templated DTS and then running it through `dtc`. You can also just do that manually for now.
* Unlike the C code the OCaml Sail code has the ability to generate random instructions which was maybe once used by TestRig but they no longer use it.

Fixes #509

22 files changed, 133 insertions, 1534 deletions

diff --git a/CODE_STYLE.md b/CODE_STYLE.md
index 4463e3a..f4eef22 100644
--- a/CODE_STYLE.md
+++ b/CODE_STYLE.md
@@ -6,7 +6,7 @@ RISC-V Sail model.
 Where something is not specified, please look for existing code similar to what
 is being added and copy the predominant style.
 
-For C and OCaml, the formatting rules should be followed where applicable.
+For C the formatting rules should be followed where applicable.
 For other languages, follow the standard style for that language if it exists;
 for example, Python should follow the standard PEP-8 style.
 
@@ -86,7 +86,7 @@ Implementation
 * Do not use strings for anything that is not text
 
 * No new compile-time warnings from the Sail compiler should be introduced
-  (this does not include C or OCaml warnings for the code generated by the Sail
+  (this does not include C warnings for the code generated by the Sail
   compiler)
 
 * Do not use the `ext*` types and hooks for standard extensions unless
diff --git a/Dockerfile b/Dockerfile
deleted file mode 100644
index ed27b8c..0000000
--- a/Dockerfile
+++ /dev/null
@@ -1,5 +0,0 @@
-FROM ocaml/opam
-USER root
-RUN DEBIAN_FRONTEND=noninteractive apt-get -y install zlib1g-dev pkg-config libgmp-dev z3
-USER opam
-RUN opam install sail
diff --git a/Makefile b/Makefile
index f19b6d5..34fd2bf 100644
--- a/Makefile
+++ b/Makefile
@@ -128,8 +128,6 @@ SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(S
 SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS))
 SAIL_COQ_SRCS  = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS))
 
-PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml)
-
 SAIL_FLAGS += --require-version 0.18
 SAIL_FLAGS += --strict-var
 SAIL_FLAGS += -dno_cast
@@ -208,7 +206,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
 
 .PHONY:
 
-all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH)
+all: c_emulator/riscv_sim_$(ARCH)
 .PHONY: all
 
 # the following ensures empty sail-generated .c files don't hang around and
@@ -230,44 +228,12 @@ riscv.smt_model: $(SAIL_SRCS)
 cgen: $(SAIL_SRCS) model/main.sail
 	$(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
-generated_definitions/ocaml/$(ARCH)/riscv.ml: $(SAIL_SRCS) Makefile
-	mkdir -p generated_definitions/ocaml/$(ARCH)
-	$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml/$(ARCH) -o riscv $(SAIL_SRCS)
-
-# cp -f is required because the generated_definitions/ocaml/$ARCH/*.ml files can
-# be read-only, which would otherwise make subsequent builds fail.
-ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) Makefile
-	mkdir -p ocaml_emulator/_sbuild
-	cp ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild
-	cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild
-	cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native
-
-ocaml_emulator/_sbuild/coverage.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile
-	mkdir -p ocaml_emulator/_sbuild
-	cp $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild
-	cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild
-	cp ocaml_emulator/_tags.bisect ocaml_emulator/_sbuild/_tags
-	cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native && cp -L riscv_ocaml_sim.native coverage.native
-
-ocaml_emulator/riscv_ocaml_sim_$(ARCH): ocaml_emulator/_sbuild/riscv_ocaml_sim.native
-	rm -f $@ && cp -L $^ $@ && rm -f $^
-
-ocaml_emulator/coverage_$(ARCH): ocaml_emulator/_sbuild/coverage.native
-	rm -f ocaml_emulator/riscv_ocaml_sim_$(ARCH) && cp -L $^ ocaml_emulator/riscv_ocaml_sim_$(ARCH) # since the test scripts runs this file
-	rm -rf bisect*.out bisect ocaml_emulator/coverage_$(ARCH) $^
-	./test/run_tests.sh # this will generate bisect*.out files in this directory
-	mkdir ocaml_emulator/bisect && mv bisect*.out bisect/
-	mkdir ocaml_emulator/coverage_$(ARCH) && bisect-ppx-report -html ocaml_emulator/coverage_$(ARCH)/ -I ocaml_emulator/_sbuild/ bisect/bisect*.out
-
 cloc:
 	cloc --by-file --force-lang C,sail $(SAIL_SRCS)
 
 gcovr:
 	gcovr -r . --html --html-detail -o index.html
 
-ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml
-	ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@
-
 c_preserve_fns=-c_preserve _set_Misa_C
 
 generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
@@ -284,8 +250,6 @@ $(SOFTFLOAT_LIBS):
 # convenience target
 .PHONY: csim
 csim: c_emulator/riscv_sim_$(ARCH)
-.PHONY: osim
-osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH)
 .PHONY: rvfi
 rvfi: c_emulator/riscv_rvfi_$(ARCH)
 
@@ -470,29 +434,12 @@ 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
-	$(MAKE) riscv_rmem
-
-opam-install:
-	if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi
-	mkdir -p $(INSTALL_DIR)/bin
-	cp c_emulator/riscv_sim_RV64 $(INSTALL_DIR)/bin
-	cp c_emulator/riscv_sim_RV32 $(INSTALL_DIR)/bin
-
-opam-uninstall:
-	if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi
-	rm $(INSTALL_DIR)/bin/riscv_sim_RV64
-	rm $(INSTALL_DIR)/bin/riscv_sim_RV32
-
 clean:
-	-rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/*
+	-rm -rf generated_definitions/c/* generated_definitions/latex/*
 	-rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/*
 	-rm -rf generated_definitions/for-rmem/*
 	-$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean
 	-rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64  c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64
-	-rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp
 	-rm -f *.gcno *.gcda
 	-rm -f z3_problems
 	-Holmake cleanAll
@@ -500,4 +447,3 @@ clean:
 	-rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.vos handwritten_support/mem_metadata.vok handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux
 	-rm -f sail_doc/riscv_RV32.json
 	-rm -f sail_doc/riscv_RV64.json
-	ocamlbuild -clean
diff --git a/README.md b/README.md
index d6259c6..79ca3f6 100644
--- a/README.md
+++ b/README.md
@@ -36,7 +36,7 @@ What is Sail?
 engineer-friendly language, much like earlier vendor pseudocode, but more precisely defined and with tooling to support a wide range of use-cases.
 <p>
 
-Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate executable emulators (in C or OCaml), show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate  theorem-prover definitions for
+Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate executable emulators, show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate  theorem-prover definitions for
 interactive proof (in Isabelle, HOL4, and Coq), support proof about binary code (in Islaris), and (in progress) generate a reference ISA model in SystemVerilog that can be used for formal hardware verification.
 <p>
 
@@ -139,13 +139,9 @@ mapping clause assembly = SRET() <-> "sret"
 Sequential execution
 ----------
 
-The model builds OCaml and C emulators that can execute RISC-V ELF
+The model builds a C emulator that can execute RISC-V ELF
 files, and both emulators provide platform support sufficient to boot
-Linux, FreeBSD and seL4.  The OCaml emulator can generate its own
-platform device-tree description, while the C emulator currently
-requires a consistent description to be manually provided.  The C
-emulator can be linked against the Spike emulator for execution with
-per-instruction tandem-verification.
+Linux, FreeBSD and seL4. The C emulator can be linked against the Spike emulator for execution with per-instruction tandem-verification.
 
 The C emulator, for the Linux boot, currently runs at approximately
 300 KIPS on an Intel i7-7700 (when detailed per-instruction tracing
@@ -154,8 +150,8 @@ is disabled), and there are many opportunities for future optimisation
 boot Linux in about 4 minutes, and FreeBSD in about 2 minutes. Memory
 usage for the C emulator when booting Linux is approximately 140MB.
 
-The files in the OCaml and C emulator directories implement ELF loading and the
-platform devices, define the physical memory map, and use command-line
+The files in the C emulator directory implements ELF loading and the
+platform devices, defines the physical memory map, and usees command-line
 options to select implementation-specific ISA choices.
 
 
@@ -208,19 +204,6 @@ Those tests have also been run on RISC-V hardware, on a SiFive RISC-V
 FU540 multicore proto board (Freedom Unleashed), kindly on loan from
 Imperas. To date, only sequentially consistent behaviour was observed there.
 
-
-
-Use in test generation
-----------------------
-
-The Sail OCaml backend can produce QuickCheck-style random generators for
-types in Sail specifications, which have been used to produce random
-instructions sequences for testing.  The generation of individual
-types can be overridden by the developer to, for example, remove
-implementation-specific instructions or introduce register biasing.
-
-
-
 Generating theorem-prover definitions
 --------------------------------------
 
@@ -254,7 +237,6 @@ sail-riscv
 - model                   // Sail specification modules
 - generated_definitions   // files generated by Sail, in RV32 and RV64 subdirectories
   -  c
-  -  ocaml
   -  lem
   -  isabelle
   -  coq
@@ -263,7 +245,6 @@ sail-riscv
 - prover_snapshots        // snapshots of generated theorem prover definitions
 - handwritten_support     // prover support files
 - c_emulator              // supporting platform files for C emulator
-- ocaml_emulator          // supporting platform files for OCaml emulator
 - doc                     // documentation, including a reading guide
 - test                    // test files
   - riscv-tests           // snapshot of tests from the riscv/riscv-tests github repo
@@ -280,9 +261,8 @@ Install [Sail](https://github.com/rems-project/sail/) [using opam](https://githu
 ```
 $ make
 ```
-will build the 64-bit OCaml simulator in
-`ocaml_emulator/riscv_ocaml_sim_RV64` and the C simulator in
-`c_emulator/riscv_sim_RV64`.
+
+will build the C simulator in `c_emulator/riscv_sim_RV64`.
 
 If you get an error message saying `sail: unknown option '--require-version'.` it's because your Sail compiler is too old. You need version 0.18 or later.
 
@@ -295,9 +275,7 @@ built using:
 $ ARCH=RV32 make
 ```
 
-which creates the 32-bit OCaml simulator in
-`ocaml_emulator/riscv_ocaml_sim_RV32` and the C simulator in
-`c_emulator/riscv_sim_RV32`.
+which creates the C simulator in `c_emulator/riscv_sim_RV32`.
 
 The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and
 `riscv_hol_build` invoke the respective prover to process the
@@ -313,19 +291,9 @@ corresponding prover libraries in the Sail directory
 
 ### Executing test binaries
 
-The C and OCaml simulators can be used to execute small test binaries.  The
-OCaml simulator depends on the Device Tree Compiler package, which can be
-installed in Ubuntu with:
-
-```
-$ sudo apt-get install device-tree-compiler
-```
-
-Then, you can run test binaries:
-
+The C simulator can be used to execute small test binaries.
 
 ```
-$ ./ocaml_emulator/riscv_ocaml_sim_<arch>  <elf-file>
 $ ./c_emulator/riscv_sim_<arch> <elf-file>
 ```
 
@@ -337,17 +305,11 @@ can be run using `test/run_tests.sh`.
 ### Configuring platform options
 
 Some information on additional configuration options for each
-simulator is available from `./ocaml_emulator/riscv_ocaml_sim_<arch>
--h` and `./c_emulator/riscv_sim_<arch> -h`.
+simulator is available from `./c_emulator/riscv_sim_<arch> -h`.
 
 Some useful options are: configuring whether misaligned accesses trap
-(`--enable-misaligned` for C and `-enable-misaligned` for OCaml), and
-whether page-table walks update PTE bits (`--enable-dirty-update` for C
-and `-enable-dirty-update` for OCaml).
-
-### Experimental integration with riscv-config
-
-There is also (as yet unmerged) support for [integration with riscv-config](https://github.com/rems-project/sail-riscv/pull/43) to allow configuring the compiled model according to a riscv-config yaml specification.
+(`--enable-misaligned`), and
+whether page-table walks update PTE bits (`--enable-dirty-update`).
 
 ### Booting OS images
 
@@ -363,26 +325,12 @@ Licence
 
 The model is made available under the BSD two-clause licence in LICENCE.
 
-
 Authors
 -------
 
- Prashanth Mundkur, SRI International;
- Rishiyur S. Nikhil (Bluespec Inc.);
- Jon French, University of Cambridge;
- Brian Campbell, University of Edinburgh;
- Robert Norton-Wright, University of Cambridge and Microsoft;
- Alasdair Armstrong, University of Cambridge;
- Thomas Bauereiss, University of Cambridge;
- Shaked Flur, University of Cambridge;
- Christopher Pulte, University of Cambridge;
- Peter Sewell, University of Cambridge;
- Alexander Richardson, University of Cambridge;
- Hesham Almatary, University of Cambridge;
- Jessica Clarke, University of Cambridge;
- Nathaniel Wesley Filardo, Microsoft;
- Peter Rugg, University of Cambridge;
- Scott Johnson, Aril Computer Corp.
+Originally written by Prashanth Mundkur at SRI International, and further developed by others, especially researchers at the University of Cambridge.
+
+See `LICENCE` and Git blame for a complete list of authors.
 
 Funding
 -------
diff --git a/build_simulators.sh b/build_simulators.sh
index 8ad23e0..8fb7641 100755
--- a/build_simulators.sh
+++ b/build_simulators.sh
@@ -10,8 +10,5 @@ function test_build () {
     fi
 }
 
-test_build make ARCH=RV32 ocaml_emulator/riscv_ocaml_sim_RV32
-test_build make ARCH=RV64 ocaml_emulator/riscv_ocaml_sim_RV64
-
 test_build make ARCH=RV32 c_emulator/riscv_sim_RV32
 test_build make ARCH=RV64 c_emulator/riscv_sim_RV64
diff --git a/doc/ExtendingGuide.md b/doc/ExtendingGuide.md
index b32b9a9..c00683b 100644
--- a/doc/ExtendingGuide.md
+++ b/doc/ExtendingGuide.md
@@ -60,7 +60,7 @@ construct of the Sail language. `riscv_platform.sail` can be examined
 to see how this is done for the SiFive core-local interrupt (CLINT)
 controller, the HTIF timer and terminal devices.  The
 implementation of the actual functionality provided by these MMIO
-devices would need to be added to the C and OCaml emulators.
+devices would need to be added to the C emulators.
 
 If this functionality requires the definition of new interrupt
 sources, their encodings would need to be added to `riscv_types.sail`,
diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md
index 5c8d0f6..bf64793 100644
--- a/doc/ReadingGuide.md
+++ b/doc/ReadingGuide.md
@@ -63,12 +63,12 @@ such as the platform memory map.
   controller, and the MMIO interfaces to the clock, timer and terminal
   devices.  Sail `extern` definitions are used to connect externally
   provided (i.e. external to the Sail model) platform functionality,
-  such as those provided by the platform support in the C and OCaml
-  emulators.  This file also contains the externally selectable
+  such as those provided by the platform support in the C
+  emulator.  This file also contains the externally selectable
   options for platform behavior, such as the handling of misaligned
   memory accesses, the handling of PTE dirty-bit updates during
   address translation, etc.  These platform options can be specified
-  via command line switches in the C and OCaml emulators.
+  via command line switches in the C emulator.
 
 - `riscv_mem.sail` contains the functions that convert accesses to
   physical addresses into accesses to physical memory, or MMIO
@@ -128,7 +128,7 @@ Structure of the C emulator
 ----------------------------
 
 The diagram below illustrates how the C emulator is built from the
-Sail model.  The OCaml emulator follows the same approach.
+Sail model.
 
 <img src="figs/riscvcsimdeps.svg">
 
diff --git a/model/prelude.sail b/model/prelude.sail
index a441e3a..34ff30e 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -47,8 +47,8 @@ val sub_vec_int = pure {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits(
 
 overload operator - = {sub_vec, sub_vec_int}
 
-val quot_round_zero = pure {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
-val rem_round_zero = pure {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
+val quot_round_zero = pure {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
+val rem_round_zero = pure {interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
 
 /* The following defines % as euclidean modulus */
 overload operator % = {emod_int}
@@ -58,20 +58,20 @@ overload max = {max_int}
 
 val print_string = pure "print_string" : (string, string) -> unit
 
-val print_instr    = pure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_reg      = pure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_mem      = pure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_platform = pure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_instr    = pure {interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_reg      = pure {interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_mem      = pure {interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_platform = pure {interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
 
-val print_step = pure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit
+val print_step = pure {c: "print_step"} : unit -> unit
 
 function print_step() = ()
 
-val get_config_print_instr = pure {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
-val get_config_print_reg = pure {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
-val get_config_print_mem = pure {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
+val get_config_print_instr = pure {c:"get_config_print_instr"} : unit -> bool
+val get_config_print_reg = pure {c:"get_config_print_reg"} : unit -> bool
+val get_config_print_mem = pure {c:"get_config_print_mem"} : unit -> bool
 
-val get_config_print_platform = pure {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
+val get_config_print_platform = pure {c:"get_config_print_platform"} : unit -> bool
 // defaults for other backends
 function get_config_print_instr () = false
 function get_config_print_reg () = false
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index b7a498c..6155e1c 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -15,13 +15,11 @@
 */
 
 val elf_tohost = pure {
-  ocaml: "Elf_loader.elf_tohost",
   interpreter: "Elf_loader.elf_tohost",
   c: "elf_tohost"
 } :  unit -> int
 
 val elf_entry = pure {
-  ocaml: "Elf_loader.elf_entry",
   interpreter: "Elf_loader.elf_entry",
   c: "elf_entry"
 } : unit -> int
@@ -29,42 +27,39 @@ val elf_entry = pure {
 // Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096)
 // because this model performs `cbo.zero` with a single write, and the behaviour
 // with cache blocks larger than a page is not clearly defined.
-val plat_cache_block_size_exp = pure {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12)
+val plat_cache_block_size_exp = pure {c: "plat_cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12)
 
 /* Main memory */
-val plat_ram_base = pure {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
-val plat_ram_size = pure {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
+val plat_ram_base = pure {c: "plat_ram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
+val plat_ram_size = pure {c: "plat_ram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
 
 /* whether the MMU should update dirty bits in PTEs */
-val plat_enable_dirty_update = pure {ocaml: "Platform.enable_dirty_update",
-                                     interpreter: "Platform.enable_dirty_update",
+val plat_enable_dirty_update = pure {interpreter: "Platform.enable_dirty_update",
                                      c: "plat_enable_dirty_update",
                                      lem: "plat_enable_dirty_update"} : unit -> bool
 
 /* whether the platform supports misaligned accesses without trapping to M-mode. if false,
  * misaligned loads/stores are trapped to Machine mode.
  */
-val plat_enable_misaligned_access = pure {ocaml: "Platform.enable_misaligned_access",
-                                          interpreter: "Platform.enable_misaligned_access",
+val plat_enable_misaligned_access = pure {interpreter: "Platform.enable_misaligned_access",
                                           c: "plat_enable_misaligned_access",
                                           lem: "plat_enable_misaligned_access"} : unit -> bool
 
 /* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */
-val plat_mtval_has_illegal_inst_bits = pure {ocaml: "Platform.mtval_has_illegal_inst_bits",
-                                             interpreter: "Platform.mtval_has_illegal_inst_bits",
+val plat_mtval_has_illegal_inst_bits = pure {interpreter: "Platform.mtval_has_illegal_inst_bits",
                                              c: "plat_mtval_has_illegal_inst_bits",
                                              lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool
 
 /* ROM holding reset vector and device-tree DTB */
-val plat_rom_base   = pure {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
-val plat_rom_size   = pure {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits
+val plat_rom_base   = pure {interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
+val plat_rom_size   = pure {interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits
 
 /* Location of clock-interface, which should match with the spec in the DTB */
-val plat_clint_base = pure {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits
-val plat_clint_size = pure {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits
+val plat_clint_base = pure {interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits
+val plat_clint_size = pure {interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits
 
 /* Location of HTIF ports */
-val plat_htif_tohost = pure {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits
+val plat_htif_tohost = pure {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits
 function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ())
 // todo: fromhost
 
@@ -124,7 +119,7 @@ function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen
 
 /* CLINT (Core Local Interruptor), based on Spike. */
 
-val plat_insns_per_tick = pure {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int
+val plat_insns_per_tick = pure {interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int
 
 // assumes a single hart, since this typically is a vector of per-hart registers.
 register mtimecmp : bits(64)  // memory-mapped internal clint register.
@@ -284,8 +279,8 @@ function tick_clock() = {
 
 /* Basic terminal character I/O. */
 
-val plat_term_write = impure {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit
-val plat_term_read  = impure {ocaml: "Platform.term_read",  c: "plat_term_read", lem: "plat_term_read"}  : unit -> bits(8)
+val plat_term_write = impure {c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit
+val plat_term_read  = impure {c: "plat_term_read", lem: "plat_term_read"}  : unit -> bits(8)
 
 /* Spike's HTIF device interface, which multiplexes the above MMIO devices. */
 
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 79a4678..fdf84db 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -47,84 +47,84 @@ register float_fflags : bits(64)
 /* **************************************************************** */
 /* ADD/SUB/MUL/DIV                                                  */
 
-val     extern_f16Add = pure {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Add = pure {c: "softfloat_f16add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit
 val      riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Add (rm, v1, v2) = {
   extern_f16Add(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f16Sub = pure {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Sub = pure {c: "softfloat_f16sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit
 val      riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Sub (rm, v1, v2) = {
   extern_f16Sub(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f16Mul = pure {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Mul = pure {c: "softfloat_f16mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit
 val      riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Mul (rm, v1, v2) = {
   extern_f16Mul(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f16Div = pure {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Div = pure {c: "softfloat_f16div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit
 val      riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Div (rm, v1, v2) = {
   extern_f16Div(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f32Add = pure {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Add = pure {c: "softfloat_f32add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit
 val      riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Add (rm, v1, v2) = {
   extern_f32Add(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f32Sub = pure {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Sub = pure {c: "softfloat_f32sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
 val      riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Sub (rm, v1, v2) = {
   extern_f32Sub(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f32Mul = pure {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Mul = pure {c: "softfloat_f32mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
 val      riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Mul (rm, v1, v2) = {
   extern_f32Mul(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f32Div = pure {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Div = pure {c: "softfloat_f32div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit
 val      riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Div (rm, v1, v2) = {
   extern_f32Div(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f64Add = pure {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Add = pure {c: "softfloat_f64add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit
 val      riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Add (rm, v1, v2) = {
   extern_f64Add(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f64Sub = pure {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Sub = pure {c: "softfloat_f64sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
 val      riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Sub (rm, v1, v2) = {
   extern_f64Sub(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f64Mul = pure {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Mul = pure {c: "softfloat_f64mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
 val      riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Mul (rm, v1, v2) = {
   extern_f64Mul(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f64Div = pure {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Div = pure {c: "softfloat_f64div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit
 val      riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Div (rm, v1, v2) = {
   extern_f64Div(rm, v1, v2);
@@ -134,21 +134,21 @@ function riscv_f64Div (rm, v1, v2) = {
 /* **************************************************************** */
 /* MULTIPLY-ADD                                                     */
 
-val     extern_f16MulAdd = pure {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit
+val     extern_f16MulAdd = pure {c: "softfloat_f16muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit
 val      riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16MulAdd (rm, v1, v2, v3) = {
   extern_f16MulAdd(rm, v1, v2, v3);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f32MulAdd = pure {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
+val     extern_f32MulAdd = pure {c: "softfloat_f32muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
 val      riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32MulAdd (rm, v1, v2, v3) = {
   extern_f32MulAdd(rm, v1, v2, v3);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f64MulAdd = pure {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
+val     extern_f64MulAdd = pure {c: "softfloat_f64muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
 val      riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64MulAdd (rm, v1, v2, v3) = {
   extern_f64MulAdd(rm, v1, v2, v3);
@@ -158,21 +158,21 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = {
 /* **************************************************************** */
 /* SQUARE ROOT                                                      */
 
-val     extern_f16Sqrt = pure {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit
+val     extern_f16Sqrt = pure {c: "softfloat_f16sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit
 val      riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Sqrt (rm, v) = {
   extern_f16Sqrt(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f32Sqrt = pure {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit
+val     extern_f32Sqrt = pure {c: "softfloat_f32sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit
 val      riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Sqrt (rm, v) = {
   extern_f32Sqrt(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f64Sqrt = pure {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit
+val     extern_f64Sqrt = pure {c: "softfloat_f64sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit
 val      riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Sqrt (rm, v) = {
   extern_f64Sqrt(rm, v);
@@ -182,56 +182,56 @@ function riscv_f64Sqrt (rm, v) = {
 /* **************************************************************** */
 /* CONVERSIONS                                                      */
 
-val     extern_f16ToI32 = pure {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToI32 = pure {c: "softfloat_f16toi32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit
 val      riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W)
 function riscv_f16ToI32 (rm, v) = {
   extern_f16ToI32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f16ToUi32 = pure {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToUi32 = pure {c: "softfloat_f16toui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit
 val      riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU)
 function riscv_f16ToUi32 (rm, v) = {
   extern_f16ToUi32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_i32ToF16 = pure {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit
+val     extern_i32ToF16 = pure {c: "softfloat_i32tof16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit
 val      riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H)
 function riscv_i32ToF16 (rm, v) = {
   extern_i32ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_ui32ToF16 = pure {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit
+val     extern_ui32ToF16 = pure {c: "softfloat_ui32tof16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit
 val      riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H)
 function riscv_ui32ToF16 (rm, v) = {
   extern_ui32ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f16ToI64 = pure {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToI64 = pure {c: "softfloat_f16toi64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit
 val      riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L)
 function riscv_f16ToI64 (rm, v) = {
   extern_f16ToI64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f16ToUi64 = pure {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToUi64 = pure {c: "softfloat_f16toui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit
 val      riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU)
 function riscv_f16ToUi64 (rm, v) = {
   extern_f16ToUi64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_i64ToF16 = pure {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit
+val     extern_i64ToF16 = pure {c: "softfloat_i64tof16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit
 val      riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H)
 function riscv_i64ToF16 (rm, v) = {
   extern_i64ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_ui64ToF16 = pure {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit
+val     extern_ui64ToF16 = pure {c: "softfloat_ui64tof16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit
 val      riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H)
 function riscv_ui64ToF16 (rm, v) = {
   extern_ui64ToF16(rm, v);
@@ -239,154 +239,154 @@ function riscv_ui64ToF16 (rm, v) = {
 }
 
 
-val     extern_f32ToI32 = pure {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToI32 = pure {c: "softfloat_f32toi32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
 val      riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W)
 function riscv_f32ToI32 (rm, v) = {
   extern_f32ToI32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f32ToUi32 = pure {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToUi32 = pure {c: "softfloat_f32toui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit
 val      riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU)
 function riscv_f32ToUi32 (rm, v) = {
   extern_f32ToUi32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_i32ToF32 = pure {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit
+val     extern_i32ToF32 = pure {c: "softfloat_i32tof32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit
 val      riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S)
 function riscv_i32ToF32 (rm, v) = {
   extern_i32ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_ui32ToF32 = pure {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit
+val     extern_ui32ToF32 = pure {c: "softfloat_ui32tof32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit
 val      riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S)
 function riscv_ui32ToF32 (rm, v) = {
   extern_ui32ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f32ToI64 = pure {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToI64 = pure {c: "softfloat_f32toi64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit
 val      riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L)
 function riscv_f32ToI64 (rm, v) = {
   extern_f32ToI64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f32ToUi64 = pure {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToUi64 = pure {c: "softfloat_f32toui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit
 val      riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU)
 function riscv_f32ToUi64 (rm, v) = {
   extern_f32ToUi64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_i64ToF32 = pure {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit
+val     extern_i64ToF32 = pure {c: "softfloat_i64tof32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit
 val      riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S)
 function riscv_i64ToF32 (rm, v) = {
   extern_i64ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_ui64ToF32 = pure {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit
+val     extern_ui64ToF32 = pure {c: "softfloat_ui64tof32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit
 val      riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S)
 function riscv_ui64ToF32 (rm, v) = {
   extern_ui64ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f64ToI32 = pure {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToI32 = pure {c: "softfloat_f64toi32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit
 val      riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W)
 function riscv_f64ToI32 (rm, v) = {
   extern_f64ToI32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f64ToUi32 = pure {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToUi32 = pure {c: "softfloat_f64toui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit
 val      riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU)
 function riscv_f64ToUi32 (rm, v) = {
   extern_f64ToUi32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_i32ToF64 = pure {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit
+val     extern_i32ToF64 = pure {c: "softfloat_i32tof64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit
 val      riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D)
 function riscv_i32ToF64 (rm, v) = {
   extern_i32ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_ui32ToF64 = pure {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit
+val     extern_ui32ToF64 = pure {c: "softfloat_ui32tof64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit
 val      riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D)
 function riscv_ui32ToF64 (rm, v) = {
   extern_ui32ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f64ToI64 = pure {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToI64 = pure {c: "softfloat_f64toi64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit
 val      riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L)
 function riscv_f64ToI64 (rm, v) = {
   extern_f64ToI64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f64ToUi64 = pure {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToUi64 = pure {c: "softfloat_f64toui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit
 val      riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU)
 function riscv_f64ToUi64 (rm, v) = {
   extern_f64ToUi64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_i64ToF64 = pure {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit
+val     extern_i64ToF64 = pure {c: "softfloat_i64tof64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit
 val      riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D)
 function riscv_i64ToF64 (rm, v) = {
   extern_i64ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_ui64ToF64 = pure {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit
+val     extern_ui64ToF64 = pure {c: "softfloat_ui64tof64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit
 val      riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D)
 function riscv_ui64ToF64 (rm, v) = {
   extern_ui64ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f16ToF32 = pure {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToF32 = pure {c: "softfloat_f16tof32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit
 val      riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S)
 function riscv_f16ToF32 (rm, v) = {
   extern_f16ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f16ToF64 = pure {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToF64 = pure {c: "softfloat_f16tof64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit
 val      riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D)
 function riscv_f16ToF64 (rm, v) = {
   extern_f16ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f32ToF64 = pure {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToF64 = pure {c: "softfloat_f32tof64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit
 val      riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D)
 function riscv_f32ToF64 (rm, v) = {
   extern_f32ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
-val     extern_f32ToF16 = pure {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToF16 = pure {c: "softfloat_f32tof16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit
 val      riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H)
 function riscv_f32ToF16 (rm, v) = {
   extern_f32ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f64ToF16 = pure {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToF16 = pure {c: "softfloat_f64tof16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit
 val      riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H)
 function riscv_f64ToF16 (rm, v) = {
   extern_f64ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f64ToF32 = pure {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToF32 = pure {c: "softfloat_f64tof32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit
 val      riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S)
 function riscv_f64ToF32 (rm, v) = {
   extern_f64ToF32(rm, v);
@@ -396,126 +396,126 @@ function riscv_f64ToF32 (rm, v) = {
 /* **************************************************************** */
 /* COMPARISONS                                                      */
 
-val     extern_f16Lt = pure {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit
+val     extern_f16Lt = pure {c: "softfloat_f16lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit
 val      riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Lt (v1, v2) = {
   extern_f16Lt(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f16Lt_quiet = pure {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit
+val     extern_f16Lt_quiet = pure {c: "softfloat_f16lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit
 val      riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Lt_quiet (v1, v2) = {
   extern_f16Lt_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f16Le = pure {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit
+val     extern_f16Le = pure {c: "softfloat_f16le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit
 val      riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Le (v1, v2) = {
   extern_f16Le(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f16Le_quiet = pure {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit
+val     extern_f16Le_quiet = pure {c: "softfloat_f16le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit
 val      riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Le_quiet (v1, v2) = {
   extern_f16Le_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f16Eq = pure {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit
+val     extern_f16Eq = pure {c: "softfloat_f16eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit
 val      riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Eq (v1, v2) = {
   extern_f16Eq(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f32Lt = pure {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit
+val     extern_f32Lt = pure {c: "softfloat_f32lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit
 val      riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Lt (v1, v2) = {
   extern_f32Lt(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f32Lt_quiet = pure {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit
+val     extern_f32Lt_quiet = pure {c: "softfloat_f32lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit
 val      riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Lt_quiet (v1, v2) = {
   extern_f32Lt_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f32Le = pure {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit
+val     extern_f32Le = pure {c: "softfloat_f32le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit
 val      riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Le (v1, v2) = {
   extern_f32Le(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f32Le_quiet = pure {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit
+val     extern_f32Le_quiet = pure {c: "softfloat_f32le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit
 val      riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Le_quiet (v1, v2) = {
   extern_f32Le_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f32Eq = pure {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit
+val     extern_f32Eq = pure {c: "softfloat_f32eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit
 val      riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Eq (v1, v2) = {
   extern_f32Eq(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f64Lt = pure {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit
+val     extern_f64Lt = pure {c: "softfloat_f64lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit
 val      riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Lt (v1, v2) = {
   extern_f64Lt(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f64Lt_quiet = pure {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit
+val     extern_f64Lt_quiet = pure {c: "softfloat_f64lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit
 val      riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Lt_quiet (v1, v2) = {
   extern_f64Lt_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f64Le = pure {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit
+val     extern_f64Le = pure {c: "softfloat_f64le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit
 val      riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Le (v1, v2) = {
   extern_f64Le(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f64Le_quiet = pure {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit
+val     extern_f64Le_quiet = pure {c: "softfloat_f64le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit
 val      riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Le_quiet (v1, v2) = {
   extern_f64Le_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f64Eq = pure {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit
+val     extern_f64Eq = pure {c: "softfloat_f64eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit
 val      riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Eq (v1, v2) = {
   extern_f64Eq(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
-val     extern_f16roundToInt = pure {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit
+val     extern_f16roundToInt = pure {c: "softfloat_f16roundToInt", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit
 val      riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H)
 function riscv_f16roundToInt (rm, v, exact) = {
   extern_f16roundToInt(rm, v, exact);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
-val     extern_f32roundToInt = pure {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit
+val     extern_f32roundToInt = pure {c: "softfloat_f32roundToInt", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit
 val      riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S)
 function riscv_f32roundToInt (rm, v, exact) = {
   extern_f32roundToInt(rm, v, exact);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
-val     extern_f64roundToInt = pure {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit
+val     extern_f64roundToInt = pure {c: "softfloat_f64roundToInt", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit
 val      riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D)
 function riscv_f64roundToInt (rm, v, exact) = {
   extern_f64roundToInt(rm, v, exact);
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index da04278..6e88327 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -165,11 +165,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
  * where cancellation can be performed.
  */
 
-val speculate_conditional = impure {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool
+val speculate_conditional = impure {interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool
 
-val load_reservation = impure {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
-val match_reservation = pure {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
-val cancel_reservation = impure {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
+val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
+val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
+val cancel_reservation = impure {interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
 
 /* Exception delegation: given an exception and the privilege at which
  * it occured, returns the privilege at which it should be handled.
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 295a4da..1f34d2d 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -79,39 +79,39 @@ bitfield Misa : xlenbits = {
 register misa : Misa
 
 /* whether misa is R/W */
-val sys_enable_writable_misa = pure {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
+val sys_enable_writable_misa = pure "sys_enable_writable_misa" : unit -> bool
 /* whether misa.c was enabled at boot */
-val sys_enable_rvc = pure {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
+val sys_enable_rvc = pure "sys_enable_rvc" : unit -> bool
 /* whether misa.{f,d} were enabled at boot */
-val sys_enable_fdext = pure {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
+val sys_enable_fdext = pure "sys_enable_fdext" : unit -> bool
 /* whether Svinval was enabled at boot */
-val sys_enable_svinval = pure {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool
+val sys_enable_svinval = pure "sys_enable_svinval" : unit -> bool
 /* whether Zcb was enabled at boot */
-val sys_enable_zcb = pure {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool
+val sys_enable_zcb = pure "sys_enable_zcb" : unit -> bool
 /* whether zfinx was enabled at boot */
-val sys_enable_zfinx = pure {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
+val sys_enable_zfinx = pure "sys_enable_zfinx" : unit -> bool
 /* whether the N extension was enabled at boot */
-val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
+val sys_enable_next = pure "sys_enable_next" : unit -> bool
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
    supervisor mode is implemented and non-bare addressing modes are supported. */
-val sys_enable_writable_fiom = pure {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
+val sys_enable_writable_fiom = pure "sys_enable_writable_fiom" : unit -> bool
 
 /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */
-val sys_pmp_count = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
+val sys_pmp_count = pure "sys_pmp_count" : unit -> range(0, 64)
 /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g.
    G=0 -> 4 bytes, G=10 -> 4096 bytes. */
-val sys_pmp_grain = pure {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63)
+val sys_pmp_grain = pure "sys_pmp_grain" : unit -> range(0, 63)
 
 /* whether misa.v was enabled at boot */
-val sys_enable_vext = pure {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool
+val sys_enable_vext = pure "sys_enable_vext" : unit -> bool
 
 /* whether misa.b was enabled at boot */
-val sys_enable_bext = pure {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool
+val sys_enable_bext = pure "sys_enable_bext" : unit -> bool
 
 // CBO extensions. Zicbop cannot be enabled/disabled because it has no effect
 // at all on this model.
-val sys_enable_zicbom = pure {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool
-val sys_enable_zicboz = pure {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool
+val sys_enable_zicbom = pure "sys_enable_zicbom" : unit -> bool
+val sys_enable_zicboz = pure "sys_enable_zicboz" : unit -> bool
 
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
@@ -734,7 +734,6 @@ mapping opst_code : seed_opst <-> bits(2) = {
  *       read_seed_csr. Hence it appears here.
  */
 val get_16_random_bits = impure {
-    ocaml: "Platform.get_16_random_bits",
     interpreter: "Platform.get_16_random_bits",
     c: "plat_get_16_random_bits",
     lem: "plat_get_16_random_bits"
diff --git a/ocaml_emulator/_tags b/ocaml_emulator/_tags
deleted file mode 100644
index 168de09..0000000
--- a/ocaml_emulator/_tags
+++ /dev/null
@@ -1,3 +0,0 @@
-<**/*.ml>: bin_annot, annot
-<*.m{l,li}>: package(lem), package(linksem), package(zarith)
-<riscv_ocaml_sim.native>: package(lem), package(linksem), package(zarith)
diff --git a/ocaml_emulator/_tags.bisect b/ocaml_emulator/_tags.bisect
deleted file mode 100644
index ca6f27a..0000000
--- a/ocaml_emulator/_tags.bisect
+++ /dev/null
@@ -1,3 +0,0 @@
-<**/*.ml>: bin_annot, annot
-<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(bisect_ppx)
-<riscv_ocaml_sim.native>: package(lem), package(linksem), package(zarith), package(bisect_ppx)
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
deleted file mode 100644
index b9921a0..0000000
--- a/ocaml_emulator/platform.ml
+++ /dev/null
@@ -1,197 +0,0 @@
-open Sail_lib;;
-module P = Platform_impl;;
-module Elf = Elf_loader;;
-
-(* Platform configuration *)
-
-let config_enable_rvc                  = ref true
-let config_enable_next                 = ref false
-let config_enable_writable_misa        = ref true
-let config_enable_dirty_update         = ref false
-let config_enable_misaligned_access    = ref false
-let config_mtval_has_illegal_inst_bits = ref false
-let config_enable_svinval              = ref false
-let config_enable_zcb                  = ref false
-let config_enable_writable_fiom        = ref true
-let config_enable_vext                 = ref true
-let config_enable_bext                 = ref false
-let config_enable_zicbom               = ref false
-let config_enable_zicboz               = ref false
-let config_pmp_count                   = ref Big_int.zero
-let config_pmp_grain                   = ref Big_int.zero
-
-let set_config_pmp_count x = config_pmp_count := Big_int.of_int x
-let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x
-
-let platform_arch = ref P.RV64
-
-(* logging *)
-
-let config_print_instr       = ref true
-let config_print_step        = ref false
-let config_print_reg         = ref true
-let config_print_mem_access  = ref true
-let config_print_platform    = ref true
-
-let print_instr s =
-  if !config_print_instr
-  then print_endline s
-  else ()
-
-let print_step () =
-  if !config_print_step
-  then print_endline ""
-  else ()
-
-let print_reg s =
-  if !config_print_reg
-  then print_endline s
-  else ()
-
-let print_mem_access s =
-  if !config_print_mem_access
-  then print_endline s
-  else ()
-
-let print_platform s =
-  if !config_print_platform
-  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
-    | P.RV64 -> Big_int.of_int 64
-    | P.RV32 -> Big_int.of_int 32
-
-let arch_bits_of_int i =
-  get_slice_int (cur_arch_bitwidth (), Big_int.of_int i, Big_int.zero)
-
-let arch_bits_of_int64 i =
-  get_slice_int (cur_arch_bitwidth (), Big_int.of_int64 i, Big_int.zero)
-
-let rom_size_ref = ref 0
-let make_rom arch start_pc =
-  let reset_vec =
-    List.concat (List.map P.uint32_to_bytes (P.reset_vec_int arch start_pc)) in
-  let dtb = P.make_dtb (P.make_dts arch) in
-  let rom = reset_vec @ dtb in
-  ( rom_size_ref := List.length rom;
-    (*
-    List.iteri (fun i c ->
-                print_mem_access "rom[0x%Lx] <- %x\n"
-                                 (Int64.add P.rom_base (Int64.of_int i))
-                                 c
-               ) rom;
-     *)
-    rom )
-
-let enable_writable_misa ()          = !config_enable_writable_misa
-let enable_rvc ()                    = !config_enable_rvc
-let enable_next ()                   = !config_enable_next
-let enable_fdext ()                  = false
-let enable_vext ()                   = !config_enable_vext
-let enable_bext ()                   = !config_enable_bext
-let enable_zicbom ()                 = !config_enable_zicbom
-let enable_zicboz ()                 = !config_enable_zicboz
-let enable_dirty_update ()           = !config_enable_dirty_update
-let enable_misaligned_access ()      = !config_enable_misaligned_access
-let mtval_has_illegal_inst_bits ()   = !config_mtval_has_illegal_inst_bits
-let enable_svinval ()                = !config_enable_svinval
-let enable_zcb ()                    = !config_enable_zcb
-let enable_zfinx ()                  = false
-let enable_writable_fiom ()          = !config_enable_writable_fiom
-let pmp_count ()                     = !config_pmp_count
-let pmp_grain ()                     = !config_pmp_grain
-
-let rom_base ()   = arch_bits_of_int64 P.rom_base
-let rom_size ()   = arch_bits_of_int   !rom_size_ref
-
-let dram_base ()  = arch_bits_of_int64 P.dram_base
-let dram_size ()  = arch_bits_of_int64 !P.dram_size_ref
-
-let cache_block_size_exp () = Big_int.of_int64 !P.cache_block_size_exp_ref
-
-let clint_base () = arch_bits_of_int64 P.clint_base
-let clint_size () = arch_bits_of_int64 P.clint_size
-
-let insns_per_tick () = Big_int.of_int P.insns_per_tick
-
-let htif_tohost () =
-  arch_bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
-
-(* Entropy Source - get random bits *)
-
-(* This function can be changed to support deterministic sequences of
-   pseudo-random bytes. This is useful for testing. *)
-let get_16_random_bits () = arch_bits_of_int (Random.int 0xFFFF)
-
-(* load reservation *)
-
-let speculate_conditional () = true
-
-let reservation = ref "none"  (* shouldn't match any valid address *)
-
-let load_reservation addr =
-  print_platform (Printf.sprintf "reservation <- %s\n" (string_of_bits addr));
-  reservation := string_of_bits addr
-
-let match_reservation addr =
-  print_platform (Printf.sprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr));
-  string_of_bits addr = !reservation
-
-let cancel_reservation () =
-  print_platform (Printf.sprintf "reservation <- none\n");
-  reservation := "none"
-
-let read_mem (rk, addrsize, addr, len) =
-  Sail_lib.fast_read_ram (len, addr)
-
-let write_mem_ea _ = ()
-
-let write_mem (wk, addrsize, addr, len, value) =
-  Sail_lib.write_ram' (len, Sail_lib.uint addr, value); true
-
-let excl_res _ = true
-
-let barrier _ = ()
-
-(* terminal I/O *)
-
-let term_write char_bits =
-  let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
-  P.term_write (char_of_int (Big_int.to_int big_char))
-
-let term_read () =
-  let c = P.term_read () in
-  arch_bits_of_int (int_of_char c)
-
-(* physical memory *)
-
-let get_mem_bytes addr len =
-  read_mem_bytes addr len
-
-(* returns starting value for PC, i.e. start of reset vector *)
-let init arch elf_file =
-  platform_arch := arch;
-  Elf.load_elf elf_file;
-
-  print_platform (Printf.sprintf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ())));
-  print_platform (Printf.sprintf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size);
-
-  let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in
-  let rom = make_rom arch start_pc in
-  let rom_base = Big_int.of_int64 P.rom_base in
-  let rec write_rom ofs = function
-    | [] -> ()
-    | h :: tl -> let addr = Big_int.add rom_base (Big_int.of_int ofs) in
-                 (wram addr h);
-                 write_rom (ofs + 1) tl
-  in ( write_rom 0 rom;
-       get_slice_int (cur_arch_bitwidth (), rom_base, Big_int.zero)
-     )
diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml
deleted file mode 100644
index 2732d94..0000000
--- a/ocaml_emulator/platform_impl.ml
+++ /dev/null
@@ -1,220 +0,0 @@
-(* architecture *)
-
-type arch =
-  | RV32
-  | RV64
-
-let str_of_arch = function
-  | RV32 -> "RV32"
-  | RV64 -> "RV64"
-
-(* int->byte converters in little-endian order *)
-
-let uint32_to_bytes u = let open Int32 in
- List.map to_int
-  [ logand u 0xffl;
-    logand (shift_right u 8) 0xffl;
-    logand (shift_right u 16) 0xffl;
-    logand (shift_right u 24) 0xffl;
-  ]
-
-let uint64_to_bytes u = let open Int64 in
- List.map to_int
-  [ logand u 0xffL;
-    logand (shift_right u 8) 0xffL;
-    logand (shift_right u 16) 0xffL;
-    logand (shift_right u 24) 0xffL;
-    logand (shift_right u 32) 0xffL;
-    logand (shift_right u 40) 0xffL;
-    logand (shift_right u 48) 0xffL;
-    logand (shift_right u 56) 0xffL;
-  ]
-
-(* reset vector for the rom *)
-
-let reset_vec_size = 8l;;
-
-let reset_vec_int arch start_pc = [
-  0x297l;                                                 (* auipc  t0, 0x0      *)
-  (let open Int32 in
-   add 0x28593l (shift_left (mul reset_vec_size 4l) 20)); (* addi   a1, t0, ofs(dtb) *)
-  0xf1402573l;                                            (* csrr   a0, mhartid  *)
-  (match arch with
-     | RV32 -> 0x0182a283l                                (* lw     t0, 24(t0)   *)
-     | RV64 -> 0x0182b283l);                              (* ld     t0, 24(t0)   *)
-  0x28067l;                                               (* jr     t0           *)
-  0x0l;
-  (let open Int64 in to_int32 (logand start_pc 0xffffffffL));
-  (let open Int64 in to_int32 (shift_right_logical start_pc 32));
-]
-
-(* address map *)
-
-let dram_base  = 0x80000000L;;  (* Spike::DRAM_BASE *)
-let clint_base = 0x02000000L;;  (* Spike::CLINT_BASE *)
-let clint_size = 0x000c0000L;;  (* Spike::CLINT_SIZE *)
-let rom_base   = 0x00001000L;;  (* Spike::DEFAULT_RSTVEC *)
-
-let dram_size_ref = ref (Int64.(shift_left 64L 20))
-
-(* Default 64, which is mandated by RVA22. *)
-let cache_block_size_exp_ref = ref (Int64.(6L))
-
-type mem_region = {
-    addr : Int64.t;
-    size : Int64.t
-}
-
-(* dts from spike *)
-let spike_dts isa_spec mmu_spec cpu_hz insns_per_rtc_tick mems =
-    "/dts-v1/;\n"
-  ^ "\n"
-  ^ "/ {\n"
-  ^ "  #address-cells = <2>;\n"
-  ^ "  #size-cells = <2>;\n"
-  ^ "  compatible = \"ucbbar,spike-bare-dev\";\n"
-  ^ "  model = \"ucbbar,spike-bare\";\n"
-  ^ "  cpus {\n"
-  ^ "    #address-cells = <1>;\n"
-  ^ "    #size-cells = <0>;\n"
-  ^ "    timebase-frequency = <" ^ string_of_int (cpu_hz/insns_per_rtc_tick) ^ ">;\n"
-  ^ "    CPU0: cpu@0 {\n"
-  ^ "      device_type = \"cpu\";\n"
-  ^ "      reg = <0>;\n"
-  ^ "      status = \"okay\";\n"
-  ^ "      compatible = \"riscv\";\n"
-  ^ "      riscv,isa = \"" ^ isa_spec ^ "\";\n"
-  ^ "      mmu-type = \"riscv," ^ mmu_spec ^ "\";\n"
-  ^ "      clock-frequency = <" ^ string_of_int cpu_hz ^ ">;\n"
-  ^ "      CPU0_intc: interrupt-controller {\n"
-  ^ "        #interrupt-cells = <1>;\n"
-  ^ "        interrupt-controller;\n"
-  ^ "        compatible = \"riscv,cpu-intc\";\n"
-  ^ "      };\n"
-  ^ "    };\n"
-  ^ "  };\n"
-  ^ (List.fold_left (^) ""
-       (List.map (fun m ->
-         "  memory@" ^ Printf.sprintf "%Lx" m.addr ^ " {\n"
-         ^ "    device_type = \"memory\";\n"
-         ^ "    reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.addr 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.addr 0xffffffffL)
-         ^           " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.size 0xffffffffL) ^ ">;\n"
-         ^ "  };\n") mems))
-  ^ "  soc {\n"
-  ^ "    #address-cells = <2>;\n"
-  ^ "    #size-cells = <2>;\n"
-  ^ "    compatible = \"ucbbar,spike-bare-soc\", \"simple-bus\";\n"
-  ^ "    ranges;\n"
-  ^ "    clint@" ^ Printf.sprintf "%Lx" clint_base ^ " {\n"
-  ^ "      compatible = \"riscv,clint0\";\n"
-  ^ "      interrupts-extended = <&CPU0_intc 3 &CPU0_intc 7 >;\n"
-  ^ "      reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_base 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_base 0xffffffffL)
-  ^             " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_size 0xffffffffL) ^ ">;\n"
-  ^ "    };\n"
-  ^ "  };\n"
-  ^ "  htif {\n"
-  ^ "    compatible = \"ucb,htif0\";\n"
-  ^ "  };\n"
-  ^ "};\n"
-
-let cpu_hz = 1000000000;;
-let insns_per_tick = 100;;
-
-let make_mems () = [{ addr = dram_base;
-                      size = !dram_size_ref }];;
-
-let make_dts arch =
-  let isa, mmu = match arch with
-      | RV64 -> "rv64imac", "sv39"
-      | RV32 -> "rv32imac", "sv32" in
-  spike_dts isa mmu cpu_hz insns_per_tick (make_mems ());;
-
-let bytes_to_string bytes =
-  String.init (List.length bytes) (fun i -> Char.chr (List.nth bytes i))
-
-let dtc_path = ref "/usr/bin/dtc"
-
-let set_dtc path =
-  try let st = Unix.stat path in
-      if st.Unix.st_kind = Unix.S_REG && st.Unix.st_perm != 0
-      then dtc_path := path
-      else ( Printf.eprintf "%s doesn't seem like a valid executable.\n%!" path;
-             exit 1)
-  with Unix.Unix_error (e, _, _) ->
-    ( Printf.eprintf "Error accessing %s: %s\n%!" path (Unix.error_message e);
-      exit 1)
-
-let set_dram_size mb =
-  dram_size_ref := Int64.(shift_left (Int64.of_int mb) 20)
-
-(* Calculate x=log2(n) and return Some(x) if n is a power of 2, otherwise None. *)
-let log2 n =
-  let rec loop i =
-    if i >= Sys.int_size - 1 then None
-    else if (1 lsl i) = n then Some i
-    else loop (i + 1)
-  in
-  if n <= 0 then None else loop 0
-
-let set_cache_block_size b =
-  match log2 b with
-    | Some(block_size_exp) -> cache_block_size_exp_ref := Int64.(Int64.of_int block_size_exp)
-    | None -> (Printf.eprintf "Invalid cache block size provided."; exit 1)
-
-let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *)
-  try
-    let cmd = Printf.sprintf "%s -I dts" !dtc_path in
-    let (cfrom, cto, cerr) =
-      Unix.open_process_full cmd [||]
-    in (
-      output_string cto dts;
-      (* print_endline " sent dts to dtc ..."; *)
-      close_out cto;
-      (* simple and stupid for now *)
-      let rec accum_bytes cin acc =
-        match (
-          try  Some (input_byte cin)
-          with End_of_file -> None
-        ) with
-          | Some b -> accum_bytes cin (b :: acc)
-          | None   -> List.rev acc
-      in
-      (* let _ = print_endline " accumulating dtb ..." in *)
-      let dtb  = accum_bytes cfrom [] in
-      (* let _ = print_endline " accumulating emsg ..." in *)
-      let emsg = bytes_to_string (accum_bytes cerr []) in
-      match Unix.close_process_full (cfrom, cto, cerr) with
-        | Unix.WEXITED 0 -> dtb
-        | _ -> (Printf.printf "%s\n%!" ("Error executing dtc: " ^ emsg);
-                exit 1)
-    )
-  with Unix.Unix_error (e, fn, _) ->
-    (Printf.printf "%s\n" ("Error executing dtc: " ^ fn ^ ": " ^ Unix.error_message e);
-     exit 1)
-
-(* Terminal I/O *)
-
-let term_write char =
-  ignore (Unix.write_substring Unix.stderr (String.make 1 char) 0 1)
-
-let rec term_read () =
-  let buf = Bytes.make 1 '\000' in
-  let nbytes = Unix.read Unix.stdin buf 0 1 in
-  (* todo: handle nbytes == 0 *)
-  Bytes.get buf 0
-
-(* Platform diagnostics *)
-
-let show_bytes s =
-  output_string stdout s
-
-let dump_dts arch = show_bytes (make_dts arch)
-let dump_dtb arch = show_bytes (bytes_to_string (make_dtb (make_dts arch)))
-
-(*
-let save_string_to_file s fname =
-  let out = open_out fname in
-  output_string out s;
-  close_out out;;
-
- *)
diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml
deleted file mode 100644
index 20eaef6..0000000
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ /dev/null
@@ -1,211 +0,0 @@
-open Sail_lib
-open Riscv
-module PI = Platform_impl
-module P = Platform
-module Elf = Elf_loader
-
-(* OCaml driver for generated RISC-V model. *)
-
-let opt_file_arguments = ref ([] : string list)
-
-let opt_dump_dts = ref false
-let opt_dump_dtb = ref false
-let opt_signature_file = ref (None : string option)
-let signature_granularity_ref = ref 4
-let opt_isa = ref (None : string option)
-
-let report_arch () =
-  Printf.printf "RV%d\n" (Big_int.to_int Riscv.zxlen_val);
-  exit 0
-
-let set_signature_file s =
-  opt_signature_file := Some s;
-  (* turn off logging *)
-  P.config_print_instr := false;
-  P.config_print_reg := false;
-  P.config_print_mem_access := false;
-  P.config_print_platform := false
-
-let set_signature_granularity sg =
-  signature_granularity_ref := sg
-
-let options = Arg.align ([("-dump-dts",
-                           Arg.Set opt_dump_dts,
-                           " dump the platform device-tree source to stdout");
-                          ("-dump-dtb",
-                           Arg.Set opt_dump_dtb,
-                           " dump the *binary* platform device-tree blob to stdout");
-                          ("-enable-dirty-update",
-                           Arg.Set P.config_enable_dirty_update,
-                           " enable dirty-bit update during page-table walks");
-                          ("-enable-misaligned-access",
-                           Arg.Set P.config_enable_misaligned_access,
-                           " enable misaligned accesses without M-mode traps");
-                          ("-pmp-count",
-                           Arg.Int P.set_config_pmp_count,
-                           " number of supported PMPs (0, 16, 64)");
-                          ("-pmp-grain",
-                           Arg.Int P.set_config_pmp_grain,
-                           " exponent of granularity of PMP addresses (G in the spec)");
-                          ("-enable-next",
-                           Arg.Set P.config_enable_next,
-                           " enable N extension");
-                          ("-mtval-has-illegal-inst-bits",
-                           Arg.Set P.config_mtval_has_illegal_inst_bits,
-                           " mtval stores instruction bits on an illegal instruction exception");
-                          ("-enable-svinval",
-                           Arg.Set P.config_enable_svinval,
-                           " enable Svinval extension");
-                          ("-enable-zcb",
-                           Arg.Set P.config_enable_zcb,
-                           " enable Zcb (simple code size) extension");
-                          ("-enable-writable-fiom",
-                           Arg.Set P.config_enable_writable_fiom,
-                           " enable FIOM (Fence of I/O implies Memory) bit in menvcfg");
-                          ("-disable-rvc",
-                           Arg.Clear P.config_enable_rvc,
-                           " disable the RVC extension on boot");
-                          ("-disable-vext",
-                           Arg.Clear P.config_enable_vext,
-                           " disable the RVV extension on boot");
-                          ("-enable-bext",
-                           Arg.Clear P.config_enable_bext,
-                           " enable the B extension on boot");
-                           ("-enable-zicbom",
-                           Arg.Set P.config_enable_zicbom,
-                           " enable the Zicbom extension");
-                           ("-enable-zicboz",
-                           Arg.Set P.config_enable_zicboz,
-                           " enable the Zicboz extension");
-                          ("-disable-writable-misa-c",
-                           Arg.Clear P.config_enable_writable_misa,
-                           " leave misa hardwired to its initial value");
-                          ("-ram-size",
-                           Arg.Int PI.set_dram_size,
-                           " size of physical ram memory to use (in MB)");
-                          ("-cache-block-size",
-                           Arg.Int PI.set_cache_block_size,
-                           " cache block size of the cache block size (default 64; max 4096)");
-                          ("-report-arch",
-                           Arg.Unit report_arch,
-                           " report model architecture (RV32 or RV64)");
-                          ("-test-signature",
-                           Arg.String set_signature_file,
-                           " file for signature output (requires ELF signature symbols)");
-                          ("-signature-granularity",
-                           Arg.Int set_signature_granularity,
-                           " test signature granularity (in bytes)");
-                          ("-trace-delimit-step",
-                           Arg.Set P.config_print_step,
-                           " delimit instructions in the trace output");
-                          ("-isa",
-                           Arg.String (fun s -> opt_isa := Some s),
-                           " requested isa");
-                          ("-with-dtc",
-                           Arg.String PI.set_dtc,
-                           " full path to dtc to use")
-                         ])
-
-let usage_msg = "RISC-V platform options:"
-
-(* ELF architecture checks *)
-
-let get_arch () =
-  match Big_int.to_int Riscv.zxlen_val with
-    | 64 -> PI.RV64
-    | 32 -> PI.RV32
-    | n  -> failwith (Printf.sprintf "Unknown model architecture RV%d" n)
-
-let str_of_elf = function
-  | Elf.ELF_Class_64 -> "ELF64"
-  | Elf.ELF_Class_32 -> "ELF32"
-
-let elf_arg =
-  Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s])
-            usage_msg;
-  if !opt_dump_dts then (PI.dump_dts (get_arch ()); exit 0);
-  if !opt_dump_dtb then (PI.dump_dtb (get_arch ()); exit 0);
-  ( match !opt_file_arguments with
-      | f :: _ -> prerr_endline ("Sail/RISC-V: running ELF file " ^ f); f
-      | _ -> (prerr_endline "Please provide an ELF file."; exit 0)
-  )
-
-let check_elf () =
-  match (get_arch (), Elf.elf_class ()) with
-    | (PI.RV64, Elf.ELF_Class_64) ->
-          P.print_platform "RV64 model loaded ELF64.\n"
-    | (PI.RV32, Elf.ELF_Class_32) ->
-          P.print_platform "RV32 model loaded ELF32.\n"
-    | (a,  e) ->
-          (let msg = Printf.sprintf "\n%s model cannot execute %s.\n" (PI.str_of_arch a) (str_of_elf e) in
-           Printf.eprintf "%s" msg;
-           exit 1)
-
-(* post execution handlers *)
-
-let write_bytes fl bytes =
-  let i = ref 0 in
-  while !i < Bytes.length bytes do
-    for j = !signature_granularity_ref - 1 downto 0 do
-      let s = Printf.sprintf "%02x"
-          (int_of_char (Bytes.get bytes (!i + j))) in
-      output_string fl s;
-    done;
-    output_string fl "\n";
-    i := !i + !signature_granularity_ref;
-  done
-
-let write_signature f sig_start sig_end =
-  let b = Big_int.to_int sig_start in
-  let len = Big_int.to_int sig_end - b in
-  let sig_bytes = P.get_mem_bytes sig_start len in
-  let sig_file = open_out f in
-  write_bytes sig_file sig_bytes;
-  close_out sig_file
-
-let dump_signature () =
-  match !opt_signature_file with
-  | None -> ()
-  | Some f ->
-      match (Elf.elf_symbol "begin_signature",
-	     Elf.elf_symbol "end_signature") with
-      | Some b, Some e -> write_signature f b e
-      | None, _ -> Printf.eprintf "no begin_signature symbol in ELF"
-      | _, None -> Printf.eprintf "no end_signature symbol in ELF"
-
-let show_times init_s init_e run_e insts =
-  let init_time = init_e.Unix.tms_utime -. init_s.Unix.tms_utime in
-  let exec_time = run_e.Unix.tms_utime -. init_e.Unix.tms_utime in
-  Printf.eprintf "\nInitialization: %g secs\n" init_time;
-  Printf.eprintf "Execution: %g secs\n" exec_time;
-  Printf.eprintf "Instructions retired: %Ld\n" insts;
-  Printf.eprintf "Perf: %g ips\n" ((Int64.to_float insts) /. exec_time)
-
-(* model execution *)
-
-let run pc =
-  sail_call
-    (fun r ->
-      try ( zinit_model ();
-            zPC := pc;
-            zloop ()
-          )
-      with
-        | ZError_not_implemented (zs) ->
-              print_string ("Error: Not implemented: ", zs)
-        | ZError_internal_error (_) ->
-              prerr_endline "Error: internal error"
-    )
-
-let () =
-  Random.self_init ();
-
-  let init_start = Unix.times () in
-  let pc = Platform.init (get_arch ()) elf_arg in
-  let _  = check_elf () in
-  let init_end = Unix.times () in
-  let _ = run pc in
-  let run_end = Unix.times () in
-  let insts = Big_int.to_int64 (uint (!Riscv.zminstret)) in
-  dump_signature ();
-  show_times init_start init_end run_end insts
diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml
deleted file mode 100644
index 2b98751..0000000
--- a/ocaml_emulator/softfloat.ml
+++ /dev/null
@@ -1,198 +0,0 @@
-
-let f16_add rm v1 v2 =
-  ()
-
-let f16_sub rm v1 v2 =
-  ()
-
-let f16_mul rm v1 v2 =
-  ()
-
-let f16_div rm v1 v2 =
-  ()
-
-let f32_add rm v1 v2 =
-  ()
-
-let f32_sub rm v1 v2 =
-  ()
-
-let f32_mul rm v1 v2 =
-  ()
-
-let f32_div rm v1 v2 =
-  ()
-
-let f64_add rm v1 v2 =
-  ()
-
-let f64_sub rm v1 v2 =
-  ()
-
-let f64_mul rm v1 v2 =
-  ()
-
-let f64_div rm v1 v2 =
-  ()
-
-let f16_muladd rm v1 v2 v3 =
-  ()
-
-let f32_muladd rm v1 v2 v3 =
-  ()
-
-let f64_muladd rm v1 v2 v3 =
-  ()
-
-let f16_sqrt rm v =
-  ()
-
-let f32_sqrt rm v =
-  ()
-
-let f64_sqrt rm v =
-  ()
-
-let f16_to_i32 rm v =
-  ()
-
-let f16_to_ui32 rm v =
-  ()
-
-let i32_to_f16 rm v =
-  ()
-
-let ui32_to_f16 rm v =
-  ()
-
-let f16_to_i64 rm v =
-  ()
-
-let f16_to_ui64 rm v =
-  ()
-
-let i64_to_f16 rm v =
-  ()
-
-let ui64_to_f16 rm v =
-  ()
-
-let f32_to_i32 rm v =
-  ()
-
-let f32_to_ui32 rm v =
-  ()
-
-let i32_to_f32 rm v =
-  ()
-
-let ui32_to_f32 rm v =
-  ()
-
-let f32_to_i64 rm v =
-  ()
-
-let f32_to_ui64 rm v =
-  ()
-
-let i64_to_f32 rm v =
-  ()
-
-let ui64_to_f32 rm v =
-  ()
-
-let f64_to_i32 rm v =
-  ()
-
-let f64_to_ui32 rm v =
-  ()
-
-let i32_to_f64 rm v =
-  ()
-
-let ui32_to_f64 rm v =
-  ()
-
-let f64_to_i64 rm v =
-  ()
-
-let f64_to_ui64 rm v =
-  ()
-
-let i64_to_f64 rm v =
-  ()
-
-let ui64_to_f64 rm v =
-  ()
-
-let f16_to_f32 rm v =
-  ()
-
-let f16_to_f64 rm v =
-  ()
-
-let f32_to_f64 rm v =
-  ()
-
-let f32_to_f16 rm v =
-  ()
-
-let f64_to_f16 rm v =
-  ()
-
-let f64_to_f32 rm v =
-  ()
-
-let f16_lt v1 v2 =
-  ()
-
-let f16_lt_quiet v1 v2 =
-  ()
-
-let f16_le v1 v2 =
-  ()
-
-let f16_le_quiet v1 v2 =
-  ()
-
-let f16_eq v1 v2 =
-  ()
-
-let f32_lt v1 v2 =
-  ()
-
-let f32_lt_quiet v1 v2 =
-  ()
-
-let f32_le v1 v2 =
-  ()
-
-let f32_le_quiet v1 v2 =
-  ()
-
-let f32_eq v1 v2 =
-  ()
-
-let f64_lt v1 v2 =
-  ()
-
-let f64_lt_quiet v1 v2 =
-  ()
-
-let f64_le v1 v2 =
-  ()
-
-let f64_le_quiet v1 v2 =
-  ()
-
-let f64_eq v1 v2 =
-  ()
-
-let f16_round_to_int exact rm v =
-  ()
-
-let f32_round_to_int exact rm v =
-  ()
-
-let f64_round_to_int exact rm v =
-  ()
diff --git a/ocaml_emulator/tracecmp.ml b/ocaml_emulator/tracecmp.ml
deleted file mode 100644
index 5ce3970..0000000
--- a/ocaml_emulator/tracecmp.ml
+++ /dev/null
@@ -1,358 +0,0 @@
-(* Simple trace comparison checker *)
-
-type arch =
-  | RV32
-  | RV64
-
-type csr_read = {
-  csrr : string;
-  rdval : int64
-}
-
-type csr_write = {
-  csrw : string;
-  wrval : int64
-}
-
-type reg_write = {
-  reg : int;
-  rval : int64
-}
-
-type mem_op = {
-  vaddr : int64;
-  paddr : int64;
-  mval  : int64
-}
-
-type inst = {
-  count : int;
-  priv : char;
-  pc : int64;
-  inst: int32
-}
-
-type tick = {
-  time : int64
-}
-
-type htif = {
-  tohost : int64
-}
-
-type ld_res =
-  | Res_make of int64
-  | Res_match of int64 * int64
-  | Res_cancel
-
-type line =
-  | L_none
-  | L_inst of inst
-  | L_reg_write of reg_write
-  | L_csr_read of csr_read
-  | L_csr_write of csr_write
-  | L_mem_read of mem_op
-  | L_mem_write of mem_op
-  | L_tick of tick
-  | L_htif of htif
-  | L_ld_res of ld_res
-
-(* architectural support *)
-let sail_arch = ref RV64
-
-let arch_val v =
-  match !sail_arch with
-    | RV64 -> v
-    | RV32 -> Int64.logand v 0xFFFFFFFFL (* only lowest 32-bits *)
-
-let inst_count = ref 0
-
-(* csr reads
-   CSR mscratch -> 0x0000000000000000
- *)
-
-let parse_csr_read l =
-  try Scanf.sscanf l " CSR %s -> 0x%Lx"
-                   (fun csrr rdval -> L_csr_read { csrr; rdval = arch_val rdval })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_csr_read r =
-  Printf.sprintf "CSR %s -> 0x%Lx" r.csrr r.rdval
-
-(* csr writes
-   CSR mstatus <- 0x0000000a00020800 (input: 0x0000000a00020800)
- *)
-
-let parse_csr_write l =
-  try Scanf.sscanf l " CSR %s <- 0x%Lx "
-                   (fun csrw wrval -> L_csr_write { csrw; wrval = arch_val wrval })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_csr_write r =
-  Printf.sprintf "CSR %s <- 0x%Lx " r.csrw r.wrval
-
-(* mem reads
-   mem[V:0x0000000080001000, P:0x0000000080001000] -> 0x0000000000000000
- *)
-
-(* exclusion list, to avoid comparing reads to mmio htif port by spike *)
-let mem_addr_excludes = [ 0x80001000L ]
-let parse_mem_read l =
-  try Scanf.sscanf l " mem[V:0x%Lx, P:0x%Lx] -> 0x%Lx"
-                   (fun va pa v ->
-                    if List.mem va mem_addr_excludes || List.mem pa mem_addr_excludes
-                    then L_none
-                    else L_mem_read { vaddr = arch_val va; paddr = arch_val pa; mval = arch_val v })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_mem_read r =
-  Printf.sprintf "mem[V:0x%Lx, P:0x%Lx] -> 0x%Lx" r.vaddr r.paddr r.mval
-
-(* mem writes
-   mem[V:0x0000000080001000, P:0x0000000080001000] <- 0x0000000000000000
- *)
-
-let parse_mem_write l =
-  try Scanf.sscanf l  " mem[V:0x%Lx, P:0x%Lx] <- 0x%Lx"
-                   (fun va pa v ->
-                    L_mem_write { vaddr = arch_val va; paddr = arch_val pa; mval = arch_val v })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_mem_write r =
-  Printf.sprintf "mem[V:0x%Lx, P:0x%Lx] -> 0x%Lx" r.vaddr r.paddr r.mval
-
-(* reg writes
-   x16 <- 0x0000000000000000
- *)
-
-let parse_reg_write l =
-  try Scanf.sscanf l " x%u <- 0x%Lx"
-                  (fun reg rval -> L_reg_write { reg; rval = arch_val rval })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_reg_write r =
-  Printf.sprintf "x%u <- 0x%Lx" r.reg r.rval
-
-(* instructions *)
-
-let sprint_inst r =
-  Printf.sprintf "[%u] [%c]: 0x%Lx (0x%lx)" r.count r.priv r.pc r.inst
-
-(* sail instruction line:
-  [13000] [M]: 0x0000000080000E4A (0x0107971B) slli  a4, a5, 0b10000
- *)
-
-let parse_sail_inst l =
-  try Scanf.sscanf l " [%u] [%c]: 0x%Lx (0x%lx) %s"
-                   (fun count  priv  pc inst _ ->
-                    inst_count := count;
-                    L_inst { count; priv; pc; inst })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-(* spike instruction line:
-  [2] core   0 [M]: 0x0000000000001008 (0xf1402573) csrr    a0, mhartid
- *)
-
-let parse_spike_inst l =
-  try Scanf.sscanf l " [%u] core   0 [%c]: 0x%Lx (0x%lx) %s"
-                   (fun count  priv  pc inst _ ->
-                    inst_count := count;
-                    L_inst { count; priv; pc = arch_val pc; inst })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-(* clock tick
-   clint::tick mtime <- 0x1
- *)
-
-let parse_tick l =
-  try Scanf.sscanf l " clint::tick mtime <- 0x%Lx"
-                   (fun time -> L_tick { time })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_tick t =
-  Printf.sprintf "clint::tick mtime <- 0x%Lx" t.time
-
-(* htif tick
-   htif::tick 0x1
- *)
-
-let parse_htif l =
-  try Scanf.sscanf l " htif::tick 0x%Lx"
-                   (fun tohost -> L_htif { tohost })
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_htif t =
-  Printf.sprintf "htif::tick 0x%Lx" t.tohost
-
-(* Load reservations:
-   make:   reservation <- 0x80002008
-   match:  reservation: 0xffffffffffffffff, key=0x80002008
-   cancel: reservation <- none
-
- *)
-let parse_ldres_match l =
-  try Scanf.sscanf
-        l " reservation: 0x%Lx, key=0x%Lx"
-                   (fun res key -> L_ld_res (Res_match (res, key)))
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let parse_ldres_match_sail l =
-  try Scanf.sscanf
-        l " reservation: none, key=0x%Lx"
-                   (fun key -> L_ld_res (Res_match (Int64.minus_one, key)))
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let parse_ldres_change l =
-  try if l = "reservation <- none"
-      then L_ld_res Res_cancel
-      else Scanf.sscanf
-             l " reservation <- 0x%Lx"
-             (fun res -> L_ld_res (Res_make res))
-  with
-    | Scanf.Scan_failure _ -> L_none
-    | End_of_file -> L_none
-
-let sprint_ldres = function
-  | Res_make res         -> Printf.sprintf "reservation <- 0x%Lx" res
-  | Res_match (res, key) -> Printf.sprintf "reservation: 0x%Lx, key=0x%Lx" res key
-  | Res_cancel           -> Printf.sprintf "reservation <- none"
-
-(* scanners *)
-
-let popt p l = function
-  | L_none -> p l
-  | res -> res
-
-let parse_line l =
-  parse_csr_read l |> popt parse_csr_write l
-  |> popt parse_reg_write l |> popt parse_tick l |> popt parse_htif l
-  |> popt parse_ldres_change l  |> popt parse_ldres_match l
-
-let parse_sail_line l =
-  parse_line l |> popt parse_sail_inst l  |> popt parse_ldres_match_sail l
-
-let parse_spike_line l =
-  parse_line l |> popt parse_spike_inst l
-
-(* printer *)
-let sprint_line = function
-  | L_none -> "<not-parsed>"
-  | L_inst i -> sprint_inst i
-  | L_reg_write r -> Printf.sprintf "<%d> %s" !inst_count (sprint_reg_write r)
-  | L_csr_read  r -> Printf.sprintf "<%d> %s" !inst_count (sprint_csr_read r)
-  | L_csr_write r -> Printf.sprintf "<%d> %s" !inst_count (sprint_csr_write r)
-  | L_mem_read  m -> Printf.sprintf "<%d> %s" !inst_count (sprint_mem_read m)
-  | L_mem_write m -> Printf.sprintf "<%d> %s" !inst_count (sprint_mem_write m)
-  | L_tick t      -> Printf.sprintf "<%d> %s" !inst_count (sprint_tick t)
-  | L_htif t      -> Printf.sprintf "<%d> %s" !inst_count (sprint_htif t)
-  | L_ld_res r    -> Printf.sprintf "<%d> %s" !inst_count (sprint_ldres r)
-
-(* file processing *)
-
-let rec get_line ch parse =
-  let line = try  Some (input_line ch)
-             with End_of_file -> None in
-  match line with
-    | Some l -> (match parse l with
-                   | L_none -> get_line ch parse
-                   | r -> r
-                )
-    | None -> L_none
-
-let rec print_lines ch parse =
-  match (get_line ch parse) with
-    | L_none -> ()
-    | l      -> (print_endline (sprint_line l);
-                 print_lines ch parse)
-
-
-let lines_matched k l =
-  match k, l with
-    (* Special case for CSR writes to sie/sip/sstatus, since spike
-     * does a recursive call which messes the trace log.  For these
-     * registers, we just match the final written value, and need to
-     * unfortunately ignore the input value.
-     *)
-    | L_csr_write kw, L_csr_write lw ->
-          if   (   (kw.csrw = "mie"     && lw.csrw = "sie")
-                || (kw.csrw = "mip"     && lw.csrw = "sip")
-                || (kw.csrw = "mstatus" && lw.csrw = "sstatus"))
-          then kw.wrval = lw.wrval
-          else kw = lw
-    | _, _ ->   k = l
-
-let rec compare_traces k l cnt =
-  let kro = get_line k parse_spike_line in
-  let lro = get_line l parse_sail_line in
-  match kro, lro with
-    | L_none, L_none ->
-          print_endline (Printf.sprintf "Matched %d instructions" cnt)
-    | L_none, lr ->
-          print_endline  "Spike: not reached";
-          print_endline ("Sail:  " ^ sprint_line lr);
-          exit 1
-    | kr, L_none ->
-          print_endline ("Spike: " ^ sprint_line kr);
-          print_endline  "Sail:  not reached";
-          exit 1
-    | kr, lr ->
-          if   lines_matched kr lr
-          then compare_traces k l (cnt + 1)
-          else (print_endline ("Spike: " ^ sprint_line kr);
-                print_endline ("Sail:  " ^ sprint_line lr);
-                exit 1)
-
-let spike_log  = ref (None : string option)
-let sail_log   = ref (None : string option)
-let uncompress = ref false
-
-let in_file f =
-  if !uncompress
-  then Unix.open_process_in ("gunzip -c " ^ f)
-  else open_in f
-
-let options =
-  Arg.align ([( "-z",
-                Arg.Set uncompress,
-                " uncompress trace files");
-              ( "-rv32",
-                Arg.Unit (fun f -> sail_arch := RV32),
-                " sail architecture");
-              ( "-k",
-                Arg.String (fun f -> spike_log := Some f),
-                " spike trace log");
-              ( "-l",
-                Arg.String (fun f -> sail_log := Some f),
-                " sail trace log")])
-let usage = "usage: tracecmp [options]\n"
-
-let _ =
-  Arg.parse options (fun s -> print_endline usage; exit 0)
-            usage;
-  match !spike_log, !sail_log with
-    | None, None     -> (print_endline usage; exit 0)
-    | Some l, None   -> print_lines (in_file l) parse_spike_line
-    | None, Some l   -> print_lines (in_file l) parse_sail_line
-    | Some k, Some l -> compare_traces (in_file k) (in_file l) 0
diff --git a/opam b/opam
deleted file mode 100644
index a53d108..0000000
--- a/opam
+++ /dev/null
@@ -1,32 +0,0 @@
-opam-version: "2.0"
-name: "sail-riscv"
-version: "0.5"
-maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>"
-authors: [
-  "Alasdair Armstrong"
-  "Thomas Bauereiss"
-  "Brian Campbell"
-  "Shaked Flur"
-  "Jonathan French"
-  "Prashanth Mundkur"
-  "Robert Norton"
-  "Christopher Pulte"
-  "Peter Sewell"
-]
-homepage: "https://github.com/rems-project/sail-riscv/"
-bug-reports: "https://github.com/rems-project/sail-riscv/issues"
-license: "BSD3"
-dev-repo: "git+https://github.com/rems-project/sail-riscv.git"
-build: [make "LEM_DIR=%{lem:share}%" "SAIL_DIR=%{sail:share}%" "SAIL=sail" "opam-build"]
-depends: [
-  "ocaml" {>= "4.06.1"}
-  "ocamlfind"
-  "ocamlbuild"
-  "lem"
-  "sail" {>= "0.9"}
-  "linksem" {>= "0.3"}
-  "conf-gmp"
-  "conf-zlib"
-]
-synopsis:
-  "This package installs a RISC-V emulator (32 and 64 bits) built form the Sail model at https://github.com/rems-project/sail-riscv"
diff --git a/os-boot/README.md b/os-boot/README.md
index 087abac..921dd65 100644
--- a/os-boot/README.md
+++ b/os-boot/README.md
@@ -35,15 +35,6 @@ performance and benchmarking a model without any execution tracing is
 available on the optimize branch (`git checkout optimize`) of this
 repository. This currently requires the latest Sail built from source.
 
-Booting Linux with the OCaml backend
-------------------------------------
-
-The OCaml model only needs the ELF-version of the BBL, since it can generate its
-own DTB.
-```
-$ ./ocaml_emulator/riscv_ocaml_sim_<arch> bbl > execution-trace.log 2> console.log
-```
-
 Caveats for OS boot
 -------------------
 
diff --git a/test/run_tests.sh b/test/run_tests.sh
index 8c0f03f..d8016fa 100755
--- a/test/run_tests.sh
+++ b/test/run_tests.sh
@@ -55,31 +55,6 @@ cd $RISCVDIR
 make clean
 
 printf "Building 32-bit RISCV specification...\n"
-if ARCH=RV32 make ocaml_emulator/riscv_ocaml_sim_RV32 ;
-then
-    green "Building 32-bit RISCV OCaml emulator" "ok"
-else
-    red "Building 32-bit RISCV OCaml emulator" "fail"
-fi
-for test in $DIR/riscv-tests/rv32*.elf; do
-    # skip F/D tests on OCaml for now
-    pat='rv32ud-.+elf'
-    if [[ $(basename $test) =~ $pat ]];
-    then continue
-    fi
-    pat='rv32uf-.+elf'
-    if [[ $(basename $test) =~ $pat ]];
-    then continue
-    fi
-    if $RISCVDIR/ocaml_emulator/riscv_ocaml_sim_RV32 "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}"
-    then
-       green "OCaml-32 $(basename $test)" "ok"
-    else
-       red "OCaml-32 $(basename $test)" "fail"
-    fi
-done
-finish_suite "32-bit RISCV OCaml tests"
-
 
 if ARCH=RV32 make c_emulator/riscv_sim_RV32;
 then
@@ -102,31 +77,6 @@ make clean
 
 printf "Building 64-bit RISCV specification...\n"
 
-if make ocaml_emulator/riscv_ocaml_sim_RV64 ;
-then
-    green "Building 64-bit RISCV OCaml emulator" "ok"
-else
-    red "Building 64-bit RISCV OCaml emulator" "fail"
-fi
-for test in $DIR/riscv-tests/rv64*.elf; do
-    # skip F/D tests on OCaml for now
-    pat='rv64ud-.+elf'
-    if [[ $(basename $test) =~ $pat ]];
-    then continue
-    fi
-    pat='rv64uf-.+elf'
-    if [[ $(basename $test) =~ $pat ]];
-    then continue
-    fi
-    if $RISCVDIR/ocaml_emulator/riscv_ocaml_sim_RV64 "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}"
-    then
-       green "OCaml-64 $(basename $test)" "ok"
-    else
-       red "OCaml-64 $(basename $test)" "fail"
-    fi
-done
-finish_suite "64-bit RISCV OCaml tests"
-
 if make c_emulator/riscv_sim_RV64;
 then
     green "Building 64-bit RISCV C emulator" "ok"