From 415824ac0ecee5b55e18b18d203db98e9389f860 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Mon, 15 Jun 2020 06:48:35 -0700 Subject: [PATCH] [biabduction] Delete deallocation_mismatch Summary: This issue type is unused so let's delete it. Reviewed By: jvillard Differential Revision: D22019734 fbshipit-source-id: 8dad26a61 --- 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 | 17 ----------------- infer/src/absint/Localise.mli | 3 --- infer/src/base/IssueType.ml | 2 -- infer/src/base/IssueType.mli | 2 -- infer/src/biabduction/Attribute.ml | 6 ++---- infer/src/biabduction/Attribute.mli | 6 +----- infer/src/biabduction/BuiltinDefn.ml | 3 +-- infer/src/biabduction/Exceptions.ml | 4 ---- infer/src/biabduction/Exceptions.mli | 2 -- infer/src/biabduction/Tabulation.ml | 17 +---------------- infer/src/biabduction/Tabulation.mli | 4 ---- infer/src/biabduction/errdesc.ml | 20 -------------------- infer/src/biabduction/errdesc.mli | 3 --- 16 files changed, 5 insertions(+), 87 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 7d5dfd586..daeecfea5 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -402,7 +402,6 @@ OPTIONS DEAD_STORE (enabled by default), DEALLOCATE_STACK_VARIABLE (enabled by default), DEALLOCATE_STATIC_MEMORY (enabled by default), - DEALLOCATION_MISMATCH (enabled by default), DIRECT_ATOMIC_PROPERTY_ACCESS (enabled by default), DISCOURAGED_WEAK_PROPERTY_CUSTOM_SETTER (enabled by default), DIVIDE_BY_ZERO (disabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 37dfd4c21..5dbdca0b0 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -132,7 +132,6 @@ OPTIONS DEAD_STORE (enabled by default), DEALLOCATE_STACK_VARIABLE (enabled by default), DEALLOCATE_STATIC_MEMORY (enabled by default), - DEALLOCATION_MISMATCH (enabled by default), DIRECT_ATOMIC_PROPERTY_ACCESS (enabled by default), DISCOURAGED_WEAK_PROPERTY_CUSTOM_SETTER (enabled by default), DIVIDE_BY_ZERO (disabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index c223dbf4a..f4c5f8cbe 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -402,7 +402,6 @@ OPTIONS DEAD_STORE (enabled by default), DEALLOCATE_STACK_VARIABLE (enabled by default), DEALLOCATE_STATIC_MEMORY (enabled by default), - DEALLOCATION_MISMATCH (enabled by default), DIRECT_ATOMIC_PROPERTY_ACCESS (enabled by default), DISCOURAGED_WEAK_PROPERTY_CUSTOM_SETTER (enabled by default), DIVIDE_BY_ZERO (disabled by default), diff --git a/infer/src/absint/Localise.ml b/infer/src/absint/Localise.ml index 1d88febd2..54a6b4a31 100644 --- a/infer/src/absint/Localise.ml +++ b/infer/src/absint/Localise.ml @@ -434,23 +434,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_allocation_mismatch alloc dealloc = - let tags = Tags.create () in - let using (primitive_pname, called_pname, loc) = - let by_call = - if Procname.equal primitive_pname called_pname then "" - else " by call to " ^ MF.monospaced_to_string (Procname.to_simplified_string called_pname) - in - "using " - ^ MF.monospaced_to_string (Procname.to_simplified_string primitive_pname) - ^ by_call ^ " " - ^ at_line (Tags.create ()) (* ignore the tag *) loc - in - let description = - Format.sprintf "%s %s is deallocated %s" mem_dyn_allocated (using alloc) (using dealloc) - in - {no_desc with descriptions= [description]; tags= !tags} - let desc_condition_always_true_false i cond_str_opt loc = let tags = Tags.create () in diff --git a/infer/src/absint/Localise.mli b/infer/src/absint/Localise.mli index 3d8c0ef6e..484d6c51f 100644 --- a/infer/src/absint/Localise.mli +++ b/infer/src/absint/Localise.mli @@ -103,9 +103,6 @@ val is_parameter_not_null_checked_desc : error_desc -> bool val is_field_not_null_checked_desc : error_desc -> bool -val desc_allocation_mismatch : - Procname.t * Procname.t * Location.t -> Procname.t * Procname.t * Location.t -> error_desc - val desc_class_cast_exception : Procname.t option -> string -> string -> string option -> Location.t -> error_desc diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 69916cc9d..b6015d588 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -431,8 +431,6 @@ let deallocate_stack_variable = let deallocate_static_memory = register_from_string ~id:"DEALLOCATE_STATIC_MEMORY" Error Biabduction -let deallocation_mismatch = register_from_string ~id:"DEALLOCATION_MISMATCH" Error Biabduction - let _direct_atomic_property_access = register_from_string ~id:"DIRECT_ATOMIC_PROPERTY_ACCESS" Warning Linters ~user_documentation:[%blob "../../documentation/issues/DIRECT_ATOMIC_PROPERTY_ACCESS.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 8a4aa2e42..3f793df18 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -171,8 +171,6 @@ val deallocate_stack_variable : t val deallocate_static_memory : t -val deallocation_mismatch : t - val divide_by_zero : t val do_not_report : t diff --git a/infer/src/biabduction/Attribute.ml b/infer/src/biabduction/Attribute.ml index 238f902c1..851020e07 100644 --- a/infer/src/biabduction/Attribute.ml +++ b/infer/src/biabduction/Attribute.ml @@ -26,7 +26,7 @@ let attributes_in_same_category attr1 attr2 = (** Replace an attribute associated to the expression *) -let add_or_replace_check_changed tenv check_attribute_change prop atom = +let add_or_replace_check_changed tenv prop atom = match atom with | Predicates.Apred (att0, (_ :: _ as exps0)) | Anpred (att0, (_ :: _ as exps0)) -> let pairs = List.map ~f:(fun e -> (e, Prop.exp_normalize_prop tenv prop e)) exps0 in @@ -35,7 +35,6 @@ let add_or_replace_check_changed tenv check_attribute_change prop atom = let atom_map = function | (Predicates.Apred (att, exp :: _) | Anpred (att, exp :: _)) when Exp.equal nexp exp && attributes_in_same_category att att0 -> - check_attribute_change att att0 ; atom | atom' -> atom' @@ -50,8 +49,7 @@ let add_or_replace_check_changed tenv check_attribute_change prop atom = let add_or_replace tenv prop atom = (* wrapper for the most common case: do nothing *) - let check_attr_changed _ _ = () in - add_or_replace_check_changed tenv check_attr_changed prop atom + add_or_replace_check_changed tenv prop atom (** Get all the attributes of the prop *) diff --git a/infer/src/biabduction/Attribute.mli b/infer/src/biabduction/Attribute.mli index 18fff308e..a2a8a1048 100644 --- a/infer/src/biabduction/Attribute.mli +++ b/infer/src/biabduction/Attribute.mli @@ -27,11 +27,7 @@ val add_or_replace : Tenv.t -> Prop.normal Prop.t -> Predicates.atom -> Prop.nor (** Replace an attribute associated to the expression *) val add_or_replace_check_changed : - Tenv.t - -> (PredSymb.t -> PredSymb.t -> unit) - -> Prop.normal Prop.t - -> Predicates.atom - -> Prop.normal Prop.t + Tenv.t -> Prop.normal Prop.t -> Predicates.atom -> Prop.normal Prop.t (** Replace an attribute associated to the expression, and call the given function with new and old attributes if they changed. *) diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 5513e58e5..b4a4cfd1f 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -447,8 +447,7 @@ let execute_free_ tenv mk ?(mark_as_freed = true) loc acc iter = in (* mark value as freed *) let p_res = - Attribute.add_or_replace_check_changed tenv Tabulation.check_attr_dealloc_mismatch prop - (Apred (Aresource ra, [lexp])) + Attribute.add_or_replace_check_changed tenv prop (Apred (Aresource ra, [lexp])) in p_res :: acc else prop :: acc diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index 9b3dd888e..b62bd8f59 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/infer/src/biabduction/Exceptions.ml @@ -43,8 +43,6 @@ exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc -exception Deallocation_mismatch of Localise.error_desc * L.ocaml_pos - exception Divide_by_zero of Localise.error_desc * L.ocaml_pos exception Empty_vector_access of Localise.error_desc * L.ocaml_pos @@ -143,8 +141,6 @@ let recognize_exception exn : IssueToReport.t = {issue_type= IssueType.deallocate_stack_variable; description= desc; ocaml_pos= None} | Deallocate_static_memory desc -> {issue_type= IssueType.deallocate_static_memory; description= desc; ocaml_pos= None} - | Deallocation_mismatch (desc, ocaml_pos) -> - {issue_type= IssueType.deallocation_mismatch; description= desc; ocaml_pos= Some ocaml_pos} | Divide_by_zero (desc, ocaml_pos) -> {issue_type= IssueType.divide_by_zero; description= desc; ocaml_pos= Some ocaml_pos} | Empty_vector_access (desc, ocaml_pos) -> diff --git a/infer/src/biabduction/Exceptions.mli b/infer/src/biabduction/Exceptions.mli index 57f60905b..c3240ddec 100644 --- a/infer/src/biabduction/Exceptions.mli +++ b/infer/src/biabduction/Exceptions.mli @@ -42,8 +42,6 @@ exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc -exception Deallocation_mismatch of Localise.error_desc * Logging.ocaml_pos - exception Divide_by_zero of Localise.error_desc * Logging.ocaml_pos exception Field_not_null_checked of Localise.error_desc * Logging.ocaml_pos diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 4dbc7bb95..d99c69f89 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -671,19 +671,6 @@ let prop_footprint_add_pi_sigma_starfld_sigma tenv (prop : 'a Prop.t) pi_new sig Some (Prop.normalize tenv (Prop.set prop ~pi:pi' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp'')) -(** Check if the attribute change is a mismatch between a kind of allocation and a different kind of - deallocation *) -let check_attr_dealloc_mismatch att_old att_new = - match (att_old, att_new) with - | ( PredSymb.Aresource ({ra_kind= Racquire; ra_res= Rmemory mk_old} as ra_old) - , PredSymb.Aresource ({ra_kind= Rrelease; ra_res= Rmemory mk_new} as ra_new) ) - when PredSymb.compare_mem_kind mk_old mk_new <> 0 -> - let desc = Errdesc.explain_allocation_mismatch ra_old ra_new in - raise (Exceptions.Deallocation_mismatch (desc, __POS__)) - | _ -> - () - - (** [prop_copy_footprint p1 p2] copies the footprint and pure part of [p1] into [p2] *) let prop_copy_footprint_pure tenv p1 p2 = let p2' = Prop.set p2 ~pi_fp:p1.Prop.pi_fp ~sigma_fp:p1.Prop.sigma_fp in @@ -693,9 +680,7 @@ let prop_copy_footprint_pure tenv p1 p2 = let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *) (* if [atom] represents an attribute [att], add the attribure to [prop] *) - if Attribute.is_pred atom then - Attribute.add_or_replace_check_changed tenv check_attr_dealloc_mismatch prop atom - else prop + if Attribute.is_pred atom then Attribute.add_or_replace_check_changed tenv prop atom else prop in List.fold ~f:replace_attr ~init:(Prop.normalize tenv res_noattr) pi2_attr diff --git a/infer/src/biabduction/Tabulation.mli b/infer/src/biabduction/Tabulation.mli index 4eb138305..146517cd4 100644 --- a/infer/src/biabduction/Tabulation.mli +++ b/infer/src/biabduction/Tabulation.mli @@ -13,10 +13,6 @@ open! IStd val remove_constant_string_class : Tenv.t -> 'a Prop.t -> Prop.normal Prop.t (** Remove constant string or class from a prop *) -val check_attr_dealloc_mismatch : PredSymb.t -> PredSymb.t -> unit -(** Check if the attribute change is a mismatch between a kind of allocation and a different kind of - deallocation *) - val find_dereference_without_null_check_in_sexp : Predicates.strexp -> (int * PredSymb.path_pos) option (** Check whether a sexp contains a dereference without null check, and return the line number and diff --git a/infer/src/biabduction/errdesc.ml b/infer/src/biabduction/errdesc.ml index a52cb8064..172e1fa02 100644 --- a/infer/src/biabduction/errdesc.ml +++ b/infer/src/biabduction/errdesc.ml @@ -358,26 +358,6 @@ let exp_lv_dexp tenv = exp_lv_dexp_ tenv Exp.Set.empty let exp_rv_dexp tenv = exp_rv_dexp_ tenv Exp.Set.empty -(** Produce a description of a mismatch between an allocation function and a deallocation function *) -let explain_allocation_mismatch ra_alloc ra_dealloc = - let get_primitive_called is_alloc ra = - (* primitive alloc/dealloc function ultimately used, and function actually called *) - (* e.g. malloc and my_malloc *) - let primitive = - match ra.PredSymb.ra_res with - | PredSymb.Rmemory mk_alloc -> - (if is_alloc then PredSymb.mem_alloc_pname else PredSymb.mem_dealloc_pname) mk_alloc - | _ -> - ra_alloc.PredSymb.ra_pname - in - let called = ra.PredSymb.ra_pname in - (primitive, called, ra.PredSymb.ra_loc) - in - Localise.desc_allocation_mismatch - (get_primitive_called true ra_alloc) - (get_primitive_called false ra_dealloc) - - (** check whether the type of leaked [hpred] appears as a predicate in an inductive predicate in [prop] *) let leak_from_list_abstraction hpred prop = diff --git a/infer/src/biabduction/errdesc.mli b/infer/src/biabduction/errdesc.mli index 9b04eaf1c..ca04a9b33 100644 --- a/infer/src/biabduction/errdesc.mli +++ b/infer/src/biabduction/errdesc.mli @@ -23,9 +23,6 @@ val find_ident_assignment : Procdesc.Node.t -> Ident.t -> (Procdesc.Node.t * Exp val exp_rv_dexp : Tenv.t -> Procdesc.Node.t -> Exp.t -> DecompiledExp.t option (** describe rvalue [e] as a dexp *) -val explain_allocation_mismatch : PredSymb.res_action -> PredSymb.res_action -> Localise.error_desc -(** Produce a description of a mismatch between an allocation function and a deallocation function *) - val explain_array_access : Procname.t -> Tenv.t -> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc (** Produce a description of the array access performed in the current instruction, if any. *)