Added the capability to import macros files in AL

Reviewed By: dulmarod

Differential Revision: D4754545

fbshipit-source-id: e8fa4fa

infer/src/clang/cFrontend_checkers_main.ml

@@ -11,13 +11,13 @@ open! IStd
 open Lexing
 open Ctl_lexer
 
-let parse_ctl_file linters_def_file channel : CFrontend_errors.linter list =
+let parse_al_file fname channel : CTL.al_file option =
   let print_position _ lexbuf =
     let pos = lexbuf.lex_curr_p in
     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
+    try Some (Ctl_parser.al_file token lexbuf) with
     | SyntaxError msg ->
         Logging.err "%a: %s\n" print_position lexbuf msg;
         None
@@ -28,11 +28,45 @@ let parse_ctl_file linters_def_file channel : CFrontend_errors.linter list =
           print_position lexbuf;
         exit (-1) in
   let lexbuf = Lexing.from_channel channel in
-  lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = linters_def_file };
-  match parse_with_error lexbuf with
-  | Some parsed_checkers ->
+  lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fname };
+  parse_with_error lexbuf
+
+let already_imported_files = ref []
+
+let rec parse_import_file import_file channel : CTL.clause list =
+  if List.mem !already_imported_files import_file then
+    failwith ("[ERROR] Cyclic imports: file '" ^ import_file ^ "' was already imported.")
+  else (
+    match parse_al_file import_file channel with
+    | Some {import_files = imports; global_macros = curr_file_macros; checkers = _} ->
+        already_imported_files := import_file :: !already_imported_files;
+        collect_all_macros imports curr_file_macros
+    | None -> Logging.out "No macros found.\n";[])
+
+and collect_all_macros imports curr_file_macros =
+  Logging.out "#### Start parsing import macros #####\n";
+  let import_macros = parse_imports imports in
+  Logging.out "#### Add global macros to import macros #####\n";
+  List.append import_macros curr_file_macros
+
+(* Parse import files with macro definitions, and it returns a list of LET clauses *)
+and parse_imports imports_files : CTL.clause list =
+  let parse_one_import_file fimport macros =
+    Logging.out "  Loading import macros from file %s\n" fimport;
+    let in_channel = open_in fimport in
+    let parsed_macros = parse_import_file fimport in_channel in
+    In_channel.close in_channel;
+    List.append parsed_macros macros in
+  List.fold_right ~f:parse_one_import_file ~init:[] imports_files
+
+let parse_ctl_file linters_def_file channel : CFrontend_errors.linter list =
+  match parse_al_file linters_def_file channel with
+  | Some {import_files = imports; global_macros = curr_file_macros; checkers = parsed_checkers} ->
+      already_imported_files := [linters_def_file];
+      let macros = collect_all_macros imports curr_file_macros in
+      let macros_map = CFrontend_errors.build_macros_map macros in
       Logging.out "#### Start Expanding checkers #####\n";
-      let exp_checkers = CFrontend_errors.expand_checkers parsed_checkers in
+      let exp_checkers = CFrontend_errors.expand_checkers macros_map parsed_checkers in
       Logging.out "#### Checkers Expanded #####\n";
       if Config.debug_mode then List.iter ~f:CTL.print_checker exp_checkers;
       CFrontend_errors.create_parsed_linters linters_def_file exp_checkers

infer/src/clang/cFrontend_errors.ml

@@ -17,6 +17,11 @@ type linter = {
   def_file : string option;
 }
 
+(* Map a formula id to a triple (visited, parameters, definition).
+   Visited is used during the expansion phase to understand if the
+   formula was already expanded and, if yes we have a cyclic definifion *)
+type macros_map = (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t
+
 let single_to_multi checker =
   fun ctx an ->
     let condition, issue_desc_opt = checker ctx an in
@@ -221,8 +226,7 @@ let rec apply_substitution f sub =
   | ETX (ntl, sw, f1) ->
       ETX (sub_list_param ntl, sw, apply_substitution f1 sub)
 
-(* expands use of let defined formula id in checkers with their definition *)
-let expand_checkers checkers =
+let expand_formula phi _map _error_msg =
   let fail_with_circular_macro_definition name error_msg =
     Logging.out
       "[ERROR]: Macro '%s' has a circular definition.\n Cycle:\n%s"
@@ -265,28 +269,36 @@ let expand_checkers checkers =
     | EG (trans, f1) -> EG (trans, expand f1 map error_msg)
     | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map error_msg)
     | ETX (tl, sw, f1) -> ETX (tl, sw, expand f1 map error_msg) in
-  let expand_one_checker checker =
-    Logging.out " +Start expanding %s\n" checker.name;
-    (* Map a formula id to a triple (visited, parameters, definition).
-       Visited is used during the expansion phase to understand if the
-       formula was already expanded and, if yes we have a cyclic definifion *)
-    let map : (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t = ALVar.FormulaIdMap.empty in
-    let map, vars = List.fold ~f:(fun (map', vars') definition ->
-        match definition with
-        | CLet (key, params, formula) ->
-            ALVar.FormulaIdMap.add key (false, params, formula) map', List.append vars' params
-        | _ -> map', vars') ~init:(map, []) checker.definitions in
+  expand phi _map _error_msg
+
+let _build_macros_map macros init_map =
+  let macros_map = List.fold ~f:(fun map' data -> match data with
+      | CTL.CLet (key, params, formula) ->
+          if ALVar.FormulaIdMap.mem key map' then
+            failwith ("[ERROR] Macro '" ^ (ALVar.formula_id_to_string key) ^
+                      "' has more than one definition.")
+          else ALVar.FormulaIdMap.add key (false, params, formula) map'
+      | _ -> map') ~init:init_map macros in
+  macros_map
+
+let build_macros_map macros =
+  let init_map : macros_map = ALVar.FormulaIdMap.empty in
+  _build_macros_map macros init_map
+
+(* expands use of let defined formula id in checkers with their definition *)
+let expand_checkers macro_map checkers =
+  let open CTL in
+  let expand_one_checker c =
+    Logging.out " +Start expanding %s\n" c.name;
+    let map = _build_macros_map c.definitions macro_map in
     let exp_defs = List.fold ~f:(fun defs clause ->
         match clause with
         | CSet (report_when_const, phi) ->
             Logging.out "  -Expanding report_when\n";
-            let exp_report_when = expand phi map "" in
-            check_def_well_expanded vars exp_report_when;
-            CSet (report_when_const, exp_report_when) :: defs
-        | cl -> cl :: defs) ~init:[] checker.definitions in
-    { checker with definitions = exp_defs} in
-  let expanded_checkers = List.map ~f:expand_one_checker checkers in
-  expanded_checkers
+            CSet (report_when_const, expand_formula phi map "") :: defs
+        | cl -> cl :: defs) ~init:[] c.definitions in
+    { c with definitions = exp_defs} in
+  List.map ~f:expand_one_checker checkers
 
 let get_err_log translation_unit_context method_decl_opt =
   let procname = match method_decl_opt with

infer/src/clang/cFrontend_errors.mli

@@ -15,6 +15,12 @@ type linter = {
   def_file : string option;
 }
 
+(* map used to expand macro. It maps a formula id to a triple
+   (visited, parameters, definition).
+   Visited is used during the expansion phase to understand if the
+   formula was already expanded and, if yes we have a cyclic definifion *)
+type macros_map = (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t
+
 (* List of checkers that will be filled after parsing them from a file *)
 val parsed_linters : linter list ref
 
@@ -23,7 +29,9 @@ val parsed_linters : linter list ref
 (* Run frontend checkers on an AST node *)
 val invoke_set_of_checkers_on_node : CLintersContext.context -> Ctl_parser_types.ast_node -> unit
 
-val expand_checkers : CTL.ctl_checker list -> CTL.ctl_checker list
+val build_macros_map : CTL.clause list -> macros_map
+
+val expand_checkers : macros_map -> CTL.ctl_checker list -> CTL.ctl_checker list
 
 val create_parsed_linters : string -> CTL.ctl_checker list -> linter list
 

infer/src/clang/cTL.ml

@@ -74,6 +74,12 @@ type ctl_checker = {
   definitions : clause list (* A list of let/set definitions *)
 }
 
+type al_file = {
+  import_files : string list;
+  global_macros : clause list;
+  checkers : ctl_checker list
+}
+
 let equal_ast_node = Poly.(=)
 
 module Debug = struct

infer/src/clang/cTL.mli

@@ -85,6 +85,12 @@ type ctl_checker = {
   definitions : clause list (* A list of let/set definitions *)
 }
 
+type al_file = {
+  import_files : string list;
+  global_macros : clause list;
+  checkers : ctl_checker list
+}
+
 val print_checker : ctl_checker -> unit
 
 val eval_formula : t -> ast_node -> CLintersContext.context -> bool

infer/src/clang/ctl_lexer.mll

@@ -25,6 +25,7 @@
 let comment = "//" [^'\n']*
 let whitespace = [' ' '\t']
 let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_' ':']*
+let file_id = ['a'-'z' 'A'-'Z' '_' '~' '/' '.'] ['a'-'z' 'A'-'Z' '0'-'9' '_' ':' '.' '/' '-']*
 
 rule token = parse
   | whitespace+ { token lexbuf }
@@ -45,6 +46,8 @@ rule token = parse
   | "HOLDS-IN-NODE" { HOLDS_IN_NODE }
   | "WITH-TRANSITION" {WITH_TRANSITION}
   | "DEFINE-CHECKER" { DEFINE_CHECKER }
+  | "GLOBAL-MACROS" { GLOBAL_MACROS }
+  | "#IMPORT" { HASHIMPORT }
   | "SET" { SET }
   | "LET" { LET }
   | "TRUE" { TRUE }
@@ -53,6 +56,8 @@ rule token = parse
   | "}" { RIGHT_BRACE }
   | "(" { LEFT_PAREN }
   | ")" { RIGHT_PAREN }
+  | "<" { LESS_THAN }
+  | ">" { GREATER_THAN }
   | "=" { ASSIGNMENT }
   | ";" { SEMICOLON }
   | "," { COMMA }
@@ -61,6 +66,7 @@ rule token = parse
   | "NOT" { NOT }
   | "IMPLIES" { IMPLIES }
   | id { IDENTIFIER (Lexing.lexeme lexbuf) }
+  | file_id { FILE_IDENTIFIER (Lexing.lexeme lexbuf) }
   | '"' { read_string (Buffer.create 80) lexbuf }
   | _ { raise (SyntaxError ("Unexpected char: '" ^ (Lexing.lexeme lexbuf) ^"'")) }
   | eof { EOF }

infer/src/clang/ctl_parser.mly

@@ -9,6 +9,14 @@
 
 %{
   let formal_params : (ALVar.t list) ref = ref []
+
+  let is_not_infer_reserved_id id =
+    if Str.string_match (Str.regexp_string Ctl_parser_types.infer_prefix) id 0 then
+        failwith
+          ("ERROR: " ^ id ^ " contains __infer_ctl_ that is a reserved keyword "
+            ^ "which cannot be used in identifiers.")
+     else id
+
 %}
 
 %token EU
@@ -21,6 +29,10 @@
 %token AG
 %token EH
 %token DEFINE_CHECKER
+%token GLOBAL_MACROS
+%token HASHIMPORT
+%token LESS_THAN
+%token GREATER_THAN
 %token ET
 %token ETX
 %token WITH_TRANSITION
@@ -42,6 +54,7 @@
 %token NOT
 %token IMPLIES
 %token <string> IDENTIFIER
+%token <string> FILE_IDENTIFIER
 %token <string> STRING
 %token EOF
 
@@ -52,8 +65,7 @@
 %left AU, EU
 %right NOT, AX, EX, AF, EF, EG, AG, EH
 
-%start <CTL.ctl_checker list> checkers_list
-
+%start <CTL.al_file> al_file
 %%
 
 var_list:
@@ -64,6 +76,22 @@ var_list:
 formal_params:
   | var_list { formal_params := $1; $1}
 
+al_file:
+  | import_files global_macros checkers_list {
+      { CTL.import_files = $1; CTL.global_macros = $2; CTL.checkers = $3 }
+    }
+  ;
+
+import_files:
+  | { [] }
+  | HASHIMPORT LESS_THAN file_identifier GREATER_THAN import_files
+    { $3 :: $5 }
+  ;
+
+global_macros:
+  | { [] }
+  | GLOBAL_MACROS LEFT_BRACE let_clause_list RIGHT_BRACE SEMICOLON { $3 }
+  ;
 
 checkers_list:
   | EOF { [] }
@@ -85,6 +113,11 @@ clause_list:
  | clause SEMICOLON clause_list { $1 :: $3 }
 ;
 
+let_clause_list:
+ | let_clause SEMICOLON { [$1] }
+ | let_clause SEMICOLON let_clause_list { $1 :: $3 }
+;
+
 clause:
   | SET identifier ASSIGNMENT formula
     { Logging.out "\tParsed SET clause\n";
@@ -103,6 +136,10 @@ clause:
       | _ -> failwith ("[ERROR] string '%s' cannot be set in a SET clause. " ^
                         "Use either of: 'message', 'suggestion', 'severity', or 'mode'\n") in
       CTL.CDesc (alvar, $4) }
+    | let_clause { $1 }
+    ;
+
+let_clause:
   | LET formula_id_def ASSIGNMENT formula
     { Logging.out "\tParsed LET clause\n"; CTL.CLet ($2, [], $4) }
   | LET formula_id_def LEFT_PAREN formal_params RIGHT_PAREN ASSIGNMENT formula
@@ -192,12 +229,10 @@ formula:
 ;
 
 identifier:
- | IDENTIFIER { if Str.string_match (Str.regexp_string Ctl_parser_types.infer_prefix) $1 0 then (
-                      Logging.err
-                      "ERROR: %s contains __infer_ctl_ that is a reserved keyword which cannot be used in identifiers." $1;
-                      assert false)
-                else $1
-              }
+ | IDENTIFIER { is_not_infer_reserved_id $1 }
  ;
 
+file_identifier:
+  | FILE_IDENTIFIER { is_not_infer_reserved_id $1 }
+  ;
 %%

infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp

@@ -1,11 +1,19 @@
 codetoanalyze/objc/linters-for-test-only/subclassing.m, B_bar, 36, MACRO_TEST1, []
 codetoanalyze/objc/linters-for-test-only/subclassing.m, B_bar, 36, MACRO_TEST2, []
 codetoanalyze/objc/linters-for-test-only/subclassing.m, B_bar, 36, MACRO_TEST3, []
-codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 26, MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 26, GLOBAL_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 26, IMPORTED_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 26, LOCAL_MACRO_SUBCLASS, []
 codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 26, SUBCLASSING_TEST_EXAMPLE, []
-codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 41, MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 41, GLOBAL_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 41, IMPORTED_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 41, LOCAL_MACRO_SUBCLASS, []
 codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 41, SUBCLASSING_TEST_EXAMPLE, []
-codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 47, MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 47, GLOBAL_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 47, IMPORTED_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 47, LOCAL_MACRO_SUBCLASS, []
 codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 47, SUBCLASSING_TEST_EXAMPLE, []
-codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 53, MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 53, GLOBAL_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 53, IMPORTED_MACRO_SUBCLASS, []
+codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 53, LOCAL_MACRO_SUBCLASS, []
 codetoanalyze/objc/linters-for-test-only/subclassing.m, Linters_dummy_method, 53, SUBCLASSING_TEST_EXAMPLE, []

infer/tests/codetoanalyze/objc/linters-for-test-only/library.al

@@ -0,0 +1,7 @@
+
+GLOBAL-MACROS {
+
+  LET imported_is_subclass_of(x) =
+        is_class(x) HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl;
+
+};

infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al

@@ -1,3 +1,12 @@
+#IMPORT <library.al>
+
+GLOBAL-MACROS {
+
+  LET global_is_subclass_of(x) =
+        is_class(x) HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl;
+
+};
+
 
 // Check that class A is not subclassed.
 DEFINE-CHECKER SUBCLASSING_TEST_EXAMPLE = {
@@ -44,7 +53,7 @@ DEFINE-CHECKER MACRO_TEST3 = {
 };
 
 
-DEFINE-CHECKER MACRO_SUBCLASS = {
+DEFINE-CHECKER LOCAL_MACRO_SUBCLASS = {
   LET is_subclass_of(x) =
           is_class(x) HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl;
 
@@ -53,3 +62,19 @@ DEFINE-CHECKER MACRO_SUBCLASS = {
    SET message = "This is subclassing A. Class A should not be subclassed.";
 
 };
+
+DEFINE-CHECKER GLOBAL_MACRO_SUBCLASS = {
+
+   SET report_when = global_is_subclass_of(A);
+
+   SET message = "This is subclassing A. Class A should not be subclassed.";
+
+};
+
+DEFINE-CHECKER IMPORTED_MACRO_SUBCLASS = {
+
+   SET report_when = imported_is_subclass_of(A);
+
+   SET message = "This is subclassing A. Class A should not be subclassed.";
+
+};