From e02f6ab39f312ea2ebf955a7a435e7162977827e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 22 Sep 2017 06:06:32 -0700 Subject: [PATCH] [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 --- infer/src/IR/Errlog.ml | 32 +- infer/src/IR/Exceptions.ml | 729 +++++++++++++++++++++++---------- infer/src/IR/Exceptions.mli | 21 +- infer/src/backend/dotty.ml | 3 +- infer/src/backend/interproc.ml | 32 +- infer/src/backend/prop.ml | 3 +- infer/src/backend/reporting.ml | 5 +- infer/src/backend/state.ml | 6 +- infer/src/backend/symExec.ml | 28 +- 9 files changed, 574 insertions(+), 285 deletions(-) diff --git a/infer/src/IR/Errlog.ml b/infer/src/IR/Errlog.ml index b831b00e0..006502a89 100644 --- a/infer/src/IR/Errlog.ml +++ b/infer/src/IR/Errlog.ml @@ -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 diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 7035c286b..419f19f12 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -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 diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 66f607d3b..c2d382cf8 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -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 diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index ac45336ab..945724abd 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -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 diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index a18c0e306..c7b2497bc 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -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 diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 90ef2956a..a474f0b6e 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -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 diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index 06b870ba7..a011e93c1 100644 --- a/infer/src/backend/reporting.ml +++ b/infer/src/backend/reporting.ml @@ -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 diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 39304619a..669eced37 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -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' | _ -> () diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 79f82c8d7..f6504603a 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -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} *)