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

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

@@ -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,34 +434,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 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
 -------

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