You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
1351 lines
61 KiB
1351 lines
61 KiB
(*
|
|
* Copyright (c) 2009 - 2013 Monoidics ltd.
|
|
* Copyright (c) 2013 - present Facebook, Inc.
|
|
* All rights reserved.
|
|
*
|
|
* This source code is licensed under the BSD style license found in the
|
|
* LICENSE file in the root directory of this source tree. An additional grant
|
|
* of patent rights can be found in the PATENTS file in the same directory.
|
|
*)
|
|
|
|
(** Interprocedural Analysis *)
|
|
|
|
module L = Logging
|
|
module F = Format
|
|
open Utils (* No abbreviation for Utils, as every module can depend on it *)
|
|
|
|
type visitednode =
|
|
{ node: Cfg.Node.t; visits: int }
|
|
|
|
(** Set of nodes with number of visits *)
|
|
module NodeVisitSet =
|
|
Set.Make(struct
|
|
type t = visitednode
|
|
let compare_ids n1 n2 = Cfg.Node.compare n2 n1 (* higher id is better *)
|
|
let compare_distance_to_exit { node = n1 } { node = n2 } = (* smaller means higher priority *)
|
|
let n = match Cfg.Node.get_distance_to_exit n1, Cfg.Node.get_distance_to_exit n2 with
|
|
| None, None -> 0
|
|
| None, Some _ -> 1
|
|
| Some _, None -> - 1
|
|
| Some d1, Some d2 -> int_compare d1 d2 (* shorter distance to exit is better *) in
|
|
if n <> 0 then n else compare_ids n1 n2
|
|
let compare_number_of_visits x1 x2 =
|
|
let n = int_compare x1.visits x2.visits in (* visited fewer times is better *)
|
|
if n <> 0 then n else compare_distance_to_exit x1 x2
|
|
let compare x1 x2 =
|
|
if !Config.footprint then
|
|
match !Config.worklist_mode with
|
|
| 0 -> compare_ids x1.node x2.node
|
|
| 1 -> compare_distance_to_exit x1 x2
|
|
| _ -> compare_number_of_visits x1 x2
|
|
else compare_ids x1.node x2.node
|
|
end)
|
|
|
|
(* =============== START of module Worklist =============== *)
|
|
module Worklist = struct
|
|
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 =
|
|
worklist := NodeVisitSet.empty;
|
|
map := NodeMap.empty;
|
|
Cfg.Procdesc.compute_distance_to_exit_node pdesc
|
|
|
|
let is_empty () : bool =
|
|
NodeVisitSet.is_empty !worklist
|
|
|
|
let add (node : Cfg.node) : unit =
|
|
let visits = try NodeMap.find node !map with Not_found -> 0 in
|
|
worklist := NodeVisitSet.add { node = node; visits = visits } !worklist
|
|
|
|
(** remove the minimum element from the worklist, and increase its number of visits *)
|
|
let remove () : Cfg.Node.t =
|
|
try
|
|
let min = NodeVisitSet.min_elt !worklist in
|
|
worklist := NodeVisitSet.remove min !worklist;
|
|
map := NodeMap.add min.node (min.visits + 1) !map; (* increase the visits *)
|
|
min.node
|
|
with Not_found -> begin
|
|
L.out "@\n...Work list is empty! Impossible to remove edge...@\n";
|
|
assert false
|
|
end
|
|
end
|
|
(* =============== 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 =
|
|
State.reset ();
|
|
Hashtbl.clear path_set_visited;
|
|
Hashtbl.clear path_set_todo;
|
|
Join_table.reset ();
|
|
Worklist.reset pdesc
|
|
|
|
let htable_retrieve (htable : (int, Paths.PathSet.t) Hashtbl.t) (key : int) : Paths.PathSet.t =
|
|
try
|
|
Hashtbl.find htable key
|
|
with Not_found ->
|
|
Hashtbl.replace htable key 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 *)
|
|
let path_set_put_todo (node: Cfg.node) (d: Paths.PathSet.t) : bool =
|
|
let changed =
|
|
if Paths.PathSet.is_empty d then false
|
|
else
|
|
let sid = Cfg.Node.get_id node in
|
|
let old_todo = htable_retrieve path_set_todo sid in
|
|
let old_visited = htable_retrieve path_set_visited sid in
|
|
let d' = Paths.PathSet.diff d old_visited in (* differential fixpoint *)
|
|
let todo_new = Paths.PathSet.union old_todo d' in
|
|
Hashtbl.replace path_set_todo sid todo_new;
|
|
not (Paths.PathSet.equal old_todo todo_new) in
|
|
changed
|
|
|
|
let path_set_checkout_todo (node: Cfg.node) : Paths.PathSet.t =
|
|
try
|
|
let sid = Cfg.Node.get_id node in
|
|
let todo = Hashtbl.find path_set_todo sid in
|
|
Hashtbl.replace path_set_todo sid Paths.PathSet.empty;
|
|
let visited = Hashtbl.find path_set_visited sid in
|
|
let new_visited = Paths.PathSet.union visited todo in
|
|
Hashtbl.replace path_set_visited sid new_visited;
|
|
todo
|
|
with Not_found ->
|
|
L.out "@.@.ERROR: could not find todo for node %a@.@." Cfg.Node.pp node;
|
|
assert false
|
|
|
|
(* =============== END of the edge_set object =============== *)
|
|
|
|
(* =============== START: Print a complete path in a dotty file =============== *)
|
|
|
|
let pp_path_dotty f path =
|
|
let get_node_id_from_path p =
|
|
let node = Paths.Path.curr_node p in
|
|
Cfg.Node.get_id node in
|
|
let count = ref 0 in
|
|
let prev_n_id = ref 0 in
|
|
let curr_n_id = ref 0 in
|
|
prev_n_id:=- 1;
|
|
let g level p session exn_opt =
|
|
let curr_node = Paths.Path.curr_node p in
|
|
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 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 =
|
|
if !Config.footprint then begin
|
|
Config.footprint := false;
|
|
let pset' = Abs.lifted_abstract pname tenv pset in
|
|
Config.footprint := true;
|
|
pset'
|
|
end
|
|
else Abs.lifted_abstract pname tenv pset
|
|
|
|
let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.PathSet.t =
|
|
let abs_option p =
|
|
if Prover.check_inconsistency p then None
|
|
else Some (Abs.abstract pname tenv p) in
|
|
if !Config.footprint then begin
|
|
Config.footprint := false;
|
|
let pathset' = Paths.PathSet.map_option abs_option pathset in
|
|
Config.footprint := true;
|
|
pathset'
|
|
end
|
|
else Paths.PathSet.map_option abs_option pathset
|
|
|
|
let do_join_pre plist =
|
|
Dom.proplist_collapse_pre plist
|
|
|
|
let do_join_post pname tenv (pset: Paths.PathSet.t) =
|
|
if !Config.spec_abs_level <= 0 then
|
|
Dom.pathset_collapse pset
|
|
else
|
|
Dom.pathset_collapse (Dom.pathset_collapse_impl pname tenv pset)
|
|
|
|
let do_meet_pre pset =
|
|
if !Config.meet_level > 0 then
|
|
Dom.propset_meet_generate_pre pset
|
|
else
|
|
Propset.to_proplist pset
|
|
|
|
(** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *)
|
|
let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list =
|
|
let collect_do_abstract_one tenv prop =
|
|
if !Config.footprint then begin
|
|
Config.footprint := false;
|
|
let prop' = Abs.abstract_no_symop tenv prop in
|
|
Config.footprint := true;
|
|
prop' end
|
|
else Abs.abstract_no_symop tenv prop in
|
|
let pres = list_map (fun spec -> Specs.Jprop.to_prop spec.Specs.pre) (Specs.get_specs proc_name) in
|
|
let pset = Propset.from_proplist pres in
|
|
let pset' =
|
|
let f p = Prop.prop_normal_vars_to_primed_vars p in
|
|
Propset.map f pset in
|
|
|
|
L.d_strln ("#### Extracted footprint of " ^ Procname.to_string proc_name ^ ": ####");
|
|
L.d_increase_indent 1; Propset.d Prop.prop_emp pset'; L.d_decrease_indent 1; L.d_ln ();
|
|
L.d_ln ();
|
|
let pset'' = collect_do_abstract_pre pname tenv pset' in
|
|
let plist_meet = do_meet_pre pset'' in
|
|
L.d_strln ("#### Footprint of " ^ Procname.to_string proc_name ^ " after Meet ####");
|
|
L.d_increase_indent 1; Propgraph.d_proplist Prop.prop_emp plist_meet; L.d_decrease_indent 1; L.d_ln ();
|
|
L.d_ln ();
|
|
L.d_increase_indent 2; (* Indent for the join output *)
|
|
let jplist = do_join_pre plist_meet in
|
|
L.d_decrease_indent 2; L.d_ln ();
|
|
L.d_strln ("#### Footprint of " ^ Procname.to_string proc_name ^ " after Join ####");
|
|
L.d_increase_indent 1; Specs.Jprop.d_list false jplist; L.d_decrease_indent 1; L.d_ln ();
|
|
let jplist' = list_map (Specs.Jprop.map Prop.prop_rename_primed_footprint_vars) jplist in
|
|
L.d_strln ("#### Renamed footprint of " ^ Procname.to_string proc_name ^ ": ####");
|
|
L.d_increase_indent 1; Specs.Jprop.d_list false jplist'; L.d_decrease_indent 1; L.d_ln ();
|
|
let jplist'' =
|
|
let f p = Prop.prop_primed_vars_to_normal_vars (collect_do_abstract_one pname tenv p) in
|
|
list_map (Specs.Jprop.map f) jplist' in
|
|
L.d_strln ("#### Abstracted footprint of " ^ Procname.to_string proc_name ^ ": ####");
|
|
L.d_increase_indent 1; Specs.Jprop.d_list false jplist''; L.d_decrease_indent 1; L.d_ln();
|
|
jplist''
|
|
|
|
(* =============== START of symbolic execution =============== *)
|
|
|
|
(* propagate a set of results to the given node *)
|
|
let propagate pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) =
|
|
let edgeset_todo =
|
|
let f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *)
|
|
let exn_opt =
|
|
if is_exception then Some (Tabulation.prop_get_exn_name pname prop)
|
|
else None in
|
|
Paths.PathSet.add_renamed_prop prop (Paths.Path.extend curr_node exn_opt (State.get_session ()) path) edgeset_curr in
|
|
Paths.PathSet.fold f pset Paths.PathSet.empty in
|
|
let changed = path_set_put_todo curr_node edgeset_todo in
|
|
if changed then (Worklist.add curr_node)
|
|
|
|
(* propagate a set of results, including exceptions and divergence *)
|
|
let propagate_nodes_divergence
|
|
tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t)
|
|
(path: Paths.Path.t) (kind_curr_node : Cfg.Node.nodekind) (_succ_nodes: Cfg.node list)
|
|
(exn_nodes: Cfg.node list) =
|
|
let pname = Cfg.Procdesc.get_proc_name pdesc in
|
|
let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
|
|
let succ_nodes = match State.get_goto_node () with (* handle Sil.Goto_node target, if any *)
|
|
| Some node_id ->
|
|
list_filter (fun n -> Cfg.Node.get_id n = node_id) _succ_nodes
|
|
| None -> _succ_nodes in
|
|
if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then
|
|
begin
|
|
if !Config.developer_mode then Errdesc.warning_err (State.get_loc ()) "Propagating Divergence@.";
|
|
let exit_node = Cfg.Procdesc.get_exit_node pdesc in
|
|
let diverging_states = State.get_diverging_states_node () in
|
|
let prop_incons =
|
|
let mk_incons prop =
|
|
let p_abs = Abs.abstract pname tenv prop in
|
|
let p_zero = Prop.replace_sigma [] (Prop.replace_sub Sil.sub_empty p_abs) in
|
|
Prop.normalize (Prop.replace_pi [Sil.Aneq (Sil.exp_zero, Sil.exp_zero)] p_zero) in
|
|
Paths.PathSet.map mk_incons diverging_states in
|
|
(L.d_strln_color Orange) "Propagating Divergence -- diverging states:";
|
|
Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln ();
|
|
propagate pname false prop_incons exit_node
|
|
end;
|
|
list_iter (propagate pname false pset_ok) succ_nodes;
|
|
list_iter (propagate pname true pset_exn) exn_nodes
|
|
|
|
(* ===================== END of symbolic execution ===================== *)
|
|
|
|
(* =============== START of forward_tabulate =============== *)
|
|
|
|
(** Symbolic execution for a Join node *)
|
|
let do_symexec_join pname tenv curr_node (edgeset_todo : Paths.PathSet.t) =
|
|
let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
|
|
let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
|
|
let curr_id = Cfg.Node.get_id curr_node in
|
|
let succ_nodes = Cfg.Node.get_succs curr_node in
|
|
let new_dset = edgeset_todo in
|
|
let old_dset = Join_table.find curr_id 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');
|
|
list_iter (fun node ->
|
|
Paths.PathSet.iter (fun prop path ->
|
|
State.set_path path None;
|
|
propagate pname false (Paths.PathSet.from_renamed_list [(prop, path)]) node)
|
|
new_dset') succ_nodes
|
|
|
|
let prop_max_size = ref (0, Prop.prop_emp)
|
|
let prop_max_chain_size = ref (0, Prop.prop_emp)
|
|
|
|
(* Check if the prop exceeds the current max *)
|
|
let check_prop_size p path =
|
|
let size = Prop.Metrics.prop_size p in
|
|
if size > fst !prop_max_size then
|
|
(prop_max_size := (size, p);
|
|
L.d_strln ("Prop with new max size " ^ string_of_int size ^ ":");
|
|
Prop.d_prop p;
|
|
L.d_ln ())
|
|
|
|
(* Check prop size and filter out possible unabstracted lists *)
|
|
let check_prop_size edgeset_todo =
|
|
if !Config.monitor_prop_size then Paths.PathSet.iter check_prop_size edgeset_todo
|
|
|
|
let reset_prop_metrics () =
|
|
prop_max_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 =
|
|
let curr_node = Paths.Path.curr_node p in
|
|
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) 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 (list_rev (get_edges path)) *)
|
|
Paths.Path.iter_longest_sequence f pos_opt path
|
|
|
|
exception RE_EXE_ERROR
|
|
|
|
let do_before_node session node =
|
|
let loc = Cfg.Node.get_loc node in
|
|
let proc_desc = Cfg.Node.get_proc_desc node in
|
|
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
|
|
State.set_node node;
|
|
State.set_session session;
|
|
L.reset_delayed_prints ();
|
|
Printer.start_session node loc proc_name session
|
|
|
|
let do_after_node node = Printer.finish_session node
|
|
|
|
(** Return the list of normal ids occurring in the instructions *)
|
|
let instrs_get_normal_vars instrs =
|
|
let fav = Sil.fav_new () in
|
|
let do_instr instr =
|
|
let do_e e = Sil.exp_fav_add fav e in
|
|
let exps = Sil.instr_get_exps instr in
|
|
list_iter do_e exps in
|
|
list_iter do_instr instrs;
|
|
Sil.fav_filter_ident fav Ident.is_normal;
|
|
Sil.fav_to_list fav
|
|
|
|
(* checks that boolean conditions on a conditional are assignment *)
|
|
(* The check is done as follows: we check that the successors or a node that make an *)
|
|
(* set instruction are prune nodes, they are all at the same location and the condition on*)
|
|
(* which they prune is the variable (or the negation) which was set in the set instruction *)
|
|
(* we exclude function calls: if (g(x,y)) ....*)
|
|
(* we check that prune nodes have simple guards: a var or its negation*)
|
|
let check_assignement_guard node =
|
|
let pdesc = Cfg.Node.get_proc_desc node in
|
|
let pname = Cfg.Procdesc.get_proc_name pdesc in
|
|
let verbose = false in
|
|
let node_contains_call n =
|
|
let instrs = Cfg.Node.get_instrs n in
|
|
let is_call = function
|
|
| Sil.Call _ -> true
|
|
| _ -> false in
|
|
list_exists is_call instrs in
|
|
let is_set_instr i =
|
|
match i with
|
|
| Sil.Set _ -> true
|
|
| _ -> false in
|
|
let is_prune_instr i =
|
|
match i with
|
|
| Sil.Prune _ -> true
|
|
| _ -> false in
|
|
let is_letderef_instr i =
|
|
match i with
|
|
| Sil.Letderef _ -> true
|
|
| _ -> false in
|
|
let is_cil_tmp e =
|
|
match e with
|
|
| Sil.Lvar pv ->
|
|
Errdesc.pvar_is_cil_tmp pv
|
|
| _ -> false in
|
|
let is_edg_tmp e =
|
|
match e with
|
|
| Sil.Lvar pv ->
|
|
Errdesc.pvar_is_edg_tmp pv
|
|
| _ -> false in
|
|
let succs = Cfg.Node.get_succs node in
|
|
let l_node = Cfg.Node.get_last_loc node in
|
|
(* e is prune if in all successors prune nodes we have for some temp n$1: *)
|
|
(* n$1=*&e;Prune(n$1) or n$1=*&e;Prune(!n$1) *)
|
|
let is_prune_exp e =
|
|
let prune_var n =
|
|
let ins = Cfg.Node.get_instrs n in
|
|
let pi = list_filter is_prune_instr ins in
|
|
let leti = list_filter is_letderef_instr ins in
|
|
match pi, leti with
|
|
| [Sil.Prune (Sil.Var(e1), _, _, _)], [Sil.Letderef(e2, e', _, _)]
|
|
| [Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var(e1), _), _, _, _)], [Sil.Letderef(e2, e', _, _)] when (Ident.equal e1 e2) ->
|
|
if verbose then L.d_strln ("Found "^(Sil.exp_to_string e')^" as prune var");
|
|
[e']
|
|
| _ -> [] in
|
|
let prune_vars = list_flatten(list_map (fun n -> prune_var n) succs) in
|
|
list_for_all (fun e' -> Sil.exp_equal e' e) prune_vars in
|
|
let succs_loc = list_map (fun n -> Cfg.Node.get_loc n) succs in
|
|
let succs_are_all_prune_nodes () =
|
|
list_for_all (fun n -> match Cfg.Node.get_kind n with
|
|
| Cfg.Node.Prune_node(_) -> true
|
|
| _ -> false) succs in
|
|
let succs_same_loc_as_node () =
|
|
if verbose then
|
|
(L.d_str ("LOCATION NODE: line: " ^ (string_of_int l_node.Location.line) ^
|
|
" nLOC: " ^ (string_of_int l_node.Location.nLOC));
|
|
L.d_strln " ");
|
|
list_for_all (fun l ->
|
|
if verbose then
|
|
(L.d_str ("LOCATION l: line: " ^ (string_of_int l.Location.line) ^
|
|
" nLOC: " ^ (string_of_int l.Location.nLOC));
|
|
L.d_strln " ");
|
|
Location.equal l l_node) succs_loc in
|
|
let succs_have_simple_guards () = (* check that the guards of the succs are a var or its negation *)
|
|
let check_instr = function
|
|
| Sil.Prune (Sil.Var _, _, _, _) -> true
|
|
| Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var _, _), _, _, _) -> true
|
|
| Sil.Prune _ -> false
|
|
| _ -> true in
|
|
let check_guard n =
|
|
list_for_all check_instr (Cfg.Node.get_instrs n) in
|
|
list_for_all check_guard succs in
|
|
if !Config.curr_language = Config.C_CPP &&
|
|
succs_are_all_prune_nodes () &&
|
|
succs_same_loc_as_node () &&
|
|
succs_have_simple_guards () then
|
|
(let instr = Cfg.Node.get_instrs node in
|
|
match succs_loc with
|
|
| loc_succ:: _ -> (* at this point all successors are at the same location, so we can take the first*)
|
|
let set_instr_at_succs_loc =
|
|
list_filter
|
|
(fun i -> (Location.equal (Sil.instr_get_loc i) loc_succ) && is_set_instr i)
|
|
instr in
|
|
(match set_instr_at_succs_loc with
|
|
| [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*)
|
|
if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) && not (is_edg_tmp e) then (
|
|
let desc = Errdesc.explain_condition_is_assignment l_node in
|
|
let exn = Exceptions.Condition_is_assignment (desc, try assert false with Assert_failure x -> x) in
|
|
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
|
|
Reporting.log_warning pname ~loc: (Some l_node) ~pre: pre_opt exn
|
|
)
|
|
else ()
|
|
| _ -> ())
|
|
| _ -> if verbose then L.d_strln "NOT FOUND loc_succ"
|
|
) else ()
|
|
|
|
(** Perform symbolic execution for a node starting from an initial prop *)
|
|
let do_symbolic_execution handle_exn cfg tenv
|
|
(node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) =
|
|
let pdesc = Cfg.Node.get_proc_desc node in
|
|
State.mark_execution_start node;
|
|
State.set_const_map (ConstantPropagation.build_const_map pdesc); (* build the const map lazily *)
|
|
check_assignement_guard node;
|
|
let instrs = Cfg.Node.get_instrs node in
|
|
Ident.update_name_generator (instrs_get_normal_vars instrs); (* fresh normal vars must be fresh w.r.t. instructions *)
|
|
let pset =
|
|
SymExec.lifted_sym_exec handle_exn cfg tenv pdesc
|
|
(Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in
|
|
L.d_strln ".... After Symbolic Execution ....";
|
|
Propset.d prop (Paths.PathSet.to_propset pset);
|
|
L.d_ln (); L.d_ln();
|
|
State.mark_execution_end node;
|
|
pset
|
|
|
|
let mark_visited summary node =
|
|
let id = Cfg.Node.get_id node in
|
|
let stats = summary.Specs.stats in
|
|
if !Config.footprint
|
|
then stats.Specs.nodes_visited_fp <- IntSet.add id stats.Specs.nodes_visited_fp
|
|
else stats.Specs.nodes_visited_re <- IntSet.add id stats.Specs.nodes_visited_re
|
|
|
|
let forward_tabulate cfg tenv =
|
|
let handled_some_exception = ref false in
|
|
let handle_exn curr_node exn =
|
|
let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
|
|
let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
|
|
Exceptions.print_exception_html "Failure of symbolic execution: " exn;
|
|
let pre_opt = (* precondition leading to error, if any *)
|
|
State.get_normalized_pre (Abs.abstract_no_symop curr_pname) in
|
|
(match pre_opt with
|
|
| Some pre ->
|
|
L.d_strln "Precondition:"; Prop.d_prop pre; L.d_ln ()
|
|
| None -> ());
|
|
L.d_strln "SIL INSTR:";
|
|
Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node; L.d_ln ();
|
|
Reporting.log_error ~pre: pre_opt curr_pname exn;
|
|
State.mark_instr_fail pre_opt exn;
|
|
handled_some_exception := true in
|
|
|
|
while not (Worklist.is_empty ()) do
|
|
let curr_node = Worklist.remove () in
|
|
let kind_curr_node = Cfg.Node.get_kind curr_node in
|
|
let sid_curr_node = Cfg.Node.get_id 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 summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
|
|
mark_visited summary curr_node; (* mark nodes visited in fp and re phases *)
|
|
let session =
|
|
incr summary.Specs.sessions;
|
|
!(summary.Specs.sessions) in
|
|
do_before_node session curr_node;
|
|
let pathset_todo = path_set_checkout_todo curr_node in
|
|
let succ_nodes = Cfg.Node.get_succs curr_node in
|
|
let exn_nodes = Cfg.Node.get_exn curr_node in
|
|
let exe_iter f pathset =
|
|
let ps_size = Paths.PathSet.size pathset in
|
|
let cnt = ref 0 in
|
|
let exe prop path =
|
|
State.set_path path None;
|
|
incr cnt;
|
|
f prop path !cnt ps_size in
|
|
Paths.PathSet.iter exe pathset in
|
|
let log_string proc_name =
|
|
let phase_string = (if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE") in
|
|
let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
|
|
let timestamp = Specs.get_timestamp summary in
|
|
F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in
|
|
let doit () =
|
|
handled_some_exception := false;
|
|
check_prop_size pathset_todo;
|
|
L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^
|
|
"Node: " ^ string_of_int sid_curr_node ^ ", " ^
|
|
"Procedure: " ^ Procname.to_string proc_name ^ ", " ^
|
|
"Session: " ^ string_of_int session ^ ", " ^
|
|
"Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****");
|
|
L.d_increase_indent 1;
|
|
Propset.d Prop.prop_emp (Paths.PathSet.to_propset pathset_todo);
|
|
L.d_strln ".... Instructions: .... ";
|
|
Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node;
|
|
L.d_ln (); L.d_ln ();
|
|
|
|
match kind_curr_node with
|
|
| Cfg.Node.Join_node -> do_symexec_join proc_name tenv curr_node pathset_todo
|
|
| Cfg.Node.Stmt_node _
|
|
| Cfg.Node.Prune_node _
|
|
| Cfg.Node.Exit_node _
|
|
| Cfg.Node.Skip_node _
|
|
| Cfg.Node.Start_node _ ->
|
|
exe_iter
|
|
(fun prop path cnt num_paths ->
|
|
try
|
|
L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths);
|
|
L.d_increase_indent 1;
|
|
State.reset_diverging_states_goto_node ();
|
|
let pset =
|
|
do_symbolic_execution (handle_exn curr_node) cfg tenv curr_node prop path in
|
|
L.d_decrease_indent 1; L.d_ln();
|
|
propagate_nodes_divergence tenv proc_desc pset path kind_curr_node succ_nodes exn_nodes;
|
|
with exn when Exceptions.handle_exception exn && !Config.footprint ->
|
|
handle_exn curr_node exn;
|
|
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;
|
|
L.d_decrease_indent 1; L.d_ln ())
|
|
pathset_todo in
|
|
try begin
|
|
doit();
|
|
if !handled_some_exception then Printer.force_delayed_prints ();
|
|
do_after_node curr_node
|
|
end
|
|
with
|
|
| exn when Exceptions.handle_exception exn ->
|
|
handle_exn curr_node exn;
|
|
Printer.force_delayed_prints ();
|
|
do_after_node curr_node;
|
|
if not !Config.footprint then raise RE_EXE_ERROR
|
|
done;
|
|
L.d_strln ".... Work list empty. Stop ...."; L.d_ln ()
|
|
|
|
(** report an error if any Activity is reachable from a static field *)
|
|
let report_activity_leaks pname sigma tenv =
|
|
(* report an error if an expression in [activity_exps] is reachable from [field_strexp] *)
|
|
let check_reachable_activity_from_fld (fld_name, fld_strexp) activity_exps =
|
|
let _, reachable_exps =
|
|
let fld_exps = Prop.strexp_get_exps fld_strexp in
|
|
Prop.compute_reachable_hpreds sigma fld_exps in
|
|
(* raise an error if any Activity expression is in [reachable_exps] *)
|
|
list_iter
|
|
(fun (activity_exp, typ) ->
|
|
if Sil.ExpSet.mem activity_exp reachable_exps then
|
|
let err_desc = Errdesc.explain_activity_leak pname typ fld_name in
|
|
raise (Exceptions.Activity_leak (err_desc, try assert false with Assert_failure x -> x)))
|
|
activity_exps in
|
|
(* get the set of pointed-to expressions of type T <: Activity *)
|
|
let activity_exps =
|
|
list_fold_left
|
|
(fun exps hpred -> match hpred with
|
|
| Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _))
|
|
when AndroidFramework.is_activity typ tenv ->
|
|
(exp, typ) :: exps
|
|
| _ -> exps)
|
|
[]
|
|
sigma in
|
|
list_iter
|
|
(function
|
|
| Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _) when Sil.pvar_is_global pv ->
|
|
list_iter
|
|
(fun (f_name, f_strexp) ->
|
|
if not (Harness.is_generated_field f_name) then
|
|
check_reachable_activity_from_fld (f_name, f_strexp) activity_exps) static_flds
|
|
| _ -> ())
|
|
sigma
|
|
|
|
(** remove locals and formals, and check if the address of a stack variable is left in the result *)
|
|
let remove_locals_formals_and_check pdesc p =
|
|
let pname = Cfg.Procdesc.get_proc_name pdesc in
|
|
let pvars, p' = Cfg.remove_locals_formals pdesc p in
|
|
let check_pvar pvar =
|
|
let loc = Cfg.Node.get_loc (Cfg.Procdesc.get_exit_node pdesc) in
|
|
let dexp_opt, _ = Errdesc.vpath_find p (Sil.Lvar pvar) in
|
|
let desc = Errdesc.explain_stack_variable_address_escape loc pvar dexp_opt in
|
|
let exn = Exceptions.Stack_variable_address_escape (desc, try assert false with Assert_failure x -> x) in
|
|
Reporting.log_warning pname exn in
|
|
list_iter check_pvar pvars;
|
|
p'
|
|
|
|
(* Collect the analysis results for the exit node *)
|
|
let collect_analysis_result pdesc : Paths.PathSet.t =
|
|
let exit_node = Cfg.Procdesc.get_exit_node pdesc in
|
|
let exit_sid = Cfg.Node.get_id exit_node in
|
|
let pathset = path_set_get_visited exit_sid in
|
|
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)
|
|
|
|
let vset_ref_add_path vset_ref path =
|
|
Paths.Path.iter_all_nodes_nocalls (fun n -> vset_ref := Cfg.NodeSet.add n !vset_ref) path
|
|
|
|
let vset_ref_add_pathset vset_ref pathset =
|
|
Paths.PathSet.iter (fun p path -> vset_ref_add_path vset_ref path) pathset
|
|
|
|
let compute_visited vset =
|
|
let res = ref Specs.Visitedset.empty in
|
|
let node_get_all_lines n =
|
|
let node_loc = Cfg.Node.get_loc n in
|
|
let instrs_loc = list_map Sil.instr_get_loc (Cfg.Node.get_instrs n) in
|
|
let lines = list_map (fun loc -> loc.Location.line) (node_loc :: instrs_loc) in
|
|
list_remove_duplicates int_compare (list_sort int_compare lines) in
|
|
let do_node n = res := Specs.Visitedset.add (Cfg.Node.get_id n, node_get_all_lines n) !res in
|
|
Cfg.NodeSet.iter do_node vset;
|
|
!res
|
|
|
|
(** Extract specs from a pathset *)
|
|
let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
|
|
let pname = Cfg.Procdesc.get_proc_name pdesc in
|
|
let sub =
|
|
let fav = Sil.fav_new () in
|
|
Paths.PathSet.iter (fun prop path -> Prop.prop_fav_add fav prop) pathset;
|
|
let sub_list = list_map (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.knormal)))) (Sil.fav_to_list fav) in
|
|
Sil.sub_of_list sub_list in
|
|
let pre_post_visited_list =
|
|
let pplist = Paths.PathSet.elements pathset in
|
|
let f (prop, path) =
|
|
let _, prop' = Cfg.remove_locals_formals pdesc prop in
|
|
(* let () = L.out "@.BEFORE abs:@.$%a@." (Prop.pp_prop Utils.pe_text) prop' in *)
|
|
let prop'' = Abs.abstract pname tenv prop' in
|
|
(* let () = L.out "@.AFTER abs:@.$%a@." (Prop.pp_prop Utils.pe_text) prop'' in *)
|
|
let pre, post = Prop.extract_spec prop'' in
|
|
let pre' = Prop.normalize (Prop.prop_sub sub pre) in
|
|
if !Config.curr_language = Config.Java then
|
|
report_activity_leaks pname (Prop.get_sigma post) tenv;
|
|
let post' =
|
|
if Prover.check_inconsistency_base prop then None
|
|
else Some (Prop.normalize (Prop.prop_sub sub post), path) in
|
|
let visited =
|
|
let vset_ref = ref Cfg.NodeSet.empty in
|
|
vset_ref_add_path vset_ref path;
|
|
compute_visited !vset_ref in
|
|
(pre', post', visited) in
|
|
list_map f pplist in
|
|
let pre_post_map =
|
|
let add map (pre, post, visited) =
|
|
let current_posts, current_visited = try Pmap.find pre map with Not_found -> (Paths.PathSet.empty, Specs.Visitedset.empty) in
|
|
let new_posts = match post with
|
|
| None -> current_posts
|
|
| Some (post, path) -> Paths.PathSet.add_renamed_prop post path current_posts in
|
|
let new_visited = Specs.Visitedset.union visited current_visited in
|
|
Pmap.add pre (new_posts, new_visited) map in
|
|
list_fold_left add Pmap.empty pre_post_visited_list in
|
|
let specs = ref [] in
|
|
let add_spec pre ((posts : Paths.PathSet.t), visited) =
|
|
let posts' =
|
|
list_map
|
|
(fun (p, path) -> (Cfg.remove_seed_vars p, path))
|
|
(Paths.PathSet.elements (do_join_post pname tenv posts)) in
|
|
let spec =
|
|
{ Specs.pre = Specs.Jprop.Prop (1, pre);
|
|
Specs.posts = posts';
|
|
Specs.visited = visited } in
|
|
specs := spec :: !specs in
|
|
Pmap.iter add_spec pre_post_map;
|
|
!specs
|
|
|
|
let collect_postconditions tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t =
|
|
let pname = Cfg.Procdesc.get_proc_name pdesc in
|
|
let pathset = collect_analysis_result pdesc in
|
|
L.d_strln ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Analysis result ####");
|
|
Propset.d Prop.prop_emp (Paths.PathSet.to_propset pathset);
|
|
L.d_ln ();
|
|
let res =
|
|
try
|
|
let pathset = collect_do_abstract_post pname tenv pathset in
|
|
let pathset_diverging = State.get_diverging_states_proc () in
|
|
let visited =
|
|
let vset_ref = ref Cfg.NodeSet.empty in
|
|
vset_ref_add_pathset vset_ref pathset;
|
|
vset_ref_add_pathset vset_ref pathset_diverging; (* nodes from diverging states were also visited *)
|
|
compute_visited !vset_ref in
|
|
do_join_post pname tenv pathset, visited with
|
|
| exn when (match exn with Exceptions.Leak _ -> true | _ -> false) ->
|
|
raise (Failure "Leak in post collecion") in
|
|
L.d_strln ("#### [FUNCTION " ^ Procname.to_string pname ^ "] Postconditions after join ####");
|
|
L.d_increase_indent 1; Propset.d Prop.prop_emp (Paths.PathSet.to_propset (fst res)); L.d_decrease_indent 1;
|
|
L.d_ln ();
|
|
res
|
|
|
|
let create_seed_vars sigma =
|
|
let hpred_add_seed sigma = function
|
|
| Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Sil.pvar_is_abducted pv) ->
|
|
Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma
|
|
| _ -> sigma in
|
|
list_fold_left hpred_add_seed [] sigma
|
|
|
|
(** Initialize proposition for execution given formal and global
|
|
parameters. The footprint is initialized according to the
|
|
execution mode. The prop is not necessarily emp, so it
|
|
should be incorporated when the footprint is constructed. *)
|
|
let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Prop.t =
|
|
let sigma_new_formals =
|
|
let do_formal (pv, typ) =
|
|
let texp = match !Config.curr_language with
|
|
| Config.C_CPP -> Sil.Sizeof (typ, Sil.Subtype.exact)
|
|
| Config.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in
|
|
Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in
|
|
list_map do_formal new_formals in
|
|
let sigma_seed =
|
|
create_seed_vars (Prop.get_sigma prop @ sigma_new_formals) (* formals already there plus new ones *) in
|
|
let sigma = sigma_seed @ sigma_new_formals in
|
|
let new_pi =
|
|
let pi = Prop.get_pi prop in
|
|
pi
|
|
(* inactive until it becomes necessary, as it pollutes props
|
|
let fav_ids = Sil.fav_to_list (Prop.sigma_fav sigma_locals) in
|
|
let mk_undef_atom id = Prop.mk_neq (Sil.Var id) (Sil.Const (Sil.Cattribute (Sil.Aundef "UNINITIALIZED"))) in
|
|
let pi_undef = list_map mk_undef_atom fav_ids in
|
|
pi_undef @ pi *) in
|
|
let prop' =
|
|
Prop.replace_pi new_pi (Prop.prop_sigma_star prop sigma) in
|
|
Prop.replace_sigma_footprint (Prop.get_sigma_footprint prop' @ sigma_new_formals) prop'
|
|
|
|
(** Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true
|
|
as well as seed variables *)
|
|
let initial_prop tenv (curr_f: Cfg.Procdesc.t) (prop : 'a Prop.t) add_formals : Prop.normal Prop.t =
|
|
let construct_decl (x, typ) =
|
|
(Sil.mk_pvar (Mangled.from_string x) (Cfg.Procdesc.get_proc_name curr_f), typ) in
|
|
let new_formals =
|
|
if add_formals
|
|
then list_map construct_decl (Cfg.Procdesc.get_formals curr_f)
|
|
else [] in (** no new formals added *)
|
|
let prop1 = Prop.prop_reset_inst (fun inst_old -> Sil.update_inst inst_old Sil.inst_formal) prop in
|
|
let prop2 = prop_init_formals_seed tenv new_formals prop1 in
|
|
Prop.prop_rename_primed_footprint_vars (Prop.normalize prop2)
|
|
|
|
(** Construct an initial prop from the empty prop *)
|
|
let initial_prop_from_emp tenv curr_f =
|
|
initial_prop tenv curr_f Prop.prop_emp true
|
|
|
|
(** Construct an initial prop from an existing pre with formals *)
|
|
let initial_prop_from_pre tenv curr_f pre =
|
|
if !Config.footprint then
|
|
let vars = Sil.fav_to_list (Prop.prop_fav pre) in
|
|
let sub_list = list_map (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.kfootprint)))) vars in
|
|
let sub = Sil.sub_of_list sub_list in
|
|
let pre2 = Prop.prop_sub sub pre in
|
|
let pre3 = Prop.replace_sigma_footprint (Prop.get_sigma pre2) (Prop.replace_pi_footprint (Prop.get_pure pre2) pre2) in
|
|
initial_prop tenv curr_f pre3 false
|
|
else
|
|
initial_prop tenv curr_f pre false
|
|
|
|
(** 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)
|
|
: Prop.normal Specs.spec option =
|
|
let proc_name = Cfg.Procdesc.get_proc_name pdesc in
|
|
do_before_node 0 init_node;
|
|
L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
|
|
L.d_indent 1;
|
|
L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition;
|
|
L.d_ln (); L.d_ln ();
|
|
let init_prop = initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) 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;
|
|
try
|
|
path_set_worklist_reset pdesc;
|
|
Worklist.add init_node;
|
|
ignore (path_set_put_todo init_node init_edgeset);
|
|
forward_tabulate cfg tenv;
|
|
do_before_node 0 init_node;
|
|
L.d_strln_color Green ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
|
|
L.d_increase_indent 1;
|
|
L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition);
|
|
L.d_ln ();
|
|
let posts, visited =
|
|
let pset, visited = collect_postconditions tenv pdesc in
|
|
let plist = list_map (fun (p, path) -> (Cfg.remove_seed_vars p, path)) (Paths.PathSet.elements pset) in
|
|
plist, visited in
|
|
let pre =
|
|
let p = Cfg.remove_locals_ret pdesc (Specs.Jprop.to_prop precondition) in
|
|
match precondition with
|
|
| Specs.Jprop.Prop (n, _) -> Specs.Jprop.Prop (n, p)
|
|
| Specs.Jprop.Joined (n, _, jp1, jp2) -> Specs.Jprop.Joined (n, p, jp1, jp2) in
|
|
let spec = { Specs.pre = pre; Specs.posts = posts; Specs.visited = visited } in
|
|
L.d_decrease_indent 1;
|
|
do_after_node init_node;
|
|
Some spec
|
|
with RE_EXE_ERROR ->
|
|
do_before_node 0 init_node;
|
|
Printer.force_delayed_prints ();
|
|
L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string proc_name ^ "] ...ERROR");
|
|
L.d_increase_indent 1;
|
|
L.d_strln "when starting from pre:";
|
|
Prop.d_prop (Specs.Jprop.to_prop precondition);
|
|
L.d_strln "This precondition is filtered out.";
|
|
L.d_decrease_indent 1;
|
|
do_after_node init_node;
|
|
None
|
|
|
|
(** get all the nodes in the current call graph with their defined children *)
|
|
let get_procs_and_defined_children call_graph =
|
|
list_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 nstates = ref 0 in
|
|
let nodes = Cfg.Procdesc.get_nodes proc_desc in
|
|
list_iter (fun node -> nstates := !nstates + Paths.PathSet.size (path_set_get_visited (Cfg.Node.get_id node))) nodes;
|
|
F.fprintf fmt "(%d nodes containing %d states)" (list_length nodes) !nstates
|
|
|
|
(** Return functions to perform one phase of the analysis for a procedure.
|
|
Given [proc_name], return [do, get_results] where [go ()] performs the analysis phase
|
|
and [get_results ()] returns the results computed.
|
|
This function is architected so that [get_results ()] can be called even after
|
|
[go ()] was interrupted by and exception. *)
|
|
let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
|
|
: (unit -> unit) * (unit -> Prop.normal Specs.spec list) =
|
|
let start_node = Cfg.Procdesc.get_start_node pdesc in
|
|
|
|
let check_recursion_level () =
|
|
let summary = Specs.get_summary_unsafe "check_recursion_level" pname in
|
|
let recursion_level = Specs.get_timestamp summary in
|
|
if recursion_level > !Config.max_recursion then
|
|
begin
|
|
L.err "Reached maximum level of recursion, raising a Timeout@.";
|
|
raise (Timeout_exe (TOrecursion recursion_level))
|
|
end in
|
|
|
|
let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list) =
|
|
let go () =
|
|
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 specs = Specs.get_specs pname in
|
|
let mk_init precondition = (* rename spec vars to footrpint vars, and copy current to footprint *)
|
|
initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) in
|
|
list_map (fun spec -> mk_init spec.Specs.pre) specs in
|
|
let init_props = Propset.from_proplist (init_prop :: init_props_from_pres) in
|
|
let init_edgeset =
|
|
let add pset prop =
|
|
Paths.PathSet.add_renamed_prop prop (Paths.Path.start start_node) pset in
|
|
Propset.fold add Paths.PathSet.empty init_props in
|
|
L.out "@.#### Start: Footprint Computation for %a ####@." Procname.pp pname;
|
|
L.d_increase_indent 1;
|
|
L.d_strln "initial props =";
|
|
Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln();
|
|
L.d_decrease_indent 1;
|
|
path_set_worklist_reset pdesc;
|
|
check_recursion_level ();
|
|
Worklist.add start_node;
|
|
Config.arc_mode := Hashtbl.mem (Cfg.Procdesc.get_flags pdesc) Mleak_buckets.objc_arc_flag;
|
|
ignore (path_set_put_todo start_node init_edgeset);
|
|
forward_tabulate cfg tenv;
|
|
in
|
|
let get_results () =
|
|
State.process_execution_failures Reporting.log_warning pname;
|
|
let results = collect_analysis_result pdesc in
|
|
L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname;
|
|
L.out "#### Finished: Footprint Computation for %a %a ####@."
|
|
Procname.pp pname
|
|
(pp_intra_stats cfg pdesc) pname;
|
|
L.out "#### [FUNCTION %a] Footprint Analysis result ####@\n%a@."
|
|
Procname.pp pname
|
|
(Paths.PathSet.pp pe_text) results;
|
|
let specs = try extract_specs tenv pdesc results with
|
|
| Exceptions.Leak _ ->
|
|
let exn =
|
|
Exceptions.Internal_error
|
|
(Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint") in
|
|
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
|
|
Reporting.log_error pname ~pre: pre_opt exn;
|
|
[] (* retuning no specs *) in
|
|
specs in
|
|
go, get_results in
|
|
|
|
let re_execution proc_name : (unit -> unit) * (unit -> Prop.normal Specs.spec list) =
|
|
let candidate_preconditions = list_map (fun spec -> spec.Specs.pre) (Specs.get_specs proc_name) in
|
|
let valid_specs = ref [] in
|
|
let go () =
|
|
L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp proc_name;
|
|
check_recursion_level ();
|
|
let filter p =
|
|
let speco = execute_filter_prop cfg tenv pdesc start_node p in
|
|
let is_valid = match speco with
|
|
| None -> false
|
|
| Some spec ->
|
|
valid_specs := !valid_specs @ [spec];
|
|
true in
|
|
let outcome = if is_valid then "pass" else "fail" in
|
|
L.out "Finished re-execution for precondition %d %a (%s)@."
|
|
(Specs.Jprop.to_number p)
|
|
(pp_intra_stats cfg pdesc) proc_name
|
|
outcome;
|
|
speco in
|
|
if !Config.undo_join then
|
|
ignore (Specs.Jprop.filter filter candidate_preconditions)
|
|
else
|
|
ignore (list_map filter candidate_preconditions) in
|
|
let get_results () =
|
|
let specs = !valid_specs in
|
|
L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp proc_name;
|
|
L.out "#### Finished: Re-Execution for %a ####@." Procname.pp proc_name;
|
|
let valid_preconditions = list_map (fun spec -> spec.Specs.pre) specs in
|
|
let filename = DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [(Procname.to_filename proc_name)] in
|
|
if !Config.write_dotty then
|
|
Dotty.pp_speclist_dotty_file filename specs;
|
|
L.out "@.@.================================================";
|
|
L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp proc_name;
|
|
L.out "@.================================================@.";
|
|
L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text false) candidate_preconditions;
|
|
L.out "@.@.================================================";
|
|
L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp proc_name;
|
|
L.out "@.================================================@.";
|
|
L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text true) valid_preconditions;
|
|
specs in
|
|
go, get_results in
|
|
|
|
match Specs.get_phase pname with
|
|
| Specs.FOOTPRINT ->
|
|
compute_footprint
|
|
| Specs.RE_EXECUTION ->
|
|
re_execution pname
|
|
|
|
let set_current_language cfg proc_desc =
|
|
let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
|
|
Config.curr_language := language
|
|
|
|
(** reset counters before analysing a procedure *)
|
|
let reset_global_counters cfg proc_name proc_desc =
|
|
Ident.reset_name_generator ();
|
|
SymOp.reset_total ();
|
|
reset_prop_metrics ();
|
|
Abs.abs_rules_reset ();
|
|
set_current_language cfg proc_desc
|
|
|
|
(* Collect all pairs of the kind (precondition, exception) from a summary *)
|
|
let exception_preconditions tenv pname summary =
|
|
let collect_exceptions pre exns (prop, path) =
|
|
if Tabulation.prop_is_exn pname prop then
|
|
let exn_name = Tabulation.prop_get_exn_name pname prop in
|
|
if AndroidFramework.is_runtime_exception tenv exn_name then
|
|
(pre, exn_name):: exns
|
|
else exns
|
|
else exns
|
|
and collect_errors pre errors (prop, path) =
|
|
match Tabulation.lookup_global_errors prop with
|
|
| None -> errors
|
|
| Some e -> (pre, e) :: errors in
|
|
let collect_spec errors spec =
|
|
match !Config.curr_language with
|
|
| Config.Java ->
|
|
list_fold_left (collect_exceptions spec.Specs.pre) errors spec.Specs.posts
|
|
| Config.C_CPP ->
|
|
list_fold_left (collect_errors spec.Specs.pre) errors spec.Specs.posts in
|
|
list_fold_left collect_spec [] (Specs.get_specs_from_payload summary)
|
|
|
|
|
|
(* Remove the constrain of the form this != null which is true for all Java virtual calls *)
|
|
let remove_this_not_null prop =
|
|
let collect_hpred (var_option, hpreds) = function
|
|
| Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var var, _), _) when Sil.pvar_is_this pvar ->
|
|
(Some var, hpreds)
|
|
| hpred -> (var_option, hpred:: hpreds) in
|
|
let collect_atom var atoms = function
|
|
| Sil.Aneq (Sil.Var v, e)
|
|
when Ident.equal v var && Sil.exp_equal e Sil.exp_null -> atoms
|
|
| a -> a:: atoms in
|
|
match list_fold_left collect_hpred (None, []) (Prop.get_sigma prop) with
|
|
| None, _ -> prop
|
|
| Some var, filtered_hpreds ->
|
|
let filtered_atoms =
|
|
list_fold_left (collect_atom var) [] (Prop.get_pi prop) in
|
|
let prop' = Prop.replace_pi filtered_atoms Prop.prop_emp in
|
|
let prop'' = Prop.replace_sigma filtered_hpreds prop' in
|
|
Prop.normalize prop''
|
|
|
|
|
|
(** Detects if there are specs of the form {precondition} proc {runtime exception} and report
|
|
an error in that case, generating the trace that lead to the runtime exception if the method is
|
|
called in the context { precondition } *)
|
|
let report_runtime_exceptions tenv cfg pdesc summary =
|
|
let pname = Specs.get_proc_name summary in
|
|
let is_public_method =
|
|
(Specs.get_attributes summary).ProcAttributes.access = Sil.Public in
|
|
let is_main =
|
|
is_public_method
|
|
&& Procname.is_java pname
|
|
&& Procname.java_is_static pname
|
|
&& (Procname.java_get_method pname) = "main" in
|
|
let is_annotated =
|
|
let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
|
|
let annotated_signature = Annotations.get_annotated_signature proc_attributes in
|
|
let ret_annotation, _ = annotated_signature.Annotations.ret in
|
|
Annotations.ia_is_verify ret_annotation in
|
|
let is_unavoidable pre =
|
|
let prop = remove_this_not_null (Specs.Jprop.to_prop pre) in
|
|
match Prop.CategorizePreconditions.categorize [prop] with
|
|
| Prop.CategorizePreconditions.NoPres
|
|
| Prop.CategorizePreconditions.Empty -> true
|
|
| _ -> false in
|
|
let should_report pre =
|
|
is_main || is_annotated || is_unavoidable pre in
|
|
let report (pre, runtime_exception) =
|
|
if should_report pre then
|
|
let pre_str =
|
|
Utils.pp_to_string (Prop.pp_prop pe_text) (Specs.Jprop.to_prop pre) in
|
|
let exn_desc = Localise.java_unchecked_exn_desc pname runtime_exception pre_str in
|
|
let exn = Exceptions.Java_runtime_exception (runtime_exception, pre_str, exn_desc) in
|
|
Reporting.log_error pname ~pre: (Some (Specs.Jprop.to_prop pre)) exn in
|
|
list_iter report (exception_preconditions tenv pname summary)
|
|
|
|
|
|
(** update a summary after analysing a procedure *)
|
|
let update_summary prev_summary specs proc_name elapsed res =
|
|
let normal_specs = list_map Specs.spec_normalize specs in
|
|
let new_specs, changed = Fork.update_specs proc_name normal_specs in
|
|
let timestamp = max 1 (prev_summary.Specs.timestamp + if changed then 1 else 0) in
|
|
let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
|
|
let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in
|
|
let timeout = res == None || prev_summary.Specs.stats.Specs.stats_timeout in
|
|
let stats =
|
|
{ prev_summary.Specs.stats with
|
|
Specs.stats_time = stats_time;
|
|
Specs.symops = symops;
|
|
Specs.stats_timeout = timeout } in
|
|
{ prev_summary with
|
|
Specs.stats = stats;
|
|
Specs.payload = Specs.PrePosts new_specs;
|
|
Specs.timestamp = timestamp }
|
|
|
|
|
|
(** Analyze [proc_name] and return the updated summary. Use module
|
|
[Timeout] to call [perform_analysis_phase] with a time limit, and
|
|
then return the updated summary. Executed as a child process. *)
|
|
let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary =
|
|
if !Config.trace_anal then L.err "===analyze_proc@.";
|
|
let init_time = Unix.gettimeofday () in
|
|
let tenv = Exe_env.get_tenv exe_env proc_name in
|
|
let cfg = Exe_env.get_cfg exe_env proc_name in
|
|
let proc_desc = match Cfg.Procdesc.find_from_name cfg proc_name with
|
|
| Some proc_desc -> proc_desc
|
|
| None -> assert false in
|
|
reset_global_counters cfg proc_name proc_desc;
|
|
let go, get_results = perform_analysis_phase cfg tenv proc_name proc_desc in
|
|
let res = Fork.Timeout.exe_timeout (Specs.get_iterations proc_name) go () in
|
|
let specs = get_results () in
|
|
let elapsed = Unix.gettimeofday () -. init_time in
|
|
let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in
|
|
let updated_summary =
|
|
update_summary prev_summary specs proc_name elapsed res in
|
|
if (!Config.curr_language <> Config.Java && Config.report_assertion_failure)
|
|
|| !Config.report_runtime_exceptions then
|
|
report_runtime_exceptions tenv cfg proc_desc updated_summary;
|
|
updated_summary
|
|
|
|
(** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for
|
|
the procedures enabled after the analysis of [proc_name] *)
|
|
let perform_transition exe_env cg proc_name =
|
|
let proc_names = Fork.should_perform_transition cg proc_name in
|
|
let transition pname =
|
|
let tenv = Exe_env.get_tenv exe_env pname in
|
|
let joined_pres = (* disable exceptions for leaks and protect against any other errors *)
|
|
let allowleak = !Config.allowleak in
|
|
let apply_start_node f = (* apply the start node to f, and do nothing in case of exception *)
|
|
try
|
|
match Cfg.Procdesc.find_from_name (Exe_env.get_cfg exe_env pname) pname with
|
|
| Some pdesc ->
|
|
let start_node = Cfg.Procdesc.get_start_node pdesc in
|
|
f start_node
|
|
| None -> ()
|
|
with exn when exn_not_timeout exn -> () in
|
|
apply_start_node (do_before_node 0);
|
|
try
|
|
Config.allowleak := true;
|
|
let res = collect_preconditions proc_name tenv pname in
|
|
Config.allowleak := allowleak;
|
|
apply_start_node do_after_node;
|
|
res
|
|
with exn when exn_not_timeout exn ->
|
|
apply_start_node do_after_node;
|
|
Config.allowleak := allowleak;
|
|
L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
|
|
let err_name, _, mloco, _, _, _, _ = Exceptions.recognize_exception exn in
|
|
let err_str = "exception raised " ^ (Localise.to_string err_name) in
|
|
L.err "Error: %s %a@." err_str pp_ml_location_opt mloco;
|
|
[] in
|
|
Fork.transition_footprint_re_exe pname joined_pres in
|
|
list_iter transition proc_names
|
|
|
|
(** Process the result of the analysis of [proc_name]: update the
|
|
returned summary and add it to the spec table. Executed in the
|
|
parent process as soon as a child process returns a result. *)
|
|
let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary) : unit =
|
|
if !Config.trace_anal then L.err "===process_result@.";
|
|
Ident.reset_name_generator (); (* for consistency with multi-core mode *)
|
|
let summ =
|
|
{ _summ with
|
|
Specs.stats = { _summ.Specs.stats with Specs.stats_calls = calls }} in
|
|
Specs.add_summary proc_name summ;
|
|
let call_graph = Exe_env.get_cg exe_env in
|
|
perform_transition exe_env call_graph proc_name;
|
|
if !Config.only_footprint || summ.Specs.phase != Specs.FOOTPRINT then
|
|
(try Specs.store_summary proc_name summ with
|
|
Sys_error s ->
|
|
L.err "@.### System Error while writing summary of procedure %a to disk: %s@." Procname.pp proc_name s);
|
|
let procs_done = Fork.procs_become_done call_graph proc_name in
|
|
Fork.post_process_procs exe_env procs_done
|
|
|
|
(** Return true if the analysis of [proc_name] should be
|
|
skipped. Called by the parent process before attempting to analyze a
|
|
proc. *)
|
|
let filter_out (call_graph: Cg.t) (proc_name: Procname.t) : bool =
|
|
if !Config.trace_anal then L.err "===filter_out@.";
|
|
let slice_out = (* filter out if slicing is active and [proc_name] not in slice *)
|
|
(!Config.slice_fun <> "") &&
|
|
(Procname.compare (Procname.from_string_c_fun !Config.slice_fun) proc_name != 0) &&
|
|
(Cg.node_defined call_graph proc_name) &&
|
|
not (Cg.calls_recursively call_graph (Procname.from_string_c_fun !Config.slice_fun) proc_name) in
|
|
slice_out
|
|
|
|
let check_skipped_procs procs_and_defined_children =
|
|
let skipped_procs = ref Procname.Set.empty in
|
|
let proc_check_skips (pname, dep) =
|
|
let process_skip () =
|
|
let call_stats =
|
|
(Specs.get_summary_unsafe "check_skipped_procs" pname).Specs.stats.Specs.call_stats in
|
|
let do_tr_elem pn = function
|
|
| Specs.CallStats.CR_skip, _ ->
|
|
skipped_procs := Procname.Set.add pn !skipped_procs
|
|
| _ -> () in
|
|
let do_call (pn, _) (tr: Specs.CallStats.trace) = list_iter (do_tr_elem pn) tr in
|
|
Specs.CallStats.iter do_call call_stats in
|
|
if Specs.summary_exists pname then process_skip () in
|
|
list_iter proc_check_skips procs_and_defined_children;
|
|
let skipped_procs_with_summary =
|
|
Procname.Set.filter Specs.summary_exists !skipped_procs in
|
|
skipped_procs_with_summary
|
|
|
|
(** create a function to filter procedures which were skips but now have a .specs file *)
|
|
let filter_skipped_procs cg procs_and_defined_children =
|
|
let skipped_procs_with_summary = check_skipped_procs procs_and_defined_children in
|
|
let filter (pname, dep) =
|
|
let calls_recurs pn =
|
|
let r = try Cg.calls_recursively cg pname pn with Not_found -> false in
|
|
L.err "calls recursively %a %a: %b@." Procname.pp pname Procname.pp pn r;
|
|
r in
|
|
Procname.Set.exists calls_recurs skipped_procs_with_summary in
|
|
filter
|
|
|
|
(** create a function to filter procedures which were analyzed before but had no specs *)
|
|
let filter_nospecs (pname, dep) =
|
|
if Specs.summary_exists pname
|
|
then Specs.get_specs pname = []
|
|
else false
|
|
|
|
(** Perform the analysis of an exe_env *)
|
|
let do_analysis exe_env =
|
|
if !Config.trace_anal then L.err "do_analysis@.";
|
|
let cg = Exe_env.get_cg exe_env in
|
|
let procs_and_defined_children = get_procs_and_defined_children cg in
|
|
let get_calls caller_pdesc =
|
|
let calls = ref [] in
|
|
let f (callee_pname, loc) = calls := (callee_pname, loc) :: !calls in
|
|
Cfg.Procdesc.iter_calls f caller_pdesc;
|
|
list_rev !calls in
|
|
let init_proc (pname, dep) =
|
|
let cfg = Exe_env.get_cfg exe_env pname in
|
|
let pdesc = match Cfg.Procdesc.find_from_name cfg pname with
|
|
| Some pdesc -> pdesc
|
|
| None -> assert false in
|
|
let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes pdesc) in
|
|
let proc_flags = Cfg.Procdesc.get_flags pdesc in
|
|
let static_err_log = Cfg.Procdesc.get_err_log pdesc in (** err log from translation *)
|
|
let calls = get_calls pdesc in
|
|
let cyclomatic = Cfg.Procdesc.get_cyclomatic pdesc in
|
|
let attributes =
|
|
{ (Cfg.Procdesc.get_attributes pdesc) with
|
|
ProcAttributes.err_log = static_err_log; } in
|
|
|
|
Callbacks.proc_inline_synthetic_methods cfg pdesc;
|
|
Specs.init_summary
|
|
(dep, nodes, proc_flags,
|
|
calls, cyclomatic, None, attributes) in
|
|
let filter =
|
|
if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children)
|
|
else if !Config.only_nospecs then filter_nospecs
|
|
else (fun _ -> true) in
|
|
list_iter (fun x -> if filter x then init_proc x) procs_and_defined_children;
|
|
Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out
|
|
|
|
let visited_and_total_nodes cfg =
|
|
let all_nodes =
|
|
let add s n = Cfg.NodeSet.add n s in
|
|
list_fold_left add Cfg.NodeSet.empty (Cfg.Node.get_all_nodes cfg) in
|
|
let filter_node n =
|
|
Cfg.Procdesc.is_defined (Cfg.Node.get_proc_desc n) &&
|
|
match Cfg.Node.get_kind n with
|
|
| Cfg.Node.Stmt_node _ | Cfg.Node.Prune_node _
|
|
| Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ -> true
|
|
| Cfg.Node.Skip_node _ | Cfg.Node.Join_node -> false in
|
|
let counted_nodes = Cfg.NodeSet.filter filter_node all_nodes in
|
|
let visited_nodes_re = Cfg.NodeSet.filter (fun node -> snd (Printer.is_visited_phase node)) counted_nodes in
|
|
Cfg.NodeSet.elements visited_nodes_re, Cfg.NodeSet.elements counted_nodes
|
|
|
|
(** Print the stats for the given cfg; consider every defined proc unless a proc with the same name
|
|
was defined in another module, and was the one which was analyzed *)
|
|
let print_stats_cfg proc_shadowed proc_is_active cfg =
|
|
let err_table = Errlog.create_err_table () in
|
|
let active_procs = list_filter proc_is_active (Cfg.get_defined_procs cfg) in
|
|
let nvisited, ntotal = visited_and_total_nodes cfg in
|
|
let node_filter n =
|
|
let node_procname = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc n) in
|
|
Specs.summary_exists node_procname && Specs.get_specs node_procname != [] in
|
|
let nodes_visited = list_filter node_filter nvisited in
|
|
let nodes_total = list_filter node_filter ntotal in
|
|
let num_proc = ref 0 in
|
|
let num_nospec_noerror_proc = ref 0 in
|
|
let num_spec_noerror_proc = ref 0 in
|
|
let num_nospec_error_proc = ref 0 in
|
|
let num_spec_error_proc = ref 0 in
|
|
let tot_specs = ref 0 in
|
|
let tot_symops = ref 0 in
|
|
let num_timeout = ref 0 in
|
|
let compute_stats_proc proc_desc =
|
|
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
|
|
if proc_shadowed proc_desc then
|
|
L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name
|
|
else
|
|
let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in
|
|
let stats = summary.Specs.stats in
|
|
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
|
|
incr num_proc;
|
|
let specs = Specs.get_specs_from_payload summary in
|
|
tot_specs := (list_length specs) + !tot_specs;
|
|
let () =
|
|
match specs,
|
|
Errlog.size
|
|
(fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint)
|
|
err_log with
|
|
| [], 0 -> incr num_nospec_noerror_proc
|
|
| _, 0 -> incr num_spec_noerror_proc
|
|
| [], _ -> incr num_nospec_error_proc
|
|
| _, _ -> incr num_spec_error_proc in
|
|
tot_symops := !tot_symops + stats.Specs.symops;
|
|
if stats.Specs.stats_timeout then incr num_timeout;
|
|
Errlog.extend_table err_table err_log in
|
|
let print_file_stats fmt () =
|
|
let num_errors = Errlog.err_table_size_footprint Exceptions.Kerror err_table in
|
|
let num_warnings = Errlog.err_table_size_footprint Exceptions.Kwarning err_table in
|
|
let num_infos = Errlog.err_table_size_footprint Exceptions.Kinfo err_table in
|
|
let num_ok_proc = !num_spec_noerror_proc + !num_spec_error_proc in
|
|
(* F.fprintf fmt "VISITED: %a@\n" (pp_seq pp_node) nodes_visited;
|
|
F.fprintf fmt "TOTAL: %a@\n" (pp_seq pp_node) nodes_total; *)
|
|
F.fprintf fmt "@\n++++++++++++++++++++++++++++++++++++++++++++++++++@\n";
|
|
F.fprintf fmt "+ FILE: %s LOC: %n VISITED: %d/%d SYMOPS: %d@\n" (DB.source_file_to_string !DB.current_source) !Config.nLOC (list_length nodes_visited) (list_length nodes_total) !tot_symops;
|
|
F.fprintf fmt "+ num_procs: %d (%d ok, %d timeouts, %d errors, %d warnings, %d infos)@\n" !num_proc num_ok_proc !num_timeout num_errors num_warnings num_infos;
|
|
F.fprintf fmt "+ detail procs:@\n";
|
|
F.fprintf fmt "+ - No Errors and No Specs: %d@\n" !num_nospec_noerror_proc;
|
|
F.fprintf fmt "+ - Some Errors and No Specs: %d@\n" !num_nospec_error_proc;
|
|
F.fprintf fmt "+ - No Errors and Some Specs: %d@\n" !num_spec_noerror_proc;
|
|
F.fprintf fmt "+ - Some Errors and Some Specs: %d@\n" !num_spec_error_proc;
|
|
F.fprintf fmt "+ errors: %a@\n" (Errlog.pp_err_table_stats Exceptions.Kerror) err_table;
|
|
F.fprintf fmt "+ warnings: %a@\n" (Errlog.pp_err_table_stats Exceptions.Kwarning) err_table;
|
|
F.fprintf fmt "+ infos: %a@\n" (Errlog.pp_err_table_stats Exceptions.Kinfo) err_table;
|
|
F.fprintf fmt "+ specs: %d@\n" !tot_specs;
|
|
F.fprintf fmt "++++++++++++++++++++++++++++++++++++++++++++++++++@\n";
|
|
Errlog.print_err_table_details fmt err_table in
|
|
let save_file_stats () =
|
|
let source_dir = DB.source_dir_from_source_file !DB.current_source in
|
|
let stats_file = DB.source_dir_get_internal_file source_dir ".stats" in
|
|
try
|
|
let outc = open_out (DB.filename_to_string stats_file) in
|
|
let fmt = F.formatter_of_out_channel outc in
|
|
print_file_stats fmt ();
|
|
close_out outc
|
|
with Sys_error _ -> () in
|
|
list_iter compute_stats_proc active_procs;
|
|
L.out "%a" print_file_stats ();
|
|
save_file_stats ()
|
|
|
|
(** Print the stats for all the files in the exe_env *)
|
|
let print_stats exe_env =
|
|
let proc_is_active proc_desc =
|
|
Exe_env.proc_is_active exe_env (Cfg.Procdesc.get_proc_name proc_desc) in
|
|
Exe_env.iter_files (fun fname tenv cfg ->
|
|
let proc_shadowed proc_desc =
|
|
(** return true if a proc with the same name in another module was analyzed instead *)
|
|
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
|
|
Exe_env.get_source exe_env proc_name <> fname in
|
|
print_stats_cfg proc_shadowed proc_is_active cfg) exe_env
|