pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Making signature of predicates uniform

Browse Source 
Reviewed By: martinoluca

Differential Revision: D4507368

fbshipit-source-id: 4957426
master
Dino Distefano 8 years ago committed by Facebook Github Bot
parent 319e3ed271
commit fb14d31bb7
13 changed files with 275 additions and 248 deletions
Show Stats Download Patch File Download Diff File

26
infer/src/clang/ComponentKit.ml
Unescape View File

@ -12,10 +12,10 @@ open! PVariant
let get_source_range an = let get_source_range an =
match an with match an with
| CTL.Decl decl -> | Ctl_parser_types.Decl decl ->
let decl_info = Clang_ast_proj.get_decl_tuple decl in let decl_info = Clang_ast_proj.get_decl_tuple decl in
decl_info.Clang_ast_t.di_source_range decl_info.Clang_ast_t.di_source_range
| CTL.Stmt stmt -> | Ctl_parser_types.Stmt stmt ->
let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
stmt_info.Clang_ast_t.si_source_range stmt_info.Clang_ast_t.si_source_range
@ -103,7 +103,7 @@ let mutable_local_vars_advice context an =
| _ -> false in | _ -> false in
match an with match an with
| CTL.Decl (Clang_ast_t.VarDecl(decl_info, named_decl_info, qual_type, _) as decl)-> | Ctl_parser_types.Decl (Clang_ast_t.VarDecl(decl_info, named_decl_info, qual_type, _) as decl)->
let is_const_ref = match CAst_utils.get_type qual_type.qt_type_ptr with let is_const_ref = match CAst_utils.get_type qual_type.qt_type_ptr with
| Some LValueReferenceType (_, {Clang_ast_t.qt_is_const}) -> | Some LValueReferenceType (_, {Clang_ast_t.qt_is_const}) ->
qt_is_const qt_is_const
@ -137,7 +137,7 @@ let component_factory_function_advice context an =
CAst_utils.is_objc_if_descendant decl [CFrontend_config.ckcomponent_cl] in CAst_utils.is_objc_if_descendant decl [CFrontend_config.ckcomponent_cl] in
match an with match an with
| CTL.Decl (Clang_ast_t.FunctionDecl (decl_info, _, (qual_type: Clang_ast_t.qual_type), _)) -> | Ctl_parser_types.Decl (Clang_ast_t.FunctionDecl (decl_info, _, (qual_type: Clang_ast_t.qual_type), _)) ->
let objc_interface = let objc_interface =
CAst_utils.type_ptr_to_objc_interface qual_type.qt_type_ptr in CAst_utils.type_ptr_to_objc_interface qual_type.qt_type_ptr in
let condition = let condition =
@ -203,7 +203,7 @@ let component_with_unconventional_superclass_advice context an =
CTL.False, None CTL.False, None
| _ -> assert false in | _ -> assert false in
match an with match an with
| CTL.Decl (Clang_ast_t.ObjCImplementationDecl (_, _, _, _, impl_decl_info)) -> | Ctl_parser_types.Decl (Clang_ast_t.ObjCImplementationDecl (_, _, _, _, impl_decl_info)) ->
let if_decl_opt = let if_decl_opt =
CAst_utils.get_decl_opt_with_decl_ref impl_decl_info.oidi_class_interface in CAst_utils.get_decl_opt_with_decl_ref impl_decl_info.oidi_class_interface in
if Option.is_some if_decl_opt && is_ck_context context an then if Option.is_some if_decl_opt && is_ck_context context an then
@ -253,7 +253,7 @@ let component_with_multiple_factory_methods_advice context an =
}) (IList.drop_first 1 factory_methods) }) (IList.drop_first 1 factory_methods)
| _ -> assert false in | _ -> assert false in
match an with match an with
| CTL.Decl (Clang_ast_t.ObjCImplementationDecl (_, _, _, _, impl_decl_info)) -> | Ctl_parser_types.Decl (Clang_ast_t.ObjCImplementationDecl (_, _, _, _, impl_decl_info)) ->
let if_decl_opt = let if_decl_opt =
CAst_utils.get_decl_opt_with_decl_ref impl_decl_info.oidi_class_interface in CAst_utils.get_decl_opt_with_decl_ref impl_decl_info.oidi_class_interface in
(match if_decl_opt with (match if_decl_opt with
@ -281,7 +281,7 @@ let rec _component_initializer_with_side_effects_advice
in_ck_class context in_ck_class context
&& context.in_objc_static_factory_method && context.in_objc_static_factory_method
&& (match context.current_objc_impl with && (match context.current_objc_impl with
| Some d -> is_in_main_file context.translation_unit_context (CTL.Decl d) | Some d -> is_in_main_file context.translation_unit_context (Ctl_parser_types.Decl d)
| None -> false) in | None -> false) in
if condition then if condition then
match call_stmt with match call_stmt with
@ -313,7 +313,7 @@ let rec _component_initializer_with_side_effects_advice
let component_initializer_with_side_effects_advice let component_initializer_with_side_effects_advice
(context: CLintersContext.context) an = (context: CLintersContext.context) an =
match an with match an with
| CTL.Stmt (CallExpr (_, called_func_stmt :: _, _)) -> | Ctl_parser_types.Stmt (CallExpr (_, called_func_stmt :: _, _)) ->
_component_initializer_with_side_effects_advice context called_func_stmt _component_initializer_with_side_effects_advice context called_func_stmt
| _ -> CTL.False, None (* only to be called in CallExpr *) | _ -> CTL.False, None (* only to be called in CallExpr *)
@ -324,7 +324,7 @@ let component_initializer_with_side_effects_advice
let component_file_line_count_info (context: CLintersContext.context) dec = let component_file_line_count_info (context: CLintersContext.context) dec =
let condition = Config.compute_analytics && context.is_ck_translation_unit in let condition = Config.compute_analytics && context.is_ck_translation_unit in
match dec with match dec with
| CTL.Decl Clang_ast_t.TranslationUnitDecl _ when condition -> | Ctl_parser_types.Decl Clang_ast_t.TranslationUnitDecl _ when condition ->
let source_file = let source_file =
context.translation_unit_context.CFrontend_config.source_file in context.translation_unit_context.CFrontend_config.source_file in
let line_count = SourceFile.line_count source_file in let line_count = SourceFile.line_count source_file in
@ -364,11 +364,11 @@ let component_file_cyclomatic_complexity_info (context: CLintersContext.context)
List.mem ~equal:(=) [`LAnd; `LOr] boi.Clang_ast_t.boi_kind List.mem ~equal:(=) [`LAnd; `LOr] boi.Clang_ast_t.boi_kind
| _ -> false in | _ -> false in
let cyclo_loc_opt an = match an with let cyclo_loc_opt an = match an with
| CTL.Stmt stmt when (Config.compute_analytics | Ctl_parser_types.Stmt stmt when (Config.compute_analytics
&& is_cyclo_stmt stmt && is_cyclo_stmt stmt
&& is_ck_context context an) -> && is_ck_context context an) ->
Some (CFrontend_checkers.location_from_stmt context stmt) Some (CFrontend_checkers.location_from_stmt context stmt)
| CTL.Decl (Clang_ast_t.TranslationUnitDecl _ as d) | Ctl_parser_types.Decl (Clang_ast_t.TranslationUnitDecl _ as d)
when Config.compute_analytics && context.is_ck_translation_unit -> when Config.compute_analytics && context.is_ck_translation_unit ->
Some (CFrontend_checkers.location_from_decl context d) Some (CFrontend_checkers.location_from_decl context d)
| _ -> None in | _ -> None in

14
infer/src/clang/ComponentKit.mli
Unescape View File

@ -17,22 +17,22 @@ open! IStd
val contains_ck_impl : Clang_ast_t.decl list -> bool val contains_ck_impl : Clang_ast_t.decl list -> bool
val mutable_local_vars_advice : val mutable_local_vars_advice :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc option
val component_factory_function_advice : val component_factory_function_advice :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc option
val component_with_unconventional_superclass_advice : val component_with_unconventional_superclass_advice :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc option
val component_with_multiple_factory_methods_advice : val component_with_multiple_factory_methods_advice :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc list CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc list
val component_initializer_with_side_effects_advice : val component_initializer_with_side_effects_advice :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc option
val component_file_line_count_info : val component_file_line_count_info :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc list CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc list
val component_file_cyclomatic_complexity_info : val component_file_cyclomatic_complexity_info :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option CLintersContext.context -> Ctl_parser_types.ast_node -> CTL.t * CIssue.issue_desc option

31
infer/src/clang/cFrontend_checkers.ml
Unescape View File

@ -37,12 +37,12 @@ let location_from_decl lctx dec =
let location_from_an lcxt an = let location_from_an lcxt an =
match an with match an with
| CTL.Stmt st -> location_from_stmt lcxt st | Ctl_parser_types.Stmt st -> location_from_stmt lcxt st
| CTL.Decl d -> location_from_decl lcxt d | Ctl_parser_types.Decl d -> location_from_decl lcxt d
let decl_name an = let decl_name an =
match an with match an with
| CTL.Decl dec -> | Ctl_parser_types.Decl dec ->
(match Clang_ast_proj.get_named_decl_tuple dec with (match Clang_ast_proj.get_named_decl_tuple dec with
| Some (_, n) -> n.Clang_ast_t.ni_name | Some (_, n) -> n.Clang_ast_t.ni_name
| None -> "") | None -> "")
@ -50,14 +50,14 @@ let decl_name an =
let tag_name_of_node an = let tag_name_of_node an =
match an with match an with
| CTL.Stmt stmt -> Clang_ast_proj.get_stmt_kind_string stmt | Ctl_parser_types.Stmt stmt -> Clang_ast_proj.get_stmt_kind_string stmt
| CTL.Decl decl -> Clang_ast_proj.get_decl_kind_string decl | Ctl_parser_types.Decl decl -> Clang_ast_proj.get_decl_kind_string decl
let decl_ref_or_selector_name an = let decl_ref_or_selector_name an =
match CTL.next_state_via_transition an (Some CTL.PointerToDecl) with match CTL.next_state_via_transition an (Some CTL.PointerToDecl) with
| Some (CTL.Decl ObjCMethodDecl _ as decl_an) -> | Some (Ctl_parser_types.Decl ObjCMethodDecl _ as decl_an) ->
"The selector " ^ (decl_name decl_an) "The selector " ^ (decl_name decl_an)
| Some (CTL.Decl _ as decl_an) -> | Some (Ctl_parser_types.Decl _ as decl_an) ->
"The reference " ^ (decl_name decl_an) "The reference " ^ (decl_name decl_an)
| _ -> failwith("decl_ref_or_selector_name must be called with a DeclRefExpr \ | _ -> failwith("decl_ref_or_selector_name must be called with a DeclRefExpr \
or an ObjCMessageExpr, but got " ^ (tag_name_of_node an)) or an ObjCMessageExpr, but got " ^ (tag_name_of_node an))
@ -68,9 +68,10 @@ let iphoneos_target_sdk_version _ =
| None -> "0" | None -> "0"
let available_ios_sdk an = let available_ios_sdk an =
let open Ctl_parser_types in
match CTL.next_state_via_transition an (Some CTL.PointerToDecl) with match CTL.next_state_via_transition an (Some CTL.PointerToDecl) with
| Some CTL.Decl decl -> | Some Decl decl ->
(match CPredicates.get_available_attr_ios_sdk decl with (match CPredicates.get_available_attr_ios_sdk (Decl decl) with
| Some version -> version | Some version -> version
| None -> "") | None -> "")
| _ -> failwith("available_ios_sdk must be called with a DeclRefExpr \ | _ -> failwith("available_ios_sdk must be called with a DeclRefExpr \
@ -79,7 +80,7 @@ let available_ios_sdk an =
let ivar_name an = let ivar_name an =
let open Clang_ast_t in let open Clang_ast_t in
match an with match an with
| CTL.Stmt (ObjCIvarRefExpr (_, _, _, rei)) -> | Ctl_parser_types.Stmt (ObjCIvarRefExpr (_, _, _, rei)) ->
let dr_ref = rei.ovrei_decl_ref in let dr_ref = rei.ovrei_decl_ref in
let ivar_pointer = dr_ref.dr_decl_pointer in let ivar_pointer = dr_ref.dr_decl_pointer in
(match CAst_utils.get_decl ivar_pointer with (match CAst_utils.get_decl ivar_pointer with
@ -89,11 +90,13 @@ let ivar_name an =
| _ -> "" | _ -> ""
let cxx_ref_captured_in_block an = let cxx_ref_captured_in_block an =
let open Ctl_parser_types in
let open Clang_ast_t in
let capt_refs = match an with let capt_refs = match an with
| CTL.Decl d -> CPredicates.captured_variables_cxx_ref d | Decl _ -> CPredicates.captured_variables_cxx_ref an
| CTL.Stmt (Clang_ast_t.BlockExpr(_, _, _, d)) -> | Stmt (BlockExpr(_, _, _, d)) ->
CPredicates.captured_variables_cxx_ref d CPredicates.captured_variables_cxx_ref (Decl d)
| _ -> [] in | _ -> [] in
let var_desc vars var_named_decl_info = let var_desc vars var_named_decl_info =
vars ^ "'" ^ var_named_decl_info.Clang_ast_t.ni_name ^ "'" in vars ^ "'" ^ var_named_decl_info.ni_name ^ "'" in
IList.fold_left var_desc "" capt_refs IList.fold_left var_desc "" capt_refs

16
infer/src/clang/cFrontend_checkers.mli
Unescape View File

@ -16,21 +16,21 @@ val location_from_dinfo :
CLintersContext.context -> Clang_ast_t.decl_info -> Location.t CLintersContext.context -> Clang_ast_t.decl_info -> Location.t
val location_from_an : val location_from_an :
CLintersContext.context -> CTL.ast_node -> Location.t CLintersContext.context -> Ctl_parser_types.ast_node -> Location.t
val location_from_decl : val location_from_decl :
CLintersContext.context -> Clang_ast_t.decl -> Location.t CLintersContext.context -> Clang_ast_t.decl -> Location.t
val decl_name : CTL.ast_node -> string val decl_name : Ctl_parser_types.ast_node -> string
val ivar_name : CTL.ast_node -> string val ivar_name : Ctl_parser_types.ast_node -> string
val cxx_ref_captured_in_block : CTL.ast_node -> string val cxx_ref_captured_in_block : Ctl_parser_types.ast_node -> string
val decl_ref_or_selector_name : CTL.ast_node -> string val decl_ref_or_selector_name : Ctl_parser_types.ast_node -> string
val iphoneos_target_sdk_version : CTL.ast_node -> string val iphoneos_target_sdk_version : Ctl_parser_types.ast_node -> string
val available_ios_sdk : CTL.ast_node -> string val available_ios_sdk : Ctl_parser_types.ast_node -> string
val tag_name_of_node : CTL.ast_node -> string val tag_name_of_node : Ctl_parser_types.ast_node -> string

8
infer/src/clang/cFrontend_checkers_main.ml
Unescape View File

@ -36,7 +36,7 @@ let parse_ctl_file linters_files =
Logging.out "#### Start Expanding checkers #####\n"; Logging.out "#### Start Expanding checkers #####\n";
let exp_checkers = CFrontend_errors.expand_checkers parsed_checkers in let exp_checkers = CFrontend_errors.expand_checkers parsed_checkers in
Logging.out "#### Checkers Expanded #####\n"; Logging.out "#### Checkers Expanded #####\n";
if Config.debug_mode then IList.iter Ctl_parser_types.print_checker exp_checkers; if Config.debug_mode then IList.iter CTL.print_checker exp_checkers;
CFrontend_errors.make_condition_issue_desc_pair exp_checkers; CFrontend_errors.make_condition_issue_desc_pair exp_checkers;
| None -> Logging.out "No linters found.\n"); | None -> Logging.out "No linters found.\n");
In_channel.close inx) linters_files In_channel.close inx) linters_files
@ -84,7 +84,7 @@ let rec do_frontend_checks_stmt (context:CLintersContext.context) stmt =
IList.iter (do_frontend_checks_decl context) [decl] IList.iter (do_frontend_checks_decl context) [decl]
| _ -> ()); | _ -> ());
do_frontend_checks_stmt context stmt in do_frontend_checks_stmt context stmt in
CFrontend_errors.invoke_set_of_checkers_on_node context (CTL.Stmt stmt); CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Stmt stmt);
match stmt with match stmt with
| ObjCAtSynchronizedStmt (_, stmt_list) -> | ObjCAtSynchronizedStmt (_, stmt_list) ->
let stmt_context = { context with CLintersContext.in_synchronized_block = true } in let stmt_context = { context with CLintersContext.in_synchronized_block = true } in
@ -104,7 +104,7 @@ let rec do_frontend_checks_stmt (context:CLintersContext.context) stmt =
and do_frontend_checks_decl (context: CLintersContext.context) decl = and do_frontend_checks_decl (context: CLintersContext.context) decl =
let open Clang_ast_t in let open Clang_ast_t in
CFrontend_errors.invoke_set_of_checkers_on_node context (CTL.Decl decl); CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl decl);
match decl with match decl with
| FunctionDecl(_, _, _, fdi) | FunctionDecl(_, _, _, fdi)
| CXXMethodDecl (_, _, _, fdi, _) | CXXMethodDecl (_, _, _, fdi, _)
@ -166,7 +166,7 @@ let do_frontend_checks trans_unit_ctx ast =
CLocation.should_do_frontend_check trans_unit_ctx decl_info.Clang_ast_t.di_source_range in CLocation.should_do_frontend_check trans_unit_ctx decl_info.Clang_ast_t.di_source_range in
let allowed_decls = IList.filter is_decl_allowed decl_list in let allowed_decls = IList.filter is_decl_allowed decl_list in
(* We analyze the top level and then all the allowed declarations *) (* We analyze the top level and then all the allowed declarations *)
CFrontend_errors.invoke_set_of_checkers_on_node context (CTL.Decl ast); CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl ast);
IList.iter (do_frontend_checks_decl context) allowed_decls; IList.iter (do_frontend_checks_decl context) allowed_decls;
if (LintIssues.exists_issues ()) then if (LintIssues.exists_issues ()) then
store_issues source_file; store_issues source_file;

37
infer/src/clang/cFrontend_errors.ml
Unescape View File

@ -91,11 +91,12 @@ let string_to_issue_mode m =
(** Convert a parsed checker in a pair (condition, issue_desc) *) (** Convert a parsed checker in a pair (condition, issue_desc) *)
let make_condition_issue_desc_pair checkers = let make_condition_issue_desc_pair checkers =
let open CIssue in let open CIssue in
let open CTL in
let open Ctl_parser_types in let open Ctl_parser_types in
Logging.out "\n Converting checkers in (condition, issue) pairs\n"; Logging.out "\n Converting checkers in (condition, issue) pairs\n";
let do_one_checker c = let do_one_checker c =
let dummy_issue = { let dummy_issue = {
name = c.Ctl_parser_types.name; name = c.name;
description = ""; description = "";
suggestion = None; suggestion = None;
loc = Location.dummy; loc = Location.dummy;
@ -114,10 +115,10 @@ let make_condition_issue_desc_pair checkers =
{issue' with severity = string_to_err_kind sev}, cond' {issue' with severity = string_to_err_kind sev}, cond'
| CDesc (s, m) when String.equal s mode_const -> | CDesc (s, m) when String.equal s mode_const ->
{issue' with mode = string_to_issue_mode m }, cond' {issue' with mode = string_to_issue_mode m }, cond'
| _ -> issue', cond') (dummy_issue, CTL.False) c.Ctl_parser_types.definitions in | _ -> issue', cond') (dummy_issue, CTL.False) c.definitions in
if Config.debug_mode then ( if Config.debug_mode then (
Logging.out "\nMaking condition and issue desc for checker '%s'\n" Logging.out "\nMaking condition and issue desc for checker '%s'\n"
c.Ctl_parser_types.name; c.name;
Logging.out "\nCondition =\n %a\n" CTL.Debug.pp_formula condition; Logging.out "\nCondition =\n %a\n" CTL.Debug.pp_formula condition;
Logging.out "\nIssue_desc = %a\n" CIssue.pp_issue issue); Logging.out "\nIssue_desc = %a\n" CIssue.pp_issue issue);
condition, issue in condition, issue in
@ -160,7 +161,7 @@ let expand_checkers checkers =
let map : CTL.t Core.Std.String.Map.t = Core.Std.String.Map.empty in let map : CTL.t Core.Std.String.Map.t = Core.Std.String.Map.empty in
let map = IList.fold_left (fun map' d -> match d with let map = IList.fold_left (fun map' d -> match d with
| CLet (k,formula) -> Core.Std.Map.add map' ~key:k ~data:formula | CLet (k,formula) -> Core.Std.Map.add map' ~key:k ~data:formula
| _ -> map') map c.Ctl_parser_types.definitions in | _ -> map') map c.definitions in
let exp_defs = IList.fold_left (fun defs clause -> let exp_defs = IList.fold_left (fun defs clause ->
match clause with match clause with
| CSet (report_when_const, phi) -> | CSet (report_when_const, phi) ->
@ -192,15 +193,15 @@ let log_frontend_issue translation_unit_context method_decl_opt key issue_desc =
Reporting.log_issue_from_errlog err_kind errlog exn ~loc ~ltr:trace Reporting.log_issue_from_errlog err_kind errlog exn ~loc ~ltr:trace
~node_id:(0, key) ~node_id:(0, key)
let get_current_method context an = let get_current_method context (an : Ctl_parser_types.ast_node) =
match an with match an with
| CTL.Decl (FunctionDecl _ as d) | Decl (FunctionDecl _ as d)
| CTL.Decl (CXXMethodDecl _ as d) | Decl (CXXMethodDecl _ as d)
| CTL.Decl (CXXConstructorDecl _ as d) | Decl (CXXConstructorDecl _ as d)
| CTL.Decl (CXXConversionDecl _ as d) | Decl (CXXConversionDecl _ as d)
| CTL.Decl (CXXDestructorDecl _ as d) | Decl (CXXDestructorDecl _ as d)
| CTL.Decl (ObjCMethodDecl _ as d) | Decl (ObjCMethodDecl _ as d)
| CTL.Decl (BlockDecl _ as d) -> Some d | Decl (BlockDecl _ as d) -> Some d
| _ -> context.CLintersContext.current_method | _ -> context.CLintersContext.current_method
let fill_issue_desc_info_and_log context an key issue_desc loc = let fill_issue_desc_info_and_log context an key issue_desc loc =
@ -211,10 +212,10 @@ let fill_issue_desc_info_and_log context an key issue_desc loc =
(get_current_method context an) key issue_desc' (get_current_method context an) key issue_desc'
(* Calls the set of hard coded checkers (if any) *) (* Calls the set of hard coded checkers (if any) *)
let invoke_set_of_hard_coded_checkers_an context an = let invoke_set_of_hard_coded_checkers_an context (an : Ctl_parser_types.ast_node) =
let checkers, key = match an with let checkers, key = match an with
| CTL.Decl dec -> decl_checkers_list, CAst_utils.generate_key_decl dec | Decl dec -> decl_checkers_list, CAst_utils.generate_key_decl dec
| CTL.Stmt st -> stmt_checkers_list, CAst_utils.generate_key_stmt st in | Stmt st -> stmt_checkers_list, CAst_utils.generate_key_stmt st in
IList.iter (fun checker -> IList.iter (fun checker ->
let condition, issue_desc_list = checker context an in let condition, issue_desc_list = checker context an in
if CTL.eval_formula condition an context then if CTL.eval_formula condition an context then
@ -226,10 +227,10 @@ let invoke_set_of_hard_coded_checkers_an context an =
) checkers ) checkers
(* Calls the set of checkers parsed from files (if any) *) (* Calls the set of checkers parsed from files (if any) *)
let invoke_set_of_parsed_checkers_an context an = let invoke_set_of_parsed_checkers_an context (an : Ctl_parser_types.ast_node) =
let key = match an with let key = match an with
| CTL.Decl dec -> CAst_utils.generate_key_decl dec | Decl dec -> CAst_utils.generate_key_decl dec
| CTL.Stmt st -> CAst_utils.generate_key_stmt st in | Stmt st -> CAst_utils.generate_key_stmt st in
IList.iter (fun (condition, issue_desc) -> IList.iter (fun (condition, issue_desc) ->
if CIssue.should_run_check issue_desc.CIssue.mode && if CIssue.should_run_check issue_desc.CIssue.mode &&
CTL.eval_formula condition an context then CTL.eval_formula condition an context then

6
infer/src/clang/cFrontend_errors.mli
Unescape View File

@ -13,9 +13,9 @@ open! IStd
(* Module for warnings detected at translation time by the frontend *) (* Module for warnings detected at translation time by the frontend *)
(* Run frontend checkers on an AST node *) (* Run frontend checkers on an AST node *)
val invoke_set_of_checkers_on_node : CLintersContext.context -> CTL.ast_node -> unit val invoke_set_of_checkers_on_node : CLintersContext.context -> Ctl_parser_types.ast_node -> unit
val expand_checkers : Ctl_parser_types.ctl_checker list -> Ctl_parser_types.ctl_checker list val expand_checkers : CTL.ctl_checker list -> CTL.ctl_checker list
val make_condition_issue_desc_pair : val make_condition_issue_desc_pair :
Ctl_parser_types.ctl_checker list -> unit CTL.ctl_checker list -> unit

155
infer/src/clang/cPredicates.ml
Unescape View File

@ -9,20 +9,23 @@
open! IStd open! IStd
let get_available_attr_ios_sdk decl = let get_available_attr_ios_sdk an =
let open Clang_ast_t in let open Clang_ast_t in
let decl_info = Clang_ast_proj.get_decl_tuple decl in
let rec get_available_attr attrs = let rec get_available_attr attrs =
match attrs with match attrs with
| [] -> None | [] -> None
| AvailabilityAttr attr_info :: _ -> | AvailabilityAttr attr_info :: _ ->
(match attr_info.Clang_ast_t.ai_parameters with (match attr_info.ai_parameters with
| "ios" :: version :: _ -> | "ios" :: version :: _ ->
Some (String.Search_pattern.replace_all Some (String.Search_pattern.replace_all
(String.Search_pattern.create "_") ~in_:version ~with_:".") (String.Search_pattern.create "_") ~in_:version ~with_:".")
| _ -> None) | _ -> None)
| _ :: rest -> get_available_attr rest in | _ :: rest -> get_available_attr rest in
get_available_attr decl_info.Clang_ast_t.di_attributes match an with
| Ctl_parser_types.Decl decl ->
let decl_info = Clang_ast_proj.get_decl_tuple decl in
get_available_attr decl_info.di_attributes
| _ -> None
let get_ivar_attributes ivar_decl = let get_ivar_attributes ivar_decl =
let open Clang_ast_t in let open Clang_ast_t in
@ -35,7 +38,8 @@ let get_ivar_attributes ivar_decl =
| _ -> [] | _ -> []
(* list of cxx references captured by decl *) (* list of cxx references captured by decl *)
let captured_variables_cxx_ref dec = let captured_variables_cxx_ref an =
let open Clang_ast_t in
let capture_var_is_cxx_ref reference_captured_vars captured_var = let capture_var_is_cxx_ref reference_captured_vars captured_var =
let decl_ref_opt = captured_var.Clang_ast_t.bcv_variable in let decl_ref_opt = captured_var.Clang_ast_t.bcv_variable in
match CAst_utils.get_decl_opt_with_decl_ref decl_ref_opt with match CAst_utils.get_decl_opt_with_decl_ref decl_ref_opt with
@ -47,11 +51,11 @@ let captured_variables_cxx_ref dec =
named_decl_info::reference_captured_vars named_decl_info::reference_captured_vars
| _ -> reference_captured_vars) | _ -> reference_captured_vars)
| _ -> reference_captured_vars in | _ -> reference_captured_vars in
let captured_vars = match dec with match an with
| Clang_ast_t.BlockDecl (_, bdi) -> | Ctl_parser_types.Decl (BlockDecl (_, bdi)) ->
bdi.Clang_ast_t.bdi_captured_variables IList.fold_left capture_var_is_cxx_ref [] bdi.bdi_captured_variables
| _ -> [] in | _ -> []
IList.fold_left capture_var_is_cxx_ref [] captured_vars
@ -64,28 +68,36 @@ let is_declaration_kind decl s =
String.equal (Clang_ast_proj.get_decl_kind_string decl) s String.equal (Clang_ast_proj.get_decl_kind_string decl) s
(* st |= call_method(m) *) (* st |= call_method(m) *)
let call_method m st = let call_method m an =
match st with match an with
| Clang_ast_t.ObjCMessageExpr (_, _, _, omei) -> String.equal omei.omei_selector m | Ctl_parser_types.Stmt (Clang_ast_t.ObjCMessageExpr (_, _, _, omei)) ->
String.equal omei.omei_selector m
| _ -> false | _ -> false
let property_name_contains_word word decl = let property_name_contains_word word an =
match Clang_ast_proj.get_named_decl_tuple decl with match an with
| Some (_, n) -> let pname = n.Clang_ast_t.ni_name in | Ctl_parser_types.Decl decl ->
let rexp = Str.regexp_string_case_fold word in (match Clang_ast_proj.get_named_decl_tuple decl with
(try | Some (_, n) -> let pname = n.Clang_ast_t.ni_name in
Str.search_forward rexp pname 0 >= 0 let rexp = Str.regexp_string_case_fold word in
with Not_found -> false) (try
Str.search_forward rexp pname 0 >= 0
with Not_found -> false)
| _ -> false)
| _ -> false | _ -> false
let is_objc_extension lcxt = let is_objc_extension lcxt =
CGeneral_utils.is_objc_extension lcxt.CLintersContext.translation_unit_context CGeneral_utils.is_objc_extension lcxt.CLintersContext.translation_unit_context
let is_syntactically_global_var decl = let is_syntactically_global_var an =
CAst_utils.is_syntactically_global_var decl match an with
| Ctl_parser_types.Decl d -> CAst_utils.is_syntactically_global_var d
| _ -> false
let is_const_expr_var decl = let is_const_expr_var an =
CAst_utils.is_const_expr_var decl match an with
| Ctl_parser_types.Decl d -> CAst_utils.is_const_expr_var d
| _ -> false
let decl_ref_is_in names st = let decl_ref_is_in names st =
match st with match st with
@ -96,25 +108,28 @@ let decl_ref_is_in names st =
| _ -> false) | _ -> false)
| _ -> false | _ -> false
let call_function_named names st = let call_function_named names an =
CAst_utils.exists_eventually_st decl_ref_is_in names st match an with
| Ctl_parser_types.Stmt st ->
CAst_utils.exists_eventually_st decl_ref_is_in names st
| _ -> false
let is_strong_property decl = let is_strong_property an =
match decl with match an with
| Clang_ast_t.ObjCPropertyDecl (_, _, pdi) -> | Ctl_parser_types.Decl (Clang_ast_t.ObjCPropertyDecl (_, _, pdi)) ->
ObjcProperty_decl.is_strong_property pdi ObjcProperty_decl.is_strong_property pdi
| _ -> false | _ -> false
let is_assign_property decl = let is_assign_property an =
match decl with match an with
| Clang_ast_t.ObjCPropertyDecl (_, _, pdi) -> | Ctl_parser_types.Decl (Clang_ast_t.ObjCPropertyDecl (_, _, pdi)) ->
ObjcProperty_decl.is_assign_property pdi ObjcProperty_decl.is_assign_property pdi
| _ -> false | _ -> false
let is_property_pointer_type decl = let is_property_pointer_type an =
let open Clang_ast_t in let open Clang_ast_t in
match decl with match an with
| ObjCPropertyDecl (_, _, pdi) -> | Ctl_parser_types.Decl (ObjCPropertyDecl (_, _, pdi)) ->
(match CAst_utils.get_desugared_type pdi.opdi_type_ptr with (match CAst_utils.get_desugared_type pdi.opdi_type_ptr with
| Some MemberPointerType _ | Some MemberPointerType _
| Some ObjCObjectPointerType _ | Some ObjCObjectPointerType _
@ -129,9 +144,9 @@ let context_in_synchronized_block context =
context.CLintersContext.in_synchronized_block context.CLintersContext.in_synchronized_block
(* checks if ivar is defined among a set of fields and if it is atomic *) (* checks if ivar is defined among a set of fields and if it is atomic *)
let is_ivar_atomic stmt = let is_ivar_atomic an =
match stmt with match an with
| Clang_ast_t.ObjCIvarRefExpr (_, _, _, irei) -> | Ctl_parser_types.Stmt (Clang_ast_t.ObjCIvarRefExpr (_, _, _, irei)) ->
let dr_ref = irei.Clang_ast_t.ovrei_decl_ref in let dr_ref = irei.Clang_ast_t.ovrei_decl_ref in
let ivar_pointer = dr_ref.Clang_ast_t.dr_decl_pointer in let ivar_pointer = dr_ref.Clang_ast_t.dr_decl_pointer in
(match CAst_utils.get_decl ivar_pointer with (match CAst_utils.get_decl ivar_pointer with
@ -141,10 +156,10 @@ let is_ivar_atomic stmt =
| _ -> false) | _ -> false)
| _ -> false | _ -> false
let is_method_property_accessor_of_ivar stmt context = let is_method_property_accessor_of_ivar an context =
let open Clang_ast_t in let open Clang_ast_t in
match stmt with match an with
| ObjCIvarRefExpr (_, _, _, irei) -> | Ctl_parser_types.Stmt (ObjCIvarRefExpr (_, _, _, irei)) ->
let dr_ref = irei.Clang_ast_t.ovrei_decl_ref in let dr_ref = irei.Clang_ast_t.ovrei_decl_ref in
let ivar_pointer = dr_ref.Clang_ast_t.dr_decl_pointer in let ivar_pointer = dr_ref.Clang_ast_t.dr_decl_pointer in
(match context.CLintersContext.current_method with (match context.CLintersContext.current_method with
@ -180,56 +195,58 @@ let is_objc_dealloc context =
Procname.is_objc_dealloc method_name Procname.is_objc_dealloc method_name
| _ -> false | _ -> false
let captures_cxx_references decl = let captures_cxx_references an =
IList.length (captured_variables_cxx_ref decl) > 0 IList.length (captured_variables_cxx_ref an) > 0
let is_binop_with_kind str_kind stmt = let is_binop_with_kind str_kind an =
if not (Clang_ast_proj.is_valid_binop_kind_name str_kind) then if not (Clang_ast_proj.is_valid_binop_kind_name str_kind) then
failwith ("Binary operator kind " ^ str_kind ^ " is not valid"); failwith ("Binary operator kind " ^ str_kind ^ " is not valid");
match stmt with match an with
| Clang_ast_t.BinaryOperator (_, _, _, boi) -> | Ctl_parser_types.Stmt (Clang_ast_t.BinaryOperator (_, _, _, boi)) ->
String.equal (Clang_ast_proj.string_of_binop_kind boi.boi_kind) str_kind String.equal (Clang_ast_proj.string_of_binop_kind boi.boi_kind) str_kind
| _ -> false | _ -> false
let is_unop_with_kind str_kind stmt = let is_unop_with_kind str_kind an =
if not (Clang_ast_proj.is_valid_unop_kind_name str_kind) then if not (Clang_ast_proj.is_valid_unop_kind_name str_kind) then
failwith ("Unary operator kind " ^ str_kind ^ " is not valid"); failwith ("Unary operator kind " ^ str_kind ^ " is not valid");
match stmt with match an with
| Clang_ast_t.UnaryOperator (_, _, _, uoi) -> | Ctl_parser_types.Stmt (Clang_ast_t.UnaryOperator (_, _, _, uoi)) ->
String.equal (Clang_ast_proj.string_of_unop_kind uoi.uoi_kind) str_kind String.equal (Clang_ast_proj.string_of_unop_kind uoi.uoi_kind) str_kind
| _ -> false | _ -> false
let is_stmt nodename stmt = let is_node nodename an =
if not (Clang_ast_proj.is_valid_astnode_kind nodename) then
failwith ("Statement " ^ nodename ^ " is not a valid statement");
String.equal nodename (Clang_ast_proj.get_stmt_kind_string stmt)
let is_decl nodename decl =
if not (Clang_ast_proj.is_valid_astnode_kind nodename) then if not (Clang_ast_proj.is_valid_astnode_kind nodename) then
failwith ("Declaration " ^ nodename ^ " is not a valid declaration"); failwith ("Node " ^ nodename ^ " is not a valid AST node");
String.equal nodename (Clang_ast_proj.get_decl_kind_string decl) let an_str = match an with
| Ctl_parser_types.Stmt s -> Clang_ast_proj.get_stmt_kind_string s
let isa classname stmt = | Ctl_parser_types.Decl d -> Clang_ast_proj.get_decl_kind_string d in
match Clang_ast_proj.get_expr_tuple stmt with String.equal nodename an_str
| Some (_, _, expr_info) ->
let typ = CAst_utils.get_desugared_type expr_info.ei_type_ptr in let isa classname an =
CAst_utils.is_ptr_to_objc_class typ classname match an with
| Ctl_parser_types.Stmt stmt ->
(match Clang_ast_proj.get_expr_tuple stmt with
| Some (_, _, expr_info) ->
let typ = CAst_utils.get_desugared_type expr_info.ei_type_ptr in
CAst_utils.is_ptr_to_objc_class typ classname
| _ -> false)
| _ -> false | _ -> false
let decl_unavailable_in_supported_ios_sdk decl = let decl_unavailable_in_supported_ios_sdk an =
let available_attr_ios_sdk = get_available_attr_ios_sdk decl in let available_attr_ios_sdk = get_available_attr_ios_sdk an in
match available_attr_ios_sdk, Config.iphoneos_target_sdk_version with match available_attr_ios_sdk, Config.iphoneos_target_sdk_version with
| Some available_attr_ios_sdk, Some iphoneos_target_sdk_version -> | Some available_attr_ios_sdk, Some iphoneos_target_sdk_version ->
Int.equal (Utils.compare_versions available_attr_ios_sdk iphoneos_target_sdk_version) 1 Int.equal (Utils.compare_versions available_attr_ios_sdk iphoneos_target_sdk_version) 1
| _ -> false | _ -> false
let within_responds_to_selector_block (cxt:CLintersContext.context) decl =
let within_responds_to_selector_block (cxt:CLintersContext.context) an =
let open Clang_ast_t in let open Clang_ast_t in
match decl with match an with
| ObjCMethodDecl (_, named_decl_info, _) -> | Ctl_parser_types.Decl (ObjCMethodDecl (_, named_decl_info, _)) ->
(match cxt.if_context with (match cxt.if_context with
| Some if_context -> | Some if_context ->
let in_selector_block = if_context.within_responds_to_selector_block in let in_selector_block = if_context.within_responds_to_selector_block in
List.mem ~equal:String.equal in_selector_block named_decl_info.Clang_ast_t.ni_name List.mem ~equal:String.equal in_selector_block named_decl_info.ni_name
| None -> false) | None -> false)
| _ -> false | _ -> false

40
infer/src/clang/cPredicates.mli
Unescape View File

@ -11,52 +11,50 @@ open! IStd
type t = string * string list (* (name, [param1,...,paramK]) *) type t = string * string list (* (name, [param1,...,paramK]) *)
val captured_variables_cxx_ref : Clang_ast_t.decl -> Clang_ast_t.named_decl_info list val captured_variables_cxx_ref : Ctl_parser_types.ast_node -> Clang_ast_t.named_decl_info list
val call_method : string -> Clang_ast_t.stmt -> bool val call_method : string -> Ctl_parser_types.ast_node -> bool
val property_name_contains_word : string -> Clang_ast_t.decl -> bool val property_name_contains_word : string -> Ctl_parser_types.ast_node -> bool
val is_objc_extension : CLintersContext.context -> bool val is_objc_extension : CLintersContext.context -> bool
val is_syntactically_global_var : Clang_ast_t.decl -> bool val is_syntactically_global_var : Ctl_parser_types.ast_node -> bool
val is_const_expr_var : Clang_ast_t.decl -> bool val is_const_expr_var : Ctl_parser_types.ast_node -> bool
val call_function_named : string list -> Clang_ast_t.stmt -> bool val call_function_named : string list -> Ctl_parser_types.ast_node -> bool
val is_strong_property : Clang_ast_t.decl -> bool val is_strong_property : Ctl_parser_types.ast_node -> bool
val is_assign_property : Clang_ast_t.decl -> bool val is_assign_property : Ctl_parser_types.ast_node -> bool
val is_property_pointer_type : Clang_ast_t.decl -> bool val is_property_pointer_type : Ctl_parser_types.ast_node -> bool
val context_in_synchronized_block : CLintersContext.context -> bool val context_in_synchronized_block : CLintersContext.context -> bool
val is_ivar_atomic : Clang_ast_t.stmt -> bool val is_ivar_atomic : Ctl_parser_types.ast_node -> bool
val is_method_property_accessor_of_ivar : Clang_ast_t.stmt -> CLintersContext.context -> bool val is_method_property_accessor_of_ivar : Ctl_parser_types.ast_node -> CLintersContext.context -> bool
val is_objc_constructor : CLintersContext.context -> bool val is_objc_constructor : CLintersContext.context -> bool
val is_objc_dealloc : CLintersContext.context -> bool val is_objc_dealloc : CLintersContext.context -> bool
val captures_cxx_references : Clang_ast_t.decl -> bool val captures_cxx_references : Ctl_parser_types.ast_node -> bool
val is_binop_with_kind : string -> Clang_ast_t.stmt -> bool val is_binop_with_kind : string -> Ctl_parser_types.ast_node -> bool
val is_unop_with_kind : string -> Clang_ast_t.stmt -> bool val is_unop_with_kind : string -> Ctl_parser_types.ast_node -> bool
val isa : string -> Clang_ast_t.stmt -> bool val isa : string -> Ctl_parser_types.ast_node -> bool
val is_stmt : string -> Clang_ast_t.stmt -> bool val is_node : string -> Ctl_parser_types.ast_node -> bool
val is_decl : string -> Clang_ast_t.decl -> bool
val pp_predicate : Format.formatter -> t -> unit val pp_predicate : Format.formatter -> t -> unit
val decl_unavailable_in_supported_ios_sdk : Clang_ast_t.decl -> bool val decl_unavailable_in_supported_ios_sdk : Ctl_parser_types.ast_node -> bool
val get_available_attr_ios_sdk : Clang_ast_t.decl -> string option val get_available_attr_ios_sdk : Ctl_parser_types.ast_node -> string option
val within_responds_to_selector_block : CLintersContext.context -> Clang_ast_t.decl -> bool val within_responds_to_selector_block : CLintersContext.context -> Ctl_parser_types.ast_node -> bool

104
infer/src/clang/cTL.ml
Unescape View File

@ -8,13 +8,13 @@
*) *)
open! IStd open! IStd
open Ctl_parser_types
(* This module defines a language to define checkers. These checkers (* This module defines a language to define checkers. These checkers
are intepreted over the AST of the program. A checker is defined by a are intepreted over the AST of the program. A checker is defined by a
CTL formula which express a condition saying when the checker should CTL formula which express a condition saying when the checker should
report a problem *) report a problem *)
(* Transition labels used for example to switch from decl to stmt *) (* Transition labels used for example to switch from decl to stmt *)
type transitions = type transitions =
| Body (** decl to stmt *) | Body (** decl to stmt *)
@ -48,10 +48,31 @@ type t = (* A ctl formula *)
| ET of string list * transitions option * t | ET of string list * transitions option * t
| ETX of string list * transitions option * t | ETX of string list * transitions option * t
(* the kind of AST nodes where formulas are evaluated *) (* "set" clauses are used for defining mandatory variables that will be used
type ast_node = by when reporting issues: eg for defining the condition.
| Stmt of Clang_ast_t.stmt
| Decl of Clang_ast_t.decl "desc" clauses are used for defining the error message,
the suggestion, the severity.
"let" clauses are used to define temporary formulas which are then
used to abbreviate the another formula. For example
let f = a And B
set formula = f OR f
set message = "bla"
*)
type clause =
| CLet of string * t (* Let clause: let id = definifion; *)
| CSet of string * t (* Set clause: set id = definition *)
| CDesc of string * string (* Description clause eg: set message = "..." *)
type ctl_checker = {
name : string; (* Checker's name *)
definitions : clause list (* A list of let/set definitions *)
}
let equal_ast_node = Poly.(=) let equal_ast_node = Poly.(=)
@ -231,6 +252,20 @@ module Debug = struct
end end
end end
let print_checker c =
Logging.out "\n-------------------- \n";
Logging.out "\nChecker name: %s\n" c.name;
IList.iter (fun d -> (match d with
| CSet (clause_name, phi)
| CLet (clause_name, phi) ->
Logging.out " %s= \n %a\n\n"
clause_name Debug.pp_formula phi
| CDesc (clause_name, s) ->
Logging.out " %s= \n %s\n\n" clause_name s)
) c.definitions;
Logging.out "\n-------------------- \n"
let ctl_evaluation_tracker = match Config.debug_mode with let ctl_evaluation_tracker = match Config.debug_mode with
| true -> Some (ref (Debug.EvaluationTracker.create ())) | true -> Some (ref (Debug.EvaluationTracker.create ()))
| false -> None | false -> None
@ -377,49 +412,30 @@ let next_state_via_transition an trans =
linter context lcxt. That is: an, lcxt |= pred_name(params) *) linter context lcxt. That is: an, lcxt |= pred_name(params) *)
let rec eval_Atomic pred_name args an lcxt = let rec eval_Atomic pred_name args an lcxt =
match pred_name, args, an with match pred_name, args, an with
| "call_method", [m], Stmt st -> CPredicates.call_method m st | "call_method", [m], an -> CPredicates.call_method m an
(* Note: I think it should be better to change all predicated to be | "property_name_contains_word", [word], an -> CPredicates.property_name_contains_word word an
evaluated in a node an. The predicate itself should decide if it's a
stmt or decl predicate and return false for an unappropriate node *)
| "call_method", _, Decl _ -> false
| "property_name_contains_word", [word], Decl d -> CPredicates.property_name_contains_word word d
| "property_name_contains_word", _, Stmt _ -> false
| "is_objc_extension", [], _ -> CPredicates.is_objc_extension lcxt | "is_objc_extension", [], _ -> CPredicates.is_objc_extension lcxt
| "is_global_var", [], Decl d -> CPredicates.is_syntactically_global_var d | "is_global_var", [], an -> CPredicates.is_syntactically_global_var an
| "is_global_var", _, Stmt _ -> false | "is_const_var", [], an -> CPredicates.is_const_expr_var an
| "is_const_var", [], Decl d -> CPredicates.is_const_expr_var d | "call_function_named", args, an -> CPredicates.call_function_named args an
| "is_const_var", _, Stmt _ -> false | "is_strong_property", [], an -> CPredicates.is_strong_property an
| "call_function_named", args, Stmt st -> CPredicates.call_function_named args st | "is_assign_property", [], an -> CPredicates.is_assign_property an
| "call_function_named", _, Decl _ -> false | "is_property_pointer_type", [], an -> CPredicates.is_property_pointer_type an
| "is_strong_property", [], Decl d -> CPredicates.is_strong_property d
| "is_strong_property", _, Stmt _ -> false
| "is_assign_property", [], Decl d -> CPredicates.is_assign_property d
| "is_assign_property", _, Stmt _ -> false
| "is_property_pointer_type", [], Decl d -> CPredicates.is_property_pointer_type d
| "is_property_pointer_type", _, Stmt _ -> false
| "context_in_synchronized_block", [], _ -> CPredicates.context_in_synchronized_block lcxt | "context_in_synchronized_block", [], _ -> CPredicates.context_in_synchronized_block lcxt
| "is_ivar_atomic", [], Stmt st -> CPredicates.is_ivar_atomic st | "is_ivar_atomic", [], an -> CPredicates.is_ivar_atomic an
| "is_ivar_atomic", _, Decl _ -> false | "is_method_property_accessor_of_ivar", [], an ->
| "is_method_property_accessor_of_ivar", [], Stmt st -> CPredicates.is_method_property_accessor_of_ivar an lcxt
CPredicates.is_method_property_accessor_of_ivar st lcxt
| "is_method_property_accessor_of_ivar", _, Decl _ -> false
| "is_objc_constructor", [], _ -> CPredicates.is_objc_constructor lcxt | "is_objc_constructor", [], _ -> CPredicates.is_objc_constructor lcxt
| "is_objc_dealloc", [], _ -> CPredicates.is_objc_dealloc lcxt | "is_objc_dealloc", [], _ -> CPredicates.is_objc_dealloc lcxt
| "captures_cxx_references", [], Decl d -> CPredicates.captures_cxx_references d | "captures_cxx_references", [], _ -> CPredicates.captures_cxx_references an
| "captures_cxx_references", _, Stmt _ -> false | "is_binop_with_kind", [str_kind], an -> CPredicates.is_binop_with_kind str_kind an
| "is_binop_with_kind", [str_kind], Stmt st -> CPredicates.is_binop_with_kind str_kind st | "is_unop_with_kind", [str_kind], an -> CPredicates.is_unop_with_kind str_kind an
| "is_binop_with_kind", _, Decl _ -> false | "in_node", [nodename], an -> CPredicates.is_node nodename an
| "is_unop_with_kind", [str_kind], Stmt st -> CPredicates.is_unop_with_kind str_kind st | "isa", [classname], an -> CPredicates.isa classname an
| "is_unop_with_kind", _, Decl _ -> false | "decl_unavailable_in_supported_ios_sdk", [], an ->
| "in_node", [nodename], Stmt st -> CPredicates.is_stmt nodename st CPredicates.decl_unavailable_in_supported_ios_sdk an
| "in_node", [nodename], Decl d -> CPredicates.is_decl nodename d | "within_responds_to_selector_block", [], an ->
| "isa", [classname], Stmt st -> CPredicates.isa classname st CPredicates.within_responds_to_selector_block lcxt an
| "isa", _, Decl _ -> false
| "decl_unavailable_in_supported_ios_sdk", [], Decl decl ->
CPredicates.decl_unavailable_in_supported_ios_sdk decl
| "within_responds_to_selector_block", [], Decl decl ->
CPredicates.within_responds_to_selector_block lcxt decl
| "decl_unavailable_in_supported_ios_sdk", _, Stmt _ -> false
| _ -> 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 |= EF phi <=>

33
infer/src/clang/cTL.mli
Unescape View File

@ -8,6 +8,7 @@
*) *)
open! IStd open! IStd
open Ctl_parser_types
(* This module defines a language to define checkers. These checkers (* This module defines a language to define checkers. These checkers
are intepreted over the AST of the program. A checker is defined by a are intepreted over the AST of the program. A checker is defined by a
@ -57,10 +58,34 @@ type t =
there exists a descentant an of the current node such that an is of type in set T 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. *) making a transition to a node an' via label l, such that in an phi holds. *)
(** the kind of AST nodes where formulas are evaluated *) (* "set" clauses are used for defining mandatory variables that will be used
type ast_node = by when reporting issues: eg for defining the condition.
| Stmt of Clang_ast_t.stmt
| Decl of Clang_ast_t.decl "desc" clauses are used for defining the error message,
the suggestion, the severity.
"let" clauses are used to define temporary formulas which are then
used to abbreviate the another formula. For example
let f = a And B
set formula = f OR f
set message = "bla"
*)
type clause =
| CLet of string * t (* Let clause: let id = definifion; *)
| CSet of string * t (* Set clause: set id = definition *)
| CDesc of string * string (* Description clause eg: set message = "..." *)
type ctl_checker = {
name : string; (* Checker's name *)
definitions : clause list (* A list of let/set definitions *)
}
val print_checker : ctl_checker -> unit
val eval_formula : t -> ast_node -> CLintersContext.context -> bool val eval_formula : t -> ast_node -> CLintersContext.context -> bool

12
infer/src/clang/ctl_parser.mly
Unescape View File

@ -53,7 +53,7 @@
%left AU, EU %left AU, EU
%right NOT, AX, EX, AF, EF, EG, AG, EH %right NOT, AX, EX, AF, EF, EG, AG, EH
%start <Ctl_parser_types.ctl_checker list> checkers_list %start <CTL.ctl_checker list> checkers_list
%% %%
checkers_list: checkers_list:
@ -65,8 +65,8 @@ checker:
DEFINE_CHECKER identifier ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE DEFINE_CHECKER identifier ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE
{ {
Logging.out "\nParsed checker definition"; Logging.out "\nParsed checker definition";
let c = { name = $2; definitions = $5 } in let c = { CTL.name = $2; CTL.definitions = $5 } in
print_checker c; CTL.print_checker c;
c c
} }
; ;
@ -78,11 +78,11 @@ clause_list:
clause: clause:
| SET identifier ASSIGNMENT formula | SET identifier ASSIGNMENT formula
{ Logging.out "\tParsed set clause\n"; CSet ($2, $4) } { Logging.out "\tParsed set clause\n"; CTL.CSet ($2, $4) }
| SET identifier ASSIGNMENT STRING | SET identifier ASSIGNMENT STRING
{ Logging.out "\tParsed desc clause\n"; CDesc ($2, $4) } { Logging.out "\tParsed desc clause\n"; CTL.CDesc ($2, $4) }
| LET identifier ASSIGNMENT formula | LET identifier ASSIGNMENT formula
{ Logging.out "\tParsed let clause\n"; CLet ($2, $4) } { Logging.out "\tParsed let clause\n"; CTL.CLet ($2, $4) }
; ;
atomic_formula: atomic_formula:

41
infer/src/clang/ctl_parser_types.ml
Unescape View File

@ -12,31 +12,11 @@ open! IStd
(* Types used by the ctl parser *) (* Types used by the ctl parser *)
(* "set" clauses are used for defining mandatory variables that will be used (** the kind of AST nodes where formulas are evaluated *)
by when reporting issues: eg for defining the condition. type ast_node =
| Stmt of Clang_ast_t.stmt
| Decl of Clang_ast_t.decl
"desc" clauses are used for defining the error message,
the suggestion, the severity.
"let" clauses are used to define temporary formulas which are then
used to abbreviate the another formula. For example
let f = a And B
set formula = f OR f
set message = "bla"
*)
type clause =
| CLet of string * CTL.t (* Let clause: let id = definifion; *)
| CSet of string * CTL.t (* Set clause: set id = definition *)
| CDesc of string * string (* Description clause eg: set message = "..." *)
type ctl_checker = {
name : string; (* Checker's name *)
definitions : clause list (* A list of let/set definitions *)
}
let infer_prefix = "__infer_ctl_" let infer_prefix = "__infer_ctl_"
let formula_id_const = infer_prefix ^ "formula_id__" let formula_id_const = infer_prefix ^ "formula_id__"
@ -45,16 +25,3 @@ let message_const = "message"
let suggestion_const = "suggestion" let suggestion_const = "suggestion"
let severity_const = "severity" let severity_const = "severity"
let mode_const = "mode" let mode_const = "mode"
let print_checker c =
Logging.out "\n-------------------- \n";
Logging.out "\nChecker name: %s\n" c.name;
IList.iter (fun d -> (match d with
| CSet (clause_name, phi)
| CLet (clause_name, phi) ->
Logging.out " %s= \n %a\n\n"
clause_name CTL.Debug.pp_formula phi
| CDesc (clause_name, s) ->
Logging.out " %s= \n %s\n\n" clause_name s)
) c.definitions;
Logging.out "\n-------------------- \n"

Write Preview
Loading…
Cancel
Save