[inferbo] Separate Java from C arrays

Reviewed By: skcho, jvillard

Differential Revision: D13190942

fbshipit-source-id: 6b7f4225b

infer/src/bufferoverrun/arrayBlk.ml

@@ -11,102 +11,215 @@ open! IStd
 open AbsLoc
 open! AbstractDomain.Types
 module Bound = Bounds.Bound
+module F = Format
+module L = Logging
 
 module ArrInfo = struct
-  type t = {offset: Itv.t; size: Itv.t; stride: Itv.t} [@@deriving compare]
+  type t = C of {offset: Itv.t; size: Itv.t; stride: Itv.t} | Java of {length: Itv.t} | Top
+  [@@deriving compare]
 
-  let top : t = {offset= Itv.top; size= Itv.top; stride= Itv.top}
+  let top : t = Top
 
-  let make : offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
-   fun ~offset ~size ~stride -> {offset; size; stride}
+  let make_c : offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
+   fun ~offset ~size ~stride -> C {offset; size; stride}
 
 
+  let make_java : length:Itv.t -> t = fun ~length -> Java {length}
+
   let join : t -> t -> t =
    fun a1 a2 ->
     if phys_equal a1 a2 then a2
     else
-      { offset= Itv.join a1.offset a2.offset
-      ; size= Itv.join a1.size a2.size
-      ; stride= Itv.join a1.stride a2.stride }
+      match (a1, a2) with
+      | ( C {offset= offset1; size= size1; stride= stride1}
+        , C {offset= offset2; size= size2; stride= stride2} ) ->
+          C
+            { offset= Itv.join offset1 offset2
+            ; size= Itv.join size1 size2
+            ; stride= Itv.join stride1 stride2 }
+      | Java {length= length1}, Java {length= length2} ->
+          Java {length= Itv.join length1 length2}
+      | _ ->
+          Top
 
 
   let widen : prev:t -> next:t -> num_iters:int -> t =
    fun ~prev ~next ~num_iters ->
     if phys_equal prev next then next
     else
-      { offset= Itv.widen ~prev:prev.offset ~next:next.offset ~num_iters
-      ; size= Itv.widen ~prev:prev.size ~next:next.size ~num_iters
-      ; stride= Itv.widen ~prev:prev.stride ~next:next.stride ~num_iters }
+      match (prev, next) with
+      | ( C {offset= offset1; size= size1; stride= stride1}
+        , C {offset= offset2; size= size2; stride= stride2} ) ->
+          C
+            { offset= Itv.widen ~prev:offset1 ~next:offset2 ~num_iters
+            ; size= Itv.widen ~prev:size1 ~next:size2 ~num_iters
+            ; stride= Itv.widen ~prev:stride1 ~next:stride2 ~num_iters }
+      | Java {length= length1}, Java {length= length2} ->
+          Java {length= Itv.widen ~prev:length1 ~next:length2 ~num_iters}
+      | _ ->
+          Top
 
 
   let ( <= ) : lhs:t -> rhs:t -> bool =
    fun ~lhs ~rhs ->
     if phys_equal lhs rhs then true
     else
-      Itv.le ~lhs:lhs.offset ~rhs:rhs.offset
-      && Itv.le ~lhs:lhs.size ~rhs:rhs.size
-      && Itv.le ~lhs:lhs.stride ~rhs:rhs.stride
-
-
-  let plus_offset : t -> Itv.t -> t = fun arr i -> {arr with offset= Itv.plus arr.offset i}
-
-  let minus_offset : t -> Itv.t -> t = fun arr i -> {arr with offset= Itv.minus arr.offset i}
+      match (lhs, rhs) with
+      | ( C {offset= offset1; size= size1; stride= stride1}
+        , C {offset= offset2; size= size2; stride= stride2} ) ->
+          Itv.le ~lhs:offset1 ~rhs:offset2 && Itv.le ~lhs:size1 ~rhs:size2
+          && Itv.le ~lhs:stride1 ~rhs:stride2
+      | Java {length= length1}, Java {length= length2} ->
+          Itv.le ~lhs:length1 ~rhs:length2
+      | _, Top ->
+          true
+      | _ ->
+          false
+
+
+  let map_offset : f:(Itv.t -> Itv.t) -> t -> t =
+   fun ~f arr ->
+    match arr with
+    | C {offset; size; stride} ->
+        C {offset= f offset; size; stride}
+    | Java _ ->
+        L.(die InternalError) "Unexpected pointer arithmetics on Java array"
+    | Top ->
+        Top
+
+
+  let plus_offset : t -> Itv.t -> t = fun arr i -> map_offset arr ~f:(Itv.plus i)
+
+  let minus_offset : t -> Itv.t -> t =
+   fun arr i -> map_offset arr ~f:(fun offset -> Itv.minus offset i)
+
+
+  let diff : t -> t -> Itv.t =
+   fun arr1 arr2 ->
+    match (arr1, arr2) with
+    | C {offset= offset1}, C {offset= offset2} ->
+        Itv.minus offset1 offset2
+    | Java _, _ | _, Java _ ->
+        L.(die InternalError) "Unexpected pointer arithmetics on Java array"
+    | Top, _ | _, Top ->
+        Itv.top
 
-  let diff : t -> t -> Itv.t = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset
 
   let subst : t -> Bound.eval_sym -> t =
    fun arr eval_sym ->
-    {arr with offset= Itv.subst arr.offset eval_sym; size= Itv.subst arr.size eval_sym}
-
-
-  let pp : Format.formatter -> t -> unit =
-   fun fmt arr -> Format.fprintf fmt "offset : %a, size : %a" Itv.pp arr.offset Itv.pp arr.size
+    match arr with
+    | C {offset; size; stride} ->
+        C {offset= Itv.subst offset eval_sym; size= Itv.subst size eval_sym; stride}
+    | Java {length} ->
+        Java {length= Itv.subst length eval_sym}
+    | Top ->
+        Top
+
+
+  let pp : F.formatter -> t -> unit =
+   fun f arr ->
+    match arr with
+    | C {offset; size} ->
+        F.fprintf f "offset : %a, size : %a" Itv.pp offset Itv.pp size
+    | Java {length} ->
+        F.fprintf f "length : %a" Itv.pp length
+    | Top ->
+        F.pp_print_string f SpecialChars.down_tack
 
 
   let get_symbols : t -> Itv.SymbolSet.t =
    fun arr ->
-    let s1 = Itv.get_symbols arr.offset in
-    let s2 = Itv.get_symbols arr.size in
-    let s3 = Itv.get_symbols arr.stride in
-    Itv.SymbolSet.union3 s1 s2 s3
+    match arr with
+    | C {offset; size; stride} ->
+        let s1 = Itv.get_symbols offset in
+        let s2 = Itv.get_symbols size in
+        let s3 = Itv.get_symbols stride in
+        Itv.SymbolSet.union3 s1 s2 s3
+    | Java {length} ->
+        Itv.get_symbols length
+    | Top ->
+        Itv.SymbolSet.empty
 
 
   let normalize : t -> t =
    fun arr ->
-    { offset= Itv.normalize arr.offset
-    ; size= Itv.normalize arr.size
-    ; stride= Itv.normalize arr.stride }
+    match arr with
+    | C {offset; size; stride} ->
+        C {offset= Itv.normalize offset; size= Itv.normalize size; stride= Itv.normalize stride}
+    | Java {length} ->
+        Java {length= Itv.normalize length}
+    | Top ->
+        Top
 
 
-  let prune_comp : Binop.t -> t -> t -> t =
-   fun c arr1 arr2 -> {arr1 with offset= Itv.prune_comp c arr1.offset arr2.offset}
+  let prune_offset : f:(Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
+   fun ~f arr1 arr2 ->
+    match arr2 with
+    | C {offset= offset2} ->
+        map_offset arr1 ~f:(fun offset1 -> f offset1 offset2)
+    | Java _ | Top ->
+        arr1
+
 
+  let prune_comp : Binop.t -> t -> t -> t =
+   fun c arr1 arr2 -> prune_offset arr1 arr2 ~f:(Itv.prune_comp c)
 
-  let prune_eq : t -> t -> t =
-   fun arr1 arr2 -> {arr1 with offset= Itv.prune_eq arr1.offset arr2.offset}
 
+  let prune_eq : t -> t -> t = fun arr1 arr2 -> prune_offset arr1 arr2 ~f:Itv.prune_eq
 
-  let prune_ne : t -> t -> t =
-   fun arr1 arr2 -> {arr1 with offset= Itv.prune_ne arr1.offset arr2.offset}
+  let prune_ne : t -> t -> t = fun arr1 arr2 -> prune_offset arr1 arr2 ~f:Itv.prune_ne
 
+  let set_length : Itv.t -> t -> t =
+   fun size arr ->
+    match arr with
+    | C {offset; stride} ->
+        C {offset; size; stride}
+    | Java _ ->
+        Java {length= size}
+    | Top ->
+        Top
 
-  let set_length : Itv.t -> t -> t = fun size arr -> {arr with size}
 
   (* Set new stride only when the previous stride is a constant interval. *)
   let set_stride : Z.t -> t -> t =
-   fun new_stride ({offset; size; stride} as arr) ->
-    Option.value_map (Itv.is_const stride) ~default:arr ~f:(fun stride ->
-        assert ((not Z.(equal stride zero)) && not Z.(equal new_stride zero)) ;
-        if Z.equal new_stride stride then arr
-        else
-          let set itv = Itv.div_const (Itv.mult_const itv stride) new_stride in
-          {offset= set offset; size= set size; stride= Itv.of_big_int new_stride} )
+   fun new_stride arr ->
+    match arr with
+    | C {offset; size; stride} ->
+        Option.value_map (Itv.is_const stride) ~default:arr ~f:(fun stride ->
+            assert ((not Z.(equal stride zero)) && not Z.(equal new_stride zero)) ;
+            if Z.equal new_stride stride then arr
+            else
+              let set itv = Itv.div_const (Itv.mult_const itv stride) new_stride in
+              C {offset= set offset; size= set size; stride= Itv.of_big_int new_stride} )
+    | Java _ ->
+        L.(die InternalError) "Unexpected cast on Java array"
+    | Top ->
+        Top
+
+
+  let offsetof = function C {offset} -> offset | Java _ -> Itv.zero | Top -> Itv.top
+
+  let sizeof = function C {size} -> size | Java {length} -> length | Top -> Itv.top
+
+  let byte_size = function
+    | C {size; stride} ->
+        Itv.mult size stride
+    | Java _ ->
+        L.(die InternalError) "Unexpected byte-size operation on Java array"
+    | Top ->
+        Itv.top
 
 
   let lift_cmp_itv cmp_itv arr1 arr2 =
-    if Itv.eq arr1.stride arr2.stride && Itv.eq arr1.size arr2.size then
-      cmp_itv arr1.offset arr2.offset
-    else Boolean.Top
+    match (arr1, arr2) with
+    | ( C {offset= offset1; size= size1; stride= stride1}
+      , C {offset= offset2; size= size2; stride= stride2} )
+      when Itv.eq stride1 stride2 && Itv.eq size1 size2 ->
+        cmp_itv offset1 offset2
+    | Java {length= length1}, Java {length= length2} when Itv.eq length1 length2 ->
+        cmp_itv Itv.zero Itv.zero
+    | _ ->
+        Boolean.Top
 end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
@@ -117,17 +230,23 @@ let unknown : t = add Allocsite.unknown ArrInfo.top bot
 
 let is_bot : t -> bool = is_empty
 
-let make : Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
- fun a ~offset ~size ~stride -> singleton a (ArrInfo.make ~offset ~size ~stride)
+let make_c : Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
+ fun a ~offset ~size ~stride -> singleton a (ArrInfo.make_c ~offset ~size ~stride)
+
+
+let make_java : Allocsite.t -> length:Itv.t -> t =
+ fun a ~length -> singleton a (ArrInfo.make_java ~length)
+
 
+let join_itv : f:(ArrInfo.t -> Itv.t) -> t -> Itv.t =
+ fun ~f a -> fold (fun _ arr -> Itv.join (f arr)) a Itv.bot
 
-let offsetof : t -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.offset) a Itv.bot
 
-let sizeof : t -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot
+let offsetof = join_itv ~f:ArrInfo.offsetof
 
-let sizeof_byte : t -> Itv.t =
- fun a -> fold (fun _ arr -> Itv.join (Itv.mult arr.ArrInfo.size arr.ArrInfo.stride)) a Itv.bot
+let sizeof = join_itv ~f:ArrInfo.sizeof
 
+let sizeof_byte = join_itv ~f:ArrInfo.byte_size
 
 let plus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr
 
@@ -177,7 +296,7 @@ let do_prune : (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> t -> t -> t =
  fun arr_info_prune a1 a2 ->
   match is_singleton_or_more a2 with
   | IContainer.Singleton (k, v2) ->
-      if mem k a1 then add k (arr_info_prune (find k a1) v2) a1 else a1
+      update k (Option.map ~f:(fun v -> arr_info_prune v v2)) a1
   | _ ->
       a1
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -47,7 +47,7 @@ module Init = struct
         match TypModels.dispatch tenv typname with
         | Some typ_model -> (
           match typ_model with
-          | Array {element_typ; length} ->
+          | 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
           | JavaCollection ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -145,17 +145,25 @@ module Val = struct
 
   let of_pow_loc ~traces powloc = {bot with powloc; traces}
 
-  let of_array_alloc :
+  let of_c_array_alloc :
       Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> traces:TraceSet.t -> t =
    fun allocsite ~stride ~offset ~size ~traces ->
     let stride = Option.value_map stride ~default:Itv.nat ~f:Itv.of_int in
     { bot with
-      arrayblk= ArrayBlk.make allocsite ~offset ~size ~stride
+      arrayblk= ArrayBlk.make_c allocsite ~offset ~size ~stride
     ; offset_sym= Relation.Sym.of_allocsite_offset allocsite
     ; size_sym= Relation.Sym.of_allocsite_size allocsite
     ; traces }
 
 
+  let of_java_array_alloc : Allocsite.t -> length:Itv.t -> traces:TraceSet.t -> t =
+   fun allocsite ~length ~traces ->
+    { bot with
+      arrayblk= ArrayBlk.make_java allocsite ~length
+    ; size_sym= Relation.Sym.of_allocsite_size allocsite
+    ; traces }
+
+
   let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
 
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
@@ -371,21 +379,21 @@ module Val = struct
             in
             let offset = Itv.of_offset_path path in
             let size = Itv.of_length_path path in
-            ArrayBlk.make allocsite ~stride ~offset ~size
+            ArrayBlk.make_c allocsite ~stride ~offset ~size
           in
           {bot with arrayblk; traces}
     | Tstruct typename -> (
       match BufferOverrunTypModels.dispatch tenv typename with
       | Some typ_model -> (
         match typ_model with
-        | Array {deref_kind; length} ->
+        | CArray {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
+            of_c_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
@@ -399,8 +407,6 @@ module Val = struct
         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 stride = Option.map stride ~f:(fun n -> IntLit.to_int_exn n) in
-        let offset = Itv.zero in
         let size =
           match length with
           | None (* IncompleteArrayType, no-size flexible array *) ->
@@ -412,7 +418,11 @@ module Val = struct
           | Some length ->
               Itv.of_big_int (IntLit.to_big_int length)
         in
-        of_array_alloc allocsite ~stride ~offset ~size ~traces
+        if is_java then of_java_array_alloc allocsite ~length:size ~traces
+        else
+          let stride = Option.map stride ~f:(fun n -> IntLit.to_int_exn n) in
+          let offset = Itv.zero in
+          of_c_array_alloc allocsite ~stride ~offset ~size ~traces
 
 
   let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t =
@@ -1001,10 +1011,14 @@ module MemReach = struct
   let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc)
 
   let init_array_relation :
-      Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t -> t
-      =
-   fun allocsite ~offset ~size ~size_exp_opt ->
-    lift_relation (Relation.init_array allocsite ~offset ~size ~size_exp_opt)
+         Allocsite.t
+      -> offset_opt:Itv.t option
+      -> size:Itv.t
+      -> size_exp_opt:Relation.SymExp.t option
+      -> t
+      -> t =
+   fun allocsite ~offset_opt ~size ~size_exp_opt ->
+    lift_relation (Relation.init_array allocsite ~offset_opt ~size ~size_exp_opt)
 
 
   let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t =
@@ -1135,10 +1149,14 @@ module Mem = struct
 
 
   let init_array_relation :
-      Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t -> t
-      =
-   fun allocsite ~offset ~size ~size_exp_opt ->
-    map ~f:(MemReach.init_array_relation allocsite ~offset ~size ~size_exp_opt)
+         Allocsite.t
+      -> offset_opt:Itv.t option
+      -> size:Itv.t
+      -> size_exp_opt:Relation.SymExp.t option
+      -> t
+      -> t =
+   fun allocsite ~offset_opt ~size ~size_exp_opt ->
+    map ~f:(MemReach.init_array_relation allocsite ~offset_opt ~size ~size_exp_opt)
 
 
   let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t =

infer/src/bufferoverrun/bufferOverrunDomainRelation.ml

@@ -101,7 +101,7 @@ module type S = sig
   val init_param : Loc.t -> t -> t
 
   val init_array :
-    Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t
+    Allocsite.t -> offset_opt:Itv.t option -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t
 
   val forget_locs : PowLoc.t -> t -> t
 
@@ -211,7 +211,7 @@ module NoRelation = struct
 
   let init_param = f2
 
-  let init_array _allocsite ~offset:_ ~size:_ ~size_exp_opt:_ = f1
+  let init_array _allocsite ~offset_opt:_ ~size:_ ~size_exp_opt:_ = f1
 
   let forget_locs = f2
 
@@ -1433,10 +1433,8 @@ module Make (Manager : Manager_S) = struct
       meet_constraints (Constraints.eq_of param_var var) x
 
 
-    let init_array allocsite ~offset ~size ~size_exp_opt x =
-      let offset_sym = Sym.of_allocsite_offset allocsite in
+    let init_array allocsite ~offset_opt ~size ~size_exp_opt x =
       let size_sym = Sym.of_allocsite_size allocsite in
-      let offset_constrs = Constraints.itv_of offset_sym offset in
       let size_constrs =
         match size_exp_opt with
         | None ->
@@ -1448,7 +1446,16 @@ module Make (Manager : Manager_S) = struct
           | Some constr ->
               constr )
       in
-      meet_constraints (Constraints.and_ offset_constrs size_constrs) x
+      let constraints =
+        match offset_opt with
+        | Some offset ->
+            let offset_sym = Sym.of_allocsite_offset allocsite in
+            let offset_constrs = Constraints.itv_of offset_sym offset in
+            Constraints.and_ offset_constrs size_constrs
+        | None ->
+            size_constrs
+      in
+      meet_constraints constraints x
 
 
     let subst_param_caller subst_map caller =
@@ -1556,9 +1563,14 @@ module Make (Manager : Manager_S) = struct
 
 
   let init_array :
-      Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t =
-   fun allocsite ~offset ~size ~size_exp_opt ->
-    lift_default ~default:Bottom (PackedVal.init_array allocsite ~offset ~size ~size_exp_opt)
+         Allocsite.t
+      -> offset_opt:Itv.t option
+      -> size:Itv.t
+      -> size_exp_opt:SymExp.t option
+      -> t
+      -> t =
+   fun allocsite ~offset_opt ~size ~size_exp_opt ->
+    lift_default ~default:Bottom (PackedVal.init_array allocsite ~offset_opt ~size ~size_exp_opt)
 
 
   let forget_locs : PowLoc.t -> t -> t = fun locs -> lift (PackedVal.forget_locs locs)

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -83,11 +83,11 @@ let malloc size_exp =
       let size_exp = Option.value dyn_length ~default:length0 in
       Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp
     in
-    let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces in
+    let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in
     mem
     |> Dom.Mem.add_stack (Loc.of_id id) v
-    |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt
-    |> BoUtils.Exec.init_array_fields tenv integer_type_widths pname path ~node_hash typ
+    |> 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
   and check = check_alloc_size size_exp in
   {exec; check}
@@ -232,7 +232,7 @@ let set_array_length array length_exp =
           Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path
             ~represents_multiple_values
         in
-        let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in
+        let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in
         Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem
     | _ ->
         L.(die InternalError) "Unexpected type of first argument for __set_array_length() "

infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml

@@ -37,7 +37,7 @@ let mk pdesc =
                   Typ.void
               | Tstruct typename -> (
                 match BufferOverrunTypModels.dispatch tenv typename with
-                | Some (Array {element_typ}) ->
+                | Some (CArray {element_typ}) ->
                     element_typ
                 | Some _ ->
                     L.(die InternalError)

infer/src/bufferoverrun/bufferOverrunTypModels.ml

@@ -8,11 +8,11 @@
 open! IStd
 
 type typ_model =
-  | Array of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t}
+  | CArray of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t}
   | JavaCollection
 
 let std_array element_typ length =
-  Array {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length}
+  CArray {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.

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -64,7 +64,6 @@ module Exec = struct
       -> Dom.Mem.t * int =
    fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num
        ~represents_multiple_values ~dimension mem ->
-    let offset = Itv.zero in
     let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
     let path = Loc.get_path loc in
     let allocsite =
@@ -72,14 +71,19 @@ module Exec = struct
       Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values
     in
     let mem =
-      let arr =
+      let arr, offset_opt =
         let traces = Trace.(Set.singleton location ArrayDeclaration) in
-        Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces
-        |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
+        match Typ.Procname.get_language pname with
+        | Language.Clang ->
+            let offset = Itv.zero in
+            (Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces, Some offset)
+        | Language.Java ->
+            (Dom.Val.of_java_array_alloc allocsite ~length:size ~traces, None)
       in
+      let arr = Dom.Val.sets_represents_multiple_values arr ~represents_multiple_values in
+      let mem = Dom.Mem.init_array_relation allocsite ~offset_opt ~size ~size_exp_opt:None mem in
       if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem
     in
-    let mem = Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None mem in
     let loc = Loc.of_allocsite allocsite in
     let mem, _ =
       decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:true
@@ -118,7 +122,7 @@ module Exec = struct
     (mem, inst_num + 1)
 
 
-  let init_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem =
+  let init_c_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
       let field_loc = PowLoc.append_field locs ~fn:field_name in
@@ -140,10 +144,11 @@ module Exec = struct
             let offset, size = (Itv.zero, length) in
             let v =
               let traces = TraceSet.empty (* TODO: location of field declaration *) in
-              Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces
+              Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces
             in
             mem |> Dom.Mem.strong_update field_loc v
-            |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
+            |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size
+                 ~size_exp_opt:None
         | _ ->
             init_fields field_path field_typ field_loc dimension ?dyn_length mem
       in

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -56,7 +56,7 @@ module Exec : sig
     -> Dom.Mem.t
     -> Dom.Mem.t * int
 
-  val init_array_fields :
+  val init_c_array_fields :
        Tenv.t
     -> Typ.IntegerWidths.t
     -> Typ.Procname.t