pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[infer] Moving the getter for the return variable from Cfg.Procdesc to Sil

Browse Source 
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
master
jrm 10 years ago
parent d808a3ee26
commit 4013e13cbe
8 changed files with 42 additions and 47 deletions
Show Stats Download Patch File Download Diff File

3
infer/src/backend/cfg.ml
Unescape View File

@ -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 =

40
infer/src/backend/interproc.ml
Unescape View File

@ -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 *)

3
infer/src/backend/sil.ml
Unescape View File

@ -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 *)

4
infer/src/backend/sil.mli
Unescape View File

@ -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

5
infer/src/backend/symExec.ml
Unescape View File

@ -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

16
infer/src/backend/tabulation.ml
Unescape View File

@ -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

4
infer/src/backend/tabulation.mli
Unescape View File

@ -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

14
infer/src/java/jTrans.ml
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save