diff --git a/infer/src/IR/sil.ml b/infer/src/IR/sil.ml index 47f501058..16dc82d4f 100644 --- a/infer/src/IR/sil.ml +++ b/infer/src/IR/sil.ml @@ -627,8 +627,8 @@ and attribute = | Adiv0 of path_pos (** the exp. is null because of a call to a method with exp as a null receiver *) | Aobjc_null of exp - (** value was returned from a call to the given procedure *) - | Aretval of Procname.t + (** value was returned from a call to the given procedure, plus the annots of the return value *) + | Aretval of Procname.t * item_annotation (** denotes an object registered as an observers to a notification center *) | Aobserver (** denotes an object unsubscribed from observers of a notification center *) @@ -1381,7 +1381,11 @@ and attribute_compare (att1 : attribute) (att2 : attribute) : int = exp_compare exp1 exp2 | Aobjc_null _, _ -> -1 | _, Aobjc_null _ -> 1 - | Aretval pn1, Aretval pn2 -> Procname.compare pn1 pn2 + | Aretval (pn1, annots1), Aretval (pn2, annots2) -> + let n = Procname.compare pn1 pn2 in + if n <> 0 + then n + else item_annotation_compare annots1 annots2 | Aretval _, _ -> -1 | _, Aretval _ -> 1 | Aobserver, Aobserver -> 0 @@ -1900,7 +1904,7 @@ and attribute_to_string pe = function | Lfield _ -> "FIELD " ^ (exp_to_string exp) | _ -> "" in "OBJC_NULL["^ info_s ^"]" - | Aretval pn -> "RET" ^ str_binop pe Lt ^ Procname.to_string pn ^ str_binop pe Gt + | Aretval (pn, _) -> "RET" ^ str_binop pe Lt ^ Procname.to_string pn ^ str_binop pe Gt | Aobserver -> "OBSERVER" | Aunsubscribed_observer -> "UNSUBSCRIBED_OBSERVER" diff --git a/infer/src/IR/sil.mli b/infer/src/IR/sil.mli index bd18f725f..94aabad3c 100644 --- a/infer/src/IR/sil.mli +++ b/infer/src/IR/sil.mli @@ -265,7 +265,7 @@ and attribute = (** the exp. is null because of a call to a method with exp as a null receiver *) | Aobjc_null of exp (** value was returned from a call to the given procedure *) - | Aretval of Procname.t + | Aretval of Procname.t * item_annotation (** denotes an object registered as an observers to a notification center *) | Aobserver (** denotes an object unsubscribed from observers of a notification center *) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 95ff92367..0a8f74718 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1841,6 +1841,9 @@ let get_div0_attribute prop exp = let get_observer_attribute prop exp = get_attribute prop exp Sil.ACobserver +let get_retval_attribute prop exp = + get_attribute prop exp Sil.ACretval + let has_dangling_uninit_attribute prop exp = let la = get_exp_attributes prop exp in IList.exists (fun a -> Sil.attribute_equal a (Sil.Adangling (Sil.DAuninit))) la diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 32c946397..c37ffb077 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -302,6 +302,9 @@ val get_observer_attribute : 'a t -> exp -> attribute option (** Get the objc null attribute associated to the expression, if any *) val get_objc_null_attribute : 'a t -> exp -> attribute option +(** Get the retval null attribute associated to the expression, if any *) +val get_retval_attribute : 'a t -> exp -> attribute option + (** Get all the attributes of the prop *) val get_all_attributes : 'a t -> (exp * attribute) list diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 468fd112a..a2fb7e836 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -945,9 +945,21 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = match hpred with | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var _ as exp, _), _) when Sil.exp_equal exp deref_exp -> - let is_nullable = Annotations.param_is_nullable pvar ann_sig in - if is_nullable then - nullable_obj_str := Some (Pvar.to_string pvar); + + let is_nullable = + if Annotations.param_is_nullable pvar ann_sig + then + begin + nullable_obj_str := Some (Pvar.to_string pvar); + true + end + else + match Prop.get_retval_attribute prop exp with + | Some (Sil.Aretval (pname, ret_attr)) when Annotations.ia_is_nullable ret_attr -> + nullable_obj_str := Some (Procname.to_string pname); + true + | _ -> + false in (* it's ok for a non-nullable local to point to deref_exp *) is_nullable || Pvar.is_local pvar | Sil.Hpointsto (_, Sil.Estruct (flds, _), Sil.Sizeof (typ, _)) -> diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 74c9c8791..6bdd5d817 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -878,7 +878,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = IList.exists (fun (exp, attr) -> match attr with - | Sil.Aretval pname when Procname.equal callee_pname pname -> + | Sil.Aretval (pname, _) when Procname.equal callee_pname pname -> Prover.check_disequal prop exp Sil.exp_zero | _ -> false) (Prop.get_all_attributes prop) in @@ -911,7 +911,6 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = if !Config.taint_analysis then mk_retval_tainted posts' else posts' | _ -> posts - (** Check if actual_pre * missing_footprint |- false *) let inconsistent_actualpre_missing actual_pre split_opt = match split_opt with @@ -1124,7 +1123,7 @@ let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = Prop.normalize (Prop.replace_pi_footprint (Prop.get_pi_footprint p @ new_footprint_atoms) p) (** post-process the raw result of a function call *) -let exe_call_postprocess ret_ids trace_call callee_pname loc results = +let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc results = let filter_valid_res = function | Invalid_res _ -> false | Valid_res _ -> true in @@ -1245,21 +1244,24 @@ let exe_call_postprocess ret_ids trace_call callee_pname loc results = IList.map (fun (p, path) -> (quantify_path_idents_remove_constant_strings p, path)) res_with_path_idents in + let ret_annot, _ = callee_attrs.ProcAttributes.method_annotation in + let returns_nullable ret_annot = Annotations.ia_is_nullable ret_annot in let should_add_ret_attr _ = let is_likely_getter = function | Procname.Java pn_java -> IList.length (Procname.java_get_parameters pn_java) = 0 | _ -> false in - !Config.idempotent_getters && - !Config.curr_language = Config.Java && - is_likely_getter callee_pname in + (!Config.idempotent_getters && + !Config.curr_language = Config.Java && + is_likely_getter callee_pname) + || returns_nullable ret_annot in match ret_ids with | [ret_id] when should_add_ret_attr ()-> (* add attribute to remember what function call a return id came from *) let ret_var = Sil.Var ret_id in let mark_id_as_retval (p, path) = - let att_retval = Sil.Aretval callee_pname in + let att_retval = Sil.Aretval (callee_pname, ret_annot) in Prop.set_exp_attribute p ret_var att_retval, path in IList.map mark_id_as_retval res | _ -> res @@ -1298,7 +1300,7 @@ let exe_function_call actual_params formal_params in let results = IList.map exe_one_spec spec_list in - exe_call_postprocess ret_ids trace_call callee_pname loc results + exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc results (* let check_splitting_precondition sub1 sub2 = diff --git a/infer/tests/build_systems/expected_outputs/ant_report.json b/infer/tests/build_systems/expected_outputs/ant_report.json index 468c291f7..04e6f9131 100644 --- a/infer/tests/build_systems/expected_outputs/ant_report.json +++ b/infer/tests/build_systems/expected_outputs/ant_report.json @@ -244,6 +244,11 @@ "file": "codetoanalyze/java/infer/NullPointerExceptions.java", "procedure": "void NullPointerExceptions.derefNullableGetter()" }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.derefNullableRet(boolean)" + }, { "bug_type": "NULL_DEREFERENCE", "file": "codetoanalyze/java/infer/NullPointerExceptions.java", diff --git a/infer/tests/build_systems/expected_outputs/buck_report.json b/infer/tests/build_systems/expected_outputs/buck_report.json index 95815ac36..210b2d7c4 100644 --- a/infer/tests/build_systems/expected_outputs/buck_report.json +++ b/infer/tests/build_systems/expected_outputs/buck_report.json @@ -244,6 +244,11 @@ "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", "procedure": "void NullPointerExceptions.derefNullableGetter()" }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.derefNullableRet(boolean)" + }, { "bug_type": "NULL_DEREFERENCE", "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index c8adfa4f6..520575b46 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -396,6 +396,39 @@ public class NullPointerExceptions { o.toString(); } + public @Nullable Object nullableRet(boolean b) { + if (b) { + return null; + } + return new Object(); + } + + public void derefNullableRet(boolean b) { + Object ret = nullableRet(b); + ret.toString(); + } + + public void derefNullableRetOK(boolean b) { + Object ret = nullableRet(b); + if (ret != null) { + ret.toString(); + } + } + + public native @Nullable Object undefNullableRet(); + + public void derefUndefNullableRetTODO() { // TODO: should warn here + Object ret = undefNullableRet(); + ret.toString(); + } + + public void derefUndefNullableRetOK() { + Object ret = undefNullableRet(); + if (ret != null) { + ret.toString(); + } + } + public @Nullable String testSystemGetPropertyArgument() { String s = System.getProperty(null); return s; diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index 52ad0f334..8b2cc4f9a 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -62,6 +62,9 @@ public class NullPointerExceptionTest { "npeWithDollars", "someNPEAfterResourceLeak", "derefNullableGetter", + "derefNullableRet", + // TODO: report on this test + // "derefUndefNullableRet "testSystemGetPropertyArgument", "testSystemGetPropertyReturn", "derefNull",