From ddec46d4aa1a3b46d82aace1a8c4b1218f61bd73 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 19 Jun 2015 14:50:17 -0100 Subject: [PATCH] [infer] add infrastructure for function attributes in sil and clang Summary: @public This adds basic support for function attributes in Sil, and for translating attributes from the clang frontend to these new Sil attributes. For now only the sentinel attribute is translated. Note that attributes normally have parameters, but they are currently missing from the clang plugin. Test Plan: Add (match Sil.get_sentinel_func_attribute_value (Cfg.Procdesc.get_attributes callee_pdesc).Sil.func_attributes with | Some _ -> L.out "found sentinel attribute!\n" | _ -> ()); between lines 947 and 948 of symbExec.ml, then analyze a file containing: int add_all_ints(int a, ...) __attribute__ ((sentinel)); int foo(void) { return add_all_ints(1, 2, 3, (void *)0); } then `grep 'found sentinel' infer-out/log/analyzer_out` -> the sentinel attribute is correctly passed from the frontend to the backend. --- infer/src/backend/cfg.mli | 2 +- infer/src/backend/sil.ml | 14 ++++++++++++++ infer/src/backend/sil.mli | 7 +++++++ infer/src/backend/specs.ml | 1 + infer/src/clang/cEnum_decl.ml | 1 + infer/src/clang/cMethod_decl.ml | 7 +++++-- infer/src/clang/cMethod_signature.ml | 15 +++++++-------- infer/src/clang/cMethod_signature.mli | 6 ++++-- infer/src/clang/cMethod_trans.ml | 13 +++++++++++++ infer/src/clang/cTrans_models.ml | 12 ++++++------ infer/src/harness/inhabit.ml | 2 ++ infer/src/java/jTrans.ml | 4 ++++ 12 files changed, 65 insertions(+), 19 deletions(-) diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index eb65748e6..2dfddca99 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -322,4 +322,4 @@ val check_cfg_connectedness : cfg -> unit val get_block_pdesc : cfg -> Mangled.t -> Procdesc.t option (** Removes seeds variables from a prop corresponding to captured variables in an objc block *) -val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Prop.normal Prop.t \ No newline at end of file +val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Prop.normal Prop.t diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index bfccc815a..2a4b3dbf4 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -24,6 +24,9 @@ type item_annotation = (annotation * bool) list type method_annotation = item_annotation * item_annotation list +type func_attribute = + | FA_sentinel of int * int (** __attribute__((sentinel(int, int))) *) + (** Programming language. *) type language = C_CPP | Java @@ -40,6 +43,7 @@ type proc_attributes = is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) language : language; + func_attributes : func_attribute list; method_annotation : method_annotation; } @@ -52,6 +56,7 @@ let copy_proc_attributes pa = is_objc_instance_method = pa.is_objc_instance_method; is_synthetic_method = pa.is_synthetic_method; language = pa.language; + func_attributes = pa.func_attributes; method_annotation = pa.method_annotation; } @@ -100,6 +105,15 @@ let pp_item_annotation fmt item_annotation = let pp_method_annotation s fmt (ia, ial) = F.fprintf fmt "%a %s(%a)" pp_item_annotation ia s (pp_seq pp_item_annotation) ial +(** Return the value of the FA_sentinel attribute in [attr_list] if it is found *) +let get_sentinel_func_attribute_value attr_list = + (* Sentinel is the only kind of attributes *) + let is_sentinel a = true in + try + match list_find is_sentinel attr_list with + | FA_sentinel (sentinel, null_pos) -> Some (sentinel, null_pos) + with Not_found -> None + (** current language *) let curr_language = ref C_CPP diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index c589d1800..8906163da 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -43,6 +43,9 @@ type item_annotation = (annotation * bool) list type method_annotation = item_annotation * item_annotation list +type func_attribute = + | FA_sentinel of int * int + (** Visibility modifiers. *) type access = Default | Public | Private | Protected @@ -56,6 +59,7 @@ type proc_attributes = is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) language : language; + func_attributes : func_attribute list; method_annotation : method_annotation; } @@ -783,6 +787,9 @@ val item_annotation_is_empty : item_annotation -> bool (** Check if the method annodation is empty. *) val method_annotation_is_empty : method_annotation -> bool +(** Return the value of the FA_sentinel attribute in [attr_list] if it is found *) +val get_sentinel_func_attribute_value : func_attribute list -> (int * int) option + (** {2 Pretty Printing} *) (** Begin change color if using diff printing, return updated printenv and change status *) diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index e491e900c..1350cac1a 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -775,6 +775,7 @@ let reset_summary call_graph proc_name loc = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = false; Sil.language = !Sil.curr_language; + Sil.func_attributes = []; Sil.method_annotation = Sil.method_annotation_empty; } in init_summary ( diff --git a/infer/src/clang/cEnum_decl.ml b/infer/src/clang/cEnum_decl.ml index c1466c654..76651640a 100644 --- a/infer/src/clang/cEnum_decl.ml +++ b/infer/src/clang/cEnum_decl.ml @@ -21,6 +21,7 @@ let create_empty_procdesc () = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = false; Sil.language = Sil.C_CPP; + Sil.func_attributes = []; Sil.method_annotation = Sil.method_annotation_empty; } in create { diff --git a/infer/src/clang/cMethod_decl.ml b/infer/src/clang/cMethod_decl.ml index 68fe27db6..ffcc1f79c 100644 --- a/infer/src/clang/cMethod_decl.ml +++ b/infer/src/clang/cMethod_decl.ml @@ -73,7 +73,8 @@ struct let qt = get_return_type function_method_decl_info in let is_instance_method = is_instance_method function_method_decl_info is_instance is_anonym_block in let parameters = get_parameters function_method_decl_info in - CMethod_signature.make_ms procname parameters qt source_range is_instance_method + let attributes = decl_info.Clang_ast_t.di_attributes in + CMethod_signature.make_ms procname parameters qt attributes source_range is_instance_method let create_function_signature di fdecl_info name qt is_instance anonym_block_opt = let procname, is_anonym_block = @@ -140,7 +141,9 @@ struct let curr_class = if is_anonym_block then curr_class else CContext.ContextNoCls in add_method tenv cg cfg curr_class procname namespace [body] is_objc_method is_instance captured_vars is_anonym_block - | None, ms -> CMethod_signature.add ms + | None, ms -> + CMethod_trans.create_local_procdesc cfg tenv ms [] captured_vars false; + CMethod_signature.add ms let process_objc_method_decl tenv cg cfg namespace curr_class decl_info method_name method_decl_info = let class_name = CContext.get_curr_class_name curr_class in diff --git a/infer/src/clang/cMethod_signature.ml b/infer/src/clang/cMethod_signature.ml index ac14d9e08..2ceb99d1c 100644 --- a/infer/src/clang/cMethod_signature.ml +++ b/infer/src/clang/cMethod_signature.ml @@ -10,6 +10,7 @@ type method_signature = { _name : Procname.t; _args : (string * string) list; (* (name, type) *) _ret_type : string; + _attributes : Clang_ast_t.attribute list; _loc : Clang_ast_t.source_range; _is_instance : bool } @@ -23,6 +24,9 @@ let ms_get_args ms = let ms_get_ret_type ms = ms._ret_type +let ms_get_attributes ms = + ms._attributes + let ms_get_loc ms = ms._loc @@ -33,23 +37,18 @@ type methodMap = method_signature Procname.Map.t let methodMap = ref Procname.Map.empty -let make_ms procname args ret_type loc is_instance = +let make_ms procname args ret_type attributes loc is_instance = let meth_signature = { _name = procname; _args = args; _ret_type = ret_type; + _attributes = attributes; _loc = loc; _is_instance = is_instance } in meth_signature let replace_name_ms ms name = - let meth_signature = { - _name = name; - _args = ms._args; - _ret_type = ms._ret_type; - _loc = ms._loc; - _is_instance = ms._is_instance } in - meth_signature + { ms with _name = name } let ms_to_string ms = "Method "^(Procname.to_string ms._name)^" "^ diff --git a/infer/src/clang/cMethod_signature.mli b/infer/src/clang/cMethod_signature.mli index 01e777e97..d10ee122c 100644 --- a/infer/src/clang/cMethod_signature.mli +++ b/infer/src/clang/cMethod_signature.mli @@ -20,12 +20,14 @@ val ms_get_args : method_signature -> (string * string) list val ms_get_ret_type : method_signature -> string +val ms_get_attributes : method_signature -> Clang_ast_t.attribute list + val ms_get_loc : method_signature -> Clang_ast_t.source_range val ms_is_instance : method_signature -> bool -val make_ms : Procname.t -> (string * string) list -> string -> Clang_ast_t.source_range -> -bool -> method_signature +val make_ms : Procname.t -> (string * string) list -> string -> Clang_ast_t.attribute list -> +Clang_ast_t.source_range -> bool -> method_signature val replace_name_ms : method_signature -> Procname.t -> method_signature diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 245159e9f..6593cd52e 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -129,11 +129,22 @@ let get_return_type tenv ms = CTypes_decl.qual_type_to_sil_type tenv (Ast_expressions.create_qual_type (CTypes.get_function_return_type qt)) +let sil_func_attributes_of_attributes attrs = + let rec do_translation acc al = match al with + | [] -> list_rev acc + | Clang_ast_t.SentinelAttr attribute_info::tl -> + (* TODO(t7466561) right now the clang plugin does not emit attribute arguments *) + (* so we default to (0,0) --the default sentinel values. *) + do_translation (Sil.FA_sentinel(0,0)::acc) tl + | _::tl -> do_translation acc tl in + do_translation [] attrs + (** Creates a procedure description. *) let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let defined = not ((list_length fbody) == 0) in let procname = CMethod_signature.ms_get_name ms in let pname = Procname.to_string procname in + let attributes = sil_func_attributes_of_attributes (CMethod_signature.ms_get_attributes ms) in let create_new_procdesc () = let formals = get_formal_parameters tenv ms in let captured_str = list_map (fun (s, t, _) -> (Mangled.to_string s, t)) captured in @@ -159,6 +170,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = Sil.is_objc_instance_method = is_objc_inst_method; Sil.is_synthetic_method = false; Sil.language = Sil.C_CPP; + Sil.func_attributes = attributes; Sil.method_annotation = Sil.method_annotation_empty; } in create { @@ -211,6 +223,7 @@ let create_external_procdesc cfg procname is_objc_inst_method type_opt = Sil.is_objc_instance_method = is_objc_inst_method; Sil.is_synthetic_method = false; Sil.language = Sil.C_CPP; + Sil.func_attributes = []; Sil.method_annotation = Sil.method_annotation_empty; } in create { diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml index fd906bee7..40c1e844f 100644 --- a/infer/src/clang/cTrans_models.ml +++ b/infer/src/clang/cTrans_models.ml @@ -117,13 +117,13 @@ let is_objc_memory_model_controlled o = Core_foundation_model.is_objc_memory_model_controlled o let get_predefined_ms_method condition class_name method_name mk_procname - arguments return_type builtin = + arguments return_type attributes builtin = if condition then let procname = match builtin with | Some procname -> procname | None -> mk_procname class_name method_name in - let ms = CMethod_signature.make_ms procname arguments return_type + let ms = CMethod_signature.make_ms procname arguments return_type attributes (Ast_expressions.dummy_source_range ()) false in Some ms else None @@ -131,7 +131,7 @@ let get_predefined_ms_method condition class_name method_name mk_procname let get_predefined_ms_stringWithUTF8String class_name method_name mk_procname = let condition = class_name = nsstring_cl && method_name = string_with_utf8_m in get_predefined_ms_method condition class_name method_name mk_procname [("x", "char *")] - id_cl None + id_cl [] None let get_predefined_ms_retain_release class_name method_name mk_procname = let condition = is_retain_or_release method_name in @@ -139,18 +139,18 @@ let get_predefined_ms_retain_release class_name method_name mk_procname = if is_retain_method method_name || is_autorelease_method method_name then id_cl else void in get_predefined_ms_method condition nsobject_cl method_name mk_procname - [(self, class_name)] return_type (get_builtinname method_name) + [(self, class_name)] return_type [] (get_builtinname method_name) let get_predefined_ms_autoreleasepool_init class_name method_name mk_procname = let condition = (method_name = init) && (class_name = nsautorelease_pool_cl) in get_predefined_ms_method condition class_name method_name mk_procname - [(self, class_name)] void None + [(self, class_name)] void [] None let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procname = let condition = (method_name = release || method_name = drain) && (class_name = nsautorelease_pool_cl) in get_predefined_ms_method condition class_name method_name mk_procname [(self, class_name)] - void (Some SymExec.ModelBuiltins.__objc_release_autorelease_pool) + void [] (Some SymExec.ModelBuiltins.__objc_release_autorelease_pool) let get_predefined_model_method_signature class_name method_name mk_procname = match get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procname with diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index b06b6c940..381fdc4b6 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -285,6 +285,7 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = false; Sil.language = Sil.Java; + Sil.func_attributes = []; Sil.method_annotation = Sil.method_annotation_empty; } in create { @@ -335,6 +336,7 @@ let setup_harness_cfg harness_name harness_cfg env proc_file_map tenv = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = false; Sil.language = Sil.Java; + Sil.func_attributes = []; Sil.method_annotation = Sil.method_annotation_empty; } in create { diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index f87f70805..26329e849 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -295,6 +295,7 @@ let create_local_procdesc program linereader cfg tenv node m = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = am.Javalib.am_synthetic; Sil.language = Sil.Java; + Sil.func_attributes = []; Sil.method_annotation = method_annotation; } in create { @@ -329,6 +330,7 @@ let create_local_procdesc program linereader cfg tenv node m = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = cm.Javalib.cm_synthetic; Sil.language = Sil.Java; + Sil.func_attributes = []; Sil.method_annotation = method_annotation; } in create { @@ -364,6 +366,7 @@ let create_local_procdesc program linereader cfg tenv node m = Sil.is_objc_instance_method = false; Sil.is_synthetic_method = cm.Javalib.cm_synthetic; Sil.language = Sil.Java; + Sil.func_attributes = []; Sil.method_annotation = method_annotation; } in create { @@ -418,6 +421,7 @@ let create_external_procdesc program cfg tenv cn ms method_annotation is_static Sil.is_objc_instance_method = false; Sil.is_synthetic_method = false; Sil.language = Sil.Java; + Sil.func_attributes = []; Sil.method_annotation = method_annotation; } in create {