Merge pull request #931 from goblint/backtrace-marking

Add custom location marks to exception backtraces

Author: sim642

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint mainspec privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.

src/framework/constraints.ml

@@ -687,12 +687,20 @@ struct
       | Skip           -> tf_skip var edge prev_node
     end getl sidel getg sideg d
 
+  type Goblint_backtrace.mark += TfLocation of location
+
+  let () = Goblint_backtrace.register_mark_printer (function
+      | TfLocation loc ->
+        Some ("transfer function at " ^ CilType.Location.show loc)
+      | _ -> None (* for other marks *)
+    )
+
   let tf var getl sidel getg sideg prev_node (_,edge) d (f,t) =
     let old_loc  = !Tracing.current_loc in
     let old_loc2 = !Tracing.next_loc in
     Tracing.current_loc := f;
     Tracing.next_loc := t;
-    Fun.protect ~finally:(fun () ->
+    Goblint_backtrace.protect ~mark:(fun () -> TfLocation f) ~finally:(fun () ->
         Tracing.current_loc := old_loc;
         Tracing.next_loc := old_loc2
       ) (fun () ->

src/framework/control.ml

@@ -299,7 +299,9 @@ struct
       in
       let with_externs = do_extern_inits ctx file in
       (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges);    *)
+      let old_loc = !Tracing.current_loc in
       let result : Spec.D.t = List.fold_left transfer_func with_externs edges in
+      Tracing.current_loc := old_loc;
       if M.tracing then M.trace "global_inits" "startstate: %a\n" Spec.D.pretty result;
       result, !funs
     in

src/maingoblint.ml

@@ -461,8 +461,11 @@ let do_analyze change_info merged_AST =
       with e ->
         let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *)
         Goblintutil.should_warn := true; (* such that the `about to crash` message gets printed *)
-        let loc = !Tracing.current_loc in
-        Messages.error ~category:Analyzer ~loc:(Messages.Location.CilLocation loc) "About to crash!";
+        let pretty_mark () = match Goblint_backtrace.find_marks e with
+          | m :: _ -> Pretty.dprintf " at mark %s" (Goblint_backtrace.mark_to_string m)
+          | [] -> Pretty.nil
+        in
+        Messages.error ~category:Analyzer "About to crash%t!" pretty_mark;
         (* trigger Generic.SolverStats...print_stats *)
         Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal")));
         do_stats ();

src/util/backtrace/dune

@@ -0,0 +1,5 @@
+(include_subdirs no)
+
+(library
+ (name goblint_backtrace)
+ (public_name goblint.backtrace))

src/util/backtrace/goblint_backtrace.ml

@@ -0,0 +1,78 @@
+type mark = ..
+
+module Exn =
+struct
+  type t = exn
+  let equal = (==)
+  let hash = Hashtbl.hash
+end
+
+module EWH = Ephemeron.K1.Make (Exn)
+
+let marks: mark EWH.t = EWH.create 10
+
+let add_mark e m =
+  EWH.add marks e m
+
+
+(* Copied & modified from Fun. *)
+let protect ~(mark: unit -> mark) ~(finally: unit -> unit) work =
+  let finally_no_exn () =
+    try
+      finally ()
+    with e ->
+      let bt = Printexc.get_raw_backtrace () in
+      let finally_exn = Fun.Finally_raised e in
+      add_mark finally_exn (mark ());
+      Printexc.raise_with_backtrace finally_exn bt
+  in
+  match work () with
+  | result ->
+    finally_no_exn ();
+    result
+  | exception work_exn ->
+    let work_bt = Printexc.get_raw_backtrace () in
+    finally_no_exn ();
+    add_mark work_exn (mark ());
+    Printexc.raise_with_backtrace work_exn work_bt
+
+
+let mark_printers: (mark -> string option) list ref = ref []
+
+let register_mark_printer f =
+  mark_printers := f :: !mark_printers
+
+let apply_mark_printers m =
+  List.find_map (fun f ->
+      match f m with
+      | Some s -> Some s
+      | None
+      | exception _ -> None
+    ) !mark_printers
+
+let mark_to_string_default m =
+  Obj.Extension_constructor.(name (of_val m))
+
+let mark_to_string m =
+  match apply_mark_printers m with
+  | Some s -> s
+  | None -> mark_to_string_default m
+
+let find_marks e =
+  List.rev (EWH.find_all marks e)
+
+let print_marktrace oc e =
+  let ms = find_marks e in
+  List.iter (fun m ->
+      Printf.fprintf oc "Marked with %s\n" (mark_to_string m)
+    ) ms
+
+let () =
+  Printexc.set_uncaught_exception_handler (fun e bt ->
+      (* Copied & modified from Printexc.default_uncaught_exception_handler. *)
+      Printf.eprintf "Fatal error: exception %s\n" (Printexc.to_string e);
+      if Printexc.backtrace_status () then
+        print_marktrace stderr e;
+      Printexc.print_raw_backtrace stderr bt;
+      flush stderr
+    )

src/util/backtrace/goblint_backtrace.mli

@@ -0,0 +1,33 @@
+(** Backtraces with custom marks. *)
+
+(** {2 Mark definition} *)
+
+type mark = ..
+(** Extensible type of marks. *)
+
+val register_mark_printer: (mark -> string option) -> unit
+(** Register printing function for custom mark.
+    The function should return [None] for other marks. *)
+
+val mark_to_string: mark -> string
+(** Convert mark to string using registered printers, or {!mark_to_string_default} if unhandled. *)
+
+val mark_to_string_default: mark -> string
+(** Convert mark to default string. *)
+
+
+(** {2 Mark usage} *)
+
+val add_mark: exn -> mark -> unit
+(** Add mark to exception. *)
+
+val protect: mark:(unit -> mark) -> finally:(unit -> unit) -> (unit -> 'a) -> 'a
+(** {!Fun.protect} with additional [~mark] addition to all exceptions. *)
+
+val print_marktrace: out_channel -> exn -> unit
+(** Print trace of marks of an exception.
+
+    Used by default for uncaught exceptions. *)
+
+val find_marks: exn -> mark list
+(** Find all marks of an exception. *)