[K-Bug] The debugger reports "No source file named definition.kore."

[pxhdev]

What component is the issue in?

llvm-backend

Which command

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

What K Version?

version: v7.1.70 │ │Build date: Fri Jul 19 19:05:55 America 2024

Operating System

Linux

K Definitions (If Possible)

module LESSON-19-A
  imports INT

  rule I => I +Int 1
    requires I <Int 100
endmodule

Steps to Reproduce

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 lesson-19-a.k --enable-llvm-debug
$ krun -cPGM=0 --debugger

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

GNU gdb (Ubuntu 12.1-0ubuntu1~22.04.2) 12.1
Copyright (C) 2022 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./lesson-19-a-kompiled/interpreter...
(gdb) k start
Temporary breakpoint 1 at 0x6ec90
Starting program: /workspace/lesson-19-a-kompiled/interpreter /tmp/.krun-2024-07-22-08-15-56-UZF8wlgGZz/tmp.in.IAw26WbGz
A -1 /tmp/.krun-2024-07-22-08-15-56-UZF8wlgGZz/result.kore
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

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

Expected Results

I expect that I could debug the semantics as described in the tutorial.

[pxhdev]

Respond elsewhere