diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index b7104eb3f..860af9211 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -21,8 +21,8 @@ let module F = Format; let module Node = { type id = int; type nodekind = - | Start_node proc_desc - | Exit_node proc_desc + | Start_node Procname.t + | Exit_node Procname.t | Stmt_node string | Join_node | Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ @@ -33,22 +33,18 @@ let module Node = { nd_id: id, /** distance to the exit node */ mutable nd_dist_exit: option int, - /** dead program variables after executing the instructions */ - mutable nd_dead_pvars_after: list Pvar.t, - /** dead program variables before executing the instructions */ - mutable nd_deads_before: list Pvar.t, /** exception nodes in the cfg */ mutable nd_exn: list t, /** instructions for symbolic execution */ mutable nd_instrs: list Sil.instr, /** kind of node */ - mutable nd_kind: nodekind, + nd_kind: nodekind, /** location in the source code */ - mutable nd_loc: Location.t, + nd_loc: Location.t, /** predecessor nodes in the cfg */ mutable nd_preds: list t, /** proc desc from cil */ - mutable nd_proc: option proc_desc, + nd_proc: option proc_desc, /** successor nodes in the cfg */ mutable nd_succs: list t } @@ -66,20 +62,13 @@ let module Node = { /** data type for the control flow graph */ type cfg = { - node_id: ref int, - node_list: ref (list t), - name_pdesc_tbl: Procname.Hash.t proc_desc, /** Map proc name to procdesc */ - mutable priority_set: Procname.Set.t - /** set of function names to be analyzed first */ + mutable node_id: int, + mutable node_list: list t, + name_pdesc_tbl: Procname.Hash.t proc_desc /** Map proc name to procdesc */ }; - let create_cfg () => - /** create a new empty cfg */ - { - node_id: ref 0, - node_list: ref [], - name_pdesc_tbl: Procname.Hash.create 1000, - priority_set: Procname.Set.empty - }; + + /** create a new empty cfg */ + let create_cfg () => {node_id: 0, node_list: [], name_pdesc_tbl: Procname.Hash.create 16}; /** compute the list of procedures added or changed in [cfg_new] over [cfg_old] */ let mark_unchanged_pdescs cfg_new cfg_old => { @@ -149,8 +138,8 @@ let module Node = { Procname.Hash.iter mark_pdesc_if_unchanged new_procs }; let node_id_gen cfg => { - incr cfg.node_id; - !cfg.node_id + cfg.node_id = cfg.node_id + 1; + cfg.node_id }; let pdesc_tbl_add cfg proc_name proc_desc => Procname.Hash.add cfg.name_pdesc_tbl proc_name proc_desc; @@ -160,8 +149,6 @@ let module Node = { let dummy () => { nd_id: 0, nd_dist_exit: None, - nd_dead_pvars_after: [], - nd_deads_before: [], nd_instrs: [], nd_kind: Skip_node "dummy", nd_loc: Location.dummy, @@ -173,14 +160,12 @@ let module Node = { let compare node1 node2 => int_compare node1.nd_id node2.nd_id; let hash node => Hashtbl.hash node.nd_id; let equal node1 node2 => compare node1 node2 == 0; - let get_all_nodes cfg => !cfg.node_list; + let get_all_nodes cfg => cfg.node_list; let create cfg loc kind instrs pdesc => { let node_id = node_id_gen cfg; let node = { nd_id: node_id, nd_dist_exit: None, - nd_dead_pvars_after: [], - nd_deads_before: [], nd_instrs: instrs, nd_kind: kind, nd_loc: loc, @@ -189,7 +174,7 @@ let module Node = { nd_succs: [], nd_exn: [] }; - cfg.node_list := [node, ...!cfg.node_list]; + cfg.node_list = [node, ...cfg.node_list]; pdesc.pd_nodes = [node, ...pdesc.pd_nodes]; node }; @@ -298,16 +283,13 @@ let module Node = { /** Get the node kind */ let get_kind node => node.nd_kind; - /** Set the node kind */ - let set_kind node kind => node.nd_kind = kind; - /** Comparison for node kind */ let kind_compare k1 k2 => switch (k1, k2) { - | (Start_node pd1, Start_node pd2) => int_compare pd1.pd_id pd2.pd_id + | (Start_node pn1, Start_node pn2) => Procname.compare pn1 pn2 | (Start_node _, _) => (-1) | (_, Start_node _) => 1 - | (Exit_node pd1, Exit_node pd2) => int_compare pd1.pd_id pd2.pd_id + | (Exit_node pn1, Exit_node pn2) => Procname.compare pn1 pn2 | (Exit_node _, _) => (-1) | (_, Exit_node _) => 1 | (Stmt_node s1, Stmt_node s2) => string_compare s1 s2 @@ -359,27 +341,12 @@ let module Node = { | [instr, ..._] => Sil.instr_get_loc instr | [] => n.nd_loc }; - - /** Set the location of the node */ - let set_loc n loc => n.nd_loc = loc; let pp_id f id => F.fprintf f "%d" id; let pp f node => pp_id f (get_id node); let proc_desc_from_name cfg proc_name => try (Some (pdesc_tbl_find cfg proc_name)) { | Not_found => None }; - let set_dead_pvars node after dead => - if after { - node.nd_dead_pvars_after = dead - } else { - node.nd_deads_before = dead - }; - let get_dead_pvars node after => - if after { - node.nd_dead_pvars_after - } else { - node.nd_deads_before - }; let get_distance_to_exit node => node.nd_dist_exit; /** Append the instructions to the list of instructions to execute */ @@ -424,7 +391,7 @@ let module Node = { }; let remove_node' filter_out_fun cfg => { let remove_node_in_cfg nodes => IList.filter filter_out_fun nodes; - cfg.node_list := remove_node_in_cfg !cfg.node_list + cfg.node_list = remove_node_in_cfg cfg.node_list }; let remove_node_set cfg nodes => remove_node' (fun node' => not (NodeSet.mem node' nodes)) cfg; let proc_desc_remove cfg name remove_nodes => { @@ -741,8 +708,8 @@ let module Node = { instrs; let convert_node_kind = fun - | Start_node _ => Start_node resolved_proc_desc - | Exit_node _ => Exit_node resolved_proc_desc + | Start_node _ => Start_node resolved_proc_name + | Exit_node _ => Exit_node resolved_proc_name | node_kind => node_kind; let node_map = ref NodeMap.empty; let rec convert_node node => { diff --git a/infer/src/IR/Cfg.rei b/infer/src/IR/Cfg.rei index 794f382c6..5daaf9e8b 100644 --- a/infer/src/IR/Cfg.rei +++ b/infer/src/IR/Cfg.rei @@ -140,8 +140,8 @@ let module Node: { /** kind of cfg node */ type nodekind = - | Start_node Procdesc.t - | Exit_node Procdesc.t + | Start_node Procname.t + | Exit_node Procname.t | Stmt_node string | Join_node | Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ @@ -188,10 +188,6 @@ let module Node: { /** Get all the nodes */ let get_all_nodes: cfg => list t; - /** Get the (after/before) dead program variables. - After/before indicated with the true/false flag. */ - let get_dead_pvars: t => bool => list Pvar.t; - /** Get the distance to the exit node, if it has been computed */ let get_distance_to_exit: t => option int; @@ -258,16 +254,6 @@ let module Node: { /** Replace the instructions to be executed. */ let replace_instrs: t => list Sil.instr => unit; - /** Set the (after/before) dead program variables. - After/before indicated with the true/false flag. */ - let set_dead_pvars: t => bool => list Pvar.t => unit; - - /** Set the node kind */ - let set_kind: t => nodekind => unit; - - /** Set the source location of the node */ - let set_loc: t => Location.t => unit; - /** Set the successor nodes and exception nodes, and build predecessor links */ let set_succs_exn: cfg => t => list t => list t => unit; }; diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 36448c724..016a153c4 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -947,21 +947,19 @@ let pp_local_list fmt etl = IList.iter (fun (id, ty) -> Format.fprintf fmt " %a:%a" Mangled.pp id (Typ.pp_full pe_text) ty) etl -let pp_cfgnodelabel fmt (n : Cfg.Node.t) = +let pp_cfgnodelabel pdesc fmt (n : Cfg.Node.t) = let pp_label fmt n = match Cfg.Node.get_kind n with - | Cfg.Node.Start_node (pdesc) -> - (* let def = if Cfg.Procdesc.is_defined pdesc then "defined" else "declared" in *) - (* Format.fprintf fmt "Start %a (%s)" pp_id (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) def *) + | Cfg.Node.Start_node pname -> Format.fprintf fmt "Start %s\\nFormals: %a\\nLocals: %a" - (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) + (Procname.to_string pname) pp_etlist (Cfg.Procdesc.get_formals pdesc) pp_local_list (Cfg.Procdesc.get_locals pdesc); if IList.length (Cfg.Procdesc.get_captured pdesc) <> 0 then Format.fprintf fmt "\\nCaptured: %a" pp_local_list (Cfg.Procdesc.get_captured pdesc) - | Cfg.Node.Exit_node (pdesc) -> - Format.fprintf fmt "Exit %s" (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) + | Cfg.Node.Exit_node pname -> + Format.fprintf fmt "Exit %s" (Procname.to_string pname) | Cfg.Node.Join_node -> Format.fprintf fmt "+" | Cfg.Node.Prune_node (is_true_branch, _, _) -> @@ -992,8 +990,11 @@ pp_cfgnodename src pp_cfgnodename dest *) -let pp_cfgnode fmt (n: Cfg.Node.t) = - F.fprintf fmt "%a [label=\"%a\" %a]\n\t\n" pp_cfgnodename n pp_cfgnodelabel n pp_cfgnodeshape n; +let pp_cfgnode pdesc fmt (n: Cfg.Node.t) = + F.fprintf fmt "%a [label=\"%a\" %a]\n\t\n" + pp_cfgnodename n + (pp_cfgnodelabel pdesc) n + pp_cfgnodeshape n; let print_edge n1 n2 is_exn = let color = if is_exn then "[color=\"red\" ]" else "" in match Cfg.Node.get_kind n2 with @@ -1020,8 +1021,9 @@ let pp_cfgnode fmt (n: Cfg.Node.t) = let print_icfg source fmt cfg = let print_node node = let loc = Cfg.Node.get_loc node in + let pdesc = Cfg.Node.get_proc_desc node in if (Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file source) then - F.fprintf fmt "%a\n" pp_cfgnode node in + F.fprintf fmt "%a\n" (pp_cfgnode pdesc) node in IList.iter print_node (Cfg.Node.get_all_nodes cfg) let write_icfg_dotty_to_file source cfg fname = diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index bd32844f4..ce5697e01 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -454,8 +454,7 @@ end = struct let curr_loc = Cfg.Node.get_loc curr_node in match Cfg.Node.get_kind curr_node with | Cfg.Node.Join_node -> () (* omit join nodes from error traces *) - | Cfg.Node.Start_node pdesc -> - let pname = Cfg.Procdesc.get_proc_name pdesc in + | Cfg.Node.Start_node pname -> let name = Procname.to_string pname in let name_id = Procname.to_filename pname in let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in @@ -480,8 +479,7 @@ end = struct [(Io_infer.Xml.tag_kind,"condition"); (Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in trace := mk_trace_elem level curr_loc descr node_tags :: !trace - | Cfg.Node.Exit_node pdesc -> - let pname = Cfg.Procdesc.get_proc_name pdesc in + | Cfg.Node.Exit_node pname -> let descr = "return from a call to " ^ (Procname.to_string pname) in let name = Procname.to_string pname in let name_id = Procname.to_filename pname in @@ -708,4 +706,3 @@ end = struct IList.fold_left (fun ps (p, pa) -> add_renamed_prop p pa ps) empty pl end (* =============== END of the PathSet module ===============*) - diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 3e9337870..09256f28d 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -539,8 +539,7 @@ let write_html_file linereader filename procs = IList.iter (fun n -> match Cfg.Node.get_kind n with - | Cfg.Node.Start_node proc_desc -> - let proc_name = Cfg.Procdesc.get_proc_name proc_desc in + | Cfg.Node.Start_node proc_name -> let num_specs = IList.length (Specs.get_specs proc_name) in let label = (Escape.escape_xml (Procname.to_string proc_name)) ^ diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 2aabf03fe..68490f513 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -422,9 +422,9 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst if defined then (if !Config.arc_mode then Cfg.Procdesc.set_flag procdesc Mleak_buckets.objc_arc_flag "true"; - let start_kind = Cfg.Node.Start_node procdesc in + let start_kind = Cfg.Node.Start_node proc_name in let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in - let exit_kind = Cfg.Node.Exit_node procdesc in + let exit_kind = Cfg.Node.Exit_node proc_name in let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node) in diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 9168d03b7..b5efd323c 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -237,9 +237,10 @@ let add_harness_to_cg harness_name harness_node cg = let setup_harness_cfg harness_name env cg cfg = (* each procedure has different scope: start names from id 0 *) Ident.NameGenerator.reset (); + let procname = Procname.Java harness_name in let procdesc = let proc_attributes = - { (ProcAttributes.default (Procname.Java harness_name) Config.Java) with + { (ProcAttributes.default procname Config.Java) with ProcAttributes.is_defined = true; loc = env.pc; } in @@ -251,8 +252,8 @@ let setup_harness_cfg harness_name env cg cfg = Cfg.Node.create cfg env.pc nodekind instrs procdesc in let (start_node, exit_node) = let create_node kind = Cfg.Node.create cfg env.pc kind [] procdesc in - let start_kind = Cfg.Node.Start_node procdesc in - let exit_kind = Cfg.Node.Exit_node procdesc in + let start_kind = Cfg.Node.Start_node procname in + let exit_kind = Cfg.Node.Exit_node procname in (create_node start_kind, create_node exit_kind) in Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node; diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 18f345337..71fc7557c 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -269,9 +269,9 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio ret_type = JTransType.return_type program tenv ms; } in Cfg.Procdesc.create cfg proc_attributes in - let start_kind = Cfg.Node.Start_node procdesc in + let start_kind = Cfg.Node.Start_node proc_name in let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in - let exit_kind = (Cfg.Node.Exit_node procdesc) in + let exit_kind = (Cfg.Node.Exit_node proc_name) in let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node]; Cfg.Procdesc.set_start_node procdesc start_node; @@ -321,9 +321,9 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio ret_type = JTransType.return_type program tenv ms; } in Cfg.Procdesc.create cfg proc_attributes in - let start_kind = Cfg.Node.Start_node procdesc in + let start_kind = Cfg.Node.Start_node proc_name in let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in - let exit_kind = (Cfg.Node.Exit_node procdesc) in + let exit_kind = (Cfg.Node.Exit_node proc_name) in let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in let exn_kind = Cfg.Node.exn_sink_kind in let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc in diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 1d267127b..cd54fa458 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -171,6 +171,7 @@ module Make let cfg = Cfg.Node.create_cfg () in let pdesc = Cfg.Procdesc.create cfg (ProcAttributes.default test_pname !Config.curr_language) in + let pname = Cfg.Procdesc.get_proc_name pdesc in let create_node kind cmds = Cfg.Node.create cfg dummy_loc kind cmds pdesc in @@ -234,12 +235,12 @@ module Make (fun acc instr -> structured_instr_to_node acc exn_handlers instr) (last_node, assert_map) instrs in - let start_node = create_node (Cfg.Node.Start_node pdesc) [] in + let start_node = create_node (Cfg.Node.Start_node pname) [] in Cfg.Procdesc.set_start_node pdesc start_node; let no_exn_handlers = [] in let last_node, assert_map = structured_instrs_to_node start_node M.empty no_exn_handlers program in - let exit_node = create_node (Cfg.Node.Exit_node pdesc) [] in + let exit_node = create_node (Cfg.Node.Exit_node pname) [] in set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers; Cfg.Procdesc.set_exit_node pdesc exit_node; pdesc, assert_map