[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

@@ -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

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] *)

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

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

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 ->