Skip to content

Commit

Permalink
Remove the OCaml emulator
Browse files Browse the repository at this point in the history 
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 riscv#509
  • Loading branch information
@Timmmm
Timmmm authored Sep 19, 2024
1 parent c61351e commit bdf95b0
Show file tree
Hide file tree
Showing 22 changed files with 133 additions and 1,534 deletions.
4 changes: 2 additions & 2 deletions CODE_STYLE.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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
Expand Down
5 changes: 0 additions & 5 deletions Dockerfile
View file

This file was deleted.

58 changes: 2 additions & 56 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)

Expand Down Expand Up @@ -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
82 changes: 15 additions & 67 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down Expand Up @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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
--------------------------------------
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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>
```
Expand All @@ -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
Expand All @@ -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
-------
Expand Down
3 changes: 0 additions & 3 deletions build_simulators.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion doc/ExtendingGuide.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`,
Expand Down
8 changes: 4 additions & 4 deletions doc/ReadingGuide.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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">

Expand Down
22 changes: 11 additions & 11 deletions model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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
Expand Down
Loading

0 comments on commit bdf95b0

Please sign in to comment.