diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 9d7610d8b..a151c252e 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -67,7 +67,7 @@ module InstrBasicCostWithReason = struct match CostModels.Call.dispatch tenv callee_pname fun_arg_list with | Some model -> BasicCostWithReason.of_basic_cost - (model get_summary (Lazy.force model_env) ~ret inferbo_mem) + (model {get_summary; model_env= Lazy.force model_env} ~ret inferbo_mem) | None -> ( match callee_cost_opt with | Some callee_cost -> @@ -85,7 +85,9 @@ module InstrBasicCostWithReason = struct BasicCostWithReason.t = match CostAutoreleaseModels.Call.dispatch tenv callee_pname fun_arg_list with | Some model -> - let autoreleasepool_size = model get_summary (Lazy.force model_env) ~ret inferbo_mem in + let autoreleasepool_size = + model {get_summary; model_env= Lazy.force model_env} ~ret inferbo_mem + in BasicCostWithReason.of_basic_cost autoreleasepool_size | None -> let fun_cost = diff --git a/infer/src/cost/costAutoreleaseModels.ml b/infer/src/cost/costAutoreleaseModels.ml index dc878d673..20548bc25 100644 --- a/infer/src/cost/costAutoreleaseModels.ml +++ b/infer/src/cost/costAutoreleaseModels.ml @@ -9,8 +9,9 @@ open! IStd module BasicCost = CostDomain.BasicCost module BasicCostWithReason = CostDomain.BasicCostWithReason open BufferOverrunUtils.ModelEnv +open CostUtils.CostModelEnv -let unit_cost _get_summary {pname; location} ~ret:_ _inferbo_mem = +let unit_cost {model_env= {pname; location}} ~ret:_ _inferbo_mem = let autoreleasepool_trace = Bounds.BoundTrace.of_modeled_function (Procname.to_string pname) location in @@ -18,7 +19,7 @@ let unit_cost _get_summary {pname; location} ~ret:_ _inferbo_mem = module NSArray = struct - let index_of_object_passing_test array get_summary ({pname; location= _} as model_env) ~ret + let index_of_object_passing_test array ({get_summary; model_env= {pname}} as cost_model_env) ~ret inferbo_mem = match pname with | WithBlockParameters (_, [block_name]) -> ( @@ -30,7 +31,7 @@ module NSArray = struct let length = CostModels.BoundsOfNSCollection.linear_length ~of_function:(Procname.to_simplified_string pname) - array get_summary model_env ~ret inferbo_mem + array cost_model_env ~ret inferbo_mem in BasicCost.mult_loop ~iter:length ~body:callee_cost | None -> @@ -40,11 +41,7 @@ module NSArray = struct end module Call = struct - let dispatch : - ( Tenv.t - , (Procname.t -> CostDomain.summary option) -> CostUtils.model - , unit ) - ProcnameDispatcher.Call.dispatcher = + let dispatch : (Tenv.t, CostUtils.model, unit) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in make_dispatcher [ +PatternMatch.ObjectiveC.implements "NSObject" &:: "autorelease" &--> unit_cost diff --git a/infer/src/cost/costAutoreleaseModels.mli b/infer/src/cost/costAutoreleaseModels.mli index badc59bff..984656839 100644 --- a/infer/src/cost/costAutoreleaseModels.mli +++ b/infer/src/cost/costAutoreleaseModels.mli @@ -8,9 +8,5 @@ open! IStd module Call : sig - val dispatch : - ( Tenv.t - , (Procname.t -> CostDomain.summary option) -> CostUtils.model - , unit ) - ProcnameDispatcher.Call.dispatcher + val dispatch : (Tenv.t, CostUtils.model, unit) ProcnameDispatcher.Call.dispatcher end diff --git a/infer/src/cost/costModels.ml b/infer/src/cost/costModels.ml index 1ce14f9a6..2d68f1fca 100644 --- a/infer/src/cost/costModels.ml +++ b/infer/src/cost/costModels.ml @@ -9,10 +9,11 @@ open! IStd module BasicCost = CostDomain.BasicCost module BasicCostWithReason = CostDomain.BasicCostWithReason open BufferOverrunUtils.ModelEnv +open CostUtils.CostModelEnv -let unit_cost_model _get_summary _model_env ~ret:_ _inferbo_mem = BasicCost.one () +let unit_cost_model _model_env ~ret:_ _inferbo_mem = BasicCost.one () -let cost_of_exp exp ~degree_kind ~of_function _get_summary {integer_type_widths; location} ~ret:_ +let cost_of_exp exp ~degree_kind ~of_function {model_env= {integer_type_widths; location}} ~ret:_ inferbo_mem = let itv = BufferOverrunSemantics.eval integer_type_widths exp inferbo_mem @@ -25,7 +26,7 @@ let linear = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Linear let log = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Log -let provider_get _get_summary {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t = +let provider_get {model_env= {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 ~is_expensive:true path in @@ -34,7 +35,7 @@ let provider_get _get_summary {pname; location} ~ret:(_, ret_typ) _ : BasicCost. module BoundsOf (Container : CostUtils.S) = struct - let of_length exp _get_summary {location} ~ret:_ mem ~of_function ~degree_kind = + let of_length exp {model_env= {location}} ~ret:_ mem ~of_function ~degree_kind = let itv = Container.length exp mem |> BufferOverrunDomain.Val.get_itv in CostUtils.of_itv ~itv ~degree_kind ~of_function location @@ -43,14 +44,14 @@ module BoundsOf (Container : CostUtils.S) = struct let logarithmic_length = of_length ~degree_kind:Polynomials.DegreeKind.Log - let n_log_n_length exp get_summary env ~ret mem ~of_function = - let log_n = logarithmic_length exp ~of_function get_summary env mem ~ret in - let n = linear_length exp ~of_function get_summary env mem ~ret in + let n_log_n_length exp cost_model_env ~ret mem ~of_function = + let log_n = logarithmic_length exp ~of_function cost_model_env mem ~ret in + let n = linear_length exp ~of_function cost_model_env mem ~ret in BasicCost.mult n log_n end module IntHashMap = struct - let keys {ProcnameDispatcher.Call.FuncArg.exp; typ} _get_summary {location} ~ret:_ inferbo_mem = + let keys {ProcnameDispatcher.Call.FuncArg.exp; typ} {model_env= {location}} ~ret:_ inferbo_mem = let locs = BufferOverrunSemantics.eval_locs exp inferbo_mem in match AbsLoc.PowLoc.is_singleton_or_more locs with | Singleton this_loc -> ( @@ -66,7 +67,7 @@ module IntHashMap = struct end module JavaString = struct - let substring_aux ~begin_idx ~end_v _get_summary {integer_type_widths; location} inferbo_mem = + let substring_aux ~begin_idx ~end_v {integer_type_widths; location} inferbo_mem = let begin_v = BufferOverrunSemantics.eval integer_type_widths begin_idx inferbo_mem in let begin_itv = BufferOverrunDomain.Val.get_itv begin_v in let end_itv = BufferOverrunDomain.Val.get_itv end_v in @@ -86,29 +87,29 @@ module JavaString = struct location - let substring_no_end exp begin_idx get_summary model_env ~ret:_ inferbo_mem = + let substring_no_end exp begin_idx {model_env} ~ret:_ inferbo_mem = substring_aux ~begin_idx ~end_v:(BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem) - get_summary model_env inferbo_mem + model_env inferbo_mem - let substring begin_idx end_idx get_summary ({integer_type_widths} as model_env) ~ret:_ - inferbo_mem = + let substring begin_idx end_idx {model_env= {integer_type_widths} as model_env} ~ret:_ inferbo_mem + = substring_aux ~begin_idx ~end_v:(BufferOverrunSemantics.eval integer_type_widths end_idx inferbo_mem) - get_summary model_env inferbo_mem + model_env inferbo_mem (** O(|m|) where m is the given string and |.| is the length function *) - let indexOf_char exp _get_summary ({location} as model_env) ~ret:_ inferbo_mem = + let indexOf_char exp {model_env= {location} as model_env} ~ret:_ inferbo_mem = 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 _get_summary - ({integer_type_widths; location} as model_env) ~ret:_ inferbo_mem = + let indexOf_char_starting_from exp start_exp + {model_env= {integer_type_widths; location} as model_env} ~ret:_ inferbo_mem = let itv = CostUtils.string_len_range_itv model_env exp ~from:(Some (start_exp, integer_type_widths)) @@ -119,7 +120,7 @@ module JavaString = struct (** O(|m|.|n|) where m and n are the given strings *) - let indexOf_str exp index_exp _get_summary ({location} as model_env) ~ret:_ inferbo_mem = + let indexOf_str exp index_exp {model_env= {location} as model_env} ~ret:_ inferbo_mem = let itv = BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem |> BufferOverrunDomain.Val.get_itv @@ -145,15 +146,15 @@ module BoundsOfArray = BoundsOf (CostUtils.Array) module BoundsOfCString = BoundsOf (CostUtils.CString) module NSString = struct - let get_length str ~of_function _get_summary ({location} as model_env) ~ret:_ mem = + let get_length str ~of_function {model_env= {location} as model_env} ~ret:_ mem = let itv = BufferOverrunModels.NSString.get_length model_env str mem |> BufferOverrunDomain.Val.get_itv in CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location - let op_on_two_str cost_op ~of_function str1 str2 get_summary model_env ~ret mem = - let get_length str = get_length str ~of_function get_summary model_env ~ret mem in + let op_on_two_str cost_op ~of_function str1 str2 cost_model_env ~ret mem = + let get_length str = get_length str ~of_function cost_model_env ~ret mem in cost_op (get_length str1) (get_length str2) @@ -161,7 +162,7 @@ module NSString = struct end module NSCollection = struct - let get_length str ~of_function _get_summary {location} ~ret:_ mem = + let get_length str ~of_function {model_env= {location}} ~ret:_ mem = let itv = BufferOverrunModels.NSCollection.eval_collection_length str mem |> BufferOverrunDomain.Val.get_itv @@ -169,12 +170,13 @@ module NSCollection = struct CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location - let op_on_two_coll cost_op ~of_function coll1 coll2 get_summary model_env ~ret mem = - let get_length coll = get_length coll ~of_function get_summary model_env ~ret mem in + let op_on_two_coll cost_op ~of_function coll1 coll2 cost_model_env ~ret mem = + let get_length coll = get_length coll ~of_function cost_model_env ~ret mem in cost_op (get_length coll1) (get_length coll2) - let enumerate_using_block array get_summary ({pname} as model_env) ~ret inferbo_mem = + let enumerate_using_block array ({get_summary; model_env} as cost_model_env) ~ret inferbo_mem = + let pname = model_env.pname in match pname with | WithBlockParameters (_, [block_name]) -> ( match get_summary (Procname.Block block_name) with @@ -185,7 +187,7 @@ module NSCollection = struct let length = BoundsOfNSCollection.linear_length ~of_function:(Procname.to_simplified_string pname) - array get_summary model_env ~ret inferbo_mem + array cost_model_env ~ret inferbo_mem in BasicCost.mult_loop ~iter:length ~body:callee_cost | None -> @@ -201,11 +203,7 @@ module ImmutableSet = struct end module Call = struct - let dispatch : - ( Tenv.t - , (Procname.t -> CostDomain.summary option) -> CostUtils.model - , unit ) - ProcnameDispatcher.Call.dispatcher = + let dispatch : (Tenv.t, CostUtils.model, unit) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in let int_typ = Typ.mk (Typ.Tint Typ.IInt) in let dispatcher = diff --git a/infer/src/cost/costUtils.ml b/infer/src/cost/costUtils.ml index a1ee96d56..d1878c29f 100644 --- a/infer/src/cost/costUtils.ml +++ b/infer/src/cost/costUtils.ml @@ -8,9 +8,15 @@ open! IStd module L = Logging module BasicCost = CostDomain.BasicCost -open BufferOverrunUtils.ModelEnv -type model = model_env -> ret:Ident.t * Typ.t -> BufferOverrunDomain.Mem.t -> BasicCost.t +module CostModelEnv = struct + type cost_model_env = + { model_env: BufferOverrunUtils.ModelEnv.model_env + ; get_summary: Procname.t -> CostDomain.summary option } +end + +type model = + CostModelEnv.cost_model_env -> ret:Ident.t * Typ.t -> BufferOverrunDomain.Mem.t -> BasicCost.t let unit_cost_of ~of_function loc = Bounds.NonNegativeBound.of_modeled_function of_function loc Bounds.Bound.one diff --git a/infer/src/cost/hoisting.ml b/infer/src/cost/hoisting.ml index 6504cf977..bcaaa979a 100644 --- a/infer/src/cost/hoisting.ml +++ b/infer/src/cost/hoisting.ml @@ -131,7 +131,7 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f BufferOverrunUtils.ModelEnv.mk_model_env pname ~node_hash loc tenv integer_type_widths inferbo_get_summary in - model get_summary model_env ~ret inferbo_mem ) + model CostUtils.CostModelEnv.{get_summary; model_env} ~ret inferbo_mem ) in Option.filter cost_opt ~f:CostDomain.BasicCost.is_symbolic