Technical Documentation: facebook/infer

ℹ️ Provenance: Multi-Tier Ingestion · CodeWiki Reference

Overview (README.md)

Infer

Infer is a static analysis tool for Java,
C++, Objective-C, and C. Infer is written in OCaml.

Installation

Read our Getting
Started page for
details on how to install packaged versions of Infer. To build Infer
from source, see INSTALL.md.

Contributing

See CONTRIBUTING.md.

License

Infer is MIT-licensed.

Note: Enabling Java support may require you to download and install
components licensed under the GPL.

00 Getting Started (`website/docs/00-getting-started.md`)

id: getting-started title: Getting started with Infer

Get Infer

You can use our binary releases, build infer from source, or use our Docker image.

Find our latest binary release here. Download
the tarball then extract it anywhere on your system to start using infer. For example, this
downloads infer in /opt on Linux (replace VERSION with the latest release, eg VERSION=1.0.0):

bash

VERSION=0.XX.Y; \
curl -sSL "https://github.com/facebook/infer/releases/download/v$VERSION/infer-linux-x86_64-v$VERSION.tar.xz" \
| sudo tar -C /opt -xJ && \
sudo ln -s "/opt/infer-linux-x86_64-v$VERSION/bin/infer" /usr/local/bin/infer

If the binaries do not work for you, or if you would rather build infer from
source, follow the
install from source
instructions to install Infer on your system.

Alternatively, use our Docker images.

Try Infer in your browser

Try Infer on a small example on
Codeboard.

00 Hello World (`website/docs/00-hello-world.md`)

id: hello-world title: Hello, World!

Follow the instructions in this page to try Infer on a few small examples. You
should be able to see the bugs reported by Infer, fix the bugs and run Infer
again to check that they are not reported anymore. This should give you a first
idea of how Infer works. See the User Guide for more details
about the use of Infer.

All these examples can be found in the
infer/examples
directory distributed with Infer.

Hello world Java

Here is a simple Java example to illustrate Infer at work.

java

// Hello.java
class Hello {
  int test() {
    String s = null;
    return s.length();
  }
}

To run Infer, type the following in your terminal from the same directory as
Hello.java.

bash

infer run -- javac Hello.java

You should see the following error reported by Infer.

bash

Hello.java:5: error: NULL_DEREFERENCE
  object s last assigned on line 4 could be null and is dereferenced at line 5

Now edit the file to add null checks:

java

int test() {
    String s = null;
    return s == null ? 0 : s.length();
  }

Run Infer again. This time we get no error: Infer reports No issues found.

Hello world Objective-C

Here is a simple Objective-C example to illustrate Infer at work.

objectivec

// Hello.m
#import <Foundation/Foundation.h>

@interface Hello: NSObject
@property NSString* s;
@end

@implementation Hello
NSString* m() {
    Hello* hello = nil;
    return hello->_s;
}
@end

To run Infer, type the following in your terminal from the same directory as
Hello.m.

bash

infer run -- clang -c Hello.m

You should see the following error reported by Infer.

text

Hello.m:10 NULL_DEREFERENCE
  pointer hello last assigned on line 9 could be null and is dereferenced at line 10, column 12

Now edit the file to use the getter instead of accessing the instance variable:

objectivec

NSString* m() {
    Hello* hello = nil;
    return hello.s;
}

Run Infer again. This time we get no error: Infer reports No issues found.

Hello world C

Here is a simple C example to illustrate Infer at work.

// hello.c
#include <stdlib.h>

void test() {
  int *s = NULL;
  *s = 42;
}

To run Infer, type the following in your terminal from the same directory as
hello.c.

bash

infer run -- gcc -c hello.c

You should see the following error reported by Infer.

text

hello.c:5: error: NULL_DEREFERENCE
  pointer s last assigned on line 4 could be null and is dereferenced at line 5, column 10

Now edit the file to add null checks:

void test() {
  int *s = NULL;
  if (s != NULL) {
    *s = 42;
  }
}

Run Infer again. This time we get no error: Infer reports No issues found.

When analyzing C files, Infer captures the gcc command and runs clang instead to
parse them. Thus you may get compiler errors and warnings that differ from
gcc's. So in particular, the following two commands are equivalent:

bash

infer run -- gcc -c hello.c
infer run -- clang -c hello.c

Hello world C (tree-sitter, no build system)

The tree-sitter frontend analyzes C files directly, without requiring a
compiler, headers, or build system. It is useful for quick checks, IDE
integration, and files that may not compile.

// hello.c
#include <stdlib.h>

void test() {
  int *s = NULL;
  *s = 42;
}

bash

infer --capture-tree-sitter hello.c --pulse

You should see the following error reported by Infer:

text

hello.c:6: error: NULLPTR_DEREFERENCE
  null dereference of `s`

Unlike the clang frontend, tree-sitter does not need headers or a compilation
database. It parses the source directly and analyzes what it can, even if the
file has syntax errors or missing includes. For full precision with type-aware
analysis, use the clang frontend instead (infer run -- clang -c hello.c).

Hello world Android

To be able to analyze the sample Android app, make sure that you have the
Android SDK 22
installed and up to date, as well as the "Android SDK Build-tools" and "Android
Support Repository" components.

Go to the sample Android app in
infer/examples/android_hello
and create a local.properties file with a single line
sdk.dir=<location of your Android SDK>. This sample Android app uses
gradle as its build system. You do not need to install
gradle to try it out though, thanks to the
gradlew
script in the project that will download gradle and the project's dependencies
for you.

After editing local.properties, run

bash

infer run -- ./gradlew build

Infer will output the list of found bugs:

bash

app/src/main/java/infer/inferandroidexample/MainActivity.java:29: error: NULL_DEREFERENCE
  object s last assigned on line 28 could be null and is dereferenced at line 29
  27.           setContentView(R.layout.activity_main);
  28.           String s = getDay();
  29. >         int length = s.length();
  30.           writeToFile();
  31.       }
  32.

app/src/main/java/infer/inferandroidexample/MainActivity.java:46: error: RESOURCE_LEAK
   resource of type java.io.FileOutputStream acquired to fis by call to FileOutputStream(...) at line 43 is not released after line 46
  44.               fis.write(arr);
  45.               fis.close();
  46. >         } catch (IOException e) {
  47.               //Deal with exception
  48.           }
  49.

app/src/main/java/infer/other/MainActivity.java:23: error: NULL_DEREFERENCE
  object returned by source() could be null and is dereferenced at line 23
  21.     @Override
  22.     protected void onCreate(Bundle savedInstanceState) {
  23. >     source().toString();
  24.     }
  25.

Differential analysis

If you run Infer again without changing any files, you will notice that this
time nothing gets analyzed. This is because gradle is incremental: everything
was compiled already so nothing gets recompiled. Infer captures the compilation
commands to know which files to analyze, hence it analyzes nothing in this case.
There are three solutions to remedy this:

Run gradlew clean in between Infer runs.
bash
```
./gradlew clean
```
This causes gradle to recompile everything each time, and subsequently Infer
to capture all the files again.
Run Infer indicating that the capture of compilation commands should
continue, using option --continue (or -c for short).
bash
```
infer run --continue -- ./gradlew build
```

This makes Infer add the effects of the new compilation commands to the previous
ones, and start a new analysis of the entire code.

Run Infer in reactive mode after a code change, using option --reactive (or
-r for short).
bash
```
infer run --reactive -- ./gradlew build
```

This makes Infer analyze the effects of the code change, without re-analyzing
everything. Note that only the modified files, and those dependent on them, are
re-analyzed. This analysis mode can be significantly faster.

You can learn more about the particulars of each solution in the
Infer workflow page.

Hello world iOS

Go to the sample iOS app in
infer/examples/ios_hello
and run Infer on it:

bash

infer run -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator

Infer will output the list of found bugs:

text

/* Detailed source-code truncated for AI context efficiency. */

Similarly to the case of gradle,
running the command above a second time will yield no analysis results, as
nothing gets recompiled. Either add the --reactive (or -r) flag to the
infer command:

bash

infer run --reactive -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator

or ask the build system to reinitialize the directory before running Infer
again, using

bash

xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator clean

Hello world Make

Go to the sample C project in
infer/examples/c_hello
and run Infer on it:

bash

infer run -- make

Infer will output the list of found bugs:

bash

example.c:22: error: NULL_DEREFERENCE
   pointer max last assigned on line 21 could be null and is dereferenced at line 22, column 10

example.c:36: error: NULL_DEREFERENCE
   pointer joe last assigned on line 35 could be null and is dereferenced by call to get_age() at line 36, column 10

example.c:45: error: RESOURCE_LEAK
   resource acquired to fd by call to open() at line 41, column 12 is not released after line 45, column 5

example.c:51: error: MEMORY_LEAK
   memory dynamically allocated to p by call to malloc() at line 51, column 14 is not reachable after line 51, column 3

example.c:57: error: MEMORY_LEAK
   memory dynamically allocated to p by call to malloc() at line 56, column 14 is not reachable after line 57, column 3

Similarly to the case of gradle,
running infer run -- make a second time will yield no analysis results, as
nothing gets recompiled. Either add the --reactive (or -r) flag to the
infer command:

bash

infer run --reactive -- make

or run

bash

make clean

before analyzing the project again.

01 Analyzing Apps Or Projects (`website/docs/01-analyzing-apps-or-projects.md`)

id: analyzing-apps-or-projects title: Analyzing apps or projects

To analyze files with Infer you can use the compilers javac and clang. You
can also use Infer with gcc, however, internally Infer will use clang to
compile your code. So, it may not work if your code does not compile with
clang.

Moreover, you can run Infer with a variety of build systems. Notice that you can
run infer faster by running the compilation command in parallel, e.g.
infer run -- make -j8. Please also take into account that if you wish to
analyze a project, you should probably do clean beforehand so that the
compiler compiles all the files and so Infer also analyses all the files (see
the previous section).

Here is an overview of the build systems supported by Infer. You can get more
information about how a particular build system is supported by looking at the
SYNOPSIS section of the infer-capture manual: infer capture --help.

ant

bash

infer run -- ant

Buck

Running:

bash

infer run -- buck <buck target>

will compute the list of Infer warnings in the targets passed as argument.

Running:

bash

infer run -- buck --deep <buck target>

will compute the list of Infer warnings in the targets passed as argument and
all the transitive dependencies.

The distinction between --deep and the normal Buck complation mode is only
supported for Java projects. For the other kinds of projects, the --deep
option has no effect.

cmake

The most robust way is to have cmake generate a compilation database that can
be then processed by Infer:

bash

cd build
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ..
cd ..
infer run --compilation-database build/compile_commands.json

Alternatively, one can trick cmake into using infer instead of the system's
compilers:

bash

cd build
infer compile -- cmake ..
infer run -- make -j 4

Gradle

bash

infer run -- gradle <gradle task, e.g. "build">
infer run -- ./gradlew <gradle task, e.g. "build">

Make

Infer can analyze projects that compile with make by switching the compilers
(for C/C++/Objective-C or Java) called by make with infer wrappers. This
doesn't always work, for instance if the Makefiles hardcode the absolute paths
to the compilers (eg, if make calls /usr/bin/gcc instead of gcc). This is
because this integration works by modifying PATH under the hood.

bash

infer run -- make <make target>

Maven

bash

infer run -- mvn <maven target>

Xcodebuild

The most robust way is to generate a compilation database, then pass that
database to Infer:

bash

xcodebuild <your build options> | tee xcodebuild.log
xcpretty -r json-compilation-database -o compile_commands.json < xcodebuild.log > /dev/null
infer run --skip-analysis-in-path Pods --clang-compilation-db-files-escaped compile_commands.json

xctool

Use xctool to generate a compilation database then pass it to infer:

bash

xctool.sh <your build options> -reporter json-compilation-database:compile_commands.json
infer run --skip-analysis-in-path Pods --clang-compilation-db-files-escaped compile_commands.json

Using a compilation database

Many build systems like cmake, Xcode or Buck generate compilation databases.
infer is able to use this database directly, simplifying its usage.

bash

infer --compilation-database compile_commands.json

Other build systems

If infer doesn't recognize your build system, you will get an error like this:

console

$ infer run -- foo
Usage Error: Unsupported build command foo

If your build system behaves like one of the above, you can tell infer to use
the same integration with --force-integration. For instance this will proceed
as if foo was working the same way as make:

bash

infer run --force-integration make -- foo

If your build system is more exotic, and it doesn't support outputting
compilation databases, please let us know by
opening an issue.

01 Infer Workflow (`website/docs/01-infer-workflow.md`)

id: infer-workflow title: Infer workflow

This page documents several ways of running Infer, that you can adapt to your
own project.

tl; dr:

Make sure your project is clean when you first run Infer on it (with
make clean, or gradle clean, or ...).
When running Infer several times in a row, either clean your project as in
step 1 in-between Infer runs, or add --reactive to the infer command.
These steps are not needed if you are not using an incremental build system,
for instance if you are analyzing single files with
infer run -- javac Hello.java.
After a successful Infer run, you can explore Infer's reports in more details
by running infer explore from the same directory.

The two phases of an Infer run

Regardless of the input language (Java, Objective-C, or C), there are two main
phases in an Infer run:

1. The capture phase

Compilation commands are captured by Infer to translate the files to be analyzed
into Infer's own internal intermediate language.

This translation is similar to compilation, so Infer takes information from the
compilation process to perform its own translation. This is why we call infer
with a compilation command: infer run -- javac File.java or
infer run -- clang -c file.c. What happens is that the files get compiled as
usual, and they also get translated by Infer to be analyzed in the second phase.
In particular, if no file gets compiled, also no file will be analyzed.

Infer stores the intermediate files in the results directory which by default is
created in the folder where the infer command is invoked, and is called
infer-out/. You can change the name of the results directory with the option
-o, e.g.

bash

infer run -o /tmp/out -- javac Test.java

You can run just the capture phase using the capture subcommand instead of the
run subcommand:

bash

infer capture -- javac Test.java

2. The analysis phase

In this phase, the files in infer-out/ are analyzed by Infer. Infer analyzes
each function and method separately. If Infer encounters an error when analyzing
a method or function, it stops there for that method or function, but will
continue the analysis of other methods and functions. So, a possible workflow
would be to run Infer on your code, fix the errors generated, and run it again
to find possibly more errors or to check that all the errors have been fixed.

The errors will be displayed in the standard output and also in a file
infer-out/report.txt. We filter the bugs and show the ones that are most
likely to be real.

Global (default) and differential workflows

By default, running Infer will delete the previous infer-out/ directory if it
exists. This leads to a default workflow where the entire project is analyzed
every time. Passing --reactive (or -r) to Infer prevents it from deleting
infer-out/, leading to a differential workflow.

There are exceptions to this. In particular, you can run only one of the phases
above. For instance, infer run -- javac Hello.java is equivalent to running
these two commands:

bash

infer capture -- javac Hello.java
infer analyze

Notice that the second command does not erase infer-out/, as the files it
needs to analyze live there!

You can learn more about the subcommands supported by Infer by running
infer --help, infer capture --help, or more generally
infer <subcommand> --help.

Let us highlight when you may need global and differential workflows.

Global workflow

The global workflow is well suited to running Infer on all the files in a
project, e.g., for a Gradle-based project that compiles using the gradle build
command:

bash

infer run -- gradle build

In general, running Infer on your project is as simple as running
infer run -- <your build command here> where the build command is the one you
would normally use to compile your source code.

To start a fresh analysis and be sure to analyze all the files in your project,
you have to clean the build products, for instance with make clean for a
make-based project, gradle clean for Gradle, etc.

Differential workflow

Software projects such as mobile apps use incremental build systems, where
code evolves as a sequence of code changes. For these projects, it can often
make sense to analyze only the current changes in the project, instead of
analyzing the whole project every time. It is possible to analyze only what's
changed using Infer's reactive mode.

Infer should first be run on a clean version of the project, to capture all
the compilation commands in its capture phase.

For instance, for a project compiled using Gradle,

bash

gradle clean
infer capture -- gradle build

Note that the above command does not perform an expensive analysis, but captures
all the compilation commands and stores the results in Infer's internal format.

Next, if you change some files in your project, for instance in response to an
Infer report, or as part of normal development, you can either clean and
reanalyze the entire project (as in the global workflow
above), or else tell Infer that you are interested in the effects of the code
change. The second option can be significantly faster, as only a subset of the
project needs to be analyzed: the modified files/procedures and their
dependencies.

bash

edit some/File.java
# make some changes to some/File.java
infer run --reactive -- gradle build

Note that you can run Infer with the --reactive flag the first time around as
well.

To control the granularity of the changes to be analyzed, it is possible to tell
Infer to combine several changes into one before the analysis. This is done with
the --continue option.

For example:

bash

edit some/File1.java
# make some changes to some/File1.java
infer run --reactive -- gradle build
edit some/File2.java
# make some changes to some/File2.java
infer run --reactive --continue -- gradle build

After the first invocation, Infer will analyze the results of the first change.
After the second invocation, Infer will analyze the results of both changes. If
the --continue option were omitted, it would only analyze the results of the
second change.

Finally, it is always possible to perform an analysis of the current changes in
isolation:

bash

infer run --reactive --continue -- analyze

The list of build systems supported by Infer is detailed in the
next section.

Exploring Infer reports

You can get more information about the reports generated by Infer by running
infer explore in the same directory. For instance

bash

infer run -- gradle build
infer explore

This tool allows you to see error traces leading to each bug reported by Infer,
which can be helpful in tracking down the precise cause of each bug. See the
output of infer explore --help for more information.

01 Man Pages (`website/docs/01-man-pages.md`)

id: man-pages title: Infer Manuals

Here are the man pages for all the infer commands:

01 Steps For Ci (`website/docs/01-steps-for-ci.md`)

id: steps-for-ci title: Recommended flow for CI

The recommended flow for CI integration is to determine the modified files, and
run the analysis in reactive mode starting from those files. If you would like
to run more than one analyzer, it is more efficient to separate the capture
phase, so that the result can be used by all the analyzers.

Differential Workflow

Here's how to run infer on two versions of a project and compare the results in
general.

Assume the project uses git, feature is the feature branch (the code change
you want to analyze), main is the main branch, and make builds the
project.

bash

# go to feature branch if not there already
git checkout feature
# get list of changed files
git diff --name-only origin/feature..origin/main > index.txt
## first run: feature branch
# run infer on the feature branch
infer capture -- make -j 4  # assuming a machine with 4 cores
infer analyze --changed-files-index index.txt
# store the infer report
cp infer-out/report.json report-feature.json
## second run: main branch
git checkout main
# run capture in reactive mode so that previously-captured source files are kept if they are up-to-date
infer capture --reactive --mark-if-unchanged -- make -j 4
infer analyze --incremental-analysis --changed-files-index index.txt
# compare reports
infer reportdiff --report-current report-feature.json --report-previous infer-out/report.json

At the end of this process, "infer-out/differential/" contains three files,
which follow the same format as normal infer JSON reports:

introduced.json contains the issues found in the feature branch but not in
main;
fixed.json contains the issues found in main but not in the feature branch;
preexisting.json contains the issues found in both branches.

Example: Android Gradle

The following CI script runs the infer and eradicate analyzers. Assume again
that feature is the feature branch, and main is the main branch.

bash

git diff --name-only origin/feature..origin/main > index.txt
infer capture -- ./gradlew --offline assembleDebug
infer analyze --fail-on-issue --eradicate --changed-files-index ./index.txt

Notice that

We use git to find the changed files git diff --name-only
We run capture only once, and the output is kept for the subsequent analyses
We run the eradicate analysis alongside the default analyses: --eradicate
We analyze only the changed files --changed-files-index ./index.txt

01 Suppressions (`website/docs/01-suppressions.md`)

id: suppressions title: Suppression of Infer Issues

Infer includes a language-agnostic method to suppress Infer issues in source files.

When an Infer issue is suppressed, it will not appear in the text report (infer-out/report.txt) after an Infer run. Suppressed issues will still appear in the JSON report file (infer-out/report.json) but with the added key "suppressed": true.

Two keywords are supported:

@infer-ignore ISSUE_TYPE, ISSUE_TYPE2, ...

Ignore matching Infer issues on the next or current line. Comma , is used to separate multiple issue types on the same line.
@infer-ignore-every ISSUE_TYPE, ISSUE_TYPE2, ...

Ignore all matching Infer issues in the current file. This keyword can be added anywhere in the source file.

These two keywords are meant to be added as comment lines in the source files you run Infer on.

The full name of the issue type is given as an argument to the @ignore keywords. For example, use DEAD_STORE and not 'Dead Store' which is the name used in the text report file.

Wildcards

Wildcards can be used as arguments to the @ignore keywords to suppress a larger set of Infer issue types without the need to list all of them.

For example, @infer-ignore PULSE_UNNECESSARY_COPY* will suppress all unnecessary copy issues, including PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST and PULSE_UNNECESSARY_COPY_INTERMEDIATE, etc.

Examples

Suppress a single issue

java

// @infer-ignore THREAD_SAFETY_VIOLATION
if (ConfigUtil.getBoolean(context)) {
    ...
}

// or

if (ConfigUtil.getBoolean(context)) { // @infer-ignore THREAD_SAFETY_VIOLATION
    ...
}

Suppress all issues in a file

php

% @infer-ignore-every TOPL_ERROR, TOPL_ERROR_LATENT
-module(hello).
-export([hello_world/0]).
hello_world() -> io:fwrite("hello\n").

A line without an @ignore keyword cannot be placed between the @ignore line and the line with the issues.

java

// @infer-ignore THREAD_SAFETY_VIOLATION
// some more context
if (ConfigUtil.getBoolean(context)) {
    ...
}

In this case, the issue on the if statement line is not suppressed since a line without a @infer-ignore is added between the suppression and the line with the issue.

Accumulation

When using the @infer-ignore keyword, all issue types in a contiguous block of comment lines containing the @infer-ignore keyword are accumulated and applied to the next line without a @ignore keyword. This way, long lines can be avoided, and extra context can be given.

For example:

free(x);
// a really good explanation why we are suppressing this warning
// @infer-ignore USE_AFTER_FREE
// also this one @infer-ignore DEAD_STORE
return *x;

In the example above, on the return line, both the issue types USE_AFTER_FREE and DEAD_STORE are suppressed.

Equivalent to the example above:

free(x);
// a really good explanation why we are suppressing this warning
// @infer-ignore USE_AFTER_FREE
return *x; // @infer-ignore DEAD_STORE

An alternative way to achieve the same result would be:

free(x);
// a really good explanation why we are suppressing this warning
// @infer-ignore USE_AFTER_FREE, DEAD_STORE
return *x;

02 About Infer (`website/docs/02-about-infer.md`)

id: about-Infer title: About Infer

Infer is a static program analyzer for Java, C, C++, Objective-C, and
Erlang, written in OCaml. Infer is deployed
within Meta and it is running as part of its Continuous Integration
pipeline to verify select properties of every code modification for a
large range of projects, including the main family of apps such as
Facebook, Messenger, Instagram, and WhatsApp. Infer is used at a
number of other companies too. Infer can detect deep issues such as
null pointer dereferences, data races, and many more, which can
involve reasoning about multiple functions or methods in different
files in the code.

02 Separation Logic And Biabduction (`website/docs/02-separation-logic-and-biabduction.md`)

id: separation-logic-and-bi-abduction title: Separation logic and bi-abduction

export const Math = ({ code }) => ( );

Separation logic

Separation logic is a novel kind of mathematical logic which facilitates
reasoning about mutations to computer memory. It enables scalability by breaking
reasoning into chunks corresponding to local operations on memory, and then
composing the reasoning chunks together.

Separation logic is based on a logical connective
called the separating conjunction and pronounced "and separately". Separation
logic formulae are interpreted over program allocated heaps. The logical formula
holds of a piece of program heap (a heaplet) when it
can be divided into two sub-heaplets described by and
. For example, the formula

can be read " points to and
separately points to ". This
formula describes precisely two allocated memory cells. The first cell is
allocated at the address denoted by the pointer and the
content of this cell is the value of . The second cell is
allocated at the address denoted by the pointer and the
content of this second cell is the value of . Crucially,
we know that there are precisely two cells because
stipulates that they are separated and therefore the cells are allocated in two
different parts of memory. In other words, says that
and do not hold the same value
(i.e., these pointers are not aliased). The heaplet partitioning defined by the
formula above can be visualized like so:

The important thing about the separating conjunction is the way that it fits
together with mutation to computer memory; reasoning about program commands
tends to work by updating -conjuncts in-place, mimicking
the operational in-place update of RAM.

Separation logic uses Hoare triples of the form
where
is the precondition, a
program part, and the postcondition. Triples are
abstract specifications of the behavior of the program. For example, we could
take

as a specification for a method which closes a resource given to it as a
parameter.

Now, suppose we have two resources and
, described by
and we close the
first of them. We think operationally in terms of updating the memory in place,
leaving alone, as described by this triple:

What we have here is the that specification (spec) described how
works by mentioning only one piece of
state, what is sometimes called a small specification, and in (use) we use that
specification to update a larger precondition in place.

This is an instance of a general pattern. There is a rule that lets you go from
smaller to bigger specifications

Our passage from (spec) to (use) is obtained by taking

to be
to be ,
and
to be

This rule is called the frame rule of separation logic. It is named after the
frame problem, a classic problem in artificial intelligence. Generally, the
describes state that remains unchanged; the
terminology comes from the analogy of a background scene in an animation as
unchanging while the objects and characters within the scene change.

The frame rule is the key to the principle of local reasoning in separation
logic: reasoning and specifications should concentrate on the resources that a
program accesses (the footprint), without mentioning what doesn't change.

Bi-abduction

Bi-abduction is a form of logical inference for separation logic which automates
the key ideas about local reasoning.

Usually, logic works with validity or entailment statements like

which says that implies . Infer
uses an extension of this inference question in an internal theorem prover while
it runs over program statements. Infer's question

is called bi-abduction. The problem here is for the theorem prover to
discover a pair of frame and antiframe formulae that make the entailment
statement valid.

Global analyses of large programs are normally computationally intractable.
However, bi-abduction breaks apart a large analysis of a large program into
small independent analyses of its procedures. This gives Infer the ability to
scale independently of the size of the analyzed code. Moreover, by breaking the
analysis into small independent parts, when the full program is analyzed again
because of a code change the analysis results of the unchanged part of the code
can be reused, and only the code change needs to be re-analyzed. This process
is called incremental analysis and it is very powerful when integrating a
static analysis tool like Infer in a development environment.

In order to be able to decompose a global analysis into small independent
analyses, let's first consider how a function call is analyzed in separation
logic. Assume we have the following spec for a function
:

and by analyzing the caller function, we compute that before the call of , the formula
holds. Then to utilize the specification of the
following implication must hold:

Given that, bi-abduction is used at procedure call sites for two reasons: to
discover missing state that is needed for the above implication to hold and
allow the analysis to proceed (the antiframe) as well as state that the
procedure leaves unchanged (the frame).

To see how this works suppose we have some bare code

but no overall specification; we are going to describe how to discover a
pre/post spec for it. Considering the first statement and the (spec) above, the
human might say: if only we had in the
precondition then we could proceed. Technically, we ask a bi-abduction question:

and we can fill this in easily by picking
and
, where
means the empty state. The is recording that at the start
we presume nothing. So we obtain the trivially true implication:

which, by applying logical rules, can be re-written equivalently to:

Notice that this satisfies the (Function Call) requirement to correctly make
the call. So let's add that information in the , and while
we are at it, record the information in the of the first
statement that comes from .

Now, let's move to the second statement. Its precondition
in the partial symbolic execution trace
just given does not have the information needed by
, so we can fill that in and continue by
putting in the . While
we are at it, we can thread this assertion back to the beginning.

This information on what to thread backwards can be obtained as the antiframe
part of the bi-abduction question:

where the solution picks
.
Note that the antiframe is precisely the information missing from the
precondition in order for to proceed. On
the other hand, the frame is the portion
of state not changed by ; we can thread
that through to the overall postconditon (as justified by the frame rule),
giving us:

Thus, we have obtained a and for this
code by symbolically executing it, using bi-abduction to discover preconditions
(abduction of antiframes) as well as untouched portions of memory (frames) as
we go along.

In general, bi-abduction provides a way to infer a pre/post specs from bare
code, as long as we know specs for the primitives at the base level of the code.
The human does not need to write preconditions and postconditions for all the
procedures, which is the key to having a high level of automation. This is the
basis for how Infer works, why it can scale, and how it can analyze code changes
incrementally.

Context: The logical terminology we have been using here comes from AI and
philosophy of science. Abductive inference was introduced by the philosopher
Charles Peirce, and described as the mechanism underpinning hypothesis formation
(or, guessing what might be true about the world), the most creative part of the
scientific process. Abduction and the frame problem have both attracted
significant attention in AI. Infer uses an automated form of abduction to
generate preconditions describing the memory that a program touches (the
antiframe part above), and frame inference to discover what isn't touched. Infer
then uses deductive reasoning to calculate a formula describing the effect of a
program, starting from the preconditions. In a sense, Infer approaches automated
reasoning about programs by mimicking what a human might do when trying to
understand a program: it abduces what the program needs, and deduces conclusions
of that. It is when the reasoning goes wrong that Infer reports a potential bug.

This description is by necessity simplified compared to what Infer actually
does. More technical information can be found in the following papers. The
descriptions in the papers are precise, but still simplified; there are many
engineering decisions not recorded there. Finally, beyond the papers, you can
read the source code if you wish!

Technical papers

The following papers contain some of the technical background on Infer and
information on how it is used inside Facebook.

Local
Reasoning about Programs that Alter Data Structures. An early separation
logic paper which advanced ideas about local reasoning and the frame rule.
Smallfoot:
Modular Automatic Assertion Checking with Separation Logic. First
separation logic verification tool, introduced frame inference
A Local Shape
Analysis Based on Separation Logic. Separation logic meets abstract
interpretation; calculating loop invariants via a fixed-point computation.
Compositional Shape
Analysis by Means of Bi-Abduction. The bi-abduction paper.
Moving
Fast with Software Verification. A paper about the way we use Infer at
Facebook.

04 Absint Framework (`website/docs/04-absint-framework.md`)

id: absint-framework title: Building checkers with the Infer.AI framework

Infer.AI is a framework for quickly developing abstract interpretation-based
checkers (intraprocedural or interprocedural). You define only:

An abstract domain (type of abstract state plus <=, join, and widen
operations)
Transfer functions (a transformer that takes an abstract state as input and
produces an abstract state as output)

What you get in exchange is an analysis that can run on all of the
languages Infer supports (C, Objective-C, C++, and Java)!

This guide covers how to use the framework. For background on why we built the
framework and how it works, check out these
slides from a PLDI
2017 tutorial and this
talk
from @Scale2016.

If you feel like coding instead of reading, a great way to get started with
Infer.AI is to go through the lab exercise
here.

By example: intraprocedural analysis

This section helps you get started ASAP if you already understand
abstract interpretation (or
don't, but are feeling bold).

Take a look at
liveness.ml.
This code is performing a compilers-101 style liveness analysis over
SIL, Infer's intermediate
language. Since this code is fairly small and you should already understand what
it's trying to do, it's a fairly good place to look in order to understand both
how to use the abstract interpretation framework and what SIL is.

There are basically three important bits here: defining the domain, defining the
transfer functions, and then passing the pieces to the framework to create an
analysis. Let's break down the third bit:

ocaml

module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional))
module CheckerAnalyzer =
  AbstractInterpreter.MakeRPO (TransferFunctions (CheckerMode) (CFG))

The ProcCfg.Backward (ProcCfg.Exceptional) part says: "I want the direction of
iteration to be backward" (since liveness is a backward analysis), and "I want
the analysis to follow exceptional edges". For a forward analysis that ignores
exceptional edges, you would do ProcCfg.Normal instead (and many other
combinations are possible; take a look at
ProcCfg.mli
for more). And finally, the TransferFunctions part says "Use the transfer
functions I defined above".

Now you have a CheckerAnalyzer module that exposes useful functions
like
compute_post
(take a procedure as input and compute a postcondition) and
exec_pdesc
(take a procedure and compute an invariant map from node id's to the
pre/post at each node). The next step is to hook your checker up to
the Infer command-line interface (CLI). For the liveness analysis, you
would do this by exposing a function for running the checker on a
single procedure:

ocaml

let checker ({IntraproceduralAnalysis.proc_desc; err_log} as analysis_data) =
  match Analyzer.compute_post analysis_data ~initial:Domain.empty with
  | Some post ->
      Logging.progress "Computed post %a for %a"
        Domain.pp post Procname.pp (Procdesc.get_proc_name proc_desc);
  | None -> ()

and then adding Liveness.checker to the list of registered checkers
in
registerCheckers.ml
(search for "Liveness").

you can then run infer run --liveness-only -- <your_build_command> to run your
checker on real code. See here for more
details on the build systems supported by Infer.

Other examples of simple intraprocedural checkers are
addressTaken.ml
and
Siof.ml.

Error reporting

Useful analyses have output. Basic printing to stderr or stderr is
good for debugging, but to report a programmer-readable error that is
tied to a source code location, you'll want to use
Reporting.log_issue.

By example: interprocedural analysis

Let's assume you have already read and understood the "intraprocedural analysis"
section and have an intraprocedural checker. The abstract interpretation
framework makes it easy to convert your intraprocedural analysis into a
modular interprocedural analysis. Let me emphasize the modular point once
more; global analyses cannot be expressed in this framework.

To make your checker interprocedural, you need to:

Define the type of procedure summaries for your analysis and let
registerCheckers.ml know that your checker is interprocedural
Add logic for (a) using summaries in your transfer functions and (b)
converting your intraprocedural abstract state to a summary.

A good example to look at here is
Siof.ml.
Step (1) is just:

ocaml

(* in src/checkers/SiofDomain.ml *)
(* note that as a result the type of summaries is the same as the type of domain
   elements *)
module Summary = ...
include Summary


(* in src/backend/Payloads.ml: register the payload of the analyzer *)
type t =
  { ...
  ; siof: SiofDomain.Summary.t option
  ... }


(* in src/backend/registerCheckers.ml *)
let all_checkers = [ ...
  ; {checker= SIOF; callbacks= [(interprocedural Payloads.Fields.siof Siof.checker, Clang)]}
  ... ]

Here, the type of the abstract state and the type of the summary are the same,
which makes things easier for us (no logic to convert an abstract state to a
summary).

Part (2a) is
here
and uses the analyze_dependency callback provided by the framework:

text

match analyze_dependency callee_pname with

This says: "read the summary for callee_pname, possibly computing it
first". You must then add logic for applying the summary to the
current abstract state (often, this is as simple as doing a join).

Because our summary type is the same as the abstract state, part (2b)
here simply consists in return the post computed by the analysis as
the procedure's summary, using Analyzer.compute_post.

That's it! We now have an interprocedural analysis.

To go deeper, jump to the lab
exercise
and to the API documentation, e.g. for the
Absint and
IR modules.

04 Internal API (`website/docs/04-internal-API.md`)

id: internal-API title: Infer Internal OCaml Modules API

Browse the generated documentation for Infer's OCaml code here.

You can also generate these pages from within an Infer repository with make doc.

All Categories (`website/docs/all-categories.md`)

title: List of all categories of issue types

Here are all the categories that issue types might belong to in Infer. Some issue types have no associated category at the moment. This usually indicates that the issue type is not yet mature enough to be used.

Concurrency

Concurrent accesses to the same resource conflict in a way that can give incorrect results, block progress, or result in undefined behaviour.

Issue types in this category:

Logic error

Something that does not make sense and the sign of a potential programming error.

Issue types in this category:

Memory error

Incorrect handling of pointers that isn't a null pointer dereference, but can still result in undefined behaviour and crashes.

Issue types in this category:

Null pointer dereference

The null pointer is used where a valid pointer is required, causing a memory fault and a crash. For example, it is dereferenced.

Issue types in this category:

Perf regression

Unnecessary (or blocking) computation is performed, potentially causing a performance or responsiveness regression.

Issue types in this category:

Resource leak

A resource (for example memory, or a file descriptor) has been manually allocated but not released, possibly creating memory pressure over time or even incorrect results.

Issue types in this category:

Runtime exception

A runtime exception can occur and potentially crash the program.

Issue types in this category:

Sensitive data flow

Sensitive data is flowing where it shouldn't.

Issue types in this category:

Ungated code

Code must be under a gating mechanism but isn't.

Issue types in this category:

CONFIG_IMPACT_STRICT

User defined property

A user defined (custom) property is violated.

Issue types in this category:

All Checkers (`website/docs/all-checkers.md`)

title: List of all checkers hide_table_of_contents: true

Here is an overview of the checkers currently available in Infer.

Annotation Reachability

Given pairs of source and sink annotations, e.g. @A and @B, this checker will warn whenever some method annotated with @A calls, directly or indirectly, another method annotated with @B. Besides the custom pairs, it is also possible to enable some built-in checks, such as @PerformanceCritical reaching @Expensive or @NoAllocation reaching new. It is also possible to model methods as if they were annotated, using regular expressions. This should also work in languages where there are no annotations. See flags starting with --annotation-reachability.

Visit here for more information.

Buffer Overrun Analysis (InferBO)

InferBO is a detector for out-of-bounds array accesses.

***DEPRECATED*** Use Pulse instead.

Visit here for more information.

Config Gating

Determines which config flags gate the execution of each line of code.

Visit here for more information.

Config Impact Analysis

[EXPERIMENTAL] Collects function that are called without config checks.

Visit here for more information.

Cost: Complexity Analysis

Computes the asymptotic complexity of functions with respect to execution cost or other user defined resources. Can be used to detect changes in the complexity with infer reportdiff.

Visit here for more information.

Static Constructor Stall Checker

Detect if dispatch_once is called from a static constructor.

Visit here for more information.

Fragment Retains View

Detects when Android fragments are not explicitly nullified before becoming unreachable.

Visit here for more information.

Impurity

Detects functions with potential side-effects. Same as "purity", but implemented on top of Pulse.

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Visit here for more information.

Inefficient keySet Iterator

Check for inefficient uses of iterators that iterate on keys then lookup their values, instead of iterating on key-value pairs directly.

Visit here for more information.

Lineage

Computes a dataflow graph

Visit here for more information.

Litho "Required Props"

Checks that all non-optional @Props have been specified when constructing Litho components.

Visit here for more information.

Liveness

Detection of dead stores and unused variables.

Visit here for more information.

Loop Hoisting

Detect opportunities to hoist function calls that are invariant outside of loop bodies for efficiency.

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Visit here for more information.

Parameter Not Null Checked

An Objective-C-specific analysis to detect when a block parameter is used before being checked for null first.

Visit here for more information.

Pulse

General-purpose memory and value analysis engine.

Visit here for more information.

Purity

Detects pure (side-effect-free) functions. A different implementation of "impurity".

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Visit here for more information.

RacerD

Thread safety analysis.

Visit here for more information.

Resource Leak Lab Exercise

Toy checker for the "resource leak" write-your-own-checker exercise.

Visit here for more information.

SIL validation

This checker validates that all SIL instructions in all procedure bodies conform to a (front-end specific) subset of SIL.

Visit here for more information.

Static Initialization Order Fiasco

Catches Static Initialization Order Fiascos in C++, that can lead to subtle, compiler-version-dependent errors.

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Visit here for more information.

Scope Leakage

The Java/Kotlin checker takes into account a set of "scope" annotations and a must-not-hold relation over the scopes. The checker raises an alarm if there exists a field access path from object A to object B, with respective scopes SA and SB, such that must-not-hold(SA, SB).

Visit here for more information.

Self in Block

An Objective-C-specific analysis to detect when a block captures self.

Visit here for more information.

Starvation

Detect various kinds of situations when no progress is being made because of concurrency errors.

Visit here for more information.

Swift/Obj-C Nullability

Detects missing nullability annotations in Objective-C methods called from Swift, which can lead to runtime crashes via Implicitly Unwrapped Optionals.

Visit here for more information.

Topl

Detect errors based on user-provided state machines describing temporal properties over multiple objects.

Visit here for more information.

All Issue Types (`website/docs/all-issue-types.md`)

title: List of all issue types

Here is an overview of the issue types currently reported by Infer.

ARBITRARY_CODE_EXECUTION_UNDER_LOCK

Reported as "Arbitrary Code Execution Under lock" by starvation.

A call that may execute arbitrary code (such as registered, or chained, callbacks) is made while holding a lock.
This code may deadlock whenever the callbacks obtain locks themselves, so it is an unsafe pattern.

Example:

java

SettableFuture future = null;

  public void callFutureSet() {
    future.set(null);
  }

  // synchronized means it's taking a lock implicitly
  public synchronized void example_of_bad_pattern() {
    callFutureSet(); // <- issue reported here
  }

  // If the call is made while holding multiple locks, the warning
  // will be issued only at the innermost lock acquisition. Here we
  // report in example_of_bad_pattern but we won't report below.
  public void nested_bad_pattern_no_report(Object o) {
    synchronized (o) {
      example_of_bad_pattern(); // <- no issue reported
    }
  }

BAD_ARG

Category: Runtime exception. Reported as "Bad Arg" by pulse.

Bad arg in Erlang: Reports an error when the type of an argument is wrong or the argument is badly formed. Corresponds to the badarg error in the Erlang runtime.

For example, trying to concatenate the number 3 with the list [1,2] gives badarg error because 3 is not a list.

erlang

f() ->
    3 ++ [1,2]. // badarg error

Note that although the first argument needs to be a list, the second argument may not be a list.
For instance, concatenating [1,2] with the number 3 raises no error in Erlang.

erlang

g() ->
    [1,2] ++ 3. // no error. Result: [1,2|3]

BAD_ARG_LATENT

Category: Runtime exception. Reported as "Bad Arg Latent" by pulse.

A latent BAD_ARG. See the documentation on Pulse latent issues.

BAD_GENERATOR

Category: Runtime exception. Reported as "Bad Generator" by pulse.

Bad generator in Erlang: Reports an error when a wrong type is used in a generator. Corresponds to the bad_generator error in the Erlang runtime.

For example:

erlang

list_instead_of_map() ->
    M = [],
    [{K, V} || K := V <- M]

BAD_GENERATOR_LATENT

Category: Runtime exception. Reported as "Bad Generator Latent" by pulse.

A latent BAD_GENERATOR. See the documentation on Pulse latent issues.

BAD_KEY

Category: Runtime exception. Reported as "Bad Key" by pulse.

Bad key in Erlang: Reports an error when trying to access or update a non-existing key in a map. Corresponds to the {badkey,K} error in the Erlang runtime.

For example, trying to update the key 2 in M gives {badkey,2} error because 2 is not present as a key in M.

erlang

f() ->
    M = #{},
    M#{2 := 3}.

Note that maps currently use a recency abstraction, meaning that only the most recent key/value is tracked.
Therefore, if a map is non-empty and we try to access a key other than the one we track, we just assume that it is there to avoid false positives.

BAD_KEY_LATENT

Category: Runtime exception. Reported as "Bad Key Latent" by pulse.

A latent BAD_KEY. See the documentation on Pulse latent issues.

BAD_MAP

Category: Runtime exception. Reported as "Bad Map" by pulse.

Bad map in Erlang: Reports an error when trying to access or update a key for a term that is not a map. Corresponds to the {badmap,...} error in the Erlang runtime.

For example, trying to update L as if it was a map gives {badmap,[1,2,3]} error because L is actually a list ([1,2,3]).

erlang

f() ->
    L = [1,2,3],
    L#{1 => 2}.

BAD_MAP_LATENT

Category: Runtime exception. Reported as "Bad Map Latent" by pulse.

A latent BAD_MAP. See the documentation on Pulse latent issues.

BAD_RECORD

Category: Runtime exception. Reported as "Bad Record" by pulse.

Bad record in Erlang: Reports an error when trying to access or update a record with the wrong name. Corresponds to the {badrecord,Name} error in the Erlang runtime.

For example, accessing R as a person record gives {badrecord,person} error because R is rabbit (even though both share the name field).

erlang

-record(person, {name, phone}).
-record(rabbit, {name, color}).

f() ->
    R = #rabbit{name = "Bunny", color = "Brown"},
    R#person.name.

BAD_RECORD_LATENT

Category: Runtime exception. Reported as "Bad Record Latent" by pulse.

A latent BAD_RECORD. See the documentation on Pulse latent issues.

BAD_RETURN

Reported as "Bad Return" by pulse.

Bad return in Erlang: The dynamic type of a returned value disagrees with the static type given in the spec.

For example, this function returns an integer, while the spec says it returns an atom.

erlang

-spec f() -> atom().
f() -> 1.

Note that this will not lead to a runtime error when running the Erlang program.

BAD_RETURN_LATENT

Reported as "Bad Return Latent" by pulse.

A latent BAD_RETURN. See the documentation on Pulse latent issues.

BLOCK_PARAMETER_NOT_NULL_CHECKED

Category: Null pointer dereference. Reported as "Block Parameter Not Null Checked" by parameter-not-null-checked.

This error type is reported only in Objective-C/Objective-C++. It happens when a method has a block as a parameter,
and the block is executed in the method's body without checking it for nil first. If a nil block is passed to
the method, then this will cause a crash. For example:

objectivec

- (void)uploadTaskWithRequest:(NSURLRequest*)urlRequest
                       fromFile:(NSURL*)fileURL
                       delegate:(id)delegate
                  delegateQueue:(NSOperationQueue*)delegateQueue
                     completion:(void (^)())completion {
     ...
    completion();
}

Action:
Possible solutions are adding a check for nil, or making sure that the method
is not ever called with nil. When an argument will never be nil, you can add
the annotation nonnull to the argument's type, to tell Infer (and the type
system), that the argument won't be nil. This will silence the warning.

BUFFER_OVERRUN_L1

Reported as "Buffer Overrun L1" by bufferoverrun.

This is reported when outside of buffer bound is accessed. It can corrupt memory and may introduce
security issues in C/C++.

For example, int a[3]; a[5] = 42; generates a BUFFER_OVERRUN_L1 on a[5] = 42;.

Buffer overrun reports fall into several "buckets" corresponding to the expected precision of the
report. The higher the number, the more likely it is to be a false positive.

L1: The most faithful report, when it must be unsafe. For example, array size: [3,3],
offset: [5,5].
L2: Less faithful report than L1, when it may be unsafe. For example, array size:[3,3],
offset: [0,5]. Note that the offset may be a safe value in the real execution, i.e. safe when
0, 1, or 2; unsafe when 3, 4, or 5.
L5: The least faithful report, when there is an interval top. For example, array size:
[3,3], offset: [-oo,+oo].
L4: More faithful report than L5, when there is an infinity value. For example, array size:
[3,3], offset: [0, +oo].
L3: The reports that are not included in the above cases.
S2: An array access is unsafe by symbolic values. For example, array size: [n,n], offset
[n,+oo].
U5: An array access is unsafe by unknown values, which are usually from unknown function
calls.

BUFFER_OVERRUN_L2

Reported as "Buffer Overrun L2" by bufferoverrun.

See BUFFER_OVERRUN_L1

BUFFER_OVERRUN_L3

Reported as "Buffer Overrun L3" by bufferoverrun.

See BUFFER_OVERRUN_L1

BUFFER_OVERRUN_L4

Reported as "Buffer Overrun L4" by bufferoverrun.

See BUFFER_OVERRUN_L1

BUFFER_OVERRUN_L5

Reported as "Buffer Overrun L5" by bufferoverrun.

See BUFFER_OVERRUN_L1

BUFFER_OVERRUN_S2

Reported as "Buffer Overrun S2" by bufferoverrun.

See BUFFER_OVERRUN_L1

BUFFER_OVERRUN_U5

Reported as "Buffer Overrun U5" by bufferoverrun.

See BUFFER_OVERRUN_L1

CAPTURED_STRONG_SELF

Category: Resource leak. Reported as "Captured strongSelf" by self-in-block.

This check is about when a strong pointer to self is captured in a block.
This could lead to retain cycles or unexpected behavior since to avoid retain
cycles one usually uses a local strong pointer or a captured weak pointer instead.

This will happen in one of two cases generally:

One uses weakSelf but forgot to declare it weak first.

Example:

objectivec

__typeof(self) weakSelf = self;
  int (^my_block)(BOOL) = ^(BOOL isTapped) {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    return strongSelf->x;
  };

Action: Replace the first line with __weak __typeof(self) weakSelf = self;.

One is using strongSelf, declared in a block, in another inner block.
The retain cycle is avoided in the outer block because strongSelf is a
local variable of the block. If strongSelf is used in the inner block,
then it's not a local variable anymore, but a captured variable.

Example:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong typeof(self) strongSelf = weakSelf;
    if (strongSelf) {
      int (^my_block)() = ^() {
        int x = strongSelf->x;
        ...
      };
      ...
    }
    ...
  };

In this example, strongSelf is a captured variable of the inner block, and this could cause retain cycles.

Action: Use a new pointer to self local to the inner block. In the example:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong typeof(self) strongSelf = weakSelf;
    if (strongSelf) {
      int (^my_block)() = ^() {
         __typeof(self) innerStrongSelf = weakSelf;
        int x = innerStrongSelf->x;
        ...
      };
      ...
    }
    ...
  };

Or, to improve readability, move the inner block logic into a separate method.

Another solution could be to copy the instance variable that one needs to access inside the inner block to a local variable, and use the local variable instead:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong typeof(self) strongSelf = weakSelf;
    if (strongSelf) {
      int my_x = strongSelf->x;
      int (^my_block)() = ^() {
        int x = my_x;
        ...
      };
      ...
    }
    ...
  };

CHECKERS_ALLOCATES_MEMORY

Category: Perf regression. Reported as "Allocates Memory" by annotation-reachability.

A method annotated with @NoAllocation transitively calls new.

Example:

java

class C implements I {
  @NoAllocation
  void directlyAllocatingMethod() {
    new Object();
  }
}

CHECKERS_ANNOTATION_REACHABILITY_ERROR

Category: User defined property. Reported as "Annotation Reachability Error" by annotation-reachability.

A method annotated with an annotation @A transitively calls a method annotated @B where the combination of annotations is forbidden (for example, @UiThread calling @WorkerThread).

CHECKERS_CALLS_EXPENSIVE_METHOD

Category: Perf regression. Reported as "Expensive Method Called" by annotation-reachability.

A method annotated with @PerformanceCritical transitively calls a method annotated @Expensive.

Example:

java

class C {
  @PerformanceCritical
  void perfCritical() {
    expensive();
  }

  @Expensive
  void expensive() {}
}

CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED

Reported as "Expensive Overrides Unannotated" by annotation-reachability.

A method annotated with @Expensive overrides an un-annotated method.

Example:

java

interface I {
  void foo();
}

class A implements I {
  @Expensive
  public void foo() {}
}

CHECKERS_FRAGMENT_RETAINS_VIEW

Category: Resource leak. Reported as "Fragment Retains View" by fragment-retains-view.

This error type is Android-specific. It fires when a Fragment type fails to
nullify one or more of its declared View fields in onDestroyView. In
performance-sensitive applications, a Fragment should initialize all View's
in onCreateView and nullify them in onDestroyView. If a Fragment is placed
on the back stack and fails to nullify a View in onDestroyView, it will
retain a useless reference to that View that will not be cleaned up until the
Fragment is resumed or destroyed.

Action: Nullify the View in question in onDestroyView.

COMPARED_TO_NULL_AND_DEREFERENCED

Category: Null pointer dereference. Reported as "Compared To Null And Dereferenced" by pulse.

A pointer that has both been compared to null, which suggests that it could be null, but has also been dereferenced without a null check.

CONFIG_GATED

Reported as "Config Gated" by config-gating.

A call site is gated by one or more config flags. Being gated by config X means
that changing the value of config X can be used to turn off the execution of the
reported code.

CONFIG_IMPACT

Category: Perf regression. Reported as "Config Impact" by config-impact-analysis.

Infer reports this issue when an expensive function is called without a config check. The
config is usually a boolean value that enables experimental new features and it is defined per
application/codebase, e.g. gatekeepers. To determine whether a function is expensive or not, the
checker relies on modeled functions that are assumed to be expensive, e.g. string operations,
regular expression match, or DB accesses.

Similar to Cost analysis, this issue type is reported only in
differential mode, i.e. when there are original code and modified one and we can compare Infer's
results on both of them.

For instance, if we have the following code

java

// version1
foo();
if (config_check){
   bar();
}

which is then modified to next

java

// version2
foo();
if (config_check){
   bar();
}
goo(); // added

the analysis would warn the developer that "goo() is a newly added function call and it might
cause an unexpected new behavior". However, if we were to add goo() right after bar(), then
Infer wouldn't warn about it because it is already gated under the config_check.

The analysis is inter-procedural: it can reason about impacts by code changes not only inside a
single procedure, but also the impacts that are propagated by function calls. Thus, if we were to
modify version1 to version3 below by calling goo() in foo(),

java

// version3
void foo(){
   // ....
   goo(); // added
}

then the analysis will report a CONFIG_IMPACT issue on the ungated call site of foo().

Currently, the analysis supports both Objective-C and Java but not C++.

Action: Make sure the ungated code change is semantically correct and harmless in terms of execution
cost. If you are not sure, gate it with a new or pre-existing config.

CONFIG_IMPACT_STRICT

Category: Ungated code. Reported as "Config Impact Strict" by config-impact-analysis.

This is similar to CONFIG_IMPACT issue but the analysis reports all ungated
codes irrespective of whether they are expensive or not.

CONFIG_UNGATED

Reported as "Config Ungated" by config-gating.

A call site is not gated by any config flag. There is no config value that,
if changed, would prevent this code from executing.

CONFIG_USAGE

Reported as "Config Usage" by pulse.

Infer reports this issue when a config value is used as branch condition in a function. The
config is usually a boolean value that enables experimental new features and it is defined per
application/codebase, e.g. gatekeepers.

For instance, if we have the following code

cpp

void foo() {
  if(config_check("my_new_feature")){ ... }
}

then analysis would provide information that "the function foo uses the config my_new_feature as
branch condition".

Note: This type of issue is only for providing semantic information, rather than warning or
reporting actual problem.

CONSTANT_ADDRESS_DEREFERENCE

Reported as "Constant Address Dereference" by pulse.

This is reported when an address at an absolute location, e.g. 1234,
is dereferenced. It is a more general version of the
NULLPTR_DEREFERENCE error type that is
reported when the address is a constant other than zero.

For example, int *p = (int *) 123; *p = 42; generates a CONSTANT_ADDRESS_DEREFERENCE on *p = 42;.

For more information see the NULLPTR_DEREFERENCE issue type.

CONSTANT_ADDRESS_DEREFERENCE_LATENT

Reported as "Constant Address Dereference Latent" by pulse.

A latent CONSTANT_ADDRESS_DEREFERENCE. See the documentation on Pulse latent issues.

CXX_REF_CAPTURED_IN_BLOCK

Category: Memory error. Reported as "C++ Reference Captured in Block" by self-in-block.

This check flags when a C++ reference is captured in an escaping block.
This means that the block will be leaving the current scope, i.e. it is
not annotated with __attribute__((noescape)).

Example:

text

- (void)ref_captured_in_escaping_block_bad:(int&)y {
  dispatch_async(dispatch_get_main_queue(), ^{
    int a = y;
    ...
  });
  ...;
}

This could cause crashes because C++ references are not managed pointers
(like ARC pointers) and so the referent is likely to be gone if the block
dereferences it later.

CXX_STRING_CAPTURED_IN_BLOCK

Category: Memory error. Reported as "C++ String Captured in Block" by self-in-block.

This check flags when an internal pointer of a local variable of type std::string is captured in an escaping block.
This means that the block will be leaving the current scope, i.e. it is
not annotated with __attribute__((noescape)).

Example:

text

std::string fullName;
  const char* c = fullName.c_str();
  dispatch_async(dispatch_get_main_queue(), ^{
    const char* c1 = c;
  });

This could cause crashes because the variable is likely to be freed when the code is executed, leaving the pointer dangling.

DATA_FLOW_TO_SINK

Category: Sensitive data flow. Reported as "Data Flow to Sink" by pulse.

A flow of data was detected to a sink.

DEADLOCK

Category: Concurrency. Reported as "Deadlock" by starvation.

This error is currently reported in Java. A deadlock occurs when two distinct
threads try to acquire two locks in reverse orders. The following code
illustrates a textbook example. Of course, in real deadlocks, the lock
acquisitions may be separated by deeply nested call chains.

java

public void lockAThenB() {
    synchronized(lockA) {
      synchronized(lockB) {
       // do something with both resources
      }
    }
  }

  public void lockBThenA() {
    synchronized(lockB) {
      synchronized(lockA) {
       // do something with both resources
      }
    }
  }

The standard solution to a deadlock is to fix an order of lock acquisition and
adhere to that order in all cases. Another solution may be to shrink the
critical sections (i.e., the code executing under lock) to the minimum required.

Old-style containers such as Vector are synchronized on the object monitor,
which means that deadlocks can occur even without explicit synchronisation on
both threads. For instance:

java

public void lockAThenAddToVector() {
    synchronized(lockA) {
      vector.add(object);
    }
  }

  public void lockVectorThenA() {
    synchronized(vector) {
      synchronized(lockA) {
       // do something with both resources
      }
    }
  }

Infer has support for detecting these deadlocks too.

To suppress reports of deadlocks in a method m() use the
@SuppressLint("DEADLOCK") annotation, as follows:

java

import android.annotation.SuppressLint;

  @SuppressLint("DEADLOCK")
  public void m() {
  ...
  }

DEAD_STORE

Category: Logic error. Reported as "Dead Store" by liveness.

This error is reported in C++. It fires when the value assigned to a variables
is never used (e.g., int i = 1; i = 2; return i;).

EXECUTION_TIME_COMPLEXITY_INCREASE

Reported as "Execution Time Complexity Increase" by cost.

Infer reports this issue when the execution time complexity of a
program increases in degree: e.g. from constant to linear or from
logarithmic to quadratic. This issue type is only reported in
differential mode: i.e when we are comparing the cost analysis results of
two runs of infer on a file. Check out examples in here.

EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD

Reported as "Execution Time Complexity Increase Ui Thread" by cost.

Infer reports this issue when the execution time complexity of the procedure increases in degree and the procedure runs on the UI (main) thread.

Infer considers a method as running on the UI thread whenever:

The method, one of its overrides, its class, or an ancestral class, is
annotated with @UiThread.
The method, or one of its overrides is annotated with @OnEvent, @OnClick,
etc.
The method or its callees call a Litho.ThreadUtils method such as
assertMainThread.

EXECUTION_TIME_UNREACHABLE_AT_EXIT

Reported as "Execution Time Unreachable At Exit" by cost.

This issue type indicates that the program's execution doesn't reach
the exit node (where our analysis computes the final cost of the
procedure). Hence, we cannot compute a static bound for the procedure.

Examples:

java

void exit_unreachable() {
  exit(0); // modeled as unreachable
}

void infeasible_path_unreachable() {
    Preconditions.checkState(false); // like assert false, state pruned to bottom
}

EXPENSIVE_EXECUTION_TIME

Reported as "Expensive Execution Time" by cost.

[EXPERIMENTAL] This warning indicates that the procedure has non-constant and non-top execution cost. By default, this issue type is disabled. To enable it, set enabled=true in costKind.ml.

For instance, a simple example where we report this issue is a function with linear cost:

java

int sum_linear(ArrayList<Integer> list){
 int sum = 0;
 for (Integer el: list){
   sum += el;
 }
 return sum;
}

EXPENSIVE_LOOP_INVARIANT_CALL

Reported as "Expensive Loop Invariant Call" by loop-hoisting.

We report this issue type when a function is loop-invariant and also expensive (i.e. at least has linear complexity as determined by the cost analysis).

java

int incr(int x) {
  return x + 1;
}

// incr will not be hoisted since it is cheap(constant time)
void foo_linear(int size) {
  int x = 10;
  for (int i = 0; i < size; i++) {
    incr(x); // constant call, don't hoist
  }
}

// call to foo_linear will be hoisted since it is expensive(linear in size).
void symbolic_expensive_hoist(int size) {
  for (int i = 0; i < size; i++) {
    foo_linear(size); // hoist
  }
}

GUARDEDBY_VIOLATION

Category: Concurrency. Reported as "GuardedBy Violation" by racerd.

A field annotated with @GuardedBy is being accessed by a call-chain that starts at a non-private method without synchronization.

Example:

java

class C {
  @GuardedBy("this")
  String f;

  void foo(String s) {
    f = s; // unprotected access here
  }
}

Action: Protect the offending access by acquiring the lock indicated by the @GuardedBy(...).

IMPURE_FUNCTION

Reported as "Impure Function" by impurity.

This issue type indicates impure functions. For instance, below functions would be marked as impure:

java

void makeAllZero_impure(ArrayList<Foo> list) {
  Iterator<Foo> listIterator = list.iterator();
  while (listIterator.hasNext()) {
    Foo foo = listIterator.next();
    foo.x = 0;
  }
}

INEFFICIENT_KEYSET_ITERATOR

Category: Perf regression. Reported as "Inefficient Keyset Iterator" by inefficient-keyset-iterator.

This issue is raised when

iterating over a HashMap with keySet() iterator
looking up the key each time

Example:

java

void inefficient_loop_bad(HashMap<String, Integer> testMap) {
 for (String key : testMap.keySet()) {
   Integer value = testMap.get(key); // extra look-up cost
   foo(key, value);
 }
}

Action:

Instead, it is more efficient to iterate over the loop with entrySet which returns key-vaue pairs and gets rid of the hashMap lookup.

java

void efficient_loop_ok(HashMap<String, Integer> testMap) {
  for (Map.Entry<String, Integer> entry : testMap.entrySet()) {
    String key = entry.getKey();
    Integer value = entry.getValue();
    foo(key, value);
  }
}

INFERBO_ALLOC_IS_BIG

Reported as "Alloc Is Big" by bufferoverrun.

malloc is passed a large constant value (>=10^6). For example, int n = 1000000; malloc(n); generates INFERBO_ALLOC_IS_BIG on malloc(n).

Action: Fix the size argument or make sure it is really needed.

INFERBO_ALLOC_IS_NEGATIVE

Reported as "Alloc Is Negative" by bufferoverrun.

malloc is called with a negative size. For example, int n = 3 - 5; malloc(n); generates INFERBO_ALLOC_IS_NEGATIVE on malloc(n).

Action: Fix the size argument.

INFERBO_ALLOC_IS_ZERO

Reported as "Alloc Is Zero" by bufferoverrun.

malloc is called with a zero size. For example, int n = 3 - 3; malloc(n); generates INFERBO_ALLOC_IS_ZERO on malloc(n).

Action: Fix the size argument.

INFERBO_ALLOC_MAY_BE_BIG

Reported as "Alloc May Be Big" by bufferoverrun.

malloc may be called with a large value. For example, int n = b ? 3 : 1000000; malloc(n); generates INFERBO_ALLOC_MAY_BE_BIG on malloc(n).

Action: Fix the size argument or add a bound checking, e.g. if (n < A_SMALL_NUMBER) { malloc(n); }.

INFERBO_ALLOC_MAY_BE_NEGATIVE

Reported as "Alloc May Be Negative" by bufferoverrun.

malloc may be called with a negative value. For example, int n = b ? 3 : -5; malloc(n); generates INFERBO_ALLOC_MAY_BE_NEGATIVE on malloc(n).

Action: Fix the size argument or add a bound checking, e.g. if (n > 0) { malloc(n); }.

INFINITE_EXECUTION_TIME

Reported as "Infinite Execution Time" by cost.

This warning indicates that Infer was not able to determine a static
upper bound on the execution cost of the procedure. By default, this
issue type is disabled.

Example 1: T due to expressivity

For instance, Inferbo's interval analysis is limited to affine
expressions. Hence, we can't statically estimate an upper bound on the
below example and obtain T(unknown) cost:

java

// Expected: square root(x), got T
void square_root_FP(int x) {
 int i = 0;
 while (i * i < x) {
   i++;
 }
}

Example 2: T due to unmodeled calls

Another common case where we get T cost is when Infer cannot statically determine the range of values for loop bounds. For instance,

java

void loop_over_charArray_FP(StringBuilder builder, String input) {
  for (Character c : input.toCharArray()) {}
}

Here, Infer does not have any InferBo models for the range of values returned by String.toCharArray, hence it cannot determine that we will be iterating over a char array in the size of input string.

To teach InferBo about such library calls, they should be semantically modeled in InferBo.

Example 3: T due to calling another T-costed function

Since the analysis is inter-procedural, another example we can have T cost is if at least one of the callees has T cost.

java

// Expected: constant, got T
void call_top_cost_FP() {
 square_root_FP(1); // square_root_FP has Top cost
}

INFINITE_LOOP

Category: Runtime exception. Reported as "Infinite Loop" by pulse.

An infinite loop has been detected. The program won't terminate.

Example of recursive function:

void loop(int x) {
  int y = 1;
  while (x != 3)
    y++;
}

INFINITE_RECURSION

Category: Runtime exception. Reported as "Infinite Recursion" by pulse.

A special case of MUTUAL_RECURSION_CYCLE where we detected that the recursive call is made with the exact same values, which guarantees an infinite recursion.

INTEGER_OVERFLOW_L1

Reported as "Integer Overflow L1" by bufferoverrun.

This is reported when integer overflow occurred by integer operations such as addition, subtraction,
and multiplication. For example, int n = INT_MAX; int m = n + 3; generates a INTEGER_OVERFLOW_L1
on n + 3.

Integer overflows reports fall into several "buckets" corresponding to the expected precision of the
report. The higher the number, the more likely it is to be a false positive.

L1: The most faithful report, when it must be unsafe. For example,
[2147483647,2147483647] + [1,1] in 32-bit signed integer type.
L2: Less faithful report than L1, when it may be unsafe. For example,
[2147483647,2147483647] + [0,1] in 32-bit signed integer type. Note that the integer of RHS
can be 0, which is safe.
L5: The reports that are not included in the above cases.
U5: A binary integer operation is unsafe by unknown values, which are usually from unknown
function calls.

INTEGER_OVERFLOW_L2

Reported as "Integer Overflow L2" by bufferoverrun.

See INTEGER_OVERFLOW_L1

INTEGER_OVERFLOW_L5

Reported as "Integer Overflow L5" by bufferoverrun.

See INTEGER_OVERFLOW_L1

INTEGER_OVERFLOW_U5

Reported as "Integer Overflow U5" by bufferoverrun.

See INTEGER_OVERFLOW_L1

INTERFACE_NOT_THREAD_SAFE

Category: Concurrency. Reported as "Interface Not Thread Safe" by racerd.

This error indicates that you have invoked an interface method not annotated
with @ThreadSafe from a thread-safe context (e.g., code that uses locks or is
marked @ThreadSafe). The fix is to add the @ThreadSafe annotation to the
interface or to the interface method. For background on why these annotations
are needed, see the detailed explanation
here.

INVALID_SIL

Reported as "Invalid Sil" by sil-validation.

The SIL instruction does not conform to the expected subset of instructions
expected for the front-end of the language for the analyzed code.

INVARIANT_CALL

Reported as "Invariant Call" by loop-hoisting.

We report this issue type when a function call is loop-invariant and hoistable, i.e.

the function has no side side effects (pure)
has invariant arguments and result (i.e. have the same value in all loop iterations)
it is guaranteed to execute, i.e. it dominates all loop sources

java

int foo(int x, int y) {
 return x + y;
}


void invariant_hoist(int size) {
    int x = 10;
    int y = 5;
    for (int i = 0; i < size; i++) {
      foo(x, y); // hoistable
    }
  }

IPC_ON_UI_THREAD

Category: Perf regression. Reported as "Ipc On Ui Thread" by starvation.

A blocking Binder IPC call occurs on the UI thread.

LAB_RESOURCE_LEAK

Reported as "Lab Resource Leak" by resource-leak-lab.

Toy issue.

LINEAGE_FLOW

Category: Sensitive data flow. Reported as "Lineage Flow" by lineage.

A Lineage taint flow has been detected from a source to a sink.

LOCKLESS_VIOLATION

Reported as "Lockless Violation" by starvation.

A method implements an interface signature annotated with @Lockless but which transitively acquires a lock.

Example:

java

Interface I {
    @Lockless
    public void no_lock();
}

class C implements I {
  private synchronized do_lock() {}

  public void no_lock() { // this method should not acquire any locks
    do_lock();
  }
}

LOCK_CONSISTENCY_VIOLATION

Category: Concurrency. Reported as "Lock Consistency Violation" by racerd.

This is an error reported on C++ and Objective C classes whenever:

Some class method directly uses locking primitives (not transitively).
It has a public method which writes to some member x while holding a lock.
It has a public method which reads x without holding a lock.

The above may happen through a chain of calls. Above, x may also be a
container (an array, a vector, etc).

Fixing Lock Consistency Violation reports

Avoid the offending access (most often the read). Of course, this may not be
possible.
Use synchronization to protect the read, by using the same lock protecting the
corresponding write.
Make the method doing the read access private. This should silence the
warning, since Infer looks for a pair of non-private methods. Objective-C:
Infer considers a method as private if it's not exported in the header-file
interface.

LOCK_ON_UI_THREAD

Category: Perf regression. Reported as "Lock on UI Thread" by starvation.

A method annoted as being on UIThread acquires a lock. This could be a potential performance issue

Example:

java

class Example {
    @UiThread
    void foo() {
        synchronized(this) {
        }
    }
}

MEMORY_LEAK_C

Category: Resource leak. Reported as "Memory Leak" by pulse.

Memory leak in C

This error type is only reported in C and Objective-C code. In Java we do not
report memory leaks because it is a garbage collected language.

In C, Infer reports memory leaks when objects are created with malloc and not
freed. For example:

void memory_leak_bug () {
    struct Person *p = malloc(sizeof(struct Person));
}

Memory leak in Objective-C

Additionally, in Objective-C, Infer reports memory leaks that happen when
objects from Core Foundation or Core Graphics don't get released.

objectivec

-(void) memory_leak_bug_cf {
    CGPathRef shadowPath = CGPathCreateWithRect(self.inputView.bounds, NULL); //object created and not released.
}

MEMORY_LEAK_CPP

Category: Resource leak. Reported as "Memory Leak" by pulse.

See MEMORY_LEAK_C

MISSING_NULLABILITY_ANNOTATION

Category: Null pointer dereference. Reported as "Missing Nullability Annotation" by swift-objc-nullability.

An Objective-C method that returns a pointer is being called from Swift,
but its declaration carries no nullability annotation (_Nullable or
_Nonnull). Without an annotation Swift's clang importer treats the result
as an Implicitly Unwrapped Optional (T!), so any subsequent use that
assumes non-nil values traps at runtime if the method ever returns nil.

Why this matters

Objective-C uses raw pointers and signals "may be nil" only by convention.
Swift, by contrast, requires nullability to be explicit in the type system:

Objective-C declaration	Swift import	Behaviour on `nil`
`- (NSString *)foo;`	`func foo() -> String!`	implicit unwrap, trap
`- (NSString * _Nonnull)foo;`	`func foo() -> String`	impossible by contract
`- (NSString * _Nullable)foo;`	`func foo() -> String?`	safe; caller must unwrap

The unannotated form is the dangerous one: Swift will silently let you
write api.foo().count even though the underlying call may return nil,
and the trap fires far away from the missing annotation.

Example

objc

// LegacyAPI.h - third-party header, no annotation
@interface LegacyAPI : NSObject
- (NSString *)getOptionalThing;
@end

swift

func bad(api: LegacyAPI) {
  let s = api.getOptionalThing()  // imported as String!
  print(s.count)                  // crashes if getOptionalThing returns nil
}

Infer reports MISSING_NULLABILITY_ANNOTATION on the call to
getOptionalThing.

Preferred fix: annotate the Objective-C header

Edit the declaration to state the contract explicitly. If the method may
return nil, mark it _Nullable; otherwise mark it _Nonnull:

objc

// LegacyAPI.h
@interface LegacyAPI : NSObject
- (NSString * _Nullable)getOptionalThing;
@end

Now Swift imports the result as String? and the compiler forces the
caller to handle the nil case:

swift

func good(api: LegacyAPI) {
  if let s = api.getOptionalThing() {
    print(s.count)
  }
}

For headers that already wrap whole regions in
NS_ASSUME_NONNULL_BEGIN / NS_ASSUME_NONNULL_END, only the exception
needs the explicit _Nullable.

Workaround when you cannot edit the header

If the declaration lives in a third-party framework or a header you do not
own, defend at the Swift call site by casting the result to an Optional
with as?:

swift

func goodWorkaround(api: LegacyAPI) {
  if let s = api.getOptionalThing() as? NSString {
    print(s.length)
  }
}

The as? cast lifts the IUO into a real Optional, and if let /
guard let then forces the nil case to be handled. Infer recognises this
defensive shape (an objc_msgSend whose result feeds a
_bridgeToObjectiveC call in the lowered IR) and stops reporting on the
call.

A bare force-unwrap (api.getOptionalThing()!) is not a fix: it makes
the trap explicit but does not eliminate it, and infer will continue to
report on the call.

MISSING_NULLABILITY_ANNOTATION_PULSE

Category: Null pointer dereference. Reported as "Missing Nullability Annotation" by pulse.

Why this matters

Objective-C uses raw pointers and signals "may be nil" only by convention.
Swift, by contrast, requires nullability to be explicit in the type system:

Objective-C declaration	Swift import	Behaviour on `nil`
`- (NSString *)foo;`	`func foo() -> String!`	implicit unwrap, trap
`- (NSString * _Nonnull)foo;`	`func foo() -> String`	impossible by contract
`- (NSString * _Nullable)foo;`	`func foo() -> String?`	safe; caller must unwrap

Example

objc

// LegacyAPI.h - third-party header, no annotation
@interface LegacyAPI : NSObject
- (NSString *)getOptionalThing;
@end

swift

func bad(api: LegacyAPI) {
  let s = api.getOptionalThing()  // imported as String!
  print(s.count)                  // crashes if getOptionalThing returns nil
}

Infer reports MISSING_NULLABILITY_ANNOTATION on the call to
getOptionalThing.

Preferred fix: annotate the Objective-C header

Edit the declaration to state the contract explicitly. If the method may
return nil, mark it _Nullable; otherwise mark it _Nonnull:

objc

// LegacyAPI.h
@interface LegacyAPI : NSObject
- (NSString * _Nullable)getOptionalThing;
@end

Now Swift imports the result as String? and the compiler forces the
caller to handle the nil case:

swift

func good(api: LegacyAPI) {
  if let s = api.getOptionalThing() {
    print(s.count)
  }
}

For headers that already wrap whole regions in
NS_ASSUME_NONNULL_BEGIN / NS_ASSUME_NONNULL_END, only the exception
needs the explicit _Nullable.

Workaround when you cannot edit the header

If the declaration lives in a third-party framework or a header you do not
own, defend at the Swift call site by casting the result to an Optional
with as?:

swift

func goodWorkaround(api: LegacyAPI) {
  if let s = api.getOptionalThing() as? NSString {
    print(s.length)
  }
}

A bare force-unwrap (api.getOptionalThing()!) is not a fix: it makes
the trap explicit but does not eliminate it, and infer will continue to
report on the call.

MISSING_REQUIRED_PROP

Category: Runtime exception. Reported as "Missing Required Prop" by litho-required-props.

This issues is reported when a required @Prop is missing.

Examples

Assume that the following Litho Component specification is defined as follows where prop1 is optional and prop2 is required.

java

class MyComponentSpec {

  static void onCreate(
      ComponentContext c,
      @Prop(optional = true) String prop1, @Prop int prop2) {
    ...
  }
  ...
}

When we build the corresponding component, we should have all the required props. If we are missing optional props (e..g prop1 below), it is ok.

java

MyComponent.create(c)
    .prop2(8)
    .build();

However, if we are missing a required prop, Infer gives an error below for the missing prop2.

java

MyComponent.create(c)
    .prop1("My prop 1")
    .build();

** Action **

There are two ways to fix this issue.

First, we could add the missing prop2:

java

MyComponent.create(c)
    .prop1("My prop 1")
    .prop2(x) // where x is some integer
    .build();

or alternatively, if the prop2 is not really required, we could change the component spec to reflect that:

java

class MyComponentSpec {

  static void onCreate(
      ComponentContext c,
      @Prop(optional = true) String prop1, @Prop(optional = true) int prop2) {
    ...
  }
  ...
}

MIXED_SELF_WEAKSELF

Category: Resource leak. Reported as "Mixed Self WeakSelf" by self-in-block.

This check reports an issue when an Objective-C block captures both self and weakSelf, a weak pointer to self.
Possibly the developer meant to capture only weakSelf to avoid a retain cycle, but made a typo and used self
instead of strongSelf. In this case, this could cause a retain cycle.

Example:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
      [strongSelf foo];
      int x = self->x; // typo here
    }
    return 0;
  };

Action: Fixing the typo is generally the right course of action.

Limitations: To keep this check simple and intra-procedural, we rely on names to find weakSelf:
we assume that any captured weak pointer whose name contains "self" is a weak reference to self.

MODIFIES_IMMUTABLE

Reported as "Modifies Immutable" by impurity.

This issue type indicates modifications to fields marked as @Immutable. For instance, below function mutateArray would be marked as modifying immutable field testArray:

java

@Immutable int[] testArray = new int[]{0, 1, 2, 4};
  
  int[] getTestArray() {
    return testArray;
  }                
          
  void mutateArray() {
    int[] array = getTestArray();
    array[2] = 7;
  }

MULTIPLE_WEAKSELF

Reported as "Multiple WeakSelf Use" by self-in-block.

This check reports when an Objective-C block uses weakSelf (a weak pointer to self) more than once.
This could lead to unexpected behaviour. Even if weakSelf is not nil in the first use, it could be nil
in the following uses since the object that weakSelf points to could be freed anytime.

Example:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
      [weakSelf foo];
      int x = weakSelf->x;
  };

Action:
One should assign weakSelf to a strong pointer first, and then
use it in the block.

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
      [strongSelf foo];
      int x = strongSelf->x;
    }
    ...
  };

Limitations: To keep this check simple and intra-procedural, we rely on names to find weakSelf:
we assume that any captured weak pointer whose name contains "self" is a weak reference to self.
In contrast, strongSelf is a local variable to the block, so the check supports any name given to
a local strong pointer that has been assigned weakSelf.

MUTUAL_RECURSION_CYCLE

Category: Runtime exception. Reported as "Mutual Recursion Cycle" by pulse.

A recursive call or mutually recursive call has been detected. This does not mean that the program won't terminate, just that the code is recursive. You should double-check if the recursion is intended and if it can lead to non-termination or a stack overflow.

Example of recursive function:

int factorial(int x) {
  if (x > 0) {
    return x * factorial(x-1);
  } else {
    return 1;
  }
}

NIL_BLOCK_CALL

Category: Null pointer dereference. Reported as "Nil Block Call" by pulse.

This check reports when one tries to call an Objective-C block that is nil.
This causes a crash.

Example:

objectivec

-(void) foo:(void (^)())callback {
    callback();
}

-(void) bar {
    [self foo:nil]; //crash
}

Action:

Adding a check for nil before calling the block, or making sure never to call the method foo: with nil.

NIL_BLOCK_CALL_LATENT

Category: Null pointer dereference. Reported as "Nil Block Call Latent" by pulse.

A latent NIL_BLOCK_CALL. See the documentation on Pulse latent issues.

NIL_INSERTION_INTO_COLLECTION

Category: Runtime exception. Reported as "Nil Insertion Into Collection" by pulse.

This checks reports when nil is passed to collections in Objective-C such as arrays and dictionaries. This causes a crash.

Arrays

Adding objects to an array, inserting objects at a given index, or replacing objects at a given index, can all
lead to a crash when the object is nil.

objectivec

[mArray addObject:nil];  //crash

  [mArray insertObject:nil atIndex:0];   //crash

  [mArray replaceObjectAtIndex:0 withObject:nil]; //crash

Dictionaries

Adding a nil value in a dictionary causes a crash. If the concept of nil is required, one can add
[NSNull null] instead.

objectivec

id value = nil;
  [mDict setObject:value forKey:@"somestring"]; //crash

  [mDict setObject:[NSNull null] forKey:@"somestring"]; //ok

Retrieving or removing an object from a dictionary with a nil key also causes a crash:

objectivec

id key = nil;
    mDict[key] = @"somestring"; //crash

   [mDict removeObjectForKey:nil]; //crash

Action:

In all the cases above, when passing nil causes a crash, the solutions are either making sure
that the object passed will never be nil, or adding a check for nil before calling those methods.

NIL_INSERTION_INTO_COLLECTION_LATENT

Category: Runtime exception. Reported as "Nil Insertion Into Collection" by pulse.

A latent NIL_INSERTION_INTO_COLLECTION. See the documentation on Pulse latent issues.

NIL_MESSAGING_TO_NON_POD

Category: Memory error. Reported as "Nil Messaging To Non Pod" by pulse.

In Objective-C, calling a method on nil (or in Objective-C terms, sending a message to nil) does not crash,
it simply returns a falsy value (nil/0/false). However, sending a message that returns
a non-POD C++ type (POD being "Plain Old Data", essentially
anything that cannot be compiled as a C-style struct) to nil causes undefined behaviour.

objectivec

std::shared_ptr<int> callMethodReturnsnonPOD() {
  SomeObject* obj = getObjectOrNil();
  std::shared_ptr<int> d = [obj returnsnonPOD]; // UB
  return d;
}

To fix the above issue, we need to check if obj is
not nil before calling the returnsnonPOD method:

objectivec

std::shared_ptr<int> callMethodReturnsnonPOD(bool b) {
  SomeObject* obj = getObjectOrNil(b);
  if (obj == nil) { return std::make_shared<int>(0); }
  std::shared_ptr<int> d = [obj returnsnonPOD];
  return d;
}

NIL_MESSAGING_TO_NON_POD_LATENT

Category: Memory error. Reported as "Nil Messaging To Non Pod Latent" by pulse.

A latent NIL_MESSAGING_TO_NON_POD. See the documentation on Pulse latent issues.

NO_MATCHING_BRANCH_IN_TRY

Category: Runtime exception. Reported as "No Matching Branch In Try" by pulse.

No matching branch is found when evaluating the of section of a try expression. Corresponds to the {try_clause,V} error in the Erlang runtime.

For example, if we call tail([]) and the full definition of tail is

erlang

tail(X) ->
    try X of
        [_|T] -> {ok,T}
    catch
        _ -> error
    end.

NO_MATCHING_BRANCH_IN_TRY_LATENT

Category: Runtime exception. Reported as "No Matching Branch In Try Latent" by pulse.

A latent NO_MATCHING_BRANCH_IN_TRY. See the documentation on Pulse latent issues.

NO_MATCHING_CASE_CLAUSE

Category: Runtime exception. Reported as "No Matching Case Clause" by pulse.

No matching case clause in Erlang: Reports an error when none of the clauses of a case match the expression. Corresponds to the {case_clause,V} error in the Erlang runtime.

For example, if we call tail([]) and the full definition of tail is

erlang

tail(X) ->
    case X of
        [_|T] -> T
    end.

This error is reported if either the pattern(s) or the guard(s) prevent matching any of the clauses.

NO_MATCHING_CASE_CLAUSE_LATENT

Category: Runtime exception. Reported as "No Matching Case Clause Latent" by pulse.

A latent NO_MATCHING_CASE_CLAUSE. See the documentation on Pulse latent issues.

NO_MATCHING_ELSE_CLAUSE

Category: Runtime exception. Reported as "No Matching Else Clause" by pulse.

No matching else clause in Erlang: Reports an error when none of the clauses of an else match the short-circuit result from maybe body. Corresponds to the {else_clause,V} error in the Erlang runtime.

For example, here the 1 ?= 2 expression does not match and short-circuits to 2, which does not match the single clause under else:

erlang

else_clause_error() ->
    maybe
        1 ?= 2
    else
        1 -> ok
    end.

This error is reported if either the pattern(s) or the guard(s) prevent matching any of the clauses.

NO_MATCHING_ELSE_CLAUSE_LATENT

Category: Runtime exception. Reported as "No Matching Else Clause Latent" by pulse.

A latent NO_MATCHING_ELSE_CLAUSE. See the documentation on Pulse latent issues.

NO_MATCHING_FUNCTION_CLAUSE

Category: Runtime exception. Reported as "No Matching Function Clause" by pulse.

No matching function clause in Erlang: Reports an error when none of the clauses of a function match the arguments of a call. Corresponds to the function_clause error in the Erlang runtime.

For example, if we call tail([]) and the full definition of tail is

erlang

tail([_|Xs]) -> Xs.

This error is reported if either the pattern(s) or the guard(s) prevent matching any of the clauses.

NO_MATCHING_FUNCTION_CLAUSE_LATENT

Category: Runtime exception. Reported as "No Matching Function Clause Latent" by pulse.

A latent NO_MATCHING_FUNCTION_CLAUSE. See the documentation on Pulse latent issues.

NO_MATCH_OF_RHS

Category: Runtime exception. Reported as "No Match Of Rhs" by pulse.

No match of right hand side value in Erlang: Reports an error when the right hand side value of a match expression does not match the pattern on the left hand side. Corresponds to the {badmatch,V} error in the Erlang runtime.

For example, [H|T] = [] gives the error because the left hand side pattern requires at least one element in the list on the right hand side.

NO_MATCH_OF_RHS_LATENT

Category: Runtime exception. Reported as "No Match Of Rhs Latent" by pulse.

A latent NO_MATCH_OF_RHS. See the documentation on Pulse latent issues.

NO_TRUE_BRANCH_IN_IF

Category: Runtime exception. Reported as "No True Branch In If" by pulse.

No true branch when evaluating an if expression in Erlang: Reports an error when none of the branches of an if expression evaluate to true. Corresponds to the if_clause error in the Erlang runtime.

For example, if we call sign(0) and the full definition of sign is

erlang

sign(X) ->
    if
        X > 0 -> positive;
        X < 0 -> negative
    end.

NO_TRUE_BRANCH_IN_IF_LATENT

Category: Runtime exception. Reported as "No True Branch In If Latent" by pulse.

A latent NO_TRUE_BRANCH_IN_IF. See the documentation on Pulse latent issues.

NSSTRING_INTERNAL_PTR_CAPTURED_IN_BLOCK

Category: Memory error. Reported as "NSString Captured in Block" by self-in-block.

Example:

text

std::string fullName;
  const char* c = fullName.c_str();
  dispatch_async(dispatch_get_main_queue(), ^{
    const char* c1 = c;
  });

This could cause crashes because the variable is likely to be freed when the code is executed, leaving the pointer dangling.

NULLPTR_DEREFERENCE

Category: Null pointer dereference. Reported as "Null Dereference" by pulse.

Infer reports null dereference bugs in Java, C, C++, and Objective-C
when it is possible that the null pointer is dereferenced, leading to
a crash.

Null dereference in Java

Many of Infer's reports of potential Null Pointer Exceptions (NPE) come from code of the form

java

p = foo(); // foo() might return null
  stuff();
  p.goo();   // dereferencing p, potential NPE

If you see code of this form, then you have several options.

If you are unsure whether or not foo() will return null, you should
ideally either

Change the code to ensure that foo() can not return null, or
Add a check that p is not null before dereferencing p.

Sometimes, in case (2) it is not obvious what you should do when p
is null. One possibility is to throw an exception, failing early but
explicitly. This can be done using checkNotNull as in the following
code:

java

// code idiom for failing early
import static com.google.common.base.Preconditions.checkNotNull;

  //... intervening code

  p = checkNotNull(foo()); // foo() might return null
  stuff();
  p.goo(); // p cannot be null here

The call checkNotNull(foo()) will never return null: if foo()
returns null then it fails early by throwing a Null Pointer
Exception.

Facebook NOTE: If you are absolutely sure that foo() will not be
null, then if you land your diff this case will no longer be
reported after your diff makes it to trunk.

Null dereference in C

Here is an example of an inter-procedural null dereference bug in C:

struct Person {
  int age;
  int height;
  int weight;
};
int get_age(struct Person *who) {
  return who->age;
}
int null_pointer_interproc() {
  struct Person *joe = 0;
  return get_age(joe);
}

Null dereference in Objective-C

In Objective-C, null dereferences are less common than in Java, but they still
happen and their cause can be hidden. In general, passing a message to nil does
not cause a crash and returns nil, but dereferencing a pointer directly does
cause a crash.

Example:

objectivec

(int) foo:(C*) param {  // passing nil
  D* d = [param bar];   // nil message passing
  return d->fld;        // crash
}
(void) callFoo {
  C* c = [self bar];    // returns nil
  [foo:c];              // crash reported here
}

Action:
Adding a nil check either for param above or for d, or making sure that foo: will never
be called with nil.

Calling a nil block will also cause a crash.
We have a dedicated issue type for this case: Nil Block Call.

Moreover, inserting nil into a collection will cause a crash as well. We
also have a dedicated issue type for this case:
Nil Insertion Into Collection.

NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS

Category: Null pointer dereference. Reported as "Null Dereference" by pulse.

Infer reports null dereference bugs in Java, C, C++, and Objective-C
when it is possible that the null pointer is dereferenced, leading to
a crash.

Null dereference in Java

Many of Infer's reports of potential Null Pointer Exceptions (NPE) come from code of the form

java

p = foo(); // foo() might return null
  stuff();
  p.goo();   // dereferencing p, potential NPE

If you see code of this form, then you have several options.

If you are unsure whether or not foo() will return null, you should
ideally either

Change the code to ensure that foo() can not return null, or
Add a check that p is not null before dereferencing p.

java

// code idiom for failing early
import static com.google.common.base.Preconditions.checkNotNull;

  //... intervening code

  p = checkNotNull(foo()); // foo() might return null
  stuff();
  p.goo(); // p cannot be null here

The call checkNotNull(foo()) will never return null: if foo()
returns null then it fails early by throwing a Null Pointer
Exception.

Facebook NOTE: If you are absolutely sure that foo() will not be
null, then if you land your diff this case will no longer be
reported after your diff makes it to trunk.

Null dereference in C

Here is an example of an inter-procedural null dereference bug in C:

struct Person {
  int age;
  int height;
  int weight;
};
int get_age(struct Person *who) {
  return who->age;
}
int null_pointer_interproc() {
  struct Person *joe = 0;
  return get_age(joe);
}

Null dereference in Objective-C

Example:

objectivec

(int) foo:(C*) param {  // passing nil
  D* d = [param bar];   // nil message passing
  return d->fld;        // crash
}
(void) callFoo {
  C* c = [self bar];    // returns nil
  [foo:c];              // crash reported here
}

Action:
Adding a nil check either for param above or for d, or making sure that foo: will never
be called with nil.

Calling a nil block will also cause a crash.
We have a dedicated issue type for this case: Nil Block Call.

Moreover, inserting nil into a collection will cause a crash as well. We
also have a dedicated issue type for this case:
Nil Insertion Into Collection.

NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS_LATENT

Category: Null pointer dereference. Reported as "Null Dereference" by pulse.

A latent NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS. See the documentation on Pulse latent issues.

NULLPTR_DEREFERENCE_LATENT

Category: Null pointer dereference. Reported as "Null Dereference" by pulse.

A latent NULLPTR_DEREFERENCE. See the documentation on Pulse latent issues.

NULL_ARGUMENT

Category: Runtime exception. Reported as "Null Argument" by pulse.

objc

This issue type indicates `nil` being passed as argument where a non-nil value expected.

#import <Foundation/Foundation.h>

// Test (non-nil) returned values of NSString methods against `nil`
NSString* stringNotNil(NSString* str) {
  if (!str) {
        // ERROR: NSString:stringWithString: expects a non-nil value
	return [NSString stringWithString:nil];
  }
  return str;
}

NULL_ARGUMENT_LATENT

Category: Runtime exception. Reported as "Null Argument Latent" by pulse.

A latent NULL_ARGUMENT. See the documentation on Pulse latent issues.

OPTIONAL_EMPTY_ACCESS

Category: Runtime exception. Reported as "Optional Empty Access" by pulse.

Optional Empty Access warnings are reported when we try to retrieve the value of a folly::Optional when it is empty (i.e. folly::none).

In the following example we get a warning as int_opt might be folly::none and its value is being accessed:

cpp

bool somef(int v);

folly::Optional<int> mightReturnNone(int v) {
   if (somef(v)) {
      return folly::Optional(v);
   }

   return folly::none;
}

int value_no_check() {
  folly::Optional<int> int_opt = mightReturnNone (4);
  return int_opt.value(); // Optional Empty Access warning
}

We do not get the warning anymore if we add a check whether int_opt is not empty:

cpp

int value_check() {
  folly::Optional<int> int_opt = mightReturnNone (4);
  if (int_opt.has_value()) {
     return int_opt.value(); // OK
  }
  return -1;
}

In some cases we know that we have a non-empty value and there is no need to have a check. Consider the following example where Infer does not warn:

cpp

bool somef(int v) {return v > 3;};

folly::Optional<int> mightReturnNone(int v) {
   if (somef(v)) {
      return folly::Optional(v);
   }

   return folly::none;
}

int value_no_check() {
  folly::Optional<int> int_opt = mightReturnNone (4); // cannot be folly::none
  return int_opt.value(); // OK
}

OPTIONAL_EMPTY_ACCESS_LATENT

Category: Runtime exception. Reported as "Optional Empty Access Latent" by pulse.

A latent OPTIONAL_EMPTY_ACCESS. See the documentation on Pulse latent issues.

PULSE_ASSERTION_ERROR

Category: Runtime exception. Reported as "Assertion Error" by pulse.

This error is reported in Java and in Python. It fires when we detect a path that leads to an assertion failure.

PULSE_CANNOT_INSTANTIATE_ABSTRACT_CLASS

Category: Runtime exception. Reported as "Cannot Instantiate Abstract Class" by pulse.

Instantiating an abstract class will lead to Cannot instantiate abstract class error.

hack

abstract class AbstractClass1 {}

class ConcreteClass1 extends AbstractClass1 {}

public static function makeGeneric<T>(classname<T> $cls): void {
    new $cls();
}

<<__ConsistentConstruct>>
abstract class AbstractClass2 {

  public static function makeStatic(): void {
    new static();
  }
}

class ConcreteClass2 extends AbstractClass2 {}

public function badViaGeneric(): void {
    Main::makeGeneric(AbstractClass1::class); // ERROR!
}

public function goodViaGeneric(): void {
  Main::makeGeneric(ConcreteClass1::class);
}

public function badViaStatic(): void {
  AbstractClass2::makeStatic(); // ERROR!
}

public function goodViaStatic(): void {
  ConcreteClass2::makeStatic();
}

PULSE_CONST_REFABLE

Category: Perf regression. Reported as "Const Refable Parameter" by pulse.

This issue is reported when a function parameter is a) passed by value and b) is not modified inside the function. Instead, parameter can be passed by const reference, i.e. converted to a const& so that no unnecessary copy is created at the callsite of the function.

For example,

cpp

#include <vector>

int read_first(const std::vector<int>& vec) { return vec[0]; }

void const_refable(std::vector<int> vec) {
  int first = read_first(vec); // vec is never modified, so the parameter should have type const&
}

PULSE_DICT_MISSING_KEY

Category: Runtime exception. Reported as "Dict Missing Key" by pulse.

This issue is similar to PULSE_UNINITIALIZED_VALUE, but it is to warn
reading a missing key of dictionary in Hack.

For example, in the following code, the dictionary $d has no entry for bye, so reading
$d['bye'] will throw the OutOfBoundsException exception, which is usually unexpected from
developers. We can use a safer function idx instead when keys of a dictionary is unclear.

hack

function simple_bad() : int {
  $d = dict['hi' => 42, 'hello' => 52];
  return $d['bye'];
}

PULSE_DYNAMIC_TYPE_MISMATCH

Category: Runtime exception. Reported as "Dynamic Type Mismatch" by pulse.

This error is reported in Hack. It fires when we detect an operation that is incompatible
with the dynamic type of its arguments.

For example, reading $x['key'] when $x is a vector.

PULSE_READONLY_SHARED_PTR_PARAM

Category: Perf regression. Reported as "Read-only Shared Parameter" by pulse.

This issue is reported when a shared pointer parameter is a) passed by value and b) is used only for reading, rather than lifetime extension. At the callsite, this might cause a potentially expensive unnecessary copy of the shared pointer, especially when many number of threads are sharing it. To avoid this, consider 1) passing the raw pointer instead and 2) use std::shared_ptr::get at callsites.

For example,

cpp

void callee(std::shared_ptr<T> x) {
  // read_T(*x);
}

void caller() {
  callee(shared_ptr);
}

can be changed to

cpp

void callee(T* p) {
  // read_T(*p);
}

void caller() {
  callee(shared_ptr.get());
}

PULSE_REFERENCE_STABILITY

Category: Memory error. Reported as "Reference Stability" by pulse.

The family of maps folly::F14ValueMap, folly::F14VectorMap, and by extension
folly::F14FastMap differs slightly from std::unordered_map as it does not
provide reference stability. When the map resizes such as when reserve is
called or new elements are added, all existing references become invalid and
should not be used.

operator[] is an interesting case as it can easily introduce unsafe code when
used twice in the same expression. Depending on what keys are present and which
order the compiler sequences sub-expressions, an insert via operator[] can
invalidate a reference obtained in the same expression before it's read from.
Typically, those cases can be improved by using other map functions such as
at, find, emplace, or insert_or_assign to increase code quality and
safety.

Examples:

cpp

#include <folly/container/F14Map.h>

void use_reference_after_growth_bad(folly::F14FastMap<int, int>& map) {
  const auto& valueRef = map.at(1);
  map.emplace(13, 71);
  const auto valueCopy = valueRef;
}

void unsafe_expressions_bad(folly::F14FastMap<int, int>& map) {
  // Unsafe expressions in situations where one or both keys are not present.
  map[13] = map[71];
  const auto p = map[13] * map[71];
  const auto q = f(map[13], map[71]);
}

PULSE_RESOURCE_LEAK

Category: Resource leak. Reported as "Resource Leak" by pulse.

See RESOURCE_LEAK

PULSE_TRANSITIVE_ACCESS

Category: Logic error. Reported as "Transitive Access" by pulse.

This issue tracks spurious accesses that are reachable from specific entry functions.

Spurious accesses are specified as specific load/calls.

Entry functions are specified through their enclosing class that must extend a specific
class and should not extend a list of specific classes.

PULSE_UNAWAITED_AWAITABLE

Category: Resource leak. Reported as "Unawaited Awaitable" by pulse.

Awaitable values created by calls to asynchronous methods should eventually be awaited along all codepaths (even if their value is unused). Hence the following is not OK

hack

class A {
  public static async genInt() : Awaitable<int>{
    // typically do something involving IO
  }

  public static async genBad() : Awaitable<void> {
    $_unused = self::genInt(); // ERROR: should have done $_unused = await self::genInt();
    return;
  }
}

Failure to await an Awaitable can lead to non-deterministic amount of the asynchronous call actually being executed, and can also indicate a logical confusion between T and Awaitable<T> that may not be caught by the type-checker.

PULSE_UNFINISHED_BUILDER

Category: Resource leak. Reported as "Unfinished Builder" by pulse.

Classes adhering to builder pattern are usually expected to call a finalizer function at some point to produce final result based on values that were passed to a builder itself. If finalizer function hasn't been called then builder's data won't be consumed in any meaningful way and will just be discarded.

hack

class MyBuilder {
  private int $a = 0;
  private int $b = 0;

  public function setA(int $a): MyBuilder {
    $this->a = $a;
    return $this;
  }

  public function setB(int $b): MyBuilder {
    $this->b = $b;
    return $this;
  }

  public function saveX(): Awaitable<void> {
    // typically do something involving IO
  }
}

class BuilderTester {
  public static function builderUserOK(): void {
    $b = new MyBuilder(0);
    $b->setA(42)->setB(97)->saveX();
  }

  public static function builderUserBad(): void {
    $b = new MyBuilder(0);
    $b->setA(42)->setB(97); // ERROR: saveX hasn't been called so the builder's data is discarded
  }
}

PULSE_UNINITIALIZED_CONST

Category: Runtime exception. Reported as "Uninitialized Const" by pulse.

This issue is similar to PULSE_UNINITIALIZED_VALUE, but it is to detect the uninitialized abstract const value in Hack.

For example, in the following code, the FIELD can be read by the static method get_field.

It is problematic invoking static::FIELD, since it may be resolved to a A::FIELD access, if called from A::get_field(). Because FIELD is abstract in A, it is never assigned a value and the vm will crash. Unfortunately, Hack's type system cannot catch this.
In the B class, FIELD is initialized, thus invoking B::get_field is safe.

hack

abstract class A {
  abstract const string FIELD;
  
  public static function get_field(): string {
    return static::FIELD;
  }
}

function call_get_field_bad(): string {
  return A::get_field();
}

class B extends A {
  const string FIELD = "defined";
}

function call_get_field_ok(): string {
  return B::get_field();
}

PULSE_UNINITIALIZED_METHOD

Category: Runtime exception. Reported as "Uninitialized Method" by pulse.

This issue is similar to PULSE_UNINITIALIZED_CONST, but it is to detect the uninitialized method call in Hack.

For example, in the following code, the static method foo is declared only in the interface and the abstract class. Thus, calling the static method can introduce an unexpected exception or a fatal error, while the type checker does miss the issue.

hack

interface MyInterface {
  public static function foo(): string;
}

abstract class MyAbstractClass {
  public abstract static function foo(): string;
}

function interface_method_static_method_bad(): string {
  // Uncaught exception 'TypehintViolationException'
  $c = MyInterface::class;
  return $c::foo();
}

function abstract_class_static_method_bad(): string {
  // Fatal error: Cannot call abstract method
  $c = MyAbstractClass::class;
  return $c::foo();
}

PULSE_UNINITIALIZED_VALUE

Category: Memory error. Reported as "Uninitialized Value" by pulse.

The code uses a variable that has not been initialized, leading to unpredictable or unintended results.

Using uninitialized values can lead to undefined behaviors possibly resulting in crashes, security failures and invalid results.

This can easily be fixed by assigning all variables to an initial value when declaring them.

This, for example, in C:

struct coordinates {
  int x;
  int y;
};

void foo() {
  struct coordinates c;
  c.x = 42;
  c.y++; // uninitialized value c.y!

  int z;
  if (z == 0) { // uninitialized value z!
    // something
  }
}

PULSE_UNNECESSARY_COPY

Category: Perf regression. Reported as "Unnecessary Copy" by pulse.

This is reported when Infer detects an unnecessary copy of an object via copy constructor where neither the source nor the copied variable are modified before the variable goes out of scope. Rather than the copy, a reference to the source object could be used to save memory.

For example,

cpp

struct A {
  int a;
};

int unnecessary_copy(A& x){
  auto y = x; // calls copy constructor
  return y.a; // y is not modified after copy, hence we could avoid the copy by adding & after auto as below
}

int use_reference_instead(A& x){
  auto& y = x; // copy the ref only
  return y.a;
}

PULSE_UNNECESSARY_COPY_ASSIGNMENT

Category: Perf regression. Reported as "Unnecessary Copy Assignment" by pulse.

See PULSE_UNNECESSARY_COPY.

PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST

Category: Perf regression. Reported as "Unnecessary Copy Assignment from Const" by pulse.

See PULSE_UNNECESSARY_COPY.

PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE

Category: Perf regression. Reported as "Unnecessary Copy Assignment Movable" by pulse.

See PULSE_UNNECESSARY_COPY_MOVABLE.

PULSE_UNNECESSARY_COPY_INTERMEDIATE

Category: Perf regression. Reported as "Unnecessary Copy Intermediate" by pulse.

This is reported when Infer detects an unnecessary temporary copy of an intermediate object where copy is created to be passed down to a function unnecessarily. Instead, the intermediate object should either be moved into the callee or the type of the callee's parameter should be made const &.

A prime example of this occurs when we call a function with a call-by-value parameter as follows:

cpp

void callee(ExpensiveObject obj) {
  // ....
}

void caller() {
  callee(myExpensiveObj); // a copy of myExpensiveObj is created
  // the copy is destroyed right after the call  
}

In this case, when we call callee, under the hood, a copy of the argument myExpensiveObj is created to be passed to the function call. However, the copy might be unnecessary if

callee doesn’t modify its parameter → then we can change its type to const ExpensiveObject&, getting rid of the copy at caller
even if callee might modify the object, if the argument myExpensiveObj is never used later on, we can get rid of the copy by moving it instead: callee(std::move(myExpensiveObj)).

The analysis is careful about suggesting moves blindly though: if the argument myExpensiveObj is of type const & ExpensiveObject then we also recommend that for move to work, const-reference needs to be removed.

PS: We check for other conditions on the argument here: e.g. it should be local to the procedure, as moving a non-local member might cause other memory correctness issues like use-after-move later on.

PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST

Category: Perf regression. Reported as "Unnecessary Copy Intermediate from Const" by pulse.

See PULSE_UNNECESSARY_COPY.

PULSE_UNNECESSARY_COPY_MOVABLE

Category: Perf regression. Reported as "Unnecessary Copy Movable" by pulse.

This is reported when Infer detects an unnecessary copy into a field where

the source is an rvalue-reference
the source is not modified before it goes out of scope or is destroyed.

Note that the copy can be modified since it has the ownership of the object.

Fix: Rather than the copying into the field, the source should be moved into it.

For example,

cpp

struct A {
  std::vector<int> vec;
};

class Test {
  A mem_a;

  void unnecessary_copy(A&& src) {
   mem_a = src;
   // fix is to move as follows
   // mem_a = std::move(src);
  }

};

PULSE_UNNECESSARY_COPY_OPTIONAL

Category: Perf regression. Reported as "Unnecessary Copy to Optional" by pulse.

This is reported when Infer detects an unnecessary copy of an object via optional value
construction where the source is not modified before it goes out of scope. To avoid the copy, we
can move the source object or change the callee's type.

For example,

cpp

void get_optional_value(std::optional<A> x) {}

void pass_non_optional_value(A x) {
  get_optional_value(x);
  // fix is to move as follows
  // get_optional_value(std::move(x));
}

PULSE_UNNECESSARY_COPY_OPTIONAL_CONST

Category: Perf regression. Reported as "Unnecessary Copy to Optional from Const" by pulse.

See PULSE_UNNECESSARY_COPY_OPTIONAL.

PULSE_UNNECESSARY_COPY_RETURN

Category: Perf regression. Reported as "Unnecessary Copy Return" by pulse.

This is similar to PULSE_UNNECESSARY_COPY, but reported when a callee returns a copied value and it is not modified in its caller. We may be able to return const-ref typed value or try std::move to avoid the copy.

For example,

cpp

class MyClass {
  T v;
 public:
  T get() {
    return v; // v is copied here, which is avoidable.
  }
};

void caller(MyClass obj) {
  T x = obj.get();
  std::cout << x; // x is not modified.
}

PULSE_UNNECESSARY_COPY_THRIFT_ASSIGNMENT

Category: Perf regression. Reported as "Unnecessary Copy Assignment into Thrift" by pulse.

This is similar to PULSE_UNNECESSARY_COPY_ASSIGNMENT, but is
reported when copied into thrift fields.

PURE_FUNCTION

Reported as "Pure Function" by purity.

This issue type indicates pure functions. For instance, below functions would be marked as pure:

java

int local_write_pure(int x, int y) {
  int k = x + y;
  k++;
  return k;
}

// no change to outside state, the local allocation is ok.
int local_alloc_pure(ArrayList<Integer> list) {
  ArrayList<Integer> list_new = new ArrayList<Integer>();
  for (Integer el : list) {
    list_new.add(el);
  }
  return list_new.size();
}

However, the following ones would not be pure:

java

void swap_impure(int[] array, int i, int j) {
  int tmp = array[i];
  array[i] = array[j]; // modifying the input array
  array[j] = tmp;
}

int a = 0;
void set_impure(int x, int y) {
  a = x + y; //modifying a global variable
}

REGEX_OP_ON_UI_THREAD

Category: Perf regression. Reported as "Regex Op On Ui Thread" by starvation.

A potentially costly operation on a regular expression occurs on the UI thread.

RETAIN_CYCLE

Category: Resource leak. Reported as "Retain Cycle" by pulse.

A retain cycle is a situation when object A retains object B, and object B
retains object A at the same time. Here is an example:

objectivec

@class Child;
@interface Parent : NSObject {
    Child *child; // Instance variables are implicitly __strong
}
@end
@interface Child : NSObject {
    Parent *parent;
}
@end

You can fix a retain cycle in ARC by using __weak variables or weak properties
for your "back links", i.e. links to direct or indirect parents in an object
hierarchy:

objectivec

@class Child;
@interface Parent : NSObject {
    Child *child;
}
@end
@interface Child : NSObject {
    __weak Parent *parent;
}
@end

RETAIN_CYCLE_NO_WEAK_INFO

Category: Resource leak. Reported as "Retain Cycle No Weak Info" by pulse.

A retain cycle is a situation when object A retains object B, and object B
retains object A at the same time. Here is an example:

objectivec

@class Child;
@interface Parent : NSObject {
    Child *child; // Instance variables are implicitly __strong
}
@end
@interface Child : NSObject {
    Parent *parent;
}
@end

You can fix a retain cycle in ARC by using __weak variables or weak properties
for your "back links", i.e. links to direct or indirect parents in an object
hierarchy:

objectivec

@class Child;
@interface Parent : NSObject {
    Child *child;
}
@end
@interface Child : NSObject {
    __weak Parent *parent;
}
@end

SCOPE_LEAKAGE

Category: Sensitive data flow. Reported as "Scope Leakage" by scope-leakage.

This issue type indicates that a class with scope annotation A stores a field
with whose (dynamic) type (or one of its super types) is annotated with scope
B such that a scope nesting restriction is violated. By "stores", we mean
either directly or transitively.

A configuration is used to list the set of scopes and the must-not-hold relation.

In the following Java example, the set of scopes is Outer and Inner, and the must-not-hold
relation is simply {(Outer, Inner)}:

java

@ScopeType(value = Outer.class)
class ClassOfOuterScope {
  final ClassOfInner c = new ClassOfInner(); // <-- warn here that ClassOfInner would leak.
}

@ScopeType(value = Inner.class)
class ClassOfInner {}

Here is a more detailed description of the analysis.

This analysis operates over Java bytecode. It assumes that types (classes, interfaces, enums,
etc.) may be annotated with so-called scope annotations. The analysis is parameterized by a set
of scopes and a "must-not-hold" relation over pairs of scopes, which it reads from a
configuration file.

The analysis aims to detect violations of the following property: if there exist a path of
fields from object OA to object OB and the type of OA (or one of its super-types) is annotated
with scope SA and the type of OB (or one of its super-types) is annotated with scope SB then
must-not-hold(SA, SB) must be false. Intuitively, the given objects have different scopes that
should not be nested, for example, different intended lifetimes, and a forbidden path from OA to
OB results in OB "leaking" out of the scope SA.

The implementation reads a configuration to determine a list of (scope) "generators" for each
type of scope and a scope class for each type of scope. A generator for a scope type SA is given
by the name of a class and a list of methods where it is understood that any of the methods
listed for the given class returns an object that is known to have scope SA. (This can be seen
as a form of lightweight modeling.) A scope class is the name of the class that represents a
given scope.

SELF_IN_BLOCK_PASSED_TO_INIT

Category: Resource leak. Reported as "Self In Block Passed To Init" by self-in-block.

This check flags when self is captured in a block that is passed to an initialiser method. That
could cause retain cycles if the initialiser code retains the block.

Example:

objectivec

[obj initWithHandler:^() {
    [self foo];
    ...
  }];

Instead it's better to use the weakSelf/strongSelf pattern.

objectivec

__weak __typeof(self) weakSelf = self;
  [obj initWithHandler:^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
        [strongSelf foo];
    }
    ...
  }];

SENSITIVE_DATA_FLOW

Category: Sensitive data flow. Reported as "Sensitive Data Flow" by pulse.

A flow of sensitive data was detected from a source.

STACK_VARIABLE_ADDRESS_ESCAPE

Category: Memory error. Reported as "Stack Variable Address Escape" by pulse.

Reported when an address pointing into the stack of the current
function will escape to its calling context. Such addresses will
become invalid by the time the function actually returns so are
potentially dangerous.

For example, directly returning a pointer to a local variable:

int* foo() {
   int x = 42;
   return &x; // <-- warn here that "&x" will escape
}

STARVATION

Reported as "UI Thread Starvation" by starvation.

This error is reported in Java, and specifically on Android. These reports are
triggered when a method that runs on the UI thread may block, thus potentially
leading to an Application Not Responding error.

Infer considers a method as running on the UI thread whenever:

The method, one of its overrides, its class, or an ancestral class, is
annotated with @UiThread.
The method, or one of its overrides is annotated with @OnEvent, @OnClick,
etc.
The method or its callees call a Litho.ThreadUtils method such as
assertMainThread.

The issue is reported when a method deemed to run on the UI thread

Makes a method call which may block.
Takes a lock, and another thread takes the same lock, and before releasing it,
makes a call that may block.

Calls that may block are considered:

Certain I/O calls.
Two way Binder.transact calls.
Certain OS calls.
Future or AsyncTask calls to get without timeouts, or with too large
timeouts.

To suppress starvation reports in a method m() use the
@SuppressLint("STARVATION") annotation, as follows:

java

import android.annotation.SuppressLint;

  @SuppressLint("STARVATION")
  public void m() {
  ...
  }

To signal to Infer that a method does not perform any blocking calls, despite
appearences, you can use the @NonBlocking annotation:

java

import com.facebook.infer.annotation.NonBlocking;

  @NonBlocking
  public void m() {
  ...
  }

This instructs Infer to filter out any potentially blocking calls in m()
(also, transitively), and thus any other method can expect no starvation reports
due to a call to m(). You will need to set up your class path appropriately to
include the JAR files in infer/annotations for this annotation to work.

STATIC_CONSTRUCTOR_STALL

Category: Concurrency. Reported as "Static Constructor Stall" by static-constructor-stall-checker.

Calling certain methods, for instance dispatch_once, during the static initialization of objects is risky. It could cause deadlocks, because other objects might not have been initialized yet.

STATIC_INITIALIZATION_ORDER_FIASCO

Category: Memory error. Reported as "Static Initialization Order Fiasco" by siof.

This error is reported in C++. It fires when the initialization of a static
variable A, accesses a static variable B from another translation unit
(usually another .cpp file). There are no guarantees whether B has been
already initialized or not at that point.

For more technical definition and techniques to avoid/remediate, see the
FAQ.

STRICT_MODE_VIOLATION

Category: Perf regression. Reported as "Strict Mode Violation" by starvation.

Android has a feature called
strict mode,
which if enabled, will flag the occasions where the main thread makes a call
that results in disk I/O, waiting on a network socket, etc. The analysis
catching starvation errors and deadlocks (the --starvation analysis) has the
ability to statically detect such violations.

To suppress this warning, it's enough to annotate the offending method with
@SuppressLint("STRICT_MODE_VIOLATION").

STRONG_SELF_NOT_CHECKED

Category: Memory error. Reported as "StrongSelf Not Checked" by self-in-block.

This checks reports a potential issue when a block captures weakSelf (a weak pointer to self),
then one assigns this pointer to a local variable strongSelf inside the block and uses this variable
without checking first whether it is nil. The problem here is that the weak pointer could be nil at
the time when the block is executed. So, the correct usage is to first check whether strongSelf is a valid
pointer, and then use it.

Example:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    int y = strongSelf->x;
    ...

Action:
Add a check for nil:

objectivec

__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
      int y = strongSelf->x;
      ...
    }

SWIFT_NPE

Category: Null pointer dereference. Reported as "Swift Null Dereference" by pulse.

Pulse detected a Swift code path that reads from an Optional value known
to be nil. The dereference itself is unsafe -- not the surrounding
type annotation.

The check is Swift-specific and considers an unwrap unsafe only when the
.none case is reachable along some path. Unwraps on values that are
known .some (literal payload, prior if let / guard let binding,
?? default) are silent. Unknown receivers (e.g. the result of an
unmodelled extern call) are also silent.

Force-unwrap of an Optional whose `nil` case is reachable

swift

func unwrapsKnownNil_bad() {
  let x: Int? = nil
  _ = x!                 // SWIFT_NPE: x is known .none here
}

Fix by binding the value before use:

swift

func unwrapsKnownNil_good() {
  let x: Int? = nil
  if let v = x {
    _ = v                 // OK: only reached on the .some branch
  }
}

Or provide a default:

swift

func defaultsToZero_good() {
  let x: Int? = nil
  let _ = x ?? 0          // OK: no force-unwrap
}

Implicitly Unwrapped Optional (`T!`) whose underlying value is `nil`

T! types are written as non-optional but compile to Optional<T> and
trap on access if the value is nil.

swift

func iuoFromBridge_bad(api: LegacyAPI) {
  let s: String! = api.getUnannotatedString()   // ObjC returns nullable
  _ = s.count                                   // SWIFT_NPE on .none
}

Treat the value as a regular Optional and bind it explicitly:

swift

func iuoBound_good(api: LegacyAPI) {
  guard let s = api.getUnannotatedString() else { return }
  _ = s.count                                   // OK
}

If the underlying source can be annotated, mark the ObjC return
_Nonnull (or change the Swift type from T? / T! to T) so the
guarantee shows up in the signature.

`Optional.unsafelyUnwrapped` on a known-`nil` receiver

swift

func unsafelyUnwrappedNil_bad() {
  let x: Int? = nil
  _ = x.unsafelyUnwrapped       // SWIFT_NPE
}

unsafelyUnwrapped has the same trap semantics as ! but skips the
runtime check in optimised builds. Prefer the same fixes as above
(if let, guard let, ??).

SWIFT_NPE_LATENT

Category: Null pointer dereference. Reported as "Swift Null Dereference" by pulse.

A latent SWIFT_NPE. See the documentation on Pulse latent issues.

TAINT_ERROR

Category: Sensitive data flow. Reported as "Taint Error" by pulse.

A taint flow was detected from a source to a sink

THREAD_SAFETY_VIOLATION

Category: Concurrency. Reported as "Thread Safety Violation" by racerd.

This warning indicates a potential data race in Java. The analyser is called
RacerD and this section gives brief but a mostly complete description of its
features. See the RacerD page for more in-depth information and
examples.

Thread-safety: What is a data race

Here a data race is a pair of accesses to the same member field such that:

at least one is a write, and,
at least one occurs without any lock synchronization, and,
the two accesses occur on threads (if known) which can run in parallel.

Thread-safety: Potential fixes

Synchronizing the accesses (using the synchronized keyword, thread-exclusion
such as atomic objects, volatile etc).
Making an offending method private -- this will exclude it from being checked
at the top level, though it will be checked if called by a public method which
may itself, e.g., hold a lock when calling it.
Putting the two accesses on the same thread, e.g., by using @MainThread or
@ThreadConfined.

Thread-safety: Conditions checked before reporting

The class and method are not marked @ThreadSafe(enableChecks = false), and,

The method is declared synchronized, or employs (non-transitively) locking,
or,
The class is not marked @NotThreadSafe, and,
- The class/method is marked @ThreadSafe, or one of the configured synonyms
  in .inferconfig, or,
- A parent class, or an override method are marked with the above annotations.

NB currently RacerD does not take into account @GuardedBy.

Thread-safety: Thread annotations recognized by RacerD

These class and method annotations imply the method is on the main thread:
@MainThread, @UiThread

These method annotations imply the method is on the main thread: @OnBind,
@OnEvent, @OnMount, @OnUnbind, @OnUnmount

Both classes of annotations work through the inheritance tree (i.e. if a parent
class or method is marked with one of these annotations, so is the child class /
method override).

In addition to these, RacerD recognizes many lifecycle methods as necessarily
running on the main thread, eg Fragment.onCreate etc.

Finally, the thread status of being on the main thread propagates backwards
through the call graph (ie if foo calls bar and bar is marked @UiThtread
then foo is automatically considered on the main thread too). Calling
assertMainThread, assertOnUiThread, checkOnMainThread has the same effect.

NB RacerD currently does not recognize @WorkerThread, @BinderThread or
@AnyThread.

Thread-safety: Other annotations and what they do

These annotations can be found at com.facebook.infer.annotation.*.

@Functional This is a method annotation indicating the method always returns
the same value. When a method foo is annotated @Functional, RacerD will
ignore any writes of the return value of foo. For example, in
this.x = foo(), the write to this.x is ignored. The reasoning is that if
the method returns the same value whenever it's called, any data race on
this.x is benign, if that is the only write.
@ThreadConfined This is a class/method/field annotation which takes a single
parameter which can be UI, ANY or a user chosen string. It indicates to
RacerD a thread identifier for the class/method/field. Thus,
@ThreadConfined(UI) is equivalent to @UiThread, and @ThreadConfined(ANY)
is equivalent to not having the annotation at all, for classes and methods.
When this annotation is applied to a field it instructs Infer to assume
(without checking) that all accesses to that field are made on the same thread
(and can, therefore, not race by definition). The intention is that RacerD
uses that to detect exclusion between accesses occurring on the same thread.
However, only the UI thread is supported at this time, and any user provided
value is considered equal to UI.
@VisibleForTesting A method annotation making Infer consider the method as
effectively private. This means it will not be checked for races against
other non-private methods of the class, but only if called by one.
@ReturnsOwnership A method annotation indicating that the method returns a
freshly owned object. Accesses to the returned value will not be considered
for data races, as the object is in-effect unique and not accessible yet from
other threads. The main utility of this annotation is in interfaces, where
Infer cannot look up the implementation and decide for itself.

TOPL_ERROR

Category: User defined property. Reported as "Topl Error" by topl.

A violation of a Topl property (user-specified).
There is an execution path in the code that drives a Topl property from a start state to an error state.

This indicates that the code has a user-defined undesired behavior.

See Topl for an example

TOPL_ERROR_LATENT

Category: User defined property. Reported as "Topl Error Latent" by topl.

A latent TOPL_ERROR. See the documentation on Pulse latent issues.

USE_AFTER_DELETE

Category: Memory error. Reported as "Use After Delete" by pulse.

An address that was invalidated by a call to delete in C++ is dereferenced.

USE_AFTER_DELETE_LATENT

Category: Memory error. Reported as "Use After Delete Latent" by pulse.

A latent USE_AFTER_DELETE. See the documentation on Pulse latent issues.

USE_AFTER_FREE

Category: Memory error. Reported as "Use After Free" by pulse.

An address that was invalidated by a call to free in C is dereferenced.

USE_AFTER_FREE_LATENT

Category: Memory error. Reported as "Use After Free Latent" by pulse.

A latent USE_AFTER_FREE. See the documentation on Pulse latent issues.

USE_AFTER_LIFETIME

Category: Memory error. Reported as "Use After Lifetime" by pulse.

The lifetime of an object has ended but that object is being
accessed. For example, the address of a variable holding a C++ object
is accessed after the variable has gone out of scope:

cpp

void foo() {
     X* p;
     { // new scope
       X x = X();
       p = &x;
     } // x has gone out of scope
     p->method(); // ERROR: you should not access *p after x has gone out of scope
}

USE_AFTER_LIFETIME_LATENT

Category: Memory error. Reported as "Use After Lifetime Latent" by pulse.

A latent USE_AFTER_LIFETIME. See the documentation on Pulse latent issues.

VECTOR_INVALIDATION

Category: Memory error. Reported as "Vector Invalidation" by pulse.

An address pointing into a C++ std::vector might have become
invalid. This can happen when an address is taken into a vector, then
the vector is mutated in a way that might invalidate the address, for
example by adding elements to the vector, which might trigger a
re-allocation of the entire vector contents (thereby invalidating the
pointers into the previous location of the contents).

For example:

cpp

void deref_vector_element_after_push_back_bad(std::vector<int>& vec) {
  int* elt = &vec[1];
  int* y = elt;
  vec.push_back(42); // if the array backing the vector was full already, this
                     // will re-allocate it and copy the previous contents
                     // into the new array, then delete the previous array
  std::cout << *y << "\n"; // bad: y might be invalid
}

VECTOR_INVALIDATION_LATENT

Category: Memory error. Reported as "Vector Invalidation Latent" by pulse.

A latent VECTOR_INVALIDATION. See the documentation on Pulse latent issues.

WEAK_SELF_IN_NO_ESCAPE_BLOCK

Reported as "Weak Self In No Escape Block" by self-in-block.

This check reports when weakSelf (a weak pointer to self) is used in
a block, and this block is passed to a "no escaping" method. This means that
the block passed to that method won't be leaving the current scope, this is
marked with the annotation NS_NOESCAPE.

The issue here is that, because the block is "no escaping", there is no need to use
weakSelf and strongSelf but we can just use self. This has the advantage of
not needing to deal with the added complexity of weak pointers, and it simplifies the
code.

Example:

objectivec

__weak __typeof(self) weakSelf = self;
  [self foo:^() { //foo's first parameter is annotates with `NS_NOESCAPE`
      [weakSelf bar];
  }];

Action:

Replace weakSelf with self:

objectivec

[self foo:^() {
      [self bar];
  }];

Limitations: To keep this check simple and intra-procedural, we rely on names to find weakSelf:
we assume that any captured weak pointer whose name contains "self" is a weak reference to self.

Checker Annotation Reachability (`website/docs/checker-annotation-reachability.md`)

title: "Annotation Reachability"

Activate with --annotation-reachability.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: Yes
Hack: No
Java: Yes
Python: No
Rust: No
Swift: Experimental

List of Issue Types

The following issue types are reported by this checker:

Checker Bufferoverrun (`website/docs/checker-bufferoverrun.md`)

title: "Buffer Overrun Analysis (InferBO)"

InferBO is a detector for out-of-bounds array accesses.

***DEPRECATED*** Use Pulse instead.

Activate with --bufferoverrun.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

You can read about its origins in this blog post.

List of Issue Types

The following issue types are reported by this checker:

Checker Config Gating (`website/docs/checker-config-gating.md`)

title: "Config Gating"

Determines which config flags gate the execution of each line of code.

Activate with --config-gating.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: No
Hack: No
Java: Experimental
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

Checker Config Impact Analysis (`website/docs/checker-config-impact-analysis.md`)

title: "Config Impact Analysis"

[EXPERIMENTAL] Collects function that are called without config checks.

Activate with --config-impact-analysis.

Supported languages:

C/C++/ObjC: Experimental
C#/.Net: No
Erlang: No
Hack: No
Java: Experimental
Python: No
Rust: No
Swift: No

This checker collects functions whose execution isn't gated by certain pre-defined gating functions. The set of gating functions is hardcoded and empty by default for now, so to use this checker, please modify the code directly in FbGKInteraction.ml.

List of Issue Types

The following issue types are reported by this checker:

Checker Cost (`website/docs/checker-cost.md`)

title: "Cost: Complexity Analysis"

Computes the asymptotic complexity of functions with respect to execution cost or other user defined resources. Can be used to detect changes in the complexity with infer reportdiff.

Activate with --cost.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: Experimental
Java: Yes
Python: No
Rust: No
Swift: No

Cost analysis statically estimates an upper bound on the worst-case execution cost of a program (WCET). This page gives an overview of how the analysis works for Java code. The analyser also has limited support for C/C++ and Objective-C.

To run the analysis, you can use run infer --cost (which will run cost analysis along with other
analyses that are run by default) or infer --cost-only (which will only run cost analysis).

For example, the command infer --cost-only -- javac File.java will run
cost analysis on File.java.

How the analysis works

The analysis computes symbolic upper bounds on the resource usage of programs—-execution cost being the main resource we consider. These costs are expressed in terms of polynomials describing the asymptotic complexity of procedures with respect to their input sizes. The main input of the analysis is the source file which is then translated to an intermediate language along with the control-flow graph of the program. The analysis then operates on this intermediate language in several phases:

1. a numerical value analysis based on InferBo computes value ranges for instructions accessing memory
1. a loop bound analysis determines upper bounds for the number of iterations of loops and generates constraints for nodes in the control-flow graph
1. a constraint solving step resolves the constraints generated in the second step and computes an upper bound on the execution cost.

Most ideas behind this analysis are based on Stefan Bydge's PhD thesis Static WCET Analysis based on Abstract Interpretation and Counting of Elements.

The analysis computes two things for each node in the CFG:

the cost of its instructions, i.e. how much one execution of this node costs,
how many times it can be executed (part 2 above)

The total cost of the node is the scalar product of these two vectors. Then, these are passed to a constraint solver (part 3 above) that computes the execution cost of the procedure based on the incoming/outgoing edges.

The results of the analysis are written into costs-report.json where for each procedure, we record the actual polynomial (for the execution cost) along with the degree of the polynomial, the procedure name, line number etc.

Types of resources/costs

Although the analysis was initially designed to reason about the execution cost, it is not limited to inferring bounds for just execution cost. In order to statically detect regressions in other types of resource usage, we have generalized the analysis to account costs for different types of resources such as Objective-C's autorelease pool size or memory allocations.

Currently, there are three types of resources/costs the analysis operates on:

1. execution cost
1. allocation cost
1. autoreleasepool size

For 1), the analysis assumes a simple sequential model with an abstract cost semantics: each primitive instruction in the intermediate language (SIL) is assumed to incur a unit execution cost.

For 2), the analysis only incurs costs for primitive operations that allocate memory (e.g. new). This is in experimental mode and hence the results are not written into costs-report.json.

For 3), the analysis incurs a cost when objects are added to Objective-C's @autoreleasepool. This usually happens in two cases: 1) when autorelease is called explicitly in non-ARC compiled code and 2) when an (autoreleased) object pointer is returned from non-ARC compiled callee to ARC compiled caller, and vice-versa.

Examples (execution cost)

For instance, assume that we had the following program:

java

void loop(ArrayList<Integer> list){
  for (int i = 0; i <= list.size(); i++){
  }
}

Infer statically infers a polynomial (e.g. 8 · |list|+16) for the execution cost of this program by giving each instruction in Infer's intermediate language a symbolic cost (where |...| refers to the length of a list). Here---overlooking the actual constants---the analysis infers that this program’s asymptotic complexity is O(|list|), that is loop is linear in the size of its input list. Then, at diff time, if a developer modifies this code to,

java

void loop(ArrayList<Integer> list){
  for (int i = 0; i <= list.size(); i++){
    foo(i); // newly added function call
  }
}

where foo has a linear cost in its parameter, then Infer automatically detects that the complexity of loop has increased from O(|list|) to O(|list|^2) and then reports an EXECUTION_TIME_COMPLEXITY_INCREASE issue.

Differential mode

Unlike other Infer analyses (which on reports found issues/bugs in report.json when running infer once), cost analysis also has a special mode that reports an issue for differential analysis (i.e. when comparing the analysis results on the original and the modified files). For each procedure, costs-report.json includes the actual polynomial (for the execution cost) along with the degree of the polynomial, the procedure name, line number etc. Then, in the differential mode, these costs-report.json files are compared.

Differential cost analysis in action:

first run infer's cost analysis on File.java and copy inter-out/costs-report.json to previous-costs-report.json (Note that the file should be copied outside the result directory because the directory will be removed in the second infer run.)
modify File.java as shown above
re-run infer on File.java and copy infer-out/costs-report.json to current-costs-report.json
run infer reportdiff --costs-current current-costs-report.json --costs-previous previous-costs-report.json.
Inspect infer-out/differential/introduced.json to see the newly found complexity increase issue(s).

Limitations

There are a number of known limitations to the design of the static cost analysis:

InferBo 's intervals are limited to affine expressions, not full-blown polynomials. Hence, we can not automatically infer bounds involving square roots.
We do not handle recursion.
If the execution cost of a program depends on an unknown call (e.g. due to iterating over an unmodeled library call), we can't compute a static upper bound and return T (unknown cost). See INFINITE_EXECUTION_COST for details.

List of Issue Types

The following issue types are reported by this checker:

Checker Fragment Retains View (`website/docs/checker-fragment-retains-view.md`)

title: "Fragment Retains View"

Detects when Android fragments are not explicitly nullified before becoming unreachable.

Activate with --fragment-retains-view.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

CHECKERS_FRAGMENT_RETAINS_VIEW

Checker Impurity (`website/docs/checker-impurity.md`)

title: "Impurity"

Detects functions with potential side-effects. Same as "purity", but implemented on top of Pulse.

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Activate with --impurity.

Supported languages:

C/C++/ObjC: Experimental
C#/.Net: No
Erlang: No
Hack: Experimental
Java: Experimental
Python: No
Rust: No
Swift: No

This is an experimental inter-procedural analysis that detects impure functions. It is meant to be an improvement over the purity analysis with a negation on the issue types. For each function, impurity analysis keeps track of not only the impurity of the function but also some additional information such as which parameters/globals the function modifies. It models functions with no summary/model as impure. The analysis relies on Pulse summaries to determine impurity.

List of Issue Types

The following issue types are reported by this checker:

Checker Inefficient Keyset Iterator (`website/docs/checker-inefficient-keyset-iterator.md`)

title: "Inefficient keySet Iterator"

Check for inefficient uses of iterators that iterate on keys then lookup their values, instead of iterating on key-value pairs directly.

Activate with --inefficient-keyset-iterator.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

INEFFICIENT_KEYSET_ITERATOR

Checker Lineage (`website/docs/checker-lineage.md`)

title: "Lineage"

Computes a dataflow graph

Activate with --lineage.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: Yes
Hack: No
Java: No
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

LINEAGE_FLOW

Checker Litho Required Props (`website/docs/checker-litho-required-props.md`)

title: "Litho \"Required Props\""

Checks that all non-optional @Props have been specified when constructing Litho components.

Activate with --litho-required-props.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

This analysis checks that all non-optional @Prop`s have been specified when constructing Litho components. This is a Litho specific checker.

What are required Props?

In a nutshell, a Litho Component is essentially a class that defines immutable inputs, called prop (annotated with @Prop) in component hierarchy methods. For each Component there is a corresponding spec class which defines the required props:. E.g:

java

class MyComponentSpec {

  static void onCreate(
      ComponentContext c,
      @Prop(optional = true) String prop1, @Prop int prop2) {
    ...
  }
  ...
}

MyComponentSpec defines two props: a String prop called prop1 and an int prop named prop2. For each prop defined on the spec, the annotation processor creates a builder pattern method that has the same name as the prop.

Developers pass down values for these props by calling the appropriate methods:

java

MyComponent.create(c)
    .prop1("My prop 1")
    .prop2(256)
    .build();

If the required props are not called, then annotation processor throws an exception in run time. This is really bad and that's where this checker comes into play to detect such cases statically.

Note that, the functions create() and build() could be defined in different methods and there could be various function calls, aliasing, and control flow patterns in between. Hence, this checker is inter-procedural.

Check out the examples defined in the issue type MISSING_REQUIRED_PROP.

List of Issue Types

The following issue types are reported by this checker:

MISSING_REQUIRED_PROP

Checker Liveness (`website/docs/checker-liveness.md`)

title: "Liveness"

Detection of dead stores and unused variables.

Activate with --liveness.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: No
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

DEAD_STORE

Checker Loop Hoisting (`website/docs/checker-loop-hoisting.md`)

title: "Loop Hoisting"

Detect opportunities to hoist function calls that are invariant outside of loop bodies for efficiency.

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Activate with --loop-hoisting.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

This checker detects opportunities to hoist function calls that are invariant to outside of loop bodies. The hoisting analysis relies on purity analysis to determine whether a function is pure or not.

It has an additional mode that reports loop-invariant functions that are expensive (i.e. at least linear). This is enabled by the flag --hoisting-report-only-expensive.

List of Issue Types

The following issue types are reported by this checker:

Checker Parameter Not Null Checked (`website/docs/checker-parameter-not-null-checked.md`)

title: "Parameter Not Null Checked"

An Objective-C-specific analysis to detect when a block parameter is used before being checked for null first.

Activate with --parameter-not-null-checked.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: No
Python: No
Rust: No
Swift: No

This checker checks that an Objective-C block that is passed as a parameter
to a function or method is checked for nil before it's being executed.

List of Issue Types

The following issue types are reported by this checker:

BLOCK_PARAMETER_NOT_NULL_CHECKED

Checker Pulse (`website/docs/checker-pulse.md`)

title: "Pulse"

General-purpose memory and value analysis engine.

Activate with --pulse.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: Experimental
Hack: Yes
Java: Yes
Python: No
Rust: Experimental
Swift: No

What is Infer:Pulse?

Pulse is an interprocedural memory safety analysis. Pulse can detect, for instance, Null dereferences in Java. Errors are only reported when all conditions on the erroneous path are true regardless of input. An example of a Null dereference found by Pulse is given below.

java

class Person {
    Person emergencyContact;
    String address;

    Person getEmergencyContact() {
        return this.emergencyContact;
    }
}

class Registry {
    void create() {
        Person p = new Person();
        Person c = p.getEmergencyContact();
        // Null dereference here
        System.out.println(c.address);
    }

    void printContact(Person p) {
        // No null dereference, as we don't know anything about `p`
        System.out.println(p.getEmergencyContact().address);
    }
}

How to run pulse for Java:

bash

infer run --pulse -- javac Test.java

Pulse reports a Null dereference on this file on create(), as it tries to access the field address of object c, and c has value null. In contrast, Pulse gives no report for printContact(Person p), as we cannot be sure that p.getEmergencyContact() will return null. But, thanks to the fact that the analysis is inter-procedural, Pulse will report a Null dereference on calls to printContact(p) when it detects that p is null.

Latent Issues

When an error can occur only on some values of the parameters of the current function, Pulse does not report an issue. Such issues are called latent. But, if Pulse then sees a call site at which all the conditions for the error are satisfied then the error becomes manifest and is reported. This example (in C) illustrates how latent issues are created and then reported when they become manifest:

// for more realism, imagine that this function does other things as well
void set_to_null_if_positive(int n, int** p) {
  if (n > 0) {
    *p = NULL;
  }
}

void latent_null_dereference(int n, int* p) {
  set_to_null_if_positive(n, &p);
  *p = 42; // NULL dereference! but only if n > 0 so no report yet
}

void manifest_error(int *p) {
  // no way to avoid the bug here => Pulse reports an error
  latent_null_dereference(1, p);
}

Unknown Functions

In order to avoid false positives, Pulse makes optimistic assumptions about calls to unknown functions. Unknown functions (or unknown methods) are functions for which Infer didn't find any code. For example, it could be because the function belongs to a third-party library and we know only its signature, or because a function is made through a function pointer that Pulse wasn't able to resolve to a concrete function. In either case, Pulse will scramble the parts of the state reachable from the parameters of the call. In general, this helps avoid false positives but note that this may cause false negatives as well as false positives:

void unknown(int* p); // third-party code that does [*p = 5]
                      // Infer doesn't have access to that code

void false_negative() {
  int* x = (int*) malloc(sizeof(int));
  if (x) {
    // unknown call to x makes Pulse forget that x was allocated, in case it frees x
    unknown(x);
  }
} // no memory leak reported: false negative!

void false_positive(int *x) {
  unknown(x); // this sets *x to 5
  if (x != 5) {
    // unreachable
    int* p = NULL;
    *p = 42; // false positive reported here
  }
}

You can check if a given function called any unknown functions by inspecting its Pulse summary. For example, for the code above:

console

$ infer --pulse-only -- clang -c unknown_code.c
  No issues found
$ infer debug --procedures --procedures-filter 'false_negative' --procedures-summary
...
    skipped_calls={ unknown -> call to skipped function occurs here }

Pulse x Nullsafe

Nullsafe is a type checker for @Nullable annotations for Java. Classes following the Nullsafe discipline are annotated with @Nullsafe.

Consider the classes Person and Registry from the previous example. Assuming that class Person is annotated with @Nullsafe. In this case, we also annotate getEmergencyContact() with @Nullable, to make explicit that this method can return the null value. There is still the risk that classes depending on Person have Null dereferences. In this case, Pulse would report a Null dereference on Registry. It could also be the case that class Registry is annotated with @Nullsafe. By default Pulse reports on @Nullsafe files too, see the --pulse-nullsafe-report-npe option (Facebook-specific: Pulse does not report on @Nullsafe files).

java

@Nullsafe(Nullsafe.Mode.LOCAL)
class Person {
    Person emergencyContact;
    String address;

    @Nullable Person getEmergencyContact() {
        return this.emergencyContact;
    }
}

class Registry {
    ... // Pulse reports here
}

List of Issue Types

The following issue types are reported by this checker:

Checker Purity (`website/docs/checker-purity.md`)

title: "Purity"

Detects pure (side-effect-free) functions. A different implementation of "impurity".

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Activate with --purity.

Supported languages:

C/C++/ObjC: Experimental
C#/.Net: No
Erlang: No
Hack: No
Java: Experimental
Python: No
Rust: No
Swift: No

This is an experimental inter-procedural analysis that detects pure (side-effect free) functions. For each function, purity analysis keeps track of not only the purity of the function but also some additional information such as whether the function modifies a global variable or which of the parameters are modified. It models functions with no summary/model as modifying the global state (hence impure).

If the function is pure (i.e. doesn't modify any global state or its parameters and doesn't call any unknown functions), then it reports an PURE_FUNCTION issue.

Weaknesses

There are two issues with the existing purity analysis:

In order to detect which parameters are modified, we need an alias analysis which is difficult to get right.
Just keeping track of modified arguments doesn't suffice.

Too see the issue with the first point, consider the following simple program:

java

void foo(Foo a){
  Foo b = a;
  b.x = 10; 
}

in order to determine that foo is impure, we need to know that the write to b's field is actually changing the function parameter a, i.e. we need to check if b is aliasing a. This is known as alias analysis and is hard to get right in a scalable manner. When this analysis was being developed, Infer didn't have a unified alias analysis and using biabduction seemed like a too daunting task at the time. Hence, we relied on InferBo's aliasing mechanism which was easy to invoke and integrate with. However, InferBo's aliasing analysis is far from perfect and causes issues for purity.
To see the issue with the second point, consider the following program:

java

boolean contains(Integer i, ArrayList<Integer> list){
  Iterator<Integer> listIterator = list.iterator();
  while(listIterator.hasNext()) {
    Integer el = listIterator.next();
    if (i.equals(el)){
      return true;
    }
  }
  return false;
 }

The existing purity analysis concludes that the above function contains is impure because it calls an impure function next() which modifies the iterator (hence it thinks it also modifies the list). However, notice that contains doesn't have an observable side-effect: list.iterator() returns a new object, hasNext() and equals() are pure, and next() only modifies the fields of the fresh object listIterator. Therefore, contains should be considered as pure.

To alleviate this problem, we have developed an Impurity analysis which uses pulse which can successfully analyze this program as pure \o/

The analysis is used by:

Loop-hoisting analysis which identifies loop-invariant function calls, i.e. functions that are pure and have loop-invariant arguments.
Cost analysis which identifies control variables in the loop that affect how many times a loop is executed. In this computation, we need to prune control variables that do not affect how many times a loop is executed. In this pruning step, we need to compute loop-invariant variables (which requires the above analysis).

List of Issue Types

The following issue types are reported by this checker:

PURE_FUNCTION

Checker Racerd (`website/docs/checker-racerd.md`)

title: "RacerD"

Thread safety analysis.

Activate with --racerd.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: Yes
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

RacerD finds data races in your C++/Objective C and Java code. This page gives a more in-depth
explanation of how the analysis works for Java code, but may be less complete than the
Thread Safety Violation bug description page.
For information on C++ and Objective C, see the
Lock Consistency violation page.

To run the analysis, you can use plain infer (to run RacerD along with other
analyses that are run by default) or infer --racerd-only (to run only RacerD).

For example, the command infer --racerd-only -- javac File.java will run
RacerD on File.java.

Background

RacerD statically analyzes Java code to detect potential concurrency bugs. This
analysis does not attempt to prove the absence of concurrency issues, rather, it
searches for a high-confidence class of data races. At the moment RacerD
concentrates on race conditions between methods in a class that is itself
intended to be thread safe. A race condition occurs when there are two
concurrent accesses to a class member variable that are not separated by mutual
exclusion, and at least one of the accesses is a write. Mutual exclusion can be
ensured by synchronization primitives such as locks, or by knowledge that both
accesses occur on the same thread.

Triggering the analysis

RacerD doesn't try to check all code for concurrency issues; it only looks at
code that it believes can run in a concurrent context. There are two signals
that RacerD looks for: (1) Explicitly annotating a class/method with
@ThreadSafe and (2) using a lock via the synchronized keyword. In both
cases, RacerD will look for concurrency issues in the code containing the signal
and all of its dependencies. In particular, it will report races between any
non-private methods of the same class that can perform conflicting accesses.
Annotating a class/interface with @ThreadSafe also triggers checking for all
of the subclasses of the class/implementations of the interface.

Warnings

Let's take a look at the different types of concurrency issues that RacerD
flags. Two of the warning types are data races (Unprotected write and
Read/write race), and the third warning type encourages adding @ThreadSafe
annotations to interfaces to trigger additional checking.

Unprotected write

RacerD will report an unprotected write when one or more writes can run in
parallel without synchronization. These come in two flavors: (1) a self-race (a
write-write race that occurs due to a method running in parallel with itself)
and (2) two conflicting writes to the same location. Here's an example of the
self-race flavor:

text

@ThreadSafe
public class Dinner {
  private int mTemperature;

  public void makeDinner() {
    boilWater();
  }

  private void boilWater() {
    mTemperature = 100; // unprotected write.
  }
}

The class Dinner will generate the following report on the public method
makeDinner():

There may be a Thread Safety Violation: makeDinner() indirectly writes to mTemperature outside of synchronization.

This warning can be fixed by synchronizing the access to mTemperature, making
mTemperature volatile, marking makeDinner as @VisibleForTesting, or
suppressing the warning by annotating the Dinner class or makeDinner method
with @ThreadSafe(enableChecks = false).

Read/Write Race

We sometimes need to protect read accesses as well as writes. Consider the
following class with unsynchronized methods.

text

@ThreadSafe
public class Account {

  int mBalance = 0;

  public void deposit(int amount) {
    if (amount > 0) {
      mBalance += amount;
    }
  }

  public int withdraw(int amount){
    if (amount >= 0 && mBalance - amount >= 0) {
      mBalance -= amount;
      return mBalance;
    } else {
      return 0;
    }
  }
}

If you run the withdraw() method in parallel with itself or with deposit()
you can get unexpected results here. For instance, if the stored balance is 11
and you run withdraw(10) in parallel with itself you can get a negative
balance. Furthermore, if you synchronize only the write statement
mBalance -= amount, then you can still get this bad result. The reason is that
there is a read/write race between the boolean condition
mBalance - amount >= 0 and the writes. RacerD will duly warn

Read/Write race. Public method int Account.withdraw(int) reads from field Account.mBalance. Potentially races with writes in methods void Account.deposit(int), int Account.withdraw(int)

on the line with this boolean condition.

A solution to the threading problem here is to make both methods synchronized
to wrap both read and write accesses, or to use an AtomicInteger for
mBalance rather than an ordinary int.

Interface not thread-safe

In the following code, RacerD will report an Interface not thread-safe warning
on the call to i.bar():

text

interface I {
  void bar();
}

@ThreadSafe
class C {
  void foo(I i) {
    i.bar(); // RacerD warns here
  }
}

The way to fix this warning is to add a @ThreadSafe annotation to the
interface I, which will enforce the thread-safety of each of the
implementations of I.

You might wonder why it's necessary to annotate I -- can't RacerD just look at
all the implementations of i at the call site for bar? Although this is a
fine idea in principle, it's a bad idea in practice due to a (a) separate
compilation and (b) our diff-based deployment model. In the example above, the
compiler doesn't have to know about all implementations (or indeed, any
implementations) of I at the time it compiles this code, so there's no
guarantee that RacerD will know about or be able to check all implementations of
I. That's (a). For (b), say that we check that all implementations of I are
thread-safe at the time this code is written, but we don't add the annotation.
If someone else comes along and adds a new implementation of I that is not
thread-safe, RacerD will have no way of knowing that this will cause a potential
bug in foo. But if I is annotated, RacerD will enforce that all new
implementations of I are thread-safe, and foo will remain bug-free.

Annotations to help RacerD understand your code

Getting started with RacerD doesn't require any annotations at all -- RacerD
will look at your usage of locks and figure out what data is not guarded
consistently. But increasing the coverage and signal-to-noise ratio may require
adding @ThreadSafe annotations along with some of the other annotations
described below. Most of annotations described below can be used via the Maven
Central package available
here.

`@ThreadConfined`

The intuitive idea of thread-safety is that a class is impervious to concurrency
issues for all concurrent contexts, even those that have not been written yet
(it is future-proof). RacerD implements this by naively assuming that any method
can potentially be called on any thread. You may determine, however, that an
object, method, or field is only ever accessed on a single thread during program
execution. Annotating such elements with @ThreadConfined informs RacerD of
this restriction. Note that a thread-confined method cannot race with itself but
it can still race with other methods.

text

List mCache;

@ThreadConfined(UI)
void prepareCache() {
  // populate the cache
  mCache.add(...);
  // post cache cleanup task to run later
  mUIExecutor.execute(new Runnable() {
    @ThreadConfined(UI)
    public void run() {
      mCache.clear();
    }
  });
}

In this example, both prepareCache and run touch mCache. But there's no
possibility of a race between the two methods because both of them will run
sequentially on the UI thread. Adding a @ThreadConfined(UI) or @UiThread
annotation to these methods will stop it from warning that there is a race on
mCache. We could also choose to add a @ThreadConfined annotation to mCache
itself.

`@Functional`

Not all races are bugs; a race can be benign. Consider the following:

text

@Functional Boolean askNetworkIfShouldShowFeature();

private Boolean mShouldShowFeature;

@ThreadSafe boolean shouldShowFeature() {
  if (mShouldShowFeature == null) {
    mShouldShowFeature = askNetworkIfShouldShowFeature();
  }
  return mShouldShowFeature;
}

This code caches the result of an expensive network call that checks whether the
current user should be shown an experimental feature. This code looks racy, and
indeed it is: if two threads execute shouldShowFeature() at the same time, one
may read mShouldShowFeature at the same time the other is writing it.

However, this is actually a benign race that the programmer intentionally
allows for performance reasons. The reason this code is safe is that the
programmer knows that askNetworkIfShouldShowFeature() will always return the
same value in the same run of the app. Adding synchronization would remove the
race, but acquiring/releasing locks and lock contention would potentially slow
down every call to shouldShowFeature(). The benign race approach makes every
call after the first fast without changing the safety of the code.

RacerD will report a race on this code by default, but adding the
@Functional annotation to askNetworkIfShouldShowFeature() informs RacerD that
the function is always expected to return the same value. This assumption allows
RacerD to understand that this particular code is safe, though it will still
(correctly) warn if mShouldShowFeature is read/written elsewhere.

Be sure not to use the @Functional pattern for singleton instantiation, as
it's possible the "singleton" can be constructed more than once.

text

public class MySingleton {
  private static sInstance;

  // Not @Functional
  public MySingleton getInstance() {
    if (sInstance == null) {
      // Different threads may construct their own instances.
      sInstance == new MySingleton();
    }
    return sInstance;
  }
}

`@ReturnsOwnership`

RacerD does not warn on unprotected writes to owned objects. An object is
owned if it has been freshly allocated in the current thread and has not escaped
to another thread. RacerDf automatically tracks ownership in most cases, but it
needs help with abstract and interface methods that return ownership:

text

@ThreadSafe
public interface Car {
  @ReturnsOwnership abstract Car buyCar();

  void carsStuff() {
    Car myCar = new Car();
    myCar.wheels = 4; // RacerD won't warn here because it knows myCar is owned
    Car otherCar = buyCar();
    otherCar.wheels = 3; // RacerD would normally warn here, but won't because of the `@ReturnsOwnership` annotation
  }
}

`@VisibleForTesting`

RacerD reports races between any two non-private methods of a class that may
run in a concurrent context. Sometimes, a RacerD report may be false because one
of the methods cannot actually be called from outside the current class. One fix
is making the method private to enforce this, but this might break unit tests
that need to call the method in order to test it. In this case, the
@VisibleForTesting annotation will allow RacerD to consider the method as
effectively private and will still allow it to be called from the unit test:

text

@VisibleForTesting void setF() {
  this.f = ...; // RacerD would normally warn here, but @VisibleForTesting will silence the warning
}

synchronized void setFWithLock() {
  setF();
}

Unlike the other annotations shown here, this one lives in
Android.

Interprocedural Reasoning

An important feature of RacerD is that it finds races by analyzing not just one
file or class, but by looking at memory accesses that occur after going through
several procedure calls. It handles this even between classes and between files.

Here is a very basic example

text

@ThreadSafe
class A{

  void m1(B bb) {
    bb.meth_write();
  }
}

class B{
 Integer x;

 void meth_write() {
   x = 88;
 }

}

Class B is not annotated @ThreadSafe and does not have any locks, so RacerD
does not directly look for threading issues there. However, method m1() in
class A has a potential self-race, if it is run in parallel with itself and
the same argument for each call. RacerD discovers this.

text

InterProc.java:17: error: THREAD_SAFETY_VIOLATION
  Unprotected write. Non-private method `A.m1` indirectly writes to field `&this.B.x` outside of synchronization.
 Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in
 parallel with other non-private methods in the class (incuding itself).
  15.
  16.     void m1(B bb) {
  17. >     bb.meth_write();
  18.     }
  19.   }

RacerD does this sort of reasoning using what is known as a compositional
inteprocedural analysis. There, each method is analyzed independently of its
context to produce a summary of the behaviour of the procedure. In this case the
summaries for m1()' andmeth()' include information as follows.

text

Procedure: void A.m1(B)
Accesses: { Unprotected({ 1 }) -> { Write to &bb.B.x at void B.meth_write() at line 17 } }

Procedure: void B.meth_write()
Accesses { Unprotected({ 0 }) -> { Write to &this.B.x at  at line 25 } }

The descriptions here are cryptic and do not include all the information in the
summaries, but the main point is that you can use RacerD to look for races in
codebases where the mutations done by threads might occur only after a chain of
procedure calls.

Reasoning about concurrency divides into bug detection and proving absence of
bugs. RacerD is on the detection side of reasoning.

The rapid growth in the number of interleavings is problematic for tools that
attempt exhaustive exploration. With just 150 instructions for two threads, the
number 10^88 of interleavings is more that the estimated number of atoms in the
known universe.
There has been important work which uses various techniques to attempt to reduce the number of interleavings
while still in principle covering all possibilities, but scale is still a
challenge. Note that RacerD is not exhaustive: it has false negatives (missed
bugs). But in compensation it is fast, and effective (it finds bugs in
practice).

Static analysis for concurrency has attracted a lot of attention from
researchers, but difficulties with scalability and precision have meant that
previous techniques have had little industrial impact. Automatic static race
detection itself has seen significant work. The most advanced approaches,
exemplified by the Chord
tool, often use a whole-program analysis paired with a sophisticated alias
analysis, two features we have consciously avoided. Generally speaking, the
leading research tools can be more precise, but RacerD is faster and can operate
without the whole program: we have opted to go for speed in a way that enables
industrial deployment on a large, rapidly changing codebase, while trying to use
as simple techniques as possible to cover many (not all) of the patterns covered
by slower but precise research tools.

An industrial static analysis tool from
Contemplate also targets
@ThreadSafe annotations, but limits the amount of inter-procedural reasoning:
“This analysis is interprocedural, but to keep the overall analysis scalable,
only calls to private and protected methods on the same class are followed”.
RacerD does deep, cross-file and cross-class inter-procedural reasoning, and yet
still scales; the inter-class capability was one of the first requests from
Facebook engineers.
A separate blog post looked at 100 recent data race fixes
in Infer's deployment in various bug categories, and for data races observed
that 53 of them were inter-file (and thus involving multiple classes).
See above for an example of RacerD's interprocedural
capabilities.

One reaction to the challenge of developing effective static race detectors has
been to ask the programmer to do more work to help the analyzer. Examples of
this approach include the
Clang Thread Safety Analyzer,
the typing of locks in
Rust, and the use/checking of @GuardedBy annotations in
Java
including in
Google's Error Prone analyzer.
When lock annotations are present they make the analyzer's life easier. It is possible to have a very effective race analysis without decreeing
that such annotations must be present. This was essential for our deployment,
since requiring lock annotations would have been a show stopper for converting
many thousands of lines of code to a concurrent context. We believe that this
finding should be transportable to new type systems and language designs, as
well as to other analyses for existing languages.

Another reaction to difficulties in static race detection has been to instead
develop dynamic analyses, automatic testing tools which work by running a
program to attempt to find flaws. Google's Thread Sanitizer is a widely used and
mature tool in this area, which has been used in production to find many bugs in
C-family languages.
The Thread Sanitizer authors explicitly call out limitations with static race analyzers
as part of their motivation: “It seems unlikely that static detectors will work
effectively in our environment: Google’s code is large and complex enough that
it would be expensive to add the annotations required by a typical static
detector”.

We have worked to limit the annotations that RacerD needs, for reasons similar
those expressed by the Thread Sanitizer authors. And we have sought to bring the
complementary benefits of static analysis — possibility of cheaper analysis and
fast reporting, and ability to analyze code before it is placed in a context to
run — to race detection. But we are interested as well in the future in
leveraging ideas in the dynamic techniques to improve or add to our analysis for
race detection.

Limitations

There are a number of known limitations to the design of the race detector.

It looks for races involving syntactically identical access paths, and misses
races due to aliasing
It misses races that arise from a locally declared object escaping its scope
It uses a boolean locks abstraction, and so misses races where two accesses
are mistakenly protected by different locks
It assumes a deep ownership model, which misses races where local objects
refer to or contain non-owned objects.
It avoids reasoning about weak memory and Java's volatile keyword

Most of these limitations are consistent with the design goal of reducing false
positives, even if they lead to false negatives. They also allow technical
tradeoffs which are different than if we were to favour reduction of false
negatives over false positives.

A different kind of limitation concerns the bugs searched for: Data races are
the most basic form of concurrency error, but there are many types of
concurrency issues out there that RacerD does not check for (but might in the
future). Examples include deadlock, atomicity, and check-then-act bugs (shown
below). You must look for these bugs yourself!

text

@ThreadSafe
public class SynchronizedList<T> {
  synchronized boolean isEmpty() { ... }
  synchronized T add(T item) { ... }

// Not thread safe!!!
public class ListUtil<T> {
  public void addIfEmpty(SynchronizedList<T> list, T item) {
    if (list.isEmpty()) {
      // In a race, another thread can add to the list here.
      list.add(item);
    }
  }
}

Finally, using synchronized blindly as a means to fix every unprotected write
or read is not always safe. Even with RacerD, finding, understanding, and fixing
concurrency issues is difficult. If you would like to learn more about best
practices, Java Concurrency in Practice is an excellent
resource.

List of Issue Types

The following issue types are reported by this checker:

Checker Resource Leak Lab (`website/docs/checker-resource-leak-lab.md`)

title: "Resource Leak Lab Exercise"

Toy checker for the "resource leak" write-your-own-checker exercise.

Activate with --resource-leak-lab.

Supported languages:

C/C++/ObjC: No
C#/.Net: Yes
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

This toy checker does nothing by default. Hack on it to make it report resource leaks! See the lab instructions.

List of Issue Types

The following issue types are reported by this checker:

LAB_RESOURCE_LEAK

Checker Scope Leakage (`website/docs/checker-scope-leakage.md`)

title: "Scope Leakage"

Activate with --scope-leakage.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

SCOPE_LEAKAGE

Checker Self In Block (`website/docs/checker-self-in-block.md`)

title: "Self in Block"

An Objective-C-specific analysis to detect when a block captures self.

Activate with --self-in-block.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: No
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

Checker Sil Validation (`website/docs/checker-sil-validation.md`)

title: "SIL validation"

This checker validates that all SIL instructions in all procedure bodies conform to a (front-end specific) subset of SIL.

Activate with --sil-validation.

Supported languages:

C/C++/ObjC: No
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

INVALID_SIL

Checker Siof (`website/docs/checker-siof.md`)

title: "Static Initialization Order Fiasco"

Catches Static Initialization Order Fiascos in C++, that can lead to subtle, compiler-version-dependent errors.

***DEPRECATED*** This checker is deprecated and will be removed in a future release.

Activate with --siof.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: No
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

STATIC_INITIALIZATION_ORDER_FIASCO

Checker Starvation (`website/docs/checker-starvation.md`)

title: "Starvation"

Detect various kinds of situations when no progress is being made because of concurrency errors.

Activate with --starvation.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: Yes
Python: No
Rust: No
Swift: No

Detect several kinds of "starvation" problems:

deadlocks
violations of @Lockless annotations
violations of Android's "strict mode"
doing expensive operations on the Android UI thread

List of Issue Types

The following issue types are reported by this checker:

Checker Static Constructor Stall Checker (`website/docs/checker-static-constructor-stall-checker.md`)

title: "Static Constructor Stall Checker"

Detect if dispatch_once is called from a static constructor.

Activate with --static-constructor-stall-checker.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: No
Python: No
Rust: No
Swift: No

List of Issue Types

The following issue types are reported by this checker:

STATIC_CONSTRUCTOR_STALL

Checker Swift Objc Nullability (`website/docs/checker-swift-objc-nullability.md`)

title: "Swift/Obj-C Nullability"

Detects missing nullability annotations in Objective-C methods called from Swift, which can lead to runtime crashes via Implicitly Unwrapped Optionals.

Activate with --swift-objc-nullability.

Supported languages:

C/C++/ObjC: Yes
C#/.Net: No
Erlang: No
Hack: No
Java: No
Python: No
Rust: No
Swift: Yes

Swift/Obj-C Nullability

Reports calls from Swift code to Objective-C methods whose declaration
has no _Nullable or _Nonnull annotation on a pointer return type.
The Swift clang importer treats such results as Implicitly Unwrapped
Optionals (T!), so any subsequent use that assumes the result is
non-nil traps at runtime if the method ever returns nil. The checker
raises the trap-prone call sites at compile time so the team that owns
the Objective-C declaration can decide the contract explicitly.

The recommended fix lives on the
MISSING_NULLABILITY_ANNOTATION
issue page: annotate the Objective-C declaration with _Nullable or
_Nonnull, or cast the result with as? at the Swift call site.

What is deliberately ignored

To keep reports actionable, the checker does not report at call sites
where the developer cannot or should not be asked to act:

Callees declared in headers under an Apple SDK or under a prebuilt
framework's public-header directory: the consumer cannot edit those
declarations.
Calls whose return value is null-checked by the Swift caller
before use, e.g. if let s = api.foo() { ... }.
Calls whose return value is explicitly cast through an as?
Optional cast, e.g. if let s = api.foo() as? NSString { ... }.

A bare force-unwrap (api.foo()!) is intentionally NOT treated as a
fix — it makes the trap explicit but does not eliminate it.

List of Issue Types

The following issue types are reported by this checker:

MISSING_NULLABILITY_ANNOTATION

Checker Topl (`website/docs/checker-topl.md`)

title: "Topl"

Detect errors based on user-provided state machines describing temporal properties over multiple objects.

Activate with --topl.

Supported languages:

C/C++/ObjC: Experimental
C#/.Net: No
Erlang: Experimental
Hack: No
Java: Experimental
Python: No
Rust: No
Swift: No

Topl

What is it?

Topl is an analysis framework, built on top of Infer, for statically finding violations of temporal properties. Many analyses can be encoded as temporal properties supported by Topl, such as taint analysis. As a simple example, suppose that we don't want a value returned by method source() to be sent as an argument to a method sink(). This can be specified as follows:

text

property Taint
  prefix "Main"
  start -> start: *
  start -> tracking: source(Ret) => x := Ret
  tracking -> error: sink(Arg, VoidRet) when x == Arg

This specifies an automaton called Taint that has three states (start, tracking, error). Two of those states (start and error) have special meaning; other states (tracking) can have any names. The first transition (start → tracking) is taken when a method called source() is called, and its return value is stored in a register called x; the second transition (tracking → error) is taken when a method called sink() is called, but only if its argument equals what was previously saved in register x.
This property is violated in the following Java code:

text

public class Main {
  static void f() { g(tito(source())); }
  static void g(Object x) { h(x); }
  static void h(Object x) { sink(x); }
  static Object tito(Object x) { return x; }
  static Object source() { return "dirty"; }
  static void sink(Object x) {}
}

Note that source() and sink() are not called from the same method, and that the “dirty” object is passed around a few times before finally reaching the sink. Assuming that the property is in a file taint.topl and the Java code in a file Main.java, you can invoke Infer with the following command:

text

infer --topl --topl-properties taint.topl  -- javac Main.java

It will display the following error:

text

Main.java:2: error: Topl Error
  property Taint reaches state error.
  1.   public class Main {
  2. >   static void f() { g(tito(source())); }
  3.     static void g(Object x) { h(x); }
  4.     static void h(Object x) { sink(x); }

To get a full trace, use the command

text

infer explore

Specifying Properties

A property is a nondeterministic automaton that can remember values in registers. An execution that drives the automaton from the start state to the error state will make Infer report an issue, and the trace that it produces will indicate which parts of the program drive which transitions of the automaton.

The general form of a property is the following:

text

property Name
  message "Optional error message" // This line can be missing
  prefix "Prefix" // There can be zero, one, or more prefix declarations
  sourceState -> targetState: Pattern(Arg1,...,ArgN,Ret) when Condition => Action

The property name and the optional error message are used for reporting issues. The prefix declarations are used to simplify Patterns. The core of the property is the list of transitions.

Each transition has a source state and a target state. The special transition label * means that the transition is always taken. Typically, there is a transition

text

start -> start: *

meaning that the property can start anywhere, not just at the beginning of a method.

Otherwise, the label on a transition contains:

a Pattern, which indicates what kind of instruction in the program drives this transition;
a list of transition variable bindings (above named Arg1, ..., but any identifier starting with uppercase letters works);
possibly a boolean Condition, which can refer to transition variables, registers and fields;
possibly and Action, which is a list sequence of assignments of the form register := TransitionVariable (registers do not need to be declared, and any identifier starting with a lowercase letter works).

There are two types of patterns:

a regex that matches method names
- if the regex uses non-letters (such as dots) it must be within double-quotes; otherwise, double quotes are optional
- the prefix declarations are used to add potential prefixes to the regex. The combine regex is essentially “(prefix_regex_a | prefix_regex_b) transition_pattern_regex“
- for a method with n arguments, there must be n+1 transition variables to get a match. The first n transition variables get bound to the argument values, and the last transition variable gets bound to the return value. This is true even for the case in which the return type is void.
the special keyword #ArrayWrite. In that case, there should be two transition variables like “(Array, Index)” — Array gets bound to the array object, and Index gets bound to the index at which the write happens.

The condition supports the following kinds of expressions:

Referring to identifiers: transition variables and registers
Field access over objects in the form Identifier:Type.FieldName, e.g. X:MyClass.myField (this is currently only supported for Erlang)
Integer literals
The usual comparison operators (==, !=, <, >, >=, <=) and conjunctions (&&)
Reachability predicates of the form Ident1 ~~> Ident2 meaning that Ident2 can be reached via pointers/fields from Ident1 in the heap

For several examples, see https://github.com/facebook/infer/tree/main/infer/tests/codetoanalyze/java/topl

Limitations

By design, some problems may be missed. Topl is built on Pulse, which attempts to minimize false positives, at the cost of sometimes having false negatives.
Analysis time increases exponentially with the number of registers used in properties.
- In theory, there should be no significant slowdown if registers belong to different properties, but the implementation is not yet optimized.
- If there are many registers within the same property, then the slowdown is unavoidable (without some significant breakthrough). However, the maximum number of registers we ever used for one practical property was 3.

List of Issue Types

The following issue types are reported by this checker:

Man Infer Analyze (`website/docs/man-infer-analyze.md`)

id: man-infer-analyze title: infer analyze

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Capture (`website/docs/man-infer-capture.md`)

id: man-infer-capture title: infer capture

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Compile (`website/docs/man-infer-compile.md`)

id: man-infer-compile title: infer compile

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Debug (`website/docs/man-infer-debug.md`)

id: man-infer-debug title: infer debug

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Explore (`website/docs/man-infer-explore.md`)

id: man-infer-explore title: infer explore

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Help (`website/docs/man-infer-help.md`)

id: man-infer-help title: infer help

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Report (`website/docs/man-infer-report.md`)

id: man-infer-report title: infer report

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Reportdiff (`website/docs/man-infer-reportdiff.md`)

id: man-infer-reportdiff title: infer reportdiff

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer Run (`website/docs/man-infer-run.md`)

id: man-infer-run title: infer run

import HtmlWrap from "@site/src/components/HtmlWrap";

Man Infer (`website/docs/man-infer.md`)

id: man-infer title: infer

import HtmlWrap from "@site/src/components/HtmlWrap";

Support (`website/docs/support.md`)

title: Infer | Need help? id: support

Need help?

Do not hesitate to ask questions using the following channels, or to submit pull
request!

GitHub issues

The GitHub issues page is a good
place to ask questions, find answers, and report issues.

Please include as many details as possible when submitting a GitHub issue. If
you are able to run Infer, please include the contents of
infer-out/toplevel.log in your report. If not, please include at least your
operating system and the version of Infer that you are using.

Updates

Keep up to date with the latest Infer news on our
Facebook page and our
Twitter account.

IRC

Our IRC channel is #infer on Libera Chat.

Troubleshooting

Infer cannot analyze my CocoaPods project

In the presence of CocoaPods, you should use xcworkspace and not xcodeproj in
the compilation command that you supply to Infer. Here is an example you can
adapt to your project:

bash

infer run -- xcodebuild -workspace HelloWorld.xcworkspace -scheme HelloWorld

`infer [options] -- ` fails during a linking step

The linker will sometimes not work if files have been compiled using a different
compiler, such as the one Infer uses under the hood to
analyze your files.

A workaround consists in setting the LD environment variable to a dummy
linker, for instance:

text

LD=/bin/true infer [options] -- <build command>

I get a compilation error involving PCH files when running Infer

For instance,
error: PCH file uses an older PCH format that is no longer supported.

This is a known issue.

Please run Infer with the following environment variable setting:

bash

GCC_PRECOMPILE_PREFIX_HEADER=NO

Infer reports a "Too many open files" error

The maximum number of files a program can simultaneously hold open is a bit low
on MacOs. You can increase the limit by running these commands for example:

bash

sysctl -w kern.maxfiles=20480
sysctl -w kern.maxfilesperproc=22480
ulimit -S -n 2048

Note that the settings will be reset at the next reboot.

I get a lint error when running Infer with gradle

You need to manually disable linters to run Infer. For instance

bash

infer run -- gradle build -x lint

Running `infer [options] -- ` fails with some other error

Please make sure that:

`` runs successfully on its own.
infer is in your $PATH (try which infer, it should show where infer is
located)

I get errors compiling Infer

Make sure the dependencies are up to date. They may change as we
update Infer itself. See the installation
document
for an up-to-date list of dependencies and how to get them.

My problem is not listed here

Do not hesitate to contact us.

FAQ

Here are some frequently asked questions. More to come.

How do I suppress Infer warnings on a class or method?

In Java code, you can do this for some error types by annotating
your class or method with @SuppressLint(""), for example
@SuppressLint("NULL_DEREFERENCE"). However, not all checkers honor
this annotation.

Is Infer supported for Windows?

Infer is not supported on Windows at the moment. You may try installing Infer on
a Linux virtual machine if your project can be compiled on Linux.

How does Infer compare to the Clang Static Analyzer?

Infer and Clang Static Analyzer (CSA) will typically find different
kinds of issues on the same project. One thing that sets Infer apart
from other static analysis tools is its ability to reason and find
issues across multiple files. But CSA will find many kinds of issues
that Infer doesn't find: we send big respect to CSA! Really, these
tools complement one another and it makes sense to use both.

How does Infer compare to Android linters and Findbugs?

Infer finds deeper infer-procedural bugs sometimes spanning multiple files.
Linters, in contrast, typically implement simple syntactic checks that are local
within one procedure. But they are valuable and Infer doesn't try to duplicate
what they are good at. At Facebook we run both Infer and a collection of Android
linters. Findbugs can be useful too; it is more akin to linters.

Versions (`website/docs/versions.md`)

id: versions title: Documentation Versions

Browse the documentation for different versions:

Dependencies Charon Docs Limitations (`dependencies/charon/docs/limitations.md`)

Current limitations of Charon

Charon is alpha software. In particular, it is currently poorly documented, doesn't support all the
Rust features we'd like, and has several breaking changes planned in the near future.

Planned breaking changes

https://github.com/AeneasVerif/charon/issues/287
https://github.com/AeneasVerif/charon/issues/194
https://github.com/AeneasVerif/charon/issues/582
Some potential rework of how we handle builtins like SliceIndexMut
Name matcher behavior likely to change in subtle ways
(https://github.com/AeneasVerif/charon/issues/319).

Known unsoundnesses

Unsupported Rust features

Tracked here: https://github.com/AeneasVerif/charon/issues/142

Missing information in the translated output

Bodies of functions in foreign crates often cause errors (https://github.com/AeneasVerif/charon/issues/543);
Bodies of std functions (https://github.com/AeneasVerif/charon/issues/545);
Drops (https://github.com/AeneasVerif/charon/issues/152);
Layout information (https://github.com/AeneasVerif/charon/issues/581);
Lifetime information inside function bodies (not planned).

Dependencies Charon Docs Transformations (`dependencies/charon/docs/transformations.md`)

Charon transformations

Charon has options to make the generated code easier to use. Some are currently not optional but
could be made so on request.

Control-flow reconstruction

The MIR we get from rustc is a control-flow graph (CFG), where control-flow happens with gotos that
can jump arbitrarily around the code.

Charon by default transforms this CFG into structured control-flow, i.e. with nested
match/if/loop constructs.

To turn this off, pass --ullbc to charon (ULLBC stands for Unstructured LLBC).

`--hide-marker-traits`

This option removes mentions of the following built-in traits from the output crate:

core::marker::Sized
core::marker::Tuple
core::marker::Send
core::marker::Sync
core::marker::Unpin

This is a convenience option, meant to reduce noise for Charon consumers that output user-readable
things.

Note that for historical reasons Charon removes mentions of the Allocator trait regardless of this
setting. This should eventually be changed, open an issue if you have a need for it.

Note that today this is implemented by calling IndexMap::remove to remove the entry in the
trait_clauses/trait_refs vectors. This abuses the confusion between newtype-indexed vectors and
newtype-indexed maps we have in Charon, which can cause annoying footguns. See
https://github.com/AeneasVerif/charon/issues/490.

`--remove-associated-types`

This option takes a pattern, and transforms the associated types of all the traits that match the
pattern. This transforms code like:

rust

trait Iterator {
  type Item;
  fn next(&mut self) -> Option<Self::Item>;
}
fn use_iterator<I: Iterator>(it: I) { ... }

into:

rust

trait Iterator<Item> {
  fn next(&mut self) -> Option<Item>;
}
fn use_iterator<I: Iterator<Clause0Item>, Clause0Item>(it: I) { ... }

This transformation has limitations:

GATs cannot be transformed this way;
Some recursive traits cannot be transformed this way, e.g.:

rust

trait Bar {
    type BarTy;
}
trait Foo {
    type FooTy: Foo + Bar;
}
// becomes:
trait Bar<BarTy> {}
trait Foo {
    type FooTy: Foo + Bar<Self::FooTy_BarTy>;
    // We need to supply an argument to `Bar` but we can't add a type parameter, so we add a
    // new associated type.
    type FooTy_BarTy;
}

We're currently missing assoc type information to transform dyn Trait (https://github.com/AeneasVerif/charon/issues/123).
We currently don't track bound lifetimes in quantified clauses properly (https://github.com/AeneasVerif/charon/issues/534).
Type aliases don't have the correct clauses in scope (https://github.com/AeneasVerif/charon/issues/531).
We don't take into account unicity of trait implementations. This means we won't detect type
equalities due to the same trait predicate appearing twice, or a trait predicate coinciding with
an existing trait impl. See the dictionary_passing_style_woes.rs test file for an example.

Make implied bounds explicit

WIP: https://github.com/AeneasVerif/charon/issues/585

Dependencies Charon Docs Usage (`dependencies/charon/docs/usage.md`)

Usage

To run Charon, you should run the Charon binary from within the crate that you
want to compile, as if you wanted to build the crate with cargo build. The
Charon executable is located at bin/charon.

Charon will build the crate and its dependencies, then extract the AST. Charon
provides various options and flags to tweak its behaviour: you can display a
detailed documentation with --help.
In particular, you can pretty-print the translated crate with both --print-ullbc and --print-llbc, depending on the Charon intermediate representation you wish to use.

If there is a Charon.toml file at the root of your project, charon will also take options from it.
The file supports the same options at the cli interface, except for the options that relate to
input/output like --print-llbc. Example Charon.toml:

toml

[charon]
extract_opaque_bodies = true
[rustc]
flags = ["--cfg", "abc"]

Remark: because Charon is compiled with Rust nightly (this is a requirement to implement a rustc
driver), it will build your crate with Rust nightly. You can find the nightly version pinned for
Charon in rust-toolchain.template.

Names

Each item (function, trait decl, type decl etc) in Charon has a unique name, that looks like a Rust
path (e.g., std::boxed::Box). This name can be used to uniquely identify items using patterns.

These patterns are used most notably for the --include/--exclude cli options, and made available
in Rust and OCaml with NameMatcher. Caveat: the Rust and OCaml name matchers differ in input syntax
and behavior; this is tracked in https://github.com/AeneasVerif/charon/issues/319.

TODO: explain syntax and behavior.

Note: for well-known built-in items, you can often use ItemMeta.lang_item instead; it contains an
identifier meant for this purpose, documented
here.

CLI options

TODO: explain the main options, and LLBC vs ULLBC

In short: LLBC is the name we give to the output of Charon. It stands for Low-Level Borrow Calculus
and is the name used in the formalisations of the Aeneas project. Charon was initially created as
part of the Aeneas project, and therefore inherits that name. ULLBC means Unstructured LLBC, i.e.,
LLBC without the control-flow reconstruction.

ULLBC is a slightly simplified MIR, where we try to remove as much redundancies
as possible. For instance, we drastically simplify the representation of constants coming
from the Rust compiler.

LLBC is ULLBC where we restructured the control-flow with loops, if ... then ... else ..., etc. instead of gotos. Consequently, we merge MIR
statements and terminators into a single LLBC statement type.

Remark: most of the transformations which transform the MIR to ULLBC then LLBC are implemented
by means of micro-passes. Depending on the need, we could make them optional and control them with
flags. If you want to know more about the details, see transformation_passes in
src/bin/charon-driver/driver.rs, which applies the micro-passes one after the other.

Dependencies Charon Docs What Charon Does For You (`dependencies/charon/docs/what_charon_does_for_you.md`)

What Charon Does For You

The purpose of Charon is to centralize the efforts of extracting information from rustc internals
and turning them into a uniform and usable shape. Here are some things that Charon does once so you
don't have to do it yourself:

TODO: explain each item

Trait resolution (explicitly track how each trait bound was proven to hold);
Reconstruct expressions from all the various constant representations;
Hide the distinction between early- and late-bound lifetime variables;
Make non-overriden default methods in impl blocks appear as normal methods;
Handle trait method implementations that have a more general signature than as declared in the trait (WIP: https://github.com/AeneasVerif/charon/issues/513);
Represent closures as normal structs that implement the Fn* traits;
Represent VTables as normal structs stored in statics (WIP: see https://github.com/AeneasVerif/charon/issues/123);
Many useful post-processing transformations to make the output more usable; see the dedicated file.

Dependencies Charon Docs What Charon Translates (`dependencies/charon/docs/what_charon_translates.md`)

Charon item selection

Items and opacity

An item is a module, function, type decl, static, const, trait decl, or trait impl. A crate is considered a module.

Each item has an opacity level^1:

Transparent — the item is fully translated.
Foreign — the default for items outside the current crate. Translation depends on normal Rust visibility: for types, translate fully if it's a struct with all-public fields or an enum; for other items this is equivalent to Opaque.
Opaque — only the name and signature are translated, not the contents. For functions and globals, the body is not translated. For types (structs, enums, unions), the fields/variants are not translated. For traits and trait impls, the default method is only translated if it is used somewhere else. For modules, the contents are not explored (but items referenced from elsewhere are still translated).
Invisible — nothing is translated for this item. The corresponding map will not have an entry for the item ID. Useful when even the signature causes errors.

Selection process

Charon starts from a set of entry points and explores outward using a work-queue:

The entry point items are enqueued for processing.
Each item is processed according to its opacity:
- Transparent module: enqueue all items directly inside it.
- Non-transparent module: do nothing (contents are not explored).
- Transparent non-module item: translate it fully (including body).
- Foreign or opaque non-module item: translate only the signature.
- Invisible item: do nothing.
Whenever processing an item encounters a reference to a new item, that new item is enqueued for processing.

This is a dependency-driven algorithm that pulls in items as they are needed. With the default settings, the entry point is the current crate (a module), which is transparent, so all its direct items are enqueued. Those items reference foreign items from dependencies, which get enqueued as foreign (signatures only). The result: the whole current crate is translated, plus the signatures of all foreign items it references.

How opacity is determined

Each item's opacity is calculated from its name by matching against a list of patterns. The patterns come from two sources: CLI flags and source annotations.

Source annotations

The source-level attributes #[charon::opaque] and #[charon::exclude] set the opacity of individual items. They can only make items more opaque, never less^2.

When both a source annotation and a CLI pattern apply, the more opaque of the two wins (Transparent < Foreign < Opaque < Invisible). This means --include cannot override a #[charon::opaque] annotation.

CLI flags

--start-from — Entry points for translation. Can be specified multiple times. Default: crate (the entire current crate).
--start-from-attribute[=<ATTR>] — Use items annotated with a given attribute as entry points. Default attribute if none specified: verify::start_from.
--start-from-pub — Use all pub items from the current crate as entry points
--include — Set matched items to transparent.
--opaque — Set matched items to opaque.
--exclude — Set matched items to invisible.
--extract-opaque-bodies — Alias for --include *. Makes all items transparent.
--translate-all-methods — Include provided trait methods even if unused. Equivalent to making all trait declarations transparent.

Pattern list

Charon builds an ordered list of (pattern, opacity) pairs from the CLI flags^3:

text

_              → Foreign      (default: everything starts as foreign)
crate          → Transparent  (current crate is always transparent)
<--include>    → Transparent  (user whitelist)
<--opaque>     → Opaque       (user blacklist)
<--exclude>    → Invisible    (user exclusion)

The default is equivalent to --opaque '*' --include crate: everything is foreign except items in the current crate which are transparent.

Pattern syntax

Patterns use a name-matcher syntax (charon/src/name_matcher/). Examples:

crate::module::item — matches this item and all its subitems
crate::module::item::_ — matches only the subitems (not the item itself)
core::convert::{impl core::convert::Into<_> for _} — a specific trait impl
_ or * — glob, matches any single path segment
{impl core::convert::Into<_> for _} works without the core::convert prefix, in this case we do a global search for impls.

Patterns are prefix matches: crate::foo matches crate::foo, crate::foo::bar, crate::foo::bar::baz, etc.^4

Currently matching on inherent impl blocks isn't supported, writing crate::module::_::method is the standard workaround.

Precedence

When multiple patterns match the same item, the most precise pattern wins^5:

Longer patterns beat shorter ones.
Among equal-length patterns, a non-glob final element beats a glob.

Example with --opaque crate::module --include crate::module::_:

Item	Matching patterns	Most precise	Result
`crate::module`	`_`, `crate`, `crate::module`	`crate::module` (length 2)	Opaque
`crate::module::foo`	`_`, `crate`, `crate::module`, `crate::module::_`	`crate::module::_` (length 3)	Transparent

Note: pattern matching currently has limitations — e.g. it parses u64 as a path instead of the built-in type, and it is not possible to filter a trait impl (only its methods)^6.

--- METRICS ---

Files Extracted: 57
Estimated Token Budget: ~69153 tokens
Canonical Reference: https://codewiki.google/github.com/facebook/infer

Technical Documentation: facebook/infer

Overview (README.md) Copy Section

Infer

Installation Copy Chapter

Contributing Copy Chapter

License Copy Chapter

00 Getting Started (`website/docs/00-getting-started.md`) Copy Section

id: getting-started title: Getting started with Infer Copy Chapter

Get Infer Copy Chapter

Try Infer in your browser Copy Chapter

00 Hello World (`website/docs/00-hello-world.md`) Copy Section

id: hello-world title: Hello, World! Copy Chapter

Hello world Java Copy Chapter

Hello world Objective-C Copy Chapter

Hello world C Copy Chapter

Hello world C (tree-sitter, no build system) Copy Chapter

Hello world Android Copy Chapter

Differential analysis Copy Section

Hello world iOS Copy Chapter

Hello world Make Copy Chapter

01 Analyzing Apps Or Projects (`website/docs/01-analyzing-apps-or-projects.md`) Copy Section

id: analyzing-apps-or-projects title: Analyzing apps or projects Copy Chapter

ant Copy Section

Buck Copy Section

cmake Copy Section

Gradle Copy Section

Make Copy Section

Maven Copy Section

Xcodebuild Copy Section

xctool Copy Section

Using a compilation database Copy Section

Other build systems Copy Section

01 Infer Workflow (`website/docs/01-infer-workflow.md`) Copy Section

id: infer-workflow title: Infer workflow Copy Chapter

The two phases of an Infer run Copy Chapter

1. The capture phase Copy Section

2. The analysis phase Copy Section

Global (default) and differential workflows Copy Chapter

Global workflow Copy Section

Differential workflow Copy Section

Exploring Infer reports Copy Chapter

01 Man Pages (`website/docs/01-man-pages.md`) Copy Section

id: man-pages title: Infer Manuals Copy Chapter

01 Steps For Ci (`website/docs/01-steps-for-ci.md`) Copy Section

id: steps-for-ci title: Recommended flow for CI Copy Chapter

Differential Workflow Copy Section

Example: Android Gradle Copy Section

01 Suppressions (`website/docs/01-suppressions.md`) Copy Section

id: suppressions title: Suppression of Infer Issues Copy Chapter

Wildcards Copy Section

Examples Copy Section

Accumulation

02 About Infer (`website/docs/02-about-infer.md`) Copy Section

id: about-Infer title: About Infer Copy Chapter

02 Separation Logic And Biabduction (`website/docs/02-separation-logic-and-biabduction.md`) Copy Section

id: separation-logic-and-bi-abduction title: Separation logic and bi-abduction Copy Chapter

Separation logic Copy Chapter

Bi-abduction Copy Chapter

Technical papers Copy Chapter

04 Absint Framework (`website/docs/04-absint-framework.md`) Copy Section

id: absint-framework title: Building checkers with the Infer.AI framework Copy Chapter

By example: intraprocedural analysis Copy Chapter

Error reporting Copy Chapter

By example: interprocedural analysis Copy Chapter

04 Internal API (`website/docs/04-internal-API.md`) Copy Section

id: internal-API title: Infer Internal OCaml Modules API Copy Chapter

All Categories (`website/docs/all-categories.md`) Copy Section

title: List of all categories of issue types Copy Chapter

Concurrency Copy Chapter

Logic error Copy Chapter

Memory error Copy Chapter

Null pointer dereference Copy Chapter

Perf regression Copy Chapter

Resource leak Copy Chapter

Runtime exception Copy Chapter

Sensitive data flow Copy Chapter

Ungated code Copy Chapter

User defined property Copy Chapter

All Checkers (`website/docs/all-checkers.md`) Copy Section

title: List of all checkers hide_table_of_contents: true Copy Chapter

Overview (README.md)

Installation

Contributing

License

00 Getting Started (`website/docs/00-getting-started.md`)

id: getting-started title: Getting started with Infer

Get Infer

Try Infer in your browser

00 Hello World (`website/docs/00-hello-world.md`)

id: hello-world title: Hello, World!

Hello world Java

Hello world Objective-C

Hello world C

Hello world C (tree-sitter, no build system)

Hello world Android

Differential analysis

Hello world iOS

Hello world Make

01 Analyzing Apps Or Projects (`website/docs/01-analyzing-apps-or-projects.md`)

id: analyzing-apps-or-projects title: Analyzing apps or projects

ant

Buck

cmake

Gradle

Make

Maven

Xcodebuild

xctool

Using a compilation database

Other build systems

01 Infer Workflow (`website/docs/01-infer-workflow.md`)

id: infer-workflow title: Infer workflow

The two phases of an Infer run

1. The capture phase

2. The analysis phase

Global (default) and differential workflows

Global workflow

Differential workflow

Exploring Infer reports

01 Man Pages (`website/docs/01-man-pages.md`)

id: man-pages title: Infer Manuals

01 Steps For Ci (`website/docs/01-steps-for-ci.md`)

id: steps-for-ci title: Recommended flow for CI

Differential Workflow

Example: Android Gradle

01 Suppressions (`website/docs/01-suppressions.md`)

id: suppressions title: Suppression of Infer Issues

Wildcards

Examples

02 About Infer (`website/docs/02-about-infer.md`)

id: about-Infer title: About Infer

02 Separation Logic And Biabduction (`website/docs/02-separation-logic-and-biabduction.md`)

id: separation-logic-and-bi-abduction title: Separation logic and bi-abduction

Separation logic

Bi-abduction

Technical papers

04 Absint Framework (`website/docs/04-absint-framework.md`)

id: absint-framework title: Building checkers with the Infer.AI framework

By example: intraprocedural analysis

Error reporting

By example: interprocedural analysis

04 Internal API (`website/docs/04-internal-API.md`)

id: internal-API title: Infer Internal OCaml Modules API

All Categories (`website/docs/all-categories.md`)

title: List of all categories of issue types

Concurrency

Logic error

Memory error

Null pointer dereference

Perf regression

Resource leak

Runtime exception

Sensitive data flow

Ungated code

User defined property

All Checkers (`website/docs/all-checkers.md`)

title: List of all checkers hide_table_of_contents: true

Annotation Reachability

Buffer Overrun Analysis (InferBO)

Config Gating