[sledge] Make --trace option optional

Reviewed By: mbouaziz

Differential Revision: D14075524

fbshipit-source-id: 97c9ae13c

sledge/src/config.ml

@@ -84,7 +84,10 @@ type t =
         (** Dump $(i,input.bc) translated to LLAIR in human-readable form to
             $(i,output.llair), or $(b,-) for $(b,stdout). *)
   ; trace: Trace.trace_mods_funs
-         [@aka ["t"]] [@docv "spec"] [@conv trace_conv]
+         [@aka ["t"]]
+         [@docv "spec"]
+         [@conv trace_conv]
+         [@default Trace.none.trace_mods_funs]
         (** Enable debug tracing according to $(i,spec), which is a sequence
             of module and function names separated by $(b,+) or $(b,-). For
             example, $(b,Control-Control.exec_inst) enables all tracing in

sledge/src/trace/trace.ml

@@ -19,8 +19,8 @@ type trace_mod_funs =
 type trace_mods_funs = trace_mod_funs Map.M(String).t
 type config = {trace_all: bool; trace_mods_funs: trace_mods_funs}
 
-let config : config ref =
+let none = {trace_all= false; trace_mods_funs= Map.empty (module String)}
-  ref {trace_all= false; trace_mods_funs= Map.empty (module String)}
+let config : config ref = ref none
 
 let init ?(margin = 300) ~config:c () =
   Format.set_margin margin ;

sledge/src/trace/trace.mli

@@ -21,6 +21,8 @@ type config =
   ; trace_mods_funs: trace_mods_funs
         (** Specify tracing of individual toplevel modules *) }
 
+val none : config
+
 val init : ?margin:int -> config:config -> unit -> unit
 (** Initialize the configuration of debug tracing. *)