From bcb5b8356f2e7fca2dc8b15240b7bc26763a1a35 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 7 May 2020 08:48:52 -0700 Subject: [PATCH] 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 | 3 --- infer/src/backend/SummaryReporting.ml | 20 -------------------- infer/src/backend/SummaryReporting.mli | 18 ------------------ infer/src/backend/ondemand.ml | 7 +++---- infer/src/deadcode/Makefile | 4 ++-- infer/src/dune.in | 12 +++++------- infer/src/topl/Topl.ml | 15 ++++++++------- infer/src/topl/Topl.mli | 3 --- infer/src/topl/dune | 18 ++++++++++++++++++ 9 files changed, 36 insertions(+), 64 deletions(-) delete mode 100644 infer/src/backend/SummaryReporting.ml delete mode 100644 infer/src/backend/SummaryReporting.mli create mode 100644 infer/src/topl/dune diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index f8de022dc..6e8e28fac 100644 --- a/infer/src/backend/Summary.mli +++ b/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 diff --git a/infer/src/backend/SummaryReporting.ml b/infer/src/backend/SummaryReporting.ml deleted file mode 100644 index b099d56da..000000000 --- a/infer/src/backend/SummaryReporting.ml +++ /dev/null @@ -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 diff --git a/infer/src/backend/SummaryReporting.mli b/infer/src/backend/SummaryReporting.mli deleted file mode 100644 index 7704e045d..000000000 --- a/infer/src/backend/SummaryReporting.mli +++ /dev/null @@ -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). *) diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 6c7858a24..c9ffff6f4 100644 --- a/infer/src/backend/ondemand.ml +++ b/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 - if Topl.is_active () then Topl.add_errors exe_env summary ; - summary + Callbacks.iterate_procedure_callbacks exe_env callee_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 = diff --git a/infer/src/deadcode/Makefile b/infer/src/deadcode/Makefile index cb98db47e..29577f98b 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 ./absint ./atd ./base ./biabduction ./bufferoverrun ./c_stubs ./checkers ./cost ./istd ./nullsafe ./pulse ./quandary ./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 +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 -I topl ml_src_files:=$(shell \ cd $(INFER_BUILD_DIR); \ diff --git a/infer/src/dune.in b/infer/src/dune.in index 60feccf00..d788f264d 100644 --- a/infer/src/dune.in +++ b/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 ;; diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index ea2a146a4..637c53f20 100644 --- a/infer/src/topl/Topl.ml +++ b/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 proc_desc = summary.Summary.proc_desc in +let add_errors env proc_desc err_log biabduction_summary = 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 diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli index ac2d1b585..341c13590 100644 --- a/infer/src/topl/Topl.mli +++ b/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. *) diff --git a/infer/src/topl/dune b/infer/src/topl/dune new file mode 100644 index 000000000..c4c0670c3 --- /dev/null +++ b/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)) +)