Added the capability to define macros in AL

Reviewed By: dulmarod

Differential Revision: D4721779

fbshipit-source-id: 52da9f0

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 =

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."));
+                     ("[ERROR]: Formula identifier '" ^ name ^ "' is undefined. Cannot expand."))
-    | Atomic _ -> acc
+    | Atomic (name, actual_param) -> (* it may be a macro *)
-    | Not f1 -> Not (expand f1 map)
+        let error_msg' = error_msg ^ "  -Expanding formula identifier '" ^ name ^"'\n" in
-    | And (f1, f2) -> And (expand f1 map, expand f2 map)
+        (match Core.Std.String.Map.find map name with
-    | Or (f1, f2) -> Or (expand f1 map, expand f2 map)
+         | Some (true, _, _) ->
-    | Implies (f1, f2) -> Implies (expand f1 map, expand f2 map)
+             fail_with_circular_macro_definition name error_msg'
-    | InNode (node_type_list, f1) -> InNode (node_type_list, expand f1 map)
+         | Some (false, formal_params, f1) -> (* in this case it should be a defined macro *)
-    | AU (f1, f2) -> AU (expand f1 map, expand f2 map)
+             (match List.zip formal_params actual_param with
-    | EU (trans, f1, f2) -> EU (trans, expand f1 map, expand f2 map)
+              | Some sub ->
-    | EF (trans, f1) -> EF (trans, expand f1 map)
+                  let f1_sub = apply_substitution f1 sub in
-    | AF f1 -> AF (expand f1 map)
+                  let map' = Core.Std.String.Map.add map
-    | AG f1 -> AG (expand f1 map)
+                      ~key:name ~data:(true, formal_params, f1) in
-    | EX (trans, f1) -> EX (trans, expand f1 map)
+                  expand f1_sub map' error_msg'
-    | AX f1 -> AX (expand f1 map)
+              | None -> failwith ("[ERROR]: Formula identifier '" ^ name ^
-    | EH (cl, f1) -> EH (cl, expand f1 map)
+                                  "' is no called with the right number of parameters"))
-    | EG (trans, f1) -> EG (trans, expand f1 map)
+         | None -> acc) (* in this case it should be a predicate *)
-    | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map)
+    | Not f1 -> Not (expand f1 map error_msg)
-    | ETX (tl, sw, f1) -> ETX (tl, sw, expand f1 map) in
+    | 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

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

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 = "..." *)
 

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

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, []

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.";
+
+};

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