From 2ca98c80ffe40b818ee25213a7650d43b56bd44d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 17 Mar 2020 09:05:51 -0700
Subject: [PATCH] [sledge] Rename vector to iarray

Summary:
The term "vector" evokes expectations of being automatically growable,
and these are just immutable arrays.

Reviewed By: ngorogiannis

Differential Revision: D20482762

fbshipit-source-id: 0cd2c9c23
---
 sledge/bin/domain_itv.ml                     |  4 +-
 sledge/bin/frontend.ml                       | 46 +++++------
 sledge/bin/sledge.ml                         |  2 +-
 sledge/lib/control.ml                        | 12 +--
 sledge/lib/domain_intf.ml                    |  4 +-
 sledge/lib/domain_sh.ml                      |  8 +-
 sledge/lib/domain_used_globals.ml            |  4 +-
 sledge/lib/equality.ml                       |  4 +-
 sledge/lib/exec.ml                           |  4 +-
 sledge/lib/exec.mli                          |  2 +-
 sledge/lib/exp.ml                            | 36 ++++-----
 sledge/lib/exp.mli                           |  6 +-
 sledge/lib/import/{vector.ml => IArray.ml}   |  4 +-
 sledge/lib/import/{vector.mli => IArray.mli} |  6 +-
 sledge/lib/import/import.ml                  |  4 +-
 sledge/lib/import/import.mli                 |  4 +-
 sledge/lib/import/set.ml                     |  2 +-
 sledge/lib/import/set_intf.ml                |  2 +-
 sledge/lib/llair.ml                          | 74 +++++++++---------
 sledge/lib/llair.mli                         | 18 ++---
 sledge/lib/term.ml                           | 80 ++++++++++----------
 sledge/lib/term.mli                          |  8 +-
 sledge/lib/typ.ml                            | 18 ++---
 sledge/lib/typ.mli                           | 12 +--
 24 files changed, 182 insertions(+), 182 deletions(-)
 rename sledge/lib/import/{vector.ml => IArray.ml} (97%)
 rename sledge/lib/import/{vector.mli => IArray.mli} (97%)

diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml
index 8802e12de..882a2ff85 100644
--- a/sledge/bin/domain_itv.ml
+++ b/sledge/bin/domain_itv.ml
@@ -217,12 +217,12 @@ let exec_kill q r =
 (** perform a series [move_vec] of reg:=exp moves at state [q] *)
 let exec_move q move_vec =
   let defs, uses =
-    Vector.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty)
+    IArray.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty)
       ~f:(fun (defs, uses) (r, e) ->
         (Reg.Set.add defs r, Exp.fold_regs e ~init:uses ~f:Reg.Set.add) )
   in
   assert (Reg.Set.disjoint defs uses) ;
-  Vector.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a)
+  IArray.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a)
 
 let exec_inst q i =
   match (i : Llair.inst) with
diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml
index da16631a3..c3dd27efd 100644
--- a/sledge/bin/frontend.ml
+++ b/sledge/bin/frontend.ml
@@ -245,13 +245,13 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
           let packed = Llvm.is_packed llt in
           if Llvm.is_literal llt then
             let elts =
-              Vector.map ~f:(xlate_type x) (Vector.of_array llelts)
+              IArray.map ~f:(xlate_type x) (IArray.of_array llelts)
             in
             Typ.tuple elts ~bits ~byts ~packed
           else
             let name = struct_name llt in
             let elts =
-              Vector.init len ~f:(fun i -> lazy (xlate_type x llelts.(i)))
+              IArray.init len ~f:(fun i -> lazy (xlate_type x llelts.(i)))
             in
             Typ.struct_ ~name elts ~bits ~byts ~packed
       | Function -> fail "expected to be unsized: %a" pp_lltype llt ()
@@ -263,7 +263,7 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
           let llargs = Llvm.param_types llt in
           let len = Array.length llargs in
           let args =
-            Vector.init len ~f:(fun i -> xlate_type x llargs.(i))
+            IArray.init len ~f:(fun i -> xlate_type x llargs.(i))
           in
           Typ.function_ ~return ~args
       | Struct when Llvm.is_opaque llt -> Typ.opaque ~name:(struct_name llt)
@@ -423,17 +423,17 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.num_operands llv in
         let f i = xlate_value x (Llvm.operand llv i) in
-        Exp.record typ (Vector.init len ~f)
+        Exp.record typ (IArray.init len ~f)
     | ConstantDataVector ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.vector_size (Llvm.type_of llv) in
         let f i = xlate_value x (Llvm.const_element llv i) in
-        Exp.record typ (Vector.init len ~f)
+        Exp.record typ (IArray.init len ~f)
     | ConstantDataArray ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.array_length (Llvm.type_of llv) in
         let f i = xlate_value x (Llvm.const_element llv i) in
-        Exp.record typ (Vector.init len ~f)
+        Exp.record typ (IArray.init len ~f)
     | ConstantStruct ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let is_recursive =
@@ -443,13 +443,13 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
         in
         if is_recursive then
           let elt_thks =
-            Vector.init (Llvm.num_operands llv) ~f:(fun i ->
+            IArray.init (Llvm.num_operands llv) ~f:(fun i ->
                 lazy (xlate_value x (Llvm.operand llv i)) )
           in
           struct_rec ~id:llv typ elt_thks
         else
           Exp.record typ
-            (Vector.init (Llvm.num_operands llv) ~f:(fun i ->
+            (IArray.init (Llvm.num_operands llv) ~f:(fun i ->
                  xlate_value x (Llvm.operand llv i) ))
     | BlockAddress ->
         let parent = find_name (Llvm.operand llv 0) in
@@ -601,7 +601,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
           match (typ : Typ.t) with
           | Tuple {elts} | Struct {elts} ->
               ( Exp.select typ rcd indices.(i)
-              , Vector.get elts indices.(i)
+              , IArray.get elts indices.(i)
               , Exp.update typ ~rcd indices.(i) )
           | Array {elt} ->
               ( Exp.select typ rcd indices.(i)
@@ -776,7 +776,7 @@ let exception_typs =
   let pi8 = Typ.pointer ~elt:Typ.byt in
   let i32 = Typ.integer ~bits:32 ~byts:4 in
   let exc =
-    Typ.tuple ~packed:false (Vector.of_array [|pi8; i32|]) ~bits:96 ~byts:12
+    Typ.tuple ~packed:false (IArray.of_array [|pi8; i32|]) ~bits:96 ~byts:12
   in
   (pi8, i32, exc)
 
@@ -815,12 +815,12 @@ let xlate_jump :
   | [] -> (jmp, blocks)
   | reg_exps ->
       let mov =
-        Llair.Inst.move ~reg_exps:(Vector.of_list_rev reg_exps) ~loc
+        Llair.Inst.move ~reg_exps:(IArray.of_list_rev reg_exps) ~loc
       in
       let lbl = find_name instr ^ ".jmp." ^ dst_lbl in
       let blk =
         Llair.Block.mk ~lbl
-          ~cmnd:(Vector.of_array [|mov|])
+          ~cmnd:(IArray.of_array [|mov|])
           ~term:(Llair.Term.goto ~dst:jmp ~loc)
       in
       let blocks =
@@ -898,7 +898,7 @@ let xlate_instr :
     else
       let reg = xlate_name x instr in
       let exp = xlate instr in
-      let reg_exps = Vector.of_array [|(reg, exp)|] in
+      let reg_exps = IArray.of_array [|(reg, exp)|] in
       emit_inst (Llair.Inst.move ~reg_exps ~loc)
   in
   let opcode = Llvm.instr_opcode instr in
@@ -1052,7 +1052,7 @@ let xlate_instr :
                 ~throw:None ~loc
             in
             continue (fun (insts, term) ->
-                let cmnd = Vector.of_list insts in
+                let cmnd = IArray.of_list insts in
                 ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) ) )
   | Invoke -> (
       let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in
@@ -1149,7 +1149,7 @@ let xlate_instr :
         in
         xlate_cases 1 []
       in
-      let tbl = Vector.of_list cases in
+      let tbl = IArray.of_list cases in
       let blk = Llvm.block_of_value (Llvm.operand instr 1) in
       let els, blocks = xlate_jump x instr blk loc blocks in
       emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) ~blocks
@@ -1168,7 +1168,7 @@ let xlate_instr :
         in
         dests 1 []
       in
-      let tbl = Vector.of_list lldests in
+      let tbl = IArray.of_list lldests in
       emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) ~blocks
   | LandingPad ->
       (* Translate the landingpad clauses to code to load the type_info from
@@ -1200,14 +1200,14 @@ let xlate_instr :
       let lbl = name ^ ".unwind" in
       let reg = xlate_name x instr in
       let jump_unwind i sel rev_blocks =
-        let exp = Exp.record exc_typ (Vector.of_array [|exc; sel|]) in
+        let exp = Exp.record exc_typ (IArray.of_array [|exc; sel|]) in
         let mov =
-          Llair.Inst.move ~reg_exps:(Vector.of_array [|(reg, exp)|]) ~loc
+          Llair.Inst.move ~reg_exps:(IArray.of_array [|(reg, exp)|]) ~loc
         in
         let lbl_i = lbl ^ "." ^ Int.to_string i in
         let blk =
           Llair.Block.mk ~lbl:lbl_i
-            ~cmnd:(Vector.of_array [|mov|])
+            ~cmnd:(IArray.of_array [|mov|])
             ~term:(Llair.Term.goto ~dst:(Llair.Jump.mk lbl) ~loc)
         in
         (Llair.Jump.mk lbl_i, blk :: rev_blocks)
@@ -1224,7 +1224,7 @@ let xlate_instr :
           let lbl i = name ^ "." ^ Int.to_string i in
           let jump i = Llair.Jump.mk (lbl i) in
           let block i term =
-            Llair.Block.mk ~lbl:(lbl i) ~cmnd:Vector.empty ~term
+            Llair.Block.mk ~lbl:(lbl i) ~cmnd:IArray.empty ~term
           in
           let match_filter i rev_blocks =
             jump_unwind i
@@ -1278,7 +1278,7 @@ let xlate_instr :
           ( [load_ti]
           , term_unwind
           , List.rev_append rev_blocks
-              [Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term] ) )
+              [Llair.Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term] ) )
   | Resume ->
       let llrcd = Llvm.operand instr 0 in
       let typ = xlate_type x (Llvm.type_of llrcd) in
@@ -1332,7 +1332,7 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
   let lbl = label_of_block blk in
   let pos = skip_phis blk in
   let insts, term, blocks = xlate_instrs pop x pos in
-  Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term :: blocks
+  Llair.Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term :: blocks
   |>
   [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl]
 
@@ -1375,7 +1375,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
               trav_blocks
                 (List.rev_append (xlate_block pop x blk) rev_cfg)
                 blk
-          | At_end _ -> Vector.of_list_rev rev_cfg
+          | At_end _ -> IArray.of_list_rev rev_cfg
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
diff --git a/sledge/bin/sledge.ml b/sledge/bin/sledge.ml
index f1fa86e22..c1f88a74a 100644
--- a/sledge/bin/sledge.ml
+++ b/sledge/bin/sledge.ml
@@ -85,7 +85,7 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
     Per_function (Reg.Map.map summary_table ~f:Reg.Set.union_list)
   else
     Declared
-      (Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
+      (IArray.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
            Reg.Set.add acc g.reg ))
 
 let analyze =
diff --git a/sledge/lib/control.ml b/sledge/lib/control.ml
index 29ff8e0b7..83cce7404 100644
--- a/sledge/lib/control.ml
+++ b/sledge/lib/control.ml
@@ -328,7 +328,7 @@ module Make (Dom : Domain_intf.Dom) = struct
     let exit_state =
       match (freturn, exp) with
       | Some freturn, Some return_val ->
-          Dom.exec_move pre_state (Vector.of_ (freturn, return_val))
+          Dom.exec_move pre_state (IArray.of_ (freturn, return_val))
       | None, None -> pre_state
       | _ -> violates Llair.Func.invariant block.parent
     in
@@ -360,7 +360,7 @@ module Make (Dom : Domain_intf.Dom) = struct
     | Some (from_call, retn_site, stk, unwind_state) ->
         let fthrow = func.fthrow in
         let exit_state =
-          Dom.exec_move unwind_state (Vector.of_ (fthrow, exc))
+          Dom.exec_move unwind_state (IArray.of_ (fthrow, exc))
         in
         let post_state = Dom.post func.locals from_call exit_state in
         let retn_state =
@@ -390,7 +390,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
     match block.term with
     | Switch {key; tbl; els} ->
-        Vector.fold tbl
+        IArray.fold tbl
           ~f:(fun x (case, jump) ->
             match Dom.exec_assume state (Exp.eq key case) with
             | Some state -> exec_jump stk state block jump |> Work.seq x
@@ -398,13 +398,13 @@ module Make (Dom : Domain_intf.Dom) = struct
           ~init:
             ( match
                 Dom.exec_assume state
-                  (Vector.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) ->
+                  (IArray.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) ->
                        Exp.and_ (Exp.dq key case) b ))
               with
             | Some state -> exec_jump stk state block els
             | None -> Work.skip )
     | Iswitch {ptr; tbl} ->
-        Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
+        IArray.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
             match
               Dom.exec_assume state
                 (Exp.eq ptr
@@ -458,7 +458,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x =
    fun opts pgm stk state block ->
     [%Trace.info "exec block %%%s" block.lbl] ;
-    match Vector.fold_result ~f:exec_inst ~init:state block.cmnd with
+    match IArray.fold_result ~f:exec_inst ~init:state block.cmnd with
     | Ok state -> exec_term opts pgm stk state block
     | Error (state, inst) ->
         Report.invalid_access_inst (Dom.report_fmt_thunk state) inst ;
diff --git a/sledge/lib/domain_intf.ml b/sledge/lib/domain_intf.ml
index 0d419052b..4fb95c3be 100644
--- a/sledge/lib/domain_intf.ml
+++ b/sledge/lib/domain_intf.ml
@@ -11,13 +11,13 @@ module type Dom = sig
 
   val pp : t pp
   val report_fmt_thunk : t -> Format.formatter -> unit
-  val init : Global.t vector -> t
+  val init : Global.t iarray -> t
   val join : t -> t -> t option
   val is_false : t -> bool
   val dnf : t -> t list
   val exec_assume : t -> Exp.t -> t option
   val exec_kill : t -> Reg.t -> t
-  val exec_move : t -> (Reg.t * Exp.t) vector -> t
+  val exec_move : t -> (Reg.t * Exp.t) iarray -> t
   val exec_inst : t -> Llair.inst -> t option
 
   val exec_intrinsic :
diff --git a/sledge/lib/domain_sh.ml b/sledge/lib/domain_sh.ml
index fb1187812..0434101a1 100644
--- a/sledge/lib/domain_sh.ml
+++ b/sledge/lib/domain_sh.ml
@@ -17,7 +17,7 @@ let simplify_states = ref true
 let simplify q = if !simplify_states then Sh.simplify q else q
 
 let init globals =
-  Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
+  IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.reg; init= Some arr} ->
         let loc = Term.var (Reg.var reg) in
         let len = Term.size_of (Exp.typ arr) in
@@ -38,7 +38,7 @@ let exec_assume q b = Exec.assume q (Exp.term b) |> Option.map ~f:simplify
 let exec_kill q r = Exec.kill q (Reg.var r) |> simplify
 
 let exec_move q res =
-  Exec.move q (Vector.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))
+  Exec.move q (IArray.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))
   |> simplify
 
 let exec_inst pre inst =
@@ -46,7 +46,7 @@ let exec_inst pre inst =
   | Move {reg_exps; _} ->
       Some
         (Exec.move pre
-           (Vector.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e))))
+           (IArray.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e))))
   | Load {reg; ptr; len; _} ->
       Exec.load pre ~reg:(Reg.var reg) ~ptr:(Exp.term ptr)
         ~len:(Exp.term len)
@@ -218,7 +218,7 @@ let retn formals freturn {areturn; subst; frame} q =
         (* pass return value *)
         match freturn with
         | Some freturn ->
-            (Exec.move q (Vector.of_ (areturn, Term.var freturn)), inv_subst)
+            (Exec.move q (IArray.of_ (areturn, Term.var freturn)), inv_subst)
         | None -> (Exec.kill q areturn, inv_subst) )
     | None -> (q, inv_subst)
   in
diff --git a/sledge/lib/domain_used_globals.ml b/sledge/lib/domain_used_globals.ml
index 8f1add5eb..a6f4f8b92 100644
--- a/sledge/lib/domain_used_globals.ml
+++ b/sledge/lib/domain_used_globals.ml
@@ -14,7 +14,7 @@ let report_fmt_thunk = Fun.flip pp
 let empty = Reg.Set.empty
 
 let init globals =
-  [%Trace.info "pgm globals: {%a}" (Vector.pp ", " Global.pp) globals] ;
+  [%Trace.info "pgm globals: {%a}" (IArray.pp ", " Global.pp) globals] ;
   empty
 
 let join l r = Some (Reg.Set.union l r)
@@ -34,7 +34,7 @@ let exec_assume st exp = Some (used_globals ~init:st exp)
 let exec_kill st _ = st
 
 let exec_move st reg_exps =
-  Vector.fold reg_exps ~init:st ~f:(fun st (_, rhs) ->
+  IArray.fold reg_exps ~init:st ~f:(fun st (_, rhs) ->
       used_globals ~init:st rhs )
 
 let exec_inst st inst =
diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index cd1b2fe7b..d7ca83147 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -179,7 +179,7 @@ let orient e f =
       | Ap2 (Memory, _, x) -> 1 + height x
       | Ap3 (Extract, x, _, _) -> 1 + height x
       | ApN (Concat, xs) ->
-          1 + Vector.fold ~init:0 ~f:(fun h x -> max h (height x)) xs
+          1 + IArray.fold ~init:0 ~f:(fun h x -> max h (height x)) xs
       | _ -> 0
     in
     let o = compare (rank e) (rank f) in
@@ -237,7 +237,7 @@ let rec solve_extract ?f a o l b s =
 (* α₀^…^αᵢ^αⱼ^…^αᵥ = β ==> |α₀^…^αᵥ| = |β| ∧ … ∧ αⱼ = β[n₀+…+nᵢ,nⱼ) ∧ …
    where nₓ ≡ |αₓ| and m = |β| *)
 and solve_concat ?f a0V b m s =
-  Vector.fold_until a0V ~init:(s, Term.zero)
+  IArray.fold_until a0V ~init:(s, Term.zero)
     ~f:(fun (s, oI) aJ ->
       let nJ = Term.agg_size_exn aJ in
       let oJ = Term.add oI nJ in
diff --git a/sledge/lib/exec.ml b/sledge/lib/exec.ml
index e5783c824..58b2d32b8 100644
--- a/sledge/lib/exec.ml
+++ b/sledge/lib/exec.ml
@@ -56,13 +56,13 @@ let move_spec us reg_exps =
   let xs = Var.Set.empty in
   let foot = Sh.emp in
   let ws, rs =
-    Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
+    IArray.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
       ~f:(fun (ws, rs) (reg, exp) ->
         (Var.Set.add ws reg, Var.Set.union rs (Term.fv exp)) )
   in
   let sub, ms, _ = assign ~ws ~rs ~us in
   let post =
-    Vector.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) ->
+    IArray.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) ->
         Sh.and_ (Term.eq (Term.var reg) (Term.rename sub exp)) post )
   in
   {xs; foot; sub; ms; post}
diff --git a/sledge/lib/exec.mli b/sledge/lib/exec.mli
index 28a05b0e3..04e66ab58 100644
--- a/sledge/lib/exec.mli
+++ b/sledge/lib/exec.mli
@@ -9,7 +9,7 @@
 
 val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
-val move : Sh.t -> (Var.t * Term.t) vector -> Sh.t
+val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t
 val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option
 val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option
 val memset : Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> Sh.t option
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index 06c18d60b..be83b6615 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -74,7 +74,7 @@ module T = struct
     | Ap1 of op1 * Typ.t * t
     | Ap2 of op2 * Typ.t * t * t
     | Ap3 of op3 * Typ.t * t * t * t
-    | ApN of opN * Typ.t * t vector
+    | ApN of opN * Typ.t * t iarray
   [@@deriving compare, equal, hash, sexp]
 end
 
@@ -174,7 +174,7 @@ let rec pp fs exp =
     | Ap3 (Conditional, _, cnd, thn, els) ->
         pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
     | ApN (Record, _, elts) -> pf "{%a}" pp_record elts
-    | ApN (Struct_rec, _, elts) -> pf "{|%a|}" (Vector.pp ",@ " pp) elts
+    | ApN (Struct_rec, _, elts) -> pf "{|%a|}" (IArray.pp ",@ " pp) elts
   in
   fix_flip pp_ (fun _ _ -> ()) fs exp
   [@@warning "-9"]
@@ -184,20 +184,20 @@ and pp_record fs elts =
     fs "%a"
       (fun fs elts ->
         match
-          String.init (Vector.length elts) ~f:(fun i ->
-              match (Vector.get elts i).desc with
+          String.init (IArray.length elts) ~f:(fun i ->
+              match (IArray.get elts i).desc with
               | Integer {data} -> Char.of_int_exn (Z.to_int data)
               | _ -> raise (Invalid_argument "not a string") )
         with
         | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
         | exception _ ->
-            Format.fprintf fs "@[<h>%a@]" (Vector.pp ",@ " pp) elts )
+            Format.fprintf fs "@[<h>%a@]" (IArray.pp ",@ " pp) elts )
       elts]
   [@@warning "-9"]
 
 (** Invariant *)
 
-let valid_idx idx elts = 0 <= idx && idx < Vector.length elts
+let valid_idx idx elts = 0 <= idx && idx < IArray.length elts
 
 let rec invariant exp =
   Invariant.invariant [%here] exp [%sexp_of: t]
@@ -242,7 +242,7 @@ let rec invariant exp =
       match typ with
       | Tuple {elts} | Struct {elts} ->
           assert (valid_idx idx elts) ;
-          assert (Typ.castable (Vector.get elts idx) (typ_of elt))
+          assert (Typ.castable (IArray.get elts idx) (typ_of elt))
       | Array {elt= typ_elt} -> assert (Typ.castable typ_elt (typ_of elt))
       | _ -> assert false )
   | Ap2 (op, typ, x, y) -> (
@@ -266,12 +266,12 @@ let rec invariant exp =
     match typ with
     | Array {elt} ->
         assert (
-          Vector.for_all args ~f:(fun arg -> Typ.castable elt (typ_of arg))
+          IArray.for_all args ~f:(fun arg -> Typ.castable elt (typ_of arg))
         )
     | Tuple {elts} | Struct {elts} ->
-        assert (Vector.length elts = Vector.length args) ;
+        assert (IArray.length elts = IArray.length args) ;
         assert (
-          Vector.for_all2_exn elts args ~f:(fun typ arg ->
+          IArray.for_all2_exn elts args ~f:(fun typ arg ->
               Typ.castable typ (typ_of arg) ) )
     | _ -> assert false )
   [@@warning "-9"]
@@ -286,7 +286,7 @@ and typ_of exp =
   | Ap1 (Select idx, typ, _) -> (
     match typ with
     | Array {elt} -> elt
-    | Tuple {elts} | Struct {elts} -> Vector.get elts idx
+    | Tuple {elts} | Struct {elts} -> IArray.get elts idx
     | _ -> violates invariant exp )
   | Ap2
       ( (Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Ord | Uno)
@@ -466,7 +466,7 @@ let splat typ byt =
 
 let record typ elts =
   { desc= ApN (Record, typ, elts)
-  ; term= Term.record (Vector.map ~f:(fun elt -> elt.term) elts) }
+  ; term= Term.record (IArray.map ~f:(fun elt -> elt.term) elts) }
   |> check invariant
 
 let select typ rcd idx =
@@ -486,13 +486,13 @@ let struct_rec key =
     | None ->
         (* Add placeholder to prevent computing [elts] in calls to
            [struct_rec] from [elt_thks] for recursive occurrences of [id]. *)
-        let elta = Array.create ~len:(Vector.length elt_thks) null in
-        let elts = Vector.of_array elta in
+        let elta = Array.create ~len:(IArray.length elt_thks) null in
+        let elts = IArray.of_array elta in
         Hashtbl.set memo_id ~key:id ~data:elts ;
         let term =
-          rec_app ~id (Vector.map ~f:(fun elt -> lazy elt.term) elts)
+          rec_app ~id (IArray.map ~f:(fun elt -> lazy elt.term) elts)
         in
-        Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+        IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
         {desc= ApN (Struct_rec, typ, elts); term} |> check invariant
     | Some elts ->
         (* Do not check invariant as invariant will be checked above after
@@ -501,7 +501,7 @@ let struct_rec key =
            constructed here shares the array in the memo table, so that the
            update after forcing the recursive thunks also updates this
            value. *)
-        {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id Vector.empty}
+        {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id IArray.empty}
 
 let size_of exp = integer Typ.siz (Z.of_int (Typ.size_of (typ exp)))
 
@@ -515,7 +515,7 @@ let fold_exps e ~init ~f =
       | Ap2 (_, _, x, y) -> fold_exps_ y (fold_exps_ x z)
       | Ap3 (_, _, w, x, y) -> fold_exps_ w (fold_exps_ y (fold_exps_ x z))
       | ApN (_, _, xs) ->
-          Vector.fold xs ~init:z ~f:(fun z elt -> fold_exps_ elt z)
+          IArray.fold xs ~init:z ~f:(fun z elt -> fold_exps_ elt z)
       | _ -> z
     in
     f z e
diff --git a/sledge/lib/exp.mli b/sledge/lib/exp.mli
index d7a76cc80..1f4ca615e 100644
--- a/sledge/lib/exp.mli
+++ b/sledge/lib/exp.mli
@@ -87,7 +87,7 @@ and desc = private
   | Ap1 of op1 * Typ.t * t
   | Ap2 of op2 * Typ.t * t * t
   | Ap3 of op3 * Typ.t * t * t * t
-  | ApN of opN * Typ.t * t vector
+  | ApN of opN * Typ.t * t iarray
 [@@deriving compare, equal, hash, sexp]
 
 val pp : t pp
@@ -183,7 +183,7 @@ val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t
 val splat : Typ.t -> t -> t
 
 (* records (struct / array values) *)
-val record : Typ.t -> t vector -> t
+val record : Typ.t -> t iarray -> t
 val select : Typ.t -> t -> int -> t
 val update : Typ.t -> rcd:t -> int -> elt:t -> t
 
@@ -191,7 +191,7 @@ val struct_rec :
      (module Hashtbl.Key.S with type t = 'id)
   -> id:'id
   -> Typ.t
-  -> t lazy_t vector
+  -> t lazy_t iarray
   -> t
 (** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
     value. Cycles are detected using [Id]. The caller of [struct_rec Id]
diff --git a/sledge/lib/import/vector.ml b/sledge/lib/import/IArray.ml
similarity index 97%
rename from sledge/lib/import/vector.ml
rename to sledge/lib/import/IArray.ml
index 531be5c4f..12dacd1be 100644
--- a/sledge/lib/import/vector.ml
+++ b/sledge/lib/import/IArray.ml
@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Vector - Immutable view of an array *)
+(** IArray - Immutable view of an array *)
 
 module Array = Base.Array
 module Hash = Base.Hash
@@ -26,7 +26,7 @@ let t_of_sexp a_of_sexp s = v (Array.t_of_sexp a_of_sexp s)
 let sexp_of_t sexp_of_a x = Array.sexp_of_t sexp_of_a (a x)
 
 module Infix = struct
-  type +'a vector = 'a t [@@deriving compare, equal, hash, sexp]
+  type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
 let to_list x = Array.to_list (a x)
diff --git a/sledge/lib/import/vector.mli b/sledge/lib/import/IArray.mli
similarity index 97%
rename from sledge/lib/import/vector.mli
rename to sledge/lib/import/IArray.mli
index 66939b8f4..f9d23cc55 100644
--- a/sledge/lib/import/vector.mli
+++ b/sledge/lib/import/IArray.mli
@@ -5,10 +5,10 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Vector - Immutable view of an array
+(** IArray - Immutable view of an array
 
     Note that vectors and arrays can be interconverted without copying. So
-    Vector is not a safe immutable data structure, it only attempts to make
+    IArray is not a safe immutable data structure, it only attempts to make
     it inconvenient to mutate. *)
 
 open Import0
@@ -16,7 +16,7 @@ open Import0
 type +'a t [@@deriving compare, equal, hash, sexp]
 
 module Infix : sig
-  type +'a vector = 'a t [@@deriving compare, equal, hash, sexp]
+  type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
 val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
diff --git a/sledge/lib/import/import.ml b/sledge/lib/import/import.ml
index ffef8a938..79515663f 100644
--- a/sledge/lib/import/import.ml
+++ b/sledge/lib/import/import.ml
@@ -172,8 +172,8 @@ module Array = struct
   let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
 end
 
-module Vector = Vector
-include Vector.Infix
+module IArray = IArray
+include IArray.Infix
 module List = List
 
 type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
diff --git a/sledge/lib/import/import.mli b/sledge/lib/import/import.mli
index cc25447a5..b9df250bd 100644
--- a/sledge/lib/import/import.mli
+++ b/sledge/lib/import/import.mli
@@ -153,8 +153,8 @@ module Array : sig
   val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
 end
 
-module Vector = Vector
-include module type of Vector.Infix
+module IArray = IArray
+include module type of IArray.Infix
 module List = List
 
 type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
diff --git a/sledge/lib/import/set.ml b/sledge/lib/import/set.ml
index 783975da5..32f168a0e 100644
--- a/sledge/lib/import/set.ml
+++ b/sledge/lib/import/set.ml
@@ -32,7 +32,7 @@ module Make (Elt : OrderedType) : S with type elt = Elt.t = struct
   let of_ x = S.add x empty
   let of_option = Option.fold ~f:(fun x y -> S.add y x) ~init:empty
   let of_list = S.of_list
-  let of_vector x = S.of_list (Vector.to_list x)
+  let of_vector x = S.of_list (IArray.to_list x)
   let add s e = S.add e s
   let add_option yo x = Option.fold ~f:(fun x y -> S.add y x) ~init:x yo
   let add_list ys x = List.fold ~f:(fun x y -> S.add y x) ~init:x ys
diff --git a/sledge/lib/import/set_intf.ml b/sledge/lib/import/set_intf.ml
index 8709f100f..29b98cb6a 100644
--- a/sledge/lib/import/set_intf.ml
+++ b/sledge/lib/import/set_intf.ml
@@ -23,7 +23,7 @@ module type S = sig
   val of_ : elt -> t
   val of_option : elt option -> t
   val of_list : elt list -> t
-  val of_vector : elt Vector.t -> t
+  val of_vector : elt IArray.t -> t
 
   (* constructors *)
   val add : t -> elt -> t
diff --git a/sledge/lib/llair.ml b/sledge/lib/llair.ml
index db11fceec..3b6e00d7c 100644
--- a/sledge/lib/llair.ml
+++ b/sledge/lib/llair.ml
@@ -10,7 +10,7 @@
 [@@@warning "+9"]
 
 type inst =
-  | Move of {reg_exps: (Reg.t * Exp.t) vector; loc: Loc.t}
+  | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
   | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
   | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t}
   | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
@@ -22,7 +22,7 @@ type inst =
   | Abort of {loc: Loc.t}
 [@@deriving sexp]
 
-type cmnd = inst vector [@@deriving sexp]
+type cmnd = inst iarray [@@deriving sexp]
 type label = string [@@deriving sexp]
 
 type jump = {mutable dst: block; mutable retreating: bool}
@@ -38,8 +38,8 @@ and 'a call =
   ; loc: Loc.t }
 
 and term =
-  | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}
-  | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
+  | Switch of {key: Exp.t; tbl: (Exp.t * jump) iarray; els: jump; loc: Loc.t}
+  | Iswitch of {ptr: Exp.t; tbl: jump iarray; loc: Loc.t}
   | Call of Exp.t call
   | Return of {exp: Exp.t option; loc: Loc.t}
   | Throw of {exc: Exp.t; loc: Loc.t}
@@ -74,9 +74,9 @@ let sexp_of_term = function
   | Switch {key; tbl; els; loc} ->
       sexp_ctor "Switch"
         [%sexp
-          {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}]
+          {key: Exp.t; tbl: (Exp.t * jump) iarray; els: jump; loc: Loc.t}]
   | Iswitch {ptr; tbl; loc} ->
-      sexp_ctor "Iswitch" [%sexp {ptr: Exp.t; tbl: jump vector; loc: Loc.t}]
+      sexp_ctor "Iswitch" [%sexp {ptr: Exp.t; tbl: jump iarray; loc: Loc.t}]
   | Call {callee; typ; actuals; areturn; return; throw; recursive; loc} ->
       sexp_ctor "Call"
         [%sexp
@@ -116,16 +116,16 @@ let equal_block x y = Int.equal x.sort_index y.sort_index
 
 type functions = func String.Map.t [@@deriving sexp_of]
 
-type t = {globals: Global.t vector; functions: functions}
+type t = {globals: Global.t iarray; functions: functions}
 [@@deriving sexp_of]
 
 let pp_inst fs inst =
   let pf pp = Format.fprintf fs pp in
   match inst with
   | Move {reg_exps; loc} ->
-      let regs, exps = Vector.unzip reg_exps in
-      pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Reg.pp) regs
-        (Vector.pp ",@ " Exp.pp) exps Loc.pp loc
+      let regs, exps = IArray.unzip reg_exps in
+      pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (IArray.pp ",@ " Reg.pp) regs
+        (IArray.pp ",@ " Exp.pp) exps Loc.pp loc
   | Load {reg; ptr; len; loc} ->
       pf "@[<2>%a@ := load %a@ %a;@]\t%a" Reg.pp reg Exp.pp len Exp.pp ptr
         Loc.pp loc
@@ -167,19 +167,19 @@ let pp_term fs term =
   let pp_goto fs jmp = Format.fprintf fs "goto %a;" pp_jump jmp in
   match term with
   | Switch {key; tbl; els; loc} -> (
-    match Vector.to_array tbl with
+    match IArray.to_array tbl with
     | [||] -> pf "@[%a@]\t%a" pp_goto els Loc.pp loc
     | [|(z, jmp)|] when Exp.is_false z ->
         pf "@[if %a@;<1 2>%a@ @[else@;<1 2>%a@]@]\t%a" Exp.pp key pp_goto
           els pp_goto jmp Loc.pp loc
     | _ ->
         pf "@[<2>switch %a@ @[%a@ else: %a@]@]\t%a" Exp.pp key
-          (Vector.pp "@ " (fun fs (case, jmp) ->
+          (IArray.pp "@ " (fun fs (case, jmp) ->
                Format.fprintf fs "%a: %a" Exp.pp case pp_goto jmp ))
           tbl pp_goto els Loc.pp loc )
   | Iswitch {ptr; tbl; loc} ->
       pf "@[<2>iswitch %a@ @[<hv>%a@]@]\t%a" Exp.pp ptr
-        (Vector.pp "@ " (fun fs jmp ->
+        (IArray.pp "@ " (fun fs jmp ->
              Format.fprintf fs "%s: %a" jmp.dst.lbl pp_goto jmp ))
         tbl Loc.pp loc
   | Call {callee; actuals; areturn; return; throw; recursive; loc; _} ->
@@ -195,19 +195,19 @@ let pp_term fs term =
   | Throw {exc; loc} -> pf "@[<2>throw %a@]\t%a" Exp.pp exc Loc.pp loc
   | Unreachable -> pf "unreachable"
 
-let pp_cmnd = Vector.pp "@ " pp_inst
+let pp_cmnd = IArray.pp "@ " pp_inst
 
 let pp_block fs {lbl; cmnd; term; parent= _; sort_index} =
   Format.fprintf fs "@[<v 2>%%%s: #%i@ @[<v>%a%t%a@]@]" lbl sort_index
     pp_cmnd cmnd
-    (fun fs -> if Vector.is_empty cmnd then () else Format.fprintf fs "@ ")
+    (fun fs -> if IArray.is_empty cmnd then () else Format.fprintf fs "@ ")
     pp_term term
 
 (** Initial cyclic values *)
 
 let rec dummy_block =
   { lbl= "dummy"
-  ; cmnd= Vector.empty
+  ; cmnd= IArray.empty
   ; term= Unreachable
   ; parent= dummy_func
   ; sort_index= 0 }
@@ -254,7 +254,7 @@ module Inst = struct
   let union_locals inst vs =
     match inst with
     | Move {reg_exps; _} ->
-        Vector.fold
+        IArray.fold
           ~f:(fun vs (reg, _) -> Reg.Set.add vs reg)
           ~init:vs reg_exps
     | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
@@ -269,7 +269,7 @@ module Inst = struct
   let fold_exps inst ~init ~f =
     match inst with
     | Move {reg_exps; loc= _} ->
-        Vector.fold reg_exps ~init ~f:(fun acc (_reg, exp) -> f acc exp)
+        IArray.fold reg_exps ~init ~f:(fun acc (_reg, exp) -> f acc exp)
     | Load {reg= _; ptr; len; loc= _} -> f (f init ptr) len
     | Store {ptr; exp; len; loc= _} -> f (f (f init ptr) exp) len
     | Memset {dst; byt; len; loc= _} -> f (f (f init dst) byt) len
@@ -307,7 +307,7 @@ module Term = struct
     | Call {typ; actuals; areturn; _} -> (
       match typ with
       | Pointer {elt= Function {args; return= retn_typ; _}} ->
-          assert (Vector.length args = List.length actuals) ;
+          assert (IArray.length args = List.length actuals) ;
           assert (Option.is_some retn_typ || Option.is_none areturn)
       | _ -> assert false )
     | Return {exp; _} -> (
@@ -318,11 +318,11 @@ module Term = struct
     | Throw _ | Unreachable -> assert true
 
   let goto ~dst ~loc =
-    Switch {key= Exp.false_; tbl= Vector.empty; els= dst; loc}
+    Switch {key= Exp.false_; tbl= IArray.empty; els= dst; loc}
     |> check invariant
 
   let branch ~key ~nzero ~zero ~loc =
-    let tbl = Vector.of_array [|(Exp.false_, zero)|] in
+    let tbl = IArray.of_array [|(Exp.false_, zero)|] in
     let els = nzero in
     Switch {key; tbl; els; loc} |> check invariant
 
@@ -398,7 +398,7 @@ module Func = struct
   type t = func [@@deriving sexp_of]
 
   let is_undefined = function
-    | {entry= {cmnd; term= Unreachable; _}; _} -> Vector.is_empty cmnd
+    | {entry= {cmnd; term= Unreachable; _}; _} -> IArray.is_empty cmnd
     | _ -> false
 
   let fold_cfg ~init ~f func =
@@ -410,9 +410,9 @@ module Func = struct
           let f s j = fold_cfg_ s j.dst in
           match blk.term with
           | Switch {tbl; els; _} ->
-              let s = Vector.fold ~f:(fun s (_, j) -> f s j) ~init:s tbl in
+              let s = IArray.fold ~f:(fun s (_, j) -> f s j) ~init:s tbl in
               f s els
-          | Iswitch {tbl; _} -> Vector.fold ~f ~init:s tbl
+          | Iswitch {tbl; _} -> IArray.fold ~f ~init:s tbl
           | Call {return; throw; _} ->
               let s = f s return in
               Option.fold ~f ~init:s throw
@@ -472,40 +472,40 @@ module Func = struct
   let mk ~(name : Global.t) ~formals ~freturn ~fthrow ~entry ~cfg =
     let locals =
       let locals_cmnd locals cmnd =
-        Vector.fold_right ~f:Inst.union_locals cmnd ~init:locals
+        IArray.fold_right ~f:Inst.union_locals cmnd ~init:locals
       in
       let locals_block locals block =
         locals_cmnd (Term.union_locals block.term locals) block.cmnd
       in
       let init = locals_block Reg.Set.empty entry in
-      Vector.fold ~f:locals_block cfg ~init
+      IArray.fold ~f:locals_block cfg ~init
     in
     let func = {name; formals; freturn; fthrow; locals; entry} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
-        Vector.find_exn cfg ~f:(fun k -> String.equal lbl k.lbl)
+        IArray.find_exn cfg ~f:(fun k -> String.equal lbl k.lbl)
       in
       let set_dst jmp = jmp.dst <- lookup cfg jmp.dst.lbl in
       match block.term with
       | Switch {tbl; els; _} ->
-          Vector.iter tbl ~f:(fun (_, jmp) -> set_dst jmp) ;
+          IArray.iter tbl ~f:(fun (_, jmp) -> set_dst jmp) ;
           set_dst els
-      | Iswitch {tbl; _} -> Vector.iter tbl ~f:set_dst
+      | Iswitch {tbl; _} -> IArray.iter tbl ~f:set_dst
       | Call {return; throw; _} ->
           set_dst return ;
           Option.iter throw ~f:set_dst
       | Return _ | Throw _ | Unreachable -> ()
     in
     resolve_parent_and_jumps entry ;
-    Vector.iter cfg ~f:resolve_parent_and_jumps ;
+    IArray.iter cfg ~f:resolve_parent_and_jumps ;
     func |> check invariant
 
   let mk_undefined ~name ~formals ~freturn ~fthrow =
     let entry =
-      Block.mk ~lbl:"" ~cmnd:Vector.empty ~term:Term.unreachable
+      Block.mk ~lbl:"" ~cmnd:IArray.empty ~term:Term.unreachable
     in
-    let cfg = Vector.empty in
+    let cfg = IArray.empty in
     mk ~name ~entry ~formals ~freturn ~fthrow ~cfg
 end
 
@@ -539,9 +539,9 @@ let set_derived_metadata functions =
         in
         ( match src.term with
         | Switch {tbl; els; _} ->
-            Vector.iter tbl ~f:(fun (_, jmp) -> jump jmp) ;
+            IArray.iter tbl ~f:(fun (_, jmp) -> jump jmp) ;
             jump els
-        | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump
+        | Iswitch {tbl; _} -> IArray.iter tbl ~f:jump
         | Call ({callee; return; throw; _} as call) ->
             ( match
                 Option.bind ~f:(Func.find functions)
@@ -582,17 +582,17 @@ let invariant pgm =
   @@ fun () ->
   assert (
     not
-      (Vector.contains_dup pgm.globals ~compare:(fun g1 g2 ->
+      (IArray.contains_dup pgm.globals ~compare:(fun g1 g2 ->
            Reg.compare g1.Global.reg g2.Global.reg )) )
 
 let mk ~globals ~functions =
-  { globals= Vector.of_list_rev globals
+  { globals= IArray.of_list_rev globals
   ; functions= set_derived_metadata functions }
   |> check invariant
 
 let pp fs {globals; functions} =
   Format.fprintf fs "@[<v>@[%a@]@ @ @ @[%a@]@]"
-    (Vector.pp "@\n@\n" Global.pp_defn)
+    (IArray.pp "@\n@\n" Global.pp_defn)
     globals
     (List.pp "@\n@\n" Func.pp)
     ( String.Map.data functions
diff --git a/sledge/lib/llair.mli b/sledge/lib/llair.mli
index 20363dd53..9cfff18e7 100644
--- a/sledge/lib/llair.mli
+++ b/sledge/lib/llair.mli
@@ -10,7 +10,7 @@
 
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
-  | Move of {reg_exps: (Reg.t * Exp.t) vector; loc: Loc.t}
+  | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
       (** Move each value [exp] into corresponding register [reg]. All of
           the moves take effect simultaneously. *)
   | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
@@ -36,7 +36,7 @@ type inst = private
   | Abort of {loc: Loc.t}  (** Trigger abnormal program termination *)
 
 (** A (straight-line) command is a sequence of instructions. *)
-type cmnd = inst vector
+type cmnd = inst iarray
 
 (** A label is a name of a block. *)
 type label = string
@@ -58,10 +58,10 @@ and 'a call =
 
 (** Block terminators for function call/return or other control transfers. *)
 and term = private
-  | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}
+  | Switch of {key: Exp.t; tbl: (Exp.t * jump) iarray; els: jump; loc: Loc.t}
       (** Invoke the [jump] in [tbl] associated with the integer expression
           [case] which is equal to [key], if any, otherwise invoke [els]. *)
-  | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
+  | Iswitch of {ptr: Exp.t; tbl: jump iarray; loc: Loc.t}
       (** Invoke the [jump] in [tbl] whose [dst] is equal to [ptr]. *)
   | Call of Exp.t call
       (** Call function with arguments. A [global] for non-virtual call. *)
@@ -96,7 +96,7 @@ and func = private
 type functions
 
 type t = private
-  { globals: Global.t vector  (** Global variable definitions. *)
+  { globals: Global.t iarray  (** Global variable definitions. *)
   ; functions: functions  (** (Global) function definitions. *) }
 
 val pp : t pp
@@ -109,7 +109,7 @@ module Inst : sig
   type t = inst
 
   val pp : t pp
-  val move : reg_exps:(Reg.t * Exp.t) vector -> loc:Loc.t -> inst
+  val move : reg_exps:(Reg.t * Exp.t) iarray -> loc:Loc.t -> inst
   val load : reg:Reg.t -> ptr:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val store : ptr:Exp.t -> exp:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memset : dst:Exp.t -> byt:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
@@ -143,9 +143,9 @@ module Term : sig
   (** Construct a [Switch] representing a conditional branch. *)
 
   val switch :
-    key:Exp.t -> tbl:(Exp.t * jump) vector -> els:jump -> loc:Loc.t -> term
+    key:Exp.t -> tbl:(Exp.t * jump) iarray -> els:jump -> loc:Loc.t -> term
 
-  val iswitch : ptr:Exp.t -> tbl:jump vector -> loc:Loc.t -> term
+  val iswitch : ptr:Exp.t -> tbl:jump iarray -> loc:Loc.t -> term
 
   val call :
        callee:Exp.t
@@ -185,7 +185,7 @@ module Func : sig
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> entry:block
-    -> cfg:block vector
+    -> cfg:block iarray
     -> func
 
   val mk_undefined :
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 7375a4587..f33541d4c 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -64,8 +64,8 @@ and T : sig
     | Ap1 of op1 * t
     | Ap2 of op2 * t * t
     | Ap3 of op3 * t * t * t
-    | ApN of opN * t vector
-    | RecN of recN * t vector  (** NOTE: cyclic *)
+    | ApN of opN * t iarray
+    | RecN of recN * t iarray  (** NOTE: cyclic *)
     | Label of {parent: string; name: string}
     | Nondet of {msg: string}
     | Float of {data: string}
@@ -81,8 +81,8 @@ end = struct
     | Ap1 of op1 * t
     | Ap2 of op2 * t * t
     | Ap3 of op3 * t * t * t
-    | ApN of opN * t vector
-    | RecN of recN * t vector  (** NOTE: cyclic *)
+    | ApN of opN * t iarray
+    | RecN of recN * t iarray  (** NOTE: cyclic *)
     | Label of {parent: string; name: string}
     | Nondet of {msg: string}
     | Float of {data: string}
@@ -183,10 +183,10 @@ let rec ppx strength fs term =
     | Ap3 (Extract, agg, off, len) -> pf "%a[%a,%a)" pp agg pp off pp len
     | Ap1 (Splat, byt) -> pf "%a^" pp byt
     | Ap2 (Memory, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
-    | ApN (Concat, args) when Vector.is_empty args -> pf "@<2>⟨⟩"
-    | ApN (Concat, args) -> pf "(%a)" (Vector.pp "@,^" pp) args
+    | ApN (Concat, args) when IArray.is_empty args -> pf "@<2>⟨⟩"
+    | ApN (Concat, args) -> pf "(%a)" (IArray.pp "@,^" pp) args
     | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts
-    | RecN (Record, elts) -> pf "{|%a|}" (Vector.pp ",@ " pp) elts
+    | RecN (Record, elts) -> pf "{|%a|}" (IArray.pp ",@ " pp) elts
     | Ap1 (Select idx, rcd) -> pf "%a[%i]" pp rcd idx
     | Ap2 (Update idx, rcd, elt) ->
         pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
@@ -199,15 +199,15 @@ and pp_record strength fs elts =
     fs "%a"
       (fun fs elts ->
         match
-          String.init (Vector.length elts) ~f:(fun i ->
-              match Vector.get elts i with
+          String.init (IArray.length elts) ~f:(fun i ->
+              match IArray.get elts i with
               | Integer {data} -> Char.of_int_exn (Z.to_int data)
               | _ -> raise (Invalid_argument "not a string") )
         with
         | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
         | exception _ ->
             Format.fprintf fs "@[<h>%a@]"
-              (Vector.pp ",@ " (ppx strength))
+              (IArray.pp ",@ " (ppx strength))
               elts )
       elts]
 
@@ -270,8 +270,8 @@ let rec assert_aggregate = function
   | Ap2 (Memory, _, _) -> ()
   | Ap3 (Extract, a, _, _) -> assert_aggregate a
   | ApN (Concat, a0N) ->
-      assert (Vector.length a0N <> 1) ;
-      Vector.iter ~f:assert_aggregate a0N
+      assert (IArray.length a0N <> 1) ;
+      IArray.iter ~f:assert_aggregate a0N
   | _ -> assert false
 
 let invariant e =
@@ -283,7 +283,7 @@ let invariant e =
   | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       assert_aggregate e
   | ApN (Record, elts) | RecN (Record, elts) ->
-      assert (not (Vector.is_empty elts))
+      assert (not (IArray.is_empty elts))
   | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false
   | Ap1 (Convert {src; dst}, _) ->
       assert (Typ.convertible src dst) ;
@@ -600,7 +600,7 @@ let simp_cond cnd thn els =
 let rec agg_size_exn = function
   | Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n
   | ApN (Concat, a0U) ->
-      Vector.fold a0U ~init:zero ~f:(fun a0I aJ ->
+      IArray.fold a0U ~init:zero ~f:(fun a0I aJ ->
           simp_add2 a0I (agg_size_exn aJ) )
   | _ -> invalid_arg "agg_size_exn"
 
@@ -653,7 +653,7 @@ let rec simp_or x y =
 
 (* memory *)
 
-let empty_agg = ApN (Concat, Vector.of_array [||])
+let empty_agg = ApN (Concat, IArray.of_array [||])
 let simp_splat byt = Ap1 (Splat, byt)
 
 let simp_memory siz arr =
@@ -712,7 +712,7 @@ let rec simp_extract agg off len =
     | ApN (Concat, na1N) -> (
       match len with
       | Integer {data= l} ->
-          Vector.fold_map_until na1N ~init:(l, off)
+          IArray.fold_map_until na1N ~init:(l, off)
             ~f:(fun (l, oI) naI ->
               let nI = agg_size_exn naI in
               if Z.equal Z.zero l then
@@ -739,14 +739,14 @@ and simp_concat xs =
   (* (α^(β^γ)^δ) ==> (α^β^γ^δ) *)
   let flatten xs =
     let exists_sub_Concat =
-      Vector.exists ~f:(function ApN (Concat, _) -> true | _ -> false)
+      IArray.exists ~f:(function ApN (Concat, _) -> true | _ -> false)
     in
     let concat_sub_Concat xs =
-      Vector.concat
-        (Vector.fold_right xs ~init:[] ~f:(fun x s ->
+      IArray.concat
+        (IArray.fold_right xs ~init:[] ~f:(fun x s ->
              match x with
              | ApN (Concat, ys) -> ys :: s
-             | x -> Vector.of_array [|x|] :: s ))
+             | x -> IArray.of_array [|x|] :: s ))
     in
     if exists_sub_Concat xs then concat_sub_Concat xs else xs
   in
@@ -766,8 +766,8 @@ and simp_concat xs =
     | _ -> None
   in
   let xs = flatten xs in
-  let xs = Vector.map_adjacent empty_agg xs ~f:simp_adjacent in
-  (if Vector.length xs = 1 then Vector.get xs 0 else ApN (Concat, xs))
+  let xs = IArray.map_adjacent empty_agg xs ~f:simp_adjacent in
+  (if IArray.length xs = 1 then IArray.get xs 0 else ApN (Concat, xs))
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
@@ -808,18 +808,18 @@ let rec simp_eq x y =
         simp_cond c (simp_eq e t) (simp_eq e f)
     (* α^β^δ = α^γ^δ ==> β = γ *)
     | ApN (Concat, a), ApN (Concat, b) ->
-        let m = Vector.length a in
-        let n = Vector.length b in
+        let m = IArray.length a in
+        let n = IArray.length b in
         let length_common_prefix =
           let rec find_lcp i =
-            if equal (Vector.get a i) (Vector.get b i) then find_lcp (i + 1)
+            if equal (IArray.get a i) (IArray.get b i) then find_lcp (i + 1)
             else i
           in
           find_lcp 0
         in
         let length_common_suffix =
           let rec find_lcs i =
-            if equal (Vector.get a (m - 1 - i)) (Vector.get b (n - 1 - i))
+            if equal (IArray.get a (m - 1 - i)) (IArray.get b (n - 1 - i))
             then find_lcs (i + 1)
             else i
           in
@@ -829,8 +829,8 @@ let rec simp_eq x y =
         if length_common = 0 then Ap2 (Eq, x, y)
         else
           let pos = length_common_prefix in
-          let a = Vector.sub ~pos ~len:(m - length_common) a in
-          let b = Vector.sub ~pos ~len:(n - length_common) b in
+          let a = IArray.sub ~pos ~len:(m - length_common) a in
+          let b = IArray.sub ~pos ~len:(n - length_common) b in
           simp_eq (simp_concat a) (simp_concat b)
     | ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
       , (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
@@ -939,10 +939,10 @@ let rec_app key =
     | None ->
         (* Add placeholder to prevent computing [elts] in calls to [rec_app]
            from [elt_thks] for recursive occurrences of [id]. *)
-        let elta = Array.create ~len:(Vector.length elt_thks) dummy in
-        let elts = Vector.of_array elta in
+        let elta = Array.create ~len:(IArray.length elt_thks) dummy in
+        let elts = IArray.of_array elta in
         Hashtbl.set memo_id ~key:id ~data:elts ;
-        Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+        IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
         RecN (op, elts) |> check invariant
     | Some elts ->
         (* Do not check invariant as invariant will be checked above after
@@ -1024,7 +1024,7 @@ let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els
 let splat byt = norm1 Splat byt
 let memory ~siz ~arr = norm2 Memory siz arr
 let extract ~agg ~off ~len = norm3 Extract agg off len
-let concat xs = normN Concat (Vector.of_array xs)
+let concat xs = normN Concat (IArray.of_array xs)
 let record elts = normN Record elts
 let select ~rcd ~idx = norm1 (Select idx) rcd
 let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
@@ -1053,7 +1053,7 @@ let map e ~f =
     if x' == x && y' == y && z' == z then e else norm3 op x' y' z'
   in
   let mapN op ~f xs =
-    let xs' = Vector.map_preserving_phys_equal ~f xs in
+    let xs' = IArray.map_preserving_phys_equal ~f xs in
     if xs' == xs then e else normN op xs'
   in
   let map_qset mk ~f args =
@@ -1069,7 +1069,7 @@ let map e ~f =
   | ApN (op, xs) -> mapN op ~f xs
   | RecN (_, xs) ->
       assert (
-        xs == Vector.map_preserving_phys_equal ~f xs
+        xs == IArray.map_preserving_phys_equal ~f xs
         || fail "Term.map does not support updating subterms of RecN." () ) ;
       e
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> e
@@ -1089,11 +1089,11 @@ let map_rec_pre ~f e =
       | RecN (op, xs) -> (
         match List.Assoc.find ~equal:( == ) memo e with
         | None ->
-            let xs' = Vector.copy xs in
+            let xs' = IArray.copy xs in
             let e' = RecN (op, xs') in
             let memo = List.Assoc.add ~equal:( == ) memo e e' in
             let changed = ref false in
-            Vector.map_inplace xs' ~f:(fun x ->
+            IArray.map_inplace xs' ~f:(fun x ->
                 let x' = map_rec_pre_f memo x in
                 if x' != x then changed := true ;
                 x' ) ;
@@ -1115,7 +1115,7 @@ let iter e ~f =
   | Ap1 (_, x) -> f x
   | Ap2 (_, x, y) -> f x ; f y
   | Ap3 (_, x, y, z) -> f x ; f y ; f z
-  | ApN (_, xs) | RecN (_, xs) -> Vector.iter ~f xs
+  | ApN (_, xs) | RecN (_, xs) -> IArray.iter ~f xs
   | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> ()
 
@@ -1124,7 +1124,7 @@ let exists e ~f =
   | Ap1 (_, x) -> f x
   | Ap2 (_, x, y) -> f x || f y
   | Ap3 (_, x, y, z) -> f x || f y || f z
-  | ApN (_, xs) | RecN (_, xs) -> Vector.exists ~f xs
+  | ApN (_, xs) | RecN (_, xs) -> IArray.exists ~f xs
   | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> false
 
@@ -1134,7 +1134,7 @@ let fold e ~init:s ~f =
   | Ap2 (_, x, y) -> f y (f x s)
   | Ap3 (_, x, y, z) -> f z (f y (f x s))
   | ApN (_, xs) | RecN (_, xs) ->
-      Vector.fold ~f:(fun s x -> f x s) xs ~init:s
+      IArray.fold ~f:(fun s x -> f x s) xs ~init:s
   | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> s
 
@@ -1146,7 +1146,7 @@ let fold_terms e ~init ~f =
       | Ap2 (_, x, y) -> fold_terms_ y (fold_terms_ x s)
       | Ap3 (_, x, y, z) -> fold_terms_ z (fold_terms_ y (fold_terms_ x s))
       | ApN (_, xs) | RecN (_, xs) ->
-          Vector.fold ~f:(fun s x -> fold_terms_ x s) xs ~init:s
+          IArray.fold ~f:(fun s x -> fold_terms_ x s) xs ~init:s
       | Add args | Mul args ->
           Qset.fold args ~init:s ~f:(fun arg _ s -> fold_terms_ arg s)
       | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> s
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index 71bb6a822..b952d945b 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -78,8 +78,8 @@ and T : sig
     | Ap1 of op1 * t  (** Unary application *)
     | Ap2 of op2 * t * t  (** Binary application *)
     | Ap3 of op3 * t * t * t  (** Ternary application *)
-    | ApN of opN * t vector  (** N-ary application *)
-    | RecN of recN * t vector
+    | ApN of opN * t iarray  (** N-ary application *)
+    | RecN of recN * t iarray
         (** Recursive n-ary application, may recursively refer to itself
             (transitively) from its args. NOTE: represented by cyclic
             values. *)
@@ -214,7 +214,7 @@ val concat : t array -> t
 val eq_concat : t * t -> (t * t) array -> t
 
 (* records (struct / array values) *)
-val record : t vector -> t
+val record : t iarray -> t
 val select : rcd:t -> idx:int -> t
 val update : rcd:t -> idx:int -> elt:t -> t
 
@@ -223,7 +223,7 @@ val rec_app :
      (module Hashtbl.Key.S with type t = 'id)
   -> id:'id
   -> recN
-  -> t lazy_t vector
+  -> t lazy_t iarray
   -> t
 
 val size_of : Typ.t -> t
diff --git a/sledge/lib/typ.ml b/sledge/lib/typ.ml
index c8bd6a658..1840b8b12 100644
--- a/sledge/lib/typ.ml
+++ b/sledge/lib/typ.ml
@@ -8,15 +8,15 @@
 (** Types *)
 
 type t =
-  | Function of {return: t option; args: t vector}
+  | Function of {return: t option; args: t iarray}
   | Integer of {bits: int; byts: int}
   | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]}
   | Pointer of {elt: t}
   | Array of {elt: t; len: int; bits: int; byts: int}
-  | Tuple of {elts: t vector; bits: int; byts: int; packed: bool}
+  | Tuple of {elts: t iarray; bits: int; byts: int; packed: bool}
   | Struct of
       { name: string
-      ; elts: t vector (* possibly cyclic, name unique *)
+      ; elts: t iarray (* possibly cyclic, name unique *)
             [@compare.ignore] [@equal.ignore] [@sexp_drop_if fun _ -> true]
       ; bits: int
       ; byts: int
@@ -48,7 +48,7 @@ let rec pp fs typ =
       pf "%s @[%a@] %s" opn pps elts cls
   | Struct {name} | Opaque {name} -> pf "%%%s" name
 
-and pps fs typs = Vector.pp ",@ " pp fs typs
+and pps fs typs = IArray.pp ",@ " pp fs typs
 
 let pp_defn fs = function
   | Struct {name; elts; packed} ->
@@ -70,9 +70,9 @@ let invariant t =
   match t with
   | Function {return; args} ->
       assert (Option.for_all ~f:is_sized return) ;
-      assert (Vector.for_all ~f:is_sized args)
+      assert (IArray.for_all ~f:is_sized args)
   | Array {elt} -> assert (is_sized elt)
-  | Tuple {elts} | Struct {elts} -> assert (Vector.for_all ~f:is_sized elts)
+  | Tuple {elts} | Struct {elts} -> assert (IArray.for_all ~f:is_sized elts)
   | Integer {bits} | Float {bits} -> assert (bits > 0)
   | Pointer _ | Opaque _ -> assert true
 
@@ -100,12 +100,12 @@ let struct_ =
     | None ->
         (* Add placeholder defn to prevent computing [elts] in calls to
            [struct] from [elts] for recursive occurrences of [name]. *)
-        let elts = Array.create ~len:(Vector.length elt_thks) dummy_typ in
+        let elts = Array.create ~len:(IArray.length elt_thks) dummy_typ in
         let typ =
-          Struct {name; elts= Vector.of_array elts; bits; byts; packed}
+          Struct {name; elts= IArray.of_array elts; bits; byts; packed}
         in
         Hashtbl.set defns ~key:name ~data:typ ;
-        Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ;
+        IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ;
         typ |> check invariant
 
 (** Constants *)
diff --git a/sledge/lib/typ.mli b/sledge/lib/typ.mli
index 110073261..4d42bf387 100644
--- a/sledge/lib/typ.mli
+++ b/sledge/lib/typ.mli
@@ -8,7 +8,7 @@
 (** Types *)
 
 type t = private
-  | Function of {return: t option; args: t vector}
+  | Function of {return: t option; args: t iarray}
       (** (Global) function names have type Pointer to Function. *)
   | Integer of {bits: int; byts: int}  (** Integer of given bitwidth. *)
   | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]}
@@ -16,10 +16,10 @@ type t = private
   | Pointer of {elt: t}  (** Pointer to element type. *)
   | Array of {elt: t; len: int; bits: int; byts: int}
       (** Statically-sized array of [len] elements of type [elt]. *)
-  | Tuple of {elts: t vector; bits: int; byts: int; packed: bool}
+  | Tuple of {elts: t iarray; bits: int; byts: int; packed: bool}
       (** Anonymous aggregate of heterogeneous types. *)
   | Struct of
-      {name: string; elts: t vector; bits: int; byts: int; packed: bool}
+      {name: string; elts: t iarray; bits: int; byts: int; packed: bool}
       (** Uniquely named aggregate of heterogeneous types. Every cycle of
           recursive types contains a [Struct]. NOTE: recursive [Struct]
           types are represented by cyclic values. *)
@@ -39,15 +39,15 @@ val byt : t
 val int : t
 val siz : t
 val ptr : t
-val function_ : return:t option -> args:t vector -> t
+val function_ : return:t option -> args:t iarray -> t
 val integer : bits:int -> byts:int -> t
 val float : bits:int -> byts:int -> enc:[`Extended | `IEEE | `Pair] -> t
 val pointer : elt:t -> t
 val array : elt:t -> len:int -> bits:int -> byts:int -> t
-val tuple : t vector -> bits:int -> byts:int -> packed:bool -> t
+val tuple : t iarray -> bits:int -> byts:int -> packed:bool -> t
 
 val struct_ :
-  name:string -> bits:int -> byts:int -> packed:bool -> t lazy_t vector -> t
+  name:string -> bits:int -> byts:int -> packed:bool -> t lazy_t iarray -> t
 
 val opaque : name:string -> t