diff --git a/infer/src/Makefile b/infer/src/Makefile index 078eabfc8..3ba0b3528 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -22,6 +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 \ -cflags -g -lflags -g \ -cflags -short-paths \ -cflags -safe-string \ diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index d1ccc2d1c..18c51bd75 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -822,6 +822,10 @@ and latex = CLOpt.mk_option ~deprecated:["latex"] ~long:"latex" ~f:create_outfile ~meta:"file" "Print latex report to a file" +and linters_def_file = + CLOpt.mk_string_opt ~long:"linters-def-file" ~exes:CLOpt.[Clang] + ~meta:"file" "Specify the file containing linters definition" + and load_average = CLOpt.mk_float ~long:"load-average" ~short:"l" ~default:(float_of_int ncpu) ~exes:CLOpt.[Toplevel] ~meta:"float" @@ -1423,6 +1427,7 @@ and javac_verbose_out = !verbose_out and jobs = !jobs and join_cond = !join_cond and latex = !latex +and linters_def_file = !linters_def_file and load_average = !load_average and load_analysis_results = !load_results and makefile_cmdline = !makefile diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 45e26154e..c445af4e1 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -203,6 +203,7 @@ val javac_verbose_out : string val jobs : int val join_cond : int val latex : outfile option +val linters_def_file : string option val load_analysis_results : string option val makefile_cmdline : string val merge : bool diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index 6c6fb0651..0ca1151c1 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -9,6 +9,37 @@ open! Utils open CFrontend_utils +open Lexing +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 + 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 + | SyntaxError msg -> + Logging.err "%a: %s\n" print_position lexbuf msg; + None + | 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 = _ } -> + Logging.out "Parsed checker: %s\n" s) 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; + close_in inx + | None -> + Logging.out "No linters file specified. Nothing to parse.\n" + let rec do_frontend_checks_stmt (context:CLintersContext.context) stmt = let open Clang_ast_t in @@ -81,6 +112,7 @@ let store_issues source_file = let do_frontend_checks trans_unit_ctx ast = try + parse_ctl_file Config.linters_def_file; let source_file = trans_unit_ctx.CFrontend_config.source_file in Logging.out "Start linting file %s@\n" (DB.source_file_to_string source_file); match ast with diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll new file mode 100644 index 000000000..1fc659c84 --- /dev/null +++ b/infer/src/clang/ctl_lexer.mll @@ -0,0 +1,74 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +{ + open Lexing + open Ctl_parser + + exception SyntaxError of string + + let next_line lexbuf = + 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 + } +} + +let comment = "//" [^'\n']* +let whitespace = [' ' '\t'] +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 } + | "{" { LEFT_BRACE } + | "}" { RIGHT_BRACE } + | "(" { LEFT_PAREN } + | ")" { RIGHT_PAREN } + | "=" { ASSIGNMENT } + | ";" { SEMICOLON } + | "," { COMMA } + | "AND" { AND } + | "OR" { OR } + | "NOT" { NOT } + | id { IDENTIFIER (Lexing.lexeme lexbuf) } + | '"' { read_string (Buffer.create 80) lexbuf } + | _ { raise (SyntaxError ("Unexpected char: '" ^ (Lexing.lexeme lexbuf) ^"'")) } + | eof { EOF } + +and read_string buf = parse +| '"' { STRING (Buffer.contents buf) } +| '\\' '/' { Buffer.add_char buf '/'; read_string buf lexbuf } +| '\\' '\\' { Buffer.add_char buf '\\'; read_string buf lexbuf } +| '\\' 'b' { Buffer.add_char buf '\b'; read_string buf lexbuf } +| '\\' 'f' { Buffer.add_char buf '\012'; read_string buf lexbuf } +| '\\' 'n' { Buffer.add_char buf '\n'; read_string buf lexbuf } +| '\\' 'r' { Buffer.add_char buf '\r'; read_string buf lexbuf } +| '\\' 't' { Buffer.add_char buf '\t'; read_string buf lexbuf } +| [^ '"' '\\']+ { Buffer.add_string buf (Lexing.lexeme lexbuf); read_string buf lexbuf } +| _ { raise (SyntaxError ("Illegal string character: " ^ Lexing.lexeme lexbuf)) } +| eof { raise (SyntaxError ("String is not terminated")) } diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly new file mode 100644 index 000000000..738312d7d --- /dev/null +++ b/infer/src/clang/ctl_parser.mly @@ -0,0 +1,108 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +%{ + open Ctl_parser_types +%} + +%token EU +%token AU +%token EF +%token AF +%token EX +%token AX +%token EG +%token AG +%token EH +%token ET +%token DEFINE_CHECKER +%token SET +%token LET +%token TRUE +%token FALSE +%token LEFT_BRACE +%token RIGHT_BRACE +%token LEFT_PAREN +%token RIGHT_PAREN +%token ASSIGNMENT +%token SEMICOLON +%token COMMA +%token AND +%token OR +%token NOT +%token QUOTES +%token COMMENT +%token COMMENT_LINE +%token IDENTIFIER +%token STRING +%token EOF + +%start checkers_list + +%% +checkers_list: + | EOF { [] } + | checker SEMICOLON checkers_list { $1::$3 } + ; + +checker: + DEFINE_CHECKER IDENTIFIER ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE + { Logging.out "Parsed checker \n"; { name = $2; definitions = $5 } } +; + +clause_list: + | clause SEMICOLON { [$1] } + | clause SEMICOLON clause_list { $1 :: $3 } +; + +clause: + | SET IDENTIFIER ASSIGNMENT formula + { Logging.out "Parsed set clause\n"; CSet ($2, $4) } + | SET IDENTIFIER ASSIGNMENT STRING + { Logging.out "Parsed desc clause\n"; CDesc ($2, $4) } + | LET IDENTIFIER ASSIGNMENT formula + { Logging.out "Parsed let clause\n"; CLet ($2, $4) } +; + +atomic_formula: + | TRUE { Logging.out "Parsed True\n"; CTL.True } + | FALSE { Logging.out "Parsed False\n"; CTL.False } + | IDENTIFIER LEFT_PAREN params RIGHT_PAREN + { Logging.out "Parsed predicate\n"; CTL.Atomic($1, $3) } + ; + + formula_id: + | IDENTIFIER { CTL.Atomic($1,[]) } + ; + +params: + | {[]} + | IDENTIFIER { [$1] } + | IDENTIFIER COMMA params { $1 :: $3 } + ; + +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)} +; + +%% diff --git a/infer/src/clang/ctl_parser_types.ml b/infer/src/clang/ctl_parser_types.ml new file mode 100644 index 000000000..3f9b142ed --- /dev/null +++ b/infer/src/clang/ctl_parser_types.ml @@ -0,0 +1,37 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + + +(* Types used by the ctl parser *) + +(* "set" clauses are used for defining mandatory variables that will be used + by when reporting issues: eg for defining the condition. + + "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 *) +} diff --git a/infer/src/clang/linter_rules/linters.al b/infer/src/clang/linter_rules/linters.al new file mode 100644 index 000000000..4af58cddd --- /dev/null +++ b/infer/src/clang/linter_rules/linters.al @@ -0,0 +1,60 @@ +// Copyright (c) 2016 - present Facebook, Inc. +// All rights reserved. +// +// This source code is licensed under the BSD style license found in the +// LICENSE file in the root directory of this source tree. An additional grant +// of patent rights can be found in the PATENTS file in the same directory. + +// DIRECT_ATOMIC_PROPERTY_ACCESS: +// a property declared atomic should not be accessed directly via its ivar +define-checker DIRECT_ATOMIC_PROPERTY_ACCESS = { + + set formula = + (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"; +}; + +// ASSIGN_POINTER_WARNING: +// a property with a pointer type should not be declared `assign` +define-checker ASSIGN_POINTER_WARNING = { + + set formula = + 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"; +}; + +// 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 = + ( + (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 + ); +};