Added parsing for InNode and ETX and added formulas of missing checkers

Reviewed By: martinoluca

Differential Revision: D4231492

fbshipit-source-id: d30e60f
master
Dino Distefano 8 years ago committed by Facebook Github Bot
parent 3093f2aa3c
commit 116e90d38c

@ -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

@ -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"

@ -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

@ -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 }

@ -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) }

@ -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.";
};

Loading…
Cancel
Save