<commit_before>(* This file is part of the Kind 2 model checker.

   Copyright (c) 2015 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   http://www.apache.org/licenses/LICENSE-2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)

open Lib

(*

module Dummy =
struct
  let main _ = failwith "not implemented"
  let on_exit _ = ()
end
*)

module BMC = Base
module IND = Step
module IND2 = Step2
module InvGenTS = InvGenGraph.TwoState
module InvGenOS = InvGenGraph.OneState
module TestGen = TestgenDF
module C2I = C2I
module C2Icnf = C2Icnf

(* module IC3 = Dummy *)

let children_pgid = ref 0

(* Child processes forked

   This is an association list of PID to process type. We need a
   reference here, because we may need to terminate asynchronously
   after an exception. *)
let child_pids = ref []

(* Input system. *)
let input_sys_ref = ref None
(* Current input system. *)
let cur_input_sys = ref None
(* Current analysis params. *)
let cur_aparam = ref None
(* Current transition system. *)
let cur_trans_sys = ref None

(* Generic signal handler. *)
let generic_sig_handler = Sys.Signal_handle exception_on_signal
(* Installs a generic signal handler for a signal. *)
let set_generic_handler_for s =
  Sys.set_signal s generic_sig_handler

(* Installs the relevant handler for sigalrm:
   - default if no timeout, or
   - [timeout] - [Stat.total_time] if there is one.
   Raises [TimeoutWall] if [timeout] < [Stat.total_time]. *)
let set_sigalrm_handler () =
  match Flags.timeout_wall () with

  | timeout when timeout > 0. ->

    (* Retrieving total time. *)
    let elapsed = Stat.get_float Stat.total_time in

    if timeout < elapsed then raise TimeoutWall else (

      (* Install signal handler for SIGALRM after wallclock timeout. *)
      Sys.set_signal Sys.sigalrm (Sys.Signal_handle
        (fun _ -> raise TimeoutWall)
      ) ;
      (* Set interval timer for wallclock timeout. *)
      Unix.setitimer Unix.ITIMER_REAL {
          Unix.it_interval = 0. ; Unix.it_value = timeout -. elapsed
      } |> ignore

    )

  | _ ->
    (* No timeout. *)
    let _ (* { Unix.it_interval = i; Unix.it_value = v } *) =
      Unix.setitimer
        Unix.ITIMER_REAL
        { Unix.it_interval = 0.; Unix.it_value = 0. }
    in
    (* Install generic signal handler for SIGALRM. *)
    set_generic_handler_for Sys.sigalrm

(* Renices the current process. Used for invariant generation. *)
let renice () =
  let nice =  (Flags.Invgen.renice ()) in

  if nice < 0 then
    Event.log L_info
      "Ignoring negative niceness value for invariant generation."

  else if nice > 0 then
    let nice' = Unix.nice nice in
    Event.log L_info "Renicing invariant generation to %d" nice'

(* Main function of the process *)
let main_of_process = function
  | `IC3 -> IC3.main
  | `BMC -> BMC.main
  | `IND -> IND.main
  | `IND2 -> IND2.main
  | `INVGEN -> renice () ; InvGenTS.main
  | `INVGENOS -> renice () ; InvGenOS.main
  | `C2I -> renice () ; C2I.main
  | `Interpreter -> Interpreter.main (Flags.Interpreter.input_file ())
  | `Supervisor -> InvarManager.main child_pids
  | `Parser -> (fun _ _ _ -> ())

(* Cleanup function of the process *)
let on_exit_of_process = function
  | `IC3 -> IC3.on_exit
  | `BMC -> BMC.on_exit
  | `IND -> IND.on_exit
  | `IND2 -> IND2.on_exit
  | `INVGEN -> InvGenTS.on_exit
  | `INVGENOS -> InvGenOS.on_exit
  | `C2I -> C2I.on_exit
  | `Interpreter -> Interpreter.on_exit
  | `Supervisor -> InvarManager.on_exit
  | `Parser -> ignore

(*
(* Messaging type of the process *)
let init_messaging_of_process = function 
  | `IC3 -> Kind2Message.init_ic3
  | `BMC -> Kind2Message.init_bmc
  | `IND -> Kind2Message.init_indStep
  | `INVGEN -> Kind2Message.init_invarGen 
  | `Supervisor -> Kind2Message.init_invarManager (List.map fst !child_pids)
*)


let debug_ext_of_process = function
  | `IC3 -> "ic3"
  | `BMC -> "bmc"
  | `IND -> "ind"
  | `IND2 -> "ind2"
  | `INVGEN -> "invgenTS"
  | `INVGENOS -> "invgenOS"
  | `C2I -> "c2i"
  | `Interpreter -> "interp"
  | `Parser -> "parser"
  | `Supervisor -> "super"

(* Exit status if timeout *)
let status_timeout = 0
(* Exit status if one property is falsifiable. *)
let status_unsafe = 10
(* Exit status if all properties are valid. *)
let status_safe = 20

(* Decides what the exit status is by looking at a transition system.

   The exit status is
   * 0 if some properties are unknown or k-true (timeout),
   * 10 if some properties are falsifiable (unsafe),
   * 20 if all properties are invariants (safe). *)
let status_of_trans_sys sys =
  (* Checking if some properties are unknown of falsifiable. *)
  let unknown, falsifiable =
    TransSys.get_prop_status_all sys
    |> List.fold_left (fun (u,f) -> function
      | (_, Property.PropUnknown)
      | (_, Property.PropKTrue _) -> u+1,f
      | (_, Property.PropFalse _) -> u,f+1
      | _ -> u,f
    ) (0,0)
    |> fun (u,f) -> u > 0, f > 0
  in
  (* Getting relevant exit code. *)
  let exit_status =
    if unknown then status_timeout
    else if falsifiable then status_unsafe
    else status_safe
  in
  (* Exit status. *)
  exit_status

(* Exit status if child caught a signal, the signal number is added to
   the value *)
let status_signal = 128

(* Exit status if child raised an exception *)
let status_error = 2

(* Exit status from an optional [results]. *)
let status_of_sys sys_opt = match sys_opt with
| None -> status_timeout
| Some sys -> status_of_trans_sys sys

(* Exit status from an optional [results]. *)
let status_of_results results_opt = match results_opt with
| None -> status_timeout
| Some results -> (
  match Analysis.results_is_safe results with
  | None -> status_timeout
  | Some true -> status_safe
  | Some false -> status_unsafe
)

(* Return the status code from an exception *)
let status_of_exn process status = function
  (* Normal termination *)
  | Exit -> status

  (* Got unknown, issue error but normal termination. *)
  | SMTSolver.Unknown ->
    Event.log L_error
      "In %a: a check-sat resulted in \"unknown\", exiting."
      pp_print_kind_module process ;
    status

  (* Termination message *)
  | Event.Terminate -> (

    Event.log L_debug
      "Received termination message" ;

    status

  ) 

  (* Catch wallclock timeout *)
  | TimeoutWall -> (

    Event.log_timeout true ;

    status

  ) 

  (* Catch CPU timeout *)
  | TimeoutVirtual -> (

    Event.log_timeout false ;

    status

  ) 

  (* Signal caught *)
  | Signal s -> (

    Event.log_interruption s ;

    (* Return exit status and signal number *)
    status_signal + s

  )
    
  (* Other exception, return exit status for error. *)
  | e ->
    Event.log L_fatal
      "Runtime error in %a: %s"
      pp_print_kind_module process
      (Printexc.to_string e) ;
    status_error

let status_of_exn_sys process sys_opt =
  status_of_exn process (status_of_sys sys_opt)

let status_of_exn_results process results_opt =
  status_of_exn process (status_of_results results_opt)

(* Kill all kids cleanly. *)
let slaughter_kids process sys =

  (* Ignore SIGALRM from now on *)
  Sys.set_signal Sys.sigalrm Sys.Signal_ignore ;

  (* Clean exit from invariant manager *)
  InvarManager.on_exit sys ;

  Event.log L_info "Killing all remaining child processes" ;

  (* Kill all child processes *)
  List.iter
    (function pid, _ ->

      Event.log L_debug "Sending SIGTERM to PID %d" pid ;

      Unix.kill pid Sys.sigterm)

    !child_pids ;

  Event.log L_debug
    "Waiting for remaining child processes to terminate" ;

  ( try

    (* Install signal handler for SIGALRM after wallclock timeout *)
    Sys.set_signal
      Sys.sigalrm
      (Sys.Signal_handle (function _ -> raise TimeoutWall)) ;

    (* Set interval timer for wallclock timeout. Used to detect we have been
       waiting for kids to die for too long. *)
    let _ (* { Unix.it_interval = i; Unix.it_value = v } *) =
      Unix.setitimer
        Unix.ITIMER_REAL
        { Unix.it_interval = 0.; Unix.it_value = 1. }
    in

    (try

       while true do

         (* Wait for child process to terminate *)
         let pid, status = Unix.wait () in

         (* Kill processes left in process group of child process *)
         (try Unix.kill (- pid) Sys.sigkill with _ -> ()) ;

         (* Remove killed process from list *)
         child_pids := List.remove_assoc pid !child_pids ;

         (* Log termination status *)
         Event.log L_debug
           "Process %d %a" pid pp_print_process_status status

       done

     with TimeoutWall -> ()) ;

  with

    (* No more child processes, this is the normal exit *)
    | Unix.Unix_error (Unix.ECHILD, _, _) ->

      Event.log L_info
        "All child processes terminated." ;

    (* Unix.wait was interrupted *)
    | Unix.Unix_error (Unix.EINTR, _, _) ->

      (* Ignoring exit code, whatever happened does not change the
         outcome of the analysis. *)
      status_of_exn_sys process None (Signal 0) |> ignore

    (* Exception in Unix.wait loop *)
    | e ->

      (* Ignoring exit code, whatever happened does not change the
         outcome of the analysis. *)
      status_of_exn_sys process None e |> ignore ) ;

  (* Deactivate timeout. *)
  let _ (* { Unix.it_interval = i; Unix.it_value = v } *) =
    Unix.setitimer
      Unix.ITIMER_REAL
      { Unix.it_interval = 0.; Unix.it_value = 0. }
  in
  (* Install generic signal handler for SIGALRM. *)
  set_generic_handler_for Sys.sigalrm ;

  (* Log termination status *)
  ( try
    ( match !child_pids with
      | [] -> ()
      | kids ->

        kids |> Event.log L_debug
          "Some processes (%a) did not exit, killing them." (
            pp_print_list (fun ppf (pid, _) ->
              Format.pp_print_int ppf pid
            ) ",@ "
          ) ;

        (* Kill all remaining processes in the process groups of child
           processes *)
        kids |> List.iter (fun (pid, _) ->
          try
            Unix.kill (- pid) Sys.sigkill
          with _ -> ()
        ) ;

        (* Waiting for all kids to be actually done. *)
        kids |> List.iter (fun _ -> Unix.wait () |> ignore) )
    with

      (* No more child processes, this is the normal exit *)
      | Unix.Unix_error (Unix.ECHILD, _, _) ->

        Event.log L_info
          "All child processes terminated." ) ;

  (* Cleaning kids list. *)
  child_pids := [] ;

  (* Draining mailbox. *)
  Event.recv () |> ignore ;

  (* Restore sigalrm handler for next analysis if any. *)
  set_sigalrm_handler ()



(* Called after everything has been cleaned up. All kids dead etc. *)
let clean_exit process results exn =

  (* Exit status of process depends on exception *)
  let status = status_of_exn_results process results exn in

  (* Close tags in XML output *)
  Event.terminate_log () ;

  (* Exit with status *)
  exit status

(* Clean up before exit *)
let on_exit process results exn =

(*
  let pp_print_hashcons_stat ppf (l, c, t, s, m, g) =

    Format.fprintf
      ppf
      "Number of buckets: %d@,\
       Number of entries in table: %d@,\
       Sum of sizes of buckets: %d@,\
       Size of smallest bucket: %d@,\
       Median bucket size: %d@,\
       Size of greatest bucket: %d@,"
      l
      c
      t
      s
      m
      g

  in

  Event.log L_info
    "@[<hv>Hashconsing for state variables:@,%a@]"
    pp_print_hashcons_stat (StateVar.stats ());

  Event.log L_info
    "@[<hv>Hashconsing for variables:@,%a@]"
    pp_print_hashcons_stat (Var.stats ());

  Event.log L_info
    "@[<hv>Hashconsing for terms:@,%a@]"
    pp_print_hashcons_stat (Term.stats ());

  Event.log L_info
    "@[<hv>Hashconsing for symbols:@,%a@]"
    pp_print_hashcons_stat (Symbol.stats ());
*)

  (* Killing kids. *)
  try
    slaughter_kids process (!cur_trans_sys)
  with
    (* We're past the timeout, but we're exiting anyways. *)
    TimeoutWall -> () ;

  (* Exiting. *)
  clean_exit process None exn


(* Call cleanup function of process and exit.

   Give the exception [exn] that was raised or [Exit] on normal
   termination. *)
let on_exit_child messaging_thread process exn =

  (* Exit status of process depends on exception *)
  let status = status_of_exn process 0 exn in

  (* Call cleanup of process *)
  (on_exit_of_process process) !cur_trans_sys ;

  Event.log L_debug
    "Process %d terminating"
    (Unix.getpid ()) ;

  Event.terminate_log () ;

  ( match messaging_thread with
    | Some t -> Event.exit t
    | None -> () ) ;

  ( debug kind2
      "Process %a terminating"
      pp_print_kind_module process
    in

    (* Exit process with status *)
    exit status )



(* Fork and run a child process *)
let run_process messaging_setup process =

  (* Fork a new process *)
  let pid = Unix.fork () in

  match pid with

    (* We are the child process *)
    | 0 -> (

        (* Make the process leader of a new session *)
        ignore (Unix.setsid ());
<commit_msg>don't close log on technique crash, fixes #385<commit_after>(* This file is part of the Kind 2 model checker.

   Copyright (c) 2015 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   http://www.apache.org/licenses/LICENSE-2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)

open Lib

(*

module Dummy =
struct
  let main _ = failwith "not implemented"
  let on_exit _ = ()
end
*)

module BMC = Base
module IND = Step
module IND2 = Step2
module InvGenTS = InvGenGraph.TwoState
module InvGenOS = InvGenGraph.OneState
module TestGen = TestgenDF
module C2I = C2I
module C2Icnf = C2Icnf

(* module IC3 = Dummy *)

let children_pgid = ref 0

(* Child processes forked

   This is an association list of PID to process type. We need a
   reference here, because we may need to terminate asynchronously
   after an exception. *)
let child_pids = ref []

(* Input system. *)
let input_sys_ref = ref None
(* Current input system. *)
let cur_input_sys = ref None
(* Current analysis params. *)
let cur_aparam = ref None
(* Current transition system. *)
let cur_trans_sys = ref None

(* Generic signal handler. *)
let generic_sig_handler = Sys.Signal_handle exception_on_signal
(* Installs a generic signal handler for a signal. *)
let set_generic_handler_for s =
  Sys.set_signal s generic_sig_handler

(* Installs the relevant handler for sigalrm:
   - default if no timeout, or
   - [timeout] - [Stat.total_time] if there is one.
   Raises [TimeoutWall] if [timeout] < [Stat.total_time]. *)
let set_sigalrm_handler () =
  match Flags.timeout_wall () with

  | timeout when timeout > 0. ->

    (* Retrieving total time. *)
    let elapsed = Stat.get_float Stat.total_time in

    if timeout < elapsed then raise TimeoutWall else (

      (* Install signal handler for SIGALRM after wallclock timeout. *)
      Sys.set_signal Sys.sigalrm (Sys.Signal_handle
        (fun _ -> raise TimeoutWall)
      ) ;
      (* Set interval timer for wallclock timeout. *)
      Unix.setitimer Unix.ITIMER_REAL {
          Unix.it_interval = 0. ; Unix.it_value = timeout -. elapsed
      } |> ignore

    )

  | _ ->
    (* No timeout. *)
    let _ (* { Unix.it_interval = i; Unix.it_value = v } *) =
      Unix.setitimer
        Unix.ITIMER_REAL
        { Unix.it_interval = 0.; Unix.it_value = 0. }
    in
    (* Install generic signal handler for SIGALRM. *)
    set_generic_handler_for Sys.sigalrm

(* Renices the current process. Used for invariant generation. *)
let renice () =
  let nice =  (Flags.Invgen.renice ()) in

  if nice < 0 then
    Event.log L_info
      "Ignoring negative niceness value for invariant generation."

  else if nice > 0 then
    let nice' = Unix.nice nice in
    Event.log L_info "Renicing invariant generation to %d" nice'

(* Main function of the process *)
let main_of_process = function
  | `IC3 -> IC3.main
  | `BMC -> BMC.main
  | `IND -> IND.main
  | `IND2 -> IND2.main
  | `INVGEN -> renice () ; InvGenTS.main
  | `INVGENOS -> renice () ; InvGenOS.main
  | `C2I -> renice () ; C2I.main
  | `Interpreter -> Interpreter.main (Flags.Interpreter.input_file ())
  | `Supervisor -> InvarManager.main child_pids
  | `Parser -> (fun _ _ _ -> ())

(* Cleanup function of the process *)
let on_exit_of_process = function
  | `IC3 -> IC3.on_exit
  | `BMC -> BMC.on_exit
  | `IND -> IND.on_exit
  | `IND2 -> IND2.on_exit
  | `INVGEN -> InvGenTS.on_exit
  | `INVGENOS -> InvGenOS.on_exit
  | `C2I -> C2I.on_exit
  | `Interpreter -> Interpreter.on_exit
  | `Supervisor -> InvarManager.on_exit
  | `Parser -> ignore

(*
(* Messaging type of the process *)
let init_messaging_of_process = function 
  | `IC3 -> Kind2Message.init_ic3
  | `BMC -> Kind2Message.init_bmc
  | `IND -> Kind2Message.init_indStep
  | `INVGEN -> Kind2Message.init_invarGen 
  | `Supervisor -> Kind2Message.init_invarManager (List.map fst !child_pids)
*)


let debug_ext_of_process = function
  | `IC3 -> "ic3"
  | `BMC -> "bmc"
  | `IND -> "ind"
  | `IND2 -> "ind2"
  | `INVGEN -> "invgenTS"
  | `INVGENOS -> "invgenOS"
  | `C2I -> "c2i"
  | `Interpreter -> "interp"
  | `Parser -> "parser"
  | `Supervisor -> "super"

(* Exit status if timeout *)
let status_timeout = 0
(* Exit status if one property is falsifiable. *)
let status_unsafe = 10
(* Exit status if all properties are valid. *)
let status_safe = 20

(* Decides what the exit status is by looking at a transition system.

   The exit status is
   * 0 if some properties are unknown or k-true (timeout),
   * 10 if some properties are falsifiable (unsafe),
   * 20 if all properties are invariants (safe). *)
let status_of_trans_sys sys =
  (* Checking if some properties are unknown of falsifiable. *)
  let unknown, falsifiable =
    TransSys.get_prop_status_all sys
    |> List.fold_left (fun (u,f) -> function
      | (_, Property.PropUnknown)
      | (_, Property.PropKTrue _) -> u+1,f
      | (_, Property.PropFalse _) -> u,f+1
      | _ -> u,f
    ) (0,0)
    |> fun (u,f) -> u > 0, f > 0
  in
  (* Getting relevant exit code. *)
  let exit_status =
    if unknown then status_timeout
    else if falsifiable then status_unsafe
    else status_safe
  in
  (* Exit status. *)
  exit_status

(* Exit status if child caught a signal, the signal number is added to
   the value *)
let status_signal = 128

(* Exit status if child raised an exception *)
let status_error = 2

(* Exit status from an optional [results]. *)
let status_of_sys sys_opt = match sys_opt with
| None -> status_timeout
| Some sys -> status_of_trans_sys sys

(* Exit status from an optional [results]. *)
let status_of_results results_opt = match results_opt with
| None -> status_timeout
| Some results -> (
  match Analysis.results_is_safe results with
  | None -> status_timeout
  | Some true -> status_safe
  | Some false -> status_unsafe
)

(* Return the status code from an exception *)
let status_of_exn process status = function
  (* Normal termination *)
  | Exit -> status

  (* Got unknown, issue error but normal termination. *)
  | SMTSolver.Unknown ->
    Event.log L_error
      "In %a: a check-sat resulted in \"unknown\", exiting."
      pp_print_kind_module process ;
    status

  (* Termination message *)
  | Event.Terminate -> (

    Event.log L_debug
      "Received termination message" ;

    status

  ) 

  (* Catch wallclock timeout *)
  | TimeoutWall -> (

    Event.log_timeout true ;

    status

  ) 

  (* Catch CPU timeout *)
  | TimeoutVirtual -> (

    Event.log_timeout false ;

    status

  ) 

  (* Signal caught *)
  | Signal s -> (

    Event.log_interruption s ;

    (* Return exit status and signal number *)
    status_signal + s

  )
    
  (* Other exception, return exit status for error. *)
  | e ->
    Event.log L_fatal
      "Runtime error in %a: %s"
      pp_print_kind_module process
      (Printexc.to_string e) ;
    status_error

let status_of_exn_sys process sys_opt =
  status_of_exn process (status_of_sys sys_opt)

let status_of_exn_results process results_opt =
  status_of_exn process (status_of_results results_opt)

(* Kill all kids cleanly. *)
let slaughter_kids process sys =

  (* Ignore SIGALRM from now on *)
  Sys.set_signal Sys.sigalrm Sys.Signal_ignore ;

  (* Clean exit from invariant manager *)
  InvarManager.on_exit sys ;

  Event.log L_info "Killing all remaining child processes" ;

  (* Kill all child processes *)
  List.iter
    (function pid, _ ->

      Event.log L_debug "Sending SIGTERM to PID %d" pid ;

      Unix.kill pid Sys.sigterm)

    !child_pids ;

  Event.log L_debug
    "Waiting for remaining child processes to terminate" ;

  ( try

    (* Install signal handler for SIGALRM after wallclock timeout *)
    Sys.set_signal
      Sys.sigalrm
      (Sys.Signal_handle (function _ -> raise TimeoutWall)) ;

    (* Set interval timer for wallclock timeout. Used to detect we have been
       waiting for kids to die for too long. *)
    let _ (* { Unix.it_interval = i; Unix.it_value = v } *) =
      Unix.setitimer
        Unix.ITIMER_REAL
        { Unix.it_interval = 0.; Unix.it_value = 1. }
    in

    (try

       while true do

         (* Wait for child process to terminate *)
         let pid, status = Unix.wait () in

         (* Kill processes left in process group of child process *)
         (try Unix.kill (- pid) Sys.sigkill with _ -> ()) ;

         (* Remove killed process from list *)
         child_pids := List.remove_assoc pid !child_pids ;

         (* Log termination status *)
         Event.log L_debug
           "Process %d %a" pid pp_print_process_status status

       done

     with TimeoutWall -> ()) ;

  with

    (* No more child processes, this is the normal exit *)
    | Unix.Unix_error (Unix.ECHILD, _, _) ->

      Event.log L_info
        "All child processes terminated." ;

    (* Unix.wait was interrupted *)
    | Unix.Unix_error (Unix.EINTR, _, _) ->

      (* Ignoring exit code, whatever happened does not change the
         outcome of the analysis. *)
      status_of_exn_sys process None (Signal 0) |> ignore

    (* Exception in Unix.wait loop *)
    | e ->

      (* Ignoring exit code, whatever happened does not change the
         outcome of the analysis. *)
      status_of_exn_sys process None e |> ignore ) ;

  (* Deactivate timeout. *)
  let _ (* { Unix.it_interval = i; Unix.it_value = v } *) =
    Unix.setitimer
      Unix.ITIMER_REAL
      { Unix.it_interval = 0.; Unix.it_value = 0. }
  in
  (* Install generic signal handler for SIGALRM. *)
  set_generic_handler_for Sys.sigalrm ;

  (* Log termination status *)
  ( try
    ( match !child_pids with
      | [] -> ()
      | kids ->

        kids |> Event.log L_debug
          "Some processes (%a) did not exit, killing them." (
            pp_print_list (fun ppf (pid, _) ->
              Format.pp_print_int ppf pid
            ) ",@ "
          ) ;

        (* Kill all remaining processes in the process groups of child
           processes *)
        kids |> List.iter (fun (pid, _) ->
          try
            Unix.kill (- pid) Sys.sigkill
          with _ -> ()
        ) ;

        (* Waiting for all kids to be actually done. *)
        kids |> List.iter (fun _ -> Unix.wait () |> ignore) )
    with

      (* No more child processes, this is the normal exit *)
      | Unix.Unix_error (Unix.ECHILD, _, _) ->

        Event.log L_info
          "All child processes terminated." ) ;

  (* Cleaning kids list. *)
  child_pids := [] ;

  (* Draining mailbox. *)
  Event.recv () |> ignore ;

  (* Restore sigalrm handler for next analysis if any. *)
  set_sigalrm_handler ()



(* Called after everything has been cleaned up. All kids dead etc. *)
let clean_exit process results exn =

  (* Exit status of process depends on exception *)
  let status = status_of_exn_results process results exn in

  (* Close tags in XML output *)
  Event.terminate_log () ;

  (* Exit with status *)
  exit status

(* Clean up before exit *)
let on_exit process results exn =

(*
  let pp_print_hashcons_stat ppf (l, c, t, s, m, g) =

    Format.fprintf
      ppf
      "Number of buckets: %d@,\
       Number of entries in table: %d@,\
       Sum of sizes of buckets: %d@,\
       Size of smallest bucket: %d@,\
       Median bucket size: %d@,\
       Size of greatest bucket: %d@,"
      l
      c
      t
      s
      m
      g

  in

  Event.log L_info
    "@[<hv>Hashconsing for state variables:@,%a@]"
    pp_print_hashcons_stat (StateVar.stats ());

  Event.log L_info
    "@[<hv>Hashconsing for variables:@,%a@]"
    pp_print_hashcons_stat (Var.stats ());

  Event.log L_info
    "@[<hv>Hashconsing for terms:@,%a@]"
    pp_print_hashcons_stat (Term.stats ());

  Event.log L_info
    "@[<hv>Hashconsing for symbols:@,%a@]"
    pp_print_hashcons_stat (Symbol.stats ());
*)

  (* Killing kids. *)
  try
    slaughter_kids process (!cur_trans_sys)
  with
    (* We're past the timeout, but we're exiting anyways. *)
    TimeoutWall -> () ;

  (* Exiting. *)
  clean_exit process None exn


(* Call cleanup function of process and exit.

   Give the exception [exn] that was raised or [Exit] on normal
   termination. *)
let on_exit_child messaging_thread process exn =

  (* Exit status of process depends on exception *)
  let status = status_of_exn process 0 exn in

  (* Call cleanup of process *)
  (on_exit_of_process process) !cur_trans_sys ;

  Event.log L_debug
    "Process %d terminating"
    (Unix.getpid ()) ;

  ( match messaging_thread with
    | Some t -> Event.exit t
    | None -> () ) ;

  ( debug kind2
      "Process %a terminating"
      pp_print_kind_module process
    in

    (* Exit process with status *)
    exit status )



(* Fork and run a child process *)
let run_process messaging_setup process =

  (* Fork a new process *)
  let pid = Unix.fork () in

  match pid with

    (* We are the child process *)
    | 0 -> (

        (* Make the process leader of a new session *)
        ignore (Unix.setsid ());

{'fraction_non_alphanumeric': 0.10390340845176047, 'fraction_numerical': 0.005811991450748059, 'mean_word_length': 2.6690053652496903, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 191, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1915268', 'n_tokens_mistral': 8840, 'n_tokens_neox': 8380, 'n_words': 2752}