VM assertion failure when building the standard library

[Vtec234]

Description

I am reliably unable to build the Lean standard library with a Release build of the master branch and get this error:

terminate called after throwing an instance of 'lean::exception'
  what():  vm check failed: is_composite(o) (possibly due to incorrect axioms, or sorry)

It also seems to happen on MinGW, and it has been mentioned on Zulip.

Using Lean in single-threaded (-j1) mode doesn't help, which makes me think this is not a race condition. Combined with the fact that both of

• building Lean in Debug mode
• using the Nightly binary from elan

do work, I'm thinking this is undefined behaviour that happens to work sometimes if the compiler does the right undefined thing.

Steps to Reproduce

1. Build Lean with -DCMAKE_BUILD_TYPE=RELEASE
2. Try to ../bin/lean --make in the library/ folder

Versions

Lean (version 3.5.0, commit 014fd37, RELEASE)
Arch Linux, GCC 9.1.0

[cipher1024]

What platform are you on?

[Vtec234]

I've minimized this to the following bit of C++ which is either UB (?) or miscompiled by GCC 9.1.0 (self-contained, compile with g++ -O2):

#include <cstddef>
#include <cstdint>

enum class foo_kind { A, B, C };

struct alignas(4) foo {
    foo_kind m_kind;
};

foo_kind kind_(foo * o) {
    if ((reinterpret_cast<std::uintptr_t>(o) & 1) == 0)
        return o->m_kind;
    else
        return foo_kind::A;
}

bool is_bc(foo * o) { return kind_(o) == foo_kind::B || kind_(o) == foo_kind::C; }

void loop(foo * o);

__attribute__((always_inline)) inline void loop_if_bc(foo * o) {
    if (__builtin_expect(!is_bc(o), 0))
        throw "what"; // Should never be thrown if loop_if_bc is called only with B/C kind foos.
                      // But with GCC, it's *always* thrown.
    loop(o);
}

void loop(foo * o) {
    switch (o->m_kind) {
    case foo_kind::A: return;
    case foo_kind::B: loop_if_bc(o); break;
    case foo_kind::C: loop_if_bc(o); break;
    }
}

int main(int, char**, char**) {
    foo obj { foo_kind::C };
    loop(&obj);
    return 0;
}

The real code from which this is derived is in vm_obj_cell::dealloc.

[digama0]

You can test the above snippet under various compilers using godbolt. (To be clear, the expected behavior is nontermination, and if you see a "terminate called" then the bug is being exercised.) This is almost certainly a bug in GCC, considering that it is affected by things like the inline attribute and whether the __builtin_expect annotation is present. It looks like it manifests on GCC 9.1 and 9.2 but not on trunk, so it must have been recently fixed.

A workaround is to replace is_bc with:

bool is_bc(foo * o) {
    foo_kind k = kind_(o);
    return k == foo_kind::B || k == foo_kind::C;
}

(Presumably we want it to optimize to this anyway, so it shouldn't cause any problems to do this.)

[gebner]

[...] is either UB [...]

I'm pretty sure it is. Both infinite loops and infinite recursion are UB unless they perform some kind of IO: http://eel.is/c++draft/basic.exec#intro.progress-1

[digama0]

OMG, I had no idea the C++ standards people were that crazy. I guess that's one way to solve the halting problem...

It's actually pretty tricky to modify the example to avoid the infinite recursion, because the recursive calls seem to be part of the bug. But of course the original source is traversing a tree and that kind of recursion is perfectly well terminating.

[Vtec234]

@gebner indeed the infinite recursion was only introduced by me when minimizing the example. It's not present in the original code, and in fact the bug can be reproduced without it:

#include <cstddef>
#include <cstdint>

enum class foo_kind { A, B, C };

struct alignas(4) foo {
    foo_kind m_kind;
};

foo_kind kind_(foo * o) {
    if ((reinterpret_cast<std::uintptr_t>(o) & 1) == 0)
        return o->m_kind;
    else
        return foo_kind::A;
}

bool is_bc(foo * o) { return kind_(o) == foo_kind::B || kind_(o) == foo_kind::C; }

__attribute__((always_inline)) inline void loop_if_bc(foo * o, int depth) {
    if (__builtin_expect(!is_bc(o), 0))
        throw "what";
    if (depth > 0) return;
    loop_if_bc(o, depth+1);
}

void destruct_foo(foo * o) {
    switch (o->m_kind) {
    case foo_kind::A: return;
    case foo_kind::B: loop_if_bc(o, 0); break;
    case foo_kind::C: loop_if_bc(o, 0); break;
    }
}

int main(int, char**, char**) {
    foo obj { foo_kind::C };
    destruct_foo(&obj);
    return 0;
}

yields

terminate called after throwing an instance of 'char const*'

@digama0 Since Lean uses __builtin_expect in a lot of places, I was thinking of fixing this by redefining LEAN_UNLIKELY/LIKELY to be a no-op on GCC 9.1/9.2 . A local fix to is_composite (~is_bc) would also work, but I'm worried that other places which use LIKELY could also miscompile.

[Vtec234]

Filed in GCC Bugzilla as https://gcc.gnu.org/bugzilla/show_bug.cgi?id=91597 .