diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index e2b190562..338d2ed39 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -74,8 +74,8 @@ module Node = struct [@@deriving compare] type nodekind = - | Start_node of Typ.Procname.t - | Exit_node of Typ.Procname.t + | Start_node + | Exit_node | Stmt_node of stmt_nodekind | Join_node | Prune_node of bool * Sil.if_kind * string (** (true/false branch, if_kind, comment) *) @@ -303,11 +303,11 @@ module Node = struct F.fprintf fmt "statements (%a)" pp_stmt s | Prune_node (_, _, descr) -> F.fprintf fmt "assume %s" descr - | Exit_node _ -> + | Exit_node -> F.pp_print_string fmt "exit" | Skip_node s -> F.fprintf fmt "skip (%s)" s - | Start_node _ -> + | Start_node -> F.pp_print_string fmt "start" | Join_node -> F.pp_print_string fmt "join" @@ -328,11 +328,11 @@ module Node = struct "Instructions" | Prune_node (_, _, descr) -> "Conditional" ^ " " ^ descr - | Exit_node _ -> + | Exit_node -> "Exit" | Skip_node _ -> "Skip" - | Start_node _ -> + | Start_node -> "Start" | Join_node -> "Join" @@ -557,7 +557,7 @@ let create_node pdesc loc kind instrs = create_node_internal pdesc loc kind (Ins otherwise nullify and abstract instructions cannot be added after a conditional. *) let node_set_succs_exn pdesc (node : Node.t) succs exn = match (node.kind, succs) with - | Join_node, [({Node.kind= Exit_node _} as exit_node)] -> + | Join_node, [({Node.kind= Exit_node} as exit_node)] -> let kind = Node.Stmt_node BetweenJoinAndExit in let node' = create_node_internal pdesc node.loc kind node.instrs in set_succs_exn_base node [node'] exn ; @@ -691,21 +691,12 @@ let has_modify_in_block_attr procdesc pvar = (** Applies f_instr_list to all the instructions in all the nodes of the cfg *) let convert_cfg ~callee_pdesc ~resolved_pdesc ~f_instr_list = - let resolved_pname = get_proc_name resolved_pdesc - and callee_start_node = get_start_node callee_pdesc + let callee_start_node = get_start_node callee_pdesc and callee_exit_node = get_exit_node callee_pdesc in - let convert_node_kind = function - | Node.Start_node _ -> - Node.Start_node resolved_pname - | Node.Exit_node _ -> - Node.Exit_node resolved_pname - | node_kind -> - node_kind - in let node_map = ref NodeMap.empty in let rec convert_node node = let loc = Node.get_loc node - and kind = convert_node_kind (Node.get_kind node) + and kind = Node.get_kind node and instrs = f_instr_list (Node.get_instrs node) in create_node_internal resolved_pdesc loc kind instrs and loop callee_nodes = @@ -1027,7 +1018,7 @@ let specialize_with_block_args callee_pdesc pname_with_block_args block_args = let is_connected proc_desc = - let is_exit_node n = match Node.get_kind n with Node.Exit_node _ -> true | _ -> false in + let is_exit_node n = match Node.get_kind n with Node.Exit_node -> true | _ -> false in let is_between_join_and_exit_node n = match Node.get_kind n with | Node.Stmt_node BetweenJoinAndExit | Node.Stmt_node Destruction -> ( @@ -1053,9 +1044,9 @@ let is_connected proc_desc = let succs = Node.get_succs n in let preds = Node.get_preds n in match Node.get_kind n with - | Node.Start_node _ -> + | Node.Start_node -> if List.is_empty succs || not (List.is_empty preds) then Error `Other else Ok () - | Node.Exit_node _ -> + | Node.Exit_node -> if (not (List.is_empty succs)) || List.is_empty preds then Error `Other else Ok () | Node.Stmt_node _ | Node.Prune_node _ | Node.Skip_node _ -> if List.is_empty succs || List.is_empty preds then Error `Other else Ok () diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index a327950bc..623c0e3cb 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -69,8 +69,8 @@ module Node : sig (** kind of cfg node *) type nodekind = - | Start_node of Typ.Procname.t - | Exit_node of Typ.Procname.t + | Start_node + | Exit_node | Stmt_node of stmt_nodekind | Join_node | Prune_node of bool * Sil.if_kind * string (** (true/false branch, if_kind, comment) *) diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 4baa7184e..e9e760687 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -1092,7 +1092,8 @@ let pp_local_list fmt etl = List.iter ~f:(Procdesc.pp_local fmt) etl let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) = let pp_label fmt n = match Procdesc.Node.get_kind n with - | Procdesc.Node.Start_node pname -> + | Procdesc.Node.Start_node -> + let pname = Procdesc.Node.get_proc_name n in let pname_string = Escape.escape_dotty (Typ.Procname.to_string pname) in let attributes = Procdesc.get_attributes pdesc in let byvals = attributes.ProcAttributes.by_vals in @@ -1103,7 +1104,8 @@ let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) = let method_annotation = attributes.ProcAttributes.method_annotation in if not (Annot.Method.is_empty method_annotation) then Format.fprintf fmt "\\nAnnotation: %a" (Annot.Method.pp pname_string) method_annotation - | Procdesc.Node.Exit_node pname -> + | Procdesc.Node.Exit_node -> + let pname = Procdesc.Node.get_proc_name n in Format.fprintf fmt "Exit %s" (Escape.escape_dotty (Typ.Procname.to_string pname)) | Procdesc.Node.Join_node -> Format.pp_print_char fmt '+' @@ -1128,7 +1130,7 @@ let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) = let pp_cfgnodeshape fmt (n : Procdesc.Node.t) = match Procdesc.Node.get_kind n with - | Procdesc.Node.Start_node _ | Procdesc.Node.Exit_node _ -> + | Procdesc.Node.Start_node | Procdesc.Node.Exit_node -> F.pp_print_string fmt "color=yellow style=filled" | Procdesc.Node.Prune_node _ -> F.fprintf fmt "shape=\"invhouse\"" @@ -1147,7 +1149,7 @@ let pp_cfgnode pdesc fmt (n : Procdesc.Node.t) = let print_edge n1 n2 is_exn = let color = if is_exn then "[color=\"red\" ]" else "" in match Procdesc.Node.get_kind n2 with - | Procdesc.Node.Exit_node _ when is_exn -> + | Procdesc.Node.Exit_node when is_exn -> (* don't print exception edges to the exit node *) () | _ -> diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index f3d411dd1..faf53c851 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -14,7 +14,7 @@ let add_abstraction_instructions pdesc = let open Procdesc in (* true if there is a succ node s.t.: it is an exit node, or the succ of >1 nodes *) let converging_node node = - let is_exit node = match Node.get_kind node with Node.Exit_node _ -> true | _ -> false in + let is_exit node = match Node.get_kind node with Node.Exit_node -> true | _ -> false in let succ_nodes = Node.get_succs node in if List.exists ~f:is_exit succ_nodes then true else @@ -22,9 +22,9 @@ let add_abstraction_instructions pdesc = in let node_requires_abstraction node = match Node.get_kind node with - | Node.Start_node _ | Node.Join_node -> + | Node.Start_node | Node.Join_node -> false - | Node.Exit_node _ | Node.Stmt_node _ | Node.Prune_node _ | Node.Skip_node _ -> + | Node.Exit_node | Node.Stmt_node _ | Node.Prune_node _ | Node.Skip_node _ -> converging_node node in let do_node node = diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 89072e53b..212e13e47 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -332,7 +332,8 @@ let write_html_file linereader filename procs = List.iter ~f:(fun n -> match Procdesc.Node.get_kind n with - | Procdesc.Node.Start_node proc_name -> + | Procdesc.Node.Start_node -> + let proc_name = Procdesc.Node.get_proc_name n in let num_specs = match Summary.get proc_name with | None -> diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index ae6b1a453..baa44652e 100644 --- a/infer/src/biabduction/Paths.ml +++ b/infer/src/biabduction/Paths.ml @@ -481,7 +481,8 @@ end = struct match Procdesc.Node.get_kind curr_node with | Procdesc.Node.Join_node -> () (* omit join nodes from error traces *) - | Procdesc.Node.Start_node pname -> + | Procdesc.Node.Start_node -> + let pname = Procdesc.Node.get_proc_name curr_node in let descr = "start of procedure " ^ Typ.Procname.to_simplified_string pname in let node_tags = [Errlog.Procedure_start pname] in trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace @@ -507,7 +508,8 @@ end = struct in let node_tags = [Errlog.Condition is_true_branch] in trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace - | Procdesc.Node.Exit_node pname -> + | Procdesc.Node.Exit_node -> + let pname = Procdesc.Node.get_proc_name curr_node in let descr = "return from a call to " ^ Typ.Procname.to_string pname in let node_tags = [Errlog.Procedure_end pname] in trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index f1bf682eb..3ac0a3643 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -477,9 +477,9 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = do_symexec_join proc_cfg tenv wl curr_node pathset_todo | Procdesc.Node.Stmt_node _ | Procdesc.Node.Prune_node _ - | Procdesc.Node.Exit_node _ + | Procdesc.Node.Exit_node | Procdesc.Node.Skip_node _ - | Procdesc.Node.Start_node _ -> + | Procdesc.Node.Start_node -> exe_iter (do_prop curr_node handle_exn) pathset_todo in let do_node_and_handle curr_node session = diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index ab6accf72..eb00267b3 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -136,7 +136,7 @@ module BoundMap = struct let compute_node_upper_bound bound_map node = let node_id = NodeCFG.Node.id node in match Procdesc.Node.get_kind node with - | Procdesc.Node.Exit_node _ -> + | Procdesc.Node.Exit_node -> Node.IdMap.add node_id BasicCost.one bound_map | _ -> ( let exit_state_opt = diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 210fcfae4..c04de1215 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -286,10 +286,8 @@ let create_local_procdesc ?(set_objc_accessor_attr = false) trans_unit_ctx cfg t Cfg.create_proc_desc cfg proc_attributes in if defined then ( - let start_kind = Procdesc.Node.Start_node proc_name in - let start_node = Procdesc.create_node procdesc loc_start start_kind [] in - let exit_kind = Procdesc.Node.Exit_node proc_name in - let exit_node = Procdesc.create_node procdesc loc_exit exit_kind [] in + let start_node = Procdesc.create_node procdesc loc_start Procdesc.Node.Start_node [] in + let exit_node = Procdesc.create_node procdesc loc_exit Procdesc.Node.Exit_node [] in Procdesc.set_start_node procdesc start_node ; Procdesc.set_exit_node procdesc exit_node ) in diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index f24db28a2..d9cd05e1c 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -313,11 +313,10 @@ let create_callee_attributes tenv program cn ms procname = Option.bind ~f (JClasspath.lookup_node cn program) -let create_empty_cfg proc_name source_file procdesc = - let start_kind = Procdesc.Node.Start_node proc_name in - let start_node = Procdesc.create_node procdesc (Location.none source_file) start_kind [] in - let exit_kind = Procdesc.Node.Exit_node proc_name in - let exit_node = Procdesc.create_node procdesc (Location.none source_file) exit_kind [] in +let create_empty_cfg source_file procdesc = + let location = Location.none source_file in + let start_node = Procdesc.create_node procdesc location Procdesc.Node.Start_node [] in + let exit_node = Procdesc.create_node procdesc location Procdesc.Node.Exit_node [] in Procdesc.node_set_succs_exn procdesc start_node [exit_node] [exit_node] ; Procdesc.set_start_node procdesc start_node ; Procdesc.set_exit_node procdesc exit_node ; @@ -346,7 +345,7 @@ let create_am_procdesc source_file program icfg am proc_name : Procdesc.t = in Cfg.create_proc_desc icfg.JContext.cfg proc_attributes in - create_empty_cfg proc_name source_file procdesc + create_empty_cfg source_file procdesc let create_native_procdesc source_file program icfg cm proc_name = @@ -370,7 +369,7 @@ let create_native_procdesc source_file program icfg cm proc_name = in Cfg.create_proc_desc icfg.JContext.cfg proc_attributes in - create_empty_cfg proc_name source_file procdesc + create_empty_cfg source_file procdesc let create_empty_procdesc source_file program linereader icfg cm proc_name = @@ -397,7 +396,7 @@ let create_empty_procdesc source_file program linereader icfg cm proc_name = ; ret_type= JTransType.return_type program tenv ms } in let proc_desc = Cfg.create_proc_desc icfg.JContext.cfg proc_attributes in - create_empty_cfg proc_name source_file proc_desc + create_empty_cfg source_file proc_desc (** Creates a procedure description. *) @@ -436,10 +435,8 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name = ; ret_type= JTransType.return_type program tenv ms } in let procdesc = Cfg.create_proc_desc cfg proc_attributes in - let start_kind = Procdesc.Node.Start_node proc_name in - let start_node = Procdesc.create_node procdesc loc_start start_kind [] in - let exit_kind = Procdesc.Node.Exit_node proc_name in - let exit_node = Procdesc.create_node procdesc loc_exit exit_kind [] in + let start_node = Procdesc.create_node procdesc loc_start Procdesc.Node.Start_node [] in + let exit_node = Procdesc.create_node procdesc loc_exit Procdesc.Node.Exit_node [] in let exn_kind = Procdesc.Node.exn_sink_kind in let exn_node = Procdesc.create_node procdesc loc_exit exn_kind [] in JContext.add_exn_node proc_name exn_node ; diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 261f4e2d9..19fe1d0ef 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -158,7 +158,6 @@ struct let pdesc = Cfg.create_proc_desc cfg (ProcAttributes.default (SourceFile.invalid __FILE__) test_pname) in - let pname = Procdesc.get_proc_name pdesc in let create_node kind cmds = Procdesc.create_node pdesc dummy_loc kind cmds in let set_succs cur_node succs ~exn_handlers = Procdesc.node_set_succs_exn pdesc cur_node succs exn_handlers @@ -228,13 +227,13 @@ struct ~f:(fun acc instr -> structured_instr_to_node acc exn_handlers instr) ~init:(last_node, assert_map) instrs in - let start_node = create_node (Procdesc.Node.Start_node pname) [] in + let start_node = create_node Procdesc.Node.Start_node [] in 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 (Procdesc.Node.Exit_node pname) [] in + let exit_node = create_node Procdesc.Node.Exit_node [] in set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers ; Procdesc.set_exit_node pdesc exit_node ; (pdesc, assert_map)