[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

@@ -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),

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),

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),

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

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
 

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"]

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

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 prop atom
-  add_or_replace_check_changed tenv check_attr_changed prop atom
 
 
 (** Get all the attributes of the prop *)

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
+  Tenv.t -> Prop.normal Prop.t -> Predicates.atom -> Prop.normal Prop.t
-  -> (PredSymb.t -> PredSymb.t -> unit)
-  -> 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. *)
 

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
+          Attribute.add_or_replace_check_changed tenv prop (Apred (Aresource ra, [lexp]))
-            (Apred (Aresource ra, [lexp]))
         in
         p_res :: acc
       else prop :: acc

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) ->

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

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
+    if Attribute.is_pred atom then Attribute.add_or_replace_check_changed tenv prop atom else prop
-      Attribute.add_or_replace_check_changed tenv check_attr_dealloc_mismatch prop atom
-    else prop
   in
   List.fold ~f:replace_attr ~init:(Prop.normalize tenv res_noattr) pi2_attr
 

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

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 =

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. *)