diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5fcb4faa0..d0a971f7e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -17,6 +17,7 @@ module L = Logging module Models = BufferOverrunModels module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace +module TypModels = BufferOverrunTypModels module Payload = SummaryPayload.Make (struct type t = BufferOverrunSummary.t @@ -44,8 +45,8 @@ module Init = struct BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~represents_multiple_values ~dimension mem | Typ.Tstruct typname -> ( - match Models.TypName.dispatch tenv typname with - | Some {Models.declare_local} -> + match TypModels.dispatch tenv typname with + | Some {TypModels.declare_local} -> let model_env = Models.mk_model_env pname node_hash location tenv integer_type_widths in diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 70cc173cf..25f857810 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -33,27 +33,6 @@ type check_fun = model_env -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.Condi type model = {exec: exec_fun; check: check_fun} -type declare_local_fun = - decl_local:BoUtils.Exec.decl_local - -> model_env - -> Loc.t - -> inst_num:int - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int - -type declare_symbolic_fun = - decl_sym_val:BoUtils.Exec.decl_sym_val - -> Itv.SymbolPath.partial - -> model_env - -> depth:int - -> Loc.t - -> Dom.Mem.t - -> Dom.Mem.t - -type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} - let no_exec _model_env ~ret:_ mem = mem let no_check _model_env _mem cond_set = cond_set @@ -300,23 +279,6 @@ module Folly = struct end module StdArray = struct - let typ typ length = - let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num - ~represents_multiple_values ~dimension mem = - (* should this be deferred to the constructor? *) - let length = Some (IntLit.of_int64 length) in - BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num - ~represents_multiple_values ~dimension mem - in - let declare_symbolic ~decl_sym_val path {pname; tenv; location} ~depth loc mem = - let offset = Itv.zero in - let size = Itv.of_int64 length in - BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname path tenv - location ~depth loc typ ~offset ~size mem - in - {declare_local; declare_symbolic} - - let constructor _size = let exec _model_env ~ret:_ mem = mem (* initialize? *) in {exec; check= no_check} @@ -340,22 +302,6 @@ module StdArray = struct mem in {exec; check= no_check} - - - let no_typ_model = - let no_model kind pname location mem = - L.(debug BufferOverrun Verbose) - "No %s type model in %a at %a" kind Typ.Procname.pp pname Location.pp location ; - mem - in - let declare_local ~decl_local:_ {pname; location} _loc ~inst_num ~represents_multiple_values:_ - ~dimension:_ mem = - (no_model "local" pname location mem, inst_num) - in - let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc mem = - no_model "symbolic" pname location mem - in - {declare_local; declare_symbolic} end (* Java's Collections are represented by their size. We don't care about the elements. @@ -363,18 +309,6 @@ end - each time we add an element, we increase the length of the array - each time we delete an element, we decrease the length of the array *) module Collection = struct - let typ = - let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num - ~represents_multiple_values ~dimension mem = - BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num - ~represents_multiple_values ~dimension mem - in - let declare_symbolic ~decl_sym_val:_ path {location} ~depth:_ loc mem = - BoUtils.Exec.decl_sym_collection path location loc mem - in - {declare_local; declare_symbolic} - - let new_list _ = let exec {pname; node_hash; location} ~ret:(id, _) mem = let loc = Loc.of_id id in @@ -543,13 +477,3 @@ module Call = struct &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $!--> Collection.addAll_at_index ; +PatternMatch.implements_collection &:: "size" <>$ capt_exp $!--> Collection.size ] end - -module TypName = struct - let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher = - let open ProcnameDispatcher.TypName in - make_dispatcher - [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ - ; +PatternMatch.implements_collection &::.*--> Collection.typ - ; +PatternMatch.implements_iterator &::.*--> Collection.typ - ; -"std" &:: "array" &::.*--> StdArray.no_typ_model ] -end diff --git a/infer/src/bufferoverrun/bufferOverrunTypModels.ml b/infer/src/bufferoverrun/bufferOverrunTypModels.ml new file mode 100644 index 000000000..ce3925a76 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunTypModels.ml @@ -0,0 +1,80 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open AbsLoc +module BoUtils = BufferOverrunUtils +module Dom = BufferOverrunDomain + +type model_env = BufferOverrunModels.model_env = + { pname: Typ.Procname.t + ; node_hash: int + ; location: Location.t + ; tenv: Tenv.t + ; integer_type_widths: Typ.IntegerWidths.t } + +type declare_local_fun = + decl_local:BoUtils.Exec.decl_local + -> model_env + -> Loc.t + -> inst_num:int + -> represents_multiple_values:bool + -> dimension:int + -> Dom.Mem.t + -> Dom.Mem.t * int + +type declare_symbolic_fun = + decl_sym_val:BoUtils.Exec.decl_sym_val + -> Itv.SymbolPath.partial + -> model_env + -> depth:int + -> Loc.t + -> Dom.Mem.t + -> Dom.Mem.t + +type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} + +let std_array typ length = + let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num + ~represents_multiple_values ~dimension mem = + (* should this be deferred to the constructor? *) + let length = Some (IntLit.of_int64 length) in + BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num + ~represents_multiple_values ~dimension mem + in + let declare_symbolic ~decl_sym_val path {pname; tenv; location} ~depth loc mem = + let offset = Itv.zero in + let size = Itv.of_int64 length in + BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname path tenv + location ~depth loc typ ~offset ~size mem + in + {declare_local; declare_symbolic} + + +(* Java's Collections are represented by their size. We don't care about the elements. +- when they are constructed, we set the size to 0 +- each time we add an element, we increase the length of the array +- each time we delete an element, we decrease the length of the array *) + +let collection = + let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num + ~represents_multiple_values ~dimension mem = + BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num + ~represents_multiple_values ~dimension mem + in + let declare_symbolic ~decl_sym_val:_ path {location} ~depth:_ loc mem = + BoUtils.Exec.decl_sym_collection path location loc mem + in + {declare_local; declare_symbolic} + + +let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher = + let open ProcnameDispatcher.TypName in + make_dispatcher + [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> std_array + ; +PatternMatch.implements_collection &::.*--> collection + ; +PatternMatch.implements_iterator &::.*--> collection ]