[sledge] Switch IArray from Core_kernel.Array to NS.Array

Summary:
Change implementation of IArray from a wrapper of
Core_kernel.Array.Permissioned to NS.Array, and remove magic.  Also
add operations to Array and Iter in order to ensure that IArray is an
extremely thin wrapper of Array: only defining conversions to/from
arrays as well as adding hashing support.

Reviewed By: jvillard

Differential Revision: D24306095

fbshipit-source-id: 97b9187be

sledge/nonstdlib/array.ml

@@ -11,10 +11,56 @@ include Array
 
 type 'a t = 'a array [@@deriving compare, equal, sexp]
 
+let of_ x = [|x|]
+
+let of_list_rev = function
+  | [] -> [||]
+  | hd :: tl ->
+      let len = 1 + List.length tl in
+      let a = make len hd in
+      let rec back_fill i = function
+        | [] -> a
+        | hd :: tl ->
+            a.(i) <- hd ;
+            back_fill (i - 1) tl
+      in
+      back_fill (len - 2) tl
+
 let is_empty = function [||] -> true | _ -> false
 let map xs ~f = map ~f xs
 let map_endo xs ~f = map_endo map xs ~f
 
+let reduce_adjacent xs ~f =
+  let n = length xs - 1 in
+  let rec reduce_adjacent_ j i xs =
+    if i < n then (
+      match f xs.(i - j) xs.(i + 1) with
+      | None ->
+          if j != 0 then xs.(i + 1 - j) <- xs.(i + 1) ;
+          reduce_adjacent_ j (i + 1) xs
+      | Some x ->
+          let xs = if j = 0 then copy xs else xs in
+          xs.(i - j) <- x ;
+          reduce_adjacent_ (j + 1) (i + 1) xs )
+    else if j = 0 then xs
+    else sub xs ~pos:0 ~len:(n + 1 - j)
+  in
+  reduce_adjacent_ 0 0 xs
+
+let split xys =
+  let n = length xys in
+  if n = 0 then ([||], [||])
+  else
+    let x0, y0 = xys.(0) in
+    let xs = make n x0 in
+    let ys = make n y0 in
+    for i = 1 to n - 1 do
+      let xI, yI = xys.(i) in
+      xs.(i) <- xI ;
+      ys.(i) <- yI
+    done ;
+    (xs, ys)
+
 let combine_exn xs ys =
   let len = length xs in
   if len <> length ys then invalid_arg "Array.combine_exn" ;
@@ -23,6 +69,33 @@ let combine_exn xs ys =
 let combine xs ys =
   try Some (combine_exn xs ys) with Invalid_argument _ -> None
 
+let iter xs ~f = iter ~f xs
+let iteri xs ~f = iteri ~f xs
+let exists xs ~f = exists ~f xs
+let for_all xs ~f = for_all ~f xs
 let fold xs ~init ~f = fold ~f ~init xs
+let fold_right xs ~init ~f = fold_right ~f ~init xs
+let fold_map xs ~init ~f = fold_map ~f ~init xs
+
+let fold_map_until xs ~init ~f ~finish =
+  let l = length xs in
+  if l = 0 then finish (init, [||])
+  else
+    match f init xs.(0) with
+    | `Stop r -> r
+    | `Continue (s, y) ->
+        let ys = make l y in
+        let rec fold_map_until_ s i =
+          if i = l then finish (s, ys)
+          else
+            match f s xs.(i) with
+            | `Stop r -> r
+            | `Continue (s, y) ->
+                ys.(i) <- y ;
+                fold_map_until_ s (i + 1)
+        in
+        fold_map_until_ s 1
+
+let for_all2_exn xs ys ~f = for_all2 ~f xs ys
 let to_list_rev_map xs ~f = fold ~f:(fun ys x -> f x :: ys) ~init:[] xs
 let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)

sledge/nonstdlib/array.mli

@@ -10,15 +10,34 @@ include module type of ContainersLabels.Array
 
 type 'a t = 'a array [@@deriving compare, equal, sexp]
 
-val is_empty : 'a t -> bool
+val of_ : 'a -> 'a t
+val of_list_rev : 'a list -> 'a t
 val map : 'a t -> f:('a -> 'b) -> 'b t
 
 val map_endo : 'a t -> f:('a -> 'a) -> 'a t
 (** Like [map], but specialized to require [f] to be an endofunction, which
     enables preserving [==] if [f] preserves [==] of every element. *)
 
+val reduce_adjacent : 'a t -> f:('a -> 'a -> 'a option) -> 'a t
+val split : ('a * 'b) t -> 'a t * 'b t
 val combine : 'a t -> 'b t -> ('a * 'b) t option
 val combine_exn : 'a t -> 'b t -> ('a * 'b) t
+val is_empty : 'a t -> bool
+val iter : 'a t -> f:('a -> unit) -> unit
+val iteri : 'a t -> f:(int -> 'a -> unit) -> unit
+val exists : 'a t -> f:('a -> bool) -> bool
+val for_all : 'a t -> f:('a -> bool) -> bool
+val for_all2_exn : 'a t -> 'b t -> f:('a -> 'b -> bool) -> bool
 val fold : 'a array -> init:'s -> f:('s -> 'a -> 's) -> 's
+val fold_right : 'a t -> init:'s -> f:('a -> 's -> 's) -> 's
+val fold_map : 'a t -> init:'s -> f:('s -> 'a -> 's * 'b) -> 's * 'b t
+
+val fold_map_until :
+     'a t
+  -> init:'s
+  -> f:('s -> 'a -> [`Continue of 's * 'b | `Stop of 'c])
+  -> finish:('s * 'b t -> 'c)
+  -> 'c
+
 val to_list_rev_map : 'a array -> f:('a -> 'b) -> 'b list
 val pp : (unit, unit) fmt -> 'a pp -> 'a array pp

sledge/nonstdlib/iArray.ml

@@ -8,67 +8,15 @@
 (** IArray - Immutable view of an array *)
 
 open! NS0
-include Core_kernel.Perms.Export
+include Array
 
-include (
-  Core_kernel.Array.Permissioned :
-    module type of Core_kernel.Array.Permissioned
-      with type ('a, 'p) t := ('a, 'p) Core_kernel.Array.Permissioned.t )
+type 'a t = 'a array
 
-type 'a t = ('a, immutable) Core_kernel.Array.Permissioned.t
-
-let a2i (a : 'a array) : 'a t = Obj.magic a
-let i2a (a : 'a t) : 'a array = Obj.magic a
-let compare compare_elt = compare compare_elt compare_immutable
-
-let hash_fold_t hash_fold_elt s (a : _ t) =
-  Hash.Builtin.hash_fold_array_frozen hash_fold_elt s (i2a a)
-
-let t_of_sexp elt_of_sexp = t_of_sexp elt_of_sexp immutable_of_sexp
-let sexp_of_t sexp_of_elt = sexp_of_t sexp_of_elt sexp_of_immutable
+let hash_fold_t = hash_fold_array_frozen
 
 module Import = struct
   type 'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
-let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
-let empty = Obj.magic [||]
-let of_ x = create ~len:1 x
-let of_array = a2i
-
-let contains_dup ~compare xs =
-  let equal x y = compare x y = 0 in
-  Option.is_some
-    (find_consecutive_duplicate ~equal (sorted_copy ~compare xs))
-
-let fold_map xs ~init ~f =
-  let a, ys = Array.fold_map (i2a xs) ~init ~f in
-  (a, a2i ys)
-
-type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
-
-let fold_map_until xs ~init ~f ~finish =
-  With_return.with_return (fun {return} ->
-      finish
-        (fold_map xs ~init ~f:(fun s x ->
-             match f s x with Continue x -> x | Stop x -> return x )) )
-
-let map_endo xs ~f = map_endo map xs ~f
-
-let combine_adjacent ~f xs =
-  let xs = i2a xs in
-  let n = Array.length xs - 1 in
-  let rec combine_adjacent_ j i xs =
-    if i < n then (
-      match f xs.(i - j) xs.(i + 1) with
-      | None ->
-          if j != 0 then xs.(i + 1 - j) <- xs.(i + 1) ;
-          combine_adjacent_ j (i + 1) xs
-      | Some x ->
-          let xs = if j = 0 then Array.copy xs else xs in
-          xs.(i - j) <- x ;
-          combine_adjacent_ (j + 1) (i + 1) xs )
-    else if j = 0 then xs
-    else Array.sub xs ~pos:0 ~len:(n + 1 - j)
-  in
-  a2i (combine_adjacent_ 0 0 xs)
+let to_array xs = xs
+let of_array xs = xs

sledge/nonstdlib/iArray.mli

@@ -14,22 +14,17 @@
     mutate. *)
 
 open! NS0
-include module type of Core_kernel.Perms.Export
 
-include
-  module type of Core_kernel.Array.Permissioned
-    with type ('a, 'p) t := ('a, 'p) Core_kernel.Array.Permissioned.t
-
-type 'a t = ('a, immutable) Core_kernel.Array.Permissioned.t
-[@@deriving compare, equal, hash, sexp]
+type 'a t [@@deriving compare, equal, hash, sexp]
 
 module Import : sig
   type 'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
 val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
-val empty : 'a t
-val of_ : 'a -> 'a t
+
+val to_array : 'a t -> 'a array
+(** [to_array v] is the array backing [v], no copy is performed. *)
 
 val of_array : 'a array -> 'a t
 (** [of_array a] is an iarray that shares its representation with array [a],
@@ -38,22 +33,39 @@ val of_array : 'a array -> 'a t
     not be used after conversion, or with care for multi-step initialization
     of an iarray. *)
 
-val contains_dup : compare:('a -> 'a -> int) -> 'a t -> bool
+val empty : 'a t
+val of_ : 'a -> 'a t
+val of_list : 'a list -> 'a t
+val of_list_rev : 'a list -> 'a t
+val init : int -> f:(int -> 'a) -> 'a t
+val sub : 'a t -> pos:int -> len:int -> 'a t
+val concat : 'a t list -> 'a t
+val map : 'a t -> f:('a -> 'b) -> 'b t
+
+val map_endo : 'a t -> f:('a -> 'a) -> 'a t
+(** Like map, but specialized to require [f] to be an endofunction, which
+    enables preserving [==] if [f] preserves [==] of every element. *)
+
+val reduce_adjacent : 'a t -> f:('a -> 'a -> 'a option) -> 'a t
+val split : ('a * 'b) t -> 'a t * 'b t
+val is_empty : 'a t -> bool
+val length : 'a t -> int
+val get : 'a t -> int -> 'a
+val to_iter : 'a t -> 'a iter
+val iter : 'a t -> f:('a -> unit) -> unit
+val iteri : 'a t -> f:(int -> 'a -> unit) -> unit
+val exists : 'a t -> f:('a -> bool) -> bool
+val for_all : 'a t -> f:('a -> bool) -> bool
+val for_all2_exn : 'a t -> 'b t -> f:('a -> 'b -> bool) -> bool
+val fold : 'a t -> init:'s -> f:('s -> 'a -> 's) -> 's
+val fold_right : 'a t -> init:'s -> f:('a -> 's -> 's) -> 's
 
 val fold_map :
   'a t -> init:'accum -> f:('accum -> 'a -> 'accum * 'b) -> 'accum * 'b t
 
-type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
-
 val fold_map_until :
      'a t
-  -> init:'accum
-  -> f:('accum -> 'a -> ('accum * 'b, 'final) continue_or_stop)
-  -> finish:('accum * 'b t -> 'final)
-  -> 'final
-
-val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-(** Like map, but specialized to require [f] to be an endofunction, which
-    enables preserving [==] if [f] preserves [==] of every element. *)
-
-val combine_adjacent : f:('a -> 'a -> 'a option) -> 'a t -> 'a t
+  -> init:'s
+  -> f:('s -> 'a -> [`Continue of 's * 'b | `Stop of 'c])
+  -> finish:('s * 'b t -> 'c)
+  -> 'c

sledge/nonstdlib/iter.ml

@@ -14,6 +14,9 @@ end
 let pop seq =
   match head seq with Some x -> Some (x, drop 1 seq) | None -> None
 
+let find seq ~f = find (CCOpt.if_ f) seq
+let find_exn seq ~f = CCOpt.get_exn (find ~f seq)
+
 let contains_dup (type elt) seq ~cmp =
   let module S = CCSet.Make (struct
     type t = elt
@@ -50,3 +53,14 @@ let fold_until (type res) seq ~init ~f ~finish =
         | `Stop r -> raise_notrace (Stop r) ) ;
     finish !state
   with Stop r -> r
+
+let fold_result (type s e) seq ~init ~f =
+  let state = ref init in
+  let exception Stop of (s, e) result in
+  try
+    seq (fun x ->
+        match f !state x with
+        | Ok s -> state := s
+        | Error _ as e -> raise_notrace (Stop e) ) ;
+    Ok !state
+  with Stop e -> e

sledge/nonstdlib/iter.mli

@@ -12,6 +12,8 @@ module Import : sig
 end
 
 val pop : 'a iter -> ('a * 'a iter) option
+val find : 'a t -> f:('a -> bool) -> 'a option
+val find_exn : 'a t -> f:('a -> bool) -> 'a
 val contains_dup : 'a iter -> cmp:('a -> 'a -> int) -> bool
 
 val fold_opt : 'a t -> init:'s -> f:('s -> 'a -> 's option) -> 's option
@@ -25,3 +27,6 @@ val fold_until :
   -> f:('s -> 'a -> [`Continue of 's | `Stop of 'b])
   -> finish:('s -> 'b)
   -> 'b
+
+val fold_result :
+  'a t -> init:'s -> f:('s -> 'a -> ('s, 'e) result) -> ('s, 'e) result

sledge/src/control.ml

@@ -482,7 +482,9 @@ module Make (Dom : Domain_intf.Dom) = struct
       -> Work.x =
    fun opts pgm stk state block ->
     [%Trace.info "exec block %%%s" block.lbl] ;
-    match IArray.fold_result ~f:exec_inst ~init:state block.cmnd with
+    match
+      Iter.fold_result ~f:exec_inst ~init:state (IArray.to_iter 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 ;

sledge/src/llair/llair.ml

@@ -129,7 +129,7 @@ let pp_inst fs inst =
   let pf pp = Format.fprintf fs pp in
   match inst with
   | Move {reg_exps; loc} ->
-      let regs, exps = IArray.unzip reg_exps in
+      let regs, exps = IArray.split 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} ->
@@ -501,7 +501,8 @@ module Func = struct
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
-        IArray.find_exn cfg ~f:(fun k -> String.equal lbl k.lbl)
+        Iter.find_exn (IArray.to_iter 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
@@ -602,7 +603,7 @@ module Program = struct
     let@ () = Invariant.invariant [%here] pgm [%sexp_of: program] in
     assert (
       not
-        (IArray.contains_dup pgm.globals ~compare:(fun g1 g2 ->
+        (Iter.contains_dup (IArray.to_iter pgm.globals) ~cmp:(fun g1 g2 ->
              Reg.compare g1.Global.reg g2.Global.reg )) )
 
   let mk ~globals ~functions =

sledge/src/ses/equality.ml

@@ -247,13 +247,13 @@ 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 =
-  IArray.fold_until a0V ~init:(s, Term.zero)
+  Iter.fold_until (IArray.to_iter a0V) ~init:(s, Term.zero)
     ~f:(fun (s, oI) aJ ->
       let nJ = Term.seq_size_exn aJ in
       let oJ = Term.add oI nJ in
       match solve_ ?f aJ (Term.extract ~seq:b ~off:oI ~len:nJ) s with
-      | Some s -> Continue (s, oJ)
-      | None -> Stop None )
+      | Some s -> `Continue (s, oJ)
+      | None -> `Stop None )
     ~finish:(fun (s, n0V) -> solve_ ?f n0V m s)
 
 and solve_ ?f d e s =

sledge/src/ses/term.ml

@@ -670,7 +670,7 @@ let rec simp_extract seq off len =
             ~f:(fun (l, oI) naI ->
               let nI = seq_size_exn naI in
               if Z.equal Z.zero l then
-                Continue ((l, oI), simp_extract naI oI zero)
+                `Continue ((l, oI), simp_extract naI oI zero)
               else
                 let oI_nI = simp_sub oI nI in
                 match oI_nI with
@@ -678,8 +678,8 @@ let rec simp_extract seq off len =
                     let oJ = if Z.sign data <= 0 then zero else oI_nI in
                     let lI = Z.(max zero (min l (neg data))) in
                     let l = Z.(l - lI) in
-                    Continue ((l, oJ), simp_extract naI oI (integer lI))
-                | _ -> Stop (Ap3 (Extract, seq, off, len)) )
+                    `Continue ((l, oJ), simp_extract naI oI (integer lI))
+                | _ -> `Stop (Ap3 (Extract, seq, off, len)) )
             ~finish:(fun (_, e1N) -> simp_concat e1N)
       | _ -> Ap3 (Extract, seq, off, len) )
     (* α[o,l) *)
@@ -720,7 +720,7 @@ and simp_concat xs =
     | _ -> None
   in
   let xs = flatten xs in
-  let xs = IArray.combine_adjacent ~f:simp_adjacent xs in
+  let xs = IArray.reduce_adjacent ~f:simp_adjacent xs in
   (if IArray.length xs = 1 then IArray.get xs 0 else ApN (Concat, xs))
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]