From 8e4fea76931933d607b5e67f825b08f6a30789b7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 14 Jan 2019 06:07:11 -0800 Subject: [PATCH] [labs] fiddling Summary: Changing the text a bit. Reviewed By: mbouaziz Differential Revision: D13650583 fbshipit-source-id: a1ff99124 --- docker/master-java/Dockerfile | 3 +++ infer/src/labs/README.md | 37 +++++++++++++++++++++++++++-------- 2 files changed, 32 insertions(+), 8 deletions(-) diff --git a/docker/master-java/Dockerfile b/docker/master-java/Dockerfile index b48822846..dcd8503f4 100644 --- a/docker/master-java/Dockerfile +++ b/docker/master-java/Dockerfile @@ -63,3 +63,6 @@ ENV BUILD_MODE=default # prevent exiting by compulsively hitting Control-D ENV IGNOREEOF=9 + +# should be moved earlier +ENV INFER_OPAM_SWITCH=4.07.1 diff --git a/infer/src/labs/README.md b/infer/src/labs/README.md index 5b7d7df8f..7d9bcdbd2 100644 --- a/infer/src/labs/README.md +++ b/infer/src/labs/README.md @@ -14,9 +14,16 @@ Using Docker is the fastest way: you do not need to clone the Infer repository a 2. Run the infer Docker image with `docker run -it -v $HOME/infer-docker:/infer-host infer/infer:infer-latest-java-dev /bin/bash`. This will give you a prompt *inside the Docker image*. Do not close that terminal for the duration of the lab. -3. Within Docker, copy the /infer directory to your mount point: `cp -av /infer/. /infer-host` +3. Within Docker, pull the latest version of infer, copy the /infer directory to your mount point, then set up the opam environment for OCaml: -4. You can now edit the files *locally* in `$HOME/infer-docker` and build infer *inside Docker* in `/infer-host` using the shell prompt gotten in step 2. The quickest way is to run `make byte` from `/infer-host`. +```shell +cd /infer +git pull +cp -av /infer/. /infer-host +eval $(opam env) +``` + +You can now edit the files *locally* in `$HOME/infer-docker` and build infer *inside Docker* in `/infer-host` using the shell prompt gotten in step 2. The quickest way is to run `make byte` from `/infer-host`. ### (a') ...or, alternatively, build Infer locally from scratch @@ -28,13 +35,13 @@ See [CONTRIBUTING.md](https://github.com/facebook/infer/blob/master/CONTRIBUTING ## (1) Warm up: running, testing, and debugging Infer -(a) Change to the test directory (`cd infer/tests/codetoanalyze/java/lab`) and run the checker on a single file: +(a) Change to the test directory (`cd infer/tests/codetoanalyze/java/lab`) and run infer: ``` infer --resource-leak-only -- javac Leaks.java ``` -Infer should report 3 bugs. +Infer should report 7 resource leaks. These reports come from the separation logic based biabduction analysis. (b) Run the analyzer on a single test file to produce the debug HTML: @@ -50,10 +57,12 @@ firefox 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_printf`/`Logging.d_printfln` 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. Try adding `Logging.d_printfln "Hi Infer";` inside of the case for `Call`, recompiling/re-running. You should see the text you printed inside the appropriate CFG node log in the debug HTML. +(c) The `Logging.d_printf`/`Logging.d_printfln` 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. Try adding `Logging.d_printfln "Hi Infer";` inside of the case for `Call` in [ResourceLeaks.ml](./ResourceLeaks.ml), recompiling/re-running. You should see the text you printed inside the appropriate CFG node log in the debug HTML. (d) The `Logging.debug_dev` function prints to the console. 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). Try adding `Logging.debug_dev "Hi Infer;"` to the `compute_post` function, recompile/re-run and see your text printed on the command line. +Note: Using `Logging.debug_dev` generates warnings telling you that this function is deprecated. This is used to prevent developers from landing leftover debug instructions. + ## (2) Integer domain for straight-line programs (a) Let's start with a simple-minded analysis: count the number of open resources. Change `ResourceLeakDomain.t` to be of type `int`: @@ -86,7 +95,7 @@ Let's stick with just an integer domain to keep things simple until (5). ## (3) Integer domain for branching and looping programs -(a) Run your checker on [LeaksBranch.java](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/lab/LeaksBranch.java) it again. Uh oh, it crashed! Fix it by implementing `join` for your domain. +(a) Run your checker on [LeaksBranch.java](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/lab/LeaksBranch.java). Uh oh, it crashed! Fix it by implementing `join` for your domain. (b) Now run on [LeaksLoop.java](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/lab/LeaksLoop.java), and implement `widen`. Hmm... There's a termination bug in the abstract domain--do you see it? @@ -96,7 +105,7 @@ Let's stick with just an integer domain to keep things simple until (5). - Hint: `AbstractDomain.TopLifted` may be useful for this. Just put all the code in ResourceLeakDomain.ml that corresponds to the signature `AbstractDomain.S` into a submodule `FiniteBounds`, then let `TopLifted` do all the lifting with -``` +```OCaml include AbstractDomain.TopLifter (FiniteBounds) ``` @@ -105,7 +114,19 @@ include AbstractDomain.TopLifter (FiniteBounds) ## (4) Interprocedural analysis -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 tests in [LeaksInterprocedural.java](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/lab/LeaksInterprocedural.java). +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: + +```OCaml + match Payload.read pdesc callee_procname with + | Some summary -> + (* interprocedural analysis produced a summary: use it *) + () + | None -> + (* No summary for [callee_procname]; it's native code or missing for some reason *) + () +``` + +This improvement should allow your analysis to pass the tests in [LeaksInterprocedural.java](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/lab/LeaksInterprocedural.java). Hint: What do return values look like in infer? They are assignments to a special variable, detected by `Var.is_return`. You may also want to match only return variables of some specific object type. Use this code to look at the classname of the type of the return value: