[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

@@ -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,

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. */

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,

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 */

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

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;

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;