Fix future clause warnings introduced by upcoming sail release

[jordancarlin]

The in-development next version of Sail introduces new warnings to catch incomplete pattern matching from potential future clauses. This refactors riscv_insts_end.sail to avoid this by adding a new wildcard match for undefined extensions and reordering the end clauses.

Warning: Incomplete pattern match statement at model/riscv_insts_zicboz.sail:11.0-8:
11 |function clause extensionEnabled(Ext_Zicboz) = sys_enable_zicboz()
   |^------^
   | 
The following expression is unmatched: <future extension clause>

Warning: Incomplete pattern match statement at model/riscv_insts_end.sail:23.0-8:
23 |function clause execute C_ILLEGAL(s) = { handle_illegal(); RETIRE_FAIL }
   |^------^
   | 
The following expression is unmatched: <future ast clause>(undefined)

[jrtc27]

I don't like this; it silences what would otherwise be actual legitimate incomplete match warnings. That is, now if a new extension is added you don't get a new warning, but previously you would.

[github-actions]

Test Results

396 tests  ±0   396 ✅ ±0   0s ⏱️ ±0s
  4 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 19780f8. ± Comparison against base commit 70edcb0.

[jordancarlin]

I don't like this; it silences what would otherwise be actual legitimate incomplete match warnings. That is, now if a new extension is added you don't get a new warning, but previously you would.

Open to other approaches, but we definitely need to do something otherwise we will introduce new warnings with the next Sail update. Maybe @Alasdair has a suggestion?

[jrtc27]

I don't like this; it silences what would otherwise be actual legitimate incomplete match warnings. That is, now if a new extension is added you don't get a new warning, but previously you would.

Open to other approaches, but we definitely need to do something otherwise we will introduce new warnings with the next Sail update. Maybe @Alasdair has a suggestion?

My view is that the existence of this warning for this code is a bug in the Sail compiler and so should be fixed there. For non-scattered matches it perhaps makes sense, but this warning does not seem to me like a sensible thing to be doing for scattered matches.

[jrtc27]

I don't like this; it silences what would otherwise be actual legitimate incomplete match warnings. That is, now if a new extension is added you don't get a new warning, but previously you would.

Open to other approaches, but we definitely need to do something otherwise we will introduce new warnings with the next Sail update. Maybe @Alasdair has a suggestion?

My view is that the existence of this warning for this code is a bug in the Sail compiler and so should be fixed there. For non-scattered matches it perhaps makes sense, but this warning does not seem to me like a sensible thing to be doing for scattered matches.

Note that rems-project/sail#825 uses a non-scattered match as the motivating example, and there are no tests that use a scattered match. I strongly believe this warning was not intended to occur here and this is an oversight in its implementation.

[jordancarlin]

I don't like this; it silences what would otherwise be actual legitimate incomplete match warnings. That is, now if a new extension is added you don't get a new warning, but previously you would.

Open to other approaches, but we definitely need to do something otherwise we will introduce new warnings with the next Sail update. Maybe @Alasdair has a suggestion?

My view is that the existence of this warning for this code is a bug in the Sail compiler and so should be fixed there. For non-scattered matches it perhaps makes sense, but this warning does not seem to me like a sensible thing to be doing for scattered matches.

Note that rems-project/sail#825 uses a non-scattered match as the motivating example, and there are no tests that use a scattered match. I strongly believe this warning was not intended to occur here and this is an oversight in its implementation.

Yeah, I just found the same thing and agree that it should probably not apply for scattered matches. Will open an issue against sail.

[jrtc27]

I'm guessing this is a result of how scattered definitions are handled. Internally the individual clauses are collected and turned into a single non-scattered definition at the site of the final clause, not where the end is, and so the corresponding scattered enum is still open in its mind. What it should instead be doing is basing it on the end; if the enum is still open when the function is ended then it's fair to give a warning I suppose, but if the enum is not then it shouldn't.

(I forget if it's legal to not include an end, but if so then probably scattered matches without an end should not warn, since they're still open)

[Timmmm]

Yeah I noticed this too. An extra problem is that when we use the new project file you'll theoretically be able to exclude entire extensions from compilation (I think this helps the SV/formal backends), but since I put all of the extension clauses in one file they'll still be defined. And they kind of need to be because some of them are used by e.g. legalise_mstatus(). So we might need the extensionEnabled(_) = false anyway, even though I agree it kind of sucks that we are giving up on the nice new warning.

Also maybe I'm blind but how does this PR fix the warning for execute?

[jordancarlin]

Yeah I noticed this too. An extra problem is that when we use the new project file you'll theoretically be able to exclude entire extensions from compilation (I think this helps the SV/formal backends), but since I put all of the extension clauses in one file they'll still be defined. And they kind of need to be because some of them are used by e.g. legalise_mstatus(). So we might need the extensionEnabled(_) = false anyway, even though I agree it kind of sucks that we are giving up on the nice new warning.

That's a good point. I hadn't considered the interaction with the module system. It seems like maybe the wildcard match is the way to go then. It means we won't get warnings if someone forgets to implement an extensionEnabled clause for a particular extension we won't get a warnings, but I don't see that as a huge issue. Especially since the default will be to have the extensions disabled.

Also maybe I'm blind but how does this PR fix the warning for execute?

For execute moving the end ast before the final ILLEGAL clauses is sufficient.

[jrtc27]

But if they forget to implement extensionEnabled they should get a warning!

[Timmmm]

But if they forget to implement extensionEnabled they should get a warning!

Yeah definitely, but I can't see a way to achieve that given all the constraints.

[Timmmm]

I'd say we should merge this unless @jrtc27 or @Alasdair have a better solution. I'll put it on the meeting agenda.

[bacam]

The other obvious options are to turn the warning off in Sail (I suspect it's too noisy to be useful), or if you do put in a wildcard clause make it an internal_error so that tests will fail in a fast and obvious way.

[jrtc27]

But if they forget to implement extensionEnabled they should get a warning!

Yeah definitely, but I can't see a way to achieve that given all the constraints.

If the compiler were fixed to handle scattered functions more sensibly for this warning then that would achieve it? That’s the right thing to do…

[Alasdair]

As I mentioned in my reply on the Sail issue there is a little bit of subtlety in this issue. For context: Now OCaml 5 is a thing, one of the things I've been doing is re-architecting the Sail frontend to make it more (amenable to) parallelism via separate compilation of different modules and files. In that context, scattered definitions present a bit a of an issue because you don't necessarily have all the information about all the clauses if they are being checked separately. That's why at the moment the completeness checker is just treating all scattered definitions as 'open' in the sense that it's just assuming that other separately checked thing could be adding clauses that we don't know about.

Without a global check, handling this warning more sensibly would I think require checking that each module/compilation unit extends the function and enumeration clause in a 1-to-1 way (For example a module adding three new enumeration members, also adds the three corresponding function clauses). I think that's possible in theory but I haven't worked through the details in my head.

[jordancarlin]

Without a global check, handling this warning more sensibly would I think require checking that each module/compilation unit extends the function and enumeration clause in a 1-to-1 way (For example a module adding three new enumeration members, also adds the three corresponding function clauses). I think that's possible in theory but I haven't worked through the details in my head.

Unfortunately I think that even that wouldn't work in this case because all of the extensions are listed in extensions.sail. If we exclude a particular module then the extensionEnabled clause will not be defined but the extension will still be in the enum.

[Alasdair]

Yes, that's a good point I hadn't considered.