From 0d4b57a6257d70bbdef8ed1c7afd0d275dd1310c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 02:59:18 -0700 Subject: [PATCH] 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 | 6 ++-- infer/src/absint/AnalysisCallbacks.ml | 29 +++++++++++++++++++ infer/src/absint/AnalysisCallbacks.mli | 31 +++++++++++++++++++++ infer/src/absint/dune | 14 ++++++++++ infer/src/{absint => checkers}/LowerHil.ml | 0 infer/src/{absint => checkers}/LowerHil.mli | 0 infer/src/checkers/registerCheckers.ml | 2 ++ infer/src/deadcode/Makefile | 4 +-- infer/src/deadcode/dune.in | 2 +- infer/src/dune.in | 5 ++-- infer/src/unit/analyzerTester.ml | 1 + 11 files changed, 86 insertions(+), 8 deletions(-) create mode 100644 infer/src/absint/AnalysisCallbacks.ml create mode 100644 infer/src/absint/AnalysisCallbacks.mli create mode 100644 infer/src/absint/dune rename infer/src/{absint => checkers}/LowerHil.ml (100%) rename infer/src/{absint => checkers}/LowerHil.mli (100%) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 6b4b1df63..8b733d1bd 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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 ; diff --git a/infer/src/absint/AnalysisCallbacks.ml b/infer/src/absint/AnalysisCallbacks.ml new file mode 100644 index 000000000..dd6a31ba8 --- /dev/null +++ b/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 diff --git a/infer/src/absint/AnalysisCallbacks.mli b/infer/src/absint/AnalysisCallbacks.mli new file mode 100644 index 000000000..f80c72b3e --- /dev/null +++ b/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 *) diff --git a/infer/src/absint/dune b/infer/src/absint/dune new file mode 100644 index 000000000..cb81fae1e --- /dev/null +++ b/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)) +) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/checkers/LowerHil.ml similarity index 100% rename from infer/src/absint/LowerHil.ml rename to infer/src/checkers/LowerHil.ml diff --git a/infer/src/absint/LowerHil.mli b/infer/src/checkers/LowerHil.mli similarity index 100% rename from infer/src/absint/LowerHil.mli rename to infer/src/checkers/LowerHil.mli diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 385d5f83f..dc34919c8 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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 diff --git a/infer/src/deadcode/Makefile b/infer/src/deadcode/Makefile index b3f03e36e..91eecedfb 100644 --- a/infer/src/deadcode/Makefile +++ b/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 -INCLUDE_FOLDERS = -I IR -I atd -I base -I c_stubs -I istd -I scripts +LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./c_stubs ./istd ./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); \ diff --git a/infer/src/deadcode/dune.in b/infer/src/deadcode/dune.in index 21a665010..b58ee2c87 100644 --- a/infer/src/deadcode/dune.in +++ b/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 diff --git a/infer/src/dune.in b/infer/src/dune.in index e60af4a80..b949ff894 100644 --- a/infer/src/dune.in +++ b/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) diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 110546aff..fd444f423 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/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) ->