pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

ProcCfg: fold on nodes only

Browse Source 
Summary:
We never really need the list of nodes/succs/preds, we only need to fold over them.
This will reduce garbage for computed lists like in the Exceptional CFG or the OneInstrPerNode CFG.

Reviewed By: ngorogiannis

Differential Revision: D8185665

fbshipit-source-id: d042beb
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent dee25640f8
commit 42b3958a07
13 changed files with 228 additions and 178 deletions
Show Stats Download Patch File Download Diff File

21
infer/src/absint/AbstractInterpreter.ml
Unescape View File

@ -104,17 +104,16 @@ struct
let rec exec_worklist cfg work_queue inv_map proc_data ~debug = let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
let compute_pre node inv_map = let compute_pre node inv_map =
let extract_post_ pred = extract_post (CFG.id pred) inv_map in let extract_post_ pred = extract_post (CFG.id pred) inv_map in
CFG.preds cfg node CFG.fold_preds cfg node ~init:None ~f:(fun joined_post_opt pred ->
|> List.fold ~init:None ~f:(fun joined_post_opt pred -> match extract_post_ pred with
match extract_post_ pred with | None ->
| None -> joined_post_opt
joined_post_opt | Some post as some_post ->
| Some post as some_post -> match joined_post_opt with
match joined_post_opt with | None ->
| None -> some_post
some_post | Some joined_post ->
| Some joined_post -> Some (Domain.join joined_post post) )
Some (Domain.join joined_post post) )
in in
match Scheduler.pop work_queue with match Scheduler.pop work_queue with
| Some (_, [], work_queue') -> | Some (_, [], work_queue') ->

147
infer/src/absint/ProcCfg.ml
Unescape View File

@ -116,22 +116,22 @@ module type S = sig
val instrs : node -> Sil.instr list val instrs : node -> Sil.instr list
(** get the instructions from a node *) (** get the instructions from a node *)
val succs : t -> node -> node list val fold_succs : t -> (node, node, 'accum) Container.fold
val preds : t -> node -> node list val fold_preds : t -> (node, node, 'accum) Container.fold
(** all predecessors (normal and exceptional) *) (** fold over all predecessors (normal and exceptional) *)
val normal_succs : t -> node -> node list val fold_normal_succs : t -> (node, node, 'accum) Container.fold
(** non-exceptional successors *) (** fold over non-exceptional successors *)
val normal_preds : t -> node -> node list val fold_normal_preds : t -> (node, node, 'accum) Container.fold
(** non-exceptional predecessors *) (** fold over non-exceptional predecessors *)
val exceptional_succs : t -> node -> node list val fold_exceptional_succs : t -> (node, node, 'accum) Container.fold
(** exceptional successors *) (** fold over exceptional successors *)
val exceptional_preds : t -> node -> node list val fold_exceptional_preds : t -> (node, node, 'accum) Container.fold
(** exceptional predecessors *) (** fold over exceptional predecessors *)
val start_node : t -> node val start_node : t -> node
@ -139,7 +139,7 @@ module type S = sig
val proc_desc : t -> Procdesc.t val proc_desc : t -> Procdesc.t
val nodes : t -> node list val fold_nodes : (t, node, 'accum) Container.fold
val from_pdesc : Procdesc.t -> t val from_pdesc : Procdesc.t -> t
@ -156,18 +156,18 @@ module Normal = struct
let instrs = Procdesc.Node.get_instrs let instrs = Procdesc.Node.get_instrs
let normal_succs _ n = Procdesc.Node.get_succs n let fold_normal_succs _ n ~init ~f = n |> Procdesc.Node.get_succs |> List.fold ~init ~f
let normal_preds _ n = Procdesc.Node.get_preds n let fold_normal_preds _ n ~init ~f = n |> Procdesc.Node.get_preds |> List.fold ~init ~f
(* prune away exceptional control flow *) (* prune away exceptional control flow *)
let exceptional_succs _ _ = [] let fold_exceptional_succs _ _ ~init ~f:_ = init
let exceptional_preds _ _ = [] let fold_exceptional_preds _ _ ~init ~f:_ = init
let succs = normal_succs let fold_succs = fold_normal_succs
let preds = normal_preds let fold_preds = fold_normal_preds
let start_node = Procdesc.get_start_node let start_node = Procdesc.get_start_node
@ -175,7 +175,7 @@ module Normal = struct
let proc_desc t = t let proc_desc t = t
let nodes = Procdesc.get_nodes let fold_nodes = Procdesc.fold_nodes
let from_pdesc pdesc = pdesc let from_pdesc pdesc = pdesc
@ -192,7 +192,7 @@ module Exceptional = struct
include (DefaultNode : module type of DefaultNode with type t := node) include (DefaultNode : module type of DefaultNode with type t := node)
let exceptional_succs _ n = Procdesc.Node.get_exn n let fold_exceptional_succs _ n ~init ~f = n |> Procdesc.Node.get_exn |> List.fold ~init ~f
let from_pdesc pdesc = let from_pdesc pdesc =
(* map from a node to its exceptional predecessors *) (* map from a node to its exceptional predecessors *)
@ -207,46 +207,52 @@ module Exceptional = struct
Procdesc.IdMap.add exn_succ_node_id (n :: existing_exn_preds) exn_preds_acc Procdesc.IdMap.add exn_succ_node_id (n :: existing_exn_preds) exn_preds_acc
else exn_preds_acc else exn_preds_acc
in in
List.fold ~f:add_exn_pred ~init:exn_preds_acc (exceptional_succs pdesc n) fold_exceptional_succs pdesc n ~f:add_exn_pred ~init:exn_preds_acc
in in
let exceptional_preds = let exceptional_preds =
List.fold ~f:add_exn_preds ~init:Procdesc.IdMap.empty (Procdesc.get_nodes pdesc) Procdesc.fold_nodes pdesc ~f:add_exn_preds ~init:Procdesc.IdMap.empty
in in
(pdesc, exceptional_preds) (pdesc, exceptional_preds)
let instrs = Procdesc.Node.get_instrs let instrs = Procdesc.Node.get_instrs
let nodes (t, _) = Procdesc.get_nodes t let fold_nodes (t, _) ~init ~f = Procdesc.fold_nodes t ~init ~f
let normal_succs _ n = Procdesc.Node.get_succs n let fold_normal_succs _ n ~init ~f = n |> Procdesc.Node.get_succs |> List.fold ~init ~f
let normal_preds _ n = Procdesc.Node.get_preds n let fold_normal_preds _ n ~init ~f = n |> Procdesc.Node.get_preds |> List.fold ~init ~f
let exceptional_preds (_, exn_pred_map) n = let fold_exceptional_preds (_, exn_pred_map) n ~init ~f =
try Procdesc.IdMap.find (Procdesc.Node.get_id n) exn_pred_map with Caml.Not_found -> [] match Procdesc.IdMap.find (Procdesc.Node.get_id n) exn_pred_map with
| exn_preds ->
List.fold exn_preds ~init ~f
| exception Caml.Not_found ->
init
(** get all normal and exceptional successors of [n]. *) let fold_avoid_duplicates fold_normal_alpha fold_normal_idset fold_exceptional t n ~init ~f =
let succs t n = (* need a copy of [fold_normal] otherwise OCaml wants the types *)
let normal_succs = normal_succs t n in let acc_normal = fold_normal_alpha t n ~init ~f in
match exceptional_succs t n with let normal_set =
| [] -> lazy
normal_succs (fold_normal_idset t n ~init:IdSet.empty ~f:(fun set node ->
| exceptional_succs -> IdSet.add (Procdesc.Node.get_id node) set ))
normal_succs @ exceptional_succs |> List.sort ~compare:Procdesc.Node.compare in
|> List.remove_consecutive_duplicates ~equal:Procdesc.Node.equal let f acc node =
if IdSet.mem (Procdesc.Node.get_id node) (Lazy.force_val normal_set) then acc else f acc node
in
fold_exceptional t n ~init:acc_normal ~f
(** fold over all normal and exceptional successors of [n]. *)
let fold_succs t n ~init ~f =
fold_avoid_duplicates fold_normal_succs fold_normal_succs fold_exceptional_succs t n ~init ~f
(** get all normal and exceptional predecessors of [n]. *)
let preds t n = (** fold over all normal and exceptional predecessors of [n]. *)
let normal_preds = normal_preds t n in let fold_preds t n ~init ~f =
match exceptional_preds t n with fold_avoid_duplicates fold_normal_preds fold_normal_preds fold_exceptional_preds t n ~init ~f
| [] ->
normal_preds
| exceptional_preds ->
normal_preds @ exceptional_preds |> List.sort ~compare:Procdesc.Node.compare
|> List.remove_consecutive_duplicates ~equal:Procdesc.Node.equal
let proc_desc (pdesc, _) = pdesc let proc_desc (pdesc, _) = pdesc
@ -264,21 +270,21 @@ module Backward (Base : S) = struct
let instrs n = List.rev (Base.instrs n) let instrs n = List.rev (Base.instrs n)
let succs = Base.preds let fold_succs = Base.fold_preds
let preds = Base.succs let fold_preds = Base.fold_succs
let start_node = Base.exit_node let start_node = Base.exit_node
let exit_node = Base.start_node let exit_node = Base.start_node
let normal_succs = Base.normal_preds let fold_normal_succs = Base.fold_normal_preds
let normal_preds = Base.normal_succs let fold_normal_preds = Base.fold_normal_succs
let exceptional_succs = Base.exceptional_preds let fold_exceptional_succs = Base.fold_exceptional_preds
let exceptional_preds = Base.exceptional_succs let fold_exceptional_preds = Base.fold_exceptional_succs
end end
module OneInstrPerNode (Base : S with type node = Procdesc.Node.t and type id = Procdesc.Node.id) = module OneInstrPerNode (Base : S with type node = Procdesc.Node.t and type id = Procdesc.Node.id) =
@ -305,27 +311,32 @@ struct
let last_of_node node = (node, max 0 (List.length (Base.instrs node) - 1)) let last_of_node node = (node, max 0 (List.length (Base.instrs node) - 1))
let normal_succs _ _ = (* not used *) assert false let fold_normal_succs _ _ ~init:_ ~f:_ = (* not used *) assert false
let exceptional_succs _ _ = (* not used *) assert false let fold_exceptional_succs _ _ ~init:_ ~f:_ = (* not used *) assert false
let succs cfg (node, index) = let fold_succs cfg (node, index) ~init ~f =
let succ_index = index + 1 in let succ_index = index + 1 in
if IList.mem_nth (Base.instrs node) succ_index then [(node, succ_index)] if IList.mem_nth (Base.instrs node) succ_index then f init (node, succ_index)
else List.map ~f:first_of_node (Base.succs cfg node) else
let f acc node = f acc (first_of_node node) in
Base.fold_succs cfg node ~init ~f
let call_on_last ~f acc node = f acc (last_of_node node)
let normal_preds cfg (node, index) = let fold_normal_preds cfg (node, index) ~init ~f =
if index >= 1 then [(node, index - 1)] if index >= 1 then f init (node, index - 1)
else List.map ~f:last_of_node (Base.normal_preds cfg node) else Base.fold_normal_preds cfg node ~init ~f:(call_on_last ~f)
let exceptional_preds cfg (node, index) = let fold_exceptional_preds cfg (node, index) ~init ~f =
if index >= 1 then [] else List.map ~f:last_of_node (Base.exceptional_preds cfg node) if index >= 1 then init else Base.fold_exceptional_preds cfg node ~init ~f:(call_on_last ~f)
let preds cfg (node, index) = let fold_preds cfg (node, index) ~init ~f =
if index >= 1 then [(node, index - 1)] else List.map ~f:last_of_node (Base.preds cfg node) if index >= 1 then f init (node, index - 1)
else Base.fold_preds cfg node ~init ~f:(call_on_last ~f)
let start_node cfg = first_of_node (Base.start_node cfg) let start_node cfg = first_of_node (Base.start_node cfg)
@ -334,15 +345,15 @@ struct
let proc_desc = Base.proc_desc let proc_desc = Base.proc_desc
let nodes = let fold_nodes cfg ~init ~f =
let nodes_of_node node = let f init node =
match Base.instrs node with match Base.instrs node with
| [] -> | [] ->
[(node, 0)] f init (node, 0)
| instrs -> | instrs ->
List.mapi ~f:(fun index _instr -> (node, index)) instrs List.foldi instrs ~init ~f:(fun index acc _instr -> f acc (node, index))
in in
fun cfg -> List.concat_map ~f:nodes_of_node (Base.nodes cfg) Base.fold_nodes cfg ~init ~f
let from_pdesc = Base.from_pdesc let from_pdesc = Base.from_pdesc

26
infer/src/absint/ProcCfg.mli
Unescape View File

@ -49,23 +49,23 @@ module type S = sig
val instrs : node -> Sil.instr list val instrs : node -> Sil.instr list
(** get the instructions from a node *) (** get the instructions from a node *)
val succs : t -> node -> node list val fold_succs : t -> (node, node, 'accum) Container.fold
(** all successors (normal and exceptional) *) (** fold over all successors (normal and exceptional) *)
val preds : t -> node -> node list val fold_preds : t -> (node, node, 'accum) Container.fold
(** all predecessors (normal and exceptional) *) (** fold over all predecessors (normal and exceptional) *)
val normal_succs : t -> node -> node list val fold_normal_succs : t -> (node, node, 'accum) Container.fold
(** non-exceptional successors *) (** fold over non-exceptional successors *)
val normal_preds : t -> node -> node list val fold_normal_preds : t -> (node, node, 'accum) Container.fold
(** non-exceptional predecessors *) (** fold over non-exceptional predecessors *)
val exceptional_succs : t -> node -> node list val fold_exceptional_succs : t -> (node, node, 'accum) Container.fold
(** exceptional successors *) (** fold over exceptional successors *)
val exceptional_preds : t -> node -> node list val fold_exceptional_preds : t -> (node, node, 'accum) Container.fold
(** exceptional predescessors *) (** fold over exceptional predescessors *)
val start_node : t -> node val start_node : t -> node
@ -73,7 +73,7 @@ module type S = sig
val proc_desc : t -> Procdesc.t val proc_desc : t -> Procdesc.t
val nodes : t -> node list val fold_nodes : (t, node, 'accum) Container.fold
val from_pdesc : Procdesc.t -> t val from_pdesc : Procdesc.t -> t

4
infer/src/absint/Scheduler.ml
Unescape View File

@ -50,7 +50,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
let priority t = t.priority let priority t = t.priority
let compute_priority cfg node visited_preds = let compute_priority cfg node visited_preds =
List.length (CFG.preds cfg node) - IdSet.cardinal visited_preds Container.length ~fold:(CFG.fold_preds cfg) node - IdSet.cardinal visited_preds
let make cfg node = let make cfg node =
@ -81,7 +81,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in
M.add id_to_schedule new_work worklist_acc M.add id_to_schedule new_work worklist_acc
in in
let new_worklist = List.fold ~f:schedule_succ ~init:t.worklist (CFG.succs t.cfg node) in let new_worklist = CFG.fold_succs t.cfg node ~f:schedule_succ ~init:t.worklist in
{t with worklist= new_worklist} {t with worklist= new_worklist}

6
infer/src/backend/preanal.ml
Unescape View File

@ -139,8 +139,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
let node_removetmps_instruction loc ids = let node_removetmps_instruction loc ids =
if ids <> [] then Some (Sil.Remove_temps (List.rev ids, loc)) else None if ids <> [] then Some (Sil.Remove_temps (List.rev ids, loc)) else None
in in
List.iter Container.iter nullify_proc_cfg ~fold:ProcCfg.Exceptional.fold_nodes ~f:(fun node ->
~f:(fun node ->
match NullifyAnalysis.extract_post (ProcCfg.Exceptional.id node) nullify_inv_map with match NullifyAnalysis.extract_post (ProcCfg.Exceptional.id node) nullify_inv_map with
| Some (_, to_nullify) -> | Some (_, to_nullify) ->
let pvars_to_nullify, ids_to_remove = let pvars_to_nullify, ids_to_remove =
@ -162,8 +161,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
|> IList.opt_cons (node_removetmps_instruction loc ids_to_remove) |> IList.opt_cons (node_removetmps_instruction loc ids_to_remove)
|> Procdesc.Node.append_instrs node |> Procdesc.Node.append_instrs node
| None -> | None ->
() ) () ) ;
(ProcCfg.Exceptional.nodes nullify_proc_cfg) ;
(* nullify all address taken variables *) (* nullify all address taken variables *)
if not (AddressTaken.Domain.is_empty address_taken_vars) then if not (AddressTaken.Domain.is_empty address_taken_vars) then
let exit_node = ProcCfg.Exceptional.exit_node nullify_proc_cfg in let exit_node = ProcCfg.Exceptional.exit_node nullify_proc_cfg in

15
infer/src/biabduction/interproc.ml
Unescape View File

@ -300,10 +300,12 @@ let propagate_nodes_divergence tenv (proc_cfg: ProcCfg.Exceptional.t) (pset: Pat
Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons) ; Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons) ;
L.d_ln () ; L.d_ln () ;
propagate wl pname ~is_exception:false prop_incons exit_node ) ; propagate wl pname ~is_exception:false prop_incons exit_node ) ;
ProcCfg.Exceptional.normal_succs proc_cfg curr_node Container.iter curr_node
|> List.iter ~f:(propagate wl pname ~is_exception:false pset_ok) ; ~fold:(ProcCfg.Exceptional.fold_normal_succs proc_cfg)
ProcCfg.Exceptional.exceptional_succs proc_cfg curr_node ~f:(propagate wl pname ~is_exception:false pset_ok) ;
|> List.iter ~f:(propagate wl pname ~is_exception:true pset_exn) Container.iter curr_node
~fold:(ProcCfg.Exceptional.fold_exceptional_succs proc_cfg)
~f:(propagate wl pname ~is_exception:true pset_exn)
(* ===================== END of symbolic execution ===================== *) (* ===================== END of symbolic execution ===================== *)
@ -313,13 +315,11 @@ let propagate_nodes_divergence tenv (proc_cfg: ProcCfg.Exceptional.t) (pset: Pat
let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo: Paths.PathSet.t) = let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo: Paths.PathSet.t) =
let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
let curr_node_id = ProcCfg.Exceptional.id curr_node in let curr_node_id = ProcCfg.Exceptional.id curr_node in
let succ_nodes = ProcCfg.Exceptional.normal_succs proc_cfg curr_node in
let new_dset = edgeset_todo in let new_dset = edgeset_todo in
let old_dset = Join_table.find wl.Worklist.join_table curr_node_id in let old_dset = Join_table.find wl.Worklist.join_table curr_node_id in
let old_dset', new_dset' = Dom.pathset_join pname tenv old_dset new_dset in let old_dset', new_dset' = Dom.pathset_join pname tenv old_dset new_dset in
Join_table.add wl.Worklist.join_table curr_node_id (Paths.PathSet.union old_dset' new_dset') ; Join_table.add wl.Worklist.join_table curr_node_id (Paths.PathSet.union old_dset' new_dset') ;
List.iter Container.iter curr_node ~fold:(ProcCfg.Exceptional.fold_normal_succs proc_cfg) ~f:(fun node ->
~f:(fun node ->
Paths.PathSet.iter Paths.PathSet.iter
(fun prop path -> (fun prop path ->
State.set_path path None ; State.set_path path None ;
@ -327,7 +327,6 @@ let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo: Paths.PathSet.t) =
(Paths.PathSet.from_renamed_list [(prop, path)]) (Paths.PathSet.from_renamed_list [(prop, path)])
node ) node )
new_dset' ) new_dset' )
succ_nodes
let prop_max_size = ref (0, Prop.prop_emp) let prop_max_size = ref (0, Prop.prop_emp)

22
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -322,19 +322,14 @@ module Report = struct
let rec is_end_of_block_or_procedure (cfg: CFG.t) node rem_instrs = let rec is_end_of_block_or_procedure (cfg: CFG.t) node rem_instrs =
List.for_all rem_instrs ~f:Sil.instr_is_auxiliary List.for_all rem_instrs ~f:Sil.instr_is_auxiliary
&& &&
match CFG.succs cfg node with match IContainer.singleton_or_more node ~fold:(CFG.fold_succs cfg) with
| [] -> | IContainer.Empty ->
true true
| [succ] | Singleton succ ->
-> ( (* [succ] is a join, i.e. [node] is the end of a block *)
is_end_of_block_or_procedure cfg succ (CFG.instrs succ) IContainer.mem_nth succ 1 ~fold:(CFG.fold_preds cfg)
|| || is_end_of_block_or_procedure cfg succ (CFG.instrs succ)
match CFG.preds cfg succ with | More ->
| _ :: _ :: _ ->
true (* [succ] is a join, i.e. [node] is the end of a block *)
| _ ->
false )
| _ :: _ :: _ ->
false false
end end
@ -503,8 +498,7 @@ module Report = struct
let check_proc let check_proc
: Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t = : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t =
fun summary pdesc tenv cfg inv_map -> fun summary pdesc tenv cfg inv_map ->
CFG.nodes cfg CFG.fold_nodes cfg ~f:(check_node summary pdesc tenv cfg inv_map) ~init:PO.ConditionSet.empty
|> List.fold ~f:(check_node summary pdesc tenv cfg inv_map) ~init:PO.ConditionSet.empty
let make_err_trace : Trace.t -> string -> Errlog.loc_trace = let make_err_trace : Trace.t -> string -> Errlog.loc_trace =

18
infer/src/checkers/cost.ml
Unescape View File

@ -191,7 +191,7 @@ module BoundMap = struct
Node.IdMap.add node_id BasicCost.zero bound_map Node.IdMap.add node_id BasicCost.zero bound_map
in in
let bound_map = let bound_map =
List.fold (NodeCFG.nodes node_cfg) ~f:compute_node_upper_bound ~init:Node.IdMap.empty NodeCFG.fold_nodes node_cfg ~f:compute_node_upper_bound ~init:Node.IdMap.empty
in in
print_upper_bound_map bound_map ; bound_map print_upper_bound_map bound_map ; bound_map
@ -215,10 +215,10 @@ end
module StructuralConstraints = struct module StructuralConstraints = struct
type t = {single: Node.id list; sum: Node.IdSet.t list} type t = {single: Node.id list; sum: Node.IdSet.t list}
(* (*
Finds subset of constraints of node k. Finds subset of constraints of node k.
It returns a pair (single_constraints, sum_constraints) where single constraints are It returns a pair (single_constraints, sum_constraints) where single constraints are
of the form 'x_k <= x_j' and sum constraints are of the form 'x_k <= x_j1 +...+ x_jn'. of the form 'x_k <= x_j' and sum constraints are of the form 'x_k <= x_j1 +...+ x_jn'.
*) *)
let get_constraints_of_node constraints k = let get_constraints_of_node constraints k =
let c = Node.IdMap.find_opt k constraints in let c = Node.IdMap.find_opt k constraints in
@ -267,7 +267,7 @@ module StructuralConstraints = struct
{single= List.append preds.single succs.single; sum= List.append preds.sum succs.sum} acc {single= List.append preds.single succs.single; sum= List.append preds.sum succs.sum} acc
in in
let constraints = let constraints =
List.fold (NodeCFG.nodes node_cfg) ~f:compute_node_constraints ~init:Node.IdMap.empty NodeCFG.fold_nodes node_cfg ~f:compute_node_constraints ~init:Node.IdMap.empty
in in
print_constraints_map constraints ; constraints print_constraints_map constraints ; constraints
end end
@ -411,12 +411,12 @@ module MinTree = struct
with_cache (minimum_propagation bound_map constraints) |> Staged.unstage with_cache (minimum_propagation bound_map constraints) |> Staged.unstage
in in
let min_trees = let min_trees =
List.fold NodeCFG.fold_nodes node_cfg
~f:(fun acc node -> ~f:(fun acc node ->
let nid = Node.id node in let nid = Node.id node in
let tree = minimum_propagation (nid, Node.IdSet.empty) in let tree = minimum_propagation (nid, Node.IdSet.empty) in
(nid, tree) :: acc ) (nid, tree) :: acc )
~init:[] (NodeCFG.nodes node_cfg) ~init:[]
in in
List.iter List.iter
~f:(fun (nid, t) -> L.(debug Analysis Medium) "@\n node %a = %a @\n" Node.pp_id nid pp t) ~f:(fun (nid, t) -> L.(debug Analysis Medium) "@\n node %a = %a @\n" Node.pp_id nid pp t)
@ -599,7 +599,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
"@\n[COST ANALYSIS] PROCESSING MIN_TREE for PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" "@\n[COST ANALYSIS] PROCESSING MIN_TREE for PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n"
Typ.Procname.pp Typ.Procname.pp
(Procdesc.get_proc_name proc_desc) (Procdesc.get_proc_name proc_desc)
(List.length (NodeCFG.nodes node_cfg)) (Container.length ~fold:NodeCFG.fold_nodes node_cfg)
BasicCost.pp exit_cost ; BasicCost.pp exit_cost ;
check_and_report_infinity exit_cost proc_desc summary ; check_and_report_infinity exit_cost proc_desc summary ;
Payload.update_summary {post= exit_cost} summary Payload.update_summary {post= exit_cost} summary

2
infer/src/checkers/liveness.ml
Unescape View File

@ -201,5 +201,5 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
| None -> | None ->
() ) () )
in in
List.iter (CFG.nodes cfg) ~f:report_on_node ; Container.iter cfg ~fold:CFG.fold_nodes ~f:report_on_node ;
summary summary

25
infer/src/istd/IContainer.ml
Unescape View File

@ -0,0 +1,25 @@
(*
* Copyright (c) 2018 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
type 'a singleton_or_more = Empty | Singleton of 'a | More
let singleton_or_more ~fold t =
With_return.with_return (fun {return} ->
fold t ~init:Empty ~f:(fun acc item ->
match acc with Empty -> Singleton item | _ -> return More ) )
let mem_nth ~fold t index =
With_return.with_return (fun {return} ->
let _ : int =
fold t ~init:index ~f:(fun index _ -> if index <= 0 then return true else index - 1)
in
false )

17
infer/src/istd/IContainer.mli
Unescape View File

@ -0,0 +1,17 @@
(*
* Copyright (c) 2018 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
type 'a singleton_or_more = Empty | Singleton of 'a | More
val singleton_or_more :
fold:('t, 'a, 'a singleton_or_more) Container.fold -> 't -> 'a singleton_or_more
val mem_nth : fold:('t, _, int) Container.fold -> 't -> int -> bool

83
infer/src/unit/procCfgTests.ml
Unescape View File

@ -51,7 +51,10 @@ let tests =
let pp_node_list fmt l = F.pp_print_list ~pp_sep Procdesc.Node.pp fmt l in let pp_node_list fmt l = F.pp_print_list ~pp_sep Procdesc.Node.pp fmt l in
F.fprintf fmt "Expected output %a but got %a" pp_node_list expected pp_node_list actual F.fprintf fmt "Expected output %a but got %a" pp_node_list expected pp_node_list actual
in in
let create_test input expected _ = assert_equal ~cmp ~pp_diff input expected in let create_test ~fold input expected _ =
let input = Container.to_list input ~fold in
assert_equal ~cmp ~pp_diff input expected
in
let instr_test = let instr_test =
let instr_test_ _ = let instr_test_ _ =
( match ProcCfg.Normal.instrs n1 with ( match ProcCfg.Normal.instrs n1 with
@ -83,66 +86,70 @@ let tests =
let n1'' = BackwardInstrCfg.underlying_node backward_instr_n1 in let n1'' = BackwardInstrCfg.underlying_node backward_instr_n1 in
assert_bool "underlying_node should return node of underlying CFG type" (phys_equal n1 n1'') ; assert_bool "underlying_node should return node of underlying CFG type" (phys_equal n1 n1'') ;
(* test the preds/succs using backward + instr cfg *) (* test the preds/succs using backward + instr cfg *)
let check_backward_instr_ f backward_instr_node expected_instrs = let check_backward_instr_ fold backward_instr_node expected_instrs =
match f backward_instr_proc_cfg backward_instr_node with match Container.to_list ~fold:(fold backward_instr_proc_cfg) backward_instr_node with
| [n] -> | [n] ->
assert_equal (BackwardInstrCfg.instrs n) expected_instrs assert_equal (BackwardInstrCfg.instrs n) expected_instrs
| _ -> | _ ->
assert_failure "Expected exactly one node" assert_failure "Expected exactly one node"
in in
check_backward_instr_ BackwardInstrCfg.preds backward_instr_n1 [dummy_instr2] ; check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n1 [dummy_instr2] ;
let backward_instr_n2 = BackwardInstrCfg.of_underlying_node n2 in let backward_instr_n2 = BackwardInstrCfg.of_underlying_node n2 in
check_backward_instr_ BackwardInstrCfg.preds backward_instr_n2 [] ; check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n2 [] ;
let backward_instr_n3 = BackwardInstrCfg.of_underlying_node n3 in let backward_instr_n3 = BackwardInstrCfg.of_underlying_node n3 in
check_backward_instr_ BackwardInstrCfg.preds backward_instr_n3 [] ; check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n3 [] ;
check_backward_instr_ BackwardInstrCfg.normal_succs backward_instr_n2 [dummy_instr2] check_backward_instr_ BackwardInstrCfg.fold_normal_succs backward_instr_n2 [dummy_instr2]
in in
"instr_test" >:: instr_test_ "instr_test" >:: instr_test_
in in
let graph_tests = let graph_tests =
[ (* test the succs of the normal cfg. forward... *) [ (* test the succs of the normal cfg. forward... *)
("succs_n1", ProcCfg.Normal.succs normal_proc_cfg n1, [n2]) ("succs_n1", ProcCfg.Normal.fold_succs normal_proc_cfg, n1, [n2])
; ("normal_succs_n1", ProcCfg.Normal.normal_succs normal_proc_cfg n1, [n2]) ; ("normal_succs_n1", ProcCfg.Normal.fold_normal_succs normal_proc_cfg, n1, [n2])
; ("succs_n2", ProcCfg.Normal.succs normal_proc_cfg n2, [n4]) ; ("succs_n2", ProcCfg.Normal.fold_succs normal_proc_cfg, n2, [n4])
; ("normal_succs_n2", ProcCfg.Normal.normal_succs normal_proc_cfg n2, [n4]) ; ("normal_succs_n2", ProcCfg.Normal.fold_normal_succs normal_proc_cfg, n2, [n4])
; ("succs_n3", ProcCfg.Normal.succs normal_proc_cfg n3, [n4]) ; ("succs_n3", ProcCfg.Normal.fold_succs normal_proc_cfg, n3, [n4])
; ("normal_succs_n3", ProcCfg.Normal.normal_succs normal_proc_cfg n3, [n4]) ; ("normal_succs_n3", ProcCfg.Normal.fold_normal_succs normal_proc_cfg, n3, [n4])
; (* ... and backward... *) ; (* ... and backward... *)
("succs_n1_bw", BackwardCfg.preds backward_proc_cfg n1, [n2]) ("succs_n1_bw", BackwardCfg.fold_preds backward_proc_cfg, n1, [n2])
; ("normal_succs_n1_bw", BackwardCfg.normal_preds backward_proc_cfg n1, [n2]) ; ("normal_succs_n1_bw", BackwardCfg.fold_normal_preds backward_proc_cfg, n1, [n2])
; ("succs_n2_bw", BackwardCfg.preds backward_proc_cfg n2, [n4]) ; ("succs_n2_bw", BackwardCfg.fold_preds backward_proc_cfg, n2, [n4])
; ("normal_succs_n2_bw", BackwardCfg.normal_preds backward_proc_cfg n2, [n4]) ; ("normal_succs_n2_bw", BackwardCfg.fold_normal_preds backward_proc_cfg, n2, [n4])
; ("succs_n3_bw", BackwardCfg.preds backward_proc_cfg n3, [n4]) ; ("succs_n3_bw", BackwardCfg.fold_preds backward_proc_cfg, n3, [n4])
; ("normal_succs_n3_bw", BackwardCfg.normal_preds backward_proc_cfg n3, [n4]) ; ("normal_succs_n3_bw", BackwardCfg.fold_normal_preds backward_proc_cfg, n3, [n4])
; (* test the preds of the normal cfg... *) ; (* test the preds of the normal cfg... *)
("preds_n2", ProcCfg.Normal.normal_preds normal_proc_cfg n2, [n1]) ("preds_n2", ProcCfg.Normal.fold_normal_preds normal_proc_cfg, n2, [n1])
; ("normal_preds_n2", ProcCfg.Normal.normal_preds normal_proc_cfg n2, [n1]) ; ("normal_preds_n2", ProcCfg.Normal.fold_normal_preds normal_proc_cfg, n2, [n1])
; (* ...and the backward cfg... *) ; (* ...and the backward cfg... *)
("preds_n2_bw", BackwardCfg.normal_succs backward_proc_cfg n2, [n1]) ("preds_n2_bw", BackwardCfg.fold_normal_succs backward_proc_cfg, n2, [n1])
; ("normal_preds_n2_bw", BackwardCfg.normal_succs backward_proc_cfg n2, [n1]) ; ("normal_preds_n2_bw", BackwardCfg.fold_normal_succs backward_proc_cfg, n2, [n1])
; (* we shouldn't see any exn succs or preds even though we added them *) ; (* we shouldn't see any exn succs or preds even though we added them *)
("no_exn_succs_n1", ProcCfg.Normal.exceptional_succs normal_proc_cfg n1, []) ("no_exn_succs_n1", ProcCfg.Normal.fold_exceptional_succs normal_proc_cfg, n1, [])
; ("no_exn_preds_n3", ProcCfg.Normal.exceptional_preds normal_proc_cfg n3, []) ; ("no_exn_preds_n3", ProcCfg.Normal.fold_exceptional_preds normal_proc_cfg, n3, [])
; (* same in the backward cfg *) ; (* same in the backward cfg *)
("no_exn_succs_n1_bw", BackwardCfg.exceptional_preds backward_proc_cfg n1, []) ("no_exn_succs_n1_bw", BackwardCfg.fold_exceptional_preds backward_proc_cfg, n1, [])
; ("no_exn_preds_n3_bw", BackwardCfg.exceptional_succs backward_proc_cfg n3, []) ; ("no_exn_preds_n3_bw", BackwardCfg.fold_exceptional_succs backward_proc_cfg, n3, [])
; (* now, test the exceptional succs in the exceptional cfg. *) ; (* now, test the exceptional succs in the exceptional cfg. *)
("exn_succs_n1", ProcCfg.Exceptional.exceptional_succs exceptional_proc_cfg n1, [n3]) ("exn_succs_n1", ProcCfg.Exceptional.fold_exceptional_succs exceptional_proc_cfg, n1, [n3])
; ("exn_succs_n2", ProcCfg.Exceptional.exceptional_succs exceptional_proc_cfg n2, [n3]) ; ("exn_succs_n2", ProcCfg.Exceptional.fold_exceptional_succs exceptional_proc_cfg, n2, [n3])
; ("exn_succs_n3", ProcCfg.Exceptional.exceptional_succs exceptional_proc_cfg n3, [n4]) ; ("exn_succs_n3", ProcCfg.Exceptional.fold_exceptional_succs exceptional_proc_cfg, n3, [n4])
; (* test exceptional pred links *) ; (* test exceptional pred links *)
("exn_preds_n3", ProcCfg.Exceptional.exceptional_preds exceptional_proc_cfg n3, [n2; n1]) ( "exn_preds_n3"
, ProcCfg.Exceptional.fold_exceptional_preds exceptional_proc_cfg
, n3
, [n2; n1] )
; (* succs should return both normal and exceptional successors *) ; (* succs should return both normal and exceptional successors *)
("exn_all_succs_n1", ProcCfg.Exceptional.succs exceptional_proc_cfg n1, [n3; n2]) ("exn_all_succs_n1", ProcCfg.Exceptional.fold_succs exceptional_proc_cfg, n1, [n3; n2])
; (* but, should not return duplicates *) ; (* but, should not return duplicates *)
("exn_all_succs_n3", ProcCfg.Exceptional.succs exceptional_proc_cfg n3, [n4]) ("exn_all_succs_n3", ProcCfg.Exceptional.fold_succs exceptional_proc_cfg, n3, [n4])
; (* similarly, preds should return both normal and exceptional predecessors *) ; (* similarly, preds should return both normal and exceptional predecessors *)
("exn_all_preds_n3", ProcCfg.Exceptional.preds exceptional_proc_cfg n3, [n2; n1]) ("exn_all_preds_n3", ProcCfg.Exceptional.fold_preds exceptional_proc_cfg, n3, [n2; n1])
; ("exn_all_preds_n4", ProcCfg.Exceptional.preds exceptional_proc_cfg n4, [n3; n2]) ; ("exn_all_preds_n4", ProcCfg.Exceptional.fold_preds exceptional_proc_cfg, n4, [n3; n2])
; (* finally, normal_succs/normal_preds shouldn't return exceptional edges *) ; (* finally, normal_succs/normal_preds shouldn't return exceptional edges *)
("exn_normal_succs_n1", ProcCfg.Exceptional.normal_succs exceptional_proc_cfg n1, [n2]) ("exn_normal_succs_n1", ProcCfg.Exceptional.fold_normal_succs exceptional_proc_cfg, n1, [n2])
; ("exn_normal_preds_n2", ProcCfg.Exceptional.normal_preds exceptional_proc_cfg n2, [n1]) ] ; ("exn_normal_preds_n2", ProcCfg.Exceptional.fold_normal_preds exceptional_proc_cfg, n2, [n1])
|> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected) ]
|> List.map ~f:(fun (name, fold, input, expected) -> name >:: create_test ~fold input expected)
in in
let tests = instr_test :: graph_tests in let tests = instr_test :: graph_tests in
"procCfgSuite" >::: tests "procCfgSuite" >::: tests

20
infer/src/unit/schedulerTests.ml
Unescape View File

@ -57,33 +57,33 @@ module MockProcCfg = struct
let equal_id = Int.equal let equal_id = Int.equal
let succs t n = let fold_succs t n ~init ~f =
let node_id = id n in let node_id = id n in
List.find ~f:(fun (node, _) -> equal_id (id node) node_id) t List.find ~f:(fun (node, _) -> equal_id (id node) node_id) t
|> Option.value_map ~f:snd ~default:[] |> Option.value_map ~f:snd ~default:[] |> List.fold ~init ~f
let preds t n = let fold_preds t n ~init ~f =
try try
let node_id = id n in let node_id = id n in
List.filter List.filter
~f:(fun (_, succs) -> List.exists ~f:(fun node -> equal_id (id node) node_id) succs) ~f:(fun (_, succs) -> List.exists ~f:(fun node -> equal_id (id node) node_id) succs)
t t
|> List.map ~f:fst |> List.map ~f:fst |> List.fold ~init ~f
with with
| Not_found_s _ | Caml.Not_found -> | Not_found_s _ | Caml.Not_found ->
[] init
let nodes t = List.map ~f:fst t let fold_nodes t ~init ~f = List.map ~f:fst t |> List.fold ~init ~f
let normal_succs = succs let fold_normal_succs = fold_succs
let normal_preds = preds let fold_normal_preds = fold_preds
let exceptional_succs _ _ = [] let fold_exceptional_succs _ _ ~init ~f:_ = init
let exceptional_preds _ _ = [] let fold_exceptional_preds _ _ ~init ~f:_ = init
let from_adjacency_list t = t let from_adjacency_list t = t

Write Preview
Loading…
Cancel
Save