From f02952c003225f2443d4e204563468e1126dda6e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 16 Nov 2020 12:52:24 -0800
Subject: [PATCH] [sledge] Rename Sh.seg.seq to cnt

Summary:
The `seq` name of this field refers to the expected sort of it's
value, where the others refer to the role they play. So rename
seq (for sequence) to cnt (for contents).

Reviewed By: ngorogiannis

Differential Revision: D24951507

fbshipit-source-id: fd6640517
---
 sledge/src/domain_sh.ml        | 12 ++---
 sledge/src/exec.ml             | 84 +++++++++++++++++-----------------
 sledge/src/sh.ml               | 20 ++++----
 sledge/src/sh.mli              | 11 +++--
 sledge/src/solver.ml           | 70 ++++++++++++++--------------
 sledge/src/test/sh_test.ml     |  4 +-
 sledge/src/test/solver_test.ml | 58 +++++++++++------------
 7 files changed, 132 insertions(+), 127 deletions(-)

diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 2c8f10cf0..2081bed0c 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -30,8 +30,8 @@ let init globals =
             | _ -> violates Llair.GlobalDefn.invariant global
           in
           let len = Term.integer (Z.of_int siz) in
-          let seq = X.term seq in
-          Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
+          let cnt = X.term seq in
+          Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; cnt})
       | _ -> q )
 
 let join p q =
@@ -93,7 +93,7 @@ let garbage_collect (q : Sh.t) ~wrt =
       let new_set =
         List.fold q.heap current ~f:(fun seg current ->
             if value_determined_by q.ctx current seg.loc then
-              List.fold (Context.class_of q.ctx seg.seq) current
+              List.fold (Context.class_of q.ctx seg.cnt) current
                 ~f:(fun e c ->
                   Term.Set.union c (Term.Set.of_iter (Term.atoms e)) )
             else current )
@@ -324,9 +324,9 @@ let%test_module _ =
     let b = Term.var b_
     let n = Term.var n_
     let endV = Term.var end_
-    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; seq= a}
-    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= endV}
-    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main}
+    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; cnt= a}
+    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; cnt= endV}
+    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; cnt= main}
 
     let%expect_test _ =
       pp (garbage_collect seg_main ~wrt:(Term.Set.of_list [])) ;
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 9301bf3df..0401d215d 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -28,7 +28,7 @@ module Fresh : sig
        ?bas:Term.t
     -> ?len:Term.t
     -> ?siz:Term.t
-    -> ?seq:Term.t
+    -> ?cnt:Term.t
     -> Term.t
     -> Sh.seg t
   (** Segment with fresh variables for omitted arguments. *)
@@ -55,15 +55,15 @@ end = struct
     let xs = Var.Set.add x xs in
     return (Term.var x) {wrt; xs}
 
-  let seg ?bas ?len ?siz ?seq loc =
+  let seg ?bas ?len ?siz ?cnt loc =
     let freshen term nam =
       match term with Some term -> return term | None -> var nam
     in
     let* bas = freshen bas "b" in
     let* len = freshen len "m" in
     let* siz = freshen siz "n" in
-    let* seq = freshen seq "a" in
-    return Sh.{loc; bas; len; siz; seq}
+    let* cnt = freshen cnt "a" in
+    return Sh.{loc; bas; len; siz; cnt}
 
   let assign ~ws ~rs {wrt; xs} =
     let ovs = Var.Set.inter ws rs in
@@ -89,9 +89,11 @@ let gen_spec us specm =
 
 let null_eq ptr = Sh.pure (Formula.eq0 ptr)
 
-let eq_concat (siz, seq) ms =
-  Formula.eq (Term.sized ~siz ~seq)
-    (Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
+let eq_concat (siz, cnt) ms =
+  Formula.eq
+    (Term.sized ~siz ~seq:cnt)
+    (Term.concat
+       (Array.map ~f:(fun (siz, cnt) -> Term.sized ~siz ~seq:cnt) ms))
 
 open Fresh.Import
 
@@ -123,7 +125,7 @@ let load_spec reg ptr len =
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let post =
     Sh.and_
-      (Formula.eq (Term.var reg) (Term.rename sub seg.seq))
+      (Formula.eq (Term.var reg) (Term.rename sub seg.cnt))
       (Sh.rename sub foot)
   in
   {foot; sub; ms; post}
@@ -135,7 +137,7 @@ let load_spec reg ptr len =
 let store_spec ptr exp len =
   let+ seg = Fresh.seg ptr ~siz:len in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with seq= exp} in
+  let post = Sh.seg {seg with cnt= exp} in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d-[b;m)->⟨l,α⟩ }
@@ -145,7 +147,7 @@ let store_spec ptr exp len =
 let memset_spec dst byt len =
   let+ seg = Fresh.seg dst ~siz:len in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with seq= Term.splat byt} in
+  let post = Sh.seg {seg with cnt= Term.splat byt} in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ }
@@ -170,7 +172,7 @@ let memcpy_dj_spec dst src len =
   let dst_heap = Sh.seg dst_seg in
   let+ src_seg = Fresh.seg src ~siz:len in
   let src_heap = Sh.seg src_seg in
-  let dst_seg' = {dst_seg with seq= src_seg.seq} in
+  let dst_seg' = {dst_seg with cnt= src_seg.cnt} in
   let dst_heap' = Sh.seg dst_seg' in
   let foot = Sh.star dst_heap src_heap in
   let post = Sh.star dst_heap' src_heap in
@@ -200,23 +202,23 @@ let memmov_dj_spec = memcpy_dj_spec
 let memmov_foot dst src len =
   let* bas = Fresh.var "b" in
   let* siz = Fresh.var "m" in
-  let* seq_dst = Fresh.var "a" in
-  let* seq_mid = Fresh.var "a" in
-  let* seq_src = Fresh.var "a" in
+  let* cnt_dst = Fresh.var "a" in
+  let* cnt_mid = Fresh.var "a" in
+  let* cnt_src = Fresh.var "a" in
   let src_dst = Term.sub src dst in
-  let mem_dst = (src_dst, seq_dst) in
+  let mem_dst = (src_dst, cnt_dst) in
   let siz_mid = Term.sub len src_dst in
-  let mem_mid = (siz_mid, seq_mid) in
-  let mem_src = (src_dst, seq_src) in
+  let mem_mid = (siz_mid, cnt_mid) in
+  let mem_src = (src_dst, cnt_src) in
   let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in
   let* siz_dst_mid_src = Fresh.var "m" in
-  let+ seq_dst_mid_src = Fresh.var "a" in
+  let+ cnt_dst_mid_src = Fresh.var "a" in
   let eq_mem_dst_mid_src =
-    eq_concat (siz_dst_mid_src, seq_dst_mid_src) mem_dst_mid_src
+    eq_concat (siz_dst_mid_src, cnt_dst_mid_src) mem_dst_mid_src
   in
   let seg =
     Sh.seg
-      {loc= dst; bas; len= siz; siz= siz_dst_mid_src; seq= seq_dst_mid_src}
+      {loc= dst; bas; len= siz; siz= siz_dst_mid_src; cnt= cnt_dst_mid_src}
   in
   let foot =
     Sh.and_ eq_mem_dst_mid_src
@@ -233,9 +235,9 @@ let memmov_dn_spec dst src len =
   let* bas, siz, _, mem_mid, mem_src, foot = memmov_foot dst src len in
   let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in
   let* siz_mid_src_src = Fresh.var "m" in
-  let+ seq_mid_src_src = Fresh.var "a" in
+  let+ cnt_mid_src_src = Fresh.var "a" in
   let eq_mem_mid_src_src =
-    eq_concat (siz_mid_src_src, seq_mid_src_src) mem_mid_src_src
+    eq_concat (siz_mid_src_src, cnt_mid_src_src) mem_mid_src_src
   in
   let post =
     Sh.and_ eq_mem_mid_src_src
@@ -244,7 +246,7 @@ let memmov_dn_spec dst src len =
          ; bas
          ; len= siz
          ; siz= siz_mid_src_src
-         ; seq= seq_mid_src_src })
+         ; cnt= cnt_mid_src_src })
   in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -256,9 +258,9 @@ let memmov_up_spec dst src len =
   let* bas, siz, mem_src, mem_mid, _, foot = memmov_foot src dst len in
   let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in
   let* siz_src_src_mid = Fresh.var "m" in
-  let+ seq_src_src_mid = Fresh.var "a" in
+  let+ cnt_src_src_mid = Fresh.var "a" in
   let eq_mem_src_src_mid =
-    eq_concat (siz_src_src_mid, seq_src_src_mid) mem_src_src_mid
+    eq_concat (siz_src_src_mid, cnt_src_src_mid) mem_src_src_mid
   in
   let post =
     Sh.and_ eq_mem_src_src_mid
@@ -267,7 +269,7 @@ let memmov_up_spec dst src len =
          ; bas
          ; len= siz
          ; siz= siz_src_src_mid
-         ; seq= seq_src_src_mid })
+         ; cnt= cnt_src_src_mid })
   in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -353,8 +355,8 @@ let calloc_spec reg num len =
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
-  let seq = Term.splat Term.zero in
-  let+ seg = Fresh.seg loc ~bas:loc ~len:siz ~siz ~seq in
+  let cnt = Term.splat Term.zero in
+  let+ seg = Fresh.seg loc ~bas:loc ~len:siz ~siz ~cnt in
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {foot; sub; ms; post}
 
@@ -374,7 +376,7 @@ let posix_memalign_spec reg ptr siz =
       ~rs:(Var.Set.union foot.us (Term.fv siz))
   in
   let* q = Fresh.var "q" in
-  let pseg' = {pseg with seq= q} in
+  let pseg' = {pseg with cnt= q} in
   let+ qseg = Fresh.seg q ~bas:q ~len:siz ~siz in
   let eok = Term.zero in
   let enomem = Term.integer (Z.of_int 12) in
@@ -404,8 +406,8 @@ let realloc_spec reg ptr siz =
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
   let* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in
-  let a0 = pseg.seq in
-  let a1 = rseg.seq in
+  let a0 = pseg.cnt in
+  let a1 = rseg.cnt in
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
@@ -433,8 +435,8 @@ let rallocx_spec reg ptr siz =
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
   let* rseg = Fresh.seg loc ~bas:loc ~len:siz ~siz in
-  let a0 = pseg.seq in
-  let a1 = rseg.seq in
+  let a0 = pseg.cnt in
+  let a1 = rseg.cnt in
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
@@ -465,8 +467,8 @@ let xallocx_spec reg ptr siz ext =
   let siz = Term.rename sub siz in
   let ext = Term.rename sub ext in
   let* seg' = Fresh.seg ptr ~bas:ptr ~len:reg ~siz:reg in
-  let a0 = seg.seq in
-  let a1 = seg'.seq in
+  let a0 = seg.cnt in
+  let a1 = seg'.cnt in
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.and_
@@ -524,13 +526,13 @@ let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
  *)
 let mallctl_read_spec r i w n =
   let* iseg = Fresh.seg i in
-  let* rseg = Fresh.seg r ~siz:iseg.seq in
+  let* rseg = Fresh.seg r ~siz:iseg.cnt in
   let+ a = Fresh.var "a" in
   let foot =
     Sh.and_ (Formula.eq0 w)
       (Sh.and_ (Formula.eq0 n) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
-  let rseg' = {rseg with seq= a} in
+  let rseg' = {rseg with cnt= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -543,7 +545,7 @@ let mallctlbymib_read_spec p l r i w n =
   let wl = size_of_int_mul l in
   let* pseg = Fresh.seg p ~siz:wl in
   let* iseg = Fresh.seg i in
-  let m = iseg.seq in
+  let m = iseg.cnt in
   let* rseg = Fresh.seg r ~siz:m in
   let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
   let+ a = Fresh.var "a" in
@@ -551,7 +553,7 @@ let mallctlbymib_read_spec p l r i w n =
     Sh.and_ (Formula.eq0 w)
       (Sh.and_ (Formula.eq0 n) (Sh.star const (Sh.seg rseg)))
   in
-  let rseg' = {rseg with seq= a} in
+  let rseg' = {rseg with cnt= a} in
   let post = Sh.star (Sh.seg rseg') const in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -596,12 +598,12 @@ let mallctlbymib_specs p j r i w n =
  *)
 let mallctlnametomib_spec p o =
   let* oseg = Fresh.seg o in
-  let n = oseg.seq in
+  let n = oseg.cnt in
   let wn = size_of_int_mul n in
   let* pseg = Fresh.seg p ~siz:wn in
   let+ a = Fresh.var "a" in
   let foot = Sh.star (Sh.seg oseg) (Sh.seg pseg) in
-  let pseg' = {pseg with seq= a} in
+  let pseg' = {pseg with cnt= a} in
   let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 2539e2c56..2c27dca18 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -11,7 +11,7 @@ open Fol
 
 [@@@warning "+9"]
 
-type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
+type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; cnt: Term.t}
 [@@deriving compare, equal, sexp]
 
 type starjunction =
@@ -46,18 +46,18 @@ let map_seg ~f h =
   let bas = f h.bas in
   let len = f h.len in
   let siz = f h.siz in
-  let seq = f h.seq in
+  let cnt = f h.cnt in
   if
     loc == h.loc
     && bas == h.bas
     && len == h.len
     && siz == h.siz
-    && seq == h.seq
+    && cnt == h.cnt
   then h
-  else {loc; bas; len; siz; seq}
+  else {loc; bas; len; siz; cnt}
 
-let fold_terms_seg {loc; bas; len; siz; seq} s ~f =
-  f loc (f bas (f len (f siz (f seq s))))
+let fold_terms_seg {loc; bas; len; siz; cnt} s ~f =
+  f loc (f bas (f len (f siz (f cnt s))))
 
 let fold_vars_seg seg s ~f =
   fold_terms_seg ~f:(Iter.fold ~f << Term.vars) seg s
@@ -109,15 +109,15 @@ let var_strength ?(xs = Var.Set.empty) q =
   in
   var_strength_ xs m q
 
-let pp_chunk x fs (siz, seq) = Term.ppx x fs (Term.sized ~siz ~seq)
+let pp_chunk x fs (siz, cnt) = Term.ppx x fs (Term.sized ~siz ~seq:cnt)
 
-let pp_seg x fs {loc; bas; len; siz; seq} =
+let pp_seg x fs {loc; bas; len; siz; cnt} =
   let term_pp = Term.ppx x in
   Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
     (fun fs (bas, len) ->
       if (not (Term.equal loc bas)) || not (Term.equal len siz) then
         Format.fprintf fs " %a, %a " term_pp bas term_pp len )
-    (bas, len) (pp_chunk x) (siz, seq)
+    (bas, len) (pp_chunk x) (siz, cnt)
 
 let pp_seg_norm ctx fs seg =
   let x _ = None in
@@ -144,7 +144,7 @@ let pp_block x fs segs =
   in
   let term_pp = Term.ppx x in
   let pp_chunks =
-    List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.seq))
+    List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.cnt))
   in
   match segs with
   | {loc; bas; len; _} :: _ ->
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 6677deb91..212b6c393 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -9,10 +9,13 @@
 
 open Fol
 
-(** Segment of memory starting at [loc] containing [seq] (a byte-array) of
-    size [siz], contained in an enclosing allocation-block starting at [bas]
-    of length [len]. *)
-type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
+(** Segment of memory. *)
+type seg =
+  { loc: Term.t  (** location (address) where segment starts *)
+  ; bas: Term.t  (** base address of enclosing allocation-block *)
+  ; len: Term.t  (** length of enclosing allocation-block *)
+  ; siz: Term.t  (** size of segment / length of the contents *)
+  ; cnt: Term.t  (** contents of segment, a sequence / byte array *) }
 
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 364008c87..309a5e41c 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -194,8 +194,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx)
         msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.bas= b; len= m; seq= a} = msg in
-  let {Sh.bas= b'; len= m'; seq= a'} = ssg in
+  let {Sh.bas= b; len= m; cnt= a} = msg in
+  let {Sh.bas= b'; len= m'; cnt= a'} = ssg in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
@@ -223,18 +223,18 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let o_n = Term.integer o_n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv n) in
-  let com = Sh.star (Sh.seg {msg with siz= n; seq= a0}) com in
+  let com = Sh.star (Sh.seg {msg with siz= n; cnt= a0}) com in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(n, a0); (o_n, a1)|])
       (Sh.star
-         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; seq= a1})
+         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; cnt= a1})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -263,8 +263,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let n_o = Term.integer n_o in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
@@ -276,7 +276,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
             (eq_concat (n, a') [|(o, a); (n_o, a1')|])
             (Sh.star
                (Sh.seg
-                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; seq= a1'})
+                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; cnt= a1'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -299,20 +299,20 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let l_k = Term.integer l_k in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv n) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (n, a1)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -341,8 +341,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let l_k = Term.integer l_k in
   let ko_ln = Term.integer ko_ln in
   let ln = Term.add l n in
@@ -351,15 +351,15 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
          (Sh.star
-            (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
+            (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; cnt= a2})
             (Sh.rem_seg msg min)))
   in
   let sub =
@@ -388,8 +388,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let l_k = Term.integer l_k in
   let ko_l = Term.integer ko_l in
   let ln_ko = Term.integer ln_ko in
@@ -399,13 +399,13 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv l) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; seq= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; cnt= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -414,7 +414,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
          (Sh.and_
             (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
             (Sh.star
-               (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
+               (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; cnt= a2'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
@@ -438,8 +438,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let k_l = Term.integer k_l in
   let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
   let com = Sh.star (Sh.seg msg) com in
@@ -450,7 +450,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -475,8 +475,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let k_l = Term.integer k_l in
   let ln_ko = Term.integer ln_ko in
   let ko = Term.add k o in
@@ -490,9 +490,9 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
                (Sh.star
-                  (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
+                  (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; cnt= a2'})
                   (Sh.rem_seg ssg sub)))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -516,8 +516,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
   let k_l = Term.integer k_l in
   let ln_k = Term.integer ln_k in
   let ko_ln = Term.integer ko_ln in
@@ -526,13 +526,13 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let com =
-    Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; seq= a1}) com
+    Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; cnt= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
       (Sh.star
-         (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
+         (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; cnt= a2})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -541,7 +541,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; cnt= a0'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index dfa4f9731..b2a5a6215 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -58,8 +58,8 @@ let%test_module _ =
     let%expect_test _ =
       pp
         (star
-           (seg {loc= x; bas= x; len= !16; siz= !8; seq= a})
-           (seg {loc= x + !8; bas= x; len= !16; siz= !8; seq= b})) ;
+           (seg {loc= x; bas= x; len= !16; siz= !8; cnt= a})
+           (seg {loc= x + !8; bas= x; len= !16; siz= !8; cnt= b})) ;
       [%expect {|
           %x_6 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}]
 
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index e71762c1a..0d7098c46 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -78,7 +78,7 @@ let%test_module _ =
 
     let%expect_test _ =
       check_frame
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
         [] Sh.emp ;
       [%expect
         {|
@@ -87,9 +87,9 @@ let%test_module _ =
 
     let%expect_test _ =
       check_frame
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
         []
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -98,8 +98,8 @@ let%test_module _ =
         ) infer_frame:   emp |}]
 
     let%expect_test _ =
-      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; seq= a2} in
-      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in
+      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; cnt= a2} in
+      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; cnt= a} in
       let minued = Sh.star common seg1 in
       let subtrahend =
         Sh.and_ (Formula.eq m n)
@@ -120,10 +120,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
-           (Sh.seg {loc= l2; bas= b; len= m; siz= n; seq= a2}))
+           (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a})
+           (Sh.seg {loc= l2; bas= b; len= m; siz= n; cnt= a2}))
         []
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -135,10 +135,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
         [a3_]
-        (Sh.seg {loc= l; bas= l; len= !16; siz= !16; seq= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -148,10 +148,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
         [a3_; m_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= !16; seq= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -164,10 +164,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; cnt= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; cnt= a2}))
         [a3_; m_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -180,12 +180,12 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
+           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; cnt= a})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= !16}))
         [a2_; m_; n_]
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})
-           (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})) ;
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})
+           (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ;
       [%expect
         {|
         ( infer_frame:
@@ -202,12 +202,12 @@ let%test_module _ =
     let%expect_test _ =
       infer_frame
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
+           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; cnt= a})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= !16}))
         [a2_; m_; n_]
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})) ;
+           (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ;
       [%expect
         {|
         ( infer_frame:
@@ -223,9 +223,9 @@ let%test_module _ =
 
     let seg_split_symbolically =
       Sh.star
-        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; seq= a2})
+        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; cnt= a2})
         (Sh.seg
-           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); seq= a3})
+           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); cnt= a3})
 
     let%expect_test _ =
       check_frame
@@ -233,7 +233,7 @@ let%test_module _ =
            Formula.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
            seg_split_symbolically)
         [m_; a_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -266,7 +266,7 @@ let%test_module _ =
       infer_frame
         (Sh.and_ (Formula.le n !2) seg_split_symbolically)
         [m_; a_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
       [%expect
         {|
         ( infer_frame: