[sledge] Represent function formal parameters and actual arguments in order

Summary:
Previously, when LLAIR was in SSA form, blocks took parameters just
like functions, and it was sometimes necessary to partially apply a
block to some of the parameters. For example, blocks to which function
calls return would need to accept the return value as an argument, and
sometimes immediately jump to another block passing the rest of the
arguments as well. These "trampoline" blocks were partial applications
of the eventual block to all but the final, return value,
argument.

This partial application mechanism meant that function parameters and
arguments were represented as a stack, with the first argument at the
bottom, that is, in reverse order.

Now that LLAIR is free of SSA, this confusion is no longer needed, and
this diff changes the representation of function formal parameters and
actual arguments to be in the natural order. This also brings Call
instructions in line with Intrinsic instructions, which will make
changing the handling of intrinsics from Calls to Intrinsic less
error-prone.

Reviewed By: jvillard

Differential Revision: D25146163

fbshipit-source-id: d3ed07a45

sledge/cli/domain_itv.ml

@@ -281,10 +281,12 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     let mangle r =
       Llair.Reg.mk (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
     in
-    let args = List.combine_exn formals actuals in
+    let args = IArray.combine_exn formals actuals in
-    let q' = List.fold ~f:(fun (f, a) q -> assign (mangle f) a q) args q in
+    let q' =
+      IArray.fold ~f:(fun (f, a) q -> assign (mangle f) a q) args q
+    in
     let callee_env =
-      List.fold formals ([], []) ~f:(fun f (is, fs) ->
+      IArray.fold formals ([], []) ~f:(fun f (is, fs) ->
           match apron_typ_of_llair_typ (Llair.Reg.typ f) with
           | None -> (is, fs)
           | Some Texpr1.Int -> (apron_var_of_reg (mangle f) :: is, fs)
@@ -296,8 +298,10 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     let q'' = Abstract1.change_environment man q' callee_env false in
     let q''' =
       Abstract1.rename_array man q''
-        (Array.map ~f:(mangle >> apron_var_of_reg) (Array.of_list formals))
+        (Array.map
-        (Array.map ~f:apron_var_of_reg (Array.of_list formals))
+           ~f:(mangle >> apron_var_of_reg)
+           (IArray.to_array formals))
+        (Array.map ~f:apron_var_of_reg (IArray.to_array formals))
     in
     (q''', {areturn; caller_q= q})
 

sledge/cli/frontend.ml

@@ -441,13 +441,12 @@ let rec xlate_intrinsic_exp :
   | _ -> None
 
 and xlate_values x len val_i =
-  let rec loop i (pre, args) =
+  let xlate_i j pre_0_i =
-    if i < 0 then (pre, args)
+    let pre_j, arg_j = xlate_value x (val_i j) in
-    else
+    (arg_j, Iter.append pre_0_i (Iter.of_list pre_j))
-      let pre_i, arg_i = xlate_value x (val_i i) in
-      loop (i - 1) (pre_i @ pre, arg_i :: args)
   in
-  loop (len - 1) ([], [])
+  let pre, vals = Iter.(fold_map (0 -- (len - 1)) empty ~f:xlate_i) in
+  (Iter.to_list pre, IArray.of_iter vals)
 
 and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
     =
@@ -485,22 +484,22 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.num_operands llv in
         let pre, args = xlate_values x len (Llvm.operand llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | ConstantDataVector ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.vector_size (Llvm.type_of llv) in
         let pre, args = xlate_values x len (Llvm.const_element llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | ConstantDataArray ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.array_length (Llvm.type_of llv) in
         let pre, args = xlate_values x len (Llvm.const_element llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | ConstantStruct ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.num_operands llv in
         let pre, args = xlate_values x len (Llvm.operand llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | BlockAddress ->
         let parent = find_name (Llvm.operand llv 0) in
         let name = find_name (Llvm.operand llv 1) in
@@ -1446,9 +1445,9 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
   let typ = xlate_type x (Llvm.type_of llf) in
   let name = Function.mk typ (find_name llf) in
   let formals =
-    Llvm.fold_left_params
+    Iter.from_iter (fun f -> Llvm.iter_params f llf)
-      (fun rev_args param -> xlate_name x param :: rev_args)
+    |> Iter.map ~f:(xlate_name x)
-      [] llf
+    |> IArray.of_iter
   in
   let freturn =
     match typ with

sledge/nonstdlib/array.ml

@@ -12,6 +12,7 @@ include Array
 type 'a t = 'a array [@@deriving compare, equal, sexp]
 
 let of_ x = [|x|]
+let of_iter = Iter.to_array
 
 let of_list_rev = function
   | [] -> [||]
@@ -101,5 +102,6 @@ let fold_map_until xs s ~f ~finish =
         fold_map_until_ s 1
 
 let for_all2_exn xs ys ~f = for_all2 ~f xs ys
+let fold2_exn xs ys init ~f = fold2 ~f:(fun s x y -> f x y s) ~init xs ys
 let to_list_rev_map xs ~f = fold ~f:(fun x ys -> f x :: ys) xs []
 let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)

sledge/nonstdlib/array.mli

@@ -11,6 +11,7 @@ include module type of ContainersLabels.Array
 type 'a t = 'a array [@@deriving compare, equal, sexp]
 
 val of_ : 'a -> 'a t
+val of_iter : 'a iter -> 'a t
 val of_list_rev : 'a list -> 'a t
 val map : 'a t -> f:('a -> 'b) -> 'b t
 val mapi : 'a t -> f:(int -> 'a -> 'b) -> 'b t
@@ -41,5 +42,6 @@ val fold_map_until :
   -> finish:('b t * 's -> 'c)
   -> 'c
 
+val fold2_exn : 'a t -> 'b t -> 's -> f:('a -> 'b -> 's -> 's) -> 's
 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.mli

@@ -35,6 +35,7 @@ val of_array : 'a array -> 'a t
 
 val empty : 'a t
 val of_ : 'a -> 'a t
+val of_iter : 'a iter -> '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
@@ -49,6 +50,8 @@ val map_endo : 'a t -> f:('a -> 'a) -> 'a t
 
 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 length : 'a t -> int
 val get : 'a t -> int -> 'a
@@ -68,3 +71,5 @@ val fold_map_until :
   -> f:('a -> 's -> [`Continue of 'b * 's | `Stop of 'c])
   -> finish:('b t * 's -> 'c)
   -> 'c
+
+val fold2_exn : 'a t -> 'b t -> 's -> f:('a -> 'b -> 's -> 's) -> 's

sledge/src/control.ml

@@ -32,7 +32,7 @@ module Make (Dom : Domain_intf.Dom) = struct
          t
       -> 'a
       -> unwind:
-           (   Llair.Reg.t list
+           (   Llair.Reg.t iarray
             -> Llair.Reg.Set.t
             -> Dom.from_call
             -> 'a
@@ -43,7 +43,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       | Return of
           { recursive: bool  (** return from a possibly-recursive call *)
           ; dst: Llair.Jump.t
-          ; formals: Llair.Reg.t list
+          ; formals: Llair.Reg.t iarray
           ; locals: Llair.Reg.Set.t
           ; from_call: Dom.from_call
           ; stk: t }
@@ -491,15 +491,16 @@ module Make (Dom : Domain_intf.Dom) = struct
       ~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions)
       opts.entry_points
     |> function
-    | Some {name; formals= []; freturn; locals; entry} ->
+    | Some {name; formals; freturn; locals; entry}
+      when IArray.is_empty formals ->
         Some
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
                    ~globals:
                      (Domain_used_globals.by_function opts.globals name)
-                   ~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
+                   ~actuals:IArray.empty ~areturn:None ~formals:IArray.empty
-                   (Dom.init pgm.globals)))
+                   ~freturn ~locals (Dom.init pgm.globals)))
              entry)
     | _ -> None
 

sledge/src/domain_intf.ml

@@ -24,7 +24,7 @@ module type Dom = sig
        skip_throw:bool
     -> Llair.Reg.t option
     -> Llair.Function.t
-    -> Llair.Exp.t list
+    -> Llair.Exp.t iarray
     -> t
     -> t option option
 
@@ -33,16 +33,16 @@ module type Dom = sig
   val call :
        summaries:bool
     -> globals:Llair.Global.Set.t
-    -> actuals:Llair.Exp.t list
+    -> actuals:Llair.Exp.t iarray
     -> areturn:Llair.Reg.t option
-    -> formals:Llair.Reg.t list
+    -> formals:Llair.Reg.t iarray
     -> freturn:Llair.Reg.t option
     -> locals:Llair.Reg.Set.t
     -> t
     -> t * from_call
 
   val post : Llair.Reg.Set.t -> from_call -> t -> t
-  val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t
+  val retn : Llair.Reg.t iarray -> Llair.Reg.t option -> from_call -> t -> t
 
   val resolve_callee :
        (Llair.Function.t -> Llair.func list)
@@ -57,7 +57,7 @@ module type Dom = sig
   val pp_summary : summary pp
 
   val create_summary :
-    locals:Llair.Reg.Set.t -> formals:Llair.Reg.t list -> t -> summary * t
+    locals:Llair.Reg.Set.t -> formals:Llair.Reg.t iarray -> t -> summary * t
 
   val apply_summary : t -> summary -> t option
 end

sledge/src/domain_relation.ml

@@ -13,7 +13,7 @@ module type State_domain_sig = sig
 
   val create_summary :
        locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.t list
+    -> formals:Llair.Reg.t iarray
     -> entry:t
     -> current:t
     -> summary * t
@@ -76,11 +76,11 @@ module Make (State_domain : State_domain_sig) = struct
       pf
         "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
          globals: {@[%a@]}@ current: %a@]"
-        (List.pp ",@ " Llair.Exp.pp)
+        (IArray.pp ",@ " Llair.Exp.pp)
-        (List.rev actuals)
+        actuals
-        (List.pp ",@ " Llair.Reg.pp)
+        (IArray.pp ",@ " Llair.Reg.pp)
-        (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp
+        formals Llair.Reg.Set.pp locals Llair.Global.Set.pp globals
-        globals State_domain.pp current]
+        State_domain.pp current]
     ;
     let caller_current, state_from_call =
       State_domain.call ~summaries ~globals ~actuals ~areturn ~formals

sledge/src/domain_relation.mli

@@ -13,7 +13,7 @@ module type State_domain_sig = sig
 
   val create_summary :
        locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.t list
+    -> formals:Llair.Reg.t iarray
     -> entry:t
     -> current:t
     -> summary * t

sledge/src/domain_sh.ml

@@ -75,7 +75,7 @@ let exec_inst inst pre =
 
 let exec_intrinsic ~skip_throw r i es q =
   Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r)
-    (Llair.Function.name i) (List.map ~f:X.term es)
+    (Llair.Function.name i) (IArray.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
 let value_determined_by ctx us a =
@@ -110,17 +110,17 @@ let and_eqs sub formals actuals q =
     let actual' = Term.rename sub actual in
     Sh.and_ (Formula.eq (Term.var formal) actual') q
   in
-  List.fold2_exn ~f:and_eq formals actuals q
+  IArray.fold2_exn ~f:and_eq formals actuals q
 
 let localize_entry globals actuals formals freturn locals shadow pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
-  let formals_set = Var.Set.of_list formals in
+  let formals_set = Var.Set.of_iter (IArray.to_iter formals) in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let wrt =
     Term.Set.of_iter
       (Iter.append
          (Iter.map ~f:X.global (Llair.Global.Set.to_iter globals))
-         (Iter.map ~f:Term.var (List.to_iter formals)))
+         (Iter.map ~f:Term.var (IArray.to_iter formals)))
   in
   let function_summary_pre = garbage_collect entry ~wrt in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
@@ -147,32 +147,30 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
        globals: {@[%a@]}@ q: %a@]"
-      (List.pp ",@ " Llair.Exp.pp)
+      (IArray.pp ",@ " Llair.Exp.pp)
-      (List.rev actuals)
+      actuals
-      (List.pp ",@ " Llair.Reg.pp)
+      (IArray.pp ",@ " Llair.Reg.pp)
-      (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp globals
+      formals Llair.Reg.Set.pp locals Llair.Global.Set.pp globals pp q]
-      pp q]
   ;
-  let actuals = List.map ~f:X.term actuals in
+  let actuals = IArray.map ~f:X.term actuals in
   let areturn = Option.map ~f:X.reg areturn in
-  let formals = List.map ~f:X.reg formals in
+  let formals = IArray.map ~f:X.reg formals in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let modifs = Var.Set.of_option areturn in
   (* quantify modifs, their current value will be overwritten and so does
      not need to be saved in the freshening renaming *)
   let q = Sh.exists modifs q in
   (* save current values of shadowed formals and locals with a renaming *)
-  let q', shadow =
+  let formals_freturn_locals =
-    Sh.freshen q ~wrt:(Var.Set.add_list formals freturn_locals)
+    Iter.fold ~f:Var.Set.add (IArray.to_iter formals) freturn_locals
   in
+  let q', shadow = Sh.freshen q ~wrt:formals_freturn_locals in
   let unshadow = Var.Subst.invert shadow in
   assert (Var.Set.disjoint modifs (Var.Subst.domain shadow)) ;
   (* pass arguments by conjoining equations between formals and actuals *)
   let entry = and_eqs shadow formals actuals q' in
   (* note: locals and formals are in scope *)
-  assert (
+  assert (Var.Set.subset formals_freturn_locals ~of_:entry.us) ;
-    Var.Set.subset (Var.Set.add_list formals freturn_locals) ~of_:entry.us
-  ) ;
   (* simplify *)
   let entry = simplify entry in
   ( if not summaries then (entry, {areturn; unshadow; frame= Sh.emp})
@@ -201,14 +199,16 @@ let post locals _ q =
 let retn formals freturn {areturn; unshadow; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}%a%a@ unshadow: %a@ q: %a@ frame: %a@]"
-      (List.pp ", " Llair.Reg.pp)
+      (IArray.pp ", " Llair.Reg.pp)
       formals
       (Option.pp "@ freturn: %a" Llair.Reg.pp)
       freturn
       (Option.pp "@ areturn: %a" Var.pp)
       areturn Var.Subst.pp unshadow pp q pp frame]
   ;
-  let formals = List.map ~f:X.reg formals in
+  let formals =
+    Var.Set.of_iter (Iter.map ~f:X.reg (IArray.to_iter formals))
+  in
   let freturn = Option.map ~f:X.reg freturn in
   let q =
     match areturn with
@@ -223,9 +223,7 @@ let retn formals freturn {areturn; unshadow; frame} q =
     | None -> q
   in
   (* exit scope of formals *)
-  let q =
+  let q = Sh.exists (Var.Set.union formals (Var.Set.of_option freturn)) q in
-    Sh.exists (Var.Set.add_list formals (Var.Set.of_option freturn)) q
-  in
   (* reinstate shadowed values of locals *)
   let q = Sh.rename unshadow q in
   (* reconjoin frame *)
@@ -251,11 +249,11 @@ let pp_summary fs {xs; foot; post} =
 let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
     pf "formals %a@ entry: %a@ current: %a"
-      (List.pp ",@ " Llair.Reg.pp)
+      (IArray.pp ",@ " Llair.Reg.pp)
       formals pp entry pp post]
   ;
   let formals =
-    Var.Set.of_iter (Iter.map ~f:X.reg (List.to_iter formals))
+    Var.Set.of_iter (Iter.map ~f:X.reg (IArray.to_iter formals))
   in
   let locals = X.regs locals in
   let foot = Sh.exists locals entry in

sledge/src/domain_sh.mli

@@ -11,7 +11,7 @@ include Domain_intf.Dom
 
 val create_summary :
      locals:Llair.Reg.Set.t
-  -> formals:Llair.Reg.t list
+  -> formals:Llair.Reg.t iarray
   -> entry:t
   -> current:t
   -> summary * t

sledge/src/domain_used_globals.ml

@@ -70,7 +70,7 @@ let exec_intrinsic ~skip_throw:_ _ intrinsic actuals st =
       ; "__cxa_allocate_exception"
       ; "_ZN5folly13usingJEMallocEv" ]
       ~f:(String.equal name)
-  then List.fold ~f:used_globals actuals st |> fun res -> Some (Some res)
+  then IArray.fold ~f:used_globals actuals st |> fun res -> Some (Some res)
   else None
 
 type from_call = t [@@deriving sexp]
@@ -78,7 +78,7 @@ type from_call = t [@@deriving sexp]
 (* Set abstract state to bottom (i.e. empty set) at function entry *)
 let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
     ~locals:_ st =
-  (empty, List.fold ~f:used_globals actuals st)
+  (empty, IArray.fold ~f:used_globals actuals st)
 
 let resolve_callee lookup ptr st =
   let st = used_globals ptr st in

sledge/src/exec.ml

@@ -738,7 +738,7 @@ let nondet pre = function Some reg -> kill pre reg | None -> pre
 let abort _ = None
 
 let intrinsic ~skip_throw :
-    Sh.t -> Var.t option -> string -> Term.t list -> Sh.t option option =
+    Sh.t -> Var.t option -> string -> Term.t iarray -> Sh.t option option =
  fun pre areturn intrinsic actuals ->
   let name =
     match String.index intrinsic '.' with
@@ -746,60 +746,60 @@ let intrinsic ~skip_throw :
     | Some i -> String.take i intrinsic
   in
   let skip pre = Some (Some pre) in
-  ( match (areturn, name, actuals) with
+  ( match (areturn, name, IArray.to_array actuals) with
   (*
    * cstdlib - memory management
    *)
   (* void* malloc(size_t size) *)
-  | Some reg, "malloc", [size]
+  | Some reg, "malloc", [|size|]
   (* void* aligned_alloc(size_t alignment, size_t size) *)
-   |Some reg, "aligned_alloc", [size; _] ->
+   |Some reg, "aligned_alloc", [|_; size|] ->
       Some (exec_spec pre (malloc_spec reg size))
   (* void* calloc(size_t number, size_t size) *)
-  | Some reg, "calloc", [size; number] ->
+  | Some reg, "calloc", [|number; size|] ->
       Some (exec_spec pre (calloc_spec reg number size))
   (* int posix_memalign(void** ptr, size_t alignment, size_t size) *)
-  | Some reg, "posix_memalign", [size; _; ptr] ->
+  | Some reg, "posix_memalign", [|ptr; _; size|] ->
       Some (exec_spec pre (posix_memalign_spec reg ptr size))
   (* void* realloc(void* ptr, size_t size) *)
-  | Some reg, "realloc", [size; ptr] ->
+  | Some reg, "realloc", [|ptr; size|] ->
       Some (exec_spec pre (realloc_spec reg ptr size))
   (*
    * jemalloc - non-standard API
    *)
   (* void* mallocx(size_t size, int flags) *)
-  | Some reg, "mallocx", [_; size] ->
+  | Some reg, "mallocx", [|size; _|] ->
       Some (exec_spec pre (mallocx_spec reg size))
   (* void* rallocx(void* ptr, size_t size, int flags) *)
-  | Some reg, "rallocx", [_; size; ptr] ->
+  | Some reg, "rallocx", [|ptr; size; _|] ->
       Some (exec_spec pre (rallocx_spec reg ptr size))
   (* size_t xallocx(void* ptr, size_t size, size_t extra, int flags) *)
-  | Some reg, "xallocx", [_; extra; size; ptr] ->
+  | Some reg, "xallocx", [|ptr; size; extra; _|] ->
       Some (exec_spec pre (xallocx_spec reg ptr size extra))
   (* size_t sallocx(void* ptr, int flags) *)
-  | Some reg, "sallocx", [_; ptr] ->
+  | Some reg, "sallocx", [|ptr; _|] ->
       Some (exec_spec pre (sallocx_spec reg ptr))
   (* void dallocx(void* ptr, int flags) *)
-  | None, "dallocx", [_; ptr]
+  | None, "dallocx", [|ptr; _|]
   (* void sdallocx(void* ptr, size_t size, int flags) *)
-   |None, "sdallocx", [_; _; ptr] ->
+   |None, "sdallocx", [|ptr; _; _|] ->
       Some (exec_spec pre (dallocx_spec ptr))
   (* size_t nallocx(size_t size, int flags) *)
-  | Some reg, "nallocx", [_; size] ->
+  | Some reg, "nallocx", [|size; _|] ->
       Some (exec_spec pre (nallocx_spec reg size))
   (* size_t malloc_usable_size(void* ptr) *)
-  | Some reg, "malloc_usable_size", [ptr] ->
+  | Some reg, "malloc_usable_size", [|ptr|] ->
       Some (exec_spec pre (malloc_usable_size_spec reg ptr))
   (* int mallctl(const char* name, void* oldp, size_t* oldlenp, void* newp,
      size_t newlen) *)
-  | Some _, "mallctl", [newlen; newp; oldlenp; oldp; _] ->
+  | Some _, "mallctl", [|_; oldp; oldlenp; newp; newlen|] ->
       Some (exec_specs pre (mallctl_specs oldp oldlenp newp newlen))
   (* int mallctlnametomib(const char* name, size_t* mibp, size_t* miblenp) *)
-  | Some _, "mallctlnametomib", [miblenp; mibp; _] ->
+  | Some _, "mallctlnametomib", [|_; mibp; miblenp|] ->
       Some (exec_spec pre (mallctlnametomib_spec mibp miblenp))
   (* int mallctlbymib(const size_t* mib, size_t miblen, void* oldp, size_t*
      oldlenp, void* newp, size_t newlen); *)
-  | Some _, "mallctlbymib", [newlen; newp; oldlenp; oldp; miblen; mib] ->
+  | Some _, "mallctlbymib", [|mib; miblen; oldp; oldlenp; newp; newlen|] ->
       Some
         (exec_specs pre
            (mallctlbymib_specs mib miblen oldp oldlenp newp newlen))
@@ -808,17 +808,18 @@ let intrinsic ~skip_throw :
    * cstring
    *)
   (* size_t strlen (const char* ptr) *)
-  | Some reg, "strlen", [ptr] -> Some (exec_spec pre (strlen_spec reg ptr))
+  | Some reg, "strlen", [|ptr|] ->
+      Some (exec_spec pre (strlen_spec reg ptr))
   (*
    * cxxabi
    *)
-  | Some _, "__cxa_allocate_exception", [_] when skip_throw ->
+  | Some _, "__cxa_allocate_exception", [|_|] when skip_throw ->
       skip (Sh.false_ pre.us)
   (*
    * folly
    *)
   (* bool folly::usingJEMalloc() *)
-  | Some _, "_ZN5folly13usingJEMallocEv", [] -> skip pre
+  | Some _, "_ZN5folly13usingJEMallocEv", [||] -> skip pre
   | _ -> None )
   $> function
   | None -> ()
@@ -826,5 +827,4 @@ let intrinsic ~skip_throw :
       [%Trace.info
         "@[<2>exec intrinsic@ @[%a%s(@[%a@])@] from@ @[{ %a@ }@]@]"
           (Option.pp "%a := " Var.pp)
-          areturn intrinsic (List.pp ",@ " Term.pp) (List.rev actuals) Sh.pp
+          areturn intrinsic (IArray.pp ",@ " Term.pp) actuals Sh.pp pre]
-          pre]

sledge/src/exec.mli

@@ -27,5 +27,5 @@ val intrinsic :
   -> Sh.t
   -> Var.t option
   -> string
-  -> Term.t list
+  -> Term.t iarray
   -> Sh.t option option

sledge/src/llair/llair.ml

@@ -38,7 +38,7 @@ type jump = {mutable dst: block; mutable retreating: bool}
 and 'a call =
   { callee: 'a
   ; typ: Typ.t
-  ; actuals: Exp.t list
+  ; actuals: Exp.t iarray
   ; areturn: Reg.t option
   ; return: jump
   ; throw: jump option
@@ -62,7 +62,7 @@ and block =
 
 and func =
   { name: Function.t
-  ; formals: Reg.t list
+  ; formals: Reg.t iarray
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t
@@ -97,7 +97,7 @@ with type jump := jump
   type nonrec 'a call = 'a call =
     { callee: 'a
     ; typ: Typ.t
-    ; actuals: Exp.t list
+    ; actuals: Exp.t iarray
     ; areturn: Reg.t option
     ; return: jump
     ; throw: jump option
@@ -143,7 +143,7 @@ let hash_fold_term s = function
       let s = [%hash_fold: int] s 3 in
       let s = [%hash_fold: Exp.t] s callee in
       let s = [%hash_fold: Typ.t] s typ in
-      let s = [%hash_fold: Exp.t list] s actuals in
+      let s = [%hash_fold: Exp.t iarray] s actuals in
       let s = [%hash_fold: Reg.t option] s areturn in
       let s = [%hash_fold: jump] s return in
       let s = [%hash_fold: jump option] s throw in
@@ -191,7 +191,7 @@ let sexp_of_term = function
         [%sexp
           { callee: Exp.t
           ; typ: Typ.t
-          ; actuals: Exp.t list
+          ; actuals: Exp.t iarray
           ; areturn: Reg.t option
           ; return: jump
           ; throw: jump option
@@ -213,7 +213,7 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
 let sexp_of_func {name; formals; freturn; fthrow; locals; entry; loc} =
   [%sexp
     { name: Function.t
-    ; formals: Reg.t list
+    ; formals: Reg.t iarray
     ; freturn: Reg.t option
     ; fthrow: Reg.t
     ; locals: Reg.Set.t
@@ -260,8 +260,7 @@ let pp_inst fs inst =
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
 
 let pp_actuals pp_actual fs actuals =
-  Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_actual)
+  Format.fprintf fs "@ (@[%a@])" (IArray.pp ",@ " pp_actual) actuals
-    (List.rev actuals)
 
 let pp_formal fs reg = Reg.pp fs reg
 
@@ -325,7 +324,7 @@ and dummy_func =
       Function.mk
         (Typ.pointer ~elt:(Typ.function_ ~args:IArray.empty ~return:None))
         "dummy"
-  ; formals= []
+  ; formals= IArray.empty
   ; freturn= None
   ; fthrow= Reg.mk Typ.ptr "dummy"
   ; locals= Reg.Set.empty
@@ -425,7 +424,7 @@ module Term = struct
     | Call {typ; actuals; areturn; _} -> (
       match typ with
       | Pointer {elt= Function {args; return= retn_typ; _}} ->
-          assert (IArray.length args = List.length actuals) ;
+          assert (IArray.length args = IArray.length actuals) ;
           assert (Option.is_some retn_typ || Option.is_none areturn)
       | _ -> assert false )
     | Return {exp; _} -> (

sledge/src/llair/llair.mli

@@ -56,7 +56,7 @@ type jump = {mutable dst: block; mutable retreating: bool}
 and 'a call =
   { callee: 'a
   ; typ: Typ.t  (** Type of the callee. *)
-  ; actuals: Exp.t list  (** Stack of arguments, first-arg-last. *)
+  ; actuals: Exp.t iarray  (** Actual arguments. *)
   ; areturn: Reg.t option  (** Register to receive return value. *)
   ; return: jump  (** Return destination. *)
   ; throw: jump option  (** Handler destination. *)
@@ -95,7 +95,7 @@ and block = private
     parameters are the function parameters. *)
 and func = private
   { name: Function.t
-  ; formals: Reg.t list  (** Formal parameters, first-param-last stack *)
+  ; formals: Reg.t iarray  (** Formal parameters *)
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t  (** Local registers *)
@@ -155,7 +155,7 @@ module Term : sig
   val call :
        callee:Exp.t
     -> typ:Typ.t
-    -> actuals:Exp.t list
+    -> actuals:Exp.t iarray
     -> areturn:Reg.t option
     -> return:jump
     -> throw:jump option
@@ -188,7 +188,7 @@ module Func : sig
 
   val mk :
        name:Function.t
-    -> formals:Reg.t list
+    -> formals:Reg.t iarray
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> entry:block
@@ -198,7 +198,7 @@ module Func : sig
 
   val mk_undefined :
        name:Function.t
-    -> formals:Reg.t list
+    -> formals:Reg.t iarray
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> loc:Loc.t