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.

Note, I left the targets to actually build the OCaml code since I believe it is used by TestRig for its random instruction generation.

Fixes #509
  • Loading branch information
@Timmmm
Timmmm committed Sep 9, 2024
1 parent a58c58c commit c7d03e8
Show file tree
Hide file tree
Showing 22 changed files with 132 additions and 1,517 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.

54 changes: 2 additions & 52 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)

Expand Down Expand Up @@ -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
73 changes: 15 additions & 58 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 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>

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

Expand All @@ -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
--------------------------------------

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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>
```

Expand All @@ -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

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

0 comments on commit c7d03e8

Please sign in to comment.