alive-exec crashes with an assertion failure on a valid LLVM IR program

[Roticv912]

alive-exec crashes with an internal assertion failure when executing the following LLVM IR program.

IR program:

target datalayout = "e-p:64:64:64-i32:32:32"

@value = global i32 41
@value_ptr = global ptr @value
@aggregate = global { i32, [2 x i8] } { i32 7, [2 x i8] c"hi" }

define void @main() {
  %initial = load i32, ptr @value
  store i32 42, ptr @value
  %ptr = load ptr, ptr @value_ptr
  %updated = load i32, ptr %ptr
  %aggregate_value = load { i32, [2 x i8] }, ptr @aggregate
  ret void
}

Command:

alive-exec global.ll

Result:

alive-exec: /alive2/ir/memory.cpp:2309: std::pair<smt::expr, smt::expr> IR::Memory::alloc(const smt::expr*, uint64_t, BlockKind, const smt::expr&, const smt::expr&, std::optional<unsigned int>, unsigned int*, bool): Assertion `(has_null_block && bid == 0) || is_globalvar(bid, !state->isSource())' failed.

The crash then produces a stack dump:

Stack dump:
0. Program arguments: /alive2/build/alive-exec /TestingIBDA/workdir/ll/task_28/global.ll

Stack dump without symbol names:
0  libLLVM.so.23.0 0x00007255d5d8863f llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) + 63
1  libLLVM.so.23.0 0x00007255d5d85f0b llvm::sys::RunSignalHandlers() + 43
2  libLLVM.so.23.0 0x00007255d5d8948a
3  libc.so.6       0x00007255cfac8330
4  libc.so.6       0x00007255cfb21b2c pthread_kill + 284
5  libc.so.6       0x00007255cfac827e gsignal + 30
6  libc.so.6       0x00007255cfaab8ff abort + 223
7  libc.so.6       0x00007255cfaab81b
8  libc.so.6       0x00007255cfabe517
9  alive-exec      0x0000643c6b07e6be
10 alive-exec      0x0000643c6b0dd38f
11 alive-exec      0x0000643c6b0dd4c6
12 alive-exec      0x0000643c6b0bc3ef
13 alive-exec      0x0000643c6b122548
14 alive-exec      0x0000643c6afe6373
15 alive-exec      0x0000643c6afe4157
16 libc.so.6       0x00007255cfaad1ca
17 libc.so.6       0x00007255cfaad28b __libc_start_main + 139
18 alive-exec      0x0000643c6afe5995

[IamYJLee]

I’d like to try fixing this issue.

[IamYJLee]

Minimal reproducer

target datalayout = "e-p:64:64:64-i32:32:32"

@aggregate = global { i32, [2 x i8] } { i32 7, [2 x i8] c"hi" }

define void @main() {
  %aggregate_value = load { i32, [2 x i8] }, ptr @aggregate
  ret void
}

[IamYJLee]

Following this comment:

https://github.com/AliveToolkit/alive2#running-the-standalone-llvm-execution-tool-alive-exec

This tool uses Alive2 as an interpreter for an LLVM function. It is currently highly experimental and has many restrictions. For example, the function cannot take inputs, cannot use memory, cannot depend on undefined behaviors, and cannot include loops that execute too many iterations.

alive-exec does not currently support memory. so inputs containing global variables may trigger a crash.
Would it be reasonable to improve this behavior so that alive-exec emits a clear diagnostic, such as “memory is not supported,” instead of hitting an assertion?