Implemented CTL parser

Reviewed By: dulmarod

Differential Revision: D3980883

fbshipit-source-id: 5f030da

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 \

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

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

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

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

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 <string> IDENTIFIER
+%token <string> STRING
+%token EOF
+
+%start <Ctl_parser_types.ctl_checker list> 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)}
+;
+
+%%

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 *)
+}

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
+				 	);
+};