@ -7,11 +7,13 @@
open ! IStd
module BasicCost = CostDomain . BasicCost
module BasicCostWithReason = CostDomain . BasicCostWithReason
open BufferOverrunUtils . ModelEnv
let unit_cost_model _ model_env ~ ret : _ _ inferbo_mem = BasicCost . one ()
let unit_cost_model _ get_summary _ model_env ~ ret : _ _ inferbo_mem = BasicCost . one ()
let cost_of_exp exp ~ degree_kind ~ of_function { integer_type_widths ; location } ~ ret : _ inferbo_mem =
let cost_of_exp exp ~ degree_kind ~ of_function _ get_summary { integer_type_widths ; location } ~ ret : _
inferbo_mem =
let itv =
BufferOverrunSemantics . eval integer_type_widths exp inferbo_mem
| > BufferOverrunDomain . Val . get_itv
@ -23,7 +25,7 @@ let linear = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Linear
let log = cost_of_exp ~ degree_kind : Polynomials . DegreeKind . Log
let provider_get {pname ; location } ~ ret : ( _ , ret_typ ) _ : BasicCost . t =
let provider_get _get_summary {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
@ -32,7 +34,7 @@ let provider_get {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t =
module BoundsOf ( Container : CostUtils . S ) = struct
let of_length exp {location } ~ ret : _ mem ~ of_function ~ degree_kind =
let of_length exp _get_summary {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
@ -41,14 +43,14 @@ module BoundsOf (Container : CostUtils.S) = struct
let logarithmic_length = of_length ~ degree_kind : Polynomials . DegreeKind . Log
let n_log_n_length exp env ~ ret mem ~ of_function =
let log_n = logarithmic_length exp ~ of_function env mem ~ ret in
let n = linear_length exp ~ of_function env mem ~ ret in
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
BasicCost . mult n log_n
end
module IntHashMap = struct
let keys { ProcnameDispatcher . Call . FuncArg . exp ; typ } {location } ~ ret : _ inferbo_mem =
let keys { ProcnameDispatcher . Call . FuncArg . exp ; typ } _get_summary {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 -> (
@ -64,7 +66,7 @@ module IntHashMap = struct
end
module JavaString = struct
let substring_aux ~ begin_idx ~ end_v {integer_type_widths ; location } inferbo_mem =
let substring_aux ~ begin_idx ~ end_v _get_summary {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
@ -84,28 +86,29 @@ module JavaString = struct
location
let substring_no_end exp begin_idx model_env ~ ret : _ inferbo_mem =
let substring_no_end exp begin_idx get_summary model_env ~ ret : _ inferbo_mem =
substring_aux ~ begin_idx
~ end_v : ( BufferOverrunModels . JavaString . get_length model_env exp inferbo_mem )
model_env inferbo_mem
get_summary model_env inferbo_mem
let substring begin_idx end_idx ( { integer_type_widths } as model_env ) ~ ret : _ inferbo_mem =
let substring begin_idx end_idx get_summary ( { integer_type_widths } as model_env ) ~ ret : _
inferbo_mem =
substring_aux ~ begin_idx
~ end_v : ( BufferOverrunSemantics . eval integer_type_widths end_idx inferbo_mem )
model_env inferbo_mem
get_summary model_env inferbo_mem
(* * 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 indexOf_char exp _get_summary ({ 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 ({ integer_type_widths ; location } as model_env ) ~ ret : _
inferbo_mem =
let indexOf_char_starting_from exp start_exp _get_summary
( { 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 ) )
@ -116,7 +119,7 @@ module JavaString = struct
(* * O ( |m|.|n| ) where m and n are the given strings *)
let indexOf_str exp index_exp ({ location } as model_env ) ~ ret : _ inferbo_mem =
let indexOf_str exp index_exp _get_summary ({ location } as model_env ) ~ ret : _ inferbo_mem =
let itv =
BufferOverrunModels . JavaString . get_length model_env exp inferbo_mem
| > BufferOverrunDomain . Val . get_itv
@ -142,15 +145,15 @@ module BoundsOfArray = BoundsOf (CostUtils.Array)
module BoundsOfCString = BoundsOf ( CostUtils . CString )
module NSString = struct
let get_length str ~ of_function ({ location } as model_env ) ~ ret : _ mem =
let get_length str ~ of_function _get_summary ({ 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 model_env ~ ret mem =
let get_length str = get_length str ~ of_function model_env ~ ret mem in
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
cost_op ( get_length str1 ) ( get_length str2 )
@ -158,7 +161,7 @@ module NSString = struct
end
module NSCollection = struct
let get_length str ~ of_function {location } ~ ret : _ mem =
let get_length str ~ of_function _get_summary {location } ~ ret : _ mem =
let itv =
BufferOverrunModels . NSCollection . eval_collection_length str mem
| > BufferOverrunDomain . Val . get_itv
@ -166,9 +169,29 @@ 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 model_env ~ ret mem =
let get_length coll = get_length coll ~ of_function model_env ~ ret mem in
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
cost_op ( get_length coll1 ) ( get_length coll2 )
let enumerate_using_block array get_summary ( { pname } as model_env ) ~ ret inferbo_mem =
match pname with
| WithBlockParameters ( _ , [ block_name ] ) -> (
match get_summary ( Procname . Block block_name ) with
| Some { CostDomain . post = callee_summary } ->
let { BasicCostWithReason . cost = callee_cost } =
CostDomain . get_cost_kind OperationCost callee_summary
in
let length =
BoundsOfNSCollection . linear_length
~ of_function : ( Procname . to_simplified_string pname )
array get_summary model_env ~ ret inferbo_mem
in
BasicCost . mult_loop ~ iter : length ~ body : callee_cost
| None ->
BasicCost . zero )
| _ ->
BasicCost . zero
end
module ImmutableSet = struct
@ -178,7 +201,11 @@ module ImmutableSet = struct
end
module Call = struct
let dispatch : ( Tenv . t , CostUtils . model , unit ) ProcnameDispatcher . Call . dispatcher =
let dispatch :
( Tenv . t
, ( Procname . t -> CostDomain . summary option ) -> CostUtils . model
, unit )
ProcnameDispatcher . Call . dispatcher =
let open ProcnameDispatcher . Call in
let int_typ = Typ . mk ( Typ . Tint Typ . IInt ) in
let dispatcher =
@ -239,6 +266,9 @@ module Call = struct
; + PatternMatch . ObjectiveC . implements " NSMutableArray "
& :: " addObjectsFromArray: " < > $ any_arg $+ capt_exp
$- -> BoundsOfNSCollection . linear_length ~ of_function : " NSArray.addObjectsFromArray: "
; + PatternMatch . ObjectiveC . implements_collection
& :: " enumerateObjectsUsingBlock: " < > $ capt_exp $+ any_arg
$- -> NSCollection . enumerate_using_block
; + PatternMatch . Java . implements_collections
& :: " sort " $ capt_exp
$+ .. . $- -> BoundsOfCollection . n_log_n_length ~ of_function : " Collections.sort "