From 2be47108111bbdad247541147c53978bf0d9da2f Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 9 Oct 2018 03:19:59 -0700 Subject: [PATCH] [AI] Enable debugging only based on --write-html Reviewed By: ezgicicek Differential Revision: D10238681 fbshipit-source-id: 08eeedd26 --- infer/src/absint/AbstractInterpreter.ml | 35 ++++++++++++++++-------- infer/src/absint/AbstractInterpreter.mli | 11 ++++---- infer/src/absint/LowerHil.ml | 4 ++- infer/src/backend/preanal.ml | 8 ++---- infer/src/checkers/cost.ml | 6 +--- infer/src/checkers/hoisting.ml | 1 - infer/src/checkers/liveness.ml | 4 +-- 7 files changed, 36 insertions(+), 33 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index b0e4b6006..9b96916db 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -9,6 +9,14 @@ open! IStd module F = Format module L = Logging +type debug = + | Default + | DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + (** If Default is used from LowerHil, debug html files will be opened twice and closed twice (boom!), + because both LowerHil-AI and SIL-AI want to print instructions and pre/post states. + When using LowerHil-AI, we're not interested in the underlying SIL instructions, + it's the only case where want to disable it. *) + type 'a state = {pre: 'a; post: 'a; visit_count: int} module type S = sig @@ -19,7 +27,7 @@ module type S = sig type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t val compute_post : - ?debug:bool + ?debug:debug -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> TransferFunctions.Domain.astate option @@ -28,7 +36,6 @@ module type S = sig TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate - -> debug:bool -> invariant_map val exec_pdesc : @@ -89,7 +96,8 @@ struct let node_id = Node.id node in let update_inv_map pre ~visit_count = let exec_instrs instrs = - if debug then + if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + then NodePrinter.start_session ~pp_name:(TransferFunctions.pp_session_name node) (Node.underlying_node node) ; @@ -101,7 +109,8 @@ struct in Instrs.fold ~f:compute_post ~init:pre instrs in - if debug then ( + if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + then ( L.d_strln ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre (Instrs.pp Pp.text) instrs Domain.pp astate_post @@ -123,7 +132,8 @@ struct let prev = old_state.pre in let next = astate_pre in let res = Domain.widen ~prev ~next ~num_iters in - if debug then debug_absint_operation (`Widen (num_iters, (prev, next, res))) node ; + if Config.write_html then + debug_absint_operation (`Widen (num_iters, (prev, next, res))) node ; res ) else astate_pre in @@ -153,7 +163,8 @@ struct some_post | Some joined_post -> let res = Domain.join joined_post post in - if debug then debug_absint_operation (`Join (joined_post, post, res)) node ; + if Config.write_html then + debug_absint_operation (`Join (joined_post, post, res)) node ; Some res ) ) in match Scheduler.pop work_queue with @@ -173,7 +184,7 @@ struct (* compute and return an invariant map for [cfg] *) - let exec_cfg cfg proc_data ~initial ~debug = + let exec_cfg_internal ~debug cfg proc_data ~initial = let start_node = CFG.start_node cfg in let inv_map', work_queue' = exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data ~debug @@ -181,15 +192,15 @@ struct exec_worklist cfg work_queue' inv_map' proc_data ~debug - (* compute and return an invariant map for [pdesc] *) - let exec_pdesc ({ProcData.pdesc} as proc_data) = - exec_cfg (CFG.from_pdesc pdesc) proc_data ~debug:Config.write_html + let exec_cfg = exec_cfg_internal ~debug:Default + (* compute and return an invariant map for [pdesc] *) + let exec_pdesc ({ProcData.pdesc} as proc_data) = exec_cfg (CFG.from_pdesc pdesc) proc_data (* compute and return the postcondition of [pdesc] *) - let compute_post ?(debug = Config.write_html) ({ProcData.pdesc} as proc_data) ~initial = + let compute_post ?(debug = Default) ({ProcData.pdesc} as proc_data) ~initial = let cfg = CFG.from_pdesc pdesc in - let inv_map = exec_cfg cfg proc_data ~initial ~debug in + let inv_map = exec_cfg_internal cfg proc_data ~initial ~debug in extract_post (Node.id (CFG.exit_node cfg)) inv_map end diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index 7c83386c5..4915244ab 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -7,6 +7,8 @@ open! IStd +type debug = Default | DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + type 'a state = {pre: 'a; post: 'a; visit_count: int} (** type of an intraprocedural abstract interpreter *) @@ -19,21 +21,18 @@ module type S = sig type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t val compute_post : - ?debug:bool + ?debug:debug -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> TransferFunctions.Domain.astate option - (** compute and return the postcondition for the given procedure starting from [initial]. If - [debug] is true, print html debugging output. *) + (** compute and return the postcondition for the given procedure starting from [initial]. *) val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate - -> debug:bool -> invariant_map - (** compute and return invariant map for the given CFG/procedure starting from [initial]. if - [debug] is true, print html debugging output. *) + (** compute and return invariant map for the given CFG/procedure starting from [initial]. *) val exec_pdesc : TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 65ab55b7d..aa36f0071 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -92,10 +92,12 @@ module MakeAbstractInterpreterWithConfig struct module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig)) + let debug = AbstractInterpreter.DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial = Preanal.do_preanalysis pdesc tenv ; let initial' = (initial, IdAccessPathMapDomain.empty) in - Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial') + Option.map ~f:fst (Interpreter.compute_post ~debug proc_data ~initial:initial') end module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index faf53c851..a06ad1142 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -124,9 +124,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map = let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc pdesc in let nullify_proc_data = ProcData.make pdesc tenv liveness_inv_map in let initial = (VarDomain.empty, VarDomain.empty) in - let nullify_inv_map = - NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial ~debug:false - in + let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in (* only nullify pvars that are local; don't nullify those that can escape *) let is_local pvar = not (Pvar.is_return pvar || Pvar.is_global pvar) in let node_nullify_instructions loc pvars = @@ -172,9 +170,7 @@ let do_liveness pdesc tenv = let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in let initial = Liveness.Domain.empty in let liveness_inv_map = - LivenessAnalysis.exec_cfg liveness_proc_cfg - (ProcData.make_default pdesc tenv) - ~initial ~debug:false + LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) ~initial in add_nullify_instrs pdesc tenv liveness_inv_map ; Procdesc.signal_did_preanalysis pdesc diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 9e89609f8..8df95d147 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -746,7 +746,6 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = let reaching_defs_invariant_map = ReachingDefs.Analyzer.exec_cfg node_cfg proc_data ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc) - ~debug:false in (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) let control_maps, loop_head_to_loop_nodes = Loop_control.get_control_maps node_cfg in @@ -754,14 +753,12 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = let control_dep_invariant_map = let proc_data = ProcData.make proc_desc tenv control_maps in Control.ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:Control.ControlDepSet.empty - ~debug:false in let instr_cfg = InstrCFG.from_pdesc proc_desc in let invariant_map_NodesBasicCost = let proc_data = ProcData.make proc_desc tenv inferbo_invariant_map in (*compute_WCET cfg invariant_map min_trees in *) AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty - ~debug:false in (* compute loop invariant map for control var analysis *) let loop_inv_map = @@ -779,10 +776,9 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = in let initWCET = (BasicCost.zero, ReportedOnNodes.empty) in match - AnalyzerWCET.compute_post + AnalyzerWCET.compute_post ~initial:initWCET (ProcData.make proc_desc tenv {basic_cost_map= invariant_map_NodesBasicCost; get_node_nb_exec; summary}) - ~debug:false ~initial:initWCET with | Some (exit_cost, _) -> L.internal_error "@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index d55fd6e09..a22b9830d 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -80,7 +80,6 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t = let reaching_defs_invariant_map = ReachingDefs.Analyzer.exec_cfg cfg proc_data ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc) - ~debug:false in (* get dominators *) let idom = Dominators.get_idoms proc_desc in diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 92f3f95fe..08830ae1f 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -122,14 +122,14 @@ module CapturedByRefAnalyzer = let get_captured_by_ref_invariant_map proc_desc proc_data = let cfg = ProcCfg.Exceptional.from_pdesc proc_desc in - CapturedByRefAnalyzer.exec_cfg cfg proc_data ~initial:VarSet.empty ~debug:false + CapturedByRefAnalyzer.exec_cfg cfg proc_data ~initial:VarSet.empty let checker {Callbacks.tenv; summary; proc_desc} : Summary.t = let proc_data = ProcData.make_default proc_desc tenv in let captured_by_ref_invariant_map = get_captured_by_ref_invariant_map proc_desc proc_data in let cfg = CFG.from_pdesc proc_desc in - let invariant_map = Analyzer.exec_cfg cfg proc_data ~initial:Domain.empty ~debug:false in + let invariant_map = Analyzer.exec_cfg cfg proc_data ~initial:Domain.empty in (* we don't want to report in harmless cases like int i = 0; if (...) { i = ... } else { i = ... } that create an intentional dead store as an attempt to imitate default value semantics. use dead stores to a "sentinel" value as a heuristic for ignoring this case *)