diff --git a/infer/src/clang/cFrontend_checkers.mli b/infer/src/clang/cFrontend_checkers.mli index 164433697..a09842ab2 100644 --- a/infer/src/clang/cFrontend_checkers.mli +++ b/infer/src/clang/cFrontend_checkers.mli @@ -51,3 +51,9 @@ val location_from_dinfo : val location_from_decl : CLintersContext.context -> Clang_ast_t.decl -> Location.t + +val decl_name_from_an : CTL.ast_node -> string + +val ivar_name : CTL.ast_node -> string + +val var_descs_name : CTL.ast_node -> string diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index 54ac2dbb2..74198b6a7 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -25,23 +25,12 @@ let parse_ctl_file filename = | Ctl_parser.Error -> Logging.err "%a: syntax error\n" print_position lexbuf; exit (-1) in - let parse_and_print lexbuf = match parse_with_error lexbuf with - | Some l -> - IList.iter (fun { Ctl_parser_types.name = s; Ctl_parser_types.definitions = defs } -> - Logging.out "Parsed checker definition: %s\n" s; - IList.iter (fun d -> match d with - | Ctl_parser_types.CSet ("report_when", phi) -> - Logging.out " Report when: \n %a\n" - CTL.Debug.pp_formula phi - | _ -> ()) defs - ) l; - | None -> () in match filename with | Some fn -> let inx = open_in fn in let lexbuf = Lexing.from_channel inx in lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fn }; - parse_and_print lexbuf; + let _ = parse_with_error lexbuf in close_in inx | None -> Logging.out "No linters file specified. Nothing to parse.\n" diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 256aa25e9..bec54349a 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -98,7 +98,7 @@ module Debug = struct (Utils.pp_comma_seq Format.pp_print_string) arglist pp_formula phi | ET (arglist, trans, phi) - | ETX (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" + | ETX (arglist, trans, phi) -> Format.fprintf fmt "ETX[%a][%a](%a)" (Utils.pp_comma_seq Format.pp_print_string) arglist pp_transition trans pp_formula phi diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll index 1e7d79384..b29861e9d 100644 --- a/infer/src/clang/ctl_lexer.mll +++ b/infer/src/clang/ctl_lexer.mll @@ -40,6 +40,9 @@ rule token = parse | "ALSWAYS-HOLDS-EVERYWHERE" { AG } | "INSTANCEOF" { EH } | "IN-NODE" { ET } + | "IN-EXCLUSIVE-NODE" { ETX } + | "WHEN" { WHEN } + | "HOLDS-IN-NODE" { HOLDS_IN_NODE } | "WITH-TRANSITION" {WITH_TRANSITION} | "DEFINE-CHECKER" { DEFINE_CHECKER } | "SET" { SET } diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 04bb1f294..13770cd4a 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -23,7 +23,10 @@ %token EH %token DEFINE_CHECKER %token ET +%token ETX %token WITH_TRANSITION +%token WHEN +%token HOLDS_IN_NODE %token SET %token LET %token TRUE @@ -60,7 +63,20 @@ checkers_list: checker: DEFINE_CHECKER IDENTIFIER ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE - { Logging.out "Parsed checker \n\n"; { name = $2; definitions = $5 } } + { let name = $2 in + let definitions = $5 in + Logging.out "\nParsed checker definition: %s\n" name; + IList.iter (fun d -> (match d with + | Ctl_parser_types.CSet (clause_name, phi) + | Ctl_parser_types.CLet (clause_name, phi) -> + Logging.out " %s= \n %a\n\n" + clause_name CTL.Debug.pp_formula phi + | Ctl_parser_types.CDesc (clause_name, s) -> + Logging.out " %s= \n %s\n\n" clause_name s) + ) definitions; + Logging.out "\n-------------------- \n"; + { name = name; definitions = definitions } + } ; clause_list: @@ -98,6 +114,7 @@ transition_label: | IDENTIFIER { match $1 with | "Body" | "body" -> Some CTL.Body | "InitExpr" | "initexpr" -> Some CTL.InitExpr + | "Cond" | "cond" -> Some CTL.Cond | _ -> None } ; @@ -118,8 +135,12 @@ formula: | formula AG { Logging.out "\tParsed AG\n"; CTL.AG ($1) } | formula EH params { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) } | formula EF { Logging.out "\tParsed EF\n"; CTL.EF (None, $1) } + | WHEN formula HOLDS_IN_NODE params + { Logging.out "\tParsed InNode\n"; CTL.InNode ($4, $2)} | ET params WITH_TRANSITION transition_label formula_EF { Logging.out "\tParsed ET\n"; CTL.ET ($2, $4, $5)} + | ETX params WITH_TRANSITION transition_label formula_EF + { Logging.out "\tParsed ETX\n"; CTL.ETX ($2, $4, $5)} | formula AND formula { Logging.out "\tParsed AND\n"; CTL.And ($1, $3) } | formula OR formula { Logging.out "\tParsed OR\n"; CTL.Or ($1, $3) } | formula IMPLIES formula { Logging.out "\tParsed IMPLIES\n"; CTL.Implies ($1, $3) } diff --git a/infer/src/clang/linter_rules/linters.al b/infer/src/clang/linter_rules/linters.al index 983d7daf5..2f9b66ca9 100644 --- a/infer/src/clang/linter_rules/linters.al +++ b/infer/src/clang/linter_rules/linters.al @@ -10,12 +10,14 @@ DEFINE-CHECKER DIRECT_ATOMIC_PROPERTY_ACCESS = { SET report_when = - (NOT context_in_synchronized_block()) - AND NOT is_method_property_accessor_of_ivar() - AND NOT is_objc_constructor() - AND NOT is_objc_dealloc(); - - SET message = "Direct access to ivar %s of an atomic property"; + WHEN + ((NOT context_in_synchronized_block()) AND is_ivar_atomic()) + AND NOT is_method_property_accessor_of_ivar() + AND NOT is_objc_constructor() + AND NOT is_objc_dealloc() + HOLDS-IN-NODE ObjCIvarRefExpr; + + SET message = "Direct access to ivar %ivar_name of an atomic property"; SET suggestion = "Accessing an ivar of an atomic property makes the property nonatomic"; SET severity = "WARNING"; }; @@ -25,9 +27,11 @@ DEFINE-CHECKER DIRECT_ATOMIC_PROPERTY_ACCESS = { DEFINE-CHECKER ASSIGN_POINTER_WARNING = { SET report_when = - is_assign_property() AND is_property_pointer_type(); + WHEN + is_assign_property() AND is_property_pointer_type() + HOLDS-IN-NODE ObjCPropertyDecl; - SET message = "Property `%s` is a pointer type marked with the `assign` attribute"; + SET message = "Property `%decl_name` is a pointer type marked with the `assign` attribute"; SET suggestion = "Use a different attribute like `strong` or `weak`."; SET severity = "WARNING"; }; @@ -39,26 +43,41 @@ DEFINE-CHECKER BAD_POINTER_COMPARISON = { LET is_binop = is_stmt(BinaryOperator); LET is_binop_eq = is_binop_with_kind(EQ); LET is_binop_ne = is_binop_with_kind(NE); - LET is_binop_neq = Or (is_binop_eq, is_binop_ne); + LET is_binop_neq = is_binop_eq OR is_binop_ne; LET is_unop_lnot = is_unop_with_kind(LNot); LET is_implicit_cast_expr = is_stmt(ImplicitCastExpr); LET is_expr_with_cleanups = is_stmt(ExprWithCleanups); LET is_nsnumber = isa(NSNumber); + LET eu =( + (NOT is_binop_neq) + AND (is_expr_with_cleanups + OR is_implicit_cast_expr + OR is_binop + OR is_unop_lnot) + ) + HOLDS-UNTIL + ( + is_nsnumber + ); + + LET etx = + IN-EXCLUSIVE-NODE IfStmt, ForStmt, WhileStmt, ConditionalOperator WITH-TRANSITION Cond + (eu) + HOLDS-EVENTUALLY; + SET report_when = - ( - (NOT is_binop_neq) AND ( - is_expr_with_cleanups - OR is_implicit_cast_expr - OR is_binop - OR is_unop_lnot) - ) - HOLDS-UNTIL - ( - is_nsnumber - ); + WHEN + etx + HOLDS-IN-NODE IfStmt, ForStmt, WhileStmt, ConditionalOperator; + + SET description = "Implicitly checking whether NSNumber pointer is nil"; + + SET suggestion = + "Did you mean to compare against the unboxed value instead? Please either explicitly compare the NSNumber instance to nil, or use one of the NSNumber accessors before the comparison."; }; + DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = { LET exists_method_calling_addObserver = @@ -103,6 +122,72 @@ DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = { remove_observer_in_method INSTANCEOF ObjCImplementationDecl, ObjCProtocolDecl) HOLDS-EVENTUALLY; - SET report_when = NOT (eventually_addObserver IMPLIES eventually_removeObserver); + SET report_when = + WHEN + NOT (eventually_addObserver IMPLIES eventually_removeObserver) + HOLDS-IN-NODE ObjCImplementationDecl, ObjCProtocolDecl; + + SET description = + "Object self is registered in a notification center but not being removed before deallocation"; + + SET suggestion = + "Consider removing the object from the notification center before its deallocation."; + +}; + +DEFINE-CHECKER strong_delegate_warning = { + + LET name_contains_delegate = property_name_contains_word(delegate); + LET name_does_not_contains_queue = NOT property_name_contains_word(queue); + + SET report_when = + WHEN + name_contains_delegate AND name_does_not_contains_queue AND is_strong_property() + HOLDS-IN-NODE ObjCPropertyDecl; + + SET description = "Property or ivar %decl_name declared strong"; + SET suggestion = "In general delegates should be declared weak or assign"; }; + +DEFINE-CHECKER global_var_init_with_calls_warning = { + + LET is_global_var = + is_objc_extension() AND is_global_var() AND (NOT is_const_var()); + + LET makes_an_expensive_call = + (is_stmt(CallExpr) AND NOT call_function_named(CGPointMake)) + OR is_stmt(CXXTemporaryObjectExpr) + OR is_stmt(CXXMemberCallExpr) + OR is_stmt(CXXOperatorCallExpr) + OR is_stmt(ObjCMessageExpr); + + LET is_initialized_with_expensive_call = + IN-NODE VarDecl WITH-TRANSITION InitExpr + (makes_an_expensive_call HOLDS-EVENTUALLY) + HOLDS-EVENTUALLY; + + SET report_when = + WHEN + (ctl_is_global_var AND ctl_is_initialized_with_expensive_call) + HOLDS-IN-NODE VarDecl; + + SET description = + "Global variable %decl_name is initialized using a function or method call"; + SET suggestion = + "If the function/method call is expensive, it can affect the starting time of the app."; +}; + + +DEFINE-CHECKER ctl_captured_cxx_ref_in_objc_block_warning = { + SET report_when = + WHEN + captures_cxx_references() + HOLDS-IN-NODE BlockDecl; + + SET description = + "C++ Reference variable(s) %var_desc_name captured by Objective-C block"; + + SET suggestion = "C++ References are unmanaged and may be invalid by the time the block executes."; + + };