From 8dd56e431f6f7b2c2344041b5c6261c844a0ca14 Mon Sep 17 00:00:00 2001 From: wolf99 <281700+wolf99@users.noreply.github.com> Date: Sat, 30 Dec 2023 14:50:17 +0000 Subject: [PATCH] Lint markdown - without changes to content --- CONTRIBUTING.md | 93 ++--- FILES.md | 6 +- INSTALL.md | 6 - ISSUE_TEMPLATE.md | 1 + README.md | 2 +- docker/README.md | 4 +- examples/README.md | 3 +- facebook-clang-plugins/README.md | 6 +- facebook-clang-plugins/clang-ocaml/README.md | 17 +- .../libtooling/ATD_GUIDELINES.md | 59 +-- facebook-clang-plugins/libtooling/README.md | 5 +- infer/documentation/checkers/Cost.md | 22 +- .../checkers/LithoRequiredProps.md | 4 +- infer/documentation/checkers/Pulse.md | 2 + infer/documentation/checkers/Purity.md | 8 +- infer/documentation/checkers/RacerD.md | 28 +- infer/documentation/checkers/Starvation.md | 1 + infer/documentation/checkers/Topl.md | 19 +- .../ARBITRARY_CODE_EXECUTION_UNDER_LOCK.md | 1 + infer/documentation/issues/BAD_ARG.md | 2 + infer/documentation/issues/BAD_KEY.md | 1 + infer/documentation/issues/BAD_MAP.md | 1 + infer/documentation/issues/BAD_RECORD.md | 4 +- infer/documentation/issues/BAD_RETURN.md | 1 + infer/documentation/issues/BUFFER_OVERRUN.md | 34 +- .../issues/CAPTURED_STRONG_SELF.md | 61 ++- .../EXECUTION_TIME_COMPLEXITY_INCREASE.md | 2 - ...TION_TIME_COMPLEXITY_INCREASE_UI_THREAD.md | 1 - .../EXECUTION_TIME_UNREACHABLE_AT_EXIT.md | 2 +- .../issues/EXPENSIVE_EXECUTION_TIME.md | 1 + infer/documentation/issues/IMPURE_FUNCTION.md | 1 + .../issues/INEFFICIENT_KEYSET_ITERATOR.md | 3 +- .../issues/INFINITE_AUTORELEASEPOOL_SIZE.md | 1 - .../issues/INFINITE_EXECUTION_TIME.md | 13 +- .../documentation/issues/INTEGER_OVERFLOW.md | 16 +- infer/documentation/issues/INVARIANT_CALL.md | 1 + .../issues/MISSING_REQUIRED_PROP.md | 4 +- .../issues/MODIFIES_IMMUTABLE.md | 7 +- .../issues/NO_MATCHING_BRANCH_IN_TRY.md | 1 + .../issues/NO_MATCHING_CASE_CLAUSE.md | 1 + .../issues/NO_MATCHING_FUNCTION_CLAUSE.md | 1 + .../issues/NO_TRUE_BRANCH_IN_IF.md | 1 + infer/documentation/issues/NULL_ARGUMENT.md | 4 +- .../issues/PULSE_TRANSITIVE_ACCESS.md | 3 +- .../issues/PULSE_UNNECESSARY_COPY.md | 2 +- .../PULSE_UNNECESSARY_COPY_INTERMEDIATE.md | 10 +- .../issues/PULSE_UNNECESSARY_COPY_MOVABLE.md | 3 +- infer/documentation/issues/RESOURCE_LEAK.md | 10 +- infer/documentation/issues/SCOPE_LEAKAGE.md | 5 +- infer/src/erlang/README.md | 50 ++- infer/src/labs/README.md | 33 +- infer/tests/codetoanalyze/erlang/README.md | 3 + website/README.md | 24 +- website/docs/00-hello-world.md | 24 +- .../02-separation-logic-and-biabduction.md | 29 +- website/docs/all-checkers.md | 1 - website/docs/all-issue-types.md | 393 +++++++++++------- .../docs/checker-annotation-reachability.md | 4 +- website/docs/checker-biabduction.md | 2 + website/docs/checker-bufferoverrun.md | 2 + .../docs/checker-config-impact-analysis.md | 2 + website/docs/checker-cost.md | 25 +- website/docs/checker-datalog.md | 4 +- website/docs/checker-fragment-retains-view.md | 4 +- website/docs/checker-impurity.md | 3 +- .../checker-inefficient-keyset-iterator.md | 4 +- website/docs/checker-lineage.md | 2 +- website/docs/checker-litho-required-props.md | 4 +- website/docs/checker-liveness.md | 4 +- website/docs/checker-loop-hoisting.md | 3 +- .../checker-parameter-not-null-checked.md | 3 +- website/docs/checker-printf-args.md | 4 +- website/docs/checker-pulse.md | 5 +- website/docs/checker-purity.md | 11 +- website/docs/checker-quandary.md | 3 +- website/docs/checker-racerd.md | 39 +- website/docs/checker-resource-leak-lab.md | 2 + website/docs/checker-scope-leakage.md | 4 +- website/docs/checker-self-in-block.md | 4 +- website/docs/checker-sil-validation.md | 4 +- website/docs/checker-siof.md | 4 +- website/docs/checker-starvation.md | 4 +- website/docs/checker-topl.md | 38 +- website/docs/support.md | 2 +- website/docs/versions.md | 1 + 85 files changed, 655 insertions(+), 577 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9d65399d62e..beca63e1618 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,6 +1,5 @@ # Contribution Guidelines - ## Reporting Issues If you encounter a problem when using infer or if you have any questions, please open a @@ -14,6 +13,7 @@ We welcome contributions via [pull requests on GitHub](https://github.com/facebo You'll want to install a few more dependencies to comfortably hack on the infer codebase; in order to do this run `./build_infer.sh` which will allow you to then run: + ```sh make devsetup ``` @@ -23,14 +23,11 @@ make devsetup - The default build mode ("dev") makes all build warnings *fatal*. If you want the build to ignore warnings, for example to be able to test an infer executable before polishing the code to remove warnings, you can build in "dev-noerror" mode with `make BUILD_MODE=dev-noerror`. - - Faster edit/build cycle when working on OCaml code inside infer/src/: build inside infer/src/ (skips building the models after infer has been built), and build only what is needed for type checking with `make -j -C infer/src check`. You need to have run `make -j` at some point before. - - Alternatively, if you want to test your changes on a small example, build in bytecode mode: `make -j -C infer/src byte`. - - In general, `make` commands from the root of the repository make sure that dependencies are in a consistent and up-to-date state (e.g., they rebuild infer and the models before running steps that use infer), while running `make` commands from within subdirectories generally assumes that @@ -40,26 +37,23 @@ make devsetup necessary before running the test, but running `make -C infer/tests/codetoanalyze/java/biabduction/ test` will just execute the test. - ### Debugging OCaml Code - Printf-debug using `Logging.debug_dev`. It comes with a warning so that you don't accidentally push code with calls to `debug_dev` to the repo. - - Browse the documentation of OCaml modules in your browser with `make doc` - - When using `ocamldebug`, and in particular when setting break points with `break @ ` don't forget that an infer module `M` is in reality called `InferModules__M`, or `InferBase__M`, or ... See the html documentation of the OCaml modules from `make doc` if you're unsure of a module name. -```console -$ ledit ocamldebug infer/bin/infer.bc.exe -(ocd) break @ InferModules__InferAnalyze 100 -Breakpoint 1 at 9409684: file backend/InferAnalyze.ml, line 99, characters 18-78 -``` + ```console + $ ledit ocamldebug infer/bin/infer.bc.exe + (ocd) break @ InferModules__InferAnalyze 100 + Breakpoint 1 at 9409684: file backend/InferAnalyze.ml, line 99, characters 18-78 + ``` - To test the infer OCaml code you can use the OCaml toplevel. To build the OCaml toplevel with the infer modules pre-loaded, run @@ -71,7 +65,6 @@ Breakpoint 1 at 9409684: file backend/InferAnalyze.ml, line 99, characters 18-78 Many operations require the results directory and database to be initialized with `ResultsDir.assert_results_dir ""`. - ## Contributor License Agreement We require contributors to sign our Contributor License Agreement. In @@ -88,80 +81,71 @@ Thanks! ### All Languages - Indent with spaces, not tabs. - - Line width limit is 100 characters. - - In general, follow the style of surrounding code. ### OCaml - The module IStd (infer/src/istd/IStd.ml) is automatically opened in every file. Beware that this can cause weird errors such as: -``` -$ pwd -/somewhere/infer/infer/src -$ cat base/toto.ml -let b = List.mem true [true; false] -$ make -[...] -File "base/toto.ml", line 1, characters 17-21: -Error: This variant expression is expected to have type 'a list - The constructor true does not belong to type list -``` + + ```console + $ pwd + /somewhere/infer/infer/src + $ cat base/toto.ml + let b = List.mem true [true; false] + $ make + [...] + File "base/toto.ml", line 1, characters 17-21: + Error: This variant expression is expected to have type 'a list + The constructor true does not belong to type list + ``` - All modules open `IStd` using `open! IStd`. This is to make that fact more explicit (there's also the compilation flag mentioned above), and also it helps merlin find the right types. In particular this also opens `Core.Std`. - - Do not add anything to `IStd` unless you have a compelling reason to do so, for instance if you find some utility function is missing and is not provided by [`Core`](https://ocaml.janestreet.com/ocaml-core/latest/doc/core/). - - Polymorphic equality is disabled; use type-specific equality instead, even for primitive types (e.g., `Int.equal`). However, if your module uses a lot of polymorphic variants with no arguments you may safely `open PolyVariantEqual`. If you try and use polymorphic equality `=` in your code you will get a compilation error, such as: -``` -Error: This expression has type int but an expression was expected of type - [ `no_polymorphic_compare ] -``` + + ```console + Error: This expression has type int but an expression was expected of type + [ `no_polymorphic_compare ] + ``` - Alias and use `module L = Logging` for all your logging needs. Refer to its API in Logging.mli for documentation. - - Check that your code compiles without warnings with `make -j test_build` (this also runs as part of `make test`). - - Apart from `IStd` and `PolyVariantEqual`, refrain from globally `open`ing modules. Using local open instead when it improves readability: `let open MyModule in ...`. - - Avoid the use of module aliases, except for the following commonly-aliased modules. Use module aliases consistently (e.g., do not alias `L` to a module other than `Logging`). -```OCaml -module CLOpt = CommandLineOption -module F = Format -module L = Logging -module MF = MarkupFormatter -``` + + ```OCaml + module CLOpt = CommandLineOption + module F = Format + module L = Logging + module MF = MarkupFormatter + ``` - Use `[@@deriving compare, equal]` to write comparison/equality functions whenever possible. Watch out for [this issue](https://github.com/ocaml-ppx/ppx_deriving/issues/116) when writing `type nonrec t = t [@@deriving compare]`. - - Use named arguments whenever the purpose of the argument is not immediately obvious. In particular, use named arguments for boolean and integer parameters unless the name of the function mentions them explicitly. Also use named arguments to disambiguate between several arguments of the same type. - - Use named arguments for functions taken as argument; it is common to name a function argument `f`. For instance: `List.map : 'a list -> f:('a -> 'b) -> 'b list`. - - In modules defining a type `t`, functions that take an argument of that type should generally have that argument come first, except for optional arguments: `val f : ?optional:bool -> t -> ...`. - - Use the `_hum` suffix to flag functions that output human-readable strings. - - Format code with [ocamlformat](https://github.com/ocaml-ppx/ocamlformat). ### C/C++/Objective-C @@ -172,7 +156,6 @@ Follow `clang-format` (see ".clang-format" at the root of the repository). - Make sure infer builds: `make -j test_build`. Refer to the [installation document](https://github.com/facebook/infer/blob/main/INSTALL.md) for details. - - Run the tests: `make -j 4 test` (adjust 4 to the number of cores available of your machine). The tests (almost) all consist of the same three ingredients: 1. Some source code to run infer on. @@ -180,12 +163,9 @@ Follow `clang-format` (see ".clang-format" at the root of the repository). one line is one issue reported by infer. 3. A `Makefile` that orchestrates the test, for instance running infer on the source code and comparing the results with issues.exp using `diff`. - - If your changes modified some of the expected outputs and if the changes make sense, you can update the expected test results by running `make test-replace`. - - If relevant, add a test for your change. - - To add a test that infer finds (or does not find) a particular issue, add your test in "infer/tests/codetoanalyze/{language}/{analyzer}/". Look at the `Makefile` in that directory and make sure it runs your test. "{analyzer}" is often an infer analyzer (as in @@ -200,21 +180,18 @@ Follow `clang-format` (see ".clang-format" at the root of the repository). - Test procedures documenting current limitations of the analyzer should have the prefix `FP_` (for "false positive") or `FN_` (for "false negative") and a comment explaining why the analyzer gets the wrong answer. - - - To add a test that a certain build system integration or a command-line option works in a certain way, add a test in "infer/tests/build_systems/". - - If you created a new Makefile for your test, add it to the root "Makefile", either to the `DIRECT_TESTS` (first case) or to the `BUILD_SYSTEMS_TESTS` variable (second case). Gate the test appropriately if it depends on Java or Clang or Xcode (see how other tests do it). - - It can be useful to look at the debug HTML output of infer to see the detail of the symbolic execution. For instance: -```sh -$ infer --debug -- clang -c examples/hello.c -$ firefox infer-out/captured/hello.c.*.html -``` + + ```console + infer --debug -- clang -c examples/hello.c + firefox infer-out/captured/hello.c.*.html + ``` ## Updating infer.opam and infer.opam.locked diff --git a/FILES.md b/FILES.md index b5abcab16c0..e4676209fec 100644 --- a/FILES.md +++ b/FILES.md @@ -1,7 +1,7 @@ -#Files in infer/bin/ +# Files in infer/bin/ ## Top-level commands -*infer* : Main command to run Infer. Check out the docs for instructions on how to use it. +`infer` : Main command to run Infer. Check out the docs for instructions on how to use it. -*infer-* : Infer subcommands. Running `infer- [options]` is the same as running `infer [options]`. +`infer-` : Infer subcommands. Running `infer- [options]` is the same as running `infer [options]`. diff --git a/INSTALL.md b/INSTALL.md index e0486e3d2ba..e545e627795 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -8,7 +8,6 @@ the instructions in our [Getting Started](http://fbinfer.com/docs/getting-started/#get-infer) page to install Infer. - ## Infer dependencies for MacOSX Here are the prerequisites to be able to compile Infer on MacOSX. This @@ -35,7 +34,6 @@ You can install some of these dependencies using brew install autoconf automake cmake opam pkg-config sqlite gmp mpfr java ``` - ## Infer dependencies for Linux Here are the prerequisites to be able to compile Infer on Linux. This @@ -52,7 +50,6 @@ is required to compile everything from source. See also the distro-specific instructions for Ubuntu and Debian below. - ## Install Infer from source Run the following commands to get Infer up and running: @@ -78,7 +75,6 @@ Objective-C source code. See `./build-infer.sh --help` for more options, eg `./build-infer.sh` on its own will build the analyzers for both Java and C/ObjC. - ## Install Infer from source without opam If for some reason you prefer to install Infer's OCaml dependencies by @@ -94,13 +90,11 @@ sudo make install export PATH=`pwd`/infer/bin:$PATH ``` - ## How to install the dependencies on Linux See the Dockerfile in docker/ for inspiration. It includes the dependencies needed to build Infer on Debian 9 (stretch). - ### Setting up opam Get opam from your distribution, or from the diff --git a/ISSUE_TEMPLATE.md b/ISSUE_TEMPLATE.md index 1e6b57fa9cb..2d41b852b45 100644 --- a/ISSUE_TEMPLATE.md +++ b/ISSUE_TEMPLATE.md @@ -1,6 +1,7 @@ Please make sure your issue is not addressed in the [FAQ](https://fbinfer.com/docs/support#troubleshooting). Please include the following information: + - [ ] The version of infer from `infer --version`. - [ ] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc. - [ ] Which command you ran, for example `infer -- make`. diff --git a/README.md b/README.md index 6032b8888e7..427b6d0dbab 100644 --- a/README.md +++ b/README.md @@ -20,5 +20,5 @@ See [CONTRIBUTING.md](./CONTRIBUTING.md). Infer is MIT-licensed. -Note: Enabling Java support may require you to download and install +Note: Enabling Java support may require you to download and install components licensed under the GPL. diff --git a/docker/README.md b/docker/README.md index 0a2e281fe34..9c07f0f9eda 100644 --- a/docker/README.md +++ b/docker/README.md @@ -5,7 +5,6 @@ contains a docker file to install Infer within a [docker](https://www.docker.com/) container. This can be used to quickly try Infer or to deploy Infer. - ## Pre-requisites To use this docker image, you will need a working docker @@ -13,12 +12,11 @@ installation. See the instructions for [Linux](http://docs.docker.com/linux/step_one/) or [MacOSX](http://docs.docker.com/mac/step_one/) as appropriate. - ## How to use This docker file will use the latest [released](https://github.com/facebook/infer/releases) version of -Infer. +Infer. 1. Get docker running, e.g. using Docker Quickstart Terminal. 2. go to the version of your choice, e.g. `cd docker/1.1.0/` diff --git a/examples/README.md b/examples/README.md index 9a7d53a0a35..ee57fad0eac 100644 --- a/examples/README.md +++ b/examples/README.md @@ -5,7 +5,7 @@ Contents -------- - `Hello.java`: try this example by running -```infer -- javac Hello.java ``` +```infer -- javac Hello.java``` - `Hello.m`: try this example by running ```infer -- clang -c Hello.m``` @@ -38,4 +38,3 @@ Note The infer toplevel command must be in your PATH for the commands above to succeed. Otherwise, modify the commands to use the correct path to infer, eg ```../infer/bin/infer -- javac Hello.java``` - diff --git a/facebook-clang-plugins/README.md b/facebook-clang-plugins/README.md index e6255ab64fb..8ad1477f10f 100644 --- a/facebook-clang-plugins/README.md +++ b/facebook-clang-plugins/README.md @@ -7,10 +7,8 @@ Structure of the repository --------------------------- - libtooling : frontend plugins (currently a clang-to-json AST exporter), - - clang-ocaml : OCaml libraries to process the JSON output of frontend plugins, - Quick start ----------- @@ -19,13 +17,15 @@ The plugin requires recent version of the clang compiler, re-compiled from sourc To compile and use the required version of clang, please run ./clang/setup.sh. Caveat: + - Because of the nature of C++, clang and the plugins need to be compiled with the exact same C++ libraries. - Also, the default stripping command of clang in release mode breaks plugins. Once the target compiler is installed, `make test` should run the unit tests. OCaml users may also run: -``` + +```console make -C clang-ocaml test #requires proper ocaml libraries, see included clang-ocaml/README ``` diff --git a/facebook-clang-plugins/clang-ocaml/README.md b/facebook-clang-plugins/clang-ocaml/README.md index 798af91688d..263a48ebdff 100644 --- a/facebook-clang-plugins/clang-ocaml/README.md +++ b/facebook-clang-plugins/clang-ocaml/README.md @@ -1,8 +1,7 @@ - # Ocaml frontend to the Clang AST - Additional requirements: + - ocaml >= 4.02 - camlzip - yojson @@ -10,11 +9,13 @@ Additional requirements: - atdgen >= 2.0.0 The simplest way to install these dependencies is + 1) to install ocaml and opam using your system package manager (e.g. homebrew on MAC OS). 2) run 'opam install camlzip yojson atd atdgen' Assuming that the current dir is the root of the git repository and CLANG_PREFIX=/usr/local, you may compile and run tests with -``` + +```console export CLANG_PREFIX=/usr/local make -C clang-ocaml depend make -C clang-ocaml test @@ -34,6 +35,7 @@ Refer to [clang_ast_proj.mli.p](clang_ast_proj.mli.p) for a list of currently av ### Visitors The `Clang_ast_visit` module provides hooks to be run on AST nodes. Currently there is support for visitors in `Decl`, `Stmt`, `Type` and `SourceLocation` nodes. Here is basic example, that prints kinds of all decl and stmt nodes: + ```OCaml let print_decl _ decl = prerr (Clang_ast_proj.get_decl_kind_string decl) @@ -59,17 +61,16 @@ It's possible to extend existing OCaml variant types in the AST structure with m For example, see how [infer's frontend](https://github.com/facebook/infer/blob/8c6615963f79f03a644ae9087eb160da89a09a1a/infer/src/clang/clang_ast_extend.ml) uses this feature to extend `type_ptr`. - ## Implementation details High level: -- The plugin YojsonASTExporter defined in libtooling/ASTExporter.cpp outputs AST trees in an extended JSON format called "Yojson". Respectively, BiniouASTExporter outputs the AST in the "Biniou" format. +- The plugin YojsonASTExporter defined in libtooling/ASTExporter.cpp outputs AST trees in an extended JSON format called "Yojson". Respectively, BiniouASTExporter outputs the AST in the "Biniou" format. - Most of the ATD definitions are embedded in the C++ code of the ASTExporter. Refer to [ATD guidelines](../libtooling/ATD_GUIDELINES.md) for more information. - - We use scripts in libtooling/atdlib to extract and process the ATD definitions, then we use `atdgen` to generate the OCaml type definitions and json stub. Utility functions in `Clang_ast_proj`: + - This module relies heavily on the C preprocessor - it uses information from clang headers to generate OCaml code. - Clang provides `.inc` and `.def` files that provide information about available Node kinds. For example, [`TypeNode.def`](https://github.com/llvm-mirror/clang/blob/fe32c6a33461a8c60e18c0414d4844a47442328a/include/clang/AST/TypeNodes.def) contains information about all possible types that clang can produce. Internally clang uses the same headers. - In order to add new function, one needs to identify clang header that contains relevant information. Sometimes it's useful to read clang codebase to see how certain enums are generated - usually clang includes same headers to generate them. For example decl kind enum is [defined](https://github.com/llvm-mirror/clang/blob/c5dd58546ce4d20cd71cc26cb790e7f91c8f908f/include/clang/AST/DeclBase.h#L84-L91) by including `clang/AST/DeclNodes.inc` file. @@ -77,19 +78,23 @@ Utility functions in `Clang_ast_proj`: - If something doesn't work, `build/Clang_ast_proj.ml` will contain generated code. This way, it's easier to see what happens during macro expansion. Visitors: + - Implemented via [atdgen validation](https://mjambon.github.io/atdgen-doc/atdgen#field-validator) - Adding support for a new visitor requires changing ATD annotations in ASTExporter and modifying `Clang_ast_visit.ml` - Refer to existing visitors to see how it's done - It is possible to modify the current node inside a visitor as long as its fields are mutable Extensible variants: + - Implemented via [atdgen custom wrapper](https://mjambon.github.io/atdgen-doc/atdgen#field-t). It defines `type_ptr` to be extensible variant. - When looking at Yojson/Biniou output, `type_ptr` will be of type int. It's up to atdgen serializer to call `wrap`/`unwrap` Testing: + - The main program [`clang_ast_yojson_validator.ml`](clang_ast_yojson_validator.ml) is meant to parse, re-print, and compare yojson files emitted by ASTExporter. We use ydump (part of the yojson package) to normalize the original json and the re-emitted json before comparing them. - `clang_ast_main_test.ml` runs custom validators to confirm that visitors work as expected. Its output is recorded and checked into repository. ## ATD docs + https://mjambon.github.io/atdgen-doc/atdgen https://mjambon.github.io/atdgen-doc/atd-syntax diff --git a/facebook-clang-plugins/libtooling/ATD_GUIDELINES.md b/facebook-clang-plugins/libtooling/ATD_GUIDELINES.md index 4f44ffa1753..060aec6ddd2 100644 --- a/facebook-clang-plugins/libtooling/ATD_GUIDELINES.md +++ b/facebook-clang-plugins/libtooling/ATD_GUIDELINES.md @@ -1,5 +1,4 @@ -Guidelines for writing ATD annotations in ASTExporter.cpp -========================================================= +# Guidelines for writing ATD annotations in ASTExporter.cpp The ATD specifications inlined in ASTExporter.cpp are used to generate Ocaml parsers using `atdgen`. Those annotations must reflect closely the Yojson/Json/Biniou emitted by the C++ plugin. @@ -7,11 +6,11 @@ closely the Yojson/Json/Biniou emitted by the C++ plugin. The ATD language and the parser generating tool `atdgen` are documented here: https://atd.readthedocs.io/en/latest/atdgen.html -ATD basics ----------- +## ATD basics The definition of object in ASTExporter.cpp typically look like this: -``` + +```cpp //@atd type record = { //@atd mandatory_field : string //@atd ?optional_int : int option @@ -28,15 +27,15 @@ The `` annotations are currently required to disambigua made the first letters of the C++ types, except for a few exceptions (e.g. `CXX` is mapped to `x`). Valid Yojson values for this specification are for instance: -``` + +```json { "mandatory_field" : "foo" } { "mandatory_field" : "foo", "optional_int" : 3 } ``` -Simple example --------------- +## Simple example -``` +```cpp //@atd type source_location = { //@atd ?file : string option; //@atd ?line : int option; @@ -76,11 +75,11 @@ void ASTExporter::dumpSourceLocation(SourceLocation Loc) { Note that parser expects the C++ code to emit the corresponding fields in the same order. -More complex example --------------------- +## More complex example To get types of AST nodes, exporter relies on generated header files from clang. -``` + +```cpp //@atd type decl_ref = { //@atd kind : decl_kind; (* ATD type declared below *) //@atd ?name : string; @@ -128,7 +127,8 @@ void ASTExporter::dumpBareDeclRef(const Decl &D) { The complex definition for decl_kind is processed in several stages. First we use an adequate node of the clang preprocessor and expand the `#include ` to following code: -``` + +```cpp //@atd type decl_kind = [ //@atd | AccessSpec //@atd | Block @@ -138,7 +138,8 @@ First we use an adequate node of the clang preprocessor and expand the `#include ``` Then we extract the ATD specifications by looking for `//@atd`-style comments -``` + +```text type decl_kind = [ | AccessSpec | Block @@ -148,12 +149,12 @@ type decl_kind = [ ``` After calling `atdgen`, the final Ocaml type is: + ``` type decl_kind = `AccessSpec | `Block | `Captured | `ClassScopeFunctionSpecialization (* ... *) ``` -Testing -------- +## Testing Compiling with `DEBUG=1` will make the ATDWriter enforce the general well-formedness of the emitted Yojson/Json/Biniou. For instance, a missing tag will trigger an assert failure. @@ -163,8 +164,7 @@ It's is important to test both exporter (`make test`) and atd annotations (`make When changing the exporter, sometimes tests will fail due to exporting new information. To record this fact, run `make record-test-outputs` -Mapping clang AST nodes to ocaml values ---------------------------------------- +## Mapping clang AST nodes to ocaml values Clang AST entities of a given type are typically represented by a cluster of classes. @@ -176,15 +176,17 @@ before, we heavily rely on a (hacky) C-preprocessing stage and several scripts. Let us study how declarations are handled more precisely. Handling for statement and type nodes is very similar. -##### Default values for node tuples -``` +### Default values for node tuples + +```cpp #define DECL(DERIVED, BASE) //@atd #define @DERIVED@_decl_tuple @BASE@_tuple #define ABSTRACT_DECL(DECL) DECL #include ``` After one step of preprocessing + ATD-extraction, this creates the following intermediate code (see `build/ast_inline.atd.inc`) -``` + +```cpp #define access_spec_decl_tuple decl_tuple #define block_decl_tuple decl_tuple #define captured_decl_tuple decl_tuple @@ -197,7 +199,7 @@ This defines the default value of each `xxxx_decl_tuple` to be that of the base The `@...@` signs are processed by python macros in `libtooling/atdlib`. For instance, `@CaptureDecl@` gives `capture_decl`. -##### Overriding node tuples when outputting data +### Overriding node tuples when outputting data When the visiting method for nodes of given type is effectively written, it is expected that the corresponding `#define xxxx_decl_tuple` is overwritten to add the specific information of the kind of nodes. @@ -205,8 +207,7 @@ It is important to name tuples correctly. For example, for `SomeNewNodeDecl`, tu It is also required to specify how many fields tuple for given node has via `XxxTupleSize()` method -``` - +```cpp //@atd #define decl_tuple decl_info //@atd type decl_info = { //@atd (* ... *) @@ -241,11 +242,11 @@ void ASTExporter::VisitNamedDecl(const NamedDecl *D) { } ``` -##### Putting everything together +### Putting everything together The final definitions of the `xxx_decl_tuple` are meant to be inlined in the declaration of the actual sum type for all declarations. -``` +```cpp // main variant for declarations //@atd type decl = [ #define DECL(DERIVED, BASE) //@atd | DERIVED@@Decl of (@DERIVED@_decl_tuple) @@ -256,7 +257,8 @@ The final definitions of the `xxx_decl_tuple` are meant to be inlined in the dec ``` This expands first to: (see `build/ast_inline.atd.p`) -``` + +```text type decl = [ | AccessSpecDecl of (access_spec_decl_tuple) | BlockDecl of (block_decl_tuple) @@ -267,7 +269,8 @@ type decl = [ ``` Then after a last stage of preprocessing: (see `build/clang_ast.atd`) -``` + +```text type decl = [ AccessSpecDecl of (decl_info) | BlockDecl diff --git a/facebook-clang-plugins/libtooling/README.md b/facebook-clang-plugins/libtooling/README.md index 8eaa35e2180..d7f783fbbbf 100644 --- a/facebook-clang-plugins/libtooling/README.md +++ b/facebook-clang-plugins/libtooling/README.md @@ -1,13 +1,14 @@ - Front end plugins for Clang --------------------------- Assuming that the current dir is the root of the git repository and CLANG_PREFIX=/usr/local, you may compile and run tests with -``` + +```console export CLANG_PREFIX=/usr/local make -C libtooling test ``` More information: + - [`ATD_GUIDELINES`](https://github.com/facebook/infer/blob/main/facebook-clang-plugins/libtooling/ATD_GUIDELINES.md) for documentation about ASTExporter. - http://clang.llvm.org/docs/ClangPlugins.html for general documentation about clang plugins diff --git a/infer/documentation/checkers/Cost.md b/infer/documentation/checkers/Cost.md index f8df5bd31de..e3340e80710 100644 --- a/infer/documentation/checkers/Cost.md +++ b/infer/documentation/checkers/Cost.md @@ -6,10 +6,10 @@ analyses that are run by default) or `infer --cost-only` (which will only run co 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](/docs/checker-bufferoverrun) computes value ranges for instructions accessing memory - 2) a loop bound analysis determines upper bounds for the number of iterations of loops and generates constraints for nodes in the control-flow graph - 3) a constraint solving step resolves the constraints generated in the second step and computes an upper bound on the execution cost. @@ -17,32 +17,29 @@ The analysis computes symbolic upper bounds on the resource usage of programs— Most ideas behind this analysis are based on Stefan Bydge's PhD thesis [Static WCET Analysis based on Abstract Interpretation and Counting of Elements](https://www.semanticscholar.org/paper/Static-WCET-Analysis-Based-on-Abstract-and-Counting-Bygde/ee5157164d497725c1f42dc6c475a59a87c99957). 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 - 2) allocation cost - 3) 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 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 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. +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) @@ -68,22 +65,21 @@ void loop(ArrayList list){ 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`](/docs/next/all-issue-types#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. + +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](/docs/checker-bufferoverrun) '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](/docs/next/all-issue-types#infinite_execution_time) for details. diff --git a/infer/documentation/checkers/LithoRequiredProps.md b/infer/documentation/checkers/LithoRequiredProps.md index 3a9e875006e..41a771312af 100644 --- a/infer/documentation/checkers/LithoRequiredProps.md +++ b/infer/documentation/checkers/LithoRequiredProps.md @@ -1,7 +1,7 @@ This analysis checks that all non-optional [`@Prop`](https://fblitho.com/docs/props)`s have been specified when constructing Litho components. This is a [Litho](https://fblitho.com/) 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 @@ -31,4 +31,4 @@ If the required props are not called, then annotation processor throws an except 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](/docs/next/all-issue-types#missing_required_prop). \ No newline at end of file +Check out the examples defined in the issue type [MISSING_REQUIRED_PROP](/docs/next/all-issue-types#missing_required_prop). diff --git a/infer/documentation/checkers/Pulse.md b/infer/documentation/checkers/Pulse.md index 13aae741936..b0772249df0 100644 --- a/infer/documentation/checkers/Pulse.md +++ b/infer/documentation/checkers/Pulse.md @@ -28,6 +28,7 @@ class Registry { ``` How to run pulse for Java: + ```bash infer run --pulse -- javac Test.java ``` @@ -84,6 +85,7 @@ void false_positive(int *x) { ``` 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 diff --git a/infer/documentation/checkers/Purity.md b/infer/documentation/checkers/Purity.md index 2313160cdd3..e1a8c4877c1 100644 --- a/infer/documentation/checkers/Purity.md +++ b/infer/documentation/checkers/Purity.md @@ -2,10 +2,10 @@ This is an experimental inter-procedural analysis that detects pure (side-effect 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`](/docs/next/all-issue-types#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. @@ -14,7 +14,7 @@ Too see the issue with the first point, consider the following simple program: ```java void foo(Foo a){ Foo b = a; - b.x = 10; + b.x = 10; } ``` @@ -36,11 +36,9 @@ boolean contains(Integer i, ArrayList list){ 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](/docs/next/checker-impurity) analysis which uses [pulse](/docs/next/checker-pulse) which can successfully analyze this program as pure \o/ - The analysis is used by: -- [Loop-hoisting](/docs/next/checker-loop-hoisting) analysis which identifies loop-invariant function calls, i.e. functions that are pure and have loop-invariant arguments. +- [Loop-hoisting](/docs/next/checker-loop-hoisting) analysis which identifies loop-invariant function calls, i.e. functions that are pure and have loop-invariant arguments. - [Cost](/docs/next/checker-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). diff --git a/infer/documentation/checkers/RacerD.md b/infer/documentation/checkers/RacerD.md index 3fe81110a3b..0b085667995 100644 --- a/infer/documentation/checkers/RacerD.md +++ b/infer/documentation/checkers/RacerD.md @@ -1,5 +1,5 @@ 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 +explanation of how the analysis works _for Java code_, but may be less complete than the [Thread Safety Violation bug description page](/docs/next/all-issue-types#thread_safety_violation). For information on C++ and Objective C, see the [Lock Consistency violation page](/docs/next/all-issue-types#lock_consistency_violation). @@ -49,7 +49,7 @@ 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: -``` +```java @ThreadSafe public class Dinner { private int mTemperature; @@ -79,7 +79,7 @@ with `@ThreadSafe(enableChecks = false)`. We sometimes need to protect read accesses as well as writes. Consider the following class with unsynchronized methods. -``` +```java @ThreadSafe public class Account { @@ -123,7 +123,7 @@ to wrap both read and write accesses, or to use an `AtomicInteger` for In the following code, RacerD will report an `Interface not thread-safe` warning on the call to `i.bar()`: -``` +```java interface I { void bar(); } @@ -175,7 +175,7 @@ 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. -``` +```java List mCache; @ThreadConfined(UI) @@ -203,7 +203,7 @@ itself. Not all races are bugs; a race can be benign. Consider the following: -``` +```java @Functional Boolean askNetworkIfShouldShowFeature(); private Boolean mShouldShowFeature; @@ -238,7 +238,7 @@ RacerD to understand that this particular code is safe, though it will still Be sure not to use the `@Functional` pattern for _singleton instantiation_, as it's possible the "singleton" can be constructed more than once. -``` +```java public class MySingleton { private static sInstance; @@ -260,7 +260,7 @@ 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: -``` +```java @ThreadSafe public interface Car { @ReturnsOwnership abstract Car buyCar(); @@ -284,7 +284,7 @@ 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: -``` +```java @VisibleForTesting void setF() { this.f = ...; // RacerD would normally warn here, but @VisibleForTesting will silence the warning } @@ -305,7 +305,7 @@ several procedure calls. It handles this even between classes and between files. Here is a very basic example -``` +```java @ThreadSafe class A{ @@ -329,7 +329,7 @@ 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. -``` +```console 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 @@ -344,9 +344,9 @@ InterProc.java:17: error: THREAD_SAFETY_VIOLATION 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()' and`meth()' include information as follows. +summaries for `m1()` and `meth()` include information as follows. -``` +```console Procedure: void A.m1(B) Accesses: { Unprotected({ 1 }) -> { Write to &bb.B.x at void B.meth_write() at line 17 } } @@ -460,7 +460,7 @@ 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! -``` +```java @ThreadSafe public class SynchronizedList { synchronized boolean isEmpty() { ... } diff --git a/infer/documentation/checkers/Starvation.md b/infer/documentation/checkers/Starvation.md index 55643eedb6c..ac83bb88af4 100644 --- a/infer/documentation/checkers/Starvation.md +++ b/infer/documentation/checkers/Starvation.md @@ -1,4 +1,5 @@ Detect several kinds of "starvation" problems: + - deadlocks - violations of `@Lockless` annotations - violations of [Android's "strict mode"](https://developer.android.com/reference/android/os/StrictMode) diff --git a/infer/documentation/checkers/Topl.md b/infer/documentation/checkers/Topl.md index 891537bea2f..92f8d97f163 100644 --- a/infer/documentation/checkers/Topl.md +++ b/infer/documentation/checkers/Topl.md @@ -15,7 +15,7 @@ property Taint 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: -``` +```java public class Main { static void f() { g(tito(source())); } static void g(Object x) { h(x); } @@ -28,13 +28,13 @@ public class Main { 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: -``` +```console infer --topl --topl-properties taint.topl -- javac Main.java ``` It will display the following error: -``` +```console Main.java:2: error: Topl Error property Taint reaches state error. 1. public class Main { @@ -45,7 +45,7 @@ Main.java:2: error: Topl Error To get a full trace, use the command -``` +```console infer explore ``` @@ -82,12 +82,13 @@ Otherwise, the label on a transition contains: 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*. + * 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 @@ -100,5 +101,5 @@ For several examples, see https://github.com/facebook/infer/tree/main/infer/test * 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. + * 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. diff --git a/infer/documentation/issues/ARBITRARY_CODE_EXECUTION_UNDER_LOCK.md b/infer/documentation/issues/ARBITRARY_CODE_EXECUTION_UNDER_LOCK.md index 5730b489d01..401435e80f8 100644 --- a/infer/documentation/issues/ARBITRARY_CODE_EXECUTION_UNDER_LOCK.md +++ b/infer/documentation/issues/ARBITRARY_CODE_EXECUTION_UNDER_LOCK.md @@ -2,6 +2,7 @@ A call that may execute arbitrary code (such as registered, or chained, callback This code may deadlock whenever the callbacks obtain locks themselves, so it is an unsafe pattern. Example: + ```java SettableFuture future = null; diff --git a/infer/documentation/issues/BAD_ARG.md b/infer/documentation/issues/BAD_ARG.md index 59cb8a7b96e..30155aacffd 100644 --- a/infer/documentation/issues/BAD_ARG.md +++ b/infer/documentation/issues/BAD_ARG.md @@ -1,6 +1,7 @@ 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 @@ -8,6 +9,7 @@ f() -> 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] diff --git a/infer/documentation/issues/BAD_KEY.md b/infer/documentation/issues/BAD_KEY.md index 0b42607d411..6a918e27957 100644 --- a/infer/documentation/issues/BAD_KEY.md +++ b/infer/documentation/issues/BAD_KEY.md @@ -1,6 +1,7 @@ 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 = #{}, diff --git a/infer/documentation/issues/BAD_MAP.md b/infer/documentation/issues/BAD_MAP.md index 05f78b20348..1104dde5774 100644 --- a/infer/documentation/issues/BAD_MAP.md +++ b/infer/documentation/issues/BAD_MAP.md @@ -1,6 +1,7 @@ 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], diff --git a/infer/documentation/issues/BAD_RECORD.md b/infer/documentation/issues/BAD_RECORD.md index 2601d781451..77622c9a3bb 100644 --- a/infer/documentation/issues/BAD_RECORD.md +++ b/infer/documentation/issues/BAD_RECORD.md @@ -1,6 +1,8 @@ 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). +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}). diff --git a/infer/documentation/issues/BAD_RETURN.md b/infer/documentation/issues/BAD_RETURN.md index c941665d2c6..ae3785bbc71 100644 --- a/infer/documentation/issues/BAD_RETURN.md +++ b/infer/documentation/issues/BAD_RETURN.md @@ -1,6 +1,7 @@ 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. diff --git a/infer/documentation/issues/BUFFER_OVERRUN.md b/infer/documentation/issues/BUFFER_OVERRUN.md index 8ed667268d3..397e0f76e1a 100644 --- a/infer/documentation/issues/BUFFER_OVERRUN.md +++ b/infer/documentation/issues/BUFFER_OVERRUN.md @@ -6,23 +6,17 @@ For example, `int a[3]; a[5] = 42;` generates a `BUFFER_OVERRUN_L1` on `a[5] = 4 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. +* `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. diff --git a/infer/documentation/issues/CAPTURED_STRONG_SELF.md b/infer/documentation/issues/CAPTURED_STRONG_SELF.md index ca7a3786a30..aba3f51ad49 100644 --- a/infer/documentation/issues/CAPTURED_STRONG_SELF.md +++ b/infer/documentation/issues/CAPTURED_STRONG_SELF.md @@ -6,18 +6,17 @@ This will happen in one of two cases generally: 1. One uses `weakSelf` but forgot to declare it weak first. -Example: + 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;`. + ```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;`. 2. 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 @@ -26,7 +25,7 @@ Example: Example: -```objectivec + ```objectivec __weak __typeof(self) weakSelf = self; int (^my_block)() = ^() { __strong typeof(self) strongSelf = weakSelf; @@ -39,33 +38,33 @@ Example: } ... }; -``` + ``` -In this example, `strongSelf` is a captured variable of the inner block, and this could cause retain cycles. + 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: + **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; + ```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. + 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: + 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 + ```objectivec __weak __typeof(self) weakSelf = self; int (^my_block)() = ^() { __strong typeof(self) strongSelf = weakSelf; @@ -79,4 +78,4 @@ Another solution could be to copy the instance variable that one needs to access } ... }; -``` + ``` diff --git a/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE.md b/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE.md index 25e243f358d..1c1b536129d 100644 --- a/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE.md +++ b/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE.md @@ -3,5 +3,3 @@ 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](/docs/next/checker-cost#examples). - - diff --git a/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD.md b/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD.md index 7567476ca9a..80d9561b4f5 100644 --- a/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD.md +++ b/infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD.md @@ -8,4 +8,3 @@ Infer considers a method as running on the UI thread whenever: etc. - The method or its callees call a `Litho.ThreadUtils` method such as `assertMainThread`. - diff --git a/infer/documentation/issues/EXECUTION_TIME_UNREACHABLE_AT_EXIT.md b/infer/documentation/issues/EXECUTION_TIME_UNREACHABLE_AT_EXIT.md index 57e06958bf4..7b612ad76c1 100644 --- a/infer/documentation/issues/EXECUTION_TIME_UNREACHABLE_AT_EXIT.md +++ b/infer/documentation/issues/EXECUTION_TIME_UNREACHABLE_AT_EXIT.md @@ -2,8 +2,8 @@ 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 diff --git a/infer/documentation/issues/EXPENSIVE_EXECUTION_TIME.md b/infer/documentation/issues/EXPENSIVE_EXECUTION_TIME.md index f4050bbf5b1..6072b8a649e 100644 --- a/infer/documentation/issues/EXPENSIVE_EXECUTION_TIME.md +++ b/infer/documentation/issues/EXPENSIVE_EXECUTION_TIME.md @@ -1,6 +1,7 @@ \[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](https://github.com/facebook/infer/blob/main/infer/src/base/costKind.ml#L55). For instance, a simple example where we report this issue is a function with linear cost: + ```java int sum_linear(ArrayList list){ int sum = 0; diff --git a/infer/documentation/issues/IMPURE_FUNCTION.md b/infer/documentation/issues/IMPURE_FUNCTION.md index 647e0bdd75b..d58c3784fca 100644 --- a/infer/documentation/issues/IMPURE_FUNCTION.md +++ b/infer/documentation/issues/IMPURE_FUNCTION.md @@ -1,4 +1,5 @@ This issue type indicates impure functions. For instance, below functions would be marked as impure: + ```java void makeAllZero_impure(ArrayList list) { Iterator listIterator = list.iterator(); diff --git a/infer/documentation/issues/INEFFICIENT_KEYSET_ITERATOR.md b/infer/documentation/issues/INEFFICIENT_KEYSET_ITERATOR.md index dbac7f8b11e..5d7e6585947 100644 --- a/infer/documentation/issues/INEFFICIENT_KEYSET_ITERATOR.md +++ b/infer/documentation/issues/INEFFICIENT_KEYSET_ITERATOR.md @@ -1,4 +1,5 @@ This issue is raised when + - iterating over a HashMap with `ketSet()` iterator - looking up the key each time @@ -16,7 +17,7 @@ void inefficient_loop_bad(HashMap testMap) { **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 testMap) { for (Map.Entry entry : testMap.entrySet()) { diff --git a/infer/documentation/issues/INFINITE_AUTORELEASEPOOL_SIZE.md b/infer/documentation/issues/INFINITE_AUTORELEASEPOOL_SIZE.md index 55d99820b09..184198322f1 100644 --- a/infer/documentation/issues/INFINITE_AUTORELEASEPOOL_SIZE.md +++ b/infer/documentation/issues/INFINITE_AUTORELEASEPOOL_SIZE.md @@ -2,4 +2,3 @@ the Objective-C's autoreleasepool size in the procedure. This issuee type is similar to [INFINITE_EXECUTION_COST](#infinite_execution_time), with the difference that rather than the execution cost, we account for the size of the Objective-C autoreleasepool size. By default, this issue type is disabled. - diff --git a/infer/documentation/issues/INFINITE_EXECUTION_TIME.md b/infer/documentation/issues/INFINITE_EXECUTION_TIME.md index 458c2900041..609bb2273b4 100644 --- a/infer/documentation/issues/INFINITE_EXECUTION_TIME.md +++ b/infer/documentation/issues/INFINITE_EXECUTION_TIME.md @@ -7,6 +7,7 @@ issue type is disabled. 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) { @@ -16,20 +17,23 @@ void square_root_FP(int x) { } } ``` -### 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, + +### 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](https://github.com/facebook/infer/blob/main/infer/src/bufferoverrun/bufferOverrunModels.ml). +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](https://github.com/facebook/infer/blob/main/infer/src/bufferoverrun/bufferOverrunModels.ml). ### 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 @@ -38,4 +42,3 @@ void call_top_cost_FP() { square_root_FP(1); // square_root_FP has Top cost } ``` - diff --git a/infer/documentation/issues/INTEGER_OVERFLOW.md b/infer/documentation/issues/INTEGER_OVERFLOW.md index 7d8be846bff..b42d1711878 100644 --- a/infer/documentation/issues/INTEGER_OVERFLOW.md +++ b/infer/documentation/issues/INTEGER_OVERFLOW.md @@ -5,14 +5,14 @@ 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. +* `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. +* `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. +* `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. +* `U5`: A binary integer operation is unsafe by unknown values, which are usually from unknown + function calls. diff --git a/infer/documentation/issues/INVARIANT_CALL.md b/infer/documentation/issues/INVARIANT_CALL.md index 45561cf26d5..68695308796 100644 --- a/infer/documentation/issues/INVARIANT_CALL.md +++ b/infer/documentation/issues/INVARIANT_CALL.md @@ -1,4 +1,5 @@ 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 diff --git a/infer/documentation/issues/MISSING_REQUIRED_PROP.md b/infer/documentation/issues/MISSING_REQUIRED_PROP.md index 4e10ef23daa..a476ec4ca81 100644 --- a/infer/documentation/issues/MISSING_REQUIRED_PROP.md +++ b/infer/documentation/issues/MISSING_REQUIRED_PROP.md @@ -1,6 +1,5 @@ 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. @@ -48,7 +47,6 @@ MyComponent.create(c) or alternatively, if the `prop2` is not really required, we could change the component spec to reflect that: - ```java class MyComponentSpec { @@ -59,4 +57,4 @@ class MyComponentSpec { } ... } -``` \ No newline at end of file +``` diff --git a/infer/documentation/issues/MODIFIES_IMMUTABLE.md b/infer/documentation/issues/MODIFIES_IMMUTABLE.md index c3b3779cd5d..c633758d9b4 100644 --- a/infer/documentation/issues/MODIFIES_IMMUTABLE.md +++ b/infer/documentation/issues/MODIFIES_IMMUTABLE.md @@ -1,11 +1,12 @@ 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; diff --git a/infer/documentation/issues/NO_MATCHING_BRANCH_IN_TRY.md b/infer/documentation/issues/NO_MATCHING_BRANCH_IN_TRY.md index e85ac352999..49278ff362a 100644 --- a/infer/documentation/issues/NO_MATCHING_BRANCH_IN_TRY.md +++ b/infer/documentation/issues/NO_MATCHING_BRANCH_IN_TRY.md @@ -1,6 +1,7 @@ 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 diff --git a/infer/documentation/issues/NO_MATCHING_CASE_CLAUSE.md b/infer/documentation/issues/NO_MATCHING_CASE_CLAUSE.md index 7489b5c2940..74f49ed33e7 100644 --- a/infer/documentation/issues/NO_MATCHING_CASE_CLAUSE.md +++ b/infer/documentation/issues/NO_MATCHING_CASE_CLAUSE.md @@ -1,6 +1,7 @@ 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 diff --git a/infer/documentation/issues/NO_MATCHING_FUNCTION_CLAUSE.md b/infer/documentation/issues/NO_MATCHING_FUNCTION_CLAUSE.md index 3dc7709c01e..e2c95554d66 100644 --- a/infer/documentation/issues/NO_MATCHING_FUNCTION_CLAUSE.md +++ b/infer/documentation/issues/NO_MATCHING_FUNCTION_CLAUSE.md @@ -1,6 +1,7 @@ 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. ``` diff --git a/infer/documentation/issues/NO_TRUE_BRANCH_IN_IF.md b/infer/documentation/issues/NO_TRUE_BRANCH_IN_IF.md index 9462891a71d..aa52421cfce 100644 --- a/infer/documentation/issues/NO_TRUE_BRANCH_IN_IF.md +++ b/infer/documentation/issues/NO_TRUE_BRANCH_IN_IF.md @@ -1,6 +1,7 @@ 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 diff --git a/infer/documentation/issues/NULL_ARGUMENT.md b/infer/documentation/issues/NULL_ARGUMENT.md index 86a58942c1d..bad95a4e33d 100644 --- a/infer/documentation/issues/NULL_ARGUMENT.md +++ b/infer/documentation/issues/NULL_ARGUMENT.md @@ -1,4 +1,4 @@ -```objc +```objectivec This issue type indicates `nil` being passed as argument where a non-nil value expected. #import @@ -7,7 +7,7 @@ This issue type indicates `nil` being passed as argument where a non-nil value e NSString* stringNotNil(NSString* str) { if (!str) { // ERROR: NSString:stringWithString: expects a non-nil value - return [NSString stringWithString:nil]; + return [NSString stringWithString:nil]; } return str; } diff --git a/infer/documentation/issues/PULSE_TRANSITIVE_ACCESS.md b/infer/documentation/issues/PULSE_TRANSITIVE_ACCESS.md index 72b8bbb53f3..eb042be1ace 100644 --- a/infer/documentation/issues/PULSE_TRANSITIVE_ACCESS.md +++ b/infer/documentation/issues/PULSE_TRANSITIVE_ACCESS.md @@ -2,6 +2,5 @@ This issue tracks spurious accesses that are reachable from specific entry funct Spurious accesses are specified as specific load/calls. -Entry functions are specified through their enclosing class that must extend a specific +Entry functions are specified through their enclosing class that must extend a specific class and should not extend a list of specific classes. - diff --git a/infer/documentation/issues/PULSE_UNNECESSARY_COPY.md b/infer/documentation/issues/PULSE_UNNECESSARY_COPY.md index fd86aeb0c52..ad1dda9fe53 100644 --- a/infer/documentation/issues/PULSE_UNNECESSARY_COPY.md +++ b/infer/documentation/issues/PULSE_UNNECESSARY_COPY.md @@ -16,4 +16,4 @@ int use_reference_instead(A& x){ auto& y = x; // copy the ref only return y.a; } -``` \ No newline at end of file +``` diff --git a/infer/documentation/issues/PULSE_UNNECESSARY_COPY_INTERMEDIATE.md b/infer/documentation/issues/PULSE_UNNECESSARY_COPY_INTERMEDIATE.md index 9248583039b..5281e5d5bfc 100644 --- a/infer/documentation/issues/PULSE_UNNECESSARY_COPY_INTERMEDIATE.md +++ b/infer/documentation/issues/PULSE_UNNECESSARY_COPY_INTERMEDIATE.md @@ -9,17 +9,15 @@ void callee(ExpensiveObject obj) { void caller() { callee(myExpensiveObj); // a copy of myExpensiveObj is created - // the copy is destroyed right after the call + // 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))`. - +- `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. \ No newline at end of file +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. diff --git a/infer/documentation/issues/PULSE_UNNECESSARY_COPY_MOVABLE.md b/infer/documentation/issues/PULSE_UNNECESSARY_COPY_MOVABLE.md index 7620d7a5fc8..e88d3e01a62 100644 --- a/infer/documentation/issues/PULSE_UNNECESSARY_COPY_MOVABLE.md +++ b/infer/documentation/issues/PULSE_UNNECESSARY_COPY_MOVABLE.md @@ -1,4 +1,5 @@ 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. @@ -24,4 +25,4 @@ class Test { }; -``` \ No newline at end of file +``` diff --git a/infer/documentation/issues/RESOURCE_LEAK.md b/infer/documentation/issues/RESOURCE_LEAK.md index 1403702131d..6ffea8fb88a 100644 --- a/infer/documentation/issues/RESOURCE_LEAK.md +++ b/infer/documentation/issues/RESOURCE_LEAK.md @@ -18,14 +18,14 @@ This is an example of a resource leak in C code: For the remaining of this section, we will consider examples of resource leaks in Java code. -TIP: A common source of bugs is exceptions skipping past close() -statements. That is the first thing to look for if INFER reports a potential +TIP: A common source of bugs is **exceptions skipping past close() +statements**. That is the first thing to look for if INFER reports a potential resource leak. ### Basics and Standard Idiom -Some objects in Java, the resources, are supposed to be closed when you -stop using them, and failure to close is a resource leak. Resources +Some objects in Java, the *resources*, are supposed to be closed when you +stop using them, and failure to close is a *resource leak*. Resources include input streams, output streams, readers, writers, sockets, http connections, cursors, and json parsers. @@ -263,7 +263,7 @@ legitimate to simply convert the code over to try-with-resources if you have access to Java 7, so as to save yourself some brain-cycles. You will also end up with cleaner code. -If try-with-resources is so great you should always use it. But you +If try-with-resources is so great you should *always* use it. But you shouldn't… Try-with-resources gives resources static scoping, and works via a stack discipline. Sometimes, you want a resource to persist beyond scope, as in the escaping example above. In an escaping example maybe you could refactor lots diff --git a/infer/documentation/issues/SCOPE_LEAKAGE.md b/infer/documentation/issues/SCOPE_LEAKAGE.md index 88b4e9a7dbe..bee319745ba 100644 --- a/infer/documentation/issues/SCOPE_LEAKAGE.md +++ b/infer/documentation/issues/SCOPE_LEAKAGE.md @@ -5,8 +5,9 @@ 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)\}: +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 { diff --git a/infer/src/erlang/README.md b/infer/src/erlang/README.md index 63d7d932f54..e085a995f2e 100644 --- a/infer/src/erlang/README.md +++ b/infer/src/erlang/README.md @@ -8,22 +8,24 @@ Also, make sure that the Erlang compiler `erlc` is installed. To see the error "no match of rhs" put the following in a file `ex1.erl`: - - -module(ex1). - -export([bad/0, good/0]). - bad() -> - [H | _] = get_list(0), - H. - good() -> - [H | _] = get_list(2), - H. - get_list(X) when X =< 0 -> []; - get_list(X) when X > 0 -> [X | get_list(X - 1)]. - +```erlang +-module(ex1). +-export([bad/0, good/0]). +bad() -> + [H | _] = get_list(0), + H. +good() -> + [H | _] = get_list(2), + H. +get_list(X) when X =< 0 -> []; +get_list(X) when X > 0 -> [X | get_list(X - 1)]. +``` Then run Infer with the following command: - infer --pulse-only -- erlc ex1.erl +```console +infer --pulse-only -- erlc ex1.erl +``` ## User-Specified Properties @@ -31,26 +33,30 @@ Then run Infer with the following command: Put the following in a file called `WriteAfterClose.topl`: +``` property WriteAfterClose start -> start: * start -> closed: "file:close/1"(A,Ret) => f:=A closed -> error: "file:write/2"(F,D,Ret) when F==f +``` Put the following in a file called `ex2.erl`: - -module(ex2). - -export([bad/1,good/1]). - good(F) -> nop(F), file:write(F, "hi"). - bad(F) -> op(F), file:write(F, "hi"). - nop(_) -> ok. - op(F) -> file:close(F). +```erlang +-module(ex2). +-export([bad/1,good/1]). +good(F) -> nop(F), file:write(F, "hi"). +bad(F) -> op(F), file:write(F, "hi"). +nop(_) -> ok. +op(F) -> file:close(F). +``` Run the following command: - infer --topl-only --topl-properties WriteAfterClose.topl -- erlc ex2.erl - +```console +infer --topl-only --topl-properties WriteAfterClose.topl -- erlc ex2.erl +``` ### Taint ### Taint with Transformations - diff --git a/infer/src/labs/README.md b/infer/src/labs/README.md index cf1f05526da..ad21cbf428d 100644 --- a/infer/src/labs/README.md +++ b/infer/src/labs/README.md @@ -18,15 +18,15 @@ Using Docker is the fastest way: you do not need to clone the Infer repository a 3. Within Docker, pull the latest version of infer, copy the /infer directory to your mount point, then fully build infer once: -```shell -cd /infer -git branch --unset-upstream -git pull -git branch --set-upstream-to=origin/main master -git pull -cp -av /infer/. /infer-host -make -C /infer-host -j 4 -``` + ```shell + cd /infer + git branch --unset-upstream + git pull + git branch --set-upstream-to=origin/main master + git pull + cp -av /infer/. /infer-host + make -C /infer-host -j 4 + ``` 4. Outside Docker, you will likely need to change the permissions of `$HOME/infer-docker` to make the files editable by your user: `sudo chown $USER -R $HOME/infer-docker`. @@ -45,12 +45,11 @@ For Java, ensure that you have the following jar files in your `$CLASSPATH`: - infer/lib/java/android/android-23.jar - infer/dependencies/java/sun-tools/tools.jar - ## (1) Warm up: running, testing, and debugging Infer (a) Change to the test directory (`cd infer/tests/codetoanalyze/java/lab`) and run infer in its default configuration: -``` +```console infer -- javac Leaks.java ``` @@ -58,13 +57,13 @@ Infer should report 7 resource leaks. These reports come from the separation log (b) Run the analyzer on a single test file to produce the debug HTML: -``` +```console infer -g --resource-leak-lab-only -- javac Leaks.java ``` Then, open the debug HTML: -``` +```console firefox infer-out/captured/*.html ``` @@ -118,7 +117,6 @@ include AbstractDomain.TopLifted (FiniteBounds) - Hint#2: use `open AbstractDomain.Types` to be able to write, e.g., `Top` instead of `AbstractDomain.Top`. - ## (4) Interprocedural analysis Augment the summary type with state to indicate whether the current procedure returns a resource. Allowing a resource to escape to the caller should not be considered a leak. Use this information in callers too by reading from the callee's summary. Use the `analyze_dependency` field of the `InterproceduralAnalysis.t` record passed to the analysis like so: @@ -145,19 +143,14 @@ Hint: What do return values look like in infer? They are assignments to a specia Then `ret_var` is the return variable (if `Var.is_return ret_var` returns true), of type `ret_typename` (really `ret_typename*` in infer's intermediate representation). - ## (5) Access paths (a) Change the simple counting domain to a domain that overapproximates the set of storage locations that hold a resource. As a concrete goal, the new domain should allow you to print the name of the resource(s) that leak in the error message (rather than just the number of resources). The new domain should also allow your analysis to get the correct answer on your false negative and false positive tests from 2(d) and 2(e). Think about the following questions when designing your new domain: - How should we abstract storage locations? Is abstracting the stack program variables (`Var.t`) enough, or do we need an abstraction of the heap as well? - - How will we handle aliasing (storage locations that store the same address)? More precisely, how to handle assignement? We will need to make some simplifying assumptions and cut some corners here. Developing a full memory model that accounts for aliasing perfectly is out of the scope of this lab (check out how the Pulse analysis does it!). - - Will it be easy to extend the domain to incorporate information from the callee summaries/represent state that will be instantiated by callers? - - Some modules that might be useful in creating your new domain (depending on what approach you choose): `AbstractDomain.FiniteSet`, `AbstractDomain.Map`, `AccessPath`, `Var`, `FormalMap`. - - It's okay for the domain to diverge in certain cases for the purpose of this lab. Can you write a method that would make your checker diverge? (b) Write some tests that demonstrate the limitations of your new domain: both false positives (names prefixed with `FP_` and false negatives (prefixed with `FN_`). Add them to [LeaksAccessPaths.java](https://github.com/facebook/infer/blob/main/infer/tests/codetoanalyze/java/lab/LeaksAccessPath.java). @@ -166,13 +159,13 @@ Then `ret_var` is the return variable (if `Var.is_return ret_var` returns true), Hint: You will find the `FormalMap` module useful for this. This module lets you go back and forth between the index of a formal and its name. This utility module is also used in the `RacerD` and `TaintAnalysis` modules. - ## (6) Making it practical (a) Real resource leaks frequently involve failing to close resources along exceptional control-flow paths. For simplicity, the initial version of the current analysis uses a filtered view of the CFG that skips exceptional edges (`ProcCfg.Normal`). To find more bugs, you might want to switch to using `ProcCfg.Exceptional` and make sure that your analysis gets the right answer on some realistic exception examples like [LeaksExceptions.java](https://github.com/facebook/infer/blob/main/infer/tests/codetoanalyze/java/lab/LeaksExceptions.java). (b) Try running on real code! The instructions [here](http://fm.csl.sri.com/SSFT17/infer-instr.html) have several suggestions for open-source Android apps to point your analysis at. Try `./gradlew assembleDebug -x test` first to make sure everything builds correctly without Infer (if not, you are probably missing some dependencies--the error messages should guide you). Once that's working, try `./gradlew clean; infer run --resource-leak-lab-only -- ./gradlew assembleDebug -x test`. + - Found a real bug? Bonus points! Send a pull request to fix it! Very frequently, the best fix is to use try-with-resources. - Found a false positive in your analysis? Try re-running Infer with `--debug` and see if you can narrow down the root cause/fix it. - How does your analysis compare to Infer's production resource leak analysis? Run with `infer -- ` to see if your analysis finds bugs that Infer misses, or vice versa. diff --git a/infer/tests/codetoanalyze/erlang/README.md b/infer/tests/codetoanalyze/erlang/README.md index 0129b1089a4..c2bdf3b7369 100644 --- a/infer/tests/codetoanalyze/erlang/README.md +++ b/infer/tests/codetoanalyze/erlang/README.md @@ -3,6 +3,7 @@ ## Directories Put the test in the folder based on the analyzer that is being tested: + - Pulse: `pulse` or `pulse-otp` if OTP specs (`--erlang-with-otp-specs`) are needed. - Topl: `topl`. - Create new files/directories as needed. @@ -11,11 +12,13 @@ Put the test in the folder based on the analyzer that is being tested: ## Naming Test functions should be named `(fp_|fpl_|fn_|fnl_)?test_.*_(Ok|Latent|Bad)`, where the suffix (`_Ok`, `_Bad`, `_Latent`) indicates the expected outcome: + - `_Ok` means that no issue is expected, - `_Bad` means that a (manifest) issue is expected, - `_Latent` means that a [latent issue](https://fbinfer.com/docs/next/checker-pulse/#latent-issues) is expected (e.g. because the function has arguments). The prefixes (`fp_`, `fpl_`, `fn_`, `fnl_`) correspond to deviations with the reported output: + - `fp_` means a false positive: no issue, or a latent issue was expected, but Infer reports a manifest issue. - `fpl_` is false positive latent, meaning that no issue was expected but a latent one is reported. - `fn_` means a false negative: manifest or latent issue is expected, but no issue is reported. diff --git a/website/README.md b/website/README.md index 950c635fccc..9e122c12501 100644 --- a/website/README.md +++ b/website/README.md @@ -2,37 +2,37 @@ This website is built using Docusaurus 3, a modern static website generator. -### Installation +## Installation NOTE: On Debian, you likely want to use `corepack yarn` (yarn "classic") instead of `yarn`, e.g. `corepack yarn start`. -``` -$ yarn +```console +yarn ``` -### Local Development +## Local Development -``` -$ yarn start +```console +yarn start ``` This command starts a local development server and open up a browser window. Most changes are reflected live without having to restart the server. -### Build +## Build -``` -$ yarn build +```console +yarn build ``` This command generates static content into the `build` directory and can be served using any static contents hosting service. -### Deployment +## Deployment -``` -$ GIT_USER= USE_SSH=1 yarn deploy +```console +GIT_USER= USE_SSH=1 yarn deploy ``` If you are using GitHub pages for hosting, this command is a convenient way to diff --git a/website/docs/00-hello-world.md b/website/docs/00-hello-world.md index 63946e8d86c..14e92d7b9bc 100644 --- a/website/docs/00-hello-world.md +++ b/website/docs/00-hello-world.md @@ -81,7 +81,7 @@ infer run -- clang -c Hello.m You should see the following error reported by Infer. -``` +```console Hello.m:10 NULL_DEREFERENCE pointer hello last assigned on line 9 could be null and is dereferenced at line 10, column 12 ``` @@ -120,7 +120,7 @@ infer run -- gcc -c hello.c You should see the following error reported by Infer. -``` +```console hello.c:5: error: NULL_DEREFERENCE pointer s last assigned on line 4 could be null and is dereferenced at line 5, column 10 ``` @@ -217,7 +217,6 @@ There are three solutions to remedy this: This causes gradle to recompile everything each time, and subsequently Infer to capture all the files again. - 2. Run Infer indicating that the capture of compilation commands should continue, using option `--continue` (or `-c` for short). @@ -225,9 +224,8 @@ There are three solutions to remedy this: infer run --continue -- ./gradlew build ``` -This makes Infer add the effects of the new compilation commands to the previous + This makes Infer add the effects of the new compilation commands to the previous ones, and start a new analysis of the entire code. - 3. Run Infer in reactive mode after a code change, using option `--reactive` (or `-r` for short). @@ -248,13 +246,13 @@ Go to the sample iOS app in [`infer/examples/ios_hello`](https://github.com/facebook/infer/tree/main/examples/ios_hello/) and run Infer on it: -```bash +```console infer run -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator ``` Infer will output the list of found bugs: -```bash +```console AppDelegate.m:20: error: MEMORY_LEAK memory dynamically allocated to shadowPath by call to CGPathCreateWithRect() at line 20, column 28 is not reachable after line 20, column 5 @@ -285,14 +283,14 @@ 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 +```console 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 +```console xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator clean ``` @@ -302,13 +300,13 @@ Go to the sample C project in [`infer/examples/c_hello`](https://github.com/facebook/infer/tree/main/examples/c_hello/) and run Infer on it: -```bash +```console infer run -- make ``` Infer will output the list of found bugs: -```bash +```console example.c:22: error: NULL_DEREFERENCE pointer max last assigned on line 21 could be null and is dereferenced at line 22, column 10 @@ -330,13 +328,13 @@ 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 +```console infer run --reactive -- make ``` or run -```bash +```console make clean ``` diff --git a/website/docs/02-separation-logic-and-biabduction.md b/website/docs/02-separation-logic-and-biabduction.md index 818ecb2561c..9dc622816af 100644 --- a/website/docs/02-separation-logic-and-biabduction.md +++ b/website/docs/02-separation-logic-and-biabduction.md @@ -134,8 +134,8 @@ 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 +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. @@ -309,17 +309,14 @@ read the source code if you wish! 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. +- [Local Reasoning about Programs that Alter Data Structures.](http://link.springer.com/chapter/10.1007%2F3-540-44802-0_1) + An early separation logic paper which advanced ideas about local reasoning and + the frame rule. +- [Smallfoot:Modular Automatic Assertion Checking with Separation Logic.](http://link.springer.com/chapter/10.1007/11804192_6) + First separation logic verification tool, introduced frame inference +- [A Local Shape Analysis Based on Separation Logic.](http://link.springer.com/chapter/10.1007%2F11691372_19) + Separation logic meets abstract interpretation; calculating loop invariants via a fixed-point computation. +- [Compositional Shape Analysis by Means of Bi-Abduction.](http://dl.acm.org/citation.cfm?id=2049700) + The bi-abduction paper. +- [Moving Fast with Software Verification.](https://research.facebook.com/publications/moving-fast-with-software-verification/) + A paper about the way we use Infer at Facebook. diff --git a/website/docs/all-checkers.md b/website/docs/all-checkers.md index b43f3ceb4a0..553fae70712 100644 --- a/website/docs/all-checkers.md +++ b/website/docs/all-checkers.md @@ -168,4 +168,3 @@ Detect various kinds of situations when no progress is being made because of con Detect errors based on user-provided state machines describing temporal properties over multiple objects. [Visit here for more information.](/docs/next/checker-topl) - diff --git a/website/docs/all-issue-types.md b/website/docs/all-issue-types.md index ed2bfd733ed..75042616db6 100644 --- a/website/docs/all-issue-types.md +++ b/website/docs/all-issue-types.md @@ -12,6 +12,7 @@ A call that may execute arbitrary code (such as registered, or chained, callback This code may deadlock whenever the callbacks obtain locks themselves, so it is an unsafe pattern. Example: + ```java SettableFuture future = null; @@ -41,6 +42,7 @@ Reported as "Bad Arg" by [pulse](/docs/next/checker-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 @@ -48,6 +50,7 @@ f() -> 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] @@ -58,6 +61,7 @@ g() -> Reported as "Bad Arg Latent" by [pulse](/docs/next/checker-pulse). A latent [BAD_ARG](#bad_arg). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## BAD_KEY Reported as "Bad Key" by [pulse](/docs/next/checker-pulse). @@ -65,6 +69,7 @@ Reported as "Bad Key" by [pulse](/docs/next/checker-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 = #{}, @@ -79,6 +84,7 @@ Therefore, if a map is non-empty and we try to access a key other than the one w Reported as "Bad Key Latent" by [pulse](/docs/next/checker-pulse). A latent [BAD_KEY](#bad_key). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## BAD_MAP Reported as "Bad Map" by [pulse](/docs/next/checker-pulse). @@ -86,6 +92,7 @@ Reported as "Bad Map" by [pulse](/docs/next/checker-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], @@ -97,6 +104,7 @@ f() -> Reported as "Bad Map Latent" by [pulse](/docs/next/checker-pulse). A latent [BAD_MAP](#bad_map). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## BAD_RECORD Reported as "Bad Record" by [pulse](/docs/next/checker-pulse). @@ -104,6 +112,7 @@ Reported as "Bad Record" by [pulse](/docs/next/checker-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}). @@ -118,6 +127,7 @@ f() -> Reported as "Bad Record Latent" by [pulse](/docs/next/checker-pulse). A latent [BAD_RECORD](#bad_record). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## BAD_RETURN Reported as "Bad Return" by [pulse](/docs/next/checker-pulse). @@ -125,6 +135,7 @@ Reported as "Bad Return" by [pulse](/docs/next/checker-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. @@ -137,16 +148,19 @@ Note that this will *not* lead to a runtime error when running the Erlang progra Reported as "Bad Return Latent" by [pulse](/docs/next/checker-pulse). A latent [BAD_RETURN](#bad_return). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## BIABDUCTION_MEMORY_LEAK Reported as "Memory Leak" by [biabduction](/docs/next/checker-biabduction). See [MEMORY_LEAK](#memory_leak). + ## BIABDUCTION_RETAIN_CYCLE Reported as "Retain Cycle" by [biabduction](/docs/next/checker-biabduction). See [RETAIN_CYCLE](#retain_cycle). + ## BLOCK_PARAMETER_NOT_NULL_CHECKED Reported as "Block Parameter Not Null Checked" by [parameter-not-null-checked](/docs/next/checker-parameter-not-null-checked). @@ -184,57 +198,57 @@ For example, `int a[3]; a[5] = 42;` generates a `BUFFER_OVERRUN_L1` on `a[5] = 4 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. +* `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](/docs/next/checker-bufferoverrun). See [BUFFER_OVERRUN_L1](#buffer_overrun_l1) + ## BUFFER_OVERRUN_L3 Reported as "Buffer Overrun L3" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [BUFFER_OVERRUN_L1](#buffer_overrun_l1) + ## BUFFER_OVERRUN_L4 Reported as "Buffer Overrun L4" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [BUFFER_OVERRUN_L1](#buffer_overrun_l1) + ## BUFFER_OVERRUN_L5 Reported as "Buffer Overrun L5" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [BUFFER_OVERRUN_L1](#buffer_overrun_l1) + ## BUFFER_OVERRUN_S2 Reported as "Buffer Overrun S2" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [BUFFER_OVERRUN_L1](#buffer_overrun_l1) + ## BUFFER_OVERRUN_U5 Reported as "Buffer Overrun U5" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [BUFFER_OVERRUN_L1](#buffer_overrun_l1) + ## CAPTURED_STRONG_SELF Reported as "Captured strongSelf" by [self-in-block](/docs/next/checker-self-in-block). @@ -247,18 +261,17 @@ This will happen in one of two cases generally: 1. One uses `weakSelf` but forgot to declare it weak first. -Example: + 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;`. + ```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;`. 2. 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 @@ -267,60 +280,60 @@ Example: Example: -```objectivec - __weak __typeof(self) weakSelf = self; - int (^my_block)() = ^() { - __strong typeof(self) strongSelf = weakSelf; - if (strongSelf) { + ```objectivec + __weak __typeof(self) weakSelf = self; int (^my_block)() = ^() { - int x = strongSelf->x; + __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. + 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: + **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) { + ```objectivec + __weak __typeof(self) weakSelf = self; int (^my_block)() = ^() { - __typeof(self) innerStrongSelf = weakSelf; - int x = innerStrongSelf->x; + __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. + 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: + 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; + ```objectivec + __weak __typeof(self) weakSelf = self; int (^my_block)() = ^() { - int x = my_x; + __strong typeof(self) strongSelf = weakSelf; + if (strongSelf) { + int my_x = strongSelf->x; + int (^my_block)() = ^() { + int x = my_x; + ... + }; + ... + } ... }; - ... - } - ... - }; -``` + ``` ## CHECKERS_ALLOCATES_MEMORY @@ -517,16 +530,19 @@ For more information see the [`NULLPTR_DEREFERENCE`](#nullptr_dereference) issue Reported as "Constant Address Dereference Latent" by [pulse](/docs/next/checker-pulse). A latent [CONSTANT_ADDRESS_DEREFERENCE](#constant_address_dereference). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## CREATE_INTENT_FROM_URI Reported as "Create Intent From Uri" by [quandary](/docs/next/checker-quandary). Create an intent/start a component using a (possibly user-controlled) URI. may or may not be an issue depending on where the URI comes from. + ## CROSS_SITE_SCRIPTING Reported as "Cross Site Scripting" by [quandary](/docs/next/checker-quandary). Untrusted data flows into HTML; XSS risk. + ## CXX_REF_CAPTURED_IN_BLOCK Reported as "C++ Reference Captured in Block" by [self-in-block](/docs/next/checker-self-in-block). @@ -537,7 +553,7 @@ not annotated with `__attribute__((noescape))`. Example: -``` +```cpp - (void)ref_captured_in_escaping_block_bad:(int&)y { dispatch_async(dispatch_get_main_queue(), ^{ int a = y; @@ -555,17 +571,18 @@ dereferences it later. Reported as "Dangling Pointer Dereference" by [biabduction](/docs/next/checker-biabduction). - ## DATALOG_FACT Reported as "Datalog Fact" by [datalog](/docs/next/checker-datalog). Datalog fact used as input for a datalog solver. + ## DATA_FLOW_TO_SINK Reported as "Data Flow to Sink" by [pulse](/docs/next/checker-pulse). A flow of data was detected to a sink. + ## DEADLOCK Reported as "Deadlock" by [starvation](/docs/next/checker-starvation). @@ -642,7 +659,6 @@ is never used (e.g., `int i = 1; i = 2; return i;`). Reported as "Divide By Zero" by [biabduction](/docs/next/checker-biabduction). - ## EMPTY_VECTOR_ACCESS Reported as "Empty Vector Access" by [biabduction](/docs/next/checker-biabduction). @@ -670,8 +686,6 @@ 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](/docs/next/checker-cost#examples). - - ## EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD Reported as "Execution Time Complexity Increase Ui Thread" by [cost](/docs/next/checker-cost). @@ -680,14 +694,13 @@ Infer reports this issue when the execution time complexity of the procedure inc Infer considers a method as running on the UI thread whenever: -- The method, one of its overrides, its class, or an ancestral class, is +* 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`, +* 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 +* 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](/docs/next/checker-cost). @@ -696,8 +709,8 @@ 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 @@ -715,6 +728,7 @@ Reported as "Expensive Execution Time" by [cost](/docs/next/checker-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](https://github.com/facebook/infer/blob/main/infer/src/base/costKind.ml#L55). For instance, a simple example where we report this issue is a function with linear cost: + ```java int sum_linear(ArrayList list){ int sum = 0; @@ -757,6 +771,7 @@ void symbolic_expensive_hoist(int size) { Reported as "Exposed Insecure Intent Handling" by [quandary](/docs/next/checker-quandary). Undocumented. + ## GUARDEDBY_VIOLATION Reported as "GuardedBy Violation" by [racerd](/docs/next/checker-racerd). @@ -783,6 +798,7 @@ Action: Protect the offending access by acquiring the lock indicated by the `@Gu Reported as "Impure Function" by [impurity](/docs/next/checker-impurity). This issue type indicates impure functions. For instance, below functions would be marked as impure: + ```java void makeAllZero_impure(ArrayList list) { Iterator listIterator = list.iterator(); @@ -798,8 +814,9 @@ void makeAllZero_impure(ArrayList list) { Reported as "Inefficient Keyset Iterator" by [inefficient-keyset-iterator](/docs/next/checker-inefficient-keyset-iterator). This issue is raised when -- iterating over a HashMap with `ketSet()` iterator -- looking up the key each time + +* iterating over a HashMap with `ketSet()` iterator +* looking up the key each time Example: @@ -815,7 +832,7 @@ void inefficient_loop_bad(HashMap testMap) { **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 testMap) { for (Map.Entry entry : testMap.entrySet()) { @@ -833,6 +850,7 @@ Reported as "Alloc Is Big" by [bufferoverrun](/docs/next/checker-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](/docs/next/checker-bufferoverrun). @@ -840,6 +858,7 @@ Reported as "Alloc Is Negative" by [bufferoverrun](/docs/next/checker-bufferover `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](/docs/next/checker-bufferoverrun). @@ -847,6 +866,7 @@ Reported as "Alloc Is Zero" by [bufferoverrun](/docs/next/checker-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](/docs/next/checker-bufferoverrun). @@ -854,6 +874,7 @@ Reported as "Alloc May Be Big" by [bufferoverrun](/docs/next/checker-bufferoverr `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](/docs/next/checker-bufferoverrun). @@ -861,6 +882,7 @@ Reported as "Alloc May Be Negative" by [bufferoverrun](/docs/next/checker-buffer `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](/docs/next/checker-cost). @@ -874,6 +896,7 @@ issue type is disabled. 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) { @@ -883,20 +906,23 @@ void square_root_FP(int x) { } } ``` -### 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, + +### 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](https://github.com/facebook/infer/blob/main/infer/src/bufferoverrun/bufferOverrunModels.ml). +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](https://github.com/facebook/infer/blob/main/infer/src/bufferoverrun/bufferOverrunModels.ml). ### 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 @@ -906,12 +932,12 @@ void call_top_cost_FP() { } ``` - ## INSECURE_INTENT_HANDLING Reported as "Insecure Intent Handling" by [quandary](/docs/next/checker-quandary). Undocumented. + ## INTEGER_OVERFLOW_L1 Reported as "Integer Overflow L1" by [bufferoverrun](/docs/next/checker-bufferoverrun). @@ -923,33 +949,33 @@ 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. +* `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](/docs/next/checker-bufferoverrun). See [INTEGER_OVERFLOW_L1](#integer_overflow_l1) + ## INTEGER_OVERFLOW_L5 Reported as "Integer Overflow L5" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [INTEGER_OVERFLOW_L1](#integer_overflow_l1) + ## INTEGER_OVERFLOW_U5 Reported as "Integer Overflow U5" by [bufferoverrun](/docs/next/checker-bufferoverrun). See [INTEGER_OVERFLOW_L1](#integer_overflow_l1) + ## INTERFACE_NOT_THREAD_SAFE Reported as "Interface Not Thread Safe" by [racerd](/docs/next/checker-racerd). @@ -973,9 +999,10 @@ expected for the front-end of the language for the analyzed code. Reported as "Invariant Call" by [loop-hoisting](/docs/next/checker-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 + +* 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) { @@ -997,16 +1024,19 @@ void invariant_hoist(int size) { Reported as "Ipc On Ui Thread" by [starvation](/docs/next/checker-starvation). A blocking `Binder` IPC call occurs on the UI thread. + ## JAVASCRIPT_INJECTION Reported as "Javascript Injection" by [quandary](/docs/next/checker-quandary). Untrusted data flows into JavaScript. + ## LAB_RESOURCE_LEAK Reported as "Lab Resource Leak" by [resource-leak-lab](/docs/next/checker-resource-leak-lab). Toy issue. + ## LOCKLESS_VIOLATION Reported as "Lockless Violation" by [starvation](/docs/next/checker-starvation). @@ -1036,20 +1066,20 @@ Reported as "Lock Consistency Violation" by [racerd](/docs/next/checker-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. +* 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 +* 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 +* 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 +* 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. @@ -1059,6 +1089,7 @@ container (an array, a vector, etc). Reported as "Logging Private Data" by [quandary](/docs/next/checker-quandary). Undocumented. + ## MEMORY_LEAK_C Reported as "Memory Leak" by [pulse](/docs/next/checker-pulse). @@ -1093,13 +1124,13 @@ objects from Core Foundation or Core Graphics don't get released. Reported as "Memory Leak" by [pulse](/docs/next/checker-pulse). See [MEMORY_LEAK_C](#memory_leak_c) + ## MISSING_REQUIRED_PROP Reported as "Missing Required Prop" by [litho-required-props](/docs/next/checker-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. @@ -1147,7 +1178,6 @@ MyComponent.create(c) or alternatively, if the `prop2` is not really required, we could change the component spec to reflect that: - ```java class MyComponentSpec { @@ -1159,6 +1189,7 @@ class MyComponentSpec { ... } ``` + ## MIXED_SELF_WEAKSELF Reported as "Mixed Self WeakSelf" by [self-in-block](/docs/next/checker-self-in-block). @@ -1191,13 +1222,14 @@ we assume that any captured weak pointer whose name contains "self" is a weak re Reported as "Modifies Immutable" by [impurity](/docs/next/checker-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; @@ -1271,6 +1303,7 @@ Adding a check for `nil` before calling the block, or making sure never to call Reported as "Nil Block Call Latent" by [pulse](/docs/next/checker-pulse). A latent [NIL_BLOCK_CALL](#nil_block_call). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NIL_INSERTION_INTO_COLLECTION Reported as "Nil Insertion Into Collection" by [pulse](/docs/next/checker-pulse). @@ -1321,6 +1354,7 @@ that the object passed will never be `nil`, or adding a check for `nil` before c Reported as "Nil Insertion Into Collection" by [pulse](/docs/next/checker-pulse). A latent [NIL_INSERTION_INTO_COLLECTION](#nil_insertion_into_collection). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NIL_MESSAGING_TO_NON_POD Reported as "Nil Messaging To Non Pod" by [pulse](/docs/next/checker-pulse). @@ -1355,6 +1389,7 @@ std::shared_ptr callMethodReturnsnonPOD(bool b) { Reported as "Nil Messaging To Non Pod Latent" by [pulse](/docs/next/checker-pulse). A latent [NIL_MESSAGING_TO_NON_POD](#nil_messaging_to_non_pod). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NO_MATCHING_BRANCH_IN_TRY Reported as "No Matching Branch In Try" by [pulse](/docs/next/checker-pulse). @@ -1362,6 +1397,7 @@ Reported as "No Matching Branch In Try" by [pulse](/docs/next/checker-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 @@ -1376,6 +1412,7 @@ tail(X) -> Reported as "No Matching Branch In Try Latent" by [pulse](/docs/next/checker-pulse). A latent [NO_MATCHING_BRANCH_IN_TRY](#no_matching_branch_in_try). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NO_MATCHING_CASE_CLAUSE Reported as "No Matching Case Clause" by [pulse](/docs/next/checker-pulse). @@ -1383,6 +1420,7 @@ Reported as "No Matching Case Clause" by [pulse](/docs/next/checker-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 @@ -1397,6 +1435,7 @@ This error is reported if either the pattern(s) or the guard(s) prevent matching Reported as "No Matching Case Clause Latent" by [pulse](/docs/next/checker-pulse). A latent [NO_MATCHING_CASE_CLAUSE](#no_matching_case_clause). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NO_MATCHING_FUNCTION_CLAUSE Reported as "No Matching Function Clause" by [pulse](/docs/next/checker-pulse). @@ -1404,6 +1443,7 @@ Reported as "No Matching Function Clause" by [pulse](/docs/next/checker-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. ``` @@ -1415,6 +1455,7 @@ This error is reported if either the pattern(s) or the guard(s) prevent matching Reported as "No Matching Function Clause Latent" by [pulse](/docs/next/checker-pulse). A latent [NO_MATCHING_FUNCTION_CLAUSE](#no_matching_function_clause). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NO_MATCH_OF_RHS Reported as "No Match Of Rhs" by [pulse](/docs/next/checker-pulse). @@ -1428,6 +1469,7 @@ For example, `[H|T] = []` gives the error because the left hand side pattern req Reported as "No Match Of Rhs Latent" by [pulse](/docs/next/checker-pulse). A latent [NO_MATCH_OF_RHS](#no_match_of_rhs). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NO_TRUE_BRANCH_IN_IF Reported as "No True Branch In If" by [pulse](/docs/next/checker-pulse). @@ -1435,6 +1477,7 @@ Reported as "No True Branch In If" by [pulse](/docs/next/checker-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 @@ -1448,6 +1491,7 @@ sign(X) -> Reported as "No True Branch In If Latent" by [pulse](/docs/next/checker-pulse). A latent [NO_TRUE_BRANCH_IN_IF](#no_true_branch_in_if). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NULLPTR_DEREFERENCE Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse). @@ -1655,11 +1699,13 @@ also have a dedicated issue type for this case: Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse). A latent [NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS](#nullptr_dereference_in_nullsafe_class). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NULLPTR_DEREFERENCE_LATENT Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse). A latent [NULLPTR_DEREFERENCE](#nullptr_dereference). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NULL_ARGUMENT Reported as "Null Argument" by [pulse](/docs/next/checker-pulse). @@ -1673,7 +1719,7 @@ This issue type indicates `nil` being passed as argument where a non-nil value e NSString* stringNotNil(NSString* str) { if (!str) { // ERROR: NSString:stringWithString: expects a non-nil value - return [NSString stringWithString:nil]; + return [NSString stringWithString:nil]; } return str; } @@ -1684,11 +1730,13 @@ NSString* stringNotNil(NSString* str) { Reported as "Null Argument Latent" by [pulse](/docs/next/checker-pulse). A latent [NULL_ARGUMENT](#null_argument). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## NULL_DEREFERENCE Reported as "Null Dereference" by [biabduction](/docs/next/checker-biabduction). See [NULLPTR_DEREFERENCE](#nullptr_dereference). + ## OPTIONAL_EMPTY_ACCESS Reported as "Optional Empty Access" by [pulse](/docs/next/checker-pulse). @@ -1750,6 +1798,7 @@ int value_no_check() { Reported as "Optional Empty Access Latent" by [pulse](/docs/next/checker-pulse). A latent [OPTIONAL_EMPTY_ACCESS](#optional_empty_access). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## PREMATURE_NIL_TERMINATION_ARGUMENT Reported as "Premature Nil Termination Argument" by [biabduction](/docs/next/checker-biabduction). @@ -1878,6 +1927,7 @@ void unsafe_expressions_bad(folly::F14FastMap& map) { Reported as "Resource Leak" by [pulse](/docs/next/checker-pulse). See [RESOURCE_LEAK](#resource_leak) + ## PULSE_TRANSITIVE_ACCESS Reported as "Transitive Access" by [pulse](/docs/next/checker-pulse). @@ -1886,10 +1936,9 @@ This issue tracks spurious accesses that are reachable from specific entry funct Spurious accesses are specified as specific load/calls. -Entry functions are specified through their enclosing class that must extend a specific +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 Reported as "Unawaited Awaitable" by [pulse](/docs/next/checker-pulse). @@ -1925,7 +1974,7 @@ For example, in the following code, the `FIELD` can be read by the static method ```hack abstract class A { abstract const string FIELD; - + public static function get_field(): string { return static::FIELD; } @@ -1979,6 +2028,7 @@ void foo() { Reported as "Uninitialized Value" by [pulse](/docs/next/checker-pulse). A latent [PULSE_UNINITIALIZED_VALUE](#pulse_uninitialized_value). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## PULSE_UNNECESSARY_COPY Reported as "Unnecessary Copy" by [pulse](/docs/next/checker-pulse). @@ -2002,21 +2052,25 @@ int use_reference_instead(A& x){ return y.a; } ``` + ## PULSE_UNNECESSARY_COPY_ASSIGNMENT Reported as "Unnecessary Copy Assignment" by [pulse](/docs/next/checker-pulse). See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy). + ## PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST Reported as "Unnecessary Copy Assignment from Const" by [pulse](/docs/next/checker-pulse). See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy). + ## PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE Reported as "Unnecessary Copy Assignment Movable" by [pulse](/docs/next/checker-pulse). See [PULSE_UNNECESSARY_COPY_MOVABLE](#pulse_unnecessary_copy_movable). + ## PULSE_UNNECESSARY_COPY_INTERMEDIATE Reported as "Unnecessary Copy Intermediate" by [pulse](/docs/next/checker-pulse). @@ -2032,32 +2086,33 @@ void callee(ExpensiveObject obj) { void caller() { callee(myExpensiveObj); // a copy of myExpensiveObj is created - // the copy is destroyed right after the call + // 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))`. - +* `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 Reported as "Unnecessary Copy Intermediate from Const" by [pulse](/docs/next/checker-pulse). See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy). + ## PULSE_UNNECESSARY_COPY_MOVABLE Reported as "Unnecessary Copy Movable" by [pulse](/docs/next/checker-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. + +* 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. @@ -2082,6 +2137,7 @@ class Test { }; ``` + ## PULSE_UNNECESSARY_COPY_OPTIONAL Reported as "Unnecessary Copy to Optional" by [pulse](/docs/next/checker-pulse). @@ -2107,6 +2163,7 @@ void pass_non_optional_value(A x) { Reported as "Unnecessary Copy to Optional from Const" by [pulse](/docs/next/checker-pulse). See [PULSE_UNNECESSARY_COPY_OPTIONAL](#pulse_unnecessary_copy_optional). + ## PULSE_UNNECESSARY_COPY_RETURN Reported as "Unnecessary Copy Return" by [pulse](/docs/next/checker-pulse). @@ -2173,11 +2230,13 @@ void set_impure(int x, int y) { Reported as "Taint Error" by [quandary](/docs/next/checker-quandary). Generic taint error when nothing else fits. + ## REGEX_OP_ON_UI_THREAD Reported as "Regex Op On Ui Thread" by [starvation](/docs/next/checker-starvation). A potentially costly operation on a regular expression occurs on the UI thread. + ## RESOURCE_LEAK Reported as "Resource Leak" by [biabduction](/docs/next/checker-biabduction). @@ -2202,14 +2261,14 @@ This is an example of a resource leak in C code: For the remaining of this section, we will consider examples of resource leaks in Java code. -TIP: A common source of bugs is exceptions skipping past close() -statements. That is the first thing to look for if INFER reports a potential +TIP: A common source of bugs is **exceptions skipping past close() +statements**. That is the first thing to look for if INFER reports a potential resource leak. ### Basics and Standard Idiom -Some objects in Java, the resources, are supposed to be closed when you -stop using them, and failure to close is a resource leak. Resources +Some objects in Java, the *resources*, are supposed to be closed when you +stop using them, and failure to close is a *resource leak*. Resources include input streams, output streams, readers, writers, sockets, http connections, cursors, and json parsers. @@ -2347,10 +2406,10 @@ during execution of the GZIPOutputStream constructor. Here are resources that can throw exceptions i their constructor(s). -- ObjectInputStream , ObjectOutputStream, PipedInputStream, PipedOutputStream, +* ObjectInputStream , ObjectOutputStream, PipedInputStream, PipedOutputStream, PipedReader, PipedWriter, JarInputStream, JarOutputStream, GZIPInputStream, GZIPOutputStream , ZipFile all throw IOException -- PrintStream throws UnsupportedEncodingException +* PrintStream throws UnsupportedEncodingException The constructors for FileInputStream, FileOutputStream and RandomAccessFile throw FileNotFoundException, but these cases are not problematic in the sense @@ -2447,7 +2506,7 @@ legitimate to simply convert the code over to try-with-resources if you have access to Java 7, so as to save yourself some brain-cycles. You will also end up with cleaner code. -If try-with-resources is so great you should always use it. But you +If try-with-resources is so great you should *always* use it. But you shouldn't… Try-with-resources gives resources static scoping, and works via a stack discipline. Sometimes, you want a resource to persist beyond scope, as in the escaping example above. In an escaping example maybe you could refactor lots @@ -2502,8 +2561,9 @@ 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)\}: +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 { @@ -2540,26 +2600,31 @@ given scope. Reported as "Sensitive Data Flow" by [pulse](/docs/next/checker-pulse). A flow of sensitive data was detected from a source. + ## SHELL_INJECTION Reported as "Shell Injection" by [quandary](/docs/next/checker-quandary). Environment variable or file data flowing to shell. + ## SHELL_INJECTION_RISK Reported as "Shell Injection Risk" by [quandary](/docs/next/checker-quandary). Code injection if the caller of the endpoint doesn't sanitize on its end. + ## SQL_INJECTION Reported as "Sql Injection" by [quandary](/docs/next/checker-quandary). Untrusted and unescaped data flows to SQL. + ## SQL_INJECTION_RISK Reported as "Sql Injection Risk" by [quandary](/docs/next/checker-quandary). Untrusted and unescaped data flows to SQL. + ## STACK_VARIABLE_ADDRESS_ESCAPE Reported as "Stack Variable Address Escape" by [pulse](/docs/next/checker-pulse). @@ -2588,25 +2653,25 @@ 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 +* 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`, +* 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 +* 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 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 +* 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 @@ -2707,6 +2772,7 @@ a local strong pointer that has been assigned `weakSelf`. Reported as "Taint Error" by [pulse](/docs/next/checker-pulse). A taint flow was detected from a source to a sink + ## THREAD_SAFETY_VIOLATION Reported as "Thread Safety Violation" by [racerd](/docs/next/checker-racerd). @@ -2720,30 +2786,30 @@ examples. 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. +* 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 +* 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 +* 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 +* 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, +* 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 +* 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. + * A parent class, or an override method are marked with the above annotations. NB currently RacerD **does not take into account `@GuardedBy`**. @@ -2774,14 +2840,14 @@ NB RacerD currently **does not recognize `@WorkerThread`, `@BinderThread` or These annotations can be found at `com.facebook.infer.annotation.*`. -- `@Functional` This is a method annotation indicating the method always returns +* `@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 +* `@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)` @@ -2793,11 +2859,11 @@ These annotations can be found at `com.facebook.infer.annotation.*`. 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 +* `@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 +* `@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 @@ -2819,61 +2885,73 @@ See [Topl](/docs/next/checker-topl##what-is-it) for an example Reported as "Topl Error Latent" by [topl](/docs/next/checker-topl). A latent [TOPL_ERROR](#topl_error). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## UNTRUSTED_BUFFER_ACCESS Reported as "Untrusted Buffer Access" by [quandary](/docs/next/checker-quandary). Untrusted data of any kind flowing to buffer. + ## UNTRUSTED_DESERIALIZATION Reported as "Untrusted Deserialization" by [quandary](/docs/next/checker-quandary). User-controlled deserialization. + ## UNTRUSTED_DESERIALIZATION_RISK Reported as "Untrusted Deserialization Risk" by [quandary](/docs/next/checker-quandary). User-controlled deserialization + ## UNTRUSTED_ENVIRONMENT_CHANGE_RISK Reported as "Untrusted Environment Change Risk" by [quandary](/docs/next/checker-quandary). User-controlled environment mutation. + ## UNTRUSTED_FILE Reported as "Untrusted File" by [quandary](/docs/next/checker-quandary). User-controlled file creation; may be vulnerable to path traversal and more. + ## UNTRUSTED_FILE_RISK Reported as "Untrusted File Risk" by [quandary](/docs/next/checker-quandary). User-controlled file creation; may be vulnerable to path traversal and more. + ## UNTRUSTED_HEAP_ALLOCATION Reported as "Untrusted Heap Allocation" by [quandary](/docs/next/checker-quandary). Untrusted data of any kind flowing to heap allocation. this can cause crashes or DOS. + ## UNTRUSTED_INTENT_CREATION Reported as "Untrusted Intent Creation" by [quandary](/docs/next/checker-quandary). Creating an Intent from user-controlled data. + ## UNTRUSTED_URL_RISK Reported as "Untrusted Url Risk" by [quandary](/docs/next/checker-quandary). Untrusted flag, environment variable, or file data flowing to URL. + ## UNTRUSTED_VARIABLE_LENGTH_ARRAY Reported as "Untrusted Variable Length Array" by [quandary](/docs/next/checker-quandary). Untrusted data of any kind flowing to stack buffer allocation. Trying to allocate a stack buffer that's too large will cause a stack overflow. + ## USER_CONTROLLED_SQL_RISK Reported as "User Controlled Sql Risk" by [quandary](/docs/next/checker-quandary). Untrusted data flows to SQL (no injection risk). + ## USE_AFTER_DELETE Reported as "Use After Delete" by [pulse](/docs/next/checker-pulse). @@ -2885,6 +2963,7 @@ An address that was invalidated by a call to `delete` in C++ is dereferenced. Reported as "Use After Delete Latent" by [pulse](/docs/next/checker-pulse). A latent [USE_AFTER_DELETE](#use_after_delete). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## USE_AFTER_FREE Reported as "Use After Free" by [pulse](/docs/next/checker-pulse). @@ -2896,6 +2975,7 @@ An address that was invalidated by a call to `free` in C is dereferenced. Reported as "Use After Free Latent" by [pulse](/docs/next/checker-pulse). A latent [USE_AFTER_FREE](#use_after_free). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## USE_AFTER_LIFETIME Reported as "Use After Lifetime" by [pulse](/docs/next/checker-pulse). @@ -2920,6 +3000,7 @@ void foo() { Reported as "Use After Lifetime Latent" by [pulse](/docs/next/checker-pulse). A latent [USE_AFTER_LIFETIME](#use_after_lifetime). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## VECTOR_INVALIDATION Reported as "Vector Invalidation" by [pulse](/docs/next/checker-pulse). @@ -2948,6 +3029,7 @@ void deref_vector_element_after_push_back_bad(std::vector& vec) { Reported as "Vector Invalidation Latent" by [pulse](/docs/next/checker-pulse). A latent [VECTOR_INVALIDATION](#vector_invalidation). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues). + ## WEAK_SELF_IN_NO_ESCAPE_BLOCK Reported as "Weak Self In No Escape Block" by [self-in-block](/docs/next/checker-self-in-block). @@ -2983,4 +3065,3 @@ Replace `weakSelf` with `self`: *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`. - diff --git a/website/docs/checker-annotation-reachability.md b/website/docs/checker-annotation-reachability.md index ff0aec87dc1..6c912cae9d5 100644 --- a/website/docs/checker-annotation-reachability.md +++ b/website/docs/checker-annotation-reachability.md @@ -8,6 +8,7 @@ Given pairs of source and sink annotations, e.g. `@A` and `@B`, this checker wil Activate with `--annotation-reachability`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -15,11 +16,10 @@ Supported languages: - Java: Yes - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [CHECKERS_ALLOCATES_MEMORY](/docs/next/all-issue-types#checkers_allocates_memory) - [CHECKERS_ANNOTATION_REACHABILITY_ERROR](/docs/next/all-issue-types#checkers_annotation_reachability_error) - [CHECKERS_CALLS_EXPENSIVE_METHOD](/docs/next/all-issue-types#checkers_calls_expensive_method) diff --git a/website/docs/checker-biabduction.md b/website/docs/checker-biabduction.md index 8f929e7883e..627a41b2ee4 100644 --- a/website/docs/checker-biabduction.md +++ b/website/docs/checker-biabduction.md @@ -10,6 +10,7 @@ This analysis deals with a range of issues, many linked to memory safety. Activate with `--biabduction`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: Yes - Erlang: No @@ -22,6 +23,7 @@ Read more about its foundations in the [Separation Logic and Biabduction page](s ## List of Issue Types The following issue types are reported by this checker: + - [BIABDUCTION_MEMORY_LEAK](/docs/next/all-issue-types#biabduction_memory_leak) - [BIABDUCTION_RETAIN_CYCLE](/docs/next/all-issue-types#biabduction_retain_cycle) - [DANGLING_POINTER_DEREFERENCE](/docs/next/all-issue-types#dangling_pointer_dereference) diff --git a/website/docs/checker-bufferoverrun.md b/website/docs/checker-bufferoverrun.md index 7593e19f362..ab197c18afb 100644 --- a/website/docs/checker-bufferoverrun.md +++ b/website/docs/checker-bufferoverrun.md @@ -8,6 +8,7 @@ InferBO is a detector for out-of-bounds array accesses. Activate with `--bufferoverrun`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -20,6 +21,7 @@ You can read about its origins in this [blog post](https://research.fb.com/infer ## List of Issue Types The following issue types are reported by this checker: + - [BUFFER_OVERRUN_L1](/docs/next/all-issue-types#buffer_overrun_l1) - [BUFFER_OVERRUN_L2](/docs/next/all-issue-types#buffer_overrun_l2) - [BUFFER_OVERRUN_L3](/docs/next/all-issue-types#buffer_overrun_l3) diff --git a/website/docs/checker-config-impact-analysis.md b/website/docs/checker-config-impact-analysis.md index 095a7828b9e..9a31341eca1 100644 --- a/website/docs/checker-config-impact-analysis.md +++ b/website/docs/checker-config-impact-analysis.md @@ -8,6 +8,7 @@ description: "[EXPERIMENTAL] Collects function that are called without config ch Activate with `--config-impact-analysis`. Supported languages: + - C/C++/ObjC: Experimental - C#/.Net: No - Erlang: No @@ -20,5 +21,6 @@ This checker collects functions whose execution isn't gated by certain pre-defin ## List of Issue Types The following issue types are reported by this checker: + - [CONFIG_IMPACT](/docs/next/all-issue-types#config_impact) - [CONFIG_IMPACT_STRICT](/docs/next/all-issue-types#config_impact_strict) diff --git a/website/docs/checker-cost.md b/website/docs/checker-cost.md index 6e9d2e815e5..51966b358ff 100644 --- a/website/docs/checker-cost.md +++ b/website/docs/checker-cost.md @@ -8,6 +8,7 @@ Computes the asymptotic complexity of functions with respect to execution cost o Activate with `--cost`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -23,10 +24,10 @@ analyses that are run by default) or `infer --cost-only` (which will only run co 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](/docs/checker-bufferoverrun) computes value ranges for instructions accessing memory - 2) a loop bound analysis determines upper bounds for the number of iterations of loops and generates constraints for nodes in the control-flow graph - 3) a constraint solving step resolves the constraints generated in the second step and computes an upper bound on the execution cost. @@ -34,32 +35,29 @@ The analysis computes symbolic upper bounds on the resource usage of programs— Most ideas behind this analysis are based on Stefan Bydge's PhD thesis [Static WCET Analysis based on Abstract Interpretation and Counting of Elements](https://www.semanticscholar.org/paper/Static-WCET-Analysis-Based-on-Abstract-and-Counting-Bygde/ee5157164d497725c1f42dc6c475a59a87c99957). 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 - 2) allocation cost - 3) 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 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. +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) @@ -85,30 +83,29 @@ void loop(ArrayList list){ 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`](/docs/next/all-issue-types#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. + +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](/docs/checker-bufferoverrun) '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](/docs/next/all-issue-types#infinite_execution_time) for details. - ## List of Issue Types The following issue types are reported by this checker: + - [EXECUTION_TIME_COMPLEXITY_INCREASE](/docs/next/all-issue-types#execution_time_complexity_increase) - [EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD](/docs/next/all-issue-types#execution_time_complexity_increase_ui_thread) - [EXECUTION_TIME_UNREACHABLE_AT_EXIT](/docs/next/all-issue-types#execution_time_unreachable_at_exit) diff --git a/website/docs/checker-datalog.md b/website/docs/checker-datalog.md index 9d27bf3142c..1cfaada0278 100644 --- a/website/docs/checker-datalog.md +++ b/website/docs/checker-datalog.md @@ -8,6 +8,7 @@ Experimental datalog-based points-to analysis. Activate with `--datalog`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -15,9 +16,8 @@ Supported languages: - Java: Experimental - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [DATALOG_FACT](/docs/next/all-issue-types#datalog_fact) diff --git a/website/docs/checker-fragment-retains-view.md b/website/docs/checker-fragment-retains-view.md index f6525120c1e..b2c116d9100 100644 --- a/website/docs/checker-fragment-retains-view.md +++ b/website/docs/checker-fragment-retains-view.md @@ -10,6 +10,7 @@ Detects when Android fragments are not explicitly nullified before becoming unre Activate with `--fragment-retains-view`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -17,9 +18,8 @@ Supported languages: - Java: Yes - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [CHECKERS_FRAGMENT_RETAINS_VIEW](/docs/next/all-issue-types#checkers_fragment_retains_view) diff --git a/website/docs/checker-impurity.md b/website/docs/checker-impurity.md index 206fb484cfe..3de67313c44 100644 --- a/website/docs/checker-impurity.md +++ b/website/docs/checker-impurity.md @@ -8,6 +8,7 @@ Detects functions with potential side-effects. Same as "purity", but implemented Activate with `--impurity`. Supported languages: + - C/C++/ObjC: Experimental - C#/.Net: No - Erlang: No @@ -17,9 +18,9 @@ Supported languages: This is an experimental inter-procedural analysis that detects impure functions. It is meant to be an improvement over the [purity](/docs/next/checker-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](/docs/next/checker-pulse) summaries to determine impurity. - ## List of Issue Types The following issue types are reported by this checker: + - [IMPURE_FUNCTION](/docs/next/all-issue-types#impure_function) - [MODIFIES_IMMUTABLE](/docs/next/all-issue-types#modifies_immutable) diff --git a/website/docs/checker-inefficient-keyset-iterator.md b/website/docs/checker-inefficient-keyset-iterator.md index 6a63965f3a8..759567ec6dd 100644 --- a/website/docs/checker-inefficient-keyset-iterator.md +++ b/website/docs/checker-inefficient-keyset-iterator.md @@ -8,6 +8,7 @@ Check for inefficient uses of iterators that iterate on keys then lookup their v Activate with `--inefficient-keyset-iterator`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -15,9 +16,8 @@ Supported languages: - Java: Yes - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [INEFFICIENT_KEYSET_ITERATOR](/docs/next/all-issue-types#inefficient_keyset_iterator) diff --git a/website/docs/checker-lineage.md b/website/docs/checker-lineage.md index ff1cbe28edd..f88711b4d1f 100644 --- a/website/docs/checker-lineage.md +++ b/website/docs/checker-lineage.md @@ -8,10 +8,10 @@ Computes a dataflow graph Activate with `--lineage`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: Yes - Hack: No - Java: No - Python: No - diff --git a/website/docs/checker-litho-required-props.md b/website/docs/checker-litho-required-props.md index b65b8dedf9d..cb4782c539c 100644 --- a/website/docs/checker-litho-required-props.md +++ b/website/docs/checker-litho-required-props.md @@ -8,6 +8,7 @@ Checks that all non-optional `@Prop`s have been specified when constructing Lith Activate with `--litho-required-props`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -17,8 +18,8 @@ Supported languages: This analysis checks that all non-optional [`@Prop`](https://fblitho.com/docs/props)`s have been specified when constructing Litho components. This is a [Litho](https://fblitho.com/) 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 @@ -53,4 +54,5 @@ Check out the examples defined in the issue type [MISSING_REQUIRED_PROP](/docs/n ## List of Issue Types The following issue types are reported by this checker: + - [MISSING_REQUIRED_PROP](/docs/next/all-issue-types#missing_required_prop) diff --git a/website/docs/checker-liveness.md b/website/docs/checker-liveness.md index 6d6fc87fb20..5e659c606d5 100644 --- a/website/docs/checker-liveness.md +++ b/website/docs/checker-liveness.md @@ -8,6 +8,7 @@ Detection of dead stores and unused variables. Activate with `--liveness`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -15,9 +16,8 @@ Supported languages: - Java: No - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [DEAD_STORE](/docs/next/all-issue-types#dead_store) diff --git a/website/docs/checker-loop-hoisting.md b/website/docs/checker-loop-hoisting.md index c191287305b..0da7a8eae3b 100644 --- a/website/docs/checker-loop-hoisting.md +++ b/website/docs/checker-loop-hoisting.md @@ -8,6 +8,7 @@ Detect opportunities to hoist function calls that are invariant outside of loop Activate with `--loop-hoisting`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -19,9 +20,9 @@ This checker detects opportunities to hoist function calls that are invariant to It has an additional mode that reports [loop-invariant functions that are expensive](/docs/next/all-issue-types#expensive_loop_invariant_call) (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: + - [EXPENSIVE_LOOP_INVARIANT_CALL](/docs/next/all-issue-types#expensive_loop_invariant_call) - [INVARIANT_CALL](/docs/next/all-issue-types#invariant_call) diff --git a/website/docs/checker-parameter-not-null-checked.md b/website/docs/checker-parameter-not-null-checked.md index 24fb3167d65..0e277195e8f 100644 --- a/website/docs/checker-parameter-not-null-checked.md +++ b/website/docs/checker-parameter-not-null-checked.md @@ -8,6 +8,7 @@ An Objective-C-specific analysis to detect when a block parameter is used before Activate with `--parameter-not-null-checked`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -18,8 +19,8 @@ Supported languages: 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](/docs/next/all-issue-types#block_parameter_not_null_checked) diff --git a/website/docs/checker-printf-args.md b/website/docs/checker-printf-args.md index 446fdfcddc1..4e7a6202703 100644 --- a/website/docs/checker-printf-args.md +++ b/website/docs/checker-printf-args.md @@ -10,6 +10,7 @@ Detect mismatches between the Java `printf` format strings and the argument type Activate with `--printf-args`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -17,9 +18,8 @@ Supported languages: - Java: Yes - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [CHECKERS_PRINTF_ARGS](/docs/next/all-issue-types#checkers_printf_args) diff --git a/website/docs/checker-pulse.md b/website/docs/checker-pulse.md index 9dff1f46377..de6045ac937 100644 --- a/website/docs/checker-pulse.md +++ b/website/docs/checker-pulse.md @@ -8,6 +8,7 @@ General-purpose memory and value analysis engine. Activate with `--pulse`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: Experimental @@ -45,6 +46,7 @@ class Registry { ``` How to run pulse for Java: + ```bash infer run --pulse -- javac Test.java ``` @@ -101,6 +103,7 @@ void false_positive(int *x) { ``` 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 @@ -131,10 +134,10 @@ class Registry { } ``` - ## List of Issue Types The following issue types are reported by this checker: + - [BAD_ARG](/docs/next/all-issue-types#bad_arg) - [BAD_ARG_LATENT](/docs/next/all-issue-types#bad_arg_latent) - [BAD_KEY](/docs/next/all-issue-types#bad_key) diff --git a/website/docs/checker-purity.md b/website/docs/checker-purity.md index 6b8274d6b8b..b150490affc 100644 --- a/website/docs/checker-purity.md +++ b/website/docs/checker-purity.md @@ -8,6 +8,7 @@ Detects pure (side-effect-free) functions. A different implementation of "impuri Activate with `--purity`. Supported languages: + - C/C++/ObjC: Experimental - C#/.Net: No - Erlang: No @@ -19,10 +20,10 @@ This is an experimental inter-procedural analysis that detects pure (side-effect 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`](/docs/next/all-issue-types#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. @@ -31,7 +32,7 @@ Too see the issue with the first point, consider the following simple program: ```java void foo(Foo a){ Foo b = a; - b.x = 10; + b.x = 10; } ``` @@ -53,17 +54,15 @@ boolean contains(Integer i, ArrayList list){ 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](/docs/next/checker-impurity) analysis which uses [pulse](/docs/next/checker-pulse) which can successfully analyze this program as pure \o/ - The analysis is used by: -- [Loop-hoisting](/docs/next/checker-loop-hoisting) analysis which identifies loop-invariant function calls, i.e. functions that are pure and have loop-invariant arguments. +- [Loop-hoisting](/docs/next/checker-loop-hoisting) analysis which identifies loop-invariant function calls, i.e. functions that are pure and have loop-invariant arguments. - [Cost](/docs/next/checker-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](/docs/next/all-issue-types#pure_function) diff --git a/website/docs/checker-quandary.md b/website/docs/checker-quandary.md index 8f514b81cd3..e947ea931da 100644 --- a/website/docs/checker-quandary.md +++ b/website/docs/checker-quandary.md @@ -10,6 +10,7 @@ The Quandary taint analysis detects flows of values between sources and sinks, e Activate with `--quandary`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -26,10 +27,10 @@ and you can define custom sources and sinks in your `.inferconfig` file (see example [here](https://github.com/facebook/infer/blob/main/infer/tests/codetoanalyze/java/quandary/.inferconfig)). - ## List of Issue Types The following issue types are reported by this checker: + - [CREATE_INTENT_FROM_URI](/docs/next/all-issue-types#create_intent_from_uri) - [CROSS_SITE_SCRIPTING](/docs/next/all-issue-types#cross_site_scripting) - [EXPOSED_INSECURE_INTENT_HANDLING](/docs/next/all-issue-types#exposed_insecure_intent_handling) diff --git a/website/docs/checker-racerd.md b/website/docs/checker-racerd.md index bfc37ceac73..0a49e13798a 100644 --- a/website/docs/checker-racerd.md +++ b/website/docs/checker-racerd.md @@ -8,6 +8,7 @@ Thread safety analysis. Activate with `--racerd`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: Yes - Erlang: No @@ -41,7 +42,7 @@ accesses occur on the same thread. ## Triggering the analysis -RacerD doesn't try to check _all_ code for concurrency issues; it only looks at +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 @@ -66,7 +67,7 @@ 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: -``` +```java @ThreadSafe public class Dinner { private int mTemperature; @@ -96,7 +97,7 @@ with `@ThreadSafe(enableChecks = false)`. We sometimes need to protect read accesses as well as writes. Consider the following class with unsynchronized methods. -``` +```java @ThreadSafe public class Account { @@ -140,7 +141,7 @@ to wrap both read and write accesses, or to use an `AtomicInteger` for In the following code, RacerD will report an `Interface not thread-safe` warning on the call to `i.bar()`: -``` +```java interface I { void bar(); } @@ -192,7 +193,7 @@ 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. -``` +```java List mCache; @ThreadConfined(UI) @@ -220,7 +221,7 @@ itself. Not all races are bugs; a race can be benign. Consider the following: -``` +```java @Functional Boolean askNetworkIfShouldShowFeature(); private Boolean mShouldShowFeature; @@ -238,7 +239,7 @@ 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 +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 @@ -252,10 +253,10 @@ 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 +Be sure not to use the `@Functional` pattern for *singleton instantiation*, as it's possible the "singleton" can be constructed more than once. -``` +```java public class MySingleton { private static sInstance; @@ -272,12 +273,12 @@ public class MySingleton { ### `@ReturnsOwnership` -RacerD does not warn on unprotected writes to _owned_ objects. An object is +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: -``` +```java @ThreadSafe public interface Car { @ReturnsOwnership abstract Car buyCar(); @@ -301,7 +302,7 @@ 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: -``` +```java @VisibleForTesting void setF() { this.f = ...; // RacerD would normally warn here, but @VisibleForTesting will silence the warning } @@ -322,7 +323,7 @@ several procedure calls. It handles this even between classes and between files. Here is a very basic example -``` +```java @ThreadSafe class A{ @@ -346,7 +347,7 @@ 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. -``` +```console 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 @@ -358,8 +359,8 @@ InterProc.java:17: error: THREAD_SAFETY_VIOLATION 19. } ``` -RacerD does this sort of reasoning using what is known as a _compositional -inteprocedural analysis_. There, each method is analyzed independently of its +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()' and`meth()' include information as follows. @@ -429,7 +430,7 @@ including in [Google's Error Prone analyzer](https://github.com/google/error-prone/blob/master/docs/bugpattern/GuardedBy.md). 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 +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. @@ -477,7 +478,7 @@ 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! -``` +```java @ThreadSafe public class SynchronizedList { synchronized boolean isEmpty() { ... } @@ -500,10 +501,10 @@ concurrency issues is difficult. If you would like to learn more about best practices, [Java Concurrency in Practice](http://jcip.net/) is an excellent resource. - ## List of Issue Types The following issue types are reported by this checker: + - [GUARDEDBY_VIOLATION](/docs/next/all-issue-types#guardedby_violation) - [INTERFACE_NOT_THREAD_SAFE](/docs/next/all-issue-types#interface_not_thread_safe) - [LOCK_CONSISTENCY_VIOLATION](/docs/next/all-issue-types#lock_consistency_violation) diff --git a/website/docs/checker-resource-leak-lab.md b/website/docs/checker-resource-leak-lab.md index 6a217a21e19..2ce3c67af34 100644 --- a/website/docs/checker-resource-leak-lab.md +++ b/website/docs/checker-resource-leak-lab.md @@ -8,6 +8,7 @@ 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 @@ -20,4 +21,5 @@ This toy checker does nothing by default. Hack on it to make it report resource ## List of Issue Types The following issue types are reported by this checker: + - [LAB_RESOURCE_LEAK](/docs/next/all-issue-types#lab_resource_leak) diff --git a/website/docs/checker-scope-leakage.md b/website/docs/checker-scope-leakage.md index ae3f7a5fabc..1d0b719a60a 100644 --- a/website/docs/checker-scope-leakage.md +++ b/website/docs/checker-scope-leakage.md @@ -8,6 +8,7 @@ The Java/Kotlin checker takes into account a set of "scope" annotations and a mu Activate with `--scope-leakage`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -15,9 +16,8 @@ Supported languages: - Java: Yes - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [SCOPE_LEAKAGE](/docs/next/all-issue-types#scope_leakage) diff --git a/website/docs/checker-self-in-block.md b/website/docs/checker-self-in-block.md index f85ee9d1044..5824572bf28 100644 --- a/website/docs/checker-self-in-block.md +++ b/website/docs/checker-self-in-block.md @@ -8,6 +8,7 @@ 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 @@ -15,11 +16,10 @@ Supported languages: - Java: No - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [CAPTURED_STRONG_SELF](/docs/next/all-issue-types#captured_strong_self) - [CXX_REF_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#cxx_ref_captured_in_block) - [MIXED_SELF_WEAKSELF](/docs/next/all-issue-types#mixed_self_weakself) diff --git a/website/docs/checker-sil-validation.md b/website/docs/checker-sil-validation.md index f899fbc696e..551d57e7783 100644 --- a/website/docs/checker-sil-validation.md +++ b/website/docs/checker-sil-validation.md @@ -8,6 +8,7 @@ This checker validates that all SIL instructions in all procedure bodies conform Activate with `--sil-validation`. Supported languages: + - C/C++/ObjC: No - C#/.Net: No - Erlang: No @@ -15,9 +16,8 @@ Supported languages: - Java: Yes - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [INVALID_SIL](/docs/next/all-issue-types#invalid_sil) diff --git a/website/docs/checker-siof.md b/website/docs/checker-siof.md index 3c8e3faf510..523627ae15c 100644 --- a/website/docs/checker-siof.md +++ b/website/docs/checker-siof.md @@ -8,6 +8,7 @@ Catches Static Initialization Order Fiascos in C++, that can lead to subtle, com Activate with `--siof`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -15,9 +16,8 @@ Supported languages: - Java: No - Python: No - - ## List of Issue Types The following issue types are reported by this checker: + - [STATIC_INITIALIZATION_ORDER_FIASCO](/docs/next/all-issue-types#static_initialization_order_fiasco) diff --git a/website/docs/checker-starvation.md b/website/docs/checker-starvation.md index 24d91cda35a..8e436136e85 100644 --- a/website/docs/checker-starvation.md +++ b/website/docs/checker-starvation.md @@ -8,6 +8,7 @@ Detect various kinds of situations when no progress is being made because of con Activate with `--starvation`. Supported languages: + - C/C++/ObjC: Yes - C#/.Net: No - Erlang: No @@ -16,15 +17,16 @@ Supported languages: - Python: No Detect several kinds of "starvation" problems: + - deadlocks - violations of `@Lockless` annotations - violations of [Android's "strict mode"](https://developer.android.com/reference/android/os/StrictMode) - doing expensive operations on the Android UI thread - ## List of Issue Types The following issue types are reported by this checker: + - [ARBITRARY_CODE_EXECUTION_UNDER_LOCK](/docs/next/all-issue-types#arbitrary_code_execution_under_lock) - [DEADLOCK](/docs/next/all-issue-types#deadlock) - [IPC_ON_UI_THREAD](/docs/next/all-issue-types#ipc_on_ui_thread) diff --git a/website/docs/checker-topl.md b/website/docs/checker-topl.md index e21e22f9e96..1d87e0c4ab0 100644 --- a/website/docs/checker-topl.md +++ b/website/docs/checker-topl.md @@ -8,12 +8,13 @@ Detect errors based on user-provided state machines describing temporal properti Activate with `--topl`. Supported languages: -- C/C++/ObjC: Experimental -- C#/.Net: No -- Erlang: Experimental -- Hack: No -- Java: Experimental -- Python: No + +* C/C++/ObjC: Experimental +* C#/.Net: No +* Erlang: Experimental +* Hack: No +* Java: Experimental +* Python: No # Topl @@ -32,7 +33,7 @@ property Taint 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: -``` +```java public class Main { static void f() { g(tito(source())); } static void g(Object x) { h(x); } @@ -45,13 +46,13 @@ public class Main { 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: -``` +```console infer --topl --topl-properties taint.topl -- javac Main.java ``` It will display the following error: -``` +```console Main.java:2: error: Topl Error property Taint reaches state error. 1. public class Main { @@ -62,7 +63,7 @@ Main.java:2: error: Topl Error To get a full trace, use the command -``` +```console infer explore ``` @@ -99,12 +100,13 @@ Otherwise, the label on a transition contains: 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*. + * 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 @@ -117,12 +119,12 @@ For several examples, see https://github.com/facebook/infer/tree/main/infer/test * 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. - + * 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: -- [TOPL_ERROR](/docs/next/all-issue-types#topl_error) -- [TOPL_ERROR_LATENT](/docs/next/all-issue-types#topl_error_latent) + +* [TOPL_ERROR](/docs/next/all-issue-types#topl_error) +* [TOPL_ERROR_LATENT](/docs/next/all-issue-types#topl_error_latent) diff --git a/website/docs/support.md b/website/docs/support.md index 100c040072b..ce6991138ca 100644 --- a/website/docs/support.md +++ b/website/docs/support.md @@ -49,7 +49,7 @@ analyze your files. A workaround consists in setting the `LD` environment variable to a dummy linker, for instance: -``` +```sh LD=/bin/true infer [options] -- ``` diff --git a/website/docs/versions.md b/website/docs/versions.md index 2cff35c5a66..59520d804f1 100644 --- a/website/docs/versions.md +++ b/website/docs/versions.md @@ -4,6 +4,7 @@ title: Documentation Versions --- Browse the documentation for different versions: + - [latest released version (1.1.0)](/docs/getting-started) - [previous version (1.0.0)](/docs/1.0.0/getting-started) - [next version](/docs/next/getting-started)