[inferbo] Restore type models

Reviewed By: skcho, jvillard

Differential Revision: D13449623

fbshipit-source-id: feebe58f1

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -32,8 +32,7 @@ type extras = Dom.OndemandEnv.t
 module CFG = ProcCfg.NormalOneInstrPerNode
 
 module Init = struct
-  let initial_state {ProcData.pdesc; tenv; extras= {Dom.OndemandEnv.integer_type_widths} as oenv}
-      start_node =
+  let initial_state {ProcData.pdesc; tenv; extras= oenv} start_node =
     let node_hash = CFG.Node.hash start_node in
     let location = CFG.Node.loc start_node in
     let pname = Procdesc.get_proc_name pdesc in
@@ -46,12 +45,14 @@ module Init = struct
             ?stride ~inst_num ~represents_multiple_values ~dimension mem
       | Typ.Tstruct typname -> (
         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
-            declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
-              ~dimension mem
+        | Some typ_model -> (
+          match typ_model with
+          | Array {element_typ; length} ->
+              BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ
+                ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem
+          | JavaCollection ->
+              BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num
+                ~represents_multiple_values ~dimension mem )
         | None ->
             (mem, inst_num) )
       | _ ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -339,7 +339,7 @@ module Val = struct
 
   let is_mone x = Itv.is_mone (get_itv x)
 
-  let of_path ~may_last_field integer_type_widths location typ path =
+  let of_path tenv ~may_last_field integer_type_widths location typ path =
     let is_java = Language.curr_language_is Java in
     L.d_printfln "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
       (if may_last_field then ", may_last_field" else "")
@@ -374,10 +374,26 @@ module Val = struct
             ArrayBlk.make allocsite ~stride ~offset ~size
           in
           {bot with arrayblk; traces}
-    | Tstruct _ ->
+    | Tstruct typename -> (
+      match BufferOverrunTypModels.dispatch tenv typename with
+      | Some typ_model -> (
+        match typ_model with
+        | Array {deref_kind; length} ->
+            let deref_path = SPath.deref ~deref_kind path in
+            let l = Loc.of_path deref_path in
+            let traces = TraceSet.singleton location (Trace.Parameter l) in
+            let allocsite = Allocsite.make_symbol deref_path in
+            let offset = Itv.zero in
+            let size = Itv.of_int_lit length in
+            of_array_alloc allocsite ~stride:None ~offset ~size ~traces
+        | JavaCollection ->
             let l = Loc.of_path path in
             let traces = TraceSet.singleton location (Trace.Parameter l) in
-        of_loc ~traces l
+            of_itv ~traces (Itv.of_normal_path ~unsigned:true path) )
+      | None ->
+          let l = Loc.of_path path in
+          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          of_loc ~traces l )
     | Tarray {length; stride} ->
         let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
         let l = Loc.of_path deref_path in
@@ -400,7 +416,7 @@ module Val = struct
 
 
   let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t =
-   fun ~default {typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
+   fun ~default {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
     match Loc.get_path l with
     | None ->
         L.d_printfln "Val.on_demand for %a -> no path" Loc.pp l ;
@@ -414,7 +430,7 @@ module Val = struct
           L.d_printfln "Val.on_demand for %a" Loc.pp l ;
           let may_last_field = may_last_field path in
           let path = OndemandEnv.canonical_path typ_of_param_path path in
-          of_path ~may_last_field integer_type_widths entry_location typ path )
+          of_path tenv ~may_last_field integer_type_widths entry_location typ path )
 
 
   module Itv = struct
@@ -1114,7 +1130,9 @@ module Mem = struct
 
   let forget_locs : PowLoc.t -> t -> t = fun locs -> map ~f:(MemReach.forget_locs locs)
 
-  let init_param_relation : Loc.t -> t -> t = fun loc -> map ~f:(MemReach.init_param_relation loc)
+  let[@warning "-32"] init_param_relation : Loc.t -> t -> t =
+   fun loc -> map ~f:(MemReach.init_param_relation loc)
+
 
   let init_array_relation :
       Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t -> t

infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml

@@ -11,7 +11,8 @@ module SPath = Symb.SymbolPath
 module FormalTyps = Caml.Map.Make (Pvar)
 
 type t =
-  { typ_of_param_path: SPath.partial -> Typ.t option
+  { tenv: Tenv.t
+  ; typ_of_param_path: SPath.partial -> Typ.t option
   ; may_last_field: SPath.partial -> bool
   ; entry_location: Location.t
   ; integer_type_widths: Typ.IntegerWidths.t }
@@ -34,6 +35,15 @@ let mk pdesc =
                   elt
               | Tvoid ->
                   Typ.void
+              | Tstruct typename -> (
+                match BufferOverrunTypModels.dispatch tenv typename with
+                | Some (Array {element_typ}) ->
+                    element_typ
+                | Some _ ->
+                    L.(die InternalError)
+                      "Deref of non-array modeled type `%a`" Typ.Name.pp typename
+                | None ->
+                    L.(die InternalError) "Deref of unmodeled type `%a`" Typ.Name.pp typename )
               | _ ->
                   L.(die InternalError) "Untyped expression is given." )
       | SPath.Field (fn, x) ->
@@ -61,7 +71,7 @@ let mk pdesc =
                      true )
     in
     let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in
-    {typ_of_param_path; may_last_field; entry_location; integer_type_widths}
+    {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths}
 
 
 let canonical_path typ_of_param_path path =

infer/src/bufferoverrun/bufferOverrunTypModels.ml

@@ -6,53 +6,13 @@
  *)
 
 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 typ_model =
+  | Array of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t}
+  | JavaCollection
 
-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}
+let std_array element_typ length =
+  Array {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length}
 
 
 (* Java's Collections are represented by their size. We don't care about the elements.
@@ -60,17 +20,7 @@ let std_array typ length =
 - 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 collection = JavaCollection
 
 let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher =
   let open ProcnameDispatcher.TypName in

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -118,63 +118,6 @@ module Exec = struct
     (mem, inst_num + 1)
 
 
-  type decl_sym_val =
-       Typ.Procname.t
-    -> Itv.SymbolPath.partial
-    -> Tenv.t
-    -> Location.t
-    -> depth:int
-    -> Loc.t
-    -> Typ.t
-    -> Dom.Mem.t
-    -> Dom.Mem.t
-
-  let decl_sym_arr :
-         decl_sym_val:decl_sym_val
-      -> Symb.SymbolPath.deref_kind
-      -> Typ.Procname.t
-      -> Itv.SymbolPath.partial
-      -> Tenv.t
-      -> Location.t
-      -> depth:int
-      -> Loc.t
-      -> Typ.t
-      -> ?offset:Itv.t
-      -> ?size:Itv.t
-      -> ?stride:int
-      -> Dom.Mem.t
-      -> Dom.Mem.t =
-   fun ~decl_sym_val deref_kind pname path tenv location ~depth loc typ ?offset ?size ?stride mem ->
-    let offset = IOption.value_default_f offset ~f:(fun () -> Itv.of_offset_path path) in
-    let size = IOption.value_default_f size ~f:(fun () -> Itv.of_length_path path) in
-    let deref_path = Itv.SymbolPath.deref ~deref_kind path in
-    let allocsite = Allocsite.make_symbol deref_path in
-    let mem =
-      let arr =
-        let traces = Trace.(Set.singleton location (Parameter loc)) in
-        let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
-        Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces
-        |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
-      in
-      mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc
-      |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
-    in
-    let deref_loc = Loc.of_allocsite allocsite in
-    decl_sym_val pname deref_path tenv location ~depth deref_loc typ mem
-
-
-  let decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t
-      =
-   fun path location loc mem ->
-    let size =
-      let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
-      let traces = Trace.(Set.singleton location (Parameter loc)) in
-      Itv.of_length_path path |> Dom.Val.of_itv ~traces
-      |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
-    in
-    Dom.Mem.add_heap loc size mem
-
-
   let init_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem =
     let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
       let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -56,35 +56,6 @@ module Exec : sig
     -> Dom.Mem.t
     -> Dom.Mem.t * int
 
-  type decl_sym_val =
-       Typ.Procname.t
-    -> Itv.SymbolPath.partial
-    -> Tenv.t
-    -> Location.t
-    -> depth:int
-    -> Loc.t
-    -> Typ.t
-    -> Dom.Mem.t
-    -> Dom.Mem.t
-
-  val decl_sym_arr :
-       decl_sym_val:decl_sym_val
-    -> Symb.SymbolPath.deref_kind
-    -> Typ.Procname.t
-    -> Itv.SymbolPath.partial
-    -> Tenv.t
-    -> Location.t
-    -> depth:int
-    -> Loc.t
-    -> Typ.t
-    -> ?offset:Itv.t
-    -> ?size:Itv.t
-    -> ?stride:int
-    -> Dom.Mem.t
-    -> Dom.Mem.t
-
-  val decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t
-
   val init_array_fields :
        Tenv.t
     -> Typ.IntegerWidths.t

infer/src/bufferoverrun/itv.ml

@@ -498,8 +498,6 @@ let of_big_int : Z.t -> t = fun n -> NonBottom (ItvPure.of_big_int n)
 
 let of_int_lit : IntLit.t -> t = fun n -> of_big_int (IntLit.to_big_int n)
 
-let of_int64 : Int64.t -> t = fun n -> of_big_int (Z.of_int64 n)
-
 let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
 
 let le : lhs:t -> rhs:t -> bool = ( <= )

infer/src/bufferoverrun/itv.mli

@@ -133,8 +133,6 @@ val of_big_int : Z.t -> t
 
 val of_int_lit : IntLit.t -> t
 
-val of_int64 : Int64.t -> t
-
 val is_const : t -> Z.t option
 
 val is_one : t -> bool