From b6c8e52e8ca70ff69ed7867d309e8f5a3c6fad4c Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Mon, 15 Jun 2020 09:33:45 -0700 Subject: [PATCH] [biabduction] Delete use after free Summary: Pulse has now a better version of this check, so let's delete it. Reviewed By: ngorogiannis Differential Revision: D22019247 fbshipit-source-id: 344678225 --- infer/man/man1/infer-full.txt | 1 - infer/man/man1/infer-report.txt | 1 - infer/man/man1/infer.txt | 1 - infer/src/absint/Localise.ml | 24 ------------------- infer/src/absint/Localise.mli | 3 --- infer/src/base/IssueType.ml | 4 ---- infer/src/base/IssueType.mli | 2 -- infer/src/biabduction/Exceptions.ml | 4 ---- infer/src/biabduction/Exceptions.mli | 2 -- infer/src/biabduction/Rearrange.ml | 4 ---- infer/src/biabduction/Tabulation.ml | 18 ++++---------- infer/src/integration/JsonReports.ml | 3 +-- .../codetoanalyze/cpp/biabduction/issues.exp | 3 --- 13 files changed, 6 insertions(+), 64 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index daeecfea5..598ac48a8 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -363,7 +363,6 @@ OPTIONS BIABDUCTION_MEMORY_LEAK (disabled by default), BIABD_CONDITION_ALWAYS_FALSE (disabled by default), BIABD_CONDITION_ALWAYS_TRUE (disabled 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 5dbdca0b0..62ccce1af 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -93,7 +93,6 @@ OPTIONS BIABDUCTION_MEMORY_LEAK (disabled by default), BIABD_CONDITION_ALWAYS_FALSE (disabled by default), BIABD_CONDITION_ALWAYS_TRUE (disabled 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 f4c5f8cbe..8bf1f854d 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -363,7 +363,6 @@ OPTIONS BIABDUCTION_MEMORY_LEAK (disabled by default), BIABD_CONDITION_ALWAYS_FALSE (disabled by default), BIABD_CONDITION_ALWAYS_TRUE (disabled 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/absint/Localise.ml b/infer/src/absint/Localise.ml index 54a6b4a31..f99b7f493 100644 --- a/infer/src/absint/Localise.ml +++ b/infer/src/absint/Localise.ml @@ -226,29 +226,6 @@ let deref_str_undef (proc_name, loc) = ^ " and is dereferenced or freed" } -(** dereference strings for a freed pointer dereference *) -let deref_str_freed ra = - let tags = Tags.create () in - let freed_or_closed_by_call = - let freed_or_closed = - match ra.PredSymb.ra_res with - | PredSymb.Rmemory _ -> - "freed" - | PredSymb.Rfile -> - "closed" - | PredSymb.Rignore -> - "freed" - | PredSymb.Rlock -> - "locked" - in - freed_or_closed ^ " " ^ by_call_to_ra tags ra - in - { tags - ; value_pre= Some (pointer_or_object ()) - ; value_post= None - ; problem_str= "was " ^ freed_or_closed_by_call ^ " and is dereferenced or freed" } - - (** dereference strings for a dangling pointer dereference *) let deref_str_dangling dangling_kind_opt = let dangling_kind_prefix = @@ -434,7 +411,6 @@ let is_parameter_not_null_checked_desc desc = has_tag desc Tags.parameter_not_nu let is_field_not_null_checked_desc desc = has_tag desc Tags.field_not_null_checked - let desc_condition_always_true_false i cond_str_opt loc = let tags = Tags.create () in let value = match cond_str_opt with None -> "" | Some s -> s in diff --git a/infer/src/absint/Localise.mli b/infer/src/absint/Localise.mli index 484d6c51f..1c33dfa7f 100644 --- a/infer/src/absint/Localise.mli +++ b/infer/src/absint/Localise.mli @@ -72,9 +72,6 @@ val deref_str_nullable : Procname.t option -> string -> deref_str val deref_str_undef : Procname.t * Location.t -> deref_str (** dereference strings for an undefined value coming from the given procedure *) -val deref_str_freed : PredSymb.res_action -> deref_str -(** dereference strings for a freed pointer dereference *) - val deref_str_dangling : PredSymb.dangling_kind option -> deref_str (** dereference strings for a dangling pointer dereference *) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 752144828..d500a14a2 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -269,10 +269,6 @@ let biabd_condition_always_true = Warning Biabduction -let biabd_use_after_free = - register_from_string ~hum:"Use After Free" ~id:"BIABD_USE_AFTER_FREE" Error Biabduction - - let buffer_overrun_l1 = register_from_string ~id:"BUFFER_OVERRUN_L1" Error BufferOverrunChecker ~user_documentation:[%blob "../../documentation/issues/BUFFER_OVERRUN.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 184b245ea..85e48585f 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -89,8 +89,6 @@ val biabd_condition_always_false : t val biabd_condition_always_true : t -val biabd_use_after_free : t - val buffer_overrun_l1 : t val buffer_overrun_l2 : t diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index b62bd8f59..49dda43e5 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/infer/src/biabduction/Exceptions.ml @@ -26,8 +26,6 @@ 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 @@ -116,8 +114,6 @@ let recognize_exception exn : IssueToReport.t = ; ocaml_pos= Some ocaml_pos } | Bad_footprint ocaml_pos -> {issue_type= IssueType.bad_footprint; description= Localise.no_desc; ocaml_pos= Some ocaml_pos} - | Biabd_use_after_free (desc, ocaml_pos) -> - {issue_type= IssueType.biabd_use_after_free; description= desc; ocaml_pos= Some ocaml_pos} | Cannot_star ocaml_pos -> {issue_type= IssueType.cannot_star; description= Localise.no_desc; ocaml_pos= Some ocaml_pos} | Class_cast_exception (desc, ocaml_pos) -> diff --git a/infer/src/biabduction/Exceptions.mli b/infer/src/biabduction/Exceptions.mli index c3240ddec..9c3e6db14 100644 --- a/infer/src/biabduction/Exceptions.mli +++ b/infer/src/biabduction/Exceptions.mli @@ -24,8 +24,6 @@ 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 diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 1426cab88..a055be874 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -1293,10 +1293,6 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = raise (Exceptions.Dangling_pointer_dereference (true, err_desc, __POS__)) | Some (Apred (Aundef _, _)) -> () - | 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.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 d99c69f89..99db12f26 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -23,7 +23,6 @@ type splitting = ; missing_typ: (Exp.t * Exp.t) list } type deref_error = - | Deref_freed of PredSymb.res_action (** dereference a freed pointer *) | Deref_minusone (** dereference -1 *) | Deref_null of PredSymb.path_pos (** dereference null *) | Deref_undef of Procname.t * Location.t * PredSymb.path_pos @@ -335,15 +334,11 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo else if Exp.equal e_sub Exp.minus_one then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) else - match Attribute.get_resource tenv actual_pre e_sub with - | Some (Apred (Aresource ({ra_kind= Rrelease} as ra), _)) -> - Some (Deref_freed ra, desc true (Localise.deref_str_freed ra)) - | _ -> ( - match Attribute.get_undef tenv actual_pre e_sub with - | Some (Apred (Aundef (s, _, loc, pos), _)) -> - Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) - | _ -> - None ) + match Attribute.get_undef tenv actual_pre e_sub with + | Some (Apred (Aundef (s, _, loc, pos), _)) -> + Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) + | _ -> + None in let check_hpred = function | Predicates.Hpointsto (lexp, se, _) -> @@ -1276,9 +1271,6 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results = else if Localise.is_empty_vector_access_desc desc then raise (Exceptions.Empty_vector_access (desc, __POS__)) else raise (Exceptions.Null_dereference (desc, __POS__)) - | Dereference_error (Deref_freed _, desc, path_opt) -> - extend_path path_opt None ; - raise (Exceptions.Biabd_use_after_free (desc, __POS__)) | Dereference_error (Deref_undef (_, _, pos), desc, path_opt) -> extend_path path_opt (Some pos) ; raise (Exceptions.Skip_pointer_dereference (desc, __POS__)) diff --git a/infer/src/integration/JsonReports.ml b/infer/src/integration/JsonReports.ml index 0a48b010b..615a41752 100644 --- a/infer/src/integration/JsonReports.ml +++ b/infer/src/integration/JsonReports.ml @@ -69,8 +69,7 @@ let should_report issue_type error_desc = ; null_dereference ; parameter_not_null_checked ; premature_nil_termination - ; empty_vector_access - ; biabd_use_after_free ] + ; empty_vector_access ] in List.mem ~equal:IssueType.equal null_deref_issue_types issue_type in diff --git a/infer/tests/codetoanalyze/cpp/biabduction/issues.exp b/infer/tests/codetoanalyze/cpp/biabduction/issues.exp index 1ca91ee31..2ccd4a602 100644 --- a/infer/tests/codetoanalyze/cpp/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/cpp/biabduction/issues.exp @@ -131,9 +131,6 @@ codetoanalyze/cpp/biabduction/types/typeid_expr.cpp, person_typeid_name, 8, DIVI codetoanalyze/cpp/biabduction/types/typeid_expr.cpp, template_type_id_person, 2, BIABDUCTION_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/biabduction/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/biabduction/types/typeid_expr.cpp, template_typeid, 2, BIABDUCTION_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/biabduction/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/biabduction/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/biabduction/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/biabduction/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/biabduction/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/biabduction/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]