From 69ead917c397fdb9d4916891601bb6b033146099 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 4 Jun 2018 07:51:08 -0700 Subject: [PATCH] Instrs: Arrays and RevArrays only Reviewed By: jvillard Differential Revision: D8187368 fbshipit-source-id: 5f069a7 --- infer/src/IR/Instrs.ml | 139 +++++++++++++++--- infer/src/IR/Instrs.mli | 50 ++++--- infer/src/IR/Procdesc.ml | 2 +- infer/src/IR/Procdesc.mli | 2 +- infer/src/absint/AbstractInterpreter.ml | 39 ++--- infer/src/absint/ProcCfg.ml | 23 ++- infer/src/absint/ProcCfg.mli | 23 ++- infer/src/backend/printer.ml | 2 +- infer/src/biabduction/SymExec.mli | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- infer/src/unit/procCfgTests.ml | 2 +- infer/src/unit/schedulerTests.ml | 2 + 12 files changed, 212 insertions(+), 76 deletions(-) diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index 4972461b6..7c1c0797f 100644 --- a/infer/src/IR/Instrs.ml +++ b/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) diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index cf0f89870..4d35ec1b9 100644 --- a/infer/src/IR/Instrs.mli +++ b/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 diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 98c0d3cab..8d166d801 100644 --- a/infer/src/IR/Procdesc.ml +++ b/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 *) diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index bb44c41b9..e772dfca1 100644 --- a/infer/src/IR/Procdesc.mli +++ b/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 diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 066c75332..5948f4cf8 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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 diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index c64d19913..61e6f6697 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/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) = diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index a9d25c300..9761e8605 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/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 diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index e6d405768..a67b1aa4f 100644 --- a/infer/src/backend/printer.ml +++ b/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)) diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index 7486e3797..9b0c0ab56 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/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. *) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index e8e10ec10..eb063f216 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 31343434f..8576b953e 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/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 diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index 92c10bac1..af17c3a14 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/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