diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index f127ed669..df0c09da3 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/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 diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 2e22d21c8..6dce6be54 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/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 diff --git a/infer/src/clang/cFrontend_errors.mli b/infer/src/clang/cFrontend_errors.mli index 6d00a798a..5b9738a61 100644 --- a/infer/src/clang/cFrontend_errors.mli +++ b/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 diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index a6041e2b8..6e9029e01 100644 --- a/infer/src/clang/cTL.ml +++ b/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 diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 5c96beb02..58a759506 100644 --- a/infer/src/clang/cTL.mli +++ b/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 diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll index 7d66babe4..3e8f996d9 100644 --- a/infer/src/clang/ctl_lexer.mll +++ b/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 } diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 19f495ac3..74b15d26f 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/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 IDENTIFIER +%token FILE_IDENTIFIER %token STRING %token EOF @@ -52,8 +65,7 @@ %left AU, EU %right NOT, AX, EX, AF, EF, EG, AG, EH -%start checkers_list - +%start 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,13 +136,17 @@ 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 { Logging.out "\tParsed let clause with formula identifier '%s(....)' \n" (ALVar.formula_id_to_string $2); CTL.CLet ($2, $4, $7) } -; + ; atomic_formula: | TRUE { Logging.out "\tParsed True\n"; CTL.True } @@ -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 } + ; %% diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp b/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp index 6ec2ded45..e80e37df4 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp +++ b/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, [] diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/library.al b/infer/tests/codetoanalyze/objc/linters-for-test-only/library.al new file mode 100644 index 000000000..f6ba13996 --- /dev/null +++ b/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; + +}; diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al b/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al index 031e29285..1d2e9804f 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al +++ b/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al @@ -1,3 +1,12 @@ +#IMPORT + +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 = { @@ -19,10 +28,10 @@ DEFINE-CHECKER MACRO_TEST1 = { }; - // Test reverse parameter of macro +// Test reverse parameter of macro DEFINE-CHECKER MACRO_TEST2 = { - LET my_macro_to_call_method_of_class(x,y) = call_class_method(y,x); + LET my_macro_to_call_method_of_class(x,y) = call_class_method(y,x); SET report_when = my_macro_to_call_method_of_class(foo, A); @@ -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."; + +};