fix disassembly problems

[KotorinMinami]

Fix Issue #21 by adding function to deal with the sign number

[github-actions]

Test Results

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

Results for commit f6e1f25. ± Comparison against base commit e1242d8.

♻️ This comment has been updated with latest results.

[Timmmm]

I think this is good, and doesn't affect execution so there's no risk.

The only slightly odd thing is that hex_bits.sail is only in this repo temporarily until we update the Sail compiler. Then we can $include <hex_bits.sail>. However there's no $include <hex_bits_unsigned.sail> in the Sail "standard library" so this file will hang around. Maybe we want to add that to the Sail compiler?

In any case I don't think that should block merging this.

Can you squash your commits and write a proper commit message. It should be something like

Change immediates to be signed in assembly

These immediates are sign extended and usually interpreted as signed, so it's less confusing to use signed numbers. This also matches SPIKE's disassembly.

(Feel free to copy/paste that.)

[KotorinMinami]

Reopening the PR: Due to certain Git-related actions, I had to close the previous PR and reopen it. @Timmmm I'm glad you can review it and provide feedback. I also think it might be a good idea to submit it to the upstream repository, "sail," if possible. If you're willing, I would appreciate discussing how to submit the application to the upstream repository, including keeping it in sync with relevant modules in the upstream repository. In fact, from the beginning, I intended to implement this function by writing a .ml file. However, upon realizing the need to submit it upstream, I decided to engage with you first. Finally, if the closing and reopening of the PR has caused any unnecessary inconvenience for you, I sincerely apologize.

[Timmmm]

No problem at all! This looks ready to merge to me now. @billmcspadden-riscv do you want to do the honours or would I be ok to merge non-risky PRs like this?

@KotorinMinami I think it probably makes sense to add this file to Sail. No need to write any OCaml; you can just add the file next to the existing hex_bits.sail. Maybe extend it to 64 bits to match that file.

[jrtc27]

I'd like to let @Alasdair look over this first given it's delving into the depths of forward and backwards mapping match functions

[jrtc27]

Your , and + whitespace doesn't conform to the style in a bunch of places, and isn't even self-consistent

[KotorinMinami]

Oh, it's my fault! I apologize for not adhering to the standards.I have made the necessary revisions. Kindly review it once again, please.

[jrtc27]

That's not true? An N-bit signed value is only valid if it's an N-1-bit signed value or it's exactly -(1 << N). This would, for example, allow parsing 0xff as a signed 8-bit value.

[KotorinMinami]

This function is designed to ensure the validity when converting from a string back to an integer. It should correspond to the hex_bits_signed_forwards function.
When using the hex_bits_signed_forwards function to convert a signed numerical value to a string, it will convert negative numbers to their absolute values and then convert them to strings. Additionally, a negative sign is added at the beginning of the result. This validation is specifically tied to this function. When calling this function, it should be ensured that the input parameter is a string converted from hex_bits_signed_forwards and that the number of bits matches.
I believe that in other SAIL files, the calls to this function meet these requirements, as other ASTs only invoke it when the value at this location should be interpreted as a signed number, as mentioned in the issue #21 .
I believe these modifications only make the output of the SAIL simulator more user-friendly and accurate, and they should not cause any other issues.

[jrtc27]

Yes, I know what this function is for. I'm saying it's buggy, because it accepts more inputs than it should.

[KotorinMinami]

I understand then, so I should no matter what, check if the bleedin' string passed in is either a non-negative number or a minus followed by a positive number, ain't it? Just let me have a think on the best way to go about it...

[Timmmm]

Good spot, though I think the behaviour here is the same as the existing unsigned one:

function hex_bits_backwards(n, str) = parse_hex_bits(n, str)
function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str)

void parse_hex_bits(lbits *res, const mpz_t n, const_sail_string hex)
{
  if (strncmp(hex, "0x", 2) != 0) {
    goto failure;
  }

  mpz_t value;
  mpz_init(value);
  if (mpz_set_str(value, hex + 2, 16) == 0) {
    res->len = mpz_get_ui(n);
    mpz_set(*res->bits, value);
    mpz_clear(value);
    return;
  }
  mpz_clear(value);

  // On failure, we return a zero bitvector of the correct width
failure:
  res->len = mpz_get_ui(n);
  mpz_set_ui(*res->bits, 0);
}

bool valid_hex_bits(const mpz_t n, const_sail_string hex) {
  if (strncmp(hex, "0x", 2) != 0) {
    return false;
  }

  for (int i = 2; i < strlen(hex); i++) {
    char c = hex[i];
    if (!((c >= '0' && c <= '9') || (c >= 'a' && c <= 'f') || (c >= 'A' && c <= 'F'))) {
      return false;
    }
  }

  return true;
}

If you do let foo : bits(8) = hex_bits_16("0xFFFF"); it will set res->len to 8 but res->bits to 0xFFFF. IIRC I think that's ok from lbits point of view - you're allowed to have "extra bits"; they're just truncated. Don't quote me on that though, it's been a while since I read sail.c.

Obviously that isn't ideal though. It probably makes sense for valid_hex_bits to actually do something with n. You only need to check the total length and the first non-zero digit so it shouldn't be too hard.

Seeing as that code needs changes I wonder if it makes more sense to just add signed support at the same time in sail.c.

On the other hand, given that it's an existing bug maybe it shouldn't block this? @Alasdair any thoughts?

[Alasdair]

See: rems-project/sail#538

Note that the potential for anything to actually go wrong here is very slim, because we statically check that the string parsing part of the mapping has no semantic effect on the model - which means it never get executed, and therefore the actual behavior of the primitive in the Sail library is mostly irrelevant.

[KotorinMinami]

@Alasdair So, if I understand correctly, you're saying that I just need to keep the solution from my last commit? And this buggy problem will be resolved in the new version release of Sail? Does that mean I can revert the commit and the code will move on to the next review? If that's the case, thank you for your help and clarification. Otherwise, could you please provide me with some further advice?

[Timmmm]

we statically check that the string parsing part of the mapping has no semantic effect on the model

That's really interesting - can you explain more how/where that works? Presumably this check can be disabled otherwise you can't actually use the reverse mapping?

[Alasdair]

@KotorinMinami yes, that seems right

@Timmmm Internally we keep track of what side effects expressions have, and anything with a string append pattern gets specially marked. It would be good to expand this check, because model checkers in EDA tools don't typically have good support for SystemVerilog strings, so if you want to do any kind of model checking with the Sail spec you need to ensure that the semantics doesn't rely on logic involving strings (which would be somewhat tasteless in an ISA spec anyway). Right now this does mean there is no practical way to use the 'string -> ast' side of the mapping , other than as part of the documentation generation flow.

[KotorinMinami]

@jrtc27 @Alasdair Could you please spare some time to move on to the next review ?

[jrtc27]

See comments

[Timmmm]

@jrtc27 any chance you could take another look at this? To refresh your memory, you pointed out that the disassembly direction of the mapping accepted too-large literals, but it turned out that:

1. It was incorrect for the unsigned mapping too.
2. Alasdair has since fixed the issue in the Sail compiler.
3. The Sail compiler doesn't let you use the disassembler anyway.

Thanks!

[Alasdair]

I think we can move forwards with this. I have corrected the implementation of valid_hex_bits and parse_hex_bits so this should now behave as intended.

Even with the previous buggy behaviour this is unlikely to cause any issues for people because we don't currently generate code for the assembly direction, and even go so far as to check that it is not used by any executable parts of the specification. The only place the assembly side of the mapping would really be visible is in the JSON output for documentation.

[jrtc27]

Sure, that's fine. I would like to see this move into the Sail runtime itself though in the long term alongside the unsigned functions, as it's much better equipped to do this efficiently and correctly.