Instrs: Arrays and RevArrays only

Reviewed By: jvillard

Differential Revision: D8187368

fbshipit-source-id: 5f069a7

infer/src/IR/Instrs.ml

@@ -8,46 +8,141 @@
 open! IStd
 module F = Format
 
-type t = Sil.instr list
+module RevArray : sig
+  type 'a t
 
-let empty = []
+  val is_empty : 'a t -> bool
 
-let singleton instr = [instr]
+  val length : 'a t -> int
 
-let append_list = List.append
+  val of_rev_array : 'a Array.t -> 'a t
 
-let prepend_one instr instrs = instr :: instrs
+  val get : 'a t -> int -> 'a
 
-let reverse_order = List.rev
+  val last_opt : 'a t -> 'a option
 
-let is_empty = List.is_empty
+  val fold : ('a t, 'a, 'accum) Container.fold
+end = struct
+  type 'a t = 'a Array.t
 
-let exists = List.exists
+  let is_empty = Array.is_empty
 
-let for_all = List.for_all
+  let length = Array.length
 
-let count = List.length
+  let of_rev_array a = a
 
-let nth_exists instrs index = IList.drop instrs index |> List.is_empty |> not
+  let get a index = a.(Array.length a - 1 - index)
 
-let nth_exn = List.nth_exn
+  let last_opt a = if is_empty a then None else Some (Array.unsafe_get a 0)
 
-let last = List.last
+  let fold a ~init ~f =
+    let f = Fn.flip f in
+    Array.fold_right a ~init ~f
+end
 
-let find_map = List.find_map
+type reversed
 
-let pp pe fmt instrs =
-  List.iter instrs ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr pe) instr)
+type not_reversed
 
+type 'rev t =
+  | NotReversed: Sil.instr Array.t -> not_reversed t
+  | Reversed: Sil.instr RevArray.t -> reversed t
 
-let filter_map = List.filter_map
+type not_reversed_t = not_reversed t
 
-let fold = List.fold
+(* Some functions are only used on non-reversed arrays, let's specialize them.
+  The argument of the type helps us make sure they can't be used otherwise. *)
+(* Functions on non-reversed arrays *)
 
-let iter = List.iter
+let of_array instrs = NotReversed instrs
 
-let map_changed ~equal instrs ~f = IList.map_changed ~equal instrs ~f
+let empty = of_array [||]
 
-let of_list instrs = instrs
+let singleton instr = of_array [|instr|]
 
-let of_rev_list instrs = List.rev instrs
+let append_list (NotReversed instrs) list = NotReversed (Array.append instrs (Array.of_list list))
+
+let prepend_one instr (NotReversed instrs) = NotReversed (Array.append [|instr|] instrs)
+
+let of_list l = NotReversed (Array.of_list l)
+
+let of_rev_list l = NotReversed (Array.of_list_rev l)
+
+let filter_map (NotReversed instrs) ~f = NotReversed (Array.filter_map instrs ~f)
+
+let map_changed =
+  let aux_changed arr ~f i =
+    for i = i to Array.length arr - 1 do Array.unsafe_get arr i |> f |> Array.unsafe_set arr i done ;
+    arr
+  in
+  let rec aux_unchanged ~equal arr ~f i =
+    if i >= Array.length arr then arr
+    else
+      let e = Array.unsafe_get arr i in
+      let e' = f e in
+      if equal e e' then aux_unchanged ~equal arr ~f (i + 1)
+      else
+        let arr = Array.copy arr in
+        Array.unsafe_set arr i e' ;
+        aux_changed arr ~f (i + 1)
+  in
+  fun ~equal (NotReversed instrs as t) ~f ->
+    let instrs' = aux_unchanged ~equal instrs ~f 0 in
+    if phys_equal instrs instrs' then t else NotReversed instrs'
+
+
+let reverse_order (NotReversed instrs) = Reversed (RevArray.of_rev_array instrs)
+
+(* Functions on both reversed and non-reversed arrays *)
+
+let is_empty (type r) (t: r t) =
+  match t with
+  | NotReversed instrs ->
+      Array.is_empty instrs
+  | Reversed rev_instrs ->
+      RevArray.is_empty rev_instrs
+
+
+let fold (type r) (t: r t) ~init ~f =
+  match t with
+  | NotReversed instrs ->
+      Array.fold instrs ~init ~f
+  | Reversed rev_instrs ->
+      RevArray.fold rev_instrs ~init ~f
+
+
+let iter t ~f = Container.iter ~fold t ~f
+
+let exists t ~f = Container.exists ~iter t ~f
+
+let for_all t ~f = Container.for_all ~iter t ~f
+
+let count (type r) (t: r t) =
+  match t with
+  | NotReversed instrs ->
+      Array.length instrs
+  | Reversed rev_instrs ->
+      RevArray.length rev_instrs
+
+
+let nth_exists t index = index < count t
+
+let nth_exn (type r) (t: r t) index =
+  match t with
+  | NotReversed instrs ->
+      instrs.(index)
+  | Reversed rev_instrs ->
+      RevArray.get rev_instrs index
+
+
+let last (type r) (t: r t) =
+  match t with
+  | NotReversed instrs ->
+      if is_empty t then None else Some (Array.last instrs)
+  | Reversed rev_instrs ->
+      RevArray.last_opt rev_instrs
+
+
+let find_map t ~f = Container.find_map ~iter t ~f
+
+let pp pe fmt t = iter t ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr pe) instr)

infer/src/IR/Instrs.mli

@@ -7,44 +7,52 @@
 
 open! IStd
 
-type t
+type reversed
 
-val empty : t
+type not_reversed
 
-val singleton : Sil.instr -> t
+type 'r t
 
-val append_list : t -> Sil.instr list -> t
+type not_reversed_t = not_reversed t
 
-val prepend_one : Sil.instr -> t -> t
+val empty : not_reversed_t
 
-val reverse_order : t -> t
+val singleton : Sil.instr -> not_reversed_t
 
-val is_empty : t -> bool
+val append_list : not_reversed_t -> Sil.instr list -> not_reversed_t
 
-val count : t -> int
+val prepend_one : Sil.instr -> not_reversed_t -> not_reversed_t
 
-val exists : t -> f:(Sil.instr -> bool) -> bool
+val of_list : Sil.instr list -> not_reversed_t
 
-val for_all : t -> f:(Sil.instr -> bool) -> bool
+val of_rev_list : Sil.instr list -> not_reversed_t
 
-val nth_exists : t -> int -> bool
+val filter_map : not_reversed_t -> f:(Sil.instr -> Sil.instr option) -> not_reversed_t
 
-val nth_exn : t -> int -> Sil.instr
+val map_changed :
+  equal:(Sil.instr -> Sil.instr -> bool) -> not_reversed_t -> f:(Sil.instr -> Sil.instr)
+  -> not_reversed_t
 
-val last : t -> Sil.instr option
+val reverse_order : not_reversed_t -> reversed t
 
-val find_map : t -> f:(Sil.instr -> 'a option) -> 'a option
+val is_empty : _ t -> bool
 
-val pp : Pp.env -> Format.formatter -> t -> unit
+val count : _ t -> int
 
-val filter_map : t -> f:(Sil.instr -> Sil.instr option) -> t
+val exists : _ t -> f:(Sil.instr -> bool) -> bool
 
-val map_changed : equal:(Sil.instr -> Sil.instr -> bool) -> t -> f:(Sil.instr -> Sil.instr) -> t
+val for_all : _ t -> f:(Sil.instr -> bool) -> bool
 
-val fold : (t, Sil.instr, 'a) Container.fold
+val nth_exists : _ t -> int -> bool
 
-val iter : (t, Sil.instr) Container.iter
+val nth_exn : _ t -> int -> Sil.instr
 
-val of_list : Sil.instr list -> t
+val last : _ t -> Sil.instr option
 
-val of_rev_list : Sil.instr list -> t
+val find_map : _ t -> f:(Sil.instr -> 'a option) -> 'a option
+
+val pp : Pp.env -> Format.formatter -> _ t -> unit
+
+val fold : (_ t, Sil.instr, 'a) Container.fold
+
+val iter : (_ t, Sil.instr) Container.iter

infer/src/IR/Procdesc.ml

@@ -33,7 +33,7 @@ module Node = struct
     { id: id  (** unique id of the node *)
     ; mutable dist_exit: int option  (** distance to the exit node *)
     ; mutable exn: t list  (** exception nodes in the cfg *)
-    ; mutable instrs: Instrs.t  (** instructions for symbolic execution *)
+    ; mutable instrs: Instrs.not_reversed_t  (** instructions for symbolic execution *)
     ; kind: nodekind  (** kind of node *)
     ; loc: Location.t  (** location in the source code *)
     ; mutable preds: t list  (** predecessor nodes in the cfg *)

infer/src/IR/Procdesc.mli

@@ -66,7 +66,7 @@ module Node : sig
   val get_id : t -> id
   (** Get the unique id of the node *)
 
-  val get_instrs : t -> Instrs.t
+  val get_instrs : t -> Instrs.not_reversed_t
   (** Get the instructions to be executed *)
 
   val get_kind : t -> nodekind

infer/src/absint/AbstractInterpreter.ml

@@ -63,25 +63,28 @@ struct
   let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
     let node_id = Node.id node in
     let update_inv_map pre ~visit_count =
-      let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in
-      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
-      let instrs =
-        let instrs = CFG.instrs node in
-        if Instrs.is_empty instrs then Instrs.singleton Sil.skip_instr else instrs
+      let exec_instrs instrs =
+        if debug then
+          NodePrinter.start_session
+            ~pp_name:(TransferFunctions.pp_session_name node)
+            (Node.underlying_node node) ;
+        let astate_post =
+          let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in
+          Instrs.fold ~f:compute_post ~init:pre instrs
+        in
+        if debug then (
+          L.d_strln
+            (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre
+               (Instrs.pp Pp.(html Green))
+               instrs Domain.pp astate_post) ;
+          NodePrinter.finish_session (Node.underlying_node node) ) ;
+        let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
+        (inv_map', Scheduler.schedule_succs work_queue node)
       in
-      if debug then
-        NodePrinter.start_session
-          ~pp_name:(TransferFunctions.pp_session_name node)
-          (Node.underlying_node node) ;
-      let astate_post = Instrs.fold ~f:compute_post ~init:pre instrs in
-      if debug then (
-        L.d_strln
-          (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre
-             (Instrs.pp Pp.(html Green))
-             instrs Domain.pp astate_post) ;
-        NodePrinter.finish_session (Node.underlying_node node) ) ;
-      let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
-      (inv_map', Scheduler.schedule_succs work_queue node)
+      (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
+      let instrs = CFG.instrs node in
+      if Instrs.is_empty instrs then exec_instrs (Instrs.singleton Sil.skip_instr)
+      else exec_instrs instrs
     in
     if InvariantMap.mem node_id inv_map then (
       let old_state = InvariantMap.find node_id inv_map in

infer/src/absint/ProcCfg.ml

@@ -113,9 +113,11 @@ end
 module type S = sig
   type t
 
+  type instrs_dir
+
   module Node : Node
 
-  val instrs : Node.t -> Instrs.t
+  val instrs : Node.t -> instrs_dir Instrs.t
   (** get the instructions from a node *)
 
   val fold_succs : t -> (Node.t, Node.t, 'accum) Container.fold
@@ -152,6 +154,8 @@ end
 module Normal = struct
   type t = Procdesc.t
 
+  type instrs_dir = Instrs.not_reversed
+
   module Node = DefaultNode
 
   let instrs = Procdesc.Node.get_instrs
@@ -186,6 +190,8 @@ end
 module Exceptional = struct
   module Node = DefaultNode
 
+  type instrs_dir = Instrs.not_reversed
+
   type id_node_map = Node.t list Procdesc.IdMap.t
 
   type t = Procdesc.t * id_node_map
@@ -264,8 +270,12 @@ module Exceptional = struct
 end
 
 (** Wrapper that reverses the direction of the CFG *)
-module Backward (Base : S) = struct
-  include Base
+module Backward (Base : S with type instrs_dir = Instrs.not_reversed) = struct
+  include (
+    Base :
+      S with type t = Base.t and type instrs_dir := Base.instrs_dir and module Node = Base.Node )
+
+  type instrs_dir = Instrs.reversed
 
   let instrs n = Instrs.reverse_order (Base.instrs n)
 
@@ -287,12 +297,17 @@ module Backward (Base : S) = struct
 end
 
 module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig
-  include S with type t = Base.t and module Node = InstrNode
+  include S
+          with type t = Base.t
+           and module Node = InstrNode
+           and type instrs_dir = Instrs.not_reversed
 
   val last_of_underlying_node : Procdesc.Node.t -> Node.t
 end = struct
   type t = Base.t
 
+  type instrs_dir = Instrs.not_reversed
+
   module Node = InstrNode
 
   let instrs (node, index) =

infer/src/absint/ProcCfg.mli

@@ -40,9 +40,11 @@ end
 module type S = sig
   type t
 
+  type instrs_dir
+
   module Node : Node
 
-  val instrs : Node.t -> Instrs.t
+  val instrs : Node.t -> instrs_dir Instrs.t
   (** get the instructions from a node *)
 
   val fold_succs : t -> (Node.t, Node.t, 'accum) Container.fold
@@ -87,17 +89,28 @@ module InstrNode : sig
 end
 
 (** Forward CFG with no exceptional control-flow *)
-module Normal : S with type t = Procdesc.t and module Node = DefaultNode
+module Normal :
+  S
+  with type t = Procdesc.t
+   and module Node = DefaultNode
+   and type instrs_dir = Instrs.not_reversed
 
 (** Forward CFG with exceptional control-flow *)
 module Exceptional :
-  S with type t = Procdesc.t * DefaultNode.t list Procdesc.IdMap.t and module Node = DefaultNode
+  S
+  with type t = Procdesc.t * DefaultNode.t list Procdesc.IdMap.t
+   and module Node = DefaultNode
+   and type instrs_dir = Instrs.not_reversed
 
 (** Wrapper that reverses the direction of the CFG *)
-module Backward (Base : S) : S with type t = Base.t and module Node = Base.Node
+module Backward (Base : S with type instrs_dir = Instrs.not_reversed) :
+  S with type t = Base.t and module Node = Base.Node and type instrs_dir = Instrs.reversed
 
 module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig
-  include S with type t = Base.t and module Node = InstrNode
+  include S
+          with type t = Base.t
+           and module Node = InstrNode
+           and type instrs_dir = Instrs.not_reversed
 
   val last_of_underlying_node : Procdesc.Node.t -> Node.t
 end

infer/src/backend/printer.ml

@@ -196,7 +196,7 @@ let force_delayed_print fmt =
             i Io_infer.Html.pp_end_color ()
         else Sil.pp_instr Pp.text fmt i
     | L.PTinstr_list, il ->
-        let il : Instrs.t = Obj.obj il in
+        let il : Instrs.not_reversed_t = Obj.obj il in
         if Config.write_html then
           F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
             (Instrs.pp (Pp.html Green))

infer/src/biabduction/SymExec.mli

@@ -16,7 +16,7 @@ val node :
 (** Symbolic execution of the instructions of a node, lifted to sets of propositions. *)
 
 val instrs :
-  ?mask_errors:bool -> Exe_env.t -> Tenv.t -> Procdesc.t -> Instrs.t
+  ?mask_errors:bool -> Exe_env.t -> Tenv.t -> Procdesc.t -> Instrs.not_reversed_t
   -> (Prop.normal Prop.t * Paths.Path.t) list -> (Prop.normal Prop.t * Paths.Path.t) list
 (** Symbolic execution of a sequence of instructions.
     If errors occur and [mask_errors] is true, just treat as skip. *)

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -460,7 +460,7 @@ module Report = struct
 
 
   let check_instrs
-      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.Node.t -> Instrs.t
+      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.Node.t -> Instrs.not_reversed_t
         -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun summary pdesc tenv cfg node instrs state cond_set ->
     match state with

infer/src/unit/procCfgTests.ml

@@ -88,7 +88,7 @@ let tests =
       let check_backward_instr_ fold backward_instr_node expected_instrs =
         match Container.to_list ~fold:(fold backward_instr_proc_cfg) backward_instr_node with
         | [n] ->
-            assert_equal (BackwardInstrCfg.instrs n) expected_instrs
+            assert_equal (BackwardInstrCfg.instrs n) (expected_instrs |> Instrs.reverse_order)
         | _ ->
             assert_failure "Expected exactly one node"
       in

infer/src/unit/schedulerTests.ml

@@ -47,6 +47,8 @@ module MockProcCfg = struct
 
   type t = (Node.t * Node.t list) list
 
+  type instrs_dir = Instrs.not_reversed
+
   let instrs _ = Instrs.empty
 
   let equal_id = Int.equal