diff --git a/Makefile b/Makefile index 5dc4913de..00d0d4d55 100644 --- a/Makefile +++ b/Makefile @@ -165,6 +165,10 @@ DIRECT_TESTS += \ java_topl \ java_tracing \ +ifeq ($(IS_FACEBOOK_TREE),yes) +DIRECT_TESTS += java_fb-performance +endif + ifneq ($(ANT),no) BUILD_SYSTEMS_TESTS += ant endif diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index 465e5c54a..04f5e2f13 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -721,6 +721,16 @@ module Call = struct None + let merge_dispatchers : + ('context, 'f) dispatcher -> ('context, 'f) dispatcher -> ('context, 'f) dispatcher = + fun dispatcher1 dispatcher2 context procname args -> + match dispatcher1 context procname args with + | Some _ as r -> + r + | None -> + dispatcher2 context procname args + + (* Function args *) let no_marker_checker _markers = true diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 4a30641d2..de9c4e660 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -228,6 +228,10 @@ module Call : sig Common with type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> FuncArg.t list -> 'f option + val merge_dispatchers : + ('context, 'f) dispatcher -> ('context, 'f) dispatcher -> ('context, 'f) dispatcher + (** Merges two dispatchers into a dispatcher *) + type ('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher type ('context, 'arg_in, 'arg_out, 'f_in, 'f_out, 'captured_types, 'markers) one_arg diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index 07eec22a8..08d5e9179 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -30,6 +30,9 @@ val is_subtype : Tenv.t -> Typ.Name.t -> Typ.Name.t -> bool val is_subtype_of_str : Tenv.t -> Typ.Name.t -> string -> bool (** Resolve [typ_str] in [tenv], then check [typ] <: [typ_str] *) +val implements : string -> Tenv.t -> string -> bool +(** Check whether class implements a given class *) + val implements_arrays : Tenv.t -> string -> bool (** Check whether class implements Java's Arrays *) diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml index 1642036a9..2b65d1645 100644 --- a/infer/src/checkers/costModels.ml +++ b/infer/src/checkers/costModels.ml @@ -9,8 +9,6 @@ open! IStd module BasicCost = CostDomain.BasicCost open BufferOverrunUtils.ModelEnv -type model = model_env -> ret:Ident.t * Typ.t -> BufferOverrunDomain.Mem.t -> BasicCost.t - module type S = sig val length : Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t end @@ -27,48 +25,25 @@ module Collection : S = struct BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem end -let of_itv ~(itv : Itv.t) ~degree_kind ~of_function loc = - let upper_bound = - match itv with Bottom -> Bounds.Bound.pinf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure - in - Bounds.NonNegativeBound.of_modeled_function of_function loc upper_bound - |> BasicCost.of_non_negative_bound ~degree_kind - - let linear exp ~of_function {integer_type_widths; location} ~ret:_ inferbo_mem = let itv = BufferOverrunSemantics.eval integer_type_widths exp inferbo_mem |> BufferOverrunDomain.Val.get_itv in - of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location + CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t = let callsite = CallSite.make pname location in let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in let itv = Itv.of_modeled_path path in - of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location - - -(** Given a string of length n and an optional starting index i (0 by - default), return itv [0, n_u-i_l] *) -let string_len_range_itv model_env exp ~from mem = - let itv = - BufferOverrunModels.JavaString.get_length model_env exp mem |> BufferOverrunDomain.Val.get_itv - in - Option.value_map from ~default:itv ~f:(fun (start_exp, integer_type_widths) -> - let start_itv = - BufferOverrunSemantics.eval integer_type_widths start_exp mem - |> BufferOverrunDomain.Val.get_itv - in - Itv.minus itv start_itv ) - |> Itv.set_lb_zero + CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location module BoundsOf (Container : S) = struct let of_length exp {location} ~ret:_ mem ~of_function ~degree_kind = let itv = Container.length exp mem |> BufferOverrunDomain.Val.get_itv in - of_itv ~itv ~degree_kind ~of_function location + CostUtils.of_itv ~itv ~degree_kind ~of_function location let linear_length = of_length ~degree_kind:Polynomials.DegreeKind.Linear @@ -87,7 +62,8 @@ module JavaString = struct let itv = Itv.minus (BufferOverrunDomain.Val.get_itv end_v) (BufferOverrunDomain.Val.get_itv begin_v) in - of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.substring" location + CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear + ~of_function:"String.substring" location let substring exp begin_idx model_env ~ret:_ inferbo_mem = @@ -104,17 +80,21 @@ module JavaString = struct (** O(|m|) where m is the given string and |.| is the length function *) let indexOf_char exp ({location} as model_env) ~ret:_ inferbo_mem = - let itv = string_len_range_itv model_env exp ~from:None inferbo_mem in - of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location + let itv = CostUtils.string_len_range_itv model_env exp ~from:None inferbo_mem in + CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" + location (** O(|m|-|n|) where m is the given string and n is the index to start searching from *) let indexOf_char_starting_from exp start_exp ({integer_type_widths; location} as model_env) ~ret:_ inferbo_mem = let itv = - string_len_range_itv model_env exp ~from:(Some (start_exp, integer_type_widths)) inferbo_mem + CostUtils.string_len_range_itv model_env exp + ~from:(Some (start_exp, integer_type_widths)) + inferbo_mem in - of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location + CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" + location (** O(|m|.|n|) where m and n are the given strings *) @@ -128,10 +108,11 @@ module JavaString = struct |> BufferOverrunDomain.Val.get_itv in let n = - of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location + CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear + ~of_function:"String.indexOf" location in let m = - of_itv ~itv:index_itv ~degree_kind:Polynomials.DegreeKind.Linear + CostUtils.of_itv ~itv:index_itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location in BasicCost.mult n m @@ -141,62 +122,65 @@ module BoundsOfCollection = BoundsOf (Collection) module BoundsOfArray = BoundsOf (Array) module Call = struct - let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher = + let dispatch : (Tenv.t, CostUtils.model) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in let int_typ = Typ.mk (Typ.Tint Typ.IInt) in - make_dispatcher - [ +PatternMatch.implements_collections - &:: "sort" $ capt_exp - $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"Collections.sort" - ; +PatternMatch.implements_list &:: "sort" $ capt_exp - $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"List.sort" - ; +PatternMatch.implements_arrays &:: "sort" $ capt_exp - $+...$--> BoundsOfArray.n_log_n_length ~of_function:"Arrays.sort" - ; +PatternMatch.implements_list &:: "contains" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"List.contains" - ; +PatternMatch.implements_collections - &:: "binarySearch" <>$ capt_exp - $+...$--> BoundsOfCollection.logarithmic_length ~of_function:"Collections.binarySearch" - ; +PatternMatch.implements_arrays &:: "binarySearch" <>$ capt_exp - $+...$--> BoundsOfArray.logarithmic_length ~of_function:"Arrays.binarySearch" - ; +PatternMatch.implements_arrays &:: "copyOf" <>$ any_arg $+ capt_exp - $+...$--> linear ~of_function:"Arrays.copyOf" - ; +PatternMatch.implements_collections - &:: "copy" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.copy" - ; +PatternMatch.implements_collections - &:: "fill" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.fill" - ; +PatternMatch.implements_arrays &:: "fill" <>$ capt_exp - $+...$--> BoundsOfArray.linear_length ~of_function:"Arrays.fill" - ; +PatternMatch.implements_collections - &:: "reverse" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.reverse" - ; +PatternMatch.implements_collections - &:: "max" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.max" - ; +PatternMatch.implements_collections - &:: "min" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.min" - ; +PatternMatch.implements_collections - &:: "shuffle" <>$ capt_exp - $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle" - ; +PatternMatch.implements_lang "String" - &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring - ; +PatternMatch.implements_lang "String" - &:: "indexOf" <>$ capt_exp - $+ capt_exp_of_typ (+PatternMatch.implements_lang "String") - $--> JavaString.indexOf_str - ; +PatternMatch.implements_lang "String" - &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ capt_exp - $--> JavaString.indexOf_char_starting_from - ; +PatternMatch.implements_lang "String" - &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $--> JavaString.indexOf_char - ; +PatternMatch.implements_lang "String" - &:: "substring" - $ any_arg_of_typ (+PatternMatch.implements_lang "String") - $+ capt_exp $+ capt_exp $--> JavaString.substring_no_end - ; +PatternMatch.implements_inject "Provider" - &:: "get" - <>--> modeled ~of_function:"Provider.get" ] + let dispatcher = + make_dispatcher + [ +PatternMatch.implements_collections + &:: "sort" $ capt_exp + $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"Collections.sort" + ; +PatternMatch.implements_list &:: "sort" $ capt_exp + $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"List.sort" + ; +PatternMatch.implements_arrays &:: "sort" $ capt_exp + $+...$--> BoundsOfArray.n_log_n_length ~of_function:"Arrays.sort" + ; +PatternMatch.implements_list &:: "contains" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"List.contains" + ; +PatternMatch.implements_collections + &:: "binarySearch" <>$ capt_exp + $+...$--> BoundsOfCollection.logarithmic_length ~of_function:"Collections.binarySearch" + ; +PatternMatch.implements_arrays &:: "binarySearch" <>$ capt_exp + $+...$--> BoundsOfArray.logarithmic_length ~of_function:"Arrays.binarySearch" + ; +PatternMatch.implements_arrays &:: "copyOf" <>$ any_arg $+ capt_exp + $+...$--> linear ~of_function:"Arrays.copyOf" + ; +PatternMatch.implements_collections + &:: "copy" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.copy" + ; +PatternMatch.implements_collections + &:: "fill" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.fill" + ; +PatternMatch.implements_arrays &:: "fill" <>$ capt_exp + $+...$--> BoundsOfArray.linear_length ~of_function:"Arrays.fill" + ; +PatternMatch.implements_collections + &:: "reverse" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.reverse" + ; +PatternMatch.implements_collections + &:: "max" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.max" + ; +PatternMatch.implements_collections + &:: "min" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.min" + ; +PatternMatch.implements_collections + &:: "shuffle" <>$ capt_exp + $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle" + ; +PatternMatch.implements_lang "String" + &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring + ; +PatternMatch.implements_lang "String" + &:: "indexOf" <>$ capt_exp + $+ capt_exp_of_typ (+PatternMatch.implements_lang "String") + $--> JavaString.indexOf_str + ; +PatternMatch.implements_lang "String" + &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ capt_exp + $--> JavaString.indexOf_char_starting_from + ; +PatternMatch.implements_lang "String" + &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $--> JavaString.indexOf_char + ; +PatternMatch.implements_lang "String" + &:: "substring" + $ any_arg_of_typ (+PatternMatch.implements_lang "String") + $+ capt_exp $+ capt_exp $--> JavaString.substring_no_end + ; +PatternMatch.implements_inject "Provider" + &:: "get" + <>--> modeled ~of_function:"Provider.get" ] + in + merge_dispatchers dispatcher FbCostModels.Call.dispatch end diff --git a/infer/src/checkers/costUtils.ml b/infer/src/checkers/costUtils.ml new file mode 100644 index 000000000..407332d4e --- /dev/null +++ b/infer/src/checkers/costUtils.ml @@ -0,0 +1,34 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module BasicCost = CostDomain.BasicCost +open BufferOverrunUtils.ModelEnv + +type model = model_env -> ret:Ident.t * Typ.t -> BufferOverrunDomain.Mem.t -> BasicCost.t + +let of_itv ~(itv : Itv.t) ~degree_kind ~of_function loc = + let upper_bound = + match itv with Bottom -> Bounds.Bound.pinf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure + in + Bounds.NonNegativeBound.of_modeled_function of_function loc upper_bound + |> BasicCost.of_non_negative_bound ~degree_kind + + +(** Given a string of length n and an optional starting index i (0 by + default), return itv [0, n_u-i_l] *) +let string_len_range_itv model_env exp ~from mem = + let itv = + BufferOverrunModels.JavaString.get_length model_env exp mem |> BufferOverrunDomain.Val.get_itv + in + Option.value_map from ~default:itv ~f:(fun (start_exp, integer_type_widths) -> + let start_itv = + BufferOverrunSemantics.eval integer_type_widths start_exp mem + |> BufferOverrunDomain.Val.get_itv + in + Itv.minus itv start_itv ) + |> Itv.set_lb_zero diff --git a/infer/src/opensource/FbCostModels.ml b/infer/src/opensource/FbCostModels.ml new file mode 100644 index 000000000..eb60fb8f0 --- /dev/null +++ b/infer/src/opensource/FbCostModels.ml @@ -0,0 +1,12 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module Call = struct + let dispatch = ProcnameDispatcher.Call.make_dispatcher [] +end diff --git a/infer/src/opensource/FbCostModels.mli b/infer/src/opensource/FbCostModels.mli new file mode 100644 index 000000000..3a3b3f615 --- /dev/null +++ b/infer/src/opensource/FbCostModels.mli @@ -0,0 +1,12 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module Call : sig + val dispatch : (Tenv.t, CostUtils.model) ProcnameDispatcher.Call.dispatcher +end diff --git a/infer/tests/codetoanalyze/java/fb-performance/Makefile b/infer/tests/codetoanalyze/java/fb-performance/Makefile new file mode 100644 index 000000000..24eb094e6 --- /dev/null +++ b/infer/tests/codetoanalyze/java/fb-performance/Makefile @@ -0,0 +1,13 @@ +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +TESTS_DIR = ../../.. + +INFER_OPTIONS = --cost-only --bufferoverrun --debug-exceptions --use-cost-threshold \ + --report-force-relative-path +INFERPRINT_OPTIONS = --issues-tests +SOURCES = $(wildcard *.java) + +include $(TESTS_DIR)/javac.make