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

Wrap Java's PatternMatch into its own module

Browse Source 
Summary: This diff refactors Java specific `PatternMatch` functions into its own module. When `PatternMatch.ml` was originally created, it was mainly for Java but now it also supports ObjC. Let's refactor it to reflect the Java/ObjC separation: move all functions that operate on Java procnames into Java submodule.

Reviewed By: jvillard

Differential Revision: D22816504

fbshipit-source-id: ff6b64b29
master
Ezgi Çiçek 4 years ago committed by Facebook GitHub Bot
parent 86f550317f
commit feefda3e59
17 changed files with 604 additions and 567 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/absint/ConcurrencyModels.ml
Unescape View File

@ -300,7 +300,7 @@ let get_current_class_and_annotated_superclasses is_annot tenv pname =
| Procname.Java java_pname -> | Procname.Java java_pname ->
let current_class = Procname.Java.get_class_type_name java_pname in let current_class = Procname.Java.get_class_type_name java_pname in
let annotated_classes = let annotated_classes =
PatternMatch.find_superclasses_with_attributes is_annot tenv current_class PatternMatch.Java.find_superclasses_with_attributes is_annot tenv current_class
in in
Some (current_class, annotated_classes) Some (current_class, annotated_classes)
| _ -> | _ ->

4
infer/src/absint/NoReturnModels.ml
Unescape View File

@ -12,5 +12,5 @@ let no_return = true
let dispatch : (Tenv.t, bool, unit) ProcnameDispatcher.ProcName.dispatcher = let dispatch : (Tenv.t, bool, unit) ProcnameDispatcher.ProcName.dispatcher =
let open ProcnameDispatcher.ProcName in let open ProcnameDispatcher.ProcName in
make_dispatcher make_dispatcher
[ +PatternMatch.implements_lang "System" &:: "exit" <>--> no_return [ +PatternMatch.Java.implements_lang "System" &:: "exit" <>--> no_return
; +PatternMatch.implements_lang "Runtime" &:: "exit" <>--> no_return ] ; +PatternMatch.Java.implements_lang "Runtime" &:: "exit" <>--> no_return ]

436
infer/src/absint/PatternMatch.ml
Unescape View File

@ -41,86 +41,6 @@ let is_subtype_of_str tenv cn1 classname_str =
is_subtype tenv cn1 typename is_subtype tenv cn1 typename
let implements interface tenv typename =
let is_interface s _ = String.equal interface (Typ.Name.name s) in
supertype_exists tenv is_interface (Typ.Name.Java.from_string typename)
let implements_arrays = implements "java.util.Arrays"
let implements_iterator = implements "java.util.Iterator"
let implements_collection = implements "java.util.Collection"
let implements_collections = implements "java.util.Collections"
let implements_list = implements "java.util.List"
let implements_xmob_utils class_name = implements ("com.moblica.common.xmob.utils." ^ class_name)
let implements_pseudo_collection =
let androidx_class_names =
List.map
~f:(fun class_name -> "androidx.collection." ^ class_name)
[ "ArrayMap"
; "ArraySet"
; "CircularArray"
; "LongSparseArray"
; "LruCache"
; "SimpleArrayMap"
; "SparseArrayCompat" ]
in
fun t s ->
implements "android.util.SparseArray" t s
|| implements "android.util.SparseIntArray" t s
|| implements_xmob_utils "IntArrayList" t s
|| List.exists ~f:(fun class_name -> implements class_name t s) androidx_class_names
let implements_enumeration = implements "java.util.Enumeration"
let implements_inject class_name = implements ("javax.inject." ^ class_name)
let implements_io class_name = implements ("java.io." ^ class_name)
let implements_nio class_name = implements ("java.nio." ^ class_name)
let implements_map = implements "java.util.Map"
let implements_androidx_map = implements "androidx.collection.SimpleArrayMap"
let implements_set = implements "java.util.Set"
let implements_map_entry = implements "java.util.Map$Entry"
let implements_queue = implements "java.util.Queue"
let implements_lang class_name = implements ("java.lang." ^ class_name)
let implements_google class_name = implements ("com.google." ^ class_name)
let implements_android class_name = implements ("android." ^ class_name)
let implements_infer_annotation class_name =
implements ("com.facebook.infer.annotation." ^ class_name)
let implements_jackson class_name = implements ("com.fasterxml.jackson." ^ class_name)
let implements_org_json class_name = implements ("org.json." ^ class_name)
let implements_app_activity = implements "android.app.Activity"
let implements_app_fragment = implements "androidx.fragment.app.Fragment"
let implements_graphql_story = implements "com.facebook.graphql.model.GraphQLStory"
let implements_psi_element = implements "com.intellij.psi.PsiElement"
let implements_view_group = implements "android.view.ViewGroup"
let implements_view_parent = implements "android.view.ViewParent"
(** The type the method is invoked on *) (** The type the method is invoked on *)
let get_this_type_nonstatic_methods_only proc_attributes = let get_this_type_nonstatic_methods_only proc_attributes =
match proc_attributes.ProcAttributes.formals with (_, t) :: _ -> Some t | _ -> None match proc_attributes.ProcAttributes.formals with (_, t) :: _ -> Some t | _ -> None
@ -174,18 +94,225 @@ let get_field_type_name tenv (typ : Typ.t) (fieldname : Fieldname.t) : string op
None None
let java_get_const_type_name (const : Const.t) : string = module Java = struct
match const with let implements interface tenv typename =
| Const.Cstr _ -> let is_interface s _ = String.equal interface (Typ.Name.name s) in
"java.lang.String" supertype_exists tenv is_interface (Typ.Name.Java.from_string typename)
| Const.Cint _ ->
"java.lang.Integer"
| Const.Cfloat _ -> let implements_arrays = implements "java.util.Arrays"
"java.lang.Double"
| _ -> let implements_iterator = implements "java.util.Iterator"
"_"
let implements_collection = implements "java.util.Collection"
let implements_collections = implements "java.util.Collections"
let implements_list = implements "java.util.List"
let implements_xmob_utils class_name = implements ("com.moblica.common.xmob.utils." ^ class_name)
let implements_pseudo_collection =
let androidx_class_names =
List.map
~f:(fun class_name -> "androidx.collection." ^ class_name)
[ "ArrayMap"
; "ArraySet"
; "CircularArray"
; "LongSparseArray"
; "LruCache"
; "SimpleArrayMap"
; "SparseArrayCompat" ]
in
fun t s ->
implements "android.util.SparseArray" t s
|| implements "android.util.SparseIntArray" t s
|| implements_xmob_utils "IntArrayList" t s
|| List.exists ~f:(fun class_name -> implements class_name t s) androidx_class_names
let implements_enumeration = implements "java.util.Enumeration"
let implements_inject class_name = implements ("javax.inject." ^ class_name)
let implements_io class_name = implements ("java.io." ^ class_name)
let implements_nio class_name = implements ("java.nio." ^ class_name)
let implements_map = implements "java.util.Map"
let implements_androidx_map = implements "androidx.collection.SimpleArrayMap"
let implements_set = implements "java.util.Set"
let implements_map_entry = implements "java.util.Map$Entry"
let implements_queue = implements "java.util.Queue"
let implements_lang class_name = implements ("java.lang." ^ class_name)
let implements_google class_name = implements ("com.google." ^ class_name)
let implements_android class_name = implements ("android." ^ class_name)
let implements_infer_annotation class_name =
implements ("com.facebook.infer.annotation." ^ class_name)
let implements_jackson class_name = implements ("com.fasterxml.jackson." ^ class_name)
let implements_org_json class_name = implements ("org.json." ^ class_name)
let implements_app_activity = implements "android.app.Activity"
let implements_app_fragment = implements "androidx.fragment.app.Fragment"
let implements_graphql_story = implements "com.facebook.graphql.model.GraphQLStory"
let implements_psi_element = implements "com.intellij.psi.PsiElement"
let implements_view_group = implements "android.view.ViewGroup"
let implements_view_parent = implements "android.view.ViewParent"
let initializer_classes =
List.map ~f:Typ.Name.Java.from_string
[ "android.app.Activity"
; "android.app.Application"
; "android.app.Fragment"
; "android.app.Service"
; "android.support.v4.app.Fragment"
; "androidx.fragment.app.Fragment"
; "junit.framework.TestCase" ]
let initializer_methods = ["onActivityCreated"; "onAttach"; "onCreate"; "onCreateView"; "setUp"]
(** Check if the type has in its supertypes from the initializer_classes list. *)
let type_has_initializer (tenv : Tenv.t) (t : Typ.t) : bool =
let is_initializer_class typename _ =
List.mem ~equal:Typ.Name.equal initializer_classes typename
in
match t.desc with
| Typ.Tstruct name | Tptr ({desc= Tstruct name}, _) ->
supertype_exists tenv is_initializer_class name
| _ ->
false
(** Check if the method is one of the known initializer methods. *)
let method_is_initializer (tenv : Tenv.t) (proc_attributes : ProcAttributes.t) : bool =
match get_this_type_nonstatic_methods_only proc_attributes with
| Some this_type ->
if type_has_initializer tenv this_type then
match proc_attributes.ProcAttributes.proc_name with
| Procname.Java pname_java ->
let mname = Procname.Java.get_method pname_java in
List.exists ~f:(String.equal mname) initializer_methods
| _ ->
false
else false
| None ->
false
let get_const_type_name (const : Const.t) : string =
match const with
| Const.Cstr _ ->
"java.lang.String"
| Const.Cint _ ->
"java.lang.Integer"
| Const.Cfloat _ ->
"java.lang.Double"
| _ ->
""
(** Checks if the class name is a Java exception *)
let is_throwable tenv typename = is_subtype_of_str tenv typename "java.lang.Throwable"
let is_enum tenv typename = is_subtype_of_str tenv typename "java.lang.Enum"
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument,
including for supertypes*)
let check_class_attributes check tenv = function
| Procname.Java java_pname ->
let check_class_annots _ {Struct.annots} = check annots in
supertype_exists tenv check_class_annots (Procname.Java.get_class_type_name java_pname)
| _ ->
false
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, for the
current class only*)
let check_current_class_attributes check tenv = function
| Procname.Java java_pname -> (
match Tenv.lookup tenv (Procname.Java.get_class_type_name java_pname) with
| Some struct_typ ->
check struct_typ.annots
| _ ->
false )
| _ ->
false
(** find superclasss with attributes (e.g., [@ThreadSafe]), including current class*)
let rec find_superclasses_with_attributes check tenv tname =
match Tenv.lookup tenv tname with
| Some struct_typ ->
let result_from_supers =
List.concat (List.map ~f:(find_superclasses_with_attributes check tenv) struct_typ.supers)
in
if check struct_typ.annots then tname :: result_from_supers else result_from_supers
| _ ->
[]
let is_override_of_lang_object_equals curr_pname =
let is_only_param_of_object_type = function
| [Procname.Parameter.JavaParameter param_type]
when JavaSplitName.equal param_type JavaSplitName.java_lang_object ->
true
| _ ->
false
in
String.equal (Procname.get_method curr_pname) "equals"
&& is_only_param_of_object_type (Procname.get_parameters curr_pname)
end
module ObjectiveC = struct
let is_core_graphics_create_or_copy _ procname =
String.is_prefix ~prefix:"CG" procname
&& ( String.is_substring ~substring:"Create" procname
|| String.is_substring ~substring:"Copy" procname )
let is_core_foundation_create_or_copy _ procname =
String.is_prefix ~prefix:"CF" procname
&& ( String.is_substring ~substring:"Create" procname
|| String.is_substring ~substring:"Copy" procname )
let is_core_graphics_release _ procname =
String.is_prefix ~prefix:"CG" procname && String.is_suffix ~suffix:"Release" procname
let is_modelled_as_alloc _ procname =
match Config.pulse_model_alloc_pattern with
| Some regex ->
Str.string_match regex procname 0
| None ->
false
let is_modelled_as_release _ procname =
match Config.pulse_model_release_pattern with
| Some regex ->
Str.string_match regex procname 0
| None ->
false
end
let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : string list = let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : string list =
(* Is this the node creating ivar? *) (* Is this the node creating ivar? *)
let initializes_array instrs = let initializes_array instrs =
@ -225,7 +352,7 @@ let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : s
Some (nvar_type_name nvar) Some (nvar_type_name nvar)
| Sil.Store {e1= Exp.Lindex (Exp.Var iv, _); e2= Exp.Const c} | Sil.Store {e1= Exp.Lindex (Exp.Var iv, _); e2= Exp.Const c}
when Ident.equal iv array_nvar -> when Ident.equal iv array_nvar ->
Some (Some (java_get_const_type_name c)) Some (Some (Java.get_const_type_name c))
| _ -> | _ ->
None ) None )
|> Option.join |> Option.join
@ -271,47 +398,6 @@ let type_is_class typ =
false false
let initializer_classes =
List.map ~f:Typ.Name.Java.from_string
[ "android.app.Activity"
; "android.app.Application"
; "android.app.Fragment"
; "android.app.Service"
; "android.support.v4.app.Fragment"
; "androidx.fragment.app.Fragment"
; "junit.framework.TestCase" ]
let initializer_methods = ["onActivityCreated"; "onAttach"; "onCreate"; "onCreateView"; "setUp"]
(** Check if the type has in its supertypes from the initializer_classes list. *)
let type_has_initializer (tenv : Tenv.t) (t : Typ.t) : bool =
let is_initializer_class typename _ =
List.mem ~equal:Typ.Name.equal initializer_classes typename
in
match t.desc with
| Typ.Tstruct name | Tptr ({desc= Tstruct name}, _) ->
supertype_exists tenv is_initializer_class name
| _ ->
false
(** Check if the method is one of the known initializer methods. *)
let method_is_initializer (tenv : Tenv.t) (proc_attributes : ProcAttributes.t) : bool =
match get_this_type_nonstatic_methods_only proc_attributes with
| Some this_type ->
if type_has_initializer tenv this_type then
match proc_attributes.ProcAttributes.proc_name with
| Procname.Java pname_java ->
let mname = Procname.Java.get_method pname_java in
List.exists ~f:(String.equal mname) initializer_methods
| _ ->
false
else false
| None ->
false
let proc_calls resolve_attributes pdesc filter : (Procname.t * ProcAttributes.t) list = let proc_calls resolve_attributes pdesc filter : (Procname.t * ProcAttributes.t) list =
let res = ref [] in let res = ref [] in
let do_instruction _ instr = let do_instruction _ instr =
@ -422,89 +508,3 @@ let get_fields_nullified procdesc =
~init:(Fieldname.Set.empty, Ident.Set.empty) ~init:(Fieldname.Set.empty, Ident.Set.empty)
in in
nullified_flds nullified_flds
(** Checks if the class name is a Java exception *)
let is_throwable tenv typename = is_subtype_of_str tenv typename "java.lang.Throwable"
let is_java_enum tenv typename = is_subtype_of_str tenv typename "java.lang.Enum"
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, including
for supertypes*)
let check_class_attributes check tenv = function
| Procname.Java java_pname ->
let check_class_annots _ {Struct.annots} = check annots in
supertype_exists tenv check_class_annots (Procname.Java.get_class_type_name java_pname)
| _ ->
false
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, for the
current class only*)
let check_current_class_attributes check tenv = function
| Procname.Java java_pname -> (
match Tenv.lookup tenv (Procname.Java.get_class_type_name java_pname) with
| Some struct_typ ->
check struct_typ.annots
| _ ->
false )
| _ ->
false
(** find superclasss with attributes (e.g., [@ThreadSafe]), including current class*)
let rec find_superclasses_with_attributes check tenv tname =
match Tenv.lookup tenv tname with
| Some struct_typ ->
let result_from_supers =
List.concat (List.map ~f:(find_superclasses_with_attributes check tenv) struct_typ.supers)
in
if check struct_typ.annots then tname :: result_from_supers else result_from_supers
| _ ->
[]
let is_override_of_java_lang_object_equals curr_pname =
let is_only_param_of_object_type = function
| [Procname.Parameter.JavaParameter param_type]
when JavaSplitName.equal param_type JavaSplitName.java_lang_object ->
true
| _ ->
false
in
String.equal (Procname.get_method curr_pname) "equals"
&& is_only_param_of_object_type (Procname.get_parameters curr_pname)
module ObjectiveC = struct
let is_core_graphics_create_or_copy _ procname =
String.is_prefix ~prefix:"CG" procname
&& ( String.is_substring ~substring:"Create" procname
|| String.is_substring ~substring:"Copy" procname )
let is_core_foundation_create_or_copy _ procname =
String.is_prefix ~prefix:"CF" procname
&& ( String.is_substring ~substring:"Create" procname
|| String.is_substring ~substring:"Copy" procname )
let is_core_graphics_release _ procname =
String.is_prefix ~prefix:"CG" procname && String.is_suffix ~suffix:"Release" procname
let is_modelled_as_alloc _ procname =
match Config.pulse_model_alloc_pattern with
| Some regex ->
Str.string_match regex procname 0
| None ->
false
let is_modelled_as_release _ procname =
match Config.pulse_model_release_pattern with
| Some regex ->
Str.string_match regex procname 0
| None ->
false
end

168
infer/src/absint/PatternMatch.mli
Unescape View File

@ -19,101 +19,125 @@ val get_type_name : Typ.t -> string
val get_vararg_type_names : Tenv.t -> Procdesc.Node.t -> Pvar.t -> string list val get_vararg_type_names : Tenv.t -> Procdesc.Node.t -> Pvar.t -> string list
(** Get the type names of a variable argument *) (** Get the type names of a variable argument *)
val method_is_initializer : Tenv.t -> ProcAttributes.t -> bool
(** Check if the method is one of the known initializer methods. *)
val is_subtype : Tenv.t -> Typ.Name.t -> Typ.Name.t -> bool val is_subtype : Tenv.t -> Typ.Name.t -> Typ.Name.t -> bool
(** Is the type a transitive subtype of the typename? *) (** Is the type a transitive subtype of the typename? *)
val is_subtype_of_str : Tenv.t -> Typ.Name.t -> string -> bool val is_subtype_of_str : Tenv.t -> Typ.Name.t -> string -> bool
(** Resolve [typ_str] in [tenv], then check [typ] <: [typ_str] *) (** Resolve [typ_str] in [tenv], then check [typ] <: [typ_str] *)
val implements : string -> Tenv.t -> string -> bool module Java : sig
(** Check whether class implements a given class *) val implements : string -> Tenv.t -> string -> bool
(** Check whether class implements a given Java class *)
val implements_arrays : Tenv.t -> string -> bool
(** Check whether class implements Java's Arrays *)
val implements_iterator : Tenv.t -> string -> bool
(** Check whether class implements Java's Iterator *)
val implements_collection : Tenv.t -> string -> bool
(** Check whether class implements a Java's Collection *)
val implements_arrays : Tenv.t -> string -> bool val implements_collections : Tenv.t -> string -> bool
(** Check whether class implements Java's Arrays *) (** Check whether class implements a Java's Collections *)
val implements_iterator : Tenv.t -> string -> bool val implements_pseudo_collection : Tenv.t -> string -> bool
(** Check whether class implements Java's Iterator *) (** Check whether class implements a pseudo Collection with support for get() and size() methods *)
val implements_collection : Tenv.t -> string -> bool val implements_enumeration : Tenv.t -> string -> bool
(** Check whether class implements a Java's Collection *) (** Check whether class implements a Java's Enumeration *)
val implements_collections : Tenv.t -> string -> bool val implements_jackson : string -> Tenv.t -> string -> bool
(** Check whether class implements a Java's Collections *) (** Check whether class implements a class from Jackson *)
val implements_pseudo_collection : Tenv.t -> string -> bool val implements_org_json : string -> Tenv.t -> string -> bool
(** Check whether class implements a pseudo Collection with support for get() and size() methods *) (** Check whether class implements a class from Json *)
val implements_enumeration : Tenv.t -> string -> bool val implements_inject : string -> Tenv.t -> string -> bool
(** Check whether class implements a Java's Enumeration *) (** Check whether class implements a Javax Inject *)
val implements_jackson : string -> Tenv.t -> string -> bool val implements_io : string -> Tenv.t -> string -> bool
(** Check whether class implements a class from Jackson *) (** Check whether class implements a Java IO *)
val implements_org_json : string -> Tenv.t -> string -> bool val implements_nio : string -> Tenv.t -> string -> bool
(** Check whether class implements a class from Json *) (** Check whether class implements a Java nio *)
val implements_inject : string -> Tenv.t -> string -> bool val implements_map : Tenv.t -> string -> bool
(** Check whether class implements a Javax Inject *) (** Check whether class implements a Java's Map *)
val implements_io : string -> Tenv.t -> string -> bool val implements_androidx_map : Tenv.t -> string -> bool
(** Check whether class implements a Java IO *) (** Check whether class implements a AndroidX's Map *)
val implements_nio : string -> Tenv.t -> string -> bool val implements_set : Tenv.t -> string -> bool
(** Check whether class implements a Java nio *) (** Check whether class implements a Java's Set *)
val implements_map : Tenv.t -> string -> bool val implements_map_entry : Tenv.t -> string -> bool
(** Check whether class implements a Java's Map *) (** Check whether class implements a Java's Map$Entry *)
val implements_androidx_map : Tenv.t -> string -> bool val implements_queue : Tenv.t -> string -> bool
(** Check whether class implements a AndroidX's Map *) (** Check whether class implements a Java's Queue *)
val implements_set : Tenv.t -> string -> bool val implements_lang : string -> Tenv.t -> string -> bool
(** Check whether class implements a Java's Set *) (** Check whether class implements a Java's lang *)
val implements_map_entry : Tenv.t -> string -> bool val implements_list : Tenv.t -> string -> bool
(** Check whether class implements a Java's Map$Entry *) (** Check whether class implements a Java's list *)
val implements_queue : Tenv.t -> string -> bool val implements_google : string -> Tenv.t -> string -> bool
(** Check whether class implements a Java's Queue *) (** Check whether class implements a class of Google *)
val implements_lang : string -> Tenv.t -> string -> bool val implements_android : string -> Tenv.t -> string -> bool
(** Check whether class implements a Java's lang *) (** Check whether class implements a class of Android *)
val implements_list : Tenv.t -> string -> bool val implements_infer_annotation : string -> Tenv.t -> string -> bool
(** Check whether class implements a Java's list *) (** Check whether class implements a class of Infer annotation *)
val implements_google : string -> Tenv.t -> string -> bool val implements_app_activity : Tenv.t -> string -> bool
(** Check whether class implements a class of Google *) (** Check whether class implements a class of [android.app.Activity] *)
val implements_android : string -> Tenv.t -> string -> bool val implements_app_fragment : Tenv.t -> string -> bool
(** Check whether class implements a class of Android *) (** Check whether class implements a class of [androidx.fragment.app.Fragment] *)
val implements_infer_annotation : string -> Tenv.t -> string -> bool val implements_graphql_story : Tenv.t -> string -> bool
(** Check whether class implements a class of Infer annotation *) (** Check whether class implements a class of [com.facebook.graphql.model.GraphQLStory] *)
val implements_app_activity : Tenv.t -> string -> bool val implements_psi_element : Tenv.t -> string -> bool
(** Check whether class implements a class of [android.app.Activity] *) (** Check whether class implements a class of [com.intellij.psi.PsiElement] *)
val implements_app_fragment : Tenv.t -> string -> bool val implements_view_group : Tenv.t -> string -> bool
(** Check whether class implements a class of [androidx.fragment.app.Fragment] *) (** Check whether class implements a class of [android.view.ViewGroup] *)
val implements_graphql_story : Tenv.t -> string -> bool val implements_view_parent : Tenv.t -> string -> bool
(** Check whether class implements a class of [com.facebook.graphql.model.GraphQLStory] *) (** Check whether class implements a class of [android.view.ViewParent] *)
val implements_psi_element : Tenv.t -> string -> bool val implements_xmob_utils : string -> Tenv.t -> string -> bool
(** Check whether class implements a class of [com.intellij.psi.PsiElement] *) (** Check whether class implements a class of xmod.utils *)
val implements_view_group : Tenv.t -> string -> bool val is_throwable : Tenv.t -> Typ.Name.t -> bool
(** Check whether class implements a class of [android.view.ViewGroup] *) (** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *)
val implements_view_parent : Tenv.t -> string -> bool val is_enum : Tenv.t -> Typ.Name.t -> bool
(** Check whether class implements a class of [android.view.ViewParent] *) (** Checks if the type is Java enum (extends java.lang.Enum) *)
val implements_xmob_utils : string -> Tenv.t -> string -> bool val check_class_attributes : (Annot.Item.t -> bool) -> Tenv.t -> Procname.t -> bool
(** Check whether class implements a class of xmod.utils *) (** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument,
including supertypes*)
val check_current_class_attributes : (Annot.Item.t -> bool) -> Tenv.t -> Procname.t -> bool
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, for
current class only*)
val find_superclasses_with_attributes :
(Annot.Item.t -> bool) -> Tenv.t -> Typ.Name.t -> Typ.Name.t list
(** find superclasss with attributes (e.g., [@ThreadSafe]), including current class*)
val is_override_of_lang_object_equals : Procname.t -> bool
(** Whether the method is an override of `java.lang.Object.equals(Object)` or
`java.lang.Object.equals(Object)` itself *)
val method_is_initializer : Tenv.t -> ProcAttributes.t -> bool
(** Check if the method is one of the known initializer methods. *)
end
val supertype_exists : Tenv.t -> (Typ.Name.t -> Struct.t -> bool) -> Typ.Name.t -> bool val supertype_exists : Tenv.t -> (Typ.Name.t -> Struct.t -> bool) -> Typ.Name.t -> bool
(** Holds iff the predicate holds on a supertype of the named type, including the type itself *) (** Holds iff the predicate holds on a supertype of the named type, including the type itself *)
@ -153,32 +177,10 @@ val type_is_class : Typ.t -> bool
val get_fields_nullified : Procdesc.t -> Fieldname.Set.t val get_fields_nullified : Procdesc.t -> Fieldname.Set.t
(** return the set of instance fields that are assigned to a null literal in [procdesc] *) (** return the set of instance fields that are assigned to a null literal in [procdesc] *)
val is_throwable : Tenv.t -> Typ.Name.t -> bool
(** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *)
val is_java_enum : Tenv.t -> Typ.Name.t -> bool
(** Checks if the type is Java enum (extends java.lang.Enum) *)
val check_class_attributes : (Annot.Item.t -> bool) -> Tenv.t -> Procname.t -> bool
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, including
supertypes*)
val check_current_class_attributes : (Annot.Item.t -> bool) -> Tenv.t -> Procname.t -> bool
(** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, for
current class only*)
val find_superclasses_with_attributes :
(Annot.Item.t -> bool) -> Tenv.t -> Typ.Name.t -> Typ.Name.t list
(** find superclasss with attributes (e.g., [@ThreadSafe]), including current class*)
val has_same_signature : Procname.t -> (Procname.t -> bool) Staged.t val has_same_signature : Procname.t -> (Procname.t -> bool) Staged.t
(** For a given [procname] checks if the method has the same method name, number, order and types of (** For a given [procname] checks if the method has the same method name, number, order and types of
parameters.) *) parameters.) *)
val is_override_of_java_lang_object_equals : Procname.t -> bool
(** Whether the method is an override of `java.lang.Object.equals(Object)` or
`java.lang.Object.equals(Object)` itself *)
module ObjectiveC : sig module ObjectiveC : sig
val is_core_graphics_create_or_copy : Tenv.t -> string -> bool val is_core_graphics_create_or_copy : Tenv.t -> string -> bool

2
infer/src/bufferoverrun/bufferOverrunAnalysis.ml
Unescape View File

@ -156,7 +156,7 @@ module TransferFunctions = struct
let is_java_enum_values tenv callee_pname = let is_java_enum_values tenv callee_pname =
Option.exists (Procname.get_class_type_name callee_pname) ~f:(fun callee_class_name -> Option.exists (Procname.get_class_type_name callee_pname) ~f:(fun callee_class_name ->
PatternMatch.is_java_enum tenv callee_class_name PatternMatch.Java.is_enum tenv callee_class_name
&& String.equal (Procname.get_method callee_pname) "values" ) && String.equal (Procname.get_method callee_pname) "values" )

210
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -1514,16 +1514,16 @@ module Call = struct
; -"__get_array_length" <>$ capt_exp $!--> get_array_length ; -"__get_array_length" <>$ capt_exp $!--> get_array_length
; -"__infer_objc_cpp_throw" <>--> bottom ; -"__infer_objc_cpp_throw" <>--> bottom
; -"__new" ; -"__new"
<>$ any_arg_of_typ (+PatternMatch.implements_collection) <>$ any_arg_of_typ (+PatternMatch.Java.implements_collection)
$+...$--> Collection.new_collection $+...$--> Collection.new_collection
; -"__new" ; -"__new"
<>$ any_arg_of_typ (+PatternMatch.implements_map) <>$ any_arg_of_typ (+PatternMatch.Java.implements_map)
$+...$--> Collection.new_collection $+...$--> Collection.new_collection
; -"__new" ; -"__new"
<>$ any_arg_of_typ (+PatternMatch.implements_org_json "JSONArray") <>$ any_arg_of_typ (+PatternMatch.Java.implements_org_json "JSONArray")
$+...$--> Collection.new_collection $+...$--> Collection.new_collection
; -"__new" ; -"__new"
<>$ any_arg_of_typ (+PatternMatch.implements_pseudo_collection) <>$ any_arg_of_typ (+PatternMatch.Java.implements_pseudo_collection)
$+...$--> Collection.new_collection $+...$--> Collection.new_collection
; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true ; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true ; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
@ -1661,162 +1661,176 @@ module Call = struct
; -"google" &:: "StrLen" <>$ capt_exp $--> strlen ; -"google" &:: "StrLen" <>$ capt_exp $--> strlen
; (* Java models *) ; (* Java models *)
-"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone
; +PatternMatch.implements_arrays &:: "asList" <>$ capt_exp $!--> create_copy_array ; +PatternMatch.Java.implements_arrays &:: "asList" <>$ capt_exp $!--> create_copy_array
; +PatternMatch.implements_arrays &:: "copyOf" <>$ capt_exp $+ capt_exp ; +PatternMatch.Java.implements_arrays
$+...$--> Collection.copyOf &:: "copyOf" <>$ capt_exp $+ capt_exp $+...$--> Collection.copyOf
; (* model sets and maps as lists *) ; (* model sets and maps as lists *)
+PatternMatch.implements_collection +PatternMatch.Java.implements_collection
&:: "<init>" <>$ capt_var_exn &:: "<init>" <>$ capt_var_exn
$+ capt_exp_of_typ (+PatternMatch.implements_collection) $+ capt_exp_of_typ (+PatternMatch.Java.implements_collection)
$--> Collection.init_with_arg $--> Collection.init_with_arg
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "<init>" <>$ any_arg $+ capt_exp $--> Collection.init_with_capacity &:: "<init>" <>$ any_arg $+ capt_exp $--> Collection.init_with_capacity
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg $--> Collection.add_at_index &:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg $--> Collection.add_at_index
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "add" <>$ capt_var_exn $+ capt_exp $--> Collection.add &:: "add" <>$ capt_var_exn $+ capt_exp $--> Collection.add
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $--> Collection.addAll_at_index &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $--> Collection.addAll_at_index
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "addAll" <>$ capt_var_exn $+ capt_exp $--> Collection.addAll &:: "addAll" <>$ capt_var_exn $+ capt_exp $--> Collection.addAll
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_at_index &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_at_index
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "remove" <>$ capt_var_exn $+ capt_exp $--> Collection.remove_at_index &:: "remove" <>$ capt_var_exn $+ capt_exp $--> Collection.remove_at_index
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "set" <>$ capt_var_exn $+ capt_exp $+ capt_exp $--> Collection.set_at_index &:: "set" <>$ capt_var_exn $+ capt_exp $+ capt_exp $--> Collection.set_at_index
; +PatternMatch.implements_collection &:: "size" <>$ capt_exp $!--> Collection.size ; +PatternMatch.Java.implements_collection &:: "size" <>$ capt_exp $!--> Collection.size
; +PatternMatch.implements_collection &:: "toArray" <>$ capt_exp $+...$--> create_copy_array ; +PatternMatch.Java.implements_collection
; +PatternMatch.implements_collections &:: "emptyList" <>--> Collection.new_collection &:: "toArray" <>$ capt_exp $+...$--> create_copy_array
; +PatternMatch.implements_collections &:: "emptyMap" <>--> Collection.new_collection ; +PatternMatch.Java.implements_collections &:: "emptyList" <>--> Collection.new_collection
; +PatternMatch.implements_collections &:: "emptySet" <>--> Collection.new_collection ; +PatternMatch.Java.implements_collections &:: "emptyMap" <>--> Collection.new_collection
; +PatternMatch.implements_collections &:: "singleton" <>--> Collection.singleton_collection ; +PatternMatch.Java.implements_collections &:: "emptySet" <>--> Collection.new_collection
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "singleton" <>--> Collection.singleton_collection
; +PatternMatch.Java.implements_collections
&:: "singletonList" <>--> Collection.singleton_collection &:: "singletonList" <>--> Collection.singleton_collection
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "singletonList" <>--> Collection.singleton_collection &:: "singletonList" <>--> Collection.singleton_collection
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "singletonMap" <>--> Collection.singleton_collection &:: "singletonMap" <>--> Collection.singleton_collection
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "singletonMap" <>--> Collection.singleton_collection &:: "singletonMap" <>--> Collection.singleton_collection
; +PatternMatch.implements_collections &::+ unmodifiable <>$ capt_exp $--> Collection.iterator ; +PatternMatch.Java.implements_collections
; +PatternMatch.implements_google "common.collect.ImmutableSet" &::+ unmodifiable <>$ capt_exp $--> Collection.iterator
; +PatternMatch.Java.implements_google "common.collect.ImmutableSet"
&:: "of" &++> Collection.of_list &:: "of" &++> Collection.of_list
; +PatternMatch.implements_google "common.base.Preconditions" ; +PatternMatch.Java.implements_google "common.base.Preconditions"
&:: "checkArgument" <>$ capt_exp $+...$--> Preconditions.check_argument &:: "checkArgument" <>$ capt_exp $+...$--> Preconditions.check_argument
; +PatternMatch.implements_google "common.base.Preconditions" ; +PatternMatch.Java.implements_google "common.base.Preconditions"
&:: "checkNotNull" <>$ capt_exp $+...$--> id &:: "checkNotNull" <>$ capt_exp $+...$--> id
; +PatternMatch.implements_google "common.base.Preconditions" ; +PatternMatch.Java.implements_google "common.base.Preconditions"
&:: "checkState" <>$ capt_exp $+...$--> Preconditions.check_argument &:: "checkState" <>$ capt_exp $+...$--> Preconditions.check_argument
; +PatternMatch.implements_infer_annotation "Assertions" ; +PatternMatch.Java.implements_infer_annotation "Assertions"
&:: "assertGet" <>$ capt_exp $+ capt_exp $--> InferAnnotation.assert_get &:: "assertGet" <>$ capt_exp $+ capt_exp $--> InferAnnotation.assert_get
; +PatternMatch.implements_infer_annotation "Assertions" ; +PatternMatch.Java.implements_infer_annotation "Assertions"
&:: "assertNotNull" <>$ capt_exp $+...$--> id &:: "assertNotNull" <>$ capt_exp $+...$--> id
; +PatternMatch.implements_infer_annotation "Assertions" ; +PatternMatch.Java.implements_infer_annotation "Assertions"
&:: "assumeNotNull" <>$ capt_exp $+...$--> id &:: "assumeNotNull" <>$ capt_exp $+...$--> id
; +PatternMatch.implements_infer_annotation "Assertions" ; +PatternMatch.Java.implements_infer_annotation "Assertions"
&:: "nullsafeFIXME" <>$ capt_exp $+...$--> id &:: "nullsafeFIXME" <>$ capt_exp $+...$--> id
; +PatternMatch.implements_infer_annotation "Assertions" &::.*--> no_model ; +PatternMatch.Java.implements_infer_annotation "Assertions" &::.*--> no_model
; +PatternMatch.implements_io "File" &:: "listFiles" <>$ capt_exp $--> File.list_files ; +PatternMatch.Java.implements_io "File" &:: "listFiles" <>$ capt_exp $--> File.list_files
; +PatternMatch.implements_io "InputStream" ; +PatternMatch.Java.implements_io "InputStream"
&:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read
; +PatternMatch.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext ; +PatternMatch.Java.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext
; +PatternMatch.implements_iterator &:: "next" <>$ capt_exp $!--> Collection.next ; +PatternMatch.Java.implements_iterator &:: "next" <>$ capt_exp $!--> Collection.next
; +PatternMatch.implements_lang "CharSequence" ; +PatternMatch.Java.implements_lang "CharSequence"
&:: "<init>" <>$ capt_exp $+ capt_exp $--> JavaString.copy_constructor &:: "<init>" <>$ capt_exp $+ capt_exp $--> JavaString.copy_constructor
; +PatternMatch.implements_lang "CharSequence" ; +PatternMatch.Java.implements_lang "CharSequence"
&:: "<init>" <>$ capt_exp $+ capt_exp_of_prim_typ char_array &:: "<init>" <>$ capt_exp $+ capt_exp_of_prim_typ char_array
$--> JavaString.constructor_from_array $--> JavaString.constructor_from_array
; +PatternMatch.implements_lang "CharSequence" ; +PatternMatch.Java.implements_lang "CharSequence"
&:: "charAt" <>$ capt_exp $+ capt_exp $--> JavaString.charAt &:: "charAt" <>$ capt_exp $+ capt_exp $--> JavaString.charAt
; +PatternMatch.implements_lang "CharSequence" ; +PatternMatch.Java.implements_lang "CharSequence"
&:: "equals" &:: "equals"
$ any_arg_of_typ (+PatternMatch.implements_lang "CharSequence") $ any_arg_of_typ (+PatternMatch.Java.implements_lang "CharSequence")
$+ any_arg_of_typ (+PatternMatch.implements_lang "CharSequence") $+ any_arg_of_typ (+PatternMatch.Java.implements_lang "CharSequence")
$--> by_value Dom.Val.Itv.unknown_bool $--> by_value Dom.Val.Itv.unknown_bool
; +PatternMatch.implements_lang "CharSequence" ; +PatternMatch.Java.implements_lang "CharSequence"
&:: "length" <>$ capt_exp $!--> JavaString.length &:: "length" <>$ capt_exp $!--> JavaString.length
; +PatternMatch.implements_lang "CharSequence" ; +PatternMatch.Java.implements_lang "CharSequence"
&:: "substring" <>$ any_arg $+ capt_exp $+ capt_exp $--> JavaString.substring &:: "substring" <>$ any_arg $+ capt_exp $+ capt_exp $--> JavaString.substring
; +PatternMatch.implements_lang "Class" ; +PatternMatch.Java.implements_lang "Class"
&:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string
; +PatternMatch.implements_lang "Class" ; +PatternMatch.Java.implements_lang "Class"
&:: "getEnumConstants" <>$ capt_exp $--> JavaClass.get_enum_constants &:: "getEnumConstants" <>$ capt_exp $--> JavaClass.get_enum_constants
; +PatternMatch.implements_lang "Class" &:: "getFields" <>$ capt_exp $--> JavaClass.get_fields ; +PatternMatch.Java.implements_lang "Class"
; +PatternMatch.implements_lang "Enum" &:: "name" &::.*--> JavaString.inferbo_constant_string &:: "getFields" <>$ capt_exp $--> JavaClass.get_fields
; +PatternMatch.implements_lang "Integer" ; +PatternMatch.Java.implements_lang "Enum"
&:: "name" &::.*--> JavaString.inferbo_constant_string
; +PatternMatch.Java.implements_lang "Integer"
&:: "intValue" <>$ capt_exp $--> JavaInteger.intValue &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue
; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf ; +PatternMatch.Java.implements_lang "Integer"
; +PatternMatch.implements_lang "Iterable" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf
; +PatternMatch.Java.implements_lang "Iterable"
&:: "iterator" <>$ capt_exp $!--> Collection.iterator &:: "iterator" <>$ capt_exp $!--> Collection.iterator
; +PatternMatch.implements_lang "Math" ; +PatternMatch.Java.implements_lang "Math"
&:: "max" <>$ capt_exp $+ capt_exp &:: "max" <>$ capt_exp $+ capt_exp
$--> eval_binop ~f:(Itv.max_sem ~use_minmax_bound:true) $--> eval_binop ~f:(Itv.max_sem ~use_minmax_bound:true)
; +PatternMatch.implements_lang "Math" ; +PatternMatch.Java.implements_lang "Math"
&:: "min" <>$ capt_exp $+ capt_exp &:: "min" <>$ capt_exp $+ capt_exp
$--> eval_binop ~f:(Itv.min_sem ~use_minmax_bound:true) $--> eval_binop ~f:(Itv.min_sem ~use_minmax_bound:true)
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "<init>" <>$ capt_exp $--> JavaString.empty_constructor &:: "<init>" <>$ capt_exp $--> JavaString.empty_constructor
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "indexOf" <>$ capt_exp $+ any_arg $+...$--> JavaString.indexOf &:: "indexOf" <>$ capt_exp $+ any_arg $+...$--> JavaString.indexOf
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "lastIndexOf" <>$ capt_exp $+ any_arg $+...$--> JavaString.indexOf &:: "lastIndexOf" <>$ capt_exp $+ any_arg $+...$--> JavaString.indexOf
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "replace" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ any_arg_of_prim_typ int_typ &:: "replace" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ any_arg_of_prim_typ int_typ
$--> JavaString.replace $--> JavaString.replace
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "split" <>$ any_arg $+ any_arg $+ capt_exp $--> JavaString.split_with_limit &:: "split" <>$ any_arg $+ any_arg $+ capt_exp $--> JavaString.split_with_limit
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "split" <>$ capt_exp $+ any_arg $--> JavaString.split &:: "split" <>$ capt_exp $+ any_arg $--> JavaString.split
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "startsWith" &:: "startsWith"
$ any_arg_of_typ (+PatternMatch.implements_lang "String") $ any_arg_of_typ (+PatternMatch.Java.implements_lang "String")
$+ any_arg_of_typ (+PatternMatch.implements_lang "String") $+ any_arg_of_typ (+PatternMatch.Java.implements_lang "String")
$--> by_value Dom.Val.Itv.unknown_bool $--> by_value Dom.Val.Itv.unknown_bool
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end
; +PatternMatch.implements_lang "StringBuilder" ; +PatternMatch.Java.implements_lang "StringBuilder"
&:: "append" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat &:: "append" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat
; +PatternMatch.implements_lang "StringBuilder" &:: "toString" <>$ capt_exp $+...$--> id ; +PatternMatch.Java.implements_lang "StringBuilder" &:: "toString" <>$ capt_exp $+...$--> id
; +PatternMatch.implements_list &:: "listIterator" <>$ capt_exp $+...$--> Collection.iterator ; +PatternMatch.Java.implements_list
; +PatternMatch.implements_list &:: "subList" <>$ any_arg $+ capt_exp $+ capt_exp &:: "listIterator" <>$ capt_exp $+...$--> Collection.iterator
$--> Collection.subList ; +PatternMatch.Java.implements_list
; +PatternMatch.implements_map &:: "entrySet" <>$ capt_exp $!--> Collection.iterator &:: "subList" <>$ any_arg $+ capt_exp $+ capt_exp $--> Collection.subList
; +PatternMatch.implements_map &:: "keySet" <>$ capt_exp $!--> Collection.iterator ; +PatternMatch.Java.implements_map &:: "entrySet" <>$ capt_exp $!--> Collection.iterator
; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ capt_exp ; +PatternMatch.Java.implements_map &:: "keySet" <>$ capt_exp $!--> Collection.iterator
; +PatternMatch.Java.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ capt_exp
$--> Collection.put_with_elem $--> Collection.put_with_elem
; +PatternMatch.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp ; +PatternMatch.Java.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp
$--> Collection.putAll $--> Collection.putAll
; +PatternMatch.implements_map &:: "size" <>$ capt_exp $!--> Collection.size ; +PatternMatch.Java.implements_map &:: "size" <>$ capt_exp $!--> Collection.size
; +PatternMatch.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator ; +PatternMatch.Java.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator
; +PatternMatch.implements_nio "ByteBuffer" &:: "get" <>$ capt_exp $--> ByteBuffer.get_int ; +PatternMatch.Java.implements_nio "ByteBuffer"
; +PatternMatch.implements_nio "ByteBuffer" &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int &:: "get" <>$ capt_exp $--> ByteBuffer.get_int
; +PatternMatch.implements_nio "ByteBuffer" &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int ; +PatternMatch.Java.implements_nio "ByteBuffer"
; +PatternMatch.implements_nio "ByteBuffer" &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int
; +PatternMatch.Java.implements_nio "ByteBuffer"
&:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int
; +PatternMatch.Java.implements_nio "ByteBuffer"
&:: "getShort" <>$ capt_exp $--> ByteBuffer.get_int &:: "getShort" <>$ capt_exp $--> ByteBuffer.get_int
; +PatternMatch.implements_nio "channels.FileChannel" ; +PatternMatch.Java.implements_nio "channels.FileChannel"
&:: "read" <>$ any_arg $+ capt_exp $+ any_arg $--> FileChannel.read &:: "read" <>$ any_arg $+ capt_exp $+ any_arg $--> FileChannel.read
; +PatternMatch.implements_org_json "JSONArray" ; +PatternMatch.Java.implements_org_json "JSONArray"
&:: "<init>" <>$ capt_var_exn &:: "<init>" <>$ capt_var_exn
$+ capt_exp_of_typ (+PatternMatch.implements_collection) $+ capt_exp_of_typ (+PatternMatch.Java.implements_collection)
$--> Collection.init_with_arg $--> Collection.init_with_arg
; +PatternMatch.implements_org_json "JSONArray" ; +PatternMatch.Java.implements_org_json "JSONArray"
&:: "length" <>$ capt_exp $!--> Collection.size &:: "length" <>$ capt_exp $!--> Collection.size
; +PatternMatch.implements_org_json "JSONArray" ; +PatternMatch.Java.implements_org_json "JSONArray"
&:: "put" <>$ capt_var_exn $+...$--> Collection.put &:: "put" <>$ capt_var_exn $+...$--> Collection.put
; +PatternMatch.implements_pseudo_collection ; +PatternMatch.Java.implements_pseudo_collection
&:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg $--> Collection.put &:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg $--> Collection.put
; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size ; +PatternMatch.Java.implements_pseudo_collection
&:: "size" <>$ capt_exp $!--> Collection.size
; (* Java linked list models *) ; (* Java linked list models *)
+PatternMatch.implements_app_activity &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next +PatternMatch.Java.implements_app_activity
; +PatternMatch.implements_app_fragment &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
; +PatternMatch.Java.implements_app_fragment
&:: "getParentFragment" <>$ capt_arg $!--> JavaLinkedList.next &:: "getParentFragment" <>$ capt_arg $!--> JavaLinkedList.next
; +PatternMatch.implements_graphql_story ; +PatternMatch.Java.implements_graphql_story
&:: "getAttachedStory" <>$ capt_arg $!--> JavaLinkedList.next &:: "getAttachedStory" <>$ capt_arg $!--> JavaLinkedList.next
; +PatternMatch.implements_psi_element &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next ; +PatternMatch.Java.implements_psi_element
; +PatternMatch.implements_view_group &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
; +PatternMatch.implements_view_parent &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next ; +PatternMatch.Java.implements_view_group
] &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
; +PatternMatch.Java.implements_view_parent
&:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next ]
end end

8
infer/src/bufferoverrun/bufferOverrunTypModels.ml
Unescape View File

@ -35,7 +35,7 @@ let dispatch : (Tenv.t, typ_model, unit) ProcnameDispatcher.TypName.dispatcher =
make_dispatcher make_dispatcher
[ -"std" &:: "array" < capt_typ &+ capt_int >--> std_array [ -"std" &:: "array" < capt_typ &+ capt_int >--> std_array
; -"std" &:: "vector" < any_typ &+ any_typ >--> std_vector ; -"std" &:: "vector" < any_typ &+ any_typ >--> std_vector
; +PatternMatch.implements_collection &::.*--> Java.collection ; +PatternMatch.Java.implements_collection &::.*--> Java.collection
; +PatternMatch.implements_iterator &::.*--> Java.collection ; +PatternMatch.Java.implements_iterator &::.*--> Java.collection
; +PatternMatch.implements_lang "Integer" &::.*--> Java.integer ; +PatternMatch.Java.implements_lang "Integer" &::.*--> Java.integer
; +PatternMatch.implements_org_json "JSONArray" &::.*--> Java.collection ] ; +PatternMatch.Java.implements_org_json "JSONArray" &::.*--> Java.collection ]

4
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -33,7 +33,7 @@ let is_allocator tenv pname =
| Procname.Java pname_java -> | Procname.Java pname_java ->
let is_throwable () = let is_throwable () =
let class_name = Procname.Java.get_class_type_name pname_java in let class_name = Procname.Java.get_class_type_name pname_java in
PatternMatch.is_throwable tenv class_name PatternMatch.Java.is_throwable tenv class_name
in in
Procname.is_constructor pname Procname.is_constructor pname
&& (not (BuiltinDecl.is_declared pname)) && (not (BuiltinDecl.is_declared pname))
@ -43,7 +43,7 @@ let is_allocator tenv pname =
let check_attributes check tenv pname = let check_attributes check tenv pname =
PatternMatch.check_class_attributes check tenv pname PatternMatch.Java.check_class_attributes check tenv pname
|| Annotations.pname_has_return_annot pname check || Annotations.pname_has_return_annot pname check

6
infer/src/checkers/inefficientKeysetIterator.ml
Unescape View File

@ -27,7 +27,7 @@ let find_first_arg_id ~fun_name ~class_name_f ~lhs_f = function
let implements_map tenv s = let implements_map tenv s =
PatternMatch.implements_map tenv s || PatternMatch.implements_androidx_map tenv s PatternMatch.Java.implements_map tenv s || PatternMatch.Java.implements_androidx_map tenv s
(** If given a node that has 4 instructions and calls fun_name, pickup bcvarY, i.e. variable for the (** If given a node that has 4 instructions and calls fun_name, pickup bcvarY, i.e. variable for the
@ -110,11 +110,11 @@ let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} =
(fun loop_head loop_nodes -> (fun loop_head loop_nodes ->
if if
find_first_arg_pvar loop_head ~fun_name:"hasNext" find_first_arg_pvar loop_head ~fun_name:"hasNext"
~class_name_f:(PatternMatch.implements_iterator tenv) ~class_name_f:(PatternMatch.Java.implements_iterator tenv)
|> Option.is_some |> Option.is_some
then then
when_dominating_preds_satisfy idom loop_head ~fun_name:"iterator" when_dominating_preds_satisfy idom loop_head ~fun_name:"iterator"
~class_name_f:(PatternMatch.implements_set tenv) ~f:(fun itr_node _ -> ~class_name_f:(PatternMatch.Java.implements_set tenv) ~f:(fun itr_node _ ->
when_dominating_preds_satisfy idom itr_node ~fun_name:"keySet" when_dominating_preds_satisfy idom itr_node ~fun_name:"keySet"
~class_name_f:(implements_map tenv) ~f:(fun _keySet_node get_pvar -> ~class_name_f:(implements_map tenv) ~f:(fun _keySet_node get_pvar ->
report_matching_get proc_desc err_log tenv get_pvar loop_nodes ) ) ) report_matching_get proc_desc err_log tenv get_pvar loop_nodes ) ) )

189
infer/src/checkers/purityModels.ml
Unescape View File

@ -50,105 +50,112 @@ module ProcName = struct
; -"__variable_initialization" <>--> PurityDomain.pure ; -"__variable_initialization" <>--> PurityDomain.pure
; +(fun _ name -> BuiltinDecl.is_declared (Procname.from_string_c_fun name)) ; +(fun _ name -> BuiltinDecl.is_declared (Procname.from_string_c_fun name))
<>--> PurityDomain.impure_global <>--> PurityDomain.impure_global
; +PatternMatch.implements_android "text.TextUtils" &:: "isEmpty" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_android "text.TextUtils" &:: "isEmpty" <>--> PurityDomain.pure
; +PatternMatch.implements_android "view.ViewGroup" &:: "getChildAt" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_android "view.ViewGroup"
; +PatternMatch.implements_android "view.View" &::+ startsWith "get" <>--> PurityDomain.pure &:: "getChildAt" <>--> PurityDomain.pure
; +PatternMatch.implements_android "view.View" ; +PatternMatch.Java.implements_android "view.View"
&::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.Java.implements_android "view.View"
&::+ startsWith "findViewById" <>--> PurityDomain.pure &::+ startsWith "findViewById" <>--> PurityDomain.pure
; +PatternMatch.implements_android "view.ViewGroup" ; +PatternMatch.Java.implements_android "view.ViewGroup"
&:: "getChildCount" <>--> PurityDomain.pure &:: "getChildCount" <>--> PurityDomain.pure
; +PatternMatch.implements_android "content.Context" ; +PatternMatch.Java.implements_android "content.Context"
&::+ startsWith "get" <>--> PurityDomain.pure &::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.implements_android "content.res.Resources" ; +PatternMatch.Java.implements_android "content.res.Resources"
&::+ startsWith "get" <>--> PurityDomain.pure &::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.implements_arrays &:: "asList" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_arrays &:: "asList" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Iterable" &:: "iterator" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Iterable" &:: "iterator" <>--> PurityDomain.pure
; +PatternMatch.implements_list &:: "listIterator" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_list &:: "listIterator" <>--> PurityDomain.pure
; +PatternMatch.implements_collection &:: "iterator" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_collection &:: "iterator" <>--> PurityDomain.pure
; +PatternMatch.implements_iterator &:: "hasNext" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_iterator &:: "hasNext" <>--> PurityDomain.pure
; +PatternMatch.implements_iterator &:: "next" <>--> modifies_first ; +PatternMatch.Java.implements_iterator &:: "next" <>--> modifies_first
; +PatternMatch.implements_iterator &:: "remove" <>--> modifies_first ; +PatternMatch.Java.implements_iterator &:: "remove" <>--> modifies_first
; +PatternMatch.implements_collection &:: "size" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_collection &:: "size" <>--> PurityDomain.pure
; +PatternMatch.implements_collection &:: "add" <>--> modifies_first ; +PatternMatch.Java.implements_collection &:: "add" <>--> modifies_first
; +PatternMatch.implements_collection &:: "addAll" <>--> modifies_first ; +PatternMatch.Java.implements_collection &:: "addAll" <>--> modifies_first
; +PatternMatch.implements_collection &:: "remove" <>--> modifies_first ; +PatternMatch.Java.implements_collection &:: "remove" <>--> modifies_first
; +PatternMatch.implements_collection &:: "isEmpty" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_collection &:: "isEmpty" <>--> PurityDomain.pure
; +PatternMatch.implements_collection &:: "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_collection &:: "get" <>--> PurityDomain.pure
; +PatternMatch.implements_collection &:: "set" <>--> modifies_first ; +PatternMatch.Java.implements_collection &:: "set" <>--> modifies_first
; +PatternMatch.implements_list &:: "contains" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_list &:: "contains" <>--> PurityDomain.pure
; +PatternMatch.implements_collection &:: "contains" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_collection &:: "contains" <>--> PurityDomain.pure
; +PatternMatch.implements_enumeration &:: "hasMoreElements" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_enumeration &:: "hasMoreElements" <>--> PurityDomain.pure
; +PatternMatch.implements_enumeration &:: "nextElement" <>--> modifies_first ; +PatternMatch.Java.implements_enumeration &:: "nextElement" <>--> modifies_first
; +PatternMatch.implements_google "common.base.Preconditions" ; +PatternMatch.Java.implements_google "common.base.Preconditions"
&::+ startsWith "check" <>--> PurityDomain.pure &::+ startsWith "check" <>--> PurityDomain.pure
; +PatternMatch.implements_inject "Provider" &:: "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_inject "Provider" &:: "get" <>--> PurityDomain.pure
; +PatternMatch.implements_io "File" &::+ startsWith "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_io "File" &::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.implements_io "OutputStream" &:: "write" <>--> PurityDomain.impure_global ; +PatternMatch.Java.implements_io "OutputStream" &:: "write" <>--> PurityDomain.impure_global
; +PatternMatch.implements_io "InputStream" &:: "read" <>--> PurityDomain.impure_global ; +PatternMatch.Java.implements_io "InputStream" &:: "read" <>--> PurityDomain.impure_global
; +PatternMatch.implements_io "PrintStream" &:: "print" <>--> PurityDomain.impure_global ; +PatternMatch.Java.implements_io "PrintStream" &:: "print" <>--> PurityDomain.impure_global
; +PatternMatch.implements_io "PrintStream" &:: "println" <>--> PurityDomain.impure_global ; +PatternMatch.Java.implements_io "PrintStream"
; +PatternMatch.implements_io "Reader" &:: "read" <>--> PurityDomain.impure_global &:: "println" <>--> PurityDomain.impure_global
; +PatternMatch.implements_io "BufferedReader" &:: "readLine" <>--> PurityDomain.impure_global ; +PatternMatch.Java.implements_io "Reader" &:: "read" <>--> PurityDomain.impure_global
; +PatternMatch.implements_jackson "databind.JsonDeserializer" ; +PatternMatch.Java.implements_io "BufferedReader"
&:: "readLine" <>--> PurityDomain.impure_global
; +PatternMatch.Java.implements_jackson "databind.JsonDeserializer"
&:: "deserialize" <>--> PurityDomain.pure &:: "deserialize" <>--> PurityDomain.pure
; +PatternMatch.implements_jackson "core.JsonParser" &:: "nextToken" <>--> modifies_first ; +PatternMatch.Java.implements_jackson "core.JsonParser" &:: "nextToken" <>--> modifies_first
; +PatternMatch.implements_jackson "core.JsonParser" ; +PatternMatch.Java.implements_jackson "core.JsonParser"
&:: "getCurrentName" <>--> PurityDomain.pure &:: "getCurrentName" <>--> PurityDomain.pure
; +PatternMatch.implements_jackson "core.JsonParser" &::+ getStarValue <>--> PurityDomain.pure ; +PatternMatch.Java.implements_jackson "core.JsonParser"
; +PatternMatch.implements_jackson "core.JsonParser" &::+ getStarValue <>--> PurityDomain.pure
; +PatternMatch.Java.implements_jackson "core.JsonParser"
&::+ startsWith "get" <>--> PurityDomain.pure &::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.implements_pseudo_collection &:: "size" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_pseudo_collection &:: "size" <>--> PurityDomain.pure
; +PatternMatch.implements_pseudo_collection &:: "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_pseudo_collection &:: "get" <>--> PurityDomain.pure
; +PatternMatch.implements_pseudo_collection &:: "valueAt" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_pseudo_collection &:: "valueAt" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Math" &:: "random" <>--> PurityDomain.impure_global ; +PatternMatch.Java.implements_lang "Math" &:: "random" <>--> PurityDomain.impure_global
; +PatternMatch.implements_lang "Math" &::.*--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Math" &::.*--> PurityDomain.pure
(* for (int|short|byte...)Value*) (* for (int|short|byte...)Value*)
; +PatternMatch.implements_lang "Number" &::+ endsWith "Value" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Number" &::+ endsWith "Value" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Boolean" &:: "valueOf" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Boolean" &:: "valueOf" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Boolean" &:: "parseBoolean" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Boolean" &:: "parseBoolean" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Boolean" &::+ endsWith "Value" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Boolean" &::+ endsWith "Value" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Number" &:: "valueOf" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Number" &:: "valueOf" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "length" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "length" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "charAt" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "charAt" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "substring" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "substring" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "CharSequence" &:: "charAt" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "CharSequence" &:: "charAt" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "equals" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "equals" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "startsWith" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "startsWith" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "valueOf" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "valueOf" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "String" &:: "replace" <>--> modifies_first ; +PatternMatch.Java.implements_lang "String" &:: "replace" <>--> modifies_first
; +PatternMatch.implements_lang "String" &:: "format" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "format" <>--> PurityDomain.pure
(* String.hashCode is deterministic whereas Object's might not be *) (* String.hashCode is deterministic whereas Object's might not be *)
; +PatternMatch.implements_lang "String" &:: "hashCode" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "String" &:: "hashCode" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "StringBuilder" &:: "<init>" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "StringBuilder" &:: "<init>" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "StringBuilder" &:: "append" <>--> modifies_first ; +PatternMatch.Java.implements_lang "StringBuilder" &:: "append" <>--> modifies_first
; +PatternMatch.implements_lang "StringBuilder" &:: "length" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "StringBuilder" &:: "length" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Object" &:: "clone" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Object" &:: "clone" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Object" &:: "equals" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Object" &:: "equals" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Object" &:: "toString" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Object" &:: "toString" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Object" &:: "getClass" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Object" &:: "getClass" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Class" &:: "getSimpleName" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Class" &:: "getSimpleName" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Class" &::+ startsWith "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Class" &::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "System" &:: "arraycopy" <>--> modifies_third ; +PatternMatch.Java.implements_lang "System" &:: "arraycopy" <>--> modifies_third
; +PatternMatch.implements_lang "Enum" &:: "valueOf" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Enum" &:: "valueOf" <>--> PurityDomain.pure
; +PatternMatch.implements_lang "Enum" &:: "ordinal" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_lang "Enum" &:: "ordinal" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "isEmpty" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "isEmpty" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "get" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "put" <>--> modifies_first ; +PatternMatch.Java.implements_map &:: "put" <>--> modifies_first
; +PatternMatch.implements_map &:: "putAll" <>--> modifies_first ; +PatternMatch.Java.implements_map &:: "putAll" <>--> modifies_first
; +PatternMatch.implements_map &:: "containsKey" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "containsKey" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "keySet" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "keySet" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "values" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "values" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "entrySet" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "entrySet" <>--> PurityDomain.pure
; +PatternMatch.implements_map &:: "size" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map &:: "size" <>--> PurityDomain.pure
; +PatternMatch.implements_map_entry &:: "getKey" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map_entry &:: "getKey" <>--> PurityDomain.pure
; +PatternMatch.implements_map_entry &:: "getValue" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_map_entry &:: "getValue" <>--> PurityDomain.pure
; +PatternMatch.implements_queue &:: "poll" <>--> modifies_first ; +PatternMatch.Java.implements_queue &:: "poll" <>--> modifies_first
; +PatternMatch.implements_queue &:: "add" <>--> modifies_first ; +PatternMatch.Java.implements_queue &:: "add" <>--> modifies_first
; +PatternMatch.implements_queue &:: "remove" <>--> modifies_first ; +PatternMatch.Java.implements_queue &:: "remove" <>--> modifies_first
; +PatternMatch.implements_queue &:: "peek" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_queue &:: "peek" <>--> PurityDomain.pure
; +PatternMatch.implements_list &:: "subList" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_list &:: "subList" <>--> PurityDomain.pure
; +PatternMatch.implements_arrays &:: "binarySearch" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_arrays &:: "binarySearch" <>--> PurityDomain.pure
; +PatternMatch.implements_org_json "JSONArray" &::+ startsWith "get" <>--> PurityDomain.pure ; +PatternMatch.Java.implements_org_json "JSONArray"
; +PatternMatch.implements_org_json "JSONObject" &::+ startsWith "get" <>--> PurityDomain.pure &::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.implements_org_json "JSONArray" &:: "length" <>--> PurityDomain.pure ] ; +PatternMatch.Java.implements_org_json "JSONObject"
&::+ startsWith "get" <>--> PurityDomain.pure
; +PatternMatch.Java.implements_org_json "JSONArray" &:: "length" <>--> PurityDomain.pure ]
end end

2
infer/src/concurrency/RacerDModels.ml
Unescape View File

@ -364,7 +364,7 @@ let is_thread_safe_method pname tenv =
let is_marked_thread_safe pname tenv = let is_marked_thread_safe pname tenv =
((* current class not marked [@NotThreadSafe] *) ((* current class not marked [@NotThreadSafe] *)
not not
(PatternMatch.check_current_class_attributes Annotations.ia_is_not_thread_safe tenv pname)) (PatternMatch.Java.check_current_class_attributes Annotations.ia_is_not_thread_safe tenv pname))
&& ConcurrencyModels.find_override_or_superclass_annotated is_thread_safe tenv pname && ConcurrencyModels.find_override_or_superclass_annotated is_thread_safe tenv pname
|> Option.is_some |> Option.is_some

71
infer/src/cost/costModels.ml
Unescape View File

@ -192,75 +192,82 @@ module Call = struct
; -"NSString" &:: "componentsSeparatedByString:" <>$ capt_exp $+ capt_exp ; -"NSString" &:: "componentsSeparatedByString:" <>$ capt_exp $+ capt_exp
$--> NSString.op_on_two_str BasicCost.mult $--> NSString.op_on_two_str BasicCost.mult
~of_function:"NSString.componentsSeparatedByString:" ~of_function:"NSString.componentsSeparatedByString:"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "sort" $ capt_exp &:: "sort" $ capt_exp
$+...$--> BoundsOfCollection.n_log_n_length ~of_function:"Collections.sort" $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"Collections.sort"
; +PatternMatch.implements_list &:: "sort" $ capt_exp ; +PatternMatch.Java.implements_list
&:: "sort" $ capt_exp
$+...$--> BoundsOfCollection.n_log_n_length ~of_function:"List.sort" $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"List.sort"
; +PatternMatch.implements_arrays &:: "sort" $ capt_exp ; +PatternMatch.Java.implements_arrays
&:: "sort" $ capt_exp
$+...$--> BoundsOfArray.n_log_n_length ~of_function:"Arrays.sort" $+...$--> BoundsOfArray.n_log_n_length ~of_function:"Arrays.sort"
; +PatternMatch.implements_list &:: "contains" <>$ capt_exp ; +PatternMatch.Java.implements_list
&:: "contains" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"List.contains" $+...$--> BoundsOfCollection.linear_length ~of_function:"List.contains"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "binarySearch" <>$ capt_exp &:: "binarySearch" <>$ capt_exp
$+...$--> BoundsOfCollection.logarithmic_length ~of_function:"Collections.binarySearch" $+...$--> BoundsOfCollection.logarithmic_length ~of_function:"Collections.binarySearch"
; +PatternMatch.implements_arrays &:: "binarySearch" <>$ capt_exp ; +PatternMatch.Java.implements_arrays
&:: "binarySearch" <>$ capt_exp
$+...$--> BoundsOfArray.logarithmic_length ~of_function:"Arrays.binarySearch" $+...$--> BoundsOfArray.logarithmic_length ~of_function:"Arrays.binarySearch"
; +PatternMatch.implements_arrays &:: "copyOf" <>$ any_arg $+ capt_exp ; +PatternMatch.Java.implements_arrays
&:: "copyOf" <>$ any_arg $+ capt_exp
$+...$--> linear ~of_function:"Arrays.copyOf" $+...$--> linear ~of_function:"Arrays.copyOf"
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "addAll" <>$ any_arg $+ any_arg $+ capt_exp &:: "addAll" <>$ any_arg $+ any_arg $+ capt_exp
$--> BoundsOfCollection.linear_length ~of_function:"Collection.addAll" $--> BoundsOfCollection.linear_length ~of_function:"Collection.addAll"
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "addAll" <>$ any_arg $+ capt_exp &:: "addAll" <>$ any_arg $+ capt_exp
$--> BoundsOfCollection.linear_length ~of_function:"Collection.addAll" $--> BoundsOfCollection.linear_length ~of_function:"Collection.addAll"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "copy" <>$ capt_exp &:: "copy" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.copy" $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.copy"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "fill" <>$ capt_exp &:: "fill" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.fill" $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.fill"
; +PatternMatch.implements_arrays &:: "fill" <>$ capt_exp ; +PatternMatch.Java.implements_arrays
&:: "fill" <>$ capt_exp
$+...$--> BoundsOfArray.linear_length ~of_function:"Arrays.fill" $+...$--> BoundsOfArray.linear_length ~of_function:"Arrays.fill"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "reverse" <>$ capt_exp &:: "reverse" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.reverse" $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.reverse"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "max" <>$ capt_exp &:: "max" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.max" $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.max"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "min" <>$ capt_exp &:: "min" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.min" $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.min"
; +PatternMatch.implements_collections ; +PatternMatch.Java.implements_collections
&:: "shuffle" <>$ capt_exp &:: "shuffle" <>$ capt_exp
$+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle" $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle"
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "indexOf" <>$ capt_exp &:: "indexOf" <>$ capt_exp
$+ capt_exp_of_typ (+PatternMatch.implements_lang "String") $+ capt_exp_of_typ (+PatternMatch.Java.implements_lang "String")
$--> JavaString.indexOf_str $--> JavaString.indexOf_str
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ capt_exp &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ capt_exp
$--> JavaString.indexOf_char_starting_from $--> JavaString.indexOf_char_starting_from
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $--> JavaString.indexOf_char &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $--> JavaString.indexOf_char
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&:: "substring" &:: "substring"
$ any_arg_of_typ (+PatternMatch.implements_lang "String") $ any_arg_of_typ (+PatternMatch.Java.implements_lang "String")
$+ capt_exp $+ capt_exp $--> JavaString.substring $+ capt_exp $+ capt_exp $--> JavaString.substring
; +PatternMatch.implements_inject "Provider" &:: "get" <>--> provider_get ; +PatternMatch.Java.implements_inject "Provider" &:: "get" <>--> provider_get
; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "<init>" <>--> unit_cost_model ; +PatternMatch.Java.implements_xmob_utils "IntHashMap" &:: "<init>" <>--> unit_cost_model
; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "getElement" <>--> unit_cost_model ; +PatternMatch.Java.implements_xmob_utils "IntHashMap"
; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "getElement" <>--> unit_cost_model
; +PatternMatch.Java.implements_xmob_utils "IntHashMap"
&:: "keys" <>$ capt_arg $--> IntHashMap.keys &:: "keys" <>$ capt_arg $--> IntHashMap.keys
; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "put" <>--> unit_cost_model ; +PatternMatch.Java.implements_xmob_utils "IntHashMap" &:: "put" <>--> unit_cost_model
; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "remove" <>--> unit_cost_model ; +PatternMatch.Java.implements_xmob_utils "IntHashMap" &:: "remove" <>--> unit_cost_model
; +PatternMatch.implements_google "common.collect.ImmutableSet" ; +PatternMatch.Java.implements_google "common.collect.ImmutableSet"
&:: "chooseTableSize" <>$ capt_exp $+...$--> ImmutableSet.choose_table_size &:: "chooseTableSize" <>$ capt_exp $+...$--> ImmutableSet.choose_table_size
; +PatternMatch.implements_google "common.collect.ImmutableSet" ; +PatternMatch.Java.implements_google "common.collect.ImmutableSet"
&:: "construct" <>$ capt_exp_of_prim_typ int_typ $+...$--> ImmutableSet.construct &:: "construct" <>$ capt_exp_of_prim_typ int_typ $+...$--> ImmutableSet.construct
; +PatternMatch.implements_google "common.collect.ImmutableSet" ; +PatternMatch.Java.implements_google "common.collect.ImmutableSet"
&:: "construct" <>$ any_arg $+ capt_exp_of_prim_typ int_typ &:: "construct" <>$ any_arg $+ capt_exp_of_prim_typ int_typ
$+...$--> ImmutableSet.construct ] $+...$--> ImmutableSet.construct ]
in in

2
infer/src/nullsafe/AnnotatedField.ml
Unescape View File

@ -29,7 +29,7 @@ let is_enum_value tenv ~class_typ (field_info : Struct.field_info) =
match (get_type_name class_typ, get_type_name field_info.typ) with match (get_type_name class_typ, get_type_name field_info.typ) with
(* enums values are fields which type is the same as the type of the enum class *) (* enums values are fields which type is the same as the type of the enum class *)
| Some class_name, Some field_type_name | Some class_name, Some field_type_name
when Typ.equal_name class_name field_type_name && PatternMatch.is_java_enum tenv class_name -> when Typ.equal_name class_name field_type_name && PatternMatch.Java.is_enum tenv class_name ->
true true
(* Could not fetch one of the class names, or they are different. Should not happen for enum values. *) (* Could not fetch one of the class names, or they are different. Should not happen for enum values. *)
| _ -> | _ ->

2
infer/src/nullsafe/Initializers.ml
Unescape View File

@ -107,7 +107,7 @@ let get_class pn =
let final_initializer_typestates_lazy tenv curr_pname curr_pdesc typecheck_proc = let final_initializer_typestates_lazy tenv curr_pname curr_pdesc typecheck_proc =
lazy lazy
(let is_initializer proc_attributes = (let is_initializer proc_attributes =
PatternMatch.method_is_initializer tenv proc_attributes PatternMatch.Java.method_is_initializer tenv proc_attributes
|| ||
let ia = let ia =
(* TODO(T62825735): support trusted callees for fields *) (* TODO(T62825735): support trusted callees for fields *)

2
infer/src/nullsafe/eradicate.ml
Unescape View File

@ -25,7 +25,7 @@ let callback1 ({IntraproceduralAnalysis.proc_desc= curr_pdesc; _} as analysis_da
has very special meaning and nullability limitations (it can never be null). has very special meaning and nullability limitations (it can never be null).
*) *)
TypeOrigin.This TypeOrigin.This
else if PatternMatch.is_override_of_java_lang_object_equals curr_pname then else if PatternMatch.Java.is_override_of_lang_object_equals curr_pname then
TypeOrigin.CurrMethodParameter ObjectEqualsOverride TypeOrigin.CurrMethodParameter ObjectEqualsOverride
else TypeOrigin.CurrMethodParameter (Normal param_signature) else TypeOrigin.CurrMethodParameter (Normal param_signature)
in in

4
infer/src/nullsafe/models.ml
Unescape View File

@ -48,7 +48,7 @@ let to_modelled_nullability ThirdPartyMethod.{ret_nullability; param_nullability
let get_special_method_modelled_nullability tenv proc_name = let get_special_method_modelled_nullability tenv proc_name =
let open IOption.Let_syntax in let open IOption.Let_syntax in
let* class_name = Procname.get_class_type_name proc_name in let* class_name = Procname.get_class_type_name proc_name in
if PatternMatch.is_java_enum tenv class_name then if PatternMatch.Java.is_enum tenv class_name then
match (Procname.get_method proc_name, Procname.get_parameters proc_name) with match (Procname.get_method proc_name, Procname.get_parameters proc_name) with
(* values() is a synthetic enum method that is never null *) (* values() is a synthetic enum method that is never null *)
| "values", [] -> | "values", [] ->
@ -138,7 +138,7 @@ let is_true_on_null proc_name = table_has_procedure true_on_null_table proc_name
let is_false_on_null proc_name = let is_false_on_null proc_name =
(* The only usecase for now - consider all overrides of `Object.equals()` correctly (* The only usecase for now - consider all overrides of `Object.equals()` correctly
implementing the Java specification contract (returning false on null). *) implementing the Java specification contract (returning false on null). *)
PatternMatch.is_override_of_java_lang_object_equals proc_name PatternMatch.Java.is_override_of_lang_object_equals proc_name
(** Check if the procedure is Map.containsKey(). *) (** Check if the procedure is Map.containsKey(). *)

59
infer/src/pulse/PulseModels.ml
Unescape View File

@ -859,7 +859,7 @@ module ProcNameDispatcher = struct
; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
; +match_builtin BuiltinDecl.__infer_initializer_list ; +match_builtin BuiltinDecl.__infer_initializer_list
<>$ capt_arg_payload $+...$--> Misc.id_first_arg <>$ capt_arg_payload $+...$--> Misc.id_first_arg
; +PatternMatch.implements_lang "System" &:: "exit" <>--> Misc.early_exit ; +PatternMatch.Java.implements_lang "System" &:: "exit" <>--> Misc.early_exit
; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size
; (* consider that all fbstrings are small strings to avoid false positives due to manual ; (* consider that all fbstrings are small strings to avoid false positives due to manual
ref-counting *) ref-counting *)
@ -892,9 +892,9 @@ module ProcNameDispatcher = struct
$++$--> StdFunction.operator_call $++$--> StdFunction.operator_call
; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload
$--> StdFunction.operator_equal $--> StdFunction.operator_equal
; +PatternMatch.implements_lang "Object" ; +PatternMatch.Java.implements_lang "Object"
&:: "clone" $ capt_arg_payload $--> JavaObject.clone &:: "clone" $ capt_arg_payload $--> JavaObject.clone
; ( +PatternMatch.implements_lang "System" ; ( +PatternMatch.Java.implements_lang "System"
&:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload &:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload
$+...$--> fun src dest -> Misc.shallow_copy_model "System.arraycopy" dest src ) $+...$--> fun src dest -> Misc.shallow_copy_model "System.arraycopy" dest src )
; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload
@ -988,54 +988,61 @@ module ProcNameDispatcher = struct
; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload
$--> StdVector.invalidate_references ShrinkToFit $--> StdVector.invalidate_references ShrinkToFit
; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add
; +PatternMatch.implements_list &:: "add" <>$ capt_arg_payload $+ capt_arg_payload ; +PatternMatch.Java.implements_list
$+ capt_arg_payload $--> JavaCollection.add_at &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload
; +PatternMatch.implements_collection $--> JavaCollection.add_at
; +PatternMatch.Java.implements_collection
&:: "remove" <>$ capt_arg_payload $+ any_arg $--> JavaCollection.remove &:: "remove" <>$ capt_arg_payload $+ any_arg $--> JavaCollection.remove
; +PatternMatch.implements_list &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload ; +PatternMatch.Java.implements_list
$+ any_arg $--> JavaCollection.remove_at &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload $+ any_arg
; +PatternMatch.implements_collection $--> JavaCollection.remove_at
; +PatternMatch.Java.implements_collection
&::+ (fun _ str -> StringSet.mem str pushback_modeled) &::+ (fun _ str -> StringSet.mem str pushback_modeled)
<>$ capt_arg_payload $+...$--> StdVector.push_back <>$ capt_arg_payload $+...$--> StdVector.push_back
; +PatternMatch.implements_queue ; +PatternMatch.Java.implements_queue
&::+ (fun _ str -> StringSet.mem str pushback_modeled) &::+ (fun _ str -> StringSet.mem str pushback_modeled)
<>$ capt_arg_payload $+...$--> StdVector.push_back <>$ capt_arg_payload $+...$--> StdVector.push_back
; +PatternMatch.implements_lang "StringBuilder" ; +PatternMatch.Java.implements_lang "StringBuilder"
&::+ (fun _ str -> StringSet.mem str pushback_modeled) &::+ (fun _ str -> StringSet.mem str pushback_modeled)
<>$ capt_arg_payload $+...$--> StdVector.push_back <>$ capt_arg_payload $+...$--> StdVector.push_back
; +PatternMatch.implements_lang "StringBuilder" ; +PatternMatch.Java.implements_lang "StringBuilder"
&:: "setLength" <>$ capt_arg_payload &:: "setLength" <>$ capt_arg_payload
$+...$--> StdVector.invalidate_references ShrinkToFit $+...$--> StdVector.invalidate_references ShrinkToFit
; +PatternMatch.implements_lang "String" ; +PatternMatch.Java.implements_lang "String"
&::+ (fun _ str -> StringSet.mem str pushback_modeled) &::+ (fun _ str -> StringSet.mem str pushback_modeled)
<>$ capt_arg_payload $+...$--> StdVector.push_back <>$ capt_arg_payload $+...$--> StdVector.push_back
; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload ; +PatternMatch.Java.implements_iterator
&:: "remove" <>$ capt_arg_payload
$+...$--> JavaIterator.remove ~desc:"remove" $+...$--> JavaIterator.remove ~desc:"remove"
; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back ; +PatternMatch.Java.implements_map &:: "put" <>$ capt_arg_payload
; +PatternMatch.implements_map &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back
; +PatternMatch.Java.implements_map &:: "putAll" <>$ capt_arg_payload
$+...$--> StdVector.push_back $+...$--> StdVector.push_back
; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
; +PatternMatch.implements_collection ; +PatternMatch.Java.implements_collection
&:: "get" <>$ capt_arg_payload $+ capt_arg_payload &:: "get" <>$ capt_arg_payload $+ capt_arg_payload
$--> StdVector.at ~desc:"Collection.get()" $--> StdVector.at ~desc:"Collection.get()"
; +PatternMatch.implements_list &:: "set" <>$ capt_arg_payload $+ capt_arg_payload ; +PatternMatch.Java.implements_list
$+ capt_arg_payload $--> JavaCollection.set &:: "set" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload
; +PatternMatch.implements_iterator &:: "hasNext" $--> JavaCollection.set
; +PatternMatch.Java.implements_iterator
&:: "hasNext"
&--> Misc.nondet ~fn_name:"Iterator.hasNext()" &--> Misc.nondet ~fn_name:"Iterator.hasNext()"
; +PatternMatch.implements_enumeration ; +PatternMatch.Java.implements_enumeration
&:: "hasMoreElements" &:: "hasMoreElements"
&--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()" &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()"
; +PatternMatch.implements_lang "Object" ; +PatternMatch.Java.implements_lang "Object"
&:: "equals" &:: "equals"
&--> Misc.nondet ~fn_name:"Object.equals" &--> Misc.nondet ~fn_name:"Object.equals"
; +PatternMatch.implements_lang "Iterable" ; +PatternMatch.Java.implements_lang "Iterable"
&:: "iterator" <>$ capt_arg_payload &:: "iterator" <>$ capt_arg_payload
$+...$--> JavaIterator.constructor ~desc:"Iterable.iterator" $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator"
; +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload ; +PatternMatch.Java.implements_iterator
&:: "next" <>$ capt_arg_payload
$!--> JavaIterator.next ~desc:"Iterator.next()" $!--> JavaIterator.next ~desc:"Iterator.next()"
; ( +PatternMatch.implements_enumeration ; ( +PatternMatch.Java.implements_enumeration
&:: "nextElement" <>$ capt_arg_payload &:: "nextElement" <>$ capt_arg_payload
$!--> fun x -> $!--> fun x ->
StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) ) StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) )

Write Preview
Loading…
Cancel
Save