pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

labs/dune

Browse Source 
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
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent efd8e767cb
commit 0f95d16ac1
9 changed files with 36 additions and 129 deletions
Show Stats Download Patch File Download Diff File

59
infer/src/backend/SummaryPayload.ml
Unescape View File

@ -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

35
infer/src/backend/SummaryPayload.mli
Unescape View File

@ -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

2
infer/src/backend/registerCheckers.ml
Unescape View File

@ -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

4
infer/src/deadcode/Makefile
Unescape View File

@ -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); \

6
infer/src/dune.in
Unescape View File

@ -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)

8
infer/src/labs/README.md
Unescape View File

@ -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 ->

35
infer/src/labs/ResourceLeaks.ml
Unescape View File

@ -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

2
infer/src/labs/ResourceLeaks.mli
Unescape View File

@ -7,4 +7,4 @@
open! IStd
val checker : Callbacks.proc_callback_t
val checker : ResourceLeakDomain.t InterproceduralAnalysis.t -> ResourceLeakDomain.t option

14
infer/src/labs/dune
Unescape View File

@ -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))
)
Write Preview
Loading…
Cancel
Save