Pie in the sky idea: Type recovery for a better debugging experience

Ecosystem
1

There’s been this idea I’ve been floating in my mind for a while on improving the debugging experience for OCaml, although I haven’t yet got round to working out the details to see if it is even possible at all.

The idea is to improve debugging output by working out the concrete types for the variables in scope, to allow for pretty-printing, evaluation etc.

Of course, OCaml erases types at run-time, so a naieve approach to do this would require changing internals of the compiler.

The idea that I’ve been playing with is to somehow use the call-stack + source code to essentially recover the concrete type information for any variables in scope at runtime - the potential benefits of this, if it were possible, would be that it wouldn’t require major (if any at all) changes to the compiler, and could provide more detailed information that just looking at the type at compile time (because we’d be observing concrete types, not abstract ones).

For example, consider map for lists:

(* in List.ml at compile time *)
let rec map (f: 'a -> 'b) (ls: 'a list) = match ls with 
    | [] -> []
    | (h: 'a) :: (t: 'a list) -> (f h: 'b) :: (map f t: 'b list)

If our main program were something like:

(* main.ml *)
let () = 
   let (vl: int list) = [1;2;3;4] in
   let (vl': float list) = List.map (fun vl -> float_of_int vl) vl in
   List.iter (fun (vl: float) ->
       print_float vl
   ) vl

Now, if we put a breakpoint in list.ml at lin 4, when the breakpoint is hit, our call-stack could abstractly be mapped back to our program as:

main.ml:4
list.ml:4
------------
breakpoint

So using this, could we work out that in our current call to map, 'a has been instantiated with int and 'b has been instantiated with float:

let rec map (f: int -> float) (ls: int list) = match ls with 
    | [] -> []
    | (h: int) :: (t: int list) -> (f h: float) :: (map f t: float list)

I haven’t put much more thought into this beyond the idea, so before I try out anything more involved, I thought I’d confer with the community to get their opinions.

What do you think? Is this possible? Has this direction been explored before? Any obvious counter-examples on which this would fail?

2 Likes
2

OTOH I’m reminded of the work presented recently at the OCaml workshop: Tracing OCaml Programs (OCaml 2022 - OCaml Users and Developers Workshop 2022) - ICFP 2022 .

1 Like
3

Yup, I’m actually working in the same lab as the author of that work :smiley:, it’s from discussions with @dariusf that I came to this idea.

1 Like
4

Speaking of debugging, out of curiosity, I was (very naively) wondering about the following: could an interactive debugger be developed using algebraic effects?
Adding breakpoints and reacting to them seem to be doable using effects, and might offer new possibilities, I guess.
Or maybe this is a completely silly idea…

1 Like
5

I believe @mshinwell had either planned or done a version of this (walking the stack for refining the types) in libmonda, his library for native debugging of OCaml programs.

1 Like
6

Ah, interesting!

I guess that is the repo. Doesn’t seem like it’s had many updates in recent years. I’d be curious to hear from @mshinwell on the experience he had on doing this, challenges or obstacles he ran into, and why the project seems to have fallen by the wayside.

This seems to be the closest thing to using the source code to recover type information, although I’m not sure it does what I’m thinking of exactly.

1 Like
7

The previous work (libmonda etc) uses the name of an identifier plus its unique stamp as the DWARF type. Then, given the .cmt file, the debugger can look up this stamp to extract the OCaml type. After that the OCaml type is transformed into a representation that can be used for printing values, in parallel with traversing the relevant value in the target program’s address space (or a reconstituted DWARF expression describing such, for values optimized out).

This isn’t ideal however for a couple of reasons: it requires the .cmt files, and it also requires a lot of support in the debugger (some of which is difficult, like seeing through abstract types to determine their actual definition). The latter also entails the debugger having to dynamically load OCaml code since compilerlibs is needed.

A better approach which we’re planning to investigate at some point is to properly encode OCaml types as some kind of “representation” or “printing” type directly in DWARF, if needs be augmenting the DWARF language for very OCaml-specific cases. This should mean that the debugger side is straightforward enough (without the need to use compilerlibs) to be implemented in C++, and the loading of .cmt files by the debugger will be avoided.

1 Like
8

Hi @mshinwell! Thanks for the very quick response!

The previous work (libmonda etc) uses the name of an identifier plus its unique stamp as the DWARF type.

Right, I see - I guess this is why you need a custom switch for libmonda to work.

Right, that certainly would be a better aproach, although I guess again requries changing the debug information emitted by the compiler.

Seeing as you’re already familiar with the design space, what do you think about the idea of using the source code alone to recover type information? I understand that it would probably require a lot more work on the debugger side, but if possible, would allow debugging without having to touch the compiler at all. Assuming that I’m willing to bite the bullet and load cmt files, do you think it would be possible to use the typed-tree and the runtime stack to recover typing information?

I’m not as familiar with the exact information emitted in the debug information, so there could be something obvious I’m missing here.

1 Like
9

After re-reading @mshinwell’s comments, I now actually understand what libmonda is doing. In effect, it is already doing this: the compiler is extended to tag variables with dwarf symbols that can then uniquely be mapped back to corresponding identifiers in the CMT, and thereby used to retrieve the type. I assume then that the function type_and_env_from_dwarf_type then works out an appropriate type for printing if it can find it.

What I’m slightly suprised by is that the type_and_env_from_dwarf_type function is so simple - are there cases that aren’t handled? Could the analysis be made more precise, or is this really all that has to be done?

I’m curious why this hasn’t been backported to OCamldebug? Is there just no demand?

@mshinwell , I understand my initial response might have fallen into the realm of “not even wrong”, but it would have been nice if you had seen fit to at least grace it with a response.

1 Like
10

I will reply, but it will need a little while as this is tricky.

2 Likes
11

OK, so regarding the idea of using the call stack: yes, some kind of analysis along these lines would probably be useful. I did some initial experiments with using the stack to recover types for polymorphic function parameters in libmonda, but it needed more work.

The problem is that you need more than this: it’s also necessary to explain to the debugger where the values of the various variables are to be found at runtime. You also need the types for all of the non-polymorphic variables. That needs support in the compiler (which is implemented in the OCaml distribution for bytecode but not native code).

It might be the case that for ocamldebug it would be possible to implement something like you suggest without too much work. I was only focussing on native code debugging, since the vast majority of production OCaml executables are compiled to native code.

Regarding type_and_env_from_dwarf_type, that function is straightforward because it’s just a lookup via a .cmt file. The difficult part is what has to be done to the retrieved OCaml type to prepare it for printing, which is elsewhere in libmonda.

2 Likes