[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
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent c10c7a39a6
commit 317a74ffee

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

@ -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. *)

Loading…
Cancel
Save