Test suite missing a segmentation fault

[ehildenb]

Going back quite a ways, there has been a segmentation fault in the K test suite unnoticed.

This test two months ago: https://office.runtimeverification.com/jenkins/blue/organizations/jenkins/K/detail/release/175/pipeline/68

• Click "Build and Test K"
• Click "Show complete log"
• Search for "Segmentation"

Our testing infrastructure is missing this segfault somehow.

Pretty sure it's issues-1602, that one is segfaulting on my machine, discovered when the test started failing on: #2410

[Baltoli]

Initial investigation:

• The underlying segmentation fault is an infinite recursion in the LLVM backend's Kore parser. I'll minimise the test case and raise an issue there.
• The failure not being reported seems to be a subshell somewhere not picking up a return code.

[Baltoli]

The reporting failure is down to pipefail not being set at the top level of the test suite Makefiles. This means that when we construct command pipelines like:

cat foo.test.in 2>/dev/null \
  | $k-dist/bin/krun foo.test --dry-run 1>/dev/null -v --no-exc-wrap  -d . \
  | diff - foo.test.out

we don't consider that the krun invocation itself could fail with a non-zero exit code; the pipeline is allowed to continue executing.

This normally wouldn't be a problem, because the krun invocation wouldn't produce the expected output, and the diff command would catch this as a failing test. However, in this test, the expected output is empty, and the diff invocation succeeds despite the segfault.

I think the best thing to do here is:

• Set pipefail globally on the test suite by overriding the SHELL Makefile variable. This seems to be the consensus solution, but it may break things unexpectedly.
• Disable this test and re-run the test suite with pipefail to make sure we're not missing anything else important.
• Fix the underlying problem in the backend's macro expander.
• Re-enable the test.

[Baltoli]

There's a workaround for the segfault itself - because it's not an infinite recursion, and is just a really huge term, you can use ulimit -s to allocate more stack space. On my machine this fixes the test.

[Baltoli]

We actually rely on the non-pipefail behaviour in the test suite, by unconditionally cat-ing files that might not exist. It might be a bit of a pain to change all of these locations (looking at the failing test run for this PR), so we might want a more selective approach.

[Baltoli]

A summary of where I am on this:

• It's possible to get pipefail enabled on the test suite, but it breaks our assumptions in a number of places. Still trying to find the method that breaks the least things.
  • My assumption is that we do want to enable pipefail if not doing so could hide failures like this.
  • Given this, it should be on by default and specific test cases can opt out if they rely on a failing command's output.
• There's a workaround for the actual issue that can be applied easily.

[ehildenb]

I think we can change the non-pipefail behavior in the test-suite, by having something like:

INPUT_STDIN =

The having an override rule which does:

INPUT_STDIN = cat WHATEVER_FILE |

Then our recipes which require input stdin can do:

krun:
    $(INPUT_STDIN) $(KRUN) .... | $(CHECK) ...

for example.

[ehildenb]

How many test cases do we rely on input stdin vs not?

[ehildenb]

Either way I think we should enable pipefail on tests. It's too easy to miss failure otherwise. Is it just that one test that fails if we do this and adjust the cat ... to be allowed to be empty?

[Baltoli]

No, there are a few places in the test suite that break in different ways depending on where and how you enable pipefail checking. I'll write up a detailed summary of them tomorrow as it's not quite as simple as this one test unfortunately!

[Baltoli]

Enabling pipefail

I've tried two different ways of enabling pipefail across the test suite:

• Globally, by setting the SHELL make variable at the top of each of the included Makefiles. This has the advantage of applying everywhere with minimal repetition, but requires a specific shell (e.g. /bin/bash) to be specified.
  • In fact, enabling pipefail at all requires that we mandate bash.
• At the start of individual Makefile recipes that construct pipelines. This is more granular, and allows the option to be switched off for families of tests (see below).

Problem Tests

• Tests that don't use any standard input (and therefore rely on failing cat invocations) are actually in the majority; only 3 of the regression tests use stdin. It might make sense to adopt Everett's suggestion above for these cases.
  • The alternative is to just wrap cat in a (cat || true) subshell where it appears in recipes.
• Tests that construct specs seem to rely on the prover getting stuck at a certain configuration; this produces a non-zero exit code, and so can't be used with pipefail. Solutions to this would be:
  • Expect a specific exit code from the stuck prover.
  • Disable pipefail and rely on diff for these cases.
  • Change the behaviour of the prover, but I suspect this isn't practical / ergonomic.
• The pl-tutorial tests don't use the Makefile includes, so would need to be fixed up separately.
  • This can probably wait until after the regression tests are done.