[multicore][logging] improve thread safety

Summary:
Format is stateful and thus problematic for multicore. We use
- Format.synchronized_formatter_of_out_channel
- Format.get_std_formatter
- Format.get_err_formatter
- Format.get_str_formatter
and domain-local storage where possible to get thread-safe and interleaving-safe formatters.

This still leaves some tricky uses of global state in Logging for further work.

Reviewed By: jvillard

Differential Revision: D67188761

fbshipit-source-id: e088b0c46a7b56573b011629dd65b4f300b185df

infer/src/IR/Io_infer.ml

@@ -15,6 +15,8 @@ module L = Logging
 
 (* =============== START of module Html =============== *)
 module Html = struct
+  type t = Unix.File_descr.t * Format.formatter DLS.key
+
   (** Create a new html file *)
   let create source path =
     if SourceFile.is_invalid source then
@@ -28,7 +30,7 @@ module Html = struct
     in
     let fd = DB.Results_dir.(create_file (Abs_source_dir source)) dir_path in
     let outc = Unix.out_channel_of_descr fd in
-    let fmt = F.formatter_of_out_channel outc in
+    let fmt = F.synchronized_formatter_of_out_channel outc in
     let script =
       {|
 <script>
@@ -51,7 +53,7 @@ function toggleListingOnTop() {
     listing.classList.add(sticky_class);
   }
 }
-       
+
 function toggleListingVisibility() {
   var listing = document.querySelector("#node_listing > code");
   if (listing.style.display == "none") {
@@ -83,7 +85,7 @@ h1 { font-size:14pt }
 .with_tooltip { position: relative; }
 .with_tooltip:hover .tooltip, .visited:hover .tooltip { display: block; }
 #node_listing { margin-top: 5pt; margin-bottom: 5pt; }
-.sticky_header { position: fixed; top: 0; width: 100%; background-color: #eeeee4; }         
+.sticky_header { position: fixed; top: 0; width: 100%; background-color: #eeeee4; }
 details { padding-left: 20pt; }
 summary { margin-left: -20pt; }
 .d_with_indent { padding-left: 20pt; }
@@ -109,7 +111,7 @@ summary { margin-left: -20pt; }
 |}
         fname script style
     in
-    F.pp_print_string fmt page ;
+    F.pp_print_string (DLS.get fmt) page ;
     (fd, fmt)
 
 
@@ -132,7 +134,7 @@ summary { margin-left: -20pt; }
       Unix.openfile (DB.filename_to_string full_fname) ~mode:[O_WRONLY; O_APPEND] ~perm:0o777
     in
     let outc = Unix.out_channel_of_descr fd in
-    let fmt = F.formatter_of_out_channel outc in
+    let fmt = F.synchronized_formatter_of_out_channel outc in
     (fd, fmt)
 
 
@@ -145,7 +147,7 @@ summary { margin-left: -20pt; }
 
   (** Close an Html file *)
   let close (fd, fmt) =
-    F.fprintf fmt "</body>@\n</html>@." ;
+    F.fprintf (DLS.get fmt) "</body>@\n</html>@." ;
     Unix.close fd
 
 

infer/src/IR/Io_infer.mli

@@ -11,10 +11,12 @@ open! IStd
 (** Module to handle IO. Includes html and xml modules. *)
 
 module Html : sig
-  val close : Unix.File_descr.t * Format.formatter -> unit
+  type t = Unix.File_descr.t * Format.formatter DLS.key
+
+  val close : t -> unit
   (** Close an Html file *)
 
-  val create : SourceFile.t -> DB.Results_dir.path -> Unix.File_descr.t * Format.formatter
+  val create : SourceFile.t -> DB.Results_dir.path -> t
   (** Create a new html file *)
 
   val modified_during_analysis : SourceFile.t -> DB.Results_dir.path -> bool
@@ -23,7 +25,7 @@ module Html : sig
   val node_filename : Procname.t -> int -> string
   (** File name for the node, given the procedure name and node id *)
 
-  val open_out : SourceFile.t -> DB.Results_dir.path -> Unix.File_descr.t * Format.formatter
+  val open_out : SourceFile.t -> DB.Results_dir.path -> t
   (** Open an Html file to append data *)
 
   val pp_line_link :

infer/src/backend/printer.ml

@@ -15,9 +15,9 @@ module L = Logging
 module F = Format
 
 (** Current formatter for the html output *)
-let curr_html_formatter = ref F.std_formatter
+let curr_html_formatter = DLS.new_key F.get_std_formatter
 
-let () = AnalysisGlobalState.register_ref ~init:(fun () -> F.std_formatter) curr_html_formatter
+let () = AnalysisGlobalState.register_dls ~init:F.get_std_formatter curr_html_formatter
 
 (** Return true if the node was visited during analysis *)
 let is_visited node =
@@ -71,13 +71,14 @@ end = struct
     let proc_name = Procdesc.Node.get_proc_name node in
     let nodeid = (Procdesc.Node.get_id node :> int) in
     let node_fname = Io_infer.Html.node_filename proc_name nodeid in
-    let needs_initialization, (fd, fmt) =
+    let needs_initialization, (fd, fmt_key) =
       let node_path = ["nodes"; node_fname] in
       let modified = Io_infer.Html.modified_during_analysis source node_path in
       if modified then (false, Io_infer.Html.open_out source node_path)
       else (true, Io_infer.Html.create source node_path)
     in
-    curr_html_formatter := fmt ;
+    let fmt = DLS.get fmt_key in
+    DLS.set curr_html_formatter fmt ;
     Hashtbl.add log_files (node_fname, source) fd ;
     if needs_initialization then (
       F.fprintf fmt "<center><h1>Cfg Node %a</h1></center>"
@@ -114,7 +115,7 @@ end = struct
 
 
   let finish_session node =
-    F.fprintf !curr_html_formatter "</div>@?" ;
+    F.fprintf (DLS.get curr_html_formatter) "</div>@?" ;
     let source = (Procdesc.Node.get_loc node).file in
     let node_fname =
       let proc_name = Procdesc.Node.get_proc_name node in
@@ -124,7 +125,7 @@ end = struct
     let fd = Hashtbl.find log_files (node_fname, source) in
     Unix.close fd ;
     Hashtbl.remove log_files (node_fname, source) ;
-    curr_html_formatter := F.std_formatter
+    DLS.set curr_html_formatter (F.get_std_formatter ())
 end
 
 module ProcsHtml : sig
@@ -136,7 +137,8 @@ end = struct
     let source = loc.file in
     let nodes = List.sort ~compare:Procdesc.Node.compare (Procdesc.get_nodes pdesc) in
     let linenum = loc.Location.line in
-    let fd, fmt = Io_infer.Html.create source [Procname.to_filename proc_name] in
+    let fd, fmt_key = Io_infer.Html.create source [Procname.to_filename proc_name] in
+    let fmt = DLS.get fmt_key in
     F.fprintf fmt "<center><h1>Procedure %a</h1></center>@\n"
       (Io_infer.Html.pp_line_link source
          ~text:(Some (Escape.escape_xml (Procname.to_string ~verbosity:Verbose proc_name)))
@@ -164,7 +166,7 @@ end = struct
       (Escape.escape_xml (F.asprintf "%a" ProcAttributes.pp (Procdesc.get_attributes pdesc)))
       Sexp.pp_hum
       (SpecializedProcname.sexp_of_t {proc_name; specialization= None}) ;
-    Io_infer.Html.close (fd, fmt)
+    Io_infer.Html.close (fd, fmt_key)
 end
 
 module FilesHtml : sig
@@ -215,7 +217,8 @@ end = struct
 
   let write_html_file filename procs =
     let fname_encoding = DB.source_file_encoding filename in
-    let fd, fmt = Io_infer.Html.create filename [".."; fname_encoding] in
+    let fd, fmt_key = Io_infer.Html.create filename [".."; fname_encoding] in
+    let fmt = DLS.get fmt_key in
     F.fprintf fmt "<center><h1>File %a </h1></center>@\n<table class=\"code\">@\n" SourceFile.pp
       filename ;
     let global_err_log = Errlog.empty () in
@@ -258,7 +261,7 @@ end = struct
     LineReader.iteri linereader filename ~f:print_one_line ;
     F.fprintf fmt "</table>@\n" ;
     Errlog.pp_html filename [fname_encoding] fmt global_err_log ;
-    Io_infer.Html.close (fd, fmt)
+    Io_infer.Html.close (fd, fmt_key)
 
 
   let is_allow_listed =
@@ -327,10 +330,10 @@ end
 
 (** Execute the delayed print actions *)
 let force_delayed_prints () =
-  F.pp_print_flush !curr_html_formatter () ;
+  F.pp_print_flush (DLS.get curr_html_formatter) () ;
   (* flush html stream *)
-  L.force_and_reset_delayed_prints !curr_html_formatter ;
-  F.pp_print_flush !curr_html_formatter ()
+  L.force_and_reset_delayed_prints (DLS.get curr_html_formatter) ;
+  F.pp_print_flush (DLS.get curr_html_formatter) ()
 
 
 (** Start a session, and create a new html file for the node if it does not exist yet *)

infer/src/base/Logging.ml

@@ -95,7 +95,7 @@ let mk_file_formatter file_fmt category0 =
 
 let color_console ?(use_stdout = false) scheme =
   let scheme = Option.value scheme ~default:Normal in
-  let formatter = if use_stdout then F.std_formatter else F.err_formatter in
+  let formatter = if use_stdout then F.get_std_formatter () else F.get_err_formatter () in
   let can_colorize = Unix.(isatty (if use_stdout then stdout else stderr)) in
   if can_colorize then
     let styles = term_styles_of_style scheme in
@@ -183,15 +183,15 @@ let () = register_epilogue ()
 let log ~to_console ?(to_file = true) (lazy formatters) =
   match (to_console, to_file) with
   | false, false ->
-      F.ifprintf F.std_formatter
+      F.ifprintf (F.get_std_formatter ())
   | true, _ when not Config.print_logs ->
       F.fprintf !formatters.console_file
   | _ ->
       (* to_console might be true, but in that case so is Config.print_logs so do not print to
          stderr because it will get logs from the log file already *)
       Option.value_map !formatters.file
         ~f:(fun file_fmt -> F.fprintf file_fmt)
-        ~default:(F.fprintf F.err_formatter)
+        ~default:(F.fprintf (F.get_err_formatter ()))
 
 
 let debug_file_fmts = register_formatter "debug"
@@ -357,7 +357,7 @@ let setup_log_file () =
         let chan = Stdlib.open_out_gen [Open_append; Open_creat] 0o666 logfile_path in
         let file_fmt =
           let f = F.formatter_of_out_channel chan in
-          if Config.print_logs then dup_formatter f F.err_formatter else f
+          if Config.print_logs then dup_formatter f (F.get_err_formatter ()) else f
         in
         (file_fmt, chan, preexisting_logfile)
       in
@@ -426,7 +426,7 @@ let d_kfprintf ?color k f fmt =
       F.kfprintf k f fmt
 
 
-let d_iprintf fmt = Format.ikfprintf ignore Format.err_formatter fmt
+let d_iprintf fmt = Format.ikfprintf ignore (F.get_err_formatter ()) fmt
 
 let d_kprintf ?color k fmt =
   match get_f () with Some f -> d_kfprintf ?color k f fmt | None -> d_iprintf fmt
@@ -491,7 +491,7 @@ let d_increase_indent () = d_printf "  @["
 let d_decrease_indent () = d_printf "@]"
 
 let with_indent ?name_color ?(collapsible = false) ?(escape_result = true) ?pp_result ~f name_fmt =
-  if not Config.write_html then F.ikfprintf (fun _ -> f ()) Format.std_formatter name_fmt
+  if not Config.write_html then F.ikfprintf (fun _ -> f ()) (F.get_std_formatter ()) name_fmt
   else
     let print_block name =
       let block_tag, name_tag = if collapsible then ("details", "summary") else ("div", "div") in

infer/src/bufferoverrun/absLoc.ml

@@ -182,7 +182,7 @@ module Loc = struct
     let module SP = Symb.SymbolPath in
     function
     | BoField.Prim (Var v) ->
-        Var.pp F.str_formatter v ;
+        Var.pp (F.get_str_formatter ()) v ;
         let s = F.flush_str_formatter () in
         if Char.equal s.[0] '&' then
           F.pp_print_string fmt (String.sub s ~pos:1 ~len:(String.length s - 1))

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1003,11 +1003,12 @@ module Internal = struct
           Union_find.same_class aa bb
         in
         if Bool.(equal_in_subst <> equal_in_uf) then (
-          F.fprintf F.str_formatter "@[<v>" ;
+          let str_formatter = F.get_str_formatter () in
+          F.fprintf str_formatter "@[<v>" ;
           List.iter eqs ~f:(function x, y ->
-              F.fprintf F.str_formatter "@[%a -> %a@]@;" V.pp x V.pp y ) ;
-          F.fprintf F.str_formatter "@[See values %a %a: equal_in_subst=%b equal_in_uf=%b@]@;@]"
-            V.pp a V.pp b equal_in_subst equal_in_uf ;
+              F.fprintf str_formatter "@[%a -> %a@]@;" V.pp x V.pp y ) ;
+          F.fprintf str_formatter "@[See values %a %a: equal_in_subst=%b equal_in_uf=%b@]@;@]" V.pp
+            a V.pp b equal_in_subst equal_in_uf ;
           L.die InternalError "%s" (F.flush_str_formatter ()) ) )
 
 

infer/src/pulse/PulseTopl.ml

@@ -1008,9 +1008,9 @@ let filter_for_summary pulse_state state = drop_infeasible pulse_state state
 let description_of_step_data step_data =
   ( match step_data with
   | SmallStep (Call {procname}) | LargeStep {procname} ->
-      F.fprintf F.str_formatter "@[call to %a@]" Procname.pp_verbose procname
+      F.fprintf (F.get_str_formatter ()) "@[call to %a@]" Procname.pp_verbose procname
   | SmallStep (ArrayWrite _) ->
-      F.fprintf F.str_formatter "@[write to array@]" ) ;
+      F.fprintf (F.get_str_formatter ()) "@[write to array@]" ) ;
   F.flush_str_formatter ()