[biabduction] Delete null_test_after_dereference check

Summary: This is not used, so let's delete it.

Reviewed By: jvillard

Differential Revision: D22113242

fbshipit-source-id: e0520d859

infer/man/man1/infer-full.txt

@@ -481,7 +481,6 @@ OPTIONS
              Missing_fld (enabled by default),
              NULLPTR_DEREFERENCE (disabled by default),
              NULL_DEREFERENCE (enabled by default),
-             NULL_TEST_AFTER_DEREFERENCE (disabled by default),
              PARAMETER_NOT_NULL_CHECKED (enabled by default),
              POINTER_SIZE_MISMATCH (enabled by default),
              POINTER_TO_CONST_OBJC_CLASS (enabled by default),

infer/man/man1/infer-report.txt

@@ -201,7 +201,6 @@ OPTIONS
              Missing_fld (enabled by default),
              NULLPTR_DEREFERENCE (disabled by default),
              NULL_DEREFERENCE (enabled by default),
-             NULL_TEST_AFTER_DEREFERENCE (disabled by default),
              PARAMETER_NOT_NULL_CHECKED (enabled by default),
              POINTER_SIZE_MISMATCH (enabled by default),
              POINTER_TO_CONST_OBJC_CLASS (enabled by default),

infer/man/man1/infer.txt

@@ -481,7 +481,6 @@ OPTIONS
              Missing_fld (enabled by default),
              NULLPTR_DEREFERENCE (disabled by default),
              NULL_DEREFERENCE (enabled by default),
-             NULL_TEST_AFTER_DEREFERENCE (disabled by default),
              PARAMETER_NOT_NULL_CHECKED (enabled by default),
              POINTER_SIZE_MISMATCH (enabled by default),
              POINTER_TO_CONST_OBJC_CLASS (enabled by default),

infer/src/absint/Localise.ml

@@ -552,16 +552,6 @@ let desc_precondition_not_met kind proc_name loc =
   {no_desc with descriptions= kind_str @ ["in " ^ call_to_at_line tags proc_name loc]; tags= !tags}
 
 
-let desc_null_test_after_dereference expr_str line loc =
-  let tags = Tags.create () in
-  Tags.update tags Tags.value expr_str ;
-  let description =
-    Format.asprintf "Pointer %a was dereferenced at line %d and is tested for null %s"
-      MF.pp_monospaced expr_str line (at_line tags loc)
-  in
-  {no_desc with descriptions= [description]; tags= !tags}
-
-
 let desc_retain_cycle cycle_str loc cycle_dotty =
   Logging.d_strln "Proposition with retain cycle:" ;
   let tags = Tags.create () in

infer/src/absint/Localise.mli

@@ -122,8 +122,6 @@ val desc_leak :
   -> string option
   -> error_desc
 
-val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
-
 val desc_custom_error : Location.t -> error_desc
 (** Create human-readable error description for assertion failures *)
 

infer/src/base/IssueType.ml

@@ -775,10 +775,6 @@ let null_dereference =
     ~user_documentation:[%blob "../../documentation/issues/NULL_DEREFERENCE.md"]
 
 
-let null_test_after_dereference =
-  register_from_string ~enabled:false ~id:"NULL_TEST_AFTER_DEREFERENCE" Warning Biabduction
-
-
 let nullptr_dereference =
   register_from_string ~enabled:false ~id:"NULLPTR_DEREFERENCE" Error Pulse
     ~user_documentation:"See [NULL_DEREFERENCE](#null_dereference)."

infer/src/base/IssueType.mli

@@ -283,8 +283,6 @@ val mutable_local_variable_in_component_file : t
 
 val null_dereference : t
 
-val null_test_after_dereference : t
-
 val nullptr_dereference : t
 
 val parameter_not_null_checked : t

infer/src/biabduction/Exceptions.ml

@@ -59,8 +59,6 @@ exception Premature_nil_termination of Localise.error_desc * L.ocaml_pos
 
 exception Null_dereference of Localise.error_desc * L.ocaml_pos
 
-exception Null_test_after_dereference of Localise.error_desc * L.ocaml_pos
-
 exception Parameter_not_null_checked of Localise.error_desc * L.ocaml_pos
 
 exception Pointer_size_mismatch of Localise.error_desc * L.ocaml_pos
@@ -130,10 +128,6 @@ let recognize_exception exn : IssueToReport.t =
       {issue_type= IssueType.field_not_null_checked; description= desc; ocaml_pos= Some ocaml_pos}
   | Null_dereference (desc, ocaml_pos) ->
       {issue_type= IssueType.null_dereference; description= desc; ocaml_pos= Some ocaml_pos}
-  | Null_test_after_dereference (desc, ocaml_pos) ->
-      { issue_type= IssueType.null_test_after_dereference
-      ; description= desc
-      ; ocaml_pos= Some ocaml_pos }
   | Pointer_size_mismatch (desc, ocaml_pos) ->
       {issue_type= IssueType.pointer_size_mismatch; description= desc; ocaml_pos= Some ocaml_pos}
   | Inherently_dangerous_function desc ->

infer/src/biabduction/Exceptions.mli

@@ -58,8 +58,6 @@ exception Premature_nil_termination of Localise.error_desc * Logging.ocaml_pos
 
 exception Null_dereference of Localise.error_desc * Logging.ocaml_pos
 
-exception Null_test_after_dereference of Localise.error_desc * Logging.ocaml_pos
-
 exception Parameter_not_null_checked of Localise.error_desc * Logging.ocaml_pos
 
 exception Pointer_size_mismatch of Localise.error_desc * Logging.ocaml_pos

infer/src/biabduction/SymExec.ml

@@ -424,63 +424,6 @@ let check_arith_norm_exp {InterproceduralAnalysis.proc_desc; err_log; tenv} exp
       (Prop.exp_normalize_prop tenv prop exp, prop')
 
 
-(** Check if [cond] is testing for NULL a pointer already dereferenced *)
-let check_already_dereferenced {InterproceduralAnalysis.proc_desc; err_log; tenv} cond prop =
-  let find_hpred lhs =
-    List.find
-      ~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e lhs | _ -> false)
-      prop.Prop.sigma
-  in
-  let rec is_check_zero = function
-    | Exp.Var id ->
-        Some id
-    | Exp.UnOp (Unop.LNot, e, _) ->
-        is_check_zero e
-    | Exp.BinOp ((Binop.Eq | Binop.Ne), Exp.Const (Const.Cint i), Exp.Var id)
-    | Exp.BinOp ((Binop.Eq | Binop.Ne), Exp.Var id, Exp.Const (Const.Cint i))
-      when IntLit.iszero i ->
-        Some id
-    (* These two patterns appear frequently in Prune nodes *)
-    | Exp.BinOp
-        ( (Binop.Eq | Binop.Ne)
-        , Exp.BinOp (Binop.Eq, Exp.Var id, Exp.Const (Const.Cint i))
-        , Exp.Const (Const.Cint j) )
-    | Exp.BinOp
-        ( (Binop.Eq | Binop.Ne)
-        , Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), Exp.Var id)
-        , Exp.Const (Const.Cint j) )
-      when IntLit.iszero i && IntLit.iszero j ->
-        Some id
-    | _ ->
-        None
-  in
-  let dereferenced_line =
-    match is_check_zero cond with
-    | Some id -> (
-      match find_hpred (Prop.exp_normalize_prop tenv prop (Exp.Var id)) with
-      | Some (Predicates.Hpointsto (_, se, _)) -> (
-        match Tabulation.find_dereference_without_null_check_in_sexp se with
-        | Some n ->
-            Some (id, n)
-        | None ->
-            None )
-      | _ ->
-          None )
-    | None ->
-        None
-  in
-  match dereferenced_line with
-  | Some (id, (n, _)) ->
-      let desc =
-        Errdesc.explain_null_test_after_dereference tenv (Exp.Var id)
-          (AnalysisState.get_node_exn ()) n (AnalysisState.get_loc_exn ())
-      in
-      let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in
-      BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log exn
-  | None ->
-      ()
-
-
 let method_exists right_proc_name methods =
   if Language.curr_language_is Java then
     List.exists ~f:(fun meth_name -> Procname.equal right_proc_name meth_name) methods
@@ -1154,7 +1097,6 @@ let rec sym_exec
     ( {InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; err_log; tenv} as
     analysis_data ) instr_ (prop_ : Prop.normal Prop.t) path :
     (Prop.normal Prop.t * Paths.Path.t) list =
-  let current_pname = Procdesc.get_proc_name current_pdesc in
   AnalysisState.set_instr instr_ ;
   (* mark instruction last seen *)
   State.set_prop_tenv_pdesc prop_ tenv current_pdesc ;
@@ -1214,8 +1156,6 @@ let rec sym_exec
       execute_store analysis_data lhs_exp typ rhs_exp loc prop_ |> ret_old_path
   | Sil.Prune (cond, _, _, _) ->
       let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in
-      if not (Procname.is_java current_pname) then
-        check_already_dereferenced analysis_data cond prop__ ;
       let n_cond, prop = check_arith_norm_exp analysis_data cond prop__ in
       ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop))
   | Sil.Call (ret_id_typ, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> (

infer/src/biabduction/Tabulation.mli

@@ -13,11 +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 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
-    path position *)
-
 val create_cast_exception :
   Tenv.t -> Logging.ocaml_pos -> Procname.t option -> Exp.t -> Exp.t -> Exp.t -> exn
 (** raise a cast exception *)

infer/src/biabduction/errdesc.ml

@@ -1112,15 +1112,5 @@ let explain_unary_minus_applied_to_unsigned_expression tenv exp typ node loc =
   Localise.desc_unary_minus_applied_to_unsigned_expression exp_str_opt typ_str loc
 
 
-(** explain a test for NULL of a dereferenced pointer *)
-let explain_null_test_after_dereference tenv exp node line loc =
-  match exp_rv_dexp tenv node exp with
-  | Some de ->
-      let expr_str = DExp.to_string de in
-      Localise.desc_null_test_after_dereference expr_str line loc
-  | None ->
-      Localise.no_desc
-
-
 let warning_err loc fmt_string =
   L.(debug Analysis Medium) ("%a: Warning: " ^^ fmt_string) Location.pp loc

infer/src/biabduction/errdesc.mli

@@ -87,10 +87,6 @@ val explain_leak :
     variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the
     current node. If there is an alloc attribute, print the function call and line number. *)
 
-val explain_null_test_after_dereference :
-  Tenv.t -> Exp.t -> Procdesc.Node.t -> int -> Location.t -> Localise.error_desc
-(** explain a test for NULL of a dereferenced pointer *)
-
 val warning_err : Location.t -> ('a, Format.formatter, unit) format -> 'a
 (** warn at the given location *)
 

infer/tests/codetoanalyze/c/biabduction/issues.exp

@@ -31,7 +31,6 @@ codetoanalyze/c/biabduction/memory_leaks/cleanup_attribute.c, FP_cleanup_malloc_
 codetoanalyze/c/biabduction/memory_leaks/cleanup_attribute.c, FP_cleanup_string_good, 2, BIABDUCTION_MEMORY_LEAK, no_bucket
 codetoanalyze/c/biabduction/memory_leaks/test.c, common_realloc_leak, 3, BIABDUCTION_MEMORY_LEAK, no_bucket
 codetoanalyze/c/biabduction/memory_leaks/test.c, common_realloc_leak2, 3, BIABDUCTION_MEMORY_LEAK, no_bucket
-codetoanalyze/c/biabduction/memory_leaks/test.c, common_realloc_leak2, 5, NULL_TEST_AFTER_DEREFERENCE, no_bucket
 codetoanalyze/c/biabduction/memory_leaks/test.c, conditional_last_instruction, 2, BIABDUCTION_MEMORY_LEAK, no_bucket
 codetoanalyze/c/biabduction/memory_leaks/test.c, malloc_sizeof_value_leak_bad, 7, BIABDUCTION_MEMORY_LEAK, no_bucket
 codetoanalyze/c/biabduction/memory_leaks/test.c, malloc_sizeof_value_leak_bad, 8, ARRAY_OUT_OF_BOUNDS_L3, no_bucket
@@ -106,7 +105,6 @@ codetoanalyze/c/biabduction/null_dereference/null_pointer_dereference.c, unreach
 codetoanalyze/c/biabduction/null_dereference/short.c, ternary2_bad, 2, NULL_DEREFERENCE, B1
 codetoanalyze/c/biabduction/null_dereference/short.c, ternary4_bad, 2, NULL_DEREFERENCE, B1
 codetoanalyze/c/biabduction/null_dereference/short.c, ternary7_bad, 2, NULL_DEREFERENCE, B1
-codetoanalyze/c/biabduction/null_test_after_deref/basic.c, null_test_deref_basic_bad, 2, NULL_TEST_AFTER_DEREFERENCE, no_bucket
 codetoanalyze/c/biabduction/resource_leaks/leak.c, fileNotClosed, 5, RESOURCE_LEAK, no_bucket
 codetoanalyze/c/biabduction/resource_leaks/leak.c, socketNotClosed, 5, RESOURCE_LEAK, no_bucket
 codetoanalyze/c/biabduction/sizeof/sizeof_706.c, sentinel_bad, 0, DIVIDE_BY_ZERO, no_bucket

infer/tests/codetoanalyze/c/biabduction/null_test_after_deref/basic.c

@@ -1,21 +0,0 @@
-/*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- */
-int null_test_deref_basic_bad(int* p) {
-  int ret = *p;
-  if (p == 0)
-    return -1;
-  return ret;
-}
-
-int null_test_deref_basic_ok() {
-  int x = 0;
-  int* p = &x;
-  int ret = *p;
-  if (p == 0)
-    return -1;
-  return ret;
-}

infer/tests/codetoanalyze/objc/biabduction/issues.exp

@@ -24,7 +24,6 @@ codetoanalyze/objc/shared/block/block_no_args.m, Block_no_args.m, 10, NULL_DEREF
 codetoanalyze/objc/shared/category_procdesc/main.c, CategoryProcdescMain, 3, BIABDUCTION_MEMORY_LEAK, no_bucket, ERROR, [start of procedure CategoryProcdescMain(),Skipping performDaysWork: method has no implementation]
 codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper.init, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure init]
 codetoanalyze/objc/biabduction/blocks_in_heap/BlockInHeap.m, block_in_heap_executed_after_bi_abduction_ok_test, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure block_in_heap_executed_after_bi_abduction_ok_test(),start of procedure block_in_heap_executed_after_bi_abduction_ok_no_retain_cycle(),start of procedure assign_block_to_ivar,Executing synthesized setter setHandler:,return from a call to BlockInHeap.assign_block_to_ivar,Executing synthesized getter handler,start of procedure block,return from a call to objc_blockBlockInHeap.assign_block_to_ivar_1,return from a call to block_in_heap_executed_after_bi_abduction_ok_no_retain_cycle,Taking true branch]
-codetoanalyze/objc/biabduction/field_superclass/SubtypingExample.m, Employee.initWithName:andAge:andEducation:, 3, NULL_TEST_AFTER_DEREFERENCE, no_bucket, WARNING, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person.initWithName:andAge:,Taking false branch]
 codetoanalyze/objc/biabduction/field_superclass/SubtypingExample.m, Employee.initWithName:andAge:andEducation:, 6, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person.initWithName:andAge:,Taking true branch]
 codetoanalyze/objc/biabduction/field_superclass/SubtypingExample.m, subtyping_test, 0, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure subtyping_test(),start of procedure testFields(),start of procedure setEmployeeEducation:,return from a call to Employee.setEmployeeEducation:,start of procedure setAge:,return from a call to Person.setAge:,start of procedure setEmployeeEducation:,return from a call to Employee.setEmployeeEducation:,start of procedure getAge,return from a call to Person.getAge,return from a call to testFields]
 codetoanalyze/objc/biabduction/initialization/struct_initlistexpr.c, field_set_correctly, 2, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure field_set_correctly()]