[CTL] Add support for `in_node` predicate to check correctness of its inputs

Summary:
This will help during the creation of new checkers, and will prevent errors like misspelling of AST node names.
It will also make it possible to fail immediately during the parsing of CTL inputs.

Reviewed By: ddino

Differential Revision: D4205434

fbshipit-source-id: ed8631a

facebook-clang-plugins

@@ -1 +1 @@
-Subproject commit e13e1ecabe333209fabebedb1f80f1325669fcec
+Subproject commit 177c040de8592494c1a996aff38f09ca1b6c345c

infer/src/clang/cFrontend_checkers.ml

@@ -77,12 +77,13 @@ let var_descs_name an =
    || is_CXXOperatorCallExpr || is_ObjCMessageExpr *)
 let ctl_makes_an_expensive_call () =
   let open CTL in
-  Or (Or (Or (Or (And (Atomic ("is_stmt", ["CallExpr"]),
-                       Not (Atomic("call_function_named", ["CGPointMake"]))),
-                  Atomic ("is_stmt", ["CXXTemporaryObjectExpr"])),
-              Atomic ("is_stmt", ["CXXMemberCallExpr"])),
-          Atomic ("is_stmt", ["CXXOperatorCallExpr"])),
-      Atomic ("is_stmt", ["ObjCMessageExpr"]))
+  let white_list_functions = ["CGPointMake"] in
+  Or (Or (Or (Or (And (Atomic ("in_node", ["CallExpr"]),
+                       Not(Atomic("call_function_named", white_list_functions))),
+                  Atomic ("in_node", ["CXXTemporaryObjectExpr"])),
+              Atomic ("in_node", ["CXXMemberCallExpr"])),
+          Atomic ("in_node", ["CXXOperatorCallExpr"])),
+      Atomic ("in_node", ["ObjCMessageExpr"]))
 
 
 (*
@@ -103,9 +104,9 @@ let ctl_ns_notification_warning lctx an =
                          exists_method_calling_addObserverForName) in
   let eventually_addObserver = ET(["ObjCMethodDecl"], Some Body, add_observer) in
   let exists_method_calling_removeObserver =
-    EF (None, (Atomic ("call_method",["removeObserver:"]))) in
+    EF (None, (Atomic ("call_method", ["removeObserver:"]))) in
   let exists_method_calling_removeObserverName =
-    EF (None, (Atomic ("call_method",["removeObserver:name:object:"]))) in
+    EF (None, (Atomic ("call_method", ["removeObserver:name:object:"]))) in
   let remove_observer = Or(exists_method_calling_removeObserver,
                            exists_method_calling_removeObserverName) in
   let remove_observer_in_block = ET(["BlockDecl"], Some Body, remove_observer) in
@@ -116,7 +117,7 @@ let ctl_ns_notification_warning lctx an =
        Or(remove_observer_in_method ,
           EH(["ObjCImplementationDecl"; "ObjCProtocolDecl"], remove_observer_in_method))) in
   let condition = InNode (["ObjCImplementationDecl"; "ObjCProtocolDecl"],
-                         Not (Implies (eventually_addObserver, eventually_removeObserver))) in
+                          Not (Implies (eventually_addObserver, eventually_removeObserver))) in
   let issue_desc = {
     CIssue.issue = CIssue.Registered_observer_being_deallocated;
     CIssue.description =
@@ -131,13 +132,13 @@ let ctl_ns_notification_warning lctx an =
     a boolean in a comparison *)
 let ctl_bad_pointer_comparison_warning lctx an =
   let open CTL in
-  let is_binop = Atomic ("is_stmt", ["BinaryOperator"]) in
+  let is_binop = Atomic ("in_node", ["BinaryOperator"]) in
   let is_binop_eq = Atomic ("is_binop_with_kind", ["EQ"]) in
   let is_binop_ne = Atomic ("is_binop_with_kind", ["NE"]) in
   let is_binop_neq = Or (is_binop_eq, is_binop_ne) in
   let is_unop_lnot = Atomic ("is_unop_with_kind", ["LNot"]) in
-  let is_implicit_cast_expr = Atomic ("is_stmt", ["ImplicitCastExpr"]) in
-  let is_expr_with_cleanups = Atomic ("is_stmt", ["ExprWithCleanups"]) in
+  let is_implicit_cast_expr = Atomic ("in_node", ["ImplicitCastExpr"]) in
+  let is_expr_with_cleanups = Atomic ("in_node", ["ExprWithCleanups"]) in
   let is_nsnumber = Atomic ("isa", ["NSNumber"]) in
   (*
   NOT is_binop_neq AND

infer/src/clang/cTL.ml

@@ -347,15 +347,14 @@ let next_state_via_transition an trans =
 
 (* evaluate an atomic formula (i.e. a predicate) on a ast node an and a
    linter context lcxt. That is:  an, lcxt |= pred_name(params) *)
-let eval_Atomic pred_name params an lcxt =
-  match pred_name, params, an with
-  | "call_method", [p1], Stmt st -> Predicates.call_method p1 st
-  | "property_name_contains_word", [p1] , Decl d -> Predicates.property_name_contains_word d p1
+let eval_Atomic pred_name args an lcxt =
+  match pred_name, args, an with
+  | "call_method", [m], Stmt st -> Predicates.call_method m st
+  | "property_name_contains_word", [word], Decl d -> Predicates.property_name_contains_word word d
   | "is_objc_extension", [], _ -> Predicates.is_objc_extension lcxt
   | "is_global_var", [], Decl d -> Predicates.is_syntactically_global_var d
   | "is_const_var", [], Decl d ->  Predicates.is_const_expr_var d
-  | "call_function_named", _, Stmt st -> Predicates.call_function_named st params
-  | "is_declaration_kind", [p1], Decl d -> Predicates.is_declaration_kind d p1
+  | "call_function_named", args, Stmt st -> Predicates.call_function_named args st
   | "is_strong_property", [], Decl d -> Predicates.is_strong_property d
   | "is_assign_property", [], Decl d -> Predicates.is_assign_property d
   | "is_property_pointer_type", [], Decl d -> Predicates.is_property_pointer_type d
@@ -366,11 +365,12 @@ let eval_Atomic pred_name params an lcxt =
   | "is_objc_constructor", [], _ -> Predicates.is_objc_constructor lcxt
   | "is_objc_dealloc", [], _ -> Predicates.is_objc_dealloc lcxt
   | "captures_cxx_references", [], Decl d -> Predicates.captures_cxx_references d
-  | "is_binop_with_kind", [kind], Stmt st -> Predicates.is_binop_with_kind st kind
-  | "is_unop_with_kind", [kind], Stmt st -> Predicates.is_unop_with_kind st kind
-  | "is_stmt", [stmt_name], Stmt st -> Predicates.is_stmt st stmt_name
-  | "isa", [classname], Stmt st -> Predicates.isa st classname
-  | _ -> failwith ("ERROR: Undefined Predicate: "^pred_name)
+  | "is_binop_with_kind", [str_kind], Stmt st -> Predicates.is_binop_with_kind str_kind st
+  | "is_unop_with_kind", [str_kind], Stmt st -> Predicates.is_unop_with_kind str_kind st
+  | "in_node", [nodename], Stmt st -> Predicates.is_stmt nodename st
+  | "in_node", [nodename], Decl d -> Predicates.is_decl nodename d
+  | "isa", [classname], Stmt st -> Predicates.isa classname st
+  | _ -> failwith ("ERROR: Undefined Predicate or wrong set of arguments: " ^ pred_name)
 
 (* st, lcxt |= EF phi  <=>
    st, lcxt |= phi or exists st' in Successors(st): st', lcxt |= EF phi

infer/src/clang/ctl_parser.mly

@@ -85,7 +85,7 @@ atomic_formula:
   ;
 
  formula_id:
-  | IDENTIFIER { Logging.out "\tParsed formula identifier '%s' \n" $1; CTL.Atomic($1,[]) }
+  | IDENTIFIER { Logging.out "\tParsed formula identifier '%s' \n" $1; CTL.Atomic($1, []) }
   ;
 
 params:

infer/src/clang/predicates.ml

@@ -22,7 +22,7 @@ let get_ivar_attributes ivar_decl =
        | _ -> [])
   | _ -> []
 
-(* list of cxx references captured by stmt *)
+(* list of cxx references captured by decl *)
 let captured_variables_cxx_ref dec =
   let capture_var_is_cxx_ref reference_captured_vars captured_var =
     let decl_ref_opt = captured_var.Clang_ast_t.bcv_variable in
@@ -45,11 +45,8 @@ let captured_variables_cxx_ref dec =
 
 type t = string * string list (* (name, [param1,...,paramK]) *)
 
-let pp_predicate fmt (name, arglist) =
-  Format.fprintf fmt "%s(%a)" name (Utils.pp_comma_seq Format.pp_print_string) arglist
-
-let is_declaration_kind decl s =
-  Clang_ast_proj.get_decl_kind_string decl = s
+let pp_predicate fmt (name, args) =
+  Format.fprintf fmt "%s(%a)" name (Utils.pp_comma_seq Format.pp_print_string) args
 
 (* st |= call_method(m) *)
 let call_method m st =
@@ -57,7 +54,7 @@ let call_method m st =
   | Clang_ast_t.ObjCMessageExpr (_, _, _, omei) -> omei.omei_selector = m
   | _ -> false
 
-let property_name_contains_word decl word =
+let property_name_contains_word word decl =
   match Clang_ast_proj.get_named_decl_tuple decl with
   | Some (_, n) -> let pname = n.Clang_ast_t.ni_name in
       let rexp = Str.regexp_string_case_fold word in
@@ -84,7 +81,7 @@ let decl_ref_is_in names st =
        | _ -> false)
   | _ -> false
 
-let call_function_named st names =
+let call_function_named names st =
   Ast_utils.exists_eventually_st decl_ref_is_in names st
 
 let is_strong_property decl =
@@ -168,10 +165,10 @@ let is_objc_dealloc context =
       Procname.is_objc_dealloc method_name
   | _ -> false
 
-let captures_cxx_references stmt =
-  IList.length (captured_variables_cxx_ref stmt) > 0
+let captures_cxx_references decl =
+  IList.length (captured_variables_cxx_ref decl) > 0
 
-let is_binop_with_kind stmt str_kind =
+let is_binop_with_kind str_kind stmt =
   if not (Clang_ast_proj.is_valid_binop_kind_name str_kind) then
     failwith ("Binary operator kind " ^ str_kind ^ " is not valid");
   match stmt with
@@ -179,7 +176,7 @@ let is_binop_with_kind stmt str_kind =
       Clang_ast_proj.string_of_binop_kind boi.boi_kind = str_kind
   | _ -> false
 
-let is_unop_with_kind stmt str_kind =
+let is_unop_with_kind str_kind stmt =
   if not (Clang_ast_proj.is_valid_unop_kind_name str_kind) then
     failwith ("Unary operator kind " ^ str_kind ^ " is not valid");
   match stmt with
@@ -187,10 +184,17 @@ let is_unop_with_kind stmt str_kind =
       Clang_ast_proj.string_of_unop_kind uoi.uoi_kind = str_kind
   | _ -> false
 
-let is_stmt stmt stmt_name =
-  stmt_name = Clang_ast_proj.get_stmt_kind_string stmt
+let is_stmt nodename stmt =
+  if not (Clang_ast_proj.is_valid_astnode_kind nodename) then
+    failwith ("Statement " ^ nodename ^ " is not a valid statement");
+  nodename = Clang_ast_proj.get_stmt_kind_string stmt
+
+let is_decl nodename decl =
+  if not (Clang_ast_proj.is_valid_astnode_kind nodename) then
+    failwith ("Declaration " ^ nodename ^ " is not a valid declaration");
+  nodename = Clang_ast_proj.get_decl_kind_string decl
 
-let isa stmt classname =
+let isa classname stmt =
   match Clang_ast_proj.get_expr_tuple stmt with
   | Some (_, _, expr_info) ->
       let typ = CFrontend_utils.Ast_utils.get_desugared_type expr_info.ei_type_ptr in

infer/src/clang/predicates.mli

@@ -13,7 +13,7 @@ val captured_variables_cxx_ref : Clang_ast_t.decl -> Clang_ast_t.named_decl_info
 
 val call_method : string -> Clang_ast_t.stmt -> bool
 
-val property_name_contains_word : Clang_ast_t.decl -> string -> bool
+val property_name_contains_word : string -> Clang_ast_t.decl -> bool
 
 val is_objc_extension : CLintersContext.context -> bool
 
@@ -21,9 +21,7 @@ val is_syntactically_global_var : Clang_ast_t.decl -> bool
 
 val is_const_expr_var : Clang_ast_t.decl -> bool
 
-val is_declaration_kind : Clang_ast_t.decl -> string -> bool
-
-val call_function_named : Clang_ast_t.stmt -> string list -> bool
+val call_function_named : string list -> Clang_ast_t.stmt -> bool
 
 val is_strong_property : Clang_ast_t.decl -> bool
 
@@ -43,12 +41,14 @@ val is_objc_dealloc : CLintersContext.context -> bool
 
 val captures_cxx_references : Clang_ast_t.decl -> bool
 
-val is_binop_with_kind : Clang_ast_t.stmt -> string -> bool
+val is_binop_with_kind : string -> Clang_ast_t.stmt -> bool
+
+val is_unop_with_kind : string -> Clang_ast_t.stmt -> bool
 
-val is_unop_with_kind : Clang_ast_t.stmt -> string -> bool
+val isa : string -> Clang_ast_t.stmt -> bool
 
-val is_stmt : Clang_ast_t.stmt -> string -> bool
+val is_stmt : string -> Clang_ast_t.stmt -> bool
 
-val isa : Clang_ast_t.stmt -> string -> bool
+val is_decl : string -> Clang_ast_t.decl -> bool
 
-val pp_predicate : Format.formatter -> string * string list -> unit
+val pp_predicate : Format.formatter -> t -> unit