From 73c5dfdfa486fd0fc9759895a087537224af72cb Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Tue, 1 Nov 2016 00:57:53 -0700 Subject: [PATCH] [IR] Remove use of Cfg.Node.get_proc_desc Reviewed By: jvillard Differential Revision: D4095234 fbshipit-source-id: 20f7077 --- infer/src/IR/Cfg.re | 34 +++--- infer/src/IR/Cfg.rei | 8 +- infer/src/backend/buckets.ml | 5 +- infer/src/backend/interproc.ml | 152 ++++++++++++------------- infer/src/backend/paths.ml | 2 +- infer/src/backend/printer.ml | 30 +++-- infer/src/backend/printer.mli | 2 +- infer/src/backend/prover.ml | 43 +++---- infer/src/backend/symExec.ml | 3 +- infer/src/backend/symExec.mli | 3 +- infer/src/checkers/checkers.ml | 11 +- infer/src/checkers/dataflow.ml | 5 +- infer/src/clang/cFrontend_decl.ml | 5 +- infer/src/clang/cTrans.ml | 56 +++++---- infer/src/clang/cTrans_utils.ml | 20 ++-- infer/src/clang/cTrans_utils.mli | 2 +- infer/src/eradicate/eradicate.ml | 4 +- infer/src/eradicate/eradicateChecks.ml | 61 ++++------ infer/src/eradicate/typeCheck.ml | 34 +++--- infer/src/eradicate/typeErr.ml | 15 +-- infer/src/eradicate/typeErr.mli | 6 +- infer/src/harness/inhabit.ml | 6 +- infer/src/java/jFrontend.ml | 8 +- infer/src/java/jTrans.ml | 4 +- infer/src/java/jTransExn.ml | 6 +- infer/src/unit/analyzerTester.ml | 2 +- infer/src/unit/procCfgTests.ml | 6 +- 27 files changed, 267 insertions(+), 266 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 5a11ace11..16e203941 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -26,9 +26,10 @@ let module Node = { | Stmt_node string | Join_node | Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ - | Skip_node string + | Skip_node string; + /** a node */ - and t = { + type t = { /** unique id of the node */ nd_id: id, /** distance to the exit node */ @@ -43,13 +44,14 @@ let module Node = { nd_loc: Location.t, /** predecessor nodes in the cfg */ mutable nd_preds: list t, - /** proc desc from cil */ - nd_proc: option proc_desc, + /** name of the procedure the node belongs to */ + nd_pname: option Procname.t, /** successor nodes in the cfg */ mutable nd_succs: list t - } + }; + /** procedure description */ - and proc_desc = { + 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 */ @@ -145,7 +147,7 @@ let module Node = { nd_instrs: [], nd_kind: Skip_node "dummy", nd_loc: Location.dummy, - nd_proc: None, + nd_pname: None, nd_succs: [], nd_preds: [], nd_exn: [] @@ -165,7 +167,7 @@ let module Node = { nd_kind: kind, nd_loc: loc, nd_preds: [], - nd_proc: Some pdesc, + nd_pname: Some pdesc.pd_attributes.proc_name, nd_succs: [], nd_exn: [] }; @@ -226,13 +228,13 @@ let module Node = { }; let get_exn node => node.nd_exn; - /** Get the proc desc of the node */ - let get_proc_desc node => - switch node.nd_proc { + /** Get the name of the procedure the node belongs to */ + let get_proc_name node => + switch node.nd_pname { | None => L.out "node_get_proc_desc: at node %d@\n" node.nd_id; assert false - | Some proc_desc => proc_desc + | Some proc_name => proc_name }; /** Set the successor nodes and exception nodes, and build predecessor links */ @@ -245,11 +247,10 @@ let module Node = { /** 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 node succs exn => + 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 pdesc = get_proc_desc node; 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 @@ -355,9 +356,8 @@ let module Node = { Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name; /** Add declarations for local variables and return variable to the node */ - let add_locals_ret_declaration node locals => { + let add_locals_ret_declaration pdesc node locals => { let loc = get_loc node; - let pdesc = get_proc_desc node; let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name; let ret_var = { let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type; @@ -712,7 +712,7 @@ let module Node = { if (equal node callee_exit_node) { proc_desc_set_exit_node resolved_proc_desc new_node }; - set_succs_exn new_node (loop successors) (loop exn_nodes); + set_succs_exn callee_proc_desc new_node (loop successors) (loop exn_nodes); new_node }; [converted_node, ...loop other_node] diff --git a/infer/src/IR/Cfg.rei b/infer/src/IR/Cfg.rei index 79106a75b..1f1a049a8 100644 --- a/infer/src/IR/Cfg.rei +++ b/infer/src/IR/Cfg.rei @@ -161,7 +161,7 @@ let module Node: { let prepend_instrs: t => list Sil.instr => unit; /** Add declarations for local variables and return variable to the node */ - let add_locals_ret_declaration: t => list (Mangled.t, Typ.t) => unit; + let add_locals_ret_declaration: Procdesc.t => t => list (Mangled.t, Typ.t) => unit; /** Compare two nodes */ let compare: t => t => int; @@ -213,8 +213,8 @@ let module Node: { from a node with subsequent applications of a generator function */ let get_generated_slope: t => (t => list t) => list t; - /** Get the proc desc associated to the node */ - let get_proc_desc: t => Procdesc.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; @@ -249,7 +249,7 @@ let module Node: { let replace_instrs: t => list Sil.instr => unit; /** Set the successor nodes and exception nodes, and build predecessor links */ - let set_succs_exn: t => list t => list t => unit; + let set_succs_exn: Procdesc.t => t => list t => list t => unit; }; diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index 61d1d621a..c670e595f 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -55,7 +55,10 @@ let check_access access_opt de_opt = let find_bucket line_number null_case_flag = let find_formal_ids node = (* find ids obtained by a letref on a formal parameter *) let node_instrs = Cfg.Node.get_instrs node in - let formals = Cfg.Procdesc.get_formals (Cfg.Node.get_proc_desc node) in + let formals = match State.get_prop_tenv_pdesc () with + | None -> [] + | Some (_, _, pdesc) -> + Cfg.Procdesc.get_formals pdesc in let formal_names = IList.map fst formals in let is_formal pvar = let name = Pvar.get_name pvar in diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 117df45bd..6aeabcd93 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -297,13 +297,11 @@ let propagate_nodes_divergence (** Symbolic execution for a Join node *) let do_symexec_join pname tenv wl curr_node (edgeset_todo : Paths.PathSet.t) = - let curr_pdesc = Cfg.Node.get_proc_desc curr_node in - let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let curr_node_id = Cfg.Node.get_id curr_node in let succ_nodes = Cfg.Node.get_succs curr_node in let new_dset = edgeset_todo in let old_dset = Join_table.find wl.Worklist.join_table curr_node_id in - let old_dset', new_dset' = Dom.pathset_join curr_pname tenv old_dset new_dset in + let old_dset', new_dset' = Dom.pathset_join pname tenv old_dset new_dset in Join_table.add wl.Worklist.join_table curr_node_id (Paths.PathSet.union old_dset' new_dset'); IList.iter (fun node -> Paths.PathSet.iter (fun prop path -> @@ -334,14 +332,12 @@ let reset_prop_metrics () = exception RE_EXE_ERROR -let do_before_node source session node = +let do_before_node pname source session node = let loc = Cfg.Node.get_loc node in - let proc_desc = Cfg.Node.get_proc_desc node in - let proc_name = Cfg.Procdesc.get_proc_name proc_desc in State.set_node node; State.set_session session; L.reset_delayed_prints (); - Printer.node_start_session node loc proc_name (session :> int) source + Printer.node_start_session node loc pname (session :> int) source let do_after_node source node = Printer.node_finish_session node source @@ -363,8 +359,7 @@ let instrs_get_normal_vars instrs = (* which they prune is the variable (or the negation) which was set in the set instruction *) (* we exclude function calls: if (g(x,y)) ....*) (* we check that prune nodes have simple guards: a var or its negation*) -let check_assignement_guard node = - let pdesc = Cfg.Node.get_proc_desc node in +let check_assignement_guard pdesc node = let pname = Cfg.Procdesc.get_proc_name pdesc in let verbose = false in let node_contains_call n = @@ -467,17 +462,17 @@ let check_assignement_guard node = ) else () (** Perform symbolic execution for a node starting from an initial prop *) -let do_symbolic_execution handle_exn tenv +let do_symbolic_execution pdesc handle_exn tenv (node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) = - let pdesc = Cfg.Node.get_proc_desc node in State.mark_execution_start node; (* build the const map lazily *) State.set_const_map (ConstantPropagation.build_const_map tenv pdesc); - check_assignement_guard node; + check_assignement_guard pdesc node; let instrs = Cfg.Node.get_instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) Ident.update_name_generator (instrs_get_normal_vars instrs); - let pset = SymExec.node handle_exn tenv node (Paths.PathSet.from_renamed_list [(prop, path)]) in + let pset = + SymExec.node handle_exn tenv pdesc node (Paths.PathSet.from_renamed_list [(prop, path)]) in L.d_strln ".... After Symbolic Execution ...."; Propset.d prop (Paths.PathSet.to_propset tenv pset); L.d_ln (); L.d_ln(); @@ -508,20 +503,19 @@ let add_taint_attrs tenv proc_name proc_desc prop = Taint.add_tainting_attribute tenv attr param prop_acc) prop -let forward_tabulate tenv wl source = +let forward_tabulate tenv pdesc wl source = + let pname = Cfg.Procdesc.get_proc_name pdesc in let handle_exn_node curr_node exn = - let curr_pdesc = Cfg.Node.get_proc_desc curr_node in - let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in Exceptions.print_exception_html "Failure of symbolic execution: " exn; let pre_opt = (* precondition leading to error, if any *) - State.get_normalized_pre (Abs.abstract_no_symop curr_pname) in + State.get_normalized_pre (Abs.abstract_no_symop pname) in (match pre_opt with | Some pre -> L.d_strln "Precondition:"; Prop.d_prop pre; L.d_ln () | None -> ()); L.d_strln "SIL INSTR:"; Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node; L.d_ln (); - Reporting.log_error curr_pname exn; + Reporting.log_error pname exn; State.mark_instr_fail exn in let exe_iter f pathset = @@ -533,16 +527,16 @@ let forward_tabulate tenv wl source = f prop path !cnt ps_size in Paths.PathSet.iter exe pathset in - let print_node_preamble curr_node proc_name session pathset_todo = + let print_node_preamble curr_node session pathset_todo = let log_string proc_name = let phase_string = if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE" in let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in let timestamp = Specs.get_timestamp summary in F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in - L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^ + L.d_strln ("**** " ^ (log_string pname) ^ " " ^ "Node: " ^ string_of_int (Cfg.Node.get_id curr_node :> int) ^ ", " ^ - "Procedure: " ^ Procname.to_string proc_name ^ ", " ^ + "Procedure: " ^ Procname.to_string pname ^ ", " ^ "Session: " ^ string_of_int session ^ ", " ^ "Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****"); L.d_increase_indent 1; @@ -551,10 +545,10 @@ let forward_tabulate tenv wl source = Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node; L.d_ln (); L.d_ln () in - let do_prop curr_node proc_desc proc_name handle_exn prop_ path cnt num_paths = + let do_prop curr_node handle_exn prop_ path cnt num_paths = let prop = if Config.taint_analysis - then add_taint_attrs tenv proc_name proc_desc prop_ + then add_taint_attrs tenv pname pdesc prop_ else prop_ in L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths); @@ -562,31 +556,31 @@ let forward_tabulate tenv wl source = try State.reset_diverging_states_node (); let pset = - do_symbolic_execution handle_exn tenv curr_node prop path in + do_symbolic_execution pdesc handle_exn tenv curr_node prop path in let succ_nodes = Cfg.Node.get_succs curr_node in let exn_nodes = Cfg.Node.get_exn curr_node in - propagate_nodes_divergence tenv proc_desc pset succ_nodes exn_nodes wl; + propagate_nodes_divergence tenv pdesc pset succ_nodes exn_nodes wl; L.d_decrease_indent 1; L.d_ln(); with | exn when Exceptions.handle_exception exn && !Config.footprint -> handle_exn exn; L.d_decrease_indent 1; L.d_ln () in - let do_node curr_node proc_desc proc_name pathset_todo session handle_exn = + let do_node curr_node pathset_todo session handle_exn = check_prop_size pathset_todo; - print_node_preamble curr_node proc_name session pathset_todo; + print_node_preamble curr_node session pathset_todo; match Cfg.Node.get_kind curr_node with | Cfg.Node.Join_node -> - do_symexec_join proc_name tenv wl curr_node pathset_todo + do_symexec_join pname tenv wl curr_node pathset_todo | Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _ | Cfg.Node.Exit_node _ | Cfg.Node.Skip_node _ | Cfg.Node.Start_node _ -> - exe_iter (do_prop curr_node proc_desc proc_name handle_exn) pathset_todo in + exe_iter (do_prop curr_node handle_exn) pathset_todo in - let do_node_and_handle curr_node proc_desc proc_name session = + let do_node_and_handle curr_node session = let pathset_todo = path_set_checkout_todo wl curr_node in try begin @@ -594,7 +588,7 @@ let forward_tabulate tenv wl source = let handle_exn exn = handle_exn_called := true; handle_exn_node curr_node exn in - do_node curr_node proc_desc proc_name pathset_todo session handle_exn; + do_node curr_node pathset_todo session handle_exn; if !handle_exn_called then Printer.force_delayed_prints (); do_after_node source curr_node end @@ -607,15 +601,13 @@ let forward_tabulate tenv wl source = while not (Worklist.is_empty wl) do let curr_node = Worklist.remove wl in - let proc_desc = Cfg.Node.get_proc_desc curr_node in - let proc_name = Cfg.Procdesc.get_proc_name proc_desc in - let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in + let summary = Specs.get_summary_unsafe "forward_tabulate" pname in mark_visited summary curr_node; (* mark nodes visited in fp and re phases *) let session = incr summary.Specs.sessions; !(summary.Specs.sessions) in - do_before_node source session curr_node; - do_node_and_handle curr_node proc_desc proc_name session + do_before_node pname source session curr_node; + do_node_and_handle curr_node session done; L.d_strln ".... Work list empty. Stop ...."; L.d_ln () @@ -915,9 +907,9 @@ let initial_prop_from_pre tenv curr_f pre = (** Re-execute one precondition and return some spec if there was no re-execution error. *) let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t) source : Prop.normal Specs.spec option = - let proc_name = Cfg.Procdesc.get_proc_name pdesc in - do_before_node source 0 init_node; - L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string proc_name ^ " ####"); + let pname = Cfg.Procdesc.get_proc_name pdesc in + do_before_node pname source 0 init_node; + L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string pname ^ " ####"); L.d_indent 1; L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition; L.d_ln (); L.d_ln (); @@ -932,10 +924,10 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec try Worklist.add wl init_node; ignore (path_set_put_todo wl init_node init_edgeset); - forward_tabulate tenv wl source; - do_before_node source 0 init_node; + forward_tabulate tenv pdesc wl source; + do_before_node pname source 0 init_node; L.d_strln_color Green - ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####"); + ("#### Finished: RE-execution for " ^ Procname.to_string pname ^ " ####"); L.d_increase_indent 1; L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition); L.d_ln (); @@ -956,9 +948,9 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec do_after_node source init_node; Some spec with RE_EXE_ERROR -> - do_before_node source 0 init_node; + do_before_node pname source 0 init_node; Printer.force_delayed_prints (); - L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string proc_name ^ "] ...ERROR"); + L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string pname ^ "] ...ERROR"); L.d_increase_indent 1; L.d_strln "when starting from pre:"; Prop.d_prop (Specs.Jprop.to_prop precondition); @@ -986,13 +978,15 @@ let pp_intra_stats wl proc_desc fmt _ = nodes; F.fprintf fmt "(%d nodes containing %d states)" (IList.length nodes) !nstates +type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) + (** Return functions to perform one phase of the analysis for a procedure. Given [proc_name], return [do, get_results] where [go ()] performs the analysis phase and [get_results ()] returns the results computed. This function is architected so that [get_results ()] can be called even after [go ()] was interrupted by and exception. *) let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) source - : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = + : exe_phase = let start_node = Cfg.Procdesc.get_start_node pdesc in let check_recursion_level () = @@ -1004,7 +998,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level)) end in - let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = + let compute_footprint () : exe_phase = let go (wl : Worklist.t) () = let init_prop = initial_prop_from_emp tenv pdesc in (* use existing pre's (in recursion some might exist) as starting points *) @@ -1031,7 +1025,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so (Cfg.Procdesc.get_flags pdesc) Mleak_buckets.objc_arc_flag; ignore (path_set_put_todo wl start_node init_edgeset); - forward_tabulate tenv wl source in + forward_tabulate tenv pdesc wl source in let get_results (wl : Worklist.t) () = State.process_execution_failures Reporting.log_warning pname; let results = collect_analysis_result tenv wl pdesc in @@ -1053,15 +1047,14 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so let wl = path_set_create_worklist pdesc in go wl, get_results wl in - let re_execution proc_name - : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = + let re_execution () : exe_phase = let candidate_preconditions = IList.map (fun spec -> spec.Specs.pre) - (Specs.get_specs proc_name) in + (Specs.get_specs pname) in let valid_specs = ref [] in let go () = - L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp proc_name; + L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp pname; check_recursion_level (); let filter p = let wl = path_set_create_worklist pdesc in @@ -1074,7 +1067,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so let outcome = if is_valid then "pass" else "fail" in L.out "Finished re-execution for precondition %d %a (%s)@." (Specs.Jprop.to_number p) - (pp_intra_stats wl pdesc) proc_name + (pp_intra_stats wl pdesc) pname outcome; speco in if Config.undo_join then @@ -1083,22 +1076,22 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so ignore (IList.map filter candidate_preconditions) in let get_results () = let specs = !valid_specs in - L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp proc_name; - L.out "#### Finished: Re-Execution for %a ####@." Procname.pp proc_name; + L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname; + L.out "#### Finished: Re-Execution for %a ####@." Procname.pp pname; let valid_preconditions = IList.map (fun spec -> spec.Specs.pre) specs in let filename = DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) - [(Procname.to_filename proc_name)] in + [(Procname.to_filename pname)] in if Config.write_dotty then Dotty.pp_speclist_dotty_file filename specs; L.out "@.@.================================================"; - L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp proc_name; + L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp pname; L.out "@.================================================@."; L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text false) candidate_preconditions; L.out "@.@.================================================"; - L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp proc_name; + L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp pname; L.out "@.================================================@."; L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text true) valid_preconditions; specs, Specs.RE_EXECUTION in @@ -1106,9 +1099,9 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so match Specs.get_phase pname with | Specs.FOOTPRINT -> - compute_footprint + compute_footprint () | Specs.RE_EXECUTION -> - re_execution pname + re_execution () let set_current_language proc_desc = let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in @@ -1385,7 +1378,7 @@ let perform_transition exe_env tenv proc_name source = f start_node | None -> () with exn when SymOp.exn_not_failure exn -> () in - apply_start_node (do_before_node source 0); + apply_start_node (do_before_node proc_name source 0); try Config.allow_leak := true; let res = collect_preconditions tenv proc_name in @@ -1511,23 +1504,26 @@ let do_analysis exe_env = Ondemand.unset_callbacks () -let visited_and_total_nodes cfg = - let all_nodes = - let set = ref Cfg.NodeSet.empty in - let add _ n = set := Cfg.NodeSet.add n !set in - Cfg.iter_all_nodes add cfg; - !set in - let filter_node n = - Cfg.Procdesc.is_defined (Cfg.Node.get_proc_desc n) && +let visited_and_total_nodes ~filter cfg = + let filter_node pdesc n = + Cfg.Procdesc.is_defined pdesc && + filter pdesc && match Cfg.Node.get_kind n with | Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _ | Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ -> true | Cfg.Node.Skip_node _ | Cfg.Node.Join_node -> false in - let counted_nodes = Cfg.NodeSet.filter filter_node all_nodes in - let visited_nodes_re = - Cfg.NodeSet.filter - (fun node -> snd (Printer.node_is_visited node)) - counted_nodes in + let counted_nodes, visited_nodes_re = + let set = ref Cfg.NodeSet.empty in + let set_visited_re = ref Cfg.NodeSet.empty in + let add pdesc n = + if filter_node pdesc n then + begin + set := Cfg.NodeSet.add n !set; + if snd (Printer.node_is_visited (Cfg.Procdesc.get_proc_name pdesc) n) + then set_visited_re := Cfg.NodeSet.add n !set_visited_re + end in + Cfg.iter_all_nodes add cfg; + !set, !set_visited_re in Cfg.NodeSet.elements visited_nodes_re, Cfg.NodeSet.elements counted_nodes (** Print the stats for the given cfg. @@ -1535,12 +1531,10 @@ let visited_and_total_nodes cfg = was defined in another module, and was the one which was analyzed *) let print_stats_cfg proc_shadowed source cfg = let err_table = Errlog.create_err_table () in - let nvisited, ntotal = visited_and_total_nodes cfg in - let node_filter n = - let node_procname = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc n) in - Specs.summary_exists node_procname && Specs.get_specs node_procname != [] in - let nodes_visited = IList.filter node_filter nvisited in - let nodes_total = IList.filter node_filter ntotal in + let filter pdesc = + let pname = Cfg.Procdesc.get_proc_name pdesc in + Specs.summary_exists pname && Specs.get_specs pname != [] in + let nodes_visited, nodes_total = visited_and_total_nodes ~filter cfg in let num_proc = ref 0 in let num_nospec_noerror_proc = ref 0 in let num_spec_noerror_proc = ref 0 in diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index ce5697e01..48711d5fe 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -271,7 +271,7 @@ end = struct Invariant.reset_stats path let get_path_pos node = - let pn = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc node) in + let pn = Cfg.Node.get_proc_name node in let n_id = Cfg.Node.get_id node in (pn, (n_id :> int)) diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 09256f28d..593a0d2ae 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -77,9 +77,7 @@ end let curr_html_formatter = ref F.std_formatter (** Return true if the node was visited during footprint and during re-execution*) -let node_is_visited node = - let proc_desc = Cfg.Node.get_proc_desc node in - let proc_name = Cfg.Procdesc.get_proc_name proc_desc in +let node_is_visited proc_name node = match Specs.get_summary proc_name with | None -> false, false @@ -92,8 +90,8 @@ let node_is_visited node = is_visited_fp, is_visited_re (** Return true if the node was visited during analysis *) -let is_visited node = - let visited_fp, visited_re = node_is_visited node in +let is_visited proc_name node = + let visited_fp, visited_re = node_is_visited proc_name node in visited_fp || visited_re (* =============== START of module NodesHtml =============== *) @@ -137,21 +135,21 @@ end = struct (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) - (is_visited node) false fmt (Cfg.Node.get_id node :> int)) preds; + (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) preds; F.fprintf fmt "
SUCCS: @\n"; IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) - (is_visited node) false fmt (Cfg.Node.get_id node :> int)) succs; + (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) succs; F.fprintf fmt "
EXN: @\n"; IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) - (is_visited node) false fmt (Cfg.Node.get_id node :> int)) exns; + (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) exns; F.fprintf fmt "
@\n"; F.pp_print_flush fmt (); true @@ -422,7 +420,7 @@ let write_proc_html source whole_seconds pdesc = (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) - (is_visited n) false fmt (Cfg.Node.get_id n :> int)) + (is_visited pname n) false fmt (Cfg.Node.get_id n :> int)) nodes; (match Specs.get_summary pname with | None -> @@ -454,12 +452,12 @@ let create_err_message err_string = let write_html_proc source proof_cover table_nodes_at_linenum global_err_log proc_desc = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in - let process_node nodes_tbl n = + let process_node n = let lnum = (Cfg.Node.get_loc n).Location.line in let curr_nodes = - try Hashtbl.find nodes_tbl lnum + try Hashtbl.find table_nodes_at_linenum lnum with Not_found -> [] in - Hashtbl.replace nodes_tbl lnum (n:: curr_nodes) in + Hashtbl.replace table_nodes_at_linenum lnum ((n, proc_desc) :: curr_nodes) in let proc_loc = Cfg.Procdesc.get_loc proc_desc in let process_proc = Cfg.Procdesc.is_defined proc_desc && @@ -470,7 +468,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro DB.source_file_equal source_captured (Cfg.Procdesc.get_loc proc_desc).file in if process_proc then begin - IList.iter (process_node table_nodes_at_linenum) (Cfg.Procdesc.get_nodes proc_desc); + IList.iter process_node (Cfg.Procdesc.get_nodes proc_desc); match Specs.get_summary proc_name with | None -> () @@ -522,7 +520,7 @@ let write_html_file linereader filename procs = line_html in F.fprintf fmt "%s" str; IList.iter - (fun n -> + (fun (n, pdesc) -> let isproof = Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in Io_infer.Html.pp_node_link @@ -531,13 +529,13 @@ let write_html_file linereader filename procs = (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) - (is_visited n) + (is_visited (Cfg.Procdesc.get_proc_name pdesc) n) isproof fmt (Cfg.Node.get_id n :> int)) nodes_at_linenum; IList.iter - (fun n -> + (fun (n, _) -> match Cfg.Node.get_kind n with | Cfg.Node.Start_node proc_name -> let num_specs = IList.length (Specs.get_specs proc_name) in diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index aa6a36981..d1090588f 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -40,7 +40,7 @@ val force_delayed_prints : unit -> unit val node_finish_session : Cfg.node -> DB.source_file -> unit (** Return true if the node was visited during footprint and during re-execution *) -val node_is_visited : Cfg.Node.t -> bool * bool +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 diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 47c6c34d3..42d33d784 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -857,27 +857,28 @@ let check_inconsistency_base tenv prop = let inconsistent_ptsto _ = check_allocatedness tenv prop Exp.zero in let inconsistent_this_self_var () = - let procdesc = - Cfg.Node.get_proc_desc (State.get_node ()) in - let procedure_attr = - Cfg.Procdesc.get_attributes procdesc in - let is_java_this pvar = - procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in - let is_objc_instance_self pvar = - procedure_attr.ProcAttributes.language = Config.Clang && - Pvar.get_name pvar = Mangled.from_string "self" && - procedure_attr.ProcAttributes.is_objc_instance_method in - let is_cpp_this pvar = - procedure_attr.ProcAttributes.language = Config.Clang && - Pvar.is_this pvar && - procedure_attr.ProcAttributes.is_cpp_instance_method in - let do_hpred = function - | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) -> - Exp.equal e Exp.zero && - Pvar.is_seed pv && - (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv) - | _ -> false in - IList.exists do_hpred sigma in + match State.get_prop_tenv_pdesc () with + | None -> false + | Some (_, _, pdesc) -> + let procedure_attr = + Cfg.Procdesc.get_attributes pdesc in + let is_java_this pvar = + procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in + let is_objc_instance_self pvar = + procedure_attr.ProcAttributes.language = Config.Clang && + Pvar.get_name pvar = Mangled.from_string "self" && + procedure_attr.ProcAttributes.is_objc_instance_method in + let is_cpp_this pvar = + procedure_attr.ProcAttributes.language = Config.Clang && + Pvar.is_this pvar && + procedure_attr.ProcAttributes.is_cpp_instance_method in + let do_hpred = function + | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) -> + Exp.equal e Exp.zero && + Pvar.is_seed pv && + (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv) + | _ -> false in + IList.exists do_hpred sigma in let inconsistent_atom = function | Sil.Aeq (e1, e2) -> (match e1, e2 with diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 27d530929..9697ee2db 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1657,8 +1657,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa (** {2 Lifted Abstract Transfer Functions} *) -let node handle_exn tenv node (pset : Paths.PathSet.t) : Paths.PathSet.t = - let pdesc = Cfg.Node.get_proc_desc node in +let node handle_exn tenv pdesc node (pset : Paths.PathSet.t) : Paths.PathSet.t = let pname = Cfg.Procdesc.get_proc_name pdesc in let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) = let pset2 = diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index e8e6757ad..e3f91db99 100644 --- a/infer/src/backend/symExec.mli +++ b/infer/src/backend/symExec.mli @@ -13,7 +13,8 @@ open! Utils (** Symbolic Execution *) (** Symbolic execution of the instructions of a node, lifted to sets of propositions. *) -val node : (exn -> unit) -> Tenv.t -> Cfg.Node.t -> Paths.PathSet.t -> Paths.PathSet.t +val node : + (exn -> unit) -> Tenv.t -> Cfg.Procdesc.t -> Cfg.Node.t -> Paths.PathSet.t -> Paths.PathSet.t (** Symbolic execution of a sequence of instructions. If errors occur and [mask_errors] is true, just treat as skip. *) diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index a75f5c081..b095aef88 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -159,8 +159,7 @@ module ST = struct end end -let report_calls_and_accesses tenv callback node instr = - let proc_desc = Cfg.Node.get_proc_desc node in +let report_calls_and_accesses tenv callback proc_desc instr = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in let callee = Procname.to_string proc_name in match PatternMatch.get_java_field_access_signature instr with @@ -184,7 +183,9 @@ let report_calls_and_accesses tenv callback node instr = (** Report all field accesses and method calls of a procedure. *) let callback_check_access { Callbacks.tenv; proc_desc } = - Cfg.Procdesc.iter_instrs (report_calls_and_accesses tenv "PROC") proc_desc + Cfg.Procdesc.iter_instrs + (fun _ instr -> report_calls_and_accesses tenv "PROC" proc_desc instr) + proc_desc (** Report all field accesses and method calls of a class. *) let callback_check_cluster_access exe_env all_procs get_proc_desc _ = @@ -192,7 +193,9 @@ let callback_check_cluster_access exe_env all_procs get_proc_desc _ = match get_proc_desc proc_name with | Some proc_desc -> let tenv = Exe_env.get_tenv exe_env proc_name in - Cfg.Procdesc.iter_instrs (report_calls_and_accesses tenv "CLUSTER") proc_desc + Cfg.Procdesc.iter_instrs + (fun _ instr -> report_calls_and_accesses tenv "CLUSTER" proc_desc instr) + proc_desc | _ -> () ) all_procs diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 8fc0e6b0b..f6c9d4037 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -47,10 +47,9 @@ module type DF = sig end (** Determine if the node can throw an exception. *) -let node_throws node (proc_throws : Procname.t -> throws) : throws = +let node_throws pdesc node (proc_throws : Procname.t -> throws) : throws = let instr_throws instr = let is_return pvar = - let pdesc = Cfg.Node.get_proc_desc node in let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in Pvar.equal pvar ret_pvar in match instr with @@ -157,7 +156,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct try let state = H.find t.pre_states node in let states_succ, states_exn = St.do_node tenv node state in - propagate t node states_succ states_exn (node_throws node St.proc_throws) + propagate t node states_succ states_exn (node_throws proc_desc node St.proc_throws) with Not_found -> () done in diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index b6975d9d6..b9e371faa 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -38,8 +38,9 @@ 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 - Cfg.Node.add_locals_ret_declaration start_node (Cfg.Procdesc.get_locals procdesc); - Cfg.Node.set_succs_exn start_node meth_body_nodes []; + 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 []; Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc)) | None -> ()) with diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 4ac0b7390..b09109b78 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -591,15 +591,16 @@ struct this_expr_trans trans_state sil_loc expr_info.Clang_ast_t.ei_type_ptr let rec labelStmt_trans trans_state stmt_info stmt_list label_name = + let context = trans_state.context in (* go ahead with the translation *) let res_trans = match stmt_list with | [stmt] -> instruction trans_state stmt | _ -> assert false (* expected a stmt or at most a compoundstmt *) in (* create the label root node into the hashtbl *) - let sil_loc = CLocation.get_sil_location stmt_info trans_state.context in + 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 root_node' res_trans.root_nodes []; + Cfg.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) = @@ -723,7 +724,8 @@ struct { empty_res_trans with exps = [(const_exp, typ)] } and arraySubscriptExpr_trans trans_state expr_info stmt_list = - let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in + let context = trans_state.context in + let typ = CTypes_decl.get_type_from_expr_info expr_info context.tenv in let array_stmt, idx_stmt = (match stmt_list with | [a; i] -> a, i (* Assumption: the statement list contains 2 elements, the first is the array expr and the second the index *) @@ -748,7 +750,7 @@ struct if res_trans_idx.root_nodes <> [] then IList.iter - (fun n -> Cfg.Node.set_succs_exn n res_trans_idx.root_nodes []) + (fun n -> Cfg.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. *) @@ -1129,7 +1131,9 @@ struct "ConditinalStmt Branch" stmt_info all_res_trans in 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 n res_trans.root_nodes []) prune_nodes' in + IList.iter + (fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans.root_nodes []) + prune_nodes' in (match stmt_list with | [cond; exp1; exp2] -> let typ = @@ -1137,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 join_node succ_nodes []; + Cfg.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 @@ -1210,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 n' [prune_t; prune_f] []) + (fun n' -> Cfg.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] @@ -1243,7 +1247,7 @@ struct | Binop.LOr -> prune_nodes_f, prune_nodes_t | _ -> assert false) in IList.iter - (fun n -> Cfg.Node.set_succs_exn n res_trans_s2.root_nodes []) + (fun n -> Cfg.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 @@ -1284,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 join_node succ_nodes []; + Cfg.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 *) @@ -1297,7 +1301,9 @@ struct res_trans_b.root_nodes) in 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 n nodes_branch []) prune_nodes' in + IList.iter + (fun n -> Cfg.Node.set_succs_exn context.procdesc n nodes_branch []) + prune_nodes' in (match stmt_list with | [_; decl_stmt; cond; stmt1; stmt2] -> (* set the flat to inform that we are translating a condition of a if *) @@ -1333,7 +1339,7 @@ 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 n' [switch_special_cond_node] []) + (fun n' -> Cfg.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 @@ -1431,8 +1437,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 prune_node_t case_entry_point []; - Cfg.Node.set_succs_exn prune_node_f last_prune_nodes []; + 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 []; 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 @@ -1442,13 +1448,14 @@ 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 placeholder_entry_point default_entry_point []; + Cfg.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 switch_special_cond_node top_prune_nodes []; + Cfg.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; @@ -1529,9 +1536,13 @@ struct match loop_kind with | Loops.For _ | Loops.While _ -> res_trans_body.root_nodes | Loops.DoWhile _ -> [join_node] in - Cfg.Node.set_succs_exn join_node join_succ_nodes []; - IList.iter (fun n -> Cfg.Node.set_succs_exn n prune_t_succ_nodes []) prune_nodes_t; - IList.iter (fun n -> Cfg.Node.set_succs_exn n succ_nodes []) prune_nodes_f; + Cfg.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 []) + prune_nodes_t; + IList.iter + (fun n -> Cfg.Node.set_succs_exn context.procdesc n succ_nodes []) + prune_nodes_f; let root_nodes = match loop_kind with | Loops.For _ -> @@ -1880,6 +1891,7 @@ struct 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 + context.procdesc ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] []; ret_node in let trans_result = (match stmt_list with @@ -1912,7 +1924,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 n [ret_node] []) + (fun n -> Cfg.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 @@ -1999,7 +2011,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 call_node trans_state.succ_nodes []; + Cfg.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 @@ -2098,7 +2110,7 @@ struct and cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info = let context = trans_state.context in - let typ = CTypes_decl.get_type_from_expr_info expr_info context.CContext.tenv in + let typ = CTypes_decl.get_type_from_expr_info expr_info context.tenv in let sil_loc = CLocation.get_sil_location stmt_info context in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let is_dyn_array = cxx_new_expr_info.Clang_ast_t.xnei_is_array in @@ -2135,7 +2147,7 @@ struct let (var_exp, typ) = var_exp_typ in let res_trans_init_list = initListExpr_initializers_trans trans_state_init var_exp 0 stmts typ is_dyn_array stmt_info in - CTrans_utils.collect_res_trans res_trans_init_list + CTrans_utils.collect_res_trans context.procdesc res_trans_init_list else init_expr_trans trans_state_init var_exp_typ init_stmt_info stmt_opt in let all_res_trans = [res_trans_size; res_trans_new; res_trans_init] in let nname = "CXXNewExpr" in diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 3af8ef6d2..e42c2b42c 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -158,7 +158,7 @@ let empty_res_trans = { let undefined_expression () = Exp.Var (Ident.create_fresh Ident.knormal) (** Collect the results of translating a list of instructions, and link up the nodes created. *) -let collect_res_trans l = +let collect_res_trans pdesc l = let rec collect l rt = match l with | [] -> rt @@ -170,7 +170,7 @@ let collect_res_trans 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 n rt'.root_nodes []) rt.leaf_nodes; + IList.iter (fun n -> Cfg.Node.set_succs_exn pdesc n rt'.root_nodes []) rt.leaf_nodes; collect l' { root_nodes = root_nodes; leaf_nodes = leaf_nodes; @@ -238,14 +238,16 @@ struct (* deals with creating or not a cfg node depending of owning the *) (* priority_node. It returns nodes, ids, instrs that should be passed to parent *) let compute_results_to_parent trans_state loc nd_name stmt_info res_states_children = - let res_state = collect_res_trans res_states_children in + let res_state = collect_res_trans trans_state.context.procdesc res_states_children in let create_node = own_priority_node trans_state.priority stmt_info && res_state.instrs <> [] in if create_node then (* 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 node trans_state.succ_nodes []; - IList.iter (fun leaf -> Cfg.Node.set_succs_exn leaf [node] []) res_state.leaf_nodes; + Cfg.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] []) + 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 else [node]) in @@ -438,20 +440,20 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged = (Clang_ast_j.string_of_cast_kind cast_kind); ([], (exp, cast_typ)) -let trans_assertion_failure sil_loc context = +let trans_assertion_failure sil_loc (context : CContext.t) = let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in 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 failure_node [exit_node] []; + Cfg.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 succ_nodes = +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 prune_node succ_nodes []; + Cfg.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/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 8fd56a710..e2f18c495 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -44,7 +44,7 @@ val empty_res_trans: trans_result val undefined_expression: unit -> Exp.t -val collect_res_trans : trans_result list -> trans_result +val collect_res_trans : Cfg.Procdesc.t -> trans_result list -> trans_result val extract_var_exp_or_fail : trans_state -> Exp.t * Typ.t diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 8ff3de3ea..c82687588 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -97,7 +97,7 @@ struct checks.TypeCheck.check_ret_type; if checks.TypeCheck.eradicate then EradicateChecks.check_return_annotation tenv - find_canonical_duplicate curr_pname exit_node ret_range + find_canonical_duplicate curr_pdesc ret_range ret_ia ret_implicitly_nullable loc in let do_before_dataflow initial_typestate = @@ -326,7 +326,7 @@ struct tenv curr_pname curr_pdesc annotated_signature; - TypeErr.report_forall_checks_and_reset tenv (Checkers.ST.report_error tenv) curr_pname; + TypeErr.report_forall_checks_and_reset tenv (Checkers.ST.report_error tenv) curr_pdesc; update_summary curr_pname curr_pdesc final_typestate_opt (** Entry point for the eradicate-based checker infrastructure. *) diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index 6835c0bed..e1c09ab1f 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -67,7 +67,6 @@ let check_field_access tenv let origin_descr = TypeAnnotation.descr_origin tenv ta in report_error tenv find_canonical_duplicate - node (TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false)) (Some instr_ref) loc curr_pname @@ -87,7 +86,6 @@ let check_array_access tenv let origin_descr = TypeAnnotation.descr_origin tenv ta in report_error tenv find_canonical_duplicate - node (TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed)) (Some instr_ref) loc @@ -103,7 +101,7 @@ type from_call = | From_containsKey (** x.containsKey *) (** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *) -let check_condition tenv case_zero find_canonical_duplicate curr_pname +let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e typ ta true_branch from_call idenv linereader loc instr_ref : unit = let is_fun_nonnull ta = match TypeAnnotation.get_origin ta with | TypeOrigin.Proc proc_origin -> @@ -111,7 +109,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname Annotations.ia_is_nonnull ia | _ -> false in - let contains_instanceof_throwable node = + let contains_instanceof_throwable pdesc node = (* Check if the current procedure has a catch Throwable. *) (* That always happens in the bytecode generated by try-with-resources. *) let loc = Cfg.Node.get_loc node in @@ -128,7 +126,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname let do_node n = if Location.equal loc (Cfg.Node.get_loc n) then IList.iter do_instr (Cfg.Node.get_instrs n) in - Cfg.Procdesc.iter_nodes do_node (Cfg.Node.get_proc_desc node); + Cfg.Procdesc.iter_nodes do_node pdesc; !throwable_found in let from_try_with_resources () : bool = @@ -137,7 +135,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname | Some line -> not (string_contains "==" line || string_contains "!=" line) && (string_contains "}" line) - && contains_instanceof_throwable node + && contains_instanceof_throwable curr_pdesc node | None -> false in let is_temp = Idenv.exp_is_temp idenv e in @@ -156,10 +154,9 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname if should_report then report_error tenv find_canonical_duplicate - node (TypeErr.Condition_redundant (is_always_true, explain_expr tenv node e, nonnull)) (Some instr_ref) - loc curr_pname + loc curr_pdesc (** Check an "is zero" condition. *) let check_zero tenv find_canonical_duplicate = check_condition tenv true find_canonical_duplicate @@ -169,13 +166,14 @@ let check_nonzero tenv find_canonical_duplicate = check_condition tenv false fin (** Check an assignment to a field. *) let check_field_assignment tenv - find_canonical_duplicate curr_pname node instr_ref typestate exp_lhs + find_canonical_duplicate curr_pdesc node instr_ref typestate exp_lhs exp_rhs typ loc fname t_ia_opt typecheck_expr : unit = + let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let (t_lhs, ta_lhs, _) = - typecheck_expr node instr_ref curr_pname typestate exp_lhs + typecheck_expr node instr_ref curr_pdesc typestate exp_lhs (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in let (_, ta_rhs, _) = - typecheck_expr node instr_ref curr_pname typestate exp_rhs + typecheck_expr node instr_ref curr_pdesc typestate exp_rhs (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in let should_report_nullable = let field_is_field_injector_readwrite () = match t_ia_opt with @@ -208,20 +206,18 @@ let check_field_assignment tenv let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in report_error tenv find_canonical_duplicate - node (TypeErr.Field_annotation_inconsistent (ann, fname, origin_descr)) (Some instr_ref) - loc curr_pname + loc curr_pdesc end; if should_report_mutable then begin let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in report_error tenv find_canonical_duplicate - node (TypeErr.Field_not_mutable (fname, origin_descr)) (Some instr_ref) - loc curr_pname + loc curr_pdesc end @@ -291,11 +287,10 @@ let check_constructor_initialization tenv not may_be_assigned_in_final_typestate then report_error tenv find_canonical_duplicate - start_node (TypeErr.Field_not_initialized (fn, curr_pname)) None loc - curr_pname; + curr_pdesc; (* Check if field is over-annotated. *) if Config.eradicate_field_over_annotated && @@ -303,11 +298,10 @@ let check_constructor_initialization tenv not (may_be_nullable_in_final_typestate ()) then report_error tenv find_canonical_duplicate - start_node (TypeErr.Field_over_annotated (fn, curr_pname)) None loc - curr_pname; + curr_pdesc; ) in IList.iter do_field fields @@ -336,8 +330,9 @@ let spec_make_return_nullable curr_pname = (** Check the annotations when returning from a method. *) let check_return_annotation tenv - find_canonical_duplicate curr_pname exit_node ret_range + find_canonical_duplicate curr_pdesc ret_range ret_ia ret_implicitly_nullable loc : unit = + let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let ret_annotated_nullable = Annotations.ia_is_nullable ret_ia in let ret_annotated_present = Annotations.ia_is_present ret_ia in let ret_annotated_nonnull = Annotations.ia_is_nonnull ret_ia in @@ -376,20 +371,18 @@ let check_return_annotation tenv report_error tenv find_canonical_duplicate - exit_node (TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr)) None - loc curr_pname + loc curr_pdesc end; if return_over_annotated then begin report_error tenv find_canonical_duplicate - exit_node (TypeErr.Return_over_annotated curr_pname) None - loc curr_pname + loc curr_pdesc end | None -> () @@ -397,7 +390,7 @@ let check_return_annotation tenv (** Check the receiver of a virtual call. *) let check_call_receiver tenv find_canonical_duplicate - curr_pname + curr_pdesc node typestate call_params @@ -409,7 +402,7 @@ let check_call_receiver tenv match call_params with | ((original_this_e, this_e), typ) :: _ -> let (_, this_ta, _) = - typecheck_expr tenv node instr_ref curr_pname typestate this_e + typecheck_expr tenv node instr_ref curr_pdesc typestate this_e (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in let null_method_call = TypeAnnotation.get_value Annotations.Nullable this_ta in let optional_get_on_absent = @@ -423,17 +416,16 @@ let check_call_receiver tenv let origin_descr = TypeAnnotation.descr_origin tenv this_ta in report_error tenv find_canonical_duplicate - node (TypeErr.Call_receiver_annotation_inconsistent (ann, descr, callee_pname, origin_descr)) (Some instr_ref) - loc curr_pname + loc curr_pdesc end | [] -> () (** Check the parameters of a call. *) let check_call_parameters tenv - find_canonical_duplicate curr_pname node typestate callee_attributes + find_canonical_duplicate curr_pdesc node typestate callee_attributes sig_params call_params loc instr_ref typecheck_expr : unit = let callee_pname = callee_attributes.ProcAttributes.proc_name in let has_this = is_virtual sig_params in @@ -444,7 +436,7 @@ let check_call_parameters tenv let formal_is_nullable = Annotations.ia_is_nullable ia1 in let formal_is_present = Annotations.ia_is_present ia1 in let (_, ta2, _) = - typecheck_expr node instr_ref curr_pname typestate e2 + typecheck_expr node instr_ref curr_pdesc typestate e2 (t2, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in let parameter_not_nullable = not param_is_this && @@ -473,7 +465,6 @@ let check_call_parameters tenv let callee_loc = callee_attributes.ProcAttributes.loc in report_error tenv find_canonical_duplicate - node (TypeErr.Parameter_annotation_inconsistent ( ann, description, @@ -482,7 +473,7 @@ let check_call_parameters tenv callee_loc, origin_descr)) (Some instr_ref) - loc curr_pname; + loc curr_pdesc; if Models.Inference.enabled then Models.Inference.proc_add_parameter_nullable callee_pname param_num tot_param_num end; @@ -515,10 +506,9 @@ let check_overridden_annotations if ret_is_nullable && not ret_overridden_nullable then report_error tenv find_canonical_duplicate - start_node (TypeErr.Inconsistent_subclass_return_annotation (proc_name, overriden_proc_name)) None - loc proc_name + loc proc_desc and check_params overriden_proc_name overriden_signature = let compare pos current_param overriden_param : int = @@ -529,11 +519,10 @@ let check_overridden_annotations && Annotations.ia_is_nullable overriden_ia then report_error tenv find_canonical_duplicate - start_node (TypeErr.Inconsistent_subclass_parameter_annotation (Mangled.to_string current_name, pos, proc_name, overriden_proc_name)) None - loc proc_name in + loc proc_desc in (pos + 1) in (* TODO (#5280249): investigate why argument lists can be of different length *) diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index e2c45d78d..012c66ad0 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -157,7 +157,7 @@ type checks = (** Typecheck an expression. *) let rec typecheck_expr - find_canonical_duplicate visited checks tenv node instr_ref curr_pname + find_canonical_duplicate visited checks tenv node instr_ref (curr_pdesc : Cfg.Procdesc.t) typestate e tr_default loc : TypeState.range = match e with | Exp.Lvar pvar -> (match TypeState.lookup_pvar pvar typestate with @@ -177,7 +177,7 @@ let rec typecheck_expr | Exp.Exn e1 -> typecheck_expr find_canonical_duplicate visited checks tenv - node instr_ref curr_pname + node instr_ref curr_pdesc typestate e1 tr_default loc | Exp.Const _ -> let (typ, _, locs) = tr_default in @@ -186,7 +186,7 @@ let rec typecheck_expr let _, _, locs = tr_default in let (_, ta, locs') = typecheck_expr - find_canonical_duplicate visited checks tenv node instr_ref curr_pname typestate exp + find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate exp (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, locs) loc in let tr_new = match EradicateChecks.get_field_annotation tenv fn typ with | Some (t, ia) -> @@ -198,7 +198,7 @@ let rec typecheck_expr | None -> tr_default in if checks.eradicate then EradicateChecks.check_field_access tenv - find_canonical_duplicate curr_pname node instr_ref exp fn ta loc; + find_canonical_duplicate curr_pdesc node instr_ref exp fn ta loc; tr_new | Exp.Lindex (array_exp, index_exp) -> let (_, ta, _) = @@ -208,7 +208,7 @@ let rec typecheck_expr checks tenv node instr_ref - curr_pname + curr_pdesc typestate array_exp tr_default @@ -223,7 +223,7 @@ let rec typecheck_expr if checks.eradicate then EradicateChecks.check_array_access tenv find_canonical_duplicate - curr_pname + curr_pdesc node instr_ref array_exp @@ -429,8 +429,7 @@ let typecheck_instr annotated_signature.Annotations.params in let is_return pvar = - let pdesc = Cfg.Node.get_proc_desc node in - let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in + let ret_pvar = Cfg.Procdesc.get_ret_var curr_pdesc in Pvar.equal pvar ret_pvar in (* Apply a function to a pvar and its associated content if front-end generated. *) @@ -458,7 +457,7 @@ let typecheck_instr let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref - curr_pname typestate1 exp1 + curr_pdesc typestate1 exp1 (typ1, TypeAnnotation.const Annotations.Nullable false origin1, [loc1]) loc1 in @@ -490,7 +489,7 @@ let typecheck_instr let t_ia_opt = EradicateChecks.get_field_annotation tenv fn f_typ in if checks.eradicate then EradicateChecks.check_field_assignment tenv - find_canonical_duplicate curr_pname node + find_canonical_duplicate curr_pdesc node instr_ref typestate1 e1' e2 typ loc fn t_ia_opt (typecheck_expr find_canonical_duplicate calls_this checks tenv) | _ -> () in @@ -531,7 +530,7 @@ let typecheck_instr checks tenv node instr_ref - curr_pname + curr_pdesc typestate array_exp (t, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) @@ -539,7 +538,7 @@ let typecheck_instr if checks.eradicate then EradicateChecks.check_array_access tenv find_canonical_duplicate - curr_pname + curr_pdesc node instr_ref array_exp @@ -642,11 +641,10 @@ let typecheck_instr let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in EradicateChecks.report_error tenv find_canonical_duplicate - node (TypeErr.Condition_redundant (true, EradicateChecks.explain_expr tenv node cond, false)) (Some instr_ref) - loc curr_pname + loc curr_pdesc end; TypeState.add pvar @@ -793,7 +791,7 @@ let typecheck_instr if cflags.CallFlags.cf_virtual && checks.eradicate then EradicateChecks.check_call_receiver tenv find_canonical_duplicate - curr_pname + curr_pdesc node typestate1 call_params @@ -804,7 +802,7 @@ let typecheck_instr if checks.eradicate then EradicateChecks.check_call_parameters tenv find_canonical_duplicate - curr_pname + curr_pdesc node typestate1 callee_attributes @@ -946,7 +944,7 @@ let typecheck_instr if checks.eradicate then EradicateChecks.check_zero tenv - find_canonical_duplicate curr_pname + find_canonical_duplicate curr_pdesc node' e' typ ta true_branch EradicateChecks.From_condition idenv linereader loc instr_ref; @@ -992,7 +990,7 @@ let typecheck_instr typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in if checks.eradicate then - EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pname + EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc node e' typ ta true_branch from_call idenv linereader loc instr_ref; begin match from_call with diff --git a/infer/src/eradicate/typeErr.ml b/infer/src/eradicate/typeErr.ml index 2e7663e55..167c05473 100644 --- a/infer/src/eradicate/typeErr.ml +++ b/infer/src/eradicate/typeErr.ml @@ -306,7 +306,8 @@ type st_report_error = (** Report an error right now. *) let report_error_now tenv - (st_report_error : st_report_error) node err_instance loc pname : unit = + (st_report_error : st_report_error) err_instance loc pdesc : unit = + let pname = Cfg.Procdesc.get_proc_name pdesc in let demo_mode = true in let do_print_base ew_string kind_s s = let mname = match pname with @@ -529,7 +530,7 @@ let report_error_now tenv let always_report = Strict.err_instance_get_strict tenv err_instance <> None in st_report_error pname - (Cfg.Node.get_proc_desc node) + pdesc kind_s loc ~advice @@ -542,22 +543,22 @@ let report_error_now tenv (** Report an error unless is has been reported already, or unless it's a forall error since it requires waiting until the end of the analysis and be printed by flush. *) -let report_error tenv (st_report_error : st_report_error) find_canonical_duplicate node - err_instance instr_ref_opt loc pname_java = +let report_error tenv (st_report_error : st_report_error) find_canonical_duplicate + err_instance instr_ref_opt loc pdesc = let should_report_now = add_err find_canonical_duplicate err_instance instr_ref_opt loc in if should_report_now then - report_error_now tenv st_report_error node err_instance loc pname_java + report_error_now tenv st_report_error err_instance loc pdesc (** Report the forall checks at the end of the analysis and reset the error table *) -let report_forall_checks_and_reset tenv st_report_error proc_name = +let report_forall_checks_and_reset tenv st_report_error proc_desc = let iter (err_instance, instr_ref_opt) err_state = match instr_ref_opt, get_forall err_instance with | Some instr_ref, is_forall -> let node = InstrRef.get_node instr_ref in State.set_node node; if is_forall && err_state.always - then report_error_now tenv st_report_error node err_instance err_state.loc proc_name + then report_error_now tenv st_report_error err_instance err_state.loc proc_desc | None, _ -> () in H.iter iter err_tbl; reset () diff --git a/infer/src/eradicate/typeErr.mli b/infer/src/eradicate/typeErr.mli index 11ce8a8c6..7a03dcf19 100644 --- a/infer/src/eradicate/typeErr.mli +++ b/infer/src/eradicate/typeErr.mli @@ -81,10 +81,10 @@ type st_report_error = val report_error : Tenv.t -> st_report_error -> - (Cfg.Node.t -> Cfg.Node.t) -> Cfg.Node.t -> + (Cfg.Node.t -> Cfg.Node.t) -> err_instance -> InstrRef.t option -> Location.t -> - Procname.t -> unit + Cfg.Procdesc.t -> unit -val report_forall_checks_and_reset : Tenv.t -> st_report_error -> Procname.t -> unit +val report_forall_checks_and_reset : Tenv.t -> st_report_error -> Cfg.Procdesc.t -> unit val reset : unit -> unit diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 11d33b024..aefcf0d01 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -257,9 +257,9 @@ let setup_harness_cfg harness_name env cg cfg = (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 start_node []; - Cfg.Node.set_succs_exn start_node [harness_node] [exit_node]; - Cfg.Node.set_succs_exn harness_node [exit_node] [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]; 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 848397909..f35cd7acb 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -48,7 +48,7 @@ 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 node (get_succ_nodes node pc) (get_exn_nodes pc) in + Cfg.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 +57,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 join_node [node_true; node_false] []; + Cfg.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 +65,11 @@ let add_edges direct_successors (-1) in (* the exceptions edges here are going directly to the exit node *) - Cfg.Node.set_succs_exn start_node first_nodes exit_nodes; + Cfg.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 exn_node exit_nodes exit_nodes; + Cfg.Node.set_succs_exn context.procdesc exn_node exit_nodes exit_nodes; Array.iteri connect_nodes method_body_nodes diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 78cf3a79b..d40215250 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -272,7 +272,7 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio let start_node = Cfg.Node.create Location.dummy start_kind [] procdesc 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 start_node [exit_node] [exit_node]; + Cfg.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 @@ -329,7 +329,7 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio 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 start_node locals; + Cfg.Node.add_locals_ret_declaration procdesc start_node locals; procdesc in Some procdesc with JBir.Subroutine | JBasics.Class_structure_error _ -> diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index fecf5d859..dbf48dd2c 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -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 node_true catch_nodes exit_nodes; - Cfg.Node.set_succs_exn node_false succ_nodes exit_nodes; + Cfg.Node.set_succs_exn procdesc node_true catch_nodes exit_nodes; + Cfg.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 entry_node nodes_first_handler exit_nodes; + Cfg.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 b9a565395..198710151 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -176,7 +176,7 @@ module Make let create_node kind cmds = Cfg.Node.create dummy_loc kind cmds pdesc in let set_succs cur_node succs ~exn_handlers= - Cfg.Node.set_succs_exn cur_node succs exn_handlers in + Cfg.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 b842e610e..342f4f77e 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -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 n1 [n2] [n3]; - Cfg.Node.set_succs_exn n2 [n4] [n3]; - Cfg.Node.set_succs_exn n3 [n4] [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]; let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in