From 6861a2af155e726c39013d733af9bc6e94f88818 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Wed, 6 Jun 2018 07:03:23 -0700
Subject: [PATCH] Absint: add debugging for join and widen

Reviewed By: jeremydubreil

Differential Revision: D8283561

fbshipit-source-id: c9af6d9
---
 infer/src/absint/AbstractInterpreter.ml | 32 ++++++++++++++++++++++---
 1 file changed, 29 insertions(+), 3 deletions(-)

diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index 5948f4cf8..bfc9a27e5 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/infer/src/absint/AbstractInterpreter.ml
@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module F = Format
 module L = Logging
 
 type 'a state = {pre: 'a; post: 'a; visit_count: int}
@@ -60,6 +61,24 @@ struct
     match extract_state node_id inv_map with Some state -> Some state.pre | None -> None
 
 
+  let debug_absint_operation op node =
+    let pp_name fmt =
+      TransferFunctions.pp_session_name node fmt ;
+      match op with
+      | `Join _ ->
+          F.pp_print_string fmt " JOIN"
+      | `Widen (num_iters, _) ->
+          F.fprintf fmt " WIDEN(num_iters= %d)" num_iters
+    in
+    let underlying_node = Node.underlying_node node in
+    NodePrinter.start_session ~pp_name underlying_node ;
+    let left, right, result = match op with `Join lrr | `Widen (_, lrr) -> lrr in
+    L.d_strln
+      (Format.asprintf "LEFT: %a@.RIGHT: %a@.RESULT: %a@." Domain.pp left Domain.pp right Domain.pp
+         result) ;
+    NodePrinter.finish_session underlying_node
+
+
   let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
     let node_id = Node.id node in
     let update_inv_map pre ~visit_count =
@@ -89,8 +108,13 @@ struct
     if InvariantMap.mem node_id inv_map then (
       let old_state = InvariantMap.find node_id inv_map in
       let widened_pre =
-        if CFG.is_loop_head pdesc node then
-          Domain.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count
+        if CFG.is_loop_head pdesc node then (
+          let num_iters = old_state.visit_count in
+          let prev = old_state.pre in
+          let next = astate_pre in
+          let res = Domain.widen ~prev ~next ~num_iters in
+          if debug then debug_absint_operation (`Widen (num_iters, (prev, next, res))) node ;
+          res )
         else astate_pre
       in
       if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue)
@@ -118,7 +142,9 @@ struct
             | None ->
                 some_post
             | Some joined_post ->
-                Some (Domain.join joined_post post) )
+                let res = Domain.join joined_post post in
+                if debug then debug_absint_operation (`Join (joined_post, post, res)) node ;
+                Some res )
     in
     match Scheduler.pop work_queue with
     | Some (_, [], work_queue') ->