From 2e64566a6c75669911bbc58044bc6f30ce54a81c Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Mon, 15 Oct 2018 08:06:27 -0700 Subject: [PATCH] Finding stateless CKComponents Reviewed By: jberdine Differential Revision: D10161169 fbshipit-source-id: dd82e48ee --- infer/src/clang/cFrontend_errors.ml | 4 + infer/src/clang/cTL.ml | 29 +++++-- infer/src/clang/cTL.mli | 1 + infer/src/clang/ctl_lexer.mll | 5 ++ infer/src/clang/ctl_parser.mly | 18 +++- infer/src/clang/tableaux.ml | 10 ++- .../objcpp/linters-for-test-only/stateless.al | 86 +++++++++++++++++++ 7 files changed, 140 insertions(+), 13 deletions(-) create mode 100644 infer/tests/codetoanalyze/objcpp/linters-for-test-only/stateless.al diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index c0df4775a..b85532f8d 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/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_ diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 4144337f8..d2dcb465c 100644 --- a/infer/src/clang/cTL.ml +++ b/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 diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 205e99244..392840758 100644 --- a/infer/src/clang/cTL.mli +++ b/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 diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll index 635825b76..d54d59144 100644 --- a/infer/src/clang/ctl_lexer.mll +++ b/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 } diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index ef240b03c..07bf26da2 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/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)} diff --git a/infer/src/clang/tableaux.ml b/infer/src/clang/tableaux.ml index ad60d5731..cc03b55a9 100644 --- a/infer/src/clang/tableaux.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/objcpp/linters-for-test-only/stateless.al b/infer/tests/codetoanalyze/objcpp/linters-for-test-only/stateless.al new file mode 100644 index 000000000..c5bfedb1a --- /dev/null +++ b/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"; + +};