[GDB] Can't find side_condition_ function globally

[Robertorosmaninho]

Both GDB and LLDB, in Ubuntu 22.04 and MacOS 13.2, can't execute the match a rule with an integer.

Test file:

module TEST
  imports INT

  syntax Foo ::= foo(Int) | bar()
  rule [test]: foo(I) => bar() requires I ==Int 0
endmodule

kompile:

kompile test.k --enable-llvm-debug

run:

krun -cPGM='foo(1)' --debugger

On GDB:

(gdb) k  start
...
(gdb) k match TEST.test subject
TEST.test.sc(Traceback (most recent call last):
  File "<string>", line 764, in invoke
AttributeError: 'NoneType' object has no attribute 'value'

Python Exception <class 'AttributeError'>: 'NoneType' object has no attribute 'value'
Error occurred in Python: 'NoneType' object has no attribute 'value'

On LLDB:

(lldb) process launch --stop-at-entry
Process 85169 launched: '/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter' (arm64)
(lldb) k match TEST.test
usage: match rule term
match: error: the following arguments are required: term
(lldb) k match TEST.test subject
Traceback (most recent call last):
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 288, in __call__
    matcher(args.rule, args.term)
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 213, in __call__
    self._try_match(rule_name, subject)
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 197, in _try_match
    target_call(self.exe_ctx, f'{rule_name}.match',
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 89, in target_call
    args_cast_exp = ', '.join(
                    ^^^^^^^^^^
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 90, in <genexpr>
    f'({ty})({to_address(arg)})' for ty, arg in zip(arg_tys, args))
              ^^^^^^^^^^^^^^^
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 23, in to_address
    return value_or_raise(err, a)
           ^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/robertorosmaninho/Desktop/test/test-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py", line 16, in value_or_raise
    raise RuntimeError(err.description)
RuntimeError: unable to read data

[Robertorosmaninho]

A deeper investigation proved that the problem, at least in GDB, was actually in finding the side_condition_ llvm function generated on the interpreter. GDB can't recognize the debug info on the side condition function generated from the k file.

llvm function correspondent to the content of the requires clause from the above example compiled with debug info:

@str_lit_side_condition_124 = global [19 x i8] c"side_condition_124\00"

define i1 @side_condition_124(%mpz* %0) !dbg !407 {
entry:
  call void @llvm.dbg.value(metadata %mpz* %0, metadata !415, metadata !DIExpression()), !dbg !416
  %1 = call i1 @hook_INT_eq(%mpz* %0, %mpz* getelementptr inbounds (%mpz_hdr, %mpz_hdr* @int_0, i64 0, i32 1)), !dbg !416
  ret i1 %1, !dbg !416
}

On GDB:

(gdb) info address side_condition_124
Symbol "side_condition_124" is at 0x238ff0 in a file compiled without debugging.

Library side functions have the same debug info available:

!399 = distinct !DISubprogram(name: "side_condition_123", linkageName: "side_condition_123", scope: !388, file: !388, line: 2066, type: !389, scopeLine: 2066, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !400)

define i1 @side_condition_123(i1 %0) !dbg !399 {
entry:
  call void @llvm.dbg.value(metadata i1 %0, metadata !401, metadata !DIExpression()), !dbg !402
  %hook_BOOL_not = xor i1 %0, true
  ret i1 %hook_BOOL_not, !dbg !402
}

And, indeed, their symbol is recognized by GDB:

(gdb) info address side_condition_123
Symbol "side_condition_123" is a function at address 0x238fd0.

[Robertorosmaninho]

A partial fix would be to replace the entry['function'] with entry['debugName']. This will solve most of the issues using the requires clause on rules.

[Robertorosmaninho]

However, even this fix can't solve the following case:

• K Definition:

module TEST
  imports STRING

  syntax FooString ::= fooString(String)

  rule [testString]: fooString("Hello World!") => .K
endmodule

• kompile and krun

kompile test.k --enable-llvm-debug && krun -cPGM='fooString("Hi")' --debugger

• K Match on GDB

(gdb) k start
...
(gdb)  k match TEST.testString subject
KEQUAL.eq(Traceback (most recent call last):
  File "<string>", line 764, in invoke
AttributeError: 'NoneType' object has no attribute 'value'

Python Exception <class 'AttributeError'>: 'NoneType' object has no attribute 'value'
Error occurred in Python: 'NoneType' object has no attribute 'value'

This difference happens because when using requires, we generate two functions: a side_function_ and a MODULE.LABEL.sc. The first doesn't contain debug symbols, but the second does, so we use it to match.

In this case, we generate two functions again: KEQUAL.eq and hook_KEQUAL_eq, and none of them do have debug symbols, as shown in their metadata:

@str_lit_KEQUAL.eq = global [10 x i8] c"KEQUAL.eq\00"
@str_lit_hook_KEQUAL_eq = global [15 x i8] c"hook_KEQUAL_eq\00"

[Robertorosmaninho]

3dde152 and 67c4a41 partially solve the problem above.
It's now possible to find the function used to compute the k match, but two new issues arose then:

• We can't pretty print the function's arguments as the parameter's type is %block* instead of %string*.
• We can't pretty print the subject or the pattern when the match fails. This happens because the MatchLog entry contains no info about them. E.g., their content is just an empty string!

[Robertorosmaninho]

Further investigation is tracked in #746