[Infer][ios] Reporting error when NSNumber * is coerced to boolean in a comparison

infer/bin/inferlib.py

@@ -282,7 +282,8 @@ def should_report(analyzer, row):
         'MEMORY_LEAK',
         'RETAIN_CYCLE',
         'ASSERTION_FAILURE',
-        'ACTIVITY_LEAK'
+        'ACTIVITY_LEAK',
+        'BAD_POINTER_COMPARISON'
     ]
 
     if analyzer in [ERADICATE, CHECKERS, TRACING]:

infer/src/backend/errdesc.ml

@@ -415,6 +415,11 @@ let explain_allocation_mismatch ra_alloc ra_dealloc =
     (primitive, called, ra.Sil.ra_loc) in
   Localise.desc_allocation_mismatch (get_primitive_called true ra_alloc) (get_primitive_called false ra_dealloc)
 
+(** Produce a description of a pointer dangerously coerced to a boolean in a comparison *)
+let explain_bad_pointer_comparison exp node loc =
+  let dexp_opt = exp_rv_dexp node exp in
+  Localise.desc_bad_pointer_comparison dexp_opt loc
+
 (** check whether the type of leaked [hpred] appears as a predicate in an inductive predicate in [prop] *)
 let leak_from_list_abstraction hpred prop =
   let hpred_type = function

infer/src/backend/errdesc.mli

@@ -43,6 +43,9 @@ val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> Sil.dexp option
 (** Produce a description of a persistent reference to an Android Activity *)
 val explain_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname -> Localise.error_desc
 
+(** Produce a description of a pointer dangerously coerced to a boolean in a comparison *)
+val explain_bad_pointer_comparison : Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc
+
 (** Produce a description of a mismatch between an allocation function and a deallocation function *)
 val explain_allocation_mismatch : Sil.res_action -> Sil.res_action -> Localise.error_desc
 

infer/src/backend/exceptions.ml

@@ -38,6 +38,7 @@ exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location
 exception Array_of_pointsto of ml_location
 exception Assertion_failure of string * Localise.error_desc
 exception Bad_footprint of ml_location
+exception Bad_pointer_comparison of Localise.error_desc * ml_location
 exception Class_cast_exception of Localise.error_desc * ml_location
 exception Codequery of Localise.error_desc
 exception Comparing_floats_for_equality of Localise.error_desc * ml_location
@@ -105,6 +106,8 @@ let recognize_exception exn =
         (Localise.from_string "Assert_failure", Localise.no_desc, Some mloc, Exn_developer, High, None, Nocat)
     | Assertion_failure (error_msg, desc) ->
         (Localise.from_string error_msg, desc, None, Exn_user, High, None, Checker)
+    | Bad_pointer_comparison (desc, mloc) ->
+        (Localise.bad_pointer_comparison, desc, Some mloc, Exn_user, High, Some Kerror, Prover)
     | Bad_footprint mloc ->
         (Localise.from_string "Bad_footprint", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
     | Prop.Cannot_star mloc ->

infer/src/backend/exceptions.mli

@@ -38,6 +38,7 @@ exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location
 exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location
 exception Assertion_failure of string * Localise.error_desc
 exception Bad_footprint of ml_location
+exception Bad_pointer_comparison of Localise.error_desc * ml_location
 exception Class_cast_exception of Localise.error_desc * ml_location
 exception Codequery of Localise.error_desc
 exception Comparing_floats_for_equality of Localise.error_desc * ml_location

infer/src/backend/localise.ml

@@ -33,6 +33,7 @@ let analysis_stops = "ANALYSIS_STOPS"
 let array_out_of_bounds_l1 = "ARRAY_OUT_OF_BOUNDS_L1"
 let array_out_of_bounds_l2 = "ARRAY_OUT_OF_BOUNDS_L2"
 let array_out_of_bounds_l3 = "ARRAY_OUT_OF_BOUNDS_L3"
+let bad_pointer_comparison = "BAD_POINTER_COMPARISON"
 let class_cast_exception = "CLASS_CAST_EXCEPTION"
 let comparing_floats_for_equality = "COMPARING_FLOAT_FOR_EQUALITY"
 let condition_is_assignment = "CONDITION_IS_ASSIGNMENT"
@@ -377,6 +378,18 @@ let desc_activity_leak pname activity_typ fieldname : error_desc =
 let desc_assertion_failure loc : error_desc =
   (["could be raised"; at_line (Tags.create ()) loc], None, [])
 
+let desc_bad_pointer_comparison dexp_opt loc : error_desc =
+  let dexp_str = match dexp_opt with
+    | Some dexp -> (Sil.dexp_to_string dexp) ^ " "
+    | None -> "" in
+  let line_info = at_line (Tags.create ()) loc in
+  let check_msg =
+    "Implicitly checking whether NSNumber pointer " ^ dexp_str ^ "is nil " ^ line_info ^ "." in
+  let concern_msg = "Did you mean to compare against the unboxed value instead?" in
+  let fix_msg_rec1 = "Please either explicitly compare " ^ dexp_str ^ "to nil" in
+  let fix_msg_rec2 = "or use one of the NSNumber accessors before the comparison." in
+  ([check_msg; concern_msg; fix_msg_rec1; fix_msg_rec2], None, [])
+
 (** type of access *)
 type access =
   | Last_assigned of int * bool (* line, null_case_flag *)

infer/src/backend/localise.mli

@@ -30,6 +30,7 @@ val analysis_stops : t
 val array_out_of_bounds_l1 : t
 val array_out_of_bounds_l2 : t
 val array_out_of_bounds_l3 : t
+val bad_pointer_comparison : t
 val class_cast_exception : t
 val condition_is_assignment : t
 val condition_always_false : t
@@ -199,6 +200,8 @@ val desc_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname -> error_desc
 (* Create human-readable error description for assertion failures *)
 val desc_assertion_failure : Location.t -> error_desc
 
+val desc_bad_pointer_comparison : Sil.dexp option -> Location.t -> error_desc
+
 (** kind of precondition not met *)
 type pnm_kind =
   | Pnm_bounds

infer/src/backend/sil.ml

@@ -936,6 +936,10 @@ let fld_compare (fld1 : Ident.fieldname) fld2 = Ident.fieldname_compare fld1 fld
 
 let fld_equal fld1 fld2 = fld_compare fld1 fld2 = 0
 
+let exp_is_zero = function
+  | Const (Cint n) -> Int.iszero n
+  | _ -> false
+
 let exp_is_null_literal = function
   | Const (Cint n) -> Int.isnull n
   | _ -> false

infer/src/backend/sil.mli

@@ -561,6 +561,8 @@ val is_objc_ref_counter_field : (Ident.fieldname * typ * item_annotation) -> boo
 
 val has_objc_ref_counter : hpred -> bool
 
+val exp_is_zero : exp -> bool
+
 val exp_is_null_literal : exp -> bool
 
 (** return true if [exp] is the special this/self expression *)

infer/src/backend/symExec.ml

@@ -901,6 +901,11 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
             | Sil.Ik_land_lor -> true (* skip subpart of a condition obtained from compilation of && and || *)
             | _ -> false in
           true_branch && not skip_loop in
+        (* in comparisons, nil is translated as (void * ) 0 rather than 0 *)
+        let is_comparison_to_nil = function
+          | Sil.Cast ((Sil.Tptr (Sil.Tvoid, _)), exp) ->
+              !Config.curr_language = Config.C_CPP && Sil.exp_is_zero exp
+          | _ -> false in
         match Prop.exp_normalize_prop Prop.prop_emp cond with
         | Sil.Const (Sil.Cint i) when report_condition_always_true_false i ->
             let node = State.get_node () in
@@ -908,6 +913,26 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
             let exn = Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), try assert false with Assert_failure x -> x) in
             let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
             Reporting.log_warning pname ~pre: pre_opt exn
+        | Sil.BinOp ((Sil.Eq | Sil.Ne), lhs, rhs)
+          when true_branch && !Config.footprint && not (is_comparison_to_nil rhs) ->
+            (* iOS: check that NSNumber *'s are not used in conditionals without comparing to nil *)
+            let lhs_normal = Prop.exp_normalize_prop _prop lhs in
+            let is_nsnumber = function
+              | Sil.Tvar (Sil.TN_csu (Sil.Class, name)) -> Mangled.to_string name = "NSNumber"
+              | _ -> false in
+            let lhs_is_ns_ptr () =
+              list_exists
+                (function
+                  | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _)) ->
+                      Sil.exp_equal exp lhs_normal && is_nsnumber typ
+                  | _ -> false)
+                (Prop.get_sigma _prop) in
+            if not (Sil.exp_is_zero lhs_normal) && lhs_is_ns_ptr () then
+              let node = State.get_node () in
+              let desc = Errdesc.explain_bad_pointer_comparison lhs node loc in
+              let fail = try assert false with Assert_failure x -> x in
+              let exn = Exceptions.Bad_pointer_comparison (desc, fail) in
+              Reporting.log_warning pname exn
         | _ -> () in
       check_already_dereferenced pname cond _prop;
       check_condition_always_true_false ();

infer/tests/codetoanalyze/objc/errors/bad_ptr_comparisons/nsnumber.m

@@ -0,0 +1,52 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+#import <Foundation/Foundation.h>
+
+void bad1(NSNumber * isNum) {
+  if (isNum) {
+  }
+}
+
+void bad2(NSNumber * isNum) {
+  if (!isNum) {
+  }
+}
+
+
+void ok1(NSNumber * isNum) {
+  if (isNum != nil) {
+  }
+}
+
+void ok2(NSNumber * isNum) {
+  if (nil != isNum) {
+  }
+}
+
+void ok3(NSNumber * isNum) {
+  if (nil == isNum) {
+  }
+}
+
+
+void ok4(NSNumber * isNum) {
+  if (isNum == nil) {
+  }
+}
+
+void accessor_ok1(NSNumber * num) {
+  if (![num boolValue]) {
+  }
+}
+
+void accessor_ok2(NSNumber * num) {
+  if ([num boolValue]) {
+  }
+}

infer/tests/endtoend/objc/NSNumberTest.java

@@ -0,0 +1,66 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+package endtoend.objc;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class NSNumberTest {
+
+  public static final String NSNUMBER_FILE =
+      "infer/tests/codetoanalyze/objc/errors/bad_ptr_comparisons/nsnumber.m";
+
+  private static ImmutableList<String> inferCmd;
+
+  public static final String BAD_POINTER_COMPARISON = "BAD_POINTER_COMPARISON";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createObjCInferCommand(
+        folder,
+        NSNUMBER_FILE);
+  }
+
+  @Test
+  public void badNSNumberPointerComparisonShouldBeFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferObjC(inferCmd);
+    String[] methods = {
+      "bad1",
+      "bad2"
+    };
+    assertThat(
+        "Results should contain " + BAD_POINTER_COMPARISON,
+        inferResults,
+        containsExactly(
+            BAD_POINTER_COMPARISON,
+            NSNUMBER_FILE,
+            methods
+        )
+    );
+  }
+
+}