The long term plan here is to use the CI setup to build an AFL-instrumented
Rumur, in which case we'll be running with CC=afl-gcc, so we want a way of
avoiding picking this compiler up in the harness.

Since this script is only ever intended to run in CI, we may as well just let it
fail messily so we can more easily diagnose problems from the exception trace.

Github: closes #122 "AFL fuzzing in CI"

Github: related to #122 "AFL fuzzing in CI"

Github: related to #122 "AFL fuzzing in CI"

Github: related to #122 "AFL fuzzing in CI"

When your input model contains a syntax error and the line in which the error
occurs contains a tab, Rumur would print an error message indicating the wrong
column location in the line. We now account for tabs and offset the caret
indicator correctly.

Note that error messages for lines containing multibyte characters (e.g. "≔")
are still misaligned, but it does not seem worth it to work around this as it is
fixed upstream in Bison 3.4.

Github: closes #129 "syntax error output is misaligned with tabs"

Seems reasonable to expect people will read this document more than writing it,
in which cases smart quotes are more pleasant.

This is what Java's HashMap uses, which presumably has been battle-tested and
profiled in the real world, so it seems sensible to try such a thing for our use
case.

This also extends testing for some compilers to both Ubuntu 14.04 and Ubuntu
16.04.

A couple of weeks ago, Travis CI upgraded their default Linux environment from
Ubuntu Trusty 14.04 to Ubuntu Xenial 16.04 [0]. Clang 5 and 6 builds started
failing because the llvm-toolchain repositories we're using don't support
Xenial. I suspect other Clang builds that are passing (e.g. Clang 4) are only
doing so coincidentally. I didn't investigate the failures initially, assuming
they were yet another transient Travis failure, and when I did it was
surprisingly hard to find the answer [1].

The fix in this commit is to pin these builds to Trusty. In future we should
also (1) pin the other Linux builds and (2) extend testing to Xenial.

  [0]: https://changelog.travis-ci.com/xenial-as-the-default-build-environment-99476
  [1]: https://travis-ci.community/t/cannot-apt-get-install-clang-5-0/3250/3

Now instead of ending with a messy Python trace and leaving the temporary
directory behind, we clean up nicely. We don't bother catching all signals or
attempt to do this fully robustly. This is just for the common scenario of a
long running checker that the user interrupts.

We were using the sigsetjmp()/siglongjmp() exception mechanism when either of
two things were true:

  1. --max-errors > 1; or
  2. the model has assumptions.

As of 7dda1203, a failed assumption is signalled
via a normal return value, not via a siglongjmp(). As a result, we no longer
need to require a jmp_buf in this case. This should result in a slight speed up
for models that have assumptions but run with --max-errors < 2.

Github: related to #127 "--max-errors > 1 produces unsafe code"

The motivation for this change is to fix an error in our usage of sigsetjmp().
When using jmp_bufs (JMP_BUF_NEEDED), we use sigsetjmp() and siglongjmp() to
give us an exception-handling-like mechanism to jump back to the exploration
loop after signalling an error. This pattern is fine except that these calls are
documented to leave all non-volatile locals in an indeterminate state. We had
several of these that were important (e.g. the pointer to the state that we go
on to free).

My initial planned solution to this was to simply mark the relevant variables
volatile. However, this comes with some drawbacks. Unconditionally marking these
volatile impedes the compiler's optimiser in the case when we're not using
jmp_bufs, while conditionally marking them volatile overcomplicates the code
generation logic. To further complicate this, some of the relevant variables are
generated (ruleset iterators). We would have to cast away these variables'
volatility when passing them to rules which would introduce even further
complications.

Instead, we duplicate the sigsetjmp() calls and move them inwards. E.g. for
guards, we call sigsetjmp() as the first step in the guard itself and then use
the return value of the guard to indicate to the exploration loop whether
siglongjmp() was called. The advantage of this is that the only work done in the
siglongjmp() path is now returning from the containing function; there are no
longer any relevant non-volatile locals.

This had a couple of unanticipated side effects:

  1. The error call in case of a deadlock had to be moved into its own function
     to also avoid having any non-volatile locals. This is not a problem, just
     unexpected.
  2. Return statements now awkwardly return a boolean when they have no
     associated expression. Relatedly void-returning functions (procedures) now
     have a boolean return type. This is because a return statement can be used
     in a rule (which now returns a boolean). We could have done something more
     elaborate like have an empty return statement jump to the end of the
     rule/function, but it seemed this would be more likely to confuse the
     compiler.

Github: closes #127 "--max-errors > 1 produces unsafe code"

Github: related to #128 "negative literals are not taken into account when
determining value type"

Github: closes #128 "negative literals are not taken into account when
determining value type"

Github: related to #128 "negative literals are not taken into account when
determining value type"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

This fixes a compile error resulting from bad code generation when
counterexample traces are disabled and there are no liveness properties.

Github: closes #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

The previous pointer is used during liveness checks, but we failed to notice
that it is only defined when counterexample traces are enabled. We now enable it
if either of these features are in use.

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

We're going to need to start using it at preprocessor time.

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"