diff --git a/infer/src/IR/sil.ml b/infer/src/IR/sil.ml index 16dc82d4f..eaa2cb397 100644 --- a/infer/src/IR/sil.ml +++ b/infer/src/IR/sil.ml @@ -617,8 +617,8 @@ and attribute = | Aresource of res_action (** resource acquire/release *) | Aautorelease | Adangling of dangling_kind (** dangling pointer *) - (** undefined value obtained by calling the given procedure *) - | Aundef of Procname.t * Location.t * path_pos + (** undefined value obtained by calling the given procedure, plus its return value annots *) + | Aundef of Procname.t * item_annotation * Location.t * path_pos | Ataint of taint_info | Auntaint | Alocked @@ -1360,7 +1360,7 @@ and attribute_compare (att1 : attribute) (att2 : attribute) : int = | Adangling dk1, Adangling dk2 -> dangling_kind_compare dk1 dk2 | Adangling _, _ -> - 1 | _, Adangling _ -> 1 - | Aundef (pn1, _, _), Aundef (pn2, _, _) -> Procname.compare pn1 pn2 + | Aundef (pn1, _, _, _), Aundef (pn2, _, _, _) -> Procname.compare pn1 pn2 | Ataint ti1, Ataint ti2 -> taint_info_compare ti1 ti2 | Ataint _, _ -> -1 | _, Ataint _ -> 1 @@ -1889,7 +1889,7 @@ and attribute_to_string pe = function | DAaddr_stack_var -> "ADDR_STACK" | DAminusone -> "MINUS1" in "DANGL" ^ (str_binop pe Lt) ^ dks ^ (str_binop pe Gt) - | Aundef (pn, loc, _) -> + | Aundef (pn, _, loc, _) -> "UND" ^ (str_binop pe Lt) ^ Procname.to_string pn ^ (str_binop pe Gt) ^ ":" ^ (string_of_int loc.Location.line) | Ataint { taint_source; } -> "TAINTED[" ^ (Procname.to_string taint_source) ^ "]" diff --git a/infer/src/IR/sil.mli b/infer/src/IR/sil.mli index 94aabad3c..d1b0a8ec9 100644 --- a/infer/src/IR/sil.mli +++ b/infer/src/IR/sil.mli @@ -255,7 +255,7 @@ and attribute = | Aautorelease | Adangling of dangling_kind (** dangling pointer *) (** undefined value obtained by calling the given procedure *) - | Aundef of Procname.t * Location.t * path_pos + | Aundef of Procname.t * item_annotation * Location.t * path_pos | Ataint of taint_info | Auntaint | Alocked diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index cceaa541a..1f164cdc0 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -861,7 +861,11 @@ let execute_scan_function skip_n_arguments ({ Builtin.args } as call_args) | _ when IList.length args >= skip_n_arguments -> let varargs = ref args in for _ = 1 to skip_n_arguments do varargs := IList.tl !varargs done; - SymExec.unknown_or_scan_call ~is_scan:true None { call_args with args = !varargs } + SymExec.unknown_or_scan_call + ~is_scan:true + None + Sil.item_annotation_empty + { call_args with args = !varargs } | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute__unwrap_exception { Builtin.pdesc; prop_; path; ret_ids; args; } diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 0a8f74718..74c7d1b8a 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1888,8 +1888,8 @@ let add_or_replace_exp_attribute prop exp att = add_or_replace_exp_attribute_check_changed check_attr_changed prop exp att (** mark Sil.Var's or Sil.Lvar's as undefined *) -let mark_vars_as_undefined prop vars_to_mark callee_pname loc path_pos = - let att_undef = Sil.Aundef (callee_pname, loc, path_pos) in +let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos = + let att_undef = Sil.Aundef (callee_pname, ret_annots, loc, path_pos) in let mark_var_as_undefined exp prop = match exp with | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute prop exp att_undef diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index c37ffb077..e910f8872 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -319,8 +319,8 @@ val add_or_replace_exp_attribute_check_changed : (Sil.attribute -> Sil.attribute val add_or_replace_exp_attribute : normal t -> exp -> attribute -> normal t (** mark Sil.Var's or Sil.Lvar's as undefined *) -val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Location.t -> - Sil.path_pos -> normal t +val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Sil.item_annotation -> + Location.t -> Sil.path_pos -> normal t (** Remove an attribute from all the atoms in the heap *) val remove_attribute : Sil.attribute -> 'a t -> normal t diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index a2fb7e836..8c4e9dadd 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -945,7 +945,6 @@ 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 = if Annotations.param_is_nullable pvar ann_sig then @@ -954,12 +953,13 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = 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 + let is_nullable_attr = function + | Sil.Aretval (pname, ret_attr) + | Sil.Aundef (pname, ret_attr, _, _) when Annotations.ia_is_nullable ret_attr -> + nullable_obj_str := Some (Procname.to_string pname); + true + | _ -> false in + IList.exists is_nullable_attr (Prop.get_exp_attributes prop exp) 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, _)) -> @@ -1025,7 +1025,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = let deref_str = Localise.deref_str_dangling (Some dk) in let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__)) - | Some (Sil.Aundef (s, undef_loc, _)) -> + | Some (Sil.Aundef (s, _, undef_loc, _)) -> if !Config.angelic_execution then () else let deref_str = Localise.deref_str_undef (s, undef_loc) in diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index b8f6bf212..d896f59cb 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -797,7 +797,7 @@ let add_struct_value_to_footprint tenv abducted_pv typ prop = let prop' = add_strexp_to_footprint struct_strexp abducted_pv typ prop in prop', struct_strexp -let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = +let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_pname callee_loc= if Procname.is_infer_undefined callee_pname then prop else let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *) @@ -818,9 +818,13 @@ let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = IList.fold_left bind_exp prop (Prop.get_sigma prop) in (* To avoid obvious false positives, assume skip functions do not return null pointers *) let add_ret_non_null exp typ prop = - match typ with - | Sil.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop - | _ -> prop in + if has_nullable_annot + then + prop (* don't assume nonnull if the procedure is annotated with @Nullable *) + else + match typ with + | Sil.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop + | _ -> prop in let add_tainted_post ret_exp callee_pname prop = Prop.add_or_replace_exp_attribute prop ret_exp (Sil.Ataint callee_pname) in @@ -916,8 +920,10 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ if !Config.angelic_execution then (* when we try to deref an undefined value, add it to the footprint *) match exp_get_undef_attr n_rhs_exp' with - | Some (Sil.Aundef (callee_pname, callee_loc, _)) -> - add_constraints_on_retval pdesc prop n_rhs_exp' typ callee_pname callee_loc + | Some (Sil.Aundef (callee_pname, ret_annots, callee_loc, _)) -> + let has_nullable_annot = Annotations.ia_is_nullable ret_annots in + add_constraints_on_retval + pdesc prop n_rhs_exp' ~has_nullable_annot typ callee_pname callee_loc | _ -> prop else prop in let iter_list = @@ -929,6 +935,14 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ let undef = Sil.exp_get_undefined false in [Prop.conjoin_eq (Sil.Var id) undef prop_] +let load_ret_annots pname = + match AttributesTable.load_attributes pname with + | Some attrs -> + let ret_annots, _ = attrs.ProcAttributes.method_annotation in + ret_annots + | None -> + Sil.item_annotation_empty + let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ = let execute_set_ pdesc tenv rhs_exp acc_in iter = let (lexp, strexp, typ, st, offlist) = @@ -980,7 +994,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path Sil.Call (ret, exp', par, loc, call_flags) in instr' | _ -> _instr in - let skip_call prop path callee_pname loc ret_ids ret_typ_opt actual_args = + let skip_call prop path callee_pname ret_annots loc ret_ids ret_typ_opt actual_args = let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in Reporting.log_info current_pname exn; L.d_strln @@ -992,7 +1006,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path Specs.CallStats.trace summary.Specs.stats.Specs.call_stats callee_pname loc (Specs.CallStats.CR_skip) !Config.footprint); - unknown_or_scan_call ~is_scan:false ret_typ_opt Builtin.{ + unknown_or_scan_call ~is_scan:false ret_typ_opt ret_annots Builtin.{ pdesc= current_pdesc; instr; tenv; prop_= prop; path; ret_ids; args= actual_args; proc_name= callee_pname; loc; } in let call_args prop_ proc_name args ret_ids loc = { @@ -1065,8 +1079,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path actual_params, loc, call_flags) when Config.lazy_dynamic_dispatch -> let norm_prop, norm_args = normalize_params current_pname prop_ actual_params in - let exec_skip_call skipped_pname ret_type = - skip_call norm_prop path skipped_pname loc ret_ids (Some ret_type) norm_args in + let exec_skip_call skipped_pname ret_annots ret_type = + skip_call norm_prop path skipped_pname ret_annots loc ret_ids (Some ret_type) norm_args in let resolved_pname, summary_opt = resolve_and_analyze tenv current_pdesc norm_prop norm_args callee_pname call_flags in begin @@ -1077,9 +1091,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path | Some (Sil.Tstruct _ as typ) -> Sil.Tptr (typ, Pk_pointer) | Some typ -> typ | None -> Sil.Tvoid in - exec_skip_call resolved_pname ret_typ + let ret_annots = load_ret_annots callee_pname in + exec_skip_call resolved_pname ret_annots ret_typ | Some summary when call_should_be_skipped resolved_pname summary -> - exec_skip_call resolved_pname summary.Specs.attributes.ProcAttributes.ret_type + let proc_attrs = summary.Specs.attributes in + let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in + exec_skip_call resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type | Some summary -> proc_call summary (call_args prop_ callee_pname norm_args ret_ids loc) end @@ -1095,8 +1112,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in let exec_one_pname pname = Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc pname; - let exec_skip_call ret_type = - skip_call norm_prop path pname loc ret_ids (Some ret_type) url_handled_args in + let exec_skip_call ret_annots ret_type = + skip_call norm_prop path pname ret_annots loc ret_ids (Some ret_type) url_handled_args in match Specs.get_summary pname with | None -> let ret_typ = @@ -1104,9 +1121,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path | Some (Sil.Tstruct _ as typ) -> Sil.Tptr (typ, Pk_pointer) | Some typ -> typ | None -> Sil.Tvoid in - exec_skip_call ret_typ + let ret_annots = load_ret_annots callee_pname in + exec_skip_call ret_annots ret_typ | Some summary when call_should_be_skipped pname summary -> - exec_skip_call summary.Specs.attributes.ProcAttributes.ret_type + let proc_attrs = summary.Specs.attributes in + let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in + exec_skip_call ret_annots proc_attrs.ProcAttributes.ret_type | Some summary -> proc_call summary (call_args norm_prop pname url_handled_args ret_ids loc) in IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames @@ -1149,7 +1169,13 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path current_pdesc callee_pname loc path (sym_exec_objc_accessor objc_property_accessor ret_typ_opt) | None -> - skip_call prop path resolved_pname loc ret_ids ret_typ_opt n_actual_params + let ret_annots = match summary with + | Some summ -> + let ret_annots, _ = summ.Specs.attributes.ProcAttributes.method_annotation in + ret_annots + | None -> + load_ret_annots resolved_pname in + skip_call prop path resolved_pname ret_annots loc ret_ids ret_typ_opt n_actual_params else proc_call (Option.get summary) (call_args prop resolved_pname n_actual_params ret_ids loc) in @@ -1167,7 +1193,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path L.d_str "Unknown function pointer "; Sil.d_exp fun_exp; L.d_strln ", returning undefined value."; let callee_pname = Procname.from_string_c_fun "__function_pointer__" in - unknown_or_scan_call ~is_scan:false None Builtin.{ + unknown_or_scan_call ~is_scan:false None Sil.item_annotation_empty Builtin.{ pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_ids; args= n_actual_params; proc_name= callee_pname; loc; } end @@ -1342,7 +1368,7 @@ and check_untainted exp caller_pname callee_pname prop = else prop (** execute a call for an unknown or scan function *) -and unknown_or_scan_call ~is_scan ret_type_option +and unknown_or_scan_call ~is_scan ret_type_option ret_annots { Builtin.tenv; pdesc; prop_= pre; path; ret_ids; args= actual_pars; proc_name= callee_pname; loc; } = let remove_file_attribute prop = @@ -1377,13 +1403,16 @@ and unknown_or_scan_call ~is_scan ret_type_option | Sil.Lvar _, Sil.Tptr _ -> true | _ -> false) actual_pars in + let has_nullable_annot = Annotations.ia_is_nullable ret_annots in let pre_final = (* in Java, assume that skip functions close resources passed as params *) let pre_1 = if !Config.curr_language = Config.Java then remove_file_attribute pre else pre in let pre_2 = match ret_ids, ret_type_option with | [ret_id], Some ret_typ -> - add_constraints_on_retval pdesc pre_1 (Sil.Var ret_id) ret_typ callee_pname loc - | _ -> pre_1 in + add_constraints_on_retval + pdesc pre_1 (Sil.Var ret_id) ret_typ ~has_nullable_annot callee_pname loc + | _ -> + pre_1 in let pre_3 = add_constraints_on_actuals_by_ref tenv pre_2 actuals_by_ref callee_pname loc in let caller_pname = Cfg.Procdesc.get_proc_name pdesc in add_tainted_pre pre_3 actual_pars caller_pname callee_pname in @@ -1395,8 +1424,10 @@ and unknown_or_scan_call ~is_scan ret_type_option let ret_exps = IList.map (fun ret_id -> Sil.Var ret_id) ret_ids in IList.fold_left (fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in - let path_pos = State.get_path_pos () in - [(Prop.mark_vars_as_undefined pre_final exps_to_mark callee_pname loc path_pos, path)] + let prop_with_undef_attr = + let path_pos = State.get_path_pos () in + Prop.mark_vars_as_undefined pre_final exps_to_mark callee_pname ret_annots loc path_pos in + [(prop_with_undef_attr, path)] and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_pos) diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index 7d647b14d..330808124 100644 --- a/infer/src/backend/symExec.mli +++ b/infer/src/backend/symExec.mli @@ -26,7 +26,7 @@ val diverge : Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths. val proc_call : Specs.summary -> Builtin.t -val unknown_or_scan_call : is_scan:bool -> Sil.typ option -> Builtin.t +val unknown_or_scan_call : is_scan:bool -> Sil.typ option -> Sil.item_annotation -> Builtin.t val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 6bdd5d817..c820242bc 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -322,7 +322,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = Some (Deref_freed ra, desc true (Localise.deref_str_freed ra)) | _ -> (match Prop.get_undef_attribute actual_pre e_sub with - | Some (Sil.Aundef (s, loc, pos)) -> + | Some (Sil.Aundef (s, _, loc, pos)) -> Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) | _ -> None) in let check_hpred = function diff --git a/infer/tests/build_systems/expected_outputs/ant_report.json b/infer/tests/build_systems/expected_outputs/ant_report.json index 5417b226b..760ea8e9e 100644 --- a/infer/tests/build_systems/expected_outputs/ant_report.json +++ b/infer/tests/build_systems/expected_outputs/ant_report.json @@ -264,6 +264,16 @@ "file": "codetoanalyze/java/infer/NullPointerExceptions.java", "procedure": "void NullPointerExceptions.derefNullableRet(boolean)" }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.derefUndefNullableRet()" + }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.derefUndefNullableRetWrapper()" + }, { "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 ce87f21f6..b32274ccb 100644 --- a/infer/tests/build_systems/expected_outputs/buck_report.json +++ b/infer/tests/build_systems/expected_outputs/buck_report.json @@ -264,6 +264,16 @@ "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", + "procedure": "void NullPointerExceptions.derefUndefNullableRet()" + }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.derefUndefNullableRetWrapper()" + }, { "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 a66173dd4..b8c97e7ad 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -418,7 +418,7 @@ public class NullPointerExceptions { public native @Nullable Object undefNullableRet(); - public void derefUndefNullableRetTODO() { // TODO: should warn here + public void derefUndefNullableRet() { Object ret = undefNullableRet(); ret.toString(); } @@ -430,6 +430,29 @@ public class NullPointerExceptions { } } + public Object undefNullableWrapper() { + return undefNullableRet(); + } + + public void derefUndefNullableRetWrapper() { + undefNullableWrapper().toString(); + } + + private int returnsThreeOnlyIfRetNotNull(Object obj) { + if (obj == null) { + return 2; + } + return 3; + } + + + public void testNullablePrecision() { + Object ret = undefNullableRet(); + if (returnsThreeOnlyIfRetNotNull(ret) == 3) { + ret.toString(); // shouldn't warn here + } + } + 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 ac3e6834d..6b62ba9f3 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -63,8 +63,8 @@ public class NullPointerExceptionTest { "someNPEAfterResourceLeak", "derefNullableGetter", "derefNullableRet", - // TODO: report on this test - // "derefUndefNullableRet + "derefUndefNullableRet", + "derefUndefNullableRetWrapper", "testSystemGetPropertyArgument", "testSystemGetPropertyReturn", "derefNull",