warn on deref of nullable skip function

Reviewed By: jeremydubreil

Differential Revision: D3204133

fb-gh-sync-id: 2a108f6
fbshipit-source-id: 2a108f6

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) ^ "]"

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

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; }

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

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

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 ->
+                 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
+                   | _ -> 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

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,6 +818,10 @@ 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 =
+      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
@@ -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 prop_with_undef_attr =
       let path_pos = State.get_path_pos () in
-    [(Prop.mark_vars_as_undefined pre_final exps_to_mark callee_pname loc path_pos, path)]
+      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)

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
 

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

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",

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",

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;

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",