[inferbo] Move type models to their own file

Reviewed By: ezgicicek

Differential Revision: D13449611

fbshipit-source-id: 6b6170f56

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

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

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 ]