GDB support broken in minimal docker container

[Baltoli]

Reported on Discord

Hi, I'm also having some trouble with the debugger. I am trying to get the debugger working in a clean Docker environment with only gdb installed.

FROM runtimeverificationinc/kframework-k:ubuntu-jammy-7.1.70

RUN apt-get update && \
    apt-get install -y gdb && \
    apt-get clean && \
    rm -rf /var/lib/apt/lists/*
RUN echo "set auto-load safe-path /" >> /root/.gdbinit

RUN mkdir -p /workspace
WORKDIR /workspace

I compile and run the program as follows:

$ kompile --backend llvm --enable-llvm-debug test.k
$ krun testfile --debugger

However, I couldn't start or step through the program in gdb:

(gdb) k start
Temporary breakpoint 1 at 0x7be20
Starting program: /workspace/test-kompiled/interpreter /tmp/.krun-2024-07-21-18-01-21-7HhvVMBifn/tmp.in.9ow8yaJKOg -1 /tmp/.krun-2024-07-21-18-01-21-7HhvVMBifn/result.kore
warning: Error disabling address space randomization: Operation not permitted
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Temporary breakpoint 1, 0x00005632fa85ae20 in main ()
Python Exception <class 'gdb.error'>: No source file named definition.kore.
Error occurred in Python: No source file named definition.kore.

[pxhdev]

Actually, it is not broken only in the minimal Docker container. I tried it on my local host first (Ubuntu 22.04) and encountered the same error. I thought it might be incompatible dependencies, so I tried this minimal container, but it didn't work either. I hope this extra information is helpful.

[Baltoli]

Thanks for the additional info; we'll take a look at this for you!

[Robertorosmaninho]

This is an error related to the -g flag. We're not passing it appropriately to clang. I saw this same error here: #858
If you execute kompile --verbose ..., copy and paste the llvm-kompile command and append -g after the --, you'll be able to open the debugger as expected.

[pxhdev]

This is an error related to the -g flag. We're not passing it appropriately to clang. I saw this same error here: #858 If you execute kompile --verbose ..., copy and paste the llvm-kompile command and append -g after the --, you'll be able to open the debugger as expected.

It worked! Really appreciate the help!