[Infer][Java] Adding is_static metadata to Java procname's

infer/src/backend/procname.ml

@@ -13,12 +13,17 @@ open Str
 
 type java_type = string option * string (* e.g. ("", "int") for primitive types or ("java.io", "PrintWriter") for objects *)
 
+type method_kind =
+  | Static (* in Java, procedures called with invokestatic *)
+  | Non_Static (* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface *)
+
 (* java_signature extends base_signature with a classname and a package *)
 type java_signature = {
   classname: java_type;
   returntype: java_type option; (* option because constructors have no return type *)
   methodname: string;
-  parameters: java_type list
+  parameters: java_type list;
+  kind: method_kind
 }
 
 type objc_signature = {
@@ -52,6 +57,12 @@ let mangled_compare so1 so2 = match so1, so2 with
   | Some _, None -> 1
   | Some s1, Some s2 -> string_compare s1 s2
 
+let method_kind_compare k0 k1 =
+  match k0, k1 with
+  | _ when k0 = k1 -> 0
+  | Static, _ -> 1
+  | Non_Static, _ -> -1
+
 (** A type is a pair (package, type_name) that is translated in a string package.type_name *)
 let java_type_to_string p verbosity =
   match p with
@@ -98,6 +109,7 @@ let java_sig_compare js1 js2 =
   |> next java_type_list_compare js1.parameters js2.parameters
   |> next java_type_compare js1.classname js2.classname
   |> next java_return_type_compare js1.returntype js2.returntype
+  |> next method_kind_compare js1.kind js2.kind
 
 (** Compare objc signatures. *)
 let objc_sig_compare osig1 osig2 =
@@ -121,12 +133,13 @@ let mangled_static (plain: string) (source_file: DB.source_file) =
     else None in STATIC (plain, mangled)
 
 (** Creates a java procname, given classname, return type, method name and its parameters *)
-let mangled_java class_name ret_type method_name params =
+let mangled_java class_name ret_type method_name params _kind =
   JAVA {
     classname = class_name;
     returntype = ret_type;
     methodname = method_name;
-    parameters = params
+    parameters = params;
+    kind = _kind
   }
 
 (** Create an objc procedure name from a class_name and method_name. *)
@@ -195,11 +208,6 @@ let clang_get_method = function
   | OBJC_BLOCK name -> name
   | _ -> assert false
 
-(** Replace the method name of an existing java procname. *)
-let java_replace_method p methodname = match p with
-  | JAVA j -> JAVA { j with methodname = methodname }
-  | _ -> assert false
-
 (** Return the return type of a java procname. *)
 let java_get_return_type = function
   | JAVA j -> java_return_type_to_string j VERBOSE
@@ -210,6 +218,11 @@ let java_get_parameters = function
   | JAVA j -> list_map (fun param -> java_type_to_string param VERBOSE) j.parameters
   | _ -> assert false
 
+(** Return true if the java procedure is static *)
+let java_is_static = function
+  | JAVA j -> j.kind = Static
+  | _ -> assert false
+
 (** Prints a string of a java procname with the given level of verbosity *)
 let java_to_string ?withclass: (wc = false) j verbosity =
   match verbosity with

infer/src/backend/procname.mli

@@ -13,6 +13,10 @@ type t
 
 type java_type = string option * string
 
+type method_kind =
+  | Static (* in Java, procedures called with invokestatic *)
+  | Non_Static (* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface *)
+
 (** Comparison for proc names *)
 val compare : t -> t -> int
 
@@ -28,8 +32,8 @@ val mangled_cpp : string -> string -> t
 (** Create a static procedure name from a plain name and source file *)
 val mangled_static : string -> DB.source_file -> t
 
-(** Create a Java procedure name from its class_name method_name args_type_name return_type_name *)
-val mangled_java : java_type -> java_type option -> string -> java_type list -> t
+(** Create a Java procedure name from its class_name method_name args_type_name return_type_name method_kind *)
+val mangled_java : java_type -> java_type option -> string -> java_type list -> method_kind -> t
 
 (** Create an objc procedure name from a class_name and method_name. *)
 val mangled_objc : string -> string -> t
@@ -76,6 +80,9 @@ val java_get_return_type : t -> string
 (** Return the parameters of a java procedure name. *)
 val java_get_parameters : t -> string list
 
+(** Return true if the java procedure is static *)
+val java_is_static : t -> bool
+
 (** Check if the last parameter is a hidden inner class, and remove it if present.
 This is used in private constructors, where a proxy constructor is generated
 with an extra parameter and calls the normal constructor. *)

infer/src/backend/symExec.ml

@@ -760,7 +760,7 @@ let redirect_shared_ptr tenv cfg pname actual_params =
 
 (** recognize calls to the constructor java.net.URL and splits the argument string to be only the protocol.  *)
 let call_constructor_url_update_args tenv cfg pname actual_params =
-  let url_pname = Procname.mangled_java ((Some "java.net"), "URL") None "<init>" [(Some "java.lang"), "String"] in
+  let url_pname = Procname.mangled_java ((Some "java.net"), "URL") None "<init>" [(Some "java.lang"), "String"] Procname.Non_Static in
   if (Procname.equal url_pname pname) then
     (match actual_params with
       | [this; (Sil.Const (Sil.Cstr s), atype)] ->

infer/src/harness/harness.ml

@@ -163,7 +163,7 @@ let create_android_harness proc_file_map tenv =
                       * inhabitation module to create a harness for us *)
                           let harness_procname =
                             let harness_cls_name = PatternMatch.get_type_name typ in
-                            Procname.mangled_java (None, harness_cls_name) None "InferGeneratedHarness" [] in
+                            Procname.mangled_java (None, harness_cls_name) None "InferGeneratedHarness" [] Procname.Static in
                           let callback_fields =
                             extract_callbacks lifecycle_trace harness_procname proc_file_map tenv in
                           Inhabit.inhabit_trace lifecycle_trace callback_fields harness_procname proc_file_map tenv

infer/src/java/jFrontend.ml

@@ -156,7 +156,7 @@ let create_icfg never_null_matcher linereader program icfg source_file cn node =
   begin
     Javalib.m_iter (JTrans.create_local_procdesc program linereader cfg tenv node) node;
     Javalib.m_iter (fun m ->
-            let method_kind = JTrans.get_method_kind m in
+            let method_kind = JTransType.get_method_kind m in
             match m with
             | Javalib.ConcreteMethod cm ->
                 add_cmethod never_null_matcher program icfg node cm method_kind

infer/src/java/jTrans.ml

@@ -11,10 +11,6 @@ open Sawja_pack
 open Utils
 module L = Logging
 
-type method_kind =
-  | Static
-  | Non_Static
-
 type invoke_kind =
   | I_Virtual
   | I_Interface
@@ -27,8 +23,6 @@ let constr_loc_map : Sil.location JBasics.ClassMap.t ref = ref JBasics.ClassMap.
 
 let init_loc_map : Sil.location JBasics.ClassMap.t ref = ref JBasics.ClassMap.empty
 
-let get_method_kind m = if Javalib.is_static_method m then Static else Non_Static
-
 (** Fix the line associated to a method definition.
 Since Sawja often reports a method off by a few lines, we search
 backwards for a line where the method name is. *)
@@ -120,7 +114,7 @@ let get_field_name program static tenv cn fs context =
   | _ -> assert false
 
 
-let formals_from_signature program tenv cn ms is_static =
+let formals_from_signature program tenv cn ms kind =
   let counter = ref 0 in
   let method_name = JBasics.ms_name ms in
   let get_arg_name () =
@@ -131,9 +125,9 @@ let formals_from_signature program tenv cn ms is_static =
     let arg_name = get_arg_name () in
     let arg_type = JTransType.value_type program tenv vt in
     (arg_name, arg_type):: l in
-  let init_arg_list = match is_static with
-    | Static -> []
-    | Non_Static -> [(JConfig.this, JTransType.get_class_type program tenv cn)] in
+  let init_arg_list = match kind with
+    | Procname.Static -> []
+    | Procname.Non_Static -> [(JConfig.this, JTransType.get_class_type program tenv cn)] in
   list_rev (list_fold_left collect init_arg_list (JBasics.ms_args ms))
 
 let formals program tenv cn impl =
@@ -272,7 +266,7 @@ let create_local_procdesc program linereader cfg tenv node m =
       meth_kind = JContext.Init &&
       not (JTransStaticField.has_static_final_fields node))
   then
-    let procname = (JTransType.get_method_procname cn ms) in
+    let procname = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in
     let create_new_procdesc () =
       let trans_access = function
         | `Default -> Sil.Default
@@ -282,7 +276,7 @@ let create_local_procdesc program linereader cfg tenv node m =
       try
         match m with
         | Javalib.AbstractMethod am -> (* create a procdesc with empty body *)
-            let formals = formals_from_signature program tenv cn ms (get_method_kind m) in
+            let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in
             let method_annotation = JAnnotation.translate_method am.Javalib.am_annotations in
             let procdesc =
               let open Cfg.Procdesc in
@@ -317,7 +311,7 @@ let create_local_procdesc program linereader cfg tenv node m =
             Cfg.Procdesc.set_start_node procdesc start_node;
             Cfg.Procdesc.set_exit_node procdesc exit_node
         | Javalib.ConcreteMethod cm when is_java_native cm ->
-            let formals = formals_from_signature program tenv cn ms (get_method_kind m) in
+            let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in
             let method_annotation = JAnnotation.translate_method cm.Javalib.cm_annotations in
             let _procdesc =
               let open Cfg.Procdesc in
@@ -403,13 +397,13 @@ let create_local_procdesc program linereader cfg tenv node m =
               create_new_procdesc ()
         end
 
-let create_external_procdesc program cfg tenv cn ms method_annotation is_static =
+let create_external_procdesc program cfg tenv cn ms method_annotation kind =
   let return_type =
     match JBasics.ms_rtype ms with
     | None -> Sil.Tvoid
     | Some vt -> JTransType.value_type program tenv vt in
-  let formals = formals_from_signature program tenv cn ms is_static in
-  let procname = JTransType.get_method_procname cn ms in
+  let formals = formals_from_signature program tenv cn ms kind in
+  let procname = JTransType.get_method_procname cn ms kind in
   ignore (
       let open Cfg.Procdesc in
       let proc_attributes =
@@ -437,12 +431,12 @@ let create_external_procdesc program cfg tenv cn ms method_annotation is_static
         })
 
 (** returns the procedure description of the given method and creates it if it hasn't been created before *)
-let rec get_method_procdesc program cfg tenv cn ms is_static =
-  let procname = JTransType.get_method_procname cn ms in
+let rec get_method_procdesc program cfg tenv cn ms kind =
+  let procname = JTransType.get_method_procname cn ms kind in
   match lookup_procdesc cfg procname with
   | Unknown ->
-      create_external_procdesc program cfg tenv cn ms Sil.method_annotation_empty is_static;
-      get_method_procdesc program cfg tenv cn ms is_static
+      create_external_procdesc program cfg tenv cn ms Sil.method_annotation_empty kind;
+      get_method_procdesc program cfg tenv cn ms kind
   | Created status -> status
 
 let use_static_final_fields context =
@@ -574,7 +568,7 @@ let rec expression context pc expr =
         (* when accessing a static final field, we call the initialiser method. *)
         let cfg = JContext.get_cfg context in
         let callee_procdesc =
-          match get_method_procdesc program cfg tenv cn JBasics.clinit_signature Static with
+          match get_method_procdesc program cfg tenv cn JBasics.clinit_signature Procname.Static with
           | Called p | Defined p -> p in
         let field_type =
           JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl) in
@@ -831,7 +825,6 @@ let assume_not_null loc sil_expr =
 
 
 let rec instruction context pc instr : translation =
-  (* JUtils.log "\t\t\tinstr: %s@." (JBir.print_instr instr); *)
   let cfg = JContext.get_cfg context in
   let tenv = JContext.get_tenv context in
   let cg = JContext.get_cg context in
@@ -964,7 +957,7 @@ let rec instruction context pc instr : translation =
         let (constr_procdesc, constr_procname, call_ids, call_instrs) =
           let ret_opt = Some (Sil.Var ret_id, class_type) in
           method_invocation
-            context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Static in
+            context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Procname.Non_Static in
         let pvar = JContext.set_pvar context var class_type in
         let set_instr = Sil.Set (Sil.Lvar pvar, class_type, Sil.Var ret_id, loc) in
         let ids = ret_id :: call_ids in
@@ -999,7 +992,7 @@ let rec instruction context pc instr : translation =
               Some (sil_arg_expr, arg_typ), [], ids, instrs
           | _ -> None, args, [], [] in
         let (callee_procdesc, callee_procname, call_idl, call_instrs) =
-          method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Static in
+          method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Procname.Static in
         let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
         let call_node = create_node node_kind (ids @ call_idl) (instrs @ call_instrs) in
         let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
@@ -1012,7 +1005,7 @@ let rec instruction context pc instr : translation =
           let (ids, instrs, sil_obj_expr) = expression context pc obj in
           let (callee_procdesc, callee_procname, call_ids, call_instrs) =
             let ret_opt = Some (sil_obj_expr, sil_obj_type) in
-            method_invocation context loc pc var_opt cn ms ret_opt args I_Virtual Non_Static in
+            method_invocation context loc pc var_opt cn ms ret_opt args I_Virtual Procname.Non_Static in
           let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
           let call_node = create_node node_kind (ids @ call_ids) (instrs @ call_instrs) in
           Cg.add_edge cg caller_procname callee_procname;
@@ -1044,7 +1037,7 @@ let rec instruction context pc instr : translation =
         let (ids, instrs, sil_obj_expr) = expression context pc obj in
         let sil_obj_type = JTransType.expr_type context obj in
         let (callee_procdesc, callee_procname, call_ids, call_instrs) =
-          method_invocation context loc pc var_opt cn ms (Some (sil_obj_expr, sil_obj_type)) args I_Special Non_Static in
+          method_invocation context loc pc var_opt cn ms (Some (sil_obj_expr, sil_obj_type)) args I_Special Procname.Non_Static in
         let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
         let call_node = create_node node_kind (ids @ call_ids) (instrs @ call_instrs) in
         let procdesc = (JContext.get_procdesc context) in
@@ -1081,7 +1074,7 @@ let rec instruction context pc instr : translation =
           let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
           let (constr_procdesc, constr_procname, call_ids, call_instrs) =
             let ret_opt = Some (Sil.Var ret_id, class_type) in
-            method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Static in
+            method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Procname.Static in
           let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
           let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
           let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
@@ -1138,7 +1131,7 @@ let rec instruction context pc instr : translation =
           let (constr_procdesc, constr_procname, call_ids, call_instrs) =
             method_invocation
               context loc pc None out_of_bound_cn constr_ms
-              (Some (Sil.Var ret_id, class_type)) [] I_Special Static in
+              (Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
           let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
           let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
           let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
@@ -1178,7 +1171,7 @@ let rec instruction context pc instr : translation =
           let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
           let (constr_procdesc, constr_procname, call_ids, call_instrs) =
             method_invocation context loc pc None cce_cn constr_ms
-              (Some (Sil.Var ret_id, class_type)) [] I_Special Static in
+              (Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
           let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
           let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
           let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in

infer/src/java/jTrans.mli

@@ -22,18 +22,13 @@ type defined_status =
   | Defined of Cfg.Procdesc.t
   | Called of Cfg.Procdesc.t
 
-type method_kind =
-  | Static
-  | Non_Static
-
 (** returns the procedure description of the given method and creates it if it hasn't been created before *)
-val get_method_procdesc : JClasspath.program -> Cfg.cfg -> Sil.tenv -> JBasics.class_name -> JBasics.method_signature -> method_kind -> defined_status
+val get_method_procdesc : JClasspath.program -> Cfg.cfg -> Sil.tenv -> JBasics.class_name ->
+  JBasics.method_signature -> Procname.method_kind -> defined_status
 
 (** [create_local_procdesc linereader cfg tenv program m] creates a procedure description for the method m and adds it to cfg  *)
 val create_local_procdesc : JClasspath.program -> Printer.LineReader.t -> Cfg.cfg -> Sil.tenv -> JCode.jcode Javalib.interface_or_class -> JCode.jcode Javalib.jmethod -> unit
 
-val get_method_kind : JCode.jcode Javalib.jmethod -> method_kind
-
 (** returns the implementation of a given method *)
 val get_implementation : JCode.jcode Javalib.concrete_method -> JBir.t
 

infer/src/java/jTransType.ml

@@ -6,10 +6,8 @@ open Utils
 
 (** Type transformations between Javalib datatypes and sil datatypes *)
 
-
 exception Type_tranlsation_error of string
 
-
 let basic_type = function
   | `Int -> Sil.Tint Sil.IInt
   | `Bool -> Sil.Tint Sil.IBool
@@ -181,21 +179,21 @@ let method_signature_names ms =
   let args_types = args_to_signature (JBasics.ms_args ms) in
   (return_type_name, method_name, args_types)
 
+let get_method_kind m = if Javalib.is_static_method m then Procname.Static else Procname.Non_Static
 
 (* create a mangled procname from an abstract or concrete method *)
-let get_method_procname cn ms =
+let get_method_procname cn ms kind =
   let return_type_name, method_name, args_type_name = method_signature_names ms in
   let class_name = cn_to_java_type cn in
-  Procname.mangled_java class_name return_type_name method_name args_type_name
-
+  Procname.mangled_java class_name return_type_name method_name args_type_name kind
 
 let get_class_procnames cn node =
   let collect jmethod procnames =
-    let ms = (Javalib.get_method_signature jmethod) in
-    (get_method_procname cn ms) :: procnames in
+    let ms = Javalib.get_method_signature jmethod in
+    let kind = get_method_kind jmethod in
+    (get_method_procname cn ms kind) :: procnames in
   Javalib.m_fold collect node []
 
-
 let create_fieldname cn fs =
   let fieldname cn fs =
     let fieldname = (JBasics.fs_name fs) in
@@ -203,7 +201,6 @@ let create_fieldname cn fs =
     Mangled.from_string (classname^"."^fieldname) in
   Ident.create_fieldname (fieldname cn fs) 0
 
-
 let create_sil_class_field cn cf =
   let fs = cf.Javalib.cf_signature in
   let field_name = create_fieldname cn fs
@@ -508,15 +505,15 @@ let never_returning_null =
   let fragment_type = "android.support.v4.app.Fragment" in
   let never_null_method_sigs =
     [
-    (fragment_type, "getContext", [], "android.content.Context");
-    (fragment_type, "getActivity", [], "android.support.v4.app.FragmentActivity")
+    (fragment_type, "getContext", [], "android.content.Context", Procname.Non_Static);
+    (fragment_type, "getActivity", [], "android.support.v4.app.FragmentActivity", Procname.Non_Static)
     ] in
   let make_procname = function
-    | (class_name, method_name, arg_types, ret_type) ->
+    | (class_name, method_name, arg_types, ret_type, kind) ->
         let return_cn = JBasics.make_cn ret_type in
         let cn = JBasics.make_cn class_name
         and ms =
           JBasics.make_ms
             method_name arg_types (Some (JBasics.TObject (JBasics.TClass return_cn))) in
-        get_method_procname cn ms in
+        get_method_procname cn ms kind in
   list_map make_procname never_null_method_sigs

infer/src/java/jTransType.mli

@@ -10,8 +10,11 @@ val typename_of_classname : JBasics.class_name -> Sil.typename
 (** returns a name for a field based on a class name and a field name  *)
 val create_fieldname : JBasics.class_name -> JBasics.field_signature -> Ident.fieldname
 
+val get_method_kind : JCode.jcode Javalib.jmethod -> Procname.method_kind
+
 (** returns a procedure name based on the class name and the method's signature. *)
-val get_method_procname : JBasics.class_name -> JBasics.method_signature -> Procname.t
+val get_method_procname : JBasics.class_name -> JBasics.method_signature -> Procname.method_kind ->
+  Procname.t
 
 (** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class
 without the pointer part *)