How does bpftrace implement its printf function？

the bpftrace language supports the function printf which can write something to the terminal, but as far as I know ebpf running in kernel mode cannot call arbitrary kernel functions, so how is that implemented？ My rough guess is that bpftrace compile its printf function to bpf_trace_printk(which is a bpf helper being able to write formated text into TraceFS) and then the tracer process reads from /sys/kernel/tracing/trace_pipe to duplicate those text to stdout of the tracer process. But that routine would just be too slow.