pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Defining an AST specification language based on CTL for front-end checkers

Browse Source 
Summary:
This diff introduces a first version of a front-end checkers specification
language. The language is based on the CTL temporal logic that is interpreted
on trees. In this case the model for a formula is the AST of the program produced
by clang.

This diff introduce the language and translate most of the existing checks on
this new language. In other diff I will translate all the other checks.
Then I will generalize the framework to allow the developer to specify only
the CTL formula.

Reviewed By: martinoluca

Differential Revision: D3819211

fbshipit-source-id: f8e01eb
master
Dino Distefano 9 years ago committed by Facebook Github Bot
parent fc28683ea2
commit 05bb4a0db7
9 changed files with 837 additions and 302 deletions
Show Stats Download Patch File Download Diff File

467
infer/src/clang/cFrontend_checkers.ml
Unescape View File

@ -10,12 +10,11 @@
open! Utils open! Utils
open CFrontend_utils open CFrontend_utils
(* To create a new checker you should: *) (* To create a new checker you should: *)
(* 1. Define a checker function, say my_checker, in this module. *) (* 1. Define a checker function, say my_checker, in this module. *)
(* my_checker should define: *) (* my_checker should define: *)
(* -a) a condition that determine if the checker fires *) (* -a) a condition that determine if the checker fires *)
(* -b) a warning_desc that describes the warning (see warning_desc definition) *) (* -b) a issue_desc that describes the warning (see warning_desc definition) *)
(* 2. Add your checker to the CFrontend_checkers interface *) (* 2. Add your checker to the CFrontend_checkers interface *)
(* 3. Decide in which element of the AST my_checker should be evaluated. *) (* 3. Decide in which element of the AST my_checker should be evaluated. *)
(* - If it is a statement then you need to invoke my_checker from *) (* - If it is a statement then you need to invoke my_checker from *)
@ -23,252 +22,229 @@ open CFrontend_utils
(* - If it is a declaration invoke it from run_frontend_checkers_on_decl *) (* - If it is a declaration invoke it from run_frontend_checkers_on_decl *)
(* Helper functions *) (* Helper functions *)
let get_ivar_attributes ivar_decl =
let open Clang_ast_t in
match ivar_decl with
| ObjCIvarDecl (ivar_decl_info, _, _, _, _) ->
(match Ast_utils.get_property_of_ivar ivar_decl_info.Clang_ast_t.di_pointer with
| Some ObjCPropertyDecl (_, _, obj_c_property_decl_info) ->
obj_c_property_decl_info.Clang_ast_t.opdi_property_attributes
| _ -> [])
| _ -> []
let is_method_property_accessor_of_ivar method_decl ivar_pointer =
let open Clang_ast_t in
match method_decl with
| ObjCMethodDecl (_, _, obj_c_method_decl_info) ->
if obj_c_method_decl_info.Clang_ast_t.omdi_is_property_accessor then
let prperty_opt = obj_c_method_decl_info.Clang_ast_t.omdi_property_decl in
match Ast_utils.get_decl_opt_with_decl_ref prperty_opt with
| Some ObjCPropertyDecl (_, _, obj_c_property_decl_info) ->
(match obj_c_property_decl_info.Clang_ast_t.opdi_ivar_decl with
| Some decl_ref -> decl_ref.Clang_ast_t.dr_decl_pointer = ivar_pointer
| None -> false)
| _ -> false
else false
| _ -> false
(* checks if ivar is defined among a set of fields and if it is atomic *)
let is_ivar_atomic attributes =
IList.exists (Ast_utils.property_attribute_eq `Atomic) attributes
let name_contains_word pname word =
let rexp = Str.regexp_string_case_fold word in
try
Str.search_forward rexp pname.Clang_ast_t.ni_name 0 >= 0
with Not_found -> false
let location_from_sinfo info = let location_from_sinfo info =
CLocation.get_sil_location_from_range info.Clang_ast_t.si_source_range true CLocation.get_sil_location_from_range info.Clang_ast_t.si_source_range true
let location_from_stmt stmt =
let info, _ = Clang_ast_proj.get_stmt_tuple stmt in
CLocation.get_sil_location_from_range info.Clang_ast_t.si_source_range true
let location_from_dinfo info = let location_from_dinfo info =
CLocation.get_sil_location_from_range info.Clang_ast_t.di_source_range true CLocation.get_sil_location_from_range info.Clang_ast_t.di_source_range true
let rec is_self s = let location_from_decl dec =
let open Clang_ast_t in let info = Clang_ast_proj.get_decl_tuple dec in
match s with CLocation.get_sil_location_from_range info.Clang_ast_t.di_source_range true
| ImplicitCastExpr(_, [s], _, _) -> is_self s
| DeclRefExpr(_, _, _, dr) ->
(match dr.drti_decl_ref with
| Some decl_ref ->
(match decl_ref.dr_name with
| Some n -> n.ni_name = CFrontend_config.self
| _ -> false)
| _ -> false)
| _ -> false
let decl_ref_is_in names st =
match st with
| Clang_ast_t.DeclRefExpr (_, _, _, drti) ->
(match drti.drti_decl_ref with
| Some dr -> let ndi, _, _ = CFrontend_utils.Ast_utils.get_info_from_decl_ref dr in
IList.exists (fun n -> n = ndi.ni_name) names
| _ -> false)
| _ -> false
let call_function_named st names =
Ast_utils.exists_eventually_st decl_ref_is_in names st
let rec eventually_makes_a_call exp = let decl_name dec =
CFrontend_utils.Ast_utils.exists_eventually_st is_expensive_function_or_method_call () exp match Clang_ast_proj.get_named_decl_tuple dec with
| Some (_, n) -> n.Clang_ast_t.ni_name
| None -> ""
and is_expensive_function_or_method_call _ st = let ivar_name stmt =
let white_list_functions = ["CGPointMake"] in
let open Clang_ast_t in let open Clang_ast_t in
match st with match stmt with
| CallExpr (_, st :: _, _) -> (* for C *) | ObjCIvarRefExpr (_, _, _, rei) ->
not (call_function_named st white_list_functions) let dr_ref = rei.ovrei_decl_ref in
| CXXConstructExpr (_, stmt_list, _, _) -> let ivar_pointer = dr_ref.dr_decl_pointer in
(* Assumption: constructor is expensive iff it has a call inside *) (match Ast_utils.get_decl ivar_pointer with
(IList.exists eventually_makes_a_call) stmt_list | Some (ObjCIvarDecl (_, named_decl_info, _, _, _)) ->
| CXXTemporaryObjectExpr _ (* for C++ *) named_decl_info.Clang_ast_t.ni_name
| CXXMemberCallExpr _ | CXXOperatorCallExpr _ | _ -> "")
| ObjCMessageExpr _ -> true (* for ObjC *) | _ -> ""
| _ -> false
(* Call method m and on the pn parameter pred holds *) (* (is_CallExpr /\ not call_function_named) ||
(* st |= call_method(m(p1,...,pn,...pk)) /\ pred(pn) *) is_CXXTemporaryObjectExpr || is_CXXMemberCallExpr
let call_method_on_nth pred pn m st = || is_CXXOperatorCallExpr || is_ObjCMessageExpr *)
match st with let ctl_makes_an_expensive_call () =
| Clang_ast_t.ObjCMessageExpr (_, params, _, omei) when omei.omei_selector = m -> let open CTL in
(try let white_list_functions = ["CGPointMake"] in
let p = IList.nth params pn in Or (Or (Or (Or (And (Atomic ("is_statement_kind", ["CallExpr"]),
pred p Not(Atomic("call_function_named", white_list_functions))),
with _ -> false) Atomic ("is_statement_kind", ["CXXTemporaryObjectExpr"])),
| _ -> false Atomic ("is_statement_kind", ["CXXMemberCallExpr"])),
Atomic ("is_statement_kind", ["CXXOperatorCallExpr"])),
Atomic ("is_statement_kind", ["ObjCMessageExpr"]))
let dec_body_eventually atomic_pred param dec =
match dec with
| Clang_ast_t.ObjCMethodDecl (_, _, omdi) ->
(match omdi.Clang_ast_t.omdi_body with
| Some body -> Ast_utils.exists_eventually_st atomic_pred param body
| _ -> false)
| _ -> false
(* true if a variable is initialized with a method/function call.*) (*
(* implemented as decl |= EF is_function_or_method_call *) ET([ObjCMethodDecl][->Body] (EF call_addObserver
let is_initialized_with_expensive_call decl = Or EF call_addObserverForName)
match decl with =>
| Clang_ast_t.VarDecl (_, _ ,_, vdi) -> ET([ObjCImplementationDecl,ObjCProtocolDecl][->]
(match vdi.vdi_init_expr with ET([ObjCMethodDecl][->Body] EF remove_observer) Or
| Some init_expr -> EH([ObjCImplementationDecl, ObjCProtocolDecl] EF remove_observer)
eventually_makes_a_call init_expr *)
| _ -> false) let ctl_ns_notification decl =
| _ -> false let open CTL in
let exists_method_calling_addObserver =
EF (Atomic ("call_method", ["addObserver:selector:name:object:"])) in
let exists_method_calling_addObserverForName =
EF (Atomic ("call_method", ["addObserverForName:object:queue:usingBlock:"])) in
let add_observer = Or (exists_method_calling_addObserver,
exists_method_calling_addObserverForName) in
let eventually_addObserver = ET(["ObjCMethodDecl"], Some Body, add_observer) in
let exists_method_calling_removeObserver =
EF(Atomic ("call_method",["removeObserver:"])) in
let exists_method_calling_removeObserverName =
EF(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
let remove_observer' = Or(remove_observer, remove_observer_in_block) in
let remove_observer_in_method = ET(["ObjCMethodDecl"], Some Body, remove_observer') in
let eventually_removeObserver =
ET(["ObjCImplementationDecl"; "ObjCProtocolDecl"], None,
Or(remove_observer_in_method ,
EH(["ObjCImplementationDecl"; "ObjCProtocolDecl"], remove_observer_in_method))) in
let condition = Not (Implies (eventually_addObserver, eventually_removeObserver)) in
let issue_desc = {
CIssue.issue = CIssue.Registered_observer_being_deallocated;
CIssue.description =
Localise.registered_observer_being_deallocated_str CFrontend_config.self;
CIssue.suggestion =
Some "Consider removing the object from the notification center before its deallocation.";
CIssue.loc = location_from_decl decl;
} in
condition, issue_desc
(* name_contains_delegate AND not name_contains_queue AND is_strong_property *)
let ctl_strong_delegate dec =
let open CTL in
let name_contains_delegate =
Atomic ("property_name_contains_word", ["delegate"]) in
let name_does_not_contains_queue =
Not(Atomic ("property_name_contains_word", ["queue"])) in
let is_strong_property =
Atomic("is_strong_property", []) in
let condition = And (name_contains_delegate,
And (name_does_not_contains_queue,
is_strong_property)) in
let issue_desc = {
CIssue.issue = CIssue.Strong_delegate_warning;
CIssue.description = Printf.sprintf
"Property or ivar %s declared strong" (decl_name dec);
CIssue.suggestion = Some "In general delegates should be declared weak or assign";
CIssue.loc = location_from_decl dec
} in
condition, issue_desc
(* (is_ObjC || is_Objc++) /\ is_global_var /\ not is_const_var /\
ET([VarDecl][->InitExpr] EF ctl_makes_an_expensive_call)
*)
let ctl_global_var_init_with_calls_warning decl =
let open CTL in
let ctl_is_global_var =
And (And (Atomic ("is_objc_extension", []), Atomic ("is_global_var", [])),
Not (Atomic ("is_const_var", []))) in
let ctl_is_initialized_with_expensive_call =
ET(["VarDecl"], Some InitExpr, EF (ctl_makes_an_expensive_call ())) in
let condition = And (ctl_is_global_var, ctl_is_initialized_with_expensive_call) in
let issue_desc = {
CIssue.issue = CIssue.Global_variable_initialized_with_function_or_method_call;
CIssue.description = Printf.sprintf
"Global variable %s is initialized using a function or method call"
(decl_name decl);
CIssue.suggestion = Some
"If the function/method call is expensive, it can affect the starting time of the app.";
CIssue.loc = location_from_decl decl
} in
condition, issue_desc
(* is_assign_property AND is_property_pointer_type *)
let ctl_assign_pointer_warning decl =
let open CTL in
let condition =
And (Atomic("is_assign_property", []), Atomic("is_property_pointer_type", [])) in
let issue_desc =
{ CIssue.issue = CIssue.Assign_pointer_warning;
CIssue.description =
Printf.sprintf
"Property `%s` is a pointer type marked with the `assign` attribute"
(decl_name decl);
CIssue.suggestion = Some "Use a different attribute like `strong` or `weak`.";
CIssue.loc = location_from_decl decl
} in
condition, issue_desc
let captured_variables_cxx_ref captured_vars = (*
let capture_var_is_cxx_ref reference_captured_vars captured_var = not context_in_synchronized_block /\ not is_method_property_accessor_of_ivar
let decl_ref_opt = captured_var.Clang_ast_t.bcv_variable in /\ not is_objc_constructor /\ not is_objc_dealloc
match Ast_utils.get_decl_opt_with_decl_ref decl_ref_opt with *)
| Some VarDecl (_, named_decl_info, qual_type, _) let ctl_direct_atomic_property_access_warning stmt =
| Some ParmVarDecl (_, named_decl_info, qual_type, _) let open CTL in
| Some ImplicitParamDecl (_, named_decl_info, qual_type, _) -> let condition =
(match Ast_utils.get_desugared_type qual_type.Clang_ast_t.qt_type_ptr with And (And (And (And (Not (Atomic ("context_in_synchronized_block", [])),
| Some RValueReferenceType _ | Some LValueReferenceType _ -> Atomic("is_ivar_atomic", [])),
named_decl_info::reference_captured_vars Not (Atomic ("is_method_property_accessor_of_ivar", []))),
| _ -> reference_captured_vars) Not (Atomic ("is_objc_constructor", []))),
| _ -> reference_captured_vars in Not (Atomic ("is_objc_dealloc", []))) in
IList.fold_left capture_var_is_cxx_ref [] captured_vars let issue_desc = {
CIssue.issue = CIssue.Direct_atomic_property_access;
CIssue.description = Printf.sprintf
"Direct access to ivar %s of an atomic property" (ivar_name stmt);
CIssue.suggestion =
Some "Accessing an ivar of an atomic property makes the property nonatomic";
CIssue.loc = location_from_stmt stmt
} in
condition, issue_desc
let ctl_captured_cxx_ref_in_objc_block_warning stmt =
(* Fire if the list of captured references is not empty *)
let condition = CTL.Atomic ("captures_cxx_references", []) in
let issue_desc = {
CIssue.issue = CIssue.Cxx_reference_captured_in_objc_block;
CIssue.description = Printf.sprintf
"C++ Reference variable(s) %s captured by Objective-C block"
(Predicates.var_descs_name stmt);
CIssue.suggestion = Some ("C++ References are unmanaged and may be invalid " ^
"by the time the block executes.");
CIssue.loc = location_from_stmt stmt
} in
condition, issue_desc
(* === Warnings on properties === *) (* === Warnings on properties === *)
(* Assing Pointer Warning: a property with a pointer type should not be declared `assign` *) (* Assing Pointer Warning: a property with a pointer type should not be declared `assign` *)
let assign_pointer_warning _ decl_info pname obj_c_property_decl_info = let assign_pointer_warning lcxt decl =
let open Clang_ast_t in let open CTL in
let condition = let condition, issue_desc = ctl_assign_pointer_warning decl in
let has_assign_property () = ObjcProperty_decl.is_assign_property obj_c_property_decl_info in if CTL.eval_formula condition (Decl decl) lcxt then
let is_pointer_type () = Some issue_desc
let type_ptr = obj_c_property_decl_info.opdi_type_ptr in
let raw_ptr = Clang_ast_types.type_ptr_to_clang_pointer type_ptr in
match Clang_ast_main.PointerMap.find raw_ptr !CFrontend_config.pointer_type_index with
| MemberPointerType _ | ObjCObjectPointerType _ | BlockPointerType _ -> true
| TypedefType (_, tti) -> (Ast_utils.name_of_typedef_type_info tti) = CFrontend_config.id_cl
| exception Not_found -> false
| _ -> false in
has_assign_property() && is_pointer_type () in
if condition then
Some
{ CIssue.issue = CIssue.Assign_pointer_warning;
CIssue.description =
Printf.sprintf
"Property `%s` is a pointer type marked with the `assign` attribute"
pname.ni_name;
CIssue.suggestion = Some "Use a different attribute like `strong` or `weak`.";
CIssue.loc = location_from_dinfo decl_info
}
else None else None
(* Strong Delegate Warning: a property with name delegate should not be declared strong *) (* Strong Delegate Warning: a property with name delegate should not be declared strong *)
let strong_delegate_warning _ decl_info pname obj_c_property_decl_info = let strong_delegate_warning lcxt decl =
let condition = (name_contains_word pname "delegate") let condition, issue_desc = ctl_strong_delegate decl in
&& not (name_contains_word pname "queue") if CTL.eval_formula condition (Decl decl) lcxt then
&& ObjcProperty_decl.is_strong_property obj_c_property_decl_info in Some issue_desc
if condition then
Some { CIssue.issue = CIssue.Strong_delegate_warning;
CIssue.description = "Property or ivar "^pname.Clang_ast_t.ni_name^" declared strong";
CIssue.suggestion = Some "In general delegates should be declared weak or assign";
CIssue.loc = location_from_dinfo decl_info
}
else None else None
(* GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL warning: a global variable initialization should not *) (* GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL warning: *)
(* a global variable initialization should not *)
(* contain calls to functions or methods as these can be expensive an delay the starting time *) (* contain calls to functions or methods as these can be expensive an delay the starting time *)
(* of an app *) (* of an app *)
let global_var_init_with_calls_warning _ decl = let global_var_init_with_calls_warning lcxt decl =
let decl_info, gvar = let condition, issue_desc = ctl_global_var_init_with_calls_warning decl in
match Clang_ast_proj.get_named_decl_tuple decl with if CTL.eval_formula condition (CTL.Decl decl) lcxt then
| Some (di, ndi) -> di, ndi.ni_name Some issue_desc
| None -> assert false (* we cannot be here *) in
let condition = General_utils.is_objc_extension
&& Ast_utils.is_syntactically_global_var decl
&& (not (Ast_utils.is_const_expr_var decl))
&& is_initialized_with_expensive_call decl in
if condition then
Some {
CIssue.issue = CIssue.Global_variable_initialized_with_function_or_method_call;
CIssue.description = "Global variable " ^ gvar ^
" is initialized using a function or method call";
CIssue.suggestion = Some
"If the function/method call is expensive, it can affect the starting time of the app.";
CIssue.loc = location_from_dinfo decl_info
}
else None else None
(* Direct Atomic Property access: (* Direct Atomic Property access:
a property declared atomic should not be accessed directly via its ivar *) a property declared atomic should not be accessed directly via its ivar *)
let direct_atomic_property_access_warning context stmt_info ivar_decl_ref = let direct_atomic_property_access_warning context stmt =
let ivar_pointer = ivar_decl_ref.Clang_ast_t.dr_decl_pointer in let condition, issue_desc = ctl_direct_atomic_property_access_warning stmt in
match Ast_utils.get_decl ivar_pointer, context.CLintersContext.current_method with if CTL.eval_formula condition (CTL.Stmt stmt) context then
| Some (ObjCIvarDecl (_, named_decl_info, _, _, _) as d), Some method_decl -> Some issue_desc
let method_name = match Clang_ast_proj.get_named_decl_tuple method_decl with else None
| Some (_, method_named_decl) -> method_named_decl.Clang_ast_t.ni_name
| _ -> "" in
let ivar_name = named_decl_info.Clang_ast_t.ni_name in
let condition =
(* We warn when:
(1) we are not inside a @synchronized block
(2) the property has the atomic attribute and
(3) the access of the ivar is not in a getter or setter method
(4) the access of the ivar is not in the init method
Last two conditions avoids false positives *)
not (context.CLintersContext.in_synchronized_block)
&& is_ivar_atomic (get_ivar_attributes d)
&& not (is_method_property_accessor_of_ivar method_decl ivar_pointer)
&& not (Procname.is_objc_constructor method_name)
&& not (Procname.is_objc_dealloc method_name) in
if condition then
Some {
CIssue.issue = CIssue.Direct_atomic_property_access;
CIssue.description = "Direct access to ivar " ^ ivar_name ^
" of an atomic property";
CIssue.suggestion =
Some "Accessing an ivar of an atomic property makes the property nonatomic";
CIssue.loc = location_from_sinfo stmt_info
}
else None
| _ -> None
(* CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK: C++ references (* CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK: C++ references
should not be captured in blocks. *) should not be captured in blocks. *)
let captured_cxx_ref_in_objc_block_warning _ stmt_info captured_vars = let captured_cxx_ref_in_objc_block_warning lcxt stmt =
let capt_refs = captured_variables_cxx_ref captured_vars in let condition, issue_desc = ctl_captured_cxx_ref_in_objc_block_warning stmt in
let var_descs = if CTL.eval_formula condition (CTL.Stmt stmt) lcxt then
let var_desc vars var_named_decl_info = Some issue_desc
vars ^ "'" ^ var_named_decl_info.Clang_ast_t.ni_name ^ "'" in
IList.fold_left var_desc "" capt_refs in
(* Fire if the list of captured references is not empty *)
let condition = IList.length capt_refs > 0 in
if condition then
Some {
CIssue.issue = CIssue.Cxx_reference_captured_in_objc_block;
CIssue.description = "C++ Reference variable(s) " ^ var_descs ^
" captured by Objective-C block";
CIssue.suggestion = Some ("C++ References are unmanaged and may be invalid " ^
"by the time the block executes.");
CIssue.loc = location_from_sinfo stmt_info
}
else None else None
@ -307,55 +283,8 @@ let bad_pointer_comparison_warning _ stmt_info stmts =
None None
(* exist m1: m1.body |- EF call_method(addObserver:) => let checker_NSNotificationCenter lcxt dec =
exists m2 : m2.body |- EF call_method(removeObserver:) *) let condition, issue_desc = ctl_ns_notification dec in
let checker_NSNotificationCenter _ decl_info impl_decl_info decls = if CTL.eval_formula condition (CTL.Decl dec) lcxt then
let exists_method_calling_addObserver = Some issue_desc
IList.exists
(dec_body_eventually (call_method_on_nth is_self 1)
"addObserver:selector:name:object:") decls in
let exists_method_calling_addObserverForName =
IList.exists
(dec_body_eventually (call_method_on_nth is_self 1)
"addObserverForName:object:queue:usingBlock:") decls in
let eventually_addObserver = exists_method_calling_addObserver
|| exists_method_calling_addObserverForName in
let eventually_removeObserver decls =
let exists_method_calling_removeObserver =
IList.exists (dec_body_eventually (call_method_on_nth is_self 1) "removeObserver:") decls in
let exists_method_calling_removeObserverName =
IList.exists
(dec_body_eventually (call_method_on_nth is_self 1)
"removeObserver:name:object:") decls in
exists_method_calling_removeObserver || exists_method_calling_removeObserverName in
let rec exists_on_hierarchy f super =
match super with
| Some (decl_list, impl_decl_info) ->
(f decl_list
|| exists_on_hierarchy f (Ast_utils.get_super_impl impl_decl_info))
| None -> false in
let eventually_removeObserver_in_whole_hierarchy decls impl_decl_info =
exists_on_hierarchy eventually_removeObserver (Some (decls, impl_decl_info)) in
(* if registration happens among the given decls, then search for removeObserver across the *)
(* whole hierarchy of classes *)
let condition =
eventually_addObserver &&
match impl_decl_info with
| Some idi ->
not (eventually_removeObserver_in_whole_hierarchy decls idi)
| None -> not (eventually_removeObserver decls) in
if condition then
Some {
CIssue.issue = CIssue.Registered_observer_being_deallocated;
CIssue.description =
Localise.registered_observer_being_deallocated_str CFrontend_config.self;
CIssue.suggestion =
Some "Consider removing the object from the notification center before its deallocation.";
CIssue.loc = location_from_dinfo decl_info
}
else None else None

16
infer/src/clang/cFrontend_checkers.mli
Unescape View File

@ -13,25 +13,21 @@ open! Utils
(* Strong Delegate Warning: a property with name delegate should not be declared strong *) (* Strong Delegate Warning: a property with name delegate should not be declared strong *)
val strong_delegate_warning : val strong_delegate_warning :
CLintersContext.context -> Clang_ast_t.decl_info -> Clang_ast_t.named_decl_info -> CLintersContext.context -> Clang_ast_t.decl -> CIssue.issue_desc option
Clang_ast_t.obj_c_property_decl_info -> CIssue.issue_desc option
(* Assing Pointer Warning: a property with a pointer type should not be declared `assign` *) (* Assing Pointer Warning: a property with a pointer type should not be declared `assign` *)
val assign_pointer_warning : val assign_pointer_warning :
CLintersContext.context -> Clang_ast_t.decl_info -> Clang_ast_t.named_decl_info -> CLintersContext.context -> Clang_ast_t.decl -> CIssue.issue_desc option
Clang_ast_t.obj_c_property_decl_info -> CIssue.issue_desc option
(* Direct Atomic Property access: (* Direct Atomic Property access:
a property declared atomic should not be accesses directly via its iva *) a property declared atomic should not be accesses directly via its iva *)
val direct_atomic_property_access_warning : val direct_atomic_property_access_warning :
CLintersContext.context -> Clang_ast_t.stmt_info -> Clang_ast_t.decl_ref -> CLintersContext.context -> Clang_ast_t.stmt -> CIssue.issue_desc option
CIssue.issue_desc option
(* CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK: C++ references (* CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK: C++ references
should not be captured in blocks. *) should not be captured in blocks. *)
val captured_cxx_ref_in_objc_block_warning : val captured_cxx_ref_in_objc_block_warning :
CLintersContext.context -> Clang_ast_t.stmt_info -> CLintersContext.context -> Clang_ast_t.stmt -> CIssue.issue_desc option
Clang_ast_t.block_captured_variable list -> CIssue.issue_desc option
val bad_pointer_comparison_warning : val bad_pointer_comparison_warning :
CLintersContext.context -> CLintersContext.context ->
@ -40,9 +36,7 @@ val bad_pointer_comparison_warning :
(* REGISTERED_OBSERVER_BEING_DEALLOCATED: an object is registered in a notification center (* REGISTERED_OBSERVER_BEING_DEALLOCATED: an object is registered in a notification center
but not removed before deallocation *) but not removed before deallocation *)
val checker_NSNotificationCenter : val checker_NSNotificationCenter :
CLintersContext.context -> CLintersContext.context -> Clang_ast_t.decl -> CIssue.issue_desc option
Clang_ast_t.decl_info -> Clang_ast_t.obj_c_implementation_decl_info option ->
Clang_ast_t.decl list -> CIssue.issue_desc option
(* GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL warning: a global variable initialization should not *) (* GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL warning: a global variable initialization should not *)
(* contain calls to functions or methods as these can be expensive an delay the starting time *) (* contain calls to functions or methods as these can be expensive an delay the starting time *)

38
infer/src/clang/cFrontend_errors.ml
Unescape View File

@ -16,29 +16,29 @@ let property_checkers_list = [CFrontend_checkers.strong_delegate_warning;
CFrontend_checkers.assign_pointer_warning;] CFrontend_checkers.assign_pointer_warning;]
(* Invocation of checker belonging to property_checker_list *) (* Invocation of checker belonging to property_checker_list *)
let checkers_for_property decl_info pname_info pdi checker context = let checkers_for_property decl checker context =
checker context decl_info pname_info pdi checker context decl
(* List of checkers on ivar access *) (* List of checkers on ivar access *)
let ivar_access_checker_list = [CFrontend_checkers.direct_atomic_property_access_warning] let ivar_access_checker_list = [CFrontend_checkers.direct_atomic_property_access_warning]
(* Invocation of checker belonging to ivar_access_checker_list *) (* Invocation of checker belonging to ivar_access_checker_list *)
let checkers_for_ivar stmt_info ivar_decl_ref checker context = let checkers_for_ivar stmt checker context =
checker context stmt_info ivar_decl_ref checker context stmt
(* List of checkers for captured vars in objc blocks *) (* List of checkers for captured vars in objc blocks *)
let captured_vars_checker_list = [CFrontend_checkers.captured_cxx_ref_in_objc_block_warning] let captured_vars_checker_list = [CFrontend_checkers.captured_cxx_ref_in_objc_block_warning]
(* Invocation of checker belonging to captured_vars_checker_list *) (* Invocation of checker belonging to captured_vars_checker_list *)
let checkers_for_capture_vars stmt_info captured_vars checker context = let checkers_for_capture_vars stmt checker context =
checker context stmt_info captured_vars checker context stmt
(* List of checkers on NSNotificationCenter *) (* List of checkers on NSNotificationCenter *)
let ns_notification_checker_list = [CFrontend_checkers.checker_NSNotificationCenter] let ns_notification_checker_list = [CFrontend_checkers.checker_NSNotificationCenter]
(* Invocation of checker belonging to ns_notification_center_list *) (* Invocation of checker belonging to ns_notification_center_list *)
let checkers_for_ns decl_info impl_decl_info decls checker context = let checkers_for_ns decl checker context =
checker context decl_info impl_decl_info decls checker context decl
(* List of checkers on variables *) (* List of checkers on variables *)
let var_checker_list = [CFrontend_checkers.global_var_init_with_calls_warning; let var_checker_list = [CFrontend_checkers.global_var_init_with_calls_warning;
@ -117,16 +117,14 @@ let invoke_set_of_checkers f context key checkers =
let run_frontend_checkers_on_stmt context instr = let run_frontend_checkers_on_stmt context instr =
let open Clang_ast_t in let open Clang_ast_t in
match instr with match instr with
| ObjCIvarRefExpr (stmt_info, _, _, obj_c_ivar_ref_expr_info) -> | ObjCIvarRefExpr _ ->
let dr_ref = obj_c_ivar_ref_expr_info.Clang_ast_t.ovrei_decl_ref in let call_checker_for_ivar = checkers_for_ivar instr in
let call_checker_for_ivar = checkers_for_ivar stmt_info dr_ref in
let key = Ast_utils.generate_key_stmt instr in let key = Ast_utils.generate_key_stmt instr in
invoke_set_of_checkers invoke_set_of_checkers
call_checker_for_ivar context key ivar_access_checker_list; call_checker_for_ivar context key ivar_access_checker_list;
context context
| BlockExpr (stmt_info, _ , _, Clang_ast_t.BlockDecl (_, block_decl_info)) -> | BlockExpr _ ->
let captured_block_vars = block_decl_info.Clang_ast_t.bdi_captured_variables in let call_captured_vars_checker = checkers_for_capture_vars instr in
let call_captured_vars_checker = checkers_for_capture_vars stmt_info captured_block_vars in
let key = Ast_utils.generate_key_stmt instr in let key = Ast_utils.generate_key_stmt instr in
invoke_set_of_checkers call_captured_vars_checker context key invoke_set_of_checkers call_captured_vars_checker context key
captured_vars_checker_list; captured_vars_checker_list;
@ -158,12 +156,8 @@ let run_frontend_checkers_on_stmt context instr =
let run_frontend_checkers_on_decl context dec = let run_frontend_checkers_on_decl context dec =
let open Clang_ast_t in let open Clang_ast_t in
match dec with match dec with
| ObjCImplementationDecl (decl_info, _, decl_list, _, _) | ObjCImplementationDecl _ | ObjCProtocolDecl _ ->
| ObjCProtocolDecl (decl_info, _, decl_list, _, _) -> let call_ns_checker = checkers_for_ns dec in
let idi = match dec with
| ObjCImplementationDecl (_, _, _, _, impl_decl_info) -> Some impl_decl_info
| _ -> None in
let call_ns_checker = checkers_for_ns decl_info idi decl_list in
let key = Ast_utils.generate_key_decl dec in let key = Ast_utils.generate_key_decl dec in
invoke_set_of_checkers call_ns_checker context key ns_notification_checker_list; invoke_set_of_checkers call_ns_checker context key ns_notification_checker_list;
context context
@ -172,8 +166,8 @@ let run_frontend_checkers_on_decl context dec =
let key = Ast_utils.generate_key_decl dec in let key = Ast_utils.generate_key_decl dec in
invoke_set_of_checkers call_var_checker context key var_checker_list; invoke_set_of_checkers call_var_checker context key var_checker_list;
context context
| ObjCPropertyDecl (decl_info, pname_info, pdi) -> | ObjCPropertyDecl _ ->
let call_property_checker = checkers_for_property decl_info pname_info pdi in let call_property_checker = checkers_for_property dec in
let key = Ast_utils.generate_key_decl dec in let key = Ast_utils.generate_key_decl dec in
invoke_set_of_checkers call_property_checker context key property_checkers_list; invoke_set_of_checkers call_property_checker context key property_checkers_list;
context context

18
infer/src/clang/cFrontend_utils.ml
Unescape View File

@ -419,6 +419,24 @@ struct
Some (decl_list, impl_decl_info) Some (decl_list, impl_decl_info)
| _ -> None | _ -> None
let get_super_ObjCImplementationDecl impl_decl_info =
let objc_interface_decl_current =
get_decl_opt_with_decl_ref
impl_decl_info.Clang_ast_t.oidi_class_interface in
let objc_interface_decl_super = get_super_if objc_interface_decl_current in
let objc_implementation_decl_super =
match objc_interface_decl_super with
| Some ObjCInterfaceDecl(_, _, _, _, interface_decl_info) ->
get_decl_opt_with_decl_ref
interface_decl_info.otdi_implementation
| _ -> None in
objc_implementation_decl_super
let get_impl_decl_info dec =
match dec with
| Clang_ast_t.ObjCImplementationDecl (_, _, _, _, idi) -> Some idi
| _ -> None
let is_in_main_file decl = let is_in_main_file decl =
let decl_info = Clang_ast_proj.get_decl_tuple decl in let decl_info = Clang_ast_proj.get_decl_tuple decl in
let file_opt = (fst decl_info.Clang_ast_t.di_source_range).Clang_ast_t.sl_file in let file_opt = (fst decl_info.Clang_ast_t.di_source_range).Clang_ast_t.sl_file in

6
infer/src/clang/cFrontend_utils.mli
Unescape View File

@ -141,6 +141,8 @@ sig
the superclass, if any. *) the superclass, if any. *)
val get_super_if : Clang_ast_t.decl option -> Clang_ast_t.decl option val get_super_if : Clang_ast_t.decl option -> Clang_ast_t.decl option
val get_impl_decl_info : Clang_ast_t.decl -> Clang_ast_t.obj_c_implementation_decl_info option
(** Given an objc impl decl info, return the super class's list of decls and (** Given an objc impl decl info, return the super class's list of decls and
its objc impl decl info. *) its objc impl decl info. *)
val get_super_impl : val get_super_impl :
@ -149,6 +151,10 @@ sig
Clang_ast_t.obj_c_implementation_decl_info) Clang_ast_t.obj_c_implementation_decl_info)
option option
(** Given an objc impl decl info, return its super class implementation decl *)
val get_super_ObjCImplementationDecl :
Clang_ast_t.obj_c_implementation_decl_info -> Clang_ast_t.decl option
(** Returns true if the declaration or statement is inside the main source (** Returns true if the declaration or statement is inside the main source
file, as opposed to an imported header file. For statements, this refers file, as opposed to an imported header file. For statements, this refers
to the parent decl. *) to the parent decl. *)

317
infer/src/clang/cTL.ml
Unescape View File

@ -0,0 +1,317 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
open CFrontend_utils
(* This module defines a language to define checkers. These checkers
are intepreted over the AST of the program. A checker is defined by a
CTL formula which express a condition saying when the checker should
report a problem *)
(* Label that allows switching from a decl node to a stmt node *)
type transition_decl_to_stmt =
| Body
| InitExpr
(* In formulas below prefix
"E" means "exists a path"
"A" means "for all path" *)
type t = (* A ctl formula *)
| True
| False (* not really necessary but it makes it evaluation faster *)
| Atomic of Predicates.t
| Not of t
| And of t * t
| Or of t * t
| Implies of t * t
| AX of t
| EX of t
| AF of t
| EF of t
| AG of t
| EG of t
| AU of t * t
| EU of t * t
| EH of string list * t
| ET of string list * transition_decl_to_stmt option * t
(* the kind of AST nodes where formulas are evaluated *)
type ast_node =
| Stmt of Clang_ast_t.stmt
| Decl of Clang_ast_t.decl
(* Helper functions *)
(* true iff an ast node is a node of type among the list tl *)
let node_has_type tl an =
let an_str = match an with
| Decl d -> Clang_ast_proj.get_decl_kind_string d
| Stmt s -> Clang_ast_proj.get_stmt_kind_string s in
IList.mem (string_equal) an_str tl
(* given a decl returns a stmt such that decl--->stmt via label trs *)
let transition_from_decl_to_stmt d trs =
let open Clang_ast_t in
match trs, d with
| Some Body, ObjCMethodDecl (_, _, omdi) -> omdi.omdi_body
| Some Body, FunctionDecl (_, _, _, fdi)
| Some Body, CXXMethodDecl (_, _, _, fdi,_ )
| Some Body, CXXConstructorDecl (_, _, _, fdi, _)
| Some Body, CXXConversionDecl (_, _, _, fdi, _)
| Some Body, CXXDestructorDecl (_, _, _, fdi, _) -> fdi.fdi_body
| Some Body, BlockDecl (_, bdi) -> bdi.bdi_body
| Some InitExpr, VarDecl (_, _ ,_, vdi) -> vdi.vdi_init_expr
| Some InitExpr, ObjCIvarDecl (_, _, _, fldi, _)
| Some InitExpr, FieldDecl (_, _, _, fldi)
| Some InitExpr, ObjCAtDefsFieldDecl (_, _, _, fldi)-> fldi.fldi_init_expr
| Some InitExpr, CXXMethodDecl _
| Some InitExpr, CXXConstructorDecl _
| Some InitExpr, CXXConversionDecl _
| Some InitExpr, CXXDestructorDecl _ ->
assert false (* to be done. Requires extending to lists *)
| Some InitExpr, EnumConstantDecl (_, _, _, ecdi) -> ecdi.ecdi_init_expr
| _, _ -> None
(* given a stmt returns a decl such that stmt--->decl via label trs
NOTE: for the moment we don't have any transitions stmt to decl as
we don't have much experience.
TBD: the list need to be populated when we know what we need *)
let transition_from_stmt_to_decl st trs =
match trs, st with
| _, _ -> None (* For the moment always no transitions. TBD add transitions *)
(* Evaluation of formulas *)
(* 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
| "is_objc_extension", [], _ -> Predicates.is_objc_extension
| "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_statement_kind", [p1], Stmt st -> Predicates.is_statement_kind st p1
| "is_declaration_kind", [p1], Decl d -> Predicates.is_declaration_kind d p1
| "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
| "context_in_synchronized_block", [], _ -> Predicates.context_in_synchronized_block lcxt
| "is_ivar_atomic", [], Stmt st -> Predicates.is_ivar_atomic st
| "is_method_property_accessor_of_ivar", [], Stmt st ->
Predicates.is_method_property_accessor_of_ivar st lcxt
| "is_objc_constructor", [], _ -> Predicates.is_objc_constructor lcxt
| "is_objc_dealloc", [], _ -> Predicates.is_objc_dealloc lcxt
| "captures_cxx_references", [], Stmt st -> Predicates.captures_cxx_references st
| _ -> failwith ("ERROR: Undefined Predicate: "^pred_name)
(* st, lcxt |= EF phi <=>
st, lcxt |= phi or exists st' in Successors(st): st', lcxt |= EF phi
That is: a (st, lcxt) satifies EF phi if and only if
either (st,lcxt) satifies phi or there is a child st' of the node st
such that (st', lcxt) satifies EF phi
*)
let rec eval_EF_st phi st lcxt =
Printing.log_out "\n->>>> Evaluating EF in %s\n"
(Clang_ast_proj.get_stmt_kind_string st);
let _, succs = Clang_ast_proj.get_stmt_tuple st in
(eval_formula phi (Stmt st) lcxt) ||
IList.exists (fun s -> eval_EF phi (Stmt s) lcxt) succs
(* dec, lcxt |= EF phi <=>
dec, lcxt |= phi or exists dec' in Successors(dec): dec', lcxt |= EF phi
This is as eval_EF_st but for decl.
*)
and eval_EF_decl phi dec lcxt =
Printing.log_out "\n->>>> Evaluating EF in %s\n"
(Clang_ast_proj.get_decl_kind_string dec);
(eval_formula phi (Decl dec) lcxt) ||
(match Clang_ast_proj.get_decl_context_tuple dec with
| Some (decl_list, _) ->
IList.exists (fun d -> eval_EF phi (Decl d) lcxt) decl_list
| None -> false)
(* an, lcxt |= EF phi evaluates on decl or stmt depending on an *)
and eval_EF phi an lcxt =
match an with
| Stmt st -> eval_EF_st phi st lcxt
| Decl dec -> eval_EF_decl phi dec lcxt
(* st, lcxt |= EX phi <=> exists st' in Successors(st): st', lcxt |= phi
That is: a (st, lcxt) satifies EX phi if and only if
there exists is a child st' of the node st
such that (st', lcxt) satifies phi
*)
and eval_EX_st phi st lcxt =
Printing.log_out "\n->>>> Evaluating EX in %s\n"
(Clang_ast_proj.get_stmt_kind_string st);
let _, succs = Clang_ast_proj.get_stmt_tuple st in
IList.exists (fun s -> eval_formula phi (Stmt s) lcxt) succs
(* dec, lcxt |= EX phi <=> exists dec' in Successors(dec): dec',lcxt|= phi
Same as eval_EX_st but for decl.
*)
and eval_EX_decl phi dec lcxt =
Printing.log_out "\n->>>> Evaluating EF in %s\n"
(Clang_ast_proj.get_decl_kind_string dec);
match Clang_ast_proj.get_decl_context_tuple dec with
| Some (decl_list, _) ->
IList.exists (fun d -> eval_formula phi (Decl d) lcxt) decl_list
| None -> false
(* an |= EX phi evaluates on decl/stmt depending on the ast_node an *)
and eval_EX phi an lcxt =
match an with
| Stmt st -> eval_EX_st phi st lcxt
| Decl decl -> eval_EX_decl phi decl lcxt
(* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence
an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2)))
That is: a (an,lcxt) satifies E(phi1 U phi2) if and only if
an,lcxt satifies the formula phi2 or (phi1 and EX(E(phi1 U phi2)))
*)
and eval_EU phi1 phi2 an lcxt =
let f = Or (phi2, And (phi1, EX (EU (phi1, phi2)))) in
eval_formula f an lcxt
(* an |= A(phi1 U phi2) evaluated using the equivalence
an |= A(phi1 U phi2) <=> an |= phi2 or (phi1 and AX(A(phi1 U phi2)))
Same as EU but for the all path quantifier A
*)
and eval_AU phi1 phi2 an lcxt =
let f = Or (phi2, And (phi1, AX (AU (phi1, phi2)))) in
eval_formula f an lcxt
(* Intuitive meaning: (an,lcxt) satifies EH[Classes] phi
if the node an is among the declaration specified by the list Classes and
there exists a super class in its hierarchy whose declaration satisfy phi.
an, lcxt |= EH[Classes] phi <=>
the node an is in Classes and there exists a declaration d in Hierarchy(an)
such that d,lcxt |= phi *)
and eval_EH classes phi an lcxt =
let rec eval_super impl_decl_info =
match impl_decl_info with
| Some idi ->
(match Ast_utils.get_super_ObjCImplementationDecl idi with
| Some (Clang_ast_t.ObjCImplementationDecl(_, _, _, _, idi') as d) ->
eval_formula phi (Decl d) lcxt
|| (eval_super (Some idi'))
| _ -> false)
| None -> false in
match an with
| Decl d when node_has_type classes (Decl d) ->
Printing.log_out "\n->>>> Evaluating EH in %s\n"
(Clang_ast_proj.get_decl_kind_string d);
eval_super (Ast_utils.get_impl_decl_info d)
| _ -> false
(* an, lcxt |= ET[T][->l]phi <=>
an is a node among those defined in T and an-l->an'
("an transitions" to another node an' via an edge labelled l)
such that an',lcxt |= phi
or an is a node among those defined in T, and l is unspecified,
and an,lcxt |= EF phi
or an is not of type in T and exists an' in Successors(an):
an', lcxt |= ET[T][->l]phi
*)
and eval_ET tl trs phi an lcxt =
let open Clang_ast_t in
let evaluate_on_subdeclarations d eval =
match Clang_ast_proj.get_decl_context_tuple d with
| None -> false
| Some (decl_list, _) ->
IList.exists (fun d' -> eval phi (Decl d') lcxt) decl_list in
let evaluate_on_substmt st eval =
let _, stmt_list = Clang_ast_proj.get_stmt_tuple st in
IList.exists (fun s -> eval phi (Stmt s) lcxt) stmt_list in
let do_decl d =
Printing.log_out "\n->>>> Evaluating ET in %s\n"
(Clang_ast_proj.get_decl_kind_string d);
match trs, node_has_type tl (Decl d) with
| Some _, true ->
Printing.log_out "\n ->>>> Declaration is in types and has label";
(match transition_from_decl_to_stmt d trs with
| None ->
Printing.log_out "\n ->>>> NO transition returned";
false
| Some st ->
Printing.log_out "\n ->>>> A transition is returned \n";
eval_formula phi (Stmt st) lcxt)
| None, true ->
Printing.log_out "\n ->>>> Declaration has NO transition label\n";
eval_EF_decl phi d lcxt
| _, false ->
Printing.log_out "\n ->>>> Declaration is NOT in types and _ label\n";
evaluate_on_subdeclarations d (eval_ET tl trs) in
let do_stmt st =
Printing.log_out "\n->>>> Evaluating ET in %s\n"
(Clang_ast_proj.get_stmt_kind_string st);
match trs, node_has_type tl (Stmt st) with
| Some _, true ->
Printing.log_out "\n ->>>> Statement is in types and has label";
(match transition_from_stmt_to_decl st trs with
| None ->
Printing.log_out "\n ->>>> NO transition returned\n";
false
| Some d ->
Printing.log_out "\n ->>>> A transition is returned \n";
eval_formula phi (Decl d) lcxt)
| None, true ->
Printing.log_out "\n ->>>> Statement has NO transition label\n";
eval_EF_st phi st lcxt
| _, false ->
Printing.log_out "\n ->>>> Declaration is NOT in types and _ label\n";
evaluate_on_substmt st (eval_ET tl trs) in
match an with
| Decl d -> do_decl d
| Stmt BlockExpr(_, _, _, d) ->
(* From BlockExpr we jump directly to its BlockDecl *)
Printing.log_out "\n->>>> BlockExpr evaluated in ET, evaluating its BlockDecl \n";
eval_ET tl trs phi (Decl d) lcxt
| Stmt st -> do_stmt st
(* Formulas are evaluated on a AST node an and a linter context lcxt *)
and eval_formula f an lcxt =
match f with
| True -> true
| False -> false
| Atomic (name, params) -> eval_Atomic name params an lcxt
| Not f1 -> not (eval_formula f1 an lcxt)
| And (f1, f2) -> (eval_formula f1 an lcxt) && (eval_formula f2 an lcxt)
| Or (f1, f2) -> (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt)
| Implies (f1, f2) ->
not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt)
| AU (f1, f2) -> eval_AU f1 f2 an lcxt
| EU (f1, f2) -> eval_EU f1 f2 an lcxt
| EF f1 -> eval_EF f1 an lcxt
| AF f1 -> eval_formula (AU (True, f1)) an lcxt
| AG f1 -> eval_formula (Not (EF (Not f1))) an lcxt
| EX f1 -> eval_EX f1 an lcxt
| AX f1 -> eval_formula (Not (EX (Not f1))) an lcxt
| EH (cl, phi) -> eval_EH cl phi an lcxt
| EG f1 -> (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *)
eval_formula (And (f1, EX (EG (f1)))) an lcxt
| ET (tl, sw, phi) -> eval_ET tl sw phi an lcxt

56
infer/src/clang/cTL.mli
Unescape View File

@ -0,0 +1,56 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
(* This module defines a language to define checkers. These checkers
are intepreted over the AST of the program. A checker is defined by a
CTL formula which express a condition saying when the checker should
report a problem *)
type transition_decl_to_stmt =
| Body
| InitExpr
(* In formulas below prefix
"E" means "exists a path"
"A" means "for all path" *)
(** A ctl formula *)
type t =
| True
| False
| Atomic of Predicates.t (** Atomic formula *)
| Not of t
| And of t * t
| Or of t * t
| Implies of t * t
| AX of t (** AX phi <=> for all children of the current node phi holds *)
| EX of t (** EX phi <=> exist a child of the current node such that phi holds *)
| AF of t (** AF phi <=> for all path from the current node there is a descendant where phi holds *)
| EF of t (** EF phi <=> there exits a a path from the current node with a descendant where phi hold *)
| AG of t (** AG phi <=> for all discendant of the current node phi hold *)
| EG of t (** EG phi <=>
there exists a path (of descendants) from the current node where phi hold at each node of the path *)
| AU of t * t (** AU(phi1, phi2) <=>
for all paths from the current node phi1 holds in every node until ph2 holds *)
| EU of t * t (** EU(phi1, phi2) <=>
there exists a path from the current node such that phi1 holds until phi2 holds *)
| EH of string list * t (** EH[classes]phi <=>
there exists a node defining a super class in the hierarchy of the class
defined by the current node (if any) where phi holds *)
| ET of string list * transition_decl_to_stmt option * t (** ET[T][l] phi <=>
there exists a descentant an of the current node such that an is of type in set T
making a transition to a node an' via label l, such that in an phi holds. *)
(** the kind of AST nodes where formulas are evaluated *)
type ast_node =
| Stmt of Clang_ast_t.stmt
| Decl of Clang_ast_t.decl
val eval_formula : t -> ast_node -> CLintersContext.context -> bool

175
infer/src/clang/predicates.ml
Unescape View File

@ -0,0 +1,175 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
open CFrontend_utils
let get_ivar_attributes ivar_decl =
let open Clang_ast_t in
match ivar_decl with
| ObjCIvarDecl (ivar_decl_info, _, _, _, _) ->
(match Ast_utils.get_property_of_ivar ivar_decl_info.Clang_ast_t.di_pointer with
| Some ObjCPropertyDecl (_, _, obj_c_property_decl_info) ->
obj_c_property_decl_info.Clang_ast_t.opdi_property_attributes
| _ -> [])
| _ -> []
(* list of cxx references captured by stmt *)
let captured_variables_cxx_ref stmt =
let capture_var_is_cxx_ref reference_captured_vars captured_var =
let decl_ref_opt = captured_var.Clang_ast_t.bcv_variable in
match Ast_utils.get_decl_opt_with_decl_ref decl_ref_opt with
| Some VarDecl (_, named_decl_info, qual_type, _)
| Some ParmVarDecl (_, named_decl_info, qual_type, _)
| Some ImplicitParamDecl (_, named_decl_info, qual_type, _) ->
(match Ast_utils.get_desugared_type qual_type.Clang_ast_t.qt_type_ptr with
| Some RValueReferenceType _ | Some LValueReferenceType _ ->
named_decl_info::reference_captured_vars
| _ -> reference_captured_vars)
| _ -> reference_captured_vars in
let captured_vars = match stmt with
| Clang_ast_t.BlockExpr (_, _ , _, Clang_ast_t.BlockDecl (_, bdi)) ->
bdi.Clang_ast_t.bdi_captured_variables
| _ -> [] in
IList.fold_left capture_var_is_cxx_ref [] captured_vars
let var_descs_name stmt =
let capt_refs = captured_variables_cxx_ref stmt in
let var_desc vars var_named_decl_info =
vars ^ "'" ^ var_named_decl_info.Clang_ast_t.ni_name ^ "'" in
IList.fold_left var_desc "" capt_refs
type t = string * string list (* (name, [param1,...,paramK]) *)
let is_declaration_kind decl s =
Clang_ast_proj.get_decl_kind_string decl = s
let is_statement_kind stmt s =
Clang_ast_proj.get_stmt_kind_string stmt = s
(* st |= call_method(m) *)
let call_method m st =
match st with
| Clang_ast_t.ObjCMessageExpr (_, _, _, omei) -> omei.omei_selector = m
| _ -> false
let property_name_contains_word decl word =
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
(try
Str.search_forward rexp pname 0 >= 0
with Not_found -> false)
| _ -> false
let is_objc_extension = General_utils.is_objc_extension
let is_syntactically_global_var decl =
Ast_utils.is_syntactically_global_var decl
let is_const_expr_var decl =
Ast_utils.is_const_expr_var decl
let decl_ref_is_in names st =
match st with
| Clang_ast_t.DeclRefExpr (_, _, _, drti) ->
(match drti.drti_decl_ref with
| Some dr -> let ndi, _, _ = CFrontend_utils.Ast_utils.get_info_from_decl_ref dr in
IList.exists (fun n -> n = ndi.ni_name) names
| _ -> false)
| _ -> false
let call_function_named st names =
Ast_utils.exists_eventually_st decl_ref_is_in names st
let is_strong_property decl =
match decl with
| Clang_ast_t.ObjCPropertyDecl (_, _, pdi) ->
ObjcProperty_decl.is_strong_property pdi
| _ -> false
let is_assign_property decl =
match decl with
| Clang_ast_t.ObjCPropertyDecl (_, _, pdi) ->
ObjcProperty_decl.is_assign_property pdi
| _ -> false
let is_property_pointer_type decl =
match decl with
| Clang_ast_t.ObjCPropertyDecl (_, _, pdi) ->
let type_ptr = pdi.opdi_type_ptr in
let raw_ptr = Clang_ast_types.type_ptr_to_clang_pointer type_ptr in
(match Clang_ast_main.PointerMap.find raw_ptr !CFrontend_config.pointer_type_index with
| MemberPointerType _ | ObjCObjectPointerType _ | BlockPointerType _ -> true
| TypedefType (_, tti) ->
(Ast_utils.name_of_typedef_type_info tti) = CFrontend_config.id_cl
| exception Not_found -> false
| _ -> false)
| _ -> false
let context_in_synchronized_block context =
context.CLintersContext.in_synchronized_block
(* checks if ivar is defined among a set of fields and if it is atomic *)
let is_ivar_atomic stmt =
match stmt with
| Clang_ast_t.ObjCIvarRefExpr (_, _, _, irei) ->
let dr_ref = irei.Clang_ast_t.ovrei_decl_ref in
let ivar_pointer = dr_ref.Clang_ast_t.dr_decl_pointer in
(match Ast_utils.get_decl ivar_pointer with
| Some d ->
let attributes = get_ivar_attributes d in
IList.exists (Ast_utils.property_attribute_eq `Atomic) attributes
| _ -> false)
| _ -> false
let is_method_property_accessor_of_ivar stmt context =
let open Clang_ast_t in
match stmt with
| ObjCIvarRefExpr (_, _, _, irei) ->
let dr_ref = irei.Clang_ast_t.ovrei_decl_ref in
let ivar_pointer = dr_ref.Clang_ast_t.dr_decl_pointer in
(match context.CLintersContext.current_method with
| Some ObjCMethodDecl (_, _, mdi) ->
if mdi.omdi_is_property_accessor then
let property_opt = mdi.omdi_property_decl in
match Ast_utils.get_decl_opt_with_decl_ref property_opt with
| Some ObjCPropertyDecl (_, _, pdi) ->
(match pdi.opdi_ivar_decl with
| Some decl_ref -> decl_ref.dr_decl_pointer = ivar_pointer
| None -> false)
| _ -> false
else false
| _ -> false)
| _ -> false
let is_objc_constructor context =
match context.CLintersContext.current_method with
| Some method_decl ->
let method_name = (match Clang_ast_proj.get_named_decl_tuple method_decl with
| Some (_, mnd) -> mnd.Clang_ast_t.ni_name
| _ -> "") in
Procname.is_objc_constructor method_name
| _ -> false
let is_objc_dealloc context =
match context.CLintersContext.current_method with
| Some method_decl ->
let method_name = (match Clang_ast_proj.get_named_decl_tuple method_decl with
| Some (_, mnd) -> mnd.Clang_ast_t.ni_name
| _ -> "") in
Procname.is_objc_dealloc method_name
| _ -> false
let captures_cxx_references stmt =
IList.length (captured_variables_cxx_ref stmt) > 0

46
infer/src/clang/predicates.mli
Unescape View File

@ -0,0 +1,46 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
type t = string * string list (* (name, [param1,...,paramK]) *)
val var_descs_name : Clang_ast_t.stmt -> string (* Helper function *)
val call_method : string -> Clang_ast_t.stmt -> bool
val property_name_contains_word : Clang_ast_t.decl -> string -> bool
val is_objc_extension : bool
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 is_statement_kind : Clang_ast_t.stmt -> string -> bool
val call_function_named : Clang_ast_t.stmt -> string list -> bool
val is_strong_property : Clang_ast_t.decl -> bool
val is_assign_property : Clang_ast_t.decl -> bool
val is_property_pointer_type : Clang_ast_t.decl -> bool
val context_in_synchronized_block : CLintersContext.context -> bool
val is_ivar_atomic : Clang_ast_t.stmt -> bool
val is_method_property_accessor_of_ivar : Clang_ast_t.stmt -> CLintersContext.context -> bool
val is_objc_constructor : CLintersContext.context -> bool
val is_objc_dealloc : CLintersContext.context -> bool
val captures_cxx_references : Clang_ast_t.stmt -> bool
Write Preview
Loading…
Cancel
Save