From 40e63aa42c3ec056457a4c922e635ba2ce4c773a Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Thu, 23 Mar 2017 10:20:23 -0700 Subject: [PATCH] Added the capability to define macros in AL Reviewed By: dulmarod Differential Revision: D4721779 fbshipit-source-id: 52da9f0 --- infer/lib/linter_rules/linters.al | 4 +- infer/src/clang/cFrontend_errors.ml | 106 ++++++++++++++---- infer/src/clang/cTL.ml | 4 +- infer/src/clang/cTL.mli | 2 +- infer/src/clang/ctl_parser.mly | 7 +- .../objc/linters-for-test-only/issues.exp | 7 ++ .../linters-for-test-only/linters_example.al | 45 ++++++++ .../objc/linters-for-test-only/subclassing.m | 2 +- 8 files changed, 145 insertions(+), 32 deletions(-) diff --git a/infer/lib/linter_rules/linters.al b/infer/lib/linter_rules/linters.al index 80aa4230a..7711d9c42 100644 --- a/infer/lib/linter_rules/linters.al +++ b/infer/lib/linter_rules/linters.al @@ -153,7 +153,7 @@ DEFINE-CHECKER STRONG_DELEGATE_WARNING = { DEFINE-CHECKER GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL = { - LET is_global_var = + LET is_global_variable = is_objc_extension() AND is_global_var() AND (NOT is_const_var()); LET makes_an_expensive_call = @@ -170,7 +170,7 @@ DEFINE-CHECKER GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL = { SET report_when = WHEN - (is_global_var AND is_initialized_with_expensive_call) + (is_global_variable AND is_initialized_with_expensive_call) HOLDS-IN-NODE VarDecl; SET message = diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 607659afb..bde074742 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -137,49 +137,107 @@ let create_parsed_linters linters_def_file checkers : linter list = {condition; issue_desc; def_file = Some linters_def_file} in List.map ~f:do_one_checker checkers +let rec apply_substitution f sub = + let sub_param p = try + snd (List.find_exn sub ~f:(fun (a,_) -> String.equal p a)) + with Not_found -> p in + let sub_list_param ps = + List.map ps ~f:sub_param in + let open CTL in + match f with + | True + | False -> f + | Atomic (name, ps) -> Atomic (name, sub_list_param ps) + | Not f1 -> Not (apply_substitution f1 sub) + | And (f1, f2) -> And (apply_substitution f1 sub, apply_substitution f2 sub) + | Or (f1, f2) -> Or (apply_substitution f1 sub, apply_substitution f2 sub) + | Implies (f1, f2) -> Implies (apply_substitution f1 sub, apply_substitution f2 sub) + | InNode (node_type_list, f1) -> + InNode (sub_list_param node_type_list, apply_substitution f1 sub) + | AU (f1, f2) -> AU (apply_substitution f1 sub, apply_substitution f2 sub) + | EU (trans, f1, f2) -> + EU (trans, apply_substitution f1 sub, apply_substitution f2 sub) + | EF (trans, f1) -> EF (trans, apply_substitution f1 sub) + | AF f1 -> AF (apply_substitution f1 sub) + | AG f1 -> AG (apply_substitution f1 sub) + | EX (trans, f1) -> EX (trans, apply_substitution f1 sub) + | AX f1 -> AX (apply_substitution f1 sub) + | EH (cl, f1) -> EH (sub_list_param cl, apply_substitution f1 sub) + | EG (trans, f1) -> EG (trans, apply_substitution f1 sub) + | ET (ntl, sw, f1) -> + ET (sub_list_param ntl, sw, apply_substitution f1 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 fail_with_circular_macro_definition name error_msg = + Logging.out + "[ERROR]: Macro '%s' has a circular definition.\n Cycle:\n%s" + name error_msg; + failwith ("Cannot expand....\n") in let open CTL in let open Ctl_parser_types in - let rec expand acc map = + let rec expand acc map error_msg = match acc with | True | False -> acc | Atomic (name, [p]) when String.equal formula_id_const p -> - Logging.out " -Expanding formula identifier '%s'\n" name; + (* constant case, macro with no params *) + let error_msg' = error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in (match Core.Std.String.Map.find map name with - | Some f1 -> expand f1 map + | Some (true, _, _) -> + fail_with_circular_macro_definition name error_msg' + | Some (false, params, f1) -> + let map' = Core.Std.String.Map.add map ~key:name ~data:(true, params, f1) in + expand f1 map' error_msg' | None -> failwith - ("[ERROR]: Formula identifier '" ^ name ^ "' is undefined. Cannot expand.")); - | Atomic _ -> acc - | Not f1 -> Not (expand f1 map) - | And (f1, f2) -> And (expand f1 map, expand f2 map) - | Or (f1, f2) -> Or (expand f1 map, expand f2 map) - | Implies (f1, f2) -> Implies (expand f1 map, expand f2 map) - | InNode (node_type_list, f1) -> InNode (node_type_list, expand f1 map) - | AU (f1, f2) -> AU (expand f1 map, expand f2 map) - | EU (trans, f1, f2) -> EU (trans, expand f1 map, expand f2 map) - | EF (trans, f1) -> EF (trans, expand f1 map) - | AF f1 -> AF (expand f1 map) - | AG f1 -> AG (expand f1 map) - | EX (trans, f1) -> EX (trans, expand f1 map) - | AX f1 -> AX (expand f1 map) - | EH (cl, f1) -> EH (cl, expand f1 map) - | EG (trans, f1) -> EG (trans, expand f1 map) - | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map) - | ETX (tl, sw, f1) -> ETX (tl, sw, expand f1 map) in + ("[ERROR]: Formula identifier '" ^ name ^ "' is undefined. Cannot expand.")) + | Atomic (name, actual_param) -> (* it may be a macro *) + let error_msg' = error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in + (match Core.Std.String.Map.find map name with + | Some (true, _, _) -> + fail_with_circular_macro_definition name error_msg' + | Some (false, formal_params, f1) -> (* in this case it should be a defined macro *) + (match List.zip formal_params actual_param with + | Some sub -> + let f1_sub = apply_substitution f1 sub in + let map' = Core.Std.String.Map.add map + ~key:name ~data:(true, formal_params, f1) in + expand f1_sub map' error_msg' + | None -> failwith ("[ERROR]: Formula identifier '" ^ name ^ + "' is no called with the right number of parameters")) + | None -> acc) (* in this case it should be a predicate *) + | Not f1 -> Not (expand f1 map error_msg) + | And (f1, f2) -> And (expand f1 map error_msg, expand f2 map error_msg) + | Or (f1, f2) -> Or (expand f1 map error_msg, expand f2 map error_msg) + | Implies (f1, f2) -> Implies (expand f1 map error_msg, expand f2 map error_msg) + | InNode (node_type_list, f1) -> InNode (node_type_list, expand f1 map error_msg) + | AU (f1, f2) -> AU (expand f1 map error_msg, expand f2 map error_msg) + | EU (trans, f1, f2) -> EU (trans, expand f1 map error_msg, expand f2 map error_msg) + | EF (trans, f1) -> EF (trans, expand f1 map error_msg) + | AF f1 -> AF (expand f1 map error_msg) + | AG f1 -> AG (expand f1 map error_msg) + | EX (trans, f1) -> EX (trans, expand f1 map error_msg) + | AX f1 -> AX (expand f1 map error_msg) + | EH (cl, f1) -> EH (cl, expand f1 map error_msg) + | 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 c = Logging.out " +Start expanding %s\n" c.name; - let map : CTL.t Core.Std.String.Map.t = Core.Std.String.Map.empty in + (* 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 * string list * CTL.t) Core.Std.String.Map.t = Core.Std.String.Map.empty in let map = List.fold ~f:(fun map' d -> match d with - | CLet (k,formula) -> Core.Std.Map.add map' ~key:k ~data:formula + | CLet (k, params, formula) -> Core.Std.Map.add map' ~key:k ~data:(false, params, formula) | _ -> map') ~init:map c.definitions in let exp_defs = List.fold ~f:(fun defs clause -> match clause with | CSet (report_when_const, phi) -> Logging.out " -Expanding report_when\n"; - CSet (report_when_const, expand phi map) :: defs + CSet (report_when_const, expand phi map "") :: defs | cl -> cl :: defs) ~init:[] c.definitions in { c with definitions = exp_defs} in let expanded_checkers = List.map ~f:expand_one_checker checkers in diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index e0772803d..c0dc2a58f 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -65,7 +65,7 @@ type t = (* A ctl formula *) *) type clause = - | CLet of string * t (* Let clause: let id = definifion; *) + | CLet of string * string list * t (* Let clause: let id = definifion; *) | CSet of string * t (* Set clause: set id = definition *) | CDesc of string * string (* Description clause eg: set message = "..." *) @@ -257,7 +257,7 @@ let print_checker c = Logging.out "\nChecker name: %s\n" c.name; List.iter ~f:(fun d -> (match d with | CSet (clause_name, phi) - | CLet (clause_name, phi) -> + | CLet (clause_name, _, phi) -> Logging.out " %s= \n %a\n\n" clause_name Debug.pp_formula phi | CDesc (clause_name, s) -> diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 3c2acd2dc..9a7f8c367 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -76,7 +76,7 @@ type t = *) type clause = - | CLet of string * t (* Let clause: let id = definifion; *) + | CLet of string * string list * t (* Let clause: let id = definifion; *) | CSet of string * t (* Set clause: set id = definition *) | CDesc of string * string (* Description clause eg: set message = "..." *) diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index c9a016eeb..2006221f2 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -82,7 +82,10 @@ clause: | SET identifier ASSIGNMENT STRING { Logging.out "\tParsed desc clause\n"; CTL.CDesc ($2, $4) } | LET identifier ASSIGNMENT formula - { Logging.out "\tParsed let clause\n"; CTL.CLet ($2, $4) } + { Logging.out "\tParsed let clause\n"; CTL.CLet ($2, [], $4) } + | LET identifier LEFT_PAREN params RIGHT_PAREN ASSIGNMENT formula + { Logging.out "\tParsed let clause with formula identifier '%s(....)' \n" $2; + CTL.CLet($2, $4, $7) } ; atomic_formula: @@ -93,7 +96,7 @@ atomic_formula: ; formula_id: - | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; + | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; CTL.Atomic($1, [formula_id_const]) } ; 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 49c82d7ac..6ec2ded45 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp +++ b/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp @@ -1,4 +1,11 @@ +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, 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, 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, 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, SUBCLASSING_TEST_EXAMPLE, [] 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 cb8fed34b..031e29285 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 @@ -8,3 +8,48 @@ DEFINE-CHECKER SUBCLASSING_TEST_EXAMPLE = { SET message = "This is subclassing A. Class A should not be subclassed."; }; + +DEFINE-CHECKER MACRO_TEST1 = { + + LET call_two_methods(x,y) = call_method(x) OR call_method(y); + + SET report_when = call_two_methods(foo, bar); + + SET message = "Error message here"; + +}; + + // Test reverse parameter of macro +DEFINE-CHECKER MACRO_TEST2 = { + + 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); + + SET message = "Error message here"; + +}; + +// Test macro call macro +DEFINE-CHECKER MACRO_TEST3 = { + + LET my_macro_to_call_method_of_class(x,y) = call_class_method(y,x); + + LET call_my_macro(t,v) = my_macro_to_call_method_of_class(t,v); + + SET report_when = call_my_macro(foo, A); + + SET message = "Error message here"; + +}; + + +DEFINE-CHECKER MACRO_SUBCLASS = { + LET is_subclass_of(x) = + is_class(x) HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl; + + SET report_when = is_subclass_of(A); + + SET message = "This is subclassing A. Class A should not be subclassed."; + +}; diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/subclassing.m b/infer/tests/codetoanalyze/objc/linters-for-test-only/subclassing.m index ba8dbf92b..d60a6e875 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/subclassing.m +++ b/infer/tests/codetoanalyze/objc/linters-for-test-only/subclassing.m @@ -33,7 +33,7 @@ - (void)bar { A* a = [[A alloc] init]; - [a foo:5]; + [a foo:5]; // Error: report MACRO_TEST1, MACRO_TEST2, MACRO_TEST3 } @end