From 4013e13cbe0506cd41d101cc6595296c73df4454 Mon Sep 17 00:00:00 2001 From: jrm Date: Mon, 6 Jul 2015 09:36:46 -0700 Subject: [PATCH] [infer] Moving the getter for the return variable from Cfg.Procdesc to Sil Summary: the name of the return variable of a procedure only depends on the name of that procedure. This simplifies the need for the procedure description in a couple of places --- infer/src/backend/cfg.ml | 3 ++- infer/src/backend/interproc.ml | 40 ++++++++++++++++---------------- infer/src/backend/sil.ml | 3 ++- infer/src/backend/sil.mli | 4 ++-- infer/src/backend/symExec.ml | 5 ++-- infer/src/backend/tabulation.ml | 16 ++++++------- infer/src/backend/tabulation.mli | 4 ++-- infer/src/java/jTrans.ml | 14 +++-------- 8 files changed, 42 insertions(+), 47 deletions(-) diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index 5e8cfd778..557e1fb4d 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -333,7 +333,8 @@ module Node = struct let replace_instrs node instrs = node.nd_instrs <- instrs - let proc_desc_get_ret_var pdesc = Sil.mk_pvar Ident.name_return pdesc.pd_name + let proc_desc_get_ret_var pdesc = + Sil.get_ret_pvar pdesc.pd_name (** Add declarations for local variables and return variable to the node *) let add_locals_ret_declaration node locals = diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 944227186..08d086349 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -246,11 +246,11 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list (* =============== START of symbolic execution =============== *) (* propagate a set of results to the given node *) -let propagate proc_desc is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) = +let propagate pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) = let edgeset_todo = let f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *) let exn_opt = - if is_exception then Some (Tabulation.prop_get_exn_name proc_desc prop) + if is_exception then Some (Tabulation.prop_get_exn_name pname prop) else None in Paths.PathSet.add_renamed_prop prop (Paths.Path.extend curr_node exn_opt (State.get_session ()) path) edgeset_curr in Paths.PathSet.fold f pset Paths.PathSet.empty in @@ -263,7 +263,7 @@ let propagate_nodes_divergence (path: Paths.Path.t) (kind_curr_node : Cfg.Node.nodekind) (_succ_nodes: Cfg.node list) (exn_nodes: Cfg.node list) = let pname = Cfg.Procdesc.get_proc_name pdesc in - let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pdesc) pset in + let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in let succ_nodes = match State.get_goto_node () with (* handle Sil.Goto_node target, if any *) | Some node_id -> list_filter (fun n -> Cfg.Node.get_id n = node_id) _succ_nodes @@ -281,17 +281,17 @@ let propagate_nodes_divergence Paths.PathSet.map mk_incons diverging_states in (L.d_strln_color Orange) "Propagating Divergence -- diverging states:"; Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln (); - propagate pdesc false prop_incons exit_node + propagate pname false prop_incons exit_node end; - list_iter (propagate pdesc false pset_ok) succ_nodes; - list_iter (propagate pdesc true pset_exn) exn_nodes + list_iter (propagate pname false pset_ok) succ_nodes; + list_iter (propagate pname true pset_exn) exn_nodes (* ===================== END of symbolic execution ===================== *) (* =============== START of forward_tabulate =============== *) (** Symbolic execution for a Join node *) -let do_symexec_join proc_desc tenv curr_node (edgeset_todo : Paths.PathSet.t) = +let do_symexec_join pname tenv 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_id = Cfg.Node.get_id curr_node in @@ -303,7 +303,7 @@ let do_symexec_join proc_desc tenv curr_node (edgeset_todo : Paths.PathSet.t) = list_iter (fun node -> Paths.PathSet.iter (fun prop path -> State.set_path path None; - propagate proc_desc false (Paths.PathSet.from_renamed_list [(prop, path)]) node) + propagate pname false (Paths.PathSet.from_renamed_list [(prop, path)]) node) new_dset') succ_nodes let prop_max_size = ref (0, Prop.prop_emp) @@ -549,7 +549,7 @@ let forward_tabulate cfg tenv = L.d_ln (); L.d_ln (); match kind_curr_node with - | Cfg.Node.Join_node -> do_symexec_join proc_desc tenv curr_node pathset_todo + | Cfg.Node.Join_node -> do_symexec_join proc_name tenv curr_node pathset_todo | Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _ | Cfg.Node.Exit_node _ @@ -940,10 +940,10 @@ let reset_global_counters cfg proc_name proc_desc = set_current_language cfg proc_desc (* Collect all pairs of the kind (precondition, exception) from a summary *) -let exception_preconditions tenv pdesc summary = +let exception_preconditions tenv pname summary = let collect_exceptions pre exns (prop, path) = - if Tabulation.prop_is_exn pdesc prop then - let exn_name = Tabulation.prop_get_exn_name pdesc prop in + if Tabulation.prop_is_exn pname prop then + let exn_name = Tabulation.prop_get_exn_name pname prop in if AndroidFramework.is_runtime_exception tenv exn_name then (pre, exn_name):: exns else exns @@ -984,19 +984,19 @@ let remove_this_not_null prop = (** Detects if there are specs of the form {precondition} proc {runtime exception} and report an error in that case, generating the trace that lead to the runtime exception if the method is called in the context { precondition } *) -let report_runtime_exceptions tenv cfg proc_desc summary = - let proc_name = Specs.get_proc_name summary in +let report_runtime_exceptions tenv cfg pdesc summary = + let pname = Specs.get_proc_name summary in let is_public_method = (Specs.get_attributes summary).Sil.access = Sil.Public in let is_main = is_public_method (* TODO (#4559939): add check for static method *) - && Procname.is_java proc_name - && (Procname.java_get_method proc_name) = "main" in + && Procname.is_java pname + && (Procname.java_get_method pname) = "main" in let is_annotated = let annotated_signature = Annotations.get_annotated_signature - Specs.proc_get_method_annotation proc_desc proc_name in + Specs.proc_get_method_annotation pdesc pname in let ret_annotation, _ = annotated_signature.Annotations.ret in Annotations.ia_is_verify ret_annotation in let is_unavoidable pre = @@ -1011,10 +1011,10 @@ let report_runtime_exceptions tenv cfg proc_desc summary = if should_report pre then let pre_str = Utils.pp_to_string (Prop.pp_prop pe_text) (Specs.Jprop.to_prop pre) in - let exn_desc = Localise.java_unchecked_exn_desc proc_name runtime_exception pre_str in + let exn_desc = Localise.java_unchecked_exn_desc pname runtime_exception pre_str in let exn = Exceptions.Java_runtime_exception (runtime_exception, pre_str, exn_desc) in - Reporting.log_error proc_name ~pre: (Some (Specs.Jprop.to_prop pre)) exn in - list_iter report (exception_preconditions tenv proc_desc summary) + Reporting.log_error pname ~pre: (Some (Specs.Jprop.to_prop pre)) exn in + list_iter report (exception_preconditions tenv pname summary) (** update a summary after analysing a procedure *) diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index d5aaf920e..ee62e6301 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -3776,7 +3776,8 @@ let pp_tenv f (tenv : tenv) = let mk_pvar (name: Mangled.t) (proc_name: Procname.t) : pvar = { pv_name = name; pv_kind = Local_var proc_name } -let mk_ret_var pname = + +let get_ret_pvar pname = mk_pvar Ident.name_return pname (** [mk_pvar_callee name proc_name] creates a program var for a callee function with the given function name *) diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 01ab436d3..36c147861 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -1318,8 +1318,8 @@ val loc_none : location (** [mk_pvar name proc_name suffix] creates a program var with the given function name and suffix *) val mk_pvar : Mangled.t -> Procname.t -> pvar -(** [mk_ret_var proc_name] creates the retun pvar based on the procedure name *) -val mk_ret_var : Procname.t -> pvar +(** [get_ret_pvar proc_name] retuns the return pvar associated with the procedure name *) +val get_ret_pvar : Procname.t -> pvar (** [mk_pvar_callee name proc_name] creates a program var for a callee function with the given function name *) val mk_pvar_callee : Mangled.t -> Procname.t -> pvar diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 110dc9abc..826504bbd 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1342,10 +1342,11 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t) let lifted_sym_exec handle_exn cfg tenv pdesc (pset : Paths.PathSet.t) node (instrs : Sil.instr list) -: 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 = - if Tabulation.prop_is_exn pdesc p && not (Sil.instr_is_auxiliary instr) + if Tabulation.prop_is_exn pname p && not (Sil.instr_is_auxiliary instr) && Cfg.Node.get_kind node <> Cfg.Node.exn_handler_kind (* skip normal instructions if an exception was thrown, unless this is an exception handler node *) then diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 51beafec7..1f664cf49 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -537,8 +537,8 @@ let exp_is_exn = function | _ -> false (** check if a prop is an exception *) -let prop_is_exn pdesc prop = - let ret_pvar = Sil.Lvar (Cfg.Procdesc.get_ret_var pdesc) in +let prop_is_exn pname prop = + let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in let is_exn = function | Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Sil.exp_equal e1 ret_pvar -> exp_is_exn e2 @@ -546,8 +546,8 @@ let prop_is_exn pdesc prop = list_exists is_exn (Prop.get_sigma prop) (** when prop is an exception, return the exception name *) -let prop_get_exn_name pdesc prop = - let ret_pvar = Sil.Lvar (Cfg.Procdesc.get_ret_var pdesc) in +let prop_get_exn_name pname prop = + let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in let exn_name = ref (Mangled.from_string "") in let find_exn_name e = let do_hpred = function @@ -574,8 +574,8 @@ let lookup_global_errors prop = search_error (Prop.get_sigma prop) (** set a prop to an exception sexp *) -let prop_set_exn pdesc prop se_exn = - let ret_pvar = Sil.Lvar (Cfg.Procdesc.get_ret_var pdesc) in +let prop_set_exn pname prop se_exn = + let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in let map_hpred = function | Sil.Hpointsto (e, _, t) when Sil.exp_equal e ret_pvar -> Sil.Hpointsto(e, se_exn, t) @@ -673,7 +673,7 @@ let combine let post_p3 = (** replace [result|callee] with an aux variable dedicated to this proc *) let callee_ret_pvar = - Sil.Lvar (Sil.pvar_to_callee callee_pname (Sil.mk_ret_var callee_pname)) in + Sil.Lvar (Sil.pvar_to_callee callee_pname (Sil.get_ret_pvar callee_pname)) in match Prop.prop_iter_create post_p2 with | None -> post_p2 | Some iter -> @@ -686,7 +686,7 @@ let combine match fst (Prop.prop_iter_current iter') with | Sil.Hpointsto (e, Sil.Eexp (e', inst), t) when exp_is_exn e' -> (* resuls is an exception: set in caller *) let p = Prop.prop_iter_remove_curr_then_to_prop iter' in - prop_set_exn caller_pdesc p (Sil.Eexp (e', inst)) + prop_set_exn caller_pname p (Sil.Eexp (e', inst)) | Sil.Hpointsto (e, Sil.Eexp (e', inst), t) when list_length ret_ids = 1 -> let p = Prop.prop_iter_remove_curr_then_to_prop iter' in Prop.conjoin_eq e' (Sil.Var (list_hd ret_ids)) p diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 21df001e6..d3f17eb0d 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -23,10 +23,10 @@ val raise_cast_exception : Utils.ml_location -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a (** check if a prop is an exception *) -val prop_is_exn : Cfg.Procdesc.t -> 'a Prop.t -> bool +val prop_is_exn : Procname.t -> 'a Prop.t -> bool (** when prop is an exception, return the exception name *) -val prop_get_exn_name : Cfg.Procdesc.t -> 'a Prop.t -> Mangled.t +val prop_get_exn_name : Procname.t -> 'a Prop.t -> Mangled.t (** search in prop contains an error state *) val lookup_global_errors : 'a Prop.t -> Mangled.t option diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 7e4c6b988..1e093d8bb 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -831,13 +831,15 @@ let rec instruction context pc instr : translation = let cn = JContext.get_cn context in let program = JContext.get_program context in let meth_kind = JContext.get_meth_kind context in + let proc_name = Cfg.Procdesc.get_proc_name (JContext.get_procdesc context) in + let ret_var = Sil.get_ret_pvar proc_name in + let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let loc = get_location (JContext.get_impl context) pc meth_kind cn in let match_never_null = JContext.get_never_null_matcher context in let create_node node_kind temps sil_instrs = Cfg.Node.create cfg (get_location (JContext.get_impl context) pc meth_kind cn) node_kind sil_instrs (JContext.get_procdesc context) temps in let return_not_null () = - let proc_name = Cfg.Procdesc.get_proc_name (JContext.get_procdesc context) in (match_never_null loc.Sil.file proc_name || list_exists (fun p -> Procname.equal p proc_name) JTransType.never_returning_null) in try @@ -858,8 +860,6 @@ let rec instruction context pc instr : translation = create_node node_kind [] [] | Some expr -> let (idl, stml, sil_expr) = expression context pc expr in - let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in - let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let sil_instrs = let return_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_expr, loc) in if return_not_null () then @@ -938,8 +938,6 @@ let rec instruction context pc instr : translation = | JBir.Throw expr -> let node_kind = Cfg.Node.Stmt_node "throw" in let (ids, instrs, sil_expr) = expression context pc expr in - let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in - let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let sil_exn = Sil.Const (Sil.Cexn sil_expr) in let sil_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in let node = create_node node_kind ids (instrs @ [sil_instr]) in @@ -1076,8 +1074,6 @@ let rec instruction context pc instr : translation = let ret_opt = Some (Sil.Var ret_id, class_type) in method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Procname.Static in let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in - let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in - let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in create_node npe_kind (ids @ call_ids) npe_instrs in @@ -1133,8 +1129,6 @@ let rec instruction context pc instr : translation = context loc pc None out_of_bound_cn constr_ms (Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in - let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in - let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in let out_of_bound_instrs = instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in @@ -1173,8 +1167,6 @@ let rec instruction context pc instr : translation = method_invocation context loc pc None cce_cn constr_ms (Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in - let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in - let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in let cce_instrs = instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in