diff --git a/infer/src/Makefile b/infer/src/Makefile index 8386fffa3..0b6bc8aa5 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -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 = \ -r \ - -use-menhir \ + -use-menhir -menhir 'menhir --explain --strict' \ -cflags -g -lflags -g \ -cflags -short-paths \ -cflags -safe-string \ diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index 4062f9d8f..f3567429f 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -15,7 +15,7 @@ open Ctl_lexer let parse_ctl_file filename = let print_position _ lexbuf = 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 let parse_with_error lexbuf = try Some (Ctl_parser.checkers_list token lexbuf) with @@ -27,8 +27,14 @@ let parse_ctl_file filename = 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 = _ } -> - Logging.out "Parsed checker: %s\n" s) 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 -> diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index d8172daa0..9da7a884f 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -56,3 +56,8 @@ type ast_node = val eval_formula : t -> ast_node -> CLintersContext.context -> bool val save_dotty_when_in_debug_mode : DB.source_file -> unit + + +module Debug : sig + val pp_formula : Format.formatter -> t -> unit +end diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll index 1fc659c84..1e7d79384 100644 --- a/infer/src/clang/ctl_lexer.mll +++ b/infer/src/clang/ctl_lexer.mll @@ -17,34 +17,35 @@ let pos = lexbuf.lex_curr_p in lexbuf.lex_curr_p <- { 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 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 | whitespace+ { token lexbuf } | whitespace*("\r")?"\n" { next_line lexbuf; token lexbuf } | comment { token lexbuf } - | "holds-until" { EU } - | "holds-everywhere-until" { AU } - | "holds-eventually" { EF } - | "holds-eventually-everywhere" { AF } - | "holds-next" { EX } - | "holds-every-next" { AX } - | "always-holds" { EG } - | "always-holds-everywhere" { AG } - | "instanceof" { EH } - | "with-node" { ET } - | "define-checker" { DEFINE_CHECKER } - | "set" { SET } - | "let" { SET } - | "True" { TRUE } - | "False" { FALSE } + | "HOLDS-UNTIL" { EU } + | "HOLDS-EVERYWHERE-UNTIL" { AU } + | "HOLDS-EVENTUALLY" { EF } + | "HOLDS-EVENTUALLY-EVERYWHERE" { AF } + | "HOLDS-NEXT" { EX } + | "HOLDS-EVERYWHERE-NEXT" { AX } + | "ALWAYS-HOLDS" { EG } + | "ALSWAYS-HOLDS-EVERYWHERE" { AG } + | "INSTANCEOF" { EH } + | "IN-NODE" { ET } + | "WITH-TRANSITION" {WITH_TRANSITION} + | "DEFINE-CHECKER" { DEFINE_CHECKER } + | "SET" { SET } + | "LET" { LET } + | "TRUE" { TRUE } + | "FALSE" { FALSE } | "{" { LEFT_BRACE } | "}" { RIGHT_BRACE } | "(" { LEFT_PAREN } @@ -55,6 +56,7 @@ rule token = parse | "AND" { AND } | "OR" { OR } | "NOT" { NOT } + | "IMPLIES" { IMPLIES } | id { IDENTIFIER (Lexing.lexeme lexbuf) } | '"' { read_string (Buffer.create 80) lexbuf } | _ { raise (SyntaxError ("Unexpected char: '" ^ (Lexing.lexeme lexbuf) ^"'")) } diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 738312d7d..e655fd677 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -9,6 +9,7 @@ %{ open Ctl_parser_types + %} %token EU @@ -20,8 +21,9 @@ %token EG %token AG %token EH -%token ET %token DEFINE_CHECKER +%token ET +%token WITH_TRANSITION %token SET %token LET %token TRUE @@ -36,13 +38,18 @@ %token AND %token OR %token NOT -%token QUOTES -%token COMMENT -%token COMMENT_LINE +%token IMPLIES %token IDENTIFIER %token STRING %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 checkers_list %% @@ -53,7 +60,7 @@ checkers_list: checker: 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: @@ -63,22 +70,22 @@ clause_list: clause: | 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 - { Logging.out "Parsed desc clause\n"; CDesc ($2, $4) } + { Logging.out "\tParsed desc clause\n"; CDesc ($2, $4) } | LET IDENTIFIER ASSIGNMENT formula - { Logging.out "Parsed let clause\n"; CLet ($2, $4) } + { Logging.out "\tParsed let clause\n"; CLet ($2, $4) } ; atomic_formula: - | TRUE { Logging.out "Parsed True\n"; CTL.True } - | FALSE { Logging.out "Parsed False\n"; CTL.False } + | TRUE { Logging.out "\tParsed True\n"; CTL.True } + | FALSE { Logging.out "\tParsed False\n"; CTL.False } | 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: - | IDENTIFIER { CTL.Atomic($1,[]) } + | IDENTIFIER { Logging.out "\tParsed formula identifier '%s' \n" $1; CTL.Atomic($1,[]) } ; params: @@ -87,22 +94,36 @@ params: | 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: | LEFT_PAREN formula RIGHT_PAREN { $2 } - | formula_id { Logging.out "Parsed formula identifier\n"; $1 } - | atomic_formula { Logging.out "Parsed atomic formula\n"; $1 } - | formula EU formula { Logging.out "Parsed EU\n"; CTL.EU($1, $3) } - | formula AU formula { Logging.out "Parsed AU\n"; CTL.AU($1, $3) } - | formula EF { Logging.out "Parsed EF\n"; CTL.EF($1) } - | formula AF{ Logging.out "Parsed AF\n"; CTL.AF($1) } - | formula EX { Logging.out "Parsed EX\n"; CTL.EX($1) } - | formula AX { Logging.out "Parsed AX\n"; CTL.AX($1) } - | formula EG { Logging.out "Parsed EG\n"; CTL.EG($1) } - | formula AG { Logging.out "Parsed AG\n"; CTL.AG($1) } - | formula EH params { Logging.out "Parsed EH\n"; CTL.EH($3, $1) } - | formula AND formula { Logging.out "Parsed AND\n"; CTL.And($1, $3) } - | formula OR formula { Logging.out "Parsed OR\n"; CTL.Or($1, $3) } - | NOT formula { Logging.out "Parsed NOT\n"; CTL.Not($2)} + | formula_id { $1 } + | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 } + | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU ($1, $3) } + | formula AU formula { Logging.out "\tParsed AU\n"; CTL.AU ($1, $3) } + | formula AF { Logging.out "\tParsed AF\n"; CTL.AF ($1) } + | formula EX { Logging.out "\tParsed EX\n"; CTL.EX ($1) } + | formula AX { Logging.out "\tParsed AX\n"; CTL.AX ($1) } + | formula EG { Logging.out "\tParsed EG\n"; CTL.EG ($1) } + | 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 ($1) } + | ET params WITH_TRANSITION transition_label formula_EF + { Logging.out "\tParsed ET\n"; CTL.ET ($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) } + | NOT formula { Logging.out "\tParsed NOT\n"; CTL.Not ($2) } ; %% diff --git a/infer/src/clang/linter_rules/linters.al b/infer/src/clang/linter_rules/linters.al index 4af58cddd..983d7daf5 100644 --- a/infer/src/clang/linter_rules/linters.al +++ b/infer/src/clang/linter_rules/linters.al @@ -7,45 +7,45 @@ // DIRECT_ATOMIC_PROPERTY_ACCESS: // 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()) 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"; - set suggestion = "Accessing an ivar of an atomic property makes the property nonatomic"; - set severity = "WARNING"; + 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 severity = "WARNING"; }; // ASSIGN_POINTER_WARNING: // 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(); - set message = "Property `%s` is a pointer type marked with the `assign` attribute"; - set suggestion = "Use a different attribute like `strong` or `weak`."; - set severity = "WARNING"; + SET message = "Property `%s` is a pointer type marked with the `assign` attribute"; + SET suggestion = "Use a different attribute like `strong` or `weak`."; + SET severity = "WARNING"; }; // BAD_POINTER_COMPARISON: // Fires whenever a NSNumber is dangerously coerced to a boolean in a comparison -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_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); - - set formula = +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_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); + + SET report_when = ( (NOT is_binop_neq) AND ( is_expr_with_cleanups @@ -53,8 +53,56 @@ define-checker BAD_POINTER_COMPARISON = { OR is_binop OR is_unop_lnot) ) - holds-until + HOLDS-UNTIL ( 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); + +};