Role of the Sail OCaml simulator in the golden model

[martinberger]

Currently Sail can generate a C simulator (using the -c option) and an OCaml one (using -ocaml). The latter is much slower. Keeping them in sync occasionally causes problems, in particular in the recent P-extension PR, where a hard-coded limitation in the OCaml compiler lead to trouble with the OCaml emulator, see [1]. There is currently also a small discrepancy in typing depending on whether C or OCaml are targeted [2]. While those problems can be fixed, I wonder about the use-cases for the OCaml simulator in the RISCV model here. The RISCV OCaml tests also skip floating point arithmetic [3].

I do understand the benefits of n-version programming, but both, the C and the OCaml simulator come from the same source Sail, so the OCaml simulator is most useful in debugging the C simulator, but not the RISCV spec. So: how important is the OCaml simulator for RISCV?

1. Sail Model for RISC-V P Extension #132 (comment)

2. Inconsistent effects behavior between the Ocaml and C models  rems-project/sail#122

3. https://github.com/riscv/sail-riscv/blob/master/test/run_tests.sh#L62-L63

[b224hisl]

I have checked rems-project/sail#122. I have meet the same problem. So could I just use -no_effects when building the ocaml simulator so that my code can pass the CI? I can make cim successfully.

[jrtc27]

No you should fix your code to have the right effects annotations.

[b224hisl]

I have fixed the bugs about effects, but I met another problem when making osim:

` mkdir -p ocaml_emulator/_sbuild
cp ocaml_emulator/_tags ocaml_emulator/platform.ml ocaml_emulator/platform_impl.ml ocaml_emulator/softfloat.ml ocaml_emulator/riscv_ocaml_sim.ml generated_definitions/ocaml/RV32/*.ml ocaml_emulator/_sbuild
cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native
+ ocamlfind ocamlc -c -annot -bin-annot -package lem -package linksem -package zarith -o riscv.cmo riscv.ml
File "riscv.ml", line 459, characters 2-125:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 466, characters 2-417:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 505, characters 2-124:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 512, characters 2-126:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 626, characters 2-129:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 647, characters 2-129:
Warning 8: this pattern-matching is not exhaustive.

All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1112, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1133, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1154, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1175, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1196, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1217, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matchi
File "riscv.ml", line 1280, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1301, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1322, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1343, characters 2-130:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 1563, characters 2-202:
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
File "riscv.ml", line 2763, characters 0-13315:
Error: Too many non-constant constructors
       -- maximum is 246 non-constant constructors
Command exited with code 2.
Compilation unsuccessful after building 15 targets (14 cached) in 00:00:01.
make: *** [Makefile:221：ocaml_emulator/_sbuild/riscv_ocaml_sim.native]'

[martinberger]

@b224hisl I think you are hitting hard-coded limitation in the OCaml compiler I mention above. Have you branched your code off from the proposed P-extension code [1]. Or are you adding a large number of OCaml ADT-constructors? (Sorry I'm in a rush, so no time to look into your code)

[1] Sail Model for RISC-V P Extension #132

[jrtc27]

I've gone and filed rems-project/sail#165 against Sail to try and get this fixed

[martinberger]

I've gone and filed

Thanks. I didn't realise this was a regression. Reminds me that I should write more regression tests ...

[jrtc27]

Well, Sail 1 and Sail 2 are similar but different languages, so more like saying it's a regression from Python 2 to Python 3. I'm pretty sure the RISC-V Sail model has always been for Sail 2, but wasn't involved that far back to know.

[b224hisl]

@b224hisl I think you are hitting hard-coded limitation in the OCaml compiler I mention above. Have you branched your code off from the proposed P-extension code [1]. Or are you adding a large number of OCaml ADT-constructors? (Sorry I'm in a rush, so no time to look into your code)

[1] Sail Model for RISC-V P Extension #132

I think I didn't invole any P-extension code. I do add a large number of items like enum because the number of v-instructions is a little large. Please let me know if there is anything you want me to hange

[martinberger]

I do add a large number of items like enum because the number of v-instructions is a little large.

@b224hisl This should be fixed now, see rems-project/sail#165 Maybe pull the latest version and try locally. I think https://github.com/riscv/sail-riscv/blob/master/.github/workflows/compile.yml will automatically use the latest version of Sail if Cambridge have already published this fix to opam.

[jordancarlin]

Can be closed now that #544 is merged