From 2a926d8294e085dec49572fa10ce9a9d6a57ffff Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 11 Feb 2016 06:58:37 -0800 Subject: [PATCH] Remove uses of assert false to get original ml location. Reviewed By: jvillard, jberdine Differential Revision: D2922516 fb-gh-sync-id: 153a2dd shipit-source-id: 153a2dd --- infer/lib/python/inferlib/issues.py | 15 +- infer/src/backend/abs.ml | 5 +- infer/src/backend/errlog.ml | 27 ++- infer/src/backend/errlog.mli | 2 +- infer/src/backend/exceptions.ml | 361 ++++++++++++++++------------ infer/src/backend/exceptions.mli | 84 +++---- infer/src/backend/fork.ml | 2 +- infer/src/backend/inferprint.ml | 8 +- infer/src/backend/interproc.ml | 11 +- infer/src/backend/jsonbug.atd | 5 +- infer/src/backend/logging.ml | 4 +- infer/src/backend/logging.mli | 2 +- infer/src/backend/prop.ml | 2 +- infer/src/backend/prop.mli | 2 +- infer/src/backend/prover.ml | 18 +- infer/src/backend/rearrange.ml | 55 ++--- infer/src/backend/state.ml | 4 +- infer/src/backend/symExec.ml | 113 +++++---- infer/src/backend/tabulation.ml | 60 ++--- infer/src/backend/tabulation.mli | 2 +- infer/src/backend/utils.ml | 24 +- infer/src/backend/utils.mli | 13 +- infer/src/clang/cFrontend_errors.ml | 3 +- infer/src/eradicate/modelTables.ml | 3 +- infer/src/eradicate/modelTables.mli | 4 +- infer/src/eradicate/typeOrigin.ml | 2 +- 26 files changed, 452 insertions(+), 379 deletions(-) diff --git a/infer/lib/python/inferlib/issues.py b/infer/lib/python/inferlib/issues.py index 5600c6d3b..47368d262 100644 --- a/infer/lib/python/inferlib/issues.py +++ b/infer/lib/python/inferlib/issues.py @@ -95,8 +95,10 @@ JSON_INDEX_TRACE_NODE_TAGS_TAG = 'tags' JSON_INDEX_TRACE_NODE_TAGS_VALUE = 'value' JSON_INDEX_INFER_SOURCE_LOC = 'infer_source_loc' JSON_INDEX_ISL_FILE = 'file' -JSON_INDEX_ISL_LINE = 'line' -JSON_INDEX_ISL_COLUMN = 'column' +JSON_INDEX_ISL_LNUM = 'lnum' +JSON_INDEX_ISL_CNUM = 'cnum' +JSON_INDEX_ISL_ENUM = 'enum' + QUALIFIER_TAGS = 'qualifier_tags' BUCKET_TAGS = 'bucket' @@ -143,14 +145,15 @@ def clean_json(args, json_report): utils.dump_json_to_path(rows, temporary_file) shutil.move(temporary_file, json_report) - def _text_of_infer_loc(loc): - return u' (%s:%d:%d)' % ( + return u' (%s:%d:%d-%d:)' % ( loc[JSON_INDEX_ISL_FILE], - loc[JSON_INDEX_ISL_LINE], - loc[JSON_INDEX_ISL_COLUMN], + loc[JSON_INDEX_ISL_LNUM], + loc[JSON_INDEX_ISL_CNUM], + loc[JSON_INDEX_ISL_ENUM], ) + def text_of_report(report): filename = report[JSON_INDEX_FILENAME] kind = report[JSON_INDEX_KIND] diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index f47155803..658b918e3 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1298,14 +1298,13 @@ let check_junk ?original_prop pname tenv prop = let desc = Errdesc.explain_retain_cycle (remove_opt original_prop) cycle (State.get_loc ()) cycle_dotty in Exceptions.Retain_cycle - (remove_opt original_prop, hpred, desc, - try assert false with Assert_failure x -> x) in + (remove_opt original_prop, hpred, desc, __POS__) in let exn_leak = Exceptions.Leak (fp_part, prop, hpred, Errdesc.explain_leak tenv hpred prop alloc_attribute ml_bucket_opt, !Absarray.array_abstraction_performed, resource, - try assert false with Assert_failure x -> x) in + __POS__) in let ignore_resource, exn = (match alloc_attribute, resource with | Some _, Sil.Rmemory Sil.Mobjc when (hpred_in_cycle hpred) -> diff --git a/infer/src/backend/errlog.ml b/infer/src/backend/errlog.ml index 1aba5770b..078ed9ae2 100644 --- a/infer/src/backend/errlog.ml +++ b/infer/src/backend/errlog.ml @@ -24,12 +24,12 @@ type loc_trace = loc_trace_elem list (** Data associated to a specific error *) type err_data = - (int * int) * int * Location.t * ml_location option * loc_trace * + (int * int) * int * Location.t * ml_loc option * loc_trace * Prop.normal Prop.t option * Exceptions.err_class let err_data_compare - ((nodeid1, key1), session1, loc1, mloco1, ltr1, po1, ec1) - ((nodeid2, key2), session2, loc2, mloco2, ltr2, po2, ec2) = + ((nodeid1, key1), session1, loc1, ml_loc_opt1, ltr1, po1, ec1) + ((nodeid2, key2), session2, loc2, ml_loc_opt2, ltr2, po2, ec2) = Location.compare loc1 loc2 module ErrDataSet = (* set err_data with no repeated loc *) @@ -66,7 +66,7 @@ let empty () = ErrLogHash.create 13 type iter_fun = (int * int) -> Location.t -> - ml_location option -> + ml_loc option -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> string -> @@ -79,9 +79,9 @@ type iter_fun = let iter (f: iter_fun) (err_log: t) = ErrLogHash.iter (fun (ekind, in_footprint, err_name, desc, severity) set -> ErrDataSet.iter - (fun (node_id_key, section, loc, mloco, ltr, pre_opt, eclass) -> + (fun (node_id_key, section, loc, ml_loc_opt, ltr, pre_opt, eclass) -> f - node_id_key loc mloco ekind in_footprint err_name + node_id_key loc ml_loc_opt ekind in_footprint err_name desc severity ltr pre_opt eclass) set) err_log @@ -110,7 +110,8 @@ let pp_warnings fmt (errlog : t) = (** Print an error log in html format *) let pp_html path_to_root fmt (errlog: t) = let pp_eds fmt eds = - let pp_nodeid_session_loc fmt ((nodeid, nodekey), session, loc, mloco, ltr, pre_opt, eclass) = + let pp_nodeid_session_loc + fmt ((nodeid, nodekey), session, loc, ml_loc_opt, ltr, pre_opt, eclass) = Io_infer.Html.pp_session_link path_to_root fmt (nodeid, session, loc.Location.line) in ErrDataSet.iter (pp_nodeid_session_loc fmt) eds in let f do_fp ek (ekind, infp, err_name, desc, severity) eds = @@ -167,7 +168,7 @@ let update errlog_old errlog_new = let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn = - let err_name, desc, mloco, visibility, severity, force_kind, eclass = + let err_name, desc, ml_loc_opt, visibility, severity, force_kind, eclass = Exceptions.recognize_exception exn in let ekind = match force_kind with | Some ekind -> ekind @@ -188,14 +189,14 @@ let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn = let added = add_issue err_log (ekind, !Config.footprint, err_name, desc, severity_to_str severity) - (ErrDataSet.singleton (node_id_key, session, loc, mloco, ltr, pre_opt, eclass)) in + (ErrDataSet.singleton (node_id_key, session, loc, ml_loc_opt, ltr, pre_opt, eclass)) in let should_print_now = match exn with | Exceptions.Internal_error _ -> true | _ -> added in let print_now () = - let ex_name, desc, mloco, _, _, _, _ = Exceptions.recognize_exception exn in - L.err "%a@?" (Exceptions.pp_err node_id_key loc ekind ex_name desc mloco) (); + let ex_name, desc, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in + L.err "%a@?" (Exceptions.pp_err node_id_key loc ekind ex_name desc ml_loc_opt) (); if _ekind <> Exceptions.Kerror then begin let warn_str = let pp fmt () = @@ -265,9 +266,9 @@ module Err_table = struct ErrDataSet.iter (fun loc -> add_err loc err_name) eds in ErrLogHash.iter f err_table; - let pp ekind (nodeidkey, session, loc, mloco, ltr, pre_opt, eclass) fmt err_names = + let pp ekind (nodeidkey, session, loc, ml_loc_opt, ltr, pre_opt, eclass) fmt err_names = IList.iter (fun (err_name, desc) -> - Exceptions.pp_err nodeidkey loc ekind err_name desc mloco fmt ()) err_names in + Exceptions.pp_err nodeidkey loc ekind err_name desc ml_loc_opt fmt ()) err_names in F.fprintf fmt "@.Detailed errors during footprint phase:@."; LocMap.iter (fun nslm err_names -> F.fprintf fmt "%a" (pp Exceptions.Kerror nslm) err_names) !map_err_fp; diff --git a/infer/src/backend/errlog.mli b/infer/src/backend/errlog.mli index 02de59646..0ffd9a651 100644 --- a/infer/src/backend/errlog.mli +++ b/infer/src/backend/errlog.mli @@ -32,7 +32,7 @@ val empty : unit -> t type iter_fun = (int * int) -> Location.t -> - ml_location option -> + ml_loc option -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> string -> diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index d974c656e..fca032bed 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -29,56 +29,62 @@ type err_class = Checker | Prover | Nocat type err_kind = Kwarning | Kerror | Kinfo -exception Abduction_case_not_implemented of ml_location -exception Analysis_stops of Localise.error_desc * ml_location option -exception Array_out_of_bounds_l1 of Localise.error_desc * ml_location -exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location -exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location -exception Array_of_pointsto of ml_location -exception Bad_footprint of ml_location -exception Bad_pointer_comparison of Localise.error_desc * ml_location -exception Class_cast_exception of Localise.error_desc * ml_location +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 Codequery of Localise.error_desc -exception Comparing_floats_for_equality of Localise.error_desc * ml_location -exception Condition_is_assignment of Localise.error_desc * ml_location -exception Condition_always_true_false of Localise.error_desc * bool * ml_location -exception Context_leak of Localise.error_desc * ml_location +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 Custom_error of string * Localise.error_desc -exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_location +exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * 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_location -exception Divide_by_zero of Localise.error_desc * ml_location +exception Deallocation_mismatch of Localise.error_desc * ml_loc +exception Divide_by_zero of Localise.error_desc * ml_loc exception Eradicate of string * Localise.error_desc -exception Field_not_null_checked of Localise.error_desc * ml_location -exception Frontend_warning of string * Localise.error_desc * ml_location +exception Field_not_null_checked of Localise.error_desc * ml_loc +exception Frontend_warning of string * Localise.error_desc * 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_location -exception Missing_fld of Ident.fieldname * ml_location -exception Premature_nil_termination of Localise.error_desc * ml_location -exception Null_dereference of Localise.error_desc * ml_location -exception Null_test_after_dereference of Localise.error_desc * ml_location -exception Parameter_not_null_checked of Localise.error_desc * ml_location -exception Pointer_size_mismatch of Localise.error_desc * ml_location -exception Precondition_not_found of Localise.error_desc * ml_location -exception Precondition_not_met of Localise.error_desc * ml_location -exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_location -exception Return_expression_required of Localise.error_desc * ml_location -exception Return_statement_missing of Localise.error_desc * ml_location -exception Return_value_ignored of Localise.error_desc * ml_location +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 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 exception Skip_function of Localise.error_desc -exception Skip_pointer_dereference of Localise.error_desc * ml_location -exception Stack_variable_address_escape of Localise.error_desc * ml_location -exception Symexec_memory_error of ml_location -exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_location -exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_location -exception Uninitialized_value of Localise.error_desc * ml_location +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 Unknown_proc -exception Use_after_free of Localise.error_desc * ml_location -exception Wrong_argument_number of ml_location +exception Use_after_free of Localise.error_desc * ml_loc +exception Wrong_argument_number of ml_loc + + +let file_line_column_string (file, line, column) = + Printf.sprintf "file %s line %d column %d" file line column (** Turn an exception into a descriptive string, error description, location in ml source, and category *) let recognize_exception exn = @@ -87,161 +93,220 @@ 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, mloco, visibility, severity, force_kind, eclass = match exn with (* all the names of Exn_user errors must be defined in Localise *) - | Abduction_case_not_implemented mloc -> - (Localise.from_string "Abduction_case_not_implemented", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat) + let err_name, desc, (ml_loc_opt : 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", + Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) | Context_leak (desc, _) -> - (Localise.context_leak, desc, None, Exn_user, High, None, Nocat) - | Analysis_stops (desc, mloco) -> + (Localise.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 - (Localise.analysis_stops, desc, mloco, visibility, Medium, None, Nocat) - | Array_of_pointsto mloc -> - (Localise.from_string "Array_of_pointsto", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat) - | Array_out_of_bounds_l1 (desc, mloc) -> - (Localise.array_out_of_bounds_l1, desc, Some mloc, Exn_user, High, Some Kerror, Checker) - | Array_out_of_bounds_l2 (desc, mloc) -> - (Localise.array_out_of_bounds_l2, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Array_out_of_bounds_l3 (desc, mloc) -> - (Localise.array_out_of_bounds_l3, desc, Some mloc, Exn_developer, Medium, None, Nocat) - | Assert_failure mloc -> - (Localise.from_string "Assert_failure", Localise.no_desc, Some mloc, Exn_developer, High, None, Nocat) - | Bad_pointer_comparison (desc, mloc) -> - (Localise.bad_pointer_comparison, desc, Some mloc, Exn_user, High, Some Kerror, Prover) - | Bad_footprint mloc -> - (Localise.from_string "Bad_footprint", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat) - | Prop.Cannot_star mloc -> - (Localise.from_string "Cannot_star", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat) - | Class_cast_exception (desc, mloc) -> - (Localise.class_cast_exception, desc, Some mloc, Exn_user, High, None, Prover) + (Localise.analysis_stops, desc, ml_loc_opt, visibility, Medium, None, Nocat) + | Array_of_pointsto ml_loc -> + (Localise.from_string "Array_of_pointsto", + Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) + | Array_out_of_bounds_l1 (desc, ml_loc) -> + (Localise.array_out_of_bounds_l1, + desc, Some ml_loc, Exn_user, High, Some Kerror, Checker) + | Array_out_of_bounds_l2 (desc, ml_loc) -> + (Localise.array_out_of_bounds_l2, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) + | Array_out_of_bounds_l3 (desc, ml_loc) -> + (Localise.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 + (Localise.from_string "Assert_failure", + Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat) + | Bad_pointer_comparison (desc, ml_loc) -> + (Localise.bad_pointer_comparison, + desc, Some ml_loc, Exn_user, High, Some Kerror, Prover) + | Bad_footprint ml_loc -> + (Localise.from_string "Bad_footprint", + Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) + | Prop.Cannot_star ml_loc -> + (Localise.from_string "Cannot_star", + Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) + | Class_cast_exception (desc, ml_loc) -> + (Localise.class_cast_exception, + desc, Some ml_loc, Exn_user, High, None, Prover) | Codequery desc -> - (Localise.from_string "Codequery", desc, None, Exn_user, High, None, Prover) - | Comparing_floats_for_equality(desc, mloc) -> - (Localise.comparing_floats_for_equality, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Condition_always_true_false (desc, b, mloc) -> - let name = if b then Localise.condition_always_true else Localise.condition_always_false in - (name, desc, Some mloc, Exn_user, Medium, None, Nocat) + (Localise.from_string "Codequery", + desc, None, Exn_user, High, None, Prover) + | Comparing_floats_for_equality(desc, ml_loc) -> + (Localise.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 Localise.condition_always_true + else Localise.condition_always_false in + (name, desc, Some ml_loc, Exn_user, Medium, None, Nocat) | Custom_error (error_msg, desc) -> - (Localise.from_string error_msg, desc, None, Exn_user, High, None, Checker) - | Condition_is_assignment(desc, mloc) -> - (Localise.condition_is_assignment, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Dangling_pointer_dereference (dko, desc, mloc) -> + (Localise.from_string error_msg, + desc, None, Exn_user, High, None, Checker) + | Condition_is_assignment(desc, ml_loc) -> + (Localise.condition_is_assignment, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) + | Dangling_pointer_dereference (dko, desc, ml_loc) -> let visibility = match dko with | Some dk -> Exn_user (* only show to the user if the category was identified *) | None -> Exn_developer in - (Localise.dangling_pointer_dereference, desc, Some mloc, visibility, High, None, Prover) + (Localise.dangling_pointer_dereference, + desc, Some ml_loc, visibility, High, None, Prover) | Deallocate_stack_variable desc -> - (Localise.deallocate_stack_variable, desc, None, Exn_user, High, None, Prover) + (Localise.deallocate_stack_variable, + desc, None, Exn_user, High, None, Prover) | Deallocate_static_memory desc -> - (Localise.deallocate_static_memory, desc, None, Exn_user, High, None, Prover) - | Deallocation_mismatch (desc, mloc) -> - (Localise.deallocation_mismatch, desc, Some mloc, Exn_user, High, None, Prover) - | Divide_by_zero (desc, mloc) -> - (Localise.divide_by_zero, desc, Some mloc, Exn_user, High, Some Kerror, Checker) + (Localise.deallocate_static_memory, + desc, None, Exn_user, High, None, Prover) + | Deallocation_mismatch (desc, ml_loc) -> + (Localise.deallocation_mismatch, + desc, Some ml_loc, Exn_user, High, None, Prover) + | Divide_by_zero (desc, ml_loc) -> + (Localise.divide_by_zero, + desc, Some ml_loc, Exn_user, High, Some Kerror, Checker) | Eradicate (kind_s, desc) -> (Localise.from_string kind_s, desc, None, Exn_user, High, None, Prover) - | Field_not_null_checked (desc, mloc) -> - (Localise.field_not_null_checked, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat) - | Frontend_warning (name, desc, mloc) -> - (Localise.from_string name, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat) + | Field_not_null_checked (desc, ml_loc) -> + (Localise.field_not_null_checked, + desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) + | Frontend_warning (name, desc, ml_loc) -> + (Localise.from_string name, + desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) | Checkers (kind_s, desc) -> - (Localise.from_string kind_s, desc, None, Exn_user, High, None, Prover) - | Null_dereference (desc, mloc) -> - (Localise.null_dereference, desc, Some mloc, Exn_user, High, None, Prover) - | Null_test_after_dereference (desc, mloc) -> - (Localise.null_test_after_dereference, desc, Some mloc, Exn_user, High, None, Nocat) - | Pointer_size_mismatch (desc, mloc) -> - (Localise.pointer_size_mismatch, desc, Some mloc, Exn_user, High, Some Kerror, Checker) + (Localise.from_string kind_s, + desc, None, Exn_user, High, None, Prover) + | Null_dereference (desc, ml_loc) -> + (Localise.null_dereference, + desc, Some ml_loc, Exn_user, High, None, Prover) + | Null_test_after_dereference (desc, ml_loc) -> + (Localise.null_test_after_dereference, + desc, Some ml_loc, Exn_user, High, None, Nocat) + | Pointer_size_mismatch (desc, ml_loc) -> + (Localise.pointer_size_mismatch, + desc, Some ml_loc, Exn_user, High, Some Kerror, Checker) | Inherently_dangerous_function desc -> - (Localise.inherently_dangerous_function, desc, None, Exn_developer, Medium, None, Nocat) + (Localise.inherently_dangerous_function, + desc, None, Exn_developer, Medium, None, Nocat) | Internal_error desc -> - (Localise.from_string "Internal_error", desc, None, Exn_developer, High, None, Nocat) + (Localise.from_string "Internal_error", + desc, None, Exn_developer, High, None, Nocat) | Invalid_argument s -> let desc = Localise.verbatim_desc s in (Localise.from_string "Invalid_argument", desc, None, Exn_system, Low, None, Nocat) | Java_runtime_exception (exn_name, pre_str, desc) -> let exn_str = Typename.name exn_name in (Localise.from_string exn_str, desc, None, Exn_user, High, None, Prover) - | Leak (fp_part, _, _, (exn_vis, error_desc), done_array_abstraction, resource, mloc) -> + | Leak (fp_part, _, _, (exn_vis, error_desc), done_array_abstraction, resource, ml_loc) -> if done_array_abstraction - then (Localise.from_string "Leak_after_array_abstraction", error_desc, Some mloc, Exn_developer, High, None, Prover) + then (Localise.from_string "Leak_after_array_abstraction", + error_desc, Some ml_loc, Exn_developer, High, None, Prover) else if fp_part - then (Localise.from_string "Leak_in_footprint", error_desc, Some mloc, Exn_developer, High, None, Prover) + then (Localise.from_string "Leak_in_footprint", + error_desc, Some ml_loc, Exn_developer, High, None, Prover) else let loc_str = match resource with | Sil.Rmemory _ -> Localise.memory_leak | Sil.Rfile -> Localise.resource_leak | Sil.Rlock -> Localise.resource_leak | Sil.Rignore -> Localise.memory_leak in - (loc_str, error_desc, Some mloc, exn_vis, High, None, Prover) - | Match_failure mloc -> - (Localise.from_string "Match failure", Localise.no_desc, Some mloc, Exn_developer, High, None, Nocat) - | Missing_fld (fld, mloc) -> + (loc_str, error_desc, Some ml_loc, exn_vis, High, None, Prover) + | Match_failure (f, l, c) -> + let ml_loc = (f, l, c, c) in + (Localise.from_string "Match failure", + Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat) + | Missing_fld (fld, ml_loc) -> let desc = Localise.verbatim_desc (Ident.fieldname_to_string fld) in - (Localise.from_string "Missing_fld", desc, Some mloc, Exn_developer, Medium, None, Nocat) - | Premature_nil_termination (desc, mloc) -> - (Localise.premature_nil_termination, desc, Some mloc, Exn_user, High, None, Prover) + (Localise.from_string "Missing_fld", desc, Some ml_loc, Exn_developer, Medium, None, Nocat) + | Premature_nil_termination (desc, ml_loc) -> + (Localise.premature_nil_termination, + desc, Some ml_loc, Exn_user, High, None, Prover) | Not_found -> - (Localise.from_string "Not_found", Localise.no_desc, None, Exn_system, Low, None, Nocat) - | Parameter_not_null_checked (desc, mloc) -> - (Localise.parameter_not_null_checked, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat) - | Precondition_not_found (desc, mloc) -> - (Localise.precondition_not_found, desc, Some mloc, Exn_developer, Low, None, Nocat) - | Precondition_not_met (desc, mloc) -> - (Localise.precondition_not_met, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat) (** always a warning *) - | Retain_cycle (prop, hpred, desc, mloc) -> - (Localise.retain_cycle, desc, Some mloc, Exn_user, High, None, Prover) - | Return_expression_required (desc, mloc) -> - (Localise.return_expression_required, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Stack_variable_address_escape (desc, mloc) -> - (Localise.stack_variable_address_escape, desc, Some mloc, Exn_user, High, Some Kerror, Nocat) - | Return_statement_missing (desc, mloc) -> - (Localise.return_statement_missing, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Return_value_ignored (desc, mloc) -> - (Localise.return_value_ignored, desc, Some mloc, Exn_user, Medium, None, Nocat) + (Localise.from_string "Not_found", + Localise.no_desc, None, Exn_system, Low, None, Nocat) + | Parameter_not_null_checked (desc, ml_loc) -> + (Localise.parameter_not_null_checked, + desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) + | Precondition_not_found (desc, ml_loc) -> + (Localise.precondition_not_found, + desc, Some ml_loc, Exn_developer, Low, None, Nocat) + | Precondition_not_met (desc, ml_loc) -> + (Localise.precondition_not_met, + desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) (** always a warning *) + | Retain_cycle (prop, hpred, desc, ml_loc) -> + (Localise.retain_cycle, + desc, Some ml_loc, Exn_user, High, None, Prover) + | Return_expression_required (desc, ml_loc) -> + (Localise.return_expression_required, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) + | Stack_variable_address_escape (desc, ml_loc) -> + (Localise.stack_variable_address_escape, + desc, Some ml_loc, Exn_user, High, Some Kerror, Nocat) + | Return_statement_missing (desc, ml_loc) -> + (Localise.return_statement_missing, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) + | Return_value_ignored (desc, ml_loc) -> + (Localise.return_value_ignored, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) | Analysis_failure_exe _ -> - (Localise.from_string "Failure_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat) + (Localise.from_string "Failure_exe", + Localise.no_desc, None, Exn_system, Low, None, Nocat) | Skip_function desc -> (Localise.skip_function, desc, None, Exn_developer, Low, None, Nocat) - | Skip_pointer_dereference (desc, mloc) -> - (Localise.skip_pointer_dereference, desc, Some mloc, Exn_user, Medium, Some Kinfo, Nocat) (** always an info *) - | Symexec_memory_error mloc -> - (Localise.from_string "Symexec_memory_error", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat) + | Skip_pointer_dereference (desc, ml_loc) -> + (Localise.skip_pointer_dereference, + desc, Some ml_loc, Exn_user, Medium, Some Kinfo, Nocat) (** always an info *) + | Symexec_memory_error ml_loc -> + (Localise.from_string "Symexec_memory_error", + Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) | Sys_error s -> let desc = Localise.verbatim_desc s in - (Localise.from_string "Sys_error", desc, None, Exn_system, Low, None, Nocat) - | Tainted_value_reaching_sensitive_function (desc, mloc) -> - (Localise.tainted_value_reaching_sensitive_function, desc, Some mloc, - Exn_user, Medium, Some Kerror, Nocat) + (Localise.from_string "Sys_error", + desc, None, Exn_system, Low, None, Nocat) + | Tainted_value_reaching_sensitive_function (desc, ml_loc) -> + (Localise.tainted_value_reaching_sensitive_function, + desc, Some ml_loc, Exn_user, Medium, Some Kerror, Nocat) | Unix.Unix_error (_, s1, s2) -> let desc = Localise.verbatim_desc (s1 ^ s2) in - (Localise.from_string "Unix_error", desc, None, Exn_system, Low, None, Nocat) - | Uninitialized_value (desc, mloc) -> - (Localise.uninitialized_value, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Unary_minus_applied_to_unsigned_expression(desc, mloc) -> - (Localise.unary_minus_applied_to_unsigned_expression, desc, Some mloc, Exn_user, Medium, None, Nocat) + (Localise.from_string "Unix_error", + desc, None, Exn_system, Low, None, Nocat) + | Uninitialized_value (desc, ml_loc) -> + (Localise.uninitialized_value, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) + | Unary_minus_applied_to_unsigned_expression(desc, ml_loc) -> + (Localise.unary_minus_applied_to_unsigned_expression, + desc, Some ml_loc, Exn_user, Medium, None, Nocat) | Unknown_proc -> - (Localise.from_string "Unknown_proc", Localise.no_desc, None, Exn_developer, Low, None, Nocat) - | Use_after_free (desc, mloc) -> - (Localise.use_after_free, desc, Some mloc, Exn_user, High, None, Prover) - | Wrong_argument_number mloc -> - (Localise.from_string "Wrong_argument_number", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat) + (Localise.from_string "Unknown_proc", + Localise.no_desc, None, Exn_developer, Low, None, Nocat) + | Use_after_free (desc, ml_loc) -> + (Localise.use_after_free, + desc, Some ml_loc, Exn_user, High, None, Prover) + | Wrong_argument_number ml_loc -> + (Localise.from_string "Wrong_argument_number", + Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) | Failure _ as f -> raise f | exn -> let exn_name = Printexc.to_string exn in - (Localise.from_string exn_name, Localise.no_desc, None, Exn_developer, Low, None, Nocat) in + (Localise.from_string exn_name, + Localise.no_desc, None, Exn_developer, Low, None, Nocat) in let visibility' = - if visibility = Exn_user && filter_out_bucket desc then Exn_developer else visibility in - (err_name, desc, mloco, visibility', severity, force_kind, eclass) + if visibility = Exn_user && filter_out_bucket desc + then Exn_developer + else visibility in + (err_name, desc, ml_loc_opt, visibility', severity, force_kind, eclass) (** print a description of the exception to the html output *) let print_exception_html s exn = - let err_name, desc, mloco, _, _, _, _ = recognize_exception exn in - let mloc_string = match mloco with + let err_name, desc, ml_loc_opt, _, _, _, _ = recognize_exception exn in + let ml_loc_string = match ml_loc_opt with | None -> "" - | Some mloc -> " " ^ ml_location_string mloc in + | Some ml_loc -> " " ^ 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 ^ mloc_string) + (L.d_strln_color Red) (s ^ (Localise.to_string err_name) ^ " " ^ desc_str ^ ml_loc_string) (** string describing an error kind *) let err_kind_string = function @@ -259,7 +324,7 @@ let err_class_string = function let print_key = false (** pretty print an error given its (id,key), location, kind, name, description, and optional ml location *) -let pp_err (node_id, node_key) loc ekind ex_name desc mloco fmt () = +let pp_err (node_id, node_key) loc ekind ex_name desc ml_loc_opt fmt () = let kind = err_kind_string (if ekind = Kinfo then Kwarning else ekind) (* eclipse does not know about infos: treat as warning *) in let pp_key fmt k = if print_key then F.fprintf fmt " key: %d " k else () in F.fprintf fmt "%s:%d: %s: %a %a%a%a@\n" @@ -269,7 +334,7 @@ let pp_err (node_id, node_key) loc ekind ex_name desc mloco fmt () = Localise.pp ex_name Localise.pp_error_desc desc pp_key node_key - pp_ml_location_opt mloco + 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 = diff --git a/infer/src/backend/exceptions.mli b/infer/src/backend/exceptions.mli index 7456aa9fc..1c0c48ebb 100644 --- a/infer/src/backend/exceptions.mli +++ b/infer/src/backend/exceptions.mli @@ -29,56 +29,58 @@ type err_kind = (** class of error *) type err_class = Checker | Prover | Nocat -exception Abduction_case_not_implemented of ml_location -exception Analysis_stops of Localise.error_desc * ml_location option -exception Array_of_pointsto of ml_location -exception Array_out_of_bounds_l1 of Localise.error_desc * ml_location -exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location -exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location -exception Bad_footprint of ml_location -exception Bad_pointer_comparison of Localise.error_desc * ml_location -exception Class_cast_exception of Localise.error_desc * ml_location +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 Codequery of Localise.error_desc -exception Comparing_floats_for_equality of Localise.error_desc * ml_location -exception Condition_always_true_false of Localise.error_desc * bool * ml_location -exception Condition_is_assignment of Localise.error_desc * ml_location -exception Context_leak of Localise.error_desc * ml_location +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 Custom_error of string * Localise.error_desc -exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_location +exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * 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_location -exception Divide_by_zero of Localise.error_desc * ml_location -exception Field_not_null_checked of Localise.error_desc * ml_location +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 Eradicate of string * Localise.error_desc exception Checkers of string * Localise.error_desc -exception Frontend_warning of string * Localise.error_desc * ml_location +exception Frontend_warning of string * Localise.error_desc * 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_location -exception Missing_fld of Ident.fieldname * ml_location -exception Premature_nil_termination of Localise.error_desc * ml_location -exception Null_dereference of Localise.error_desc * ml_location -exception Null_test_after_dereference of Localise.error_desc * ml_location -exception Parameter_not_null_checked of Localise.error_desc * ml_location -exception Pointer_size_mismatch of Localise.error_desc * ml_location -exception Precondition_not_found of Localise.error_desc * ml_location -exception Precondition_not_met of Localise.error_desc * ml_location -exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_location -exception Return_expression_required of Localise.error_desc * ml_location -exception Return_statement_missing of Localise.error_desc * ml_location -exception Return_value_ignored of Localise.error_desc * ml_location +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 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 exception Skip_function of Localise.error_desc -exception Skip_pointer_dereference of Localise.error_desc * ml_location -exception Stack_variable_address_escape of Localise.error_desc * ml_location -exception Symexec_memory_error of ml_location -exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_location -exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_location -exception Uninitialized_value of Localise.error_desc * ml_location +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 Unknown_proc -exception Use_after_free of Localise.error_desc * ml_location -exception Wrong_argument_number of ml_location +exception Use_after_free of Localise.error_desc * ml_loc +exception Wrong_argument_number of ml_loc (** string describing an error class *) val err_class_string : err_class -> string @@ -94,10 +96,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 -> - Utils.ml_location option -> Format.formatter -> unit -> unit + Utils.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_location option) * exception_visibility * + (Localise.t * Localise.error_desc * (ml_loc option) * exception_visibility * exception_severity * err_kind option * err_class) diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index 046eceef2..5cb437aa3 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -431,7 +431,7 @@ let interprocedural_algorithm (* wrap _process_result and handle exceptions *) try _process_result exe_env (pname, calls) summary with | exn -> - let err_name, _, mloco, _, _, _, _ = Exceptions.recognize_exception exn in + let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in let err_str = "process_result raised " ^ (Localise.to_string err_name) in L.err "Error: %s@." err_str; let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 6b48f9fb0..d757170db 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -590,9 +590,9 @@ module BugsJson = struct let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in let file = DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in - let json_mloc = match ml_loc_opt with - | Some (file, line, column) when !reports_include_ml_loc -> - Some Jsonbug_j.{ file; line; column } + let json_ml_loc = match ml_loc_opt with + | Some (file, lnum, cnum, enum) when !reports_include_ml_loc -> + Some Jsonbug_j.{ file; lnum; cnum; enum; } | _ -> None in let bug = { bug_class = Exceptions.err_class_string eclass; @@ -609,7 +609,7 @@ module BugsJson = struct qualifier_tags = error_desc_to_qualifier_tags_records error_desc; hash = get_bug_hash kind bug_type procedure_id file node_key error_desc; dotty = error_desc_to_dotty_string error_desc; - infer_source_loc = json_mloc; + infer_source_loc = json_ml_loc; } in if not !is_first_item then pp "," else is_first_item := false; pp "%s@?" (string_of_jsonbug bug) in diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 91acfbb25..14c4d16f5 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -439,7 +439,7 @@ let check_assignement_guard node = | [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*) if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) && not (is_edg_tmp e) then ( let desc = Errdesc.explain_condition_is_assignment l_node in - let exn = Exceptions.Condition_is_assignment (desc, try assert false with Assert_failure x -> x) in + let exn = Exceptions.Condition_is_assignment (desc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~loc: (Some l_node) ~pre: pre_opt exn ) @@ -601,8 +601,7 @@ let report_context_leaks pname sigma tenv = | Some path -> path | None -> assert false in (* a path must exist in order for a leak to be reported *) let err_desc = Errdesc.explain_context_leak pname typ fld_name leak_path in - let exn = Exceptions.Context_leak - (err_desc, try assert false with Assert_failure x -> x) in + let exn = Exceptions.Context_leak (err_desc, __POS__) in Reporting.log_error pname exn) context_exps in (* get the set of pointed-to expressions of type T <: Context *) @@ -634,7 +633,7 @@ let remove_locals_formals_and_check pdesc p = let loc = Cfg.Node.get_loc (Cfg.Procdesc.get_exit_node pdesc) in let dexp_opt, _ = Errdesc.vpath_find p (Sil.Lvar pvar) in let desc = Errdesc.explain_stack_variable_address_escape loc pvar dexp_opt in - let exn = Exceptions.Stack_variable_address_escape (desc, try assert false with Assert_failure x -> x) in + let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in Reporting.log_warning pname exn in IList.iter check_pvar pvars; p' @@ -1162,9 +1161,9 @@ let perform_transition exe_env cg proc_name = apply_start_node do_after_node; Config.allowleak := allowleak; L.err "Error in collect_preconditions for %a@." Procname.pp proc_name; - let err_name, _, mloco, _, _, _, _ = Exceptions.recognize_exception exn in + 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_location_opt mloco; + L.err "Error: %s %a@." err_str pp_ml_loc_opt ml_loc_opt; [] in Fork.transition_footprint_re_exe pname joined_pres in IList.iter transition proc_names diff --git a/infer/src/backend/jsonbug.atd b/infer/src/backend/jsonbug.atd index 5b95d06cd..f5495e1e2 100644 --- a/infer/src/backend/jsonbug.atd +++ b/infer/src/backend/jsonbug.atd @@ -13,8 +13,9 @@ type json_trace_item = { type loc = { file: string; - line: int; - column: int; + lnum: int; + cnum: int; + enum: int; } type jsonbug = { diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index 605f3e79e..b3c6d3a04 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -133,8 +133,8 @@ let stdout fmt_string = (** 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) (mloc: ml_location) = - err "WARNING: %s in %a@." s pp_ml_location_opt (Some mloc) +let warning_position (s: string) (ml_loc: ml_loc) = + err "WARNING: %s in %a@." s pp_ml_loc_opt (Some ml_loc) (** dump a string *) let d_str (s: string) = add_print_action (PTstr, Obj.repr s) diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli index 5dc13bb31..4748b026c 100644 --- a/infer/src/backend/logging.mli +++ b/infer/src/backend/logging.mli @@ -97,7 +97,7 @@ val flush_streams : unit -> unit (** 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_location -> unit +val warning_position: string -> ml_loc -> unit (** dump a string *) val d_str : string -> unit diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index b25667117..8f22406f0 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -46,7 +46,7 @@ type 'a t = foot_pi: Sil.atom list; (** abduced pure part *) } -exception Cannot_star of ml_location +exception Cannot_star of ml_loc (** Pure proposition. *) type pure_prop = Sil.subst * Sil.atom list diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 791c0064c..e934ce15c 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -26,7 +26,7 @@ type struct_init_mode = | No_init | Fld_init -exception Cannot_star of ml_location +exception Cannot_star of ml_loc (** {2 Basic Functions for propositions} *) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index afd57c57e..9120a6e6c 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1165,7 +1165,7 @@ let exp_imply calc_missing subs e1_in e2_in : subst2 = do_imply (do_imply subs e1 e2) f1 f2 | _ -> d_impl_err ("exp_imply not implemented", subs, (EXC_FALSE_EXPS (e1, e2))); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)) in + raise (Exceptions.Abduction_case_not_implemented __POS__) in do_imply subs e1 e2 (** Convert a path (from lhs of a |-> to a field name present only in @@ -1237,7 +1237,7 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs (fst subs, sub2'), None, None | _ -> d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2))); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)) + raise (Exceptions.Abduction_case_not_implemented __POS__) end | Sil.Earray (size1, esel1, inst1), Sil.Earray (size2, esel2, _) -> let indices2 = IList.map fst esel2 in @@ -1265,7 +1265,7 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs sexp_imply source true calc_missing subs se1 se2' typ2' (* calculate index_frame because the rhs is a singleton array *) | _ -> d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2))); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)) + raise (Exceptions.Abduction_case_not_implemented __POS__) and struct_imply source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ident.fieldname * Sil.strexp) list) * ((Ident.fieldname * Sil.strexp) list) = match fsel1, fsel2 with @@ -1727,7 +1727,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 | Sil.Lvar p -> () | Sil.Var v -> if Ident.is_primed v then (d_impl_err ("rhs |-> not implemented", subs, (EXC_FALSE_HPRED hpred2)); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))) + raise (Exceptions.Abduction_case_not_implemented __POS__)) | _ -> () in (match Prop.prop_iter_create prop1 with | None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE)) @@ -1812,7 +1812,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 | Sil.Lvar p -> () | Sil.Var v -> if Ident.is_primed v then (d_impl_err ("rhs |-> not implemented", subs, (EXC_FALSE_HPRED hpred2)); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))) + raise (Exceptions.Abduction_case_not_implemented __POS__)) | _ -> () in if Sil.exp_equal e2 f2 && k == Sil.Lseg_PE then (subs, prop1) @@ -1863,7 +1863,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 ) | Sil.Hdllseg (Sil.Lseg_PE, _, _, _, _, _, _) -> (d_impl_err ("rhs dllsegPE not implemented", subs, (EXC_FALSE_HPRED hpred2)); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))) + raise (Exceptions.Abduction_case_not_implemented __POS__)) | Sil.Hdllseg (k, para2, iF2, oB2, oF2, iB2, elist2) -> (* for now ignore implications between PE and NE *) let iF2, oF2 = Sil.exp_sub (snd subs) iF2, Sil.exp_sub (snd subs) oF2 in let iB2, oB2 = Sil.exp_sub (snd subs) iB2, Sil.exp_sub (snd subs) oB2 in @@ -1871,14 +1871,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 | Sil.Lvar p -> () | Sil.Var v -> if Ident.is_primed v then (d_impl_err ("rhs dllseg not implemented", subs, (EXC_FALSE_HPRED hpred2)); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))) + raise (Exceptions.Abduction_case_not_implemented __POS__)) | _ -> () in let _ = match oB2 with | Sil.Lvar p -> () | Sil.Var v -> if Ident.is_primed v then (d_impl_err ("rhs dllseg not implemented", subs, (EXC_FALSE_HPRED hpred2)); - raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))) + raise (Exceptions.Abduction_case_not_implemented __POS__)) | _ -> () in (match Prop.prop_iter_create prop1 with @@ -2144,7 +2144,7 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 | MISSING_EXC s -> L.d_strln ("WARNING: footprint failed to find MISSING because: " ^ s); None - | (Exceptions.Abduction_case_not_implemented mloc as exn) -> + | (Exceptions.Abduction_case_not_implemented _ as exn) -> Reporting.log_error pname exn; None diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 760673403..ab1e13b15 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -65,15 +65,17 @@ let check_bad_index pname tenv p size index loc = let index_const_opt = get_const_opt index in if index_provably_out_of_bound () then let deref_str = Localise.deref_str_array_bound size_const_opt index_const_opt in - let exn = Exceptions.Array_out_of_bounds_l1 (Errdesc.explain_array_access deref_str p loc, try assert false with Assert_failure x -> x) in + let exn = + Exceptions.Array_out_of_bounds_l1 + (Errdesc.explain_array_access deref_str p loc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn else if size_is_constant then let deref_str = Localise.deref_str_array_bound size_const_opt index_const_opt in let desc = Errdesc.explain_array_access deref_str p loc in let exn = if index_has_bounds () - then Exceptions.Array_out_of_bounds_l2 (desc, try assert false with Assert_failure x -> x) - else Exceptions.Array_out_of_bounds_l3 (desc, try assert false with Assert_failure x -> x) in + then Exceptions.Array_out_of_bounds_l2 (desc, __POS__) + else Exceptions.Array_out_of_bounds_l3 (desc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn end @@ -111,7 +113,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') (instance_fields @ static_fields) with Not_found -> - raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in + raise (Exceptions.Bad_footprint __POS__) in let atoms', se', res_t' = create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst in @@ -165,7 +167,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp (Sil.Aeq(e, e'):: atoms', se, res_t) | Sil.Tint _, _ | Sil.Tfloat _, _ | Sil.Tvoid, _ | Sil.Tfun _, _ | Sil.Tptr _, _ -> L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln(); - raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) + raise (Exceptions.Bad_footprint __POS__) | Sil.Tvar _, _ | Sil.Tenum _, _ -> L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln(); @@ -209,7 +211,7 @@ let rec _strexp_extend_values IList.find (fun (f', t', a') -> Ident.fieldname_equal f f') (instance_fields @ static_fields) with Not_found -> - raise (Exceptions.Missing_fld (f, try assert false with Assert_failure x -> x)) in + raise (Exceptions.Missing_fld (f, __POS__)) in begin try let _, se' = IList.find (fun (f', _) -> Ident.fieldname_equal f f') fsel in @@ -238,7 +240,7 @@ let rec _strexp_extend_values [(atoms', Sil.Estruct (res_fsel', inst'), struct_typ)] end | (Sil.Off_fld (f, _)):: off', _, _ -> - raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) + raise (Exceptions.Bad_footprint __POS__) | (Sil.Off_index _):: _, Sil.Eexp _, Sil.Tint _ | (Sil.Off_index _):: _, Sil.Eexp _, Sil.Tfloat _ @@ -270,7 +272,7 @@ let rec _strexp_extend_values let res_esel' = IList.map replace_ise esel in if (Sil.typ_equal res_typ' typ') || (IList.length res_esel' = 1) then (res_atoms', Sil.Earray(size, res_esel', inst_arr), Sil.Tarray(res_typ', size_for_typ')) :: acc - else raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in + else raise (Exceptions.Bad_footprint __POS__) in IList.fold_left replace [] atoms_se_typ_list' with Not_found -> array_case_analysis_index pname tenv orig_prop @@ -280,7 +282,7 @@ let rec _strexp_extend_values e off' inst_arr inst end | _, _, _ -> - raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) + raise (Exceptions.Bad_footprint __POS__) and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp @@ -290,7 +292,7 @@ and array_case_analysis_index pname tenv orig_prop = let check_sound t' = if not (Sil.typ_equal typ_cont t' || array_cont == []) - then raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in + then raise (Exceptions.Bad_footprint __POS__) in let index_in_array = IList.exists (fun (i, _) -> Prover.check_equal Prop.prop_emp index i) array_cont in let array_is_full = @@ -421,7 +423,7 @@ let mk_ptsto_exp_footprint Errdesc.explain_dereference deref_str orig_prop (State.get_loc ()) in raise (Exceptions.Dangling_pointer_dereference - (None, err_desc, try assert false with Assert_failure x -> x)) + (None, err_desc, __POS__)) end end; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in @@ -636,7 +638,7 @@ let rearrange_arith lexp prop = if Prover.check_allocatedness prop root then raise ARRAY_ACCESS else - raise (Exceptions.Symexec_memory_error (try assert false with Assert_failure x -> x)) + raise (Exceptions.Symexec_memory_error __POS__) let pp_rearrangement_error message prop lexp = L.d_strln (".... Rearrangement Error .... " ^ message); @@ -661,7 +663,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = | Some fld -> begin pp_rearrangement_error "field splitting check failed" orig_prop lexp; - raise (Exceptions.Missing_fld (fld, try assert false with Assert_failure x -> x)) + raise (Exceptions.Missing_fld (fld, __POS__)) end in let res = if !Config.footprint @@ -836,8 +838,7 @@ let check_type_size pname prop texp off typ_from_instr = let loc = State.get_loc () in let exn = Exceptions.Pointer_size_mismatch ( - Errdesc.explain_dereference deref_str prop loc, - try assert false with Assert_failure x -> x) in + Errdesc.explain_dereference deref_str prop loc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn end @@ -888,7 +889,7 @@ let rec iter_rearrange else begin pp_rearrangement_error "cannot find predicate with root" prop lexp; if not !Config.footprint then Printer.force_delayed_prints (); - raise (Exceptions.Symexec_memory_error (try assert false with Assert_failure x -> x)) + raise (Exceptions.Symexec_memory_error __POS__) end in let recurse_on_iters iters = let f_one_iter iter' = @@ -1013,31 +1014,31 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = Errdesc.explain_dereference ~use_buckets: true ~is_nullable: is_deref_of_nullable deref_str prop loc in if Localise.is_parameter_not_null_checked_desc err_desc then - raise (Exceptions.Parameter_not_null_checked (err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Parameter_not_null_checked (err_desc, __POS__)) else if Localise.is_field_not_null_checked_desc err_desc then - raise (Exceptions.Field_not_null_checked (err_desc, try assert false with Assert_failure x -> x)) - else raise (Exceptions.Null_dereference (err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Field_not_null_checked (err_desc, __POS__)) + else raise (Exceptions.Null_dereference (err_desc, __POS__)) end; match attribute_opt with | Some (Sil.Adangling dk) -> let deref_str = Localise.deref_str_dangling (Some dk) in let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in - raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__)) | Some (Sil.Aundef (s, undef_loc, _)) -> if !Config.angelic_execution then () else let deref_str = Localise.deref_str_undef (s, undef_loc) in let err_desc = Errdesc.explain_dereference deref_str prop loc in - raise (Exceptions.Skip_pointer_dereference (err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Skip_pointer_dereference (err_desc, __POS__)) | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)) -> let deref_str = Localise.deref_str_freed ra in let err_desc = Errdesc.explain_dereference ~use_buckets: true deref_str prop loc in - raise (Exceptions.Use_after_free (err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Use_after_free (err_desc, __POS__)) | _ -> if Prover.check_equal Prop.prop_emp (Sil.root_of_lexp root) Sil.exp_minus_one then let deref_str = Localise.deref_str_dangling None in let err_desc = Errdesc.explain_dereference deref_str prop loc in - raise (Exceptions.Dangling_pointer_dereference (None, err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) (* Check that an expression representin an objc block can be null and raise a [B1] null exception.*) (* It's used to check that we don't call possibly null blocks *) @@ -1087,11 +1088,11 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = if is_field_deref then raise (Exceptions.Field_not_null_checked - (err_desc, try assert false with Assert_failure x -> x)) + (err_desc, __POS__)) else raise (Exceptions.Parameter_not_null_checked - (err_desc, try assert false with Assert_failure x -> x)) + (err_desc, __POS__)) | _ -> (* HP: fun_exp is not a footprint therefore, either is a local or it's a modified param *) @@ -1099,7 +1100,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = Localise.error_desc_set_bucket err_desc_nobuckets Localise.BucketLevel.b1 !Config.show_buckets in raise (Exceptions.Null_dereference - (err_desc, try assert false with Assert_failure x -> x)) + (err_desc, __POS__)) end (** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ]. @@ -1127,6 +1128,6 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc else begin pp_rearrangement_error "sigma is empty" prop nlexp; - raise (Exceptions.Symexec_memory_error (try assert false with Assert_failure x -> x)) + raise (Exceptions.Symexec_memory_error __POS__) end | Some iter -> iter_rearrange pname tenv nlexp typ prop iter inst diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index b3f051980..4cbff90f2 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -330,9 +330,9 @@ let process_execution_failures (log_issue : log_issue) pname = (* L.err "Node:%a node_ok:%d node_fail:%d@." Cfg.Node.pp node fs.node_ok fs.node_fail; *) match fs.node_ok, fs.first_failure with | 0, Some (loc, key, session, loc_trace, pre_opt, exn) -> - let ex_name, desc, mloco, _, _, _, _ = Exceptions.recognize_exception exn in + let ex_name, desc, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in let desc' = Localise.verbatim_desc ("exception: " ^ Localise.to_string ex_name) in - let exn' = Exceptions.Analysis_stops (desc', mloco) in + let exn' = Exceptions.Analysis_stops (desc', ml_loc_opt) in log_issue pname ~loc: (Some loc) ~node_id: (Some key) ~ltr: (Some loc_trace) ~pre: pre_opt exn' | _ -> () in diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index a6279d19b..824efb7ab 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -49,7 +49,7 @@ let rec unroll_type tenv typ off = L.d_strln ".... Invalid Field Access ...."; L.d_strln ("Fld : " ^ Ident.fieldname_to_string fld); L.d_str "Type : "; Sil.d_typ_full typ; L.d_ln (); - raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) + raise (Exceptions.Bad_footprint __POS__) end | Sil.Tarray (typ', _), Sil.Off_index _ -> typ' @@ -125,7 +125,7 @@ let rec apply_offlist else Prop.get_undef_attribute p root_lexp in let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt in let err_desc = Errdesc.explain_memory_access deref_str p (State.get_loc ()) in - let exn = (Exceptions.Uninitialized_value (err_desc, try assert false with Assert_failure x -> x)) in + let exn = (Exceptions.Uninitialized_value (err_desc, __POS__)) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn; Sil.update_inst inst_curr inst @@ -478,7 +478,11 @@ let report_raise_memory_leak tenv msg hpred prop = let resource = match Errdesc.hpred_is_open_resource prop hpred with | Some res -> res | None -> Sil.Rmemory Sil.Mmalloc in - raise (Exceptions.Leak (footprint_part, prop, hpred, Errdesc.explain_leak tenv hpred prop None None, false, resource, try assert false with Assert_failure x -> x)) + raise + (Exceptions.Leak + (footprint_part, prop, hpred, + Errdesc.explain_leak tenv hpred prop None None, false, + resource, __POS__)) (** In case of constant string dereference, return the result immediately *) let check_constant_string_dereference lexp = @@ -502,13 +506,15 @@ let exp_norm_check_arith pname prop exp = match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with | Some (Prop.Div0 div), prop' -> let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in - let exn = Exceptions.Divide_by_zero (desc, try assert false with Assert_failure x -> x) in + let exn = Exceptions.Divide_by_zero (desc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn; Prop.exp_normalize_prop prop exp, prop' | Some (Prop.UminusUnsigned (e, typ)), prop' -> - let desc = Errdesc.explain_unary_minus_applied_to_unsigned_expression e typ (State.get_node ()) (State.get_loc ()) in - let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, try assert false with Assert_failure x -> x) in + let desc = + Errdesc.explain_unary_minus_applied_to_unsigned_expression + e typ (State.get_node ()) (State.get_loc ()) in + let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn; Prop.exp_normalize_prop prop exp, prop' @@ -543,7 +549,8 @@ let check_already_dereferenced pname cond prop = match dereferenced_line with | Some (id, (n, pos)) -> let desc = Errdesc.explain_null_test_after_dereference (Sil.Var id) (State.get_node ()) n (State.get_loc ()) in - let exn = (Exceptions.Null_test_after_dereference (desc, try assert false with Assert_failure x -> x)) in + let exn = + (Exceptions.Null_test_after_dereference (desc, __POS__)) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn | None -> () @@ -1054,7 +1061,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path | Sil.Const (Sil.Cint i) when report_condition_always_true_false i -> let node = State.get_node () in let desc = Errdesc.explain_condition_always_true_false i cond node loc in - let exn = Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), try assert false with Assert_failure x -> x) in + let exn = + Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn | Sil.BinOp ((Sil.Eq | Sil.Ne), lhs, rhs) @@ -1075,8 +1083,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path if not (Sil.exp_is_zero lhs_normal) && lhs_is_ns_ptr () then let node = State.get_node () in let desc = Errdesc.explain_bad_pointer_comparison lhs node loc in - let fail = try assert false with Assert_failure x -> x in - let exn = Exceptions.Bad_pointer_comparison (desc, fail) in + let exn = Exceptions.Bad_pointer_comparison (desc, __POS__) in Reporting.log_warning pname exn | _ -> () in check_already_dereferenced pname cond _prop; @@ -1235,7 +1242,7 @@ and sym_exec_generated mask_errors cfg 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 (src, l, c) -> "at "^(src^" "^(string_of_int l)) + | Some ml_loc -> "at " ^ (ml_loc_to_string ml_loc) | None -> "") in L.d_warning ("Generated Instruction Failed with: " ^ (Localise.to_string err_name)^loc ); L.d_ln(); [(p, path)] in @@ -1320,7 +1327,7 @@ and check_untainted exp caller_pname callee_pname prop = callee_pname (State.get_loc ()) in let exn = Exceptions.Tainted_value_reaching_sensitive_function - (err_desc, try assert false with Assert_failure x -> x) in + (err_desc, __POS__) in Reporting.log_warning caller_pname exn; Prop.add_or_replace_exp_attribute prop exp (Sil.Auntaint) | _ -> @@ -1413,8 +1420,7 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop let err_desc = Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true deref_str prop loc in - raise (Exceptions.Premature_nil_termination - (err_desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Premature_nil_termination (err_desc, __POS__)) else raise e in (* IList.fold_left reverses the arguments back so that we report an *) @@ -1456,7 +1462,7 @@ and sym_exec_objc_getter field_name ret_typ_opt tenv cfg ret_ids pdesc pname loc let field_access_exp = Sil.Lfield (lexp, field_name, typ') in execute_letderef ~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc prop - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) and sym_exec_objc_setter field_name ret_typ_opt tenv cfg ret_ids pdesc pname loc args prop = L.d_strln ("No custom setter found. Executing the ObjC builtin setter with ivar "^ @@ -1469,7 +1475,7 @@ and sym_exec_objc_setter field_name ret_typ_opt tenv cfg ret_ids pdesc pname loc | _ -> assert false) in let field_access_exp = Sil.Lfield (lexp1, field_name, typ1') in execute_set ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) and sym_exec_objc_accessor property_accesor ret_typ_opt tenv cfg ret_ids pdesc callee_pname loc args prop path : Builtin.ret_typ = @@ -1501,7 +1507,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = if is_ignored && Specs.get_flag callee_pname proc_flag_ignore_return = None then let err_desc = Localise.desc_return_value_ignored callee_pname loc in - let exn = (Exceptions.Return_value_ignored (err_desc, try assert false with Assert_failure x -> x)) in + let exn = (Exceptions.Return_value_ignored (err_desc, __POS__)) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop caller_pname) in Reporting.log_warning caller_pname ~pre: pre_opt exn in check_inherently_dangerous_function caller_pname callee_pname; @@ -1525,7 +1531,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = L.d_strln (" mismatch in the number of parameters ****"); L.d_str "actual parameters: "; Sil.d_exp_list (IList.map fst actual_pars); L.d_ln (); L.d_str "formal parameters: "; Sil.d_typ_list formal_types; L.d_ln (); - raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in + raise (Exceptions.Wrong_argument_number __POS__) in let actual_params = comb actual_pars formal_types in (* Actual parameters are associated to their formal parameter type if there are enough formal parameters, and @@ -1662,7 +1668,7 @@ module ModelBuiltins = struct | [(lexp1, typ1); (lexp2, typ2); (lexp3, typ3)], _ -> let instr' = Sil.Set (lexp3, typ3, Sil.exp_zero, loc) in sym_exec_generated true cfg tenv pdesc [instr'] [(prop, path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let mk_empty_array size = Sil.Earray (size, [], Sil.inst_none) @@ -1715,7 +1721,7 @@ module ModelBuiltins = struct [(return_result_for_array_size size prop'' ret_ids, path)] | _ -> [] end - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___set_array_size cfg pdesc instr tenv _prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -1751,7 +1757,7 @@ module ModelBuiltins = struct [(prop'', path)] | _ -> [] end - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___print_value cfg pdesc instr tenv prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -1838,7 +1844,7 @@ module ModelBuiltins = struct with Not_found -> (return_result Sil.exp_zero prop ret_ids), path end in (IList.map aux props) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** replace the type of the ptsto rooted at [root_e] with [texp] in [prop] *) let replace_ptsto_texp prop root_e texp = @@ -1874,8 +1880,7 @@ module ModelBuiltins = struct !Config.curr_language = Config.Java || is_cast_to_reference in let deal_with_failed_cast val1 typ1 texp1 texp2 = Tabulation.raise_cast_exception - (try assert false with Assert_failure ml_loc -> ml_loc) - None texp1 texp2 val1 in + __POS__ None texp1 texp2 val1 in let exe_one_prop prop = if Sil.exp_equal texp2 Sil.exp_zero then [(return_result Sil.exp_zero prop ret_ids, path)] @@ -1930,7 +1935,7 @@ module ModelBuiltins = struct end in let props = create_type tenv val1 typ1 prop in IList.flatten (IList.map exe_one_prop props) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___instanceof cfg pdesc instr tenv _prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -1961,7 +1966,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in set_resource_attribute prop path n_lexp loc Sil.Rfile - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as lock *) let execute___set_lock_attribute cfg pdesc instr tenv _prop path ret_ids args callee_pname loc @@ -1971,7 +1976,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in set_resource_attribute prop path n_lexp loc Sil.Rlock - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the resource attribute of the first real argument of method as ignore, the first argument is assumed to be "this" *) let execute___method_set_ignore_attribute @@ -1982,7 +1987,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in set_resource_attribute prop path n_lexp loc Sil.Rignore - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as memory *) let execute___set_mem_attribute cfg pdesc instr tenv _prop path ret_ids args callee_pname loc @@ -1992,7 +1997,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in set_resource_attribute prop path n_lexp loc (Sil.Rmemory Sil.Mnew) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as tainted *) let execute___set_taint_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc @@ -2002,7 +2007,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Ataint pname), path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as untainted *) let execute___set_untaint_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc @@ -2012,7 +2017,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Auntaint), path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as locked*) let execute___set_locked_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc @@ -2022,7 +2027,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Alocked), path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as unlocked*) let execute___set_unlocked_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc @@ -2032,7 +2037,7 @@ module ModelBuiltins = struct let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Aunlocked), path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *) @@ -2043,7 +2048,7 @@ module ModelBuiltins = struct let caller_pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = exp_norm_check_arith caller_pname prop lexp in [(check_untainted n_lexp caller_pname callee_pname prop, path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** take a pointer to a struct, and return the value of a hidden field in the struct *) let execute___get_hidden_field cfg pdesc instr tenv _prop path ret_ids args callee_name loc @@ -2079,7 +2084,7 @@ module ModelBuiltins = struct let prop' = Prop.replace_sigma_footprint sigma_fp' (Prop.replace_sigma sigma' prop) in let prop'' = return_val (Prop.normalize prop') in [(prop'', path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** take a pointer to a struct and a value, and set a hidden field in the struct to the given value *) let execute___set_hidden_field cfg pdesc instr tenv _prop path ret_ids args callee_name loc @@ -2108,7 +2113,7 @@ module ModelBuiltins = struct let prop' = Prop.replace_sigma_footprint sigma_fp' (Prop.replace_sigma sigma' prop) in let prop'' = Prop.normalize prop' in [(prop'', path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (* Update the objective-c hidden counter by applying the operation op and the operand delta.*) (* Eg. op=+/- delta is an integer *) @@ -2133,7 +2138,7 @@ module ModelBuiltins = struct let update_counter = Sil.Set(hidden_field, typ', Sil.BinOp(op, Sil.Var tmp, Sil.Const (Sil.Cint delta)), loc) in let update_counter_instrs = [counter_to_tmp; update_counter; Sil.Remove_temps([tmp], loc)] in sym_exec_generated suppress_npe_report cfg tenv pdesc update_counter_instrs [(_prop, path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (* Given a list of args checks if the first is the flag indicating whether is a call to retain/release for which*) (* we have to suppress NPE report or not. If the flag is present it is removed from the list of args. *) @@ -2151,7 +2156,7 @@ module ModelBuiltins = struct let prop = return_result lexp _prop ret_ids in execute___objc_counter_update suppress_npe_report (Sil.PlusA) (Sil.Int.one) cfg pdesc instr tenv prop path ret_ids args' callee_name loc - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___objc_retain cfg pdesc instr tenv _prop path ret_ids args callee_name loc : Builtin.ret_typ = @@ -2192,7 +2197,7 @@ module ModelBuiltins = struct let prop' = Prop.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in [(prop', path)] else execute___no_op prop path - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Release all the objects in the pool *) let execute___release_autorelease_pool @@ -2237,11 +2242,13 @@ module ModelBuiltins = struct [(return_result val1 prop' ret_ids, path)] | _ -> [(return_result val1 prop ret_ids, path)] with Not_found -> [(return_result val1 prop ret_ids, path)]) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute_abort cfg pdesc instr tenv prop path ret_ids args callee_pname loc : Builtin.ret_typ = - raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string callee_pname), try assert false with Assert_failure x -> x)) + raise + (Exceptions.Precondition_not_found + (Localise.verbatim_desc (Procname.to_string callee_pname), __POS__)) let execute_exit cfg pdesc instr tenv prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -2283,7 +2290,7 @@ module ModelBuiltins = struct L.d_strln ".... Array containing allocated heap cells ...."; L.d_str " Instr: "; Sil.d_instr instr; L.d_ln (); L.d_str " PROP: "; Prop.d_prop prop; L.d_ln (); - raise (Exceptions.Array_of_pointsto (try assert false with Assert_failure x -> x)) + raise (Exceptions.Array_of_pointsto __POS__) end let execute_free mk cfg pdesc instr tenv _prop path ret_ids args callee_pname loc @@ -2304,7 +2311,7 @@ module ModelBuiltins = struct (Prop.exp_normalize_prop p lexp) typ loc) prop_nonzero) in IList.map (fun p -> (p, path)) plist end - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute_alloc mk can_return_null cfg pdesc instr tenv _prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -2327,7 +2334,7 @@ module ModelBuiltins = struct | [(num_obj, _); (base_exp, _)] -> (* for __new_array *) Sil.BinOp (Sil.Mult, num_obj, base_exp) | _ -> - raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in + raise (Exceptions.Wrong_argument_number __POS__) in let ret_id = match ret_ids with | [ret_id] -> ret_id | _ -> Ident.create_fresh Ident.kprimed in @@ -2373,7 +2380,7 @@ module ModelBuiltins = struct | _ -> L.d_str "pthread_create: unknown function "; Sil.d_exp routine_name; L.d_strln ", skipping call."; [(prop, path)]) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute_skip cfg pdesc instr tenv prop path ret_ids args callee_pname loc : Builtin.ret_typ = [(prop, path)] @@ -2386,7 +2393,7 @@ module ModelBuiltins = struct let varargs = ref args in for i = 1 to skip_n_arguments do varargs := IList.tl !varargs done; call_unknown_or_scan true cfg pdesc tenv prop path ret_ids None !varargs callee_pname loc - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute__unwrap_exception cfg pdesc instr tenv _prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -2401,7 +2408,7 @@ module ModelBuiltins = struct [(prop_with_exn, path)] | _ -> assert false end - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute_return_first_argument cfg pdesc instr tenv _prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -2411,7 +2418,7 @@ module ModelBuiltins = struct let arg1, prop = exp_norm_check_arith pname _prop _arg1 in let prop' = return_result arg1 prop ret_ids in [(prop', path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___split_get_nth cfg pdesc instr tenv _prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -2431,7 +2438,7 @@ module ModelBuiltins = struct [(return_result res prop ret_ids, path)] with Not_found -> assert false) | _ -> [(prop, path)]) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___create_tuple cfg pdesc instr tenv prop path ret_ids args callee_pname loc : Builtin.ret_typ = @@ -2452,7 +2459,7 @@ module ModelBuiltins = struct let en = IList.nth el n in [(return_result en prop ret_ids, path)] | _ -> [(prop, path)]) - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (* forces the expression passed as parameter to be assumed true at the point where this builtin is called, blocks if this causes an inconsistency *) @@ -2463,7 +2470,7 @@ module ModelBuiltins = struct let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop in if Prover.check_inconsistency prop_assume then execute_diverge prop_assume path else [(prop_assume, path)] - | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) (* creates a named error state *) let execute___infer_fail cfg pdesc instr tenv prop path ret_ids args callee_pname loc @@ -2477,7 +2484,7 @@ module ModelBuiltins = struct | _ -> assert false end | _ -> - raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in + raise (Exceptions.Wrong_argument_number __POS__) in let set_instr = Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)] @@ -2490,7 +2497,7 @@ module ModelBuiltins = struct | l when IList.length l = 4 -> Config.default_failure_name | _ -> - raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in + raise (Exceptions.Wrong_argument_number __POS__) in let set_instr = Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)] diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 482510cc9..99f6f7461 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -109,14 +109,16 @@ let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed S if specs == [] then begin trace_call Specs.CallStats.CR_not_found; - raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string proc_name), try assert false with Assert_failure x -> x)) + raise (Exceptions.Precondition_not_found + (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) end; let formal_parameters = IList.map (fun (x, _) -> Sil.mk_pvar_callee x proc_name) formals in IList.map f specs, formal_parameters with Not_found -> begin L.d_strln ("ERROR: found no entry for procedure " ^ Procname.to_string proc_name ^ ". Give up..."); - raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string proc_name), try assert false with Assert_failure x -> x)) + raise (Exceptions.Precondition_not_found + (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) end let check_splitting_precondition sub1 sub2 = @@ -348,7 +350,7 @@ let check_path_errors_in_post caller_pname post post_path = then post_path, Some path_pos else current_path, None in (* position not found, only use the path up to the callee *) State.set_path new_path path_pos_opt; - let exn = Exceptions.Divide_by_zero (desc, try assert false with Assert_failure x -> x) in + let exn = Exceptions.Divide_by_zero (desc, __POS__) in let pre_opt = State.get_normalized_pre (fun te p -> p) (* Abs.abstract_no_symop *) in Reporting.log_warning caller_pname ~pre: pre_opt exn | _ -> () in @@ -481,7 +483,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr L.d_str "cannot star "; Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2; L.d_ln (); - raise (Prop.Cannot_star (try assert false with Assert_failure x -> x)) + raise (Prop.Cannot_star __POS__) let hpred_typing_lhs_compare hpred1 (e2, te2) = match hpred1 with | Sil.Hpointsto(e1, _, _) -> Sil.exp_compare e1 e2 @@ -513,7 +515,7 @@ let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) lis L.d_str "cannot star "; Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2; L.d_ln (); - raise (Prop.Cannot_star (try assert false with Assert_failure x -> x)) + raise (Prop.Cannot_star __POS__) (** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] extends the footprint of [prop] with [pi,sigma] and extends the fields of |-> with [missing_fld] *) let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_new missing_fld missing_typ : Prop.normal Prop.t option = @@ -556,7 +558,7 @@ let check_attr_dealloc_mismatch att_old att_new = match att_old, att_new with Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease; Sil.ra_res = Sil.Rmemory mk_new } as ra_new) when Sil.mem_kind_compare mk_old mk_new <> 0 -> let desc = Errdesc.explain_allocation_mismatch ra_old ra_new in - raise (Exceptions.Deallocation_mismatch (desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Deallocation_mismatch (desc, __POS__)) | _ -> () (** [prop_copy_footprint p1 p2] copies the footprint and pure part of [p1] into [p2] *) @@ -796,7 +798,7 @@ let mk_actual_precondition prop actual_params formal_params = (let str = "more actual pars than formal pars in fun call (" ^ string_of_int (IList.length actual_params) ^ " vs " ^ string_of_int (IList.length formal_params) ^ ")" in L.d_warning str; L.d_ln ()); [] - | _:: _,[] -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in + | _:: _,[] -> raise (Exceptions.Wrong_argument_number __POS__) in comb formal_params actual_params in let mk_instantiation (formal_var, (actual_e, actual_t)) = Prop.mk_ptsto (Sil.Lvar formal_var) (Sil.Eexp (actual_e, Sil.inst_actual_precondition)) (Sil.Sizeof (actual_t, Sil.Subtype.exact)) in @@ -893,7 +895,7 @@ let do_taint_check caller_pname callee_pname calling_pi missing_pi sub prop = callee_pname (State.get_loc ()) in let exn = Exceptions.Tainted_value_reaching_sensitive_function - (err_desc, try assert false with Assert_failure x -> x) in + (err_desc, __POS__) in Reporting.log_warning caller_pname exn in IList.iter report_one_error taint_atoms in Sil.ExpMap.iter report_taint_errors taint_untaint_exp_map; @@ -912,26 +914,26 @@ let do_taint_check caller_pname callee_pname calling_pi missing_pi sub prop = taint_untaint_exp_map) in IList.filter not_untaint_atom missing_pi_sub -let class_cast_exn pname_opt texp1 texp2 exp ml_location = +let class_cast_exn pname_opt texp1 texp2 exp ml_loc = let desc = Errdesc.explain_class_cast_exception pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in - Exceptions.Class_cast_exception (desc, ml_location) + Exceptions.Class_cast_exception (desc, ml_loc) -let raise_cast_exception ml_location pname_opt texp1 texp2 exp = - let exn = class_cast_exn pname_opt texp1 texp2 exp ml_location in +let raise_cast_exception ml_loc pname_opt texp1 texp2 exp = + let exn = class_cast_exn pname_opt texp1 texp2 exp ml_loc in raise exn -let get_check_exn check callee_pname loc ml_location = match check with +let get_check_exn check callee_pname loc ml_loc = match check with | Prover.Bounds_check -> let desc = Localise.desc_precondition_not_met (Some Localise.Pnm_bounds) callee_pname loc in - Exceptions.Precondition_not_met (desc, ml_location) + Exceptions.Precondition_not_met (desc, ml_loc) | Prover.Class_cast_check (texp1, texp2, exp) -> - class_cast_exn (Some callee_pname) texp1 texp2 exp ml_location + class_cast_exn (Some callee_pname) texp1 texp2 exp ml_loc let check_uninitialize_dangling_deref callee_pname actual_pre sub formal_params props = IList.iter (fun (p, _ ) -> match check_dereferences callee_pname actual_pre sub p formal_params with | Some (Deref_undef_exp, desc) -> - raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, __POS__)) | _ -> ()) props (** Perform symbolic execution for a single spec *) @@ -952,7 +954,7 @@ let exe_spec | Prover.ImplFail checks -> Invalid_res (Prover_checks checks) | Prover.ImplOK (checks, sub1, sub2, frame, missing_pi, missing_sigma, frame_fld, missing_fld, frame_typ, missing_typ) -> let log_check_exn check = - let exn = get_check_exn check callee_pname loc (try assert false with Assert_failure x -> x) in + let exn = get_check_exn check callee_pname loc __POS__ in Reporting.log_warning caller_pname exn in let do_split () = let missing_pi' = @@ -1088,27 +1090,29 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r | Dereference_error (Deref_minusone, desc, path_opt) -> trace_call Specs.CallStats.CR_not_met; extend_path path_opt None; - raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAminusone, desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Dangling_pointer_dereference + (Some Sil.DAminusone, desc, __POS__)) | Dereference_error (Deref_undef_exp, desc, path_opt) -> trace_call Specs.CallStats.CR_not_met; extend_path path_opt None; - raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Dangling_pointer_dereference + (Some Sil.DAuninit, desc, __POS__)) | Dereference_error (Deref_null pos, desc, path_opt) -> trace_call Specs.CallStats.CR_not_met; extend_path path_opt (Some pos); if Localise.is_parameter_not_null_checked_desc desc then - raise (Exceptions.Parameter_not_null_checked (desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Parameter_not_null_checked (desc, __POS__)) else if Localise.is_field_not_null_checked_desc desc then - raise (Exceptions.Field_not_null_checked (desc, try assert false with Assert_failure x -> x)) - else raise (Exceptions.Null_dereference (desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Field_not_null_checked (desc, __POS__)) + else raise (Exceptions.Null_dereference (desc, __POS__)) | Dereference_error (Deref_freed ra, desc, path_opt) -> trace_call Specs.CallStats.CR_not_met; extend_path path_opt None; - raise (Exceptions.Use_after_free (desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Use_after_free (desc, __POS__)) | Dereference_error (Deref_undef (s, loc, pos), desc, path_opt) -> trace_call Specs.CallStats.CR_not_met; extend_path path_opt (Some pos); - raise (Exceptions.Skip_pointer_dereference (desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Skip_pointer_dereference (desc, __POS__)) | Prover_checks _ | Cannot_combine | Missing_sigma_not_empty | Missing_fld_not_empty -> trace_call Specs.CallStats.CR_not_met; assert false @@ -1119,13 +1123,13 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r else if IList.exists (function | Prover_checks (check :: _) -> trace_call Specs.CallStats.CR_not_met; - let exn = get_check_exn check callee_pname loc (try assert false with Assert_failure x -> x) in + let exn = get_check_exn check callee_pname loc __POS__ in raise exn | _ -> false) invalid_res then call_desc (Some Localise.Pnm_bounds) else call_desc None in trace_call Specs.CallStats.CR_not_met; - raise (Exceptions.Precondition_not_met (desc, try assert false with Assert_failure x -> x)) + raise (Exceptions.Precondition_not_met (desc, __POS__)) end else (* combine the valid results, and store diverging states *) let process_valid_res vr = @@ -1140,7 +1144,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r else if valid_res_no_miss_pi != [] then IList.flatten (IList.map (fun vr -> vr.vr_cons_res) valid_res_no_miss_pi) else if valid_res_miss_pi == [] then - raise (Exceptions.Precondition_not_met (call_desc None, try assert false with Assert_failure x -> x)) + raise (Exceptions.Precondition_not_met (call_desc None, __POS__)) else begin L.d_strln "Missing pure facts for the function call:"; @@ -1148,7 +1152,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r match Prover.find_minimum_pure_cover (IList.map (fun vr -> (vr.vr_pi, vr.vr_cons_res)) valid_res_miss_pi) with | None -> trace_call Specs.CallStats.CR_not_met; - raise (Exceptions.Precondition_not_met (call_desc None, try assert false with Assert_failure x -> x)) + raise (Exceptions.Precondition_not_met (call_desc None, __POS__)) | Some cover -> L.d_strln "Found minimum cover"; IList.iter print_pi (IList.map fst cover); diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 082bb5063..c392eef2d 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -24,7 +24,7 @@ val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * Sil.path_ (** raise a cast exception *) val raise_cast_exception : - Utils.ml_location -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a + Utils.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 diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 6c47b098c..48dcce0e4 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -237,25 +237,21 @@ let pp_elapsed_time fmt () = let elapsed = Unix.gettimeofday () -. initial_timeofday in Format.fprintf fmt "%f" elapsed -(** Type of location in ml source: file,line,column *) -type ml_location = string * int * int +(** Type of location in ml source: __POS__ *) +type ml_loc = string * int * int * int -(** String describing the file of an ml location *) -let ml_location_file_string ((file: string), (line: int), (column: int)) = - "file " ^ file - -(** Turn an ml location into a string *) -let ml_location_string ((file: string), (line: int), (column: int)) = - "file " ^ file ^ " line " ^ string_of_int line ^ " column " ^ string_of_int column +(** 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_location fmt mloc = - F.fprintf fmt "%s" (ml_location_string mloc) +let pp_ml_loc fmt ml_loc = + F.fprintf fmt "%s" (ml_loc_to_string ml_loc) -let pp_ml_location_opt fmt mloco = - if !Config.developer_mode then match mloco with +let pp_ml_loc_opt fmt ml_loc_opt = + if !Config.developer_mode then match ml_loc_opt with | None -> () - | Some mloc -> F.fprintf fmt "(%a)" pp_ml_location mloc + | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc (** {2 SymOp and Failures: units of symbolic execution} *) diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index f9c8c8d29..92a1fa8fc 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -68,17 +68,14 @@ module StringMap : Map.S with type key = string (** {2 Printing} *) -(** Type of location in ml source: file,line,column *) -type ml_location = string * int * int +(** Type of location in ml source: __POS__ *) +type ml_loc = string * int * int * int -(** String describing the file of an ml location *) -val ml_location_file_string : ml_location -> string - -(** Turn an ml location into a string *) -val ml_location_string : ml_location -> string +(** 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_location_opt : Format.formatter -> ml_location option -> unit +val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit (** Colors supported in printing *) type color = Black | Blue | Green | Orange | Red diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index d826fc666..fe305801e 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -34,8 +34,7 @@ let log_frontend_warning pdesc warn_desc = let err_desc = Errdesc.explain_frontend_warning warn_desc.description warn_desc.suggestion loc in let exn = Exceptions.Frontend_warning - (warn_desc.name, err_desc, - try assert false with Assert_failure x -> x) in + (warn_desc.name, err_desc, __POS__) in Reporting.log_error_from_errlog errlog exn ~loc:(Some loc) (* Call all checkers on properties of class c *) diff --git a/infer/src/eradicate/modelTables.ml b/infer/src/eradicate/modelTables.ml index 1f5d33e3c..f4dbb304c 100644 --- a/infer/src/eradicate/modelTables.ml +++ b/infer/src/eradicate/modelTables.ml @@ -234,8 +234,7 @@ let mk_table list = IList.iter (function (v, pn_id) -> Hashtbl.replace map pn_id v) list; map -let ml_location = - try assert false with Assert_failure x -> x +let this_file = __FILE__ let annotated_table_nullable = mk_table annotated_list_nullable let annotated_table_present = mk_table annotated_list_present diff --git a/infer/src/eradicate/modelTables.mli b/infer/src/eradicate/modelTables.mli index 26a8976cd..3a0e7a9cb 100644 --- a/infer/src/eradicate/modelTables.mli +++ b/infer/src/eradicate/modelTables.mli @@ -11,8 +11,8 @@ open Utils type model_table_t = (string, bool * bool list) Hashtbl.t -(** Location of this file. *) -val ml_location : ml_location +(** Name of this file. *) +val this_file : string val annotated_table_nullable : model_table_t val annotated_table_present : model_table_t diff --git a/infer/src/eradicate/typeOrigin.ml b/infer/src/eradicate/typeOrigin.ml index cc6814e1c..3da59fcef 100644 --- a/infer/src/eradicate/typeOrigin.ml +++ b/infer/src/eradicate/typeOrigin.ml @@ -96,7 +96,7 @@ let get_description origin = | None -> "" in let modelled_in = if Models.is_modelled_nullable po.pname - then " modelled in " ^ (Utils.ml_location_file_string ModelTables.ml_location) + then " modelled in " ^ ModelTables.this_file else "" in let description = Printf.sprintf "call to %s%s%s%s"