[Debugger] llvm-kompile-testing doesn't generate debug symbols correctly

[Robertorosmaninho]

The llvm-kompile-testing doesn't generate the debug symbols for a k file as expected.

• OS:

lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 22.04.3 LTS
Release:        22.04
Codename:       jammy

• K Version:

K version:    v6.0.144-0-g0cfe674f6f
Build date:   Sun Oct 15 15:11:21 -03 2023

• LLVM Backend Last Commit:

git log | head -n 1
commit a859fb6d77a48220d9d8b9314371933e8204c1d3

Expected Behavior:

llvm-kompile-testing definition.kore main -g -o interpreter
gdb --args ./interpreter input -1 output

GNU gdb (Ubuntu 12.1-0ubuntu1~22.04) 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 ./simple-kompiled/interpreter...
(gdb) k start
Temporary breakpoint 1 at 0x640a0
Starting program: /home/robertorosmaninho/rv/tests/issue_840/simple-kompiled/interpreter input -1 output
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Temporary breakpoint 1, 0x00005555555b80a0 in main ()
0x000055555559ccd0 in k_step (subject=<k>
  0 ~> .
</k>) at /home/robertorosmaninho/rv/tests/issue_840/simple.k:4
4         rule I => I +Int 1
(gdb) q
A debugging session is active.

        Inferior 1 [process 76700] will be killed.

Quit anyway? (y or n) y

This behavior was achieved using an interpreter generated by kompile.

Actual Behavior

lvm-kompile-testing definition.kore main -g -o interpreter
gdb --args ./interpreter input -1 output 

GNU gdb (Ubuntu 12.1-0ubuntu1~22.04) 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 ./interpreter...
(gdb) k start
Temporary breakpoint 1 at 0x6a690
Starting program: /home/robertorosmaninho/rv/tests/issue_840/interpreter input -1 output
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Temporary breakpoint 1, 0x00005555555be690 in main ()
Python Exception <class 'gdb.error'>: No source file named definition.kore.
Error occurred in Python: No source file named definition.kore.
(gdb) q
A debugging session is active.

        Inferior 1 [process 77008] will be killed.

Quit anyway? (y or n) y

Steps to reproduce:

• K File: simple.k

module SIMPLE
  imports INT

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

• input as:

LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("0")))))

• output as:

Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("100")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("100")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))

• Kompile: (To generate the definition.kore)

kompile simple.k --syntax-module SIMPLE --backend llvm --enable-llvm-debug

• Generate interpreter from llvm-kompile-testing:

llvm-kompile-testing definition.kore main -g -o interpreter

• Test GDB with llvm-kompile-testing's interpreters:

gdb --args ./interpreter input -1 output
k start

• Check expected behavior is kompiler's interpreter:

gdb --args ./simple-kompiled/interpreter input -1 output
k start

[Robertorosmaninho]

from @gtrepta, have we tried Debug on Cmake?

[Robertorosmaninho]

Let's look at the python script, maybe it has something to do with the path that's looking for. (from @dwightguth)
Try path the absolute path of definition.kore (from @gtrepta )

[Baltoli]

@Robertorosmaninho will post his additional reproduction info then un-assign himself and we can pick this back up later. This issue is the main thing blocking further changes to the debugging infrastructure.

[Robertorosmaninho]

I'm having issues reproducing this with the latest versions of llvm-backend:

LLVM Backend

git log | head -n 1
commit 29bb01e45da52e13549f4f9a38dac91aacb6d0bd

K

kompile --version
K version:    v6.1.12-0-gda72fc4726-dirty
Build date:   Tue Nov 14 11:31:32 -03 2023

Reproduction

kompile simple.k --syntax-module SIMPLE --backend llvm --enable-llvm-debug
llvm-kompile-testing /home/robertorosmaninho/rv/tests/issue_840/simple-kompiled/definition.kore main -g -o interpreter

Error:

llvm-kompile-testing /home/robertorosmaninho/rv/tests/issue_840/simple-kompiled/definition.kore main -g -o interpreter
[ERROR] Failed to execute goal org.codehaus.mojo:exec-maven-plugin:1.6.0:java (default-cli) on project llvm-backend-matching: An exception occured while executing the Java class. ERROR: Line 307: Column 26: Expected <Identifier>, but '\'
[ERROR]   axiom{} \right-assoc{}(\or{SortKItem{}} (\exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCellOpt{}, inj{SortGeneratedCounterCellOpt{}, SortKItem{}} (Val:SortGeneratedCounterCellOpt{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \bottom{SortKItem{}}())) [constructor{}()] // no junk
[ERROR]                          ^
[ERROR] -> [Help 1]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoExecutionException

[Baltoli]

Looks like something is out of date here @Robertorosmaninho; did you rebuild the pattern matching project? You shouldn't be seeing right-assoc in a compiled definition any more.

[Robertorosmaninho]

Indeed, but I've recompiled both with mvn package -U. Kompile works fine, the problem seems to be on llvm-kompile-testing

[Baltoli]

I can't reproduce this locally. Make sure you're definitely regenerating simple-kompiled/definition.kore with an up-to-date K; the fact that the file has right-assoc symbols in it suggests there is something stale in your local toolchain somehow. If I build K locally, I don't get those symbols:

$ kompile --version
K version:    v6.1.12-0-gfb08dee7c1
Build date:   Tue Nov 14 15:34:46 GMT 2023
$ kompile simple.k --syntax-module SIMPLE --backend llvm --enable-llvm-debug
$ ag '(right|left)-assoc' simple-kompiled/definition.kore
$ 

The axiom in question in my file is:

axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCellOpt{}, inj{SortGeneratedCounterCellOpt{}, SortKItem{}} (Val:SortGeneratedCounterCellOpt{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk

kompile working fine is probably a red herring; it makes sense to me that if you have an old kompile toolchain hanging around to generate these files, that it will also accept the assoc symbols.

[Robertorosmaninho]

Thanks for looking at it! I deleted my k-distribution and llvm-backend directory from K, did the checkout again, and recompiled! The error reported on the beginning of the issue is still happening even when we pass the full path of definition.kore

[Robertorosmaninho]

Hey @Baltoli, from my investigation: this line is never being executed so we're not compiling it with the debug flag appropriated. After manually setting this flag, I could move on to a new set of errors:

llvm-kompile-testing /home/robertorosmaninho/rv/tests/issue_840/simple-kompiled/definition.kore main -g -o interpreter
gdb --args ./interpreter input -1 output
...
(gdb) k start
Temporary breakpoint 1 at 0x12dcd0
Starting program: /home/robertorosmaninho/rv/tests/issue_840/interpreter input -1 output
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

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

<error reading variable: Cannot access memory at address 0x5555af642089>) at /home/robertorosmaninho/rv/tests/issue_840/simple.k:4
4	  rule I => I +Int 1
(gdb)

[Baltoli]

First properly fix the parsing of -g from llvm-kompile-testing; then look at these memory errors.

[Robertorosmaninho]

The error I mentioned here can be soulve by passing -O1 to llvm-kompile-testing as a clang flag like:

llvm-kompile-testing simple-kompiled/definition.kore main -g -O1 -o interpreter