From 219cc64cb68318b20fc4f7ef750f5267d3d994dc Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Thu, 18 Jun 2020 03:16:41 -0700 Subject: [PATCH] [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 | 1 - infer/man/man1/infer-report.txt | 1 - infer/man/man1/infer.txt | 1 - infer/src/absint/Localise.ml | 10 ---- infer/src/absint/Localise.mli | 2 - infer/src/base/IssueType.ml | 4 -- infer/src/base/IssueType.mli | 2 - infer/src/biabduction/Exceptions.ml | 6 -- infer/src/biabduction/Exceptions.mli | 2 - infer/src/biabduction/SymExec.ml | 60 ------------------- infer/src/biabduction/Tabulation.mli | 5 -- infer/src/biabduction/errdesc.ml | 10 ---- infer/src/biabduction/errdesc.mli | 4 -- .../codetoanalyze/c/biabduction/issues.exp | 2 - .../biabduction/null_test_after_deref/basic.c | 21 ------- .../codetoanalyze/objc/biabduction/issues.exp | 1 - 16 files changed, 132 deletions(-) delete mode 100644 infer/tests/codetoanalyze/c/biabduction/null_test_after_deref/basic.c diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 72666c491..7fcaebbec 100644 --- a/infer/man/man1/infer-full.txt +++ b/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), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 2ced7a413..6e88fe21f 100644 --- a/infer/man/man1/infer-report.txt +++ b/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), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 3bc2c395c..8189e6741 100644 --- a/infer/man/man1/infer.txt +++ b/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), diff --git a/infer/src/absint/Localise.ml b/infer/src/absint/Localise.ml index 6a8a48de5..f1ebbbd3d 100644 --- a/infer/src/absint/Localise.ml +++ b/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 diff --git a/infer/src/absint/Localise.mli b/infer/src/absint/Localise.mli index 351fe2889..0ed6651e3 100644 --- a/infer/src/absint/Localise.mli +++ b/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 *) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 77273dc35..f92b6dc69 100644 --- a/infer/src/base/IssueType.ml +++ b/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)." diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index ec9f551ab..e1c8e87f3 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index 27fe30148..4baeff8bf 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/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 -> diff --git a/infer/src/biabduction/Exceptions.mli b/infer/src/biabduction/Exceptions.mli index 1176bc42c..7e1e95a10 100644 --- a/infer/src/biabduction/Exceptions.mli +++ b/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 diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 097f70aa9..4f1151633 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/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) -> ( diff --git a/infer/src/biabduction/Tabulation.mli b/infer/src/biabduction/Tabulation.mli index 146517cd4..d00e62189 100644 --- a/infer/src/biabduction/Tabulation.mli +++ b/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 *) diff --git a/infer/src/biabduction/errdesc.ml b/infer/src/biabduction/errdesc.ml index 34af389fe..511a05432 100644 --- a/infer/src/biabduction/errdesc.ml +++ b/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 diff --git a/infer/src/biabduction/errdesc.mli b/infer/src/biabduction/errdesc.mli index 1c2283b8e..7089cdaab 100644 --- a/infer/src/biabduction/errdesc.mli +++ b/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 *) diff --git a/infer/tests/codetoanalyze/c/biabduction/issues.exp b/infer/tests/codetoanalyze/c/biabduction/issues.exp index a71ec33cb..e533958b1 100644 --- a/infer/tests/codetoanalyze/c/biabduction/issues.exp +++ b/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 diff --git a/infer/tests/codetoanalyze/c/biabduction/null_test_after_deref/basic.c b/infer/tests/codetoanalyze/c/biabduction/null_test_after_deref/basic.c deleted file mode 100644 index a648444b8..000000000 --- a/infer/tests/codetoanalyze/c/biabduction/null_test_after_deref/basic.c +++ /dev/null @@ -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; -} diff --git a/infer/tests/codetoanalyze/objc/biabduction/issues.exp b/infer/tests/codetoanalyze/objc/biabduction/issues.exp index 649d52f6b..fde1a8613 100644 --- a/infer/tests/codetoanalyze/objc/biabduction/issues.exp +++ b/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()]