Float: Add floating-point equals API in sail model

[Incarnation-p-lee]

trafficstars

This patch would like to introduce the floating-point equals API into the sail model. Then floating-point equals will be invoked in sail instead of the c_emulator.

• Add enum-like immutable exception flags and types to commons.
• Add float equals API for half, single and double floating-point.
• Replace the extern call of softfloat interface by the sail model.
• Adjust the build system for new files.
• Passed 712 out of 712 from ./test/run_tests.sh.

[Incarnation-p-lee]

Is there any way to avoid the global variables for the new functions and just return the result directly (might need something like #340 to be merged first)?

Thanks for the comments.

I think at least we can return the float result directly in riscv_softfloat_eq. But for migration from emulator to sail, I may prefer to do it in another PR as I am green hand for sail and I would like to limit the risk here. How do you think of it?

For #340 , I am afraid we may not need this anymore if the softfloat migrates to sail. The sofefloat in c_emulator will be depreciated soon as I understand. Feel free to correct me if any misleading.

[Timmmm]

For https://github.com/riscv/sail-riscv/pull/340 , I am afraid we may not need this anymore if the softfloat migrates to sail. The sofefloat in c_emulator will be depreciated soon as I understand.

I think that was an aspirational hope rather than someone actually saying "I will do this". It would be great though!

I need to take another look at #340. IIRC it failed because of the OCaml emulator (which we don't use) and I don't know OCaml...

Probably shouldn't block this anyway.

[Incarnation-p-lee]

For #340 , I am afraid we may not need this anymore if the softfloat migrates to sail. The sofefloat in c_emulator will be depreciated soon as I understand.

I think that was an aspirational hope rather than someone actually saying "I will do this". It would be great though!

I need to take another look at #340. IIRC it failed because of the OCaml emulator (which we don't use) and I don't know OCaml...

Probably shouldn't block this anyway.

Thanks for the comments. Lots of useful items, especially for the green hands to sail like me. I will address it soon.

[jrtc27]

Please avoid creating 16/32/64 copies of every function. You should in general be able to write one polymorphic function that handles all sizes.

[Incarnation-p-lee]

Thanks all, addressed comments with all fp tests passed.

[Timmmm]

This is much better, though I think you could go even further. There's not really much point to the riscv_f16Eq() etc functions now that they aren't using FFI.

You could just delete them, and then change the code that uses them to call your new functions instead.

Note that there's already this function in the vector extension:

val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function fp_eq(op1, op2) = {
  let (fflags, result_val) : (bits_fflags, bool) = match 'm {
    16  => riscv_f16Eq(op1, op2),
    32  => riscv_f32Eq(op1, op2),
    64  => riscv_f64Eq(op1, op2)
  };
  accrue_fflags(fflags);
  result_val
}

I would:

1. Delete fp_eq from the vector extension.
2. Delete riscv_f16Eq, riscv_f32Eq and riscv_f64Eq.
3. Move everything from riscv_float_common.sail back to where it started.
4. Change your code to be like this (not tested!):

val float_equal : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool)
function float_equal(op1, op2) = {
  let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2);
  let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2);

  let fflags = if is_nan & is_snan then float_flag_invalid else zeros();

  let is_equal : bool = if not(is_nan)
                        then op1 == op2 | ((op1 | op2) << 1) == zeros()
                        else false;

  (fflags, is_equal)
}

val float_equal_raise_flags : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function float_equal_raise_flags(op1, op2) = {
  let (is_equal, fflags) = float_equal(op1, op2);
  accrue_fflags(fflags);
  is_equal
}

And then change all the code that used fp_eq to call float_equal_raise_flags, and all the code that called riscv_f16Eq etc. to call float_equal.

Hope that makes sense! Thanks for the contribution btw!

[Incarnation-p-lee]

This is much better, though I think you could go even further. There's not really much point to the riscv_f16Eq() etc functions now that they aren't using FFI.

You could just delete them, and then change the code that uses them to call your new functions instead.

Note that there's already this function in the vector extension:

val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function fp_eq(op1, op2) = {
  let (fflags, result_val) : (bits_fflags, bool) = match 'm {
    16  => riscv_f16Eq(op1, op2),
    32  => riscv_f32Eq(op1, op2),
    64  => riscv_f64Eq(op1, op2)
  };
  accrue_fflags(fflags);
  result_val
}

I would:

1. Delete fp_eq from the vector extension.
2. Delete riscv_f16Eq, riscv_f32Eq and riscv_f64Eq.
3. Move everything from riscv_float_common.sail back to where it started.
4. Change your code to be like this (not tested!):

val float_equal : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool)
function float_equal(op1, op2) = {
  let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2);
  let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2);

  let fflags = if is_nan & is_snan then float_flag_invalid else zeros();

  let is_equal : bool = if not(is_nan)
                        then op1 == op2 | ((op1 | op2) << 1) == zeros()
                        else false;

  (fflags, is_equal)
}

val float_equal_raise_flags : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function float_equal_raise_flags(op1, op2) = {
  let (is_equal, fflags) = float_equal(op1, op2);
  accrue_fflags(fflags);
  is_equal
}

And then change all the code that used fp_eq to call float_equal_raise_flags, and all the code that called riscv_f16Eq etc. to call float_equal.

Hope that makes sense! Thanks for the contribution btw!

Thanks for comments. I see, looks you would like to suggest get rid of softfloat_interface.sail up to a point. I plan to do that later and make this change simple enough for review. But as you mentioned already, I will add that part to this PR.

[Incarnation-p-lee]

Updated with run_fp_tests.sh passed. By the way, keep float_common files for some type(s) and/or const- variables. As we will remove the file softfloat_interface, I may prefer to let the softfloat_interface depends on the float_common instead of the float_common depends on the softfloat_interface.

[Incarnation-p-lee]

LGTM just some minor nits left

Thanks a lot for comments. Addressed all except the is_equal type annotation. Passed the run_fp_tests.sh.

[Timmmm]

Addressed all except the is_equal type annotation

Ah yeah sometimes the type inference doesn't work entirely intuitively...

All LGTM anyway!

[Incarnation-p-lee]

Addressed all except the is_equal type annotation

Ah yeah sometimes the type inference doesn't work entirely intuitively...

All LGTM anyway!

Thanks. Looks like I have no authority to merge, will continue the rest part of softfloat following the pattern of this PR.

[Timmmm]

Yeah currently @billmcspadden-riscv is chief merger, but he is ill at the moment.

Also I finally figured out why I can't resolve my conversations:

You can resolve a conversation in a pull request if you opened the pull request or if you have write access to the repository where the pull request was opened.

That seems bonkers - surely the person who started a conversation should be able to resolve it? I guess it explains it at least! Anyway since you opened the PR you should be able to resolve all my conversations.

[billmcspadden-riscv]

Yes, I’m in hospital right now and have limited ability to do much work. Martin Burger can also do a merge as well.

The question for the team is: do we want to do small, incremental merges for this project, or do we want to put this on a feature branch (with a full merge once all the work is done) like what we did for Vector last year? I think we should just go ahead and do the small incremental merges on main. Thots?

Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309

On Tue, Feb 13, 2024 at 6:04 AM Tim Hutt @.***> wrote:

Yeah currently @billmcspadden-riscv https://github.com/billmcspadden-riscv is chief merger, but he is ill at the moment.

Also I finally figured out why I can't resolve my conversations:

You can resolve a conversation in a pull request if you opened the pull request or if you have write access to the repository where the pull request was opened.

That seems bonkers - surely the person who started a conversation should be able to resolve it? I guess it explains it at least! Anyway since you opened the PR you should be able to resolve all my conversations.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/pull/403#issuecomment-1941368007, or unsubscribe https://github.com/notifications/unsubscribe-auth/AXROLOCJPW74P7MSTYEVNCTYTNJGPAVCNFSM6AAAAABC5HFXZCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNBRGM3DQMBQG4 . You are receiving this because you were mentioned.Message ID: @.***>

[Incarnation-p-lee]

@Timmmm Resolved all conversations as LGTM, thanks again for the review and help.

@billmcspadden-riscv Take care. I may prefer small incremental merges.

[Timmmm]

Yeah I agree - this is a change that can easily be done piecemeal so we should do so. @Incarnation-p-lee probably a good idea to squash your commits.

[Incarnation-p-lee]

piecemeal

Cannot agree anymore, take squash merger here and we will see only one commit from the main branch. That would be much clear.

[jrtc27]

Whilst float_eq is relatively straightforward to get right, actual arithmetic operations are much more complicated. What is your strategy for ensuring correctness?

[github-actions[bot]]

Test Results

712 tests  ±0   712 :white_check_mark: ±0   0s :stopwatch: ±0s   6 suites ±0     0 :zzz: ±0    1 files   ±0     0 :x: ±0 

Results for commit a05b202d. ± Comparison against base commit 9602e3a5.

[Incarnation-p-lee]

Whilst float_eq is relatively straightforward to get right, actual arithmetic operations are much more complicated. What is your strategy for ensuring correctness?

As far as I can see, the run_tests.sh (or even simple run_fp_tests.sh) can be the accepted criteria for both the PR and the correctness. That is how I do currently. But do you have any suggestions for this?

[Timmmm]

As far as I can see, the run_tests.sh (or even simple run_fp_tests.sh) can be the accepted criteria for both the PR and the correctness. That is how I do currently. But do you have any suggestions for this?

I don't think run_fp_tests.sh is very extensive unfortunately. There are some more extensive tests (see the "Other software for testing floating-point" bit too), but we'd need to compile them for the Sail model. Maybe a good test case for Bill's new system.

I wonder if we could build a small Sail program in C with both the old (SoftFloat) and new (Sail) versions of the functions and then use CBMC to prove they are the same.

[Incarnation-p-lee]

As far as I can see, the run_tests.sh (or even simple run_fp_tests.sh) can be the accepted criteria for both the PR and the correctness. That is how I do currently. But do you have any suggestions for this?

I don't think run_fp_tests.sh is very extensive unfortunately. There are some more extensive tests (see the "Other software for testing floating-point" bit too), but we'd need to compile them for the Sail model. Maybe a good test case for Bill's new system.

I wonder if we could build a small Sail program in C with both the old (SoftFloat) and new (Sail) versions of the functions and then use CBMC to prove they are the same.

I see your point. run_fp_test.sh can only ensure the correctness of the part referenced but cannot cover everything of the softfloat in c_emulator.

I think it is one generic question about how to test the sail code. It looks like we need to think about it for a solution and I may have no idea for now, I will talk to bill in the next dev-partner meeting for more details.

[Timmmm]

I wonder if we could build a small Sail program in C with both the old (SoftFloat) and new (Sail) versions of the functions and then use CBMC to prove they are the same.

Unfortunately this doesn't work - I forgot about GMP; it gets stuck unwinding a loop in not_bits(). There are some options that look like they would help: --Ofixed-int --Ofixed-bits, but they cause a load of compilation errors for me. Oh well.

[Incarnation-p-lee]

Sorry for disturbing. If there are no more comments to address, can we squash merge this PR when free? Then we can continue the rest API implementation of float in sail.

[jrtc27]

Sorry for disturbing. If there are no more comments to address, can we squash merge this PR when free? Then we can continue the rest API implementation of float in sail.

Well my comments remain unresolved, and your responses haven't changed my opinion... seems slightly untoward for you to be saying this when there are outstanding comments you've just shrugged off.

[Incarnation-p-lee]

Sorry for disturbing. If there are no more comments to address, can we squash merge this PR when free? Then we can continue the rest API implementation of float in sail.

Well my comments remain unresolved, and your responses haven't changed my opinion... seems slightly untoward for you to be saying this when there are outstanding comments you've just shrugged off.

Yeah, sorry for the misunderstanding. I reply your comments inline about why but NO response from your side. There are two items here.

1. The comments change for the global, would like to double confirm with you whether you wish to revert this change or not.
2. The type declaration for float flags and/or status, do you prefer to move them together to the new files or only the referenced part to the new file?

Could you please help to double-check about above two items and then I can make the changes? Thanks a lot.

[Incarnation-p-lee]

Well my comments remain unresolved, and your responses haven't changed my opinion... seems slightly untoward for you to be saying this when there are outstanding comments you've just shrugged off.

Well well, wait for a moment. You say there are OUTSTANDING comments, are you indicating @Timmmm approve this PR without notice these OUTSTANDING comments? I think this is not a good way to communicate, especially in the PR review.

Indeed, you leave comments, I reply comments and there is no further response from your side. So I suppose there is no action required and ping if we can move on.

After that I would like to fast the process if there is no more comments to address, (I said IF in case someone else would like to review soon). And then you emphasize the comments are outstanding, and I just shrugged off? I don't think it is the right way to do the communication. I said in comments I am totally OK to make the change as you suggestion but I cannot guess your option until you reply the comments.

Guess how I did GCC PATCH review for a similar case:

1. You left the comments first.
2. Then I reply why I need to do this.
3. After some time, there is no respone, I will ping if it is OK for trunk.
4. Then you insist your option and reply the comments.
5. I got your point and made the changes as you suggested.
6. Then PR was accepted and merged into the trunk.

I think the above should be a better way to communicate in the PR review. Please feel free to correct me if any misleading.

[jrtc27]

Well my comments remain unresolved, and your responses haven't changed my opinion... seems slightly untoward for you to be saying this when there are outstanding comments you've just shrugged off.

Well well, wait for a moment. You say there are OUTSTANDING comments, are you indicating @Timmmm approve this PR without notice these OUTSTANDING comments? I think this is not a good way to communicate, especially in the PR review.

Indeed, you leave comments, I reply comments and there is no further response from your side. So I suppose there is no action required and ping if we can move on.

After that I would like to fast the process if there is no more comments to address, (I said IF in case someone else would like to review soon). And then you emphasize the comments are outstanding, and I just shrugged off? I don't think it is the right way to do the communication. I said in comments I am totally OK to make the change as you suggestion but I cannot guess your option until you reply the comments.

Guess how I did GCC PATCH review for a similar case:

1. You left the comments first.
2. Then I reply why I need to do this.
3. After some time, there is no respone, I will ping if it is OK for trunk.
4. Then you insist your option and reply the comments.
5. I got your point and made the changes as you suggested.
6. Then PR was accepted and merged into the trunk.

I think the above should be a better way to communicate in the PR review. Please feel free to correct me if any misleading.

Can you please tone it down several levels?

And if you really care about the details, Tim approved it before my review. But people are entirely free to give their own independent reviews; just because one person's happy doesn't mean you can ignore someone who would like to see changes.

Also, we're talking under 48 hours here. It's not reasonable to expect everyone to always be able to reply within that time period, and pinging a patch that frequently is a bit too much IMO (a week is a more standard time period, at least in the communities I generally contribute to). And when you do so, the more constructive thing to do is ask whether your comments address the concerns or not, not to assume that you've changed someone's mind just because they have yet to say anything and push for merging.

I guess the underlying point is that code review isn't a fight to be won, it's a conversation that's aiming to achieve the best reasonable outcome.

[jrtc27]

Also: projects like GCC are very different to something like sail-riscv. Many of the people reviewing patches on the GCC mailing list are full-time employees paid by their organisation to do that, or at least a large part of their job. That is not the case here; it is nobody's full-time job, for many it's just a small part of their job, and many are also volunteers. So please consider that before having high expectations of how quickly people will reply to you. And of course the more time spent discussing things like this, the less time spent doing actually useful work...

[Incarnation-p-lee]

Well my comments remain unresolved, and your responses haven't changed my opinion... seems slightly untoward for you to be saying this when there are outstanding comments you've just shrugged off.

Well well, wait for a moment. You say there are OUTSTANDING comments, are you indicating @Timmmm approve this PR without notice these OUTSTANDING comments? I think this is not a good way to communicate, especially in the PR review. Indeed, you leave comments, I reply comments and there is no further response from your side. So I suppose there is no action required and ping if we can move on. After that I would like to fast the process if there is no more comments to address, (I said IF in case someone else would like to review soon). And then you emphasize the comments are outstanding, and I just shrugged off? I don't think it is the right way to do the communication. I said in comments I am totally OK to make the change as you suggestion but I cannot guess your option until you reply the comments. Guess how I did GCC PATCH review for a similar case:

1. You left the comments first.
2. Then I reply why I need to do this.
3. After some time, there is no respone, I will ping if it is OK for trunk.
4. Then you insist your option and reply the comments.
5. I got your point and made the changes as you suggested.
6. Then PR was accepted and merged into the trunk.

I think the above should be a better way to communicate in the PR review. Please feel free to correct me if any misleading.

Can you please tone it down several levels?

Take it easy, I think our goal is the same for the the best reasonable outcome.

And if you really care about the details, Tim approved it before my review. But people are entirely free to give their own independent reviews; just because one person's happy doesn't mean you can ignore someone who would like to see changes.

I agree with you on this point as I said in comments, I am totally Ok for making changes.

Also, we're talking under 48 hours here. It's not reasonable to expect everyone to always be able to reply within that time period, and pinging a patch that frequently is a bit too much IMO (a week is a more standard time period, at least in the communities I generally contribute to). And when you do so, the more constructive thing to do is ask whether your comments address the concerns or not, not to assume that you've changed someone's mind just because they have yet to say anything and push for merging.

I guess the underlying point is that code review isn't a fight to be won, it's a conversation that's aiming to achieve the best reasonable outcome.

I think the point is not about the 48 hours or not. I think it is important to make things clear and an efficient way to communicate. You can just reply first comment similar to "Yes, please revert this change", and the second one similar to "Yes, please move all related types to the new file.", instead of saying outstanding, and shrugged off.

I think that should be more clear here. Agree there is no place to get someone to win, just to make it clear to both of us.

[Incarnation-p-lee]

Also: projects like GCC are very different to something like sail-riscv. Many of the people reviewing patches on the GCC mailing list are full-time employees paid by their organisation to do that, or at least a large part of their job. That is not the case here; it is nobody's full-time job, for many it's just a small part of their job, and many are also volunteers. So please consider that before having high expectations of how quickly people will reply to you. And of course the more time spent discussing things like this, the less time spent doing actually useful work...

Understood the timing you mentioned, sorry I didn't get any information from this repo about it. I think we are on the same page now. I will make the changes as your comments soon.