From 317a74ffee8da1035f5975b3e2a6fec461ccdeee Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 20 Feb 2020 03:28:16 -0800
Subject: [PATCH] [nullsafe] show state after each instruction in debug HTML

Summary:
This helps debug nullsafe. Before, we would only print the initial and
last state of a given node but now we can see all the intermediate steps
too.

Example before:
```
before:
  &s -> [Param s ] [UncheckedNonnull] java.lang.String*
  &this -> [this] [StrictNonnull] Toto*

after:
  &s -> [Param s ] [UncheckedNonnull] java.lang.String*
  &this -> [this] [StrictNonnull] Toto*
```

After:
```
before:
  &s -> [Param s ] [UncheckedNonnull] java.lang.String*
  &this -> [this] [StrictNonnull] Toto*

instr: n$0=*&this:Toto* [line 10]

new state:
  n$0 -> [this] [StrictNonnull] Toto*
  &s -> [Param s ] [UncheckedNonnull] java.lang.String*
  &this -> [this] [StrictNonnull] Toto*

...

instr: EXIT_SCOPE(n$0,n$1,this); [line 10]

new state:
  &s -> [Param s ] [UncheckedNonnull] java.lang.String*
  &this -> [this] [StrictNonnull] Toto*
```

Reviewed By: mityal

Differential Revision: D19973278

fbshipit-source-id: bcea33f96
---
 infer/src/nullsafe/eradicate.ml | 7 +------
 infer/src/nullsafe/typeCheck.ml | 9 +++++++--
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml
index a8736843e..2f0c3884f 100644
--- a/infer/src/nullsafe/eradicate.ml
+++ b/infer/src/nullsafe/eradicate.ml
@@ -94,16 +94,11 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
       let do_node tenv node typestate =
         NodePrinter.with_session ~pp_name node ~f:(fun () ->
             State.set_node node ;
+            if Config.write_html then L.d_printfln "before:@\n%a@\n" TypeState.pp typestate ;
             let typestates_succ, typestates_exn =
               TypeCheck.typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc
                 find_canonical_duplicate annotated_signature typestate node linereader
             in
-            if Config.write_html then (
-              let d_typestate ts = L.d_printfln "%a" TypeState.pp ts in
-              L.d_strln "before:" ;
-              d_typestate typestate ;
-              L.d_strln "after:" ;
-              List.iter ~f:d_typestate typestates_succ ) ;
             (typestates_succ, typestates_exn) )
 
 
diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml
index a8cad4878..1d6c852f9 100644
--- a/infer/src/nullsafe/typeCheck.ml
+++ b/infer/src/nullsafe/typeCheck.ml
@@ -7,6 +7,7 @@
 
 open! IStd
 module F = Format
+module L = Logging
 module DExp = DecompiledExp
 
 (** Module for type checking. *)
@@ -1199,11 +1200,15 @@ let typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canon
       (* keep unique instruction reference per-node *)
       TypeErr.InstrRef.gen instr_ref_gen
     in
-    let instr' =
+    let post =
       typecheck_instr tenv calls_this checks node idenv curr_pname curr_pdesc
         find_canonical_duplicate annotated_signature instr_ref linereader typestate instr
     in
-    handle_exceptions typestate instr ; instr'
+    if Config.write_html then (
+      L.d_printfln "instr: %a@\n" (Sil.pp_instr ~print_types:true Pp.text) instr ;
+      L.d_printfln "new state:@\n%a@\n" TypeState.pp post ) ;
+    handle_exceptions typestate instr ;
+    post
   in
   (* Reset 'always' field for forall errors to false. *)
   (* This is used to track if it is set to true for all visit to the node. *)