absint/dune

Summary:
absint/ is its own dune library. There was one last obstacle: we need
callbacks to `NodePrinter`. We'll add more to `AnalysisCallbacks` in future
diffs.

Reviewed By: ngorogiannis

Differential Revision: D21257476

fbshipit-source-id: 3a2ddef14

infer/src/absint/AbstractInterpreter.ml

@@ -369,7 +369,7 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s
 
   (* shadowed for HTML debug *)
   let exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map =
-    NodePrinter.with_session (Node.underlying_node node)
+    AnalysisCallbacks.html_debug_new_node_session (Node.underlying_node node)
       ~kind:(if is_narrowing then `ExecNodeNarrowing else `ExecNode)
       ~pp_name:(TransferFunctions.pp_session_name node)
       ~f:(fun () ->
@@ -394,7 +394,7 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s
 
   (* shadowed for HTML debug *)
   let compute_pre cfg node inv_map =
-    NodePrinter.with_session (Node.underlying_node node) ~kind:`ComputePre
+    AnalysisCallbacks.html_debug_new_node_session (Node.underlying_node node) ~kind:`ComputePre
       ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map
     )
 
@@ -470,7 +470,7 @@ module MakeWTONode (TransferFunctions : NodeTransferFunctions) = struct
 
   let debug_wto wto node =
     let underlying_node = Node.underlying_node node in
-    NodePrinter.with_session underlying_node ~kind:`WTO
+    AnalysisCallbacks.html_debug_new_node_session underlying_node ~kind:`WTO
       ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () ->
         let pp_node fmt node = node |> Node.id |> Node.pp_id fmt in
         L.d_printfln "%a" (WeakTopologicalOrder.Partition.pp ~pp_node) wto ;

infer/src/absint/AnalysisCallbacks.ml

@@ -0,0 +1,29 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module L = Logging
+
+type callbacks =
+  { html_debug_new_node_session_f:
+      'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
+      -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a }
+
+let callbacks_ref : callbacks option ref = ref None
+
+let set_callbacks callbacks = callbacks_ref := Some callbacks
+
+let get_callbacks () =
+  match !callbacks_ref with
+  | Some callbacks ->
+      callbacks
+  | None ->
+      L.die InternalError "Callbacks not set"
+
+
+let html_debug_new_node_session ?kind ~pp_name node ~f =
+  (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f

infer/src/absint/AnalysisCallbacks.mli

@@ -0,0 +1,31 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** {2 Analysis API} *)
+
+val html_debug_new_node_session :
+     ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
+  -> pp_name:(Format.formatter -> unit)
+  -> Procdesc.Node.t
+  -> f:(unit -> 'a)
+  -> 'a
+(** set to {!NodePrinter.with_session} *)
+
+(** {2 Callbacks management}*)
+
+(** These callbacks are used to break the dependency cycles between some modules. Specifically, we
+    put here functions needed for the analysis that depend on modules higher up the dependency graph
+    than this library but whose type does not. *)
+type callbacks =
+  { html_debug_new_node_session_f:
+      'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
+      -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a }
+
+val set_callbacks : callbacks -> unit
+(** make sure this is called before starting any actual analysis *)

infer/src/absint/dune

@@ -0,0 +1,14 @@
+; Copyright (c) Facebook, Inc. and its affiliates.
+;
+; This source code is licensed under the MIT license found in the
+; LICENSE file in the root directory of this source tree.
+
+(library
+ (name absint)
+ (public_name infer.absint)
+ (flags
+  (:standard -open Core -open InferIR -open InferStdlib -open IStd -open InferGenerated
+    -open InferBase))
+ (libraries core InferStdlib InferGenerated InferBase InferIR)
+ (preprocess (pps ppx_compare))
+)

infer/src/checkers/registerCheckers.ml

@@ -18,6 +18,8 @@ let () =
     ()
 
 
+let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session}
+
 type callback_fun =
   | Procedure of Callbacks.proc_callback_t
   | DynamicDispatch of Callbacks.proc_callback_t

infer/src/deadcode/Makefile

@@ -50,8 +50,8 @@ endif
 # Note that we run find under _build directory. Since we copy some
 # sources from subfolders to src/ folder to avoid duplicates we use
 # $(DEPTH_ONE) and iteration over main and library folders.
-LIBRARY_FOLDERS = . ./IR ./atd ./base ./c_stubs ./istd ./scripts
+LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./c_stubs ./istd ./scripts
-INCLUDE_FOLDERS = -I IR -I atd -I base -I c_stubs -I istd -I scripts
+INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I c_stubs -I istd -I scripts
 
 ml_src_files:=$(shell \
 	cd $(INFER_BUILD_DIR); \

infer/src/deadcode/dune.in

@@ -19,5 +19,5 @@ Format.sprintf
  (preprocess (pps ppx_compare ppx_enumerate ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
 )
 |}
-  (String.concat " " ("InferCStubs" :: common_libraries))
+  (String.concat " " ("absint" :: "InferIR" :: "InferCStubs" :: common_libraries))
 |> Jbuild_plugin.V1.send

infer/src/dune.in

@@ -12,7 +12,6 @@ let ( ^/ ) = Filename.concat
 let source_dirs =
   (if clang then ["al"; "clang"; "unit" ^/ "clang"] else ["clang_stubs"; "unit" ^/ "clang_stubs"])
   @ [ (if java then "java" else "java_stubs")
-    ; "absint"
     ; "backend"
     ; "biabduction"
     ; "bufferoverrun"
@@ -57,6 +56,8 @@ let infer_cflags =
   [ "-open"
   ; "Core"
   ; "-open"
+  ; "Absint"
+  ; "-open"
   ; "OpenSource"
   ; "-open"
   ; "InferStdlib"
@@ -86,7 +87,7 @@ let main_lib_stanza =
 )
 |}
     infer_cflags
-    (String.concat " " ("InferCStubs" :: "InferIR" :: common_libraries))
+    (String.concat " " ("absint" :: "InferCStubs" :: "InferIR" :: common_libraries))
     (String.concat " " infer_binaries)
 
 

infer/src/unit/analyzerTester.ml

@@ -296,6 +296,7 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) =
   let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)]
 
   let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests =
+    AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} ;
     let open OUnit2 in
     List.concat_map
       ~f:(fun (name, test_program) ->