diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index dad63e257..9296ca03a 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -333,6 +333,7 @@ OPTIONS Abduction_case_not_implemented (enabled by default), Array_of_pointsto (enabled by default), Assert_failure (enabled by default), + BIABD_USE_AFTER_FREE (enabled by default), BUFFER_OVERRUN_L1 (enabled by default), BUFFER_OVERRUN_L2 (enabled by default), BUFFER_OVERRUN_L3 (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 048eb30a7..41630a727 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -82,6 +82,7 @@ OPTIONS Abduction_case_not_implemented (enabled by default), Array_of_pointsto (enabled by default), Assert_failure (enabled by default), + BIABD_USE_AFTER_FREE (enabled by default), BUFFER_OVERRUN_L1 (enabled by default), BUFFER_OVERRUN_L2 (enabled by default), BUFFER_OVERRUN_L3 (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index ba1154b0c..397078acb 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -333,6 +333,7 @@ OPTIONS Abduction_case_not_implemented (enabled by default), Array_of_pointsto (enabled by default), Assert_failure (enabled by default), + BIABD_USE_AFTER_FREE (enabled by default), BUFFER_OVERRUN_L1 (enabled by default), BUFFER_OVERRUN_L2 (enabled by default), BUFFER_OVERRUN_L3 (enabled by default), diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 5c69bc9ac..b9f098561 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -43,6 +43,8 @@ exception Array_of_pointsto of L.ocaml_pos exception Bad_footprint of L.ocaml_pos +exception Biabd_use_after_free of Localise.error_desc * L.ocaml_pos + exception Cannot_star of L.ocaml_pos exception Class_cast_exception of Localise.error_desc * L.ocaml_pos @@ -128,8 +130,6 @@ exception Unknown_proc exception Unsafe_guarded_by_access of Localise.error_desc * L.ocaml_pos -exception Use_after_free of Localise.error_desc * L.ocaml_pos - exception Wrong_argument_number of L.ocaml_pos type t = @@ -201,6 +201,13 @@ let recognize_exception exn = ; visibility= Exn_developer ; severity= None ; category= Nocat } + | Biabd_use_after_free (desc, ocaml_pos) -> + { name= IssueType.biabd_use_after_free + ; description= desc + ; ocaml_pos= Some ocaml_pos + ; visibility= Exn_user + ; severity= None + ; category= Prover } | Cannot_star ocaml_pos -> { name= IssueType.cannot_star ; description= Localise.no_desc @@ -533,13 +540,6 @@ let recognize_exception exn = ; visibility= Exn_user ; severity= None ; category= Prover } - | Use_after_free (desc, ocaml_pos) -> - { name= IssueType.use_after_free - ; description= desc - ; ocaml_pos= Some ocaml_pos - ; visibility= Exn_user - ; severity= None - ; category= Prover } | Wrong_argument_number ocaml_pos -> { name= IssueType.wrong_argument_number ; description= Localise.no_desc diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index cdc3c9ac6..cca8b511e 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -43,6 +43,8 @@ exception Array_out_of_bounds_l3 of Localise.error_desc * Logging.ocaml_pos exception Bad_footprint of Logging.ocaml_pos +exception Biabd_use_after_free of Localise.error_desc * Logging.ocaml_pos + exception Cannot_star of Logging.ocaml_pos exception Class_cast_exception of Localise.error_desc * Logging.ocaml_pos @@ -134,8 +136,6 @@ exception Unknown_proc exception Unsafe_guarded_by_access of Localise.error_desc * Logging.ocaml_pos -exception Use_after_free of Localise.error_desc * Logging.ocaml_pos - exception Wrong_argument_number of Logging.ocaml_pos val severity_string : severity -> string diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 77544a9b3..8299ef6b7 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -152,7 +152,7 @@ let should_report (issue_kind : Exceptions.severity) issue_type error_desc eclas ; parameter_not_null_checked ; premature_nil_termination ; empty_vector_access - ; use_after_free ] + ; biabd_use_after_free ] in List.mem ~equal:IssueType.equal null_deref_issue_types issue_type in diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index cce8f2113..468c48fd1 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -442,6 +442,8 @@ let use_after_delete = register_from_string "USE_AFTER_DELETE" let use_after_free = register_from_string "USE_AFTER_FREE" +let biabd_use_after_free = register_from_string "BIABD_USE_AFTER_FREE" + let use_after_lifetime = register_from_string "USE_AFTER_LIFETIME" let user_controlled_sql_risk = register_from_string "USER_CONTROLLED_SQL_RISK" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 047ad8566..e7294f233 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -53,6 +53,8 @@ val assert_failure : t val bad_footprint : t +val biabd_use_after_free : t + val buffer_overrun_l1 : t val buffer_overrun_l2 : t diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index f5bffe1f6..0bc6bcd80 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -1633,7 +1633,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = | Some (Apred (Aresource ({ra_kind= Rrelease} as ra), _)) -> let deref_str = Localise.deref_str_freed ra in let err_desc = Errdesc.explain_dereference pname tenv ~use_buckets:true deref_str prop loc in - raise (Exceptions.Use_after_free (err_desc, __POS__)) + raise (Exceptions.Biabd_use_after_free (err_desc, __POS__)) | _ -> if Prover.check_equal tenv Prop.prop_emp (Exp.root_of_lexp root) Exp.minus_one then let deref_str = Localise.deref_str_dangling None in diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index d68986274..984f20de1 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -1359,7 +1359,7 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re | Dereference_error (Deref_freed _, desc, path_opt) -> trace_call CR_not_met ; extend_path path_opt None ; - raise (Exceptions.Use_after_free (desc, __POS__)) + raise (Exceptions.Biabd_use_after_free (desc, __POS__)) | Dereference_error (Deref_undef (_, _, pos), desc, path_opt) -> trace_call CR_not_met ; extend_path path_opt (Some pos) ; diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index 4f41fc84b..f2f883a9b 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -135,9 +135,9 @@ codetoanalyze/cpp/errors/types/typeid_expr.cpp, person_typeid_name, 8, DIVIDE_BY codetoanalyze/cpp/errors/types/typeid_expr.cpp, template_type_id_person, 2, MEMORY_LEAK, CPP, ERROR, [start of procedure template_type_id_person(),start of procedure Person,return from a call to Person::Person,Skipping template_typeid(): empty list of specs] codetoanalyze/cpp/errors/types/typeid_expr.cpp, template_type_id_person, 5, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure template_type_id_person(),start of procedure Person,return from a call to Person::Person,Taking false branch] codetoanalyze/cpp/errors/types/typeid_expr.cpp, template_typeid, 2, MEMORY_LEAK, CPP, ERROR, [start of procedure template_typeid(),start of procedure Person,return from a call to Person::Person,start of procedure Person,return from a call to Person::Person,start of procedure ~Person,start of procedure __infer_inner_destructor_~Person,return from a call to Person::__infer_inner_destructor_~Person,return from a call to Person::~Person,start of procedure ~Person,start of procedure __infer_inner_destructor_~Person,return from a call to Person::__infer_inner_destructor_~Person,return from a call to Person::~Person] -codetoanalyze/cpp/errors/use_after_free/foreach_map.cpp, use_after_free::Basic::test_double_delete_bad, 3, USE_AFTER_FREE, B1, ERROR, [start of procedure test_double_delete_bad,Skipping Y: method has no implementation] -codetoanalyze/cpp/errors/use_after_free/foreach_map.cpp, use_after_free::Basic::test_for_map_delete_ok_FP, 2, USE_AFTER_FREE, B5, ERROR, [start of procedure test_for_map_delete_ok_FP,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation] -codetoanalyze/cpp/errors/use_after_free/foreach_map.cpp, use_after_free::Basic::test_for_umap_delete_ok_FP, 2, USE_AFTER_FREE, B5, ERROR, [start of procedure test_for_umap_delete_ok_FP,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation] +codetoanalyze/cpp/errors/use_after_free/foreach_map.cpp, use_after_free::Basic::test_double_delete_bad, 3, BIABD_USE_AFTER_FREE, B1, ERROR, [start of procedure test_double_delete_bad,Skipping Y: method has no implementation] +codetoanalyze/cpp/errors/use_after_free/foreach_map.cpp, use_after_free::Basic::test_for_map_delete_ok_FP, 2, BIABD_USE_AFTER_FREE, B5, ERROR, [start of procedure test_for_map_delete_ok_FP,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation] +codetoanalyze/cpp/errors/use_after_free/foreach_map.cpp, use_after_free::Basic::test_for_umap_delete_ok_FP, 2, BIABD_USE_AFTER_FREE, B5, ERROR, [start of procedure test_for_umap_delete_ok_FP,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation,Loop condition is true. Entering loop body,Skipping operator*: method has no implementation] codetoanalyze/cpp/errors/vector/empty_access.cpp, ERROR_vector_as_param_by_value_clear_ok, 2, Cannot_star, no_bucket, ERROR, [start of procedure ERROR_vector_as_param_by_value_clear_ok(),Skipping vector: method has no implementation,Skipping vector: method has no implementation] codetoanalyze/cpp/errors/vector/empty_access.cpp, ERROR_vector_as_param_by_value_empty_bad, 2, Cannot_star, no_bucket, ERROR, [start of procedure ERROR_vector_as_param_by_value_empty_bad(),Skipping vector: method has no implementation,Skipping vector: method has no implementation] codetoanalyze/cpp/errors/vector/empty_access.cpp, ERROR_vector_as_param_empty_bad, 2, Cannot_star, no_bucket, ERROR, [start of procedure ERROR_vector_as_param_empty_bad(),Skipping vector: method has no implementation]