[inferbo] Move decl_local to BufferOverrunUtils

Reviewed By: mbouaziz

Differential Revision: D13690953

fbshipit-source-id: 85cd11b2f

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -17,7 +17,6 @@ module L = Logging
 module Models = BufferOverrunModels
 module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
-module TypModels = BufferOverrunTypModels
 
 module Payload = SummaryPayload.Make (struct
   type t = BufferOverrunSummary.t
@@ -33,31 +32,17 @@ module CFG = ProcCfg.NormalOneInstrPerNode
 
 module Init = struct
   let initial_state {ProcData.pdesc; tenv; extras= oenv} start_node =
+    let try_decl_local =
+      let pname = Procdesc.get_proc_name pdesc in
+      let model_env =
         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
-    let rec decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values
-        ~dimension mem =
-      match typ.Typ.desc with
-      | Typ.Tarray {elt= typ; length; stride} ->
-          let stride = Option.map ~f:IntLit.to_int_exn stride in
-          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 TypModels.dispatch tenv typname with
-        | Some (CArray {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
-        | Some JavaCollection | None ->
-            (mem, inst_num) )
-      | _ ->
-          (mem, inst_num)
+        let integer_type_widths = oenv.Dom.OndemandEnv.integer_type_widths in
+        BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
       in
-    let try_decl_local (mem, inst_num) {ProcAttributes.name; typ} =
-      let pvar = Pvar.mk name pname in
-      let loc = Loc.of_pvar pvar in
-      decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false
-        ~dimension:1 mem
+      fun (mem, inst_num) {ProcAttributes.name; typ} ->
+        let loc = Loc.of_pvar (Pvar.mk name pname) in
+        BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ)
     in
     let mem = Dom.Mem.init oenv in
     let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
@@ -185,10 +170,13 @@ module TransferFunctions = struct
     | Load (id, exp, _, _) ->
         BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem
     | Store (exp1, _, Const (Const.Cstr s), location) ->
+        let locs = Sem.eval_locs exp1 mem in
+        let model_env =
           let pname = Procdesc.get_proc_name pdesc in
           let node_hash = CFG.Node.hash node in
-        let locs = Sem.eval_locs exp1 mem in
-        BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem
+          BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+        in
+        BoUtils.Exec.decl_string model_env locs s mem
     | Store (exp1, _, exp2, location) ->
         let locs = Sem.eval_locs exp1 mem in
         let v =
@@ -232,9 +220,10 @@ module TransferFunctions = struct
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
         match Models.Call.dispatch tenv callee_pname params with
         | Some {Models.exec} ->
-            let node_hash = CFG.Node.hash node in
             let model_env =
-              Models.mk_model_env callee_pname node_hash location tenv integer_type_widths
+              let node_hash = CFG.Node.hash node in
+              BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv
+                integer_type_widths
             in
             exec model_env ~ret mem
         | None -> (
@@ -509,11 +498,12 @@ module Report = struct
         in
         match Models.Call.dispatch tenv callee_pname params with
         | Some {Models.check} ->
+            let model_env =
               let node_hash = CFG.Node.hash node in
               let pname = Procdesc.get_proc_name pdesc in
-            check
-              (Models.mk_model_env pname node_hash location tenv integer_type_widths)
-              mem cond_set
+              BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+            in
+            check model_env mem cond_set
         | None -> (
           match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
           | Some callee_summary -> (

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -15,17 +15,7 @@ module PO = BufferOverrunProofObligations
 module Sem = BufferOverrunSemantics
 module Relation = BufferOverrunDomainRelation
 module Trace = BufferOverrunTrace
-
-type model_env =
-  { pname: Typ.Procname.t
-  ; node_hash: int
-  ; location: Location.t
-  ; tenv: Tenv.t
-  ; integer_type_widths: Typ.IntegerWidths.t }
-
-let mk_model_env pname node_hash location tenv integer_type_widths =
-  {pname; node_hash; location; tenv; integer_type_widths}
-
+open BoUtils.ModelEnv
 
 type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t
 
@@ -77,7 +67,8 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set =
 
 
 let malloc size_exp =
-  let exec {pname; node_hash; location; tenv; integer_type_widths} ~ret:(id, _) mem =
+  let exec ({pname; node_hash; location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem
+      =
     let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
     let typ, stride, length0, dyn_length = get_malloc_info size_exp in
     let length = Sem.eval integer_type_widths length0 mem in
@@ -96,8 +87,7 @@ let malloc size_exp =
     mem
     |> Dom.Mem.add_stack (Loc.of_id id) v
     |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt
-    |> BoUtils.Exec.init_c_array_fields tenv integer_type_widths pname path ~node_hash typ
-         (Dom.Val.get_array_locs v) ?dyn_length
+    |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length
   and check = check_alloc_size size_exp in
   {exec; check}
 
@@ -128,7 +118,7 @@ let memset arr_exp size_exp =
 
 
 let realloc src_exp size_exp =
-  let exec {location; tenv; integer_type_widths} ~ret:(id, _) mem =
+  let exec ({location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem =
     let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
     let typ, _, length0, dyn_length = get_malloc_info size_exp in
     let length = Sem.eval integer_type_widths length0 mem in
@@ -138,7 +128,7 @@ let realloc src_exp size_exp =
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
     Option.value_map dyn_length ~default:mem ~f:(fun dyn_length ->
         let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in
-        BoUtils.Exec.set_dyn_length location tenv typ (Dom.Val.get_array_locs v) dyn_length mem )
+        BoUtils.Exec.set_dyn_length model_env typ (Dom.Val.get_array_locs v) dyn_length mem )
   and check = check_alloc_size size_exp in
   {exec; check}
 
@@ -346,11 +336,11 @@ module StdBasicString = struct
 
   (* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
   let constructor_from_char_ptr_without_len tgt src =
-    let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem =
+    let exec ({integer_type_widths} as model_env) ~ret:_ mem =
       match src with
       | Exp.Const (Const.Cstr s) ->
           let locs = Sem.eval_locs tgt mem in
-          BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem
+          BoUtils.Exec.decl_string model_env locs s mem
       | _ ->
           let tgt_locs = Sem.eval_locs tgt mem in
           let v = Sem.eval integer_type_widths src mem in

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -15,8 +15,23 @@ module PO = BufferOverrunProofObligations
 module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
+module TypModels = BufferOverrunTypModels
+
+module ModelEnv = struct
+  type model_env =
+    { pname: Typ.Procname.t
+    ; node_hash: int
+    ; location: Location.t
+    ; tenv: Tenv.t
+    ; integer_type_widths: Typ.IntegerWidths.t }
+
+  let mk_model_env pname ~node_hash location tenv integer_type_widths =
+    {pname; node_hash; location; tenv; integer_type_widths}
+end
 
 module Exec = struct
+  open ModelEnv
+
   let load_locs id locs mem =
     let v = Dom.Mem.find_set locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
@@ -31,34 +46,26 @@ module Exec = struct
 
   let load_val id v mem = load_locs id (Dom.Val.get_all_locs v) mem
 
-  type decl_local =
-       Typ.Procname.t
-    -> node_hash:int
-    -> Location.t
-    -> Loc.t
-    -> Typ.t
-    -> inst_num:int
-    -> represents_multiple_values:bool
-    -> dimension:int
-    -> Dom.Mem.t
-    -> Dom.Mem.t * int
+  let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values
+      ~dimension mem =
+    match typ.Typ.desc with
+    | Typ.Tarray {elt= typ; length; stride} ->
+        let stride = Option.map ~f:IntLit.to_int_exn stride in
+        decl_local_array model_env loc typ ~length ?stride ~inst_num ~represents_multiple_values
+          ~dimension mem
+    | Typ.Tstruct typname -> (
+      match TypModels.dispatch tenv typname with
+      | Some (CArray {element_typ; length}) ->
+          decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num
+            ~represents_multiple_values ~dimension mem
+      | Some JavaCollection | None ->
+          (mem, inst_num) )
+    | _ ->
+        (mem, inst_num)
+
 
-  let decl_local_array :
-         decl_local:decl_local
-      -> Typ.Procname.t
-      -> node_hash:int
-      -> Location.t
-      -> Loc.t
-      -> Typ.t
-      -> length:IntLit.t option
-      -> ?stride:int
-      -> inst_num:int
-      -> represents_multiple_values:bool
-      -> dimension:int
-      -> Dom.Mem.t
-      -> Dom.Mem.t * int =
-   fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num
-       ~represents_multiple_values ~dimension mem ->
+  and decl_local_array ({pname; node_hash; location} as model_env) loc typ ~length ?stride
+      ~inst_num ~represents_multiple_values ~dimension mem =
     let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
     let path = Loc.get_path loc in
     let allocsite =
@@ -81,13 +88,18 @@ module Exec = struct
     in
     let loc = Loc.of_allocsite allocsite in
     let mem, _ =
-      decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:true
+      decl_local_loc model_env loc typ ~inst_num ~represents_multiple_values:true
         ~dimension:(dimension + 1) mem
     in
     (mem, inst_num + 1)
 
 
-  let init_c_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem =
+  let decl_local model_env (mem, inst_num) (loc, typ) =
+    decl_local_loc model_env loc typ ~inst_num ~represents_multiple_values:false ~dimension:1 mem
+
+
+  let init_c_array_fields {pname; node_hash; tenv; integer_type_widths} path 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
       let field_loc = PowLoc.append_field locs ~fn:field_name in
@@ -133,7 +145,7 @@ module Exec = struct
     init_fields path typ locs 1 ?dyn_length mem
 
 
-  let rec set_dyn_length location tenv typ locs dyn_length mem =
+  let rec set_dyn_length ({location; tenv} as model_env) typ locs dyn_length mem =
     match typ.Typ.desc with
     | Tstruct typename -> (
       match Tenv.lookup tenv typename with
@@ -148,7 +160,7 @@ module Exec = struct
               in
               Dom.Mem.strong_update field_loc v mem
           | _ ->
-              set_dyn_length location tenv field_typ field_loc dyn_length mem )
+              set_dyn_length model_env field_typ field_loc dyn_length mem )
       | _ ->
           mem )
     | _ ->
@@ -157,7 +169,7 @@ module Exec = struct
 
   let get_max_char s = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c))
 
-  let decl_string pname ~node_hash integer_type_widths location locs s mem =
+  let decl_string {pname; node_hash; location; integer_type_widths} locs s mem =
     let stride = Some (Typ.width_of_ikind integer_type_widths IChar / 8) in
     let offset = Itv.zero in
     let size = Itv.of_int (String.length s + 1) in

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -11,61 +11,37 @@ module Dom = BufferOverrunDomain
 module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 
+module ModelEnv : sig
+  type model_env =
+    { pname: Typ.Procname.t
+    ; node_hash: int
+    ; location: Location.t
+    ; tenv: Tenv.t
+    ; integer_type_widths: Typ.IntegerWidths.t }
+
+  val mk_model_env :
+    Typ.Procname.t -> node_hash:int -> Location.t -> Tenv.t -> Typ.IntegerWidths.t -> model_env
+end
+
 module Exec : sig
   val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
 
   val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
 
-  type decl_local =
-       Typ.Procname.t
-    -> node_hash:int
-    -> Location.t
-    -> Loc.t
-    -> Typ.t
-    -> inst_num:int
-    -> represents_multiple_values:bool
-    -> dimension:int
-    -> Dom.Mem.t
-    -> Dom.Mem.t * int
-
-  val decl_local_array :
-       decl_local:decl_local
-    -> Typ.Procname.t
-    -> node_hash:int
-    -> Location.t
-    -> Loc.t
-    -> Typ.t
-    -> length:IntLit.t option
-    -> ?stride:int
-    -> inst_num:int
-    -> represents_multiple_values:bool
-    -> dimension:int
-    -> Dom.Mem.t
-    -> Dom.Mem.t * int
+  val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int
 
   val init_c_array_fields :
-       Tenv.t
-    -> Typ.IntegerWidths.t
-    -> Typ.Procname.t
+       ModelEnv.model_env
     -> Itv.SymbolPath.partial option
-    -> node_hash:int
     -> Typ.t
     -> PowLoc.t
     -> ?dyn_length:Exp.t
     -> Dom.Mem.t
     -> Dom.Mem.t
 
-  val set_dyn_length : Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t
+  val set_dyn_length : ModelEnv.model_env -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t
 
-  val decl_string :
-       Typ.Procname.t
-    -> node_hash:int
-    -> Typ.IntegerWidths.t
-    -> Location.t
-    -> PowLoc.t
-    -> string
-    -> Dom.Mem.t
-    -> Dom.Mem.t
+  val decl_string : ModelEnv.model_env -> PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t
 end
 
 module Check : sig