From 10a111d41b9aa3a4d4881cb9112a8051e252690a Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Thu, 28 May 2020 06:12:01 -0700
Subject: [PATCH] [inferbo] Refactor domain constructors for field

Summary:
In inferbo's domain, `Loc.t` and `Symb.SymbolPath.partial` are defined with the same *field abstraction*.  The depth of appended fields were limited in both of them exactly in the same way, e.g. `x.*.field`. Problem is that the implementation related
to the field abstraction are duplicated in their code, which had been synchronized manually. This diff avoids the duplication by adding a `BufferOverrunField.t`.

Reviewed By: ezgicicek

Differential Revision: D21743728

fbshipit-source-id: 4b01d027c
---
 infer/src/bufferoverrun/absLoc.ml             | 265 ++++++++----------
 infer/src/bufferoverrun/absLoc.mli            |  14 +-
 infer/src/bufferoverrun/arrayBlk.ml           |  12 +-
 .../bufferoverrun/bufferOverrunAnalysis.ml    |   4 +-
 .../src/bufferoverrun/bufferOverrunDomain.ml  |  13 +-
 infer/src/bufferoverrun/bufferOverrunField.ml |  52 ++++
 .../src/bufferoverrun/bufferOverrunField.mli  |  39 +++
 .../src/bufferoverrun/bufferOverrunModels.ml  |  11 +-
 .../bufferoverrun/bufferOverrunOndemandEnv.ml |  21 +-
 .../bufferoverrun/bufferOverrunSemantics.ml   |  17 +-
 infer/src/bufferoverrun/bufferOverrunUtils.ml |   4 +-
 infer/src/bufferoverrun/symb.ml               | 189 +++++--------
 infer/src/bufferoverrun/symb.mli              |  20 +-
 infer/src/cost/boundMap.ml                    |   4 +-
 infer/src/cost/costDomain.ml                  |   2 +-
 infer/src/cost/costModels.ml                  |   2 +-
 16 files changed, 348 insertions(+), 321 deletions(-)

diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml
index f89e8c0b3..015798c42 100644
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@@ -9,6 +9,7 @@
 
 open! IStd
 module F = Format
+module BoField = BufferOverrunField
 
 module Allocsite = struct
   type t =
@@ -125,121 +126,86 @@ module Allocsite = struct
 end
 
 module Loc = struct
-  type field_typ = Typ.t option
-
-  let compare_field_typ _ _ = 0
-
-  include (* Enforce invariants on Field and StarField, see Symb.mli *) (
-    struct
-      type t =
-        | Var of Var.t
-        | Allocsite of Allocsite.t
-        | Field of {prefix: t; fn: Fieldname.t; typ: field_typ}
-        | StarField of {prefix: t; last_field: Fieldname.t}
-      [@@deriving compare]
-
-      let of_var v = Var v
-
-      let of_allocsite a = Allocsite a
-
-      let append_star_field l0 ~fn =
-        let rec aux l =
-          match l with
-          | Allocsite a when Allocsite.is_unknown a ->
-              l
-          | Var _ | Allocsite _ ->
-              StarField {prefix= l0; last_field= fn}
-          | StarField {last_field} when Fieldname.equal fn last_field ->
-              l
-          | StarField {prefix} ->
-              StarField {prefix; last_field= fn}
-          | Field {prefix= l} ->
-              aux l
-        in
-        aux l0
-
-
-      let append_field ?typ l0 ~fn =
-        let rec aux ~depth l =
-          if Symb.SymbolPath.is_field_depth_beyond_limit depth then append_star_field l0 ~fn
-          else
-            match l with
-            | Allocsite a when Allocsite.is_unknown a ->
-                l
-            | Var _ | Allocsite _ ->
-                Field {prefix= l0; fn; typ}
-            | StarField {last_field} as l when Fieldname.equal fn last_field ->
-                l
-            | StarField {prefix} ->
-                StarField {prefix; last_field= fn}
-            | Field {fn= fn'} when Fieldname.equal fn fn' ->
-                StarField {prefix= l0; last_field= fn}
-            | Field {prefix= l} ->
-                aux ~depth:(depth + 1) l
-        in
-        aux ~depth:0 l0
-    end :
-      sig
-        type t = private
-          | Var of Var.t
-          | Allocsite of Allocsite.t
-          | Field of {prefix: t; fn: Fieldname.t; typ: field_typ}
-          | StarField of {prefix: t; last_field: Fieldname.t}
-        [@@deriving compare]
-
-        val of_var : Var.t -> t
-
-        val of_allocsite : Allocsite.t -> t
-
-        val append_field : ?typ:Typ.t -> t -> fn:Fieldname.t -> t
-
-        val append_star_field : t -> fn:Fieldname.t -> t
-      end )
+  type prim = Var of Var.t | Allocsite of Allocsite.t [@@deriving compare]
+
+  type t = prim BoField.t [@@deriving compare]
+
+  let of_var v = BoField.Prim (Var v)
+
+  let of_allocsite a = BoField.Prim (Allocsite a)
+
+  let prim_append_field ?typ l0 fn _aux _depth = function
+    | Allocsite a as l when Allocsite.is_unknown a ->
+        BoField.Prim l
+    | Var _ | Allocsite _ ->
+        BoField.Field {prefix= l0; fn; typ}
+
+
+  let prim_append_star_field l0 fn _aux = function
+    | Allocsite a as l when Allocsite.is_unknown a ->
+        BoField.Prim l
+    | Var _ | Allocsite _ ->
+        BoField.StarField {prefix= l0; last_field= fn}
+
+
+  let append_field = BoField.mk_append_field ~prim_append_field ~prim_append_star_field
+
+  let append_star_field = BoField.mk_append_star_field ~prim_append_star_field
 
   let equal = [%compare.equal: t]
 
   let eq l1 l2 =
-    match (l1, l2) with Allocsite as1, Allocsite as2 -> Allocsite.eq as1 as2 | _ -> Boolean.Top
+    match (l1, l2) with
+    | BoField.Prim (Allocsite as1), BoField.Prim (Allocsite as2) ->
+        Allocsite.eq as1 as2
+    | _ ->
+        Boolean.Top
 
 
   let unknown = of_allocsite Allocsite.unknown
 
   let rec is_unknown = function
-    | Var _ ->
+    | BoField.Prim (Var _) ->
         false
-    | Allocsite a ->
+    | BoField.Prim (Allocsite a) ->
         Allocsite.is_unknown a
-    | Field {prefix= x} | StarField {prefix= x} ->
+    | BoField.(Field {prefix= x} | StarField {prefix= x}) ->
         is_unknown x
 
 
   let rec pp_paren ~paren fmt =
     let module SP = Symb.SymbolPath in
     function
-    | Var v ->
+    | BoField.Prim (Var v) ->
         Var.pp F.str_formatter v ;
         let s = F.flush_str_formatter () in
         if Char.equal s.[0] '&' then
           F.pp_print_string fmt (String.sub s ~pos:1 ~len:(String.length s - 1))
         else F.pp_print_string fmt s
-    | Allocsite a ->
+    | BoField.Prim (Allocsite a) ->
         Allocsite.pp_paren ~paren fmt a
-    | Field
+    | BoField.Field
         { prefix=
-            Allocsite
-              (Allocsite.Symbol (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p)))
+            Prim
+              (Allocsite
+                (Allocsite.Symbol
+                  (BoField.Prim (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p)))))
         ; fn= f }
-    | Field
+    | BoField.Field
         { prefix=
-            Allocsite
-              (Allocsite.Known
-                {path= Some (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p))})
+            Prim
+              (Allocsite
+                (Allocsite.Known
+                  { path=
+                      Some
+                        (BoField.Prim
+                          (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p))) }))
         ; fn= f } ->
-        BufferOverrunField.pp ~pp_lhs:(SP.pp_partial_paren ~paren:true) ~sep:"->" fmt p f
-    | Field {prefix= l; fn= f} ->
-        BufferOverrunField.pp ~pp_lhs:(pp_paren ~paren:true) ~sep:"." fmt l f
-    | StarField {prefix; last_field} ->
-        BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
+        BoField.pp ~pp_lhs:(SP.pp_partial_paren ~paren:true) ~sep:"->" fmt p f
+    | BoField.Field {prefix= l; fn= f} ->
+        BoField.pp ~pp_lhs:(pp_paren ~paren:true) ~sep:"." fmt l f
+    | BoField.StarField {prefix; last_field} ->
+        BoField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
 
 
   and pp_star ~paren fmt l =
@@ -249,34 +215,39 @@ module Loc = struct
 
   let pp = pp_paren ~paren:false
 
-  let is_var = function Var _ -> true | _ -> false
+  let is_var = function BoField.Prim (Var _) -> true | _ -> false
 
   let is_c_strlen = function
-    | Field {fn} ->
-        Fieldname.equal fn (BufferOverrunField.c_strlen ())
+    | BoField.Field {fn} ->
+        Fieldname.equal fn (BoField.c_strlen ())
     | _ ->
         false
 
 
   let is_java_collection_internal_array = function
-    | Field {fn} ->
-        Fieldname.equal fn BufferOverrunField.java_collection_internal_array
+    | BoField.Field {fn} ->
+        Fieldname.equal fn BoField.java_collection_internal_array
     | _ ->
         false
 
 
-  let is_frontend_tmp = function Var x -> not (Var.appears_in_source_code x) | _ -> false
+  let is_frontend_tmp = function
+    | BoField.Prim (Var x) ->
+        not (Var.appears_in_source_code x)
+    | _ ->
+        false
+
 
   let rec is_pretty = function
-    | Var _ ->
+    | BoField.Prim (Var _) ->
         true
-    | Allocsite a ->
+    | BoField.Prim (Allocsite a) ->
         Allocsite.is_pretty a
-    | Field {prefix= loc} | StarField {prefix= loc} ->
+    | BoField.Field {prefix= loc} | StarField {prefix= loc} ->
         is_pretty loc
 
 
-  let of_c_strlen loc = append_field loc ~fn:(BufferOverrunField.c_strlen ())
+  let of_c_strlen loc = append_field loc (BoField.c_strlen ())
 
   let of_pvar pvar = of_var (Var.of_pvar pvar)
 
@@ -284,42 +255,51 @@ module Loc = struct
 
   let rec of_path path =
     match path with
-    | Symb.SymbolPath.Pvar pvar ->
+    | BoField.Prim (Symb.SymbolPath.Pvar pvar) ->
         of_pvar pvar
-    | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _ ->
+    | BoField.Prim (Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _) ->
         of_allocsite (Allocsite.make_symbol path)
-    | Symb.SymbolPath.Field {fn; prefix= path} ->
-        append_field (of_path path) ~fn
-    | Symb.SymbolPath.StarField {last_field= fn; prefix} ->
-        append_star_field (of_path prefix) ~fn
+    | BoField.Field {fn; prefix= path} ->
+        append_field (of_path path) fn
+    | BoField.StarField {last_field= fn; prefix} ->
+        append_star_field (of_path prefix) fn
 
 
   let is_return = function
-    | Var (Var.ProgramVar x) ->
+    | BoField.Prim (Var (Var.ProgramVar x)) ->
         Mangled.equal (Pvar.get_name x) Ident.name_return
     | _ ->
         false
 
 
   let is_field_of ~loc ~field_loc =
-    match field_loc with Field {prefix= l} | StarField {prefix= l} -> equal loc l | _ -> false
+    match field_loc with
+    | BoField.(Field {prefix= l} | StarField {prefix= l}) ->
+        equal loc l
+    | _ ->
+        false
+
 
+  let get_literal_string = function
+    | BoField.Prim (Allocsite a) ->
+        Allocsite.get_literal_string a
+    | _ ->
+        None
 
-  let get_literal_string = function Allocsite a -> Allocsite.get_literal_string a | _ -> None
 
   let get_literal_string_strlen = function
-    | Field {prefix= l; fn} when Fieldname.equal (BufferOverrunField.c_strlen ()) fn ->
+    | BoField.Field {prefix= l; fn} when Fieldname.equal (BoField.c_strlen ()) fn ->
         get_literal_string l
     | _ ->
         None
 
 
   let rec is_global = function
-    | Var (Var.ProgramVar pvar) ->
+    | BoField.Prim (Var (Var.ProgramVar pvar)) ->
         Pvar.is_global pvar
-    | Var (Var.LogicalVar _) | Allocsite _ ->
+    | BoField.Prim (Var (Var.LogicalVar _) | Allocsite _) ->
         false
-    | Field {prefix= loc} | StarField {prefix= loc} ->
+    | BoField.(Field {prefix= loc} | StarField {prefix= loc}) ->
         is_global loc
 
 
@@ -328,63 +308,64 @@ module Loc = struct
       if Pvar.is_constant_array pvar then Pvar.get_initializer_pname pvar else None
     in
     function
-    | Var (Var.ProgramVar pvar) ->
+    | BoField.Prim (Var (Var.ProgramVar pvar)) ->
         initializer_of_pvar pvar
-    | Var (Var.LogicalVar _) ->
+    | BoField.Prim (Var (Var.LogicalVar _)) ->
         None
-    | Allocsite allocsite ->
+    | BoField.Prim (Allocsite allocsite) ->
         Allocsite.get_path allocsite
         |> Option.bind ~f:Symb.SymbolPath.get_pvar
         |> Option.bind ~f:initializer_of_pvar
-    | Field {prefix= loc} | StarField {prefix= loc} ->
+    | BoField.(Field {prefix= loc} | StarField {prefix= loc}) ->
         get_global_array_initializer loc
 
 
   let rec get_path = function
-    | Var (LogicalVar _) ->
+    | BoField.Prim (Var (LogicalVar _)) ->
         None
-    | Var (ProgramVar pvar) ->
+    | BoField.Prim (Var (ProgramVar pvar)) ->
         Some (Symb.SymbolPath.of_pvar pvar)
-    | Allocsite allocsite ->
+    | BoField.Prim (Allocsite allocsite) ->
         Allocsite.get_path allocsite
-    | Field {prefix= l; fn; typ} ->
-        Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field ?typ p fn)
-    | StarField {prefix; last_field} ->
-        get_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field)
+    | BoField.Field {prefix= l; fn; typ} ->
+        Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.append_field ?typ p fn)
+    | BoField.StarField {prefix; last_field} ->
+        get_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.append_star_field p last_field)
 
 
   let rec get_param_path = function
-    | Var _ ->
+    | BoField.Prim (Var _) ->
         None
-    | Allocsite allocsite ->
+    | BoField.Prim (Allocsite allocsite) ->
         Allocsite.get_param_path allocsite
-    | Field {prefix= l; fn} ->
-        Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
-    | StarField {prefix; last_field} ->
-        get_param_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field)
+    | BoField.Field {prefix= l; fn} ->
+        Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.append_field p fn)
+    | BoField.StarField {prefix; last_field} ->
+        get_param_path prefix
+        |> Option.map ~f:(fun p -> Symb.SymbolPath.append_star_field p last_field)
 
 
   let rec represents_multiple_values = function
-    | Var _ ->
+    | BoField.Prim (Var _) ->
         false
-    | Allocsite allocsite ->
+    | BoField.Prim (Allocsite allocsite) ->
         Allocsite.represents_multiple_values allocsite
-    | Field _ as x when is_c_strlen x || is_java_collection_internal_array x ->
+    | BoField.Field _ as x when is_c_strlen x || is_java_collection_internal_array x ->
         false
-    | Field {prefix= l} ->
+    | BoField.Field {prefix= l} ->
         represents_multiple_values l
-    | StarField _ ->
+    | BoField.StarField _ ->
         true
 
 
   let rec exists_pvar ~f = function
-    | Var (LogicalVar _) ->
+    | BoField.Prim (Var (LogicalVar _)) ->
         false
-    | Var (ProgramVar pvar) ->
+    | BoField.Prim (Var (ProgramVar pvar)) ->
         f pvar
-    | Allocsite allocsite ->
+    | BoField.Prim (Allocsite allocsite) ->
         Allocsite.exists_pvar ~f allocsite
-    | Field {prefix= l} | StarField {prefix= l} ->
+    | BoField.(Field {prefix= l} | StarField {prefix= l}) ->
         exists_pvar ~f l
 
 
@@ -394,9 +375,9 @@ module Loc = struct
 
   let cast typ x =
     match x with
-    | Field {prefix= l; fn} ->
-        append_field l ~fn ~typ
-    | StarField _ | Var _ | Allocsite _ ->
+    | BoField.Field {prefix= l; fn} ->
+        append_field l fn ~typ
+    | BoField.(StarField _ | Prim (Var _ | Allocsite _)) ->
         x
 end
 
@@ -546,7 +527,7 @@ module PowLoc = struct
     | Unknown ->
         Unknown
     | Known ploc ->
-        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_field l ~fn)) ploc LocSet.empty)
+        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_field l fn)) ploc LocSet.empty)
 
 
   let append_star_field ploc ~fn =
@@ -557,7 +538,7 @@ module PowLoc = struct
     | Unknown ->
         Unknown
     | Known ploc ->
-        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_star_field l ~fn)) ploc LocSet.empty)
+        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_star_field l fn)) ploc LocSet.empty)
 
 
   let lift_cmp cmp_loc ploc1 ploc2 =
diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli
index c638c50ac..bfdf76c99 100644
--- a/infer/src/bufferoverrun/absLoc.mli
+++ b/infer/src/bufferoverrun/absLoc.mli
@@ -43,17 +43,9 @@ module Allocsite : sig
 end
 
 module Loc : sig
-  type field_typ
+  type prim = private Var of Var.t | Allocsite of Allocsite.t [@@deriving compare]
 
-  type t = private
-    | Var of Var.t  (** abstract location of variable *)
-    | Allocsite of Allocsite.t  (** abstract location of allocsites *)
-    | Field of {prefix: t; fn: Fieldname.t; typ: field_typ}
-        (** field appended abstract locations, i.e., [prefix.fn] *)
-    | StarField of {prefix: t; last_field: Fieldname.t}
-        (** field appended abstract locations, but some of intermediate fields are abstracted, i.e.,
-            [prefix.*.fn] *)
-  [@@deriving equal]
+  type t = prim BufferOverrunField.t [@@deriving compare, equal]
 
   include PrettyPrintable.PrintableOrderedType with type t := t
 
@@ -104,7 +96,7 @@ module Loc : sig
 
   val represents_multiple_values : t -> bool
 
-  val append_field : ?typ:Typ.typ -> t -> fn:Fieldname.t -> t
+  val append_field : ?typ:Typ.typ -> t -> Fieldname.t -> t
   (** It appends field. [typ] is the type of [fn]. *)
 end
 
diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index b67459a29..873e5ed07 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/infer/src/bufferoverrun/arrayBlk.ml
@@ -10,6 +10,7 @@
 open! IStd
 open AbsLoc
 open! AbstractDomain.Types
+module BoField = BufferOverrunField
 module Bound = Bounds.Bound
 module F = Format
 module L = Logging
@@ -136,9 +137,9 @@ module ArrInfo = struct
   let is_pointer : Symb.SymbolPath.partial -> t -> bool =
    fun path arr ->
     match (path, arr) with
-    | Deref ((Deref_COneValuePointer | Deref_CPointer), path), C {offset; size} ->
+    | BoField.Prim (Deref ((Deref_COneValuePointer | Deref_CPointer), path)), C {offset; size} ->
         Itv.is_offset_path_of path offset && Itv.is_length_path_of path size
-    | Deref (Deref_JavaPointer, path), Java {length} ->
+    | BoField.Prim (Deref (Deref_JavaPointer, path)), Java {length} ->
         Itv.is_length_path_of path length
     | _, _ ->
         false
@@ -274,7 +275,7 @@ module ArrInfo = struct
 
   let is_symbolic_length_of_path path info =
     match (path, info) with
-    | Symb.SymbolPath.Deref (_, prefix), Java {length} ->
+    | BoField.Prim (Symb.SymbolPath.Deref (_, prefix)), Java {length} ->
         Itv.is_length_path_of prefix length
     | _ ->
         false
@@ -341,11 +342,12 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> PowLoc.t * t =
         let locs = eval_locpath path in
         let add_allocsite l (powloc_acc, acc) =
           match l with
-          | Loc.Allocsite (Symbol (Symb.SymbolPath.Deref (_, prefix)) as a)
+          | BoField.Prim
+              (Loc.Allocsite (Symbol (BoField.Prim (Symb.SymbolPath.Deref (_, prefix))) as a))
             when ArrInfo.is_symbolic_length_of_path path info ->
               let length = Itv.of_length_path ~is_void:false prefix in
               (powloc_acc, add a (ArrInfo.make_java ~length) acc)
-          | Loc.Allocsite a ->
+          | BoField.Prim (Loc.Allocsite a) ->
               (powloc_acc, add a info' acc)
           | _ ->
               if ArrInfo.is_pointer path info then (PowLoc.add l powloc_acc, acc)
diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
index a58299bae..a22f7c34e 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
+++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
@@ -196,7 +196,7 @@ module TransferFunctions = struct
                 Loc.of_var (Var.of_pvar (Pvar.mk_global class_mangled))
               in
               let fn = Fieldname.make typename "$VALUES" in
-              Loc.append_field class_var ~fn
+              Loc.append_field class_var fn
             in
             let v = Dom.Mem.find loc clinit_mem in
             let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
@@ -229,7 +229,7 @@ module TransferFunctions = struct
         ~f:(fun (clinit_pname, pvar, fn, field_typ) ->
           let copy_from_class_init () =
             Option.value_map (get_summary clinit_pname) ~default:mem ~f:(fun clinit_mem ->
-                let field_loc = Loc.append_field ~typ:field_typ (Loc.of_pvar pvar) ~fn in
+                let field_loc = Loc.append_field ~typ:field_typ (Loc.of_pvar pvar) fn in
                 copy_reachable_locs_from field_loc ~from_mem:clinit_mem ~to_mem:mem )
           in
           match field_typ.Typ.desc with
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index c60a87f38..88f012c80 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -10,6 +10,7 @@
 open! IStd
 open AbsLoc
 open! AbstractDomain.Types
+module BoField = BufferOverrunField
 module F = Format
 module L = Logging
 module OndemandEnv = BufferOverrunOndemandEnv
@@ -1874,7 +1875,7 @@ module LatestPrune = struct
       match PowLoc.is_singleton_or_more (PowLoc.subst_loc (Loc.of_pvar x) eval_locpath) with
       | Empty ->
           Error `SubstBottom
-      | Singleton (Loc.Var (Var.ProgramVar x')) ->
+      | Singleton (BoField.Prim (Loc.Var (Var.ProgramVar x'))) ->
           Ok x'
       | Singleton _ | More ->
           Error `SubstFail
@@ -2235,7 +2236,7 @@ module MemReach = struct
             Some v1
           in
           let apply_simple_alias1 ((m_acc, prunes_acc) as acc) = function
-            | Loc.Var (Var.ProgramVar y), i when Pvar.equal x y && IntLit.iszero i ->
+            | BoField.Prim (Loc.Var (Var.ProgramVar y)), i when Pvar.equal x y && IntLit.iszero i ->
                 (apply_prunes prunes m_acc, PrunePairs.union pruned_val_meet prunes_acc prunes)
             | _ ->
                 acc
@@ -2259,7 +2260,7 @@ module MemReach = struct
         let tgts = Alias.find_ret m.alias in
         let replace_latest_prune l tgt acc =
           match (l, tgt) with
-          | Loc.Var (ProgramVar pvar), AliasTarget.Simple {i} when IntLit.iszero i ->
+          | BoField.Prim (Loc.Var (ProgramVar pvar)), AliasTarget.Simple {i} when IntLit.iszero i ->
               {acc with latest_prune= LatestPrune.replace ~from:pvar ~to_:return m.latest_prune}
           | _ ->
               acc
@@ -2606,7 +2607,11 @@ module Mem = struct
 
   let get_c_strlen locs m =
     let get_c_strlen' loc acc =
-      match loc with Loc.Allocsite _ -> Val.join acc (find (Loc.of_c_strlen loc) m) | _ -> acc
+      match loc with
+      | BoField.Prim (Loc.Allocsite _) ->
+          Val.join acc (find (Loc.of_c_strlen loc) m)
+      | _ ->
+          acc
     in
     PowLoc.fold get_c_strlen' locs Val.bot
 
diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml
index 4ad4c03e8..807820dc8 100644
--- a/infer/src/bufferoverrun/bufferOverrunField.ml
+++ b/infer/src/bufferoverrun/bufferOverrunField.ml
@@ -56,3 +56,55 @@ let cpp_vector_elem ~vec_typ ~elt_typ =
 
 
 let is_cpp_vector_elem fn = String.equal (Fieldname.to_simplified_string fn) cpp_vector_elem_str
+
+(** Field domain constructor *)
+
+type field_typ = Typ.t option
+
+let compare_field_typ _ _ = 0
+
+type 'prim t =
+  | Prim of 'prim
+  | Field of {prefix: 'prim t; fn: Fieldname.t; typ: field_typ}
+  | StarField of {prefix: 'prim t; last_field: Fieldname.t}
+[@@deriving compare]
+
+let is_field_depth_beyond_limit =
+  match Config.bo_field_depth_limit with
+  | None ->
+      fun _depth -> false
+  | Some limit ->
+      fun depth -> depth > limit
+
+
+let mk_append_star_field ~prim_append_star_field p0 fn =
+  let rec aux = function
+    | Prim prim ->
+        prim_append_star_field p0 fn aux prim
+    | Field {prefix= p} ->
+        aux p
+    | StarField {last_field} as p when Fieldname.equal fn last_field ->
+        p
+    | StarField {prefix} ->
+        StarField {last_field= fn; prefix}
+  in
+  aux p0
+
+
+let mk_append_field ~prim_append_field ~prim_append_star_field ?typ p0 fn =
+  let rec aux ~depth p =
+    if is_field_depth_beyond_limit depth then mk_append_star_field ~prim_append_star_field p0 fn
+    else
+      match p with
+      | Prim prim ->
+          prim_append_field ?typ p0 fn aux depth prim
+      | Field {fn= fn'} when Fieldname.equal fn fn' ->
+          StarField {last_field= fn; prefix= p0}
+      | Field {prefix= p} ->
+          aux ~depth:(depth + 1) p
+      | StarField {last_field} as p when Fieldname.equal fn last_field ->
+          p
+      | StarField {prefix} ->
+          StarField {prefix; last_field= fn}
+  in
+  aux ~depth:0 p0
diff --git a/infer/src/bufferoverrun/bufferOverrunField.mli b/infer/src/bufferoverrun/bufferOverrunField.mli
index fbdcc3c7e..3bdd0c8b5 100644
--- a/infer/src/bufferoverrun/bufferOverrunField.mli
+++ b/infer/src/bufferoverrun/bufferOverrunField.mli
@@ -6,6 +6,8 @@
  *)
 open! IStd
 
+(** {2 Inferbo-specific constant field names} *)
+
 val pp :
      pp_lhs:(Format.formatter -> 'a -> unit)
   -> sep:string
@@ -32,3 +34,40 @@ val is_cpp_vector_elem : Fieldname.t -> bool
 
 val is_java_collection_internal_array : Fieldname.t -> bool
 (** Check if the field is for Java collection's elements *)
+
+(** {2 Field domain constructor} *)
+
+type field_typ = Typ.t option
+
+type 'prim t =
+  | Prim of 'prim
+  | Field of {prefix: 'prim t; fn: Fieldname.t; typ: field_typ}
+  | StarField of {prefix: 'prim t; last_field: Fieldname.t}
+      (** Represents a path starting with [prefix] and ending with the field [last_field], the
+          middle can be anything. Invariants:
+
+          - There is at most one StarField
+          - StarField excluded, there are no duplicate fieldnames
+          - StarField can only be followed by Deref elements *)
+[@@deriving compare]
+
+val mk_append_field :
+     prim_append_field:
+       (   ?typ:Typ.t
+        -> 'prim t
+        -> Fieldname.t
+        -> (depth:int -> 'prim t -> 'prim t)
+        -> int
+        -> 'prim
+        -> 'prim t)
+  -> prim_append_star_field:('prim t -> Fieldname.t -> ('prim t -> 'prim t) -> 'prim -> 'prim t)
+  -> ?typ:Typ.t
+  -> 'prim t
+  -> Fieldname.t
+  -> 'prim t
+
+val mk_append_star_field :
+     prim_append_star_field:('prim t -> Fieldname.t -> ('prim t -> 'prim t) -> 'prim -> 'prim t)
+  -> 'prim t
+  -> Fieldname.t
+  -> 'prim t
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index a1b150f02..499be45de 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -9,6 +9,7 @@ open! IStd
 open AbsLoc
 open! AbstractDomain.Types
 module L = Logging
+module BoField = BufferOverrunField
 module BoUtils = BufferOverrunUtils
 module Dom = BufferOverrunDomain
 module PO = BufferOverrunProofObligations
@@ -525,7 +526,7 @@ module ArrObjCommon = struct
   let size_exec exp ~fn ({integer_type_widths} as model_env) ~ret:(id, _) mem =
     let locs = Sem.eval integer_type_widths exp mem |> Dom.Val.get_all_locs in
     match PowLoc.is_singleton_or_more locs with
-    | Singleton (Loc.Allocsite (Allocsite.LiteralString s)) ->
+    | Singleton (BoField.Prim (Loc.Allocsite (Allocsite.LiteralString s))) ->
         model_by_value (Dom.Val.of_int (String.length s)) id mem
     | _ ->
         let arr_locs = deref_of model_env exp ~fn mem in
@@ -568,7 +569,7 @@ end
 
 module StdVector = struct
   let append_field loc ~vec_typ ~elt_typ =
-    Loc.append_field loc ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
+    Loc.append_field loc (BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
 
 
   let append_fields locs ~vec_typ ~elt_typ =
@@ -828,7 +829,7 @@ module Collection = struct
     in
     let coll_loc = Loc.of_allocsite coll_allocsite in
     let internal_array_loc =
-      Loc.append_field coll_loc ~fn:BufferOverrunField.java_collection_internal_array
+      Loc.append_field coll_loc BufferOverrunField.java_collection_internal_array
     in
     mem
     |> Dom.Mem.add_heap internal_array_loc internal_array
@@ -1102,7 +1103,7 @@ module JavaString = struct
           ~represents_multiple_values:true
       in
       Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_loc arr_loc) mem
-      |> Dom.Mem.add_heap (Loc.append_field arr_loc ~fn)
+      |> Dom.Mem.add_heap (Loc.append_field arr_loc fn)
            (Dom.Val.of_java_array_alloc elem_alloc ~length ~traces)
       |> Dom.Mem.add_heap (Loc.of_allocsite elem_alloc) elem
     in
@@ -1224,7 +1225,7 @@ module JavaString = struct
     in
     let traces = Trace.(Set.singleton location ArrayDeclaration) in
     Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_loc arr_loc) mem
-    |> Dom.Mem.add_heap (Loc.append_field arr_loc ~fn)
+    |> Dom.Mem.add_heap (Loc.append_field arr_loc fn)
          (Dom.Val.of_java_array_alloc elem_alloc ~length:length_itv ~traces)
 
 
diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml
index c065b724d..bee30f070 100644
--- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml
+++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml
@@ -7,6 +7,7 @@
 
 open! IStd
 module L = Logging
+module BoField = BufferOverrunField
 module SPath = Symb.SymbolPath
 module FormalTyps = Caml.Map.Make (Pvar)
 
@@ -25,9 +26,9 @@ let mk pdesc =
   in
   fun tenv integer_type_widths ->
     let rec typ_of_param_path = function
-      | SPath.Pvar x ->
+      | BoField.Prim (SPath.Pvar x) ->
           FormalTyps.find_opt x formal_typs
-      | SPath.Deref (_, x) -> (
+      | BoField.Prim (SPath.Deref (_, x)) -> (
         match typ_of_param_path x with
         | None ->
             None
@@ -55,18 +56,18 @@ let mk pdesc =
                 L.(die InternalError) "Deref of unmodeled type `%a`" Typ.Name.pp typename )
           | _ ->
               L.(die InternalError) "Untyped expression is given." ) )
-      | SPath.Field {typ= Some _ as some_typ} ->
+      | BoField.Field {typ= Some _ as some_typ} ->
           some_typ
-      | SPath.Field {fn; prefix= x} -> (
-        match BufferOverrunField.get_type fn with
+      | BoField.Field {fn; prefix= x} -> (
+        match BoField.get_type fn with
         | None ->
             let lookup = Tenv.lookup tenv in
             Option.map (typ_of_param_path x) ~f:(Struct.fld_typ ~lookup ~default:Typ.void fn)
         | some_typ ->
             some_typ )
-      | SPath.StarField {last_field} ->
-          BufferOverrunField.get_type last_field
-      | SPath.Callsite {ret_typ} ->
+      | BoField.StarField {last_field} ->
+          BoField.get_type last_field
+      | BoField.Prim (SPath.Callsite {ret_typ}) ->
           Some ret_typ
     in
     let is_last_field fn (fields : Struct.field list) =
@@ -74,9 +75,9 @@ let mk pdesc =
           Fieldname.equal fn last_fn )
     in
     let rec may_last_field = function
-      | SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ ->
+      | BoField.Prim (SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _) ->
           true
-      | SPath.Field {fn; prefix= x} | SPath.StarField {last_field= fn; prefix= x} ->
+      | BoField.(Field {fn; prefix= x} | StarField {last_field= fn; prefix= x}) ->
           may_last_field x
           && Option.value_map ~default:true (typ_of_param_path x) ~f:(fun parent_typ ->
                  match parent_typ.Typ.desc with
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 7c498c6e8..d028d281e 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -11,6 +11,7 @@ open! IStd
 open AbsLoc
 open! AbstractDomain.Types
 open BufferOverrunDomain
+module BoField = BufferOverrunField
 module L = Logging
 module TraceSet = BufferOverrunTrace.Set
 
@@ -376,7 +377,7 @@ let is_cost_mode = function EvalCost -> true | _ -> false
 
 let eval_sympath_modeled_partial ~mode ~is_expensive p =
   match (mode, p) with
-  | (EvalNormal | EvalCost), Symb.SymbolPath.Callsite _ ->
+  | (EvalNormal | EvalCost), BoField.Prim (Symb.SymbolPath.Callsite _) ->
       Itv.of_modeled_path ~is_expensive p |> Val.of_itv
   | _, _ ->
       (* We only have modeled modeled function calls created in costModels. *)
@@ -385,12 +386,12 @@ let eval_sympath_modeled_partial ~mode ~is_expensive p =
 
 let rec eval_sympath_partial ~mode params p mem =
   match p with
-  | Symb.SymbolPath.Pvar x -> (
+  | BoField.Prim (Symb.SymbolPath.Pvar x) -> (
     try ParamBindings.find x params
     with Caml.Not_found ->
       L.d_printfln_escaped "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ;
       Val.Itv.top )
-  | Symb.SymbolPath.Callsite {ret_typ; cs; obj_path} -> (
+  | BoField.Prim (Symb.SymbolPath.Callsite {ret_typ; cs; obj_path}) -> (
     match mode with
     | EvalNormal | EvalCost ->
         L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Procname.pp
@@ -404,7 +405,7 @@ let rec eval_sympath_partial ~mode params p mem =
         Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
     | EvalPOCond | EvalPOReachability ->
         Val.Itv.top )
-  | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ | Symb.SymbolPath.StarField _ ->
+  | BoField.(Prim (Symb.SymbolPath.Deref _) | Field _ | StarField _) ->
       let locs = eval_locpath ~mode params p mem in
       Mem.find_set locs mem
 
@@ -412,16 +413,16 @@ let rec eval_sympath_partial ~mode params p mem =
 and eval_locpath ~mode params p mem =
   let res =
     match p with
-    | Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ ->
+    | BoField.Prim (Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _) ->
         let v = eval_sympath_partial ~mode params p mem in
         Val.get_all_locs v
-    | Symb.SymbolPath.Deref (_, p) ->
+    | BoField.Prim (Symb.SymbolPath.Deref (_, p)) ->
         let v = eval_sympath_partial ~mode params p mem in
         Val.get_all_locs v
-    | Symb.SymbolPath.Field {fn; prefix= p} ->
+    | BoField.Field {fn; prefix= p} ->
         let locs = eval_locpath ~mode params p mem in
         PowLoc.append_field ~fn locs
-    | Symb.SymbolPath.StarField {last_field= fn; prefix} ->
+    | BoField.StarField {last_field= fn; prefix} ->
         let locs = eval_locpath ~mode params prefix mem in
         PowLoc.append_star_field ~fn locs
   in
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index 4c3f6582b..ad59e4346 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -103,7 +103,9 @@ module Exec = struct
   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_path =
+        Option.map path ~f:(fun path -> Symb.SymbolPath.append_field path field_name)
+      in
       let field_loc = PowLoc.append_field locs ~fn:field_name in
       let mem =
         match field_typ.Typ.desc with
diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml
index e179bfe98..dc1b23326 100644
--- a/infer/src/bufferoverrun/symb.ml
+++ b/infer/src/bufferoverrun/symb.ml
@@ -7,6 +7,7 @@
 open! IStd
 module F = Format
 module L = Logging
+module BoField = BufferOverrunField
 
 module BoundEnd = struct
   type t = LowerBound | UpperBound [@@deriving compare]
@@ -23,85 +24,37 @@ module SymbolPath = struct
 
   let compare_deref_kind _ _ = 0
 
-  type field_typ = Typ.t option
-
-  let compare_field_typ _ _ = 0
-
-  let is_field_depth_beyond_limit =
-    match Config.bo_field_depth_limit with
-    | None ->
-        fun _depth -> false
-    | Some limit ->
-        fun depth -> depth > limit
-
-
-  include (* Enforce invariants on Field and StarField *) (
-    struct
-      type partial =
-        | Pvar of Pvar.t
-        | Deref of deref_kind * partial
-        | Field of {fn: Fieldname.t; prefix: partial; typ: field_typ}
-        | Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option [@compare.ignore]}
-        | StarField of {last_field: Fieldname.t; prefix: partial}
-      [@@deriving compare]
-
-      let of_pvar pvar = Pvar pvar
-
-      let of_callsite ?obj_path ~ret_typ cs = Callsite {ret_typ; cs; obj_path}
-
-      let deref ~deref_kind p = Deref (deref_kind, p)
-
-      let star_field p0 fn =
-        let rec aux = function
-          | Pvar _ | Callsite _ ->
-              StarField {last_field= fn; prefix= p0}
-          | Deref (_, p) | Field {prefix= p} ->
-              aux p
-          | StarField {last_field} as p when Fieldname.equal fn last_field ->
-              p
-          | StarField {prefix} ->
-              StarField {last_field= fn; prefix}
-        in
-        aux p0
-
-
-      let field ?typ p0 fn =
-        let rec aux ~depth p =
-          if is_field_depth_beyond_limit depth then star_field p0 fn
-          else
-            match p with
-            | Pvar _ | Callsite _ ->
-                Field {fn; prefix= p0; typ}
-            | Field {fn= fn'} when Fieldname.equal fn fn' ->
-                StarField {last_field= fn; prefix= p0}
-            | Field {prefix= p} | Deref (_, p) ->
-                aux ~depth:(depth + 1) p
-            | StarField {last_field} as p when Fieldname.equal fn last_field ->
-                p
-            | StarField {prefix} ->
-                StarField {last_field= fn; prefix}
-        in
-        aux ~depth:0 p0
-    end :
-      sig
-        type partial = private
-          | Pvar of Pvar.t
-          | Deref of deref_kind * partial
-          | Field of {fn: Fieldname.t; prefix: partial; typ: field_typ}
-          | Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option}
-          | StarField of {last_field: Fieldname.t; prefix: partial}
-        [@@deriving compare]
-
-        val of_pvar : Pvar.t -> partial
-
-        val of_callsite : ?obj_path:partial -> ret_typ:Typ.t -> CallSite.t -> partial
-
-        val deref : deref_kind:deref_kind -> partial -> partial
-
-        val field : ?typ:Typ.t -> partial -> Fieldname.t -> partial
-
-        val star_field : partial -> Fieldname.t -> partial
-      end )
+  type prim =
+    | Pvar of Pvar.t
+    | Deref of deref_kind * partial
+    | Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option [@compare.ignore]}
+  [@@deriving compare]
+
+  and partial = prim BoField.t [@@deriving compare]
+
+  let of_pvar pvar = BoField.Prim (Pvar pvar)
+
+  let of_callsite ?obj_path ~ret_typ cs = BoField.Prim (Callsite {ret_typ; cs; obj_path})
+
+  let deref ~deref_kind p = BoField.Prim (Deref (deref_kind, p))
+
+  let prim_append_field ?typ p0 fn aux depth = function
+    | Pvar _ | Callsite _ ->
+        BoField.Field {fn; prefix= p0; typ}
+    | Deref (_, p) ->
+        aux ~depth:(depth + 1) p
+
+
+  let prim_append_star_field p0 fn aux = function
+    | Pvar _ | Callsite _ ->
+        BoField.StarField {prefix= p0; last_field= fn}
+    | Deref (_, p) ->
+        aux p
+
+
+  let append_field = BoField.mk_append_field ~prim_append_field ~prim_append_star_field
+
+  let append_star_field = BoField.mk_append_star_field ~prim_append_star_field
 
   type t =
     | Normal of partial
@@ -122,14 +75,19 @@ module SymbolPath = struct
 
   let modeled p ~is_expensive = Modeled {p; is_expensive}
 
-  let is_this = function Pvar pvar -> Pvar.is_this pvar || Pvar.is_self pvar | _ -> false
+  let is_this = function
+    | BoField.Prim (Pvar pvar) ->
+        Pvar.is_this pvar || Pvar.is_self pvar
+    | _ ->
+        false
+
 
   let rec get_pvar = function
-    | Pvar pvar ->
+    | BoField.Prim (Pvar pvar) ->
         Some pvar
-    | Deref (_, partial) | Field {prefix= partial} | StarField {prefix= partial} ->
+    | BoField.(Prim (Deref (_, partial)) | Field {prefix= partial} | StarField {prefix= partial}) ->
         get_pvar partial
-    | Callsite _ ->
+    | BoField.Prim (Callsite _) ->
         None
 
 
@@ -139,27 +97,27 @@ module SymbolPath = struct
 
 
   let rec pp_partial_paren ~paren fmt = function
-    | Pvar pvar ->
+    | BoField.Prim (Pvar pvar) ->
         if Config.bo_debug >= 3 then Pvar.pp_value fmt pvar else Pvar.pp_value_non_verbose fmt pvar
-    | Deref (Deref_JavaPointer, p) when Config.bo_debug < 3 ->
+    | BoField.Prim (Deref (Deref_JavaPointer, p)) when Config.bo_debug < 3 ->
         pp_partial_paren ~paren fmt p
-    | Deref (Deref_ArrayIndex, p) ->
+    | BoField.Prim (Deref (Deref_ArrayIndex, p)) ->
         F.fprintf fmt "%a[*]" (pp_partial_paren ~paren:true) p
-    | Deref ((Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer), p) ->
+    | BoField.Prim (Deref ((Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer), p)) ->
         pp_pointer ~paren fmt p
-    | Field {fn; prefix= Deref ((Deref_COneValuePointer | Deref_CPointer), p)} ->
+    | BoField.Field {fn; prefix= Prim (Deref ((Deref_COneValuePointer | Deref_CPointer), p))} ->
         BufferOverrunField.pp ~pp_lhs:(pp_partial_paren ~paren:true) ~sep:"->" fmt p fn
-    | Field {fn; prefix= p} ->
+    | BoField.Field {fn; prefix= p} ->
         BufferOverrunField.pp ~pp_lhs:(pp_partial_paren ~paren:true) ~sep:"." fmt p fn
-    | Callsite {cs; obj_path= Some obj_path} ->
+    | BoField.Prim (Callsite {cs; obj_path= Some obj_path}) ->
         if paren then F.pp_print_string fmt "(" ;
         F.fprintf fmt "%a.%a" (pp_partial_paren ~paren:false) obj_path
           (Procname.pp_simplified_string ~withclass:false)
           (CallSite.pname cs) ;
         if paren then F.pp_print_string fmt ")"
-    | Callsite {cs; obj_path= None} ->
+    | BoField.Prim (Callsite {cs; obj_path= None}) ->
         Procname.pp_simplified_string ~withclass:true fmt (CallSite.pname cs)
-    | StarField {last_field; prefix} ->
+    | BoField.StarField {last_field; prefix} ->
         BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
 
 
@@ -200,54 +158,55 @@ module SymbolPath = struct
 
   let rec represents_multiple_values = function
     (* TODO depending on the result, the call might represent multiple values *)
-    | Callsite _ | Pvar _ ->
+    | BoField.Prim (Callsite _ | Pvar _) ->
         false
-    | Deref (Deref_ArrayIndex, _) | StarField _ ->
+    | BoField.Prim (Deref (Deref_ArrayIndex, _)) | BoField.StarField _ ->
         true
-    | Deref (Deref_CPointer, p)
+    | BoField.Prim (Deref (Deref_CPointer, p))
     (* Deref_CPointer is unsound here but avoids many FPs for non-array pointers *)
-    | Deref ((Deref_COneValuePointer | Deref_JavaPointer), p)
-    | Field {prefix= p} ->
+    | BoField.Prim (Deref ((Deref_COneValuePointer | Deref_JavaPointer), p))
+    | BoField.Field {prefix= p} ->
         represents_multiple_values p
 
 
   let rec represents_multiple_values_sound = function
-    | Callsite _ | StarField _ ->
+    | BoField.Prim (Callsite _) | BoField.StarField _ ->
         true
-    | Pvar _ ->
+    | BoField.Prim (Pvar _) ->
         false
-    | Deref ((Deref_ArrayIndex | Deref_CPointer), _) ->
+    | BoField.Prim (Deref ((Deref_ArrayIndex | Deref_CPointer), _)) ->
         true
-    | Deref ((Deref_COneValuePointer | Deref_JavaPointer), p) | Field {prefix= p} ->
+    | BoField.(Prim (Deref ((Deref_COneValuePointer | Deref_JavaPointer), p)) | Field {prefix= p})
+      ->
         represents_multiple_values_sound p
 
 
   let rec represents_callsite_sound_partial = function
-    | Callsite _ ->
+    | BoField.Prim (Callsite _) ->
         true
-    | Pvar _ ->
+    | BoField.Prim (Pvar _) ->
         false
-    | Deref (_, p) | Field {prefix= p} | StarField {prefix= p} ->
+    | BoField.(Prim (Deref (_, p)) | Field {prefix= p} | StarField {prefix= p}) ->
         represents_callsite_sound_partial p
 
 
   let rec exists_pvar_partial ~f = function
-    | Pvar pvar ->
+    | BoField.Prim (Pvar pvar) ->
         f pvar
-    | Deref (_, p) | Field {prefix= p} | StarField {prefix= p} ->
+    | BoField.(Prim (Deref (_, p)) | Field {prefix= p} | StarField {prefix= p}) ->
         exists_pvar_partial ~f p
-    | Callsite _ ->
+    | BoField.Prim (Callsite _) ->
         false
 
 
   let rec exists_str_partial ~f = function
-    | Pvar pvar ->
+    | BoField.Prim (Pvar pvar) ->
         f (Pvar.to_string pvar)
-    | Deref (_, x) ->
+    | BoField.Prim (Deref (_, x)) ->
         exists_str_partial ~f x
-    | Field {fn= fld; prefix= x} | StarField {last_field= fld; prefix= x} ->
+    | BoField.(Field {fn= fld; prefix= x} | StarField {last_field= fld; prefix= x}) ->
         f (Fieldname.to_string fld) || exists_str_partial ~f x
-    | Callsite _ ->
+    | BoField.Prim (Callsite _) ->
         false
 
 
@@ -264,18 +223,18 @@ module SymbolPath = struct
 
 
   let is_cpp_vector_elem = function
-    | Field {fn} ->
+    | BoField.Field {fn} ->
         BufferOverrunField.is_cpp_vector_elem fn
     | _ ->
         false
 
 
   let rec is_global_partial = function
-    | Pvar pvar ->
+    | BoField.Prim (Pvar pvar) ->
         Pvar.is_global pvar
-    | Deref (_, x) | Field {prefix= x} | StarField {prefix= x} ->
+    | BoField.(Prim (Deref (_, x)) | Field {prefix= x} | StarField {prefix= x}) ->
         is_global_partial x
-    | Callsite _ ->
+    | BoField.Prim (Callsite _) ->
         false
 
 
diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli
index c24c4150c..ea0908fd3 100644
--- a/infer/src/bufferoverrun/symb.mli
+++ b/infer/src/bufferoverrun/symb.mli
@@ -18,22 +18,16 @@ module SymbolPath : sig
   type deref_kind = Deref_ArrayIndex | Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer
   [@@deriving compare]
 
-  type partial = private
+  type prim =
     | Pvar of Pvar.t
     | Deref of deref_kind * partial
-    | Field of {fn: Fieldname.t; prefix: partial; typ: Typ.t option}
-    | Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option}
+    | Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option [@compare.ignore]}
         (** [obj_path] represents the varaible name object when a method of which is called at the
             [cs] callsite. *)
-    | StarField of {last_field: Fieldname.t; prefix: partial}
-        (** Represents a path starting with [prefix] and ending with the field [last_field], the
-            middle can be anything. Invariants:
-
-            - There is at most one StarField
-            - StarField excluded, there are no duplicate fieldnames
-            - StarField can only be followed by Deref elements *)
   [@@deriving compare]
 
+  and partial = prim BufferOverrunField.t [@@deriving compare]
+
   type t = private
     | Normal of partial
     | Offset of {p: partial; is_void: bool}
@@ -55,9 +49,9 @@ module SymbolPath : sig
 
   val deref : deref_kind:deref_kind -> partial -> partial
 
-  val field : ?typ:Typ.t -> partial -> Fieldname.t -> partial
+  val append_field : ?typ:Typ.t -> partial -> Fieldname.t -> partial
 
-  val star_field : partial -> Fieldname.t -> partial
+  val append_star_field : partial -> Fieldname.t -> partial
 
   val normal : partial -> t
 
@@ -88,8 +82,6 @@ module SymbolPath : sig
   val is_cpp_vector_elem : partial -> bool
 
   val is_global_partial : partial -> bool
-
-  val is_field_depth_beyond_limit : int -> bool
 end
 
 module Symbol : sig
diff --git a/infer/src/cost/boundMap.ml b/infer/src/cost/boundMap.ml
index 8d1be4b94..e59e5f720 100644
--- a/infer/src/cost/boundMap.ml
+++ b/infer/src/cost/boundMap.ml
@@ -23,9 +23,9 @@ let print_upper_bound_map bound_map =
 
 
 let filter_loc vars_to_keep = function
-  | AbsLoc.Loc.Var (Var.LogicalVar _) ->
+  | BufferOverrunField.Prim (AbsLoc.Loc.Var (Var.LogicalVar _)) ->
       None
-  | AbsLoc.Loc.Var var ->
+  | BufferOverrunField.Prim (AbsLoc.Loc.Var var) ->
       Control.ControlMap.find_opt var vars_to_keep
   | _ ->
       None
diff --git a/infer/src/cost/costDomain.ml b/infer/src/cost/costDomain.ml
index e3e854a6c..e304a8203 100644
--- a/infer/src/cost/costDomain.ml
+++ b/infer/src/cost/costDomain.ml
@@ -13,7 +13,7 @@ module BasicCost = struct
 
   (* NOTE: Increment the version number if you changed the [t] type.  This is for avoiding
      demarshalling failure of cost analysis results in running infer-reportdiff. *)
-  let version = 5
+  let version = 6
 end
 
 (** Module to simulate a record
diff --git a/infer/src/cost/costModels.ml b/infer/src/cost/costModels.ml
index 7e7cc5563..59b3e6a6b 100644
--- a/infer/src/cost/costModels.ml
+++ b/infer/src/cost/costModels.ml
@@ -54,7 +54,7 @@ module IntHashMap = struct
     | Singleton this_loc -> (
       match (AbsLoc.Loc.get_path this_loc, Typ.strip_ptr typ |> Typ.name) with
       | Some path, Some typ_name ->
-          let path = Symb.SymbolPath.field path (Fieldname.make typ_name "size") in
+          let path = Symb.SymbolPath.append_field path (Fieldname.make typ_name "size") in
           let itv = Itv.of_normal_path ~unsigned:true path in
           CostUtils.of_itv ~itv ~degree_kind:Linear ~of_function:"IntHashMap.keys" location
       | _, _ ->