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

Refactor the worklist data structures of the intraprocedural algorithm as non-global state.

Browse Source 
Summary:
public
The Worklist module currently encapsulates a global data structure. Likewise for the global variables for the join state and pathset todo and visited.
This diff refactors the Worklist module into an API where instances of the record can be created and passed around. All the global state is included in the record.
The Worklist data structure never escapes the Interproc module.

Reviewed By: sblackshear

Differential Revision: D2887674

fb-gh-sync-id: 65cb234
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-1
parent f4bbd44212
commit 7a7260635f
1 changed files with 154 additions and 181 deletions
Show Stats Download Patch File Download Diff File

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

@ -12,10 +12,14 @@
module L = Logging module L = Logging
module F = Format module F = Format
open Utils (* No abbreviation for Utils, as every module can depend on it *) open Utils
(** A node with a number of visits *)
type visitednode = type visitednode =
{ node: Cfg.Node.t; visits: int } {
node: Cfg.Node.t;
visits: int;
}
(** Set of nodes with number of visits *) (** Set of nodes with number of visits *)
module NodeVisitSet = module NodeVisitSet =
@ -41,30 +45,69 @@ module NodeVisitSet =
else compare_ids x1.node x2.node else compare_ids x1.node x2.node
end) end)
(** Table for the results of the join operation on nodes. *)
module Join_table : sig
type t
type node_id = int
val add : t -> node_id -> Paths.PathSet.t -> unit
val create : unit -> t
val find : t -> node_id -> Paths.PathSet.t
end = struct
type t = (int, Paths.PathSet.t) Hashtbl.t
type node_id = int
let create () : t =
Hashtbl.create 11
let find table i =
try Hashtbl.find table i with
| Not_found -> Paths.PathSet.empty
let add table i dset =
Hashtbl.replace table i dset
end
(* =============== START of module Worklist =============== *) (* =============== START of module Worklist =============== *)
module Worklist = struct module Worklist = struct
module NodeMap = Map.Make(Cfg.Node) module NodeMap = Map.Make(Cfg.Node)
let worklist : NodeVisitSet.t ref = ref NodeVisitSet.empty
let map : int NodeMap.t ref = ref NodeMap.empty
let reset pdesc = type node_id = int
worklist := NodeVisitSet.empty;
map := NodeMap.empty;
Cfg.Procdesc.compute_distance_to_exit_node pdesc
let is_empty () : bool = type t = {
NodeVisitSet.is_empty !worklist join_table : Join_table.t; (** Table of join results *)
path_set_todo : (node_id, Paths.PathSet.t) Hashtbl.t; (** Pathset todo *)
path_set_visited : (node_id, Paths.PathSet.t) Hashtbl.t; (** Pathset visited *)
mutable todo_set : NodeVisitSet.t; (** Set of nodes still to do, with visit count *)
mutable visit_map : node_id NodeMap.t; (** Map from nodes done to visit count *)
}
let add (node : Cfg.node) : unit = let create () = {
let visits = try NodeMap.find node !map with Not_found -> 0 in join_table = Join_table.create ();
worklist := NodeVisitSet.add { node = node; visits = visits } !worklist path_set_todo = Hashtbl.create 11;
path_set_visited = Hashtbl.create 11;
todo_set = NodeVisitSet.empty;
visit_map = NodeMap.empty;
}
let is_empty (wl : t) : bool =
NodeVisitSet.is_empty wl.todo_set
let add (wl : t) (node : Cfg.node) : unit =
let visits = (* recover visit count if it was visited before *)
try NodeMap.find node wl.visit_map with
| Not_found -> 0 in
wl.todo_set <- NodeVisitSet.add { node; visits } wl.todo_set
(** remove the minimum element from the worklist, and increase its number of visits *) (** remove the minimum element from the worklist, and increase its number of visits *)
let remove () : Cfg.Node.t = let remove (wl : t) : Cfg.Node.t =
try try
let min = NodeVisitSet.min_elt !worklist in let min = NodeVisitSet.min_elt wl.todo_set in
worklist := NodeVisitSet.remove min !worklist; wl.todo_set <-
map := NodeMap.add min.node (min.visits + 1) !map; (* increase the visits *) NodeVisitSet.remove min wl.todo_set;
wl.visit_map <-
NodeMap.add min.node (min.visits + 1) wl.visit_map; (* increase the visits *)
min.node min.node
with Not_found -> begin with Not_found -> begin
L.out "@\n...Work list is empty! Impossible to remove edge...@\n"; L.out "@\n...Work list is empty! Impossible to remove edge...@\n";
@ -73,28 +116,11 @@ module Worklist = struct
end end
(* =============== END of module Worklist =============== *) (* =============== END of module Worklist =============== *)
module Join_table : sig
val reset : unit -> unit
val find : int -> Paths.PathSet.t
val put : int -> Paths.PathSet.t -> unit
end = struct
let table : (int, Paths.PathSet.t) Hashtbl.t = Hashtbl.create 1024
let reset () = Hashtbl.clear table
let find i =
try Hashtbl.find table i with Not_found -> Paths.PathSet.empty
let put i dset = Hashtbl.replace table i dset
end
let path_set_visited : (int, Paths.PathSet.t) Hashtbl.t = Hashtbl.create 1024
let path_set_todo : (int, Paths.PathSet.t) Hashtbl.t = Hashtbl.create 1024
let path_set_worklist_reset pdesc = let path_set_create_worklist pdesc =
State.reset (); State.reset ();
Hashtbl.clear path_set_visited; Cfg.Procdesc.compute_distance_to_exit_node pdesc;
Hashtbl.clear path_set_todo; Worklist.create ()
Join_table.reset ();
Worklist.reset pdesc
let htable_retrieve (htable : (int, Paths.PathSet.t) Hashtbl.t) (key : int) : Paths.PathSet.t = let htable_retrieve (htable : (int, Paths.PathSet.t) Hashtbl.t) (key : int) : Paths.PathSet.t =
try try
@ -103,31 +129,28 @@ let htable_retrieve (htable : (int, Paths.PathSet.t) Hashtbl.t) (key : int) : Pa
Hashtbl.replace htable key Paths.PathSet.empty; Hashtbl.replace htable key Paths.PathSet.empty;
Paths.PathSet.empty Paths.PathSet.empty
let path_set_get_visited (sid: int) : Paths.PathSet.t =
htable_retrieve path_set_visited sid
(** Add [d] to the pathset todo at [node] returning true if changed *) (** Add [d] to the pathset todo at [node] returning true if changed *)
let path_set_put_todo (node: Cfg.node) (d: Paths.PathSet.t) : bool = let path_set_put_todo (wl : Worklist.t) (node: Cfg.node) (d: Paths.PathSet.t) : bool =
let changed = let changed =
if Paths.PathSet.is_empty d then false if Paths.PathSet.is_empty d then false
else else
let sid = Cfg.Node.get_id node in let node_id = Cfg.Node.get_id node in
let old_todo = htable_retrieve path_set_todo sid in let old_todo = htable_retrieve wl.Worklist.path_set_todo node_id in
let old_visited = htable_retrieve path_set_visited sid in let old_visited = htable_retrieve wl.Worklist.path_set_visited node_id in
let d' = Paths.PathSet.diff d old_visited in (* differential fixpoint *) let d' = Paths.PathSet.diff d old_visited in (* differential fixpoint *)
let todo_new = Paths.PathSet.union old_todo d' in let todo_new = Paths.PathSet.union old_todo d' in
Hashtbl.replace path_set_todo sid todo_new; Hashtbl.replace wl.Worklist.path_set_todo node_id todo_new;
not (Paths.PathSet.equal old_todo todo_new) in not (Paths.PathSet.equal old_todo todo_new) in
changed changed
let path_set_checkout_todo (node: Cfg.node) : Paths.PathSet.t = let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t =
try try
let sid = Cfg.Node.get_id node in let node_id = Cfg.Node.get_id node in
let todo = Hashtbl.find path_set_todo sid in let todo = Hashtbl.find wl.Worklist.path_set_todo node_id in
Hashtbl.replace path_set_todo sid Paths.PathSet.empty; Hashtbl.replace wl.Worklist.path_set_todo node_id Paths.PathSet.empty;
let visited = Hashtbl.find path_set_visited sid in let visited = Hashtbl.find wl.Worklist.path_set_visited node_id in
let new_visited = Paths.PathSet.union visited todo in let new_visited = Paths.PathSet.union visited todo in
Hashtbl.replace path_set_visited sid new_visited; Hashtbl.replace wl.Worklist.path_set_visited node_id new_visited;
todo todo
with Not_found -> with Not_found ->
L.out "@.@.ERROR: could not find todo for node %a@.@." Cfg.Node.pp node; L.out "@.@.ERROR: could not find todo for node %a@.@." Cfg.Node.pp node;
@ -135,49 +158,6 @@ let path_set_checkout_todo (node: Cfg.node) : Paths.PathSet.t =
(* =============== END of the edge_set object =============== *) (* =============== END of the edge_set object =============== *)
(* =============== START: Print a complete path in a dotty file =============== *)
let pp_path_dotty f path =
let count = ref 0 in
let prev_n_id = ref 0 in
let curr_n_id = ref 0 in
prev_n_id:=- 1;
let get_node_id_from_path p = match Paths.Path.curr_node p with
| Some node ->
Cfg.Node.get_id node
| None ->
!curr_n_id in
let g level p session exn_opt = match Paths.Path.curr_node p with
| Some curr_node ->
let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
let plist = Paths.PathSet.filter_path p curr_path_set in
incr count;
curr_n_id := get_node_id_from_path p;
Dotty.pp_dotty_prop_list_in_path f plist !prev_n_id !curr_n_id;
L.out "@.Path #%d: %a@." !count Paths.Path.pp p;
prev_n_id:=!curr_n_id
| None ->
() in
L.out "@.@.Printing Path: %a to file error_path.dot@." Paths.Path.pp path;
Dotty.reset_proposition_counter ();
Dotty.reset_dotty_spec_counter ();
F.fprintf f "@\n@\n@\ndigraph main { \nnode [shape=box]; @\n";
F.fprintf f "@\n compound = true; @\n";
(* F.fprintf f "@\n size=\"12,7\"; ratio=fill; @\n"; *)
Paths.Path.iter_longest_sequence g None path;
F.fprintf f "@\n}"
let pp_complete_path_dotty_file =
let counter = ref 0 in
fun path ->
incr counter;
let outc = open_out ("error_path" ^ string_of_int !counter ^ ".dot") in
let fmt = F.formatter_of_out_channel outc in
F.fprintf fmt "#### Dotty version: ####@.%a@.@." pp_path_dotty path;
close_out outc
(* =============== END: Print a complete path in a dotty file =============== *)
let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t = let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
if !Config.footprint then begin if !Config.footprint then begin
Config.footprint := false; Config.footprint := false;
@ -254,23 +234,28 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list
(* =============== START of symbolic execution =============== *) (* =============== START of symbolic execution =============== *)
(* propagate a set of results to the given node *) (** propagate a set of results to the given node *)
let propagate pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) = let propagate (wl : Worklist.t) pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) =
let edgeset_todo = let edgeset_todo =
let f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *) let f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *)
let exn_opt = let exn_opt =
if is_exception then Some (Tabulation.prop_get_exn_name pname prop) if is_exception
then Some (Tabulation.prop_get_exn_name pname prop)
else None in else None in
Paths.PathSet.add_renamed_prop prop (Paths.Path.extend curr_node exn_opt (State.get_session ()) path) edgeset_curr in Paths.PathSet.add_renamed_prop
prop
(Paths.Path.extend curr_node exn_opt (State.get_session ()) path)
edgeset_curr in
Paths.PathSet.fold f pset Paths.PathSet.empty in Paths.PathSet.fold f pset Paths.PathSet.empty in
let changed = path_set_put_todo curr_node edgeset_todo in let changed = path_set_put_todo wl curr_node edgeset_todo in
if changed then (Worklist.add curr_node) if changed then
Worklist.add wl curr_node
(* propagate a set of results, including exceptions and divergence *) (** propagate a set of results, including exceptions and divergence *)
let propagate_nodes_divergence let propagate_nodes_divergence
tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t) tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t)
(path: Paths.Path.t) (kind_curr_node : Cfg.Node.nodekind) (_succ_nodes: Cfg.node list) (path: Paths.Path.t) (kind_curr_node : Cfg.Node.nodekind) (_succ_nodes: Cfg.node list)
(exn_nodes: Cfg.node list) = (exn_nodes: Cfg.node list) (wl : Worklist.t) =
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
let succ_nodes = match State.get_goto_node () with (* handle Sil.Goto_node target, if any *) let succ_nodes = match State.get_goto_node () with (* handle Sil.Goto_node target, if any *)
@ -290,29 +275,29 @@ let propagate_nodes_divergence
Paths.PathSet.map mk_incons diverging_states in Paths.PathSet.map mk_incons diverging_states in
(L.d_strln_color Orange) "Propagating Divergence -- diverging states:"; (L.d_strln_color Orange) "Propagating Divergence -- diverging states:";
Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln (); Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln ();
propagate pname false prop_incons exit_node propagate wl pname false prop_incons exit_node
end; end;
IList.iter (propagate pname false pset_ok) succ_nodes; IList.iter (propagate wl pname false pset_ok) succ_nodes;
IList.iter (propagate pname true pset_exn) exn_nodes IList.iter (propagate wl pname true pset_exn) exn_nodes
(* ===================== END of symbolic execution ===================== *) (* ===================== END of symbolic execution ===================== *)
(* =============== START of forward_tabulate =============== *) (* =============== START of forward_tabulate =============== *)
(** Symbolic execution for a Join node *) (** Symbolic execution for a Join node *)
let do_symexec_join pname tenv 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_pdesc = Cfg.Node.get_proc_desc curr_node in
let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
let curr_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 curr_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 curr_pname tenv old_dset new_dset in
Join_table.put curr_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 ->
State.set_path path None; State.set_path path None;
propagate pname false (Paths.PathSet.from_renamed_list [(prop, path)]) node) propagate wl pname false (Paths.PathSet.from_renamed_list [(prop, path)]) node)
new_dset') succ_nodes new_dset') succ_nodes
let prop_max_size = ref (0, Prop.prop_emp) let prop_max_size = ref (0, Prop.prop_emp)
@ -335,30 +320,6 @@ let reset_prop_metrics () =
prop_max_size := (0, Prop.prop_emp); prop_max_size := (0, Prop.prop_emp);
prop_max_chain_size := (0, Prop.prop_emp) prop_max_chain_size := (0, Prop.prop_emp)
(** dump a path *)
let d_path (path, pos_opt) =
let step = ref 0 in
let prop_last_step = ref Prop.prop_emp in (* if the last step had a singleton prop, store it here *)
let f level p session exn_opt = match Paths.Path.curr_node p with
| Some curr_node ->
let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
let plist = Paths.PathSet.filter_path p curr_path_set in
incr step;
(* Propset.pp_proplist_dotty_file ("path" ^ (string_of_int !count) ^ ".dot") plist; *)
L.d_strln ("Path Step #" ^ string_of_int !step ^
" node " ^ string_of_int (Cfg.Node.get_id curr_node) ^
" session " ^ string_of_int session ^ ":");
Propset.d !prop_last_step (Propset.from_proplist plist); L.d_ln ();
Cfg.Node.d_instrs true None curr_node; L.d_ln (); L.d_ln ();
prop_last_step := (match plist with | [prop] -> prop | _ -> Prop.prop_emp)
| None ->
() in
L.d_str "Path: "; Paths.Path.d_stats path; L.d_ln ();
Paths.Path.d path; L.d_ln ();
(* pp_complete_path_dotty_file path; *)
(* if !Config.write_dotty then Dotty.print_icfg_dotty (IList.rev (get_edges path)) *)
Paths.Path.iter_longest_sequence f pos_opt path
exception RE_EXE_ERROR exception RE_EXE_ERROR
let do_before_node session node = let do_before_node session node =
@ -506,13 +467,15 @@ let do_symbolic_execution handle_exn cfg tenv
pset pset
let mark_visited summary node = let mark_visited summary node =
let id = Cfg.Node.get_id node in let node_id = Cfg.Node.get_id node in
let stats = summary.Specs.stats in let stats = summary.Specs.stats in
if !Config.footprint if !Config.footprint
then stats.Specs.nodes_visited_fp <- IntSet.add id stats.Specs.nodes_visited_fp then
else stats.Specs.nodes_visited_re <- IntSet.add id stats.Specs.nodes_visited_re stats.Specs.nodes_visited_fp <- IntSet.add node_id stats.Specs.nodes_visited_fp
else
stats.Specs.nodes_visited_re <- IntSet.add node_id stats.Specs.nodes_visited_re
let forward_tabulate cfg tenv = let forward_tabulate cfg tenv wl =
let handled_some_exception = ref false in let handled_some_exception = ref false in
let handle_exn curr_node exn = let handle_exn curr_node exn =
let curr_pdesc = Cfg.Node.get_proc_desc curr_node in let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
@ -530,10 +493,10 @@ let forward_tabulate cfg tenv =
State.mark_instr_fail pre_opt exn; State.mark_instr_fail pre_opt exn;
handled_some_exception := true in handled_some_exception := true in
while not (Worklist.is_empty ()) do while not (Worklist.is_empty wl) do
let curr_node = Worklist.remove () in let curr_node = Worklist.remove wl in
let kind_curr_node = Cfg.Node.get_kind curr_node in let curr_node_kind = Cfg.Node.get_kind curr_node in
let sid_curr_node = Cfg.Node.get_id curr_node in let curr_node_id = Cfg.Node.get_id curr_node in
let proc_desc = Cfg.Node.get_proc_desc curr_node in let proc_desc = Cfg.Node.get_proc_desc curr_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 formal_params = Cfg.Procdesc.get_formals proc_desc in let formal_params = Cfg.Procdesc.get_formals proc_desc in
@ -543,7 +506,7 @@ let forward_tabulate cfg tenv =
incr summary.Specs.sessions; incr summary.Specs.sessions;
!(summary.Specs.sessions) in !(summary.Specs.sessions) in
do_before_node session curr_node; do_before_node session curr_node;
let pathset_todo = path_set_checkout_todo curr_node in let pathset_todo = path_set_checkout_todo wl curr_node 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
let exe_iter f pathset = let exe_iter f pathset =
@ -563,7 +526,7 @@ let forward_tabulate cfg tenv =
handled_some_exception := false; handled_some_exception := false;
check_prop_size pathset_todo; check_prop_size pathset_todo;
L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^ L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^
"Node: " ^ string_of_int sid_curr_node ^ ", " ^ "Node: " ^ string_of_int curr_node_id ^ ", " ^
"Procedure: " ^ Procname.to_string proc_name ^ ", " ^ "Procedure: " ^ Procname.to_string proc_name ^ ", " ^
"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) ^ " ****");
@ -573,8 +536,9 @@ let forward_tabulate cfg tenv =
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 (); L.d_ln (); L.d_ln ();
match kind_curr_node with match curr_node_kind with
| Cfg.Node.Join_node -> do_symexec_join proc_name tenv curr_node pathset_todo | Cfg.Node.Join_node ->
do_symexec_join proc_name 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 _
@ -587,23 +551,30 @@ let forward_tabulate cfg tenv =
let tainted_params = Taint.tainted_params proc_name in let tainted_params = Taint.tainted_params proc_name in
Tabulation.add_param_taint proc_name formal_params prop tainted_params Tabulation.add_param_taint proc_name formal_params prop tainted_params
else prop in else prop in
L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths); L.d_strln
("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths);
L.d_increase_indent 1; L.d_increase_indent 1;
State.reset_diverging_states_goto_node (); State.reset_diverging_states_goto_node ();
let pset = let pset =
do_symbolic_execution (handle_exn curr_node) cfg tenv curr_node prop path in do_symbolic_execution (handle_exn curr_node) cfg tenv curr_node prop path in
L.d_decrease_indent 1; L.d_ln(); L.d_decrease_indent 1; L.d_ln();
propagate_nodes_divergence tenv proc_desc pset path kind_curr_node succ_nodes exn_nodes; propagate_nodes_divergence
with exn when Exceptions.handle_exception exn && !Config.footprint -> tenv proc_desc pset path curr_node_kind succ_nodes exn_nodes wl;
handle_exn curr_node exn; with
if !Config.nonstop then propagate_nodes_divergence tenv proc_desc (Paths.PathSet.from_renamed_list [(prop, path)]) path kind_curr_node succ_nodes exn_nodes; | exn when Exceptions.handle_exception exn && !Config.footprint ->
L.d_decrease_indent 1; L.d_ln ()) handle_exn curr_node exn;
if !Config.nonstop then
propagate_nodes_divergence
tenv proc_desc (Paths.PathSet.from_renamed_list [(prop, path)])
path curr_node_kind succ_nodes exn_nodes wl;
L.d_decrease_indent 1; L.d_ln ())
pathset_todo in pathset_todo in
try begin try
doit(); begin
if !handled_some_exception then Printer.force_delayed_prints (); doit();
do_after_node curr_node if !handled_some_exception then Printer.force_delayed_prints ();
end do_after_node curr_node
end
with with
| exn when Exceptions.handle_exception exn -> | exn when Exceptions.handle_exception exn ->
handle_exn curr_node exn; handle_exn curr_node exn;
@ -669,10 +640,10 @@ let remove_locals_formals_and_check pdesc p =
p' p'
(* Collect the analysis results for the exit node *) (* Collect the analysis results for the exit node *)
let collect_analysis_result pdesc : Paths.PathSet.t = let collect_analysis_result wl pdesc : Paths.PathSet.t =
let exit_node = Cfg.Procdesc.get_exit_node pdesc in let exit_node = Cfg.Procdesc.get_exit_node pdesc in
let exit_sid = Cfg.Node.get_id exit_node in let exit_node_id = Cfg.Node.get_id exit_node in
let pathset = path_set_get_visited exit_sid in let pathset = htable_retrieve wl.Worklist.path_set_visited exit_node_id in
Paths.PathSet.map (remove_locals_formals_and_check pdesc) pathset Paths.PathSet.map (remove_locals_formals_and_check pdesc) pathset
module Pmap = Map.Make (struct type t = Prop.normal Prop.t let compare = Prop.prop_compare end) module Pmap = Map.Make (struct type t = Prop.normal Prop.t let compare = Prop.prop_compare end)
@ -745,9 +716,9 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
Pmap.iter add_spec pre_post_map; Pmap.iter add_spec pre_post_map;
!specs !specs
let collect_postconditions tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t = let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t =
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let pathset = collect_analysis_result pdesc in let pathset = collect_analysis_result wl pdesc in
L.d_strln ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Analysis result ####"); L.d_strln ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Analysis result ####");
Propset.d Prop.prop_emp (Paths.PathSet.to_propset pathset); Propset.d Prop.prop_emp (Paths.PathSet.to_propset pathset);
L.d_ln (); L.d_ln ();
@ -832,7 +803,7 @@ let initial_prop_from_pre tenv curr_f pre =
initial_prop tenv curr_f pre false initial_prop tenv curr_f pre false
(** 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 cfg tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t) let execute_filter_prop wl cfg tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t)
: Prop.normal Specs.spec option = : Prop.normal Specs.spec option =
let proc_name = Cfg.Procdesc.get_proc_name pdesc in let proc_name = Cfg.Procdesc.get_proc_name pdesc in
do_before_node 0 init_node; do_before_node 0 init_node;
@ -844,17 +815,16 @@ let execute_filter_prop cfg tenv pdesc init_node (precondition : Prop.normal Spe
let init_edgeset = Paths.PathSet.add_renamed_prop init_prop (Paths.Path.start init_node) Paths.PathSet.empty in let init_edgeset = Paths.PathSet.add_renamed_prop init_prop (Paths.Path.start init_node) Paths.PathSet.empty in
do_after_node init_node; do_after_node init_node;
try try
path_set_worklist_reset pdesc; Worklist.add wl init_node;
Worklist.add init_node; ignore (path_set_put_todo wl init_node init_edgeset);
ignore (path_set_put_todo init_node init_edgeset); forward_tabulate cfg tenv wl;
forward_tabulate cfg tenv;
do_before_node 0 init_node; do_before_node 0 init_node;
L.d_strln_color Green ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####"); L.d_strln_color Green ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
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 ();
let posts, visited = let posts, visited =
let pset, visited = collect_postconditions tenv pdesc in let pset, visited = collect_postconditions wl tenv pdesc in
let plist = IList.map (fun (p, path) -> (Cfg.remove_seed_vars p, path)) (Paths.PathSet.elements pset) in let plist = IList.map (fun (p, path) -> (Cfg.remove_seed_vars p, path)) (Paths.PathSet.elements pset) in
plist, visited in plist, visited in
let pre = let pre =
@ -882,10 +852,12 @@ let execute_filter_prop cfg tenv pdesc init_node (precondition : Prop.normal Spe
let get_procs_and_defined_children call_graph = let get_procs_and_defined_children call_graph =
IList.map (fun (n, ns) -> (n, Procname.Set.elements ns)) (Cg.get_nodes_and_defined_children call_graph) IList.map (fun (n, ns) -> (n, Procname.Set.elements ns)) (Cg.get_nodes_and_defined_children call_graph)
let pp_intra_stats cfg proc_desc fmt proc_name = let pp_intra_stats wl cfg proc_desc fmt proc_name =
let nstates = ref 0 in let nstates = ref 0 in
let nodes = Cfg.Procdesc.get_nodes proc_desc in let nodes = Cfg.Procdesc.get_nodes proc_desc in
IList.iter (fun node -> nstates := !nstates + Paths.PathSet.size (path_set_get_visited (Cfg.Node.get_id node))) nodes; IList.iter (fun node ->
nstates := !nstates + Paths.PathSet.size
(htable_retrieve wl.Worklist.path_set_visited (Cfg.Node.get_id node))) 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
(** Return functions to perform one phase of the analysis for a procedure. (** Return functions to perform one phase of the analysis for a procedure.
@ -907,7 +879,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
end in end in
let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
let go () = 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
let init_props_from_pres = (* use existing pre's (in recursion some might exist) as starting points *) let init_props_from_pres = (* use existing pre's (in recursion some might exist) as starting points *)
let specs = Specs.get_specs pname in let specs = Specs.get_specs pname in
@ -924,20 +896,19 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
L.d_strln "initial props ="; L.d_strln "initial props =";
Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln(); Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln();
L.d_decrease_indent 1; L.d_decrease_indent 1;
path_set_worklist_reset pdesc;
check_recursion_level (); check_recursion_level ();
Worklist.add start_node; Worklist.add wl start_node;
Config.arc_mode := Hashtbl.mem (Cfg.Procdesc.get_flags pdesc) Mleak_buckets.objc_arc_flag; Config.arc_mode := Hashtbl.mem (Cfg.Procdesc.get_flags pdesc) Mleak_buckets.objc_arc_flag;
ignore (path_set_put_todo start_node init_edgeset); ignore (path_set_put_todo wl start_node init_edgeset);
forward_tabulate cfg tenv; forward_tabulate cfg tenv wl
in in
let get_results () = 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 pdesc in let results = collect_analysis_result wl pdesc in
L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname; L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname;
L.out "#### Finished: Footprint Computation for %a %a ####@." L.out "#### Finished: Footprint Computation for %a %a ####@."
Procname.pp pname Procname.pp pname
(pp_intra_stats cfg pdesc) pname; (pp_intra_stats wl cfg pdesc) pname;
L.out "#### [FUNCTION %a] Footprint Analysis result ####@\n%a@." L.out "#### [FUNCTION %a] Footprint Analysis result ####@\n%a@."
Procname.pp pname Procname.pp pname
(Paths.PathSet.pp pe_text) results; (Paths.PathSet.pp pe_text) results;
@ -950,7 +921,8 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
Reporting.log_error pname ~pre: pre_opt exn; Reporting.log_error pname ~pre: pre_opt exn;
[] (* retuning no specs *) in [] (* retuning no specs *) in
specs, Specs.FOOTPRINT in specs, Specs.FOOTPRINT in
go, get_results in let wl = path_set_create_worklist pdesc in
go wl, get_results wl in
let re_execution proc_name let re_execution proc_name
: (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
@ -960,7 +932,8 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp proc_name; L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp proc_name;
check_recursion_level (); check_recursion_level ();
let filter p = let filter p =
let speco = execute_filter_prop cfg tenv pdesc start_node p in let wl = path_set_create_worklist pdesc in
let speco = execute_filter_prop wl cfg tenv pdesc start_node p in
let is_valid = match speco with let is_valid = match speco with
| None -> false | None -> false
| Some spec -> | Some spec ->
@ -969,7 +942,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
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 cfg pdesc) proc_name (pp_intra_stats wl cfg pdesc) proc_name
outcome; outcome;
speco in speco in
if !Config.undo_join then if !Config.undo_join then

Write Preview
Loading…
Cancel
Save