Need a new mechanism for reserved fields

[ThinkOpenly]

In the Sail definition ("model/riscv_insts_base.sail"), the opcode encoding for "FENCE.I" is defined:

mapping clause encdec = FENCEI()
  <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111

... every bit is constant.

But, the current RISC-V ISA specification (20191213) says:

The unused fields in the FENCE.I instruction, imm[11:0], rs1, and rd, are reserved for finer-grain fences in future extensions. For forward compatibility, base implementations shall ignore these fields, and standard software shall zero these fields.

There needs to be some way to know that for these fields, they are currently expected to be zero, but that may change in the future.

An example from a downstream project, "binutils", respects the reserved fields for the purposes of decode (in "include/opcode/riscv-opc.h"):

#define MASK_FENCE_I  0x707f

If the entire opcode was constant, the mask would be like "EBREAK" (and others):

#define MASK_EBREAK  0xffffffff

[joydeep049]

I am looking into this!

[ThinkOpenly]

There has been some good discussion provoked by @joydeep049's PR #24 , which I'll copy here...

Issue #21 is asking for some sort of mechanism in the Sail code to identify which fields are reserved. It could be something simple like changing 0b00000 to reserved(0b00000), where reserved is implemented as an identity function. This would allow the code to be compiled, yet the parser would produce an AST with a "reserved" tag of sorts.

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.

[ThinkOpenly]

In #24 (comment), @joydeep049 asks:

we cannot possibly go about creating identity functions for every bit length.

How should we approach our current situation here?

The actual required inventory of identity functions is currently very small (2: 5 bit and 12 bit fields for FENCE.I, the only cases that need it per current understanding). So, maybe we take the easy-if-slightly-ugly route, akin to what is already in place for optional operands:

• Create identity functions for 5-bit and 12-bit fields, named "reserved_bits_5" and "reserved_bits_12", as described in a previous comment.
• Utilize them as wrappers around the 3 reserved fields in FENCE.I.
• Enhance the JSON backend to look for these special function names, and save that information.
• Emit JSON that includes that information.

[joydeep049]

Sure @ThinkOpenly , I'll give it a try!

[ThinkOpenly]

In #24 (comment), @joydeep049 asked:

Could you tell me more on how I could Modify the Sail JSON backend to recognize functions with names like reserved_bits_N, [...]

There is some code emerging in ThinkOpenly/sail#17 that includes code similar to what is needed here.

There is a function, optional_operand (which might get renamed at my request) that currently looks like:

let optional_operand k op =
    (*
        The current regex pattern targets a specific function name pattern 
        that starts with "maybe_*", such as "maybe_vmask", "maybe_lmul_flag", and "maybe_ta_flag".
        Since those kinds are the most prevalent ones as of now.

        TODO: come up with a more robust implementation, that doesn't involve
        specifying function names explicitly.
    *)
  let pattern = Str.regexp_case_fold ("maybe[a-z0-9_]+\\(" ^ "(" ^ op ^ ")" ^ "\\)") in
    match Hashtbl.find_opt assembly_clean k with
    | Some op_list -> extract_opt_operands_fn pattern op_list
    | None -> None, ""

This function is operating on the stored (in a Hashtbl) representation of an operand, when emitting the operand in JSON (function json_of_operand). It is looking for a specific pattern in the operand string, like maybe...(operand).

You'd want something similar, but operating on the stored representation of a field (in the encodings Hashtbl, function json_of_field), and you'd be looking for a specific pattern in the field string, like reserved_bits_X(value).

[joydeep049]

I went through the sail code as mentioned above.
I came up with this:

let optional_operand k op =
  (* Pattern to match maybe_* or reserved_bits_N functions *)
  let pattern = regexp_case_fold ("\\|reserved_bits_[0-9]+\\)(" ^ op ^ ")") in
  match Hashtbl.find_opt assembly_clean k with
  | Some op_list -> extract_opt_operands_fn pattern op_list
  | None -> None, ""

Would this work?
@ThinkOpenly

[ThinkOpenly]

let optional_operand k op =

You're working in the routine that handles operands. This issue needs to be addressed in the routine that handles fields, json_of_field, instead.

  (* Pattern to match maybe_* or reserved_bits_N functions *)
  let pattern = regexp_case_fold ("\\|reserved_bits_[0-9]+\\)(" ^ op ^ ")") in

There are no optional fields, so the comment is misleading, and the code doesn't look for "maybe_*", either. So, that part of the comment could be removed.

The syntax doesn't look quite correct to me. What is the leading \\| for, the subsequent \\), and I think you're missing the escaped parentheses ("\\(" and "\\)" that would enable extracting the field name. Have you run this code to observe its behavior?

Note carefully the function and accompanying comments in #21 (comment), including:

There is a function, optional_operand (which might get renamed at my request) that currently looks like:

let optional_operand k op =
  let pattern = Str.regexp_case_fold ("maybe[a-z0-9_]+\\(" ^ "(" ^ op ^ ")" ^ "\\)") in

This function is operating on the stored (in a Hashtbl) representation of an operand, when emitting the operand in JSON (function json_of_operand). It is looking for a specific pattern in the operand string, like maybe...(operand).

You'd want something similar, but operating on the stored representation of a field (in the encodings Hashtbl, function json_of_field), and you'd be looking for a specific pattern in the field string, like reserved_bits_X(value).

[joydeep049]

Apologies for the confusion!
I now understand how its supposed to work.
But I'm not able to find a file here which would connect to the sail JSON backend in this repo.
@ThinkOpenly

[ThinkOpenly]

I'm not able to find a file here which would connect to the sail JSON backend in this repo.

Sorry, I don't understand what it is you seek.

If you are asking how to test changes, refer to the document you created a little while ago: https://github.com/ThinkOpenly/sail-riscv/blob/JSON/doc/JSON.md.

[joydeep049]

I did not understand in which script I'm supposed to add the above suggested code that looks for functions like reserved_bits_N
@ThinkOpenly

[ThinkOpenly]

Let's walk through how to figure this out...

The "fields" JSON content is emitted in json_of_field, which is called by json_of_fields, which gets the fields data from the "encodings" Hashtbl.

The "encodings" Hashtbl is populated (Hashtbl.add encodings) in parse_encdec_mpat. You can perhaps infer by the name of this function that it handles the AST representations of mapping clause encdec instances like that shown in #21 (comment):

mapping clause encdec = FENCEI()
  <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111

There are two parts to addressing this issue:

1. Tag the fields that are optional. This would change the above "encdec" mapping to something like:

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

   You'll also need to define those "reserved_bits_N" functions, likely as identity functions. These definitions would probably go in either model/prelude.sail or model/riscv_types.sail. I'm thinking the latter is best.
2. In the OCaml code, recognize those reserved fields, and emit JSON reflecting that. I think the best place to add this code is when emitting the JSON, so you'd look in json_of_field. Here, you'll check to see if the field name is something like "reserved_bits_N(op)" and emit the field name of "op", and emit another key/value pair of "reserved" and a boolean.

Lastly, make sure your changes build correctly and produce the expected results by following the "how to test changes" link in #21 (comment).

I hope that helps!

[joydeep049]

@ThinkOpenly
I am able to fully understand what to do here. But I can seem to find the Hashtbl, json_of_field and json_of_fields in the Sail Repository only, not in this repo.
Is parse_encdec_mpat defined in this repo?

[ThinkOpenly]

I can seem to find the Hashtbl, json_of_field and json_of_fields in the Sail Repository only, not in this repo. Is parse_encdec_mpat defined in this repo?

That's a good question. There are two complementary repositories involved in the project with respect to this issue:

• https://github.com/ThinkOpenly/sail-riscv (this repository): This contains just the RISC-V Sail code, so the syntactic changes would go here. For example, changing something from field to reserved(field).
• https://github.com/ThinkOpenly/sail: As you found, this is where the parsing code (in OCaml) resides. So, this is indeed where to find Hashtbl, json_of_field, json_of_fields, and parse_encdec_mpat.