The test case bitwise-not.m triggers the following warning with GCC 9:

  C compilation failed:
  <stdin>: In function ‘rule0’:
  <stdin>:3836:126: error: promoted ~unsigned is always non-zero [-Werror=sign-compare]
  <stdin>:3836:244: error: comparison of promoted ~unsigned with constant [-Werror=sign-compare]

Github: related to #190 "assertion failure with apartment.m variant"

Github: related to #190 "assertion failure with apartment.m variant"

Previously, we would assert-fail here because this was considered a violation of
our assumptions. However, post commit d936b4e4
(or more generally, any of the ambiguous operator work), type() can be invoked
*during* type resolution, causing it to be executed on a potentially badly typed
model. We now need to throw exceptions instead of assert-failing in such
situations.

Github: fixes #190 "assertion failure with apartment.m variant"

Github: related to #190 "assertion failure with apartment.m variant"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

This is the equivalent of 10637bd7 for OR.

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

This is helpful when debugging internal failures during particular parsing
stages.

This new AST node is designed to represent a 'x & y' expression before we have
decided whether it is a logical AND or a bitwise AND. The intention here is to
move towards a situation where we can overload this operator to mean either.
This should be achievable as we have a stronger type system than C, so we should
be able to come up with precise types for both operands.

Github: related to #37 "extended operator support"

Technically you can get away without re-indexing the model and still running
symbol resolution. However, the unique identifiers will be all screwed up after
this and certain analyses on the AST won't work (e.g. checking whether a
function is pure). The XML generator doesn't rely on any of this functionality
but it seems safer to re-index anyway in case we add functionality in future
that does depend on this.

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

This addresses a number of incorrect or confusing things:

  * A left shift or right shift greater than ULONG_MAX no longer produces 0 when
    constant folded at generation time. This scenario cannot really occur due to
    practical reasons, but we may as well make the code logically consistent (or
    future proof).
  * Fix of a missing initialisation of mpz_t values that would cause crashes
    when constant folding.
  * Right shift, during both constant folding and runtime, is now a
    straightforward arithmetic right shift. This is intuitive for everything
    except shifting a negative value. We assume that users doing this know what
    they're doing and have thought through the consequences.

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

Github: related to #37 "extended operator support"

I can only assume this was copied as-is from the murphi2xml printer. It makes no
sense to carry around this string that was being ignored.

The Travis timeout is 50min and the pre-fuzzing setup typically only takes
~2min. Additionally this is build is usually done while we're still waiting on
the macOS builds to complete, so it's not a limiting factor on CI completion. So
we may as well bump fuzzing time by an extra 10min.

Similar to ArithmeticBinaryExpr, we were providing an identical implementation
of type() for each one of its children. It's unclear what the motivation for
this was as these do -- and always have -- return a boolean uniformly.

This doesn't really test any Rumur behaviour, but was rather written as an
experiment in expressivity. I don't think it will ever make sense to enable this
in the regular test suite, so it may as well live in misc/ as an example
instead.

I think these individual implementations of ::type() must have been a hangover
from when we tried to get precise about Range types yielded from such
expressions. Now that we treat the result of any arithmetic operation as the
unbounded range type, these implementations are all identical and there was no
point to duplicating them.

Github: related to #37 "extended operator support"

With a large number of threads, progress output becomes increasing spammy and
contention on the print lock can begin to degrade runtime. Since progress output
itself is non-critical, simply suppress it when the print lock is held by
another thread.

It's no longer relevant to experiment with replacing this with a spinlock. Some
cursory experiments indicated this did not affect performance on mid-size
machines. On large machines a spinlock is likely to perform worse than a pthread
mutex, that we expect has already been optimised for large machine scenarios.

Github: closes #160 "replace print mutex with a spinlock?"

Github: closes #187 "murphi2murphi: state pop design"

This stage can now keep its idea of pending_semi more in sync with the output
position, orthogonal to what other stages are doing.

Github: related to #187 "murphi2murphi: state pop design"

Currently no stages generate messages, but this is about to change.

This is not yet taken advantage of, but the goal here is to allow a more modular
implementation of Stages wherein they can have their own local concerns and not
have to think too much about what other stages are doing.

Github: related to #187 "murphi2murphi: state pop design"