A new format implementation based on GADTs

[vicuna]

Original bug ID: 6017
Reporter: bvaugon
Assigned to: @gasche
Status: closed (set by @xavierleroy on 2017-02-16T14:14:38Z)
Resolution: fixed
Priority: high
Severity: feature
Version: 4.00.1
Target version: 4.02.0+dev
Fixed in version: 4.02.0+dev
Category: standard library
Tags: patch
Related to: #5949 #6286 #6297 #7034
Monitored by: ibnfirnas @gasche @lpw25 mcclurmc @diml "Pascal Cuoq" bobot @chambart @jmeber @hcarty @yakobowski @alainfrisch

Bug description

I wrote a new implementation of formats unsing GADTs.

It contains modifications of Printf, Format and Scanf standard library
modules, and OCaml typer adaptations (principally in typing/typecore.ml).

In this new implementation, formats are compiled into GADTs trees by
the compiler and are "evaluated" by the printing and scanning functions.
The main advantages are :

• No longer use of Obj.magic in printf.ml, scanf.ml and format.ml.
• Better performances.
• Stronger static verifications of format validity (flag compatibilities, ...).
• Factorisation of format parsing in a single code (for all the stdlib
  and the OCaml compiler!) to ensure compatibility.

This new version is "mostly compatible" with the old-one. Differencies are :

• Some inconsistent formats are now statically rejected, like
  "%1.1s", "%#s", "%0c" (I had to slightly adapt the testsuite,
  principally to comment absud tests which no longer compile, so, obviously,
  I did not remove any test which still compile).
• Some bug fixes :
  • The semantic of (printf "%{...%}") (from comments of the testsuite).
  • The semantic of (scanf "%[^...]@x").
  • The '@%' escape syntax, like in (Format.printf "@%d%s" 42 "hello").
  • The managment of nested "%{...%}" and "%(...%)".
  • Buffer overflows dues to too big padding (or precision).
  • ...
• To obtain compatibility of Printf and Format formats, some '@' usages
  with an "invalid Format-like syntax" but a "valid Printf-like syntax"
  are now accepted by Format printing functions and literally printed.
  It is a small disadvantage because it is slightly less convenient to
  learn Format "formatting info" syntax by practice, sorry.

Since the OCaml standard library and the OCaml compilers use formats, the
bootstrap is a bit complicated.

I attach two patches (ocaml-4.00.1_new-formats_patch-{1,2}.diff) and
instructions to apply them into "howto-apply-new-formats-patches.txt".
This .txt file can be used (with a slight adaptation from your config.)
as an installation shell-script.

Please do not hesitate to send me any comments or questions about this code.

Benoît Vaugon.

File attachments

• fix-incompatible-formats-raising-time-patch.diff
• format_gadt_distinguish_N_L.txt
• howto-apply-new-formats-NOPAIR-patches.txt
• howto-apply-new-formats-PAIR-patches.txt
• howto-apply-new-formats-patches.txt
• ocaml-4.00.1_new-formats_NOPAIR_patch-1.diff
• ocaml-4.00.1_new-formats_NOPAIR_patch-2.diff
• ocaml-4.00.1_new-formats_PAIR_fix-expected-type.diff
• ocaml-4.00.1_new-formats_PAIR_patch-1.diff
• ocaml-4.00.1_new-formats_PAIR_patch-2.diff
• ocaml-4.00.1_new-formats_patch-1.diff
• ocaml-4.00.1_new-formats_patch-2.diff
• special_case_for_small_arities.ml

[vicuna]

Comment author: @gasche

While I have not yet reviewed the implementation in detail, I have
been in contact with Benoît during the polishing part of this
considerable work, which I happily support. Here are some general
comments on the general design to help people get an understanding of
this change. Apologies in advance for any inaccuracy.

The change can be summarized as this: instead of being kept as
a format string all the way to runtime use of the format (where it is
parsed by the printf/scanf/formatf) function, it is replaced by a GADT
value that describes the format (with a subtle enough typing to mirror
the way phantom types are currently used in the format6 type). Instead
of re-parsing the format at runtime, the GADT value is matched over
the produce the desired semantics.

Below is a more detailed high-level comment.

The current way OCaml handles format strings can be roughly summarized
as follows:

• there is no syntactic difference between formats and string literals

• the type inference engines handles string literals as having an
  ambiguous type (either [string] or [(...) format6]), which is
  propagated through inference, and possibly forced by other operators
  that do expect either a string or a format (printf/scanf/format,
  format_of_string...); the type parameters of the [(...) format6]
  type are determined by parsing the format to determine the number
  and type of its expected parameters, etc.

• At runtime, the functions in Printf/Scanf/Format parse the format
  string for a second time, printing or reading as it goes. This part
  is full of unsafe code (Obj.magic) to get an undetermined number of
  parameters, etc. The details of how advanced features of the format
  work are often quite horrible; for example, advanced number
  formatting options (padding, decimal, etc.) are interpreted by
  calling the C [sprintf] function, but those formats are sometimes
  rewritten instead of being passed as is (to handle advanced feature
  such as "%.*d which allows to pass the decimal length as a dynamic
  parameter, implemented as rewriting the format passed to [sprintf]
  at runtime).

The duplicated parsing, once at type-checking time and once at
runtime, is source of numerous causes of bugs: some formats that are
ill-supported at runtime are accepted by the type-checker. The use of
unsafe Obj.magic is also a cause of bugs. Several segfault bugs have
been found in the last few months, and Benoît has found some more
during his reimplementation work.

The change by Benoît turns format handling into the following picture:

• still no syntactic treatment of format strings (this is to be
  constrasted with the various Camlp4 extensions implementing custom
  formats by adding a custom lexical syntax for formats; which is
  probably the right design after all, but cannot be adopted here for
  compatibility reasons)

• at typing time, the (tricky) inference part is unchanged; but when
  a string is determined to be a format, it is parsed in the same way
  as before (with some bugfixes "en passant" from Benoît), but this
  information is used to construct a term at a GADT type ([(...)
  format6] is defined as a GADT), which has precisely the expected
  type. Here is an choice piece of the new format6 declaration:

  • | Float : (* %[feEgGF] *)

  •  float_conv * ('x, 'y) padding * ('y, float -> 'a) precision *
    

  •  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
    

  •    ('x, 'b, 'c, 'd, 'e, 'f) format6
    

  • | Bool : (* %[bB] *)

  •  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
    

  •    (bool -> 'a, 'b, 'c, 'd, 'e, 'f) format6
    

  • | Flush : (* %! *)

  •  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
    

  •    ('a, 'b, 'c, 'd, 'e, 'f) format6
    

  • | String_literal : (* abc *)

  •  string * ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
    

  •    ('a, 'b, 'c, 'd, 'e, 'f) format6
    

  [..]

  • | End_of_format :

  •    ('f, 'b, 'c, 'e, 'e, 'f) format6
    

  The format "this is %b" will be transformed into the following GADT
  value (approximatively):
  String_literal ("this is ", Bool (End_of_format))

• at runtime, there is no format string to be parsed again: the
  printf/scanf/format implementation can directly interpret the GADT
  description of the format. Thanks to the rich GADT typing, there
  is no need for unsafe features anymore: Obj.magic is gone. An
  amusing aspect of the change is that
  [string_of_format : (...) format6 -> string] was previously the
  identity (as the runtime representation of formats was precisely
  the string), and is now a function "unparsing" the GADT value:

  +let bprint_format buf fmt =

  • let rec fmtiter : type a b c d e f .

  •  (a, b, c, d, e, f) format6 -> bool -> unit =
    

  • fun fmt ign_flag -> match fmt with
  • | String (pad, rest) ->

  •  buffer_add_char buf '%'; bprint_ignored_flag buf ign_flag;
    

  •  bprint_padding buf pad; buffer_add_char buf 's';
    

  •  fmtiter rest false;
    

  • | Caml_string (pad, rest) ->

  •  buffer_add_char buf '%'; bprint_ignored_flag buf ign_flag;
    

  •  bprint_padding buf pad; buffer_add_char buf 'S';
    

  •  fmtiter rest false;
    

  • | Int (iconv, pad, prec, rest) ->

  •  bprint_int_fmt buf ign_flag iconv pad prec;
    

  •  fmtiter rest false;
    

I believe this change is highly desirable: it rationalizes the runtime
handling of formats, removes a heap of bugs, documents a pile of
obscure features, and has as its core an elegant use of GADTs.

However, due to the large number of features in the OCaml format
types, the patch is not small. The [format6] GADT has 23
constructors, each handling an orthogonal feature of format. Handling
all this stuff makes for a very large patch: in total, 1835 lines are
removed (mostly the runtime handling of format), and 3304 lines are
added. I find the code well-written and easy to read, but its review
and discussion may still take a bit of time.

[vicuna]

Comment author: @yallop

I like this idea a lot. If I'm not mistaken, format could now be written entirely as a library, without special compiler support, using ppx or camlp4 to turn the strings into a GADT tree. (Of course, we'll want to keep format around for backwards compatibility).

[vicuna]

Comment author: @alainfrisch

This is an impressive piece of work, which I'd like to see integrated at some point. It probably deserves to be tested in the wild, on large code bases. I know there is some reluctance against using recent additions to the language within the core compiler or stdlib. What about integrating the patch on the trunk after the branch for the next release has been created? This would make it easy to test it, while providing a full release cycle before it is officially release, and a release branch for bug fix releases, if required.

[vicuna]

Comment author: @johnwhitington

This looks great.

What is the effect on the readability of type errors? An improvement? Worse? The same? It's rather hard to explain to students those complicated format4 / format6 types...

[vicuna]

Comment author: bvaugon

I confirm that typing errors with format types are difficult to understand (and to explain to students). Unfortunately, this patch does not change anything because the inferred types are the same, and the unification produces the same typing errors.

However, I have a suggestion to try to improve this problem about error messages containing format types, and I would like some outside opinions on this potential issue. What do you think to modify the type pretty-printer to display format types in this way:

"%d%s%c" format

rather than:

(int -> string -> char -> 'a,' b, 'c,' d, 'd, 'a) format6

We then get this kind of error message:

This expression has type "%d%s%c" format but an expression was expected of type "%d%d%c" format.

Unfortunately, all type parameters are not necessarily instantiated when generating the error message. These cases would require the display of format types like:

"%d%?%?" format

or maybe:

"%d%['a]%['c]" format

to name type parameters.

Does someone have an opinion or a better idea ?

[vicuna]

Comment author: @gasche

I'd rather not mix a discussion about a change to the runtime with new feature ideas about printf/scanf/format. My gut feeling would be to first discuss and handle what can be done purely as an internal change, with no modification to the observable behavior. Then, once we know for sure the status of the change, we can act on it and have room for discussion of observable changes based on this experience.

If you think there is value in having these other discussions right now rather than in a few weeks/months, I would suggest a separate bugtracker issue.

[vicuna]

Comment author: bobot

That's a great work. I was wondering if the author can think of ways for improving Format.ikfprintf, Format.ifprintf, Printf.ifprintf:

let debug = ref false

let dprintf fmt =
if !debug
then Format.fprintf Format.err_formatter fmt
else Format.ifprintf Format.err_formatter fmt

Such a function is useful for printing conditionaly debugging information. With the old implementation the cost is quite high since even when debug is false the format string is parsed. With the new implementation that should be faster but there is some allocation.

Currently the best dprintf version that I know, consists to use specialize version without ifprintf:

let dprintf0 fmt =
if !debug
then Format.fprintf Format.err_formatter fmt

let dprintf1 fmt x1 =
if !debug
then Format.fprintf Format.err_formatter fmt x1

let dprintf2 fmt x1 x2 =
if !debug
then Format.fprintf Format.err_formatter fmt x1 x2

...

But the user must select the correct version.

Is it possible to reduce the cost of ifprintf? A specialized version of make_printf: (a, b, c, c, c, unit) CamlinternalFormatBasics.format6 -> a that construct nothing except closure? By adding the number of remaining argument in format6 for faster application for small arities?

Once again thank you for this great job,

[vicuna]

Comment author: @gasche

I'm not sure there is some allocation: the generated GADTs are constant immutable values, and there should therefore be pre-allocated by the compilers.

[vicuna]

Comment author: bvaugon

The GADT representing the format is not allocated by printing
functions, but an accumulator (an heterogeneous linked list
storing arguments to delay printing) and intermediate closures
are allocated each time {if,k,...}printf are called. I can easily
write an ifprintf which do not allocate the accumulator, but it
is more difficult to remove closure creations.

[vicuna]

Comment author: bvaugon

Oh, sorry, to write an ifprintf which allocates nothing (as in
bytecode and native version) if the number of arguments is less than a
bound N (3 in the following example) is simple with the new
implementation of formats. It looks like this:

type ('a, 'b) iprintf_acc =
| IPrintf_arg_0 : ('b, 'b) iprintf_acc
| IPrintf_arg_1 : ('a1 -> 'b, 'b) iprintf_acc
| IPrintf_arg_2 : ('a1 -> 'a2 -> 'b, 'b) iprintf_acc
| IPrintf_arg_3 : ('a1 -> 'a2 -> 'a3 -> 'b, 'b) iprintf_acc
| IPrintf_arg_N : ('aR, 'b) iprintf_acc -> ('ai -> 'aR, 'b) iprintf_acc

let rec fun_of_iprintf_acc : type a . (a, unit) iprintf_acc -> a =
fun acc -> match acc with
| IPrintf_arg_0 -> ()
| IPrintf_arg_1 -> iprintf_ignore_1
| IPrintf_arg_2 -> iprintf_ignore_2
| IPrintf_arg_3 -> iprintf_ignore_3
| IPrintf_arg_N rest -> fun _ -> fun_of_iprintf_acc rest
and iprintf_ignore_1 : type a1 . a1 -> unit = fun _ -> ()
and iprintf_ignore_2 : type a1 a2 . a1 -> a2 -> unit = fun _ _ -> ()
and iprintf_ignore_3 : type a1 a2 a3 . a1 -> a2 -> a3 -> unit = fun _ _ _ -> ()

let rec iprintf_acc_succ : type a b c .
(a, c -> b) iprintf_acc -> (a, b) iprintf_acc =
fun acc -> match acc with
| IPrintf_arg_0 -> IPrintf_arg_1
| IPrintf_arg_1 -> IPrintf_arg_2
| IPrintf_arg_2 -> IPrintf_arg_3
| IPrintf_arg_3 -> IPrintf_arg_N IPrintf_arg_3
| IPrintf_arg_N rest -> IPrintf_arg_N (iprintf_acc_succ rest)

let rec make_iprintf fmt = make_iprintf_aux IPrintf_arg_0 fmt
and make_iprintf_aux : type a b c x .
(x, a) iprintf_acc ->
(a, b, c, c, c, unit) CamlinternalFormatBasics.format6 -> x =
fun acc fmt -> match fmt with
| Char rest -> make_iprintf_aux (iprintf_acc_succ acc) rest
| Bool rest -> make_iprintf_aux (iprintf_acc_succ acc) rest
| String_literal (_, rest) -> make_iprintf_aux acc rest
| End_of_format -> fun_of_iprintf_acc acc
| _ -> assert false (* Other cases not yet implemented *)

let ifprintf _ fmt = make_iprintf fmt

However, if this code is integrated into the standard library, it may
be even increase the size of camlinternalFormat.ml. Does it matter?

[vicuna]

Comment author: bobot

Nice, you still need to look at all the formatter but at least it does just that.

I tried by adding the size of the formatter in format6 (your format6 is format6_aux):
type ('a, 'b, 'c, 'd, 'e, 'f) format6 =
| App0: ('f, 'b, 'c, 'd, 'e, 'f) format6_aux
-> ('f, 'b, 'c, 'd, 'e, 'f) format6
| App1: ('a1 -> 'f, 'b, 'c, 'd, 'e, 'f) format6_aux
-> ('a1 -> 'f, 'b, 'c, 'd, 'e, 'f) format6
| App2: ('a1 -> 'a2 -> 'f, 'b, 'c, 'd, 'e, 'f) format6_aux
-> ('a1 -> 'a2 -> 'f, 'b, 'c, 'd, 'e, 'f) format6
| App3: ('a1 -> 'a2 -> 'a3 -> 'f, 'b, 'c, 'd, 'e, 'f) format6_aux
-> ('a1 -> 'a2 -> 'a3 -> 'f, 'b, 'c, 'd, 'e, 'f) format6
| App4: ('a1 -> 'a2 -> 'a3 -> 'a4 -> 'f, 'b, 'c, 'd, 'e, 'f) format6_aux
-> ('a1 -> 'a2 -> 'a3 -> 'a4 -> 'f, 'b, 'c, 'd, 'e, 'f) format6
| Appn: ('a, 'b, 'c, 'd, 'e, 'f) format6_aux ->
('a, 'b, 'c, 'd, 'e, 'f) format6

The nice point is that ifprintf and printf, fprintf, ... can be implemented without any closure but you need one function as big as make_printf by arity.

...

let app4 : type a1 a2 a3 a4 b c d .
(b,c) print -> (b -> d) -> b ->
(a1 -> a2 -> a3 -> a4 -> d, b, c, c, c, d) format6_aux ->
a1 -> a2 -> a3 -> a4 -> d =
fun print k o fmt x1 x2 x3 x4 ->
begin match docst print o fmt with
| Bool fmt -> print.string o (string_of_bool x1); app3 print k o fmt x2 x3 x4
| Alpha fmt -> print.alpha o (x1 o x2); app2 print k o fmt x3 x4
| String_literal _ -> assert false (* docst should have take care of it *)
end

let make_print2 : type a b c d .
(b,c) print -> (b -> d) ->
(b -> (b, c) acc -> d) ->
b ->
(a, b, c, c, c, d) format6 -> a =
fun print k output o fmt ->
match fmt with
| App0 fmt -> app0 print k o fmt
| App1 fmt -> app1 print k o fmt
| App2 fmt -> app2 print k o fmt
| App3 fmt -> app3 print k o fmt
| App4 fmt -> app4 print k o fmt
| Appn fmt -> make_printf output o End_of_acc fmt

(all the code for just a few case is uploaded as special_case_for_small_arities.ml)

I can't think of a generic version of app that doesn't use a closure, except if the inliner can create all the version by itself with the following definitions:

let app_gen f1 f2 x2 x1 o = ... f1 o ... f2 x2 o ...

let app3 x3 x2 x1 o = app_gen (app1 x3) (app2 x3) x2 x1 o
let app4 x4 x3 x2 x1 o = app_gen (app2 x4 x3) (app3 x4 x3) x2 x1 o
let app5 x5 x3 x2 x1 o = app_gen (app3 x5 x4 x3) (app4 x5 x4 x3) x2 x1 o

[vicuna]

Comment author: bobot

Just another question about your patch:

Do you only need the type acc to start printing only when the application is complete? Is it specified in the documentation or is it for respecting the old behavior?

[vicuna]

Comment author: @gasche

If the question is "do you really need acc?", the answer is 'yes'. As it is the interpretation of the GADT values that does the consumption of the arguments one after the other, you need the accumulator to delay all printing actions until all arguments have been consumed.

Otherwise constructing the closure

let print_id = Printf.printf "%s: %d\n" Conf.i18n_id_name

would start printing stuff before the remaining %d argument is given. This is clearly not the correct semantics (because it would be printed only once, instead of each time print_id is applied, as expected by the user).

[vicuna]

Comment author: bobot

My second question was: Is this behavior specified somewhere in the documentation or is it only for respecting the old behavior (which must be done!)?

Gabriel, in another world where it is not specified if printf can start printing before complete application (it is also a possible semantics), you will write

let print_id id = Printf.printf "%s: %d\n" Conf.i18n_id_name id

and in this other world Benoît will implement a make_printf which process directly the argument and which is easier to inline. So its easier in this world to make printf as fast as using directly the output functions:

http://www.lexifi.com/blog/note-about-performance-printf-and-format

But we are not in this other world, so Benoît created the acc type, and we should hope that the improvement done in the inliner will be greater in this world than in the other.

I really like the patch proposed by Benoît and it already give speed-up and simplification, that's why I want to know if we can push it further.

[vicuna]

Comment author: @gasche

I am strongly opposed to any change of the semantics that would amount to printing starting before complete application. This is certain to break existing programs¹, and I don't think a patch doing that should be accepted.

¹: and not even some hitting some bug or misbehavior of the current implementation and not noticing it; some perfectly reasonable user programs.

There is in fact a similar problem with invalid_arg failures due to runtime-invalid format, that is done "wrong" in the patch. I'm writing a longer (too long) message about my first forays at patch review, and will write about this more than anyone (except maybe Benoît) wants to read :-)

Regarding performances, Benoît had made early measurements on a much simpler prototype, that shown that the performance it when compared to "using directly the output functions" was reasonable (around 10%-30%, iirc., compared to the several-times slowdown observed by Alain). Benoît, do you think you could update those small speed experiments for the current patch?

I would even be in favor of considering reverting some of the changes made by Alain on performance grounds, turning Format.printf into direct printers in the compiler code. But that will be evaluated and discussed with him in due time.

On a related note, replacing formats with direct printing function may result in large increase in code size. Benoît's expansion into a GADT preserves the compact code size we had with the previous one -- as opposed to some other translation schemes that produce large code closures. It is unclear that always inlining to the native functions will actually improve performances (I've often seen excessive -inline tunings results in slowdown) -- but that will be left to the tricky inliner heuristics to decide.