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

[logging] don't log debug html for preanalyses

Browse Source 
Summary:
It's distracting to see the debug HTML for the preanalysis when you're trying to debug something else.
Also, it breaks the nice bi-abduction debug feature of marking the visited nodes as green.

Reviewed By: akotulski

Differential Revision: D4858578

fbshipit-source-id: 8e77976
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent d7f39970d1
commit 093b3c6478
3 changed files with 28 additions and 21 deletions
Show Stats Download Patch File Download Diff File

12
infer/src/backend/preanal.ml
Unescape View File

@ -203,7 +203,8 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc pdesc in let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc pdesc in
let nullify_proc_data = ProcData.make pdesc tenv liveness_inv_map in let nullify_proc_data = ProcData.make pdesc tenv liveness_inv_map in
let initial = VarDomain.empty, VarDomain.empty in let initial = VarDomain.empty, VarDomain.empty in
let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in let nullify_inv_map =
NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial ~debug:false in
(* only nullify pvars that are local; don't nullify those that can escape *) (* only nullify pvars that are local; don't nullify those that can escape *)
let is_local pvar = let is_local pvar =
@ -255,7 +256,8 @@ module CopyProp =
let do_copy_propagation pdesc tenv = let do_copy_propagation pdesc tenv =
let proc_cfg = ExceptionalOneInstrPerNodeCfg.from_pdesc pdesc in let proc_cfg = ExceptionalOneInstrPerNodeCfg.from_pdesc pdesc in
let initial = CopyPropagation.Domain.empty in let initial = CopyPropagation.Domain.empty in
let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) ~initial in let copy_prop_inv_map =
CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) ~initial ~debug:false in
(* [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some (* [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some
ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an
ident. *) ident. *)
@ -301,7 +303,11 @@ let do_liveness pdesc tenv =
let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
let initial = Liveness.Domain.empty in let initial = Liveness.Domain.empty in
let liveness_inv_map = let liveness_inv_map =
LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) ~initial in LivenessAnalysis.exec_cfg
liveness_proc_cfg
(ProcData.make_default pdesc tenv)
~initial
~debug:false in
if Config.copy_propagation then do_copy_propagation pdesc tenv; if Config.copy_propagation then do_copy_propagation pdesc tenv;
add_nullify_instrs pdesc tenv liveness_inv_map; add_nullify_instrs pdesc tenv liveness_inv_map;
Procdesc.signal_did_preanalysis pdesc Procdesc.signal_did_preanalysis pdesc

33
infer/src/checkers/AbstractInterpreter.ml
Unescape View File

@ -26,6 +26,7 @@ module type S = sig
TransferFunctions.Domain.astate option TransferFunctions.Domain.astate option
val exec_cfg : val exec_cfg :
?debug:bool ->
TransferFunctions.CFG.t -> TransferFunctions.CFG.t ->
TransferFunctions.extras ProcData.t -> TransferFunctions.extras ProcData.t ->
initial:TransferFunctions.Domain.astate -> initial:TransferFunctions.Domain.astate ->
@ -69,7 +70,7 @@ module MakeNoCFG
| Some state -> Some state.pre | Some state -> Some state.pre
| None -> None | None -> None
let exec_node node astate_pre work_queue inv_map ({ ProcData.pdesc; } as proc_data) = let exec_node node astate_pre work_queue inv_map ({ ProcData.pdesc; } as proc_data) ~debug =
let node_id = CFG.id node in let node_id = CFG.id node in
let update_inv_map pre visit_count = let update_inv_map pre visit_count =
let compute_post (pre, inv_map) (instr, id_opt) = let compute_post (pre, inv_map) (instr, id_opt) =
@ -81,20 +82,18 @@ module MakeNoCFG
let instr_ids = match CFG.instr_ids node with let instr_ids = match CFG.instr_ids node with
| [] -> [Sil.skip_instr, None] | [] -> [Sil.skip_instr, None]
| l -> l in | l -> l in
let underlying_node = CFG.underlying_node node in if debug then NodePrinter.start_session (CFG.underlying_node node);
NodePrinter.start_session underlying_node;
let astate_post, inv_map_post = let astate_post, inv_map_post =
List.fold ~f:compute_post ~init:(pre, inv_map) instr_ids in List.fold ~f:compute_post ~init:(pre, inv_map) instr_ids in
if Config.write_html if debug
then then
begin begin
let str = let instrs = List.map ~f:fst instr_ids in
let instrs = List.map ~f:fst instr_ids in L.d_strln
Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@."
Domain.pp pre (Sil.pp_instr_list Pp.text) instrs Domain.pp astate_post in Domain.pp pre (Sil.pp_instr_list Pp.text) instrs Domain.pp astate_post);
L.d_strln str NodePrinter.finish_session (CFG.underlying_node node);
end; end;
NodePrinter.finish_session underlying_node;
let inv_map'' = let inv_map'' =
InvariantMap.add node_id { pre; post=astate_post; visit_count; } inv_map_post in InvariantMap.add node_id { pre; post=astate_post; visit_count; } inv_map_post in
inv_map'', Scheduler.schedule_succs work_queue node in inv_map'', Scheduler.schedule_succs work_queue node in
@ -114,7 +113,7 @@ module MakeNoCFG
let visit_count = 1 in let visit_count = 1 in
update_inv_map astate_pre visit_count update_inv_map astate_pre visit_count
let rec exec_worklist cfg work_queue inv_map proc_data = let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
let compute_pre node inv_map = let compute_pre node inv_map =
(* if the [pred] -> [node] transition was normal, use post([pred]) *) (* if the [pred] -> [node] transition was normal, use post([pred]) *)
let extract_post_ pred = extract_post (CFG.id pred) inv_map in let extract_post_ pred = extract_post (CFG.id pred) inv_map in
@ -128,21 +127,21 @@ module MakeNoCFG
| [] -> None in | [] -> None in
match Scheduler.pop work_queue with match Scheduler.pop work_queue with
| Some (_, [], work_queue') -> | Some (_, [], work_queue') ->
exec_worklist cfg work_queue' inv_map proc_data exec_worklist cfg work_queue' inv_map proc_data ~debug
| Some (node, _, work_queue') -> | Some (node, _, work_queue') ->
let inv_map_post, work_queue_post = match compute_pre node inv_map with let inv_map_post, work_queue_post = match compute_pre node inv_map with
| Some astate_pre -> exec_node node astate_pre work_queue' inv_map proc_data | Some astate_pre -> exec_node node astate_pre work_queue' inv_map proc_data ~debug
| None -> inv_map, work_queue' in | None -> inv_map, work_queue' in
exec_worklist cfg work_queue_post inv_map_post proc_data exec_worklist cfg work_queue_post inv_map_post proc_data ~debug
| None -> | None ->
inv_map inv_map
(* compute and return an invariant map for [cfg] *) (* compute and return an invariant map for [cfg] *)
let exec_cfg cfg proc_data ~initial = let exec_cfg ?(debug=Config.write_html) cfg proc_data ~initial =
let start_node = CFG.start_node cfg in let start_node = CFG.start_node cfg in
let inv_map', work_queue' = let inv_map', work_queue' =
exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data in exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data ~debug in
exec_worklist cfg work_queue' inv_map' proc_data exec_worklist cfg work_queue' inv_map' proc_data ~debug
(* compute and return an invariant map for [pdesc] *) (* compute and return an invariant map for [pdesc] *)
let exec_pdesc ({ ProcData.pdesc; } as proc_data) = let exec_pdesc ({ ProcData.pdesc; } as proc_data) =

4
infer/src/checkers/AbstractInterpreter.mli
Unescape View File

@ -26,8 +26,10 @@ module type S = sig
initial:TransferFunctions.Domain.astate -> initial:TransferFunctions.Domain.astate ->
TransferFunctions.Domain.astate option TransferFunctions.Domain.astate option
(** compute and return invariant map for the given CFG/procedure starting from [initial] *) (** compute and return invariant map for the given CFG/procedure starting from [initial]. if
[debug] is true, print html debugging output. *)
val exec_cfg : val exec_cfg :
?debug:bool ->
TransferFunctions.CFG.t -> TransferFunctions.CFG.t ->
TransferFunctions.extras ProcData.t -> TransferFunctions.extras ProcData.t ->
initial:TransferFunctions.Domain.astate -> initial:TransferFunctions.Domain.astate ->

Write Preview
Loading…
Cancel
Save