From 4bca15afff7a5264e7d2eb05174382d04652e4b4 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 21 Dec 2016 11:10:00 -0800 Subject: [PATCH] [infer][backend] Add the distinction between models and regular procedure as part of the attributes Summary: Adding the information that a procedure has been modelled as part of the attributes, during the translation, instead of getting this information from where is the summary loaded from. This is more consistent with the use of the attributes in other parts of the analysis, but is also useful in the context of the lazy dynamic dispatch algorithm where the procedures, including the models, are cloned and reanalyzed with more specialized parameters. The information about whether a procedure is a model must persist when cloning the procedures. Reviewed By: sblackshear Differential Revision: D4356892 fbshipit-source-id: 40ff5ca --- infer/src/IR/AttributesTable.re | 9 --------- infer/src/IR/AttributesTable.rei | 4 ---- infer/src/IR/ProcAttributes.re | 2 ++ infer/src/IR/ProcAttributes.rei | 1 + infer/src/backend/tabulation.ml | 6 +++++- infer/src/clang/cMethod_trans.ml | 1 + infer/src/java/jTrans.ml | 3 +++ 7 files changed, 12 insertions(+), 14 deletions(-) diff --git a/infer/src/IR/AttributesTable.re b/infer/src/IR/AttributesTable.re index 5ab5e115f..d04fecf8c 100644 --- a/infer/src/IR/AttributesTable.re +++ b/infer/src/IR/AttributesTable.re @@ -135,15 +135,6 @@ let get_correct_type_from_objc_class_name type_name => */ Some (Typ.Tstruct type_name); - -/** Returns true if the method is defined under project root */ -let pname_is_under_project_root callee_pname => - switch (load_attributes callee_pname) { - | Some attrs => SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file - | None => false - }; - - type t = { num_bindings: int, num_buckets: int, diff --git a/infer/src/IR/AttributesTable.rei b/infer/src/IR/AttributesTable.rei index 3ed080c44..1f5dd0a49 100644 --- a/infer/src/IR/AttributesTable.rei +++ b/infer/src/IR/AttributesTable.rei @@ -28,10 +28,6 @@ let load_defined_attributes: cache_none::bool => Procname.t => option ProcAttrib corresponds to the class definition. */ let get_correct_type_from_objc_class_name: Typename.t => option Typ.t; - -/** Returns true if the method is defined under project root */ -let pname_is_under_project_root: Procname.t => bool; - /* Find the file where the procedure was captured, if a cfg for that file exists. Return also a boolean indicating whether the procedure is defined in an include file. */ diff --git a/infer/src/IR/ProcAttributes.re b/infer/src/IR/ProcAttributes.re index 866586f9a..35addfef1 100644 --- a/infer/src/IR/ProcAttributes.re +++ b/infer/src/IR/ProcAttributes.re @@ -58,6 +58,7 @@ type t = { is_objc_instance_method: bool, /** the procedure is an objective-C instance method */ is_cpp_instance_method: bool, /** the procedure is an C++ instance method */ is_java_synchronized_method: bool, /** the procedure is a Java synchronized method */ + is_model: bool, /** the procedure is a model */ is_synthetic_method: bool, /** the procedure is a synthetic method */ language: Config.language, /** language of the procedure */ loc: Location.t, /** location of this procedure in the source code */ @@ -88,6 +89,7 @@ let default proc_name language => { is_java_synchronized_method: false, is_defined: false, is_objc_instance_method: false, + is_model: false, is_synthetic_method: false, language, loc: Location.dummy, diff --git a/infer/src/IR/ProcAttributes.rei b/infer/src/IR/ProcAttributes.rei index 766cd8a41..3babb7945 100644 --- a/infer/src/IR/ProcAttributes.rei +++ b/infer/src/IR/ProcAttributes.rei @@ -53,6 +53,7 @@ type t = { is_objc_instance_method: bool, /** the procedure is an objective-C instance method */ is_cpp_instance_method: bool, /** the procedure is an C++ instance method */ is_java_synchronized_method: bool, /** the procedure is a Java synchronized method */ + is_model: bool, /** the procedure is a model */ is_synthetic_method: bool, /** the procedure is a synthetic method */ language: Config.language, /** language of the procedure */ loc: Location.t, /** location of this procedure in the source code */ diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 80c40f467..37434cf10 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -664,7 +664,11 @@ let prop_set_exn tenv pname prop se_exn = (** Include a subtrace for a procedure call if the callee is not a model. *) let include_subtrace callee_pname = - not (Specs.is_model callee_pname) && (AttributesTable.pname_is_under_project_root callee_pname) + match Specs.proc_resolve_attributes callee_pname with + | Some attrs -> + not attrs.ProcAttributes.is_model + && (SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file) + | None -> false (** combine the spec's post with a splitting and actual precondition *) let combine tenv diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index c0dcf8a9f..837af77a5 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -413,6 +413,7 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst is_defined = defined; is_objc_instance_method = is_objc_inst_method; is_cpp_instance_method = is_cpp_inst_method; + is_model = Config.models_mode; loc = loc_start; translation_unit = Some trans_unit_ctx.CFrontend_config.source_file; method_annotation; diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 5941d6f83..0549f3fae 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -291,6 +291,7 @@ let create_am_procdesc program icfg am proc_name : Procdesc.t = is_abstract = true; is_bridge_method = am.Javalib.am_bridge; is_defined = true; + is_model = Config.models_mode; is_synthetic_method = am.Javalib.am_synthetic; method_annotation; ret_type = JTransType.return_type program tenv ms; @@ -320,6 +321,7 @@ let create_native_procdesc program icfg cm proc_name = exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; formals; is_bridge_method = cm.Javalib.cm_bridge; + is_model = Config.models_mode; is_synthetic_method = cm.Javalib.cm_synthetic; method_annotation; ret_type = JTransType.return_type program tenv ms; @@ -353,6 +355,7 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name = formals; is_bridge_method = cm.Javalib.cm_bridge; is_defined = true; + is_model = Config.models_mode; is_synthetic_method = cm.Javalib.cm_synthetic; is_java_synchronized_method = cm.Javalib.cm_synchronized; loc = loc_start;