[labs] fiddling

Summary: Changing the text a bit.

Reviewed By: mbouaziz

Differential Revision: D13650583

fbshipit-source-id: a1ff99124

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

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: