From e933ee958a2e8a24407413353ee7aa2d17b71a31 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 3 Nov 2016 02:18:57 -0700 Subject: [PATCH] [IR] Rearrange the cfg module to make nodes, procd descs, and cfgs independent types. Reviewed By: jberdine Differential Revision: D4118243 fbshipit-source-id: 73c910c --- infer/src/IR/Cfg.re | 971 ++++++++++++++---------------- infer/src/IR/Cfg.rei | 310 +++++----- infer/src/backend/exe_env.ml | 2 +- infer/src/backend/interproc.ml | 12 +- infer/src/backend/paths.ml | 14 +- infer/src/backend/paths.mli | 8 +- infer/src/backend/printer.ml | 4 +- infer/src/backend/printer.mli | 4 +- infer/src/backend/state.ml | 2 +- infer/src/backend/state.mli | 2 +- infer/src/clang/cFrontend.ml | 2 +- infer/src/clang/cFrontend_decl.ml | 11 +- infer/src/clang/cMethod_trans.ml | 14 +- infer/src/clang/cTrans.ml | 40 +- infer/src/clang/cTrans_utils.ml | 14 +- infer/src/harness/inhabit.ml | 22 +- infer/src/java/jFrontend.ml | 13 +- infer/src/java/jTrans.ml | 50 +- infer/src/java/jTransExn.ml | 8 +- infer/src/unit/analyzerTester.ml | 8 +- infer/src/unit/procCfgTests.ml | 12 +- 21 files changed, 746 insertions(+), 777 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 16e203941..80ca1a4c0 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -16,7 +16,6 @@ let module L = Logging; let module F = Format; -/* ============== START of ADT node and proc_desc ============== */ /* =============== START of module Node =============== */ let module Node = { type id = int; @@ -31,165 +30,53 @@ let module Node = { /** a node */ type t = { /** unique id of the node */ - nd_id: id, + id: id, /** distance to the exit node */ - mutable nd_dist_exit: option int, + mutable dist_exit: option int, /** exception nodes in the cfg */ - mutable nd_exn: list t, + mutable exn: list t, /** instructions for symbolic execution */ - mutable nd_instrs: list Sil.instr, + mutable instrs: list Sil.instr, /** kind of node */ - nd_kind: nodekind, + kind: nodekind, /** location in the source code */ - nd_loc: Location.t, + loc: Location.t, /** predecessor nodes in the cfg */ - mutable nd_preds: list t, + mutable preds: list t, /** name of the procedure the node belongs to */ - nd_pname: option Procname.t, + pname: option Procname.t, /** successor nodes in the cfg */ - mutable nd_succs: list t - }; - - /** procedure description */ - type proc_desc = { - pd_attributes: ProcAttributes.t, /** attributes of the procedure */ - pd_id: int, /** unique proc_desc identifier */ - mutable pd_nodes: list t, /** list of nodes of this procedure */ - mutable pd_nodes_num: int, /** number of nodes */ - mutable pd_start_node: t, /** start node of this procedure */ - mutable pd_exit_node: t /** exit node of ths procedure */ + mutable succs: list t }; let exn_handler_kind = Stmt_node "exception handler"; let exn_sink_kind = Stmt_node "exceptions sink"; let throw_kind = Stmt_node "throw"; - - /** data type for the control flow graph */ - type cfg = {name_pdesc_tbl: Procname.Hash.t proc_desc /** Map proc name to procdesc */}; - - /** create a new empty cfg */ - let create_cfg () => {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 => { - let pdescs_eq pd1 pd2 => { - /* map of exp names in pd1 -> exp names in pd2 */ - let exp_map = ref Exp.Map.empty; - /* map of node id's in pd1 -> node id's in pd2 */ - let id_map = ref IntMap.empty; - /* formals are the same if their types are the same */ - let formals_eq formals1 formals2 => - IList.equal (fun (_, typ1) (_, typ2) => Typ.compare typ1 typ2) formals1 formals2; - let nodes_eq n1s n2s => { - /* nodes are the same if they have the same id, instructions, and succs/preds up to renaming - with [exp_map] and [id_map] */ - let node_eq n1 n2 => { - let id_compare n1 n2 => { - let (id1, id2) = (n1.nd_id, n2.nd_id); - try { - let id1_mapping = IntMap.find id1 !id_map; - Pervasives.compare id1_mapping id2 - } { - | Not_found => - /* assume id's are equal and enforce by adding to [id_map] */ - id_map := IntMap.add id1 id2 !id_map; - 0 - } - }; - let instrs_eq instrs1 instrs2 => - IList.equal - ( - fun i1 i2 => { - let (n, exp_map') = Sil.instr_compare_structural i1 i2 !exp_map; - exp_map := exp_map'; - n - } - ) - instrs1 - instrs2; - id_compare n1 n2 == 0 && - IList.equal id_compare n1.nd_succs n2.nd_succs && - IList.equal id_compare n1.nd_preds n2.nd_preds && instrs_eq n1.nd_instrs n2.nd_instrs - }; - try (IList.for_all2 node_eq n1s n2s) { - | Invalid_argument _ => false - } - }; - let att1 = pd1.pd_attributes - and att2 = pd2.pd_attributes; - att1.ProcAttributes.is_defined == att2.ProcAttributes.is_defined && - Typ.equal att1.ProcAttributes.ret_type att2.ProcAttributes.ret_type && - formals_eq att1.ProcAttributes.formals att2.ProcAttributes.formals && - nodes_eq pd1.pd_nodes pd2.pd_nodes - }; - let old_procs = cfg_old.name_pdesc_tbl; - let new_procs = cfg_new.name_pdesc_tbl; - let mark_pdesc_if_unchanged pname new_pdesc => - try { - let old_pdesc = Procname.Hash.find old_procs pname; - let changed = - /* in continue_capture mode keep the old changed bit */ - Config.continue_capture && old_pdesc.pd_attributes.ProcAttributes.changed || - not (pdescs_eq old_pdesc new_pdesc); - new_pdesc.pd_attributes.changed = changed - } { - | Not_found => () - }; - Procname.Hash.iter mark_pdesc_if_unchanged new_procs - }; - let pdesc_tbl_add cfg proc_name proc_desc => - Procname.Hash.add cfg.name_pdesc_tbl proc_name proc_desc; - let pdesc_tbl_remove cfg proc_name => Procname.Hash.remove cfg.name_pdesc_tbl proc_name; - let pdesc_tbl_find cfg proc_name => Procname.Hash.find cfg.name_pdesc_tbl proc_name; - let iter_proc_desc cfg f => Procname.Hash.iter f cfg.name_pdesc_tbl; let dummy () => { - nd_id: 0, - nd_dist_exit: None, - nd_instrs: [], - nd_kind: Skip_node "dummy", - nd_loc: Location.dummy, - nd_pname: None, - nd_succs: [], - nd_preds: [], - nd_exn: [] - }; - let compare node1 node2 => int_compare node1.nd_id node2.nd_id; - let hash node => Hashtbl.hash node.nd_id; + id: 0, + dist_exit: None, + instrs: [], + kind: Skip_node "dummy", + loc: Location.dummy, + pname: None, + succs: [], + preds: [], + exn: [] + }; + let compare node1 node2 => int_compare node1.id node2.id; + let hash node => Hashtbl.hash node.id; let equal node1 node2 => compare node1 node2 == 0; - /** Create a new cfg node */ - let create loc kind instrs pdesc => { - pdesc.pd_nodes_num = pdesc.pd_nodes_num + 1; - let node_id = pdesc.pd_nodes_num; - let node = { - nd_id: node_id, - nd_dist_exit: None, - nd_instrs: instrs, - nd_kind: kind, - nd_loc: loc, - nd_preds: [], - nd_pname: Some pdesc.pd_attributes.proc_name, - nd_succs: [], - nd_exn: [] - }; - pdesc.pd_nodes = [node, ...pdesc.pd_nodes]; - node - }; - /** Get the unique id of the node */ - let get_id node => node.nd_id; + let get_id node => node.id; /** compare node ids */ let id_compare = int_compare; - let get_succs node => node.nd_succs; + let get_succs node => node.succs; type node = t; let module NodeSet = Set.Make { type t = node; let compare = compare; }; - let module NodeMap = Map.Make { - type t = node; - let compare = compare; - }; let module IdMap = Map.Make { type t = id; let compare = id_compare; @@ -203,12 +90,12 @@ let module Node = { NodeSet.singleton n } else { NodeSet.union - acc (slice_nodes (IList.filter (fun s => not (NodeSet.mem s !visited)) n.nd_succs)) + acc (slice_nodes (IList.filter (fun s => not (NodeSet.mem s !visited)) n.succs)) } }; IList.fold_left do_node NodeSet.empty nodes }; - NodeSet.elements (slice_nodes node.nd_succs) + NodeSet.elements (slice_nodes node.succs) }; let get_sliced_preds node f => { let visited = ref NodeSet.empty; @@ -219,46 +106,26 @@ let module Node = { NodeSet.singleton n } else { NodeSet.union - acc (slice_nodes (IList.filter (fun s => not (NodeSet.mem s !visited)) n.nd_preds)) + acc (slice_nodes (IList.filter (fun s => not (NodeSet.mem s !visited)) n.preds)) } }; IList.fold_left do_node NodeSet.empty nodes }; - NodeSet.elements (slice_nodes node.nd_preds) + NodeSet.elements (slice_nodes node.preds) }; - let get_exn node => node.nd_exn; + let get_exn node => node.exn; /** Get the name of the procedure the node belongs to */ let get_proc_name node => - switch node.nd_pname { + switch node.pname { | None => - L.out "node_get_proc_desc: at node %d@\n" node.nd_id; + L.out "get_proc_name: at node %d@\n" node.id; assert false - | Some proc_name => proc_name - }; - - /** Set the successor nodes and exception nodes, and build predecessor links */ - let set_succs_exn_base node succs exn => { - node.nd_succs = succs; - node.nd_exn = exn; - IList.iter (fun n => n.nd_preds = [node, ...n.nd_preds]) succs - }; - - /** Set the successor and exception nodes. - If this is a join node right before the exit node, add an extra node in the middle, - otherwise nullify and abstract instructions cannot be added after a conditional. */ - let set_succs_exn pdesc node succs exn => - switch (node.nd_kind, succs) { - | (Join_node, [{nd_kind: Exit_node _} as exit_node]) => - let kind = Stmt_node "between_join_and_exit"; - let node' = create node.nd_loc kind node.nd_instrs pdesc; - set_succs_exn_base node [node'] exn; - set_succs_exn_base node' [exit_node] exn - | _ => set_succs_exn_base node succs exn + | Some pname => pname }; /** Get the predecessors of the node */ - let get_preds node => node.nd_preds; + let get_preds node => node.preds; /** Generates a list of nodes starting at a given node and recursively adding the results of the generator */ @@ -276,7 +143,7 @@ let module Node = { }; /** Get the node kind */ - let get_kind node => node.nd_kind; + let get_kind node => node.kind; /** Comparison for node kind */ let kind_compare k1 k2 => @@ -311,7 +178,7 @@ let module Node = { }; /** Get the instructions to be executed */ - let get_instrs node => node.nd_instrs; + let get_instrs node => node.instrs; /** Get the list of callee procnames from the node */ let get_callees node => { @@ -328,143 +195,41 @@ let module Node = { }; /** Get the location of the node */ - let get_loc n => n.nd_loc; + let get_loc n => n.loc; /** Get the source location of the last instruction in the node */ let get_last_loc n => switch (IList.rev (get_instrs n)) { | [instr, ..._] => Sil.instr_get_loc instr - | [] => n.nd_loc + | [] => n.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 get_distance_to_exit node => node.nd_dist_exit; + let get_distance_to_exit node => node.dist_exit; /** Append the instructions to the list of instructions to execute */ - let append_instrs node instrs => node.nd_instrs = node.nd_instrs @ instrs; + let append_instrs node instrs => node.instrs = node.instrs @ instrs; /** Add the instructions at the beginning of the list of instructions to execute */ - let prepend_instrs node instrs => node.nd_instrs = instrs @ node.nd_instrs; + let prepend_instrs node instrs => node.instrs = instrs @ node.instrs; /** Replace the instructions to be executed. */ - let replace_instrs node instrs => node.nd_instrs = instrs; - let proc_desc_get_ret_var pdesc => - Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name; + let replace_instrs node instrs => node.instrs = instrs; /** Add declarations for local variables and return variable to the node */ - let add_locals_ret_declaration pdesc node locals => { + let add_locals_ret_declaration node (proc_attributes: ProcAttributes.t) locals => { let loc = get_loc node; - let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name; + let pname = proc_attributes.proc_name; let ret_var = { - let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type; - (proc_desc_get_ret_var pdesc, ret_type) + let ret_type = proc_attributes.ret_type; + (Pvar.get_ret_pvar pname, ret_type) }; - let construct_decl (x, typ) => (Pvar.mk x proc_name, typ); + let construct_decl (x, typ) => (Pvar.mk x pname, typ); let ptl = [ret_var, ...IList.map construct_decl locals]; let instr = Sil.Declare_locals ptl loc; prepend_instrs node [instr] }; - /** Counter for identifiers of procdescs */ - let proc_desc_id_counter = ref 0; - let proc_desc_create cfg proc_attributes => { - incr proc_desc_id_counter; - let pdesc = { - pd_attributes: proc_attributes, - pd_id: !proc_desc_id_counter, - pd_nodes: [], - pd_nodes_num: 0, - pd_start_node: dummy (), - pd_exit_node: dummy () - }; - pdesc_tbl_add cfg proc_attributes.ProcAttributes.proc_name pdesc; - pdesc - }; - let proc_desc_remove cfg name => pdesc_tbl_remove cfg name; - let proc_desc_get_start_node proc_desc => proc_desc.pd_start_node; - let proc_desc_get_err_log proc_desc => proc_desc.pd_attributes.ProcAttributes.err_log; - let proc_desc_get_attributes proc_desc => proc_desc.pd_attributes; - let proc_desc_get_exit_node proc_desc => proc_desc.pd_exit_node; - - /** Compute the distance of each node to the exit node, if not computed already */ - let proc_desc_compute_distance_to_exit_node proc_desc => { - let exit_node = proc_desc.pd_exit_node; - let rec mark_distance dist nodes => { - let next_nodes = ref []; - let do_node node => - switch node.nd_dist_exit { - | Some _ => () - | None => - node.nd_dist_exit = Some dist; - next_nodes := node.nd_preds @ !next_nodes - }; - IList.iter do_node nodes; - if (!next_nodes !== []) { - mark_distance (dist + 1) !next_nodes - } - }; - mark_distance 0 [exit_node] - }; - - /** Set the start node of the proc desc */ - let proc_desc_set_start_node pdesc node => pdesc.pd_start_node = node; - - /** Set the exit node of the proc desc */ - let proc_desc_set_exit_node pdesc node => pdesc.pd_exit_node = node; - - /** Set a flag for the proc desc */ - let proc_desc_set_flag pdesc key value => - proc_flags_add pdesc.pd_attributes.ProcAttributes.proc_flags key value; - - /** Return the return type of the procedure */ - let proc_desc_get_ret_type proc_desc => proc_desc.pd_attributes.ProcAttributes.ret_type; - let proc_desc_get_proc_name proc_desc => proc_desc.pd_attributes.ProcAttributes.proc_name; - - /** Return [true] iff the procedure is defined, and not just declared */ - let proc_desc_is_defined proc_desc => proc_desc.pd_attributes.ProcAttributes.is_defined; - let proc_desc_is_java_synchroinized proc_desc => - proc_desc.pd_attributes.ProcAttributes.is_java_synchronized_method; - let proc_desc_get_loc proc_desc => proc_desc.pd_attributes.ProcAttributes.loc; - - /** Return name and type of formal parameters */ - let proc_desc_get_formals proc_desc => proc_desc.pd_attributes.ProcAttributes.formals; - - /** Return name and type of local variables */ - let proc_desc_get_locals proc_desc => proc_desc.pd_attributes.ProcAttributes.locals; - - /** Return name and type of captured variables */ - let proc_desc_get_captured proc_desc => proc_desc.pd_attributes.ProcAttributes.captured; - - /** Return the visibility attribute */ - let proc_desc_get_access proc_desc => proc_desc.pd_attributes.ProcAttributes.access; - let proc_desc_get_nodes proc_desc => proc_desc.pd_nodes; - - /** List of nodes in the procedure up to the first branching */ - let proc_desc_get_slope proc_desc => - get_generated_slope (proc_desc_get_start_node proc_desc) get_succs; - - /** List of nodes in the procedure sliced by a predicate up to the first branching */ - let proc_desc_get_sliced_slope proc_desc f => - get_generated_slope (proc_desc_get_start_node proc_desc) (fun n => get_sliced_succs n f); - - /** Get flags for the proc desc */ - let proc_desc_get_flags proc_desc => proc_desc.pd_attributes.ProcAttributes.proc_flags; - - /** Append the locals to the list of local variables */ - let proc_desc_append_locals proc_desc new_locals => - proc_desc.pd_attributes.ProcAttributes.locals = - proc_desc.pd_attributes.ProcAttributes.locals @ new_locals; - - /** check or indicate if we have performed preanalysis on the CFG */ - let proc_desc_did_preanalysis proc_desc => - proc_desc.pd_attributes.ProcAttributes.did_preanalysis; - let proc_desc_signal_did_preanalysis proc_desc => - proc_desc.pd_attributes.ProcAttributes.did_preanalysis = true; - /** Print extended instructions for the node, highlighting the given subinstruction if present */ let pp_instrs pe0 sub_instrs::sub_instrs instro fmt node => { @@ -536,24 +301,124 @@ let module Node = { let pp fmt () => F.fprintf fmt "%s\n%a@?" str (pp_instrs pe None sub_instrs::true) node; pp_to_string pp () }; - let proc_desc_iter_nodes f proc_desc => IList.iter f (IList.rev (proc_desc_get_nodes proc_desc)); - let proc_desc_fold_nodes f acc proc_desc => - IList.fold_left f acc (IList.rev (proc_desc_get_nodes proc_desc)); - let proc_desc_fold_calls f acc pdesc => { +}; + +/* =============== END of module Node =============== */ + +/** Map over nodes */ +let module NodeMap = Map.Make Node; + + +/** Hash table with nodes as keys. */ +let module NodeHash = Hashtbl.Make Node; + + +/** Set of nodes. */ +let module NodeSet = Node.NodeSet; + + +/** Map with node id keys. */ +let module IdMap = Node.IdMap; + +/* =============== START of module Procdesc =============== */ +let module Procdesc = { + + /** procedure description */ + type t = { + attributes: ProcAttributes.t, /** attributes of the procedure */ + id: int, /** unique proc_desc identifier */ + mutable nodes: list Node.t, /** list of nodes of this procedure */ + mutable nodes_num: int, /** number of nodes */ + mutable start_node: Node.t, /** start node of this procedure */ + mutable exit_node: Node.t /** exit node of ths procedure */ + }; + + /** Compute the distance of each node to the exit node, if not computed already */ + let compute_distance_to_exit_node pdesc => { + let exit_node = pdesc.exit_node; + let rec mark_distance dist nodes => { + let next_nodes = ref []; + let do_node (node: Node.t) => + switch node.dist_exit { + | Some _ => () + | None => + node.dist_exit = Some dist; + next_nodes := node.preds @ !next_nodes + }; + IList.iter do_node nodes; + if (!next_nodes !== []) { + mark_distance (dist + 1) !next_nodes + } + }; + mark_distance 0 [exit_node] + }; + + /** check or indicate if we have performed preanalysis on the CFG */ + let did_preanalysis pdesc => pdesc.attributes.did_preanalysis; + let signal_did_preanalysis pdesc => pdesc.attributes.did_preanalysis = true; + let get_attributes pdesc => pdesc.attributes; + let get_err_log pdesc => pdesc.attributes.err_log; + let get_exit_node pdesc => pdesc.exit_node; + + /** Get flags for the proc desc */ + let get_flags pdesc => pdesc.attributes.proc_flags; + + /** Return name and type of formal parameters */ + let get_formals pdesc => pdesc.attributes.formals; + let get_loc pdesc => pdesc.attributes.loc; + + /** Return name and type of local variables */ + let get_locals pdesc => pdesc.attributes.locals; + + /** Return name and type of captured variables */ + let get_captured pdesc => pdesc.attributes.captured; + + /** Return the visibility attribute */ + let get_access pdesc => pdesc.attributes.access; + let get_nodes pdesc => pdesc.nodes; + let get_proc_name pdesc => pdesc.attributes.proc_name; + + /** Return the return type of the procedure */ + let get_ret_type pdesc => pdesc.attributes.ret_type; + let get_ret_var pdesc => Pvar.mk Ident.name_return (get_proc_name pdesc); + let get_start_node pdesc => pdesc.start_node; + + /** List of nodes in the procedure sliced by a predicate up to the first branching */ + let get_sliced_slope pdesc f => + Node.get_generated_slope (get_start_node pdesc) (fun n => Node.get_sliced_succs n f); + + /** List of nodes in the procedure up to the first branching */ + let get_slope pdesc => Node.get_generated_slope (get_start_node pdesc) Node.get_succs; + + /** Return [true] iff the procedure is defined, and not just declared */ + let is_defined pdesc => pdesc.attributes.is_defined; + let is_java_synchronized pdesc => pdesc.attributes.is_java_synchronized_method; + let iter_nodes f pdesc => IList.iter f (IList.rev (get_nodes pdesc)); + let fold_calls f acc pdesc => { let do_node a node => IList.fold_left - (fun b callee_pname => f b (callee_pname, get_loc node)) a (get_callees node); - IList.fold_left do_node acc (proc_desc_get_nodes pdesc) + (fun b callee_pname => f b (callee_pname, Node.get_loc node)) a (Node.get_callees node); + IList.fold_left do_node acc (get_nodes pdesc) }; /** iterate over the calls from the procedure: (callee,location) pairs */ - let proc_desc_iter_calls f pdesc => proc_desc_fold_calls (fun _ call => f call) () pdesc; - let proc_desc_iter_slope f proc_desc => { + let iter_calls f pdesc => fold_calls (fun _ call => f call) () pdesc; + let iter_instrs f pdesc => { + let do_node node => IList.iter (fun i => f node i) (Node.get_instrs node); + iter_nodes do_node pdesc + }; + let fold_nodes f acc pdesc => IList.fold_left f acc (IList.rev (get_nodes pdesc)); + let fold_instrs f acc pdesc => { + let fold_node acc node => + IList.fold_left (fun acc instr => f acc node instr) acc (Node.get_instrs node); + fold_nodes fold_node acc pdesc + }; + let iter_slope f pdesc => { let visited = ref NodeSet.empty; let rec do_node node => { visited := NodeSet.add node !visited; f node; - switch (get_succs node) { + switch (Node.get_succs node) { | [n] => if (not (NodeSet.mem n !visited)) { do_node n @@ -561,18 +426,22 @@ let module Node = { | _ => () } }; - do_node (proc_desc_get_start_node proc_desc) + do_node (get_start_node pdesc) + }; + let iter_slope_calls f pdesc => { + let do_node node => IList.iter (fun callee_pname => f callee_pname) (Node.get_callees node); + iter_slope do_node pdesc }; /** iterate between two nodes or until we reach a branching structure */ - let proc_desc_iter_slope_range f src_node dst_node => { + let iter_slope_range f src_node dst_node => { let visited = ref NodeSet.empty; let rec do_node node => { visited := NodeSet.add node !visited; f node; - switch (get_succs node) { + switch (Node.get_succs node) { | [n] => - if (not (NodeSet.mem n !visited) && not (equal node dst_node)) { + if (not (NodeSet.mem n !visited) && not (Node.equal node dst_node)) { do_node n } | _ => () @@ -580,214 +449,103 @@ let module Node = { }; do_node src_node }; - let proc_desc_iter_slope_calls f proc_desc => { - let do_node node => IList.iter (fun callee_pname => f callee_pname) (get_callees node); - proc_desc_iter_slope do_node proc_desc - }; - let proc_desc_iter_instrs f proc_desc => { - let do_node node => IList.iter (fun i => f node i) (get_instrs node); - proc_desc_iter_nodes do_node proc_desc - }; - let proc_desc_fold_instrs f acc proc_desc => { - let fold_node acc node => - IList.fold_left (fun acc instr => f acc node instr) acc (get_instrs node); - proc_desc_fold_nodes fold_node acc proc_desc + + /** Set the exit node of the proc desc */ + let set_exit_node pdesc node => pdesc.exit_node = node; + + /** Set a flag for the proc desc */ + let set_flag pdesc key value => proc_flags_add pdesc.attributes.proc_flags key value; + + /** Set the start node of the proc desc */ + let set_start_node pdesc node => pdesc.start_node = node; + + /** Append the locals to the list of local variables */ + let append_locals pdesc new_locals => + pdesc.attributes.locals = pdesc.attributes.locals @ new_locals; + + /** Set the successor nodes and exception nodes, and build predecessor links */ + let set_succs_exn_base (node: Node.t) succs exn => { + node.succs = succs; + node.exn = exn; + IList.iter (fun (n: Node.t) => n.preds = [node, ...n.preds]) succs }; - /* clone a procedure description and apply the type substitutions where - the parameters are used */ - let proc_desc_specialize_types callee_proc_desc resolved_attributes substitutions => { - let cfg = create_cfg (); - let resolved_proc_desc = proc_desc_create cfg resolved_attributes; - let resolved_proc_name = proc_desc_get_proc_name resolved_proc_desc - and callee_start_node = proc_desc_get_start_node callee_proc_desc - and callee_exit_node = proc_desc_get_exit_node callee_proc_desc; - let convert_pvar pvar => Pvar.mk (Pvar.get_name pvar) resolved_proc_name; - let convert_exp = - fun - | Exp.Lvar origin_pvar => Exp.Lvar (convert_pvar origin_pvar) - | exp => exp; - let extract_class_name = - fun - | Typ.Tptr (Tstruct name) _ => Typename.name name - | _ => failwith "Expecting classname for Java types"; - let subst_map = ref Ident.IdentMap.empty; - let redirected_class_name origin_id => - try (Some (Ident.IdentMap.find origin_id !subst_map)) { - | Not_found => None - }; - let convert_instr instrs => - fun - | Sil.Load id (Exp.Lvar origin_pvar as origin_exp) origin_typ loc => { - let (_, specialized_typ) = { - let pvar_name = Pvar.get_name origin_pvar; - try (IList.find (fun (n, _) => Mangled.equal n pvar_name) substitutions) { - | Not_found => (pvar_name, origin_typ) - } - }; - subst_map := Ident.IdentMap.add id specialized_typ !subst_map; - [Sil.Load id (convert_exp origin_exp) specialized_typ loc, ...instrs] - } - | Sil.Load id (Exp.Var origin_id as origin_exp) origin_typ loc => { - let updated_typ = - switch (Ident.IdentMap.find origin_id !subst_map) { - | Typ.Tptr typ _ => typ - | _ => failwith "Expecting a pointer type" - | exception Not_found => origin_typ - }; - [Sil.Load id (convert_exp origin_exp) updated_typ loc, ...instrs] - } - | Sil.Load id origin_exp origin_typ loc => [ - Sil.Load id (convert_exp origin_exp) origin_typ loc, - ...instrs - ] - | Sil.Store assignee_exp origin_typ origin_exp loc => { - let set_instr = - Sil.Store (convert_exp assignee_exp) origin_typ (convert_exp origin_exp) loc; - [set_instr, ...instrs] - } - | Sil.Call - return_ids - (Exp.Const (Const.Cfun (Procname.Java callee_pname_java))) - [(Exp.Var id, _), ...origin_args] - loc - call_flags - when call_flags.CallFlags.cf_virtual && redirected_class_name id != None => { - let redirected_typ = Option.get (redirected_class_name id); - let redirected_pname = - Procname.replace_class - (Procname.Java callee_pname_java) (extract_class_name redirected_typ) - and args = { - let other_args = IList.map (fun (exp, typ) => (convert_exp exp, typ)) origin_args; - [(Exp.Var id, redirected_typ), ...other_args] - }; - let call_instr = - Sil.Call return_ids (Exp.Const (Const.Cfun redirected_pname)) args loc call_flags; - [call_instr, ...instrs] - } - | Sil.Call return_ids origin_call_exp origin_args loc call_flags => { - let converted_args = IList.map (fun (exp, typ) => (convert_exp exp, typ)) origin_args; - let call_instr = - Sil.Call return_ids (convert_exp origin_call_exp) converted_args loc call_flags; - [call_instr, ...instrs] - } - | Sil.Prune origin_exp loc is_true_branch if_kind => [ - Sil.Prune (convert_exp origin_exp) loc is_true_branch if_kind, - ...instrs - ] - | Sil.Declare_locals typed_vars loc => { - let new_typed_vars = IList.map (fun (pvar, typ) => (convert_pvar pvar, typ)) typed_vars; - [Sil.Declare_locals new_typed_vars loc, ...instrs] - } - | Sil.Nullify _ - | Abstract _ - | Sil.Remove_temps _ => - /* these are generated instructions that will be replaced by the preanalysis */ - instrs; - let convert_node_kind = - fun - | 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 => { - let loc = get_loc node - and kind = convert_node_kind (get_kind node) - and instrs = IList.fold_left convert_instr [] (get_instrs node) |> IList.rev; - create loc kind instrs resolved_proc_desc - } - and loop callee_nodes => - switch callee_nodes { - | [] => [] - | [node, ...other_node] => - let converted_node = - try (NodeMap.find node !node_map) { - | Not_found => - let new_node = convert_node node - and successors = get_succs node - and exn_nodes = get_exn node; - node_map := NodeMap.add node new_node !node_map; - if (equal node callee_start_node) { - proc_desc_set_start_node resolved_proc_desc new_node - }; - if (equal node callee_exit_node) { - proc_desc_set_exit_node resolved_proc_desc new_node - }; - set_succs_exn callee_proc_desc new_node (loop successors) (loop exn_nodes); - new_node - }; - [converted_node, ...loop other_node] - }; - ignore (loop [callee_start_node]); - resolved_proc_desc + + /** Create a new cfg node */ + let create_node pdesc loc kind instrs => { + pdesc.nodes_num = pdesc.nodes_num + 1; + let node_id = pdesc.nodes_num; + let node = { + Node.id: node_id, + dist_exit: None, + instrs, + kind, + loc, + preds: [], + pname: Some pdesc.attributes.proc_name, + succs: [], + exn: [] + }; + pdesc.nodes = [node, ...pdesc.nodes]; + node }; -}; -/* =============== END of module Node =============== */ -type node = Node.t; + /** Set the successor and exception nodes. + If this is a join node right before the exit node, add an extra node in the middle, + otherwise nullify and abstract instructions cannot be added after a conditional. */ + let node_set_succs_exn pdesc (node: Node.t) succs exn => + switch (node.kind, succs) { + | (Join_node, [{Node.kind: Exit_node _} as exit_node]) => + let kind = Node.Stmt_node "between_join_and_exit"; + let node' = create_node pdesc node.loc kind node.instrs; + set_succs_exn_base node [node'] exn; + set_succs_exn_base node' [exit_node] exn + | _ => set_succs_exn_base node succs exn + }; +}; -type cfg = Node.cfg; +/* =============== END of module Procdesc =============== */ -/* =============== START of module Procdesc =============== */ -let module Procdesc = { - type t = Node.proc_desc; - let compute_distance_to_exit_node = Node.proc_desc_compute_distance_to_exit_node; - let create = Node.proc_desc_create; - let remove = Node.proc_desc_remove; - let did_preanalysis = Node.proc_desc_did_preanalysis; - let signal_did_preanalysis = Node.proc_desc_signal_did_preanalysis; - let find_from_name = Node.proc_desc_from_name; - let get_attributes = Node.proc_desc_get_attributes; - let get_err_log = Node.proc_desc_get_err_log; - let get_exit_node = Node.proc_desc_get_exit_node; - let get_flags = Node.proc_desc_get_flags; - let get_formals = Node.proc_desc_get_formals; - let get_loc = Node.proc_desc_get_loc; - let get_locals = Node.proc_desc_get_locals; - let get_captured = Node.proc_desc_get_captured; - let get_access = Node.proc_desc_get_access; - let get_nodes = Node.proc_desc_get_nodes; - let get_slope = Node.proc_desc_get_slope; - let get_sliced_slope = Node.proc_desc_get_sliced_slope; - let get_proc_name = Node.proc_desc_get_proc_name; - let get_ret_type = Node.proc_desc_get_ret_type; - let get_ret_var pdesc => Pvar.mk Ident.name_return (get_proc_name pdesc); - let get_start_node = Node.proc_desc_get_start_node; - let is_defined = Node.proc_desc_is_defined; - let is_java_synchronized = Node.proc_desc_is_java_synchroinized; - let iter_nodes = Node.proc_desc_iter_nodes; - let fold_calls = Node.proc_desc_fold_calls; - let iter_calls = Node.proc_desc_iter_calls; - let iter_instrs = Node.proc_desc_iter_instrs; - let fold_instrs = Node.proc_desc_fold_instrs; - let iter_slope = Node.proc_desc_iter_slope; - let iter_slope_calls = Node.proc_desc_iter_slope_calls; - let iter_slope_range = Node.proc_desc_iter_slope_range; - let set_exit_node = Node.proc_desc_set_exit_node; - let set_flag = Node.proc_desc_set_flag; - let set_start_node = Node.proc_desc_set_start_node; - let append_locals = Node.proc_desc_append_locals; - let specialize_types = Node.proc_desc_specialize_types; +/** data type for the control flow graph */ +type cfg = { + mutable proc_desc_id_counter: int /** Counter for identifiers of procdescs */, + proc_desc_table: Procname.Hash.t Procdesc.t /** Map proc name to procdesc */ }; -/* =============== END of module Procdesc =============== */ -/** Hash table with nodes as keys. */ -let module NodeHash = Hashtbl.Make Node; +/** create a new empty cfg */ +let create_cfg () => {proc_desc_id_counter: 0, proc_desc_table: Procname.Hash.create 16}; +let add_proc_desc cfg pname pdesc => Procname.Hash.add cfg.proc_desc_table pname pdesc; -/** Set of nodes. */ -let module NodeSet = Node.NodeSet; +let remove_proc_desc cfg pname => Procname.Hash.remove cfg.proc_desc_table pname; +let iter_proc_desc cfg f => Procname.Hash.iter f cfg.proc_desc_table; -/** Map with node id keys. */ -let module IdMap = Node.IdMap; +let find_proc_desc_from_name cfg pname => + try (Some (Procname.Hash.find cfg.proc_desc_table pname)) { + | Not_found => None + }; -let iter_proc_desc = Node.iter_proc_desc; + +/** Create a new procdesc */ +let create_proc_desc cfg (proc_attributes: ProcAttributes.t) => { + cfg.proc_desc_id_counter = cfg.proc_desc_id_counter + 1; + let pdesc = { + Procdesc.attributes: proc_attributes, + id: cfg.proc_desc_id_counter, + nodes: [], + nodes_num: 0, + start_node: Node.dummy (), + exit_node: Node.dummy () + }; + add_proc_desc cfg proc_attributes.proc_name pdesc; + pdesc +}; /** Iterate over all the nodes in the cfg */ -let iter_all_nodes f (cfg: cfg) => { - let do_proc_desc _ (pdesc: Procdesc.t) => IList.iter (fun node => f pdesc node) pdesc.pd_nodes; +let iter_all_nodes f cfg => { + let do_proc_desc _ (pdesc: Procdesc.t) => IList.iter (fun node => f pdesc node) pdesc.nodes; iter_proc_desc cfg do_proc_desc }; @@ -859,13 +617,13 @@ let load_cfg_from_file (filename: DB.filename) :option cfg => unless an updated copy already exists */ let save_source_files cfg => { let process_proc _ pdesc => { - let loc = Node.proc_desc_get_loc pdesc; + let loc = Procdesc.get_loc pdesc; let source_file = loc.Location.file; let source_file_str = DB.source_file_to_abs_path source_file; let dest_file = DB.source_file_in_resdir source_file; let dest_file_str = DB.filename_to_string dest_file; let needs_copy = - Node.proc_desc_is_defined pdesc && + Procdesc.is_defined pdesc && Sys.file_exists source_file_str && ( not (Sys.file_exists dest_file_str) || DB.file_modified_time (DB.filename_from_string source_file_str) > @@ -878,14 +636,14 @@ let save_source_files cfg => { } } }; - Node.iter_proc_desc cfg process_proc + iter_proc_desc cfg process_proc }; /** Save the .attr files for the procedures in the cfg. */ let save_attributes source_file cfg => { - let save_proc proc_desc => { - let attributes = Procdesc.get_attributes proc_desc; + let save_proc pdesc => { + let attributes = Procdesc.get_attributes pdesc; let loc = attributes.loc; let attributes' = { let loc' = @@ -903,7 +661,7 @@ let save_attributes source_file cfg => { /** Inline a synthetic (access or bridge) method. */ -let inline_synthetic_method ret_id etl proc_desc loc_call :option Sil.instr => { +let inline_synthetic_method ret_id etl pdesc loc_call :option Sil.instr => { let modified = ref None; let debug = false; let found instr instr' => { @@ -950,22 +708,22 @@ let inline_synthetic_method ret_id etl proc_desc loc_call :option Sil.instr => { found instr instr' | _ => () }; - Procdesc.iter_instrs do_instr proc_desc; + Procdesc.iter_instrs do_instr pdesc; !modified }; /** Find synthetic (access or bridge) Java methods in the procedure and inline them in the cfg. */ -let proc_inline_synthetic_methods cfg proc_desc :unit => { +let proc_inline_synthetic_methods cfg pdesc :unit => { let instr_inline_synthetic_method = fun | Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl loc _ => - switch (Procdesc.find_from_name cfg pn) { + switch (find_proc_desc_from_name cfg pn) { | Some pd => let is_access = Procname.java_is_access_method pn; let attributes = Procdesc.get_attributes pd; - let is_synthetic = attributes.ProcAttributes.is_synthetic_method; - let is_bridge = attributes.ProcAttributes.is_bridge_method; + let is_synthetic = attributes.is_synthetic_method; + let is_bridge = attributes.is_bridge_method; if (is_access || is_bridge || is_synthetic) { inline_synthetic_method ret_id etl pd loc } else { @@ -989,20 +747,88 @@ let proc_inline_synthetic_methods cfg proc_desc :unit => { Node.replace_instrs node instrs' } }; - Procdesc.iter_nodes node_inline_synthetic_methods proc_desc + Procdesc.iter_nodes node_inline_synthetic_methods pdesc }; /** Inline the java synthetic methods in the cfg */ let inline_java_synthetic_methods cfg => { - let f proc_name proc_desc => - if (Procname.is_java proc_name) { - proc_inline_synthetic_methods cfg proc_desc + let f pname pdesc => + if (Procname.is_java pname) { + proc_inline_synthetic_methods cfg pdesc }; iter_proc_desc cfg f }; +/** compute the list of procedures added or changed in [cfg_new] over [cfg_old] */ +let mark_unchanged_pdescs cfg_new cfg_old => { + let pdescs_eq (pd1: Procdesc.t) (pd2: Procdesc.t) => { + /* map of exp names in pd1 -> exp names in pd2 */ + let exp_map = ref Exp.Map.empty; + /* map of node id's in pd1 -> node id's in pd2 */ + let id_map = ref IntMap.empty; + /* formals are the same if their types are the same */ + let formals_eq formals1 formals2 => + IList.equal (fun (_, typ1) (_, typ2) => Typ.compare typ1 typ2) formals1 formals2; + let nodes_eq n1s n2s => { + /* nodes are the same if they have the same id, instructions, and succs/preds up to renaming + with [exp_map] and [id_map] */ + let node_eq (n1: Node.t) (n2: Node.t) => { + let id_compare (n1: Node.t) (n2: Node.t) => { + let (id1, id2) = (n1.id, n2.id); + try { + let id1_mapping = IntMap.find id1 !id_map; + Pervasives.compare id1_mapping id2 + } { + | Not_found => + /* assume id's are equal and enforce by adding to [id_map] */ + id_map := IntMap.add id1 id2 !id_map; + 0 + } + }; + let instrs_eq instrs1 instrs2 => + IList.equal + ( + fun i1 i2 => { + let (n, exp_map') = Sil.instr_compare_structural i1 i2 !exp_map; + exp_map := exp_map'; + n + } + ) + instrs1 + instrs2; + id_compare n1 n2 == 0 && + IList.equal id_compare n1.succs n2.succs && + IList.equal id_compare n1.preds n2.preds && instrs_eq n1.instrs n2.instrs + }; + try (IList.for_all2 node_eq n1s n2s) { + | Invalid_argument _ => false + } + }; + let att1 = pd1.attributes + and att2 = pd2.attributes; + att1.is_defined == att2.is_defined && + Typ.equal att1.ret_type att2.ret_type && + formals_eq att1.formals att2.formals && nodes_eq pd1.nodes pd2.nodes + }; + let old_procs = cfg_old.proc_desc_table; + let new_procs = cfg_new.proc_desc_table; + let mark_pdesc_if_unchanged pname (new_pdesc: Procdesc.t) => + try { + let old_pdesc = Procname.Hash.find old_procs pname; + let changed = + /* in continue_capture mode keep the old changed bit */ + Config.continue_capture && old_pdesc.attributes.changed || + not (pdescs_eq old_pdesc new_pdesc); + new_pdesc.attributes.changed = changed + } { + | Not_found => () + }; + Procname.Hash.iter mark_pdesc_if_unchanged new_procs +}; + + /** Save a cfg into a file */ let store_cfg_to_file save_sources::save_sources=true @@ -1015,7 +841,7 @@ let store_cfg_to_file }; if Config.incremental_procs { switch (load_cfg_from_file filename) { - | Some old_cfg => Node.mark_unchanged_pdescs cfg old_cfg + | Some old_cfg => mark_unchanged_pdescs cfg old_cfg | None => () } }; @@ -1024,25 +850,156 @@ let store_cfg_to_file }; +/** clone a procedure description and apply the type substitutions where + the parameters are used */ +let specialize_types_proc callee_pdesc resolved_pdesc substitutions => { + let resolved_pname = Procdesc.get_proc_name resolved_pdesc + and callee_start_node = Procdesc.get_start_node callee_pdesc + and callee_exit_node = Procdesc.get_exit_node callee_pdesc; + let convert_pvar pvar => Pvar.mk (Pvar.get_name pvar) resolved_pname; + let convert_exp = + fun + | Exp.Lvar origin_pvar => Exp.Lvar (convert_pvar origin_pvar) + | exp => exp; + let extract_class_name = + fun + | Typ.Tptr (Tstruct name) _ => Typename.name name + | _ => failwith "Expecting classname for Java types"; + let subst_map = ref Ident.IdentMap.empty; + let redirected_class_name origin_id => + try (Some (Ident.IdentMap.find origin_id !subst_map)) { + | Not_found => None + }; + let convert_instr instrs => + fun + | Sil.Load id (Exp.Lvar origin_pvar as origin_exp) origin_typ loc => { + let (_, specialized_typ) = { + let pvar_name = Pvar.get_name origin_pvar; + try (IList.find (fun (n, _) => Mangled.equal n pvar_name) substitutions) { + | Not_found => (pvar_name, origin_typ) + } + }; + subst_map := Ident.IdentMap.add id specialized_typ !subst_map; + [Sil.Load id (convert_exp origin_exp) specialized_typ loc, ...instrs] + } + | Sil.Load id (Exp.Var origin_id as origin_exp) origin_typ loc => { + let updated_typ = + switch (Ident.IdentMap.find origin_id !subst_map) { + | Typ.Tptr typ _ => typ + | _ => failwith "Expecting a pointer type" + | exception Not_found => origin_typ + }; + [Sil.Load id (convert_exp origin_exp) updated_typ loc, ...instrs] + } + | Sil.Load id origin_exp origin_typ loc => [ + Sil.Load id (convert_exp origin_exp) origin_typ loc, + ...instrs + ] + | Sil.Store assignee_exp origin_typ origin_exp loc => { + let set_instr = + Sil.Store (convert_exp assignee_exp) origin_typ (convert_exp origin_exp) loc; + [set_instr, ...instrs] + } + | Sil.Call + return_ids + (Exp.Const (Const.Cfun (Procname.Java callee_pname_java))) + [(Exp.Var id, _), ...origin_args] + loc + call_flags + when call_flags.CallFlags.cf_virtual && redirected_class_name id != None => { + let redirected_typ = Option.get (redirected_class_name id); + let redirected_pname = + Procname.replace_class + (Procname.Java callee_pname_java) (extract_class_name redirected_typ) + and args = { + let other_args = IList.map (fun (exp, typ) => (convert_exp exp, typ)) origin_args; + [(Exp.Var id, redirected_typ), ...other_args] + }; + let call_instr = + Sil.Call return_ids (Exp.Const (Const.Cfun redirected_pname)) args loc call_flags; + [call_instr, ...instrs] + } + | Sil.Call return_ids origin_call_exp origin_args loc call_flags => { + let converted_args = IList.map (fun (exp, typ) => (convert_exp exp, typ)) origin_args; + let call_instr = + Sil.Call return_ids (convert_exp origin_call_exp) converted_args loc call_flags; + [call_instr, ...instrs] + } + | Sil.Prune origin_exp loc is_true_branch if_kind => [ + Sil.Prune (convert_exp origin_exp) loc is_true_branch if_kind, + ...instrs + ] + | Sil.Declare_locals typed_vars loc => { + let new_typed_vars = IList.map (fun (pvar, typ) => (convert_pvar pvar, typ)) typed_vars; + [Sil.Declare_locals new_typed_vars loc, ...instrs] + } + | Sil.Nullify _ + | Abstract _ + | Sil.Remove_temps _ => + /* these are generated instructions that will be replaced by the preanalysis */ + instrs; + let convert_node_kind = + fun + | Node.Start_node _ => Node.Start_node resolved_pname + | Node.Exit_node _ => Node.Exit_node resolved_pname + | node_kind => node_kind; + let node_map = ref NodeMap.empty; + let rec convert_node node => { + let loc = Node.get_loc node + and kind = convert_node_kind (Node.get_kind node) + and instrs = IList.fold_left convert_instr [] (Node.get_instrs node) |> IList.rev; + Procdesc.create_node resolved_pdesc loc kind instrs + } + and loop callee_nodes => + switch callee_nodes { + | [] => [] + | [node, ...other_node] => + let converted_node = + try (NodeMap.find node !node_map) { + | Not_found => + let new_node = convert_node node + and successors = Node.get_succs node + and exn_nodes = Node.get_exn node; + node_map := NodeMap.add node new_node !node_map; + if (Node.equal node callee_start_node) { + Procdesc.set_start_node resolved_pdesc new_node + }; + if (Node.equal node callee_exit_node) { + Procdesc.set_exit_node resolved_pdesc new_node + }; + Procdesc.node_set_succs_exn callee_pdesc new_node (loop successors) (loop exn_nodes); + new_node + }; + [converted_node, ...loop other_node] + }; + ignore (loop [callee_start_node]); + resolved_pdesc +}; + + /** Creates a copy of a procedure description and a list of type substitutions of the form (name, typ) where name is a parameter. The resulting proc desc is isomorphic but all the type of the parameters are replaced in the instructions according to the list. The virtual calls are also replaced to match the parameter types */ -let specialize_types callee_proc_desc resolved_proc_name args => { +let specialize_types callee_pdesc resolved_pname args => { /* TODO (#9333890): This currently only works when the callee is defined in the same file. Add support to search for the callee procedure description in the execution environment */ - let callee_attributes = Procdesc.get_attributes callee_proc_desc; + let callee_attributes = Procdesc.get_attributes callee_pdesc; let resolved_formals = IList.fold_left2 (fun accu (name, _) (_, arg_typ) => [(name, arg_typ), ...accu]) [] - callee_attributes.ProcAttributes.formals + callee_attributes.formals args |> IList.rev; let resolved_attributes = { ...callee_attributes, - ProcAttributes.formals: resolved_formals, - proc_name: resolved_proc_name + formals: resolved_formals, + proc_name: resolved_pname }; AttributesTable.store_attributes resolved_attributes; - Procdesc.specialize_types callee_proc_desc resolved_attributes resolved_formals + let resolved_pdesc = { + let tmp_cfg = create_cfg (); + create_proc_desc tmp_cfg resolved_attributes + }; + specialize_types_proc callee_pdesc resolved_pdesc resolved_formals }; diff --git a/infer/src/IR/Cfg.rei b/infer/src/IR/Cfg.rei index 1f1a049a8..1a081e689 100644 --- a/infer/src/IR/Cfg.rei +++ b/infer/src/IR/Cfg.rei @@ -15,125 +15,13 @@ open! Utils; /** Control Flow Graph for Interprocedural Analysis */ -/** {2 ADT node and proc_desc} */ -type node; - -type cfg; - - -/** Load a cfg from a file */ -let load_cfg_from_file: DB.filename => option cfg; - - -/** Save a cfg into a file, and save a copy of the source files if the boolean is true */ -let store_cfg_to_file: - save_sources::bool? => source_file::DB.source_file => DB.filename => cfg => unit; - - -/** proc description */ -let module Procdesc: { +/** node of the control flow graph */ +let module Node: { - /** proc description */ + /** type of nodes */ type t; - /** Compute the distance of each node to the exit node, if not computed already */ - let compute_distance_to_exit_node: t => unit; - - /** Create a procdesc */ - let create: cfg => ProcAttributes.t => t; - - /** true if we ran the preanalysis on the CFG associated with [t] */ - let did_preanalysis: t => bool; - - /** indicate that we have performed preanalysis on the CFG assoociated with [t] */ - let signal_did_preanalysis: t => unit; - - /** [remove cfg name remove_nodes] remove the procdesc [name] - from the control flow graph [cfg]. */ - let remove: cfg => Procname.t => unit; - - /** Find the procdesc given the proc name. Return None if not found. */ - let find_from_name: cfg => Procname.t => option t; - - /** Get the attributes of the procedure. */ - let get_attributes: t => ProcAttributes.t; - let get_err_log: t => Errlog.t; - let get_exit_node: t => node; - - /** Get flags for the proc desc */ - let get_flags: t => proc_flags; - - /** Return name and type of formal parameters */ - let get_formals: t => list (Mangled.t, Typ.t); - - /** Return loc information for the procedure */ - let get_loc: t => Location.t; - - /** Return name and type of local variables */ - let get_locals: t => list (Mangled.t, Typ.t); - - /** Return name and type of block's captured variables */ - let get_captured: t => list (Mangled.t, Typ.t); - - /** Return the visibility attribute */ - let get_access: t => PredSymb.access; - let get_nodes: t => list node; - - /** Get the procedure's nodes up until the first branching */ - let get_slope: t => list node; - - /** Get the sliced procedure's nodes up until the first branching */ - let get_sliced_slope: t => (node => bool) => list node; - let get_proc_name: t => Procname.t; - - /** Return the return type of the procedure and type string */ - let get_ret_type: t => Typ.t; - let get_ret_var: t => Pvar.t; - let get_start_node: t => node; - - /** Return [true] iff the procedure is defined, and not just declared */ - let is_defined: t => bool; - - /** Return [true] if the procedure signature has the Java synchronized keyword */ - let is_java_synchronized: t => bool; - - /** iterate over all the nodes of a procedure */ - let iter_nodes: (node => unit) => t => unit; - - /** fold over the calls from the procedure: (callee, location) pairs */ - let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a; - - /** iterate over the calls from the procedure: (callee, location) pairs */ - let iter_calls: ((Procname.t, Location.t) => unit) => t => unit; - - /** iterate over all nodes and their instructions */ - let iter_instrs: (node => Sil.instr => unit) => t => unit; - - /** fold over all nodes and their instructions */ - let fold_instrs: ('a => node => Sil.instr => 'a) => 'a => t => 'a; - - /** iterate over all nodes until we reach a branching structure */ - let iter_slope: (node => unit) => t => unit; - - /** iterate over all calls until we reach a branching structure */ - let iter_slope_calls: (Procname.t => unit) => t => unit; - - /** iterate between two nodes or until we reach a branching structure */ - let iter_slope_range: (node => unit) => node => node => unit; - let set_exit_node: t => node => unit; - - /** Set a flag for the proc desc */ - let set_flag: t => string => string => unit; - let set_start_node: t => node => unit; - - /** append a list of new local variables to the existing list of local variables */ - let append_locals: t => list (Mangled.t, Typ.t) => unit; -}; - - -/** node of the control flow graph */ -let module Node: { - type t = node; /** type of nodes */ + /** node id */ type id = private int; /** kind of cfg node */ @@ -154,25 +42,15 @@ let module Node: { /** kind of Stmt_node for a throw instruction. */ let throw_kind: nodekind; + /** Add declarations for local variables and return variable to the node */ + let add_locals_ret_declaration: t => ProcAttributes.t => list (Mangled.t, Typ.t) => unit; + /** Append the instructions to the list of instructions to execute */ let append_instrs: t => list Sil.instr => unit; - /** Add the instructions at the beginning of the list of instructions to execute */ - let prepend_instrs: t => list Sil.instr => unit; - - /** Add declarations for local variables and return variable to the node */ - let add_locals_ret_declaration: Procdesc.t => t => list (Mangled.t, Typ.t) => unit; - /** Compare two nodes */ let compare: t => t => int; - /** Create a new cfg node with the given location, kind, list of instructions, - and add it to the procdesc. */ - let create: Location.t => nodekind => list Sil.instr => Procdesc.t => t; - - /** create a new empty cfg */ - let create_cfg: unit => cfg; - /** Dump extended instructions for the node */ let d_instrs: sub_instrs::bool => option Sil.instr => t => unit; @@ -182,63 +60,65 @@ let module Node: { /** Check if two nodes are equal */ let equal: t => t => bool; - /** Get the distance to the exit node, if it has been computed */ - let get_distance_to_exit: t => option int; + /** Get the list of callee procnames from the node */ + let get_callees: t => list Procname.t; /** Return a description of the node */ let get_description: printenv => t => string; + /** Get the distance to the exit node, if it has been computed */ + let get_distance_to_exit: t => option int; + /** Get the exception nodes from the current node */ let get_exn: t => list t; + /** Get a list of unique nodes until the first branch starting + from a node with subsequent applications of a generator function */ + let get_generated_slope: t => (t => list t) => list t; + /** Get the unique id of the node */ let get_id: t => id; - /** compare node ids */ - let id_compare: id => id => int; + /** Get the instructions to be executed */ + let get_instrs: t => list Sil.instr; - /** Get the source location of the node */ - let get_loc: t => Location.t; + /** Get the kind of the current node */ + let get_kind: t => nodekind; /** Get the source location of the last instruction in the node */ let get_last_loc: t => Location.t; - /** Get the kind of the current node */ - let get_kind: t => nodekind; + /** Get the source location of the node */ + let get_loc: t => Location.t; /** Get the predecessor nodes of the current node */ let get_preds: t => list t; - /** Get a list of unique nodes until the first branch starting - from a node with subsequent applications of a generator function */ - let get_generated_slope: t => (t => list t) => list t; - /** Get the name of the procedure the node belongs to */ let get_proc_name: t => Procname.t; - /** Get the instructions to be executed */ - let get_instrs: t => list Sil.instr; - - /** Get the list of callee procnames from the node */ - let get_callees: t => list Procname.t; - - /** Get the successor nodes of the current node */ - let get_succs: t => list t; + /** Get the predecessor nodes of a node where the given predicate evaluates to true */ + let get_sliced_preds: t => (t => bool) => list t; /** Get the successor nodes of a node where the given predicate evaluates to true */ let get_sliced_succs: t => (t => bool) => list t; - /** Get the predecessor nodes of a node where the given predicate evaluates to true */ - let get_sliced_preds: t => (t => bool) => list t; + /** Get the successor nodes of the current node */ + let get_succs: t => list t; /** Hash function for nodes */ let hash: t => int; + /** compare node ids */ + let id_compare: id => id => int; + /** Comparison for node kind */ let kind_compare: nodekind => nodekind => int; /** Pretty print the node */ let pp: Format.formatter => t => unit; + + /** Pretty print a node id */ let pp_id: Format.formatter => id => unit; /** Print extended instructions for the node, @@ -247,12 +127,122 @@ let module Node: { /** Replace the instructions to be executed. */ let replace_instrs: t => list Sil.instr => unit; +}; + + +/** procedure description */ +let module Procdesc: { + + /** proc description */ + type t; + + /** append a list of new local variables to the existing list of local variables */ + let append_locals: t => list (Mangled.t, Typ.t) => unit; + + /** Compute the distance of each node to the exit node, if not computed already */ + let compute_distance_to_exit_node: t => unit; + + /** Create a new cfg node with the given location, kind, list of instructions, + and add it to the procdesc. */ + let create_node: t => Location.t => Node.nodekind => list Sil.instr => Node.t; + + /** true if we ran the preanalysis on the CFG associated with [t] */ + let did_preanalysis: t => bool; + + /** fold over the calls from the procedure: (callee, location) pairs */ + let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a; + + /** fold over all nodes and their instructions */ + let fold_instrs: ('a => Node.t => Sil.instr => 'a) => 'a => t => 'a; + + /** Return the visibility attribute */ + let get_access: t => PredSymb.access; + + /** Get the attributes of the procedure. */ + let get_attributes: t => ProcAttributes.t; + + /** Return name and type of block's captured variables */ + let get_captured: t => list (Mangled.t, Typ.t); + let get_err_log: t => Errlog.t; + let get_exit_node: t => Node.t; + + /** Get flags for the proc desc */ + let get_flags: t => proc_flags; + + /** Return name and type of formal parameters */ + let get_formals: t => list (Mangled.t, Typ.t); + + /** Return loc information for the procedure */ + let get_loc: t => Location.t; + + /** Return name and type of local variables */ + let get_locals: t => list (Mangled.t, Typ.t); + let get_nodes: t => list Node.t; + let get_proc_name: t => Procname.t; + + /** Return the return type of the procedure and type string */ + let get_ret_type: t => Typ.t; + let get_ret_var: t => Pvar.t; + + /** Get the sliced procedure's nodes up until the first branching */ + let get_sliced_slope: t => (Node.t => bool) => list Node.t; + + /** Get the procedure's nodes up until the first branching */ + let get_slope: t => list Node.t; + let get_start_node: t => Node.t; + + /** Return [true] iff the procedure is defined, and not just declared */ + let is_defined: t => bool; + + /** Return [true] if the procedure signature has the Java synchronized keyword */ + let is_java_synchronized: t => bool; + + /** iterate over the calls from the procedure: (callee, location) pairs */ + let iter_calls: ((Procname.t, Location.t) => unit) => t => unit; + + /** iterate over all nodes and their instructions */ + let iter_instrs: (Node.t => Sil.instr => unit) => t => unit; + + /** iterate over all the nodes of a procedure */ + let iter_nodes: (Node.t => unit) => t => unit; + + /** iterate over all nodes until we reach a branching structure */ + let iter_slope: (Node.t => unit) => t => unit; + + /** iterate over all calls until we reach a branching structure */ + let iter_slope_calls: (Procname.t => unit) => t => unit; + + /** iterate between two nodes or until we reach a branching structure */ + let iter_slope_range: (Node.t => unit) => Node.t => Node.t => unit; /** Set the successor nodes and exception nodes, and build predecessor links */ - let set_succs_exn: Procdesc.t => t => list t => list t => unit; + let node_set_succs_exn: t => Node.t => list Node.t => list Node.t => unit; + + /** Set the exit node of the procedure */ + let set_exit_node: t => Node.t => unit; + + /** Set a flag for the proc desc */ + let set_flag: t => string => string => unit; + let set_start_node: t => Node.t => unit; + + /** indicate that we have performed preanalysis on the CFG assoociated with [t] */ + let signal_did_preanalysis: t => unit; }; +/** A control-flow graph */ +type cfg; + + +/** Load a cfg from a file */ +let load_cfg_from_file: DB.filename => option cfg; + + +/** Save a cfg into a file, and save a copy of the source files if the boolean is true */ +let store_cfg_to_file: + save_sources::bool? => source_file::DB.source_file => DB.filename => cfg => unit; + + /** Hash table with nodes as keys. */ let module NodeHash: Hashtbl.S with type key = Node.t; @@ -267,10 +257,22 @@ let module IdMap: Map.S with type key = Node.id; /** {2 Functions for manipulating an interprocedural CFG} */ +/** create a new empty cfg */ +let create_cfg: unit => cfg; + + +/** Create a new procdesc */ +let create_proc_desc: cfg => ProcAttributes.t => Procdesc.t; + + /** Iterate over all the procdesc's */ let iter_proc_desc: cfg => (Procname.t => Procdesc.t => unit) => unit; +/** Find the procdesc given the proc name. Return None if not found. */ +let find_proc_desc_from_name: cfg => Procname.t => option Procdesc.t; + + /** Get all the procedures (defined and declared) */ let get_all_procs: cfg => list Procdesc.t; @@ -287,6 +289,10 @@ let iter_all_nodes: (Procdesc.t => Node.t => unit) => cfg => unit; let check_cfg_connectedness: cfg => unit; +/** Remove the procdesc from the control flow graph. */ +let remove_proc_desc: cfg => Procname.t => unit; + + /** Creates a copy of a procedure description and a list of type substitutions of the form (name, typ) where name is a parameter. The resulting procdesc is isomorphic but all the type of the parameters are replaced in the instructions according to the list. diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 265267ccd..b261d63fb 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -187,7 +187,7 @@ let get_cfg exe_env pname = let get_proc_desc exe_env pname = match get_cfg exe_env pname with | Some cfg -> - Cfg.Procdesc.find_from_name cfg pname + Cfg.find_proc_desc_from_name cfg pname | None -> None diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 6aeabcd93..a7a6a3290 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -99,7 +99,7 @@ module Worklist = struct let is_empty (wl : t) : bool = NodeVisitSet.is_empty wl.todo_set - let add (wl : t) (node : Cfg.node) : unit = + let add (wl : t) (node : Cfg.Node.t) : unit = let visits = (* recover visit count if it was visited before *) try NodeMap.find node wl.visit_map with | Not_found -> 0 in @@ -136,7 +136,7 @@ let htable_retrieve (htable : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t) (key : C Paths.PathSet.empty (** Add [d] to the pathset todo at [node] returning true if changed *) -let path_set_put_todo (wl : Worklist.t) (node: Cfg.node) (d: Paths.PathSet.t) : bool = +let path_set_put_todo (wl : Worklist.t) (node: Cfg.Node.t) (d: Paths.PathSet.t) : bool = let changed = if Paths.PathSet.is_empty d then false else @@ -149,7 +149,7 @@ let path_set_put_todo (wl : Worklist.t) (node: Cfg.node) (d: Paths.PathSet.t) : not (Paths.PathSet.equal old_todo todo_new) in changed -let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t = +let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.Node.t) : Paths.PathSet.t = try let node_id = Cfg.Node.get_id node in let todo = Hashtbl.find wl.Worklist.path_set_todo node_id in @@ -250,7 +250,7 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = (** propagate a set of results to the given node *) let propagate - (wl : Worklist.t) pname ~is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) = + (wl : Worklist.t) pname ~is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.Node.t) = let edgeset_todo = (* prop must be a renamed prop by the invariant preserved by PropSet *) let f prop path edgeset_curr = @@ -270,7 +270,7 @@ let propagate (** propagate a set of results, including exceptions and divergence *) let propagate_nodes_divergence tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t) - (succ_nodes: Cfg.node list) (exn_nodes: Cfg.node list) (wl : Worklist.t) = + (succ_nodes: Cfg.Node.t list) (exn_nodes: Cfg.Node.t list) (wl : Worklist.t) = let pname = Cfg.Procdesc.get_proc_name pdesc in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then @@ -463,7 +463,7 @@ let check_assignement_guard pdesc node = (** Perform symbolic execution for a node starting from an initial prop *) let do_symbolic_execution pdesc handle_exn tenv - (node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) = + (node : Cfg.Node.t) (prop: Prop.normal Prop.t) (path : Paths.Path.t) = State.mark_execution_start node; (* build the const map lazily *) State.set_const_map (ConstantPropagation.build_const_map tenv pdesc); diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 48711d5fe..dd6399d2c 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -36,7 +36,7 @@ module Path : sig val create_loc_trace : t -> PredSymb.path_pos option -> Errlog.loc_trace (** return the current node of the path *) - val curr_node : t -> Cfg.node option + val curr_node : t -> Cfg.Node.t option (** dump a path *) val d : t -> unit @@ -45,13 +45,13 @@ module Path : sig val d_stats : t -> unit (** extend a path with a new node reached from the given session, with an optional string for exceptions *) - val extend : Cfg.node -> Typename.t option -> session -> t -> t + val extend : Cfg.Node.t -> Typename.t option -> session -> t -> t (** extend a path with a new node reached from the given session, with an optional string for exceptions *) val add_description : t -> string -> t (** iterate over each node in the path, excluding calls, once *) - val iter_all_nodes_nocalls : (Cfg.node -> unit) -> t -> unit + val iter_all_nodes_nocalls : (Cfg.Node.t -> unit) -> t -> unit (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given. Do not iterate past the given position. @@ -69,7 +69,7 @@ module Path : sig val pp_stats : Format.formatter -> t -> unit (** create a new path with given start node *) - val start : Cfg.node -> t + val start : Cfg.Node.t -> t (* (** equality for paths *) @@ -86,8 +86,8 @@ end = struct type path = (* INVARIANT: stats are always set to dummy_stats unless we are in the middle of a traversal *) (* in particular: a new traversal cannot be initiated during an existing traversal *) - | Pstart of Cfg.node * stats (** start node *) - | Pnode of Cfg.node * Typename.t option * session * path * stats * string option + | Pstart of Cfg.Node.t * stats (** start node *) + | Pnode of Cfg.Node.t * Typename.t option * session * path * stats * string option (** we got to [node] from last [session] perhaps propagating exception [exn_opt], and continue with [path]. *) | Pjoin of path * path * stats (** join of two paths *) @@ -157,7 +157,7 @@ end = struct let start node = Pstart (node, get_dummy_stats ()) - let extend (node: Cfg.node) exn_opt session path = + let extend (node: Cfg.Node.t) exn_opt session path = Pnode (node, exn_opt, session, path, get_dummy_stats (), None) let join p1 p2 = diff --git a/infer/src/backend/paths.mli b/infer/src/backend/paths.mli index 495feb0c6..fffd18a4d 100644 --- a/infer/src/backend/paths.mli +++ b/infer/src/backend/paths.mli @@ -31,7 +31,7 @@ module Path : sig val create_loc_trace : t -> PredSymb.path_pos option -> Errlog.loc_trace (** return the current node of the path *) - val curr_node : t -> Cfg.node option + val curr_node : t -> Cfg.Node.t option (** dump a path *) val d : t -> unit @@ -40,12 +40,12 @@ module Path : sig val d_stats : t -> unit (** extend a path with a new node reached from the given session, with an optional string for exceptions *) - val extend : Cfg.node -> Typename.t option -> session -> t -> t + val extend : Cfg.Node.t -> Typename.t option -> session -> t -> t val add_description : t -> string -> t (** iterate over each node in the path, excluding calls, once *) - val iter_all_nodes_nocalls : (Cfg.node -> unit) -> t -> unit + val iter_all_nodes_nocalls : (Cfg.Node.t -> unit) -> t -> unit (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given. Do not iterate past the given position. @@ -63,7 +63,7 @@ module Path : sig val pp_stats : Format.formatter -> t -> unit (** create a new path with given start node *) - val start : Cfg.node -> t + val start : Cfg.Node.t -> t end (** Set of (prop,path) pairs, where the identity is given by prop *) diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 1f635bcc8..16266bb67 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -100,7 +100,7 @@ let is_visited proc_name node = when starting and finishing the processing of a node *) module NodesHtml : sig val start_node : - int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> + int -> Location.t -> Procname.t -> Cfg.Node.t list -> Cfg.Node.t list -> Cfg.Node.t list -> DB.source_file -> bool val finish_node : Procname.t -> int -> DB.source_file -> unit end = struct @@ -237,7 +237,7 @@ let force_delayed_print fmt = let (loc: Location.t) = Obj.obj loc in Location.pp fmt loc | (L.PTnode_instrs, b_n) -> - let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in + let (b: bool), (io: Sil.instr option), (n: Cfg.Node.t) = Obj.obj b_n in if Config.write_html then F.fprintf fmt "%a%a%a" diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index d1090588f..11ced5fdb 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -37,13 +37,13 @@ val curr_html_formatter : Format.formatter ref val force_delayed_prints : unit -> unit (** Finish a session, and perform delayed print actions if required *) -val node_finish_session : Cfg.node -> DB.source_file -> unit +val node_finish_session : Cfg.Node.t -> DB.source_file -> unit (** Return true if the node was visited during footprint and during re-execution *) val node_is_visited : Procname.t -> Cfg.Node.t -> bool * bool (** Start a session, and create a new html fine for the node if it does not exist yet *) -val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> DB.source_file -> unit +val node_start_session : Cfg.Node.t -> Location.t -> Procname.t -> int -> DB.source_file -> unit (** Write html file for the procedure. The boolean indicates whether to print whole seconds only. *) diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 7bd428ece..ce0f202b0 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -336,7 +336,7 @@ let set_path path pos_opt = let set_prop_tenv_pdesc prop tenv pdesc = !gs.last_prop_tenv_pdesc <- Some (prop, tenv, pdesc) -let set_node (node: Cfg.node) = +let set_node (node: Cfg.Node.t) = !gs.last_instr <- None; !gs.last_node <- node diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index 8a571f935..82b5ac4e8 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -115,7 +115,7 @@ val set_const_map : const_map -> unit val set_instr : Sil.instr -> unit (** Set last node seen in symbolic execution *) -val set_node : Cfg.node -> unit +val set_node : Cfg.Node.t -> unit (** Get last path seen in symbolic execution *) val set_path : Paths.Path.t -> PredSymb.path_pos option -> unit diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 64c8f239f..a4ca949f0 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -26,7 +26,7 @@ let compute_icfg trans_unit_ctx tenv ast = CFrontend_config.global_translation_unit_decls := decl_list; Logging.out_debug "@\n Start creating icfg@\n"; let cg = Cg.create (Some trans_unit_ctx.CFrontend_config.source_file) in - let cfg = Cfg.Node.create_cfg () in + let cfg = Cfg.create_cfg () in IList.iter (CFrontend_declImpl.translate_one_declaration trans_unit_ctx tenv cg cfg `DeclTraversal) decl_list; diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index bc7dff5ea..49bcd1e19 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -26,7 +26,7 @@ struct Logging.out_debug "@\n@\n>>---------- ADDING METHOD: '%s' ---------<<@\n@." (Procname.to_string procname); try - (match Cfg.Procdesc.find_from_name cfg procname with + (match Cfg.find_proc_desc_from_name cfg procname with | Some procdesc -> if (Cfg.Procdesc.is_defined procdesc && not (model_exists procname)) then (let context = @@ -38,9 +38,10 @@ struct "\n\n>>---------- Start translating body of function: '%s' ---------<<\n@." (Procname.to_string procname); let meth_body_nodes = T.instructions_trans context body extra_instrs exit_node in + let proc_attributes = Cfg.Procdesc.get_attributes procdesc in Cfg.Node.add_locals_ret_declaration - procdesc start_node (Cfg.Procdesc.get_locals procdesc); - Cfg.Node.set_succs_exn procdesc start_node meth_body_nodes []; + start_node proc_attributes (Cfg.Procdesc.get_locals procdesc); + Cfg.Procdesc.node_set_succs_exn procdesc start_node meth_body_nodes []; Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc)) | None -> ()) with @@ -51,7 +52,7 @@ struct assert false | Assert_failure (file, line, column) -> Logging.out "Fatal error: exception Assert_failure(%s, %d, %d)\n%!" file line column; - Cfg.Procdesc.remove cfg procname; + Cfg.remove_proc_desc cfg procname; CMethod_trans.create_external_procdesc cfg procname is_objc_method None; () @@ -111,7 +112,7 @@ struct let attrs = { (ProcAttributes.default procname Config.Clang) with loc = loc; objc_accessor = property_accessor; } in - ignore (Cfg.Procdesc.create cfg attrs) + ignore (Cfg.create_proc_desc cfg attrs) | _ -> ()) in process_accessor obj_c_property_decl_info.Clang_ast_t.opdi_getter_method ~getter:true; process_accessor obj_c_property_decl_info.Clang_ast_t.opdi_setter_method ~getter:false diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 8527e6dac..71d7c1f46 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -328,11 +328,11 @@ let sil_func_attributes_of_attributes attrs = do_translation [] attrs let should_create_procdesc cfg procname defined = - match Cfg.Procdesc.find_from_name cfg procname with + match Cfg.find_proc_desc_from_name cfg procname with | Some previous_procdesc -> let is_defined_previous = Cfg.Procdesc.is_defined previous_procdesc in if defined && (not is_defined_previous) then - (Cfg.Procdesc.remove cfg (Cfg.Procdesc.get_proc_name previous_procdesc); + (Cfg.remove_proc_desc cfg (Cfg.Procdesc.get_proc_name previous_procdesc); true) else false | None -> true @@ -418,14 +418,14 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst method_annotation; ret_type; } in - Cfg.Procdesc.create cfg proc_attributes in + Cfg.create_proc_desc cfg proc_attributes in 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 proc_name in - let start_node = Cfg.Node.create loc_start start_kind [] procdesc in + let start_node = Cfg.Procdesc.create_node procdesc loc_start start_kind [] in let exit_kind = Cfg.Node.Exit_node proc_name in - let exit_node = Cfg.Node.create loc_exit exit_kind [] procdesc in + let exit_node = Cfg.Procdesc.create_node procdesc loc_exit exit_kind [] in Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node) in if should_create_procdesc cfg proc_name defined then @@ -434,7 +434,7 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst (** Create a procdesc for objc methods whose signature cannot be found. *) let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = - match Cfg.Procdesc.find_from_name cfg proc_name with + match Cfg.find_proc_desc_from_name cfg proc_name with | Some _ -> () | None -> let ret_type, formals = @@ -450,7 +450,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = loc; ret_type; } in - ignore (Cfg.Procdesc.create cfg proc_attributes) + ignore (Cfg.create_proc_desc cfg proc_attributes) let create_procdesc_with_pointer context pointer class_name_opt name = let open CContext in diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 6c89cf65e..520f46521 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -600,7 +600,7 @@ struct (* create the label root node into the hashtbl *) let sil_loc = CLocation.get_sil_location stmt_info context in let root_node' = GotoLabel.find_goto_label trans_state.context label_name sil_loc in - Cfg.Node.set_succs_exn context.procdesc root_node' res_trans.root_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc root_node' res_trans.root_nodes []; { empty_res_trans with root_nodes = [root_node']; leaf_nodes = trans_state.succ_nodes } and var_deref_trans trans_state stmt_info (decl_ref : Clang_ast_t.decl_ref) = @@ -750,7 +750,7 @@ struct if res_trans_idx.root_nodes <> [] then IList.iter - (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans_idx.root_nodes []) + (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n res_trans_idx.root_nodes []) res_trans_a.leaf_nodes; (* Note the order of res_trans_idx.ids @ res_trans_a.ids is important. *) @@ -1132,7 +1132,7 @@ struct let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in IList.iter - (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans.root_nodes []) + (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n res_trans.root_nodes []) prune_nodes' in (match stmt_list with | [cond; exp1; exp2] -> @@ -1141,7 +1141,7 @@ struct context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in let var_typ = add_reference_if_glvalue typ expr_info in let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in - Cfg.Node.set_succs_exn context.procdesc join_node succ_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc join_node succ_nodes []; let pvar = mk_temp_sil_var procdesc "SIL_temp_conditional___" in Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)]; let continuation' = mk_cond_continuation trans_state.continuation in @@ -1214,7 +1214,7 @@ struct let prune_t = mk_prune_node true e' instrs' in let prune_f = mk_prune_node false e' instrs' in IList.iter - (fun n' -> Cfg.Node.set_succs_exn context.procdesc n' [prune_t; prune_f] []) + (fun n' -> Cfg.Procdesc.node_set_succs_exn context.procdesc n' [prune_t; prune_f] []) res_trans_cond.leaf_nodes; let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then [prune_t; prune_f] @@ -1247,7 +1247,7 @@ struct | Binop.LOr -> prune_nodes_f, prune_nodes_t | _ -> assert false) in IList.iter - (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans_s2.root_nodes []) + (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n res_trans_s2.root_nodes []) prune_to_s2; let root_nodes_to_parent = if (IList.length res_trans_s1.root_nodes) = 0 @@ -1288,7 +1288,7 @@ struct let succ_nodes = trans_state.succ_nodes in let sil_loc = CLocation.get_sil_location stmt_info context in let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in - Cfg.Node.set_succs_exn context.procdesc join_node succ_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc join_node succ_nodes []; let trans_state' = { trans_state with succ_nodes = [join_node] } in let do_branch branch stmt_branch prune_nodes = (* leaf nodes are ignored here as they will be already attached to join_node *) @@ -1302,7 +1302,7 @@ struct let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in IList.iter - (fun n -> Cfg.Node.set_succs_exn context.procdesc n nodes_branch []) + (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n nodes_branch []) prune_nodes' in (match stmt_list with | [_; decl_stmt; cond; stmt1; stmt2] -> @@ -1339,7 +1339,8 @@ struct let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in create_node node_kind res_trans_cond_tmp.instrs sil_loc context in IList.iter - (fun n' -> Cfg.Node.set_succs_exn context.procdesc n' [switch_special_cond_node] []) + (fun n' -> + Cfg.Procdesc.node_set_succs_exn context.procdesc n' [switch_special_cond_node] []) res_trans_cond_tmp.leaf_nodes; let root_nodes = if res_trans_cond_tmp.root_nodes <> [] then res_trans_cond_tmp.root_nodes @@ -1437,8 +1438,8 @@ struct let case_entry_point = connected_instruction (IList.rev case_content) last_nodes in (* connects between cases, then continuation has priority about breaks *) let prune_node_t, prune_node_f = create_prune_nodes_for_case case in - Cfg.Node.set_succs_exn context.procdesc prune_node_t case_entry_point []; - Cfg.Node.set_succs_exn context.procdesc prune_node_f last_prune_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc prune_node_t case_entry_point []; + Cfg.Procdesc.node_set_succs_exn context.procdesc prune_node_f last_prune_nodes []; case_entry_point, [prune_node_t; prune_node_f] | DefaultStmt(stmt_info, default_content) :: rest -> let sil_loc = CLocation.get_sil_location stmt_info context in @@ -1448,14 +1449,15 @@ struct translate_and_connect_cases rest next_nodes [placeholder_entry_point] in let default_entry_point = connected_instruction (IList.rev default_content) last_nodes in - Cfg.Node.set_succs_exn + Cfg.Procdesc.node_set_succs_exn context.procdesc placeholder_entry_point default_entry_point []; default_entry_point, last_prune_nodes | _ -> assert false in let top_entry_point, top_prune_nodes = translate_and_connect_cases list_of_cases succ_nodes succ_nodes in let _ = connected_instruction (IList.rev pre_case_stmts) top_entry_point in - Cfg.Node.set_succs_exn context.procdesc switch_special_cond_node top_prune_nodes []; + Cfg.Procdesc.node_set_succs_exn + context.procdesc switch_special_cond_node top_prune_nodes []; let top_nodes = res_trans_decl.root_nodes in IList.iter (fun n' -> Cfg.Node.append_instrs n' []) succ_nodes; @@ -1536,12 +1538,12 @@ struct match loop_kind with | Loops.For _ | Loops.While _ -> res_trans_body.root_nodes | Loops.DoWhile _ -> [join_node] in - Cfg.Node.set_succs_exn context.procdesc join_node join_succ_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc join_node join_succ_nodes []; IList.iter - (fun n -> Cfg.Node.set_succs_exn context.procdesc n prune_t_succ_nodes []) + (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n prune_t_succ_nodes []) prune_nodes_t; IList.iter - (fun n -> Cfg.Node.set_succs_exn context.procdesc n succ_nodes []) + (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n succ_nodes []) prune_nodes_f; let root_nodes = match loop_kind with @@ -1890,7 +1892,7 @@ struct let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let mk_ret_node instrs = let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in - Cfg.Node.set_succs_exn + Cfg.Procdesc.node_set_succs_exn context.procdesc ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] []; ret_node in @@ -1924,7 +1926,7 @@ struct let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in let ret_node = mk_ret_node instrs in IList.iter - (fun n -> Cfg.Node.set_succs_exn procdesc n [ret_node] []) + (fun n -> Cfg.Procdesc.node_set_succs_exn procdesc n [ret_node] []) res_trans_stmt.leaf_nodes; let root_nodes_to_parent = if IList.length res_trans_stmt.root_nodes >0 @@ -2011,7 +2013,7 @@ struct autorelease_pool_vars, sil_loc, CallFlags.default) in let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in let call_node = create_node node_kind [stmt_call] sil_loc context in - Cfg.Node.set_succs_exn context.procdesc call_node trans_state.succ_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc call_node trans_state.succ_nodes []; let trans_state'={ trans_state with continuation = None; succ_nodes =[call_node] } in instructions trans_state' stmts diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index cecd51718..058351e9b 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -54,7 +54,7 @@ struct let create_node node_kind instrs loc context = let procdesc = CContext.get_procdesc context in - Cfg.Node.create loc node_kind instrs procdesc + Cfg.Procdesc.create_node procdesc loc node_kind instrs let create_prune_node branch e_cond instrs_cond loc ik context = let (e_cond', _) = extract_exp_from_list e_cond @@ -170,7 +170,9 @@ let collect_res_trans pdesc l = if rt'.leaf_nodes <> [] then rt'.leaf_nodes else rt.leaf_nodes in if rt'.root_nodes <> [] then - IList.iter (fun n -> Cfg.Node.set_succs_exn pdesc n rt'.root_nodes []) rt.leaf_nodes; + IList.iter + (fun n -> Cfg.Procdesc.node_set_succs_exn pdesc n rt'.root_nodes []) + rt.leaf_nodes; collect l' { root_nodes = root_nodes; leaf_nodes = leaf_nodes; @@ -244,9 +246,9 @@ struct (* We need to create a node *) let node_kind = Cfg.Node.Stmt_node (nd_name) in let node = Nodes.create_node node_kind res_state.instrs loc trans_state.context in - Cfg.Node.set_succs_exn trans_state.context.procdesc node trans_state.succ_nodes []; + Cfg.Procdesc.node_set_succs_exn trans_state.context.procdesc node trans_state.succ_nodes []; IList.iter - (fun leaf -> Cfg.Node.set_succs_exn trans_state.context.procdesc leaf [node] []) + (fun leaf -> Cfg.Procdesc.node_set_succs_exn trans_state.context.procdesc leaf [node] []) res_state.leaf_nodes; (* Invariant: if root_nodes is empty then the params have not created a node.*) let root_nodes = (if res_state.root_nodes <> [] then res_state.root_nodes @@ -447,13 +449,13 @@ let trans_assertion_failure sil_loc (context : CContext.t) = let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context) and failure_node = Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in - Cfg.Node.set_succs_exn context.procdesc failure_node [exit_node] []; + Cfg.Procdesc.node_set_succs_exn context.procdesc failure_node [exit_node] []; { empty_res_trans with root_nodes = [failure_node]; } let trans_assume_false sil_loc (context : CContext.t) succ_nodes = let instrs_cond = [Sil.Prune (Exp.zero, sil_loc, true, Sil.Ik_land_lor)] in let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in - Cfg.Node.set_succs_exn context.procdesc prune_node succ_nodes []; + Cfg.Procdesc.node_set_succs_exn context.procdesc prune_node succ_nodes []; { empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] } let trans_assertion trans_state sil_loc = diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index aefcf0d01..51dad7090 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -238,28 +238,28 @@ 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 proc_attributes = + { (ProcAttributes.default procname Config.Java) with + ProcAttributes.is_defined = true; + loc = env.pc; + } in let procdesc = - let proc_attributes = - { (ProcAttributes.default procname Config.Java) with - ProcAttributes.is_defined = true; - loc = env.pc; - } in - Cfg.Procdesc.create cfg proc_attributes in + Cfg.create_proc_desc cfg proc_attributes in let harness_node = (* important to reverse the list or there will be scoping issues! *) let instrs = (IList.rev env.instrs) in let nodekind = Cfg.Node.Stmt_node "method_body" in - Cfg.Node.create env.pc nodekind instrs procdesc in + Cfg.Procdesc.create_node procdesc env.pc nodekind instrs in let (start_node, exit_node) = - let create_node kind = Cfg.Node.create env.pc kind [] procdesc in + let create_node kind = Cfg.Procdesc.create_node procdesc env.pc kind [] 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; - Cfg.Node.add_locals_ret_declaration procdesc start_node []; - Cfg.Node.set_succs_exn procdesc start_node [harness_node] [exit_node]; - Cfg.Node.set_succs_exn procdesc harness_node [exit_node] [exit_node]; + Cfg.Node.add_locals_ret_declaration start_node proc_attributes []; + Cfg.Procdesc.node_set_succs_exn procdesc start_node [harness_node] [exit_node]; + Cfg.Procdesc.node_set_succs_exn procdesc harness_node [exit_node] [exit_node]; add_harness_to_cg harness_name harness_node cg (** create a procedure named harness_name that calls each of the methods in trace in the specified diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index f35cd7acb..52bc61b22 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -48,7 +48,8 @@ let add_edges if super_call then (fun _ -> exit_nodes) else JTransExn.create_exception_handlers context [exn_node] get_body_nodes impl in let connect node pc = - Cfg.Node.set_succs_exn context.procdesc node (get_succ_nodes node pc) (get_exn_nodes pc) in + Cfg.Procdesc.node_set_succs_exn + context.procdesc node (get_succ_nodes node pc) (get_exn_nodes pc) in let connect_nodes pc translated_instruction = match translated_instruction with | JTrans.Skip -> () @@ -57,7 +58,7 @@ let add_edges connect node_true pc; connect node_false pc | JTrans.Loop (join_node, node_true, node_false) -> - Cfg.Node.set_succs_exn context.procdesc join_node [node_true; node_false] []; + Cfg.Procdesc.node_set_succs_exn context.procdesc join_node [node_true; node_false] []; connect node_true pc; connect node_false pc in let first_nodes = @@ -65,11 +66,11 @@ let add_edges direct_successors (-1) in (* the exceptions edges here are going directly to the exit node *) - Cfg.Node.set_succs_exn context.procdesc start_node first_nodes exit_nodes; + Cfg.Procdesc.node_set_succs_exn context.procdesc start_node first_nodes exit_nodes; if not super_call then (* the exceptions node is just before the exit node *) - Cfg.Node.set_succs_exn context.procdesc exn_node exit_nodes exit_nodes; + Cfg.Procdesc.node_set_succs_exn context.procdesc exn_node exit_nodes exit_nodes; Array.iteri connect_nodes method_body_nodes @@ -192,7 +193,7 @@ let compute_source_icfg source_basename package_opt source_file = let icfg = { JContext.cg = Cg.create (Some source_file); - JContext.cfg = Cfg.Node.create_cfg (); + JContext.cfg = Cfg.create_cfg (); JContext.tenv = tenv } in let select test procedure cn node = if test node then @@ -212,7 +213,7 @@ let compute_source_icfg let compute_class_icfg source_file linereader program tenv node = let icfg = { JContext.cg = Cg.create (Some source_file); - JContext.cfg = Cfg.Node.create_cfg (); + JContext.cfg = Cfg.create_cfg (); JContext.tenv = tenv } in begin try diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index d40215250..99f37678f 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -267,12 +267,12 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio method_annotation; ret_type = JTransType.return_type program tenv ms; } in - Cfg.Procdesc.create cfg proc_attributes in + Cfg.create_proc_desc cfg proc_attributes in let start_kind = Cfg.Node.Start_node proc_name in - let start_node = Cfg.Node.create Location.dummy start_kind [] procdesc in + let start_node = Cfg.Procdesc.create_node procdesc Location.dummy start_kind [] in let exit_kind = (Cfg.Node.Exit_node proc_name) in - let exit_node = Cfg.Node.create Location.dummy exit_kind [] procdesc in - Cfg.Node.set_succs_exn procdesc start_node [exit_node] [exit_node]; + let exit_node = Cfg.Procdesc.create_node procdesc Location.dummy exit_kind [] in + Cfg.Procdesc.node_set_succs_exn procdesc start_node [exit_node] [exit_node]; Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node; procdesc @@ -291,7 +291,7 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio method_annotation; ret_type = JTransType.return_type program tenv ms; } in - Cfg.Procdesc.create cfg proc_attributes; + Cfg.create_proc_desc cfg proc_attributes; | Javalib.ConcreteMethod cm -> let impl = get_implementation cm in let locals, formals = locals_formals program tenv cn impl in @@ -304,32 +304,32 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in update_constr_loc cn ms loc_start; update_init_loc cn ms loc_exit; + let proc_attributes = + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.access = trans_access cm.Javalib.cm_access; + exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; + formals; + is_bridge_method = cm.Javalib.cm_bridge; + is_defined = true; + is_synthetic_method = cm.Javalib.cm_synthetic; + is_java_synchronized_method = cm.Javalib.cm_synchronized; + loc = loc_start; + locals; + method_annotation; + ret_type = JTransType.return_type program tenv ms; + } in let procdesc = - let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with - ProcAttributes.access = trans_access cm.Javalib.cm_access; - exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; - formals; - is_bridge_method = cm.Javalib.cm_bridge; - is_defined = true; - is_synthetic_method = cm.Javalib.cm_synthetic; - is_java_synchronized_method = cm.Javalib.cm_synchronized; - loc = loc_start; - locals; - method_annotation; - ret_type = JTransType.return_type program tenv ms; - } in - Cfg.Procdesc.create cfg proc_attributes in + Cfg.create_proc_desc cfg proc_attributes in let start_kind = Cfg.Node.Start_node proc_name in - let start_node = Cfg.Node.create loc_start start_kind [] procdesc in + let start_node = Cfg.Procdesc.create_node procdesc loc_start start_kind [] in let exit_kind = (Cfg.Node.Exit_node proc_name) in - let exit_node = Cfg.Node.create loc_exit exit_kind [] procdesc in + let exit_node = Cfg.Procdesc.create_node procdesc loc_exit exit_kind [] in let exn_kind = Cfg.Node.exn_sink_kind in - let exn_node = Cfg.Node.create loc_exit exn_kind [] procdesc in + let exn_node = Cfg.Procdesc.create_node procdesc loc_exit exn_kind [] in JContext.add_exn_node proc_name exn_node; Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node; - Cfg.Node.add_locals_ret_declaration procdesc start_node locals; + Cfg.Node.add_locals_ret_declaration start_node proc_attributes locals; procdesc in Some procdesc with JBir.Subroutine | JBasics.Class_structure_error _ -> @@ -709,7 +709,7 @@ let rec instruction (context : JContext.t) pc instr : translation = let file = loc.Location.file in let match_never_null = Inferconfig.never_return_null_matcher in let create_node node_kind sil_instrs = - Cfg.Node.create loc node_kind sil_instrs context.procdesc in + Cfg.Procdesc.create_node context.procdesc loc node_kind sil_instrs in let return_not_null () = match_never_null loc.Location.file proc_name in let trans_monitor_enter_exit context expr pc loc builtin node_desc = diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index dbf48dd2c..b01413fe7 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -30,7 +30,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle let catch_block_table = Hashtbl.create 1 in let exn_message = "exception handler" in let procdesc = context.procdesc in - let create_node loc node_kind instrs = Cfg.Node.create loc node_kind instrs procdesc in + let create_node loc node_kind instrs = Cfg.Procdesc.create_node procdesc loc node_kind instrs in let ret_var = Cfg.Procdesc.get_ret_var procdesc in let ret_type = Cfg.Procdesc.get_ret_type procdesc in let id_ret_val = Ident.create_fresh Ident.knormal in @@ -91,8 +91,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle let node_false = let instrs_false = [instr_call_instanceof; instr_prune_false] @ (if rethrow_exception then [instr_rethrow_exn] else []) in create_node loc node_kind_false instrs_false in - Cfg.Node.set_succs_exn procdesc node_true catch_nodes exit_nodes; - Cfg.Node.set_succs_exn procdesc node_false succ_nodes exit_nodes; + Cfg.Procdesc.node_set_succs_exn procdesc node_true catch_nodes exit_nodes; + Cfg.Procdesc.node_set_succs_exn procdesc node_false succ_nodes exit_nodes; let is_finally = handler.JBir.e_catch_type = None in if is_finally then [node_true] (* TODO (#4759480): clean up the translation so prune nodes are not created at all *) @@ -109,7 +109,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle | n:: _ -> Cfg.Node.get_loc n | [] -> Location.dummy in let entry_node = create_entry_node loc in - Cfg.Node.set_succs_exn procdesc entry_node nodes_first_handler exit_nodes; + Cfg.Procdesc.node_set_succs_exn procdesc entry_node nodes_first_handler exit_nodes; Hashtbl.add catch_block_table handler_list [entry_node] in Hashtbl.iter (fun _ handler_list -> create_entry_block handler_list) handler_table; catch_block_table diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 198710151..a93643654 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -168,15 +168,15 @@ module Make type assert_map = string M.t let structured_program_to_cfg program test_pname = - let cfg = Cfg.Node.create_cfg () in + let cfg = Cfg.create_cfg () in let pdesc = - Cfg.Procdesc.create cfg (ProcAttributes.default test_pname !Config.curr_language) in + Cfg.create_proc_desc 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 dummy_loc kind cmds pdesc in + Cfg.Procdesc.create_node pdesc dummy_loc kind cmds in let set_succs cur_node succs ~exn_handlers= - Cfg.Node.set_succs_exn pdesc cur_node succs exn_handlers in + Cfg.Procdesc.node_set_succs_exn pdesc cur_node succs exn_handlers in let mk_prune_nodes_for_cond cond_exp if_kind = let mk_prune_node cond_exp if_kind true_branch = let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 342f4f77e..2f9df7ef6 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -16,9 +16,9 @@ module InstrCfg = ProcCfg.OneInstrPerNode (ProcCfg.Normal) module BackwardInstrCfg = ProcCfg.Backward (InstrCfg) let tests = - let cfg = Cfg.Node.create_cfg () in + let cfg = Cfg.create_cfg () in let test_pdesc = - Cfg.Procdesc.create cfg (ProcAttributes.default Procname.empty_block !Config.curr_language) in + Cfg.create_proc_desc cfg (ProcAttributes.default Procname.empty_block !Config.curr_language) in let dummy_instr1 = Sil.Remove_temps ([], Location.dummy) in let dummy_instr2 = Sil.Abstract Location.dummy in let dummy_instr3 = Sil.Remove_temps ([Ident.create_fresh Ident.knormal], Location.dummy) in @@ -28,7 +28,7 @@ let tests = let instrs3 = [dummy_instr4] in let instrs4 = [] in let create_node instrs = - Cfg.Node.create Location.dummy (Cfg.Node.Stmt_node "") instrs test_pdesc in + Cfg.Procdesc.create_node test_pdesc Location.dummy (Cfg.Node.Stmt_node "") instrs in let n1 = create_node instrs1 in let n2 = create_node instrs2 in let n3 = create_node instrs3 in @@ -37,9 +37,9 @@ let tests = Cfg.Procdesc.set_start_node test_pdesc n1; (* let -> represent normal transitions and -*-> represent exceptional transitions *) (* creating graph n1 -> n2, n1 -*-> n3, n2 -> n4, n2 -*-> n3, n3 -> n4 , n3 -*> n4 *) - Cfg.Node.set_succs_exn test_pdesc n1 [n2] [n3]; - Cfg.Node.set_succs_exn test_pdesc n2 [n4] [n3]; - Cfg.Node.set_succs_exn test_pdesc n3 [n4] [n4]; + Cfg.Procdesc.node_set_succs_exn test_pdesc n1 [n2] [n3]; + Cfg.Procdesc.node_set_succs_exn test_pdesc n2 [n4] [n3]; + Cfg.Procdesc.node_set_succs_exn test_pdesc n3 [n4] [n4]; let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in