Finding stateless CKComponents

Reviewed By: jberdine

Differential Revision: D10161169

fbshipit-source-id: dd82e48ee

infer/src/clang/cFrontend_errors.ml

@@ -295,6 +295,8 @@ let rec apply_substitution f sub =
       EG (trans, apply_substitution f1 sub)
   | ET (ntl, sw, f1) ->
       ET (sub_list_param ntl, sw, apply_substitution f1 sub)
+  | InObjCClass (f1, f2) ->
+      InObjCClass (apply_substitution f1 sub, apply_substitution f2 sub)
 
 
 let expand_formula phi map_ error_msg_ =
@@ -356,6 +358,8 @@ let expand_formula phi map_ error_msg_ =
         EG (trans, expand f1 map error_msg)
     | ET (tl, sw, f1) ->
         ET (tl, sw, expand f1 map error_msg)
+    | InObjCClass (f1, f2) ->
+        InObjCClass (expand f1 map error_msg, expand f2 map error_msg)
   in
   expand phi map_ error_msg_
 

infer/src/clang/cTL.ml

@@ -64,21 +64,14 @@ type t =
   | EU of transitions option * t * t
   | EH of ALVar.alexp list * t
   | ET of ALVar.alexp list * transitions option * t
+  | InObjCClass of t * t
 [@@deriving compare]
 
 let equal = [%compare.equal: t]
 
 let has_transition phi =
   match phi with
-  | True
-  | False
-  | Atomic _
-  | Not _
-  | And (_, _)
-  | Or (_, _)
-  | Implies (_, _)
-  | InNode (_, _)
-  | EH (_, _) ->
+  | True | False | Atomic _ | Not _ | And _ | Or _ | Implies _ | InNode _ | EH _ | InObjCClass _ ->
       false
   | AX (trans_opt, _)
   | AF (trans_opt, _)
@@ -212,6 +205,8 @@ module Debug = struct
         Format.fprintf fmt "ET[%a][%a](%a)"
           (Pp.comma_seq Format.pp_print_string)
           (nodes_to_string arglist) pp_transition trans pp_formula phi
+    | InObjCClass (phi1, phi2) ->
+        if full_print then Format.fprintf fmt "InObjCClass(%a, %a)" pp_formula phi1 pp_formula phi2
 
 
   let pp_ast ~ast_node_to_highlight ?(prettifier = Fn.id) fmt root =
@@ -1305,6 +1300,20 @@ and eval_ET tl trs phi an lcxt =
   eval_formula f an lcxt
 
 
+and eval_InObjCClass an lcxt f1 f2 =
+  match an with
+  | Ctl_parser_types.Decl (Clang_ast_t.ObjCInterfaceDecl (_, _, _, _, otdi)) ->
+      let open Option.Monad_infix in
+      eval_formula f1 an lcxt
+      >>= fun _ ->
+      otdi.otdi_implementation
+      >>= fun dr ->
+      CAst_utils.get_decl dr.Clang_ast_t.dr_decl_pointer
+      >>= fun n -> eval_formula f2 (Ctl_parser_types.Decl n) lcxt
+  | _ ->
+      None
+
+
 (* Formulas are evaluated on a AST node an and a linter context lcxt *)
 and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
   debug_eval_begin (debug_create_payload an f lcxt) ;
@@ -1352,5 +1361,7 @@ and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
         eval_formula (And (f1, EX (trans, EG (trans, f1)))) an lcxt
     | ET (tl, sw, phi) ->
         eval_ET tl sw phi an lcxt
+    | InObjCClass (f1, f2) ->
+        eval_InObjCClass an lcxt f1 f2
   in
   debug_eval_end res ; res

infer/src/clang/cTL.mli

@@ -65,6 +65,7 @@ type t =
   | ET of ALVar.alexp list * transitions option * t
       (** ET[T][l] phi <=> there exists a descentant an of the current node such that an is of type in set T
           making a transition to a node an' via label l, such that in an phi holds. *)
+  | InObjCClass of t * t
 [@@deriving compare]
 
 (* "set" clauses are used for defining mandatory variables that will be used

infer/src/clang/ctl_lexer.mll

@@ -41,6 +41,9 @@ rule token = parse
   | "HOLDS-EVERYWHERE-ALWAYS" { AG }
   | "HOLDS-IN-SOME-SUPERCLASS-OF" { EH }
   | "IN-NODE" { ET }
+  | "HOLDS-IN-OBJC-CLASS" { HOLDS_IN_OBJCCLASS }
+  | "INTERFACE" { INTERFACE }
+  | "IMPLEMENTATION" { IMPLEMENTATION }
   | "WHEN" { WHEN }
   | "HOLDS-IN-NODE" { HOLDS_IN_NODE }
   | "WITH-TRANSITION" {WITH_TRANSITION}
@@ -61,6 +64,8 @@ rule token = parse
   | "=" { ASSIGNMENT }
   | ";" { SEMICOLON }
   | "," { COMMA }
+  | "[" { LEFT_SQBRACE }
+  | "]" { RIGHT_SQBRACE }
   | "AND" { AND }
   | "OR" { OR }
   | "NOT" { NOT }

infer/src/clang/ctl_parser.mly

@@ -50,6 +50,9 @@
 %token WITH_TRANSITION
 %token WHEN
 %token HOLDS_IN_NODE
+%token HOLDS_IN_OBJCCLASS
+%token INTERFACE
+%token IMPLEMENTATION
 %token SET
 %token LET
 %token TRUE
@@ -61,6 +64,8 @@
 %token ASSIGNMENT
 %token SEMICOLON
 %token COMMA
+%token LEFT_SQBRACE
+%token RIGHT_SQBRACE
 %token AND
 %token OR
 %token NOT
@@ -255,6 +260,16 @@ formula_with_paren:
  | LEFT_PAREN formula RIGHT_PAREN { $2 }
 ;
 
+when_formula:
+| INTERFACE  LEFT_SQBRACE formula RIGHT_SQBRACE
+  IMPLEMENTATION LEFT_SQBRACE formula RIGHT_SQBRACE HOLDS_IN_OBJCCLASS
+   { L.(debug Linters Verbose) "\tParsed HOLDS-IN-OBJC-CLASS @\n";
+        CTL.InObjCClass ($3, $7) }
+| formula HOLDS_IN_NODE node_list
+     { L.(debug Linters Verbose) "\tParsed InNode@\n"; CTL.InNode ($3, $1)}
+;
+
+
 formula:
   | formula_with_paren { $1 }
   | formula_id { CTL.Atomic($1, []) }
@@ -277,8 +292,7 @@ formula:
   | formula EF WITH_TRANSITION transition_label
      { L.(debug Linters Verbose) "\tParsed EF WITH-TRANSITION '%a'@\n" CTL.Debug.pp_transition $4;
        CTL.EF($4, $1) }
-  | WHEN formula HOLDS_IN_NODE node_list
-     { L.(debug Linters Verbose) "\tParsed InNode@\n"; CTL.InNode ($4, $2)}
+  | WHEN when_formula { $2 }
   | ET node_list WITH_TRANSITION transition_label formula_EF
      { L.(debug Linters Verbose) "\tParsed ET with transition '%a'@\n" CTL.Debug.pp_transition $4;
        CTL.ET ($2, $4, $5)}

infer/src/clang/tableaux.ml

@@ -152,6 +152,10 @@ let rec normalize phi =
   | InNode (nl, phi1) ->
       let phi1' = normalize phi1 in
       InNode (nl, phi1')
+  | InObjCClass (phi1, phi2) ->
+      let phi1' = normalize phi1 in
+      let phi2' = normalize phi2 in
+      InObjCClass (phi1', phi2')
 
 
 (* Given a phi0 build the list of its subformulae including itself.
@@ -165,7 +169,7 @@ let formula_closure phi0 =
         [phi]
     | Not phi1 ->
         phi :: do_subformula phi1
-    | And (phi1, phi2) | Or (phi1, phi2) | EU (_, phi1, phi2) ->
+    | And (phi1, phi2) | Or (phi1, phi2) | EU (_, phi1, phi2) | InObjCClass (phi1, phi2) ->
         let cl1 = do_subformula phi1 in
         let cl2 = do_subformula phi2 in
         phi :: (cl1 @ cl2)
@@ -234,6 +238,8 @@ let add_valid_formulae an checker lcxt cl =
         if Option.is_some (eval_formula phi an lcxt) then add_in_set phi acc_set else acc_set
     | And (phi1, phi2) when is_valid phi1 acc_set && is_valid phi2 acc_set ->
         add_in_set phi acc_set
+    | InObjCClass (phi1, phi2) when is_valid phi1 acc_set && is_valid phi2 acc_set ->
+        add_in_set phi acc_set
     | Or (phi1, phi2) when is_valid phi1 acc_set || is_valid phi2 acc_set ->
         add_in_set phi acc_set
     | Not phi1 when not (is_valid phi1 acc_set) ->
@@ -274,7 +280,7 @@ let rec is_state_only_formula phi =
       (*L.(debug Linters Medium) "@\n ****** FOUND state_only_formula ***** @\n" ;*) true
   | Not phi1 ->
       is_state_only_formula phi1
-  | And (phi1, phi2) | Or (phi1, phi2) | Implies (phi1, phi2) ->
+  | And (phi1, phi2) | Or (phi1, phi2) | Implies (phi1, phi2) | InObjCClass (phi1, phi2) ->
       is_state_only_formula phi1 && is_state_only_formula phi2
   | InNode (_, phi1) ->
       is_state_only_formula phi1

infer/tests/codetoanalyze/objcpp/linters-for-test-only/stateless.al

@@ -0,0 +1,86 @@
+// Copyright (c) 2018-present, Facebook, Inc.
+//
+// This source code is licensed under the MIT license found in the
+// LICENSE file in the root directory of this source tree.
+
+// Requirements for stateless component implemented in this rule:
+// 1. Subclass of CKCompositeComponent
+// 2. Has only 1 method, which is constructor class method newWith...
+// 3. Does not conform to any protocols
+// 4. Does not have any ivars
+// 5. Does not have any properties
+// 6. Does not have any methods
+// 7. Does not have a view configuration. Which means, it should only have a call to either of:
+//   a. [super(or self) newWithComponent: ....];
+//   b. [super(or self) newWithView:{} component: ...];
+// 8. Does not declare a scope in the constructor: which means does call *CKComponentScope *nameOfLocalScopeVariable(....);
+DEFINE-CHECKER CKSTATELESS_COMPONENT = {
+
+ LET is_subclass_of(x) =
+        is_class(x) HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl;
+
+ LET receiver_is_super_or_self = is_receiver_super() OR is_receiver_self();
+
+ LET eventually_call_newWithComponent =
+  IN-NODE ObjCMethodDecl WITH-TRANSITION Body
+     ((call_method(REGEXP("newWithComponent:.*")) AND receiver_is_super_or_self) HOLDS-EVENTUALLY)
+   HOLDS-EVENTUALLY;
+
+
+  // ObjCMessageExpr -> MaterializeTemporaryExpr -> CXXBindTemporaryExpr -> CXXConstructExpr[]
+  LET view_is_empty =
+   WHEN
+   (is_node("MaterializeTemporaryExpr") AND
+    (is_node("CXXBindTemporaryExpr") AND
+      (cxx_construct_expr_has_no_parameters() HOLDS-NEXT)
+    ) HOLDS-NEXT
+   ) HOLDS-NEXT
+   HOLDS-IN-NODE ObjCMessageExpr;
+
+   LET eventually_call_newWithViewcomponent =
+    IN-NODE ObjCMethodDecl WITH-TRANSITION Body
+       ((call_method(REGEXP("newWithView:component:.*")) AND receiver_is_super_or_self
+         AND
+         view_is_empty)
+          HOLDS-EVENTUALLY)
+     HOLDS-EVENTUALLY;
+
+
+  LET is_scope_declaration =
+   WHEN
+     (cxx_construct_expr_has_name("CKComponentScope") HOLDS-NEXT)
+   HOLDS-IN-NODE DeclStmt;
+
+  LET eventually_declare_scope =
+   IN-NODE ObjCMethodDecl WITH-TRANSITION Body
+      (is_scope_declaration HOLDS-EVENTUALLY)
+    HOLDS-EVENTUALLY;
+
+
+  LET implementation_requirements =
+  WHEN
+   objc_class_has_only_one_constructor_method_named(REGEXP("newWith.+"))
+   AND (NOT (is_objc_instance_method_named(REGEXP(".*")) HOLDS-NEXT)) // has not instance methods
+   AND (eventually_call_newWithViewcomponent OR eventually_call_newWithComponent) // has view configuration
+   AND (NOT eventually_declare_scope)
+   AND (NOT (is_node("ObjCIvarDecl") HOLDS-EVENTUALLY))
+   AND (NOT (is_node("ObjCPropertyDecl") HOLDS-EVENTUALLY))
+ HOLDS-IN-NODE ObjCImplementationDecl;
+
+   LET interface_requirements =
+    WHEN
+       is_subclass_of("CKCompositeComponent") AND
+       (NOT adhere_to_protocol()) AND
+      (NOT (is_node("ObjCPropertyDecl") HOLDS-EVENTUALLY))
+      AND (NOT (is_node("ObjCIvarDecl") HOLDS-EVENTUALLY))
+     HOLDS-IN-NODE ObjCInterfaceDecl;
+
+  SET report_when = WHEN
+            INTERFACE [interface_requirements]
+            IMPLEMENTATION [implementation_requirements]
+         HOLDS-IN-OBJC-CLASS;
+
+  SET message = "This is a CKStateless Component and, for performance reason, can be replaced by a C function";
+  SET mode = "ON";
+
+};