From 43f3a33c0c311134479bf0a6f5a2f2df974fdb90 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Mon, 13 Mar 2017 03:46:17 -0700 Subject: [PATCH] [infer][AL-DSL] Added predicates to query method calls of a certain class (Real Version). Reviewed By: dulmarod Differential Revision: D4689148 fbshipit-source-id: 97716fd --- infer/lib/linter_rules/linters.al | 8 ++-- infer/src/clang/cPredicates.ml | 79 +++++++++++++++++++++++++++---- infer/src/clang/cPredicates.mli | 12 ++++- infer/src/clang/cTL.ml | 25 +++++++--- 4 files changed, 105 insertions(+), 19 deletions(-) diff --git a/infer/lib/linter_rules/linters.al b/infer/lib/linter_rules/linters.al index 78845ee9c..763322361 100644 --- a/infer/lib/linter_rules/linters.al +++ b/infer/lib/linter_rules/linters.al @@ -81,10 +81,10 @@ DEFINE-CHECKER BAD_POINTER_COMPARISON = { DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = { LET exists_method_calling_addObserver = - call_method(addObserver:selector:name:object:) HOLDS-EVENTUALLY; + call_method_strict(addObserver:selector:name:object:) HOLDS-EVENTUALLY; LET exists_method_calling_addObserverForName = - call_method(addObserverForName:object:queue:usingBlock:) HOLDS-EVENTUALLY; + call_method_strict(addObserverForName:object:queue:usingBlock:) HOLDS-EVENTUALLY; LET add_observer = exists_method_calling_addObserver OR exists_method_calling_addObserverForName; @@ -95,10 +95,10 @@ DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = { HOLDS-EVENTUALLY; LET exists_method_calling_removeObserver = - call_method(removeObserver:) HOLDS-EVENTUALLY; + call_method_strict(removeObserver:) HOLDS-EVENTUALLY; LET exists_method_calling_removeObserverName = - call_method(removeObserver:name:object:) HOLDS-EVENTUALLY; + call_method_strict(removeObserver:name:object:) HOLDS-EVENTUALLY; LET remove_observer = exists_method_calling_removeObserver OR exists_method_calling_removeObserverName; diff --git a/infer/src/clang/cPredicates.ml b/infer/src/clang/cPredicates.ml index b7e8db2ee..cfc88e36d 100644 --- a/infer/src/clang/cPredicates.ml +++ b/infer/src/clang/cPredicates.ml @@ -61,28 +61,91 @@ let captured_variables_cxx_ref an = type t = string * string list (* (name, [param1,...,paramK]) *) +(* true if and only if string contained occurs in container *) +let str_contains container contained = + let rexp = Str.regexp_string_case_fold contained in + try + Str.search_forward rexp container 0 >= 0 + with Not_found -> false + let pp_predicate fmt (name, arglist) = Format.fprintf fmt "%s(%a)" name (Pp.comma_seq Format.pp_print_string) arglist let is_declaration_kind decl s = String.equal (Clang_ast_proj.get_decl_kind_string decl) s -(* st |= call_method(m) *) -let call_method m an = +let _is_objc_interface_named comp an expected_name = + match an with + | Ctl_parser_types.Decl Clang_ast_t.ObjCInterfaceDecl(_, ni, _, _, _) -> + comp ni.ni_name expected_name + | _ -> false + +(* is an objc interface with name expected_name *) +let is_objc_interface_named_strict an expected_name = + _is_objc_interface_named (String.equal) an expected_name + +(* is an objc interface with name expected_name *) +let is_objc_interface_named an expected_name = + _is_objc_interface_named (str_contains) an expected_name + +let _is_object_of_class_named comp receiver cname = + let open Clang_ast_t in + match receiver with + | PseudoObjectExpr (_, _, ei) + | ImplicitCastExpr (_, _, ei, _) + | ParenExpr (_, _, ei) -> + (match CAst_utils.type_ptr_to_objc_interface ei.ei_type_ptr with + | Some interface -> comp (Ctl_parser_types.Decl interface) cname + | _ -> false) + | _ -> false + +(* checkes whether an object is of a certain class *) +let is_object_of_class_named_strict receiver cname = + _is_object_of_class_named (is_objc_interface_named_strict) receiver cname + +(* checkes whether an object is of a certain class *) +let is_object_of_class_named receiver cname = + _is_object_of_class_named (is_objc_interface_named) receiver cname + +let _call_method comp an m = match an with | Ctl_parser_types.Stmt (Clang_ast_t.ObjCMessageExpr (_, _, _, omei)) -> - String.equal omei.omei_selector m + comp omei.omei_selector m | _ -> false +(* an |= call_method(m) where the name must be exactly m *) +let call_method_strict an m = + _call_method (String.equal) an m + +(* an |= call_method(m) where we check is the name contains m *) +let call_method an m = + _call_method (str_contains) an m + +let _call_class_method comp an cname mname = + Logging.out "...Evaluating call_class_method\n"; + match an with + | Ctl_parser_types.Stmt (Clang_ast_t.ObjCMessageExpr (_, receiver :: _, _, omei)) -> + is_object_of_class_named receiver cname && + comp omei.omei_selector mname + | _ -> false + +(* an is a node calling method mname of class cname. + The equality is strict. +*) +let call_class_method_strict an cname mname = + _call_class_method (String.equal) an cname mname + +(* an is a node calling method whose name contains mname of a + class whose name contains cname. +*) +let call_class_method an cname mname = + _call_class_method (str_contains) an cname mname + let property_name_contains_word word an = match an with | Ctl_parser_types.Decl decl -> (match Clang_ast_proj.get_named_decl_tuple decl with - | Some (_, n) -> let pname = n.Clang_ast_t.ni_name in - let rexp = Str.regexp_string_case_fold word in - (try - Str.search_forward rexp pname 0 >= 0 - with Not_found -> false) + | Some (_, n) -> str_contains n.Clang_ast_t.ni_name word | _ -> false) | _ -> false diff --git a/infer/src/clang/cPredicates.mli b/infer/src/clang/cPredicates.mli index 427f0e8c0..12dbbd4ee 100644 --- a/infer/src/clang/cPredicates.mli +++ b/infer/src/clang/cPredicates.mli @@ -13,7 +13,17 @@ type t = string * string list (* (name, [param1,...,paramK]) *) val captured_variables_cxx_ref : Ctl_parser_types.ast_node -> Clang_ast_t.named_decl_info list -val call_method : string -> Ctl_parser_types.ast_node -> bool +val call_method_strict : Ctl_parser_types.ast_node -> string -> bool + +val call_method : Ctl_parser_types.ast_node -> string -> bool + +val call_class_method : Ctl_parser_types.ast_node -> string -> string -> bool + +val call_class_method_strict : Ctl_parser_types.ast_node -> string -> string -> bool + +val is_objc_interface_named_strict : Ctl_parser_types.ast_node -> string -> bool + +val is_objc_interface_named : Ctl_parser_types.ast_node -> string -> bool val property_name_contains_word : string -> Ctl_parser_types.ast_node -> bool diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 0567676f4..70a97cbc9 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -412,8 +412,17 @@ let next_state_via_transition an trans = linter context lcxt. That is: an, lcxt |= pred_name(params) *) let rec eval_Atomic pred_name args an lcxt = match pred_name, args, an with - | "call_method", [m], an -> CPredicates.call_method m an - | "property_name_contains_word", [word], an -> CPredicates.property_name_contains_word word an + | "call_method", [m], an -> CPredicates.call_method an m + | "call_method_strict", [m], an -> CPredicates.call_method_strict an m + | "call_class_method", [c; m], an -> CPredicates.call_class_method an c m + | "call_class_method_strict", [c; m], an -> + CPredicates.call_class_method_strict an c m + | "is_objc_interface_named", [name], an -> + CPredicates.is_objc_interface_named an name + | "is_objc_interface_named_strict", [name], an -> + CPredicates.is_objc_interface_named_strict an name + | "property_name_contains_word", [word], an -> + CPredicates.property_name_contains_word word an | "is_objc_extension", [], _ -> CPredicates.is_objc_extension lcxt | "is_global_var", [], an -> CPredicates.is_syntactically_global_var an | "is_const_var", [], an -> CPredicates.is_const_expr_var an @@ -421,22 +430,26 @@ let rec eval_Atomic pred_name args an lcxt = | "is_strong_property", [], an -> CPredicates.is_strong_property an | "is_assign_property", [], an -> CPredicates.is_assign_property an | "is_property_pointer_type", [], an -> CPredicates.is_property_pointer_type an - | "context_in_synchronized_block", [], _ -> CPredicates.context_in_synchronized_block lcxt + | "context_in_synchronized_block", [], _ -> + CPredicates.context_in_synchronized_block lcxt | "is_ivar_atomic", [], an -> CPredicates.is_ivar_atomic an | "is_method_property_accessor_of_ivar", [], an -> CPredicates.is_method_property_accessor_of_ivar an lcxt | "is_objc_constructor", [], _ -> CPredicates.is_objc_constructor lcxt | "is_objc_dealloc", [], _ -> CPredicates.is_objc_dealloc lcxt | "captures_cxx_references", [], _ -> CPredicates.captures_cxx_references an - | "is_binop_with_kind", [str_kind], an -> CPredicates.is_binop_with_kind str_kind an - | "is_unop_with_kind", [str_kind], an -> CPredicates.is_unop_with_kind str_kind an + | "is_binop_with_kind", [str_kind], an -> + CPredicates.is_binop_with_kind str_kind an + | "is_unop_with_kind", [str_kind], an -> + CPredicates.is_unop_with_kind str_kind an | "in_node", [nodename], an -> CPredicates.is_node nodename an | "isa", [classname], an -> CPredicates.isa classname an | "decl_unavailable_in_supported_ios_sdk", [], an -> CPredicates.decl_unavailable_in_supported_ios_sdk lcxt an | "within_responds_to_selector_block", [], an -> CPredicates.within_responds_to_selector_block lcxt an - | _ -> failwith ("ERROR: Undefined Predicate or wrong set of arguments: " ^ pred_name) + | _ -> failwith + ("ERROR: Undefined Predicate or wrong set of arguments: " ^ pred_name) (* an, lcxt |= EF phi <=> an, lcxt |= phi or exists an' in Successors(st): an', lcxt |= EF phi