Skip to content

Latest commit

 

History

History
213 lines (162 loc) · 8.92 KB

INSTALL.md

File metadata and controls

213 lines (162 loc) · 8.92 KB

Installation

We provide two ways to install SAVER. The first one is to install full VirtualBox image. This image contains all benchmarks, dependencies, and FootPatch for comparison as well as our tool, SAVER. Also, we have wrote some scripts to conveniently reproduce our tables. Thus, if your focus is on reproducing the results, we recommend you to install the VM.

The second way to install SAVER is to download a binary executable file for Linux. We recommend this way if your purpose is to apply SAVER to your C project. We have confirmed that this executable works in an Ubuntu 16.04 system, hence we believe that it may also work in other similar systems, too. If you experience any trouble using SAVER in your setup, please contact the author(s). We would be happy to help you.

1. Installing a Virtual Machine Image

  1. Download and install VirtualBox at here
  2. Download the VM image: ICSE20_SAVER_artifacts.tar.gz
  3. Install the .vdi file with VirtualBox.

NOTE:

  • This is a large file: The size of the tarball itself is 6GB. If you decompress it, you obtain an additional 20GB .vdi file.
  • The experiment setup: Our data was obtained using a 32GB of memory and four virtual processors powered by an Intel Core i7-7700 processor. Also, about 10GB of additional disk space may be required running our scripts.

2. Installing a Linux Binary

  1. Download the tarball: saver.tar.gz
  2. Decompress it with tar xvzf saver.tar.gz
  3. Add the directory where the bin file is located to the PATH. For example, you may use ones like below:
    • export PATH=".../saver/bin/infer:$PATH"
    • alias infer=".../saver/bin/infer"

Testing

An Example Test

We show a brief test run on a simple conditional leak example. Below is a test program (located at tests/overview-example/) which shows a conditional memory leak. If the program executes the else branch, memory dynamically allocated to p never gets freed.

  1 #include <stdio.h>
  2 #include <stdlib.h>
  3 
  4 int main() {
  5   int *p, *q;
  6   int i;
  7 
  8   p = malloc(1); // o1
  9   if (i)
 10     q = p;
 11   else
 12     q = malloc(2); // o2
 13 
 14   *q = 1;
 15   free(q);
 16 
 17   return 0; // o1 leaks here
 18 }

First, let Infer compile this file and diagnose the problem:

infer -g run -- clang overview-example.c

Infer then reports the following memory-leak:

overview-example.c:12: error: MEMORY_LEAK (biabduction/Abs.ml:1082:18-25:)
  memory dynamically allocated by call to `malloc()` at line 8, column 7 is not reachable after line 12, column 9.
  10.       q = p;
  11.     else
  12. >     q = malloc(2); // o2
  13.   
  14.     *q = 1;

We have already prepared an error report in .json format called error-report.json in the directory:

{
  "err_type": "MEMORY_LEAK",
  "source": { "node": { "filename": "overview-example.c", "procedure": "main", "line": 8 }, "exp": null },
    "sink": { "node": { "filename": "overview-example.c", "procedure": "main", "line": 12 }, "exp": null }
}

The error report consists of source and sink information for a memory leak which can be obtained from usual memory leak detectors. This serves as an error report that SAVER can consume. Feed it to SAVER, and it will suggest a fix.

infer saver --error-report report.json

SAVER should output the following:

...
- Searching begins ... 
-- Final Patches: 
- [+] { Insert: if ({ main:i == { 0 } }) free(*(main:p)) at 3 (line 17, column 3) }
...

If this output is confirmed, SAVER is properly set up.

Basic Usage

Generalizing the previous example, we show how to run SAVER on any arbitrary C projects and kinds of errors. To run SAVER on your C project (or program) and obtain some patches, there are three necessary steps:

  1. Capture the program with Infer,
  2. Prepare an error report describing the error, and
  3. Creating a patch according to the patch instructions generated by SAVER.

1. Capture your program by Infer

Basically, SAVER utilizes Facebook Infer's front-end for patch generation. Infer is not only able to capture a single C source file, it is also capable of capturing a full C project where building tools like make is required. To learn more about Infer, please consult this Infer documentation (https://fbinfer.com/docs/analyzing-apps-or-projects) as it articulates really well on this topic.

NOTE: If you do not need Infer's memory leak alarms but only the capturing, use the following command. It makes Infer only perform a very simple analysis while capturing the program.

  infer -g run --nullsafe-only -- [compile command]

2. Prepare error reports

The error report should contain (1) the kind of a memory-leak error, and (2) the source and sink locations (program locations) of that error. The error report need not be obtained only from Infer alarms, any static analysis tool will do. However, Infer's leak detection is particularly good, and its bug reports are optimal cases where every piece of information is contained for writing our error report.

To make Infer create such information, run the following:

  infer -g run -- [compile command]

where compile command can be either of make [make_target] or clang [FILE]. Errors detected are organized into a single file inside your C project: infer-out/bugs.txt.

Now, we explain how to prepare an error report for SAVER with respect to different types of memory-errors, out of the information created from above.

.json File for Memory-Leak Errors

Create a .json file as follows.

  • Set "err_type" to "MEMORY_LEAK".
  • For the "source" key,
    • For the "node" key,
      • Set "filename" to the name of the C source file containing the allocation site.
      • Set "procedure" to the name of the procedure enclosing the allocation site.
      • Set "line" to the line number of the allocation site.
  • For the "sink" key,
    • For the "node" key,
      • Set "filename" to the name of the C source file where the allocated object becomes unreachable.
      • Set "procedure" to the name of the procedure where the allocated object becomes unreachable.
      • Set "line" to the line number of the location where the allocated object becomes unreachable.

Consult the above example error-report.json file if unclear.

.json File for Use-After-Free Errors

Create a .json file as follows.

  • Set "err_type" to "USE_AFTER_FREE".
  • For the "source" key,
    • For the "node" key,
      • Set "filename" to the name of the C source file where the object is freed.
      • Set "procedure" to the name of the procedure enclosing the location where the object is freed.
      • Set "line" to the line number of the location where the object is freed.
  • For the "sink" key,
    • For the "node" key,
      • Set "filename" to the name of the C source file where the object is used.
      • Set "procedure" to the name of the procedure enclosing the location where the object is used.
      • Set "line" to the line number of the location where the object is used.
.json File for Double-Free Errors

Create a .json file as follows.

  • Set "err_type" to "DOUBLE_FREE".
  • For the "source" key,
    • For the "node" key,
      • Set "filename" to the name of the C source file where the object is freed for the first time.
      • Set "procedure" to the name of the procedure enclosing the location where the object is freed for the first time.
      • Set "line" to the line number of the location where the object is freed for the first time.
  • For the "sink" key,
    • For the "node" key,
      • Set "filename" to the name of the C source file where the object is freed for the second time.
      • Set "procedure" to the name of the procedure enclosing the location where the object is freed for the second time.
      • Set "line" to the line number of the location where the object is freed for the second time.

3. Running SAVER

Now we can run SAVER with the command:

  infer saver --error-report [error-json]

where [error-json] is the filename of the error report.

SAVER then outputs patch instruction(s):

  • Insert free(exp) at line X.
X: ...;
(+): free(exp);
  • Delete free(exp) at line X.
(-)X: free(exp);
  • Replace exp at line Y by tmp and insert an assignment command (tmp := exp) at X.
X: ...;
(+) tmp := exp;
...
(-)Y: foo(exp);
(+)Y: foo(tmp);

Currently, these patches do not tell the exact location with respect to the source file, so you many need to manually translate the lines and columns to the location on a CFG. The CFG representation of a source file FILE.c is located at infer-out/captured/[FILE]*.html.