Unused cases in a switch do not trigger warnings

[jeanthom]

Consider those two elaboratables:

class Impl1(Elaboratable):
    def __init__(self):
        self.sel = Signal()
        self.A = Signal()
        self.B = Signal()

    def elaborate(self, platform):
        m = Module()

        with m.Switch(self.sel):
            with m.Case():
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(1),
                ]
            with m.Case(0):
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(0),
                ]
            with m.Case(1):
                m.d.comb += [
                    self.A.eq(0),
                    self.B.eq(0)
                ]

        return m

class Impl2(Elaboratable):
    def __init__(self):
        self.sel = Signal()
        self.A = Signal()
        self.B = Signal()

    def elaborate(self, platform):
        m = Module()

        with m.Switch(self.sel):
            with m.Case(0):
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(0),
                ]
            with m.Case(1):
                m.d.comb += [
                    self.A.eq(0),
                    self.B.eq(0)
                ]
            with m.Case():
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(1),
                ]

        return m

Because the default/wildcard case was declared first in Impl1, it prevents Case(0) and Case(1) from being matched. This is a bit misleading for newbies who would expect cases to be position agnostic (and therefore Impl1 having equivalent behaviour as Impl2).

As discussed on IRC, a sensible way of dealing with that issue would be to trigger warnings whenever some cases are unreachable. We still have to figure out how we can silence those warnings when they are undesired (think code generation).

[FFY00]

I've submitted a PR. To enabling filtering out the warning I propose declaring a new warning type, which could then be ignored.

[whitequark]

I've submitted a PR.

Sorry but any attempt to fix this issue (or any other issue that touches language features) is premature until we actually agree on the design. I prefer to have no fix at all to a careless fix that negatively impacts downstream.

To enabling filtering out the warning I propose declaring a new warning type, which could then be ignored.

I don't like the solution of explicitly disabling lints by name. Sometimes it's unavoidable, sure, like in case of UnusedElaboratable, but for syntactic lints my preference is to allow silencing the lint through the use of an idiomatic but more verbose pattern. Take a look at _check_signed_cond to see what I mean here.

[jeanthom]

We had a discussion about this issue on IRC: https://freenode.irclog.whitequark.org/nmigen/2020-06-16#1592311000-1592313032;

Long story short, the issue goes much further than just checking the position of the default case. We should actually check for unreachable cases in a switch (which covers the default case being in first position, but also other scenarios), but we shouldn't forget that in some applications (eg. generated code) those checks are unneeded and for those situations we should let the user disable those warnings.

[FFY00]

Sorry but any attempt to fix this issue (or any other issue that touches language features) is premature until we actually agree on the design. I prefer to have no fix at all to a careless fix that negatively impacts downstream.

The purpose was mainly to get something started.

I don't like the solution of explicitly disabling lints by name. Sometimes it's unavoidable, sure, like in case of UnusedElaboratable, but for syntactic lints my preference is to allow silencing the lint through the use of an idiomatic but more verbose pattern. Take a look at _check_signed_cond to see what I mean here.

I am not sure if I parse this correctly. Warnings are very easy to suppress, actually more than anything you could ever do programmatically. But you can build something directly, or on top of the warnings module, it does not make much difference here. The benefits of using the warnings module is that we would not have to care about the warning suppression in the code that is issuing them. Anyway, there is no need for me to try being a perfectionist and force you to spend some of your time arguing about the technicalities of the implementation, so I will not pick this battle.

Can you describe the mechanism you had in mind? Or do you prefer to implement it yourself?

[whitequark]

The purpose was mainly to get something started.

The life of a language feature does not start with code.

Can you describe the mechanism you had in mind?

The specific mechanism for disabling the warnings for unreachable cases, or the general approach? The general approach can be seen in _check_signed_cond. The specific mechanism for unreachable cases is something I don't know yet, and which we can work out in this issue.

Or do you prefer to implement it yourself?

There can be no implementation until there is a design! Which is what this issue is about.

[FFY00]

The specific mechanism for disabling the warnings for unreachable cases, or the general approach?

The mechanism to disable the warnings.

The specific mechanism for unreachable cases is something I don't know yet, and which we can work out in this issue.

I was thinking we could just do it when exiting the context manager. This is what makes the most sense to me.

[whitequark]

Ah sorry, I was unclear earlier. I meant that I don't know yet what kind of user-visible mechanism there should be to disable the warnings for unreachable cases, and that we should discuss that. It doesn't really matter at this point how the logic of emitting the warnings should be implemented—in general until the design is done I don't care at all about the implementation in cases where it's clear that some reasonable implementation is possible.

[FFY00]

Okay, what do you want to do?

I proposed declaring a new warning type which could then be filtered. We can declare a warning type for these cases and then subclass the specific warnings from there. Warnings are easily filterable, but we can even provide a helper function to do just that if you want. This is what I was proposing above, I am not sure if it was clear enough. You didn't seem to be a fan of my approach.

[FFY00]

Just a note. I am not knowledgable enough in the code structure to propose a direct way to do this in the code, so you'll have to be the one providing an option.

[whitequark]

I'm not expecting you to propose any way to do this in the code! Implementation is secondary to the interface; until we decided on the interface it doesn't even make sense to talk about the implementation for the most part.

Anyway, let's see which options we have for the interface used to suppres the warning:

1. Using Python's warnings module. This has the advantage that it's semi-standard. The drawbacks are that it increases rightward drift of code (due to the with warnings.catch_warnings statement) and that Python's catch_warnings function is broken in multithreaded applications, as the documentation admits. Because of the last point I think it should never be used outside of tests.
2. Using an explicit keyword argument for with m.Case():. Since it's just our own code it doesn't suffer from problems of (1). This has the drawback that it's not composable: the m.Case interface gains a new argument whose meaning doesn't directly affect the semantics of the code. If we end up with a lot more lints, we'll have a lot more of such arguments, and that sounds like it would make the language harder to learn. But maybe that's okay.
3. Adding a context manager that configures nMigen's existing linter, and extend this linter (which currently just exists to suppress the UnusedElaboratable warning) to make it possible to suppress other warnings too. In effect this would create something similar to Rust's #[allow]/#[deny]/#[warn] mechanism.

Both (2) and (3) seem generally alright, with a weak preference for (3). If we go with (2) this issue is easy to fix; (3) will need further design work to figure out how linter options should be configured.

[whitequark]

Of course there can be other possible strategies that I'm missing, so anyone reading these comments is welcome to suggest alternatives.

[FFY00]

I have a preference towards 3). Can you point me to the linter code?

[whitequark]

Sure, search for _linter in nmigen._utils and nmigen._unused. The current implementation is extremely bare-bones (it basically exists to make it bearable to write tests that create and then don't simulate elaboratables), so first we'd need to design an interface that would accommodate this issue (at the very least it should be possible to disable lints per lexical scope, and we should probably do something about the rightward drift too).

[whitequark]

I've filed an RFC #436 to discuss this.

[whitequark]

Looking over this again, there is basically no reason to ever have cases after with m.Case(); if you programmatically generate cases it's trivial to break from the loop, and if you don't then this could potentially find bugs in the code generator.

Sorry @FFY00, I think I wasn't feeling very well when first looking at the issue and didn't approach it in the most constructive way. I'll add this functionality taking your PR as a base.

[whitequark]

Discussed on the 2023-02-06 weekly meeting, with no conclusion reached beyond no one objecting to catching common cases of this issue without a full exhaustiveness check.

In my view, there are three intersecting issues at play here:

1. Exhaustiveness checking, undoubtedly useful (and already tracked at Switch attribute for unique and/or full Cases #451) but difficult to implement in the general case. Even a limited implementation of exhaustiveness checking requires a linter override, which we currently don't have an interface for (Amaranth Linter #360, [RFC] Extending the linter interface to allow per-scope settings #436); if you end up with lints that are false positives and that you can't turn off, people learn to ignore them, which is very bad.
2. It's easy to make a typo and end up with with m.Case(): unintentionally, which looks like with m.Case(0) and is easy to overlook. This is why we have with m.Default():. However it's tricky to warn on a literal m.Case() since it's only distinct at the call site from something like m.Case(*[]), and the latter should be allowed in metaprogrammed code.
3. Novice Amaranth designers not recognizing that with m.Switch(): is a priority-case statement. An exhaustiveness check (1) would quickly clarify that when used on code like the one in this issue, but it seems like a tall order to require a full exhaustiveness check to catch something that isn't even about exhaustiveness.

Even if we implement (1) we still should do something about (2) since an exhaustiveness check will say nothing about an m.Case(): at the end of a switch.

The key difficulty here is the lack of a linter interface, which I don't think will get better any time soon. So I'm focusing on solutions that avoid it. One such solution is always emitting a warning for a literal m.Case(), and then emitting a warning if there are any cases past m.Default() specifically (but not m.Case(*[]), as would be in metaprogrammed code). These checks will have no false positives and therefore we don't need to turn them off.

[whitequark]

Now that m.Default(): and m.Case(): mean two separate (opposite, in fact) things, we can solve this by warning on any case that comes after m.Default():, without any of the complex proposed mechanisms.