warning on deref of nullable retvals

Reviewed By: jberdine

Differential Revision: D3199166

fb-gh-sync-id: 8b57e37
fbshipit-source-id: 8b57e37

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"
 

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 *)

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

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
 

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, _)) ->

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 =

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

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

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;

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