new mechanism for reserved fields as mentioned in Issue #21

[joydeep049]

closes #21 Used the same mask as defined in binutils to make sure only the essential bits are retrieved while the others are zeroed out. Please review @ThinkOpenly

[joydeep049]

Thank you for the review! @ThinkOpenly As per my understanding, in this issue we basically had to "let everyone know" that even though the imm,rs1 and rd fields are zeroed out currently, we might use them later. I was not sure how exactly to implement this. Two ways came to mind:

1. Simple - Add comments and let people know, hence the use of the doc comments.
2. Do something similar to what binutils did and mask it. It seems this idea was mistaken and therefore doesn't yield any results.

[ThinkOpenly]

As per my understanding, in this issue we basically had to "let everyone know" that even though the imm,rs1 and rd fields are zeroed out currently, we might use them later. I was not sure how exactly to implement this. Two ways came to mind:

1. Simple - Add comments and let people know, hence the use of the doc comments.
2. Do something similar to what binutils did and mask it. It seems this idea was mistaken and therefore doesn't yields any results.

The goal with the project is to formalize what's currently in the Sail code into a more useful format. I've chosen JSON. So, there needs to be a clear means to translate important aspects found in the Sail code into a JSON representation. In the case under discussion, certain fields are reserved (and not constant as the Sail code currently represents).

The means I suggested in my last comment was to add an annotation to the fields, like reserved(0b00000). This is an ad-hoc annotation, but at least serves our purposes in a fairly straightforward and Sail-compatible way. What is needed, though, is a definition of the reserved function, even if it is just an identity function. Unfortunately, Sail's reasonably strong typing might force us to create an identity function for every field length:

function reserved_bits_5 f : bits(5) -> bits(5) = f

Looking a bit deeper, it looks like the Sail code has kind of made a mess of this. It does represent the "reserved" case of the fence.i instruction, but it does it as a new (invalid) mnemonic, fence.i.reserved, in a different file (model/riscv_insts_hints.sail):

mapping clause assembly = FENCEI_RESERVED(imm, rs, rd)
      if imm != 0b000000000000 | rs != zreg | rd != zreg
  <-> "fence.i.reserved." ^ reg_name(rd) ^ "." ^ reg_name(rs) ^ "." ^ hex_bits_12(imm)
      if imm != 0b000000000000 | rs != zreg | rd != zreg

sigh. Strange choices. Sail does not offer a ready way to handle this, though. This needs some further thought.

[joydeep049]

@ThinkOpenly You're right. Reserved fences are being used here in (model/riscv_insts_hints.sail), but I think the way we want to use it here is a bit different. And we cannot possibly go about creating identity functions for every bit length.

How should we approach our current situation here? Any ideas and suggestions are welcome.

Thanx!

[ThinkOpenly]

Let's move the general discussion to the associated issue #21. I've already added a comment there.

[joydeep049]

Hello @ThinkOpenly , I've made the changes as discussed in here. Could you tell me more on how I could Modify the Sail JSON backend to recognize functions with names like reserved_bits_N, where N is the bit length.

[ThinkOpenly]

Could you tell me more on how I could Modify the Sail JSON backend to recognize functions with names like reserved_bits_N, where N is the bit length.

I put a response in issue #21.

[joydeep049]

Could you tell me more on how I could Modify the Sail JSON backend to recognize functions with names like reserved_bits_N, where N is the bit length.

I put a response in issue #21.

I'm working on this . Apologies for the late reply (was travelling since last 2 days).

[ThinkOpenly]

Looks like you have some minor, but annoying whitespace issues to resolve here.

[ThinkOpenly]

This needs a rebase, too. :-/

[joydeep049]

@@ -206,12 +206,12 @@ all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH)
 json: $(SAIL_SRCS) model/main.sail Makefile
    @sail -json $(SAIL_FLAGS) $(SAIL_SRCS)

- 
+
 .PHONY: check-json
 check-json:
    sail -json $(SAIL_FLAGS) $(SAIL_SRCS) | python3 -c "import json; import sys; j=json.load(sys.stdin)"

- 
+
 output: $(SAIL_SRCS) model/main.sail Makefile
    sail -output-sail $(SAIL_FLAGS) $(SAIL_SRCS)

diff --git a/doc/JSON.md b/doc/JSON.md
index 965f989..7a8b2b1 100644
--- a/doc/JSON.md
+++ b/doc/JSON.md
@@ -17,5 +17,3 @@ After Installing the prerequisites

 4.  Within that clone : `make json`
-
-
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 48bdff2..fdd6497 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -43,10 +43,10 @@ function amo_width_valid(size : word_width) -> bool = {
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)

- 
+
 mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if extension("Zalrsc") & amo_width_valid(size)
   <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)
- 
+

 /* We could set load-reservations on physical or virtual addresses.
@@ -56,7 +56,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
  */

 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
- 
+
   let width_bytes = size_bytes(width);

   // This is checked during decoding.
@@ -[80](https://github.com/ThinkOpenly/sail-riscv/actions/runs/9745438581/job/26893375243?pr=24#step:4:81),7 +80,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
             MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
             MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
           },
- 
+
       }
     }
   }
@@ -[92](https://github.com/ThinkOpenly/sail-riscv/actions/runs/9745438581/job/26893375243?pr=24#step:4:93),10 +92,10 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)

- 
+
 mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)                                      if extension("Zalrsc") & amo_width_valid(size)
   <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)
- 
+

 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
@@ -110,7 +110,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
      */
     X(rd) = zero_extend(0b1); RETIRE_SUCCESS
   } else {
- 
+
     /* normal non-rmem case
       * rmem: SC is allowed to succeed (but might fail later)
       */
@@ -140,7 +140,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
                       MemValue(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
                       MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
                       MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
- 
+
                     }
                   }
                 }
@@ -171,15 +171,15 @@ mapping encdec_amoop : amoop <-> bits(5) = {
   AMOMAXU <-> 0b11[100](https://github.com/ThinkOpenly/sail-riscv/actions/runs/9745438581/job/26893375243?pr=24#step:4:101)
 }

- 
+
 mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)                                                if extension("Zaamo") & amo_width_valid(size)
   <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0[101](https://github.com/ThinkOpenly/sail-riscv/actions/runs/9745438581/job/26893375243?pr=24#step:4:102)111 if extension("Zaamo") & amo_width_valid(size)
- 
+

 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
- 
+
   let 'width_bytes = size_bytes(width);

Just a snippet of the formatting suggestions in CI (failing). Most of them are a - followed by a + . So is it asking me to remove one line and then add one????

@ThinkOpenly

[ThinkOpenly]

Just a snippet of the formatting suggestions in CI (failing). Most of them are a - followed by a + . So is it asking me to remove one line and then add one????

@ThinkOpenly

The two failing CI tests are:

trim trailing whitespace.................................................Failed
fix end of files.........................................................Failed

Given that whitespace is difficult to visualize, I selected text in the area of the +/- indicators, and this is what I see: It appears that there are a couple of spaces on line 75 that it doesn't like. git diff shows me something similar:

The "end of file" issue is also shown by git diff:

+// function to declare bitwise reserved fields.
+function reserved_bits_5 f : bits(5) -> bits(5) = f
+function reserved_bits_12 f : bits(12) -> bits(12) = f
\ No newline at end of file

I confess to not full understanding how this occurs, or how to remedy it. If you add a blank line after the last line, that resolves the "end of file" issue, but gets flagged as a whitespace issue. I think these things are artifacts of using Windows as a development environment, but I could be wrong.

[joydeep049]

Just a snippet of the formatting suggestions in CI (failing). Most of them are a - followed by a + . So is it asking me to remove one line and then add one???? @ThinkOpenly

The two failing CI tests are:

trim trailing whitespace.................................................Failed
fix end of files.........................................................Failed

Given that whitespace is difficult to visualize, I selected text in the area of the +/- indicators, and this is what I see: It appears that there are a couple of spaces on line 75 that it doesn't like. git diff shows me something similar:

The "end of file" issue is also shown by git diff:

+// function to declare bitwise reserved fields.
+function reserved_bits_5 f : bits(5) -> bits(5) = f
+function reserved_bits_12 f : bits(12) -> bits(12) = f
\ No newline at end of file

I confess to not full understanding how this occurs, or how to remedy it. If you add a blank line after the last line, that resolves the "end of file" issue, but gets flagged as a whitespace issue. I think these things are artifacts of using Windows as a development environment, but I could be wrong.

I am working with Ubuntu 🥲.

[joydeep049]

The Pre-commit checks have passed. However, there remains one more issue.

791 |  <-> reserved_bits_12(0b000000000000 : bits(12)) @ reserved_bits_5(0b00000 : bits(5)) @ (0b001 : bits(3)) @ reserved_bits_5(0b00000 : bits(5)) @ (0b0001111 : bits(7))
    |                                                    ^--------------------------------^
    | Cannot infer width here, as there are multiple subpatterns with unclear width in vector concatenation pattern
    | 
    | Caused by model/riscv_insts_base.sail:791.6-49:
    | 791 |  <-> reserved_bits_12(0b000000000000 : bits(12)) @ reserved_bits_5(0b00000 : bits(5)) @ (0b001 : bits(3)) @ reserved_bits_5(0b00000 : bits(5)) @ (0b0001111 : bits(7))
    |     |      ^-----------------------------------------^
    |     | A previous subpattern is here
make: *** [Makefile:317: generated_definitions/c/riscv_rvfi_model_RV64.c] Error 1

I also went through the sail manual by Alasdair Armstrong (https://alasdair.github.io/manual) but couldn't find anything that could help. I also raised my issue in the slack chat.

[joydeep049]

Closer to figuring it out. Probably, if we want to concatenate imm, rs1 and rd in the reserved form, we will have to add them as fields in the FENCEI() instruction, similar to below:

/*!
 * The FENCE_TSO instruction is a memory
 * ordering instruction that provides a stronger memory consistency model
 * compared to the standard FENCE instruction. It ensures that all memory
 * operations preceding and following the FENCE_TSO instruction are globally
 * ordered. The FENCE_TSO instruction includes two 4-bit fields, 'pred' and
 * 'succ', which represent the memory ordering requirements before and after
 * the FENCE_TSO instruction, respectively.
 */
union clause ast = FENCE_TSO : (bits(4), bits(4))

$[format I]
mapping clause encdec = FENCE_TSO(pred, succ)
  <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111

After the changes I'm proposing, it will look something like:

union clause ast = FENCEI : (bits(12), bits(5), bits(5))

// The rs1, rd and imm fields are marked as reserved to indicate
// that they are not currently used but may be reserved for future extensions.
mapping clause encdec = FENCEI(imm, rs1, rd)
  <-> imm @ rs1 @ 0b001 @ rd @ 0b0001111 

 /* fence.i is a nop for the memory model */
function clause execute FENCEI(imm, rs1, rd) = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SUCCESS }

mapping clause assembly = FENCEI(imm, rs1, rd) <-> "fence.i"

We would then have to add the reserved transformation to those operands earlier in the pipeline. Is this a suitable solution? @ThinkOpenly

(Although this would completely change the idea of how a fencei instruction is used, and would possibly require a lot of changes.)

[ThinkOpenly]

I'm having trouble following your discussion. Your first reference is for FENCE_TSO, and the second is for FENCEI, which are two different instructions, so it's difficult to compare them as before-and-after your suggested changes.

I'm starting to think that, IF every reserved bit vector is specified as a string of zero bits (this should be verified), then maybe it's better to specify the "reserved" functions as actually providing a value rather than being an identity function:

function reserved_bits_5 () = 0b00000

and then using them directly, without a parameter:

mapping clause encdec = FENCEI()
  <-> reserved_bits12() @ reserved_bits5() @ 0b001 @ reserved_bits5() @ 0b0001111

Whether that helps with the latest issues you are seeing, I don't know.

[joydeep049]

I'm having trouble following your discussion. Your first reference is for FENCE_TSO, and the second is for FENCEI, which are two different instructions, so it's difficult to compare them as before-and-after your suggested changes.

I did not mean to compare the two instructions directly. Just made an observation that all the instructions which had variables in their encdec mapping contained those variables as fields.

I'm starting to think that, IF every reserved bit vector is specified as a string of zero bits (this should be verified), then maybe it's better to specify the "reserved" functions as actually providing a value rather than being an identity function:

function reserved_bits_5 () = 0b00000

and then using them directly, without a parameter:

mapping clause encdec = FENCEI()
  <-> reserved_bits12() @ reserved_bits5() @ 0b001 @ reserved_bits5() @ 0b0001111

Whether that helps with the latest issues you are seeing, I don't know.

I'll try this!

[joydeep049]

function reserved_bits_5 () = 0b00000

Using this method gave the following error:

Type error:
model/riscv_types.sail:413.0-37:
413 |function reserved_bits_5 () = 0b00000
    |^-----------------------------------^
    | Cannot infer function type for unannotated function
make: *** [Makefile:242: generated_definitions/ocaml/RV64/riscv.ml] Error 1

I used mapping to define the imm,rs1 and rd values in model/riscv_types.sail. It will allow us to make changes to the value later on as we require.

Changes to the files other than model/riscv_types.sail and model/riscv_insts_base.sail are a result of running pre-commit on all files.

(Reminder to approve workflow for the OCaml code in the sail repository)

@ThinkOpenly

[ThinkOpenly]

function reserved_bits_5 () = 0b00000

Using this method gave the following error:

Type error:
model/riscv_types.sail:413.0-37:
413 |function reserved_bits_5 () = 0b00000
    |^-----------------------------------^
    | Cannot infer function type for unannotated function
make: *** [Makefile:242: generated_definitions/ocaml/RV64/riscv.ml] Error 1

Maybe it should provide the input-output types (not tested):

function reserved_bits_5 () : unit -> bits(5) = 0b00000

[joydeep049]

function reserved_bits_5 () = 0b00000

Using this method gave the following error:

Type error:
model/riscv_types.sail:413.0-37:
413 |function reserved_bits_5 () = 0b00000
    |^-----------------------------------^
    | Cannot infer function type for unannotated function
make: *** [Makefile:242: generated_definitions/ocaml/RV64/riscv.ml] Error 1

Maybe it should provide the input-output types (not tested):

function reserved_bits_5 () : unit -> bits(5) = 0b00000

Type error:
model/riscv_insts_base.sail:791.27-44:
791 |  <-> reserved_bits_12() @ reserved_bits_5() @ 0b001 @ reserved_bits_5() @ 0b0001111
    |                           ^---------------^
    | Cannot infer width here, as there are multiple subpatterns with unclear width in vector concatenation pattern
    | 
    | Caused by model/riscv_insts_base.sail:791.6-24:
    | 791 |  <-> reserved_bits_12() @ reserved_bits_5() @ 0b001 @ reserved_bits_5() @ 0b0001111
    |     |      ^----------------^
    |     | A previous subpattern is here
make: *** [Makefile:242: generated_definitions/ocaml/RV64/riscv.ml] Error 1

Getting the same error as before. I did try this before as well by reading from the sail manual but nothing else worked. @ThinkOpenly

[ThinkOpenly]

Getting the same error as before.

Not that I don't trust you, but could you show the code you added for both reserved_bits_5 and reserved_bits_12 here, and where you added them? Sail does seem to have trouble inferring widths for some things that have very obvious widths, which is quite disappointing. Let's verify your code first.

[joydeep049]

Getting the same error as before.

Not that I don't trust you, but could you show the code you added for both reserved_bits_5 and reserved_bits_12 here, and where you added them? Sail does seem to have trouble inferring widths for some things that have very obvious widths, which is quite disappointing. Let's verify your code first.

function reserved_bits_12 () : unit -> bits(12) = 0b000000000000
function reserved_bits_5 () : unit -> bits(5) = 0b00000

This is the code. 🥲🥲

[ThinkOpenly]

Getting the same error as before.

Not that I don't trust you, but could you show the code you added for both reserved_bits_5 and reserved_bits_12 here, and where you added them? Sail does seem to have trouble inferring widths for some things that have very obvious widths, which is quite disappointing. Let's verify your code first.

function reserved_bits_12 () : unit -> bits(12) = 0b000000000000
function reserved_bits_5 () : unit -> bits(5) = 0b00000

This is the code. 🥲🥲

I opened an issue with upstream Sail to try to clarify the restrictions we seem to be running into with bidirectional mapping clauses. https://github.com/rems-project/sail/issues/651. It appears that it may not be possible to use functions in these clauses, somewhat surprisingly to me.

Using what might be considered a workaround (or a hack!), maybe try something like (tested lightly):

enum reserved_bits_enum = { ZERO }
mapping reserved_bits_5 : reserved_bits_enum <-> bits(5) = { ZERO <-> 0b00000 }
mapping reserved_bits_12 : reserved_bits_enum <-> bits(12) = { ZERO <-> 0b000000000000 }

mapping clause encdec = FENCEI()
  <-> reserved_bits_12(ZERO) @ reserved_bits_5(ZERO) @ 0b001 @ reserved_bits_5(ZERO) @ 0b0001111

There may be less ugly ways of doing the same.

[ThinkOpenly]

There may be less ugly ways of doing the same.

Possibly slightly less ugly:

enum reserved_bits_enum = { RESERVED }
mapping bits_5 : reserved_bits_enum <-> bits(5) = { RESERVED <-> 0b00000 }
mapping bits_12 : reserved_bits_enum <-> bits(12) = { RESERVED <-> 0b000000000000 }
mapping size_bits : word_width <-> bits(12) = {
  BYTE   <-> bits_12(RESERVED),
  HALF   <-> bits_5(RESERVED) @ bits_5(RESERVED) @ 0b01,
[...]

[joydeep049]

I have made the suggested changes and they seem to work fine. @ThinkOpenly

(Reminder to approve the workflows in the sail repository. We might have to make some changes to the OCaml code.)

[ThinkOpenly]

I have made the suggested changes and they seem to work fine.

:tada:

(Reminder to approve the workflows in the sail repository. We might have to make some changes to the OCaml code.)

Do I? The actions ran (successfully, with a couple of warnings about using an outdated version of Node.js). What changes to the OCaml code?

You still need to rebase.

[joydeep049]

I meant my PR in `ThinkOpenly/sail'. @ThinkOpenly

[joydeep049]

Should we merge this? @ThinkOpenly

[ThinkOpenly]

Now that we have good code, we need to clean up the branch before merging. You should rebase against the target branch (https://github.com/ThinkOpenly/sail-riscv/tree/JSON), since you seem to have a commit from jriyyya lumped into your PR that you reverted with yet another commit. Also, given the net changes are pretty small, could you squash your commits into a single commit? (Or, I can do it when merging.)

[joydeep049]

My git client misbehaved while I was rebasing after squashing. Should I do it again or is this again? Also seems like it did not accept my final commit message. @ThinkOpenly

[ThinkOpenly]

This is still in a pretty weird state. I expect a single commit. Currently, there are 3 in this PR:

• one from jriyyya (a rebase to the target branch should fix this)
• one "initial commit" that I think should just be removed
• one "address failing tests" that has the 6 or 7 new lines that are the change, but also includes reversions of the previous 2 commits.

Also seems like it did not accept my final commit message.

Yeah, the commit message in the final commit is a bit of a mess.

If you need help with git, let me know.

[joydeep049]

Hello @ThinkOpenly

I have squashed all into a single commit. Hope this works.

Additionally, I wanted to inform you that I've submitted my LFX application. Looking forward to your feedback on both the application and this PR.

[ThinkOpenly]

I have squashed all into a single commit. Hope this works.

Well... getting closer. The single commit has Riya as the author, and you as the committer:

Can you fix that?