Move ml_loc and operations to Logging

Summary:public
Refactor the ml_loc type and associated operations from Utils to Logging.  Seems a better fit, and reduces dependencies.

Reviewed By: cristianoc

Differential Revision: D3161440

fb-gh-sync-id: 2e09c25
fbshipit-source-id: 2e09c25

infer/src/backend/errlog.ml

@@ -23,7 +23,7 @@ type loc_trace = loc_trace_elem list
 
 (** Data associated to a specific error *)
 type err_data =
-  (int * int) * int * Location.t * ml_loc option * loc_trace *
+  (int * int) * int * Location.t * L.ml_loc option * loc_trace *
   Prop.normal Prop.t option * Exceptions.err_class
 
 let err_data_compare
@@ -65,7 +65,7 @@ let empty () = ErrLogHash.create 13
 type iter_fun =
   (int * int) ->
   Location.t ->
-  ml_loc option ->
+  L.ml_loc option ->
   Exceptions.err_kind ->
   bool ->
   Localise.t -> Localise.error_desc -> string ->

infer/src/backend/errlog.mli

@@ -30,7 +30,7 @@ val empty : unit -> t
 type iter_fun =
   (int * int) ->
   Location.t ->
-  ml_loc option ->
+  Logging.ml_loc option ->
   Exceptions.err_kind ->
   bool ->
   Localise.t -> Localise.error_desc -> string ->

infer/src/backend/exceptions.ml

@@ -28,59 +28,59 @@ type err_class = Checker | Prover | Nocat
 type err_kind =
     Kwarning | Kerror | Kinfo
 
-exception Abduction_case_not_implemented of ml_loc
-exception Analysis_stops of Localise.error_desc * ml_loc option
-exception Array_out_of_bounds_l1 of Localise.error_desc * ml_loc
-exception Array_out_of_bounds_l2 of Localise.error_desc * ml_loc
-exception Array_out_of_bounds_l3 of Localise.error_desc * ml_loc
-exception Array_of_pointsto of ml_loc
-exception Bad_footprint of ml_loc
-exception Bad_pointer_comparison of Localise.error_desc * ml_loc
-exception Class_cast_exception of Localise.error_desc * ml_loc
+exception Abduction_case_not_implemented of L.ml_loc
+exception Analysis_stops of Localise.error_desc * L.ml_loc option
+exception Array_out_of_bounds_l1 of Localise.error_desc * L.ml_loc
+exception Array_out_of_bounds_l2 of Localise.error_desc * L.ml_loc
+exception Array_out_of_bounds_l3 of Localise.error_desc * L.ml_loc
+exception Array_of_pointsto of L.ml_loc
+exception Bad_footprint of L.ml_loc
+exception Bad_pointer_comparison of Localise.error_desc * L.ml_loc
+exception Class_cast_exception of Localise.error_desc * L.ml_loc
 exception Codequery of Localise.error_desc
-exception Comparing_floats_for_equality of Localise.error_desc * ml_loc
-exception Condition_is_assignment of Localise.error_desc * ml_loc
-exception Condition_always_true_false of Localise.error_desc * bool * ml_loc
-exception Context_leak of Localise.error_desc * ml_loc
+exception Comparing_floats_for_equality of Localise.error_desc * L.ml_loc
+exception Condition_is_assignment of Localise.error_desc * L.ml_loc
+exception Condition_always_true_false of Localise.error_desc * bool * L.ml_loc
+exception Context_leak of Localise.error_desc * L.ml_loc
 exception Custom_error of string * Localise.error_desc
-exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_loc
+exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * L.ml_loc
 exception Deallocate_stack_variable of Localise.error_desc
 exception Deallocate_static_memory of Localise.error_desc
-exception Deallocation_mismatch of Localise.error_desc * ml_loc
-exception Divide_by_zero of Localise.error_desc * ml_loc
+exception Deallocation_mismatch of Localise.error_desc * L.ml_loc
+exception Divide_by_zero of Localise.error_desc * L.ml_loc
 exception Eradicate of string * Localise.error_desc
-exception Field_not_null_checked of Localise.error_desc * ml_loc
-exception Frontend_warning of string * Localise.error_desc * ml_loc
+exception Field_not_null_checked of Localise.error_desc * L.ml_loc
+exception Frontend_warning of string * Localise.error_desc * L.ml_loc
 exception Checkers of string * Localise.error_desc
 exception Inherently_dangerous_function of Localise.error_desc
 exception Internal_error of Localise.error_desc
 exception Java_runtime_exception of Typename.t * string * Localise.error_desc
 exception Leak of
     bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc)
-    * bool * Sil.resource * ml_loc
-exception Missing_fld of Ident.fieldname * ml_loc
-exception Premature_nil_termination of Localise.error_desc * ml_loc
-exception Null_dereference of Localise.error_desc * ml_loc
-exception Null_test_after_dereference of Localise.error_desc * ml_loc
-exception Parameter_not_null_checked of Localise.error_desc * ml_loc
-exception Pointer_size_mismatch of Localise.error_desc * ml_loc
-exception Precondition_not_found of Localise.error_desc * ml_loc
-exception Precondition_not_met of Localise.error_desc * ml_loc
-exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_loc
-exception Registered_observer_being_deallocated of Localise.error_desc * ml_loc
-exception Return_expression_required of Localise.error_desc * ml_loc
-exception Return_statement_missing of Localise.error_desc * ml_loc
-exception Return_value_ignored of Localise.error_desc * ml_loc
+    * bool * Sil.resource * L.ml_loc
+exception Missing_fld of Ident.fieldname * L.ml_loc
+exception Premature_nil_termination of Localise.error_desc * L.ml_loc
+exception Null_dereference of Localise.error_desc * L.ml_loc
+exception Null_test_after_dereference of Localise.error_desc * L.ml_loc
+exception Parameter_not_null_checked of Localise.error_desc * L.ml_loc
+exception Pointer_size_mismatch of Localise.error_desc * L.ml_loc
+exception Precondition_not_found of Localise.error_desc * L.ml_loc
+exception Precondition_not_met of Localise.error_desc * L.ml_loc
+exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * L.ml_loc
+exception Registered_observer_being_deallocated of Localise.error_desc * L.ml_loc
+exception Return_expression_required of Localise.error_desc * L.ml_loc
+exception Return_statement_missing of Localise.error_desc * L.ml_loc
+exception Return_value_ignored of Localise.error_desc * L.ml_loc
 exception Skip_function of Localise.error_desc
-exception Skip_pointer_dereference of Localise.error_desc * ml_loc
-exception Stack_variable_address_escape of Localise.error_desc * ml_loc
-exception Symexec_memory_error of ml_loc
-exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_loc
-exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_loc
-exception Uninitialized_value of Localise.error_desc * ml_loc
+exception Skip_pointer_dereference of Localise.error_desc * L.ml_loc
+exception Stack_variable_address_escape of Localise.error_desc * L.ml_loc
+exception Symexec_memory_error of L.ml_loc
+exception Tainted_value_reaching_sensitive_function of Localise.error_desc * L.ml_loc
+exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L.ml_loc
+exception Uninitialized_value of Localise.error_desc * L.ml_loc
 exception Unknown_proc
-exception Use_after_free of Localise.error_desc * ml_loc
-exception Wrong_argument_number of ml_loc
+exception Use_after_free of Localise.error_desc * L.ml_loc
+exception Wrong_argument_number of L.ml_loc
 
 
 (** Turn an exception into a descriptive string, error description, location in ml source, and category *)
@@ -90,7 +90,7 @@ let recognize_exception exn =
     match Localise.error_desc_get_bucket desc with
     | None -> false
     | Some bucket -> bucket <> Localise.BucketLevel.b1 in
-  let err_name, desc, (ml_loc_opt : ml_loc option), visibility, severity, force_kind, eclass =
+  let err_name, desc, (ml_loc_opt : L.ml_loc option), visibility, severity, force_kind, eclass =
     match exn with (* all the names of Exn_user errors must be defined in Localise *)
     | Abduction_case_not_implemented ml_loc ->
         (Localise.from_string "Abduction_case_not_implemented",
@@ -304,7 +304,7 @@ let print_exception_html s exn =
   let err_name, desc, ml_loc_opt, _, _, _, _ = recognize_exception exn in
   let ml_loc_string = match ml_loc_opt with
     | None -> ""
-    | Some ml_loc -> " " ^ ml_loc_to_string ml_loc in
+    | Some ml_loc -> " " ^ L.ml_loc_to_string ml_loc in
   let desc_str = pp_to_string Localise.pp_error_desc desc in
   (L.d_strln_color Red) (s ^ (Localise.to_string err_name) ^ " " ^ desc_str ^ ml_loc_string)
 
@@ -334,7 +334,7 @@ let pp_err (_, node_key) loc ekind ex_name desc ml_loc_opt fmt () =
     Localise.pp ex_name
     Localise.pp_error_desc desc
     pp_key node_key
-    pp_ml_loc_opt ml_loc_opt
+    L.pp_ml_loc_opt ml_loc_opt
 
 (** Return true if the exception is not serious and should be handled in timeout mode *)
 let handle_exception exn =

infer/src/backend/exceptions.mli

@@ -27,59 +27,60 @@ type err_kind =
 (** class of error *)
 type err_class = Checker | Prover | Nocat
 
-exception Abduction_case_not_implemented of ml_loc
-exception Analysis_stops of Localise.error_desc * ml_loc option
-exception Array_of_pointsto of ml_loc
-exception Array_out_of_bounds_l1 of Localise.error_desc * ml_loc
-exception Array_out_of_bounds_l2 of Localise.error_desc * ml_loc
-exception Array_out_of_bounds_l3 of Localise.error_desc * ml_loc
-exception Bad_footprint of ml_loc
-exception Bad_pointer_comparison of Localise.error_desc * ml_loc
-exception Class_cast_exception of Localise.error_desc * ml_loc
+exception Abduction_case_not_implemented of Logging.ml_loc
+exception Analysis_stops of Localise.error_desc * Logging.ml_loc option
+exception Array_of_pointsto of Logging.ml_loc
+exception Array_out_of_bounds_l1 of Localise.error_desc * Logging.ml_loc
+exception Array_out_of_bounds_l2 of Localise.error_desc * Logging.ml_loc
+exception Array_out_of_bounds_l3 of Localise.error_desc * Logging.ml_loc
+exception Bad_footprint of Logging.ml_loc
+exception Bad_pointer_comparison of Localise.error_desc * Logging.ml_loc
+exception Class_cast_exception of Localise.error_desc * Logging.ml_loc
 exception Codequery of Localise.error_desc
-exception Comparing_floats_for_equality of Localise.error_desc * ml_loc
-exception Condition_always_true_false of Localise.error_desc * bool * ml_loc
-exception Condition_is_assignment of Localise.error_desc * ml_loc
-exception Context_leak of Localise.error_desc * ml_loc
+exception Comparing_floats_for_equality of Localise.error_desc * Logging.ml_loc
+exception Condition_always_true_false of Localise.error_desc * bool * Logging.ml_loc
+exception Condition_is_assignment of Localise.error_desc * Logging.ml_loc
+exception Context_leak of Localise.error_desc * Logging.ml_loc
 exception Custom_error of string * Localise.error_desc
-exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_loc
+exception Dangling_pointer_dereference of
+    Sil.dangling_kind option * Localise.error_desc * Logging.ml_loc
 exception Deallocate_stack_variable of Localise.error_desc
 exception Deallocate_static_memory of Localise.error_desc
-exception Deallocation_mismatch of Localise.error_desc * ml_loc
-exception Divide_by_zero of Localise.error_desc * ml_loc
-exception Field_not_null_checked of Localise.error_desc * ml_loc
+exception Deallocation_mismatch of Localise.error_desc * Logging.ml_loc
+exception Divide_by_zero of Localise.error_desc * Logging.ml_loc
+exception Field_not_null_checked of Localise.error_desc * Logging.ml_loc
 exception Eradicate of string * Localise.error_desc
 exception Checkers of string * Localise.error_desc
-exception Frontend_warning of string * Localise.error_desc * ml_loc
+exception Frontend_warning of string * Localise.error_desc * Logging.ml_loc
 exception Inherently_dangerous_function of Localise.error_desc
 exception Internal_error of Localise.error_desc
 exception Java_runtime_exception of Typename.t * string * Localise.error_desc
 exception Leak of
     bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc)
-    * bool * Sil.resource * ml_loc
-exception Missing_fld of Ident.fieldname * ml_loc
-exception Premature_nil_termination of Localise.error_desc * ml_loc
-exception Null_dereference of Localise.error_desc * ml_loc
-exception Null_test_after_dereference of Localise.error_desc * ml_loc
-exception Parameter_not_null_checked of Localise.error_desc * ml_loc
-exception Pointer_size_mismatch of Localise.error_desc * ml_loc
-exception Precondition_not_found of Localise.error_desc * ml_loc
-exception Precondition_not_met of Localise.error_desc * ml_loc
-exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_loc
-exception Registered_observer_being_deallocated of Localise.error_desc * ml_loc
-exception Return_expression_required of Localise.error_desc * ml_loc
-exception Return_statement_missing of Localise.error_desc * ml_loc
-exception Return_value_ignored of Localise.error_desc * ml_loc
+    * bool * Sil.resource * Logging.ml_loc
+exception Missing_fld of Ident.fieldname * Logging.ml_loc
+exception Premature_nil_termination of Localise.error_desc * Logging.ml_loc
+exception Null_dereference of Localise.error_desc * Logging.ml_loc
+exception Null_test_after_dereference of Localise.error_desc * Logging.ml_loc
+exception Parameter_not_null_checked of Localise.error_desc * Logging.ml_loc
+exception Pointer_size_mismatch of Localise.error_desc * Logging.ml_loc
+exception Precondition_not_found of Localise.error_desc * Logging.ml_loc
+exception Precondition_not_met of Localise.error_desc * Logging.ml_loc
+exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * Logging.ml_loc
+exception Registered_observer_being_deallocated of Localise.error_desc * Logging.ml_loc
+exception Return_expression_required of Localise.error_desc * Logging.ml_loc
+exception Return_statement_missing of Localise.error_desc * Logging.ml_loc
+exception Return_value_ignored of Localise.error_desc * Logging.ml_loc
 exception Skip_function of Localise.error_desc
-exception Skip_pointer_dereference of Localise.error_desc * ml_loc
-exception Stack_variable_address_escape of Localise.error_desc * ml_loc
-exception Symexec_memory_error of ml_loc
-exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_loc
-exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_loc
-exception Uninitialized_value of Localise.error_desc * ml_loc
+exception Skip_pointer_dereference of Localise.error_desc * Logging.ml_loc
+exception Stack_variable_address_escape of Localise.error_desc * Logging.ml_loc
+exception Symexec_memory_error of Logging.ml_loc
+exception Tainted_value_reaching_sensitive_function of Localise.error_desc * Logging.ml_loc
+exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Logging.ml_loc
+exception Uninitialized_value of Localise.error_desc * Logging.ml_loc
 exception Unknown_proc
-exception Use_after_free of Localise.error_desc * ml_loc
-exception Wrong_argument_number of ml_loc
+exception Use_after_free of Localise.error_desc * Logging.ml_loc
+exception Wrong_argument_number of Logging.ml_loc
 
 (** string describing an error class *)
 val err_class_string : err_class -> string
@@ -96,10 +97,10 @@ val print_exception_html : string -> exn -> unit
 (** pretty print an error given its (id,key), location, kind, name, description,
     and optional ml location *)
 val pp_err : int * int -> Location.t -> err_kind -> Localise.t -> Localise.error_desc ->
-  ml_loc option -> Format.formatter -> unit -> unit
+  Logging.ml_loc option -> Format.formatter -> unit -> unit
 
 (** Turn an exception into an error name, error description,
     location in ml source, and category *)
 val recognize_exception : exn ->
-  (Localise.t * Localise.error_desc * (ml_loc option) * exception_visibility *
+  (Localise.t * Localise.error_desc * (Logging.ml_loc option) * exception_visibility *
    exception_severity * err_kind option * err_class)

infer/src/backend/interproc.ml

@@ -1342,7 +1342,7 @@ let perform_transition exe_env tenv proc_name =
         L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
         let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
         let err_str = "exception raised " ^ (Localise.to_string err_name) in
-        L.err "Error: %s %a@." err_str pp_ml_loc_opt ml_loc_opt;
+        L.err "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt;
         [] in
     transition_footprint_re_exe proc_name joined_pres in
   if Specs.get_phase proc_name == Specs.FOOTPRINT

infer/src/backend/logging.ml

@@ -129,6 +129,28 @@ let stderr fmt_string =
 let stdout fmt_string =
   do_print F.std_formatter fmt_string
 
+(** Type of location in ml source: __POS__ *)
+type ml_loc = string * int * int * int
+
+(** Convert a ml location to a string *)
+let ml_loc_to_string (file, lnum, cnum, enum) =
+  Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum
+
+(** Pretty print a location of ml source *)
+let pp_ml_loc fmt ml_loc =
+  F.fprintf fmt "%s" (ml_loc_to_string ml_loc)
+
+let pp_ml_loc_opt fmt ml_loc_opt =
+  if !Config.developer_mode then match ml_loc_opt with
+    | None -> ()
+    | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc
+
+let assert_false ((file, lnum, cnum, _) as ml_loc) =
+  Printf.eprintf "\nASSERT FALSE %s\nCALL STACK\n%s\n%!"
+    (ml_loc_to_string ml_loc)
+    (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000));
+  raise (Assert_failure (file, lnum, cnum))
+
 (** print a warning with information of the position in the ml source where it oririnated.
     use as: warning_position "description" (try assert false with Assert_failure x -> x); *)
 let warning_position (s: string) (ml_loc: ml_loc) =

infer/src/backend/logging.mli

@@ -93,6 +93,18 @@ val set_err_formatter : Format.formatter -> unit
 (** Flush the current streams *)
 val flush_streams : unit -> unit
 
+(** Type of location in ml source: __POS__ *)
+type ml_loc = string * int * int * int
+
+(** Convert a ml location to a string *)
+val ml_loc_to_string : ml_loc -> string
+
+(** Pretty print a location of ml source *)
+val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit
+
+(** Print stack trace and throw assert false *)
+val assert_false : ml_loc -> 'a
+
 (** print a warning with information of the position in the ml source where it oririnated.
     use as: warning_position "description" (try assert false with Assert_failure x -> x); *)
 val warning_position: string -> ml_loc -> unit

infer/src/backend/prop.ml

@@ -46,7 +46,7 @@ type 'a t =
     foot_pi: pi;  (** abduced pure part *)
   }
 
-exception Cannot_star of ml_loc
+exception Cannot_star of L.ml_loc
 
 (** {2 Basic Functions for Propositions} *)
 

infer/src/backend/prop.mli

@@ -29,7 +29,7 @@ type struct_init_mode =
   | No_init
   | Fld_init
 
-exception Cannot_star of ml_loc
+exception Cannot_star of Logging.ml_loc
 
 (** {2 Basic Functions for propositions} *)
 

infer/src/backend/symExec.ml

@@ -1216,7 +1216,7 @@ and instrs ?(mask_errors=false) tenv pdesc instrs ppl =
     with exn when exn_not_failure exn && mask_errors ->
       let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in
       let loc = (match ml_source with
-          | Some ml_loc -> "at " ^ (ml_loc_to_string ml_loc)
+          | Some ml_loc -> "at " ^ (L.ml_loc_to_string ml_loc)
           | None -> "") in
       L.d_warning
         ("Generated Instruction Failed with: " ^

infer/src/backend/tabulation.mli

@@ -26,7 +26,7 @@ val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * Sil.path_
 
 (** raise a cast exception *)
 val raise_cast_exception :
-  ml_loc -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a
+  Logging.ml_loc -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a
 
 (** check if a prop is an exception *)
 val prop_is_exn : Procname.t -> 'a Prop.t -> bool

infer/src/backend/utils.ml

@@ -237,22 +237,6 @@ let pp_elapsed_time fmt () =
   let elapsed = Unix.gettimeofday () -. initial_timeofday in
   Format.fprintf fmt "%f" elapsed
 
-(** Type of location in ml source: __POS__ *)
-type ml_loc = string * int * int * int
-
-(** Convert a ml location to a string *)
-let ml_loc_to_string (file, lnum, cnum, enum) =
-  Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum
-
-(** Pretty print a location of ml source *)
-let pp_ml_loc fmt ml_loc =
-  F.fprintf fmt "%s" (ml_loc_to_string ml_loc)
-
-let pp_ml_loc_opt fmt ml_loc_opt =
-  if !Config.developer_mode then match ml_loc_opt with
-    | None -> ()
-    | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc
-
 (** {2 SymOp and Failures: units of symbolic execution} *)
 
 type failure_kind =
@@ -1000,9 +984,3 @@ let run_in_footprint_mode f x =
 
 let run_with_abs_val_equal_zero f x =
   set_reference_and_call_function Config.abs_val 0 f x
-
-let assert_false ((file, lnum, cnum, _) as ml_loc) =
-  Printf.eprintf "\nASSERT FALSE %s\nCALL STACK\n%s\n%!"
-    (ml_loc_to_string ml_loc)
-    (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000));
-  raise (Assert_failure (file, lnum, cnum))

infer/src/backend/utils.mli

@@ -68,15 +68,6 @@ module StringMap : Map.S with type key = string
 
 (** {2 Printing} *)
 
-(** Type of location in ml source: __POS__ *)
-type ml_loc = string * int * int * int
-
-(** Convert a ml location to a string *)
-val ml_loc_to_string : ml_loc -> string
-
-(** Pretty print a location of ml source *)
-val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit
-
 (** Colors supported in printing *)
 type color = Black | Blue | Green | Orange | Red
 
@@ -380,6 +371,3 @@ val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b
 (** [set_reference_and_call_function ref val f x] calls f x with ref set to val.
     Restore the initial value also in case of exception. *)
 val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
-
-(** Pritn stack trace and throw assert false *)
-val assert_false : ml_loc -> 'a