[Infer][iOS][Linters][CTL] Rewrite BAD_POINTER_COMPARISON rule into Computation Tree Logics formula

Reviewed By: ddino

Differential Revision: D3930047

fbshipit-source-id: bb90e92

infer/src/clang/cFrontend_checkers.ml

@@ -22,9 +22,6 @@ open CFrontend_utils
 (*    - If it is a declaration invoke it from run_frontend_checkers_on_decl *)
 
 (* Helper functions *)
-let location_from_sinfo info =
-  CLocation.get_sil_location_from_range info.Clang_ast_t.si_source_range true
-
 let location_from_stmt stmt =
   let info, _ = Clang_ast_proj.get_stmt_tuple stmt in
   CLocation.get_sil_location_from_range info.Clang_ast_t.si_source_range true
@@ -109,6 +106,38 @@ let ctl_ns_notification decl =
   } in
   condition, issue_desc
 
+(* BAD_POINTER_COMPARISON: Fires whenever a NSNumber is dangerously coerced to
+    a boolean in a comparison *)
+let ctl_bad_pointer_comparison_warning stmt =
+  let open CTL in
+  let is_binop = Atomic ("is_stmt", ["BinaryOperator"]) in
+  let is_binop_eq = Atomic ("is_binop_with_kind", ["EQ"]) in
+  let is_binop_ne = Atomic ("is_binop_with_kind", ["NE"]) in
+  let is_binop_neq = Or (is_binop_eq, is_binop_ne) in
+  let is_unop_lnot = Atomic ("is_unop_with_kind", ["LNot"]) in
+  let is_implicit_cast_expr = Atomic ("is_stmt", ["ImplicitCastExpr"]) in
+  let is_expr_with_cleanups = Atomic ("is_stmt", ["ExprWithCleanups"]) in
+  let is_nsnumber = Atomic ("isa", ["NSNumber"]) in
+  (*
+  NOT is_binop_neq AND
+  (is_expr_with_cleanups OR is_implicit_cast_expr OR is_binop OR is_unop_lnot)
+  UNTIL is_nsnumber
+  *)
+  let p = Or (is_expr_with_cleanups, Or (is_implicit_cast_expr, Or (is_binop, is_unop_lnot))) in
+  let p' = And (Not is_binop_neq, p) in
+  let condition = EU (p', is_nsnumber) in
+  let issue_desc =
+    { CIssue.
+      issue = CIssue.Bad_pointer_comparison;
+      description = "Implicitly checking whether NSNumber pointer is nil";
+      suggestion =
+        Some ("Did you mean to compare against the unboxed value instead? " ^
+              "Please either explicitly compare the NSNumber instance to nil, " ^
+              "or use one of the NSNumber accessors before the comparison.");
+      loc = location_from_stmt stmt
+    } in
+  condition, issue_desc
+
 (* name_contains_delegate AND not name_contains_queue AND is_strong_property *)
 let ctl_strong_delegate dec =
   let open CTL in
@@ -247,44 +276,14 @@ let captured_cxx_ref_in_objc_block_warning lcxt stmt  =
     Some issue_desc
   else None
 
-
-(* BAD_POINTER_COMPARISON: Fires whenever a NSNumber is dangerously coerced to
-    a boolean in a comparison *)
-let bad_pointer_comparison_warning _ stmt_info stmts =
-  let rec condition stmts =
-    let condition_aux stmt =
-      match (stmt: Clang_ast_t.stmt) with
-      | BinaryOperator (_, _, _, boi) when
-          (boi.boi_kind = `EQ) || (boi.boi_kind = `NE) -> false
-      | BinaryOperator (_, stmts, _, _) -> condition stmts
-      | UnaryOperator (_, stmts, _, uoi) when uoi.uoi_kind = `LNot ->
-          condition stmts
-      | ImplicitCastExpr (_, stmts, _, _)
-      | ExprWithCleanups (_, stmts, _, _) ->
-          condition stmts
-      | stmt ->
-          match Clang_ast_proj.get_expr_tuple stmt with
-          | Some (_, _, expr_info) ->
-              let typ = CFrontend_utils.Ast_utils.get_desugared_type expr_info.ei_type_ptr in
-              CFrontend_utils.Ast_utils.is_ptr_to_objc_class typ "NSNumber"
-          | _ -> false in
-    IList.exists condition_aux stmts in
-  if condition stmts then
-    Some { CIssue.
-           issue = CIssue.Bad_pointer_comparison;
-           description = "Implicitly checking whether NSNumber pointer is nil";
-           suggestion =
-             Some ("Did you mean to compare against the unboxed value instead? " ^
-                   "Please either explicitly compare the NSNumber instance to nil, " ^
-                   "or use one of the NSNumber accessors before the comparison.");
-           loc = location_from_sinfo stmt_info
-         }
-  else
-    None
-
-
 let checker_NSNotificationCenter lcxt dec =
   let condition, issue_desc = ctl_ns_notification dec in
   if CTL.eval_formula  condition (CTL.Decl dec) lcxt then
     Some issue_desc
   else None
+
+let bad_pointer_comparison_warning lcxt stmt =
+  let condition, issue_desc = ctl_bad_pointer_comparison_warning stmt in
+  if CTL.eval_formula condition (CTL.Stmt stmt) lcxt then
+    Some issue_desc
+  else None

infer/src/clang/cFrontend_checkers.mli

@@ -30,8 +30,7 @@ val captured_cxx_ref_in_objc_block_warning :
   CLintersContext.context -> Clang_ast_t.stmt -> CIssue.issue_desc option
 
 val bad_pointer_comparison_warning :
-  CLintersContext.context ->
-  Clang_ast_t.stmt_info -> Clang_ast_t.stmt list -> CIssue.issue_desc option
+  CLintersContext.context -> Clang_ast_t.stmt -> CIssue.issue_desc option
 
 (* REGISTERED_OBSERVER_BEING_DEALLOCATED: an object is registered in a notification center
    but not removed before deallocation *)

infer/src/clang/cFrontend_errors.ml

@@ -52,29 +52,29 @@ let checker_for_var dec checker context =
 let conditional_op_checker_list = [CFrontend_checkers.bad_pointer_comparison_warning]
 
 (* Invocation of checker belonging to conditional_op_checker_list *)
-let checker_for_conditional_op stmt_info first_stmt checker context =
-  checker context stmt_info first_stmt
+let checker_for_conditional_op first_stmt checker context =
+  checker context first_stmt
 
 (* List of checkers on if-statement *)
 let if_stmt_checker_list = [CFrontend_checkers.bad_pointer_comparison_warning]
 
 (* Invocation of checker belonging to if_stmt_checker_list *)
-let checker_for_if_stmt stmt_info cond checker context =
-  checker context stmt_info cond
+let checker_for_if_stmt cond checker context =
+  checker context cond
 
 (* List of checkers on for statement *)
 let for_stmt_checker_list = [CFrontend_checkers.bad_pointer_comparison_warning]
 
 (* Invocation of checker belonging to for_stmt_checker_list *)
-let checker_for_for_stmt stmt_info cond checker context =
-  checker context stmt_info cond
+let checker_for_for_stmt cond checker context =
+  checker context cond
 
 (* List of checkers on while statement *)
 let while_stmt_checker_list = [CFrontend_checkers.bad_pointer_comparison_warning]
 
 (* Invocation of checker belonging to while_stmt_checker_list *)
-let checker_for_while_stmt stmt_info cond checker context =
-  checker context stmt_info cond
+let checker_for_while_stmt cond checker context =
+  checker context cond
 
 let get_err_log method_decl_opt =
   let procname = match method_decl_opt with
@@ -129,23 +129,23 @@ let run_frontend_checkers_on_stmt context instr =
       invoke_set_of_checkers call_captured_vars_checker context key
         captured_vars_checker_list;
       context
-  | IfStmt (stmt_info, _ :: _ :: cond :: _) ->
-      let call_checker = checker_for_if_stmt stmt_info [cond] in
+  | IfStmt (_, _ :: _ :: cond :: _) ->
+      let call_checker = checker_for_if_stmt cond in
       let key = Ast_utils.generate_key_stmt cond in
       invoke_set_of_checkers call_checker context key if_stmt_checker_list;
       context
-  | ConditionalOperator (stmt_info, first_stmt :: _, _) ->
-      let call_checker = checker_for_conditional_op stmt_info [first_stmt] in
+  | ConditionalOperator (_, first_stmt :: _, _) ->
+      let call_checker = checker_for_conditional_op first_stmt in
       let key = Ast_utils.generate_key_stmt first_stmt in
       invoke_set_of_checkers call_checker context key conditional_op_checker_list;
       context
-  | ForStmt (stmt_info, [_; _; cond; _; _]) ->
-      let call_checker = checker_for_for_stmt stmt_info [cond] in
+  | ForStmt (_, [_; _; cond; _; _]) ->
+      let call_checker = checker_for_for_stmt cond in
       let key = Ast_utils.generate_key_stmt cond in
       invoke_set_of_checkers call_checker context key for_stmt_checker_list;
       context
-  | WhileStmt (stmt_info, [_; cond; _]) ->
-      let call_checker = checker_for_while_stmt stmt_info [cond] in
+  | WhileStmt (_, [_; cond; _]) ->
+      let call_checker = checker_for_while_stmt cond in
       let key = Ast_utils.generate_key_stmt cond in
       invoke_set_of_checkers call_checker context key while_stmt_checker_list;
       context

infer/src/clang/cTL.ml

@@ -116,6 +116,10 @@ let eval_Atomic pred_name params an lcxt =
   | "is_objc_constructor", [], _ -> Predicates.is_objc_constructor lcxt
   | "is_objc_dealloc", [], _ -> Predicates.is_objc_dealloc lcxt
   | "captures_cxx_references", [], Stmt st -> Predicates.captures_cxx_references st
+  | "is_binop_with_kind", [kind], Stmt st -> Predicates.is_binop_with_kind st kind
+  | "is_unop_with_kind", [kind], Stmt st -> Predicates.is_unop_with_kind st kind
+  | "is_stmt", [stmt_name], Stmt st -> Predicates.is_stmt st stmt_name
+  | "isa", [classname], Stmt st -> Predicates.isa st classname
   | _ -> failwith ("ERROR: Undefined Predicate: "^pred_name)
 
 (* st, lcxt |= EF phi  <=>

infer/src/clang/predicates.ml

@@ -173,3 +173,30 @@ let is_objc_dealloc context =
 
 let captures_cxx_references stmt =
   IList.length (captured_variables_cxx_ref stmt) > 0
+
+let is_binop_with_kind stmt str_kind =
+  let kind = match str_kind with
+    | "EQ" -> `EQ
+    | "NE" -> `NE
+    | _ -> failwith ("Kind " ^ str_kind ^ " is invalid or not yet supported") in
+  match stmt with
+  | Clang_ast_t.BinaryOperator (_, _, _, boi) when boi.boi_kind = kind -> true
+  | _ -> false
+
+let is_unop_with_kind stmt str_kind =
+  let kind = match str_kind with
+    | "LNot" -> `LNot
+    | _ -> failwith ("Kind " ^ str_kind ^ " is invalid or not yet supported") in
+  match stmt with
+  | Clang_ast_t.UnaryOperator (_, _, _, uoi) when uoi.uoi_kind = kind -> true
+  | _ -> false
+
+let is_stmt stmt stmt_name =
+  stmt_name = Clang_ast_proj.get_stmt_kind_string stmt
+
+let isa stmt classname =
+  match Clang_ast_proj.get_expr_tuple stmt with
+  | Some (_, _, expr_info) ->
+      let typ = CFrontend_utils.Ast_utils.get_desugared_type expr_info.ei_type_ptr in
+      CFrontend_utils.Ast_utils.is_ptr_to_objc_class typ classname
+  | _ -> false

infer/src/clang/predicates.mli

@@ -44,3 +44,11 @@ val is_objc_constructor : CLintersContext.context -> bool
 val is_objc_dealloc : CLintersContext.context -> bool
 
 val captures_cxx_references : Clang_ast_t.stmt -> bool
+
+val is_binop_with_kind : Clang_ast_t.stmt -> string -> bool
+
+val is_unop_with_kind : Clang_ast_t.stmt -> string -> bool
+
+val is_stmt : Clang_ast_t.stmt -> string -> bool
+
+val isa : Clang_ast_t.stmt -> string -> bool