diff --git a/infer/documentation/checkers/ASTLanguage.md b/infer/documentation/checkers/ASTLanguage.md new file mode 100644 index 000000000..b4ba6e402 --- /dev/null +++ b/infer/documentation/checkers/ASTLanguage.md @@ -0,0 +1,689 @@ +For C/C++ and Objective-C languages, we provide a linters framework. These are +checks about the syntax of the program; it could be about a property, or about +code inside one method, or that a class or method have certain properties. We +provide [a few checks](/docs/linters-bug-types) and we have developed a domain +specific language (DSL) to make it easier to write checks. + +## AL: A declarative language for writing linters in Infer + +One of the major advantage of Infer when compared with other static analyzers is +the fact it performs sophisticated inter-procedural/inter-file analysis. That +is, Infer can detect bugs which involve tracking values through many procedure +calls and the procedures may live in different files. These may be very subtle +bugs and designing static analyses to do that is quite involved and normally +requires deep static analysis expertise. + +However, there are many important software bugs that are confined in the code of +a single procedure (called intra-procedural). To detect these bugs simpler +analyses may suffice which do not require deep technical expertise in static +analysis. Often these bugs can be expressed by referring to the syntax of the +program, or the types of certain expressions. We have defined a new language to +easily design checkers which identify these kind of bugs. The language is called +AL (AST Language) and its main feature is the ability to reason about the +Abstract Syntax Tree of a program in a concise declarative way. AL's checkers +are interpreted by Infer to analyze programs. Thus, to detect new kind of bugs +in Infer one can just write a check in AL. We will see in more detail later, +that for writing AL formulas we also need predicates: simple functions that +check a property of the AST. Predicates are written in OCaml inside Infer, thus +it requires a bit of OCaml knowledge and getting familiar with the OCaml data +structure for the clang AST. + +## Getting the clang AST + +When you write a linter that traverses the AST of some programs to check some +property, you probably need to understand what the AST looks like. You can get +the AST of programs using clang directly, or using Infer. + +If you have a clang command `clang File.m` then you can get +the AST with + +```bash +clang -Xclang -ast-dump -fsyntax-only File.m +``` + +You can also get the AST using Infer. One advantage of this is that you don't +need to know the speicifc clang command, just the general build command. +Moreover, what you get here is exactly the form of the AST that Infer has as +input. + +For this you need to install an OCaml package `biniou` with +`opam install biniou`. See [the opam website](https://opam.ocaml.org/) for +instructions on how to install opam. + +Then, the AST can be created by Infer in debug mode. Call Infer with + +```bash +infer --debug -- +``` + +This will, among other things, generate a file `/path/to/File.m.ast.sh` for +every file `/path/to/File.m` that is being analyzed. Run this script with +`bash File.m.ast.sh` and a file `/path/to/File.m.ast.bdump` will be generated, +that contains the AST of the program in `bdump` format (similar to json). If you +get an error about `bdump` not being found you may need to run +`eval $(opam env)` to get the `bdump` executable (provided by the biniou opam +package) into your `PATH`. + +For general info on the clang AST, you can check out +[clang's website](http://clang.llvm.org/docs/IntroductionToTheClangAST.html). + +## Using AL to write linters + +Let's start with an example. Suppose we want to write the following +Objective-C's linter: + +_"a property containing the word 'delegate', but not containing the word 'queue' +should not be declared strong"_. + +We can write this property in the following way: + +```bash +DEFINE-CHECKER STRONG_DELEGATE_WARNING = { + + LET name_contains_delegate = + declaration_has_name(REGEXP("[dD]elegate")); + + LET name_does_not_contain_queue = + NOT declaration_has_name(REGEXP("[qQ]ueue")); + + SET report_when = + WHEN + name_contains_delegate + AND name_does_not_contain_queue + AND is_strong_property() + HOLDS-IN-NODE ObjCPropertyDecl; + + SET message = "Property or ivar %decl_name% declared strong"; + SET suggestion = "In general delegates should be declared weak or assign"; + SET severity = "WARNING" + }; +``` + +The linter definition starts with the keyword `DEFINE-CHECKER` followed by the +checker's name. The first `LET` clause defines the _formula variable_ +`name_contains_delegate` using the predicate `declaration_has_name` which return +true/false depending whether the property's name contains a word in the language +of the regular expression `[dD]elegate`. In general a predicate is a simple +atomic formula evaluated on an AST node. The list of available predicates is in +the module +[`cPredicates.mli`](https://github.com/facebook/infer/blob/master/infer/src/clang/cPredicates.mli) +(this list is continuously growing and if you need a new predicate you can add +it in ocaml). Formula variables can be used to simplify other definitions. The +`SET report_when` is mandatory and defines a formula that, when evaluates to +true, will tell Infer to report an error. In the case above, the formula is +saying that we should report when visiting an `ObjCPropertyDecl` (that is the +AST node declaring a property in Objective-C) where it holds that: the name +contains "delegate/Delegate" (`name_contains_delegate`) and the name doesn't +contain "queue/Queue" (`name_does_not_contain_queue`) and the node is defining a +"strong" property (`is_strong_property()`). + +The `SET message` clause defines the error message that will be displayed to the +user. Notice that the message can include placeholders like `%decl_name%`. +Placeholders are evaluated by Infer and substituted by their current value when +the error message is reported. In this case the name of the declaration. The +`SET suggestion` clause define an optional hint to give to programmer on how to +fix the problem. + +The general structure of a checker is the following: + +```bash +DEFINE-CHECKER id_of_the_checker = { + + LET formula = ; + LET …. + + SET report_when = ; + + SET name = ; + SET message = ; + SET suggestion = ; + SET doc_url = ; + SET severity = INFO | LIKE | ADVICE | WARNING | ERROR; + SET mode = ON | OFF + SET whitelist_path = {path1, path2, ..., pathn }; + SET blacklist_path = {path1, path2, ..., pathn }; + }; +``` + +The default severity is `WARNING` and the default mode is `ON`, so these are +optional. If the check is `OFF` it will only be available in debug mode (flags +`--debug` or `--linters-developer-mode`). `INFOs` are generally also not +reported, except with some specialzed flags. `name` and `doc_url` are used only +for CI comments at the moment (in Phabricator). + +## Defining Paths + +`whitelist_path` and `blacklist_path` are optional, by default the rule is +enabled everywhere. For specifying paths, one can use either string constants +(`"File.m"`) or regexes (`REGEXP("path/to/.*")`) or variables. The variables +stand for a list of paths, and are defined in a separate block: + +```bash + GLOBAL-PATHS { + path1 = {"A.m", REGEXP("path/to/.*")}; + }; +``` + +## Defining Macros + +It is possible to define macros that can be used in several checkers. This is +done in the following way: + +```bash +GLOBAL-MACROS { + LET is_subclass_of(x) = + is_class(x) HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl; + }; +``` + +`GLOBAL-MACROS` is the section of an AL specification where one can define a +list of global macros. In the example we are defining the macro `is_subclass(x)` +which can now be used in checkers instead of its complex definition. + +It is possible to import a library of macros and paths with the following +command: + +``` +#IMPORT +``` + +In an AL file, the command above import and make available all the macros and +paths defined in the `library.al` file. + +## AL Predicates + +The simplest formulas we can write are predicates. They are defined inside +Infer. We provide a +[library](https://github.com/facebook/infer/blob/master/infer/src/clang/cPredicates.mli), +but if the predicate that you require is not available, you will need to extend +the library. Here are the some of the currently defined predicates: + +``` +call_class_method ("class_name", "method_name") +call_function ("method_name") +call_instance_method ("class_name", "method_name") +call_method ("method_name") +captures_cxx_references () +context_in_synchronized_block () +declaration_has_name ("decl_name") +declaration_ref_name ("decl_ref_name") +decl_unavailable_in_supported_ios_sdk () +has_cast_kind("cast_kind") // useful in a cast node +has_type ("type") // only builtin types, pointers and Objective-C classes available at the moment +isa ("class_name") +is_assign_property () +is_binop_with_kind ("kind") +is_class ("class_name") +is_const_var () +is_global_var () +is_ivar_atomic () +is_method_property_accessor_of_ivar () +is_node ("node_name") +is_objc_constructor () +is_objc_dealloc () +is_objc_extension () +is_objc_interface_named ("name") +is_property_pointer_type () +is_strong_property () +is_weak_property () +is_unop_with_kind ("kind") +method_return_type ("type") // only builtin type, pointers, and Objective-C classes available at the moment +objc_method_has_nth_parameter_of_type("type") +using_namespace("namespace") +within_responds_to_selector_block () +``` + +In general, the parameters of predicates can be constants, or variables, or +regular expressions. Variables are used in macros, see below. The syntax for +using regexes is `REGEX("your_reg_exp_here")`. + +**NOTE:** The predicates that expect types, such as `has_type` or +`method_return_type` or `objc_method_has_nth_parameter_of_type` also accept +regexes, but the syntax is a bit different: `REGEX('your_reg_exp_here')`, and +this regex can be embedded inside another string, for example: +`has_type("REGEXP('NS.+')*" )` which stands for pointer to a class of name +starting with NS. + +If you need to add a new predicate, write the predicate in +[cPredicates.ml](https://github.com/facebook/infer/blob/master/infer/src/clang/cPredicates.ml) +and then register it in +[CTL.ml](https://github.com/facebook/infer/blob/master/infer/src/clang/cTL.ml#L728). + +## AL Formulas + +Formulas are defined using a variation of the +[_CTL temporal logic_](https://en.wikipedia.org/wiki/Computation_tree_logic). +CTL is a logic expressing properties of a tree model. In the case of AL, the +tree is the AST of the program. Formulas are defined according to the following +grammar: + +``` +formula ::= predicate + | NOT formula + | formula1 OR formula2 + | formula1 AND formula2 + | formula1 IMPLIES formula2 + | formula1 HOLDS-UNTIL formula2 + | formula1 HOLDS-EVERYWHERE-UNTIL formula2 + | formula HOLDS-EVENTUALLY + | formula HOLDS-EVERYWHERE-EVENTUALLY + | formula HOLDS-NEXT + | formula HOLDS-EVERYWHERE-NEXT + | formula HOLDS-ALWAYS + | formula HOLDS-EVERYWHERE-ALWAYS + | WHEN formula HOLDS-IN-NODE node-name-list + | IN-NODE node-name-list WITH-TRANSITION transition-name + formula HOLDS-EVENTUALLY +``` + +The first four cases (`NOT`, `OR`, `AND`, `IMPLIES`) are classic boolean +operators with the usual semantics. The others are temporal operators describing +how the truth-value of a formula is evaluated in a tree. Let's consider case by +case. + +| Formula | Semantic meaning | +| ------------------- | :-------------------------------------------------------------------------------------------: | +| F1 _HOLDS-UNTIL_ F2 | from the current node, there exists a path where F1 holds at every node until F2 becomes true | + +An example is depicted in the following tree. When `F1` or `F2` hold in a node +this is indicated between square brackets. The formula `F1 HOLDS-UNTIL F2` holds +in the green nodes. + +![](/img/AL/holds_until.jpeg) + +--- + +| Formula | Semantic meaning | +| -------------------- | :--------------------------------------------------------------------------: | +| F _HOLDS-EVENTUALLY_ | from the current node there exists a path where at some point F becomes true | + +In the picture below, as `F` holds in `n10`, then `F HOLDS-EVENTUALLY` holds in +the green nodes `n1`, `n7`, `n10`. This is because from these nodes there is a +path reaching `n10` where `F` holds. Note that it holds for `n10` as well +because there exists a trivial path of length 0 from `n1` to itself. + +![](/img/AL/holds_eventually.jpeg) + +--- + +| Formula | Semantic meaning | +| ----------------------------- | :-----------------------------------------------------------------------: | +| F HOLDS-EVERYWHERE-EVENTUALLY | in every path starting from the current node at some point F becomes true | + +For example, in the tree below, the formula holds in every green node because +every paths starting from each of them eventually reaches a node where F holds. + +![](/img/AL/holds_everywhere_eventually.jpeg) + +--- + +| Formula | Semantic meaning | +| ------------ | :--------------------------------------------------------------------------: | +| F HOLDS-NEXT | from the current node (we are visiting) there exists a child where F is true | + +In the tree below, the formula `F HOLDS-NEXT` it is true only in n1 as it's the +only node with a child where `F` holds (node n3). In AL, `NEXT` is synonym of +child as, in terms of a path in the tree, a child is the next node. + +![](/img/AL/holds_next.jpeg) + +--- + +| Formula | Semantic meaning | +| ----------------------- | :-----------------------------------------------------: | +| F HOLDS-EVERYWHERE-NEXT | from the current node in every existing child F is true | + +In the tree below, the formula `F HOLDS-EVERYWHERE-NEXT` it is true in n1 as +it's the only node for which in every child `F` holds (node n2, n3, and n7). + +![](/img/AL/holds_everywhere_next.jpeg) + +--- + +| Formula | Semantic meaning | +| -------------- | :-------------------------------------------------------------------: | +| F HOLDS-ALWAYS | from the current node there exists a path where F holds at every node | + +In the tree below `F HOLDS-ALWAYS` holds in `n1`, `n2`, `n8` because for each of +these nodes there exists a path where `F` holds at each node in the path. + +![](/img/AL/always_holds.jpeg) + +--- + +| Formula | Semantic meaning | +| ------------------------- | :--------------------------------------------------------: | +| F HOLDS-EVERYWHERE-ALWAYS | from the current node, in every path F holds at every node | + +`F HOLDS-EVERYWHERE-ALWAYS` holds in `n2`, `n4`, `n5`, and `n8` because when we +visit those nodes in every path that start from them `F` holds in every node. + +![](/img/AL/always_holds_everywhere.jpeg) + +--- + +| Formula | Semantic meaning | +| ---------------------------------- | :----------------------------------------------: | +| WHEN F HOLDS-IN-NODE node1,…,nodeK | we are in a node among node1,…,nodeK and F holds | + +`WHEN F HOLDS-IN-NODE` `n2`, `n7`, `n6` holds only in node `n2` as it is the +only node in the list `n2`, `n7`, `n6` where F holds. + +![](/img/AL/holds_in_node.jpeg) + +Let's consider an example of checker using formula +`WHEN F HOLDS-IN-NODE node1,…,nodeK` for checking that a property with pointer +type should not be declared _"assign"_: + +``` +DEFINE-CHECKER ASSIGN_POINTER_WARNING = { + + SET report_when = + WHEN + is_assign_property() AND is_property_pointer_type() + HOLDS-IN-NODE ObjCPropertyDecl; + + SET message = "Property `%decl_name%` is a pointer type marked with the `assign` attribute"; + SET suggestion = "Use a different attribute like `strong` or `weak`."; + SET severity = "WARNING"; + }; +``` + +The checker uses two predefined predicates `is_assign_property()` and +`is_property_pointer_type()` which are true if the property being declared is +assign and has a pointer type respectively. We want to check both conditions +only on nodes declaring properties, i.e., `ObjCPropertyDecl`. + +--- + +| Formula | Semantic meaning | +| ----------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------: | +| IN-NODE node1,…, nodeK WITH-TRANSITION t F HOLDS-EVENTUALLY | from the current node there exists a path which eventually reaches a node among “node1,…,nodeK” with a transition t reaching a child where F holds | + +The following tree explain the concept: + +![](/img/AL/in_node_with_transition.jpeg) + +The concept of transition is needed because of the special structure of the +clang AST. Certain kind of nodes, for example statements, have a list of +children that are statements as well. In this case there is no special tag +attached to the edge between the node and the children. Other nodes have +records, where some of the fields point to other nodes. For example a node +representing a function declaration will have a record where one of the fields +is body. This is pointing to a statement representing the function's body. For +records, sometimes we need to specify that we need a particular node reachable +via a particular field (i.e., a transition). + +**Hint** A good way to learn how to write checkers is looking at existing +checkers in the file +[linters.al](https://github.com/facebook/infer/blob/master/infer/lib/linter_rules/linters.al). + +## Example checks + +In the following we show a few examples of simple checks you may wish to write +and the corresponding formulas: + +- A check for flagging a Objective-C class that inherits from a class that + shouldn't be subclassed. + +``` +DEFINE-CHECKER SUBCLASSING_TEST_EXAMPLE = { + SET report_when = is_class("A") HOLDS-IN-SOME-SUPERCLASS-OF ObjCInterfaceDecl; + SET message = "This is subclassing A. Class A should not be subclassed."; +}; +``` + +- A check for flagging an Objective-C instance method call: + +``` +DEFINE-CHECKER CALL_INSTANCE_METHOD = { + SET report_when = call_instance_method("A", "foo:"); + SET message = "Do not call this method"; +}; +``` + +- A check for flagging an Objective-C instance method call of any method of a + class: + +``` +DEFINE-CHECKER CALL_ANY_INSTANCE_METHODS = { + SET report_when = call_instance_method(A, REGEXP("*")); + SET message = "Do not call any method of class A"; +}; +``` + +- A check for flagging an Objective-C class method call: + +``` +DEFINE-CHECKER CALL_CLASS_METHOD = { + SET report_when = call_class_method("A", "foo:"); + SET message = "Do not call this method"; +}; +``` + +- A check for flagging an Objective-C method call of a method with int return + type: + +``` +DEFINE-CHECKER TEST_RETURN_METHOD = { + SET report_when = WHEN method_return_type("int") + HOLDS-IN-NODE ObjCMethodDecl; + SET message = "Method return int"; +}; +``` + +- A check for flagging a variable declaration with type long + +``` +DEFINE-CHECKER TEST_VAR_TYPE_CHECK = { + SET report_when = WHEN has_type("long") + HOLDS-IN-NODE VarDecl; + SET message = "Var %name% has type long"; +}; +``` + +- A check for flagging a method that has a parameter of type A\* + +``` +DEFINE-CHECKER TEST_PARAM_TYPE_CHECK = { + LET method_has_a_parameter_with_type(x) = + WHEN HOLDS-NEXT WITH-TRANSITION Parameters (has_type(x)) + HOLDS-IN-NODE ObjCMethodDecl; + SET report_when = + method_has_a_parameter_with_type("A*" ); + SET message = "Found a method with a parameter of type A"; +}; +``` + +- A check for flagging a method that has all the parameters of type A\* (and at + least one) + +``` +DEFINE-CHECKER TEST_PARAM_TYPE_CHECK2 = { + LET method_has_at_least_a_parameter = + WHEN HOLDS-NEXT WITH-TRANSITION Parameters (TRUE) + HOLDS-IN-NODE ObjCMethodDecl; + + LET method_has_all_parameter_with_type(x) = + WHEN HOLDS-EVERYWHERE-NEXT WITH-TRANSITION Parameters (has_type(x)) + HOLDS-IN-NODE ObjCMethodDecl; + + SET report_when = method_has_at_least_a_parameter AND + method_has_all_parameter_with_type("int"); + SET message = "All the parameters of the method have type int"; +}; +``` + +- A check for flagging a method that has the 2nd parameter of type A\* + +``` +DEFINE-CHECKER TEST_NTH_PARAM_TYPE_CHECK = { + SET report_when = + WHEN objc_method_has_nth_parameter_of_type("2", "A*") + HOLDS-IN-NODE ObjCMethodDecl; + SET message = "Found a method with the 2nd parameter of type A*"; + SET severity = "LIKE"; +}; +``` + +- A check for flagging a protocol that inherits from a given protocol. + `HOLDS-EVENTUALLY WITH-TRANSITION Protocol` means follow the `Protocol` branch + in the AST until the condition holds. + +``` +DEFINE-CHECKER TEST_PROTOCOL_DEF_INHERITANCE = { + LET is_subprotocol_of(x) = declaration_has_name(x) HOLDS-EVENTUALLY WITH-TRANSITION Protocol; + SET report_when = + WHEN is_subprotocol_of("P") + HOLDS-IN-NODE ObjCProtocolDecl; + SET message = "Do not inherit from Protocol P"; +}; +``` + +- A check for flagging when a constructor is defined with a parameter of a type + that implements a given protocol (or that inherits from it). + `HOLDS-NEXT WITH-TRANSITION Parameters` means, starting in the + `ObjCMethodDecl` node, follow the `Parameters` branch in the AST and check + that the condition holds there. + +``` +DEFINE-CHECKER TEST_PROTOCOL_TYPE_INHERITANCE = { + + LET method_has_parameter_subprotocol_of(x) = + WHEN + HOLDS-NEXT WITH-TRANSITION Parameters + (has_type_subprotocol_of(x)) + HOLDS-IN-NODE ObjCMethodDecl; + + SET report_when = + WHEN + declaration_has_name(REGEXP("^newWith.*:$")) AND + method_has_parameter_subprotocol_of("P") + HOLDS-IN-NODE ObjCMethodDecl; + + SET message = "Do not define parameters of type P."; +}; +``` + +- A check for flagging a variable declaration of type NSArray applied to A. + +``` +DEFINE-CHECKER TEST_GENERICS_TYPE = { + SET report_when = + WHEN has_type("NSArray*") + HOLDS-IN-NODE VarDecl; + SET message = "Do not create arrays of type A"; +}; +``` + +- A check for flagging using a property or variable that is not available in the + supported API. decl_unavailable_in_supported_ios_sdk is a predicate that works + on a declaration, checks the available attribute from the declaration and + compares it with the supported iOS SDK. Notice that we flag the occurrence of + the variable or property, but the attribute is in the declaration, so we need + the transition `PointerToDecl` that follows the pointer from the usage to the + declaration. + +``` +DEFINE-CHECKER UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK = { + SET report_when = + WHEN HOLDS-NEXT WITH-TRANSITION PointerToDecl + (decl_unavailable_in_supported_ios_sdk() AND + HOLDS-IN-NODE DeclRefExpr; + SET message = "%name% is not available in the required iOS SDK version"; +}; +``` + +- A check for flagging using a given namespace + +``` +DEFINE-CHECKER TEST_USING_NAMESPACE = { + SET report_when = using_namespace("N"); + SET message = "Do not use namespace N"; +}; +``` + +- A check for flagging the use of given enum constants + +``` +DEFINE-CHECKER ENUM_CONSTANTS = { + SET report_when = is_enum_constant(REGEXP("MyName.*")); + SET message = "Do not use the enum MyName"; +}; +``` + +## AST info in messages + +When you write the message of your rule, you may want to specify which +particular AST items were involved in the issue, such as a type or a variable +name. We have a mechanism for that, we specified a few placeholders that can be +used in rules with the syntax `%placeholder%` and it will be substituted by the +correct AST info. At the moment we have `%type%`, `%child_type%` and `%name%` +that print the type of the node, the type of the node's child, and a string +representation of the node, respectively. As with predicates, we can add more as +needed. + +## Testing your rule + +To test your rule you need to run it with Infer. If you are adding a new linter +you can test it in a separate al file that you can pass to Infer with the option +`--linters-def-file file.al`. Pass the option +`--linters-developer-mode --linter ` to Infer to print debug +information and only run the linter you are developing, so it will be faster and +the debug info will be only about your linter. + +To test your code, write a small example that triggers the rule. Then, run your +code with + +``` +infer --linters-developer-mode --linters-def-file file.al -- clang -c Test.m +``` + +the bug should be printed in the screen, like, for instance: + +``` +infer/tests/codetoanalyze/objcpp/linters/global-var/B.mm:34: warning: GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL + Global variable kLineSize is initialized using a function or method call at line 34, column 1. If the function/method call is expensive, + it can affect the starting time of the app. + 32. static float kPadding = [A bar] ? 10.0 : 11.0; // Error + 33. + 34. > static const float kLineSize = 1 / [A scale]; // Error + 35. + 36. static const float ok = 37; + 37. +``` + +Moreover, the bug can be found in the file `infer-out/report.json` where +`infer-out` is the results directory where Infer operates, that is created in +the current directory. You can specify a different directory with the option +`-o`. + +## Debugging + +If there are syntax errors or other parsing errors with your al file, you will +get an error message when testing the rule, remember to use +`linters-developer-mode` when you are developing a rule. If the rule gets parsed +but still doesn't behave as you expect, you can debug it, by adding the +following line to a test source file in the line where you want to debug the +rule: `//INFER_BREAKPOINT`. Then run infer again in linters developer mode, and +it will stop the execution of the linter on the line of the breakpoint. Then you +can follow the execution step by step. It shows the current formula that is +being evaluated, and the current part of the AST that is being checked. A red +node means that the formula failed, a green node means that it succeeded. + +## Demo + + + +## Command line options for linters + +The linters are run by default when you run Infer. However, there is a way of +running only the linters, which is faster than also running Infer. This is by +adding the option `--linters` to the analysis command as in this example: + +```bash +infer run --linters -- clang -c Test.m +``` + +There are a few other command-line options that are useful for using or +developing new linters in Infer. Read about them in the [`infer capture` manual](man-pages). diff --git a/infer/documentation/checkers/Eradicate.md b/infer/documentation/checkers/Eradicate.md new file mode 100644 index 000000000..fda2978e9 --- /dev/null +++ b/infer/documentation/checkers/Eradicate.md @@ -0,0 +1,75 @@ +> "I call it my billion-dollar mistake. It was the invention of the null +> reference in 1965." +> +> [Tony Hoare](http://en.wikipedia.org/wiki/Tony_Hoare) + +### What is Infer:Eradicate? + +Infer:Eradicate is a type checker for `@Nullable` annotations for Java. It is part +of the Infer static analysis suite of tools. The goal is to eradicate null +pointer exceptions. + +@Nullable +annotations denote that a parameter, field or the return value of a method can +be null. When decorating a parameter, this denotes that the parameter can +legitimately be null and the method will need to deal with it. When decorating a +method, this denotes the method might legitimately return null. + +Starting from @Nullable-annotated programs, the checker performs a flow +sensitive analysis to propagate the nullability through assignments and calls, +and flags errors for unprotected accesses to nullable values or +inconsistent/missing annotations. It can also be used to add annotations to a +previously un-annotated program. + +### What is the @Nullable convention? + +If you say nothing, you're saying that the value cannot be null. This is the +recommended option when possible: + +Program safely, annotate nothing! + +When this cannot be done, add a @Nullable annotation before the type to indicate +that the value can be null. + +### What is annotated? + +Annotations are placed at the interface of method calls and field accesses: + +- Parameters and return type of a method declaration. +- Field declarations. + +Local variable declarations are not annotated: their nullability is inferred. + +### How is Infer:Eradicate invoked? + +Eradicate can be invoked by adding the option `--eradicate` to the checkers mode +as in this example: + +```bash +infer run -a checkers --eradicate -- javac Test.java +``` + +The checker will report an error on the following program that accesses a +nullable value without null check: + +```java +class C { + int getLength(@Nullable String s) { + return s.length(); + } +} +``` + +But it will not report an error on this guarded dereference: + +```java +class C { + int getLength(@Nullable String s) { + if (s != null) { + return s.length(); + } else { + return -1; + } + } +} +``` diff --git a/infer/documentation/checkers/Quandary.md b/infer/documentation/checkers/Quandary.md new file mode 100644 index 000000000..245d699df --- /dev/null +++ b/infer/documentation/checkers/Quandary.md @@ -0,0 +1,8 @@ +Quandary is a static taint analyzer that identifies a variety of unsafe +information flows. It has a small list of built-in +[sources](https://github.com/facebook/infer/blob/master/infer/src/quandary/JavaTrace.ml#L36) +and +[sinks](https://github.com/facebook/infer/blob/master/infer/src/quandary/JavaTrace.ml#L178), +and you can define custom sources and sinks in your `.inferconfig` file (see +example +[here](https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/quandary/.inferconfig)). diff --git a/infer/documentation/checkers/RacerD.md b/infer/documentation/checkers/RacerD.md new file mode 100644 index 000000000..9a62410bc --- /dev/null +++ b/infer/documentation/checkers/RacerD.md @@ -0,0 +1,489 @@ +RacerD finds data races in your C++ and Java code. This page gives a more in-depth +explanation of how the analysis works *for Java code*, but may be less complete than the +[Thread Safety Violation bug description page](#thread-safety-violation). + +To run the analysis, you can use plain `infer` (to run RacerD along with other +analyses that are run by default) or `infer --racerd-only` (to run only RacerD). + +For example, the command `infer --racerd-only -- javac File.java` will run +RacerD on File.java. + +## Background + +RacerD statically analyzes Java code to detect potential concurrency bugs. This +analysis does not attempt to prove the absence of concurrency issues, rather, it +searches for a high-confidence class of data races. At the moment RacerD +concentrates on race conditions between methods in a class that is itself +intended to be thread safe. A race condition occurs when there are two +concurrent accesses to a class member variable that are not separated by mutual +exclusion, and at least one of the accesses is a write. Mutual exclusion can be +ensured by synchronization primitives such as locks, or by knowledge that both +accesses occur on the same thread. + +## Triggering the analysis + +RacerD doesn't try to check _all_ code for concurrency issues; it only looks at +code that it believes can run in a concurrent context. There are two signals +that RacerD looks for: (1) Explicitly annotating a class/method with +`@ThreadSafe` and (2) using a lock via the `synchronized` keyword. In both +cases, RacerD will look for concurrency issues in the code containing the signal +and all of its dependencies. In particular, it will report races between any +non-`private` methods of the same class that can peform conflicting accesses. +Annotating a class/interface with `@ThreadSafe` also triggers checking for all +of the subclasses of the class/implementations of the interface. + +## Warnings + +Let's take a look at the different types of concurrency issues that RacerD +flags. Two of the warning types are data races (`Unprotected write` and +`Read/write race`), and the third warning type encourages adding `@ThreadSafe` +annotations to interfaces to trigger additional checking. + +### Unprotected write + +RacerD will report an unprotected write when one or more writes can run in +parallel without synchronization. These come in two flavors: (1) a self-race (a +write-write race that occurs due to a method running in parallel with itself) +and (2) two conflicting writes to the same location. Here's an example of the +self-race flavor: + +``` +@ThreadSafe +public class Dinner { + private int mTemperature; + + public void makeDinner() { + boilWater(); + } + + private void boilWater() { + mTemperature = 100; // unprotected write. + } +} +``` + +The class `Dinner` will generate the following report on the public method +`makeDinner()`: + +`There may be a Thread Safety Violation: makeDinner() indirectly writes to mTemperature outside of synchronization.` + +This warning can be fixed by synchronizing the access to `mTemperature`, making +`mTemperature` `volatile`, marking `makeDinner` as `@VisibleForTesting`, or +suppressing the warning by annotating the `Dinner` class or `makeDinner` method +with `@ThreadSafe(enableChecks = false)`. + +### Read/Write Race + +We sometimes need to protect read accesses as well as writes. Consider the +following class with unsynchronized methods. + +``` +@ThreadSafe +public class Account { + + int mBalance = 0; + + public void deposit(int amount) { + if (amount > 0) { + mBalance += amount; + } + } + + public int withdraw(int amount){ + if (amount >= 0 && mBalance - amount >= 0) { + mBalance -= amount; + return mBalance; + } else { + return 0; + } + } +} +``` + +If you run the `withdraw()` method in parallel with itself or with `deposit()` +you can get unexpected results here. For instance, if the stored balance is 11 +and you run `withdraw(10)` in parallel with itself you can get a negative +balance. Furthermore, if you synchronize only the write statement +`mBalance -= amount`, then you can still get this bad result. The reason is that +there is a read/write race between the boolean condition +`mBalance - amount >= 0` and the writes. RacerD will duly warn + +`Read/Write race. Public method int Account.withdraw(int) reads from field Account.mBalance. Potentially races with writes in methods void Account.deposit(int), int Account.withdraw(int)` + +on the line with this boolean condition. + +A solution to the threading problem here is to make both methods `synchronized` +to wrap both read and write accesses, or to use an `AtomicInteger` for +`mBalance` rather than an ordinary `int`. + +### Interface not thread-safe + +In the following code, RacerD will report an `Interface not thread-safe` warning +on the call to `i.bar()`: + +``` +interface I { + void bar(); +} + +@ThreadSafe +class C { + void foo(I i) { + i.bar(); // RacerD warns here + } +} +``` + +The way to fix this warning is to add a `@ThreadSafe` annotation to the +interface `I`, which will enforce the thread-safety of each of the +implementations of `I`. + +You might wonder why it's necessary to annotate `I` -- can't RacerD just look at +all the implementations of `i` at the call site for `bar`? Although this is a +fine idea idea in principle, it's a bad idea in practice due to a (a) separate +compilation and (b) our diff-based deployment model. In the example above, the +compiler doesn't have to know about all implementations (or indeed, any +implementations) of `I` at the time it compiles this code, so there's no +guarantee that RacerD will know about or be able to check all implementations of +`I`. That's (a). For (b), say that we check that all implementations of `I` are +thread-safe at the time this code is written, but we don't add the annotation. +If someone else comes along and adds a new implementation of `I` that is not +thread-safe, RacerD will have no way of knowing that this will cause a potential +bug in `foo`. But if `I` is annotated, RacerD will enforce that all new +implementations of `I` are thread-safe, and `foo` will remain bug-free. + +## Annotations to help RacerD understand your code + +Getting started with RacerD doesn't require any annotations at all -- RacerD +will look at your usage of locks and figure out what data is not guarded +consistently. But increasing the coverage and signal-to-noise ratio may require +adding `@ThreadSafe` annotations along with some of the other annotations +described below. Most of annotations described below can be used via the Maven +Central package available +[here](https://maven-repository.com/artifact/com.facebook.infer.annotation/infer-annotation). + +### `@ThreadConfined` + +The intuitive idea of thread-safety is that a class is impervious to concurrency +issues for all concurrent contexts, even those that have not been written yet +(it is future-proof). RacerD implements this by naively assuming that any method +can potentially be called on any thread. You may determine, however, that an +object, method, or field is only ever accessed on a single thread during program +execution. Annotating such elements with `@ThreadConfined` informs RacerD of +this restriction. Note that a thread-confined method cannot race with itself but +it can still race with other methods. + +``` +List mCache; + +@ThreadConfined(UI) +void prepareCache() { + // populate the cache + mCache.add(...); + // post cache cleanup task to run later + mUIExecutor.execute(new Runnable() { + @ThreadConfined(UI) + public void run() { + mCache.clear(); + } + }); +} +``` + +In this example, both `prepareCache` and `run` touch `mCache`. But there's no +possibility of a race between the two methods because both of them will run +sequentially on the UI thread. Adding a `@ThreadConfined(UI)` or `@UiThread` +annotation to these methods will stop it from warning that there is a race on +`mCache`. We could also choose to add a `@ThreadConfined` annotation to `mCache` +itself. + +### `@Functional` + +Not all races are bugs; a race can be benign. Consider the following: + +``` +@Functional Boolean askNetworkIfShouldShowFeature(); + +private Boolean mShouldShowFeature; + +@ThreadSafe boolean shouldShowFeature() { + if (mShouldShowFeature == null) { + mShouldShowFeature = askNetworkIfShouldShowFeature(); + } + return mShouldShowFeature; +} +``` + +This code caches the result of an expensive network call that checks whether the +current user should be shown an experimental feature. This code looks racy, and +indeed it is: if two threads execute `shouldShowFeature()` at the same time, one +may read `mShouldShowFeature` at the same time the other is writing it. + +However, this is actually a _benign_ race that the programmer intentionally +allows for performance reasons. The reason this code is safe is that the +programmer knows that `askNetworkIfShouldShowFeature()` will always return the +same value in the same run of the app. Adding synchronization would remove the +race, but acquiring/releasing locks and lock contention would potentially slow +down every call to `shouldShowFeature()`. The benign race approach makes every +call after the first fast without changing the safety of the code. + +RacerD will report a race on this code by default, but adding the +`@Functional annotation to askNetworkIfShouldShowFeature()` informs RacerD that +the function is always expected to return the same value. This assumption allows +RacerD to understand that this particular code is safe, though it will still +(correctly) warn if `mShouldShowFeature` is read/written elsewhere. + +Be sure not to use the `@Functional` pattern for _singleton instantiation_, as +it's possible the "singleton" can be constructed more than once. + +``` +public class MySingleton { + private static sInstance; + + // Not @Functional + public MySingleton getInstance() { + if (sInstance == null) { + // Different threads may construct their own instances. + sInstance == new MySingleton(); + } + return sInstance; + } +} +``` + +### `@ReturnsOwnership` + +RacerD does not warn on unprotected writes to _owned_ objects. An object is +owned if it has been freshly allocated in the current thread and has not escaped +to another thread. RacerDf automatically tracks ownership in most cases, but it +needs help with `abstract` and `interface` methods that return ownership: + +``` +@ThreadSafe +public interface Car { + @ReturnsOwnership abstract Car buyCar(); + + void carsStuff() { + Car myCar = new Car(); + myCar.wheels = 4; // RacerD won't warn here because it knows myCar is owned + Car otherCar = buyCar(); + otherCar.wheels = 3; // RacerD would normally warn here, but won't because of the `@ReturnsOwnership` annotation + } +} +``` + +### `@VisibleForTesting` + +RacerD reports races between any two non`-private` methods of a class that may +run in a concurrent context. Sometimes, a RacerD report may be false because one +of the methods cannot actually be called from outside the current class. One fix +is making the method `private` to enforce this, but this might break unit tests +that need to call the method in order to test it. In this case, the +`@VisibleForTesting` annotation will allow RacerD to consider the method as +effectively `private` will still allowing it to be called from the unit test: + +``` +@VisibleForTesting void setF() { + this.f = ...; // RacerD would normally warn here, but @VisibleForTesting will silence the warning +} + +synchronized void setFWithLock() { + setF(); +} +``` + +Unlike the other annotations shown here, this one lives in +[Android](https://developer.android.com/reference/android/support/annotation/VisibleForTesting.html). + +## Interprocedural Reasoning + +An important feature of RacerD is that it finds races by analyzing not just one +file or class, but by looking at memory accesses that occur after going through +several procedure calls. It handles this even between classes and between files. + +Here is a very basic example + +``` +@ThreadSafe +class A{ + + void m1(B bb) { + bb.meth_write(); + } +} + +class B{ + Integer x; + + void meth_write() { + x = 88; + } + +} +``` + +Class `B` is not annotated `@ThreadSafe` and does not have any locks, so RacerD +does not directly look for threading issues there. However, method `m1()` in +class `A` has a potential self-race, if it is run in parallel with itself and +the same argument for each call. RacerD discovers this. + +``` +InterProc.java:17: error: THREAD_SAFETY_VIOLATION + Unprotected write. Non-private method `A.m1` indirectly writes to field `&this.B.x` outside of synchronization. + Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in + parallel with other non-private methods in the class (incuding itself). + 15. + 16. void m1(B bb) { + 17. > bb.meth_write(); + 18. } + 19. } +``` + +RacerD does this sort of reasoning using what is known as a _compositional +inteprocedural analysis_. There, each method is analyzed independently of its +context to produce a summary of the behaviour of the procedure. In this case the +summaries for `m1()' and`meth()' include information as follows. + +``` +Procedure: void A.m1(B) +Accesses: { Unprotected({ 1 }) -> { Write to &bb.B.x at void B.meth_write() at line 17 } } + +Procedure: void B.meth_write() +Accesses { Unprotected({ 0 }) -> { Write to &this.B.x at at line 25 } } +``` + +The descriptions here are cryptic and do not include all the information in the +summaries, but the main point is that you can use RacerD to look for races in +codebases where the mutations done by threads might occur only after a chain of +procedure calls. + +## Context and Selected Related Work + +Reasoning about concurrency divides into bug detection and proving absence of +bugs. RacerD is on the detection side of reasoning. + +The rapid growth in the number of interleavings is problematic for tools that +attempt exhaustive exploration. With just 150 instructions for two threads, the +number 10^88 of interleavings is more that the estimated number of atoms in the +known universe. +[There has been important work which uses various techniques to attempt to reduce the number of interleavings](https://en.wikipedia.org/wiki/Partial_order_reduction) +while still in principle covering all possibilities, but scale is still a +challenge. Note that RacerD is not exhaustive: it has false negatives (missed +bugs). But in compensation it is fast, and effective (it finds bugs in +practice). + +Static analysis for concurrency has attracted a lot of attention from +researchers, but difficulties with scalability and precision have meant that +previous techniques have had little industrial impact. Automatic static race +detection itself has seen significant work. The most advanced approaches, +exemplified by the [Chord](http://www.cis.upenn.edu/~mhnaik/pubs/pldi06.pdf) +tool, often use a whole-program analysis paired with a sophisticated alias +analysis, two features we have consciously avoided. Generally speaking, the +leading research tools can be more precise, but RacerD is faster and can operate +without the whole program: we have opted to go for speed in a way that enables +industrial deployment on a large, rapidly changing codebase, while trying to use +as simple techniques as possible to cover many (not all) of the patterns covered +by slower but precise research tools. + +An industrial static analysis tool from +[Contemplate](http://homepages.inf.ed.ac.uk/dts/pub/avocs2015.pdf) also targets +@ThreadSafe annotations, but limits the amount of inter-procedural reasoning: +“This analysis is interprocedural, but to keep the overall analysis scalable, +only calls to private and protected methods on the same class are followed”. +RacerD does deep, cross-file and cross-class inter-procedural reasoning, and yet +still scales; the inter-class capability was one of the first requests from +Facebook engineers. +[A separate blog post looked at 100 recent data race fixes](https://code.facebook.com/posts/1537144479682247/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/) +in Infer's deployment in various bug categories, and for data races observed +that 53 of them were inter-file (and thus involving multiple classes). +[See above](racerd#interprocedural) for an example of RacerD's interprocedural +capabilities. + +One reaction to the challenge of developing effective static race detectors has +been to ask the programmer to do more work to help the analyzer. Examples of +this approach include the +[Clang Thread Safety Analyzer](https://clang.llvm.org/docs/ThreadSafetyAnalysis.html), +the typing of [locks](https://doc.rust-lang.org/std/sync/struct.Mutex.html) in +Rust, and the use/checking of @GuardedBy annotations in +[Java](https://homes.cs.washington.edu/~mernst/pubs/locking-semantics-nfm2016.pdf) +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, and we +have +[GuardedBy checking as part of Infer](checkers-bug-types#UNSAFE_GUARDEDBY_ACCESS) +(though separate from the race detector). Our GuardedBy checker can find some +bugs that RacerD does not (see +[this example on anonymous inner classes](checkers-bug-types#anonymous_inner)), +but the race detector finds a greater number because it can work on un-annotated +code. It is possible to have a very effective race analysis without decreeing +that such annotations must be present. This was essential for our deployment, +since _requiring_ lock annotations would have been a show stopper for converting +many thousands of lines of code to a concurrent context. We believe that this +finding should be transportable to new type systems and language designs, as +well as to other analyses for existing languages. + +Another reaction to difficulties in static race detection has been to instead +develop dynamic analyses, automatic testing tools which work by running a +program to attempt to find flaws. Google's Thread Sanitizer is a widely used and +mature tool in this area, which has been used in production to find many bugs in +C-family languages. +[The Thread Sanitizer authors explicitly call out limitations with static race analyzers](http://www.cs.columbia.edu/~junfeng/11fa-e6121/papers/thread-sanitizer.pdf) +as part of their motivation: “It seems unlikely that static detectors will work +effectively in our environment: Google’s code is large and complex enough that +it would be expensive to add the annotations required by a typical static +detector”. + +We have worked to limit the annotations that RacerD needs, for reasons similar +those expressed by the Thread Sanitizer authors. And we have sought to bring the +complementary benefits of static analysis — possibility of cheaper analysis and +fast reporting, and ability to analyze code before it is placed in a context to +run — to race detection. But we are interested as well in the future in +leveraging ideas in the dynamic techniques to improve or add to our analysis for +race detection. + +## Limitations + +There are a number of known limitations to the design of the race detector. + +- It looks for races involving syntactically identical access paths, and misses + races due to aliasing +- It misses races that arise from a locally declared object escaping its scope +- It uses a boolean locks abstraction, and so misses races where two accesses + are mistakenly protected by different locks +- It assumes a deep ownership model, which misses races where local objects + refer to or contain non-owned objects. +- It avoids reasoning about weak memory and Java's volatile keyword + +Most of these limitations are consistent with the design goal of reducing false +positives, even if they lead to false negatives. They also allow technical +tradeoffs which are different than if we were to favour reduction of false +negatives over false positives. + +A different kind of limitation concerns the bugs searched for: Data races are +the most basic form of concurrency error, but there are many types of +concurrency issues out there that RacerD does not check for (but might in the +future). Examples include deadlock, atomicity, and check-then-act bugs (shown +below). You must look for these bugs yourself! + +``` +@ThreadSafe +public class SynchronizedList { + synchronized boolean isEmpty() { ... } + synchronized T add(T item) { ... } + +// Not thread safe!!! +public class ListUtil { + public void addIfEmpty(SynchronizedList list, T item) { + if (list.isEmpty()) { + // In a race, another thread can add to the list here. + list.add(item); + } + } +} +``` + +Finally, using `synchronized` blindly as a means to fix every unprotected write +or read is not always safe. Even with RacerD, finding, understanding, and fixing +concurrency issues is difficult. If you would like to learn more about best +practices, [Java Concurrency in Practice](http://jcip.net/) is an excellent +resource. diff --git a/infer/documentation/checkers/Starvation.md b/infer/documentation/checkers/Starvation.md new file mode 100644 index 000000000..55643eedb --- /dev/null +++ b/infer/documentation/checkers/Starvation.md @@ -0,0 +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) +- doing expensive operations on the Android UI thread diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 388da23e0..8a317a8f9 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -14,31 +14,32 @@ DESCRIPTION OPTIONS --annotation-reachability - Activates: the annotation reachability checker. Given a pair of - source and sink annotation, e.g. @PerformanceCritical and - @Expensive, this checker will warn whenever some method annotated - with @PerformanceCritical calls, directly or indirectly, another - method annotated with @Expensive (Conversely: + Activates: checker annotation-reachability: Given a pair of source + and sink annotation, e.g. `@PerformanceCritical` and `@Expensive`, + this checker will warn whenever some method annotated with + `@PerformanceCritical` calls, directly or indirectly, another + method annotated with `@Expensive` (Conversely: --no-annotation-reachability) --annotation-reachability-only - Activates: Enable --annotation-reachability and disable all other + Activates: Enable annotation-reachability and disable all other checkers (Conversely: --no-annotation-reachability-only) --no-biabduction - Deactivates: the separation logic based bi-abduction analysis - using the checkers framework (Conversely: --biabduction) + Deactivates: checker biabduction: This analysis deals with a range + of issues, many linked to memory safety. (Conversely: + --biabduction) --biabduction-only - Activates: Enable --biabduction and disable all other checkers + Activates: Enable biabduction and disable all other checkers (Conversely: --no-biabduction-only) --bufferoverrun - Activates: the buffer overrun analysis (Conversely: - --no-bufferoverrun) + Activates: checker bufferoverrun: InferBO is a detector for + out-of-bounds array accesses. (Conversely: --no-bufferoverrun) --bufferoverrun-only - Activates: Enable --bufferoverrun and disable all other checkers + Activates: Enable bufferoverrun and disable all other checkers (Conversely: --no-bufferoverrun-only) --changed-files-index file @@ -47,11 +48,11 @@ OPTIONS relative to project root or be absolute --class-loads - Activates: Java class loading analysis (Conversely: - --no-class-loads) + Activates: checker class-loads: Compute set of Java classes + loaded. (Conversely: --no-class-loads) --class-loads-only - Activates: Enable --class-loads and disable all other checkers + Activates: Enable class-loads and disable all other checkers (Conversely: --no-class-loads-only) --continue-analysis @@ -61,12 +62,13 @@ OPTIONS --incremental-analysis. (Conversely: --no-continue-analysis) --cost - Activates: checker for performance cost analysis (Conversely: - --no-cost) + Activates: checker cost: Computes the time complexity of functions + and methods. Can be used to detect changes in runtime complexity + with `infer reportdiff`. (Conversely: --no-cost) --cost-only - Activates: Enable --cost and disable all other checkers - (Conversely: --no-cost-only) + Activates: Enable cost and disable all other checkers (Conversely: + --no-cost-only) --custom-symbols json Specify named lists of symbols available to rules @@ -103,24 +105,24 @@ OPTIONS --no-default-checkers Deactivates: Default checkers: --biabduction, --fragment-retains-view, --inefficient-keyset-iterator, --linters, - --liveness, --racerd, --siof, --self_in_block, --starvation, + --liveness, --racerd, --siof, --self-in-block, --starvation, --uninit (Conversely: --default-checkers) --eradicate - Activates: the eradicate @Nullable checker for Java annotations - (Conversely: --no-eradicate) + Activates: checker eradicate: The eradicate `@Nullable` checker + for Java annotations. (Conversely: --no-eradicate) --eradicate-only - Activates: Enable --eradicate and disable all other checkers + Activates: Enable eradicate and disable all other checkers (Conversely: --no-eradicate-only) --no-fragment-retains-view - Deactivates: detects when Android fragments are not explicitly - nullified before becoming unreabable (Conversely: - --fragment-retains-view) + Deactivates: checker fragment-retains-view: Detects when Android + fragments are not explicitly nullified before becoming + unreachable. (Conversely: --fragment-retains-view) --fragment-retains-view-only - Activates: Enable --fragment-retains-view and disable all other + Activates: Enable fragment-retains-view and disable all other checkers (Conversely: --no-fragment-retains-view-only) --help @@ -136,30 +138,32 @@ OPTIONS section --immutable-cast - Activates: the detection of object cast from immutable type to - mutable type. For instance, it will detect cast from ImmutableList - to List, ImmutableMap to Map, and ImmutableSet to Set. - (Conversely: --no-immutable-cast) + Activates: checker immutable-cast: Detection of object cast from + immutable types to mutable types. For instance, it will detect + casts from `ImmutableList` to `List`, `ImmutableMap` to `Map`, and + `ImmutableSet` to `Set`. (Conversely: --no-immutable-cast) --immutable-cast-only - Activates: Enable --immutable-cast and disable all other checkers + Activates: Enable immutable-cast and disable all other checkers (Conversely: --no-immutable-cast-only) --impurity - Activates: [EXPERIMENTAL] Impurity analysis (Conversely: - --no-impurity) + Activates: checker impurity: Detects functions with potential + side-effects. Same as "purity", but implemented on top of Pulse. + (Conversely: --no-impurity) --impurity-only - Activates: Enable --impurity and disable all other checkers + Activates: Enable impurity and disable all other checkers (Conversely: --no-impurity-only) --no-inefficient-keyset-iterator - Deactivates: Check for inefficient uses of keySet iterator that - access both the key and the value. (Conversely: - --inefficient-keyset-iterator) + Deactivates: checker inefficient-keyset-iterator: Check for + inefficient uses of iterators that iterate on keys then lookup + their values, instead of iterating on key-value pairs directly. + (Conversely: --inefficient-keyset-iterator) --inefficient-keyset-iterator-only - Activates: Enable --inefficient-keyset-iterator and disable all + Activates: Enable inefficient-keyset-iterator and disable all other checkers (Conversely: --no-inefficient-keyset-iterator-only) --jobs,-j int @@ -170,34 +174,37 @@ OPTIONS (Conversely: --no-keep-going) --no-linters - Deactivates: syntactic linters (Conversely: --linters) + Deactivates: checker linters: Declarative linting framework over + the Clang AST. (Conversely: --linters) --linters-only - Activates: Enable --linters and disable all other checkers + Activates: Enable linters and disable all other checkers (Conversely: --no-linters-only) --litho-required-props - Activates: [EXPERIMENTAL] Required Prop check for Litho - (Conversely: --no-litho-required-props) + Activates: checker litho-required-props: Checks that all + non-option `@Prop`s have been specified when constructing Litho + components. (Conversely: --no-litho-required-props) --litho-required-props-only - Activates: Enable --litho-required-props and disable all other + Activates: Enable litho-required-props and disable all other checkers (Conversely: --no-litho-required-props-only) --no-liveness - Deactivates: the detection of dead stores and unused variables - (Conversely: --liveness) + Deactivates: checker liveness: Detection of dead stores and unused + variables. (Conversely: --liveness) --liveness-only - Activates: Enable --liveness and disable all other checkers + Activates: Enable liveness and disable all other checkers (Conversely: --no-liveness-only) --loop-hoisting - Activates: checker for loop-hoisting (Conversely: - --no-loop-hoisting) + Activates: checker loop-hoisting: Detect opportunities to hoist + function calls that are invariant outside of loop bodies for + efficiency. (Conversely: --no-loop-hoisting) --loop-hoisting-only - Activates: Enable --loop-hoisting and disable all other checkers + Activates: Enable loop-hoisting and disable all other checkers (Conversely: --no-loop-hoisting-only) --perf-profiler-data-file file @@ -212,13 +219,13 @@ OPTIONS --no-print-logs) --printf-args - Activates: the detection of mismatch between the Java printf - format strings and the argument types For, example, this checker - will warn about the type error in `printf("Hello %d", "world")` - (Conversely: --no-printf-args) + Activates: checker printf-args: Detect mismatches between the Java + `printf` format strings and the argument types For example, this + checker will warn about the type error in `printf("Hello %d", + "world")` (Conversely: --no-printf-args) --printf-args-only - Activates: Enable --printf-args and disable all other checkers + Activates: Enable printf-args and disable all other checkers (Conversely: --no-printf-args-only) --progress-bar-style { auto | plain | multiline } @@ -229,7 +236,7 @@ OPTIONS Specify the root directory of the project --pulse - Activates: [EXPERIMENTAL] memory and lifetime analysis + Activates: checker pulse: Memory and lifetime analysis. (Conversely: --no-pulse) --pulse-cut-to-one-path-procedures-pattern string @@ -248,22 +255,27 @@ OPTIONS Pulse. Accepted formats are method or namespace::method --pulse-only - Activates: Enable --pulse and disable all other checkers + Activates: Enable pulse and disable all other checkers (Conversely: --no-pulse-only) --purity - Activates: [EXPERIMENTAL] Purity analysis (Conversely: + Activates: checker purity: Detects pure (side-effect-free) + functions. A different implementation of "impurity". (Conversely: --no-purity) --purity-only - Activates: Enable --purity and disable all other checkers + Activates: Enable purity and disable all other checkers (Conversely: --no-purity-only) --quandary - Activates: the quandary taint analysis (Conversely: --no-quandary) + Activates: checker quandary: The Quandary taint analysis detects + flows of values between sources and sinks, except if the value + went through a "sanitizer". In addition to some defaults, users + can specify their own sources, sinks, and sanitizers functions. + (Conversely: --no-quandary) --quandary-only - Activates: Enable --quandary and disable all other checkers + Activates: Enable quandary and disable all other checkers (Conversely: --no-quandary-only) --quiet,-q @@ -271,11 +283,11 @@ OPTIONS --no-quiet | -Q) --no-racerd - Deactivates: the RacerD thread safety analysis (Conversely: + Deactivates: checker racerd: Thread safety analysis. (Conversely: --racerd) --racerd-only - Activates: Enable --racerd and disable all other checkers + Activates: Enable racerd and disable all other checkers (Conversely: --no-racerd-only) --reactive,-r @@ -294,21 +306,23 @@ OPTIONS --results-dir,-o dir Write results and internal files in the specified directory - --no-self_in_block - Deactivates: checker to flag incorrect uses of when Objective-C - blocks capture self (Conversely: --self_in_block) + --no-self-in-block + Deactivates: checker self-in-block: An Objective-C-specific + analysis to detect when a block captures `self`. (Conversely: + --self-in-block) - --self_in_block-only - Activates: Enable --self_in_block and disable all other checkers - (Conversely: --no-self_in_block-only) + --self-in-block-only + Activates: Enable self-in-block and disable all other checkers + (Conversely: --no-self-in-block-only) --no-siof - Deactivates: the Static Initialization Order Fiasco analysis (C++ - only) (Conversely: --siof) + Deactivates: checker siof: Catches Static Initialization Order + Fiascos in C++, that can lead to subtle, + compiler-version-dependent errors. (Conversely: --siof) --siof-only - Activates: Enable --siof and disable all other checkers - (Conversely: --no-siof-only) + Activates: Enable siof and disable all other checkers (Conversely: + --no-siof-only) --sqlite-cache-size int SQLite cache size in pages (if positive) or kB (if negative), @@ -322,25 +336,29 @@ OPTIONS 65536. --no-starvation - Deactivates: starvation analysis (Conversely: --starvation) + Deactivates: checker starvation: Detect various kinds of + situations when no progress is being made because of concurrency + errors. (Conversely: --starvation) --starvation-only - Activates: Enable --starvation and disable all other checkers + Activates: Enable starvation and disable all other checkers (Conversely: --no-starvation-only) --topl - Activates: TOPL (Conversely: --no-topl) + Activates: checker topl: Detects errors based on user-provided + state machines describing multi-object monitors. (Conversely: + --no-topl) --topl-only - Activates: Enable --topl and disable all other checkers - (Conversely: --no-topl-only) + Activates: Enable topl and disable all other checkers (Conversely: + --no-topl-only) --no-uninit - Deactivates: checker for use of uninitialized values (Conversely: - --uninit) + Deactivates: checker uninit: Warns when values are used before + having been initialized. (Conversely: --uninit) --uninit-only - Activates: Enable --uninit and disable all other checkers + Activates: Enable uninit and disable all other checkers (Conversely: --no-uninit-only) BUCK OPTIONS --merge diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 950c5f15c..fdbceb1f9 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -57,11 +57,11 @@ OPTIONS options (see also --help-full for options reserved for internal use). --annotation-reachability - Activates: the annotation reachability checker. Given a pair of - source and sink annotation, e.g. @PerformanceCritical and - @Expensive, this checker will warn whenever some method annotated - with @PerformanceCritical calls, directly or indirectly, another - method annotated with @Expensive (Conversely: + Activates: checker annotation-reachability: Given a pair of source + and sink annotation, e.g. `@PerformanceCritical` and `@Expensive`, + this checker will warn whenever some method annotated with + `@PerformanceCritical` calls, directly or indirectly, another + method annotated with `@Expensive` (Conversely: --no-annotation-reachability) See also infer-analyze(1). --annotation-reachability-custom-pairs json @@ -103,7 +103,7 @@ OPTIONS given sources spec See also infer-analyze(1). --annotation-reachability-only - Activates: Enable --annotation-reachability and disable all other + Activates: Enable annotation-reachability and disable all other checkers (Conversely: --no-annotation-reachability-only) See also infer-analyze(1). @@ -112,12 +112,12 @@ OPTIONS --buck-compilation-database option. See also infer-capture(1). --no-biabduction - Deactivates: the separation logic based bi-abduction analysis - using the checkers framework (Conversely: --biabduction) - See also infer-analyze(1). + Deactivates: checker biabduction: This analysis deals with a range + of issues, many linked to memory safety. (Conversely: + --biabduction) See also infer-analyze(1). --biabduction-only - Activates: Enable --biabduction and disable all other checkers + Activates: Enable biabduction and disable all other checkers (Conversely: --no-biabduction-only) See also infer-analyze(1). --bo-debug int @@ -175,11 +175,12 @@ OPTIONS See also infer-capture(1) and infer-run(1). --bufferoverrun - Activates: the buffer overrun analysis (Conversely: - --no-bufferoverrun) See also infer-analyze(1). + Activates: checker bufferoverrun: InferBO is a detector for + out-of-bounds array accesses. (Conversely: --no-bufferoverrun) + See also infer-analyze(1). --bufferoverrun-only - Activates: Enable --bufferoverrun and disable all other checkers + Activates: Enable bufferoverrun and disable all other checkers (Conversely: --no-bufferoverrun-only) See also infer-analyze(1). --capture-blacklist regex @@ -228,11 +229,11 @@ OPTIONS function that each analysis has to model. See also infer-analyze(1) and infer-capture(1). --class-loads - Activates: Java class loading analysis (Conversely: - --no-class-loads) See also infer-analyze(1). + Activates: checker class-loads: Compute set of Java classes + loaded. (Conversely: --no-class-loads) See also infer-analyze(1). --class-loads-only - Activates: Enable --class-loads and disable all other checkers + Activates: Enable class-loads and disable all other checkers (Conversely: --no-class-loads-only) See also infer-analyze(1). --compilation-database +path @@ -263,16 +264,17 @@ OPTIONS See also infer-analyze(1). --cost - Activates: checker for performance cost analysis (Conversely: - --no-cost) See also infer-analyze(1). + Activates: checker cost: Computes the time complexity of functions + and methods. Can be used to detect changes in runtime complexity + with `infer reportdiff`. (Conversely: --no-cost) See also infer-analyze(1). --cost-issues-tests file Write a list of cost issues in a format suitable for cost tests to file See also infer-report(1). --cost-only - Activates: Enable --cost and disable all other checkers - (Conversely: --no-cost-only) See also infer-analyze(1). + Activates: Enable cost and disable all other checkers (Conversely: + --no-cost-only) See also infer-analyze(1). --costs-current path Costs report of the latest revision See also infer-reportdiff(1). @@ -332,7 +334,7 @@ OPTIONS --no-default-checkers Deactivates: Default checkers: --biabduction, --fragment-retains-view, --inefficient-keyset-iterator, --linters, - --liveness, --racerd, --siof, --self_in_block, --starvation, + --liveness, --racerd, --siof, --self-in-block, --starvation, --uninit (Conversely: --default-checkers) See also infer-analyze(1). --no-default-linters @@ -551,11 +553,11 @@ OPTIONS off. See also infer-report(1). --eradicate - Activates: the eradicate @Nullable checker for Java annotations - (Conversely: --no-eradicate) See also infer-analyze(1). + Activates: checker eradicate: The eradicate `@Nullable` checker + for Java annotations. (Conversely: --no-eradicate) See also infer-analyze(1). --eradicate-only - Activates: Enable --eradicate and disable all other checkers + Activates: Enable eradicate and disable all other checkers (Conversely: --no-eradicate-only) See also infer-analyze(1). --external-java-packages +prefix @@ -587,12 +589,12 @@ OPTIONS ndk-build, xcodebuild. See also infer-capture(1) and infer-run(1). --no-fragment-retains-view - Deactivates: detects when Android fragments are not explicitly - nullified before becoming unreabable (Conversely: - --fragment-retains-view) See also infer-analyze(1). + Deactivates: checker fragment-retains-view: Detects when Android + fragments are not explicitly nullified before becoming + unreachable. (Conversely: --fragment-retains-view) See also infer-analyze(1). --fragment-retains-view-only - Activates: Enable --fragment-retains-view and disable all other + Activates: Enable fragment-retains-view and disable all other checkers (Conversely: --no-fragment-retains-view-only) See also infer-analyze(1). @@ -654,30 +656,33 @@ OPTIONS See also infer-explore(1). --immutable-cast - Activates: the detection of object cast from immutable type to - mutable type. For instance, it will detect cast from ImmutableList - to List, ImmutableMap to Map, and ImmutableSet to Set. - (Conversely: --no-immutable-cast) See also infer-analyze(1). + Activates: checker immutable-cast: Detection of object cast from + immutable types to mutable types. For instance, it will detect + casts from `ImmutableList` to `List`, `ImmutableMap` to `Map`, and + `ImmutableSet` to `Set`. (Conversely: --no-immutable-cast) + See also infer-analyze(1). --immutable-cast-only - Activates: Enable --immutable-cast and disable all other checkers + Activates: Enable immutable-cast and disable all other checkers (Conversely: --no-immutable-cast-only) See also infer-analyze(1). --impurity - Activates: [EXPERIMENTAL] Impurity analysis (Conversely: - --no-impurity) See also infer-analyze(1). + Activates: checker impurity: Detects functions with potential + side-effects. Same as "purity", but implemented on top of Pulse. + (Conversely: --no-impurity) See also infer-analyze(1). --impurity-only - Activates: Enable --impurity and disable all other checkers + Activates: Enable impurity and disable all other checkers (Conversely: --no-impurity-only) See also infer-analyze(1). --no-inefficient-keyset-iterator - Deactivates: Check for inefficient uses of keySet iterator that - access both the key and the value. (Conversely: - --inefficient-keyset-iterator) See also infer-analyze(1). + Deactivates: checker inefficient-keyset-iterator: Check for + inefficient uses of iterators that iterate on keys then lookup + their values, instead of iterating on key-value pairs directly. + (Conversely: --inefficient-keyset-iterator) See also infer-analyze(1). --inefficient-keyset-iterator-only - Activates: Enable --inefficient-keyset-iterator and disable all + Activates: Enable inefficient-keyset-iterator and disable all other checkers (Conversely: --no-inefficient-keyset-iterator-only) See also infer-analyze(1). @@ -720,8 +725,8 @@ OPTIONS together with --linters-developer-mode) See also infer-capture(1). --no-linters - Deactivates: syntactic linters (Conversely: --linters) - See also infer-analyze(1). + Deactivates: checker linters: Declarative linting framework over + the Clang AST. (Conversely: --linters) See also infer-analyze(1). --linters-def-file +file Specify the file containing linters definition (e.g. 'linters.al') @@ -749,7 +754,7 @@ OPTIONS (Conversely: --no-linters-ignore-clang-failures) See also infer-capture(1). --linters-only - Activates: Enable --linters and disable all other checkers + Activates: Enable linters and disable all other checkers (Conversely: --no-linters-only) See also infer-analyze(1). --linters-validate-syntax-only @@ -766,17 +771,19 @@ OPTIONS report. (Conversely: --no-list-issue-types) See also infer-help(1). --litho-required-props - Activates: [EXPERIMENTAL] Required Prop check for Litho - (Conversely: --no-litho-required-props) See also infer-analyze(1). + Activates: checker litho-required-props: Checks that all + non-option `@Prop`s have been specified when constructing Litho + components. (Conversely: --no-litho-required-props) + See also infer-analyze(1). --litho-required-props-only - Activates: Enable --litho-required-props and disable all other + Activates: Enable litho-required-props and disable all other checkers (Conversely: --no-litho-required-props-only) See also infer-analyze(1). --no-liveness - Deactivates: the detection of dead stores and unused variables - (Conversely: --liveness) See also infer-analyze(1). + Deactivates: checker liveness: Detection of dead stores and unused + variables. (Conversely: --liveness) See also infer-analyze(1). --liveness-dangerous-classes json Specify classes where the destructor should be ignored when @@ -786,7 +793,7 @@ OPTIONS not read explicitly by the program. See also infer-analyze(1). --liveness-only - Activates: Enable --liveness and disable all other checkers + Activates: Enable liveness and disable all other checkers (Conversely: --no-liveness-only) See also infer-analyze(1). --load-average,-l float @@ -794,11 +801,12 @@ OPTIONS that specified (Buck and make only) See also infer-capture(1). --loop-hoisting - Activates: checker for loop-hoisting (Conversely: - --no-loop-hoisting) See also infer-analyze(1). + Activates: checker loop-hoisting: Detect opportunities to hoist + function calls that are invariant outside of loop bodies for + efficiency. (Conversely: --no-loop-hoisting) See also infer-analyze(1). --loop-hoisting-only - Activates: Enable --loop-hoisting and disable all other checkers + Activates: Enable loop-hoisting and disable all other checkers (Conversely: --no-loop-hoisting-only) See also infer-analyze(1). --max-nesting int @@ -831,13 +839,13 @@ OPTIONS infer-run(1). --printf-args - Activates: the detection of mismatch between the Java printf - format strings and the argument types For, example, this checker - will warn about the type error in `printf("Hello %d", "world")` - (Conversely: --no-printf-args) See also infer-analyze(1). + Activates: checker printf-args: Detect mismatches between the Java + `printf` format strings and the argument types For example, this + checker will warn about the type error in `printf("Hello %d", + "world")` (Conversely: --no-printf-args) See also infer-analyze(1). --printf-args-only - Activates: Enable --printf-args and disable all other checkers + Activates: Enable printf-args and disable all other checkers (Conversely: --no-printf-args-only) See also infer-analyze(1). --procedures @@ -890,7 +898,7 @@ OPTIONS infer-run(1). --pulse - Activates: [EXPERIMENTAL] memory and lifetime analysis + Activates: checker pulse: Memory and lifetime analysis. (Conversely: --no-pulse) See also infer-analyze(1). --pulse-cut-to-one-path-procedures-pattern string @@ -912,26 +920,30 @@ OPTIONS See also infer-analyze(1). --pulse-only - Activates: Enable --pulse and disable all other checkers + Activates: Enable pulse and disable all other checkers (Conversely: --no-pulse-only) See also infer-analyze(1). --purity - Activates: [EXPERIMENTAL] Purity analysis (Conversely: + Activates: checker purity: Detects pure (side-effect-free) + functions. A different implementation of "impurity". (Conversely: --no-purity) See also infer-analyze(1). --purity-only - Activates: Enable --purity and disable all other checkers + Activates: Enable purity and disable all other checkers (Conversely: --no-purity-only) See also infer-analyze(1). --quandary - Activates: the quandary taint analysis (Conversely: --no-quandary) - See also infer-analyze(1). + Activates: checker quandary: The Quandary taint analysis detects + flows of values between sources and sinks, except if the value + went through a "sanitizer". In addition to some defaults, users + can specify their own sources, sinks, and sanitizers functions. + (Conversely: --no-quandary) See also infer-analyze(1). --quandary-endpoints json Specify endpoint classes for Quandary See also infer-analyze(1). --quandary-only - Activates: Enable --quandary and disable all other checkers + Activates: Enable quandary and disable all other checkers (Conversely: --no-quandary-only) See also infer-analyze(1). --quandary-sanitizers json @@ -948,7 +960,7 @@ OPTIONS --no-quiet | -Q) See also infer-analyze(1) and infer-report(1). --no-racerd - Deactivates: the RacerD thread safety analysis (Conversely: + Deactivates: checker racerd: Thread safety analysis. (Conversely: --racerd) See also infer-analyze(1). --racerd-guardedby @@ -956,7 +968,7 @@ OPTIONS --no-racerd-guardedby) See also infer-analyze(1). --racerd-only - Activates: Enable --racerd and disable all other checkers + Activates: Enable racerd and disable all other checkers (Conversely: --no-racerd-only) See also infer-analyze(1). --no-racerd-unknown-returns-owned @@ -1015,17 +1027,20 @@ OPTIONS --select N Select bug number N. If omitted, prompt for input. See also infer-explore(1). - --no-self_in_block - Deactivates: checker to flag incorrect uses of when Objective-C - blocks capture self (Conversely: --self_in_block) See also infer-analyze(1). + --no-self-in-block + Deactivates: checker self-in-block: An Objective-C-specific + analysis to detect when a block captures `self`. (Conversely: + --self-in-block) See also infer-analyze(1). - --self_in_block-only - Activates: Enable --self_in_block and disable all other checkers - (Conversely: --no-self_in_block-only) See also infer-analyze(1). + --self-in-block-only + Activates: Enable self-in-block and disable all other checkers + (Conversely: --no-self-in-block-only) See also infer-analyze(1). --no-siof - Deactivates: the Static Initialization Order Fiasco analysis (C++ - only) (Conversely: --siof) See also infer-analyze(1). + Deactivates: checker siof: Catches Static Initialization Order + Fiascos in C++, that can lead to subtle, + compiler-version-dependent errors. (Conversely: --siof) + See also infer-analyze(1). --siof-check-iostreams Activates: Do not assume that iostreams (cout, cerr, ...) are @@ -1035,8 +1050,8 @@ OPTIONS option on. (Conversely: --no-siof-check-iostreams) See also infer-analyze(1). --siof-only - Activates: Enable --siof and disable all other checkers - (Conversely: --no-siof-only) See also infer-analyze(1). + Activates: Enable siof and disable all other checkers (Conversely: + --no-siof-only) See also infer-analyze(1). --siof-safe-methods +string Methods that are SIOF-safe; "foo::bar" will match "foo::bar()", @@ -1107,11 +1122,12 @@ OPTIONS 65536. See also infer-analyze(1), infer-capture(1), and infer-run(1). --no-starvation - Deactivates: starvation analysis (Conversely: --starvation) - See also infer-analyze(1). + Deactivates: checker starvation: Detect various kinds of + situations when no progress is being made because of concurrency + errors. (Conversely: --starvation) See also infer-analyze(1). --starvation-only - Activates: Enable --starvation and disable all other checkers + Activates: Enable starvation and disable all other checkers (Conversely: --no-starvation-only) See also infer-analyze(1). --threadsafe-aliases json @@ -1119,18 +1135,20 @@ OPTIONS @ThreadSafe See also infer-analyze(1). --topl - Activates: TOPL (Conversely: --no-topl) See also infer-analyze(1). + Activates: checker topl: Detects errors based on user-provided + state machines describing multi-object monitors. (Conversely: + --no-topl) See also infer-analyze(1). --topl-only - Activates: Enable --topl and disable all other checkers - (Conversely: --no-topl-only) See also infer-analyze(1). + Activates: Enable topl and disable all other checkers (Conversely: + --no-topl-only) See also infer-analyze(1). --no-uninit - Deactivates: checker for use of uninitialized values (Conversely: - --uninit) See also infer-analyze(1). + Deactivates: checker uninit: Warns when values are used before + having been initialized. (Conversely: --uninit) See also infer-analyze(1). --uninit-only - Activates: Enable --uninit and disable all other checkers + Activates: Enable uninit and disable all other checkers (Conversely: --no-uninit-only) See also infer-analyze(1). --unsafe-malloc @@ -1570,8 +1588,9 @@ INTERNAL OPTIONS Cancel the effect of --nullable-annotation-name. --nullsafe - Activates: [RESERVED] Reserved for nullsafe typechecker, use - --eradicate for now (Conversely: --no-nullsafe) + Activates: checker nullsafe: [RESERVED] Reserved for nullsafe + typechecker, use `--eradicate` for now. (Conversely: + --no-nullsafe) --nullsafe-disable-field-not-initialized-in-nonstrict-classes Activates: Nullsafe: In this mode field not initialized issues @@ -1734,6 +1753,10 @@ INTERNAL OPTIONS Reset the list of folders containing linters definitions to be empty (see linters-def-folder). + --resource-leak-lab + Activates: checker resource-leak-lab: (Conversely: + --no-resource-leak-lab) + --scheduler { file | restart | callgraph } Specify the scheduler used for the analysis phase diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 508acbf1d..0130eee37 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -57,11 +57,11 @@ OPTIONS options (see also --help-full for options reserved for internal use). --annotation-reachability - Activates: the annotation reachability checker. Given a pair of - source and sink annotation, e.g. @PerformanceCritical and - @Expensive, this checker will warn whenever some method annotated - with @PerformanceCritical calls, directly or indirectly, another - method annotated with @Expensive (Conversely: + Activates: checker annotation-reachability: Given a pair of source + and sink annotation, e.g. `@PerformanceCritical` and `@Expensive`, + this checker will warn whenever some method annotated with + `@PerformanceCritical` calls, directly or indirectly, another + method annotated with `@Expensive` (Conversely: --no-annotation-reachability) See also infer-analyze(1). --annotation-reachability-custom-pairs json @@ -103,7 +103,7 @@ OPTIONS given sources spec See also infer-analyze(1). --annotation-reachability-only - Activates: Enable --annotation-reachability and disable all other + Activates: Enable annotation-reachability and disable all other checkers (Conversely: --no-annotation-reachability-only) See also infer-analyze(1). @@ -112,12 +112,12 @@ OPTIONS --buck-compilation-database option. See also infer-capture(1). --no-biabduction - Deactivates: the separation logic based bi-abduction analysis - using the checkers framework (Conversely: --biabduction) - See also infer-analyze(1). + Deactivates: checker biabduction: This analysis deals with a range + of issues, many linked to memory safety. (Conversely: + --biabduction) See also infer-analyze(1). --biabduction-only - Activates: Enable --biabduction and disable all other checkers + Activates: Enable biabduction and disable all other checkers (Conversely: --no-biabduction-only) See also infer-analyze(1). --bo-debug int @@ -175,11 +175,12 @@ OPTIONS See also infer-capture(1) and infer-run(1). --bufferoverrun - Activates: the buffer overrun analysis (Conversely: - --no-bufferoverrun) See also infer-analyze(1). + Activates: checker bufferoverrun: InferBO is a detector for + out-of-bounds array accesses. (Conversely: --no-bufferoverrun) + See also infer-analyze(1). --bufferoverrun-only - Activates: Enable --bufferoverrun and disable all other checkers + Activates: Enable bufferoverrun and disable all other checkers (Conversely: --no-bufferoverrun-only) See also infer-analyze(1). --capture-blacklist regex @@ -228,11 +229,11 @@ OPTIONS function that each analysis has to model. See also infer-analyze(1) and infer-capture(1). --class-loads - Activates: Java class loading analysis (Conversely: - --no-class-loads) See also infer-analyze(1). + Activates: checker class-loads: Compute set of Java classes + loaded. (Conversely: --no-class-loads) See also infer-analyze(1). --class-loads-only - Activates: Enable --class-loads and disable all other checkers + Activates: Enable class-loads and disable all other checkers (Conversely: --no-class-loads-only) See also infer-analyze(1). --compilation-database +path @@ -263,16 +264,17 @@ OPTIONS See also infer-analyze(1). --cost - Activates: checker for performance cost analysis (Conversely: - --no-cost) See also infer-analyze(1). + Activates: checker cost: Computes the time complexity of functions + and methods. Can be used to detect changes in runtime complexity + with `infer reportdiff`. (Conversely: --no-cost) See also infer-analyze(1). --cost-issues-tests file Write a list of cost issues in a format suitable for cost tests to file See also infer-report(1). --cost-only - Activates: Enable --cost and disable all other checkers - (Conversely: --no-cost-only) See also infer-analyze(1). + Activates: Enable cost and disable all other checkers (Conversely: + --no-cost-only) See also infer-analyze(1). --costs-current path Costs report of the latest revision See also infer-reportdiff(1). @@ -332,7 +334,7 @@ OPTIONS --no-default-checkers Deactivates: Default checkers: --biabduction, --fragment-retains-view, --inefficient-keyset-iterator, --linters, - --liveness, --racerd, --siof, --self_in_block, --starvation, + --liveness, --racerd, --siof, --self-in-block, --starvation, --uninit (Conversely: --default-checkers) See also infer-analyze(1). --no-default-linters @@ -551,11 +553,11 @@ OPTIONS off. See also infer-report(1). --eradicate - Activates: the eradicate @Nullable checker for Java annotations - (Conversely: --no-eradicate) See also infer-analyze(1). + Activates: checker eradicate: The eradicate `@Nullable` checker + for Java annotations. (Conversely: --no-eradicate) See also infer-analyze(1). --eradicate-only - Activates: Enable --eradicate and disable all other checkers + Activates: Enable eradicate and disable all other checkers (Conversely: --no-eradicate-only) See also infer-analyze(1). --external-java-packages +prefix @@ -587,12 +589,12 @@ OPTIONS ndk-build, xcodebuild. See also infer-capture(1) and infer-run(1). --no-fragment-retains-view - Deactivates: detects when Android fragments are not explicitly - nullified before becoming unreabable (Conversely: - --fragment-retains-view) See also infer-analyze(1). + Deactivates: checker fragment-retains-view: Detects when Android + fragments are not explicitly nullified before becoming + unreachable. (Conversely: --fragment-retains-view) See also infer-analyze(1). --fragment-retains-view-only - Activates: Enable --fragment-retains-view and disable all other + Activates: Enable fragment-retains-view and disable all other checkers (Conversely: --no-fragment-retains-view-only) See also infer-analyze(1). @@ -654,30 +656,33 @@ OPTIONS See also infer-explore(1). --immutable-cast - Activates: the detection of object cast from immutable type to - mutable type. For instance, it will detect cast from ImmutableList - to List, ImmutableMap to Map, and ImmutableSet to Set. - (Conversely: --no-immutable-cast) See also infer-analyze(1). + Activates: checker immutable-cast: Detection of object cast from + immutable types to mutable types. For instance, it will detect + casts from `ImmutableList` to `List`, `ImmutableMap` to `Map`, and + `ImmutableSet` to `Set`. (Conversely: --no-immutable-cast) + See also infer-analyze(1). --immutable-cast-only - Activates: Enable --immutable-cast and disable all other checkers + Activates: Enable immutable-cast and disable all other checkers (Conversely: --no-immutable-cast-only) See also infer-analyze(1). --impurity - Activates: [EXPERIMENTAL] Impurity analysis (Conversely: - --no-impurity) See also infer-analyze(1). + Activates: checker impurity: Detects functions with potential + side-effects. Same as "purity", but implemented on top of Pulse. + (Conversely: --no-impurity) See also infer-analyze(1). --impurity-only - Activates: Enable --impurity and disable all other checkers + Activates: Enable impurity and disable all other checkers (Conversely: --no-impurity-only) See also infer-analyze(1). --no-inefficient-keyset-iterator - Deactivates: Check for inefficient uses of keySet iterator that - access both the key and the value. (Conversely: - --inefficient-keyset-iterator) See also infer-analyze(1). + Deactivates: checker inefficient-keyset-iterator: Check for + inefficient uses of iterators that iterate on keys then lookup + their values, instead of iterating on key-value pairs directly. + (Conversely: --inefficient-keyset-iterator) See also infer-analyze(1). --inefficient-keyset-iterator-only - Activates: Enable --inefficient-keyset-iterator and disable all + Activates: Enable inefficient-keyset-iterator and disable all other checkers (Conversely: --no-inefficient-keyset-iterator-only) See also infer-analyze(1). @@ -720,8 +725,8 @@ OPTIONS together with --linters-developer-mode) See also infer-capture(1). --no-linters - Deactivates: syntactic linters (Conversely: --linters) - See also infer-analyze(1). + Deactivates: checker linters: Declarative linting framework over + the Clang AST. (Conversely: --linters) See also infer-analyze(1). --linters-def-file +file Specify the file containing linters definition (e.g. 'linters.al') @@ -749,7 +754,7 @@ OPTIONS (Conversely: --no-linters-ignore-clang-failures) See also infer-capture(1). --linters-only - Activates: Enable --linters and disable all other checkers + Activates: Enable linters and disable all other checkers (Conversely: --no-linters-only) See also infer-analyze(1). --linters-validate-syntax-only @@ -766,17 +771,19 @@ OPTIONS report. (Conversely: --no-list-issue-types) See also infer-help(1). --litho-required-props - Activates: [EXPERIMENTAL] Required Prop check for Litho - (Conversely: --no-litho-required-props) See also infer-analyze(1). + Activates: checker litho-required-props: Checks that all + non-option `@Prop`s have been specified when constructing Litho + components. (Conversely: --no-litho-required-props) + See also infer-analyze(1). --litho-required-props-only - Activates: Enable --litho-required-props and disable all other + Activates: Enable litho-required-props and disable all other checkers (Conversely: --no-litho-required-props-only) See also infer-analyze(1). --no-liveness - Deactivates: the detection of dead stores and unused variables - (Conversely: --liveness) See also infer-analyze(1). + Deactivates: checker liveness: Detection of dead stores and unused + variables. (Conversely: --liveness) See also infer-analyze(1). --liveness-dangerous-classes json Specify classes where the destructor should be ignored when @@ -786,7 +793,7 @@ OPTIONS not read explicitly by the program. See also infer-analyze(1). --liveness-only - Activates: Enable --liveness and disable all other checkers + Activates: Enable liveness and disable all other checkers (Conversely: --no-liveness-only) See also infer-analyze(1). --load-average,-l float @@ -794,11 +801,12 @@ OPTIONS that specified (Buck and make only) See also infer-capture(1). --loop-hoisting - Activates: checker for loop-hoisting (Conversely: - --no-loop-hoisting) See also infer-analyze(1). + Activates: checker loop-hoisting: Detect opportunities to hoist + function calls that are invariant outside of loop bodies for + efficiency. (Conversely: --no-loop-hoisting) See also infer-analyze(1). --loop-hoisting-only - Activates: Enable --loop-hoisting and disable all other checkers + Activates: Enable loop-hoisting and disable all other checkers (Conversely: --no-loop-hoisting-only) See also infer-analyze(1). --max-nesting int @@ -831,13 +839,13 @@ OPTIONS infer-run(1). --printf-args - Activates: the detection of mismatch between the Java printf - format strings and the argument types For, example, this checker - will warn about the type error in `printf("Hello %d", "world")` - (Conversely: --no-printf-args) See also infer-analyze(1). + Activates: checker printf-args: Detect mismatches between the Java + `printf` format strings and the argument types For example, this + checker will warn about the type error in `printf("Hello %d", + "world")` (Conversely: --no-printf-args) See also infer-analyze(1). --printf-args-only - Activates: Enable --printf-args and disable all other checkers + Activates: Enable printf-args and disable all other checkers (Conversely: --no-printf-args-only) See also infer-analyze(1). --procedures @@ -890,7 +898,7 @@ OPTIONS infer-run(1). --pulse - Activates: [EXPERIMENTAL] memory and lifetime analysis + Activates: checker pulse: Memory and lifetime analysis. (Conversely: --no-pulse) See also infer-analyze(1). --pulse-cut-to-one-path-procedures-pattern string @@ -912,26 +920,30 @@ OPTIONS See also infer-analyze(1). --pulse-only - Activates: Enable --pulse and disable all other checkers + Activates: Enable pulse and disable all other checkers (Conversely: --no-pulse-only) See also infer-analyze(1). --purity - Activates: [EXPERIMENTAL] Purity analysis (Conversely: + Activates: checker purity: Detects pure (side-effect-free) + functions. A different implementation of "impurity". (Conversely: --no-purity) See also infer-analyze(1). --purity-only - Activates: Enable --purity and disable all other checkers + Activates: Enable purity and disable all other checkers (Conversely: --no-purity-only) See also infer-analyze(1). --quandary - Activates: the quandary taint analysis (Conversely: --no-quandary) - See also infer-analyze(1). + Activates: checker quandary: The Quandary taint analysis detects + flows of values between sources and sinks, except if the value + went through a "sanitizer". In addition to some defaults, users + can specify their own sources, sinks, and sanitizers functions. + (Conversely: --no-quandary) See also infer-analyze(1). --quandary-endpoints json Specify endpoint classes for Quandary See also infer-analyze(1). --quandary-only - Activates: Enable --quandary and disable all other checkers + Activates: Enable quandary and disable all other checkers (Conversely: --no-quandary-only) See also infer-analyze(1). --quandary-sanitizers json @@ -948,7 +960,7 @@ OPTIONS --no-quiet | -Q) See also infer-analyze(1) and infer-report(1). --no-racerd - Deactivates: the RacerD thread safety analysis (Conversely: + Deactivates: checker racerd: Thread safety analysis. (Conversely: --racerd) See also infer-analyze(1). --racerd-guardedby @@ -956,7 +968,7 @@ OPTIONS --no-racerd-guardedby) See also infer-analyze(1). --racerd-only - Activates: Enable --racerd and disable all other checkers + Activates: Enable racerd and disable all other checkers (Conversely: --no-racerd-only) See also infer-analyze(1). --no-racerd-unknown-returns-owned @@ -1015,17 +1027,20 @@ OPTIONS --select N Select bug number N. If omitted, prompt for input. See also infer-explore(1). - --no-self_in_block - Deactivates: checker to flag incorrect uses of when Objective-C - blocks capture self (Conversely: --self_in_block) See also infer-analyze(1). + --no-self-in-block + Deactivates: checker self-in-block: An Objective-C-specific + analysis to detect when a block captures `self`. (Conversely: + --self-in-block) See also infer-analyze(1). - --self_in_block-only - Activates: Enable --self_in_block and disable all other checkers - (Conversely: --no-self_in_block-only) See also infer-analyze(1). + --self-in-block-only + Activates: Enable self-in-block and disable all other checkers + (Conversely: --no-self-in-block-only) See also infer-analyze(1). --no-siof - Deactivates: the Static Initialization Order Fiasco analysis (C++ - only) (Conversely: --siof) See also infer-analyze(1). + Deactivates: checker siof: Catches Static Initialization Order + Fiascos in C++, that can lead to subtle, + compiler-version-dependent errors. (Conversely: --siof) + See also infer-analyze(1). --siof-check-iostreams Activates: Do not assume that iostreams (cout, cerr, ...) are @@ -1035,8 +1050,8 @@ OPTIONS option on. (Conversely: --no-siof-check-iostreams) See also infer-analyze(1). --siof-only - Activates: Enable --siof and disable all other checkers - (Conversely: --no-siof-only) See also infer-analyze(1). + Activates: Enable siof and disable all other checkers (Conversely: + --no-siof-only) See also infer-analyze(1). --siof-safe-methods +string Methods that are SIOF-safe; "foo::bar" will match "foo::bar()", @@ -1107,11 +1122,12 @@ OPTIONS 65536. See also infer-analyze(1), infer-capture(1), and infer-run(1). --no-starvation - Deactivates: starvation analysis (Conversely: --starvation) - See also infer-analyze(1). + Deactivates: checker starvation: Detect various kinds of + situations when no progress is being made because of concurrency + errors. (Conversely: --starvation) See also infer-analyze(1). --starvation-only - Activates: Enable --starvation and disable all other checkers + Activates: Enable starvation and disable all other checkers (Conversely: --no-starvation-only) See also infer-analyze(1). --threadsafe-aliases json @@ -1119,18 +1135,20 @@ OPTIONS @ThreadSafe See also infer-analyze(1). --topl - Activates: TOPL (Conversely: --no-topl) See also infer-analyze(1). + Activates: checker topl: Detects errors based on user-provided + state machines describing multi-object monitors. (Conversely: + --no-topl) See also infer-analyze(1). --topl-only - Activates: Enable --topl and disable all other checkers - (Conversely: --no-topl-only) See also infer-analyze(1). + Activates: Enable topl and disable all other checkers (Conversely: + --no-topl-only) See also infer-analyze(1). --no-uninit - Deactivates: checker for use of uninitialized values (Conversely: - --uninit) See also infer-analyze(1). + Deactivates: checker uninit: Warns when values are used before + having been initialized. (Conversely: --uninit) See also infer-analyze(1). --uninit-only - Activates: Enable --uninit and disable all other checkers + Activates: Enable uninit and disable all other checkers (Conversely: --no-uninit-only) See also infer-analyze(1). --unsafe-malloc diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index 9d55e1670..c4f5a93fa 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -38,12 +38,20 @@ type t = | Uninit [@@deriving equal, enumerate] -type support = NoSupport | Support | ExperimentalSupport | ToySupport +type support = NoSupport | ExperimentalSupport | Support -type cli_flags = {long: string; deprecated: string list; show_in_help: bool} +(** see .mli for how to fill these *) +type kind = + | UserFacing of {title: string; markdown_body: string} + | UserFacingDeprecated of {title: string; markdown_body: string; deprecation_message: string} + | Internal + | Exercise + +type cli_flags = {deprecated: string list; show_in_help: bool} type config = { id: string + ; kind: kind ; support: Language.t -> support ; short_documentation: string ; cli_flags: cli_flags option @@ -62,223 +70,304 @@ let config_unsafe checker = let supports_java (language : Language.t) = match language with Clang -> NoSupport | Java -> Support in - let supports_java_experimental (language : Language.t) = - match language with Clang -> NoSupport | Java -> ExperimentalSupport - in match checker with | AnnotationReachability -> { id= "annotation-reachability" + ; kind= UserFacing {title= "Annotation Reachability"; markdown_body= ""} ; support= supports_clang_and_java ; short_documentation= - "the annotation reachability checker. Given a pair of source and sink annotation, e.g. \ - @PerformanceCritical and @Expensive, this checker will warn whenever some method \ - annotated with @PerformanceCritical calls, directly or indirectly, another method \ - annotated with @Expensive" - ; cli_flags= Some {long= "annotation-reachability"; deprecated= []; show_in_help= true} + "Given a pair of source and sink annotation, e.g. `@PerformanceCritical` and \ + `@Expensive`, this checker will warn whenever some method annotated with \ + `@PerformanceCritical` calls, directly or indirectly, another method annotated with \ + `@Expensive`" + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | Biabduction -> { id= "biabduction" + ; kind= + UserFacing + { title= "Biabduction" + ; markdown_body= + "Read more about its foundations in the [Separation Logic and Biabduction \ + page](separation-logic-and-bi-abduction)." } ; support= supports_clang_and_java ; short_documentation= - "the separation logic based bi-abduction analysis using the checkers framework" - ; cli_flags= Some {long= "biabduction"; deprecated= []; show_in_help= true} + "This analysis deals with a range of issues, many linked to memory safety." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | BufferOverrunAnalysis -> - { id= "buffer-overrun-analysis" + { id= "bufferoverrun-analysis" + ; kind= Internal ; support= supports_clang_and_java ; short_documentation= - "internal part of the buffer overrun analysis that computes values at each program \ - point, automatically triggered when analyses that depend on these are run" + "Internal part of the buffer overrun analysis that computes values at each program \ + point, automatically triggered when analyses that depend on these are run." ; cli_flags= None ; enabled_by_default= false ; activates= [] } | BufferOverrunChecker -> - { id= "buffer-overrun-checker" + { id= "bufferoverrun" + ; kind= + UserFacing + { title= "Buffer Overrun Analysis (InferBO)" + ; markdown_body= + "You can read about its origins in this [blog \ + post](https://research.fb.com/inferbo-infer-based-buffer-overrun-analyzer/)." } ; support= supports_clang_and_java - ; short_documentation= "the buffer overrun analysis" - ; cli_flags= Some {long= "bufferoverrun"; deprecated= []; show_in_help= true} + ; short_documentation= "InferBO is a detector for out-of-bounds array accesses." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [BufferOverrunAnalysis] } | ClassLoads -> - { id= "class-loading-analysis" + { id= "class-loads" + ; kind= + UserFacingDeprecated + { title= "Class loading analysis" + ; markdown_body= "" + ; deprecation_message= "Unmaintained prototype." } ; support= supports_java - ; short_documentation= "Java class loading analysis" - ; cli_flags= Some {long= "class-loads"; deprecated= []; show_in_help= true} + ; short_documentation= "Compute set of Java classes loaded." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | Cost -> - { id= "cost-analysis" + { id= "cost" + ; kind= UserFacing {title= "Cost: Runtime Complexity Analysis"; markdown_body= ""} ; support= supports_clang_and_java - ; short_documentation= "checker for performance cost analysis" - ; cli_flags= Some {long= "cost"; deprecated= []; show_in_help= true} + ; short_documentation= + "Computes the time complexity of functions and methods. Can be used to detect changes in \ + runtime complexity with `infer reportdiff`." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [BufferOverrunAnalysis] } | Eradicate -> { id= "eradicate" + ; kind= + UserFacing + {title= "Eradicate"; markdown_body= [%blob "../../documentation/checkers/Eradicate.md"]} ; support= supports_java - ; short_documentation= "the eradicate @Nullable checker for Java annotations" - ; cli_flags= Some {long= "eradicate"; deprecated= []; show_in_help= true} + ; short_documentation= "The eradicate `@Nullable` checker for Java annotations." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | FragmentRetainsView -> { id= "fragment-retains-view" + ; kind= + UserFacingDeprecated + { title= "Fragment Retains View" + ; markdown_body= "" + ; deprecation_message= "Unmaintained due to poor precision." } ; support= supports_java ; short_documentation= - "detects when Android fragments are not explicitly nullified before becoming unreabable" - ; cli_flags= Some {long= "fragment-retains-view"; deprecated= []; show_in_help= true} + "Detects when Android fragments are not explicitly nullified before becoming unreachable." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | ImmutableCast -> { id= "immutable-cast" + ; kind= + UserFacingDeprecated + { title= "Immutable Cast" + ; markdown_body= + "Casts flagged by this checker are unsafe because calling mutation operations on \ + the cast objects will fail at runtime." + ; deprecation_message= "Unmaintained due to poor actionability of the reports." } ; support= supports_java ; short_documentation= - "the detection of object cast from immutable type to mutable type. For instance, it will \ - detect cast from ImmutableList to List, ImmutableMap to Map, and ImmutableSet to Set." - ; cli_flags= Some {long= "immutable-cast"; deprecated= []; show_in_help= true} + "Detection of object cast from immutable types to mutable types. For instance, it will \ + detect casts from `ImmutableList` to `List`, `ImmutableMap` to `Map`, and \ + `ImmutableSet` to `Set`." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | Impurity -> { id= "impurity" + ; kind= Internal ; support= supports_clang_and_java_experimental - ; short_documentation= "[EXPERIMENTAL] Impurity analysis" - ; cli_flags= Some {long= "impurity"; deprecated= []; show_in_help= true} + ; short_documentation= + "Detects functions with potential side-effects. Same as \"purity\", but implemented on \ + top of Pulse." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [Pulse] } | InefficientKeysetIterator -> { id= "inefficient-keyset-iterator" + ; kind= UserFacing {title= "Inefficient keySet Iterator"; markdown_body= ""} ; support= supports_java ; short_documentation= - "Check for inefficient uses of keySet iterator that access both the key and the value." - ; cli_flags= Some {long= "inefficient-keyset-iterator"; deprecated= []; show_in_help= true} + "Check for inefficient uses of iterators that iterate on keys then lookup their values, \ + instead of iterating on key-value pairs directly." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | Linters -> - { id= "al-linters" + { id= "linters" + ; kind= + UserFacingDeprecated + { title= "AST Language (AL)" + ; markdown_body= [%blob "../../documentation/checkers/ASTLanguage.md"] + ; deprecation_message= "On end-of-life support, may be removed in the future." } ; support= supports_clang - ; short_documentation= "syntactic linters" - ; cli_flags= Some {long= "linters"; deprecated= []; show_in_help= true} + ; short_documentation= "Declarative linting framework over the Clang AST." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | LithoRequiredProps -> { id= "litho-required-props" - ; support= supports_java_experimental - ; short_documentation= "[EXPERIMENTAL] Required Prop check for Litho" - ; cli_flags= Some {long= "litho-required-props"; deprecated= []; show_in_help= true} + ; kind= UserFacing {title= "Litho \"Required Props\""; markdown_body= ""} + ; support= supports_java + ; short_documentation= + "Checks that all non-option `@Prop`s have been specified when constructing Litho \ + components." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | Liveness -> { id= "liveness" + ; kind= UserFacing {title= "Liveness"; markdown_body= ""} ; support= supports_clang - ; short_documentation= "the detection of dead stores and unused variables" - ; cli_flags= Some {long= "liveness"; deprecated= []; show_in_help= true} + ; short_documentation= "Detection of dead stores and unused variables." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | LoopHoisting -> { id= "loop-hoisting" + ; kind= UserFacing {title= "Loop Hoisting"; markdown_body= ""} ; support= supports_clang_and_java - ; short_documentation= "checker for loop-hoisting" - ; cli_flags= Some {long= "loop-hoisting"; deprecated= []; show_in_help= true} + ; short_documentation= + "Detect opportunities to hoist function calls that are invariant outside of loop bodies \ + for efficiency." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [BufferOverrunAnalysis; Purity] } | NullsafeDeprecated -> { id= "nullsafe" + ; kind= Internal ; support= (fun _ -> NoSupport) - ; short_documentation= "[RESERVED] Reserved for nullsafe typechecker, use --eradicate for now" - ; cli_flags= - Some - { long= "nullsafe" - ; deprecated= ["-check-nullable"; "-suggest-nullable"] - ; show_in_help= false } + ; short_documentation= + "[RESERVED] Reserved for nullsafe typechecker, use `--eradicate` for now." + ; cli_flags= Some {deprecated= ["-check-nullable"; "-suggest-nullable"]; show_in_help= false} ; enabled_by_default= false ; activates= [] } | PrintfArgs -> { id= "printf-args" + ; kind= + UserFacingDeprecated + { title= "`printf()` Argument Types" + ; markdown_body= "" + ; deprecation_message= "Unmaintained." } ; support= supports_java ; short_documentation= - "the detection of mismatch between the Java printf format strings and the argument types \ - For, example, this checker will warn about the type error in `printf(\"Hello %d\", \ + "Detect mismatches between the Java `printf` format strings and the argument types For \ + example, this checker will warn about the type error in `printf(\"Hello %d\", \ \"world\")`" - ; cli_flags= Some {long= "printf-args"; deprecated= []; show_in_help= true} + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | Pulse -> { id= "pulse" + ; kind= UserFacing {title= "Pulse"; markdown_body= ""} ; support= supports_clang_and_java_experimental - ; short_documentation= "[EXPERIMENTAL] memory and lifetime analysis" - ; cli_flags= Some {long= "pulse"; deprecated= ["-ownership"]; show_in_help= true} + ; short_documentation= "Memory and lifetime analysis." + ; cli_flags= Some {deprecated= ["-ownership"]; show_in_help= true} ; enabled_by_default= false ; activates= [] } | Purity -> { id= "purity" + ; kind= Internal ; support= supports_clang_and_java_experimental - ; short_documentation= "[EXPERIMENTAL] Purity analysis" - ; cli_flags= Some {long= "purity"; deprecated= []; show_in_help= true} + ; short_documentation= + "Detects pure (side-effect-free) functions. A different implementation of \"impurity\"." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [BufferOverrunAnalysis] } | Quandary -> { id= "quandary" + ; kind= + UserFacing + {title= "Quandary"; markdown_body= [%blob "../../documentation/checkers/Quandary.md"]} ; support= supports_clang_and_java - ; short_documentation= "the quandary taint analysis" - ; cli_flags= Some {long= "quandary"; deprecated= []; show_in_help= true} + ; short_documentation= + "The Quandary taint analysis detects flows of values between sources and sinks, except \ + if the value went through a \"sanitizer\". In addition to some defaults, users can \ + specify their own sources, sinks, and sanitizers functions." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [] } | RacerD -> - { id= "RacerD" + { id= "racerd" + ; kind= + UserFacing + {title= "RacerD"; markdown_body= [%blob "../../documentation/checkers/RacerD.md"]} ; support= supports_clang_and_java - ; short_documentation= "the RacerD thread safety analysis" - ; cli_flags= Some {long= "racerd"; deprecated= ["-threadsafety"]; show_in_help= true} + ; short_documentation= "Thread safety analysis." + ; cli_flags= Some {deprecated= ["-threadsafety"]; show_in_help= true} ; enabled_by_default= true ; activates= [] } | ResourceLeakLabExercise -> { id= "resource-leak-lab" - ; support= (fun _ -> ToySupport) + ; kind= Exercise + ; support= (fun _ -> Support) ; short_documentation= "" - ; cli_flags= Some {long= "resource-leak"; deprecated= []; show_in_help= false} + ; cli_flags= Some {deprecated= []; show_in_help= false} ; enabled_by_default= false ; activates= [] } | SIOF -> - { id= "SIOF" + { id= "siof" + ; kind= UserFacing {title= "Static Initialization Order Fiasco"; markdown_body= ""} ; support= supports_clang - ; short_documentation= "the Static Initialization Order Fiasco analysis (C++ only)" - ; cli_flags= Some {long= "siof"; deprecated= []; show_in_help= true} + ; short_documentation= + "Catches Static Initialization Order Fiascos in C++, that can lead to subtle, \ + compiler-version-dependent errors." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | SelfInBlock -> { id= "self-in-block" + ; kind= UserFacing {title= "Self in Block"; markdown_body= ""} ; support= supports_clang ; short_documentation= - "checker to flag incorrect uses of when Objective-C blocks capture self" - ; cli_flags= Some {long= "self_in_block"; deprecated= []; show_in_help= true} + "An Objective-C-specific analysis to detect when a block captures `self`." + ; cli_flags= Some {deprecated= ["-self_in_block"]; show_in_help= true} ; enabled_by_default= true ; activates= [] } | Starvation -> { id= "starvation" + ; kind= + UserFacing + { title= "Starvation" + ; markdown_body= [%blob "../../documentation/checkers/Starvation.md"] } ; support= supports_clang_and_java - ; short_documentation= "starvation analysis" - ; cli_flags= Some {long= "starvation"; deprecated= []; show_in_help= true} + ; short_documentation= + "Detect various kinds of situations when no progress is being made because of \ + concurrency errors." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } | TOPL -> - { id= "TOPL" + { id= "topl" + ; kind= UserFacing {title= "TOPL"; markdown_body= ""} ; support= supports_clang_and_java_experimental - ; short_documentation= "TOPL" - ; cli_flags= Some {long= "topl"; deprecated= []; show_in_help= true} + ; short_documentation= + "Detects errors based on user-provided state machines describing multi-object monitors." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [Biabduction] } | Uninit -> { id= "uninit" + ; kind= UserFacing {title= "Uninitialized Variable"; markdown_body= ""} ; support= supports_clang - ; short_documentation= "checker for use of uninitialized values" - ; cli_flags= Some {long= "uninit"; deprecated= []; show_in_help= true} + ; short_documentation= "Warns when values are used before having been initialized." + ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } let config c = let config = config_unsafe c in - let is_illegal_id_char c = match c with 'a' .. 'z' | 'A' .. 'Z' | '-' -> false | _ -> true in + let is_illegal_id_char c = match c with 'a' .. 'z' | '-' -> false | _ -> true in String.find config.id ~f:is_illegal_id_char |> Option.iter ~f:(fun c -> L.die InternalError diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli index ec1e26d70..f2b9f3791 100644 --- a/infer/src/base/Checker.mli +++ b/infer/src/base/Checker.mli @@ -40,24 +40,36 @@ type t = (** per-language support for each checker *) type support = | NoSupport (** checker does not run at all for this language *) - | Support (** checker is expected to give reasonable results *) | ExperimentalSupport (** checker runs but is not expected to give reasonable results *) - | ToySupport - (** the checker is for teaching purposes only (like experimental but with no plans to improve - it) *) + | Support (** checker is expected to give reasonable results *) type cli_flags = - { long: string - (** The flag to enable this option on the command line, without the leading "--" (like the - [~long] argument of {!CommandLineOption} functions). *) - ; deprecated: string list + { deprecated: string list (** More command-line flags, similar to [~deprecated] arguments in {!CommandLineOption}. *) ; show_in_help: bool } +type kind = + | UserFacing of + { title: string (** the title of the documentation web page *) + ; markdown_body: string (** main text of the documentation *) } + (** can report issues to users *) + | UserFacingDeprecated of + { title: string (** the title of the documentation web page *) + ; markdown_body: string (** main text of the documentation *) + ; deprecation_message: string } + (** can report issues to users but should probably be deleted from infer *) + | Internal + (** Analysis that only serves other analyses. Do not use to mean experimental! Please still + document experimental checkers as they will become non-experimental. *) + | Exercise (** reserved for the "resource leak" lab exercise *) + type config = { id: string + (** Unique identifier. Used to generate web URLs for the documentation as well as the flag + to enable this option on the command line. *) + ; kind: kind ; support: Language.t -> support - ; short_documentation: string + ; short_documentation: string (** used in man pages and as a short intro on the website *) ; cli_flags: cli_flags option (** If [None] then the checker cannot be enabled/disabled from the command line. *) ; enabled_by_default: bool diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 6c261c5be..5b45e4c9d 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -537,25 +537,25 @@ and () = | None -> (* HACK: return a constant ref if the checker cannot be enabled/disabled from the command line *) ref config.enabled_by_default - | Some {long; deprecated; show_in_help} -> + | Some {deprecated; show_in_help} -> let in_help = if show_in_help then in_analyze_help else [] in - CLOpt.mk_bool ?f ~long ~in_help ~default:config.enabled_by_default ~deprecated - config.short_documentation + CLOpt.mk_bool ?f ~long:config.id ~in_help ~default:config.enabled_by_default ~deprecated + (Printf.sprintf "checker %s: %s" config.id config.short_documentation) in all_checkers := (checker, config, var) :: !all_checkers in List.iter Checker.all ~f:mk_checker ; let mk_only (_checker, config, var) = - Option.iter config.cli_flags ~f:(fun {long; show_in_help} -> + Option.iter config.cli_flags ~f:(fun {show_in_help} -> let (_ : bool ref) = - CLOpt.mk_bool_group ~long:(long ^ "-only") + CLOpt.mk_bool_group ~long:(config.id ^ "-only") ~in_help:InferCommand.[(Analyze, manual_generic)] ~f:(fun b -> disable_all_checkers () ; var := b ; b ) ( if show_in_help then - Printf.sprintf "Enable $(b,--%s) and disable all other checkers" long + Printf.sprintf "Enable %s and disable all other checkers" config.id else "" ) [] (* do all the work in ~f *) [] (* do all the work in ~f *) @@ -571,8 +571,8 @@ and () = ^ ( List.rev_filter_map ~f:(fun (_, config, _) -> match config.cli_flags with - | Some {long} when config.enabled_by_default -> - Some (Printf.sprintf "$(b,--%s)" long) + | Some _ when config.enabled_by_default -> + Some (Printf.sprintf "$(b,--%s)" config.id) | _ -> None ) !all_checkers diff --git a/infer/tests/codetoanalyze/objc/self-in-block/Makefile b/infer/tests/codetoanalyze/objc/self-in-block/Makefile index f85b79b71..70c4bdb31 100644 --- a/infer/tests/codetoanalyze/objc/self-in-block/Makefile +++ b/infer/tests/codetoanalyze/objc/self-in-block/Makefile @@ -6,7 +6,7 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS) -fobjc-arc -INFER_OPTIONS = --self_in_block-only --debug-exceptions --project-root $(TESTS_DIR) +INFER_OPTIONS = --self-in-block-only --debug-exceptions --project-root $(TESTS_DIR) INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.m)