From a87bedb5dd7e68b964b74cf6beb61253af376a92 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Tue, 30 Jun 2015 07:22:07 -0200 Subject: [PATCH] [Bucketing] Promote NPEs originating from a call with a null parameter to bucket b1. --- infer/src/backend/buckets.ml | 17 +++++--- infer/src/backend/buckets.mli | 7 +-- infer/src/backend/errdesc.ml | 43 ++++++++++--------- .../null_pointer_dereference.c | 4 ++ .../tests/endtoend/c/NullDereferenceTest.java | 1 + 5 files changed, 43 insertions(+), 29 deletions(-) diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index 36f27ed9e..a8268f418 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -39,8 +39,9 @@ let check_nested_loop path pos_opt = Paths.Path.iter_longest_sequence f pos_opt path; in_nested_loop () -(** Check that we know where the value was last assigned, and that there is a local access instruction at that line. **) -let check_access access_opt = +(** Check that we know where the value was last assigned, +and that there is a local access instruction at that line. **) +let check_access access_opt de_opt = let find_bucket line_number null_case_flag = let find_formal_ids node = (* find ids obtained by a letref on a formal parameter *) let node_instrs = Cfg.Node.get_instrs node in @@ -99,11 +100,17 @@ let check_access access_opt = find_bucket n false | Some (Localise.Last_accessed (n, is_nullable)) when is_nullable -> Some Localise.BucketLevel.b1 - | _ -> None + | _ -> + begin + match de_opt with + | Some (Sil.Dconst _) -> + Some Localise.BucketLevel.b1 + | _ -> None + end -let classify_access desc access_opt is_nullable = +let classify_access desc access_opt de_opt is_nullable = let default_bucket = if is_nullable then Localise.BucketLevel.b1 else Localise.BucketLevel.b5 in let show_in_message = !Config.show_buckets in - match check_access access_opt with + match check_access access_opt de_opt with | None -> Localise.error_desc_set_bucket desc default_bucket show_in_message | Some bucket -> Localise.error_desc_set_bucket desc bucket show_in_message diff --git a/infer/src/backend/buckets.mli b/infer/src/backend/buckets.mli index 8c67c12b0..c18d2ad3e 100644 --- a/infer/src/backend/buckets.mli +++ b/infer/src/backend/buckets.mli @@ -1,6 +1,6 @@ (* -* Copyright (c) 2009-2013 Monoidics ltd. -* Copyright (c) 2013- Facebook. +* Copyright (c) 2009 -2013 Monoidics ltd. +* Copyright (c) 2013 - Facebook. * All rights reserved. *) @@ -9,4 +9,5 @@ open Utils (** Classify the bucket of an error desc using Location.access and nullable information *) -val classify_access : Localise.error_desc -> Localise.access option -> bool -> Localise.error_desc +val classify_access : +Localise.error_desc -> Localise.access option -> Sil.dexp option -> bool -> Localise.error_desc diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index b2ec57e3d..ef1130229 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -141,7 +141,7 @@ let find_ident_assignment node id : (Cfg.Node.t * Sil.exp) option = visited := Cfg.NodeSet.add node !visited; let res = ref None in let find_instr = function - | Sil.Letderef(_id, e, _,_) when Ident.equal _id id -> + | Sil.Letderef(_id, e, _, _) when Ident.equal _id id -> res := Some (node, e); true | _ -> false in @@ -728,20 +728,20 @@ let explain_dereference_access outermost_array is_nullable _de_opt prop = (** Create a description of a dereference operation *) let create_dereference_desc - ?use_buckets:(use_buckets=false) - ?outermost_array:(outermost_array=false) - ?is_nullable:(is_nullable=false) - ?is_premature_nil:(is_premature_nil=false) - _de_opt deref_str prop loc = + ?use_buckets: (use_buckets = false) + ?outermost_array: (outermost_array = false) + ?is_nullable: (is_nullable = false) + ?is_premature_nil: (is_premature_nil = false) + de_opt deref_str prop loc = let value_str, access_opt = - explain_dereference_access outermost_array is_nullable _de_opt prop in + explain_dereference_access outermost_array is_nullable de_opt prop in let access_opt' = match access_opt with | Some (Localise.Last_accessed _) when outermost_array -> None (* don't report last accessed for arrays *) | _ -> access_opt in let desc = Localise.dereference_string deref_str value_str access_opt' loc in let desc = if !Sil.curr_language = Sil.C_CPP && not is_premature_nil then - match _de_opt with + match de_opt with | Some (Sil.Dpvar pvar) | Some (Sil.Dpvaraddr pvar) -> (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with @@ -749,7 +749,7 @@ let create_dereference_desc | _ -> desc) | _ -> desc else desc in - if use_buckets then Buckets.classify_access desc access_opt' is_nullable + if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable else desc (** explain memory access performed by the current instruction @@ -757,11 +757,11 @@ if outermost_array is true, the outermost array access is removed if outermost_dereference is true, stop at the outermost dereference (skipping e.g. outermost field access) *) let _explain_access - ?use_buckets:(use_buckets=false) - ?outermost_array:(outermost_array=false) - ?outermost_dereference:(outermost_dereference=false) - ?is_nullable:(is_nullable=false) - ?is_premature_nil:(is_premature_nil=false) + ?use_buckets: (use_buckets = false) + ?outermost_array: (outermost_array = false) + ?outermost_dereference: (outermost_dereference = false) + ?is_nullable: (is_nullable = false) + ?is_premature_nil: (is_premature_nil = false) deref_str prop loc = let rec find_outermost_dereference node e = match e with | Sil.Const c -> @@ -822,18 +822,18 @@ let _explain_access (** Produce a description of which expression is dereferenced in the current instruction, if any. The subexpression to focus on is obtained by removing field and index accesses. *) let explain_dereference - ?use_buckets:(use_buckets=false) - ?is_nullable:(is_nullable=false) - ?is_premature_nil:(is_premature_nil=false) + ?use_buckets: (use_buckets = false) + ?is_nullable: (is_nullable = false) + ?is_premature_nil: (is_premature_nil = false) deref_str prop loc = _explain_access - ~use_buckets ~outermost_array:false ~outermost_dereference:true ~is_nullable ~is_premature_nil + ~use_buckets ~outermost_array: false ~outermost_dereference: true ~is_nullable ~is_premature_nil deref_str prop loc (** Produce a description of the array access performed in the current instruction, if any. The subexpression to focus on is obtained by removing the outermost array access. *) let explain_array_access deref_str prop loc = - _explain_access ~outermost_array:true deref_str prop loc + _explain_access ~outermost_array: true deref_str prop loc (** Produce a description of the memory access performed in the current instruction, if any. *) let explain_memory_access deref_str prop loc = @@ -865,7 +865,8 @@ let explain_nth_function_parameter use_buckets deref_str prop n pvar_off = let arg = fst (list_nth args (n - 1)) in let dexp_opt = exp_rv_dexp node arg in let dexp_opt' = match dexp_opt with - | Some de -> Some (dexp_apply_pvar_off de pvar_off) + | Some de -> + Some (dexp_apply_pvar_off de pvar_off) | None -> None in create_dereference_desc ~use_buckets dexp_opt' deref_str prop loc with exn when exn_not_timeout exn -> Localise.no_desc) @@ -899,7 +900,7 @@ let find_pvar_with_exp prop exp = (** return a description explaining value [exp] in [prop] in terms of a source expression using the formal parameters of the call *) let explain_dereference_as_caller_expression - ?use_buckets:(use_buckets=false) + ?use_buckets: (use_buckets = false) deref_str actual_pre spec_pre exp node loc formal_params = let find_formal_param_number name = let rec find n = function diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c b/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c index 5aeeb4c2b..d1bbbc0b4 100644 --- a/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c @@ -89,6 +89,10 @@ void potentially_null_pointer_passed_as_argument() { free(p); } +void null_passed_as_argument() { + assign(NULL, 42); // NULL dereference +} + void allocated_pointer_passed_as_argument() { int *p = NULL; p = (int*) malloc(sizeof(int)); diff --git a/infer/tests/endtoend/c/NullDereferenceTest.java b/infer/tests/endtoend/c/NullDereferenceTest.java index 08e405bfd..2463c2ce8 100644 --- a/infer/tests/endtoend/c/NullDereferenceTest.java +++ b/infer/tests/endtoend/c/NullDereferenceTest.java @@ -44,6 +44,7 @@ public class NullDereferenceTest { "no_check_for_null_after_malloc", "no_check_for_null_after_realloc", "potentially_null_pointer_passed_as_argument", + "null_passed_as_argument", "function_call_can_return_null_pointer", }; assertThat(