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

Fixing warning on parser.

Browse Source 
Reviewed By: jberdine

Differential Revision: D4044385

fbshipit-source-id: 843a3bf
master
Dino Distefano 8 years ago committed by Facebook Github Bot
parent f45cf115e6
commit 28b15c06af
6 changed files with 153 additions and 71 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/Makefile
Unescape View File

@ -22,7 +22,7 @@ OCAML_FATAL_WARNINGS = +5+6+8+10+11+12+18+19+20+23+26+29+27+32+33+34+35+37+38+39
OCAMLBUILD_OPTIONS = \ OCAMLBUILD_OPTIONS = \
-r \ -r \
-use-menhir \ -use-menhir -menhir 'menhir --explain --strict' \
-cflags -g -lflags -g \ -cflags -g -lflags -g \
-cflags -short-paths \ -cflags -short-paths \
-cflags -safe-string \ -cflags -safe-string \

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

@ -15,7 +15,7 @@ open Ctl_lexer
let parse_ctl_file filename = let parse_ctl_file filename =
let print_position _ lexbuf = let print_position _ lexbuf =
let pos = lexbuf.lex_curr_p in let pos = lexbuf.lex_curr_p in
Logging.out "%s:%d:%d" pos.pos_fname Logging.err "%s:%d:%d" pos.pos_fname
pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1) in pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1) in
let parse_with_error lexbuf = let parse_with_error lexbuf =
try Some (Ctl_parser.checkers_list token lexbuf) with try Some (Ctl_parser.checkers_list token lexbuf) with
@ -27,8 +27,14 @@ let parse_ctl_file filename =
exit (-1) in exit (-1) in
let parse_and_print lexbuf = match parse_with_error lexbuf with let parse_and_print lexbuf = match parse_with_error lexbuf with
| Some l -> | Some l ->
IList.iter (fun { Ctl_parser_types.name = s; Ctl_parser_types.definitions = _ } -> IList.iter (fun { Ctl_parser_types.name = s; Ctl_parser_types.definitions = defs } ->
Logging.out "Parsed checker: %s\n" s) l; 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 | None -> () in
match filename with match filename with
| Some fn -> | Some fn ->

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

@ -56,3 +56,8 @@ type ast_node =
val eval_formula : t -> ast_node -> CLintersContext.context -> bool val eval_formula : t -> ast_node -> CLintersContext.context -> bool
val save_dotty_when_in_debug_mode : DB.source_file -> unit val save_dotty_when_in_debug_mode : DB.source_file -> unit
module Debug : sig
val pp_formula : Format.formatter -> t -> unit
end

38
infer/src/clang/ctl_lexer.mll
Unescape View File

@ -17,34 +17,35 @@
let pos = lexbuf.lex_curr_p in let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <- lexbuf.lex_curr_p <-
{ pos with pos_bol = lexbuf.lex_curr_pos; { pos with pos_bol = lexbuf.lex_curr_pos;
pos_lnum = pos.pos_lnum + 1 pos_lnum = pos.pos_lnum + 1;
pos_cnum = 1;
} }
} }
let comment = "//" [^'\n']* let comment = "//" [^'\n']*
let whitespace = [' ' '\t'] let whitespace = [' ' '\t']
let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_' ':']*
rule token = parse rule token = parse
| whitespace+ { token lexbuf } | whitespace+ { token lexbuf }
| whitespace*("\r")?"\n" { next_line lexbuf; token lexbuf } | whitespace*("\r")?"\n" { next_line lexbuf; token lexbuf }
| comment { token lexbuf } | comment { token lexbuf }
| "holds-until" { EU } | "HOLDS-UNTIL" { EU }
| "holds-everywhere-until" { AU } | "HOLDS-EVERYWHERE-UNTIL" { AU }
| "holds-eventually" { EF } | "HOLDS-EVENTUALLY" { EF }
| "holds-eventually-everywhere" { AF } | "HOLDS-EVENTUALLY-EVERYWHERE" { AF }
| "holds-next" { EX } | "HOLDS-NEXT" { EX }
| "holds-every-next" { AX } | "HOLDS-EVERYWHERE-NEXT" { AX }
| "always-holds" { EG } | "ALWAYS-HOLDS" { EG }
| "always-holds-everywhere" { AG } | "ALSWAYS-HOLDS-EVERYWHERE" { AG }
| "instanceof" { EH } | "INSTANCEOF" { EH }
| "with-node" { ET } | "IN-NODE" { ET }
| "define-checker" { DEFINE_CHECKER } | "WITH-TRANSITION" {WITH_TRANSITION}
| "set" { SET } | "DEFINE-CHECKER" { DEFINE_CHECKER }
| "let" { SET } | "SET" { SET }
| "True" { TRUE } | "LET" { LET }
| "False" { FALSE } | "TRUE" { TRUE }
| "FALSE" { FALSE }
| "{" { LEFT_BRACE } | "{" { LEFT_BRACE }
| "}" { RIGHT_BRACE } | "}" { RIGHT_BRACE }
| "(" { LEFT_PAREN } | "(" { LEFT_PAREN }
@ -55,6 +56,7 @@ rule token = parse
| "AND" { AND } | "AND" { AND }
| "OR" { OR } | "OR" { OR }
| "NOT" { NOT } | "NOT" { NOT }
| "IMPLIES" { IMPLIES }
| id { IDENTIFIER (Lexing.lexeme lexbuf) } | id { IDENTIFIER (Lexing.lexeme lexbuf) }
| '"' { read_string (Buffer.create 80) lexbuf } | '"' { read_string (Buffer.create 80) lexbuf }
| _ { raise (SyntaxError ("Unexpected char: '" ^ (Lexing.lexeme lexbuf) ^"'")) } | _ { raise (SyntaxError ("Unexpected char: '" ^ (Lexing.lexeme lexbuf) ^"'")) }

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

@ -9,6 +9,7 @@
%{ %{
open Ctl_parser_types open Ctl_parser_types
%} %}
%token EU %token EU
@ -20,8 +21,9 @@
%token EG %token EG
%token AG %token AG
%token EH %token EH
%token ET
%token DEFINE_CHECKER %token DEFINE_CHECKER
%token ET
%token WITH_TRANSITION
%token SET %token SET
%token LET %token LET
%token TRUE %token TRUE
@ -36,13 +38,18 @@
%token AND %token AND
%token OR %token OR
%token NOT %token NOT
%token QUOTES %token IMPLIES
%token COMMENT
%token COMMENT_LINE
%token <string> IDENTIFIER %token <string> IDENTIFIER
%token <string> STRING %token <string> STRING
%token EOF %token EOF
/* associativity and priority (lower to higher) of operators */
%nonassoc IMPLIES
%left OR
%left AND
%left AU, EU
%right NOT, AX, EX, AF, EF, EG, AG, EH
%start <Ctl_parser_types.ctl_checker list> checkers_list %start <Ctl_parser_types.ctl_checker list> checkers_list
%% %%
@ -53,7 +60,7 @@ checkers_list:
checker: checker:
DEFINE_CHECKER IDENTIFIER ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE DEFINE_CHECKER IDENTIFIER ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE
{ Logging.out "Parsed checker \n"; { name = $2; definitions = $5 } } { Logging.out "Parsed checker \n\n"; { name = $2; definitions = $5 } }
; ;
clause_list: clause_list:
@ -63,22 +70,22 @@ clause_list:
clause: clause:
| SET IDENTIFIER ASSIGNMENT formula | SET IDENTIFIER ASSIGNMENT formula
{ Logging.out "Parsed set clause\n"; CSet ($2, $4) } { Logging.out "\tParsed set clause\n"; CSet ($2, $4) }
| SET IDENTIFIER ASSIGNMENT STRING | SET IDENTIFIER ASSIGNMENT STRING
{ Logging.out "Parsed desc clause\n"; CDesc ($2, $4) } { Logging.out "\tParsed desc clause\n"; CDesc ($2, $4) }
| LET IDENTIFIER ASSIGNMENT formula | LET IDENTIFIER ASSIGNMENT formula
{ Logging.out "Parsed let clause\n"; CLet ($2, $4) } { Logging.out "\tParsed let clause\n"; CLet ($2, $4) }
; ;
atomic_formula: atomic_formula:
| TRUE { Logging.out "Parsed True\n"; CTL.True } | TRUE { Logging.out "\tParsed True\n"; CTL.True }
| FALSE { Logging.out "Parsed False\n"; CTL.False } | FALSE { Logging.out "\tParsed False\n"; CTL.False }
| IDENTIFIER LEFT_PAREN params RIGHT_PAREN | IDENTIFIER LEFT_PAREN params RIGHT_PAREN
{ Logging.out "Parsed predicate\n"; CTL.Atomic($1, $3) } { Logging.out "\tParsed predicate\n"; CTL.Atomic($1, $3) }
; ;
formula_id: formula_id:
| IDENTIFIER { CTL.Atomic($1,[]) } | IDENTIFIER { Logging.out "\tParsed formula identifier '%s' \n" $1; CTL.Atomic($1,[]) }
; ;
params: params:
@ -87,22 +94,36 @@ params:
| IDENTIFIER COMMA params { $1 :: $3 } | IDENTIFIER COMMA params { $1 :: $3 }
; ;
transition_label:
| IDENTIFIER { match $1 with
| "Body" | "body" -> Some CTL.Body
| "InitExpr" | "initexpr" -> Some CTL.InitExpr
| _ -> None }
;
formula_EF:
| LEFT_PAREN formula RIGHT_PAREN EF { $2 }
;
formula: formula:
| LEFT_PAREN formula RIGHT_PAREN { $2 } | LEFT_PAREN formula RIGHT_PAREN { $2 }
| formula_id { Logging.out "Parsed formula identifier\n"; $1 } | formula_id { $1 }
| atomic_formula { Logging.out "Parsed atomic formula\n"; $1 } | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 }
| formula EU formula { Logging.out "Parsed EU\n"; CTL.EU($1, $3) } | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU ($1, $3) }
| formula AU formula { Logging.out "Parsed AU\n"; CTL.AU($1, $3) } | formula AU formula { Logging.out "\tParsed AU\n"; CTL.AU ($1, $3) }
| formula EF { Logging.out "Parsed EF\n"; CTL.EF($1) } | formula AF { Logging.out "\tParsed AF\n"; CTL.AF ($1) }
| formula AF{ Logging.out "Parsed AF\n"; CTL.AF($1) } | formula EX { Logging.out "\tParsed EX\n"; CTL.EX ($1) }
| formula EX { Logging.out "Parsed EX\n"; CTL.EX($1) } | formula AX { Logging.out "\tParsed AX\n"; CTL.AX ($1) }
| formula AX { Logging.out "Parsed AX\n"; CTL.AX($1) } | formula EG { Logging.out "\tParsed EG\n"; CTL.EG ($1) }
| formula EG { Logging.out "Parsed EG\n"; CTL.EG($1) } | formula AG { Logging.out "\tParsed AG\n"; CTL.AG ($1) }
| formula AG { Logging.out "Parsed AG\n"; CTL.AG($1) } | formula EH params { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) }
| formula EH params { Logging.out "Parsed EH\n"; CTL.EH($3, $1) } | formula EF { Logging.out "\tParsed EF\n"; CTL.EF ($1) }
| formula AND formula { Logging.out "Parsed AND\n"; CTL.And($1, $3) } | ET params WITH_TRANSITION transition_label formula_EF
| formula OR formula { Logging.out "Parsed OR\n"; CTL.Or($1, $3) } { Logging.out "\tParsed ET\n"; CTL.ET ($2, $4, $5)}
| NOT formula { Logging.out "Parsed NOT\n"; CTL.Not($2)} | 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) }
| NOT formula { Logging.out "\tParsed NOT\n"; CTL.Not ($2) }
; ;
%% %%

94
infer/src/clang/linter_rules/linters.al
Unescape View File

@ -7,45 +7,45 @@
// DIRECT_ATOMIC_PROPERTY_ACCESS: // DIRECT_ATOMIC_PROPERTY_ACCESS:
// a property declared atomic should not be accessed directly via its ivar // a property declared atomic should not be accessed directly via its ivar
define-checker DIRECT_ATOMIC_PROPERTY_ACCESS = { DEFINE-CHECKER DIRECT_ATOMIC_PROPERTY_ACCESS = {
set formula = SET report_when =
(NOT context_in_synchronized_block()) (NOT context_in_synchronized_block())
AND NOT is_method_property_accessor_of_ivar() AND NOT is_method_property_accessor_of_ivar()
AND NOT is_objc_constructor() AND NOT is_objc_constructor()
AND NOT is_objc_dealloc(); AND NOT is_objc_dealloc();
set message = "Direct access to ivar %s of an atomic property"; SET message = "Direct access to ivar %s of an atomic property";
set suggestion = "Accessing an ivar of an atomic property makes the property nonatomic"; SET suggestion = "Accessing an ivar of an atomic property makes the property nonatomic";
set severity = "WARNING"; SET severity = "WARNING";
}; };
// ASSIGN_POINTER_WARNING: // ASSIGN_POINTER_WARNING:
// a property with a pointer type should not be declared `assign` // a property with a pointer type should not be declared `assign`
define-checker ASSIGN_POINTER_WARNING = { DEFINE-CHECKER ASSIGN_POINTER_WARNING = {
set formula = SET report_when =
is_assign_property() AND is_property_pointer_type(); is_assign_property() AND is_property_pointer_type();
set message = "Property `%s` is a pointer type marked with the `assign` attribute"; SET message = "Property `%s` is a pointer type marked with the `assign` attribute";
set suggestion = "Use a different attribute like `strong` or `weak`."; SET suggestion = "Use a different attribute like `strong` or `weak`.";
set severity = "WARNING"; SET severity = "WARNING";
}; };
// BAD_POINTER_COMPARISON: // BAD_POINTER_COMPARISON:
// Fires whenever a NSNumber is dangerously coerced to a boolean in a comparison // Fires whenever a NSNumber is dangerously coerced to a boolean in a comparison
define-checker BAD_POINTER_COMPARISON = { DEFINE-CHECKER BAD_POINTER_COMPARISON = {
let is_binop = is_stmt(BinaryOperator); LET is_binop = is_stmt(BinaryOperator);
let is_binop_eq = is_binop_with_kind(EQ); LET is_binop_eq = is_binop_with_kind(EQ);
let is_binop_ne = is_binop_with_kind(NE); LET is_binop_ne = is_binop_with_kind(NE);
let is_binop_neq = Or (is_binop_eq, is_binop_ne); LET is_binop_neq = Or (is_binop_eq, is_binop_ne);
let is_unop_lnot = is_unop_with_kind(LNot); LET is_unop_lnot = is_unop_with_kind(LNot);
let is_implicit_cast_expr = is_stmt(ImplicitCastExpr); LET is_implicit_cast_expr = is_stmt(ImplicitCastExpr);
let is_expr_with_cleanups = is_stmt(ExprWithCleanups); LET is_expr_with_cleanups = is_stmt(ExprWithCleanups);
let is_nsnumber = isa(NSNumber); LET is_nsnumber = isa(NSNumber);
set formula = SET report_when =
( (
(NOT is_binop_neq) AND ( (NOT is_binop_neq) AND (
is_expr_with_cleanups is_expr_with_cleanups
@ -53,8 +53,56 @@ define-checker BAD_POINTER_COMPARISON = {
OR is_binop OR is_binop
OR is_unop_lnot) OR is_unop_lnot)
) )
holds-until HOLDS-UNTIL
( (
is_nsnumber is_nsnumber
); );
}; };
DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = {
LET exists_method_calling_addObserver =
call_method(addObserver:selector:name:object:) HOLDS-EVENTUALLY;
LET exists_method_calling_addObserverForName =
call_method(addObserverForName:object:queue:usingBlock:) HOLDS-EVENTUALLY;
LET add_observer =
exists_method_calling_addObserver OR exists_method_calling_addObserverForName;
LET eventually_addObserver =
IN-NODE ObjCMethodDecl WITH-TRANSITION Body
(add_observer)
HOLDS-EVENTUALLY;
LET exists_method_calling_removeObserver =
call_method(removeObserver:) HOLDS-EVENTUALLY;
LET exists_method_calling_removeObserverName =
call_method(removeObserver:name:object:) HOLDS-EVENTUALLY;
LET remove_observer =
exists_method_calling_removeObserver OR exists_method_calling_removeObserverName;
LET remove_observer_in_block =
IN-NODE BlockDecl WITH-TRANSITION Body
(remove_observer)
HOLDS-EVENTUALLY;
LET remove_observer1 =
remove_observer OR remove_observer_in_block;
LET remove_observer_in_method =
IN-NODE ObjCMethodDecl WITH-TRANSITION Body
(remove_observer1)
HOLDS-EVENTUALLY;
LET eventually_removeObserver =
IN-NODE ObjCImplementationDecl, ObjCProtocolDecl WITH-TRANSITION _
(remove_observer_in_method OR
remove_observer_in_method INSTANCEOF ObjCImplementationDecl, ObjCProtocolDecl)
HOLDS-EVENTUALLY;
SET report_when = NOT (eventually_addObserver IMPLIES eventually_removeObserver);
};

Write Preview
Loading…
Cancel
Save