Remove the OCaml emulator

[Timmmm]

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

[github-actions]

Test Results

396 tests   - 316   396 ✅  - 316   0s ⏱️ ±0s
  4 suites  -   2     0 💤 ±  0 
  1 files   ±  0     0 ❌ ±  0 

Results for commit 842bc30. ± Comparison against base commit c61351e.

This pull request removes 316 tests.

Building 32-bit RISCV OCaml emulator
Building 64-bit RISCV OCaml emulator
OCaml-32 rv32mi-p-breakpoint.elf
OCaml-32 rv32mi-p-csr.elf
OCaml-32 rv32mi-p-illegal.elf
OCaml-32 rv32mi-p-ma_addr.elf
OCaml-32 rv32mi-p-ma_fetch.elf
OCaml-32 rv32mi-p-mcsr.elf
OCaml-32 rv32mi-p-sbreak.elf
OCaml-32 rv32mi-p-scall.elf
…

♻️ This comment has been updated with latest results.

[Alasdair]

The Sail to OCaml translation could also use quite a few changes, as it's the first thing I ever implemented when I started working on Sail. It still uses ocamlbuild for example, whereas the OCaml ecosystem has now mostly move to dune.

Removing the use here would actually free me to make some much needed changes.

[Timmmm]

@PeterRugg This PR removes OCaml support from the model, which I think would affect TestRig. Is that a deal breaker? What's the status of TestRig?

[jrtc27]

We use an independent Haskell generator these days (https://github.com/CTSRD-CHERI/QuickCheckVEngine). I don’t know if the old Sail model-based OCaml one even still works, likely not, it hasn’t been touched in 5 years.

[PeterRugg]

Yeah, we certainly don't compare against the ocaml model, and can't see any reason why we would. Losing the sail-based test generation is sad, but as @jrtc27 says, we never really got chance to investigate using it properly.

[arichardson]

I believe the one thing we are losing here is the ability to generate the DTB for the OS boot. I wonder if this should be added to the C simulator first? Otherwise I am more than happy to see the ocaml simulator being removed since it makes it a lot easier to add new extensions with hooks.

[arichardson]

I believe the one thing we are losing here is the ability to generate the DTB for the OS boot. I wonder if this should be added to the C simulator first? Otherwise I am more than happy to see the ocaml simulator being removed since it makes it a lot easier to add new extensions with hooks.

Looks like it's just a simple string template (let spike_dts isa_spec mmu_spec cpu_hz insns_per_rtc_tick mems), so should be easy to move over to C.

[Timmmm]

I have actually implemented that for our C++ emulator so I'll port it over.

[Timmmm]

I have actually implemented that for our C++ emulator so I'll port it over.

I actually haven't implemented it - I was thinking of something else. It is pretty simple; just generate a string template and then run dtc to compile it.

But doing that in C is a right pain, so I'm voting we defer this and add it again if/when somebody asks for it.

If you want to boot Linux you can still manually make a DTB.

[arichardson]

I have actually implemented that for our C++ emulator so I'll port it over.

I actually haven't implemented it - I was thinking of something else. It is pretty simple; just generate a string template and then run dtc to compile it.

But doing that in C is a right pain, so I'm voting we defer this and add it again if/when somebody asks for it.

If you want to boot Linux you can still manually make a DTB.

Seems fine to me. It would be nice to generate this so that operating systems can parse it and boot, but can be done as a follow-up when needed.

[jordancarlin]

LGTM

[Timmmm]

I'll merge this in a few days if nobody objects.