Reviewed By: jeremydubreil Differential Revision: D5118057 fbshipit-source-id: a11ea08master
Sam Blackshear
8 years ago
committed by
Facebook Github Bot
parent
c8cad5b0f1
commit
927b08346e
@ -0,0 +1,35 @@
|
||||
(*
|
||||
* Copyright (c) 2017 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
module F = Format
|
||||
module L = Logging
|
||||
|
||||
(* Extremely simple abstraction of resources: count the number of acquired resources. If there's
|
||||
not a corresponding number of releases, there may be a leak. *)
|
||||
type astate = int (* 3(a) *)
|
||||
|
||||
(* For now, type of abstract state and summary are the same *)
|
||||
type summary = astate (* 4(a) *)
|
||||
|
||||
let (<=) ~lhs ~rhs =
|
||||
lhs <= rhs
|
||||
|
||||
let join =
|
||||
Pervasives.max
|
||||
|
||||
let widen ~prev ~next ~num_iters:_ =
|
||||
join prev next
|
||||
|
||||
let pp fmt astate =
|
||||
F.fprintf fmt "Resource count: %d" astate
|
||||
|
||||
(* At the beginning of a procedure, assume no resources are held *)
|
||||
let initial = 0
|
||||
@ -0,0 +1,126 @@
|
||||
(*
|
||||
* Copyright (c) 2017 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
module F = Format
|
||||
module L = Logging
|
||||
|
||||
module Domain = ResourceLeakDomain
|
||||
|
||||
(* Boilerplate to write/read our summaries alongside the summaries of other analyzers *)
|
||||
module Summary = Summary.Make(struct
|
||||
type payload = Domain.astate
|
||||
|
||||
let update_payload resources_payload (summary : Specs.summary) =
|
||||
{ summary with payload = { summary.payload with resources = Some resources_payload }}
|
||||
|
||||
let read_payload (summary : Specs.summary) =
|
||||
summary.payload.resources
|
||||
end)
|
||||
|
||||
type extras = FormalMap.t
|
||||
|
||||
module TransferFunctions (CFG : ProcCfg.S) = struct
|
||||
module CFG = CFG
|
||||
module Domain = Domain
|
||||
type nonrec extras = extras
|
||||
|
||||
(* Take an abstract state and instruction, produce a new abstract state *)
|
||||
let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; } _ (instr : HilInstr.t) =
|
||||
let is_closeable procname tenv = match procname with
|
||||
| Typ.Procname.Java java_procname ->
|
||||
let is_closable_interface typename _ = match Typ.Name.name typename with
|
||||
| "java.io.AutoCloseable" | "java.io.Closeable" -> true
|
||||
| _ -> false in
|
||||
PatternMatch.supertype_exists
|
||||
tenv
|
||||
is_closable_interface
|
||||
(Typ.Name.Java.from_string (Typ.Procname.java_get_class_name java_procname))
|
||||
| _ ->
|
||||
false in
|
||||
(* We assume all constructors of a subclass of Closeable acquire a resource *)
|
||||
let acquires_resource procname tenv =
|
||||
Typ.Procname.is_constructor procname && is_closeable procname tenv in
|
||||
(* We assume the close method of a Closeable releases all of its resources *)
|
||||
let releases_resource procname tenv = match Typ.Procname.get_method procname with
|
||||
| "close" -> is_closeable procname tenv
|
||||
| _ -> false in
|
||||
match instr with
|
||||
| Call (_return_opt, Direct callee_procname, _actuals, _, _loc) ->
|
||||
(* function call [return_opt] := invoke [callee_procname]([actuals]) *)
|
||||
(* (1)(b) *)
|
||||
let astate' =
|
||||
if acquires_resource callee_procname tenv
|
||||
then astate + 1 (* 3(a) *)
|
||||
else if releases_resource callee_procname tenv
|
||||
then astate - 1 (* 3(a) *)
|
||||
else astate in
|
||||
begin
|
||||
match Summary.read_summary pdesc callee_procname with
|
||||
| Some _summary ->
|
||||
(* Looked up the summary for callee_procname... do something with it *)
|
||||
(* 4(a) *)
|
||||
(* 5(b) *)
|
||||
astate'
|
||||
| None ->
|
||||
(* No summary for callee_procname; it's native code or missing for some reason *)
|
||||
astate'
|
||||
end
|
||||
| Assign (_lhs_access_path, _rhs_exp, _loc) ->
|
||||
(* an assigment [lhs_access_path] := [rhs_exp] *)
|
||||
astate
|
||||
| Assume (_assume_exp, _, _, _loc) ->
|
||||
(* a conditional assume([assume_exp]). blocks if [assume_exp] evaluates to false *)
|
||||
astate
|
||||
| Call (_, Indirect _, _, _, _) ->
|
||||
(* This should never happen in Java. Fail if it does. *)
|
||||
failwithf "Unexpected indirect call %a" HilInstr.pp instr
|
||||
end
|
||||
|
||||
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
|
||||
module Analyzer =
|
||||
AbstractInterpreter.Make
|
||||
(* Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
|
||||
ignore them *)
|
||||
(ProcCfg.Normal) (* 5(a) *)
|
||||
(LowerHil.Make(TransferFunctions))
|
||||
|
||||
(* Lift our intraprocedural abstract interpreter into an interprocedural one that computes
|
||||
summaries of the type we defined earlier *)
|
||||
module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
|
||||
|
||||
(* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
|
||||
let checker ({ Callbacks.summary; } as callback) : Specs.summary =
|
||||
(* Report an error when we have acquired more resources than we have released *)
|
||||
let report leak_count (proc_data : extras ProcData.t) =
|
||||
if leak_count > 0 (* 3(a) *)
|
||||
then
|
||||
let last_loc = Procdesc.Node.get_loc (Procdesc.get_exit_node proc_data.pdesc) in
|
||||
let issue_kind = Localise.to_issue_id Localise.resource_leak in
|
||||
let message = F.asprintf "Leaked %d resource(s)" leak_count in
|
||||
let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in
|
||||
Reporting.log_error_from_summary summary ~loc:last_loc exn in
|
||||
(* Convert the abstract state to a summary. for now, just the identity function *)
|
||||
let convert_to_summary (post : Domain.astate) : Domain.summary =
|
||||
(* 4(a) *)
|
||||
post in
|
||||
let compute_post (proc_data : extras ProcData.t) =
|
||||
let initial = ResourceLeakDomain.initial, IdAccessPathMapDomain.empty in
|
||||
match Analyzer.compute_post proc_data ~initial ~debug:false with
|
||||
| Some (post, _) ->
|
||||
(* 1(c) *)
|
||||
report post proc_data;
|
||||
Some (convert_to_summary post)
|
||||
| None ->
|
||||
failwithf
|
||||
"Analyzer failed to compute post for %a"
|
||||
Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) in
|
||||
|
||||
Interprocedural.compute_and_store_post ~compute_post ~make_extras:FormalMap.make callback
|
||||
@ -0,0 +1,130 @@
|
||||
(1) Warm up: running and debugging Infer
|
||||
This step assumes you have already downloaded Infer, compiled it successfully, and set up your OCaml dev environment.
|
||||
|
||||
(a) Run the analyzer on the tests: `cd infer/tests/codetoanalyze/java/checkers; make test`. The tests should pass.
|
||||
|
||||
(b) Add a new test method with a resource leak to `Leaks.java`, then run the tests again. The tests should now fail. As the failure message indicates, run `make replace` to update the expected output. The tests should now pass again.
|
||||
|
||||
(c) Run the analyzer on a single test file to produce the debug HTML: `infer --debug -a checkers --no-default-checkers --resource-leak -- javac Leaks.java`. Then, open the debug HTML: `open infer-out/captured/*.html`. This helpful artifact shows the Infer warnings alongside the code they are complaining about. It also displays the CFG node(s) associated with each line of code. Clicking a CFG node shows the Infer IR associated with the node, and the pre/post state computed while analyzing the instruction. Come back to the debug HTML early and often when you can't understand what your analysis is doing--it will help!
|
||||
|
||||
(c) The `Logging.d_str`/`Logging.d_strln` functions print to the debug HTML. The logging is contextual: it will print to the log for the CFG node that's being analyzed at the time the logging statement execute. Add a `Logging.d_strln` inside of the case for `Call`, recompile/re-run, and try to find the text you printed inside the appropriate CFG node log in the debug HTML.
|
||||
|
||||
(d) The `L.stdout`/`L.stderr` and functions print to the command line. This can be useful for printing information that doesn't happen in the context of a particular CFG node (e.g., performing post-processing on a summary). Add a `Logging.stderr` to the `compute_post` function, recompile/re-run and see your text printed on the command line.
|
||||
|
||||
(2) Reasoning about abstract domains
|
||||
|
||||
(a) Look at the `ResourceLeakDomain.ml`. There's a termination bug in the abstract domain--do you see it?.
|
||||
- Write a test method that makes the analyzer diverge.
|
||||
- Fix the domain to make your test pass and ensure that the analyzer will always terminate. Make sure your fix is sufficiently general (remember: the allocation count can be negative :)).
|
||||
|
||||
(b) 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` 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)?
|
||||
|
||||
(c) In addition, there are programs that do not leak resources that the analyzer will flag. Write a simple test method `FP_noleakOk` that exhibits this problem (that is, a false positive test that demonstrates the imprecision of the analyzer)?
|
||||
|
||||
(d) Do your false negative and false positive examples have a common underlying cause? Can the domain be improved to address them?
|
||||
|
||||
(3) Improving the domain
|
||||
|
||||
(a) Change the simple counting domain to a domain that overapproximates the set of storage locations that hold a resource. As a concrete goal, the new domain should allow you to print the name of the resource(s) that leak in the error message (rather than just the number of resources). The new domain should also allow your analysis to get the correct answer on your false negative and false positive tests from (2)(b) and (2)(c). Think about the following questions when designing your new domain:
|
||||
- How should we abstract storage locations? Is abstracting the stack program variables (`Var.t`)'s enough, or do we need an abstraction of the heap as well?
|
||||
- How will we handle aliasing (storage locations that store the same address?)
|
||||
- Will it be easy to extend the domain to incorporate information from the callee summaries/represent state that will be instantiated by callers (see (3))?
|
||||
- Some code that might be useful in creating your new domain (depending on what approach you choose): `AbstractDomain.FiniteSet`, `AbstractDomain.Map`, `AccessPath`, `Var`.
|
||||
|
||||
(b) Write some tests that demonstrate the limitations of your new domain: both false positives (names prefixed with `FP_` and false negatives (prefixed with `FN_`).
|
||||
|
||||
(4) Interprocedural analysis
|
||||
At this point, you likely have a fairly advanced intraprocedural analysis that is capable of finding resource leaks in real programs. Feel free to skip to (5) if you are eager to get started with bugfinding; many real resource leak bugs are intraprocedural. Alternatively, continue on with (4) to make your analysis interprocedural.
|
||||
|
||||
(a) Augment the summary type with state to indicate when the current procedure returns a resource. Allowing a resource to escape to the caller should not be considered a leak. This improvement should allow your analysis to pass the following tests:
|
||||
|
||||
```
|
||||
FileInputStream returnResourceOk() {
|
||||
return new FileInputStream("file.txt");
|
||||
}
|
||||
|
||||
FileInputStream returnResourceWrapperOk() {
|
||||
return returnResourceOk();
|
||||
}
|
||||
|
||||
void returnResourceThenCloseOk() {
|
||||
returnResourceWrapperOk().close();
|
||||
}
|
||||
|
||||
void returnResourceThenLeakBad() {
|
||||
returnResourceWrapperOk(); // warning
|
||||
}
|
||||
```
|
||||
|
||||
(b) Augment the summary type with state to indicate formals that are closed by the current function. This should allow your analysis to pass the following tests:
|
||||
|
||||
```
|
||||
void closeResourceOk(Closeable c) {
|
||||
c.close();
|
||||
}
|
||||
|
||||
void closeResourceWrapperOk(c) {
|
||||
closeResourceOk(c);
|
||||
}
|
||||
|
||||
void closeResourceDirectOK() {
|
||||
closeResourceOk(new FileInputStream("file.txt"));
|
||||
}
|
||||
|
||||
void closeResourceTransitiveOk()
|
||||
closeResourceOk(new FileInputStream("file.txt"));
|
||||
}
|
||||
|
||||
void closeOne(Closeable c1, Closeable c2) {
|
||||
c2.close();
|
||||
}
|
||||
|
||||
void closeOnlyOneBad() {
|
||||
closeOne(new FileInputStream("1.txt"), new FileInputStream("2.txt")); // warning
|
||||
}
|
||||
```
|
||||
|
||||
Hint: you might find the `FormalMap.t` stored in `proc_data.extras` useful for this. This module lets you go back and forth between the index of a formal and its name. This utility module is also used in `ThreadSafety` and `TaintAnalysis` modules.
|
||||
|
||||
(5) Making it practical
|
||||
|
||||
(a) Real resource leaks frequently involve failing to close resources along exceptional control-flow paths. For simplicity, the initial version of the current analysis uses a filtered view of the CFG that skips exceptional edges (`ProcCfg.Normal`). To find more bugs, you might want to switch to using `ProcCfg.Exceptional` and make sure that your analysis gets the right answer on some realistic exception examples like:
|
||||
|
||||
```
|
||||
void tryWithResourcesOk() {
|
||||
// this is syntactic sugar that makes sure stream gets closed
|
||||
try (FileInputStream stream = new FileInputStream("file.txt")) {
|
||||
...
|
||||
}
|
||||
}
|
||||
|
||||
void closeInFinallyOk() {
|
||||
FileInputStream stream = null;
|
||||
try {
|
||||
stream = new FileInputStream("file.txt");
|
||||
} finally {
|
||||
if (stream != null) {
|
||||
stream.close();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void closeInCatchBad() {
|
||||
FileInputStream stream = null;
|
||||
try {
|
||||
stream = new FileInputStream("file.txt");
|
||||
} catch {
|
||||
// ok not to close here, since we never acquired the resource
|
||||
}
|
||||
if (stream != null) {
|
||||
stream.close();
|
||||
}
|
||||
}
|
||||
|
||||
```
|
||||
|
||||
(b) Try running on real code! The instructions [here](http://fm.csl.sri.com/SSFT17/infer-instr.html) have several suggestions for open-source Android apps to point your analysis at. Try `./gradlew assembleDebug -x test` first to make sure everything builds correctly without Infer (if not, you are probably missing some dependencies--the error messages should guide you). Once that's working, try
|
||||
`./gradlew clean; infer -a checkers --no-default-checkers --resource-leak -- ./gradlew assembleDebug -x test`.
|
||||
- Found a real bug? Bonus points! Send a pull request to fix it! Very frequently, the best fix is to use try-with-resources.
|
||||
- Found a false positive in your analysis? Try re-running Infer with `--debug` and see if you can narrow down the root cause/fix it?
|
||||
- How does your analysis compare to Infer's production resource leak analysis? Run with `infer -- <gradle command>` to see if your analysis finds bugs that Infer misses, or vice versa.
|
||||
@ -0,0 +1,45 @@
|
||||
/*
|
||||
* Copyright (c) 2017 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
package codetoanalyze.java.checkers;
|
||||
|
||||
import java.io.FileInputStream;
|
||||
import java.io.FileNotFoundException;
|
||||
import java.io.IOException;
|
||||
|
||||
public class Leaks {
|
||||
|
||||
void basicLeakBad() throws FileNotFoundException {
|
||||
new FileInputStream("file.txt");
|
||||
}
|
||||
|
||||
void doubleLeakBad() throws FileNotFoundException {
|
||||
new FileInputStream("file1.txt");
|
||||
new FileInputStream("file2.txt");
|
||||
}
|
||||
|
||||
void basicReleaseOk() throws IOException, FileNotFoundException {
|
||||
FileInputStream stream = new FileInputStream("file.txt");
|
||||
stream.close();
|
||||
}
|
||||
|
||||
void acquireTwoForgetOneBad() throws IOException, FileNotFoundException {
|
||||
FileInputStream stream1 = new FileInputStream("file.txt");
|
||||
FileInputStream stream2 = new FileInputStream("file.txt");
|
||||
stream1.close();
|
||||
}
|
||||
|
||||
void acquireTwoThenReleaseOk() throws IOException, FileNotFoundException {
|
||||
FileInputStream stream1 = new FileInputStream("file.txt");
|
||||
FileInputStream stream2 = new FileInputStream("file.txt");
|
||||
stream1.close();
|
||||
stream2.close();
|
||||
}
|
||||
|
||||
}
|
||||
Loading…
Reference in new issue