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

[IR] Clean up unused parts of Cfg

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D4081060

fbshipit-source-id: 5df5f71
master
Cristiano Calcagno 8 years ago committed by Facebook Github Bot
parent 278c705790
commit ecda199e9d
9 changed files with 50 additions and 97 deletions
Show Stats Download Patch File Download Diff File

71
infer/src/IR/Cfg.re
Unescape View File

@ -21,8 +21,8 @@ let module F = Format;
let module Node = {
type id = int;
type nodekind =
| Start_node proc_desc
| Exit_node proc_desc
| Start_node Procname.t
| Exit_node Procname.t
| Stmt_node string
| Join_node
| Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */
@ -33,22 +33,18 @@ let module Node = {
nd_id: id,
/** distance to the exit node */
mutable nd_dist_exit: option int,
/** dead program variables after executing the instructions */
mutable nd_dead_pvars_after: list Pvar.t,
/** dead program variables before executing the instructions */
mutable nd_deads_before: list Pvar.t,
/** exception nodes in the cfg */
mutable nd_exn: list t,
/** instructions for symbolic execution */
mutable nd_instrs: list Sil.instr,
/** kind of node */
mutable nd_kind: nodekind,
nd_kind: nodekind,
/** location in the source code */
mutable nd_loc: Location.t,
nd_loc: Location.t,
/** predecessor nodes in the cfg */
mutable nd_preds: list t,
/** proc desc from cil */
mutable nd_proc: option proc_desc,
nd_proc: option proc_desc,
/** successor nodes in the cfg */
mutable nd_succs: list t
}
@ -66,20 +62,13 @@ let module Node = {
/** data type for the control flow graph */
type cfg = {
node_id: ref int,
node_list: ref (list t),
name_pdesc_tbl: Procname.Hash.t proc_desc, /** Map proc name to procdesc */
mutable priority_set: Procname.Set.t
/** set of function names to be analyzed first */
mutable node_id: int,
mutable node_list: list t,
name_pdesc_tbl: Procname.Hash.t proc_desc /** Map proc name to procdesc */
};
let create_cfg () =>
/** create a new empty cfg */
{
node_id: ref 0,
node_list: ref [],
name_pdesc_tbl: Procname.Hash.create 1000,
priority_set: Procname.Set.empty
};
let create_cfg () => {node_id: 0, node_list: [], name_pdesc_tbl: Procname.Hash.create 16};
/** compute the list of procedures added or changed in [cfg_new] over [cfg_old] */
let mark_unchanged_pdescs cfg_new cfg_old => {
@ -149,8 +138,8 @@ let module Node = {
Procname.Hash.iter mark_pdesc_if_unchanged new_procs
};
let node_id_gen cfg => {
incr cfg.node_id;
!cfg.node_id
cfg.node_id = cfg.node_id + 1;
cfg.node_id
};
let pdesc_tbl_add cfg proc_name proc_desc =>
Procname.Hash.add cfg.name_pdesc_tbl proc_name proc_desc;
@ -160,8 +149,6 @@ let module Node = {
let dummy () => {
nd_id: 0,
nd_dist_exit: None,
nd_dead_pvars_after: [],
nd_deads_before: [],
nd_instrs: [],
nd_kind: Skip_node "dummy",
nd_loc: Location.dummy,
@ -173,14 +160,12 @@ let module Node = {
let compare node1 node2 => int_compare node1.nd_id node2.nd_id;
let hash node => Hashtbl.hash node.nd_id;
let equal node1 node2 => compare node1 node2 == 0;
let get_all_nodes cfg => !cfg.node_list;
let get_all_nodes cfg => cfg.node_list;
let create cfg loc kind instrs pdesc => {
let node_id = node_id_gen cfg;
let node = {
nd_id: node_id,
nd_dist_exit: None,
nd_dead_pvars_after: [],
nd_deads_before: [],
nd_instrs: instrs,
nd_kind: kind,
nd_loc: loc,
@ -189,7 +174,7 @@ let module Node = {
nd_succs: [],
nd_exn: []
};
cfg.node_list := [node, ...!cfg.node_list];
cfg.node_list = [node, ...cfg.node_list];
pdesc.pd_nodes = [node, ...pdesc.pd_nodes];
node
};
@ -298,16 +283,13 @@ let module Node = {
/** Get the node kind */
let get_kind node => node.nd_kind;
/** Set the node kind */
let set_kind node kind => node.nd_kind = kind;
/** Comparison for node kind */
let kind_compare k1 k2 =>
switch (k1, k2) {
| (Start_node pd1, Start_node pd2) => int_compare pd1.pd_id pd2.pd_id
| (Start_node pn1, Start_node pn2) => Procname.compare pn1 pn2
| (Start_node _, _) => (-1)
| (_, Start_node _) => 1
| (Exit_node pd1, Exit_node pd2) => int_compare pd1.pd_id pd2.pd_id
| (Exit_node pn1, Exit_node pn2) => Procname.compare pn1 pn2
| (Exit_node _, _) => (-1)
| (_, Exit_node _) => 1
| (Stmt_node s1, Stmt_node s2) => string_compare s1 s2
@ -359,27 +341,12 @@ let module Node = {
| [instr, ..._] => Sil.instr_get_loc instr
| [] => n.nd_loc
};
/** Set the location of the node */
let set_loc n loc => n.nd_loc = loc;
let pp_id f id => F.fprintf f "%d" id;
let pp f node => pp_id f (get_id node);
let proc_desc_from_name cfg proc_name =>
try (Some (pdesc_tbl_find cfg proc_name)) {
| Not_found => None
};
let set_dead_pvars node after dead =>
if after {
node.nd_dead_pvars_after = dead
} else {
node.nd_deads_before = dead
};
let get_dead_pvars node after =>
if after {
node.nd_dead_pvars_after
} else {
node.nd_deads_before
};
let get_distance_to_exit node => node.nd_dist_exit;
/** Append the instructions to the list of instructions to execute */
@ -424,7 +391,7 @@ let module Node = {
};
let remove_node' filter_out_fun cfg => {
let remove_node_in_cfg nodes => IList.filter filter_out_fun nodes;
cfg.node_list := remove_node_in_cfg !cfg.node_list
cfg.node_list = remove_node_in_cfg cfg.node_list
};
let remove_node_set cfg nodes => remove_node' (fun node' => not (NodeSet.mem node' nodes)) cfg;
let proc_desc_remove cfg name remove_nodes => {
@ -741,8 +708,8 @@ let module Node = {
instrs;
let convert_node_kind =
fun
| Start_node _ => Start_node resolved_proc_desc
| Exit_node _ => Exit_node resolved_proc_desc
| Start_node _ => Start_node resolved_proc_name
| Exit_node _ => Exit_node resolved_proc_name
| node_kind => node_kind;
let node_map = ref NodeMap.empty;
let rec convert_node node => {

18
infer/src/IR/Cfg.rei
Unescape View File

@ -140,8 +140,8 @@ let module Node: {
/** kind of cfg node */
type nodekind =
| Start_node Procdesc.t
| Exit_node Procdesc.t
| Start_node Procname.t
| Exit_node Procname.t
| Stmt_node string
| Join_node
| Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */
@ -188,10 +188,6 @@ let module Node: {
/** Get all the nodes */
let get_all_nodes: cfg => list t;
/** Get the (after/before) dead program variables.
After/before indicated with the true/false flag. */
let get_dead_pvars: t => bool => list Pvar.t;
/** Get the distance to the exit node, if it has been computed */
let get_distance_to_exit: t => option int;
@ -258,16 +254,6 @@ let module Node: {
/** Replace the instructions to be executed. */
let replace_instrs: t => list Sil.instr => unit;
/** Set the (after/before) dead program variables.
After/before indicated with the true/false flag. */
let set_dead_pvars: t => bool => list Pvar.t => unit;
/** Set the node kind */
let set_kind: t => nodekind => unit;
/** Set the source location of the node */
let set_loc: t => Location.t => unit;
/** Set the successor nodes and exception nodes, and build predecessor links */
let set_succs_exn: cfg => t => list t => list t => unit;
};

22
infer/src/backend/dotty.ml
Unescape View File

@ -947,21 +947,19 @@ let pp_local_list fmt etl =
IList.iter (fun (id, ty) ->
Format.fprintf fmt " %a:%a" Mangled.pp id (Typ.pp_full pe_text) ty) etl
let pp_cfgnodelabel fmt (n : Cfg.Node.t) =
let pp_cfgnodelabel pdesc fmt (n : Cfg.Node.t) =
let pp_label fmt n =
match Cfg.Node.get_kind n with
| Cfg.Node.Start_node (pdesc) ->
(* let def = if Cfg.Procdesc.is_defined pdesc then "defined" else "declared" in *)
(* Format.fprintf fmt "Start %a (%s)" pp_id (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) def *)
| Cfg.Node.Start_node pname ->
Format.fprintf fmt "Start %s\\nFormals: %a\\nLocals: %a"
(Procname.to_string (Cfg.Procdesc.get_proc_name pdesc))
(Procname.to_string pname)
pp_etlist (Cfg.Procdesc.get_formals pdesc)
pp_local_list (Cfg.Procdesc.get_locals pdesc);
if IList.length (Cfg.Procdesc.get_captured pdesc) <> 0 then
Format.fprintf fmt "\\nCaptured: %a"
pp_local_list (Cfg.Procdesc.get_captured pdesc)
| Cfg.Node.Exit_node (pdesc) ->
Format.fprintf fmt "Exit %s" (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc))
| Cfg.Node.Exit_node pname ->
Format.fprintf fmt "Exit %s" (Procname.to_string pname)
| Cfg.Node.Join_node ->
Format.fprintf fmt "+"
| Cfg.Node.Prune_node (is_true_branch, _, _) ->
@ -992,8 +990,11 @@ pp_cfgnodename src
pp_cfgnodename dest
*)
let pp_cfgnode fmt (n: Cfg.Node.t) =
F.fprintf fmt "%a [label=\"%a\" %a]\n\t\n" pp_cfgnodename n pp_cfgnodelabel n pp_cfgnodeshape n;
let pp_cfgnode pdesc fmt (n: Cfg.Node.t) =
F.fprintf fmt "%a [label=\"%a\" %a]\n\t\n"
pp_cfgnodename n
(pp_cfgnodelabel pdesc) n
pp_cfgnodeshape n;
let print_edge n1 n2 is_exn =
let color = if is_exn then "[color=\"red\" ]" else "" in
match Cfg.Node.get_kind n2 with
@ -1020,8 +1021,9 @@ let pp_cfgnode fmt (n: Cfg.Node.t) =
let print_icfg source fmt cfg =
let print_node node =
let loc = Cfg.Node.get_loc node in
let pdesc = Cfg.Node.get_proc_desc node in
if (Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file source) then
F.fprintf fmt "%a\n" pp_cfgnode node in
F.fprintf fmt "%a\n" (pp_cfgnode pdesc) node in
IList.iter print_node (Cfg.Node.get_all_nodes cfg)
let write_icfg_dotty_to_file source cfg fname =

7
infer/src/backend/paths.ml
Unescape View File

@ -454,8 +454,7 @@ end = struct
let curr_loc = Cfg.Node.get_loc curr_node in
match Cfg.Node.get_kind curr_node with
| Cfg.Node.Join_node -> () (* omit join nodes from error traces *)
| Cfg.Node.Start_node pdesc ->
let pname = Cfg.Procdesc.get_proc_name pdesc in
| Cfg.Node.Start_node pname ->
let name = Procname.to_string pname in
let name_id = Procname.to_filename pname in
let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in
@ -480,8 +479,7 @@ end = struct
[(Io_infer.Xml.tag_kind,"condition");
(Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in
trace := mk_trace_elem level curr_loc descr node_tags :: !trace
| Cfg.Node.Exit_node pdesc ->
let pname = Cfg.Procdesc.get_proc_name pdesc in
| Cfg.Node.Exit_node pname ->
let descr = "return from a call to " ^ (Procname.to_string pname) in
let name = Procname.to_string pname in
let name_id = Procname.to_filename pname in
@ -708,4 +706,3 @@ end = struct
IList.fold_left (fun ps (p, pa) -> add_renamed_prop p pa ps) empty pl
end
(* =============== END of the PathSet module ===============*)

3
infer/src/backend/printer.ml
Unescape View File

@ -539,8 +539,7 @@ let write_html_file linereader filename procs =
IList.iter
(fun n ->
match Cfg.Node.get_kind n with
| Cfg.Node.Start_node proc_desc ->
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
| Cfg.Node.Start_node proc_name ->
let num_specs = IList.length (Specs.get_specs proc_name) in
let label =
(Escape.escape_xml (Procname.to_string proc_name)) ^

4
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -422,9 +422,9 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst
if defined then
(if !Config.arc_mode then
Cfg.Procdesc.set_flag procdesc Mleak_buckets.objc_arc_flag "true";
let start_kind = Cfg.Node.Start_node procdesc in
let start_kind = Cfg.Node.Start_node proc_name in
let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in
let exit_kind = Cfg.Node.Exit_node procdesc in
let exit_kind = Cfg.Node.Exit_node proc_name in
let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in
Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node) in

7
infer/src/harness/inhabit.ml
Unescape View File

@ -237,9 +237,10 @@ let add_harness_to_cg harness_name harness_node cg =
let setup_harness_cfg harness_name env cg cfg =
(* each procedure has different scope: start names from id 0 *)
Ident.NameGenerator.reset ();
let procname = Procname.Java harness_name in
let procdesc =
let proc_attributes =
{ (ProcAttributes.default (Procname.Java harness_name) Config.Java) with
{ (ProcAttributes.default procname Config.Java) with
ProcAttributes.is_defined = true;
loc = env.pc;
} in
@ -251,8 +252,8 @@ let setup_harness_cfg harness_name env cg cfg =
Cfg.Node.create cfg env.pc nodekind instrs procdesc in
let (start_node, exit_node) =
let create_node kind = Cfg.Node.create cfg env.pc kind [] procdesc in
let start_kind = Cfg.Node.Start_node procdesc in
let exit_kind = Cfg.Node.Exit_node procdesc in
let start_kind = Cfg.Node.Start_node procname in
let exit_kind = Cfg.Node.Exit_node procname in
(create_node start_kind, create_node exit_kind) in
Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node;

8
infer/src/java/jTrans.ml
Unescape View File

@ -269,9 +269,9 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
ret_type = JTransType.return_type program tenv ms;
} in
Cfg.Procdesc.create cfg proc_attributes in
let start_kind = Cfg.Node.Start_node procdesc in
let start_kind = Cfg.Node.Start_node proc_name in
let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in
let exit_kind = (Cfg.Node.Exit_node procdesc) in
let exit_kind = (Cfg.Node.Exit_node proc_name) in
let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in
Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node];
Cfg.Procdesc.set_start_node procdesc start_node;
@ -321,9 +321,9 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
ret_type = JTransType.return_type program tenv ms;
} in
Cfg.Procdesc.create cfg proc_attributes in
let start_kind = Cfg.Node.Start_node procdesc in
let start_kind = Cfg.Node.Start_node proc_name in
let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in
let exit_kind = (Cfg.Node.Exit_node procdesc) in
let exit_kind = (Cfg.Node.Exit_node proc_name) in
let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in
let exn_kind = Cfg.Node.exn_sink_kind in
let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc in

5
infer/src/unit/analyzerTester.ml
Unescape View File

@ -171,6 +171,7 @@ module Make
let cfg = Cfg.Node.create_cfg () in
let pdesc =
Cfg.Procdesc.create cfg (ProcAttributes.default test_pname !Config.curr_language) in
let pname = Cfg.Procdesc.get_proc_name pdesc in
let create_node kind cmds =
Cfg.Node.create cfg dummy_loc kind cmds pdesc in
@ -234,12 +235,12 @@ module Make
(fun acc instr -> structured_instr_to_node acc exn_handlers instr)
(last_node, assert_map)
instrs in
let start_node = create_node (Cfg.Node.Start_node pdesc) [] in
let start_node = create_node (Cfg.Node.Start_node pname) [] in
Cfg.Procdesc.set_start_node pdesc start_node;
let no_exn_handlers = [] in
let last_node, assert_map =
structured_instrs_to_node start_node M.empty no_exn_handlers program in
let exit_node = create_node (Cfg.Node.Exit_node pdesc) [] in
let exit_node = create_node (Cfg.Node.Exit_node pname) [] in
set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers;
Cfg.Procdesc.set_exit_node pdesc exit_node;
pdesc, assert_map

Write Preview
Loading…
Cancel
Save