biabduction/dune

Summary: phew

Reviewed By: mityal

Differential Revision: D21261643

fbshipit-source-id: 9be463b08

infer/src/biabduction/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 biabduction)
+ (public_name infer.biabduction)
+ (flags
+  (:standard -open Core -open InferIR -open InferStdlib -open IStd -open InferGenerated
+    -open InferBase -open Absint))
+ (libraries core InferStdlib InferGenerated InferBase InferIR absint)
+ (preprocess (pps ppx_compare))
+)

infer/src/biabduction/interproc.ml

@@ -1113,11 +1113,10 @@ let analyze_procedure_aux ({InterproceduralAnalysis.proc_desc; _} as analysis_da
   summary_compact
 
 
-let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv; err_log} as analysis_data) :
+let analyze_procedure ({InterproceduralAnalysis.proc_desc; err_log} as analysis_data) :
     BiabductionSummary.t option =
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
-  if Topl.is_active () then Topl.instrument tenv proc_desc ;
   try Some (analyze_procedure_aux analysis_data)
   with exn ->
     IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;

infer/src/checkers/registerCheckers.ml

@@ -177,9 +177,12 @@ let all_checkers =
   ; { name= "biabduction"
     ; active= Config.is_checker_enabled Biabduction
     ; callbacks=
-        [ (dynamic_dispatch Payloads.Fields.biabduction Interproc.analyze_procedure, Language.Clang)
-        ; (dynamic_dispatch Payloads.Fields.biabduction Interproc.analyze_procedure, Language.Java)
-        ] }
+        [ ( dynamic_dispatch Payloads.Fields.biabduction
+              (Topl.instrument_callback Interproc.analyze_procedure)
+          , Language.Clang )
+        ; ( dynamic_dispatch Payloads.Fields.biabduction
+              (Topl.instrument_callback Interproc.analyze_procedure)
+          , Language.Java ) ] }
   ; { name= "annotation reachability"
     ; active= Config.is_checker_enabled AnnotationReachability
     ; callbacks=

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 ./absint ./atd ./base ./c_stubs ./istd ./scripts
-INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I c_stubs -I istd -I scripts
+LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./biabduction ./c_stubs ./istd ./scripts
+INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I biabduction -I c_stubs -I istd -I scripts
 
 ml_src_files:=$(shell \
 	cd $(INFER_BUILD_DIR); \

infer/src/dune.in

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

infer/src/topl/Topl.ml

@@ -294,3 +294,8 @@ let sourcefile () =
 let cfg () =
   if not (is_active ()) then L.die InternalError "Called Topl.cfg when Topl is inactive" ;
   ToplMonitor.cfg ()
+
+
+let instrument_callback biabduction ({InterproceduralAnalysis.proc_desc; tenv; _} as callback) =
+  if is_active () then instrument tenv proc_desc ;
+  biabduction callback

infer/src/topl/Topl.mli

@@ -16,10 +16,6 @@ val get_proc_attr : Procname.t -> ProcAttributes.t option
 val get_proc_desc : Procname.t -> Procdesc.t option
 (** Returns a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *)
 
-val instrument : Tenv.t -> Procdesc.t -> unit
-(** Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility to
-    instrument procedures at most once. *)
-
 val add_errors : Exe_env.t -> Summary.t -> unit
 (** Adds error using {!Reporting}. *)
 
@@ -30,3 +26,10 @@ val sourcefile : unit -> SourceFile.t
 val cfg : unit -> Cfg.t
 (** The CFG of the synthesized code. This function has a side-effect, because that's how [Cfg]
     works, so do NOT call when Topl is inactive.*)
+
+val instrument_callback :
+     (BiabductionSummary.t InterproceduralAnalysis.t -> BiabductionSummary.t option)
+  -> BiabductionSummary.t InterproceduralAnalysis.t
+  -> BiabductionSummary.t option
+(** Run biabduction with Topl instrumentation if active. Inserts calls to the TOPL automaton.
+    Mutates the arguments: it is the caller's responsibility to instrument procedures at most once. *)