From bc9c2440df5eb29fef8c9dcfe6863ccad445d212 Mon Sep 17 00:00:00 2001
From: Artem Pianykh <arr@fb.com>
Date: Wed, 24 Jun 2020 07:17:57 -0700
Subject: [PATCH] [java] Add an option to log JBir translation

Summary: Add a new option `--print-jbir` to output JBir representation in verbose debug logs.

Reviewed By: skcho

Differential Revision: D22183963

fbshipit-source-id: a5140d638
---
 infer/man/man1/infer-full.txt | 4 ++++
 infer/src/base/Config.ml      | 6 ++++++
 infer/src/base/Config.mli     | 2 ++
 infer/src/java/jTrans.ml      | 8 ++++++++
 4 files changed, 20 insertions(+)

diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index d130225ba..23d413059 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -1638,6 +1638,10 @@ INTERNAL OPTIONS
            Activates: Print the builtin functions and exit (Conversely:
            --no-print-builtins)
 
+       --print-jbir
+           Activates: Print JBir translation of Java bytecode in logs
+           (Conversely: --no-print-jbir)
+
        --print-types
            Activates: Print types in symbolic heaps (Conversely:
            --no-print-types)
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 2e1970c3e..fea08d404 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -982,6 +982,7 @@ and ( bo_debug
     , linters_developer_mode
     , only_cheap_debug
     , print_buckets
+    , print_jbir
     , print_logs
     , print_types
     , reports_include_ml_loc
@@ -1032,6 +1033,8 @@ and ( bo_debug
   and print_buckets =
     CLOpt.mk_bool ~long:"print-buckets"
       "Show the internal bucket of Infer reports in their textual description"
+  and print_jbir =
+    CLOpt.mk_bool ~long:"print-jbir" "Print JBir translation of Java bytecode in logs"
   and print_types = CLOpt.mk_bool ~long:"print-types" ~default:false "Print types in symbolic heaps"
   and keep_going =
     CLOpt.mk_bool ~deprecated_no:["-no-failures-allowed"] ~long:"keep-going"
@@ -1135,6 +1138,7 @@ and ( bo_debug
   , linters_developer_mode
   , only_cheap_debug
   , print_buckets
+  , print_jbir
   , print_logs
   , print_types
   , reports_include_ml_loc
@@ -3066,6 +3070,8 @@ and select = !select
 
 and show_buckets = !print_buckets
 
+and print_jbir = !print_jbir
+
 and siof_check_iostreams = !siof_check_iostreams
 
 and siof_safe_methods = !siof_safe_methods
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 22320c2c4..a4ab93990 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -417,6 +417,8 @@ val print_active_checkers : bool
 
 val print_builtins : bool
 
+val print_jbir : bool
+
 val print_logs : bool
 
 val print_types : bool
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index e3dff46f2..33d0d0955 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -282,6 +282,11 @@ let get_jbir_representation cm bytecode =
     bytecode
 
 
+let pp_jbir fmt jbir =
+  (Format.pp_print_list ~pp_sep:Format.pp_print_newline Format.pp_print_string)
+    fmt (JBir.print jbir)
+
+
 let trans_access = function
   | `Default ->
       PredSymb.Default
@@ -423,6 +428,9 @@ let create_cm_procdesc source_file program icfg cm proc_name =
   try
     let bytecode = get_bytecode cm in
     let jbir_code = get_jbir_representation cm bytecode in
+    if Config.print_jbir then
+      L.(debug Capture Verbose)
+        "Printing JBir of: %a@\n@[%a@]@." Procname.pp proc_name pp_jbir jbir_code ;
     let loc_start = get_start_location source_file proc_name bytecode in
     let loc_exit = get_exit_location source_file bytecode in
     let formals = translate_formals program tenv cn jbir_code in