[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

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

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

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

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

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

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

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

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

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

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

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
+      match Attribute.get_undef tenv actual_pre e_sub with
-      | Some (Apred (Aresource ({ra_kind= Rrelease} as ra), _)) ->
+      | Some (Apred (Aundef (s, _, loc, pos), _)) ->
-          Some (Deref_freed ra, desc true (Localise.deref_str_freed ra))
+          Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc)))
-      | _ -> (
+      | _ ->
-        match Attribute.get_undef tenv actual_pre e_sub with
+          None
-        | 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__))

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
+        ; empty_vector_access ]
-        ; biabd_use_after_free ]
       in
       List.mem ~equal:IssueType.equal null_deref_issue_types issue_type
     in

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<Person>(): 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<Person>, 2, BIABDUCTION_MEMORY_LEAK, CPP, ERROR, [start of procedure template_typeid<Person>(),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]