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 need for OPAM, which is a weirdly bug-prone tool.
*

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

Makefile

@@ -127,8 +127,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 += -dno_cast
 SAIL_DOC_FLAGS ?= -doc_embed plain
 
@@ -205,7 +203,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
@@ -231,40 +229,12 @@ 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
@@ -281,8 +251,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)
 
@@ -468,34 +436,16 @@ 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
 	-rm -f handwritten_support/riscv_extras.vo handwritten_support/riscv_extras.vos handwritten_support/riscv_extras.vok handwritten_support/riscv_extras.glob handwritten_support/.riscv_extras.aux
 	-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

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 an 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,8 +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
 ----------------------
 
@@ -219,8 +213,6 @@ 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 +246,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 +254,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 +270,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`.
 
 One can build either the RV32 or the RV64 model by specifying
 `ARCH=RV32` or `ARCH=RV64` on the `make` line, and using the matching
@@ -293,9 +282,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
@@ -311,19 +298,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>
 ```
 
@@ -335,17 +312,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
 
@@ -361,26 +332,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
 -------

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

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`,

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">
 

model/prelude.sail

@@ -47,16 +47,16 @@ val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n),
 
 overload operator - = {sub_vec, sub_vec_int}
 
-val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
+val quot_round_zero = {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
+val rem_round_zero = {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}
 
-val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y.
+val min_int = {interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y.
   (int('x), int('y)) -> {'z, ('x <= 'y & 'z == 'x) | ('x > 'y & 'z == 'y). int('z)}
 
-val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y.
+val max_int = {interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y.
   (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)}
 
 overload min = {min_int}
@@ -68,20 +68,20 @@ val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
 val print = "print_endline" : string -> unit
 val print_string = "print_string" : (string, string) -> unit
 
-val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_mem      = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_instr    = {interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_reg      = {interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_mem      = {interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_platform = {interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
 
-val print_step = {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit
+val print_step = {c: "print_step"} : unit -> unit
 
 function print_step() = ()
 
-val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
-val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
-val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
+val get_config_print_instr = {c:"get_config_print_instr"} : unit -> bool
+val get_config_print_reg = {c:"get_config_print_reg"} : unit -> bool
+val get_config_print_mem = {c:"get_config_print_mem"} : unit -> bool
 
-val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
+val get_config_print_platform = {c:"get_config_print_platform"} : unit -> bool
 // defaults for other backends
 function get_config_print_instr () = false
 function get_config_print_reg () = false