-
Notifications
You must be signed in to change notification settings - Fork 152
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add #trace
debugging hook
#2560
Conversation
do not incur this overhead again; the definition is cached. | ||
|
||
```k | ||
syntax {Sort} K ::= #trace(value: Sort) [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have to wonder if we might be better off changing the signature of this somewhat. People are probably going to end up pretty surprised if they try to trace a builtin sort, because it's not going to work. I would suggest we instead have two overloads, both of which have the same hook tied to them: one that takes a KItem and one that takes a K. The reason I suggest two is that if you just do K, then everything will get pretty-printed with a ~> .
at the end, but if you just do KItem, then you won't be able to pretty print k sequences. That being said, using the KItem one in most cases ought to be sufficient because it will automatically inject whatever sort you want into KItem and the injection will be pretty-printed invisibly, so you ought to get the same output as if you had pretty-printed a particular sort. Except that it will be able to handle builtin sorts.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What's the best way to write that overloaded version? If I have:
syntax K ::= #trace(value: K) [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol, klabel(#traceK)]
| #trace(value: KItem) [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol, klabel(#traceKItem)]
then I get parsing ambiguities on the argument:
[Error] Inner Parser: Parsing ambiguity.
1: syntax K ::= "#trace" "(" K ")" [function, functional, hook(IO.traceTerm), impure, klabel(#traceK), returnsUnit, symbol]
#traceK(`bar_*__TEST_Bar_Foo_Foo`(`foo(_)_TEST_Foo_Int`(#token("2","Int")),`foo(_)_TEST_Foo_Int`(#token("0","Int"))))
2: syntax K ::= "#trace" "(" KItem ")" [function, functional, hook(IO.traceTerm), impure, klabel(#traceKItem), returnsUnit, symbol]
#traceKItem(`bar_*__TEST_Bar_Foo_Foo`(`foo(_)_TEST_Foo_Int`(#token("2","Int")),`foo(_)_TEST_Foo_Int`(#token("0","Int"))))
Source(/home/bruce/code/k/k-distribution/tests/regression-new/trace/test.k)
Location(13,20,13,47)
13 | (#trace(F2) ~> #trace(bar foo(2) * foo(0)) ~> .K)
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~
This hook exposes the implementation in runtimeverification/llvm-backend#513, along with a note explaining that calling it is expensive and should only be done as a debugging aid.
Additionally, an integration test for the hook is added to ensure that it's printing the expected syntax.
Requires runtimeverification/llvm-backend#513 to be merged, and the corresponding submodule update to go through.