amaranth: Unused cases in a switch do not trigger warnings

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).

About this issue

Original URL
State: closed
Created 4 years ago
Comments: 17 (17 by maintainers)

Commits related to this issue

dsl: issue a warning if defining a case after the default Resolves #404 Signed-off-by: Filipe Laíns <lains@archlinux.org> — committed to FFY00/nmigen by FFY00 4 years ago

Most upvoted comments

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:

Exhaustiveness checking, undoubtedly useful (and already tracked at #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 (#360, #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.
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.
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 on Feb 6, 2023