From 6af61d099e46c3abac76c2842030de9a44c95085 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 23 May 2017 16:21:49 -0700 Subject: [PATCH] [HIL] Print HIL instructions in the debug HTML Summary: The debug HTML for Quandary/thread-safety was still printing the SIL instructions, which is not very helpful. Print the HIL instructions instead. Reviewed By: jeremydubreil Differential Revision: D5112696 fbshipit-source-id: a0aa925 --- infer/src/checkers/AbstractInterpreter.ml | 12 ++++++------ infer/src/checkers/AbstractInterpreter.mli | 6 ++++-- infer/src/checkers/LowerHil.ml | 17 +++++++++++++++++ infer/src/checkers/ThreadSafety.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 2 +- 5 files changed, 29 insertions(+), 10 deletions(-) diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 40c1a83e2..282dddb29 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -21,15 +21,16 @@ module type S = sig type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t val compute_post : + ?debug:bool -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> TransferFunctions.Domain.astate option val exec_cfg : - ?debug:bool -> TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> + debug:bool -> invariant_map val exec_pdesc : @@ -137,7 +138,7 @@ module MakeNoCFG inv_map (* compute and return an invariant map for [cfg] *) - let exec_cfg ?(debug=Config.write_html) cfg proc_data ~initial = + let exec_cfg cfg proc_data ~initial ~debug = 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 in @@ -145,14 +146,13 @@ module MakeNoCFG (* compute and return an invariant map for [pdesc] *) let exec_pdesc ({ ProcData.pdesc; } as proc_data) = - exec_cfg (CFG.from_pdesc pdesc) proc_data + exec_cfg (CFG.from_pdesc pdesc) proc_data ~debug:Config.write_html (* compute and return the postcondition of [pdesc] *) - let compute_post ({ ProcData.pdesc; } as proc_data) ~initial = + let compute_post ?(debug=Config.write_html) ({ ProcData.pdesc; } as proc_data) ~initial = let cfg = CFG.from_pdesc pdesc in - let inv_map = exec_cfg cfg proc_data ~initial in + let inv_map = exec_cfg cfg proc_data ~initial ~debug in extract_post (CFG.id (CFG.exit_node cfg)) inv_map - end module Interprocedural (Summ : Summary.S) = struct diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index e64404ffb..89fbaa97b 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -20,8 +20,10 @@ module type S = sig (** invariant map from node id -> state representing postcondition for node id *) type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t - (** compute and return the postcondition for the given procedure starting from [initial] *) + (** compute and return the postcondition for the given procedure starting from [initial]. If + [debug] is true, print html debugging output. *) val compute_post : + ?debug:bool -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> TransferFunctions.Domain.astate option @@ -29,10 +31,10 @@ module type S = sig (** compute and return invariant map for the given CFG/procedure starting from [initial]. if [debug] is true, print html debugging output. *) val exec_cfg : - ?debug:bool -> TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> + debug:bool -> invariant_map (** compute and return invariant map for the given procedure starting from [initial] *) diff --git a/infer/src/checkers/LowerHil.ml b/infer/src/checkers/LowerHil.ml index 991228e8f..5361b20b4 100644 --- a/infer/src/checkers/LowerHil.ml +++ b/infer/src/checkers/LowerHil.ml @@ -9,6 +9,8 @@ open! IStd +module L = Logging + module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) = struct module TransferFunctions = MakeTransferFunctions (CFG) module CFG = TransferFunctions.CFG @@ -16,6 +18,7 @@ module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S type extras = TransferFunctions.extras let exec_instr ((actual_state, id_map) as astate) extras node instr = + let f_resolve_id id = try Some (IdAccessPathMapDomain.find id id_map) with Not_found -> None in @@ -34,6 +37,20 @@ module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S else actual_state, id_map' | Instr hil_instr -> let actual_state' = TransferFunctions.exec_instr actual_state extras node hil_instr in + if Config.write_html + then + begin + let underyling_node = CFG.underlying_node node in + NodePrinter.start_session underyling_node; + L.d_strln + (Format.asprintf + "PRE: %a@.INSTR: %a@.POST: %a@." + TransferFunctions.Domain.pp (fst astate) + HilInstr.pp hil_instr + TransferFunctions.Domain.pp actual_state'); + NodePrinter.finish_session underyling_node; + end; + if phys_equal actual_state actual_state' then astate else actual_state', id_map diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 3fb460df7..750e9c0c7 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -805,7 +805,7 @@ let analyze_procedure callback = else { ThreadSafetyDomain.empty with threads; }, IdAccessPathMapDomain.empty in - match Analyzer.compute_post proc_data ~initial with + match Analyzer.compute_post proc_data ~initial ~debug:false with | Some ({ threads; locks; accesses; attribute_map; }, _) -> let return_var_ap = AccessPath.of_pvar diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 5e58f7768..15fdb4ca1 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -562,7 +562,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct proc_data.pdesc (Cg.create (SourceFile.invalid __FILE__)) proc_data.tenv; end; let initial = make_initial proc_data.pdesc in - match Analyzer.compute_post proc_data ~initial with + match Analyzer.compute_post proc_data ~initial ~debug:false with | Some (access_tree, _) -> Some (make_summary proc_data access_tree) | None ->