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

[perelo]

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

[Baltoli]

The K support for GDB can be fragile, unfortunately; we're in the process of trying to fix it at the moment and have a number of open issues:

• [Debugger] llvm-kompile-testing doesn't generate debug symbols correctly #858
• [GDB] Create script and tests for GDB to run in CI #840
• [GDB] Can't print builtin types on LHS of rules in K Match #746
• [GDB] MatchLog enum kind raises TypeError when printed #726

Sorry it's not working for you in this case; in terms of following through the K tutorial I'd say skip over the debugger content for the time being.