From 7e3298711c9a7f6ddffed508cb2b730395e59515 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Mon, 11 Sep 2017 03:11:56 -0700 Subject: [PATCH] [AL] Compute a witness child node when computing formulas to be used for more precise bug hashing Reviewed By: ddino Differential Revision: D5767064 fbshipit-source-id: bff07cf --- infer/src/clang/CLintersContext.ml | 19 +- infer/src/clang/CLintersContext.mli | 32 ++++ infer/src/clang/CProcname.ml | 3 +- infer/src/clang/ComponentKit.ml | 30 +++- infer/src/clang/cAst_utils.ml | 24 ++- infer/src/clang/cAst_utils.mli | 3 +- infer/src/clang/cFrontend_checkers_main.ml | 83 ++++----- infer/src/clang/cFrontend_errors.ml | 41 ++--- infer/src/clang/cTL.ml | 170 +++++++++++------- infer/src/clang/cTL.mli | 3 +- infer/src/clang/ctl_parser_types.ml | 135 ++++++++++++-- infer/src/clang/ctl_parser_types.mli | 12 ++ .../objc/linters-for-test-only/issues.exp | 2 +- .../objcpp/linters-for-test-only/issues.exp | 6 +- 14 files changed, 379 insertions(+), 184 deletions(-) create mode 100644 infer/src/clang/CLintersContext.mli diff --git a/infer/src/clang/CLintersContext.ml b/infer/src/clang/CLintersContext.ml index 95cfa116e..21c26c8e6 100644 --- a/infer/src/clang/CLintersContext.ml +++ b/infer/src/clang/CLintersContext.ml @@ -17,23 +17,30 @@ type if_context = type context = { translation_unit_context: CFrontend_config.translation_unit_context ; current_method: Clang_ast_t.decl option + ; parent_methods: Clang_ast_t.decl list ; in_synchronized_block: bool (** True if the translation unit contains an ObjC class impl that's a subclass of CKComponent or CKComponentController. *) ; is_ck_translation_unit: bool - (** If inside an objc class impl, contains the objc class impl decl. *) - ; current_objc_impl: Clang_ast_t.decl option - (** True if inside an objc static factory method (a class-level initializer, like +new) *) - ; in_objc_static_factory_method: bool + (** If inside an objc class, contains the objc class (impl or interface) decl. *) + ; current_objc_class: Clang_ast_t.decl option ; et_evaluation_node: string option ; if_context: if_context option } let empty translation_unit_context = { current_method= None + ; parent_methods= [] ; translation_unit_context ; in_synchronized_block= false ; is_ck_translation_unit= false - ; current_objc_impl= None - ; in_objc_static_factory_method= false + ; current_objc_class= None ; et_evaluation_node= None ; if_context= None } + +let add_parent_method decl_opt parent_methods = + match decl_opt with Some decl -> decl :: parent_methods | None -> parent_methods + +let update_current_method context decl = + { context with + current_method= Some decl + ; parent_methods= add_parent_method context.current_method context.parent_methods } diff --git a/infer/src/clang/CLintersContext.mli b/infer/src/clang/CLintersContext.mli new file mode 100644 index 000000000..40f693687 --- /dev/null +++ b/infer/src/clang/CLintersContext.mli @@ -0,0 +1,32 @@ +(* + * Copyright (c) 2016 - 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. + *) + +open! IStd + +type if_context = + { within_responds_to_selector_block: string list + ; within_available_class_block: string list + ; ios_version_guard: string list } + +type context = + { translation_unit_context: CFrontend_config.translation_unit_context + ; current_method: Clang_ast_t.decl option + ; parent_methods: Clang_ast_t.decl list + ; in_synchronized_block: bool + (** True if the translation unit contains an ObjC class impl that's a subclass + of CKComponent or CKComponentController. *) + ; is_ck_translation_unit: bool + (** If inside an objc class, contains the objc class (impl or interface) decl. *) + ; current_objc_class: Clang_ast_t.decl option + ; et_evaluation_node: string option + ; if_context: if_context option } + +val empty : CFrontend_config.translation_unit_context -> context + +val update_current_method : context -> Clang_ast_t.decl -> context diff --git a/infer/src/clang/CProcname.ml b/infer/src/clang/CProcname.ml index 52184fa58..a57bc8580 100644 --- a/infer/src/clang/CProcname.ml +++ b/infer/src/clang/CProcname.ml @@ -204,4 +204,5 @@ let from_decl translation_unit_context ?tenv meth_decl = in Typ.Procname.mangled_objc_block name | _ - -> assert false + -> Logging.die InternalError "Expected method decl, but got %s." + (Clang_ast_proj.get_decl_kind_string meth_decl) diff --git a/infer/src/clang/ComponentKit.ml b/infer/src/clang/ComponentKit.ml index e4a07dbd5..cde7faf95 100644 --- a/infer/src/clang/ComponentKit.ml +++ b/infer/src/clang/ComponentKit.ml @@ -259,14 +259,15 @@ let component_with_multiple_factory_methods_advice context an = List.filter ~f:is_unavailable_attr decl_info.Clang_ast_t.di_attributes in let is_available = List.is_empty unavailable_attrs in - CAst_utils.is_objc_factory_method if_decl decl && is_available + CAst_utils.is_objc_factory_method ~class_decl:if_decl ~method_decl:(Some decl) + && is_available | _ -> false in let check_interface if_decl = match if_decl with | Clang_ast_t.ObjCInterfaceDecl (_, _, decls, _, _) - -> let factory_methods = List.filter ~f:(is_available_factory_method if_decl) decls in + -> let factory_methods = List.filter ~f:(is_available_factory_method (Some if_decl)) decls in List.map ~f:(fun meth_decl -> { CIssue.id= "COMPONENT_WITH_MULTIPLE_FACTORY_METHODS" @@ -295,9 +296,28 @@ let component_with_multiple_factory_methods_advice context an = let in_ck_class (context: CLintersContext.context) = Option.value_map ~f:is_component_or_controller_descendant_impl ~default:false - context.current_objc_impl + context.current_objc_class && CGeneral_utils.is_objc_extension context.translation_unit_context +let is_in_factory_method (context: CLintersContext.context) = + let interface_decl_opt = + match context.current_objc_class with + | Some ObjCImplementationDecl (_, _, _, _, impl_decl_info) + -> CAst_utils.get_decl_opt_with_decl_ref impl_decl_info.oidi_class_interface + | _ + -> None + in + let methods_to_check = + match context.current_method with + | Some current_method + -> current_method :: context.parent_methods + | None + -> context.parent_methods + in + List.exists methods_to_check ~f:(fun method_decl -> + CAst_utils.is_objc_factory_method ~class_decl:interface_decl_opt + ~method_decl:(Some method_decl) ) + (** Components shouldn't have side-effects in its initializer. http://componentkit.org/docs/no-side-effects.html @@ -310,9 +330,9 @@ let in_ck_class (context: CLintersContext.context) = let rec _component_initializer_with_side_effects_advice (context: CLintersContext.context) call_stmt = let condition = - in_ck_class context && context.in_objc_static_factory_method + in_ck_class context && is_in_factory_method context && - match context.current_objc_impl with + match context.current_objc_class with | Some d -> is_in_main_file context.translation_unit_context (Ctl_parser_types.Decl d) | None diff --git a/infer/src/clang/cAst_utils.ml b/infer/src/clang/cAst_utils.ml index 9138f2708..60210ff5f 100644 --- a/infer/src/clang/cAst_utils.ml +++ b/infer/src/clang/cAst_utils.ml @@ -380,7 +380,7 @@ let qual_type_is_typedef_named qual_type (type_name: string) : bool = let if_decl_to_di_pointer_opt if_decl = match if_decl with - | Clang_ast_t.ObjCInterfaceDecl (if_decl_info, _, _, _, _) + | Some Clang_ast_t.ObjCInterfaceDecl (if_decl_info, _, _, _, _) -> Some if_decl_info.di_pointer | _ -> None @@ -392,21 +392,19 @@ let is_instance_type qual_type = | None -> false -let return_type_matches_class_type rtp type_decl_pointer = - if is_instance_type rtp then true +let return_type_matches_class_type result_type interface_decl = + if is_instance_type result_type then true else - let return_type_decl_opt = qual_type_to_objc_interface rtp in - let return_type_decl_pointer_opt = - Option.map ~f:if_decl_to_di_pointer_opt return_type_decl_opt - in - [%compare.equal : int option option] (Some type_decl_pointer) return_type_decl_pointer_opt + let return_type_decl_opt = qual_type_to_objc_interface result_type in + [%compare.equal : int option] + (if_decl_to_di_pointer_opt interface_decl) (if_decl_to_di_pointer_opt return_type_decl_opt) -let is_objc_factory_method if_decl meth_decl = - let if_type_decl_pointer = if_decl_to_di_pointer_opt if_decl in - match meth_decl with - | Clang_ast_t.ObjCMethodDecl (_, _, omdi) +let is_objc_factory_method ~class_decl:interface_decl ~method_decl:meth_decl_opt = + let open Clang_ast_t in + match meth_decl_opt with + | Some ObjCMethodDecl (_, _, omdi) -> not omdi.omdi_is_instance_method - && return_type_matches_class_type omdi.omdi_result_type if_type_decl_pointer + && return_type_matches_class_type omdi.omdi_result_type interface_decl | _ -> false diff --git a/infer/src/clang/cAst_utils.mli b/infer/src/clang/cAst_utils.mli index b8cdce16f..25002d1e6 100644 --- a/infer/src/clang/cAst_utils.mli +++ b/infer/src/clang/cAst_utils.mli @@ -134,7 +134,8 @@ val qual_type_to_objc_interface : Clang_ast_t.qual_type -> Clang_ast_t.decl opti val qual_type_is_typedef_named : Clang_ast_t.qual_type -> string -> bool -val is_objc_factory_method : Clang_ast_t.decl -> Clang_ast_t.decl -> bool +val is_objc_factory_method : + class_decl:Clang_ast_t.decl option -> method_decl:Clang_ast_t.decl option -> bool (** A class method that returns an instance of the class is a factory method. *) val name_of_decl_ref_opt : Clang_ast_t.decl_ref option -> string option diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index e45eadf03..84dd75000 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -171,19 +171,22 @@ let compute_if_context (context: CLintersContext.context) stmt = ( {within_responds_to_selector_block; within_available_class_block; ios_version_guard} : CLintersContext.if_context ) -let is_factory_method (context: CLintersContext.context) decl = - let interface_decl_opt = - match context.current_objc_impl with - | Some ObjCImplementationDecl (_, _, _, _, impl_decl_info) - -> CAst_utils.get_decl_opt_with_decl_ref impl_decl_info.oidi_class_interface - | _ - -> None - in - match interface_decl_opt with - | Some interface_decl - -> CAst_utils.is_objc_factory_method interface_decl decl +let get_method_body_opt decl = + let open Clang_ast_t in + match decl with + | FunctionDecl (_, _, _, fdi) + | CXXMethodDecl (_, _, _, fdi, _) + | CXXConstructorDecl (_, _, _, fdi, _) + | CXXConversionDecl (_, _, _, fdi, _) + | CXXDestructorDecl (_, _, _, fdi, _) + -> fdi.Clang_ast_t.fdi_body + | ObjCMethodDecl (_, _, mdi) + -> mdi.Clang_ast_t.omdi_body + | BlockDecl (_, block_decl_info) + -> block_decl_info.Clang_ast_t.bdi_body | _ - -> false + -> Logging.die InternalError "Should only be called with method, but got %s" + (Clang_ast_proj.get_decl_kind_string decl) let rec do_frontend_checks_stmt (context: CLintersContext.context) stmt = let open Clang_ast_t in @@ -231,49 +234,33 @@ let rec do_frontend_checks_stmt (context: CLintersContext.context) stmt = and do_frontend_checks_decl (context: CLintersContext.context) decl = let open Clang_ast_t in - CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl decl) ; match decl with - | FunctionDecl (_, _, _, fdi) - | CXXMethodDecl (_, _, _, fdi, _) - | CXXConstructorDecl (_, _, _, fdi, _) - | CXXConversionDecl (_, _, _, fdi, _) - | CXXDestructorDecl (_, _, _, fdi, _) + | FunctionDecl _ + | CXXMethodDecl _ + | CXXConstructorDecl _ + | CXXConversionDecl _ + | CXXDestructorDecl _ + | ObjCMethodDecl _ + | BlockDecl _ -> ( - let context' = {context with CLintersContext.current_method= Some decl} in - match fdi.Clang_ast_t.fdi_body with + let context' = CLintersContext.update_current_method context decl in + CFrontend_errors.invoke_set_of_checkers_on_node context' (Ctl_parser_types.Decl decl) ; + match get_method_body_opt decl with | Some stmt -> do_frontend_checks_stmt context' stmt | None -> () ) - | ObjCMethodDecl (_, _, mdi) - -> ( - let context' = - { context with - CLintersContext.current_method= Some decl - ; CLintersContext.in_objc_static_factory_method= is_factory_method context decl } - in - match mdi.Clang_ast_t.omdi_body with - | Some stmt - -> do_frontend_checks_stmt context' stmt - | None - -> () ) - | BlockDecl (_, block_decl_info) - -> ( - let context' = {context with CLintersContext.current_method= Some decl} in - match block_decl_info.Clang_ast_t.bdi_body with - | Some stmt - -> do_frontend_checks_stmt context' stmt - | None - -> () ) - | ObjCImplementationDecl (_, _, decls, _, _) - -> let context' = {context with current_objc_impl= Some decl} in + | ObjCImplementationDecl (_, _, decls, _, _) | ObjCInterfaceDecl (_, _, decls, _, _) + -> CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl decl) ; + let context' = {context with current_objc_class= Some decl} in List.iter ~f:(do_frontend_checks_decl context') decls - | _ -> - match Clang_ast_proj.get_decl_context_tuple decl with - | Some (decls, _) - -> List.iter ~f:(do_frontend_checks_decl context) decls - | None - -> () + | _ + -> CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl decl) ; + match Clang_ast_proj.get_decl_context_tuple decl with + | Some (decls, _) + -> List.iter ~f:(do_frontend_checks_decl context) decls + | None + -> () let context_with_ck_set context decl_list = let is_ck = diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 4336a80da..405f96bcc 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -427,24 +427,11 @@ let log_frontend_issue translation_unit_context method_decl_opt key (issue_desc: Reporting.log_issue_from_errlog err_kind errlog exn ~loc:issue_desc.loc ~ltr:trace ~node_id:(0, key) ?linters_def_file ?doc_url:issue_desc.doc_url -let get_current_method context (an: Ctl_parser_types.ast_node) = - match an with - | Decl (FunctionDecl _ as d) - | Decl (CXXMethodDecl _ as d) - | Decl (CXXConstructorDecl _ as d) - | Decl (CXXConversionDecl _ as d) - | Decl (CXXDestructorDecl _ as d) - | Decl (ObjCMethodDecl _ as d) - | Decl (BlockDecl _ as d) - -> Some d - | _ - -> context.CLintersContext.current_method - let fill_issue_desc_info_and_log context an key issue_desc linters_def_file loc = let desc = remove_new_lines (expand_message_string context issue_desc.CIssue.description an) in let issue_desc' = {issue_desc with CIssue.description= desc; CIssue.loc= loc} in log_frontend_issue context.CLintersContext.translation_unit_context - (get_current_method context an) key issue_desc' linters_def_file + context.CLintersContext.current_method key issue_desc' linters_def_file (* Calls the set of hard coded checkers (if any) *) let invoke_set_of_hard_coded_checkers_an context (an: Ctl_parser_types.ast_node) = @@ -467,20 +454,22 @@ let invoke_set_of_hard_coded_checkers_an context (an: Ctl_parser_types.ast_node) (* Calls the set of checkers parsed from files (if any) *) let invoke_set_of_parsed_checkers_an parsed_linters context (an: Ctl_parser_types.ast_node) = - let key = - match an with - | Decl dec - -> CAst_utils.generate_key_decl dec - | Stmt st - -> CAst_utils.generate_key_stmt st - in List.iter ~f:(fun (linter: linter) -> - if CIssue.should_run_check linter.issue_desc.CIssue.mode - && CTL.eval_formula linter.condition an context - then - let loc = CFrontend_checkers.location_from_an context an in - fill_issue_desc_info_and_log context an key linter.issue_desc linter.def_file loc) + if CIssue.should_run_check linter.issue_desc.CIssue.mode then + match CTL.eval_formula linter.condition an context with + | None + -> () + | Some witness + -> let key = + match witness with + | Decl dec + -> CAst_utils.generate_key_decl dec + | Stmt st + -> CAst_utils.generate_key_stmt st + in + let loc = CFrontend_checkers.location_from_an context witness in + fill_issue_desc_info_and_log context witness key linter.issue_desc linter.def_file loc) parsed_linters (* We decouple the hardcoded checkers from the parsed ones *) diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 6e8319ef9..707773553 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -26,6 +26,13 @@ type transitions = | PointerToDecl (** stmt to decl *) | Protocol (** decl to decl *) +let is_transition_to_successor trans = + match trans with + | Body | InitExpr | ParameterName _ | Parameters | Cond + -> true + | Super | PointerToDecl | Protocol + -> false + (* In formulas below prefix "E" means "exists a path" "A" means "for all path" *) @@ -257,7 +264,11 @@ module Debug = struct type eval_result = Eval_undefined | Eval_true | Eval_false type content = - {ast_node: ast_node; phi: t; lcxt: CLintersContext.context; eval_result: eval_result} + { ast_node: ast_node + ; phi: t + ; lcxt: CLintersContext.context + ; eval_result: eval_result + ; witness: ast_node option } type eval_node = {id: int; content: content} @@ -276,7 +287,8 @@ module Debug = struct ; breakpoint_line: int option ; debugger_active: bool } - let create_content ast_node phi lcxt = {ast_node; phi; eval_result= Eval_undefined; lcxt} + let create_content ast_node phi lcxt = + {ast_node; phi; eval_result= Eval_undefined; lcxt; witness= None} let create source_file = let breakpoint_token = "INFER_BREAKPOINT" in @@ -319,10 +331,18 @@ module Debug = struct | Last_occurrence n -> (n, true) in + let witness_str = + match eval_node.content.witness with + | Some witness + -> "\n- witness: " ^ Ctl_parser_types.ast_node_kind witness ^ " " + ^ Ctl_parser_types.ast_node_name witness + | None + -> "" + in let ast_str = - Format.asprintf "%a" + Format.asprintf "%a %s" (pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s")) - ast_root + ast_root witness_str in L.progress "@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n" eval_node.id (Stack.length t.eval_stack) @@ -380,13 +400,16 @@ module Debug = struct {t' with next_id= t.next_id + 1} let eval_end t result = + let result_bool = Option.is_some result in let eval_result_of_bool = function true -> Eval_true | false -> Eval_false in if Stack.is_empty t.eval_stack then raise (Empty_stack "Unbalanced number of eval_begin/eval_end invocations") ; let evaluated_tree, eval_node, ast_node_to_display = match Stack.pop_exn t.eval_stack with Tree (({id= _; content} as eval_node), children), ast_node_to_display -> - let content' = {content with eval_result= eval_result_of_bool result} in + let content' = + {content with eval_result= eval_result_of_bool result_bool; witness= result} + in let eval_node' = {eval_node with content= content'} in (Tree (eval_node', children), eval_node', ast_node_to_display) in @@ -565,48 +588,6 @@ let save_dotty_when_in_debug_mode source_file = -> () (* Helper functions *) - -let get_successor_nodes an = - (* get_decl_of_stmt get declarations that are directly embedded - as immediate children (i.e. distance 1) of an stmt (i.e., no transition). - TBD: check if a dual is needed for get_stmt_of_decl - *) - let get_decl_of_stmt st = - match st with Clang_ast_t.BlockExpr (_, _, _, d) -> [Decl d] | _ -> [] - in - match an with - | Stmt st - -> let _, succs_st = Clang_ast_proj.get_stmt_tuple st in - let succs = List.map ~f:(fun s -> Stmt s) succs_st in - succs @ get_decl_of_stmt st - | Decl dec -> - match Clang_ast_proj.get_decl_context_tuple dec with - | Some (decl_list, _) - -> List.map ~f:(fun d -> Decl d) decl_list - | None - -> [] - -let node_to_string an = - match an with - | Decl d - -> Clang_ast_proj.get_decl_kind_string d - | Stmt s - -> Clang_ast_proj.get_stmt_kind_string s - -let node_to_unique_string_id an = - match an with - | Decl d - -> let di = Clang_ast_proj.get_decl_tuple d in - Clang_ast_proj.get_decl_kind_string d ^ string_of_int di.Clang_ast_t.di_pointer - | Stmt s - -> let si, _ = Clang_ast_proj.get_stmt_tuple s in - Clang_ast_proj.get_stmt_kind_string s ^ string_of_int si.Clang_ast_t.si_pointer - -(* true iff an ast node is a node of type among the list tl *) -let node_has_type tl an = - let an_alexp = ALVar.Const (node_to_string an) in - List.mem ~equal:ALVar.equal tl an_alexp - (* given a decl returns a stmt such that decl--->stmt via label trs *) let transition_decl_to_stmt d trs = let open Clang_ast_t in @@ -756,6 +737,20 @@ let next_state_via_transition an trans = | _, _ -> [] +let choose_one_witness an1 an2 = + if Ctl_parser_types.ast_node_equal an1 an2 then an1 + else if Ctl_parser_types.is_node_successor_of an1 ~is_successor:an2 then an2 + else an1 + +let choose_witness_opt witness_opt1 witness_opt2 = + match (witness_opt1, witness_opt2) with + | Some witness1, Some witness2 + -> Some (choose_one_witness witness1 witness2) + | Some witness, None | None, Some witness + -> Some witness + | None, None + -> None + (* Evaluation of formulas *) (* evaluate an atomic formula (i.e. a predicate) on a ast node an and a linter context lcxt. That is: an, lcxt |= pred_name(params) *) @@ -857,6 +852,24 @@ let rec eval_Atomic _pred_name args an lcxt = | _ -> L.(die ExternalError) "Undefined Predicate or wrong set of arguments: '%s'" pred_name +and eval_AND an lcxt f1 f2 = + match eval_formula f1 an lcxt with + | Some witness1 -> ( + match eval_formula f2 an lcxt with + | Some witness2 + -> Some (choose_one_witness witness1 witness2) + | _ + -> None ) + | None (* we short-circuit the AND evaluation *) + -> None + +and eval_OR an lcxt f1 f2 = choose_witness_opt (eval_formula f1 an lcxt) (eval_formula f2 an lcxt) + +and eval_Implies an lcxt f1 f2 = + let witness1 = if Option.is_some (eval_formula f1 an lcxt) then None else Some an in + let witness2 = eval_formula f2 an lcxt in + choose_witness_opt witness1 witness2 + (* an, lcxt |= EF phi <=> an, lcxt |= phi or exists an' in Successors(st): an', lcxt |= EF phi @@ -871,8 +884,11 @@ and eval_EF phi an lcxt trans = let phi' = Or (phi, EX (trans, EF (trans, phi))) in eval_formula phi' an lcxt | None, _ - -> eval_formula phi an lcxt - || List.exists ~f:(fun an' -> eval_EF phi an' lcxt trans) (get_successor_nodes an) + -> let witness_opt = eval_formula phi an lcxt in + if Option.is_some witness_opt then witness_opt + else + List.fold_left (Ctl_parser_types.get_direct_successor_nodes an) ~init:witness_opt ~f: + (fun acc node -> choose_witness_opt (eval_EF phi node lcxt trans) acc ) (* an, lcxt |= EX phi <=> exists an' in Successors(st): an', lcxt |= phi @@ -882,9 +898,21 @@ and eval_EF phi an lcxt trans = *) and eval_EX phi an lcxt trans = let succs = - match trans with Some l -> next_state_via_transition an l | None -> get_successor_nodes an + match trans with + | Some l + -> next_state_via_transition an l + | None + -> Ctl_parser_types.get_direct_successor_nodes an in - List.exists ~f:(fun an' -> eval_formula phi an' lcxt) succs + let witness_opt = + List.fold_left succs ~init:None ~f:(fun acc node -> + choose_witness_opt (eval_formula phi node lcxt) acc ) + in + match (witness_opt, trans) with + | Some _, Some trans when not (is_transition_to_successor trans) + -> Some an (* We want to limit the witnesses to the successors of the original node. *) + | _ + -> witness_opt (* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2))) @@ -912,11 +940,15 @@ and in_node node_type_list phi an lctx = let holds_for_one_node n = match lctx.CLintersContext.et_evaluation_node with | Some id - -> String.equal id (node_to_unique_string_id an) && eval_formula phi an lctx + -> if String.equal id (Ctl_parser_types.ast_node_unique_string_id an) then + eval_formula phi an lctx + else None | None - -> node_has_type [n] an && eval_formula phi an lctx + -> if Ctl_parser_types.ast_node_has_kind [n] an then eval_formula phi an lctx else None in - List.exists ~f:holds_for_one_node node_type_list + (* This is basically an OR of formula holds in the various nodes in the list *) + List.fold_left node_type_list ~init:None ~f:(fun acc node -> + choose_witness_opt (holds_for_one_node node) acc ) (* Intuitive meaning: (an,lcxt) satifies EH[Classes] phi if the node an is among the declaration specified by the list Classes and @@ -952,10 +984,12 @@ and eval_ET tl trs phi an lcxt = and eval_ETX tl trs phi an lcxt = let lcxt', tl' = - match (lcxt.CLintersContext.et_evaluation_node, node_has_type tl an) with + match (lcxt.CLintersContext.et_evaluation_node, Ctl_parser_types.ast_node_has_kind tl an) with | None, true - -> let an_alexp = ALVar.Const (node_to_string an) in - ( {lcxt with CLintersContext.et_evaluation_node= Some (node_to_unique_string_id an)} + -> let an_alexp = ALVar.Const (Ctl_parser_types.ast_node_kind an) in + ( { lcxt with + CLintersContext.et_evaluation_node= + Some (Ctl_parser_types.ast_node_unique_string_id an) } , [an_alexp] ) | _, _ -> (lcxt, tl) @@ -970,26 +1004,26 @@ and eval_ETX tl trs phi an lcxt = eval_formula f an lcxt' (* Formulas are evaluated on a AST node an and a linter context lcxt *) -and eval_formula f an lcxt = +and eval_formula f an lcxt : Ctl_parser_types.ast_node option = debug_eval_begin (debug_create_payload an f lcxt) ; let res = match f with | True - -> true + -> Some an | False - -> false + -> None | Atomic (name, params) - -> eval_Atomic name params an lcxt - | Not f1 - -> not (eval_formula f1 an lcxt) + -> if eval_Atomic name params an lcxt then Some an else None + | InNode (node_type_list, f1) + -> in_node node_type_list f1 an lcxt + | Not f1 -> ( + match eval_formula f1 an lcxt with Some _ -> None | None -> Some an ) | And (f1, f2) - -> eval_formula f1 an lcxt && eval_formula f2 an lcxt + -> eval_AND an lcxt f1 f2 | Or (f1, f2) - -> eval_formula f1 an lcxt || eval_formula f2 an lcxt + -> eval_OR an lcxt f1 f2 | Implies (f1, f2) - -> not (eval_formula f1 an lcxt) || eval_formula f2 an lcxt - | InNode (node_type_list, f1) - -> in_node node_type_list f1 an lcxt + -> eval_Implies an lcxt f1 f2 | AU (trans, f1, f2) -> eval_AU f1 f2 an lcxt trans | EU (trans, f1, f2) diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 00a7b5704..2cf5fb18d 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -114,7 +114,8 @@ type al_file = val print_checker : ctl_checker -> unit -val eval_formula : t -> ast_node -> CLintersContext.context -> bool +val eval_formula : t -> ast_node -> CLintersContext.context -> ast_node option +(** return the evaluation of the formula and a witness *) val save_dotty_when_in_debug_mode : SourceFile.t -> unit diff --git a/infer/src/clang/ctl_parser_types.ml b/infer/src/clang/ctl_parser_types.ml index f0818d1fe..f3095fa03 100644 --- a/infer/src/clang/ctl_parser_types.ml +++ b/infer/src/clang/ctl_parser_types.ml @@ -81,6 +81,130 @@ let rec ast_node_name an = | _ -> "" +let ast_node_kind node = + match node with + | Stmt stmt + -> Clang_ast_proj.get_stmt_kind_string stmt + | Decl decl + -> Clang_ast_proj.get_decl_kind_string decl + +(* true iff an ast node is a node of type among the list tl *) +let ast_node_has_kind tl an = + let an_alexp = ALVar.Const (ast_node_kind an) in + List.mem ~equal:ALVar.equal tl an_alexp + +let ast_node_pointer node = + match node with + | Stmt stmt + -> let s_stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in + s_stmt_info.si_pointer + | Decl decl + -> let d_decl_info = Clang_ast_proj.get_decl_tuple decl in + d_decl_info.di_pointer + +let ast_node_unique_string_id an = Printf.sprintf "%s %d" (ast_node_kind an) (ast_node_pointer an) + +let ast_node_cast_kind an = + match an with + | Decl _ + -> "" + | Stmt stmt -> + match Clang_ast_proj.get_cast_kind stmt with + | Some cast_kind + -> Clang_ast_proj.string_of_cast_kind cast_kind + | None + -> "" + +let ast_node_equal node1 node2 = Int.equal (ast_node_pointer node1) (ast_node_pointer node2) + +let get_successor_stmts_of_stmt stmt = + let _, node_succ_stmts = Clang_ast_proj.get_stmt_tuple stmt in + node_succ_stmts + +let get_successor_decls_of_stmt stmt = + let open Clang_ast_t in + match stmt with + | DeclStmt (_, _, succ_decls) + -> succ_decls + | BlockExpr (_, _, _, decl) + -> [decl] + | _ + -> [] + +let get_successor_decls_of_decl decl = + match Clang_ast_proj.get_decl_context_tuple decl with Some (decls, _) -> decls | None -> [] + +let get_successor_stmts_of_decl decl = + let open Clang_ast_t in + match decl with + | FunctionDecl (_, _, _, fdi) + | CXXMethodDecl (_, _, _, fdi, _) + | CXXConstructorDecl (_, _, _, fdi, _) + | CXXConversionDecl (_, _, _, fdi, _) + | CXXDestructorDecl (_, _, _, fdi, _) + -> Option.to_list fdi.Clang_ast_t.fdi_body + | ObjCMethodDecl (_, _, mdi) + -> Option.to_list mdi.Clang_ast_t.omdi_body + | BlockDecl (_, block_decl_info) + -> Option.to_list block_decl_info.Clang_ast_t.bdi_body + | VarDecl (_, _, _, var_decl_info) + -> Option.to_list var_decl_info.vdi_init_expr + | ObjCIvarDecl (_, _, _, fldi, _) + | FieldDecl (_, _, _, fldi) + | ObjCAtDefsFieldDecl (_, _, _, fldi) + -> Option.to_list fldi.fldi_init_expr + | _ + -> [] + +let get_successor_stmts an = + match an with + | Stmt stmt + -> get_successor_stmts_of_stmt stmt + | Decl decl + -> get_successor_stmts_of_decl decl + +let get_successor_decls an = + match an with + | Stmt stmt + -> get_successor_decls_of_stmt stmt + | Decl decl + -> get_successor_decls_of_decl decl + +(* Either succ_node is a direct successor of node or +succ_node is a successor of one of the successors of node *) +let rec is_node_successor_of ~is_successor:succ_node node = + match succ_node with + | Stmt _ + -> let node_succ_stmts = get_successor_stmts node in + List.exists node_succ_stmts ~f:(fun (s: Clang_ast_t.stmt) -> + ast_node_equal (Stmt s) succ_node + || is_node_successor_of ~is_successor:succ_node (Stmt s) ) + | Decl _ + -> let node_succ_decls = get_successor_decls node in + List.exists node_succ_decls ~f:(fun (d: Clang_ast_t.decl) -> + ast_node_equal (Decl d) succ_node + || is_node_successor_of ~is_successor:succ_node (Decl d) ) + +let get_direct_successor_nodes an = + (* get_decl_of_stmt get declarations that are directly embedded + as immediate children (i.e. distance 1) of an stmt (i.e., no transition). + TBD: check if a dual is needed for get_stmt_of_decl + *) + let get_decl_of_stmt st = + match st with Clang_ast_t.BlockExpr (_, _, _, d) -> [Decl d] | _ -> [] + in + match an with + | Stmt st + -> let _, succs_st = Clang_ast_proj.get_stmt_tuple st in + let succs = List.map ~f:(fun s -> Stmt s) succs_st in + succs @ get_decl_of_stmt st + | Decl dec -> + match Clang_ast_proj.get_decl_context_tuple dec with + | Some (decl_list, _) + -> List.map ~f:(fun d -> Decl d) decl_list + | None + -> [] + let infer_prefix = "__infer_ctl_" (** Data structures for type parser. @@ -374,14 +498,3 @@ let stmt_node_child_type an = match stmts with [stmt] -> ast_node_type (Stmt stmt) | _ -> "" ) | _ -> "" - -let ast_node_cast_kind an = - match an with - | Decl _ - -> "" - | Stmt stmt -> - match Clang_ast_proj.get_cast_kind stmt with - | Some cast_kind - -> Clang_ast_proj.string_of_cast_kind cast_kind - | None - -> "" diff --git a/infer/src/clang/ctl_parser_types.mli b/infer/src/clang/ctl_parser_types.mli index f1e5eab72..c465ae553 100644 --- a/infer/src/clang/ctl_parser_types.mli +++ b/infer/src/clang/ctl_parser_types.mli @@ -13,14 +13,26 @@ open! IStd (** the kind of AST nodes where formulas are evaluated *) type ast_node = Stmt of Clang_ast_t.stmt | Decl of Clang_ast_t.decl +val ast_node_equal : ast_node -> ast_node -> bool + val ast_node_name : ast_node -> string val ast_node_type : ast_node -> string +val ast_node_kind : ast_node -> string + +val ast_node_has_kind : ALVar.alexp list -> ast_node -> bool + +val ast_node_unique_string_id : ast_node -> string + val stmt_node_child_type : ast_node -> string val ast_node_cast_kind : ast_node -> string +val is_node_successor_of : is_successor:ast_node -> ast_node -> bool + +val get_direct_successor_nodes : ast_node -> ast_node list + val infer_prefix : string (** Data structures for type parser. diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp b/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp index cc1ee2b9a..184a916d7 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp +++ b/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp @@ -92,7 +92,7 @@ codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m25, 101, TEST_ codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m26, 102, TEST_BUILTIN_TYPE, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m26:pname2:pname3:pname4:, 103, TEST_BUILTIN_TYPE, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m26:pname2:pname3:pname4:, 103, TEST_NTH_PARAM_TYPE_CHECK, [] -codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m26:pname2:pname3:pname4:, 103, TEST_PARAM_TYPE_CHECK, [] +codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m26:pname2:pname3:pname4:, 105, TEST_PARAM_TYPE_CHECK, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m3, 75, TEST_BUILTIN_TYPE, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m4, 76, TEST_BUILTIN_TYPE, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, TestType_m7, 79, TEST_BUILTIN_TYPE, [] diff --git a/infer/tests/codetoanalyze/objcpp/linters-for-test-only/issues.exp b/infer/tests/codetoanalyze/objcpp/linters-for-test-only/issues.exp index cbf1d313c..964ccca49 100644 --- a/infer/tests/codetoanalyze/objcpp/linters-for-test-only/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/linters-for-test-only/issues.exp @@ -4,9 +4,9 @@ codetoanalyze/objcpp/linters-for-test-only/ReferenceTest.mm, ReferenceTest_newWi codetoanalyze/objcpp/linters-for-test-only/ReferenceTest.mm, ReferenceTest_newWithActionRef:, 40, TEST_REFERENCE, [] codetoanalyze/objcpp/linters-for-test-only/ReferenceTest.mm, ReferenceTest_newWithConstAction:, 21, TEST_REFERENCE, [] codetoanalyze/objcpp/linters-for-test-only/ReferenceTest.mm, ReferenceTest_newWithConstAction:, 36, TEST_REFERENCE, [] -codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, anotherButtonComponent, 36, PARAMETER_TRANS_TYPE, [] -codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, anotherButtonComponent, 36, TEST_PARAMETER_LABEL, [] -codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, anotherButtonComponent, 36, TEST_PARAMETER_LABEL_REGEXP, [] +codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, anotherButtonComponent, 41, PARAMETER_TRANS_TYPE, [] +codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, anotherButtonComponent, 41, TEST_PARAMETER_LABEL, [] +codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, anotherButtonComponent, 41, TEST_PARAMETER_LABEL_REGEXP, [] codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, buttonComponent, 31, PARAMETER_TRANS_TYPE, [] codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, buttonComponent, 31, TEST_PARAMETER_LABEL, [] codetoanalyze/objcpp/linters-for-test-only/TestParamterLabelsChecks.mm, buttonComponent, 31, TEST_PARAMETER_LABEL_EMPTY_MAP, []