diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index bd84e415f..606e926cd 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -24,18 +24,41 @@ module Node = struct | Skip_node of string and t = { (** a node *) - nd_id : int; (** unique id of the node *) - mutable nd_dist_exit : int option; (** distance to the exit node *) - mutable nd_temps : Ident.t list; (** temporary variables *) - mutable nd_dead_pvars_after : Sil.pvar list; (** dead program variables after executing the instructions *) - mutable nd_dead_pvars_before : Sil.pvar list; (** dead program variables before executing the instructions *) - mutable nd_exn : t list; (** exception nodes in the cfg *) - mutable nd_instrs : Sil.instr list; (** instructions for symbolic execution *) - mutable nd_kind : nodekind; (** kind of node *) - mutable nd_loc : Location.t; (** location in the source code *) - mutable nd_preds : t list; (** predecessor nodes in the cfg *) - mutable nd_proc : proc_desc option; (** proc desc from cil *) - mutable nd_succs : t list; (** successor nodes in the cfg *) + (** unique id of the node *) + nd_id : int; + + (** distance to the exit node *) + mutable nd_dist_exit : int option; + + (** temporary variables *) + mutable nd_temps : Ident.t list; + + (** dead program variables after executing the instructions *) + mutable nd_dead_pvars_after : Sil.pvar list; + + (** dead program variables before executing the instructions *) + mutable nd_dead_pvars_before : Sil.pvar list; + + (** exception nodes in the cfg *) + mutable nd_exn : t list; + + (** instructions for symbolic execution *) + mutable nd_instrs : Sil.instr list; + + (** kind of node *) + mutable nd_kind : nodekind; + + (** location in the source code *) + mutable nd_loc : Location.t; + + (** predecessor nodes in the cfg *) + mutable nd_preds : t list; + + (** proc desc from cil *) + mutable nd_proc : proc_desc option; + + (** successor nodes in the cfg *) + mutable nd_succs : t list; } and proc_desc = { (** procedure description *) pd_attributes : ProcAttributes.t; (** attributes of the procedure *) @@ -482,14 +505,17 @@ module Node = struct proc_desc.pd_attributes.ProcAttributes.locals <- proc_desc.pd_attributes.ProcAttributes.locals @ new_locals - (** Print extended instructions for the node, highlighting the given subinstruction if present *) - let pp_instr pe0 ~sub_instrs instro fmt node = + (** Print extended instructions for the node, + highlighting the given subinstruction if present *) + let pp_instrs pe0 ~sub_instrs instro fmt node = let pe = match instro with | None -> pe0 | Some instr -> pe_extend_colormap pe0 (Obj.repr instr) Red in let instrs = get_instrs node in - let pp_loc fmt () = F.fprintf fmt " %a " Location.pp (get_loc node) in - let print_sub_instrs () = F.fprintf fmt "%a" (Sil.pp_instr_list pe) instrs in + let pp_loc fmt () = + F.fprintf fmt " %a " Location.pp (get_loc node) in + let print_sub_instrs () = + F.fprintf fmt "%a" (Sil.pp_instr_list pe) instrs in match get_kind node with | Stmt_node s -> if sub_instrs then print_sub_instrs () @@ -530,7 +556,10 @@ module Node = struct "Start" | Join_node -> "Join" in - let pp fmt () = F.fprintf fmt "%s\n%a@?" str (pp_instr pe None ~sub_instrs: true) node in + let pp fmt () = + F.fprintf fmt "%s\n%a@?" + str + (pp_instrs pe None ~sub_instrs: true) node in pp_to_string pp () let proc_desc_iter_nodes f proc_desc = diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index 6b9886590..02f7c18a7 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -234,13 +234,16 @@ module Node : sig (** Pretty print the node *) val pp : Format.formatter -> t -> unit - (** Print extended instructions for the node, highlighting the given subinstruction if present *) - val pp_instr : printenv -> sub_instrs: bool -> Sil.instr option -> Format.formatter -> t -> unit + (** Print extended instructions for the node, + highlighting the given subinstruction if present *) + val pp_instrs : + printenv -> sub_instrs: bool -> Sil.instr option -> Format.formatter -> t -> unit (** Replace the instructions to be executed. *) val replace_instrs : t -> Sil.instr list -> unit - (** Set the (after/before) dead program variables. After/before indicated with the true/false flag. *) + (** Set the (after/before) dead program variables. + After/before indicated with the true/false flag. *) val set_dead_pvars : t -> bool -> Sil.pvar list -> unit (** Set the node kind *) diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index b2dfb6441..6920c51cb 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -230,15 +230,17 @@ let analyze_exe_env exe_env = Specs.clear_spec_tbl (); Random.self_init (); let line_reader = Printer.LineReader.create () in - if !checkers then (* run the checkers only *) + if !checkers then begin + (** run the checkers only *) let call_graph = Exe_env.get_cg exe_env in Callbacks.iterate_callbacks Checkers.ST.store_summary call_graph exe_env end else - begin (* run the full analysis *) + begin + (** run the full analysis *) Interproc.do_analysis exe_env; - Printer.c_files_write_html line_reader exe_env; + Printer.write_all_html_files line_reader exe_env; Interproc.print_stats exe_env; let elapsed = Unix.gettimeofday () -. init_time in L.out "Interprocedural footprint analysis terminated in %f sec@." elapsed diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 5fe1d8757..3f076e9ed 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -24,13 +24,22 @@ type visitednode = 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 + let compare_ids n1 n2 = + (* higher id is better *) + Cfg.Node.compare n2 n1 + 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 -> + (* shorter distance to exit is better *) + int_compare d1 d2 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 *) @@ -193,7 +202,8 @@ let do_meet_pre pset = else Propset.to_proplist pset -(** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *) +(** Find the preconditions in the current spec table, + apply meet then join, and return the joined preconditions *) let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = let collect_do_abstract_one tenv prop = if !Config.footprint @@ -241,9 +251,11 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = (* =============== START of symbolic execution =============== *) (** propagate a set of results to the given node *) -let propagate (wl : Worklist.t) 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 f prop path edgeset_curr = (** prop must be a renamed prop by the invariant preserved by PropSet *) + (** prop must be a renamed prop by the invariant preserved by PropSet *) + let f prop path edgeset_curr = let exn_opt = if is_exception then Some (Tabulation.prop_get_exn_name pname prop) @@ -334,9 +346,10 @@ let do_before_node session node = State.set_node node; State.set_session session; L.reset_delayed_prints (); - Printer.start_session node loc proc_name session + Printer.node_start_session node loc proc_name session -let do_after_node node = Printer.finish_session node +let do_after_node node = + Printer.node_finish_session node (** Return the list of normal ids occurring in the instructions *) let instrs_get_normal_vars instrs = @@ -393,8 +406,12 @@ let check_assignement_guard node = let leti = IList.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"); + | [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 = IList.flatten(IList.map (fun n -> prune_var n) succs) in @@ -415,7 +432,8 @@ let check_assignement_guard node = " 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 *) + (* check that the guards of the succs are a var or its negation *) + let succs_have_simple_guards () = let check_instr = function | Sil.Prune (Sil.Var _, _, _, _) -> true | Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var _, _), _, _, _) -> true @@ -430,13 +448,17 @@ let check_assignement_guard 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*) + (* at this point all successors are at the same location, so we can take the first*) + | loc_succ:: _ -> let set_instr_at_succs_loc = IList.filter - (fun i -> (Location.equal (Sil.instr_get_loc i) loc_succ) && is_set_instr i) + (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*) + | [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)) then ( let desc = Errdesc.explain_condition_is_assignment l_node in let exn = Exceptions.Condition_is_assignment (desc, __POS__) in @@ -444,8 +466,10 @@ let check_assignement_guard node = Reporting.log_warning pname ~loc: (Some l_node) ~pre: pre_opt exn ) else () - | _ -> ()) - | _ -> if verbose then L.d_strln "NOT FOUND loc_succ" + | _ -> + ()) + | _ -> + if verbose then L.d_strln "NOT FOUND loc_succ" ) else () (** Perform symbolic execution for a node starting from an initial prop *) @@ -453,10 +477,12 @@ let do_symbolic_execution handle_exn 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 *) + (* build the const map lazily *) + State.set_const_map (ConstantPropagation.build_const_map pdesc); 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 *) + (* fresh normal vars must be fresh w.r.t. instructions *) + Ident.update_name_generator (instrs_get_normal_vars instrs); let pset = SymExec.lifted_sym_exec handle_exn tenv pdesc (Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in @@ -518,7 +544,8 @@ let forward_tabulate tenv wl = 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 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 @@ -616,15 +643,20 @@ let report_context_leaks pname sigma tenv = sigma in IList.iter (function - | Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _) when Sil.pvar_is_global pv -> + | Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _) + when Sil.pvar_is_global pv -> IList.iter (fun (f_name, f_strexp) -> - if not (Harness.is_generated_field f_name) then - check_reachable_context_from_fld (f_name, f_strexp) context_exps) static_flds + if not (Harness.is_generated_field f_name) + then + check_reachable_context_from_fld + (f_name, f_strexp) context_exps) + static_flds | _ -> ()) sigma -(** remove locals and formals, and check if the address of a stack variable is left in the result *) +(** 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 @@ -637,17 +669,23 @@ let remove_locals_formals_and_check pdesc p = IList.iter check_pvar pvars; p' -(* Collect the analysis results for the exit node *) +(** Collect the analysis results for the exit node. *) let collect_analysis_result wl pdesc : Paths.PathSet.t = let exit_node = Cfg.Procdesc.get_exit_node pdesc in let exit_node_id = Cfg.Node.get_id exit_node in let pathset = htable_retrieve wl.Worklist.path_set_visited exit_node_id 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) +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 + 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 _ path -> vset_ref_add_path vset_ref path) pathset @@ -659,7 +697,9 @@ let compute_visited vset = let instrs_loc = IList.map Sil.instr_get_loc (Cfg.Node.get_instrs n) in let lines = IList.map (fun loc -> loc.Location.line) (node_loc :: instrs_loc) in IList.remove_duplicates int_compare (IList.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 + 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 @@ -668,8 +708,13 @@ 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 _ -> Prop.prop_fav_add fav prop) pathset; - let sub_list = IList.map (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.knormal)))) (Sil.fav_to_list fav) in + Paths.PathSet.iter + (fun prop _ -> Prop.prop_fav_add fav prop) + pathset; + let sub_list = + IList.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 @@ -678,7 +723,8 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list = let prop'' = Abs.abstract pname tenv 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 && Cfg.Procdesc.get_access pdesc <> Sil.Private then + if !Config.curr_language = + Config.Java && Cfg.Procdesc.get_access pdesc <> Sil.Private then report_context_leaks pname (Prop.get_sigma post) tenv; let post' = if Prover.check_inconsistency_base prop then None @@ -691,7 +737,10 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list = IList.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 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 @@ -715,7 +764,8 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list = let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t = let pname = Cfg.Procdesc.get_proc_name 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); L.d_ln (); let res = @@ -725,13 +775,17 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t 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 *) + (* nodes from diverging states were also visited *) + vset_ref_add_pathset vset_ref pathset_diverging; 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_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 @@ -755,31 +809,35 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in IList.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 + create_seed_vars + (* formals already there plus new ones *) + (Prop.get_sigma prop @ sigma_new_formals) 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 = IList.map mk_undef_atom fav_ids in - pi_undef @ pi *) in + Prop.get_pi prop 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' + 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 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 x (Cfg.Procdesc.get_proc_name curr_f), typ) in let new_formals = if add_formals then IList.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 + 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 *) @@ -790,10 +848,16 @@ let initial_prop_from_emp tenv curr_f = 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 = IList.map (fun id -> (id, Sil.Var (Ident.create_fresh (Ident.kfootprint)))) vars in + let sub_list = + IList.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 + 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 @@ -807,8 +871,13 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec 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 + 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 Worklist.add wl init_node; @@ -821,7 +890,10 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec L.d_ln (); let posts, visited = 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 let pre = let p = Cfg.remove_locals_ret pdesc (Specs.Jprop.to_prop precondition) in @@ -846,14 +918,21 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec (** get all the nodes in the current call graph with their defined children *) 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 wl proc_desc fmt _ = let nstates = ref 0 in let nodes = Cfg.Procdesc.get_nodes proc_desc in - IList.iter (fun node -> - nstates := !nstates + Paths.PathSet.size - (htable_retrieve wl.Worklist.path_set_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 (** Return functions to perform one phase of the analysis for a procedure. @@ -877,9 +956,11 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = let go (wl : Worklist.t) () = 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 *) + (* use existing pre's (in recursion some might exist) as starting points *) + let init_props_from_pres = let specs = Specs.get_specs pname in - let mk_init precondition = (* rename spec vars to footrpint vars, and copy current to footprint *) + (* rename spec vars to footrpint vars, and copy current to footprint *) + let mk_init precondition = initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) in IList.map (fun spec -> mk_init spec.Specs.pre) specs in let init_props = Propset.from_proplist (init_prop :: init_props_from_pres) in @@ -894,7 +975,10 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) L.d_decrease_indent 1; check_recursion_level (); 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 wl start_node init_edgeset); forward_tabulate tenv wl in let get_results (wl : Worklist.t) () = @@ -921,7 +1005,10 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) let re_execution proc_name : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = - let candidate_preconditions = IList.map (fun spec -> spec.Specs.pre) (Specs.get_specs proc_name) in + let candidate_preconditions = + IList.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; @@ -948,8 +1035,12 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) 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 = IList.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 + let valid_preconditions = + IList.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 "@.@.================================================"; @@ -1103,7 +1194,8 @@ let update_specs proc_name phase (new_specs : Specs.NormSpec.t list) new_specs) then begin changed:= true; - L.out "Specs changed: removing pre of spec@\n%a@." (Specs.pp_spec pe_text None) old_spec; + L.out "Specs changed: removing pre of spec@\n%a@." + (Specs.pp_spec pe_text None) old_spec; current_specs := SpecMap.remove old_spec.Specs.pre !current_specs end else () in let add_spec spec = (* add a new spec by doing union of the posts *) @@ -1125,7 +1217,8 @@ let update_specs proc_name phase (new_specs : Specs.NormSpec.t list) with Not_found -> changed := true; - L.out "Specs changed: added new pre@\n%a@." (Specs.Jprop.pp_short pe_text) spec.Specs.pre; + L.out "Specs changed: added new pre@\n%a@." + (Specs.Jprop.pp_short pe_text) spec.Specs.pre; current_specs := SpecMap.add spec.Specs.pre @@ -1225,9 +1318,11 @@ let transition_footprint_re_exe proc_name joined_pres = the procedures enabled after the analysis of [proc_name] *) let perform_transition exe_env tenv proc_name = let transition () = - let joined_pres = (* disable exceptions for leaks and protect against any other errors *) + (* disable exceptions for leaks and protect against any other errors *) + let joined_pres = let allowleak = !Config.allowleak in - let apply_start_node f = (* apply the start node to f, and do nothing in case of exception *) + (* apply the start node to f, and do nothing in case of exception *) + let apply_start_node f = try match Exe_env.get_proc_desc exe_env proc_name with | Some pdesc -> @@ -1355,10 +1450,14 @@ let visited_and_total_nodes cfg = | 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 + let visited_nodes_re = + Cfg.NodeSet.filter + (fun node -> snd (Printer.node_is_visited 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 +(** 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 cfg = let err_table = Errlog.create_err_table () in @@ -1380,7 +1479,8 @@ let print_stats_cfg proc_shadowed cfg = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in if proc_shadowed proc_desc || Specs.get_summary proc_name = None then - L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name + 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 diff --git a/infer/src/backend/io_infer.ml b/infer/src/backend/io_infer.ml index 02fd12af9..7f5199ad0 100644 --- a/infer/src/backend/io_infer.ml +++ b/infer/src/backend/io_infer.ml @@ -13,113 +13,145 @@ module F = Format (* =============== START of module Html =============== *) -module Html : sig - val close : Unix.file_descr * Format.formatter -> unit (** Close an Html file *) - val create : DB.Results_dir.path_kind -> DB.Results_dir.path -> Unix.file_descr * Format.formatter (** Create a new html file *) - val modified_during_analysis : DB.Results_dir.path -> bool (** Return true if the html file was modified since the beginning of the analysis *) - val open_out : DB.Results_dir.path -> Unix.file_descr * Format.formatter (** Open an Html file to append data *) - val pp_line_link : ?with_name: bool -> ?text: (string option) -> DB.Results_dir.path -> Format.formatter -> int -> unit (** Print an html link to the given line number of the current source file *) - val pp_hline : Format.formatter -> unit -> unit (** Print a horizontal line *) - val pp_end_color : Format.formatter -> unit -> unit (** Print end color *) - - (** [pp_node_link path_to_root description isvisited isproof fmt id] prints an html link to the given node. - [path_to_root] is the path to the dir for the procedure in the spec db. - [description] is a string description. - [is_visited] indicates whether the node should be active or greyed out. - [is_proof] indicates whether the node is part of a proof and should be green. - [id] is the node identifier. *) - val pp_node_link : DB.Results_dir.path -> string -> int list -> int list -> int list -> bool -> bool -> Format.formatter -> int -> unit - val pp_proc_link : DB.Results_dir.path -> Procname.t -> Format.formatter -> string -> unit (** Print an html link to the given proc *) - val pp_session_link : ?with_name: bool -> string list -> Format.formatter -> int * int * int -> unit (** Print an html link given node id and session *) - val pp_start_color : Format.formatter -> color -> unit (** Print start color *) -end = struct +module Html = +struct + (** Create a new html file *) let create pk path = let fname, dir_path = match IList.rev path with - | fname:: dir_path -> fname, dir_path - | [] -> raise (Failure "Html.create") in - let fd = DB.Results_dir.create_file pk (IList.rev ((fname ^ ".html") :: dir_path)) in + | fname :: path_rev -> + fname, IList.rev ((fname ^ ".html") :: path_rev) + | [] -> + raise (Failure "Html.create") in + let fd = DB.Results_dir.create_file pk dir_path in let outc = Unix.out_channel_of_descr fd in let fmt = F.formatter_of_out_channel outc in - let (++) x y = x ^ "\n" ^ y in let s = - "" ++ - "\n\n" ^ fname ^ "" ++ - "" ++ - "" ++ - "" ++ - "" in + "\n\ + \n\ + \n\ + " ^ + fname ^ + "\n\ + \n\ + \ + \n\ + \ + \n" in F.fprintf fmt "%s" s; (fd, fmt) - (** get the full html filename from a path *) + (** Get the full html filename from a path *) let get_full_fname path = - let fname, dir_path = match IList.rev path with - | fname:: dir_path -> fname, dir_path - | [] -> raise (Failure "Html.open_out") in - DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir (IList.rev ((fname ^ ".html") :: dir_path)) + let dir_path = match IList.rev path with + | fname :: path_rev -> + IList.rev ((fname ^ ".html") :: path_rev) + | [] -> + raise (Failure "Html.open_out") in + DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir dir_path + (** Open an Html file to append data *) let open_out path = let full_fname = get_full_fname path in - let fd = Unix.openfile (DB.filename_to_string full_fname) [Unix.O_WRONLY; Unix.O_APPEND] 0o777 in + let fd = + Unix.openfile + (DB.filename_to_string full_fname) + [Unix.O_WRONLY; Unix.O_APPEND] + 0o777 in let outc = Unix.out_channel_of_descr fd in let fmt = F.formatter_of_out_channel outc in (fd, fmt) + (** Return true if the html file was modified since the beginning of the analysis *) let modified_during_analysis path = let fname = get_full_fname path in if DB.file_exists fname then DB.file_modified_time fname >= initial_analysis_time else false + (** Close an Html file *) let close (fd, fmt) = F.fprintf fmt "@\n@."; Unix.close fd @@ -136,58 +168,86 @@ end = struct let pp_end_color fmt () = F.fprintf fmt "%s" "" - let pp_link ?(name = None) ?(pos = None) path fmt text = + let pp_link ?(name = None) ?(pos = None) ~path fmt text = let pos_str = match pos with | None -> "" | Some s -> "#" ^ s in - let link_str = (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Rel path)) ^ ".html" ^ pos_str in + let link_str = + (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Rel path)) + ^ ".html" + ^ pos_str in let name_str = match name with | None -> "" | Some n -> "name=\"" ^ n ^ "\"" in let pr_str = "" ^ text ^ "" in F.fprintf fmt " %s" pr_str - (** [pp_node_link path_to_root description isvisited isproof fmt id] prints an html link to the given node. *) + (** [pp_node_link path_to_root description isvisited isproof fmt id] + prints an html link to the given node. *) let pp_node_link path_to_root description preds succs exn isvisited isproof fmt id = let display_name = - (if description = "" then "N" else String.sub description 0 1) ^ "_" ^ (string_of_int id) in + (if description = "" then "N" else String.sub description 0 1) + ^ "_" + ^ (string_of_int id) in let node_name = "node" ^ string_of_int id in - let style_class = if not isvisited then "dangling" else if isproof then "visitedproof" else "visited" in + let style_class = + if not isvisited + then "dangling" + else if isproof then "visitedproof" else "visited" in let node_text = let pp fmt () = - Format.fprintf fmt "%snode%d preds:%a succs:%a exn:%a %s%s" + Format.fprintf fmt + "%s\ + \ + node%d preds:%a succs:%a exn:%a %s%s\ + \ + " style_class display_name id - (pp_seq Format.pp_print_int) preds (pp_seq Format.pp_print_int) succs (pp_seq Format.pp_print_int) exn - description (if not isvisited then "\nNOT VISITED" else "") in + (pp_seq Format.pp_print_int) preds + (pp_seq Format.pp_print_int) succs + (pp_seq Format.pp_print_int) exn + description + (if not isvisited then "\nNOT VISITED" else "") in pp_to_string pp () in - if not isvisited then F.fprintf fmt " %s" node_text - else pp_link (path_to_root @ ["nodes"; node_name]) fmt node_text + if not isvisited + then F.fprintf fmt " %s" node_text + else pp_link ~path: (path_to_root @ ["nodes"; node_name]) fmt node_text (** Print an html link to the given proc *) let pp_proc_link path_to_root proc_name fmt text = - pp_link (path_to_root @ [Procname.to_filename proc_name]) fmt text + pp_link ~path: (path_to_root @ [Procname.to_filename proc_name]) fmt text (** Print an html link to the given line number of the current source file *) let pp_line_link ?(with_name = false) ?(text = None) path_to_root fmt linenum = let fname = DB.source_file_encoding !DB.current_source in let linenum_str = string_of_int linenum in let name = "LINE" ^ linenum_str in - pp_link ~name: (if with_name then Some name else None) (path_to_root @ [".."; fname]) ~pos: (Some name) - fmt (match text with Some s -> s | None -> linenum_str) + pp_link + ~name: (if with_name then Some name else None) + ~pos: (Some name) + ~path: (path_to_root @ [".."; fname]) + fmt + (match text with Some s -> s | None -> linenum_str) (** Print an html link given node id and session *) let pp_session_link ?(with_name = false) path_to_root fmt (node_id, session, linenum) = let node_name = "node" ^ (string_of_int node_id) in let path_to_node = path_to_root @ ["nodes"; node_name] in let pos = "session" ^ (string_of_int session) in - pp_link ~name: (if with_name then Some pos else None) ~pos: (Some pos) path_to_node fmt (node_name ^ "#" ^ pos); + pp_link + ~name: (if with_name then Some pos else None) + ~pos: (Some pos) + ~path: path_to_node + fmt + (node_name ^ "#" ^ pos); F.fprintf fmt "(%a)" (pp_line_link path_to_root) linenum end (* =============== END of module Html =============== *) (* =============== START of module Xml =============== *) (** Create and print xml trees *) -module Xml = struct +module Xml = +struct let tag_branch = "branch" let tag_call_trace = "call_trace" let tag_callee = "callee" @@ -252,10 +312,20 @@ module Xml = struct let indent' = if newline = "" then "" else indent ^ " " in let space = if attributes = [] then "" else " " in let pp_inside fmt () = match forest with - | [] -> () - | [String s] -> pp fmt "%s" s - | _ -> pp fmt "%s%a%s" newline (pp_forest newline indent') forest indent in - pp fmt "%s<%s%s%a>%a%s" indent name space pp_attributes attributes pp_inside () name newline + | [] -> + () + | [String s] -> + pp fmt "%s" s + | _ -> + pp fmt "%s%a%s" newline (pp_forest newline indent') forest indent in + pp fmt "%s<%s%s%a>%a%s" + indent + name + space + pp_attributes attributes + pp_inside () + name + newline | String s -> F.fprintf fmt "%s%s%s" indent s newline and pp_forest newline indent fmt forest = diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 09a850084..112861157 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -101,7 +101,7 @@ let save_global_state () = current_source = !DB.current_source; delayed_prints = L.get_delayed_prints (); footprint_mode = !Config.footprint; - html_formatter = !Printer.html_formatter; + html_formatter = !Printer.curr_html_formatter; name_generator = Ident.NameGenerator.get_current (); symexec_state = State.save_state (); } @@ -112,7 +112,7 @@ let restore_global_state st = DB.current_source := st.current_source; L.set_delayed_prints st.delayed_prints; Config.footprint := st.footprint_mode; - Printer.html_formatter := st.html_formatter; + Printer.curr_html_formatter := st.html_formatter; Ident.NameGenerator.set_current st.name_generator; State.restore_state st.symexec_state; Timeout.resume_previous_timeout () @@ -157,7 +157,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc timestamp = summary.Specs.timestamp + 1 } in Specs.add_summary callee_pname summary'; Checkers.ST.store_summary callee_pname; - Printer.proc_write_log false callee_pdesc in + Printer.write_proc_html false callee_pdesc in let log_error_and_continue exn kind = Reporting.log_error callee_pname exn; diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index f954c8ad2..514579140 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -13,30 +13,92 @@ module L = Logging module F = Format -(** return true if the node was visited during footprint and during re-execution*) -let is_visited_phase node = +(** Module to read specific lines from files. + The data from any file will stay in memory until the handle is collected by the gc. *) +module LineReader = +struct + (** Map a file name to an array of string, one for each line in the file. *) + type t = (DB.source_file, string array) Hashtbl.t + + let create () = + Hashtbl.create 1 + + let read_file fname = + let cin = open_in fname in + let lines = ref [] in + try + while true do + let line_raw = input_line cin in + let line = + let len = String.length line_raw in + if len > 0 && String.get line_raw (len -1) = '\013' then + String.sub line_raw 0 (len -1) + else line_raw in + lines := line :: !lines + done; + assert false (* execution never reaches here *) + with End_of_file -> + (close_in cin; + Array.of_list (IList.rev !lines)) + + let file_data (hash: t) fname = + try + Some (Hashtbl.find hash fname) + with Not_found -> + try + let lines_arr = read_file (DB.source_file_to_string fname) in + Hashtbl.add hash fname lines_arr; + Some lines_arr + with exn when exn_not_failure exn -> None + + let from_file_linenum_original hash fname linenum = + match file_data hash fname with + | None -> None + | Some lines_arr -> + if linenum > 0 && linenum <= Array.length lines_arr + then Some lines_arr.(linenum -1) + else None + + let from_file_linenum hash fname linenum = + let fname_in_resdir = + DB.source_file_in_resdir fname in + let sourcefile_in_resdir = + DB.abs_source_file_from_path (DB.filename_to_string fname_in_resdir) in + from_file_linenum_original hash sourcefile_in_resdir linenum + + let from_loc hash loc = + from_file_linenum hash loc.Location.file loc.Location.line +end + + +(** Current formatter for the html output *) +let curr_html_formatter = ref F.std_formatter + +(** Return true if the node was visited during footprint and during re-execution*) +let node_is_visited node = let proc_desc = Cfg.Node.get_proc_desc node in let proc_name = Cfg.Procdesc.get_proc_name proc_desc in match Specs.get_summary proc_name with - | None -> false, false + | None -> + false, false | Some summary -> let stats = summary.Specs.stats in - let is_visited_fp = IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_fp in - let is_visited_re = IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_re in + let is_visited_fp = + IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_fp in + let is_visited_re = + IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_re in is_visited_fp, is_visited_re -(** return true if the node was visited during analysis *) +(** Return true if the node was visited during analysis *) let is_visited node = - let visited_fp, visited_re = is_visited_phase node in + let visited_fp, visited_re = node_is_visited node in visited_fp || visited_re -(** current formatter for the html output *) -let html_formatter = ref F.std_formatter - -(* =============== START of module Log_nodes =============== *) +(* =============== START of module NodesHtml =============== *) -(** Print information when starting and finishing the processing of a node *) -module Log_nodes : sig +(** Print information into html files for nodes + when starting and finishing the processing of a node *) +module NodesHtml : sig val start_node : int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> bool val finish_node : int -> unit @@ -53,7 +115,7 @@ end = struct (false, Io_infer.Html.open_out ["nodes"; node_fname]) else (true, Io_infer.Html.create DB.Results_dir.Abs_source_dir ["nodes"; node_fname]) in - html_formatter := fmt; + curr_html_formatter := fmt; Hashtbl.replace log_files (node_fname, !DB.current_source) fd; if needs_initialization then (F.fprintf fmt "

Cfg Node %a

" @@ -71,17 +133,19 @@ end = struct (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) (is_visited node) false fmt (Cfg.Node.get_id node)) preds; F.fprintf fmt "
SUCCS: @\n"; - IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) - (is_visited node) false fmt (Cfg.Node.get_id node)) succs; + IList.iter (fun node -> + Io_infer.Html.pp_node_link [".."] "" + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) + (is_visited node) false fmt (Cfg.Node.get_id node)) succs; F.fprintf fmt "
EXN: @\n"; - IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) - (is_visited node) false fmt (Cfg.Node.get_id node)) exn; + IList.iter (fun node -> + Io_infer.Html.pp_node_link [".."] "" + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) + (is_visited node) false fmt (Cfg.Node.get_id node)) exn; F.fprintf fmt "
@\n"; F.pp_print_flush fmt (); true @@ -92,13 +156,16 @@ end = struct let fname = id_to_fname nodeid in let fd = Hashtbl.find log_files (fname, !DB.current_source) in Unix.close fd; - html_formatter := F.std_formatter + curr_html_formatter := F.std_formatter end -(* =============== END of module Log_nodes =============== *) +(* =============== END of module NodesHtml =============== *) + +(* =============== Printing functions =============== *) -(** printing functions *) +(** Execute the delayed print actions *) let force_delayed_print fmt = - let pe_default = if !Config.write_html then pe_html Black else pe_text in + let pe_default = + if !Config.write_html then pe_html Black else pe_text in function | (L.PTatom, a) -> let (a: Sil.atom) = Obj.obj a in @@ -122,12 +189,24 @@ let force_delayed_print fmt = F.fprintf fmt "%s@[" !s | (L.PTinstr, i) -> let (i: Sil.instr) = Obj.obj i in - if !Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green (Sil.pp_instr (pe_html Green)) i Io_infer.Html.pp_end_color () - else Sil.pp_instr pe_text fmt i + if !Config.write_html + then + F.fprintf fmt "%a%a%a" + Io_infer.Html.pp_start_color Green + (Sil.pp_instr (pe_html Green)) i + Io_infer.Html.pp_end_color () + else + Sil.pp_instr pe_text fmt i | (L.PTinstr_list, il) -> let (il: Sil.instr list) = Obj.obj il in - if !Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green (Sil.pp_instr_list (pe_html Green)) il Io_infer.Html.pp_end_color () - else Sil.pp_instr_list pe_text fmt il + if !Config.write_html + then + F.fprintf fmt "%a%a%a" + Io_infer.Html.pp_start_color Green + (Sil.pp_instr_list (pe_html Green)) il + Io_infer.Html.pp_end_color () + else + Sil.pp_instr_list pe_text fmt il | (L.PTjprop_list, shallow_jpl) -> let ((shallow: bool), (jpl: Prop.normal Specs.Jprop.t list)) = Obj.obj shallow_jpl in Specs.Jprop.pp_list pe_default shallow fmt jpl @@ -139,8 +218,15 @@ let force_delayed_print fmt = Location.pp fmt loc | (L.PTnode_instrs, b_n) -> let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in - if !Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green (Cfg.Node.pp_instr (pe_html Green) io ~sub_instrs: b) n Io_infer.Html.pp_end_color () - else F.fprintf fmt "%a" (Cfg.Node.pp_instr pe_text io ~sub_instrs: b) n + if !Config.write_html + then + F.fprintf fmt "%a%a%a" + Io_infer.Html.pp_start_color Green + (Cfg.Node.pp_instrs (pe_html Green) io ~sub_instrs: b) n + Io_infer.Html.pp_end_color () + else + F.fprintf fmt "%a" + (Cfg.Node.pp_instrs pe_text io ~sub_instrs: b) n | (L.PToff, off) -> let (off: Sil.offset) = Obj.obj off in Sil.pp_offset pe_default fmt off @@ -182,21 +268,35 @@ let force_delayed_print fmt = Prop.pp_sigma pe_default fmt sigma | (L.PTspec, spec) -> let (spec: Prop.normal Specs.spec) = Obj.obj spec in - Specs.pp_spec (if !Config.write_html then pe_html Blue else pe_text) None fmt spec + Specs.pp_spec + (if !Config.write_html then pe_html Blue else pe_text) + None fmt spec | (L.PTstr, s) -> let (s: string) = Obj.obj s in F.fprintf fmt "%s" s | (L.PTstr_color, s) -> let (s: string), (c: color) = Obj.obj s in - if !Config.write_html then F.fprintf fmt "%a%s%a" Io_infer.Html.pp_start_color c s Io_infer.Html.pp_end_color () - else F.fprintf fmt "%s" s + if !Config.write_html + then + F.fprintf fmt "%a%s%a" + Io_infer.Html.pp_start_color c + s + Io_infer.Html.pp_end_color () + else + F.fprintf fmt "%s" s | (L.PTstrln, s) -> let (s: string) = Obj.obj s in F.fprintf fmt "%s@\n" s | (L.PTstrln_color, s) -> let (s: string), (c: color) = Obj.obj s in - if !Config.write_html then F.fprintf fmt "%a%s%a@\n" Io_infer.Html.pp_start_color c s Io_infer.Html.pp_end_color () - else F.fprintf fmt "%s@\n" s + if !Config.write_html + then + F.fprintf fmt "%a%s%a@\n" + Io_infer.Html.pp_start_color c + s + Io_infer.Html.pp_end_color () + else + F.fprintf fmt "%s@\n" s | (L.PTsub, sub) -> let (sub: Sil.subst) = Obj.obj sub in Prop.pp_sub pe_default fmt sub @@ -211,54 +311,86 @@ let force_delayed_print fmt = (pp_seq (Sil.pp_typ pe_default)) fmt tl | (L.PTerror, s) -> let (s: string) = Obj.obj s in - if !Config.write_html then F.fprintf fmt "%aERROR: %s%a" Io_infer.Html.pp_start_color Red s Io_infer.Html.pp_end_color () - else F.fprintf fmt "ERROR: %s" s + if !Config.write_html + then + F.fprintf fmt "%aERROR: %s%a" + Io_infer.Html.pp_start_color Red + s + Io_infer.Html.pp_end_color () + else + F.fprintf fmt "ERROR: %s" s | (L.PTwarning, s) -> let (s: string) = Obj.obj s in - if !Config.write_html then F.fprintf fmt "%aWARNING: %s%a" Io_infer.Html.pp_start_color Orange s Io_infer.Html.pp_end_color () - else F.fprintf fmt "WARNING: %s" s + if !Config.write_html + then + F.fprintf fmt "%aWARNING: %s%a" + Io_infer.Html.pp_start_color Orange + s + Io_infer.Html.pp_end_color () + else + F.fprintf fmt "WARNING: %s" s | (L.PTinfo, s) -> let (s: string) = Obj.obj s in - if !Config.write_html then F.fprintf fmt "%aINFO: %s%a" Io_infer.Html.pp_start_color Blue s Io_infer.Html.pp_end_color () - else F.fprintf fmt "INFO: %s" s + if !Config.write_html + then + F.fprintf fmt "%aINFO: %s%a" + Io_infer.Html.pp_start_color Blue + s + Io_infer.Html.pp_end_color () + else + F.fprintf fmt "INFO: %s" s -(** set printer hook as soon as this module is loaded *) +(** Set printer hook as soon as this module is loaded *) let () = L.printer_hook := force_delayed_print (** Execute the delayed print actions *) let force_delayed_prints () = Config.forcing_delayed_prints := true; - F.fprintf !html_formatter "@?"; (* flush html stream *) - IList.iter (force_delayed_print !html_formatter) (IList.rev (L.get_delayed_prints ())); - F.fprintf !html_formatter "@?"; + F.fprintf !curr_html_formatter "@?"; (* flush html stream *) + IList.iter + (force_delayed_print !curr_html_formatter) + (IList.rev (L.get_delayed_prints ())); + F.fprintf !curr_html_formatter "@?"; L.reset_delayed_prints (); Config.forcing_delayed_prints := false (** Start a session, and create a new html fine for the node if it does not exist yet *) -let _start_session node (loc: Location.t) proc_name session = +let start_session node (loc: Location.t) proc_name session = let node_id = Cfg.Node.get_id node in - (if Log_nodes.start_node node_id loc proc_name (Cfg.Node.get_preds node) (Cfg.Node.get_succs node) (Cfg.Node.get_exn node) - then F.fprintf !html_formatter "%a@[%a@]%a" Io_infer.Html.pp_start_color Green (Cfg.Node.pp_instr (pe_html Green) None ~sub_instrs: true) node Io_infer.Html.pp_end_color ()); - F.fprintf !html_formatter "%a%a" + (if NodesHtml.start_node + node_id loc proc_name + (Cfg.Node.get_preds node) + (Cfg.Node.get_succs node) + (Cfg.Node.get_exn node) + then + F.fprintf !curr_html_formatter "%a%a%a" + Io_infer.Html.pp_start_color Green + (Cfg.Node.pp_instrs (pe_html Green) None ~sub_instrs: true) node + Io_infer.Html.pp_end_color ()); + F.fprintf !curr_html_formatter "%a%a" Io_infer.Html.pp_hline () (Io_infer.Html.pp_session_link ~with_name: true [".."]) (node_id, session, loc.Location.line); - F.fprintf !html_formatter "%a" Io_infer.Html.pp_start_color Black + F.fprintf !curr_html_formatter "%a" + Io_infer.Html.pp_start_color Black -let start_session node loc proc_name session = - if !Config.write_html then _start_session node loc proc_name session +let node_start_session node loc proc_name session = + if !Config.write_html then + start_session node loc proc_name session (** Finish a session, and perform delayed print actions if required *) -let finish_session node = +let node_finish_session node = if !Config.test == false then force_delayed_prints () else L.reset_delayed_prints (); if !Config.write_html then begin - F.fprintf !html_formatter "%a" Io_infer.Html.pp_end_color (); - Log_nodes.finish_node (Cfg.Node.get_id node) + F.fprintf !curr_html_formatter "%a" + Io_infer.Html.pp_end_color (); + NodesHtml.finish_node (Cfg.Node.get_id node) end -(** Write log file for the proc *) -let proc_write_log whole_seconds pdesc = +(** Write html file for the procedure. + The boolean indicates whether to print whole seconds only *) +let write_proc_html whole_seconds pdesc = if !Config.write_html then begin let pname = Cfg.Procdesc.get_proc_name pdesc in @@ -267,28 +399,35 @@ let proc_write_log whole_seconds pdesc = let fd, fmt = Io_infer.Html.create DB.Results_dir.Abs_source_dir [Procname.to_filename pname] in F.fprintf fmt "

Procedure %a

@\n" - (Io_infer.Html.pp_line_link ~text: (Some (Escape.escape_xml (Procname.to_string pname))) []) + (Io_infer.Html.pp_line_link + ~text: (Some (Escape.escape_xml (Procname.to_string pname))) + []) linenum; IList.iter - (fun n -> Io_infer.Html.pp_node_link [] - (Cfg.Node.get_description (pe_html Black) n) - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) - (is_visited n) false fmt (Cfg.Node.get_id n)) + (fun n -> + Io_infer.Html.pp_node_link [] + (Cfg.Node.get_description (pe_html Black) n) + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) + (is_visited n) false fmt (Cfg.Node.get_id n)) nodes; (match Specs.get_summary pname with - | None -> () + | None -> + () | Some summary -> Specs.pp_summary (pe_html Black) whole_seconds fmt summary; Io_infer.Html.close (fd, fmt)) end (** Creare a hash table mapping line numbers to the set of errors occurring on that line *) -let create_errors_per_line err_log = +let create_table_err_per_line err_log = let err_per_line = Hashtbl.create 17 in let add_err _ loc _ _ _ err_name desc _ _ _ _ = - let err_str = Localise.to_string err_name ^ " " ^ (pp_to_string Localise.pp_error_desc desc) in + let err_str = + Localise.to_string err_name ^ + " " ^ + (pp_to_string Localise.pp_error_desc desc) in try let set = Hashtbl.find err_per_line loc.Location.line in Hashtbl.replace err_per_line loc.Location.line (StringSet.add err_str set) @@ -297,148 +436,128 @@ let create_errors_per_line err_log = Errlog.iter add_err err_log; err_per_line -(** create err message for html file *) +(** Create error message for html file *) let create_err_message err_string = "\n
" ^ err_string ^ "
" -(** Module to read specific lines from files. - The data from any file will stay in memory until the handle is collected by the gc *) -module LineReader : sig - type t - - (** create a line reader *) - val create : unit -> t - - (** get the line from a source file and line number *) - val from_file_linenum_original : t -> DB.source_file -> int -> string option - - (** get the line from a source file and line number looking for the copy of the file in the results dir *) - val from_file_linenum : t -> DB.source_file -> int -> string option - - (** get the line from a location looking for the copy of the file in the results dir *) - val from_loc : t -> Location.t -> string option -end = struct - - (* map a file name to an array of string, one for each line in the file *) - type t = (DB.source_file, string array) Hashtbl.t - - let create () = - Hashtbl.create 1 - - let read_file fname = - let cin = open_in fname in - let lines = ref [] in - try - while true do - let line_raw = input_line cin in - let line = - let len = String.length line_raw in - if len > 0 && String.get line_raw (len -1) = '\013' then - String.sub line_raw 0 (len -1) - else line_raw in - lines := line :: !lines - done; - assert false (* execution never reaches here *) - with End_of_file -> - (close_in cin; - Array.of_list (IList.rev !lines)) - - let file_data (hash: t) fname = - try - Some (Hashtbl.find hash fname) - with Not_found -> - try - let lines_arr = read_file (DB.source_file_to_string fname) in - Hashtbl.add hash fname lines_arr; - Some lines_arr - with exn when exn_not_failure exn -> None - - let from_file_linenum_original hash fname linenum = - match file_data hash fname with - | None -> None - | Some lines_arr -> - if linenum > 0 && linenum <= Array.length lines_arr - then Some lines_arr.(linenum -1) - else None - - let from_file_linenum hash fname linenum = - let fname_in_resdir = DB.source_file_in_resdir fname in - let sourcefile_in_resdir = DB.abs_source_file_from_path (DB.filename_to_string fname_in_resdir) in - from_file_linenum_original hash sourcefile_in_resdir linenum - - let from_loc hash loc = - from_file_linenum hash loc.Location.file loc.Location.line -end - -(** Create filename.c.html with line numbers and links to nodes *) -let c_file_write_html linereader fname cfg = - let proof_cover = ref Specs.Visitedset.empty in - let tbl = Hashtbl.create 11 in - let process_node n = +(** Create filename.ext.html. *) +let write_html_file linereader filename cfg = + let process_node nodes_tbl n = let lnum = (Cfg.Node.get_loc n).Location.line in let curr_nodes = - try Hashtbl.find tbl lnum + try Hashtbl.find nodes_tbl lnum with Not_found -> [] in - Hashtbl.replace tbl lnum (n:: curr_nodes) in - let fname_encoding = DB.source_file_encoding fname in - let (fd, fmt) = Io_infer.Html.create DB.Results_dir.Abs_source_dir [".."; fname_encoding] in - let global_err_log = Errlog.empty () in - let do_proc proc_name proc_desc = (* add the err_log of this proc to [global_err_log] *) + Hashtbl.replace nodes_tbl lnum (n:: curr_nodes) in + let fname_encoding = + DB.source_file_encoding filename in + let (fd, fmt) = + Io_infer.Html.create DB.Results_dir.Abs_source_dir [".."; fname_encoding] in + let do_proc proof_cover table_nodes_at_linenum global_err_log proc_name proc_desc = + (* add the err_log of this proc to [global_err_log] *) let proc_loc = (Cfg.Procdesc.get_loc proc_desc) in if Cfg.Procdesc.is_defined proc_desc && (DB.source_file_equal proc_loc.Location.file !DB.current_source) then begin - IList.iter process_node (Cfg.Procdesc.get_nodes proc_desc); + IList.iter (process_node table_nodes_at_linenum) (Cfg.Procdesc.get_nodes proc_desc); match Specs.get_summary proc_name with - | None -> () + | None -> + () | Some summary -> IList.iter - (fun sp -> proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover) + (fun sp -> + proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover) (Specs.get_specs_from_payload summary); Errlog.update global_err_log summary.Specs.attributes.ProcAttributes.err_log end in - Cfg.iter_proc_desc cfg do_proc; - let err_per_line = create_errors_per_line global_err_log in + + let pp_prelude () = + let s = + "

File " ^ + (DB.source_file_to_string !DB.current_source) ^ + "

\n" ^ + "\n" in + F.fprintf fmt "%s" s in + + let print_one_line proof_cover table_nodes_at_linenum table_err_per_line line_number = + let line_html = + match LineReader.from_file_linenum linereader !DB.current_source line_number with + | Some line_raw -> + Escape.escape_xml line_raw + | None -> + raise End_of_file in + let nodes_at_linenum = + try Hashtbl.find table_nodes_at_linenum line_number + with Not_found -> [] in + let errors_at_linenum = + try + let errset = Hashtbl.find table_err_per_line line_number in + StringSet.elements errset + with Not_found -> [] in + let linenum_str = string_of_int line_number in + let line_str = "LINE" ^ linenum_str in + let str = + "\n" in + + pp_prelude (); + let global_err_log = Errlog.empty () in + let table_nodes_at_linenum = Hashtbl.create 11 in + let proof_cover = ref Specs.Visitedset.empty in + Cfg.iter_proc_desc cfg (do_proc proof_cover table_nodes_at_linenum global_err_log); + let table_err_per_line = create_table_err_per_line global_err_log in + let linenum = ref 0 in + try - (let s = "

File " ^ (DB.source_file_to_string !DB.current_source) ^ "

\n" ^ - "
" ^ + linenum_str ^ + "" ^ + line_html in + F.fprintf fmt "%s" str; + IList.iter + (fun n -> + let isproof = + Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in + Io_infer.Html.pp_node_link + [fname_encoding] + (Cfg.Node.get_description (pe_html Black) n) + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) + (is_visited n) + isproof + fmt + (Cfg.Node.get_id n)) + nodes_at_linenum; + IList.iter + (fun n -> + match Cfg.Node.get_kind n with + | Cfg.Node.Start_node proc_desc -> + let proc_name = Cfg.Procdesc.get_proc_name proc_desc in + let num_specs = IList.length (Specs.get_specs proc_name) in + let label = + (Escape.escape_xml (Procname.to_string proc_name)) ^ + ": " ^ + (string_of_int num_specs) ^ + " specs" in + Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label + | _ -> + ()) + nodes_at_linenum; + IList.iter + (fun err_string -> + F.fprintf fmt "%s" (create_err_message err_string)) + errors_at_linenum; + F.fprintf fmt "%s" "
\n" in - F.fprintf fmt "%s" s); - let linenum = ref 0 in while true do incr linenum; - let line_html = match LineReader.from_file_linenum linereader !DB.current_source !linenum with - | Some line_raw -> Escape.escape_xml line_raw - | None -> raise End_of_file in - let nodes_at_linenum = - try Hashtbl.find tbl !linenum - with Not_found -> [] in - let errors_at_linenum = - try - let errset = Hashtbl.find err_per_line !linenum in - StringSet.elements errset - with Not_found -> [] in - let linenum_str = string_of_int !linenum in - let line_str = "LINE" ^ linenum_str in - let str = - "\n" + print_one_line proof_cover table_nodes_at_linenum table_err_per_line !linenum done with End_of_file -> (F.fprintf fmt "%s" "
" ^ linenum_str ^ "" ^ line_html in - F.fprintf fmt "%s" str; - IList.iter (fun n -> - let isproof = Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in - Io_infer.Html.pp_node_link [fname_encoding] (Cfg.Node.get_description (pe_html Black) n) (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) (is_visited n) isproof fmt (Cfg.Node.get_id n)) nodes_at_linenum; - IList.iter (fun n -> match Cfg.Node.get_kind n with - | Cfg.Node.Start_node proc_desc -> - let proc_name = Cfg.Procdesc.get_proc_name proc_desc in - let num_specs = IList.length (Specs.get_specs proc_name) in - let label = (Escape.escape_xml (Procname.to_string proc_name)) ^ ": " ^ (string_of_int num_specs) ^ " specs" in - Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label - | _ -> ()) nodes_at_linenum; - IList.iter (fun err_string -> F.fprintf fmt "%s" (create_err_message err_string)) errors_at_linenum; - F.fprintf fmt "%s" "
\n"; Errlog.pp_html [fname_encoding] fmt global_err_log; Io_infer.Html.close (fd, fmt)) -let c_files_write_html linereader exe_env = - if !Config.write_html then Exe_env.iter_files (c_file_write_html linereader) exe_env +(** Create filename.ext.html for each file in the exe_env. *) +let write_all_html_files linereader exe_env = + if !Config.write_html then + Exe_env.iter_files (write_html_file linereader) exe_env diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index 87f298eaf..bcd629c4f 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -10,27 +10,6 @@ (** Printers for the analysis results *) -(** Current html formatter *) -val html_formatter : Format.formatter ref - -(** return true if the node was visited during footprint and during re-execution*) -val is_visited_phase : Cfg.Node.t -> bool * bool - -(** return true if the node was visited during analysis *) -val is_visited : Cfg.Node.t -> bool - -(** Execute the delayed print actions *) -val force_delayed_prints : unit -> unit - -(** Start a session, and create a new html fine for the node if it does not exist yet *) -val start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit - -(** Finish a session, and perform delayed print actions if required *) -val finish_session : Cfg.node -> unit - -(** Write log file for the proc, the boolean indicates whether to print whole seconds only *) -val proc_write_log : bool -> Cfg.Procdesc.t -> unit - (** Module to read specific lines from files. The data from any file will stay in memory until the handle is collected by the gc *) module LineReader : sig @@ -49,5 +28,24 @@ module LineReader : sig val from_loc : t -> Location.t -> string option end -(** Create filename.c.html with line numbers and links to nodes for each file in the exe_env *) -val c_files_write_html : LineReader.t -> Exe_env.t -> unit +(** Current html formatter *) +val curr_html_formatter : Format.formatter ref + +(** Execute the delayed print actions *) +val force_delayed_prints : unit -> unit + +(** Finish a session, and perform delayed print actions if required *) +val node_finish_session : Cfg.node -> unit + +(** Return true if the node was visited during footprint and during re-execution *) +val node_is_visited : Cfg.Node.t -> bool * bool + +(** Start a session, and create a new html fine for the node if it does not exist yet *) +val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit + +(** Write html file for the procedure. + The boolean indicates whether to print whole seconds only. *) +val write_proc_html : bool -> Cfg.Procdesc.t -> unit + +(** Create filename.ext.html for each file in the exe_env. *) +val write_all_html_files : LineReader.t -> Exe_env.t -> unit