logging.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2023                                                    *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  You can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

let src_autodetect = Logs.Src.create "Autodetect" ~doc:"Prover autodetection"

let src_prover_spec =
  Logs.Src.create "ProverSpec" ~doc:"Prover-tailored specification"

let src_prover_call = Logs.Src.create "ProverCall" ~doc:"Prover call"

let src_interpret_goal =
  Logs.Src.create "InterpretGoal" ~doc:"Goal interpretation"

let src_nier = Logs.Src.create "NIER" ~doc:"Neural Intermediate Representation"
let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"

let all_srcs () =
  [
    src_autodetect;
    src_prover_spec;
    src_prover_call;
    src_interpret_goal;
    src_nier;
    src_stack_trace;
  ]

let is_debug_level src =
  match Logs.Src.level src with Some Debug -> true | _ -> false

let reporter =
  let report src level ~over k msgf =
    let k _ =
      over ();
      k ()
    in
    msgf @@ fun ?header ?tags:_ fmt ->
    let ppf = if level = Logs.App then Fmt.stdout else Fmt.stderr in
    let pp_src fmt src =
      if Logs.Src.equal Logs.default src
      then (if level <> Logs.App then Fmt.pf fmt " ")
      else Fmt.pf fmt "@[{%s}@] " (Logs.Src.name src)
    in
    Format.kfprintf k ppf
      ("%a%a@[" ^^ fmt ^^ "@]@.")
      Logs_fmt.pp_header (level, header) pp_src src
  in
  { Logs.report }

let setup style_renderer level srcs =
  Logs.set_level ~all:true level;
  List.iter (fun src -> Logs.Src.set_level src (Some Debug)) srcs;
  Fmt_tty.setup_std_outputs ?style_renderer ();
  Logs.set_reporter reporter

exception Code_error

let code_error ~src f =
  Logs.err ~src (fun m ->
    let report_with_msg ?header:_ ?tags:_ fmt =
      m
        ("@[<v>" ^^ fmt
       ^^ "@ @[Unrecoverable error:@ please report@ the issue at@ \
           https://git.frama-c.com/pub/caisar/issues@]@]")
    in
    f report_with_msg);
  raise Code_error

exception User_error

let user_error ?loc f =
  (match loc with
  | None -> Logs.err f
  | Some loc ->
    Logs.err (fun m ->
      let report_with_loc ?header:_ ?tags:_ fmt =
        m ("@[%a:@ " ^^ fmt ^^ "@]") Why3.Loc.pp_position loc
      in
      f report_with_loc));
  raise User_error

exception Not_implemented_yet

let not_implemented_yet ?src f =
  Logs.err ?src f;
  Logs.err ?src (fun fmt ->
    fmt
      "Unimplemented feature:@ you may send a@ feature request at@ \
       https://git.frama-c.com/pub/caisar/issues");
  raise Not_implemented_yet

let protect_main f =
  try f () with
  | (User_error | Code_error | Not_implemented_yet)
    when not (is_debug_level src_stack_trace) ->
    ()
  | exn when not (is_debug_level src_stack_trace) ->
    Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)

let () =
  (* We register custom printers for a selection of exceptions otherwise Why3
     will print the related messages as "anomaly: <exception with message>". *)
  Why3.Exn_printer.register (fun fmt exn ->
    match exn with
    | Invalid_argument msg -> Fmt.pf fmt "Invalid argument: %s" msg
    | Failure msg -> Fmt.pf fmt "Failure: %s" msg
    | Sys_error msg -> Fmt.pf fmt "%s" msg
    | _ -> raise exn)