Module Flambda2_term_basics.Inlined_debuginfo

A value of type t represents one instance of inlining out a particular function application.

create ~called_code_id ~apply_dbg should be used when a function application (i.e. Apply_expr term) with debuginfo apply_dbg is to be inlined out. create must be called for each such instance of inlining.

Merge an existing value of type t with from_apply_expr, the latter corresponding to an Apply_expr term that is being inlined out.

For an instance of inlining t and a debuginfo value dbg occurring in the body of the corresponding function to be inlined, return a new debuginfo value to replace the old one.

The new debuginfo value will consistently have the same, fresh, uid on every item corresponding to the inlined body (i.e. every item except those at the head of the list, which are those---typically just one item in fact---that came from the apply_dbg passed to create). It might seem that every debuginfo value ends up with the same uid throughout---but this will not be the case in the situation where apply_dbg contains inlined frames (i.e. the inlined-out call site was only exposed by inlining) in addition to the inlined frame(s) arising from the inlined-out body. See the last example below.

In addition, the first (outermost, less deep inlining) debuginfo item arising from the inlined body is annotated with the function symbol from the application term being inlined out. Inductively, in association with the general propagation of Debuginfo.t values by Flambda 2, the consequence is that Debuginfo.t values returned from this function end up annotated with function symbols at all points except the outermost frame. (The symbol for that frame will be known by the backend, since it is the function into which everything is ultimately being inlined.) This can be seen by looking at the "FS=" annotations in the following examples.

For example in:

let@inline f x = (Sys.opaque_identity x) + 1 let@inline g x = 2 * f x let foo x = g x - f x

we have the following in f:

Paddint/44N = ((+ Popaque/43N 1) example.ml:1,19--46)

and the following in g:

Paddint/61N = ((+ Popaque/60N 1) example.ml:2,23--26; <-- this is a position in the current function example.ml:1,19--46871832529FS=camlExample.f_0_3_code) ^ \-- this is a position in the first (outermost) inlined frame Pmulint/62N = (( * 2 Paddint/61N) example.ml:2,19--26)

and the following in foo:

Paddint/80N = ((+ Popaque/79N 1) example.ml:3,18--21; example.ml:1,19--4619414450FS=camlExample.f_0_3_code) Paddint/90N = <- call this addition A ((+ Popaque/89N 1) example.ml:3,12--15; example.ml:2,23--2683388650FS=camlExample.g_1_4_code; ^ \-- this is a position in the first (outermost) inlined frame example.ml:1,19--4683388650FS=camlExample.f_0_3_code) ^ \-- this is a position in the deepest (innermost) inlined frame Pmulint/91N = (( * 2 Paddint/90N) example.ml:3,12--15; example.ml:2,19--2683388650FS=camlExample.g_1_4_code)

Note that in foo the two instances of the addition have different uids. Moreover, even though in g the addition and multiplication have different uids (indeed no uid on the multiplication, as it hasn't come from an inline frame), after inlining of g they both have the same uid.

To show why different uids may occur within a single Debuginfo.t, consider the following extension of the above example, where a call site is revealed by inlining:

let@inline bar f x = f x let baz x = bar foo x

The term marked as "addition A" above now looks like this:

Paddint/144N = ((+ Popaque/143N 1) example.ml:6,12--21; example.ml:5,23--2688799133FS=camlExample.bar_3_8_code; example.ml:3,12--15777401542FS=camlExample.foo_2_7_code; example.ml:2,23--26777401542FS=camlExample.g_1_6_code; example.ml:1,19--46777401542FS=camlExample.f_0_5_code)

The uid 88799133 corresponds to the instance of inlining that revealed the call to foo inside bar; and the uid 777401542 corresponds to the instance of inlining that populated the body of bar itself.

Equipped with the Debuginfo.t items and uids, the backend can reconstruct the inlining tree, with per-instruction granularity. The stacks of items within each Debuginfo.t show which functions got inlined into which other; and the uids enable disambiguation between different instances of inlining the same functions.