[GDB] Can't print builtin types on LHS of rules in K Match

[Robertorosmaninho]

GDB Types to Fix:

• Int
• Float
• Bool
• String
• List
• Map
• Set

Given the K definition:

module TEST
  imports INT
  imports STRING
  
  syntax Foo ::= foo(Int)
  syntax FooString ::= fooString(String)

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

Kompile:

kompile test.k --enable-llvm-debug --syntax-module TEST

Krun and GDB with Int:

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

(gdb) k start
...
(gdb) k match TEST.test subject
INT.size_int(0) => 0
Traceback (most recent call last):
  File "<string>", line 794, in invoke
gdb.error: No type named SortMInt{Sort32{}}.

Python Exception <class 'gdb.error'>: No type named SortMInt{Sort32{}}.
Error occurred in Python: No type named SortMInt{Sort32{}}

Krun and GDB with String:

 krun -cPGM='fooString("Hi")' --debugger 

(gdb) k start
...
(gdb) k match TEST.testString subject
KEQUAL.eq(0x7ffff5400080, 0x2e5310 <token_48656c6c6f20576f726c6421>) => false
Traceback (most recent call last):
  File "<string>", line 794, in invoke
gdb.error: No type named .

Python Exception <class 'gdb.error'>: No type named .
Error occurred in Python: No type named .

[Robertorosmaninho]

Wrong debug information when pattern matching bool in LHS of a rule:

module TEST
  imports BOOL

  syntax FooBool ::= fooBool(Bool)
  rule [testPatternBool]: fooBool(true) => .K
end module

Kompile:

kompile test.k --enable-llvm-debug --syntax-module TEST

krun and GDB:

krun -cPGM='fooBool(false)' --debugger
(gdb) k start
...
(gdb) k match TEST.testPatternBool subject
Subject:
true # should be false
does not match pattern:
true
(gdb)

[Robertorosmaninho]

Can't output a float subject when the k match fails on a rule with a float in its LHS:

module TEST
  imports FLOAT

  syntax FooFloat ::= fooFloat(Float)
  rule [testPatternFloat]: fooFloat(0.0) => .K 
end module

Kompile:

kompile test.k --enable-llvm-debug --syntax-module TEST

krun and GDB:

krun -cPGM='fooFloat(1.0)' --debugger 
(gdb) k start
...
(gdb) k match TEST.testPatternFloat subject
FLOAT.trueeq(1.0, 0.0) => false
Traceback (most recent call last):
  File "<string>", line 794, in invoke
gdb.error: No type named .

Python Exception <class 'gdb.error'>: No type named .
Error occurred in Python: No type named .

Edit: After some investigation, I found out that both the sort and the pattern are empty when trying to print the MatchLog::Fail:

GDB code:

 print("Debug: [sort] (" + sort + ") | " + '[pattern] (' + pattern + ')')

Output:

Debug: [sort] () | [pattern] ()

MatchLog entry:

{kind = MatchLog::FAIL, function = 0x0, debugName = 0x0, result = 0x0, args = std::vector of length 0, capacity 0, pattern = 0x2f5ef0 <str_lit_> "", subject = 0x7ffff5400088, sort = 0x2f5ef0 <str_lit_> ""}

[Robertorosmaninho]

Can't output a List subject when the k match fails on a rule with a List in its LHS:

module TEST
  imports LIST

  syntax FooList ::= fooPatternList(List)
  rule [testPatternList]: fooPatternList(.List) => .K
end module

Kompile:

kompile test.k --enable-llvm-debug --syntax-module TEST

krun and GDB:

krun -cPGM='fooPatternList(ListItem(0))' --debugger 
(gdb) k start
...
(gdb)k match TEST.testPatternList subject
LIST.size_long(ListItem ( 0 )) => 0
Traceback (most recent call last):
  File "<string>", line 794, in invoke
gdb.error: No type named SortMInt{Sort64{}}.

Python Exception <class 'gdb.error'>: No type named SortMInt{Sort64{}}.
Error occurred in Python: No type named SortMInt{Sort64{}}.

[Robertorosmaninho]

Can't output a Map subject when the k match fails on a rule with a Map in its LHS:

module TEST
  imports MAP

  syntax FooMap ::= fooPatternMap(Map)
  rule [tesPatterntMap]: fooPatternMap(.Map) => .K 
end module

Kompile:

kompile test.k --enable-llvm-debug --syntax-module TEST

krun and GDB:

krun -cPGM='fooPatternMap(0|-> 0)' --debugger
(gdb) k start
...
(gdb) k match TEST.tesPatterntMap subject
MAP.size_long(0 |-> 0) => 0
Traceback (most recent call last):
  File "<string>", line 794, in invoke
gdb.error: No type named SortMInt{Sort64{}}.

Python Exception <class 'gdb.error'>: No type named SortMInt{Sort64{}}.
Error occurred in Python: No type named SortMInt{Sort64{}}.

[Robertorosmaninho]

Can't output a Set subject when the k match fails on a rule with a Set in its LHS:

module TEST
  imports SET

  syntax FooSet ::= fooSet(Set)
  rule [testPatternSet]: fooSet(.Set) => .K
end module

Kompile:

kompile test.k --enable-llvm-debug --syntax-module TEST

krun and GDB:

krun -cPGM='fooSet(SetItem(0))' --debugger  
(gdb) k start
...
(gdb) k match TEST.testPatternSet subject
SET.size_long(SetItem ( 0 )) => 0
Traceback (most recent call last):
  File "<string>", line 794, in invoke
gdb.error: No type named SortMInt{Sort64{}}.

Python Exception <class 'gdb.error'>: No type named SortMInt{Sort64{}}.
Error occurred in Python: No type named SortMInt{Sort64{}}.

[Robertorosmaninho]

Update on this: Even though we have the correct mechanism to add SortMInt{Sort64{}} on our gdb.types we're not using it as expected. That is because we don't add it as debug info. The only apparition of this type is as a Sort Fail possibility on the phi node generated on the fail block of intern_match_*.

[Robertorosmaninho]

A possible idea to solve this is to declare the possible sorts (arguments on this phi function) as global variables...
Any thoughts on this @Baltoli?

[Baltoli]

I don't fully understand why this code is trying to print out the sort MInt{64}. Can you remind me of what's going on here?

[Robertorosmaninho]

Of course! I can say for sure about this rule [test]: foo(42) => .K the idea when using krun -cPGM='foo(0)' --debugger would be to print the 0 as subject and the 42 as the pattern. However, we have this error when we try to print the subject.

• The error within string is that both sort and pattern are empty (the result of their phi function)
• Same for Float
• Can't remember for Bool
• Neither for Set, Map, List. Although, I have a hard intuition that at least these 3 have the same issue. (Hopefully, fixing the first integer problem, this issue will be fixed as well, or at least closer to a fix.)

[Baltoli]

Yes, but why specifically is the code doing anything with MInt{...}?

[Robertorosmaninho]

That's the final type of the subject phi function. We try to cast the subject to MInt{...}, thus giving this error as the MInt is not registered as a DebugInfoType

[Baltoli]

So the problem is that the match function is not setting the sort and pattern correctly on failing log entries when testing the match - is that correct?

[Robertorosmaninho]

Yeah, I believe that is the general case, indeed! We do have a case on printing the arguments of the function in the string case:

KEQUAL.eq(0x7ffff5400080, 0x2e5310 <token_48656c6c6f20576f726c6421>) => false

But the fail case is the most complex error...

[Baltoli]

Well, I guess the fix is to look at the function that populates the match log and identify why it fails to set the log entries correctly and falls through to the final case. I don't know off-hand why that's going to be, but let me know if you want a hand debugging anything.

[Robertorosmaninho]

Yeah, I would like a hand on this, I've already tried it a lot and have yet to come up with any solutions...

[Baltoli]

Reinvestigate now that the LLVM 16 opaque pointers change has been merged.