From 373e6b39ccd036decef3c9d66c080082ccc66667 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 23 Feb 2018 20:40:57 -0800
Subject: [PATCH] [infer] Use inline record for Typ.Tarray

Summary: It uses the inline record type for `Typ.Tarray`.

Reviewed By: mbouaziz

Differential Revision: D7042272

fbshipit-source-id: c793016
---
 infer/src/IR/AccessPath.ml                    |  2 +-
 infer/src/IR/Typ.ml                           | 23 ++++++++------
 infer/src/IR/Typ.mli                          |  7 +++--
 infer/src/backend/BuiltinDefn.ml              |  9 +++---
 infer/src/backend/absarray.ml                 | 10 +++----
 infer/src/backend/dom.ml                      |  9 +++---
 infer/src/backend/dotty.ml                    |  2 +-
 infer/src/backend/prop.ml                     | 20 ++++++-------
 infer/src/backend/prover.ml                   | 14 ++++-----
 infer/src/backend/rearrange.ml                | 30 ++++++++++---------
 infer/src/backend/symExec.ml                  | 10 ++++---
 .../src/bufferoverrun/bufferOverrunChecker.ml | 14 ++++-----
 .../src/bufferoverrun/bufferOverrunModels.ml  |  8 ++---
 .../bufferoverrun/bufferOverrunSemantics.ml   |  6 ++--
 infer/src/bufferoverrun/bufferOverrunUtils.ml |  2 +-
 infer/src/checkers/uninit.ml                  |  4 +--
 infer/src/clang/cTrans.ml                     |  8 ++---
 infer/src/clang/cType_to_sil_type.ml          |  2 +-
 infer/src/java/jTrans.ml                      |  4 +--
 infer/src/java/jTransType.ml                  | 12 +++-----
 infer/src/unit/accessPathTests.ml             |  2 +-
 21 files changed, 104 insertions(+), 94 deletions(-)

diff --git a/infer/src/IR/AccessPath.ml b/infer/src/IR/AccessPath.ml
index faf0f3c8d..cf6da80b4 100644
--- a/infer/src/IR/AccessPath.ml
+++ b/infer/src/IR/AccessPath.ml
@@ -161,7 +161,7 @@ module Raw = struct
             if include_array_indexes then of_exp_ index_exp typ [] [] else []
           in
           let array_access = ArrayAccess (typ, index_access_paths) in
-          let array_typ = Typ.mk (Tarray (typ, None, None)) in
+          let array_typ = Typ.mk_array typ in
           of_exp_ root_exp array_typ (array_access :: accesses) acc
       | Exp.Cast (cast_typ, cast_exp) ->
           of_exp_ cast_exp cast_typ [] acc
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index ed1ec8599..4cf950ecc 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -127,7 +127,7 @@ module T = struct
     | Tptr of t * ptr_kind  (** pointer type *)
     | Tstruct of name  (** structured value type name *)
     | TVar of string  (** type variable (ie. C++ template variables) *)
-    | Tarray of t * IntLit.t option * IntLit.t option
+    | Tarray of {elt: t; length: IntLit.t option; stride: IntLit.t option}
         (** array type with statically fixed length and stride *)
     [@@deriving compare]
 
@@ -185,6 +185,10 @@ let mk ?default ?quals desc : t =
   mk_aux ?default ?quals desc
 
 
+let mk_array ?default ?quals ?length ?stride elt : t =
+  mk ?default ?quals (Tarray {elt; length; stride})
+
+
 let void_star = mk (Tptr (mk Tvoid, Pk_pointer))
 
 let merge_quals quals1 quals2 =
@@ -222,9 +226,9 @@ let rec pp_full pe f typ =
         F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk |> escape pe)
     | Tptr (typ, pk) ->
         F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk |> escape pe)
-    | Tarray (typ, static_len, static_stride) ->
+    | Tarray {elt; length; stride} ->
         let pp_int_opt fmt = function Some x -> IntLit.pp fmt x | None -> F.fprintf fmt "_" in
-        F.fprintf f "%a[%a*%a]" (pp_full pe) typ pp_int_opt static_len pp_int_opt static_stride
+        F.fprintf f "%a[%a*%a]" (pp_full pe) elt pp_int_opt length pp_int_opt stride
   in
   F.fprintf f "%a%a" pp_desc typ pp_quals typ
 
@@ -279,10 +283,10 @@ let rec sub_type subst generic_typ : t =
         mk ~quals:(merge_quals t.quals generic_typ.quals) t.desc
     | None ->
         generic_typ )
-  | Tarray (typ, arg1, arg2) ->
+  | Tarray {elt= typ; length; stride} ->
       let typ' = sub_type subst typ in
       if phys_equal typ typ' then generic_typ
-      else mk ~default:generic_typ (Tarray (typ', arg1, arg2))
+      else mk_array ~default:generic_typ typ' ?length ?stride
   | Tptr (typ, arg) ->
       let typ' = sub_type subst typ in
       if phys_equal typ typ' then generic_typ else mk ~default:generic_typ (Tptr (typ', arg))
@@ -483,7 +487,7 @@ let strip_ptr typ = match typ.desc with Tptr (t, _) -> t | _ -> assert false
 (** If an array type, return the type of the element.
     If not, return the default type if given, otherwise raise an exception *)
 let array_elem default_opt typ =
-  match typ.desc with Tarray (t_el, _, _) -> t_el | _ -> unsome "array_elem" default_opt
+  match typ.desc with Tarray {elt} -> elt | _ -> unsome "array_elem" default_opt
 
 
 let is_class_of_kind check_fun typ =
@@ -650,7 +654,7 @@ module Procname = struct
             mk (Tfloat FDouble)
         | typ_str when String.contains typ_str '[' ->
             let stripped_typ = String.sub typ_str ~pos:0 ~len:(String.length typ_str - 2) in
-            mk (Tptr (mk (Tarray (java_from_string stripped_typ, None, None)), Pk_pointer))
+            mk (Tptr (mk_array (java_from_string stripped_typ), Pk_pointer))
         | typ_str ->
             mk (Tstruct (Name.Java.from_string typ_str))
       in
@@ -1057,6 +1061,7 @@ module Procname = struct
     | _ ->
         QualifiedCppName.empty
 
+
   (** Convert a proc name to a filename *)
   let to_concrete_filename ?crc_only pname =
     (* filenames for clang procs are REVERSED qualifiers with '#' as separator *)
@@ -1266,8 +1271,8 @@ module Struct = struct
   (** the element typ of the final extensible array in the given typ, if any *)
   let rec get_extensible_array_element_typ ~lookup (typ: T.t) =
     match typ.desc with
-    | Tarray (typ, _, _) ->
-        Some typ
+    | Tarray {elt} ->
+        Some elt
     | Tstruct name -> (
       match lookup name with
       | Some {fields} -> (
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 1c4185bcf..82d2d067c 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -78,8 +78,8 @@ and desc =
   | Tptr of t * ptr_kind  (** pointer type *)
   | Tstruct of name  (** structured value type name *)
   | TVar of string  (** type variable (ie. C++ template variables) *)
-  | Tarray of t * IntLit.t option * IntLit.t option
-      (** array type with statically fixed stride and length *)
+  | Tarray of {elt: t; length: IntLit.t option; stride: IntLit.t option}
+      (** array type with statically fixed length and stride *)
   [@@deriving compare]
 
 and name =
@@ -109,6 +109,9 @@ and template_spec_info =
 val mk : ?default:t -> ?quals:type_quals -> desc -> t
 (** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals *)
 
+val mk_array : ?default:t -> ?quals:type_quals -> ?length:IntLit.t -> ?stride:IntLit.t -> t -> t
+(** Create an array type from a given element type. If [length] or [stride] value is given, use them as static length and size. *)
+
 val void_star : t
 (** void* type *)
 
diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml
index 543194f3c..5d1a18602 100644
--- a/infer/src/backend/BuiltinDefn.ml
+++ b/infer/src/backend/BuiltinDefn.ml
@@ -45,7 +45,7 @@ let extract_array_type typ =
     | Typ.Tarray _ ->
         Some typ
     | Typ.Tptr (elt, _) ->
-        Some (Typ.mk ~default:typ (Tarray (elt, None, None)))
+        Some (Typ.mk_array ~default:typ elt)
     | _ ->
         None
 
@@ -556,10 +556,11 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id;
     | Exp.Lfield _
     | Exp.Lindex _ ->
         e
-    | Exp.Sizeof {typ= {Typ.desc= Tarray ({Typ.desc= Tint ik}, _, _)}; dynamic_length= Some len}
+    | Exp.Sizeof {typ= {Typ.desc= Tarray {elt= {Typ.desc= Tint ik}}}; dynamic_length= Some len}
       when Typ.ikind_is_char ik ->
         evaluate_char_sizeof len
-    | Exp.Sizeof {typ= {Typ.desc= Tarray ({Typ.desc= Tint ik}, Some len, _)}; dynamic_length= None}
+    | Exp.Sizeof
+        {typ= {Typ.desc= Tarray {elt= {Typ.desc= Tint ik}; length= Some len}}; dynamic_length= None}
       when Typ.ikind_is_char ik ->
         evaluate_char_sizeof (Exp.Const (Const.Cint len))
     | Exp.Sizeof _ ->
@@ -585,7 +586,7 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id;
   in
   let cnt_te =
     Exp.Sizeof
-      { typ= Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None, Some (IntLit.of_int 1)))
+      { typ= Typ.mk_array (Typ.mk (Tint Typ.IChar)) ~stride:(IntLit.of_int 1)
       ; nbytes= None
       ; dynamic_length= Some size_exp'
       ; subtype= Subtype.exact }
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index 53a38c1f8..d3b542623 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -85,7 +85,7 @@ end = struct
           get_strexp_at_syn_offsets tenv se' t' syn_offs'
       | None ->
           fail () )
-    | Sil.Earray (_, esel, _), Typ.Tarray (t', _, _), (Index ind) :: syn_offs' ->
+    | Sil.Earray (_, esel, _), Typ.Tarray {elt= t'}, (Index ind) :: syn_offs' ->
         let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' ind) esel) in
         get_strexp_at_syn_offsets tenv se' t' syn_offs'
     | _ ->
@@ -115,7 +115,7 @@ end = struct
           Sil.Estruct (fsel', inst)
       | None ->
           assert false )
-    | Sil.Earray (len, esel, inst), Tarray (t', _, _), (Index idx) :: syn_offs' ->
+    | Sil.Earray (len, esel, inst), Tarray {elt= t'}, (Index idx) :: syn_offs' ->
         let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' idx) esel) in
         let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
         let esel' =
@@ -181,8 +181,8 @@ end = struct
               find_offset_fsel sigma_other hpred root offs fsel fields typ
           | None ->
               () )
-        | Sil.Earray (_, esel, _), Tarray (t, _, _) ->
-            find_offset_esel sigma_other hpred root offs esel t
+        | Sil.Earray (_, esel, _), Tarray {elt} ->
+            find_offset_esel sigma_other hpred root offs esel elt
         | _ ->
             ()
     and find_offset_fsel sigma_other hpred root offs fsel ftal typ =
@@ -474,7 +474,7 @@ let keep_only_indices tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (ind
 (** If the type is array, check whether we should do abstraction *)
 let array_typ_can_abstract {Typ.desc} =
   match desc with
-  | Tarray ({desc= Tptr ({desc= Tfun _}, _)}, _, _) ->
+  | Tarray {elt= {desc= Tptr ({desc= Tfun _}, _)}} ->
       false (* don't abstract arrays of pointers *)
   | _ ->
       true
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 54f5d22fe..a2863d919 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -1093,12 +1093,13 @@ and typ_partial_join (t1: Typ.t) (t2: Typ.t) =
     when Typ.equal_ptr_kind pk1 pk2 && Typ.equal_quals t1.quals t2.quals ->
       Typ.mk ~default:t1 (Tptr (typ_partial_join t1 t2, pk1))
       (* quals are the same for t1 and t2 *)
-  | Typ.Tarray (typ1, len1, stride1), Typ.Tarray (typ2, len2, stride2)
+  | ( Typ.Tarray {elt= typ1; length= len1; stride= stride1}
+    , Typ.Tarray {elt= typ2; length= len2; stride= stride2} )
     when Typ.equal_quals typ1.quals typ2.quals ->
-      let t = typ_partial_join typ1 typ2 in
-      let len = static_length_partial_join len1 len2 in
+      let elt = typ_partial_join typ1 typ2 in
+      let length = static_length_partial_join len1 len2 in
       let stride = static_length_partial_join stride1 stride2 in
-      Typ.mk ~default:t1 (Tarray (t, len, stride))
+      Typ.mk_array ~default:t1 elt ?length ?stride
       (* quals are the same for t1 and t2 *)
   | _ when Typ.equal t1 t2 ->
       t1 (* common case *)
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 737f51ed3..69fb84b47 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -337,7 +337,7 @@ let rec dotty_mk_node pe sigma =
   let n = !dotty_state_count in
   incr dotty_state_count ;
   let do_hpred_lambda exp_color = function
-    | ( Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ= {Typ.desc= Tarray (t, _, _)}})
+    | ( Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ= {Typ.desc= Tarray {elt= t}}})
       , lambda ) ->
         incr dotty_state_count ;
         (* increment once more n+1 is the box for the array *)
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index abae4ee5e..808105c1d 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -482,7 +482,7 @@ let rec create_strexp_of_type ~path tenv struct_init_mode (typ: Typ.t) len inst
           Estruct (flds, inst)
       | _ ->
           Estruct ([], inst) )
-  | Tarray (_, len_opt, _), None ->
+  | Tarray {length= len_opt}, None ->
       let len =
         match len_opt with None -> Exp.get_undefined false | Some len -> Exp.Const (Cint len)
       in
@@ -548,7 +548,7 @@ let exp_collapse_consecutive_indices_prop (typ: Typ.t) exp =
     match typ1.desc with Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ -> true | _ -> false
   in
   let typ_is_one_step_from_base =
-    match typ.desc with Tptr (t, _) | Tarray (t, _, _) -> typ_is_base t | _ -> false
+    match typ.desc with Tptr (t, _) | Tarray {elt= t} -> typ_is_base t | _ -> false
   in
   let rec exp_remove (e0: Exp.t) =
     match e0 with
@@ -674,10 +674,10 @@ module Normalize = struct
           e
       | Sizeof {nbytes= Some n} when destructive ->
           Exp.Const (Const.Cint (IntLit.of_int n))
-      | Sizeof {typ= {desc= Tarray ({desc= Tint ik}, _, _)}; dynamic_length= Some l}
+      | Sizeof {typ= {desc= Tarray {elt= {desc= Tint ik}}}; dynamic_length= Some l}
         when Typ.ikind_is_char ik && Language.curr_language_is Clang ->
           eval l
-      | Sizeof {typ= {desc= Tarray ({desc= Tint ik}, Some l, _)}}
+      | Sizeof {typ= {desc= Tarray {elt= {desc= Tint ik}; length= Some l}}}
         when Typ.ikind_is_char ik && Language.curr_language_is Clang ->
           Const (Cint l)
       | Sizeof _ ->
@@ -947,12 +947,12 @@ module Normalize = struct
               Exp.int (IntLit.div n m)
           | Const Cfloat v, Const Cfloat w ->
               Exp.float (v /. w)
-          | ( Sizeof {typ= {desc= Tarray (elt, _, _)}; dynamic_length= Some len}
+          | ( Sizeof {typ= {desc= Tarray {elt}}; dynamic_length= Some len}
             , Sizeof {typ= elt2; dynamic_length= None} )
           (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
             when Typ.equal elt elt2 ->
               len
-          | ( Sizeof {typ= {desc= Tarray (elt, Some len, _)}; dynamic_length= None}
+          | ( Sizeof {typ= {desc= Tarray {elt; length= Some len}}; dynamic_length= None}
             , Sizeof {typ= elt2; dynamic_length= None} )
           (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
             when Typ.equal elt elt2 ->
@@ -1450,20 +1450,20 @@ module Normalize = struct
             replace_hpred hpred'
         | ( Earray
               (BinOp (Mult, Sizeof {typ= t; dynamic_length= None; subtype= st1}, x), esel, inst)
-          , Sizeof {typ= {desc= Tarray (elt, _, _)} as arr} )
+          , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal t elt ->
             let dynamic_length = Some x in
             let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length; subtype= st1} in
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
         | ( Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length= None; subtype}), esel, inst)
-          , Sizeof {typ= {desc= Tarray (elt, _, _)} as arr} )
+          , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal typ elt ->
             let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length= Some x; subtype} in
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
         | ( Earray (BinOp (Mult, Sizeof {typ; dynamic_length= Some len; subtype}, x), esel, inst)
-          , Sizeof {typ= {desc= Tarray (elt, _, _)} as arr} )
+          , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal typ elt ->
             let sizeof_data =
               {Exp.typ= arr; nbytes= None; dynamic_length= Some (Exp.BinOp (Mult, x, len)); subtype}
@@ -1471,7 +1471,7 @@ module Normalize = struct
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
         | ( Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length= Some len; subtype}), esel, inst)
-          , Sizeof {typ= {desc= Tarray (elt, _, _)} as arr} )
+          , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal typ elt ->
             let sizeof_data =
               {Exp.typ= arr; nbytes= None; dynamic_length= Some (Exp.BinOp (Mult, x, len)); subtype}
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 57b7d8949..97b25d9a6 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -40,7 +40,7 @@ let rec is_java_class tenv (typ: Typ.t) =
   match typ.desc with
   | Tstruct name ->
       Typ.Name.Java.is_class name
-  | Tarray (inner_typ, _, _) | Tptr (inner_typ, _) ->
+  | Tarray {elt= inner_typ} | Tptr (inner_typ, _) ->
       is_java_class tenv inner_typ
   | _ ->
       false
@@ -454,7 +454,7 @@ end = struct
           in
           List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel
       | Sil.Earray (len, isel, _), t ->
-          let elt_t = match t with Some {Typ.desc= Tarray (t, _, _)} -> Some t | _ -> None in
+          let elt_t = match t with Some {Typ.desc= Tarray {elt}} -> Some elt | _ -> None in
           add_lt_minus1_e len ;
           List.iter
             ~f:(fun (idx, se) ->
@@ -1559,7 +1559,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2
       sexp_imply tenv source calc_index_frame calc_missing subs se1' se2 typ2
   | Sil.Earray (len, _, _), Sil.Eexp (_, inst) ->
       let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in
-      let typ2' = Typ.mk (Tarray (typ2, None, None)) in
+      let typ2' = Typ.mk_array typ2 in
       (* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2
          argument is only used by eventually passing its value to Typ.Struct.fld, Exp.Lfield,
          Typ.Struct.fld, or Typ.array_elem.  None of these are sensitive to the length field
@@ -1801,7 +1801,7 @@ let expand_hpred_pointer =
           let t' =
             match t with
             | Exp.Sizeof ({typ= t_} as sizeof_data) ->
-                Exp.Sizeof {sizeof_data with typ= Typ.mk (Tarray (t_, None, None))}
+                Exp.Sizeof {sizeof_data with typ= Typ.mk_array t_}
             | _ ->
                 L.(die InternalError) "expand_hpred_pointer: Unexpected non-sizeof type in Lindex"
           in
@@ -1847,7 +1847,7 @@ module Subtyping_check = struct
     match (t1.Typ.desc, t2.Typ.desc) with
     | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) ->
         Subtype.is_known_subtype tenv cn1 cn2
-    | Tarray (dom_type1, _, _), Tarray (dom_type2, _, _) ->
+    | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} ->
         check_subtype_java tenv dom_type1 dom_type2
     | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
         check_subtype_java tenv dom_type1 dom_type2
@@ -1887,7 +1887,7 @@ module Subtyping_check = struct
     (* and the algorithm will only work correctly if this is the case *)
       when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 ->
         Subtype.case_analysis tenv (cn1, st1) (cn2, st2)
-    | Tarray (dom_type1, _, _), Tarray (dom_type2, _, _) ->
+    | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} ->
         case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)
     | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
         case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)
@@ -2354,7 +2354,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
       match !Language.curr_language with
       | Clang ->
           Exp.Sizeof
-            { typ= Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), Some len, Some (IntLit.of_int 1)))
+            { typ= Typ.mk_array (Typ.mk (Tint Typ.IChar)) ~length:len ~stride:(IntLit.of_int 1)
             ; nbytes= None
             ; dynamic_length= None
             ; subtype= Subtype.exact }
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 28913a740..991ed3e1e 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -136,12 +136,12 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
         let e' = Sil.array_clean_new_index footprint_part e in
         let len = Exp.Var (new_id ()) in
         let se = Sil.Earray (len, [(e', se')], inst) in
-        let res_t = Typ.mk (Tarray (res_t', None, None)) in
+        let res_t = Typ.mk_array res_t' in
         (Sil.Aeq (e, e') :: atoms', se, res_t)
-    | Tarray (t', len_, stride_), off
+    | Tarray {elt= t'; length; stride}, off
       -> (
         let len =
-          match len_ with None -> Exp.Var (new_id ()) | Some len -> Exp.Const (Const.Cint len)
+          match length with None -> Exp.Var (new_id ()) | Some len -> Exp.Const (Const.Cint len)
         in
         match off with
         | [] ->
@@ -153,7 +153,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
             in
             let e' = Sil.array_clean_new_index footprint_part e in
             let se = Sil.Earray (len, [(e', se')], inst) in
-            let res_t = Typ.mk ~default:t (Tarray (res_t', len_, stride_)) in
+            let res_t = Typ.mk_array ~default:t res_t' ?length ?stride in
             (Sil.Aeq (e, e') :: atoms', se, res_t)
         | (Sil.Off_fld _) :: _ ->
             assert false )
@@ -176,7 +176,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
         in
         let e' = Sil.array_clean_new_index footprint_part e in
         let se = Sil.Earray (len, [(e', se')], inst) in
-        let res_t = mk_typ_f (Tarray (res_t', None, None)) in
+        let res_t = mk_typ_f (Tarray {elt= res_t'; length= None; stride= None}) in
         (Sil.Aeq (e, e') :: atoms', se, res_t)
     | Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ | TVar _, _ ->
         fail t off __POS__
@@ -275,10 +275,12 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
             else Exp.Var (new_id ())
       in
       let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in
-      let typ_new = Typ.mk (Tarray (typ, None, None)) in
+      let typ_new = Typ.mk_array typ in
       strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off
         inst
-  | (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ', stride)
+  | ( (Off_index e) :: off'
+    , Sil.Earray (len, esel, inst_arr)
+    , Tarray {elt= typ'; length= len_for_typ'; stride} )
     -> (
       bounds_check tenv pname orig_prop len e (State.get_loc ()) ;
       match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with
@@ -293,7 +295,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
             if Typ.equal res_typ' typ' || Int.equal (List.length res_esel') 1 then
               ( res_atoms'
               , Sil.Earray (len, res_esel', inst_arr)
-              , Typ.mk ~default:typ (Tarray (res_typ', len_for_typ', stride)) )
+              , Typ.mk_array ~default:typ res_typ' ?length:len_for_typ' ?stride )
               :: acc
             else raise (Exceptions.Bad_footprint __POS__)
           in
@@ -323,7 +325,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
   in
   if index_in_array then
     let array_default = Sil.Earray (array_len, array_cont, inst_arr) in
-    let typ_default = Typ.mk ~default:typ_array (Tarray (typ_cont, typ_array_len, None)) in
+    let typ_default = Typ.mk_array ~default:typ_array typ_cont ?length:typ_array_len in
     [([], array_default, typ_default)]
   else if !Config.footprint then
     let atoms, elem_se, elem_typ =
@@ -334,7 +336,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
       List.sort ~cmp:[%compare : Exp.t * Sil.strexp] ((index, elem_se) :: array_cont)
     in
     let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
-    let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len, None)) in
+    let typ_new = Typ.mk_array ~default:typ_array elem_typ ?length:typ_array_len in
     [(atoms, array_new, typ_new)]
   else
     let res_new =
@@ -348,7 +350,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
           List.sort ~cmp:[%compare : Exp.t * Sil.strexp] ((index, elem_se) :: array_cont)
         in
         let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
-        let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len, None)) in
+        let typ_new = Typ.mk_array ~default:typ_array elem_typ ?length:typ_array_len in
         [(atoms, array_new, typ_new)]
     in
     let rec handle_case acc isel_seen_rev = function
@@ -366,7 +368,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
                 let atoms_new = Sil.Aeq (index, i) :: atoms' in
                 let isel_new = list_rev_and_concat isel_seen_rev ((i, se') :: isel_unseen) in
                 let array_new = Sil.Earray (array_len, isel_new, inst_arr) in
-                let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len, None)) in
+                let typ_new = Typ.mk_array ~default:typ_array typ' ?length:typ_array_len in
                 (atoms_new, array_new, typ_new) :: acc' )
               ~init:[] atoms_se_typ_list
           in
@@ -1324,7 +1326,7 @@ let type_at_offset tenv texp off =
             None )
       | None ->
           None )
-    | (Off_index _) :: off', Tarray (typ', _, _) ->
+    | (Off_index _) :: off', Tarray {elt= typ'} ->
         strip_offset off' typ'
     | _ ->
         None
@@ -1390,7 +1392,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst
       | _ ->
           typ_from_instr )
     | (Sil.Off_index _) :: off ->
-        Typ.mk (Tarray (root_typ_of_offsets off, None, None))
+        Typ.mk_array (root_typ_of_offsets off)
     | _ ->
         typ_from_instr
   in
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 0a85d9dc4..8997cf337 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -40,8 +40,8 @@ let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
       try fldlist_assoc fld (fields @ statics) with Not_found -> fail Typ.Fieldname.to_string fld )
     | None ->
         fail Typ.Fieldname.to_string fld )
-  | Tarray (typ', _, _), Off_index _ ->
-      typ'
+  | Tarray {elt}, Off_index _ ->
+      elt
   | _, Off_index Const Cint i when IntLit.iszero i ->
       typ
   | _ ->
@@ -141,7 +141,9 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
   | (Sil.Off_fld _) :: _, _, _ ->
       pp_error () ;
       assert false
-  | (Sil.Off_index idx) :: offlist', Sil.Earray (len, esel, inst1), Typ.Tarray (t', len', stride')
+  | ( (Sil.Off_index idx) :: offlist'
+    , Sil.Earray (len, esel, inst1)
+    , Typ.Tarray {elt= t'; length= len'; stride= stride'} )
     -> (
       let nidx = Prop.exp_normalize_prop tenv p idx in
       match List.find ~f:(fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel with
@@ -154,7 +156,7 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
             if Exp.equal idx_ese' (fst ese) then (idx_ese', res_se') else ese
           in
           let res_se = Sil.Earray (len, List.map ~f:replace_ese esel, inst1) in
-          let res_t = Typ.mk ~default:typ (Tarray (res_t', len', stride')) in
+          let res_t = Typ.mk_array ~default:typ res_t' ?length:len' ?stride:stride' in
           (res_e', res_se, res_t, res_pred_insts_op')
       | None ->
           (* return a nondeterministic value if the index is not found after rearrangement *)
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 22a9d2507..1289c3cb2 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -66,18 +66,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               BoUtils.Exec.decl_sym_arr
                 ~decl_sym_val:(decl_sym_val ~is_last_field:false)
                 pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
-          | Typ.Tarray (typ, opt_int_lit, _) ->
+          | Typ.Tarray {elt; length} ->
               let size =
-                match opt_int_lit with
-                | Some int_lit when is_last_field && (IntLit.iszero int_lit || IntLit.isone int_lit) ->
+                match length with
+                | Some length when is_last_field && (IntLit.iszero length || IntLit.isone length) ->
                     Some (Itv.make_sym pname new_sym_num)
                 | _ ->
-                    Option.map ~f:Itv.of_int_lit opt_int_lit
+                    Option.map ~f:Itv.of_int_lit length
               in
               let offset = Itv.zero in
               BoUtils.Exec.decl_sym_arr
                 ~decl_sym_val:(decl_sym_val ~is_last_field:false)
-                pname tenv node location ~depth loc typ ~offset ?size ~inst_num ~new_sym_num
+                pname tenv node location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num
                 ~new_alloc_num mem
           | Typ.Tstruct typename -> (
             match Models.TypName.dispatch typename with
@@ -257,8 +257,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             (* array allocation in stack e.g., int arr[10] *)
             let rec decl_local pname node location loc typ ~inst_num ~dimension mem =
               match typ.Typ.desc with
-              | Typ.Tarray (typ, length, stride0) ->
-                  let stride = Option.map ~f:IntLit.to_int stride0 in
+              | Typ.Tarray {elt= typ; length; stride} ->
+                  let stride = Option.map ~f:IntLit.to_int stride in
                   BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length
                     ?stride ~inst_num ~dimension mem
               | Typ.Tstruct typname -> (
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 99f8e1076..5c23057d0 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -177,12 +177,12 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
   let set_array_length array length_exp =
     let exec {pname; node} mem =
       match array with
-      | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)} ->
+      | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
           let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
-          let stride = Option.map ~f:IntLit.to_int stride0 in
-          let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in
+          let stride = Option.map ~f:IntLit.to_int stride in
+          let v = Sem.eval_array_alloc pname node elt ?stride Itv.zero length 0 1 in
           mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
-          |> set_uninitialized node typ (Dom.Val.get_array_locs v)
+          |> set_uninitialized node elt (Dom.Val.get_array_locs v)
       | _ ->
           L.(die InternalError) "Unexpected type of first argument for __set_array_length()"
     and check = check_alloc_size length_exp in
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 577f96a86..316647524 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -68,10 +68,10 @@ module Make (CFG : ProcCfg.S) = struct
         4
     | Typ.Tstruct _ | Typ.TVar _ ->
         4 (* TODO *)
-    | Typ.Tarray (_, Some length, Some stride) ->
+    | Typ.Tarray {length= Some length; stride= Some stride} ->
         IntLit.to_int stride * IntLit.to_int length
-    | Typ.Tarray (typ, Some length, None) ->
-        sizeof typ * IntLit.to_int length
+    | Typ.Tarray {elt; length= Some length; stride= None} ->
+        sizeof elt * IntLit.to_int length
     | _ ->
         4
 
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index 3bfafc37a..0d9493421 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -136,7 +136,7 @@ module Make (CFG : ProcCfg.S) = struct
         let field_loc = PowLoc.append_field locs ~fn:field_name in
         let mem =
           match field_typ.Typ.desc with
-          | Tarray (typ, Some length, stride) ->
+          | Tarray {elt= typ; length= Some length; stride} ->
               let length = Itv.of_int_lit length in
               let length =
                 Option.value_map dyn_length ~default:length ~f:(fun dyn_length ->
diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml
index 76ae24367..7af372c61 100644
--- a/infer/src/checkers/uninit.ml
+++ b/infer/src/checkers/uninit.ml
@@ -296,8 +296,8 @@ let get_locals cfg tenv pdesc =
                                     to the fields one level down *)
         | _ ->
             acc )
-      | Typ.Tarray (t', _, _) ->
-          (fst base_ap, [AccessPath.ArrayAccess (t', [])]) :: acc
+      | Typ.Tarray {elt} ->
+          (fst base_ap, [AccessPath.ArrayAccess (elt, [])]) :: acc
       | _ ->
           base_ap :: acc )
     ~init:[] (Procdesc.get_locals cfg)
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index ba90a1ff1..467a13587 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -403,7 +403,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
                     assert false
               in
               List.map ~f:fill_typ_with_zero field_exps |> flatten_res_trans
-          | Tarray (field_typ, Some n, _) ->
+          | Tarray {elt= field_typ; length= Some n} ->
               let size = IntLit.to_int n in
               let indices = CGeneral_utils.list_range 0 (size - 1) in
               List.map indices ~f:(fun i ->
@@ -2142,8 +2142,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
       in
       let all_res_trans =
         match var_typ.Typ.desc with
-        | Typ.Tarray (typ_inside, _, _) ->
-            initListExpr_array_trans trans_state_pri init_stmt_info stmts var_exp typ_inside
+        | Typ.Tarray {elt} ->
+            initListExpr_array_trans trans_state_pri init_stmt_info stmts var_exp elt
         | Tstruct _ ->
             initListExpr_struct_trans trans_state_pri init_stmt_info stmts var_exp var_typ
         | Tint _ | Tfloat _ | Tptr _ ->
@@ -2740,7 +2740,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
       match res_trans_new.exps with
       | [(var_exp, ({desc= Tptr (t, _)} as var_typ))] when is_dyn_array ->
           (* represent dynamic array as Tarray *)
-          (var_exp, Typ.mk ~default:var_typ (Typ.Tarray (t, None, None)))
+          (var_exp, Typ.mk_array ~default:var_typ t)
       | [(var_exp, {desc= Tptr (t, _)})] when not is_dyn_array ->
           (var_exp, t)
       | _ ->
diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml
index fd542dd3f..4be87c331 100644
--- a/infer/src/clang/cType_to_sil_type.ml
+++ b/infer/src/clang/cType_to_sil_type.ml
@@ -92,7 +92,7 @@ let rec build_array_type translate_decl tenv (qual_type: Clang_ast_t.qual_type)
   let array_type = qual_type_to_sil_type translate_decl tenv qual_type in
   let length = Option.map ~f:IntLit.of_int length_opt in
   let stride = Option.map ~f:IntLit.of_int stride_opt in
-  Typ.Tarray (array_type, length, stride)
+  Typ.Tarray {elt= array_type; length; stride}
 
 and type_desc_of_attr_type translate_decl tenv type_info attr_info =
   match type_info.Clang_ast_t.ti_desugared_type with
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 5c04b654c..eb461d4b3 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -545,7 +545,7 @@ let rec expression (context: JContext.t) pc expr =
       match binop with
       | JBir.ArrayLoad _ ->
           (* add an instruction that dereferences the array *)
-          let array_typ = Typ.mk (Tarray (type_of_expr, None, None)) in
+          let array_typ = Typ.mk_array type_of_expr in
           let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
           let id = Ident.create_fresh Ident.knormal in
           let load_instr = Sil.Load (id, Exp.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in
@@ -739,7 +739,7 @@ let get_array_length context pc expr_list content_type =
   in
   let instrs, sil_len_exprs = List.fold_right ~f:get_expr_instr expr_list ~init:([], []) in
   let get_array_type_len sil_len_expr (content_type, _) =
-    (Typ.mk (Tarray (content_type, None, None)), Some sil_len_expr)
+    (Typ.mk_array content_type, Some sil_len_expr)
   in
   let array_type, array_len =
     List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None)
diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml
index 4a0c0b6eb..a1f3f3e11 100644
--- a/infer/src/java/jTransType.ml
+++ b/infer/src/java/jTransType.ml
@@ -81,7 +81,7 @@ let rec get_named_type vt : Typ.t =
     match ot with
     | JBasics.TArray vt ->
         let content_type = get_named_type vt in
-        Typ.mk (Tptr (Typ.mk (Tarray (content_type, None, None)), Typ.Pk_pointer))
+        Typ.mk (Tptr (Typ.mk_array content_type, Typ.Pk_pointer))
     | JBasics.TClass cn ->
         Typ.mk (Tptr (Typ.mk (Tstruct (typename_of_classname cn)), Typ.Pk_pointer))
 
@@ -89,7 +89,7 @@ let rec get_named_type vt : Typ.t =
 let rec create_array_type typ dim =
   if dim > 0 then
     let content_typ = create_array_type typ (dim - 1) in
-    Typ.mk (Tptr (Typ.mk (Tarray (content_typ, None, None)), Typ.Pk_pointer))
+    Typ.mk (Tptr (Typ.mk_array content_typ, Typ.Pk_pointer))
   else typ
 
 
@@ -412,7 +412,7 @@ let rec object_type program tenv ot =
   | JBasics.TClass cn ->
       get_class_type program tenv cn
   | JBasics.TArray at ->
-      Typ.mk (Tptr (Typ.mk (Tarray (value_type program tenv at, None, None)), Typ.Pk_pointer))
+      Typ.mk (Tptr (Typ.mk_array (value_type program tenv at), Typ.Pk_pointer))
 
 
 (** translate a value type *)
@@ -456,11 +456,7 @@ let get_var_type context var =
 
 
 let extract_array_type typ =
-  match typ.Typ.desc with
-  | Typ.Tptr ({desc= Tarray (vtyp, _, _)}, Typ.Pk_pointer) ->
-      vtyp
-  | _ ->
-      typ
+  match typ.Typ.desc with Typ.Tptr ({desc= Tarray {elt}}, Typ.Pk_pointer) -> elt | _ -> typ
 
 
 (** translate the type of an expression, looking in the method signature for formal parameters
diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml
index 71995d252..866e91913 100644
--- a/infer/src/unit/accessPathTests.ml
+++ b/infer/src/unit/accessPathTests.ml
@@ -21,7 +21,7 @@ let tests =
   let yF = make_access_path "y" ["f"] in
   let xArr =
     let dummy_typ = Typ.mk Tvoid in
-    let dummy_arr_typ = Typ.mk (Tarray (dummy_typ, None, None)) in
+    let dummy_arr_typ = Typ.mk_array dummy_typ in
     let base = make_base "x" ~typ:dummy_arr_typ in
     (base, [make_array_access dummy_typ])
   in