Summary:
Similarly as for issue types, we want to generate the website
documentation from infer itself so we can easily cross-reference
checkers and the issue types they report.
This imports the website documentation written for some (very few) of
the checkers. I wrote some cursory one-liners for the rest.
Reviewed By: dulmarod
Differential Revision: D21934375
fbshipit-source-id: 8c9dc2b08
Summary:
Take all the issue type documentation in the website and add it to infer
itself so it can generate the website (see further diffs).
I mostly generated this diff by writing a script to call from `utop`
with various file lists to do most of the heavy lifting for me and make
sure I didn't forget any issue types: P132800781
Reviewed By: ngorogiannis
Differential Revision: D21934372
fbshipit-source-id: f3ea8c566
Summary:
`infer help` will be used to display information about issue types and
checkers, and to generate the corresponding website documentation. We
can add more things in it over time. The goal is to avoid having to go
read the source code of infer to figure things out that are user-facing.
Reviewed By: ezgicicek
Differential Revision: D21934376
fbshipit-source-id: 2788c5af1
Summary:
We stopped relying on an arbitrary threshold. Hence,
- we don't need all the machinery for reporting at a specific node for a threshold
- we can remove
- the issue type `EXPENSIVE_EXECUTION_TIME`
- the config option `--use-cost-threshold`.
Reviewed By: skcho
Differential Revision: D21859815
fbshipit-source-id: b73a2372d
Summary:
In order to test cost analysis results, currently we rely on having an arbitrary cost threshold (200) and report issues that exceed this cost. For instance, a cost of 201 is considered expensive and reported as `EXPENSIVE_EXECUTION_TIME` issue in cost tests.
This means, if we change the cost analysis in a slight way that results in some constant cost increase under 200, we wouldn't able to detect it. I find this unsatisfactory and somewhat hacky.
This diff adds the ability to write the result of `costs-report.json` into a separate `cost-issues.exp` and then compare the actual costs (not only than relying on this arbitrary threshold reporting mechanism).
Reviewed By: skcho
Differential Revision: D21816312
fbshipit-source-id: 93b531928
Summary:
The option was misleading as it only concerns the biabduction analysis.
Moreover, this is a developer option, and one can already see it by
removing filtering altogether. I think this option was added as the
result of a user request, let's see if anyone notices.
Reviewed By: ezgicicek
Differential Revision: D21686526
fbshipit-source-id: ff383a0ca
Summary:
Don't assign different visibilities to the same issue type dynamically,
use different issue types with always static visibility instead. This is
to be able to document the visibility of each issue type.
Reviewed By: dulmarod
Differential Revision: D21686458
fbshipit-source-id: 876ab4157
Summary:
Introduce BIABD_ prefixes for a few issue types that were duplicated
between analyses, and also prefix the lab exercise issue type to avoid
sharing with biabduction.
Reviewed By: ngorogiannis
Differential Revision: D21660226
fbshipit-source-id: 3435916e6
Summary:
A buck integration for capturing simultaneously clang and java targets.
Just like the java-specific `JavaGenruleCapture` integration, it relies on
dummy targets that depend on the flavoured clang versions.
For example, a `cxx_library` target named `//clang:hello` will have an associated target
called `//clang:hello_infer` that depends on `//clang:hello#infer-capture-all`,
and whose output is a text file containing the output path of the dependency.
Reviewed By: jvillard
Differential Revision: D21620458
fbshipit-source-id: 23919387b
Summary:
`ocamlc` didn't tell us but there are a bunch of dead exceptions in
`Exceptions.ml` that translate into dead issue types.
Found with:
```
for ex in $(grep -o -e '^exception [^ ]*' infer/src/IR/Exceptions.mli | cut -d ' ' -f 2); do git grep -q -e '\braise .*'$ex || git grep -q -e 'Exceptions\.'$ex || echo $ex; done
```
Reviewed By: skcho
Differential Revision: D21618645
fbshipit-source-id: f60a3f445
Summary:
This seems to make sense as it's a separate analysis (that depends on
biabduction). This introduces unpleasant `|| is_checker_enabled TOPL`
whenever we try to figure out if biabduction will run. I think this is a
more general problem that deserves a more general solution to express
the fact that checkers can depend on others, so that, eg,
`is_checker_enabled Purity` is true when we pass `--loop-hoisting`. Will
address in another diff.
Reviewed By: ngorogiannis
Differential Revision: D21618460
fbshipit-source-id: 8b0c9a015
Summary:
We stopped relying on an external perf data file to determine which functions are on the cold start. Let's remove this issue now.
NB: Keeping the `--perf-profiler-data-file` as deprecated to prevent issues on the CI and prod.
Reviewed By: skcho
Differential Revision: D21594150
fbshipit-source-id: faa58782d
Summary:
Pulse is disabled by default anyway so it's safe to enabled it for Java
too.
Also noticed that OCaml is smart enough not to need `Language.` in
frontend of `Clang`/`Java` in all of registerCheckers.ml so delete
these.
Reviewed By: ezgicicek
Differential Revision: D21594364
fbshipit-source-id: 4b561c9a0
Summary:
Just like `CFBridgingRelease` we want to be able to model functions that are specific to a given codebase that make a transfer of memory ownership so that developers don't need to worry about releasing that memory anymore, and hence, we don't want to report leaks on that memory.
Things get a little more complicated, because some of the functions we want to model are in a specific namespace, so with this flag we take both cases into account, when we are dealing with namespaces or not.
Reviewed By: jvillard
Differential Revision: D21404409
fbshipit-source-id: c36bd7afc
Summary:
Because in the real semantics CFRelease can be used more than once, and also the variables can be used after CFRelease in general, modelling this as `free` causes many `USE_AFTER_FREE` errors. Now we change the model to not add the `Invalid CFree` attribute, but to just remove the `Allocated` attribute. So we can model memory leaks in the simple case of `Create` and not `CFRelease` before going out of scope, but we avoid the `USE_AFTER_FREE`.
Since the model for CFRelease now diverges from free, changed the command line option for modelling to `pulse-model-release-pattern`.
Reviewed By: jvillard
Differential Revision: D21324895
fbshipit-source-id: ab323d981
Summary: This diff gets only one disjunct from blacklisted callee, in order to avoid OOMing in specific cases.
Reviewed By: jvillard
Differential Revision: D21406023
fbshipit-source-id: f9214c9c6
Summary:
In the previous diff we changed the semantics of nested classes w.r.t.
to Nullsafe.
Let's make it clear if users will attempt to misuse it.
Reviewed By: artempyanykh
Differential Revision: D21230717
fbshipit-source-id: 0ecc0dd06
Summary: Specialise the above option to `true` and remove resulting dead code.
Reviewed By: dulmarod
Differential Revision: D21177041
fbshipit-source-id: 4a1c65850
Summary: This option makes RacerD angelic wrt the ownership of returned objects from procedures without summary. This will now be made the default and the option deprecated up the diff stack.
Reviewed By: dulmarod
Differential Revision: D21174676
fbshipit-source-id: 9c48d3d7d
Summary:
It is true that `Info` issues are normally not intended for the end user
and in general should be hidden by default.
However, the current behavior - show them only if `--no-filtering` is
true - is super non-intuitive and complicates already complex reporting
logic.
Lets use the general "enable/disable" mechanism for controlling this.
Reviewed By: jvillard
Differential Revision: D21154140
fbshipit-source-id: 69e4c88e4
Summary: The flags `--biabduction-fallback-model-alloc-pattern` and `--biabduction-fallback-model-free-pattern` were unused because we removed the models from .inferconfig a while ago because of too many false positives. We are implementing a better memory leak check based on Pulse, and are adding the similar flags `--pulse-model-alloc-pattern` and `--pulse-model-free-pattern`.
Reviewed By: jvillard
Differential Revision: D21061511
fbshipit-source-id: 1b3476c22
Summary:
This information can be useful for tooling responsible for further
processing (e.g. metric calculation and logging)
Reviewed By: artempyanykh
Differential Revision: D20914583
fbshipit-source-id: 61804d88f
Summary:
This diff limits the depth of abstract location by a constant.
problem: Inferbo generated too many of abstract locations, especially when struct types had many pointer fields and Inferbo was not able to analyze the objects precisely. Since the number of generated abstract locations were exponential to the number of fields, it resulted in OOM in the end.
(reported by zyh1121 in https://github.com/facebook/infer/issues/1246)
Reviewed By: jvillard
Differential Revision: D20818471
fbshipit-source-id: f8af27e5c
Summary:
It's easy to create large arrays in code, eg `int x[1UL << 16];`, but
these can generate huge nodes in SIL because zero-initialization is
translated by zero-ing structures element by element. Introduce a
builtin to use instead. Keep the naive method for small structures (with
a configurable limit on "small").
Reviewed By: dulmarod
Differential Revision: D20836836
fbshipit-source-id: 6bf5410f8
Summary:
Re-implement the generation of an HTML report (with bug traces) in
OCaml.
Kills the --only-show as a side-effect, it is of dubious use since there
is already infer-out/report.txt to get the report list as text. A
follow-up diff adds numbers to the list in infer-out/report.txt for easy
cross-referencing with `infer explore --select 123`.
Reviewed By: skcho
Differential Revision: D20672769
fbshipit-source-id: 39b3a299d
Summary:
Hopefully no one uses this. This is in Python and we'd like to get rid
of it. Easy enough to either re-implement if needed or to be
re-implemented by a third party.
Reviewed By: ngorogiannis
Differential Revision: D20626344
fbshipit-source-id: 484022482
Summary:
Seems like a more sensible name. Most tooling should read report.json so
won't notice.
Still output a bugs.txt file with a message to point to report.txt while
people migrate.
Reviewed By: mityal, artempyanykh
Differential Revision: D20626111
fbshipit-source-id: efb84d098
Summary:
The documentation of `--quiet` dates back from when it applied only to
`InferPrint.ml`. Make it more general and more in line with
expectations one might have about a `--quiet` option:
- change the doc
- make it disable the progress bar
Reviewed By: ngorogiannis
Differential Revision: D20626110
fbshipit-source-id: db096fd31
Summary:
This is likely not the final refinement, rather one step forward.
We classify all classes by 3 categories:
- Nullsafe and 0 issues
- can add Nullsafe and will be 0 issues
- the rest (class needs improvement)
Each class will fall into exactly one category.
Error messaging is WIP, they are not intended to be surfaced to the user
just yet.
Note how this diff uses the result of the previous refactoring.
Reviewed By: artempyanykh
Differential Revision: D20512999
fbshipit-source-id: 7f462d29d
Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.
Reviewed By: jvillard
Differential Revision: D20444097
fbshipit-source-id: 33b6b25a2
Summary:
This diff is doing three things:
1. Finishes work paved in D20115024, and applies it to nullsafe. In that diff, we hardened API for
file level analysis. Here we use this API in nullsafe, so now we can
analyze things on file-level, not only in proc-level like it was before!
2. Introduces a class-level analysis. For Nullsafe purposes, file is not
an interesting granularity, but we want to analyze a lot of things on
file level. Interesting part here is anonymous classes and how we link
them to their corresponding user-defined classes.
3. Introduces a first (yet to be improved) implementation of class-level
analysis. Namely it is "meta-issues" that tell what is going with class
on high level. For now these are two primitive issues, and we will
refine them in follow up diffs. They are disabled by default.
Follow ups include:
1. Refining semantics of meta-issues.
2. Adding other issues that we could not analyze before or analyzed not
user friendly. Most importantly, we will use it to improve reporting for
FIELD NOT INITIALIZED, which is not very user friendly exactly because
of lack of class-level aggregation.
Reviewed By: artempyanykh
Differential Revision: D20417841
fbshipit-source-id: 59ba7d2e3
Summary:
This was never quite finished and inferbo has a new way to do sort of
the same thing.
Reviewed By: skcho, ngorogiannis
Differential Revision: D20362619
fbshipit-source-id: 7c7935d47
Summary:
Make <infer-out>/report.json the default value for this option, as this
is what is used 99% of the time. Clean up test options using this.
Reviewed By: ngorogiannis
Differential Revision: D20362644
fbshipit-source-id: a1bb18757
Summary:
InferPrint hasn't been in charge of writing bugs.txt since forever.
This will be re-implemented as a post-processing of report.json instead
(like it is now, but in OCaml instead of python).
Reviewed By: ngorogiannis
Differential Revision: D20362641
fbshipit-source-id: 83d8cb53d
Summary:
Warning: This might be a bit brutal.
PerfStats and EventLogger are pretty much subsumed by `ScubaLogging`.
It seems no one has been looking at the data they generate recently.
Let's delete them! If we need to re-implement some parts later on, let's
do that using `ScubaLogging`, which is better (eg, still produces data
when infer crashes).
Things we lose:
- errors in the clang frontend due to missing decl translation, etc.
- errors in biabduction due to timeouts, functions not found, etc.
We could also re-implement these using BackendStats and ScubaLogging
instead of brutally deleting everything.
Reviewed By: ngorogiannis
Differential Revision: D20343087
fbshipit-source-id: 90a3121ca
Summary:
The goals are to have all the checker definitions and documentation in one
place (except how to actually run them, since that's not quite the same
concept; for example inferbo is one checker but several analyses depend on its
symbolic execution), and later on to be able to link issues reported by infer
back to the checker that generated them.
This makes apparent that the documentation of our checkers is lacking,
not touching that in this diff.
Not sure if "analysis" would be a better name than "checker" at this
point? For instance "Linters" is one of the checkers, which historically
at least we have not considered to be the case.
Reviewed By: mityal
Differential Revision: D20252386
fbshipit-source-id: fc611bfb7
Summary:
Problem: `infer report <specs file name>` is called manually sometimes to see analysis results in CLI. However, giving the specs file name is sometimes annoying, because the specs file name may be quite long and include special characters sometimes.
This diff introduces `--procedures-summary` to lookup the summaries interactively in `infer explore`.
example1: There are 8 procedures that include "max" in their names, then I selected one of them by entering a number.
```
$ infer explore --procedures --procedures-filter '.*max.*' --procedures-summary
0: minmax_div_const2_Bad_FN
1: minmax_div_const_Good
2: use_int64_max_Bad
3: use_uint64_max_Good
4: use_int64_max_Good
5: minmax_div_const_Bad
6: minmax_div_const2_Good
7: use_uint64_max_Bad
Select one number (type 'a' for selecting all, 'q' for quit): 2
void use_int64_max_Bad()
Analyzed
ERRORS: BUFFER_OVERRUN_L1
WARNINGS:
FAILURE:NONE SYMOPS:0
BufferOverrunAnalysis: StackLocs: { } MemPure: { } Alias: { ret= }
BufferOverrunChecker: Safety conditions:
{ }
```
example2: If there is only one specs file that satisfies the given filter, it reports the summary of that procedure without an interaction.
```
$ infer explore --procedures --procedures-filter '.*add_in_loop_ok.*' --procedures-summary
Selected proc name: void ArrayListTest.add_in_loop_ok()
void void ArrayListTest.add_in_loop_ok()(ArrayListTest* this)
Analyzed
ERRORS:
WARNINGS:
FAILURE:NONE SYMOPS:0
BufferOverrunAnalysis: StackLocs: { } MemPure: { } Alias:
{ i=size(__new-390022197-0-1.elements), ret= }
LatestPrune: latest { i -> (5, { }, { }) by ((5, { }, { }) >= (5, { }, { })),
__new-390022197-0-1.elements -> (⊥, { }, { __new-390022197-1-1 -> length : 5 }) by ((5, { }, { }) >= (5, { }, { })) }
BufferOverrunChecker: Safety conditions:
{ }
```
Reviewed By: jvillard
Differential Revision: D20284052
fbshipit-source-id: 2131339f1
Summary:
These were not used (and were actually activated byt the same config
param). They both are in experimental stage that never reached maturity.
Since the team does not have immediate plans to work on ObjC nullability
checker; and since "eradicate" (now known as nullsafe) is the main
solution for Java, removing it is sensible.
Reviewed By: jvillard
Differential Revision: D20279866
fbshipit-source-id: 79e64992b
Summary:
This diff renames `ZERO_XXX` issues to more appropriately named and descriptive
`XXX_UNREACHABLE_AT_EXIT` and replaces bottom with
unreachable in cost kinds and issues.
Reviewed By: skcho
Differential Revision: D20140301
fbshipit-source-id: eb6076b30
Summary:
The `--continue-analysis` option enables continuing analysis after more targets are captured by
`--continue`. For example,
```
$ infer capture -- buck build tgt1
$ infer analyze --merge
$ infer capture --continue -- bucck build tgt2
$ infer analyze --merge --continue-analyze
```
In the last analysis, it reuses the analysis results of `tgt1` from the previous analysis. If
`tgt1` and `tgt2` have a same dependency to a library, the analysis results of the library is also
reused.
Reviewed By: dulmarod
Differential Revision: D19996598
fbshipit-source-id: bb6874a6f
Summary:
Add support for nullsafe mode with `trust=all` and `trust=none` a case
with a specific trust list is not supported yet and needs to be
implemented separately.
Tests introduce one unexpected
`ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION` issue which
complains about `this` having incorrect nullability; it is a bug and
needs to be fixed separately.
Reviewed By: mityal
Differential Revision: D19662708
fbshipit-source-id: 3bc1e3952
Summary: We don't use allocation costs in prod at the moment. There is no plan to do so in the near future. Let's not report them anymore and also save some space in `costs-report.json`.
Reviewed By: skcho
Differential Revision: D19766828
fbshipit-source-id: 06dffa61d
Summary:
This diff introduces two issue types: `BUFFER_OVERRUN_T1` and `INFERBO_ALLOC_IS_TAINTED`, which
denotes tainted values are used in array accesses and memory allocations, respectively.
Note that the taint analysis is intra-procedural for now.
Reviewed By: ezgicicek
Differential Revision: D19410536
fbshipit-source-id: af85148ec
Summary:
This diff adds a taint domain in Inferbo. The taint value will be used to find vulnerable array
accesses in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D19391028
fbshipit-source-id: 566b4c0fe
Summary: This adds a check for when developers use weakSelf (and maybe strongSelf) in a block, when there is no need for it, because it won't cause a retain cycle. In general there is an annotation in Objective-C for methods that take blocks, NS_NOESCAPE, that means that the passed block won't leave the scope, i.e. is "no escaping". So we report when weakSelf is used and the block has the annotation.
Reviewed By: ngorogiannis
Differential Revision: D19662468
fbshipit-source-id: f5ac695aa
Summary:
Adding a new check as part of the SelfInBlock checker, for cases when a strong pointer to self, that is not self, is captured in the block.
This will cover the following wrong scenarios:
1. strongSelf is a local variable in a block as it should be, and then it's used in a sub-block, in which case it's a captured variable.
2. weakSelf is defined without the weak attribute by mistake.
Reviewed By: ngorogiannis
Differential Revision: D19538036
fbshipit-source-id: 151871745
Jules Villard
Ezgi Çiçek
Nikos Gorogiannis
Dulma Churchill
Sungkeun Cho
Mitya Lyubarskiy
Artem Pianykh