[exceptions] make more efforts to preserve backtraces

Summary:
Calling functions that raise exceptions (even if they get caught) may smudge
the backtraces we get from OCaml. We need to record the original backtrace
*before* calling such fuctions on the path between catching an exception and
reraising it.

Also change the heptuple returned by `Exceptions.recognize_exception` into a
record type, and make that function not raise when classifying exceptions.

Reviewed By: jberdine

Differential Revision: D5882934

fbshipit-source-id: 8e99fe8
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent 4c88e986b7
commit e02f6ab39f

@ -217,25 +217,24 @@ let update errlog_old errlog_new =
ErrLogHash.iter (fun err_key l -> ignore (add_issue errlog_old err_key l)) errlog_new
let log_issue err_kind err_log loc (node_id, node_key) session ltr ?linters_def_file ?doc_url exn =
let err_name, err_desc, ml_loc_opt, visibility, severity, force_kind, eclass =
Exceptions.recognize_exception exn
in
let err_kind = match force_kind with Some err_kind -> err_kind | _ -> err_kind in
let error = Exceptions.recognize_exception exn in
let err_kind = match error.kind with Some err_kind -> err_kind | _ -> err_kind in
let hide_java_loc_zero =
(* hide java errors at location zero unless in -developer_mode *)
not Config.developer_mode && Config.curr_language_is Config.Java
&& Int.equal loc.Location.line 0
in
let hide_memory_error =
match Localise.error_desc_get_bucket err_desc with
match Localise.error_desc_get_bucket error.description with
| Some bucket when String.equal bucket Mleak_buckets.ml_bucket_unknown_origin
-> not Mleak_buckets.should_raise_leak_unknown_origin
| _
-> false
in
let log_it =
Exceptions.equal_visibility visibility Exceptions.Exn_user
|| Config.developer_mode && Exceptions.equal_visibility visibility Exceptions.Exn_developer
Exceptions.equal_visibility error.visibility Exceptions.Exn_user
|| Config.developer_mode
&& Exceptions.equal_visibility error.visibility Exceptions.Exn_developer
in
if log_it && not hide_java_loc_zero && not hide_memory_error then
let added =
@ -244,31 +243,32 @@ let log_issue err_kind err_log loc (node_id, node_key) session ltr ?linters_def_
{ node_id_key
; session
; loc
; loc_in_ml_source= ml_loc_opt
; loc_in_ml_source= error.ml_loc
; loc_trace= ltr
; err_class= eclass
; visibility
; err_class= error.category
; visibility= error.visibility
; linters_def_file
; doc_url }
in
let err_key =
{ err_kind
; in_footprint= !Config.footprint
; err_name
; err_desc
; severity= severity_to_str severity }
; err_name= error.name
; err_desc= error.description
; severity= severity_to_str error.severity }
in
add_issue err_log err_key (ErrDataSet.singleton err_data)
in
let should_print_now = match exn with Exceptions.Internal_error _ -> true | _ -> added in
let print_now () =
let ex_name, desc, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
L.(debug Analysis Medium)
"@\n%a@\n@?" (Exceptions.pp_err ~node_key loc err_kind ex_name desc ml_loc_opt) () ;
"@\n%a@\n@?"
(Exceptions.pp_err ~node_key loc err_kind error.name error.description error.ml_loc) () ;
if err_kind <> Exceptions.Kerror then
let warn_str =
let pp fmt =
Format.fprintf fmt "%s %a" err_name.IssueType.unique_id Localise.pp_error_desc desc
Format.fprintf fmt "%s %a" error.name.IssueType.unique_id Localise.pp_error_desc
error.description
in
F.asprintf "%t" pp
in

@ -149,233 +149,518 @@ 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 *)
type t =
{ name: IssueType.t
; description: Localise.error_desc
; ml_loc: Logging.ml_loc option (** location in the infer source code *)
; visibility: visibility
; severity: severity
; kind: err_kind option
; category: err_class }
let recognize_exception exn =
let err_name, desc, (ml_loc_opt: L.ml_loc option), visibility, severity, force_kind, eclass =
match exn with
(* all the static names of errors must be defined in Config.IssueType *)
| Abduction_case_not_implemented ml_loc
-> ( IssueType.abduction_case_not_implemented
, Localise.no_desc
, Some ml_loc
, Exn_developer
, Low
, None
, Nocat )
| Context_leak (desc, _)
-> (IssueType.context_leak, desc, None, Exn_user, High, None, Nocat)
| Analysis_stops (desc, ml_loc_opt)
-> let visibility = if Config.analysis_stops then Exn_user else Exn_developer in
(IssueType.analysis_stops, desc, ml_loc_opt, visibility, Medium, None, Nocat)
| Array_of_pointsto ml_loc
-> ( IssueType.array_of_pointsto
, Localise.no_desc
, Some ml_loc
, Exn_developer
, Low
, None
, Nocat )
| Array_out_of_bounds_l1 (desc, ml_loc)
-> (IssueType.array_out_of_bounds_l1, desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
| Array_out_of_bounds_l2 (desc, ml_loc)
-> (IssueType.array_out_of_bounds_l2, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Array_out_of_bounds_l3 (desc, ml_loc)
-> (IssueType.array_out_of_bounds_l3, desc, Some ml_loc, Exn_developer, Medium, None, Nocat)
| Assert_failure (f, l, c)
-> let ml_loc = (f, l, c, c) in
(IssueType.assert_failure, Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat)
| Bad_footprint ml_loc
-> (IssueType.bad_footprint, Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Cannot_star ml_loc
-> (IssueType.cannot_star, Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Class_cast_exception (desc, ml_loc)
-> (IssueType.class_cast_exception, desc, Some ml_loc, Exn_user, High, None, Prover)
| Codequery desc
-> (IssueType.codequery, desc, None, Exn_user, High, None, Prover)
| Comparing_floats_for_equality (desc, ml_loc)
-> (IssueType.comparing_floats_for_equality, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Condition_always_true_false (desc, b, ml_loc)
-> let name =
if b then IssueType.condition_always_true else IssueType.condition_always_false
in
(name, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Custom_error (error_msg, desc)
-> (IssueType.from_string error_msg, desc, None, Exn_user, High, None, Checker)
| Dangling_pointer_dereference (dko, desc, ml_loc)
-> let visibility =
match dko with
| Some _
-> Exn_user (* only show to the user if the category was identified *)
| None
-> Exn_developer
match exn with
(* all the static names of errors must be defined in Config.IssueType *)
| Abduction_case_not_implemented ml_loc
-> { name= IssueType.abduction_case_not_implemented
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Context_leak (desc, _)
-> { name= IssueType.context_leak
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Nocat }
| Analysis_stops (desc, ml_loc_opt)
-> let visibility = if Config.analysis_stops then Exn_user else Exn_developer in
{ name= IssueType.analysis_stops
; description= desc
; ml_loc= ml_loc_opt
; visibility
; severity= Medium
; kind= None
; category= Nocat }
| Array_of_pointsto ml_loc
-> { name= IssueType.array_of_pointsto
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Array_out_of_bounds_l1 (desc, ml_loc)
-> { name= IssueType.array_out_of_bounds_l1
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Checker }
| Array_out_of_bounds_l2 (desc, ml_loc)
-> { name= IssueType.array_out_of_bounds_l2
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Array_out_of_bounds_l3 (desc, ml_loc)
-> { name= IssueType.array_out_of_bounds_l3
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Medium
; kind= None
; category= Nocat }
| Assert_failure (f, l, c)
-> let ml_loc = (f, l, c, c) in
{ name= IssueType.assert_failure
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= High
; kind= None
; category= Nocat }
| Bad_footprint ml_loc
-> { name= IssueType.bad_footprint
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Cannot_star ml_loc
-> { name= IssueType.cannot_star
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Class_cast_exception (desc, ml_loc)
-> { name= IssueType.class_cast_exception
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Codequery desc
-> { name= IssueType.codequery
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Comparing_floats_for_equality (desc, ml_loc)
-> { name= IssueType.comparing_floats_for_equality
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Condition_always_true_false (desc, b, ml_loc)
-> let name = if b then IssueType.condition_always_true else IssueType.condition_always_false in
{ name
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Custom_error (error_msg, desc)
-> { name= IssueType.from_string error_msg
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Checker }
| Dangling_pointer_dereference (dko, desc, ml_loc)
-> let visibility =
match dko with
| Some _
-> Exn_user (* only show to the user if the category was identified *)
| None
-> Exn_developer
in
{ name= IssueType.dangling_pointer_dereference
; description= desc
; ml_loc= Some ml_loc
; visibility
; severity= High
; kind= None
; category= Prover }
| Deallocate_stack_variable desc
-> { name= IssueType.deallocate_stack_variable
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Deallocate_static_memory desc
-> { name= IssueType.deallocate_static_memory
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Deallocation_mismatch (desc, ml_loc)
-> { name= IssueType.deallocation_mismatch
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Divide_by_zero (desc, ml_loc)
-> { name= IssueType.divide_by_zero
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Checker }
| Double_lock (desc, ml_loc)
-> { name= IssueType.double_lock
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Prover }
| Eradicate (kind_s, desc)
-> { name= IssueType.from_string kind_s
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Empty_vector_access (desc, ml_loc)
-> { name= IssueType.empty_vector_access
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Prover }
| Field_not_null_checked (desc, ml_loc)
-> { name= IssueType.field_not_null_checked
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= Some Kwarning
; category= Nocat }
| Frontend_warning ((name, hum), desc, ml_loc)
-> { name= IssueType.from_string name ?hum
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Linters }
| Checkers (kind_s, desc)
-> { name= IssueType.from_string kind_s
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Null_dereference (desc, ml_loc)
-> { name= IssueType.null_dereference
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Null_test_after_dereference (desc, ml_loc)
-> { name= IssueType.null_test_after_dereference
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Nocat }
| Pointer_size_mismatch (desc, ml_loc)
-> { name= IssueType.pointer_size_mismatch
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Checker }
| Inherently_dangerous_function desc
-> { name= IssueType.inherently_dangerous_function
; description= desc
; ml_loc= None
; visibility= Exn_developer
; severity= Medium
; kind= None
; category= Nocat }
| Internal_error desc
-> { name= IssueType.internal_error
; description= desc
; ml_loc= None
; visibility= Exn_developer
; severity= High
; kind= None
; category= Nocat }
| Java_runtime_exception (exn_name, _, desc)
-> let exn_str = Typ.Name.name exn_name in
{ name= IssueType.from_string exn_str
; description= desc
; ml_loc= None
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Leak (fp_part, _, (exn_vis, error_desc), done_array_abstraction, resource, ml_loc)
-> if done_array_abstraction then
{ name= IssueType.leak_after_array_abstraction
; description= error_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= High
; kind= None
; category= Prover }
else if fp_part then
{ name= IssueType.leak_in_footprint
; description= error_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= High
; kind= None
; category= Prover }
else
let name =
match resource with
| PredSymb.Rmemory _
-> IssueType.memory_leak
| PredSymb.Rfile
-> IssueType.resource_leak
| PredSymb.Rlock
-> IssueType.resource_leak
| PredSymb.Rignore
-> IssueType.memory_leak
in
(IssueType.dangling_pointer_dereference, desc, Some ml_loc, visibility, High, None, Prover)
| Deallocate_stack_variable desc
-> (IssueType.deallocate_stack_variable, desc, None, Exn_user, High, None, Prover)
| Deallocate_static_memory desc
-> (IssueType.deallocate_static_memory, desc, None, Exn_user, High, None, Prover)
| Deallocation_mismatch (desc, ml_loc)
-> (IssueType.deallocation_mismatch, desc, Some ml_loc, Exn_user, High, None, Prover)
| Divide_by_zero (desc, ml_loc)
-> (IssueType.divide_by_zero, desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
| Double_lock (desc, ml_loc)
-> (IssueType.double_lock, desc, Some ml_loc, Exn_user, High, Some Kerror, Prover)
| Eradicate (kind_s, desc)
-> (IssueType.from_string kind_s, desc, None, Exn_user, High, None, Prover)
| Empty_vector_access (desc, ml_loc)
-> (IssueType.empty_vector_access, desc, Some ml_loc, Exn_user, High, Some Kerror, Prover)
| Field_not_null_checked (desc, ml_loc)
-> ( IssueType.field_not_null_checked
, desc
, Some ml_loc
, Exn_user
, Medium
, Some Kwarning
, Nocat )
| Frontend_warning ((name, hum), desc, ml_loc)
-> (IssueType.from_string name ?hum, desc, Some ml_loc, Exn_user, Medium, None, Linters)
| Checkers (kind_s, desc)
-> (IssueType.from_string kind_s, desc, None, Exn_user, High, None, Prover)
| Null_dereference (desc, ml_loc)
-> (IssueType.null_dereference, desc, Some ml_loc, Exn_user, High, None, Prover)
| Null_test_after_dereference (desc, ml_loc)
-> (IssueType.null_test_after_dereference, desc, Some ml_loc, Exn_user, High, None, Nocat)
| Pointer_size_mismatch (desc, ml_loc)
-> (IssueType.pointer_size_mismatch, desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
| Inherently_dangerous_function desc
-> (IssueType.inherently_dangerous_function, desc, None, Exn_developer, Medium, None, Nocat)
| Internal_error desc
-> (IssueType.internal_error, desc, None, Exn_developer, High, None, Nocat)
| Java_runtime_exception (exn_name, _, desc)
-> let exn_str = Typ.Name.name exn_name in
(IssueType.from_string exn_str, desc, None, Exn_user, High, None, Prover)
| Leak (fp_part, _, (exn_vis, error_desc), done_array_abstraction, resource, ml_loc)
-> if done_array_abstraction then
( IssueType.leak_after_array_abstraction
, error_desc
, Some ml_loc
, Exn_developer
, High
, None
, Prover )
else if fp_part then
(IssueType.leak_in_footprint, error_desc, Some ml_loc, Exn_developer, High, None, Prover)
else
let loc_str =
match resource with
| PredSymb.Rmemory _
-> IssueType.memory_leak
| PredSymb.Rfile
-> IssueType.resource_leak
| PredSymb.Rlock
-> IssueType.resource_leak
| PredSymb.Rignore
-> IssueType.memory_leak
in
(loc_str, error_desc, Some ml_loc, exn_vis, High, None, Prover)
| Missing_fld (fld, ml_loc)
-> let desc = Localise.verbatim_desc (Typ.Fieldname.to_full_string fld) in
(IssueType.missing_fld, desc, Some ml_loc, Exn_developer, Medium, None, Nocat)
| Premature_nil_termination (desc, ml_loc)
-> (IssueType.premature_nil_termination, desc, Some ml_loc, Exn_user, High, None, Prover)
| Parameter_not_null_checked (desc, ml_loc)
-> ( IssueType.parameter_not_null_checked
, desc
, Some ml_loc
, Exn_user
, Medium
, Some Kwarning
, Nocat )
| Precondition_not_found (desc, ml_loc)
-> (IssueType.precondition_not_found, desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Precondition_not_met (desc, ml_loc)
-> ( IssueType.precondition_not_met
, desc
, Some ml_loc
, Exn_developer
, Medium
, Some Kwarning
, Nocat )
(* always a warning *)
| Retain_cycle (_, desc, ml_loc)
-> (IssueType.retain_cycle, desc, Some ml_loc, Exn_user, High, None, Prover)
| Registered_observer_being_deallocated (desc, ml_loc)
-> ( IssueType.registered_observer_being_deallocated
, desc
, Some ml_loc
, Exn_user
, High
, Some Kerror
, Nocat )
| Return_expression_required (desc, ml_loc)
-> (IssueType.return_expression_required, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Stack_variable_address_escape (desc, ml_loc)
-> ( IssueType.stack_variable_address_escape
, desc
, Some ml_loc
, Exn_user
, High
, Some Kerror
, Nocat )
| Return_statement_missing (desc, ml_loc)
-> (IssueType.return_statement_missing, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Return_value_ignored (desc, ml_loc)
-> (IssueType.return_value_ignored, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| SymOp.Analysis_failure_exe _
-> (IssueType.failure_exe, Localise.no_desc, None, Exn_system, Low, None, Nocat)
| Skip_function desc
-> (IssueType.skip_function, desc, None, Exn_developer, Low, None, Nocat)
| Skip_pointer_dereference (desc, ml_loc)
-> (IssueType.skip_pointer_dereference, desc, Some ml_loc, Exn_user, Medium, Some Kinfo, Nocat)
(* always an info *)
| Symexec_memory_error ml_loc
-> ( IssueType.symexec_memory_error
, Localise.no_desc
, Some ml_loc
, Exn_developer
, Low
, None
, Nocat )
| Uninitialized_value (desc, ml_loc)
-> (IssueType.uninitialized_value, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Unary_minus_applied_to_unsigned_expression (desc, ml_loc)
-> ( IssueType.unary_minus_applied_to_unsigned_expression
, desc
, Some ml_loc
, Exn_user
, Medium
, None
, Nocat )
| Unknown_proc
-> (IssueType.unknown_proc, Localise.no_desc, None, Exn_developer, Low, None, Nocat)
| Unreachable_code_after (desc, ml_loc)
-> (IssueType.unreachable_code_after, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Unsafe_guarded_by_access (desc, ml_loc)
-> (IssueType.unsafe_guarded_by_access, desc, Some ml_loc, Exn_user, High, None, Prover)
| Use_after_free (desc, ml_loc)
-> (IssueType.use_after_free, desc, Some ml_loc, Exn_user, High, None, Prover)
| Wrong_argument_number ml_loc
-> ( IssueType.wrong_argument_number
, Localise.no_desc
, Some ml_loc
, Exn_developer
, Low
, None
, Nocat )
| exn
-> L.internal_error "Backend error '%a'. Backtrace:@\n%s" Exn.pp exn (Exn.backtrace ()) ;
reraise exn
in
(err_name, desc, ml_loc_opt, visibility, severity, force_kind, eclass)
{ name
; description= error_desc
; ml_loc= Some ml_loc
; visibility= exn_vis
; severity= High
; kind= None
; category= Prover }
| Missing_fld (fld, ml_loc)
-> let desc = Localise.verbatim_desc (Typ.Fieldname.to_full_string fld) in
{ name= IssueType.missing_fld
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Medium
; kind= None
; category= Nocat }
| Premature_nil_termination (desc, ml_loc)
-> { name= IssueType.premature_nil_termination
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Parameter_not_null_checked (desc, ml_loc)
-> { name= IssueType.parameter_not_null_checked
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= Some Kwarning
; category= Nocat }
| Precondition_not_found (desc, ml_loc)
-> { name= IssueType.precondition_not_found
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Precondition_not_met (desc, ml_loc)
-> { name= IssueType.precondition_not_met
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Medium
; kind= Some Kwarning
; category= Nocat }
(* always a warning *)
| Retain_cycle (_, desc, ml_loc)
-> { name= IssueType.retain_cycle
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Registered_observer_being_deallocated (desc, ml_loc)
-> { name= IssueType.registered_observer_being_deallocated
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Nocat }
| Return_expression_required (desc, ml_loc)
-> { name= IssueType.return_expression_required
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Stack_variable_address_escape (desc, ml_loc)
-> { name= IssueType.stack_variable_address_escape
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= Some Kerror
; category= Nocat }
| Return_statement_missing (desc, ml_loc)
-> { name= IssueType.return_statement_missing
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Return_value_ignored (desc, ml_loc)
-> { name= IssueType.return_value_ignored
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| SymOp.Analysis_failure_exe _
-> { name= IssueType.failure_exe
; description= Localise.no_desc
; ml_loc= None
; visibility= Exn_system
; severity= Low
; kind= None
; category= Nocat }
| Skip_function desc
-> { name= IssueType.skip_function
; description= desc
; ml_loc= None
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Skip_pointer_dereference (desc, ml_loc)
-> { name= IssueType.skip_pointer_dereference
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= Some Kinfo
; category= Nocat }
(* always an info *)
| Symexec_memory_error ml_loc
-> { name= IssueType.symexec_memory_error
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Uninitialized_value (desc, ml_loc)
-> { name= IssueType.uninitialized_value
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Unary_minus_applied_to_unsigned_expression (desc, ml_loc)
-> { name= IssueType.unary_minus_applied_to_unsigned_expression
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Unknown_proc
-> { name= IssueType.unknown_proc
; description= Localise.no_desc
; ml_loc= None
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| Unreachable_code_after (desc, ml_loc)
-> { name= IssueType.unreachable_code_after
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= Medium
; kind= None
; category= Nocat }
| Unsafe_guarded_by_access (desc, ml_loc)
-> { name= IssueType.unsafe_guarded_by_access
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Use_after_free (desc, ml_loc)
-> { name= IssueType.use_after_free
; description= desc
; ml_loc= Some ml_loc
; visibility= Exn_user
; severity= High
; kind= None
; category= Prover }
| Wrong_argument_number ml_loc
-> { name= IssueType.wrong_argument_number
; description= Localise.no_desc
; ml_loc= Some ml_loc
; visibility= Exn_developer
; severity= Low
; kind= None
; category= Nocat }
| exn
-> { name= IssueType.failure_exe
; description=
Localise.verbatim_desc (F.asprintf "%a: %s" Exn.pp exn (Caml.Printexc.get_backtrace ()))
; ml_loc= None
; visibility= Exn_system
; severity= Low
; kind= None
; category= Nocat }
(** print a description of the exception to the html output *)
let print_exception_html s exn =
let err_name, desc, ml_loc_opt, _, _, _, _ = recognize_exception exn in
let error = recognize_exception exn in
let ml_loc_string =
match ml_loc_opt with None -> "" | Some ml_loc -> " " ^ L.ml_loc_to_string ml_loc
match error.ml_loc with None -> "" | Some ml_loc -> " " ^ L.ml_loc_to_string ml_loc
in
let desc_str = F.asprintf "%a" Localise.pp_error_desc desc in
L.d_strln_color Red (s ^ err_name.IssueType.unique_id ^ " " ^ desc_str ^ ml_loc_string)
let desc_str = F.asprintf "%a" Localise.pp_error_desc error.description in
L.d_strln_color Red (s ^ error.name.IssueType.unique_id ^ " " ^ desc_str ^ ml_loc_string)
(** string describing an error kind *)
let err_kind_string = function
@ -413,5 +698,5 @@ let pp_err ~node_key loc ekind ex_name desc ml_loc_opt fmt () =
(** Return true if the exception is not serious and should be handled in timeout mode *)
let handle_exception exn =
let _, _, _, visibility, _, _, _ = recognize_exception exn in
equal_visibility visibility Exn_user || equal_visibility visibility Exn_developer
let error = recognize_exception exn in
equal_visibility error.visibility Exn_user || equal_visibility error.visibility Exn_developer

@ -166,14 +166,13 @@ val pp_err :
-> Logging.ml_loc option -> Format.formatter -> unit -> unit
(** pretty print an error *)
val recognize_exception :
exn
-> IssueType.t
* Localise.error_desc
* Logging.ml_loc option
* visibility
* severity
* err_kind option
* err_class
(** Turn an exception into an error name, error description,
location in ml source, and category *)
type t =
{ name: IssueType.t
; description: Localise.error_desc
; ml_loc: Logging.ml_loc option (** location in the infer source code *)
; visibility: visibility
; severity: severity
; kind: err_kind option
; category: err_class }
val recognize_exception : exn -> t

@ -600,8 +600,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
in
let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
let address_struct_id =
try get_coordinate_id (List.hd_exn (List.filter ~f:(is_source_node_of_exp e) nodes_e))
with exn when SymOp.exn_not_failure exn -> assert false
get_coordinate_id (List.hd_exn (List.filter ~f:(is_source_node_of_exp e) nodes_e))
in
(* we need to exclude the address node from the sorce of fields. no fields should start from there*)
let nl' = List.filter ~f:(fun id -> address_struct_id <> id) nl in

@ -158,9 +158,7 @@ let path_set_checkout_todo (wl: Worklist.t) (node: Procdesc.Node.t) : Paths.Path
let visited = Hashtbl.find wl.Worklist.path_set_visited node_id in
let new_visited = Paths.PathSet.union visited todo in
Hashtbl.replace wl.Worklist.path_set_visited node_id new_visited ; todo
with Not_found ->
L.internal_error "@\n@\nERROR: could not find todo for node %a@\n@." Procdesc.Node.pp node ;
assert false
with Not_found -> L.die InternalError "could not find todo for node %a" Procdesc.Node.pp node
(* =============== END of the edge_set object =============== *)
@ -444,8 +442,11 @@ let forward_tabulate tenv proc_cfg wl =
propagate_nodes_divergence tenv proc_cfg pset normal_succ_nodes exn_succ_nodes wl ;
L.d_decrease_indent 1 ;
L.d_ln ()
with exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn exn ; L.d_decrease_indent 1 ; L.d_ln ()
with exn ->
let backtrace = Caml.Printexc.get_raw_backtrace () in
if Exceptions.handle_exception exn && !Config.footprint then (
handle_exn exn ; L.d_decrease_indent 1 ; L.d_ln () )
else reraise ~backtrace exn
in
let do_node curr_node pathset_todo session handle_exn =
check_prop_size pathset_todo ;
@ -471,11 +472,14 @@ let forward_tabulate tenv proc_cfg wl =
do_node curr_node pathset_todo session handle_exn ;
if !handle_exn_called then Printer.force_delayed_prints () ;
do_after_node curr_node
with exn when Exceptions.handle_exception exn ->
handle_exn_node curr_node exn ;
Printer.force_delayed_prints () ;
do_after_node curr_node ;
if not !Config.footprint then raise RE_EXE_ERROR
with exn ->
let backtrace = Caml.Printexc.get_raw_backtrace () in
if Exceptions.handle_exception exn then (
handle_exn_node curr_node exn ;
Printer.force_delayed_prints () ;
do_after_node curr_node ;
if not !Config.footprint then raise RE_EXE_ERROR )
else reraise ~backtrace exn
in
while not (Worklist.is_empty wl) do
let curr_node = Worklist.remove wl in
@ -720,7 +724,7 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * Specs.Visitedset
compute_visited !vset_ref
in
(do_join_post pname tenv pathset, visited)
with exn when match exn with Exceptions.Leak _ -> true | _ -> false ->
with Exceptions.Leak _ ->
L.d_strln "Leak in post collection" ;
assert false
in
@ -1266,9 +1270,9 @@ let perform_transition proc_cfg tenv proc_name =
Config.allow_leak := allow_leak ;
L.(debug Analysis Medium)
"Error in collect_preconditions for %a@." Typ.Procname.pp proc_name ;
let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let err_str = "exception raised " ^ err_name.IssueType.unique_id in
L.(debug Analysis Medium) "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt ; []
let error = Exceptions.recognize_exception exn in
let err_str = "exception raised " ^ error.name.IssueType.unique_id in
L.(debug Analysis Medium) "Error: %s %a@." err_str L.pp_ml_loc_opt error.ml_loc ; []
in
transition_footprint_re_exe tenv proc_name joined_pres
in

@ -350,8 +350,7 @@ let pp_prop pe0 f prop =
(* print in html mode *)
F.fprintf f "%a%a%a" Io_infer.Html.pp_start_color Pp.Blue do_print ()
Io_infer.Html.pp_end_color ()
else do_print f ()
(** print in text mode *)
else (* print in text mode *) do_print f ()
let pp_prop_with_typ pe f p = pp_prop {pe with opt= SIM_WITH_TYP} f p

@ -26,10 +26,7 @@ let log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr ?linters_
match session with None -> (State.get_session () :> int) | Some session -> session
in
let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in
let issue_type =
let err_name, _, _, _, _, _, _ = Exceptions.recognize_exception exn in
err_name
in
let issue_type = (Exceptions.recognize_exception exn).name in
if not Config.filtering (* no-filtering takes priority *) || issue_type.IssueType.enabled then
Errlog.log_issue err_kind err_log loc node_id session ltr ?linters_def_file ?doc_url exn

@ -318,9 +318,9 @@ let process_execution_failures (log_issue: log_issue) pname =
(* L.out "Node:%a node_ok:%d node_fail:%d@." Procdesc.Node.pp node fs.node_ok fs.node_fail; *)
match (fs.node_ok, fs.first_failure) with
| 0, Some (loc, key, _, loc_trace, exn) when not Config.debug_exceptions
-> let ex_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let desc' = Localise.verbatim_desc ("exception: " ^ ex_name.IssueType.unique_id) in
let exn' = Exceptions.Analysis_stops (desc', ml_loc_opt) in
-> let error = Exceptions.recognize_exception exn in
let desc' = Localise.verbatim_desc ("exception: " ^ error.name.IssueType.unique_id) in
let exn' = Exceptions.Analysis_stops (desc', error.ml_loc) in
log_issue pname ~loc ~node_id:key ~ltr:loc_trace exn'
| _
-> ()

@ -1400,14 +1400,17 @@ and instrs ?(mask_errors= false) tenv pdesc instrs ppl =
Sil.d_instr instr ;
L.d_ln () ;
try sym_exec tenv pdesc instr p path
with exn when SymOp.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 " ^ L.ml_loc_to_string ml_loc | None -> ""
in
L.d_warning ("Generated Instruction Failed with: " ^ err_name.IssueType.unique_id ^ loc) ;
L.d_ln () ;
[(p, path)]
with exn ->
let backtrace = Caml.Printexc.get_raw_backtrace () in
if SymOp.exn_not_failure exn && mask_errors then
let error = Exceptions.recognize_exception exn in
let loc =
match error.ml_loc with Some ml_loc -> "at " ^ L.ml_loc_to_string ml_loc | None -> ""
in
L.d_warning ("Generated Instruction Failed with: " ^ error.name.IssueType.unique_id ^ loc) ;
L.d_ln () ;
[(p, path)]
else reraise ~backtrace exn
in
let f plist instr = List.concat_map ~f:(exe_instr instr) plist in
List.fold ~f ~init:ppl instrs
@ -1800,9 +1803,12 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t),
L.d_ln () ;
State.mark_instr_ok () ;
Paths.PathSet.from_renamed_list results
with exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn exn ; (* calls State.mark_instr_fail *)
Paths.PathSet.empty
with exn ->
let backtrace = Caml.Printexc.get_raw_backtrace () in
if Exceptions.handle_exception exn && !Config.footprint then (
handle_exn exn ; (* calls State.mark_instr_fail *)
Paths.PathSet.empty )
else reraise ~backtrace exn
(** {2 Lifted Abstract Transfer Functions} *)

Loading…
Cancel
Save