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

[IR] Remove use of Cfg.Node.get_proc_desc

Browse Source 
Reviewed By: jvillard

Differential Revision: D4095234

fbshipit-source-id: 20f7077
master
Cristiano Calcagno 9 years ago committed by Facebook Github Bot
parent 1bd6615abc
commit 73c5dfdfa4
27 changed files with 267 additions and 266 deletions
Show Stats Download Patch File Download Diff File

34
infer/src/IR/Cfg.re
Unescape View File

@ -26,9 +26,10 @@ let module Node = {
| Stmt_node string | Stmt_node string
| Join_node | Join_node
| Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ | Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */
| Skip_node string | Skip_node string;
/** a node */ /** a node */
and t = { type t = {
/** unique id of the node */ /** unique id of the node */
nd_id: id, nd_id: id,
/** distance to the exit node */ /** distance to the exit node */
@ -43,13 +44,14 @@ let module Node = {
nd_loc: Location.t, nd_loc: Location.t,
/** predecessor nodes in the cfg */ /** predecessor nodes in the cfg */
mutable nd_preds: list t, mutable nd_preds: list t,
/** proc desc from cil */ /** name of the procedure the node belongs to */
nd_proc: option proc_desc, nd_pname: option Procname.t,
/** successor nodes in the cfg */ /** successor nodes in the cfg */
mutable nd_succs: list t mutable nd_succs: list t
} };
/** procedure description */ /** procedure description */
and proc_desc = { type proc_desc = {
pd_attributes: ProcAttributes.t, /** attributes of the procedure */ pd_attributes: ProcAttributes.t, /** attributes of the procedure */
pd_id: int, /** unique proc_desc identifier */ pd_id: int, /** unique proc_desc identifier */
mutable pd_nodes: list t, /** list of nodes of this procedure */ mutable pd_nodes: list t, /** list of nodes of this procedure */
@ -145,7 +147,7 @@ let module Node = {
nd_instrs: [], nd_instrs: [],
nd_kind: Skip_node "dummy", nd_kind: Skip_node "dummy",
nd_loc: Location.dummy, nd_loc: Location.dummy,
nd_proc: None, nd_pname: None,
nd_succs: [], nd_succs: [],
nd_preds: [], nd_preds: [],
nd_exn: [] nd_exn: []
@ -165,7 +167,7 @@ let module Node = {
nd_kind: kind, nd_kind: kind,
nd_loc: loc, nd_loc: loc,
nd_preds: [], nd_preds: [],
nd_proc: Some pdesc, nd_pname: Some pdesc.pd_attributes.proc_name,
nd_succs: [], nd_succs: [],
nd_exn: [] nd_exn: []
}; };
@ -226,13 +228,13 @@ let module Node = {
}; };
let get_exn node => node.nd_exn; let get_exn node => node.nd_exn;
/** Get the proc desc of the node */ /** Get the name of the procedure the node belongs to */
let get_proc_desc node => let get_proc_name node =>
switch node.nd_proc { switch node.nd_pname {
| None => | None =>
L.out "node_get_proc_desc: at node %d@\n" node.nd_id; L.out "node_get_proc_desc: at node %d@\n" node.nd_id;
assert false assert false
| Some proc_desc => proc_desc | Some proc_name => proc_name
}; };
/** Set the successor nodes and exception nodes, and build predecessor links */ /** Set the successor nodes and exception nodes, and build predecessor links */
@ -245,11 +247,10 @@ let module Node = {
/** Set the successor and exception nodes. /** Set the successor and exception nodes.
If this is a join node right before the exit node, add an extra node in the middle, 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. */ 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) { switch (node.nd_kind, succs) {
| (Join_node, [{nd_kind: Exit_node _} as exit_node]) => | (Join_node, [{nd_kind: Exit_node _} as exit_node]) =>
let kind = Stmt_node "between_join_and_exit"; 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; let node' = create node.nd_loc kind node.nd_instrs pdesc;
set_succs_exn_base node [node'] exn; set_succs_exn_base node [node'] exn;
set_succs_exn_base node' [exit_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; Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name;
/** Add declarations for local variables and return variable to the node */ /** 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 loc = get_loc node;
let pdesc = get_proc_desc node;
let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name; let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name;
let ret_var = { let ret_var = {
let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type; let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type;
@ -712,7 +712,7 @@ let module Node = {
if (equal node callee_exit_node) { if (equal node callee_exit_node) {
proc_desc_set_exit_node resolved_proc_desc new_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 new_node
}; };
[converted_node, ...loop other_node] [converted_node, ...loop other_node]

8
infer/src/IR/Cfg.rei
Unescape View File

@ -161,7 +161,7 @@ let module Node: {
let prepend_instrs: t => list Sil.instr => unit; let prepend_instrs: t => list Sil.instr => unit;
/** Add declarations for local variables and return variable to the node */ /** 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 */ /** Compare two nodes */
let compare: t => t => int; let compare: t => t => int;
@ -213,8 +213,8 @@ let module Node: {
from a node with subsequent applications of a generator function */ from a node with subsequent applications of a generator function */
let get_generated_slope: t => (t => list t) => list t; let get_generated_slope: t => (t => list t) => list t;
/** Get the proc desc associated to the node */ /** Get the name of the procedure the node belongs to */
let get_proc_desc: t => Procdesc.t; let get_proc_name: t => Procname.t;
/** Get the instructions to be executed */ /** Get the instructions to be executed */
let get_instrs: t => list Sil.instr; let get_instrs: t => list Sil.instr;
@ -249,7 +249,7 @@ let module Node: {
let replace_instrs: t => list Sil.instr => unit; let replace_instrs: t => list Sil.instr => unit;
/** Set the successor nodes and exception nodes, and build predecessor links */ /** 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;
}; };

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

@ -55,7 +55,10 @@ let check_access access_opt de_opt =
let find_bucket line_number null_case_flag = let find_bucket line_number null_case_flag =
let find_formal_ids node = (* find ids obtained by a letref on a formal parameter *) 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 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 formal_names = IList.map fst formals in
let is_formal pvar = let is_formal pvar =
let name = Pvar.get_name pvar in let name = Pvar.get_name pvar in

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

@ -297,13 +297,11 @@ let propagate_nodes_divergence
(** Symbolic execution for a Join node *) (** Symbolic execution for a Join node *)
let do_symexec_join pname tenv wl curr_node (edgeset_todo : Paths.PathSet.t) = 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 curr_node_id = Cfg.Node.get_id curr_node in
let succ_nodes = Cfg.Node.get_succs curr_node in let succ_nodes = Cfg.Node.get_succs curr_node in
let new_dset = edgeset_todo in let new_dset = edgeset_todo in
let old_dset = Join_table.find wl.Worklist.join_table curr_node_id 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'); Join_table.add wl.Worklist.join_table curr_node_id (Paths.PathSet.union old_dset' new_dset');
IList.iter (fun node -> IList.iter (fun node ->
Paths.PathSet.iter (fun prop path -> Paths.PathSet.iter (fun prop path ->
@ -334,14 +332,12 @@ let reset_prop_metrics () =
exception RE_EXE_ERROR 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 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_node node;
State.set_session session; State.set_session session;
L.reset_delayed_prints (); 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 = let do_after_node source node =
Printer.node_finish_session node source 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 *) (* 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 exclude function calls: if (g(x,y)) ....*)
(* we check that prune nodes have simple guards: a var or its negation*) (* we check that prune nodes have simple guards: a var or its negation*)
let check_assignement_guard node = let check_assignement_guard pdesc node =
let pdesc = Cfg.Node.get_proc_desc node in
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let verbose = false in let verbose = false in
let node_contains_call n = let node_contains_call n =
@ -467,17 +462,17 @@ let check_assignement_guard node =
) else () ) else ()
(** Perform symbolic execution for a node starting from an initial prop *) (** 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) = (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; State.mark_execution_start node;
(* build the const map lazily *) (* build the const map lazily *)
State.set_const_map (ConstantPropagation.build_const_map tenv pdesc); 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 let instrs = Cfg.Node.get_instrs node in
(* fresh normal vars must be fresh w.r.t. instructions *) (* fresh normal vars must be fresh w.r.t. instructions *)
Ident.update_name_generator (instrs_get_normal_vars instrs); 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 ...."; L.d_strln ".... After Symbolic Execution ....";
Propset.d prop (Paths.PathSet.to_propset tenv pset); Propset.d prop (Paths.PathSet.to_propset tenv pset);
L.d_ln (); L.d_ln(); 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) Taint.add_tainting_attribute tenv attr param prop_acc)
prop 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 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; Exceptions.print_exception_html "Failure of symbolic execution: " exn;
let pre_opt = (* precondition leading to error, if any *) 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 (match pre_opt with
| Some pre -> | Some pre ->
L.d_strln "Precondition:"; Prop.d_prop pre; L.d_ln () L.d_strln "Precondition:"; Prop.d_prop pre; L.d_ln ()
| None -> ()); | None -> ());
L.d_strln "SIL INSTR:"; L.d_strln "SIL INSTR:";
Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node; L.d_ln (); 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 State.mark_instr_fail exn in
let exe_iter f pathset = let exe_iter f pathset =
@ -533,16 +527,16 @@ let forward_tabulate tenv wl source =
f prop path !cnt ps_size in f prop path !cnt ps_size in
Paths.PathSet.iter exe pathset 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 log_string proc_name =
let phase_string = let phase_string =
if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE" in 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 summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
let timestamp = Specs.get_timestamp summary in let timestamp = Specs.get_timestamp summary in
F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) 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) ^ ", " ^ "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 ^ ", " ^ "Session: " ^ string_of_int session ^ ", " ^
"Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****"); "Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****");
L.d_increase_indent 1; 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; Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node;
L.d_ln (); L.d_ln () in 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 = let prop =
if Config.taint_analysis 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 else prop_ in
L.d_strln L.d_strln
("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths); ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths);
@ -562,31 +556,31 @@ let forward_tabulate tenv wl source =
try try
State.reset_diverging_states_node (); State.reset_diverging_states_node ();
let pset = 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 succ_nodes = Cfg.Node.get_succs curr_node in
let exn_nodes = Cfg.Node.get_exn 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(); L.d_decrease_indent 1; L.d_ln();
with with
| exn when Exceptions.handle_exception exn && !Config.footprint -> | exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn exn; handle_exn exn;
L.d_decrease_indent 1; L.d_ln () in 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; 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 match Cfg.Node.get_kind curr_node with
| Cfg.Node.Join_node -> | 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.Stmt_node _
| Cfg.Node.Prune_node _ | Cfg.Node.Prune_node _
| Cfg.Node.Exit_node _ | Cfg.Node.Exit_node _
| Cfg.Node.Skip_node _ | Cfg.Node.Skip_node _
| Cfg.Node.Start_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 let pathset_todo = path_set_checkout_todo wl curr_node in
try try
begin begin
@ -594,7 +588,7 @@ let forward_tabulate tenv wl source =
let handle_exn exn = let handle_exn exn =
handle_exn_called := true; handle_exn_called := true;
handle_exn_node curr_node exn in 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 (); if !handle_exn_called then Printer.force_delayed_prints ();
do_after_node source curr_node do_after_node source curr_node
end end
@ -607,15 +601,13 @@ let forward_tabulate tenv wl source =
while not (Worklist.is_empty wl) do while not (Worklist.is_empty wl) do
let curr_node = Worklist.remove wl in let curr_node = Worklist.remove wl in
let proc_desc = Cfg.Node.get_proc_desc curr_node in let summary = Specs.get_summary_unsafe "forward_tabulate" pname in
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
mark_visited summary curr_node; (* mark nodes visited in fp and re phases *) mark_visited summary curr_node; (* mark nodes visited in fp and re phases *)
let session = let session =
incr summary.Specs.sessions; incr summary.Specs.sessions;
!(summary.Specs.sessions) in !(summary.Specs.sessions) in
do_before_node source session curr_node; do_before_node pname source session curr_node;
do_node_and_handle curr_node proc_desc proc_name session do_node_and_handle curr_node session
done; done;
L.d_strln ".... Work list empty. Stop ...."; L.d_ln () 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. *) (** 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 let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t) source
: Prop.normal Specs.spec option = : Prop.normal Specs.spec option =
let proc_name = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
do_before_node source 0 init_node; do_before_node pname source 0 init_node;
L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string proc_name ^ " ####"); L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string pname ^ " ####");
L.d_indent 1; L.d_indent 1;
L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition; L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition;
L.d_ln (); L.d_ln (); L.d_ln (); L.d_ln ();
@ -932,10 +924,10 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
try try
Worklist.add wl init_node; Worklist.add wl init_node;
ignore (path_set_put_todo wl init_node init_edgeset); ignore (path_set_put_todo wl init_node init_edgeset);
forward_tabulate tenv wl source; forward_tabulate tenv pdesc wl source;
do_before_node source 0 init_node; do_before_node pname source 0 init_node;
L.d_strln_color Green 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_increase_indent 1;
L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition); L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition);
L.d_ln (); 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; do_after_node source init_node;
Some spec Some spec
with RE_EXE_ERROR -> with RE_EXE_ERROR ->
do_before_node source 0 init_node; do_before_node pname source 0 init_node;
Printer.force_delayed_prints (); 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_increase_indent 1;
L.d_strln "when starting from pre:"; L.d_strln "when starting from pre:";
Prop.d_prop (Specs.Jprop.to_prop precondition); Prop.d_prop (Specs.Jprop.to_prop precondition);
@ -986,13 +978,15 @@ let pp_intra_stats wl proc_desc fmt _ =
nodes; nodes;
F.fprintf fmt "(%d nodes containing %d states)" (IList.length nodes) !nstates 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. (** 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 Given [proc_name], return [do, get_results] where [go ()] performs the analysis phase
and [get_results ()] returns the results computed. and [get_results ()] returns the results computed.
This function is architected so that [get_results ()] can be called even after This function is architected so that [get_results ()] can be called even after
[go ()] was interrupted by and exception. *) [go ()] was interrupted by and exception. *)
let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) source 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 start_node = Cfg.Procdesc.get_start_node pdesc in
let check_recursion_level () = 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)) raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level))
end in 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 go (wl : Worklist.t) () =
let init_prop = initial_prop_from_emp tenv pdesc in let init_prop = initial_prop_from_emp tenv pdesc in
(* use existing pre's (in recursion some might exist) as starting points *) (* 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) (Cfg.Procdesc.get_flags pdesc)
Mleak_buckets.objc_arc_flag; Mleak_buckets.objc_arc_flag;
ignore (path_set_put_todo wl start_node init_edgeset); 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) () = let get_results (wl : Worklist.t) () =
State.process_execution_failures Reporting.log_warning pname; State.process_execution_failures Reporting.log_warning pname;
let results = collect_analysis_result tenv wl pdesc in 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 let wl = path_set_create_worklist pdesc in
go wl, get_results wl in go wl, get_results wl in
let re_execution proc_name let re_execution () : exe_phase =
: (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
let candidate_preconditions = let candidate_preconditions =
IList.map IList.map
(fun spec -> spec.Specs.pre) (fun spec -> spec.Specs.pre)
(Specs.get_specs proc_name) in (Specs.get_specs pname) in
let valid_specs = ref [] in let valid_specs = ref [] in
let go () = 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 (); check_recursion_level ();
let filter p = let filter p =
let wl = path_set_create_worklist pdesc in 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 let outcome = if is_valid then "pass" else "fail" in
L.out "Finished re-execution for precondition %d %a (%s)@." L.out "Finished re-execution for precondition %d %a (%s)@."
(Specs.Jprop.to_number p) (Specs.Jprop.to_number p)
(pp_intra_stats wl pdesc) proc_name (pp_intra_stats wl pdesc) pname
outcome; outcome;
speco in speco in
if Config.undo_join then 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 ignore (IList.map filter candidate_preconditions) in
let get_results () = let get_results () =
let specs = !valid_specs in let specs = !valid_specs in
L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp proc_name; L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname;
L.out "#### Finished: Re-Execution for %a ####@." Procname.pp proc_name; L.out "#### Finished: Re-Execution for %a ####@." Procname.pp pname;
let valid_preconditions = let valid_preconditions =
IList.map (fun spec -> spec.Specs.pre) specs in IList.map (fun spec -> spec.Specs.pre) specs in
let filename = let filename =
DB.Results_dir.path_to_filename DB.Results_dir.path_to_filename
(DB.Results_dir.Abs_source_dir source) (DB.Results_dir.Abs_source_dir source)
[(Procname.to_filename proc_name)] in [(Procname.to_filename pname)] in
if Config.write_dotty then if Config.write_dotty then
Dotty.pp_speclist_dotty_file filename specs; Dotty.pp_speclist_dotty_file filename specs;
L.out "@.@.================================================"; 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 "@.================================================@.";
L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text false) candidate_preconditions; L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text false) candidate_preconditions;
L.out "@.@.================================================"; 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 "@.================================================@.";
L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text true) valid_preconditions; L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text true) valid_preconditions;
specs, Specs.RE_EXECUTION in 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 match Specs.get_phase pname with
| Specs.FOOTPRINT -> | Specs.FOOTPRINT ->
compute_footprint compute_footprint ()
| Specs.RE_EXECUTION -> | Specs.RE_EXECUTION ->
re_execution pname re_execution ()
let set_current_language proc_desc = let set_current_language proc_desc =
let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in 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 f start_node
| None -> () | None -> ()
with exn when SymOp.exn_not_failure exn -> () in 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 try
Config.allow_leak := true; Config.allow_leak := true;
let res = collect_preconditions tenv proc_name in let res = collect_preconditions tenv proc_name in
@ -1511,23 +1504,26 @@ let do_analysis exe_env =
Ondemand.unset_callbacks () Ondemand.unset_callbacks ()
let visited_and_total_nodes cfg = let visited_and_total_nodes ~filter cfg =
let all_nodes = let filter_node pdesc n =
let set = ref Cfg.NodeSet.empty in Cfg.Procdesc.is_defined pdesc &&
let add _ n = set := Cfg.NodeSet.add n !set in filter pdesc &&
Cfg.iter_all_nodes add cfg;
!set in
let filter_node n =
Cfg.Procdesc.is_defined (Cfg.Node.get_proc_desc n) &&
match Cfg.Node.get_kind n with match Cfg.Node.get_kind n with
| Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _ | Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _
| Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ -> true | Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ -> true
| Cfg.Node.Skip_node _ | Cfg.Node.Join_node -> false in | Cfg.Node.Skip_node _ | Cfg.Node.Join_node -> false in
let counted_nodes = Cfg.NodeSet.filter filter_node all_nodes in let counted_nodes, visited_nodes_re =
let visited_nodes_re = let set = ref Cfg.NodeSet.empty in
Cfg.NodeSet.filter let set_visited_re = ref Cfg.NodeSet.empty in
(fun node -> snd (Printer.node_is_visited node)) let add pdesc n =
counted_nodes in 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 Cfg.NodeSet.elements visited_nodes_re, Cfg.NodeSet.elements counted_nodes
(** Print the stats for the given cfg. (** 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 *) was defined in another module, and was the one which was analyzed *)
let print_stats_cfg proc_shadowed source cfg = let print_stats_cfg proc_shadowed source cfg =
let err_table = Errlog.create_err_table () in let err_table = Errlog.create_err_table () in
let nvisited, ntotal = visited_and_total_nodes cfg in let filter pdesc =
let node_filter n = let pname = Cfg.Procdesc.get_proc_name pdesc in
let node_procname = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc n) in Specs.summary_exists pname && Specs.get_specs pname != [] in
Specs.summary_exists node_procname && Specs.get_specs node_procname != [] in let nodes_visited, nodes_total = visited_and_total_nodes ~filter cfg in
let nodes_visited = IList.filter node_filter nvisited in
let nodes_total = IList.filter node_filter ntotal in
let num_proc = ref 0 in let num_proc = ref 0 in
let num_nospec_noerror_proc = ref 0 in let num_nospec_noerror_proc = ref 0 in
let num_spec_noerror_proc = ref 0 in let num_spec_noerror_proc = ref 0 in

2
infer/src/backend/paths.ml
Unescape View File

@ -271,7 +271,7 @@ end = struct
Invariant.reset_stats path Invariant.reset_stats path
let get_path_pos node = 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 let n_id = Cfg.Node.get_id node in
(pn, (n_id :> int)) (pn, (n_id :> int))

30
infer/src/backend/printer.ml
Unescape View File

@ -77,9 +77,7 @@ end
let curr_html_formatter = ref F.std_formatter let curr_html_formatter = ref F.std_formatter
(** Return true if the node was visited during footprint and during re-execution*) (** Return true if the node was visited during footprint and during re-execution*)
let node_is_visited node = let node_is_visited proc_name node =
let proc_desc = Cfg.Node.get_proc_desc node in
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
match Specs.get_summary proc_name with match Specs.get_summary proc_name with
| None -> | None ->
false, false false, false
@ -92,8 +90,8 @@ let node_is_visited node =
is_visited_fp, is_visited_re is_visited_fp, is_visited_re
(** Return true if the node was visited during analysis *) (** Return true if the node was visited during analysis *)
let is_visited node = let is_visited proc_name node =
let visited_fp, visited_re = node_is_visited node in let visited_fp, visited_re = node_is_visited proc_name node in
visited_fp || visited_re visited_fp || visited_re
(* =============== START of module NodesHtml =============== *) (* =============== 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_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_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn 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 "<br>SUCCS: @\n"; F.fprintf fmt "<br>SUCCS: @\n";
IList.iter (fun node -> IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] "" 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_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_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn 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 "<br>EXN: @\n"; F.fprintf fmt "<br>EXN: @\n";
IList.iter (fun node -> IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] "" 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_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_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn 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 "<br>@\n"; F.fprintf fmt "<br>@\n";
F.pp_print_flush fmt (); F.pp_print_flush fmt ();
true 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_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_succs n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn 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; nodes;
(match Specs.get_summary pname with (match Specs.get_summary pname with
| None -> | 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 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 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 lnum = (Cfg.Node.get_loc n).Location.line in
let curr_nodes = let curr_nodes =
try Hashtbl.find nodes_tbl lnum try Hashtbl.find table_nodes_at_linenum lnum
with Not_found -> [] in 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 proc_loc = Cfg.Procdesc.get_loc proc_desc in
let process_proc = let process_proc =
Cfg.Procdesc.is_defined proc_desc && 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 DB.source_file_equal source_captured (Cfg.Procdesc.get_loc proc_desc).file in
if process_proc then if process_proc then
begin 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 match Specs.get_summary proc_name with
| None -> | None ->
() ()
@ -522,7 +520,7 @@ let write_html_file linereader filename procs =
line_html in line_html in
F.fprintf fmt "%s" str; F.fprintf fmt "%s" str;
IList.iter IList.iter
(fun n -> (fun (n, pdesc) ->
let isproof = let isproof =
Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in
Io_infer.Html.pp_node_link 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_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_succs n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn 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 isproof
fmt fmt
(Cfg.Node.get_id n :> int)) (Cfg.Node.get_id n :> int))
nodes_at_linenum; nodes_at_linenum;
IList.iter IList.iter
(fun n -> (fun (n, _) ->
match Cfg.Node.get_kind n with match Cfg.Node.get_kind n with
| Cfg.Node.Start_node proc_name -> | Cfg.Node.Start_node proc_name ->
let num_specs = IList.length (Specs.get_specs proc_name) in let num_specs = IList.length (Specs.get_specs proc_name) in

2
infer/src/backend/printer.mli
Unescape View File

@ -40,7 +40,7 @@ val force_delayed_prints : unit -> unit
val node_finish_session : Cfg.node -> DB.source_file -> unit val node_finish_session : Cfg.node -> DB.source_file -> unit
(** Return true if the node was visited during footprint and during re-execution *) (** 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 *) (** 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 val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> DB.source_file -> unit

43
infer/src/backend/prover.ml
Unescape View File

@ -857,27 +857,28 @@ let check_inconsistency_base tenv prop =
let inconsistent_ptsto _ = let inconsistent_ptsto _ =
check_allocatedness tenv prop Exp.zero in check_allocatedness tenv prop Exp.zero in
let inconsistent_this_self_var () = let inconsistent_this_self_var () =
let procdesc = match State.get_prop_tenv_pdesc () with
Cfg.Node.get_proc_desc (State.get_node ()) in | None -> false
let procedure_attr = | Some (_, _, pdesc) ->
Cfg.Procdesc.get_attributes procdesc in let procedure_attr =
let is_java_this pvar = Cfg.Procdesc.get_attributes pdesc in
procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in let is_java_this pvar =
let is_objc_instance_self pvar = procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in
procedure_attr.ProcAttributes.language = Config.Clang && let is_objc_instance_self pvar =
Pvar.get_name pvar = Mangled.from_string "self" && procedure_attr.ProcAttributes.language = Config.Clang &&
procedure_attr.ProcAttributes.is_objc_instance_method in Pvar.get_name pvar = Mangled.from_string "self" &&
let is_cpp_this pvar = procedure_attr.ProcAttributes.is_objc_instance_method in
procedure_attr.ProcAttributes.language = Config.Clang && let is_cpp_this pvar =
Pvar.is_this pvar && procedure_attr.ProcAttributes.language = Config.Clang &&
procedure_attr.ProcAttributes.is_cpp_instance_method in Pvar.is_this pvar &&
let do_hpred = function procedure_attr.ProcAttributes.is_cpp_instance_method in
| Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) -> let do_hpred = function
Exp.equal e Exp.zero && | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) ->
Pvar.is_seed pv && Exp.equal e Exp.zero &&
(is_java_this pv || is_cpp_this pv || is_objc_instance_self pv) Pvar.is_seed pv &&
| _ -> false in (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
IList.exists do_hpred sigma in | _ -> false in
IList.exists do_hpred sigma in
let inconsistent_atom = function let inconsistent_atom = function
| Sil.Aeq (e1, e2) -> | Sil.Aeq (e1, e2) ->
(match e1, e2 with (match e1, e2 with

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

@ -1657,8 +1657,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
(** {2 Lifted Abstract Transfer Functions} *) (** {2 Lifted Abstract Transfer Functions} *)
let node handle_exn tenv node (pset : Paths.PathSet.t) : Paths.PathSet.t = let node handle_exn tenv pdesc node (pset : Paths.PathSet.t) : Paths.PathSet.t =
let pdesc = Cfg.Node.get_proc_desc node in
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) = let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
let pset2 = let pset2 =

3
infer/src/backend/symExec.mli
Unescape View File

@ -13,7 +13,8 @@ open! Utils
(** Symbolic Execution *) (** Symbolic Execution *)
(** Symbolic execution of the instructions of a node, lifted to sets of propositions. *) (** 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. (** Symbolic execution of a sequence of instructions.
If errors occur and [mask_errors] is true, just treat as skip. *) If errors occur and [mask_errors] is true, just treat as skip. *)

11
infer/src/checkers/checkers.ml
Unescape View File

@ -159,8 +159,7 @@ module ST = struct
end end
end end
let report_calls_and_accesses tenv callback node instr = let report_calls_and_accesses tenv callback proc_desc instr =
let proc_desc = Cfg.Node.get_proc_desc node in
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let callee = Procname.to_string proc_name in let callee = Procname.to_string proc_name in
match PatternMatch.get_java_field_access_signature instr with 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. *) (** Report all field accesses and method calls of a procedure. *)
let callback_check_access { Callbacks.tenv; proc_desc } = 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. *) (** Report all field accesses and method calls of a class. *)
let callback_check_cluster_access exe_env all_procs get_proc_desc _ = 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 match get_proc_desc proc_name with
| Some proc_desc -> | Some proc_desc ->
let tenv = Exe_env.get_tenv exe_env proc_name in 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 ) all_procs

5
infer/src/checkers/dataflow.ml
Unescape View File

@ -47,10 +47,9 @@ module type DF = sig
end end
(** Determine if the node can throw an exception. *) (** 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 instr_throws instr =
let is_return pvar = 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 pdesc in
Pvar.equal pvar ret_pvar in Pvar.equal pvar ret_pvar in
match instr with match instr with
@ -157,7 +156,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
try try
let state = H.find t.pre_states node in let state = H.find t.pre_states node in
let states_succ, states_exn = St.do_node tenv node state 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 -> () with Not_found -> ()
done in done in

5
infer/src/clang/cFrontend_decl.ml
Unescape View File

@ -38,8 +38,9 @@ struct
"\n\n>>---------- Start translating body of function: '%s' ---------<<\n@." "\n\n>>---------- Start translating body of function: '%s' ---------<<\n@."
(Procname.to_string procname); (Procname.to_string procname);
let meth_body_nodes = T.instructions_trans context body extra_instrs exit_node in 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.add_locals_ret_declaration
Cfg.Node.set_succs_exn start_node meth_body_nodes []; 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)) Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc))
| None -> ()) | None -> ())
with with

56
infer/src/clang/cTrans.ml
Unescape View File

@ -591,15 +591,16 @@ struct
this_expr_trans trans_state sil_loc expr_info.Clang_ast_t.ei_type_ptr 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 rec labelStmt_trans trans_state stmt_info stmt_list label_name =
let context = trans_state.context in
(* go ahead with the translation *) (* go ahead with the translation *)
let res_trans = match stmt_list with let res_trans = match stmt_list with
| [stmt] -> | [stmt] ->
instruction trans_state stmt instruction trans_state stmt
| _ -> assert false (* expected a stmt or at most a compoundstmt *) in | _ -> assert false (* expected a stmt or at most a compoundstmt *) in
(* create the label root node into the hashtbl *) (* 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 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 } { 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) = 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)] } { empty_res_trans with exps = [(const_exp, typ)] }
and arraySubscriptExpr_trans trans_state expr_info stmt_list = 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 let array_stmt, idx_stmt = (match stmt_list with
| [a; i] -> a, i (* Assumption: the statement list contains 2 elements, | [a; i] -> a, i (* Assumption: the statement list contains 2 elements,
the first is the array expr and the second the index *) the first is the array expr and the second the index *)
@ -748,7 +750,7 @@ struct
if res_trans_idx.root_nodes <> [] if res_trans_idx.root_nodes <> []
then then
IList.iter 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; res_trans_a.leaf_nodes;
(* Note the order of res_trans_idx.ids @ res_trans_a.ids is important. *) (* 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 "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_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 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 (match stmt_list with
| [cond; exp1; exp2] -> | [cond; exp1; exp2] ->
let typ = let typ =
@ -1137,7 +1141,7 @@ struct
context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in
let var_typ = add_reference_if_glvalue typ expr_info 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 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 let pvar = mk_temp_sil_var procdesc "SIL_temp_conditional___" in
Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)]; Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)];
let continuation' = mk_cond_continuation trans_state.continuation in 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_t = mk_prune_node true e' instrs' in
let prune_f = mk_prune_node false e' instrs' in let prune_f = mk_prune_node false e' instrs' in
IList.iter 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; res_trans_cond.leaf_nodes;
let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then
[prune_t; prune_f] [prune_t; prune_f]
@ -1243,7 +1247,7 @@ struct
| Binop.LOr -> prune_nodes_f, prune_nodes_t | Binop.LOr -> prune_nodes_f, prune_nodes_t
| _ -> assert false) in | _ -> assert false) in
IList.iter 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; prune_to_s2;
let root_nodes_to_parent = let root_nodes_to_parent =
if (IList.length res_trans_s1.root_nodes) = 0 if (IList.length res_trans_s1.root_nodes) = 0
@ -1284,7 +1288,7 @@ struct
let succ_nodes = trans_state.succ_nodes in let succ_nodes = trans_state.succ_nodes in
let sil_loc = CLocation.get_sil_location stmt_info context 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 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 trans_state' = { trans_state with succ_nodes = [join_node] } in
let do_branch branch stmt_branch prune_nodes = let do_branch branch stmt_branch prune_nodes =
(* leaf nodes are ignored here as they will be already attached to join_node *) (* 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 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_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 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 (match stmt_list with
| [_; decl_stmt; cond; stmt1; stmt2] -> | [_; decl_stmt; cond; stmt1; stmt2] ->
(* set the flat to inform that we are translating a condition of a if *) (* 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 let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in
create_node node_kind res_trans_cond_tmp.instrs sil_loc context in create_node node_kind res_trans_cond_tmp.instrs sil_loc context in
IList.iter 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; res_trans_cond_tmp.leaf_nodes;
let root_nodes = let root_nodes =
if res_trans_cond_tmp.root_nodes <> [] then res_trans_cond_tmp.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 let case_entry_point = connected_instruction (IList.rev case_content) last_nodes in
(* connects between cases, then continuation has priority about breaks *) (* connects between cases, then continuation has priority about breaks *)
let prune_node_t, prune_node_f = create_prune_nodes_for_case case in 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 context.procdesc 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_f last_prune_nodes [];
case_entry_point, [prune_node_t; prune_node_f] case_entry_point, [prune_node_t; prune_node_f]
| DefaultStmt(stmt_info, default_content) :: rest -> | DefaultStmt(stmt_info, default_content) :: rest ->
let sil_loc = CLocation.get_sil_location stmt_info context in 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 translate_and_connect_cases rest next_nodes [placeholder_entry_point] in
let default_entry_point = let default_entry_point =
connected_instruction (IList.rev default_content) last_nodes in 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 default_entry_point, last_prune_nodes
| _ -> assert false in | _ -> assert false in
let top_entry_point, top_prune_nodes = let top_entry_point, top_prune_nodes =
translate_and_connect_cases list_of_cases succ_nodes succ_nodes in translate_and_connect_cases list_of_cases succ_nodes succ_nodes in
let _ = connected_instruction (IList.rev pre_case_stmts) top_entry_point 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 let top_nodes = res_trans_decl.root_nodes in
IList.iter IList.iter
(fun n' -> Cfg.Node.append_instrs n' []) succ_nodes; (fun n' -> Cfg.Node.append_instrs n' []) succ_nodes;
@ -1529,9 +1536,13 @@ struct
match loop_kind with match loop_kind with
| Loops.For _ | Loops.While _ -> res_trans_body.root_nodes | Loops.For _ | Loops.While _ -> res_trans_body.root_nodes
| Loops.DoWhile _ -> [join_node] in | Loops.DoWhile _ -> [join_node] in
Cfg.Node.set_succs_exn join_node join_succ_nodes []; Cfg.Node.set_succs_exn context.procdesc join_node join_succ_nodes [];
IList.iter (fun n -> Cfg.Node.set_succs_exn n prune_t_succ_nodes []) prune_nodes_t; IList.iter
IList.iter (fun n -> Cfg.Node.set_succs_exn n succ_nodes []) prune_nodes_f; (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 = let root_nodes =
match loop_kind with match loop_kind with
| Loops.For _ -> | Loops.For _ ->
@ -1880,6 +1891,7 @@ struct
let mk_ret_node instrs = let mk_ret_node instrs =
let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in
Cfg.Node.set_succs_exn Cfg.Node.set_succs_exn
context.procdesc
ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] []; ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] [];
ret_node in ret_node in
let trans_result = (match stmt_list with 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 instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in
let ret_node = mk_ret_node instrs in let ret_node = mk_ret_node instrs in
IList.iter 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; res_trans_stmt.leaf_nodes;
let root_nodes_to_parent = let root_nodes_to_parent =
if IList.length res_trans_stmt.root_nodes >0 if IList.length res_trans_stmt.root_nodes >0
@ -1999,7 +2011,7 @@ struct
autorelease_pool_vars, sil_loc, CallFlags.default) in autorelease_pool_vars, sil_loc, CallFlags.default) in
let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") 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 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 let trans_state'={ trans_state with continuation = None; succ_nodes =[call_node] } in
instructions trans_state' stmts instructions trans_state' stmts
@ -2098,7 +2110,7 @@ struct
and cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info = and cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info =
let context = trans_state.context in 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 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 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 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 (var_exp, typ) = var_exp_typ in
let res_trans_init_list = initListExpr_initializers_trans trans_state_init var_exp 0 stmts let res_trans_init_list = initListExpr_initializers_trans trans_state_init var_exp 0 stmts
typ is_dyn_array stmt_info in 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 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 all_res_trans = [res_trans_size; res_trans_new; res_trans_init] in
let nname = "CXXNewExpr" in let nname = "CXXNewExpr" in

20
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -158,7 +158,7 @@ let empty_res_trans = {
let undefined_expression () = Exp.Var (Ident.create_fresh Ident.knormal) 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. *) (** 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 = let rec collect l rt =
match l with match l with
| [] -> rt | [] -> rt
@ -170,7 +170,7 @@ let collect_res_trans l =
if rt'.leaf_nodes <> [] then rt'.leaf_nodes if rt'.leaf_nodes <> [] then rt'.leaf_nodes
else rt.leaf_nodes in else rt.leaf_nodes in
if rt'.root_nodes <> [] then 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' collect l'
{ root_nodes = root_nodes; { root_nodes = root_nodes;
leaf_nodes = leaf_nodes; leaf_nodes = leaf_nodes;
@ -238,14 +238,16 @@ struct
(* deals with creating or not a cfg node depending of owning the *) (* 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 *) (* 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 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 let create_node = own_priority_node trans_state.priority stmt_info && res_state.instrs <> [] in
if create_node then if create_node then
(* We need to create a node *) (* We need to create a node *)
let node_kind = Cfg.Node.Stmt_node (nd_name) in 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 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 []; Cfg.Node.set_succs_exn trans_state.context.procdesc node trans_state.succ_nodes [];
IList.iter (fun leaf -> Cfg.Node.set_succs_exn leaf [node] []) res_state.leaf_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.*) (* 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 let root_nodes = (if res_state.root_nodes <> [] then res_state.root_nodes
else [node]) in 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); (Clang_ast_j.string_of_cast_kind cast_kind);
([], (exp, cast_typ)) ([], (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 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 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 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) let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)
and failure_node = and failure_node =
Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in 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]; } { 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 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 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] } { empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] }
let trans_assertion trans_state sil_loc = let trans_assertion trans_state sil_loc =

2
infer/src/clang/cTrans_utils.mli
Unescape View File

@ -44,7 +44,7 @@ val empty_res_trans: trans_result
val undefined_expression: unit -> Exp.t 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 val extract_var_exp_or_fail : trans_state -> Exp.t * Typ.t

4
infer/src/eradicate/eradicate.ml
Unescape View File

@ -97,7 +97,7 @@ struct
checks.TypeCheck.check_ret_type; checks.TypeCheck.check_ret_type;
if checks.TypeCheck.eradicate then if checks.TypeCheck.eradicate then
EradicateChecks.check_return_annotation tenv 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 ret_ia ret_implicitly_nullable loc in
let do_before_dataflow initial_typestate = let do_before_dataflow initial_typestate =
@ -326,7 +326,7 @@ struct
tenv curr_pname curr_pdesc tenv curr_pname curr_pdesc
annotated_signature; 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 update_summary curr_pname curr_pdesc final_typestate_opt
(** Entry point for the eradicate-based checker infrastructure. *) (** Entry point for the eradicate-based checker infrastructure. *)

61
infer/src/eradicate/eradicateChecks.ml
Unescape View File

@ -67,7 +67,6 @@ let check_field_access tenv
let origin_descr = TypeAnnotation.descr_origin tenv ta in let origin_descr = TypeAnnotation.descr_origin tenv ta in
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false)) (TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false))
(Some instr_ref) (Some instr_ref)
loc curr_pname loc curr_pname
@ -87,7 +86,6 @@ let check_array_access tenv
let origin_descr = TypeAnnotation.descr_origin tenv ta in let origin_descr = TypeAnnotation.descr_origin tenv ta in
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed)) (TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed))
(Some instr_ref) (Some instr_ref)
loc loc
@ -103,7 +101,7 @@ type from_call =
| From_containsKey (** x.containsKey *) | From_containsKey (** x.containsKey *)
(** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *) (** 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 = 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 let is_fun_nonnull ta = match TypeAnnotation.get_origin ta with
| TypeOrigin.Proc proc_origin -> | TypeOrigin.Proc proc_origin ->
@ -111,7 +109,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
Annotations.ia_is_nonnull ia Annotations.ia_is_nonnull ia
| _ -> false in | _ -> false in
let contains_instanceof_throwable node = let contains_instanceof_throwable pdesc node =
(* Check if the current procedure has a catch Throwable. *) (* Check if the current procedure has a catch Throwable. *)
(* That always happens in the bytecode generated by try-with-resources. *) (* That always happens in the bytecode generated by try-with-resources. *)
let loc = Cfg.Node.get_loc node in 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 = let do_node n =
if Location.equal loc (Cfg.Node.get_loc n) if Location.equal loc (Cfg.Node.get_loc n)
then IList.iter do_instr (Cfg.Node.get_instrs n) in 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 !throwable_found in
let from_try_with_resources () : bool = let from_try_with_resources () : bool =
@ -137,7 +135,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
| Some line -> | Some line ->
not (string_contains "==" line || string_contains "!=" line) not (string_contains "==" line || string_contains "!=" line)
&& (string_contains "}" line) && (string_contains "}" line)
&& contains_instanceof_throwable node && contains_instanceof_throwable curr_pdesc node
| None -> false in | None -> false in
let is_temp = Idenv.exp_is_temp idenv e 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 if should_report then
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Condition_redundant (is_always_true, explain_expr tenv node e, nonnull)) (TypeErr.Condition_redundant (is_always_true, explain_expr tenv node e, nonnull))
(Some instr_ref) (Some instr_ref)
loc curr_pname loc curr_pdesc
(** Check an "is zero" condition. *) (** Check an "is zero" condition. *)
let check_zero tenv find_canonical_duplicate = check_condition tenv true find_canonical_duplicate 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. *) (** Check an assignment to a field. *)
let check_field_assignment tenv 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 = 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, _) = 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 (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in
let (_, ta_rhs, _) = 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 (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in
let should_report_nullable = let should_report_nullable =
let field_is_field_injector_readwrite () = match t_ia_opt with 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 let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Field_annotation_inconsistent (ann, fname, origin_descr)) (TypeErr.Field_annotation_inconsistent (ann, fname, origin_descr))
(Some instr_ref) (Some instr_ref)
loc curr_pname loc curr_pdesc
end; end;
if should_report_mutable then if should_report_mutable then
begin begin
let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in let origin_descr = TypeAnnotation.descr_origin tenv ta_rhs in
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Field_not_mutable (fname, origin_descr)) (TypeErr.Field_not_mutable (fname, origin_descr))
(Some instr_ref) (Some instr_ref)
loc curr_pname loc curr_pdesc
end end
@ -291,11 +287,10 @@ let check_constructor_initialization tenv
not may_be_assigned_in_final_typestate then not may_be_assigned_in_final_typestate then
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
start_node
(TypeErr.Field_not_initialized (fn, curr_pname)) (TypeErr.Field_not_initialized (fn, curr_pname))
None None
loc loc
curr_pname; curr_pdesc;
(* Check if field is over-annotated. *) (* Check if field is over-annotated. *)
if Config.eradicate_field_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 not (may_be_nullable_in_final_typestate ()) then
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
start_node
(TypeErr.Field_over_annotated (fn, curr_pname)) (TypeErr.Field_over_annotated (fn, curr_pname))
None None
loc loc
curr_pname; curr_pdesc;
) in ) in
IList.iter do_field fields IList.iter do_field fields
@ -336,8 +330,9 @@ let spec_make_return_nullable curr_pname =
(** Check the annotations when returning from a method. *) (** Check the annotations when returning from a method. *)
let check_return_annotation tenv 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 = 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_nullable = Annotations.ia_is_nullable ret_ia in
let ret_annotated_present = Annotations.ia_is_present 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 let ret_annotated_nonnull = Annotations.ia_is_nonnull ret_ia in
@ -376,20 +371,18 @@ let check_return_annotation tenv
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
exit_node
(TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr)) (TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr))
None None
loc curr_pname loc curr_pdesc
end; end;
if return_over_annotated then if return_over_annotated then
begin begin
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
exit_node
(TypeErr.Return_over_annotated curr_pname) (TypeErr.Return_over_annotated curr_pname)
None None
loc curr_pname loc curr_pdesc
end end
| None -> | None ->
() ()
@ -397,7 +390,7 @@ let check_return_annotation tenv
(** Check the receiver of a virtual call. *) (** Check the receiver of a virtual call. *)
let check_call_receiver tenv let check_call_receiver tenv
find_canonical_duplicate find_canonical_duplicate
curr_pname curr_pdesc
node node
typestate typestate
call_params call_params
@ -409,7 +402,7 @@ let check_call_receiver tenv
match call_params with match call_params with
| ((original_this_e, this_e), typ) :: _ -> | ((original_this_e, this_e), typ) :: _ ->
let (_, this_ta, _) = 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 (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in
let null_method_call = TypeAnnotation.get_value Annotations.Nullable this_ta in let null_method_call = TypeAnnotation.get_value Annotations.Nullable this_ta in
let optional_get_on_absent = let optional_get_on_absent =
@ -423,17 +416,16 @@ let check_call_receiver tenv
let origin_descr = TypeAnnotation.descr_origin tenv this_ta in let origin_descr = TypeAnnotation.descr_origin tenv this_ta in
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Call_receiver_annotation_inconsistent (TypeErr.Call_receiver_annotation_inconsistent
(ann, descr, callee_pname, origin_descr)) (ann, descr, callee_pname, origin_descr))
(Some instr_ref) (Some instr_ref)
loc curr_pname loc curr_pdesc
end end
| [] -> () | [] -> ()
(** Check the parameters of a call. *) (** Check the parameters of a call. *)
let check_call_parameters tenv 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 = sig_params call_params loc instr_ref typecheck_expr : unit =
let callee_pname = callee_attributes.ProcAttributes.proc_name in let callee_pname = callee_attributes.ProcAttributes.proc_name in
let has_this = is_virtual sig_params 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_nullable = Annotations.ia_is_nullable ia1 in
let formal_is_present = Annotations.ia_is_present ia1 in let formal_is_present = Annotations.ia_is_present ia1 in
let (_, ta2, _) = 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 (t2, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in
let parameter_not_nullable = let parameter_not_nullable =
not param_is_this && not param_is_this &&
@ -473,7 +465,6 @@ let check_call_parameters tenv
let callee_loc = callee_attributes.ProcAttributes.loc in let callee_loc = callee_attributes.ProcAttributes.loc in
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Parameter_annotation_inconsistent ( (TypeErr.Parameter_annotation_inconsistent (
ann, ann,
description, description,
@ -482,7 +473,7 @@ let check_call_parameters tenv
callee_loc, callee_loc,
origin_descr)) origin_descr))
(Some instr_ref) (Some instr_ref)
loc curr_pname; loc curr_pdesc;
if Models.Inference.enabled then if Models.Inference.enabled then
Models.Inference.proc_add_parameter_nullable callee_pname param_num tot_param_num Models.Inference.proc_add_parameter_nullable callee_pname param_num tot_param_num
end; end;
@ -515,10 +506,9 @@ let check_overridden_annotations
if ret_is_nullable && not ret_overridden_nullable then if ret_is_nullable && not ret_overridden_nullable then
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
start_node
(TypeErr.Inconsistent_subclass_return_annotation (proc_name, overriden_proc_name)) (TypeErr.Inconsistent_subclass_return_annotation (proc_name, overriden_proc_name))
None None
loc proc_name loc proc_desc
and check_params overriden_proc_name overriden_signature = and check_params overriden_proc_name overriden_signature =
let compare pos current_param overriden_param : int = let compare pos current_param overriden_param : int =
@ -529,11 +519,10 @@ let check_overridden_annotations
&& Annotations.ia_is_nullable overriden_ia then && Annotations.ia_is_nullable overriden_ia then
report_error tenv report_error tenv
find_canonical_duplicate find_canonical_duplicate
start_node
(TypeErr.Inconsistent_subclass_parameter_annotation (TypeErr.Inconsistent_subclass_parameter_annotation
(Mangled.to_string current_name, pos, proc_name, overriden_proc_name)) (Mangled.to_string current_name, pos, proc_name, overriden_proc_name))
None None
loc proc_name in loc proc_desc in
(pos + 1) in (pos + 1) in
(* TODO (#5280249): investigate why argument lists can be of different length *) (* TODO (#5280249): investigate why argument lists can be of different length *)

34
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -157,7 +157,7 @@ type checks =
(** Typecheck an expression. *) (** Typecheck an expression. *)
let rec typecheck_expr 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 typestate e tr_default loc : TypeState.range = match e with
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
(match TypeState.lookup_pvar pvar typestate with (match TypeState.lookup_pvar pvar typestate with
@ -177,7 +177,7 @@ let rec typecheck_expr
| Exp.Exn e1 -> | Exp.Exn e1 ->
typecheck_expr typecheck_expr
find_canonical_duplicate visited checks tenv find_canonical_duplicate visited checks tenv
node instr_ref curr_pname node instr_ref curr_pdesc
typestate e1 tr_default loc typestate e1 tr_default loc
| Exp.Const _ -> | Exp.Const _ ->
let (typ, _, locs) = tr_default in let (typ, _, locs) = tr_default in
@ -186,7 +186,7 @@ let rec typecheck_expr
let _, _, locs = tr_default in let _, _, locs = tr_default in
let (_, ta, locs') = let (_, ta, locs') =
typecheck_expr 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 (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, locs) loc in
let tr_new = match EradicateChecks.get_field_annotation tenv fn typ with let tr_new = match EradicateChecks.get_field_annotation tenv fn typ with
| Some (t, ia) -> | Some (t, ia) ->
@ -198,7 +198,7 @@ let rec typecheck_expr
| None -> tr_default in | None -> tr_default in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_field_access tenv 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 tr_new
| Exp.Lindex (array_exp, index_exp) -> | Exp.Lindex (array_exp, index_exp) ->
let (_, ta, _) = let (_, ta, _) =
@ -208,7 +208,7 @@ let rec typecheck_expr
checks tenv checks tenv
node node
instr_ref instr_ref
curr_pname curr_pdesc
typestate typestate
array_exp array_exp
tr_default tr_default
@ -223,7 +223,7 @@ let rec typecheck_expr
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_array_access tenv EradicateChecks.check_array_access tenv
find_canonical_duplicate find_canonical_duplicate
curr_pname curr_pdesc
node node
instr_ref instr_ref
array_exp array_exp
@ -429,8 +429,7 @@ let typecheck_instr
annotated_signature.Annotations.params in annotated_signature.Annotations.params in
let is_return pvar = let is_return pvar =
let pdesc = Cfg.Node.get_proc_desc node in let ret_pvar = Cfg.Procdesc.get_ret_var curr_pdesc in
let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in
Pvar.equal pvar ret_pvar in Pvar.equal pvar ret_pvar in
(* Apply a function to a pvar and its associated content if front-end generated. *) (* 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 = let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 =
typecheck_expr typecheck_expr
find_canonical_duplicate calls_this checks tenv node instr_ref 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]) (typ1, TypeAnnotation.const Annotations.Nullable false origin1, [loc1])
loc1 in loc1 in
@ -490,7 +489,7 @@ let typecheck_instr
let t_ia_opt = EradicateChecks.get_field_annotation tenv fn f_typ in let t_ia_opt = EradicateChecks.get_field_annotation tenv fn f_typ in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_field_assignment tenv 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 instr_ref typestate1 e1' e2 typ loc fn t_ia_opt
(typecheck_expr find_canonical_duplicate calls_this checks tenv) (typecheck_expr find_canonical_duplicate calls_this checks tenv)
| _ -> () in | _ -> () in
@ -531,7 +530,7 @@ let typecheck_instr
checks tenv checks tenv
node node
instr_ref instr_ref
curr_pname curr_pdesc
typestate typestate
array_exp array_exp
(t, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) (t, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc])
@ -539,7 +538,7 @@ let typecheck_instr
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_array_access tenv EradicateChecks.check_array_access tenv
find_canonical_duplicate find_canonical_duplicate
curr_pname curr_pdesc
node node
instr_ref instr_ref
array_exp array_exp
@ -642,11 +641,10 @@ let typecheck_instr
let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in
EradicateChecks.report_error tenv EradicateChecks.report_error tenv
find_canonical_duplicate find_canonical_duplicate
node
(TypeErr.Condition_redundant (TypeErr.Condition_redundant
(true, EradicateChecks.explain_expr tenv node cond, false)) (true, EradicateChecks.explain_expr tenv node cond, false))
(Some instr_ref) (Some instr_ref)
loc curr_pname loc curr_pdesc
end; end;
TypeState.add TypeState.add
pvar pvar
@ -793,7 +791,7 @@ let typecheck_instr
if cflags.CallFlags.cf_virtual && checks.eradicate then if cflags.CallFlags.cf_virtual && checks.eradicate then
EradicateChecks.check_call_receiver tenv EradicateChecks.check_call_receiver tenv
find_canonical_duplicate find_canonical_duplicate
curr_pname curr_pdesc
node node
typestate1 typestate1
call_params call_params
@ -804,7 +802,7 @@ let typecheck_instr
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_call_parameters tenv EradicateChecks.check_call_parameters tenv
find_canonical_duplicate find_canonical_duplicate
curr_pname curr_pdesc
node node
typestate1 typestate1
callee_attributes callee_attributes
@ -946,7 +944,7 @@ let typecheck_instr
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_zero tenv EradicateChecks.check_zero tenv
find_canonical_duplicate curr_pname find_canonical_duplicate curr_pdesc
node' e' typ node' e' typ
ta true_branch EradicateChecks.From_condition ta true_branch EradicateChecks.From_condition
idenv linereader loc instr_ref; idenv linereader loc instr_ref;
@ -992,7 +990,7 @@ let typecheck_instr
typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in
if checks.eradicate then 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; node e' typ ta true_branch from_call idenv linereader loc instr_ref;
begin begin
match from_call with match from_call with

15
infer/src/eradicate/typeErr.ml
Unescape View File

@ -306,7 +306,8 @@ type st_report_error =
(** Report an error right now. *) (** Report an error right now. *)
let report_error_now tenv 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 demo_mode = true in
let do_print_base ew_string kind_s s = let do_print_base ew_string kind_s s =
let mname = match pname with 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 let always_report = Strict.err_instance_get_strict tenv err_instance <> None in
st_report_error st_report_error
pname pname
(Cfg.Node.get_proc_desc node) pdesc
kind_s kind_s
loc loc
~advice ~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 (** 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. *) 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 let report_error tenv (st_report_error : st_report_error) find_canonical_duplicate
err_instance instr_ref_opt loc pname_java = err_instance instr_ref_opt loc pdesc =
let should_report_now = let should_report_now =
add_err find_canonical_duplicate err_instance instr_ref_opt loc in add_err find_canonical_duplicate err_instance instr_ref_opt loc in
if should_report_now then 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 *) (** 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 = let iter (err_instance, instr_ref_opt) err_state =
match instr_ref_opt, get_forall err_instance with match instr_ref_opt, get_forall err_instance with
| Some instr_ref, is_forall -> | Some instr_ref, is_forall ->
let node = InstrRef.get_node instr_ref in let node = InstrRef.get_node instr_ref in
State.set_node node; State.set_node node;
if is_forall && err_state.always 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 | None, _ -> () in
H.iter iter err_tbl; H.iter iter err_tbl;
reset () reset ()

6
infer/src/eradicate/typeErr.mli
Unescape View File

@ -81,10 +81,10 @@ type st_report_error =
val report_error : val report_error :
Tenv.t -> st_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 -> 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 val reset : unit -> unit

6
infer/src/harness/inhabit.ml
Unescape View File

@ -257,9 +257,9 @@ let setup_harness_cfg harness_name env cg cfg =
(create_node start_kind, create_node exit_kind) in (create_node start_kind, create_node exit_kind) in
Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node; Cfg.Procdesc.set_exit_node procdesc exit_node;
Cfg.Node.add_locals_ret_declaration start_node []; Cfg.Node.add_locals_ret_declaration procdesc start_node [];
Cfg.Node.set_succs_exn start_node [harness_node] [exit_node]; Cfg.Node.set_succs_exn procdesc start_node [harness_node] [exit_node];
Cfg.Node.set_succs_exn harness_node [exit_node] [exit_node]; Cfg.Node.set_succs_exn procdesc harness_node [exit_node] [exit_node];
add_harness_to_cg harness_name harness_node cg 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 (** create a procedure named harness_name that calls each of the methods in trace in the specified

8
infer/src/java/jFrontend.ml
Unescape View File

@ -48,7 +48,7 @@ let add_edges
if super_call then (fun _ -> exit_nodes) if super_call then (fun _ -> exit_nodes)
else JTransExn.create_exception_handlers context [exn_node] get_body_nodes impl in else JTransExn.create_exception_handlers context [exn_node] get_body_nodes impl in
let connect node pc = 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 = let connect_nodes pc translated_instruction =
match translated_instruction with match translated_instruction with
| JTrans.Skip -> () | JTrans.Skip -> ()
@ -57,7 +57,7 @@ let add_edges
connect node_true pc; connect node_true pc;
connect node_false pc connect node_false pc
| JTrans.Loop (join_node, node_true, node_false) -> | 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_true pc;
connect node_false pc in connect node_false pc in
let first_nodes = let first_nodes =
@ -65,11 +65,11 @@ let add_edges
direct_successors (-1) in direct_successors (-1) in
(* the exceptions edges here are going directly to the exit node *) (* 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 if not super_call then
(* the exceptions node is just before the exit node *) (* 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 Array.iteri connect_nodes method_body_nodes

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

@ -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 start_node = Cfg.Node.create Location.dummy start_kind [] procdesc in
let exit_kind = (Cfg.Node.Exit_node proc_name) in let exit_kind = (Cfg.Node.Exit_node proc_name) in
let exit_node = Cfg.Node.create Location.dummy exit_kind [] procdesc 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_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node; Cfg.Procdesc.set_exit_node procdesc exit_node;
procdesc 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; JContext.add_exn_node proc_name exn_node;
Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_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 procdesc in
Some procdesc Some procdesc
with JBir.Subroutine | JBasics.Class_structure_error _ -> with JBir.Subroutine | JBasics.Class_structure_error _ ->

6
infer/src/java/jTransExn.ml
Unescape View File

@ -91,8 +91,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let node_false = let node_false =
let instrs_false = [instr_call_instanceof; instr_prune_false] @ (if rethrow_exception then [instr_rethrow_exn] else []) in 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 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 procdesc node_true catch_nodes exit_nodes;
Cfg.Node.set_succs_exn node_false succ_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 let is_finally = handler.JBir.e_catch_type = None in
if is_finally if is_finally
then [node_true] (* TODO (#4759480): clean up the translation so prune nodes are not created at all *) 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 | n:: _ -> Cfg.Node.get_loc n
| [] -> Location.dummy in | [] -> Location.dummy in
let entry_node = create_entry_node loc 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.add catch_block_table handler_list [entry_node] in
Hashtbl.iter (fun _ handler_list -> create_entry_block handler_list) handler_table; Hashtbl.iter (fun _ handler_list -> create_entry_block handler_list) handler_table;
catch_block_table catch_block_table

2
infer/src/unit/analyzerTester.ml
Unescape View File

@ -176,7 +176,7 @@ module Make
let create_node kind cmds = let create_node kind cmds =
Cfg.Node.create dummy_loc kind cmds pdesc in Cfg.Node.create dummy_loc kind cmds pdesc in
let set_succs cur_node succs ~exn_handlers= 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_nodes_for_cond cond_exp if_kind =
let mk_prune_node cond_exp if_kind true_branch = let mk_prune_node cond_exp if_kind true_branch =
let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in

6
infer/src/unit/procCfgTests.ml
Unescape View File

@ -37,9 +37,9 @@ let tests =
Cfg.Procdesc.set_start_node test_pdesc n1; Cfg.Procdesc.set_start_node test_pdesc n1;
(* let -> represent normal transitions and -*-> represent exceptional transitions *) (* let -> represent normal transitions and -*-> represent exceptional transitions *)
(* creating graph n1 -> n2, n1 -*-> n3, n2 -> n4, n2 -*-> n3, n3 -> n4 , n3 -*> n4 *) (* 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 test_pdesc n1 [n2] [n3];
Cfg.Node.set_succs_exn n2 [n4] [n3]; Cfg.Node.set_succs_exn test_pdesc n2 [n4] [n3];
Cfg.Node.set_succs_exn n3 [n4] [n4]; Cfg.Node.set_succs_exn test_pdesc n3 [n4] [n4];
let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in
let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in

Write Preview
Loading…
Cancel
Save