Simplify prelude.sail by including generic_equality.sail and mapping.sail

[Timmmm]

This change includes generic_equality.sail and mapping.sail from the Sail standard library which defines a lot of things that were defined in prelude.sail.

I also removed reg_deref which as far as I can tell is removed.

hex_bits_20 is commented out because it is defined by mapping.sail (but none of the others are; I am not sure why).

[github-actions]

Unit Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit 6578d5d. ± Comparison against base commit dbea780.

[Alasdair]

LGTM.

reg_deref isn't removed, it's just called __deref in the library, and it's used to desugar the "*(ref R) = 0xABCD" syntax for de-referencing register references.

I'm not sure why the library defines hex_bits_20 only. You can technically define a polymorphic hex_bits in current Sail, but it's not very useful, as it has the type:

val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string)

which means it isn't a drop-in replacement, as the requirement to specify the width on the left hand side means it always has to go on the other side of the assembly mappings so:

mapping clause assembly = C_NOP_HINT(imm) <-> "c.nop.hint." ^ hex_bits_6(imm)

becomes

mapping clause assembly = C_NOP_HINT(hex_bits(6, imm)) <-> "c.nop.hint." ^ imm

what we could do is specify all the hex_bits_N functions as special cases of the polymorphic one though, which would cut out a lot of the boilerplate.

[Alasdair]

I added the hex_bits_N functions (up to 32) here: rems-project/sail@f228c2b

We could copy those definitions into the prelude_mapping file until the next sail release then just replace with an $include <hex_bits>. I'm not sure if we prefer uppercase or lowercase hex, those definitions print as lowercase, but you can replace the hex_str with hex_str_upper to change that.

[jrtc27]

Don't you also need _matches_prefix functions for strings?

[Alasdair]

You don't -- currently string append patterns (which used those functions) are quarantined by the effect system marking them non-executable, then they are removed from the model. The previous implementation was so broken it was causing issues elsewhere. I have some ideas for how to fix them but I don't plan on using any kind of _matches_prefix functions. In general they can only work in some backends, so we will need to use the effect system or some other static analysis pass to ensure the semantics of instructions never depends on string append patterns. It's not a super high priority thing for me right now though.

Now I'm working on hardware model checking, compiling Sail into SystemVerilog, so I'll likely try to become a bit more strict about how strings in general (and linked lists for similar reasons) are used, as they don't play very nicely with Jasper.

[jrtc27]

Ok, them being gone is simplifying, it was causing all kinds of problems for making rems-project/sail#57 work in the general case. I guess that should be closed now?

[Alasdair]

Oh, that's an old PR. Yes, it shouldn't be needed now.

I like how I said I'd look at it tomorrow (four-ish years ago) then didn't say anything more... If I do that again you should bug me some more. I suspect I probably had some grand plan of just fixing the whole string mapping situation even then. I don't think I've actually achieved that but the badness is more constrained at least. So much pain for a feature that just looked cutesy in our POPL paper.

[jrtc27]

I think you said you'd look at it, then I went away, poked it some more and discovered it didn't actually work for all cases, and doing so properly would be a whole project in and of itself, so we both just forgot about it... :)

[Timmmm]

@Alasdair I copy & pasted your new hex_bits.sail into this repo (see latest commit), however I ran into two issues:

1. Sail's lib/mapping.sail still has hex_bits_20 - presumably you should remove that and replace it with $include <hex_bits.sail>?
2. I get this error:

encountered a variety of string append pattern that is not yet implemented: s ^ s#

No file/line number. Do I need to update my Sail compiler? Maybe the hex_bits fix will need to wait until the next Sail release.

[github-actions]

Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit 4f3946f. ± Comparison against base commit 393e7ed.

♻️ This comment has been updated with latest results.

[Alasdair]

Yes, you would need the latest released version I think.

Looking at the prelude mapping.sail file, it's just bad, I don't think we should be including it.

[Alasdair]

I made the lib mapping file what it should be, at least for spc, opt_spc, and def_spc. It's not clear that it should be defining it's own string manipulation functions but I left those alone for now https://github.com/rems-project/sail/blob/5ff1cb6f8d901969923002155eadd852140a63a6/lib/mapping.sail

[Timmmm]

Ah great. I'll copy that file in too.

[Timmmm]

This worked for me with Sail 0.17.1. I think that's the version I used anyway. It seems like there's a very confusing missing dependency link in Sail's make install where if you switch versions it will build and install the new code, but it won't update the version of git hash! So you end up with sail -version that says you have Sail 0.15 (some git hash) but you actually have a totally different version/hash.

[Alasdair]

Yes, I think that can happen if you build on one commit, then checkout another and build without a make clean.

[Timmmm]

This is ready to merge.

[nwf-msr]

As a heads up, I think once sail 0.17.2 or 0.18 is released, the hex_bits.sail and mapping.sail herein will be subsets of its standard libraries. (See in particular my rems-project/sail@557282b expanding hex_bits.sail)

[Timmmm]

Yep the intention is to remove these once sail is new enough. That may happen before this is merged!

[Timmmm]

@billmcspadden-riscv any objection to merging this?