diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index 9a35b0315..8b3d07ea1 100644 --- a/infer/src/IR/Instrs.ml +++ b/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 -> diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index 674b61c28..2bc8eaba1 100644 --- a/infer/src/IR/Instrs.mli +++ b/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 diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index fef307f2a..48876649a 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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 + (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) + 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 ->