Make use of Extension() instead of have*()

[jriyyya]

As found out in the previous PR, There were few other have* function usage which can be changed to utilize the respective extension() for them. This PR aims to do so.

[jriyyya]

Hello @ThinkOpenly , I wanted to ask that the calling of these functions in only the sail files are need to be changed? There were instances of these extensions been called in Risc.v, RiscScript.sml, Riscv.thy, etc with the have* method, and weren't changed to utilize the extension() method.

[ThinkOpenly]

There were instances of these extensions been called in Risc.v, RiscScript.sml, Riscv.thy, etc with the have* method, and weren't changed to utilize the extension() method.

Good observations!

Tell me how you found these other instances. I presume you removed (or commented out) all of the have* functions in model/riscv_sys_regs.sail. With the changes in the PR, did the compilation still fail due to those other instances?

I peeked at these:

• prover_snapshots/isabelle/RV64/Riscv.thy
• prover_snapshots/coq/RV64/riscv.v
• prover_snapshots/hol4/RV64/riscvScript.sml

...all of those appear to be files generated from the Sail code, based on comments at the top of the files, the commits that added them, and the contents of prover_snapshots/README.md:

# Snapshots of theorem prover definitions

This directory contains snapshots of definitions generated from the Sail RISC-V
specification for the interactive theorem provers Isabelle/HOL, HOL4, and Coq.
These snapshots are provided for convenience, and are not guaranteed to be
up-to-date.

Are there other instances that you've found? Let's dig into them all, but if they are all files that are generated from Sail, I don't want to worry about them.

[jriyyya]

Tell me how you found these other instances. I presume you removed (or commented out) all of the have* functions in model/riscv_sys_regs.sail. With the changes in the PR, did the compilation still fail due to those other instances?

How do you build and compile the project? When I tried running the make command without commenting out anything I got this error.

echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/RV64/riscv_types.lem
lem -isa -outdir generated_definitions/isabelle/RV64 -lib Sail=/home/jriyyya/.opam/default/share/sail/src/lem_interp -lib Sail=/home/jriyyya/.opam/default/share/sail/src/gen_lib \
        handwritten_support/0.11/riscv_extras.lem handwritten_support/0.11/mem_metadata.lem handwritten_support/0.11/riscv_extras_fdext.lem \
        generated_definitions/lem/RV64/riscv_types.lem \
        generated_definitions/lem/RV64/riscv.lem
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
File "generated_definitions/lem/RV64/riscv.lem", line 18640, character 7:
  Syntax error
make: *** [Makefile:339: generated_definitions/isabelle/RV64/Riscv.thy] Error 1

So I simply searched for instances of these declaration in vscode.

Are there other instances that you've found? Let's dig into them all, but if they are all files that are generated from Sail, I don't want to worry about them.

There are instances of these have* function other than the declaration in the riscv_sys_regs.sail file itself, like at like 334 we have haveUsrMode being used as

  if not(haveUsrMode()) then {
    let m = update_MPRV(m, 0b0);
    m
  } else m
}

If we change this to utilize extension, We do have to move the declaration of the function extension() at the top.

[ThinkOpenly]

How do you build and compile the project?

I have not documented that anywhere, have I? Apologies.

Here are steps (I've omitted installing prerequisites):

1. You first need to build the Sail parser:
   1. Find a directory in which to clone that repository, and make that directory your current working directory.
   2. git clone -b json https://github.com/ThinkOpenly/sail
   3. cd sail
   4. make
2. Then, set up the environment for building in the RISC-V Sail repository:
   1. eval $(opam env)
   2. export PATH=<path-to-sail-repository>:$PATH
3. Clone this sail-risv repository.
4. Within that clone: make json

There are instances of these have* function other than the declaration in the riscv_sys_regs.sail file itself, like at like 334 we have haveUsrMode being used as

  if not(haveUsrMode()) then {
    let m = update_MPRV(m, 0b0);
    m
  } else m
}

If we change this to utilize extension, We do have to move the declaration of the function extension() at the top.

Good catch! Could you go ahead and add those changes to this pull request?

[ThinkOpenly]

Could you go ahead and add those changes to this pull request?

I guess we could also delete all of the have* function definitions, if you've commented them out and there are no build errors.

[jriyyya]

I have not documented that anywhere, have I? Apologies.

Thanks for the instruction, and yes These instructions can be added in the README, Should I proceed with it?

Good catch! Could you go ahead and add those changes to this pull request?

Yes, on it

[ThinkOpenly]

These instructions can be added in the README, Should I proceed with it?

Yes, but... I'm thinking where to best put it...

This top-level README is primarily about the RISC-V Sail model, and the instructions are pretty specific to the JSON project... How about this: create a new document in the doc directory, say JSON.md with the instructions. And, optionally, add a pointer to it in the top-level README (like is done for os-boot).

Good catch! Could you go ahead and add those changes to this pull request?

Yes, on it

Making sure you caught my comment in the middle:

I guess we could also delete all of the have* function definitions, if you've commented them out and there are no build errors.

[jriyyya]

Yes, but... I'm thinking where to best put it...

This top-level README is primarily about the RISC-V Sail model, and the instructions are pretty specific to the JSON project... How about this: create a new document in the doc directory, say JSON.md with the instructions. And, optionally, add a pointer to it in the top-level README (like is done for os-boot).

Yes, we can do that

I have also made the requested changes. I deleted all of the have definitions as there were no errors on the build. There were a few comments on the have definitions, should they be added above their respective extension in the function?

[ThinkOpenly]

There were a few comments on the have* definitions, should they be added above their respective extension in the function?

Yeah, I think carrying the comments into the extension function would be nice. Great progress, thank you!

[jriyyya]

Done!

[jriyyya]

One tiny nit, but looks really good. Thanks!

Done, Thank you!

[ThinkOpenly]

I think I'm going to squash and merge your commits. There are a lot of little changes which are pretty closely related, and it keeps the repository history a little simpler.

Ideally, when a change set includes a move of a block of code, a commit with just the move should happen first, then other changes on top. This makes it easier on the reviewer of the code, since just the differences from the original code are in the commits after the first.

I didn't ask for that here because the changes are fairly well-defined and pretty easy to distinguish. Just FYI.

Thanks so much, @jriyyya !

[jriyyya]

I will keep that in mind, Thank you!

[joydeep049]

Hello @jriyyya, Are you still working on adding these instructions to the README? Or can i proceed with it?

[jriyyya]

@joydeep049 Sure, Please go ahead

[ThinkOpenly]

FYI, this commit and other related "extension tagging" commits have been merged upstream. https://github.com/riscv/sail-riscv/commit/3d5e4769c024e310a781a05aa5e44b52cb020cdd. Congratulations, and thank you for your efforts! :tada:

[jriyyya]

That's great, Happy to know that! 🚀