Extract Tracing to goblint_tracing dune library

src/analyses/basePriv.ml

@@ -230,7 +230,7 @@ struct
       CPA.find x st.cpa
   (* let read_global ask getg cpa x =
      let (cpa', v) as r = read_global ask getg cpa x in
-     ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v);
+     ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Goblint_tracing.current_loc (is_unprotected ask x) VD.pretty v);
      r *)
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let cpa' = CPA.add x v st.cpa in
@@ -1665,7 +1665,7 @@ struct
   let read_global ask getg st x =
     let v = Priv.read_global ask getg st x in
     if !AnalysisState.postsolving && !is_dumping then
-      LVH.modify_def (VD.bot ()) (!Tracing.current_loc, x) (VD.join v) lvh;
+      LVH.modify_def (VD.bot ()) (!Goblint_tracing.current_loc, x) (VD.join v) lvh;
     v
 
   let dump () =

src/analyses/extractPthread.ml

@@ -220,7 +220,7 @@ module Tbls = struct
       let make_new_val table k =
         (* TODO: all same key occurrences instead *)
         let line = -5 - all_keys_count table in
-        let loc = { !Tracing.current_loc with line } in
+        let loc = { !Goblint_tracing.current_loc with line } in
         MyCFG.Statement
           { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, loc)) with
             sid = new_sid ()

src/analyses/stackTrace.ml

@@ -36,7 +36,7 @@ struct
   (* transfer functions *)
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [ctx.local, D.push !Tracing.current_loc ctx.local]
+    [ctx.local, D.push !Goblint_tracing.current_loc ctx.local]
 
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
@@ -46,7 +46,7 @@ struct
   let exitstate  v = D.top ()
 
   let threadenter ctx ~multiple lval f args =
-    [D.push !Tracing.current_loc ctx.local]
+    [D.push !Goblint_tracing.current_loc ctx.local]
 end
 
 

src/cdomains/valueDomain.ml

@@ -502,7 +502,7 @@ struct
 
   let warn_type op x y =
     if GobConfig.get_bool "dbg.verbose" then
-      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
+      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y
 
   let rec leq x y =
     match (x,y) with

src/common/common.mld

@@ -41,7 +41,6 @@ Printable
 {1 I/O}
 {!modules:
 Messages
-Tracing
 }
 
 

src/common/dune

@@ -8,6 +8,7 @@
    batteries.unthreaded
    zarith
    goblint_std
+   goblint_tracing
    goblint-cil
    fpath
    yojson

src/common/util/gobConfig.ml

@@ -21,7 +21,6 @@
 *)
 
 open Batteries
-open Tracing
 open Printf
 
 exception ConfigError of string
@@ -300,7 +299,7 @@ struct
     try
       let st = String.trim st in
       let x = get_value !json_conf (parse_path st) in
-      if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x;
+      if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x;
       try f x
       with Yojson.Safe.Util.Type_error (s, _) ->
         eprintf "The value for '%s' has the wrong type: %s\n" st s;
@@ -332,7 +331,7 @@ struct
 
   let wrap_get f x =
     (* self-observe options, which Spec construction depends on *)
-    if !building_spec && Tracing.tracing then Tracing.trace "config" "get during building_spec: %s\n" x;
+    if !building_spec && Goblint_tracing.tracing then Goblint_tracing.trace "config" "get during building_spec: %s\n" x;
     (* TODO: blacklist such building_spec option from server mode modification since it will have no effect (spec is already built) *)
     f x
 
@@ -352,7 +351,7 @@ struct
 
   (** Helper function for writing values. Handles the tracing. *)
   let set_path_string st v =
-    if tracing then trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v;
+    if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v;
     set_value v json_conf (parse_path st)
 
   let set_json st j =
@@ -402,7 +401,7 @@ struct
     | Some fn ->
       let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in (Fpath.to_string fn) in
       merge v;
-      if tracing then trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf
+      if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf
     | None -> raise (Sys_error (Printf.sprintf "%s: No such file or diretory" (Fpath.to_string fn)))
 end
 

src/common/util/messages.ml

@@ -339,7 +339,8 @@ let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt =
   else
     GobPretty.igprintf () fmt
 
-include Tracing
+
+include Goblint_tracing
 
 open Pretty
 

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info 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 fileutils goblint_std goblint_common goblint_domain
+  (libraries goblint.sites goblint.build-info 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 fileutils goblint_std goblint_common goblint_domain goblint_tracing
     ; 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

@@ -825,13 +825,13 @@ struct
     )
 
   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;
+    let old_loc  = !Goblint_tracing.current_loc in
+    let old_loc2 = !Goblint_tracing.next_loc in
+    Goblint_tracing.current_loc := f;
+    Goblint_tracing.next_loc := t;
     Goblint_backtrace.protect ~mark:(fun () -> TfLocation f) ~finally:(fun () ->
-        Tracing.current_loc := old_loc;
-        Tracing.next_loc := old_loc2
+        Goblint_tracing.current_loc := old_loc;
+        Goblint_tracing.next_loc := old_loc2
       ) (fun () ->
         let d       = tf var getl sidel getg sideg prev_node edge d in
         d

src/framework/control.ml

@@ -142,12 +142,12 @@ struct
     if List.mem "termination" @@ get_string_list "ana.activated" then (
       (* check if we have upjumping gotos *)
       let open Cilfacade in
-      let warn_for_upjumps fundec gotos = 
+      let warn_for_upjumps fundec gotos =
         if FunSet.mem live_funs fundec then (
           (* set nortermiantion flag *)
           AnalysisState.svcomp_may_not_terminate := true;
           (* iterate through locations to produce warnings *)
-          LocSet.iter (fun l _ -> 
+          LocSet.iter (fun l _ ->
               M.warn ~loc:(M.Location.CilLocation l) ~category:Termination "The program might not terminate! (Upjumping Goto)"
             ) gotos
         )
@@ -313,7 +313,7 @@ struct
         if M.tracing then M.trace "con" "Initializer %a\n" CilType.Location.pretty loc;
         (*incr count;
           if (get_bool "dbg.verbose")&& (!count mod 1000 = 0)  then Printf.printf "%d %!" !count;    *)
-        Tracing.current_loc := loc;
+        Goblint_tracing.current_loc := loc;
         match edge with
         | MyCFG.Entry func        ->
           if M.tracing then M.trace "global_inits" "Entry %a\n" d_lval (var func.svar);
@@ -335,9 +335,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 old_loc = !Goblint_tracing.current_loc in
       let result : Spec.D.t = List.fold_left transfer_func with_externs edges in
-      Tracing.current_loc := old_loc;
+      Goblint_tracing.current_loc := old_loc;
       if M.tracing then M.trace "global_inits" "startstate: %a\n" Spec.D.pretty result;
       result, !funs
     in

src/goblint_lib.ml

@@ -325,7 +325,6 @@ module SolverBox = SolverBox
     Various input/output interfaces and formats. *)
 
 module Messages = Messages
-module Tracing = Tracing
 
 (** {2 Front-end}
 

src/index.mld

@@ -46,6 +46,9 @@ The following libraries provide utilities which are completely independent of Go
 {2 Library goblint.timing}
 {!modules:Goblint_timing}
 
+{2 Library goblint.tracing}
+{!modules:Goblint_tracing}
+
 
 {1 Vendored}
 The following libraries are vendored in Goblint.

src/maingoblint.ml

@@ -53,7 +53,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
   let add_string l = let f str = l := str :: !l in Arg_complete.String (f, Arg_complete.empty) in
   let add_int    l = let f str = l := str :: !l in Arg_complete.Int (f, Arg_complete.empty) in
   let set_trace sys =
-    if Messages.tracing then Tracing.addsystem sys
+    if Messages.tracing then Goblint_tracing.addsystem sys
     else (prerr_endline "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Stdlib.Exit)
   in
   let configure_html () =
@@ -112,8 +112,8 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
   ; "--print_options"      , Arg_complete.Unit (fun () -> Options.print_options (); exit 0), ""
   ; "--print_all_options"  , Arg_complete.Unit (fun () -> Options.print_all_options (); exit 0), ""
   ; "--trace"              , Arg_complete.String (set_trace, Arg_complete.empty), ""
-  ; "--tracevars"          , add_string Tracing.tracevars, ""
-  ; "--tracelocs"          , add_int Tracing.tracelocs, ""
+  ; "--tracevars"          , add_string Goblint_tracing.tracevars, ""
+  ; "--tracelocs"          , add_int Goblint_tracing.tracelocs, ""
   ; "--help"               , Arg_complete.Unit (fun _ -> print_help stdout),""
   ; "--html"               , Arg_complete.Unit (fun _ -> configure_html ()),""
   ; "--sarif"               , Arg_complete.Unit (fun _ -> configure_sarif ()),""

src/util/tracing/dune

@@ -0,0 +1,9 @@
+(include_subdirs no)
+
+(library
+ (name goblint_tracing)
+ (public_name goblint.tracing)
+ (libraries
+   goblint_std
+   goblint-cil
+   goblint_build_info))

src/common/util/tracing.ml → src/util/tracing/goblint_tracing.ml

@@ -4,6 +4,7 @@
  * large domains we output. The original code generated the document object
  * even when the subsystem is not activated. *)
 
+open Goblint_std
 open GoblintCil
 open Pretty