From 0f95d16ac17bb8af4d798978f3175d0cc12a5db9 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 7 May 2020 08:49:34 -0700 Subject: [PATCH] labs/dune Summary: Last checker for good. Updated the README of the lab to reflect changes. Delete now-defunct SummaryPayload: all checkers now behave in a functional manner as far as summary payloads are concerned. Reviewed By: ngorogiannis Differential Revision: D21426550 fbshipit-source-id: 2b52b9f5b --- infer/src/backend/SummaryPayload.ml | 59 --------------------------- infer/src/backend/SummaryPayload.mli | 35 ---------------- infer/src/backend/registerCheckers.ml | 2 +- infer/src/deadcode/Makefile | 4 +- infer/src/dune.in | 6 ++- infer/src/labs/README.md | 8 ++-- infer/src/labs/ResourceLeaks.ml | 35 +++++----------- infer/src/labs/ResourceLeaks.mli | 2 +- infer/src/labs/dune | 14 +++++++ 9 files changed, 36 insertions(+), 129 deletions(-) delete mode 100644 infer/src/backend/SummaryPayload.ml delete mode 100644 infer/src/backend/SummaryPayload.mli create mode 100644 infer/src/labs/dune diff --git a/infer/src/backend/SummaryPayload.ml b/infer/src/backend/SummaryPayload.ml deleted file mode 100644 index cd48d958d..000000000 --- a/infer/src/backend/SummaryPayload.ml +++ /dev/null @@ -1,59 +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 - -module type Payload = sig - type t - - val field : (Payloads.t, t option) Field.t -end - -module type S = sig - type t - - val update_summary : t -> Summary.t -> Summary.t - - val of_summary : Summary.t -> t option - - val read_full : caller_summary:Summary.t -> callee_pname:Procname.t -> (Procdesc.t * t) option - - val read : caller_summary:Summary.t -> callee_pname:Procname.t -> t option - - val read_toplevel_procedure : Procname.t -> t option -end - -module Make (P : Payload) : S with type t = P.t = struct - type t = P.t - - let update_payloads = Field.fset P.field - - let of_payloads = Field.get P.field - - let update_summary p (summary : Summary.t) = - {summary with payloads= update_payloads summary.payloads (Some p)} - - - let of_summary (summary : Summary.t) = of_payloads summary.payloads - - let get_payload analysis_result = - let open Option.Monad_infix in - analysis_result - >>= fun summary -> of_summary summary >>| fun payload -> (Summary.get_proc_desc summary, payload) - - - let read_full ~caller_summary ~callee_pname = - Ondemand.analyze_proc_name ~caller_summary callee_pname |> get_payload - - - let read ~caller_summary ~callee_pname = - Ondemand.analyze_proc_name ~caller_summary callee_pname |> get_payload |> Option.map ~f:snd - - - let read_toplevel_procedure callee_pname = - Ondemand.analyze_proc_name_no_caller callee_pname |> get_payload |> Option.map ~f:snd -end diff --git a/infer/src/backend/SummaryPayload.mli b/infer/src/backend/SummaryPayload.mli deleted file mode 100644 index 6b042ab3e..000000000 --- a/infer/src/backend/SummaryPayload.mli +++ /dev/null @@ -1,35 +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 - -module type Payload = sig - type t - - val field : (Payloads.t, t option) Field.t -end - -module type S = sig - type t - - val update_summary : t -> Summary.t -> Summary.t - (** Update the corresponding part of the payload in the procedure summary *) - - val of_summary : Summary.t -> t option - (** Read the corresponding part of the payload from the procedure summary *) - - val read_full : caller_summary:Summary.t -> callee_pname:Procname.t -> (Procdesc.t * t) option - (** Return the proc desc and payload for the given procedure. Runs the analysis on-demand if - necessary. *) - - val read : caller_summary:Summary.t -> callee_pname:Procname.t -> t option - (** Return the payload for the given procedure. Runs the analysis on-demand if necessary. *) - - val read_toplevel_procedure : Procname.t -> t option -end - -module Make (P : Payload) : S with type t = P.t diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index 87da5ace0..1a54e636a 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -144,7 +144,7 @@ let all_checkers = ; callbacks= [ ( (* the checked-in version is intraprocedural, but the lab asks to make it interprocedural later on *) - Procedure ResourceLeaks.checker + interprocedural Payloads.Fields.lab_resource_leaks ResourceLeaks.checker , Language.Java ) ] } ; { name= "RacerD" ; active= Config.is_checker_enabled RacerD diff --git a/infer/src/deadcode/Makefile b/infer/src/deadcode/Makefile index dc4021c1b..2bafef399 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 ./concurrency ./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 concurrency -I cost -I istd -I nullsafe -I pulse -I quandary -I scripts -I topl +LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./biabduction ./bufferoverrun ./c_stubs ./checkers ./concurrency ./cost ./istd ./labs ./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 concurrency -I cost -I istd -I labs -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 ad3077167..005cdccca 100644 --- a/infer/src/dune.in +++ b/infer/src/dune.in @@ -14,7 +14,6 @@ let source_dirs = @ [ (if java then "java" else "java_stubs") ; "backend" ; "integration" - ; "labs" ; "test_determinator" ; "unit" ; "unit" ^/ "nullsafe" ] @@ -65,6 +64,8 @@ let infer_cflags = ; "-open" ; "Concurrency" ; "-open" + ; "Labs" + ; "-open" ; "Absint" ; "-open" ; "OpenSource" @@ -109,7 +110,8 @@ let main_lib_stanza = ; "costlib" ; "quandary" ; "TOPL" - ; "concurrency" ] )) + ; "concurrency" + ; "labs" ] )) (String.concat " " infer_binaries) diff --git a/infer/src/labs/README.md b/infer/src/labs/README.md index 1d624bb26..066496d92 100644 --- a/infer/src/labs/README.md +++ b/infer/src/labs/README.md @@ -84,7 +84,7 @@ Finally, look again at the HTML debug output of infer on [Leaks.java](https://gi ```OCaml let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in let message = F.asprintf "Leaked %a resource(s)" ResourceLeakDomain.pp post in - Reporting.log_error summary ~loc:last_loc IssueType.resource_leak message + Reporting.log_error proc_desc err_log ~loc:last_loc IssueType.resource_leak message ``` (d) Think about the concretization of the resource count. What does a resource count of zero mean? Is there a concrete state in the concretization of "Resource count zero" that leaks a resource? Write a simple test method `FN_leakBad` in [Leaks.java](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/lab/Leaks.java) that will produce this concrete state (that is, a false negative test where the program leaks a resource, but the analyzer doesn't catch it). @@ -116,11 +116,11 @@ include AbstractDomain.TopLifter (FiniteBounds) ## (4) Interprocedural analysis -Augment the summary type with state to indicate whether the current procedure returns a resource. Allowing a resource to escape to the caller should not be considered a leak. Use this information in callers too by reading from the callee's summary: +Augment the summary type with state to indicate whether the current procedure returns a resource. Allowing a resource to escape to the caller should not be considered a leak. Use this information in callers too by reading from the callee's summary. Use the `analyze_dependency` field of the `InterproceduralAnalysis.t` record passed to the analysis like so: ```OCaml - match Payload.read pdesc callee_procname with - | Some summary -> + match analyze_dependency callee_procname with + | Some (callee_proc_desc, callee_summary) -> (* interprocedural analysis produced a summary: use it *) () | None -> diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 2fb3ae3f3..cd37f2e8f 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -9,18 +9,11 @@ open! IStd module F = Format module L = Logging -(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *) -module Payload = SummaryPayload.Make (struct - type t = ResourceLeakDomain.t - - let field = Payloads.Fields.lab_resource_leaks -end) - module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type analysis_data = unit ProcData.t + type analysis_data = ResourceLeakDomain.t InterproceduralAnalysis.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -52,7 +45,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) - let exec_instr (astate : ResourceLeakDomain.t) {ProcData.summary= _; tenv= _} _ + let exec_instr (astate : ResourceLeakDomain.t) + {InterproceduralAnalysis.proc_desc= _; tenv= _; analyze_dependency= _; _} _ (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct _callee_procname, _actuals, _, _loc) -> @@ -82,19 +76,10 @@ module CFG = ProcCfg.Normal module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) (** Report an error when we have acquired more resources than we have released *) -let report_if_leak _post _summary (_proc_data : unit ProcData.t) = () - -(* Callback for invoking the checker from the outside--registered in RegisterCheckers *) -let checker {Callbacks.summary; exe_env} : Summary.t = - let proc_name = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env proc_name in - let proc_data = {ProcData.summary; tenv; extras= ()} in - match - Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial - (Summary.get_proc_desc summary) - with - | Some post -> - report_if_leak post summary proc_data ; - Payload.update_summary post summary - | None -> - L.(die InternalError) "Analyzer failed to compute post for %a" Procname.pp proc_name +let report_if_leak {InterproceduralAnalysis.proc_desc= _; err_log= _; _} _post = () + +(** Main function into the checker--registered in RegisterCheckers *) +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in + Option.iter result ~f:(fun post -> report_if_leak analysis_data post) ; + result diff --git a/infer/src/labs/ResourceLeaks.mli b/infer/src/labs/ResourceLeaks.mli index 489676eb8..f1f7daeaf 100644 --- a/infer/src/labs/ResourceLeaks.mli +++ b/infer/src/labs/ResourceLeaks.mli @@ -7,4 +7,4 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : ResourceLeakDomain.t InterproceduralAnalysis.t -> ResourceLeakDomain.t option diff --git a/infer/src/labs/dune b/infer/src/labs/dune new file mode 100644 index 000000000..c398fa9fb --- /dev/null +++ b/infer/src/labs/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 labs) + (public_name infer.labs) + (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)) +)