Add initial Sail snippets

[Timmmm]

Add Makefile targets to download the Sail JSON bundle from Github releases (it's a few MB so this avoids bloating the repo).

I updated a few scalar crypto functions that already had copy & pasted Sail code to use the model source instead. The result is almost identical.

See #1369.

[Timmmm]

Note, @Alasdair has demonstrated a fancier version of this with syntax highlighting and hyperlinked code (e.g. so you can click on <<< to see what it means), but that isn't used here yet.

Before:

After:

(The Sail code has changed a little since that was copy/pasted.)

[wmat]

Question, do we need to care about the version of the SAIL model we're pulling the index from? I recognize SAIL isn't at v.1.0 yet so perhaps at this point we don't, but in the future should we? Or perhaps we pair a SAIL version with the riscv-isa-manual src when we build a release for publication?

[Timmmm]

There are a couple of aspects to that:

1. We obviously want to point to a fixed version so it is repeatable. We don't want to just always use master. That is covered here by the URL being version tracked in Git. We should maybe include the Git hash of the sail-riscv repo, or maybe the hash of the JSON file just in case (a URL can change or disappear). I don't think that is a blocker though.
2. The spec sometimes changes behaviour - sometimes in backwards incompatible ways - and currently the sail-riscv repo only implements one version. We obviously want the Sail code's behaviour to match the version of the ISA manual it is included in.

For the second point my vague plan was:

1. Finish adding a way to actually specify the spec versions to the Sail model. I made an attempt here but it needs to be reworked.
2. Once that is done, use Alasdair's fancy Sail-rewriting system to generate the code for the "current" spec version. Basically you can take code that is like:

if version == 1.12
   foo
else if version == 1.13
   bar
...

and you say "yeah but I know the version is 1.12", and then it will only insert foo.

I don't think Alasdair has published that yet so I'm not exactly sure what you have to do but it will probably end up with us having separate .json bundles for each version.

However, I also don't think that is a blocker. I would suggest initially we just use it for snippets where the behaviour has never changed and is unlikely to change in future.

[wmat]

Excellent, thanks Tim, I mostly wanted to be sure the versioning question was on the table for discussion. So thanks for confirming to me that it is indeed out there.

[nadime15]

I'm curious what parts of sail are actually supposed to be integrated into the risc-v manual? Are we just talking about the execution function of each instruction?

[Timmmm]

Mostly the execute clauses, but I think there are other bits too where the behaviour would be much clearer with the Sail code, e.g. interrupt handling:

/* Interrupts are prioritized in privilege order, and for each
 * privilege, in the order: external, software, timers.
 */
function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
  let ip = Mk_Minterrupts(ip);
  if      ip[MEI] == 0b1 then Some(I_M_External)
  else if ip[MSI] == 0b1 then Some(I_M_Software)
  else if ip[MTI] == 0b1 then Some(I_M_Timer)
  else if ip[SEI] == 0b1 then Some(I_S_External)
  else if ip[SSI] == 0b1 then Some(I_S_Software)
  else if ip[STI] == 0b1 then Some(I_S_Timer)
  else                        None()
}

/* Given the current privilege level, return the pending set
 * of interrupts for the highest privilege that has any pending.
 *
 * We don't use the lowered views of {xie,xip} here, since the spec
 * allows for example the M_Timer to be delegated to the S-mode.
 */
function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
  // mideleg can only be non-zero if we support Supervisor mode.
  assert(extensionEnabled(Ext_S) | mideleg.bits == zeros());

  let pending_m = mip.bits & mie.bits & ~(mideleg.bits);
  let pending_s = mip.bits & mie.bits & mideleg.bits;

  let mIE = (priv == Machine    & mstatus[MIE] == 0b1) | priv == Supervisor | priv == User;
  let sIE = (priv == Supervisor & mstatus[SIE] == 0b1) | priv == User;

  if      mIE & (pending_m != zeros()) then Some((pending_m, Machine))
  else if sIE & (pending_s != zeros()) then Some((pending_s, Supervisor))
  else None()
}

/* Examine the current interrupt state and return an interrupt to be *
 * handled (if any), and the privilege it should be handled at.
 */
function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege)) = {
  match getPendingSet(priv) {
    None()       => None(),
    Some(ip, p)  => match findPendingInterrupt(ip) {
                      None()  => None(),
                      Some(i) => Some((i, p)),
                    }
  }
}

(And I think this code could be improved a fair bit too before we include it, e.g. getPendingSet() could be inlined, not having variables called i etc.)

[AFOliveira]

@Timmmm I have a question on this. Can you pull Sail code per instruction? Or in case of switch-case style of Sail, you are pulling that whole block?

[Timmmm]

Yeah you can, though not in this PR. E.g. for this:

function clause execute (UTYPE(imm, rd, op)) = {
  let off : xlenbits = sign_extend(imm @ 0x000);
  X(rd) = match op {
    RISCV_LUI   => off,
    RISCV_AUIPC => get_arch_pc() + off
  };
  RETIRE_SUCCESS
}

You can say "show me the code for when op=RISCV_AUIPC and it will give you

function clause execute (UTYPE(imm, rd, op)) = {
  let off : xlenbits = sign_extend(imm @ 0x000);
  X(rd) = get_arch_pc() + off;
  RETIRE_SUCCESS
}

However I've only seen that in a prototype that @Alasdair showed. I don't know if it has made it into the Sail compiler or asciidoctor-sail yet.

Also someone brought up the valid point that it might be confusing to see synthetic code in the ISA manual that isn't literally in the Sail model. But... I think it is probably fine anyway. We can hyperlink to the place the code came from (also part of that prototype), and maybe even add a little disclaimer explaining the situation.

[nadime15]

You can learn more about the features of the asciidoctor-sail plugin here: https://github.com/Alasdair/asciidoctor-sail

[AFOliveira]

@Timmmm @Alasdair I am currently working in trying to get an index of all instructions into this manual, see #1603. Do you think that whenever I have that index, it would be as easy as a couple lines of code to get that Sail into the index?

[AFOliveira]

You can learn more about the features of the asciidoctor-sail plugin here: https://github.com/Alasdair/asciidoctor-sail

I've came across that before @nadime15, but is that where all this transformations @Timmmm mentioned is being done?

[wmat]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet.

[nadime15]

@AFOliveira The last chapter, Splitting Sail Definitions, seems to describe what @Timmmm demonstrated. However, I would double-check if it actually works as expected. For instance, when I tried pulling in Sail code, including the function header (function clause execute), I had to change it a bit to make it work, which differed slightly from the description in the PDF.

[AFOliveira]

@AFOliveira The last chapter, Splitting Sail Definitions, seems to describe what @Timmmm demonstrated. However, I would double-check if it actually works as expected. For instance, when I tried pulling in Sail code, including the function header (function clause execute), I had to change it a bit to make it work, which differed slightly from the description in the PDF.

I've tried this many months ago and I was also not able to do so. Thus, my question on individual instructions, rather than blocks. Isn't what @Timmmm was describing a new feature, that may not be on that repo yet?

[AFOliveira]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet.

Moreover, I see that as a problem given that the information is not going to be static in this manual, how would ratification look? Would the output pdf be ratified rather than the asciidoc source? Would we it be dependent on Sail being ratified and this tool?

Please don't misunderstand me, I think this is awesome work, I just want to poke around and understand how this process may happen.

[wmat]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet.

Moreover, I see that as a problem given that the information is not going to be static in this manual, how would ratification look? Would the output pdf be ratified rather than the asciidoc source? Would we it be dependent on Sail being ratified and this tool?

Please don't misunderstand me, I think this is awesome work, I just want to poke around and understand how this process may happen.

The thinking was/is that the SAIL index would be versioned at the time a riscv-isa-manual release was published with the SAIL index version described within the release as a point-in-time index. However, I don't believe a decision was ever made for how to do this. I was always hopeful that v1.0 of the SAIL model would be the first version included with a published ISA release.

[Alasdair]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet

It should just work with any Asciidoctor output format, for example the Sail manual is built with the plugin outputting to html. You only need asciidoctor.js if you want to build Asciidoc into html client-side right? Last I looked, the RISC-V manuals used quite a few other plugins like asciidoctor-bibtex and asciidoctor-mathematical, do those work with asciidoctor.js?

I've came across that before @nadime15, but is that where all this transformations @Timmmm mentioned is being done?

Currently the translation is done by Sail - provided it's explicitly requested with an annotation on the definition. Right now the structure of the Sail tries to follow the granularity of the unprivileged spec, so because 4.2.2 has a single section and encoding diagram for "Integer Register-Register Operations" which combines SLL, SRA, ADDW etc. we also do the same.

I think for the transformation to really work it might require the development version of the Sail compiler/plugin, as I had to implement additional annotations in the AST to correctly re-sugar the code after the constant-folding and constant-propagation passes are applied to simplify the definition. I'm planning a new release soon though.

[AFOliveira]

Currently the translation is done by Sail - provided it's explicitly requested with an annotation on the definition. Right now the structure of the Sail tries to follow the granularity of the unprivileged spec, so because 4.2.2 has a single section and encoding diagram for "Integer Register-Register Operations" which combines SLL, SRA, ADDW etc. we also do the same.

I think for the transformation to really work it might require the development version of the Sail compiler/plugin, as I had to implement additional annotations in the AST to correctly re-sugar the code after the constant-folding and constant-propagation passes are applied to simplify the definition. I'm planning a new release soon though

@Alasdair I may not have fully understood your answer, but from what you're saying, in cases like Integer Register-Register Operations, we can't split them apart for now, correct? Would the idea be to place them in the spec exactly where that text appears so they serve as complementary information?

I see how this approach might make merging into the spec easier in its current form, but I find the switch-case style of Sail somewhat problematic. The way the spec is written in those sections makes it difficult to locate information throughout the manual, and importing that structure into Sail seems to perpetuate that issue—would you agree?

I'm working on developing a well-structured instruction index (similar to what other ISAs have) to improve manual searchability. Ideally, I’d love to have Sail indexed per instruction, but I assume that isn't feasible yet. My questions were meant to clarify whether, regardless of the current Sail source code, we will eventually be able to see this information split. Is that something your new release will enable?

[Alasdair]

I see how this approach might make merging into the spec easier in its current form, but I find the switch-case style of Sail somewhat problematic. The way the spec is written in those sections makes it difficult to locate information throughout the manual, and importing that structure into Sail seems to perpetuate that issue—would you agree?

I would agree with this regarding the structure of both the Sail and the manual. We could re-factor the Sail, but I do think staying as close as possible to current manual is also important.

My questions were meant to clarify whether, regardless of the current Sail source code, we will eventually be able to see this information split. Is that something your new release will enable?

I hope so! I did some experiments a while ago where I generated a big html document of all the instructions in the Sail model with this splitting a while ago, and it seemed to work. Right now I'm quite focused on configurability and modularisation of the model, but this is something I'd like to re-visit.

[Timmmm]

Do you think that whenever I have that index, it would be as easy as a couple lines of code to get that Sail into the index?

Yes, should be.

asciidoctor-sail plugin currently only targets PDF (as far as I know)

It definitely works with HTML too. We've been using it for CHERI for a long time.

Moreover, I see that as a problem given that the information is not going to be static in this manual, how would ratification look?

It is static. sail.json.url links to a specific release. We could add a hash in there for double checking if you want.

When a new release of the Sail model happens there would be a PR to update the sail.json.url to that file, and at that point we would review the changes in the document (which may be a little tedious but we can cross that bridge later).

[AFOliveira]

Thank you all for the explanations!
Sorry if I deviated the PR discussion a bit, I'll see how I can integrate this with my work and further ask questions if I need :)

[Timmmm]

Who do we need to review this? There's loads of scope for improvements in future but I think we need to actually start somewhere and this feels like an uncontroversial first step.

[wmat]

@aswaterman any thoughts here?