topl/dune

Summary:
Also ondemand doesn't need to call Topl itself after an analysis.

Inline last call site of SummaryReporting (ondemand.ml) and delete the
file.

Reviewed By: ngorogiannis

Differential Revision: D21424386

fbshipit-source-id: 064f4e261

infer/src/backend/Summary.mli

@@ -48,9 +48,6 @@ val get_proc_name : t -> Procname.t
 
 val get_proc_desc : t -> Procdesc.t
 
-val get_attributes : t -> ProcAttributes.t
-(** Get the attributes of the procedure. *)
-
 val get_err_log : t -> Errlog.t
 
 val get_loc : t -> Location.t

infer/src/backend/SummaryReporting.ml

@@ -1,20 +0,0 @@
-(*
- * 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
-
-type log_t = Reporting.log_t
-
-let log_error summary ~loc ?ltr ?extras issue_type error_message =
-  let attrs = Summary.get_attributes summary in
-  let err_log = Summary.get_err_log summary in
-  Reporting.log_error attrs err_log ~loc ?ltr ?extras issue_type error_message
-
-
-let log_error_using_state summary exn =
-  BiabductionReporting.log_error_using_state (Summary.get_proc_desc summary)
-    (Summary.get_err_log summary) exn

infer/src/backend/SummaryReporting.mli

@@ -1,18 +0,0 @@
-(*
- * 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
-
-(** convencience functions on top of {!Reporting} *)
-
-type log_t = Reporting.log_t
-
-val log_error : Summary.t -> loc:Location.t -> log_t
-(** Add an error to the given summary. *)
-
-val log_error_using_state : Summary.t -> exn -> unit
-(** Add an error to the given summary using biabduction state (DO NOT USE ELSEWHERE). *)

infer/src/backend/ondemand.ml

@@ -157,9 +157,7 @@ let analyze callee_summary =
   in
   current_taskbar_status := Some (t0, status) ;
   !ProcessPoolState.update_status t0 status ;
-  let summary = Callbacks.iterate_procedure_callbacks exe_env callee_summary in
+  Callbacks.iterate_procedure_callbacks exe_env callee_summary
-  if Topl.is_active () then Topl.add_errors exe_env summary ;
-  summary
 
 
 let run_proc_analysis ~caller_pdesc callee_pdesc =
@@ -192,7 +190,8 @@ let run_proc_analysis ~caller_pdesc callee_pdesc =
     summary
   in
   let log_error_and_continue exn (summary : Summary.t) kind =
-    SummaryReporting.log_error_using_state summary exn ;
+    BiabductionReporting.log_error_using_state (Summary.get_proc_desc summary)
+      (Summary.get_err_log summary) exn ;
     let stats = Summary.Stats.update summary.stats ~failure_kind:kind in
     let payloads =
       let biabduction =

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

infer/src/dune.in

@@ -17,7 +17,6 @@ let source_dirs =
     ; "integration"
     ; "labs"
     ; "test_determinator"
-    ; "topl"
     ; "unit"
     ; "unit" ^/ "nullsafe" ]
 
@@ -63,6 +62,8 @@ let infer_cflags =
   ; "-open"
   ; "Quandary"
   ; "-open"
+  ; "TOPL"
+  ; "-open"
   ; "Absint"
   ; "-open"
   ; "OpenSource"
@@ -105,7 +106,8 @@ let main_lib_stanza =
          ; "pulselib"
          ; "checkers"
          ; "costlib"
-         ; "quandary" ] ))
+         ; "quandary"
+         ; "TOPL" ] ))
     (String.concat " " infer_binaries)
 
 
@@ -144,10 +146,6 @@ let infertop_stanza =
     infer_cflags
 
 
-let topl_stanzas =
-  ["(ocamllex ToplLexer)"; "(menhir (flags --unused-token INDENT --explain) (modules ToplParser))"]
-
-
 let java_sources_lexer = if java then ["(ocamllex jSourceFileInfo)"] else []
 
 let flatten_sources_stanzas =
@@ -164,7 +162,7 @@ let flatten_sources_stanzas =
 (** The build stanzas to be passed to dune *)
 let stanzas =
   (env_stanza :: main_lib_stanza :: infer_exe_stanza :: infertop_stanza :: clang_lexer_stanzas)
-  @ java_sources_lexer @ topl_stanzas @ flatten_sources_stanzas
+  @ java_sources_lexer @ flatten_sources_stanzas
 
 
 ;;

infer/src/topl/Topl.ml

@@ -227,13 +227,10 @@ let conjoin_props env post pre =
     To compute (pre & post) the function [conjoin_props] from above is used, which returns a weaker
     formula: in particular, the spatial part of pre is dropped. To get around some limitations of
     the prover we also use [lookup_static_var]; if a call to this function fails, we don't warn. *)
-let add_errors exe_env summary =
+let add_errors env proc_desc err_log biabduction_summary =
-  let proc_desc = summary.Summary.proc_desc in
   let proc_name = Procdesc.get_proc_name proc_desc in
   if not (ToplUtils.is_synthesized proc_name) then
-    let env = Exe_env.get_tenv exe_env proc_name in
     let preposts : Prop.normal BiabductionSummary.spec list =
-      let biabduction_summary = summary.Summary.payloads.Payloads.biabduction in
       let check_phase x =
         if not BiabductionSummary.(equal_phase x.phase RE_EXECUTION) then
           L.die InternalError "Topl.add_errors should only be called after RE_EXECUTION"
@@ -269,7 +266,8 @@ let add_errors exe_env summary =
               let property, _vname = ToplAutomaton.vname (Lazy.force automaton) error in
               let message = Printf.sprintf "property %s reaches error" property in
               tt "WARN@\n" ;
-              SummaryReporting.log_error summary IssueType.topl_error ~loc message )
+              let attrs = Procdesc.get_attributes proc_desc in
+              Reporting.log_error attrs err_log IssueType.topl_error ~loc message )
           in
           (* Don't warn if [lookup_static_var] fails. *)
           Option.iter ~f:handle_state_post_value (lookup_static_var env state_var post)
@@ -296,6 +294,9 @@ let cfg () =
   ToplMonitor.cfg ()
 
 
-let instrument_callback biabduction ({InterproceduralAnalysis.proc_desc; tenv; _} as callback) =
+let instrument_callback biabduction
+    ({InterproceduralAnalysis.proc_desc; tenv; err_log} as analysis_data) =
   if is_active () then instrument tenv proc_desc ;
-  biabduction callback
+  let biabduction_summary = biabduction analysis_data in
+  if is_active () then add_errors tenv proc_desc err_log biabduction_summary ;
+  biabduction_summary

infer/src/topl/Topl.mli

@@ -16,9 +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 add_errors : Exe_env.t -> Summary.t -> unit
-(** Adds error using {!Reporting}. *)
-
 val sourcefile : unit -> SourceFile.t
 (** The (fake) sourcefile in which synthesized code resides. This function has a side-effect,
     because that's how [SourceFile] works, so do NOT call when Topl is inactive. *)

infer/src/topl/dune

@@ -0,0 +1,18 @@
+; 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.
+
+(ocamllex ToplLexer)
+
+(menhir (flags --unused-token INDENT --explain) (modules ToplParser))
+
+(library
+ (name TOPL)
+ (public_name infer.TOPL)
+ (flags
+  (:standard -open Core -open InferIR -open InferStdlib -open IStd -open InferGenerated
+    -open InferBase -open Absint -open Biabduction))
+ (libraries core InferStdlib InferGenerated InferBase InferIR absint biabduction)
+ (preprocess (pps ppx_compare ppx_hash ppx_sexp_conv))
+)