[K-Bug] `k start` in llvm gdb gives "Cannot access memory at address"

What component is the issue in?

llvm-backend

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

K version: v6.0.152

Operating System

Linux

K Definitions (If Possible)

This problem seems to occurs even for small examples, for example with lesson-02-a.k (link)

Steps to Reproduce

Install K with Debian package kframework_6.0.152_amd64_debian_bookworm.deb. My Debian version is
Debian GNU/Linux 12 (bookworm) on amd64.

echo 'colorOf(Banana())' > banana.color

kompile lesson-02-a.k --enable-llvm-debug

krun banana.color --definition lesson-02-a-kompiled --debugger

Then k start returns

[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Temporary breakpoint 1, 0x00005555555b8b00 in main ()
0x00005555555a56d0 in k_step (subject=Traceback (most recent call last):
  File "<string>", line 392, in to_string
  File "<string>", line 566, in append
gdb.MemoryError: Cannot access memory at address 0x7ffffffff000

<error reading variable: Cannot access memory at address 0x7ffffffff000>)

Note that with non functional rules, k step keeps giving the error and doesn't show output.

Expected Results

With the package version 6.0.151 (kframework_6.0.151_amd64_debian_bookworm.deb), it works as expected.

Temporary breakpoint 1, 0x00005555555b4ac0 in main ()
0x00005555555a16f0 in k_step (subject=<k>
  Yellow ( ) ~> .
</k>)

Diff between the two versions seems to point to submodule llvm-backend/src/main/native/llvm-backend between commits
ff19ef0b and 42e11681.

Note that the bug also appear to me with the latest version v6.1.39 installed with nix

Start by reproducing the failure with kompile ... --enable-llvm-debug, krun ... --debugger, and k start, then inspect the llvm-backend/src/main/native/llvm-backend submodule changes between commits ff19ef0b and 42e11681. Compare how k_step is displayed in versions 6.0.151 and 6.0.152. Done means the debugger no longer reports an inaccessible address and k step shows output for non-functional rules.