[IR] `Instrs.empty` and `Instrs.singleton` have both directions

Summary:
This makes the API of [instrs] easier to work with at the price of some
duplication in the GADT.

This allows us to construct `[skip]` in `AbstractInterpreter` without
imposing a particular direction. This will make it the next diffs about
a disjunctive domain easier.

Reviewed By: skcho

Differential Revision: D21153694

fbshipit-source-id: f86c180fa

infer/src/IR/Instrs.ml

@@ -44,31 +44,48 @@ type reversed
 
 type not_reversed
 
-type 'rev t =
+(** [Empty] and [Singleton _] can have both directions. We do not attempt to make the representation
+    canonic, e.g. [NotReversed \[||\]], [Reversed \[||\]], and [Empty] are all allowed despite
+    representing the same value. *)
+type _ t =
   | NotReversed : Sil.instr Array.t -> not_reversed t
   | Reversed : Sil.instr RevArray.t -> reversed t
+  | Empty : _ t
+  | Singleton : Sil.instr -> _ t
 
 type not_reversed_t = not_reversed t
 
-(* 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 *)
+(** {2 Functions on non-reversed arrays}
 
-let of_array instrs = NotReversed instrs
+    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. *)
 
-let get_underlying_not_reversed = function NotReversed instrs -> instrs
+let get_underlying_not_reversed = function
+  | NotReversed instrs ->
+      instrs
+  | Empty ->
+      [||]
+  | Singleton instr ->
+      [|instr|]
+
+
+let empty = Empty
 
-let empty = of_array [||]
+let singleton instr = Singleton instr
 
-let singleton instr = of_array [|instr|]
+let append_list t list =
+  let instrs = get_underlying_not_reversed t in
+  NotReversed (Array.append instrs (Array.of_list list))
 
-let append_list (NotReversed instrs) list = NotReversed (Array.append instrs (Array.of_list list))
 
 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 filter_map t ~f =
+  let instrs = get_underlying_not_reversed t in
+  NotReversed (Array.filter_map instrs ~f)
+
 
 let map_and_fold =
   let rec aux_changed arr ~f current i =
@@ -90,17 +107,19 @@ let map_and_fold =
         Array.unsafe_set arr i e' ;
         aux_changed arr ~f next (i + 1)
   in
-  fun (NotReversed instrs as t) ~f ~init ->
+  fun t ~f ~init ->
+    let instrs = get_underlying_not_reversed t in
     let instrs' = aux_unchanged instrs ~f init 0 in
     if phys_equal instrs instrs' then t else NotReversed instrs'
 
 
-let map (NotReversed _instrs as t) ~f =
+let map (t : not_reversed t) ~f =
   let f () e = ((), f e) in
   map_and_fold t ~f ~init:()
 
 
-let concat_map (NotReversed instrs as t) ~f =
+let concat_map t ~f =
+  let instrs = get_underlying_not_reversed t in
   let instrs' = Array.concat_map ~f instrs in
   if
     Int.equal (Array.length instrs) (Array.length instrs')
@@ -109,12 +128,19 @@ let concat_map (NotReversed instrs as t) ~f =
   else NotReversed instrs'
 
 
-let reverse_order (NotReversed instrs) = Reversed (RevArray.of_rev_array instrs)
+let reverse_order t =
+  let instrs = get_underlying_not_reversed t in
+  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
+  | Empty ->
+      true
+  | Singleton _ ->
+      false
   | NotReversed instrs ->
       Array.is_empty instrs
   | Reversed rev_instrs ->
@@ -123,6 +149,10 @@ let is_empty (type r) (t : r t) =
 
 let fold (type r) (t : r t) ~init ~f =
   match t with
+  | Empty ->
+      init
+  | Singleton instr ->
+      f init instr
   | NotReversed instrs ->
       Array.fold instrs ~init ~f
   | Reversed rev_instrs ->
@@ -137,6 +167,10 @@ let for_all t ~f = Container.for_all ~iter t ~f
 
 let count (type r) (t : r t) =
   match t with
+  | Empty ->
+      0
+  | Singleton _ ->
+      1
   | NotReversed instrs ->
       Array.length instrs
   | Reversed rev_instrs ->
@@ -147,6 +181,10 @@ let nth_exists t index = index < count t
 
 let nth_exn (type r) (t : r t) index =
   match t with
+  | Empty ->
+      [||].(index)
+  | Singleton instr ->
+      [|instr|].(index)
   | NotReversed instrs ->
       instrs.(index)
   | Reversed rev_instrs ->
@@ -155,6 +193,10 @@ let nth_exn (type r) (t : r t) index =
 
 let last (type r) (t : r t) =
   match t with
+  | Empty ->
+      None
+  | Singleton instr ->
+      Some instr
   | NotReversed instrs ->
       if is_empty t then None else Some (Array.last instrs)
   | Reversed rev_instrs ->

infer/src/IR/Instrs.mli

@@ -7,40 +7,44 @@
 
 open! IStd
 
+(** Manipulate possibly-reversed lists of instructions efficiently *)
+
 type reversed
 
 type not_reversed
 
-type 'r t
+type _ t
 
+(** defined for convenience: we can write [Instrs.not_reversed_t] in other modules instead of
+    [Instrs.not_reversed Instrs.t] *)
 type not_reversed_t = not_reversed t
 
-val empty : not_reversed_t
+val empty : _ t
 
-val singleton : Sil.instr -> not_reversed_t
+val singleton : Sil.instr -> _ t
 
-val append_list : not_reversed_t -> Sil.instr list -> not_reversed_t
+val append_list : not_reversed t -> Sil.instr list -> not_reversed t
 
-val of_list : Sil.instr list -> not_reversed_t
+val of_list : Sil.instr list -> not_reversed t
 
-val of_rev_list : Sil.instr list -> not_reversed_t
+val of_rev_list : Sil.instr list -> not_reversed t
 
-val filter_map : not_reversed_t -> f:(Sil.instr -> Sil.instr option) -> not_reversed_t
+val filter_map : not_reversed t -> f:(Sil.instr -> Sil.instr option) -> not_reversed t
 
-val map : not_reversed_t -> f:(Sil.instr -> Sil.instr) -> not_reversed_t
+val map : not_reversed t -> f:(Sil.instr -> Sil.instr) -> not_reversed t
 (** replace every instruction [instr] with [f instr]. Preserve physical equality. **)
 
 val map_and_fold :
-  not_reversed_t -> f:('a -> Sil.instr -> 'a * Sil.instr) -> init:'a -> not_reversed_t
+  not_reversed t -> f:('a -> Sil.instr -> 'a * Sil.instr) -> init:'a -> not_reversed t
   [@@warning "-32"]
 (** replace every instruction [instr] with [snd (f context instr)]. The context is computed by
     folding [f] on [init] and previous instructions (before [instr]) in the collection. Preserve
     physical equality. **)
 
-val concat_map : not_reversed_t -> f:(Sil.instr -> Sil.instr array) -> not_reversed_t
+val concat_map : not_reversed t -> f:(Sil.instr -> Sil.instr array) -> not_reversed t
 (** replace every instruction [instr] with the list [f instr]. Preserve physical equality. **)
 
-val reverse_order : not_reversed_t -> reversed t
+val reverse_order : not_reversed t -> reversed t
 
 val is_empty : _ t -> bool
 

infer/src/absint/AbstractInterpreter.ml

@@ -171,10 +171,9 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
         if Config.write_html then dump_html ~pp_instr pre instr result ;
         result
       in
-      if Instrs.is_empty instrs then
       (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
-        compute_post pre Sil.skip_instr
-      else Container.fold_result ~fold:Instrs.fold ~init:pre instrs ~f:compute_post
+      let instrs = if Instrs.is_empty instrs then Instrs.singleton Sil.skip_instr else instrs in
+      Container.fold_result ~fold:Instrs.fold ~init:pre instrs ~f:compute_post
     in
     match post with
     | Ok astate_post ->