Summary:
The gist of this diff is a set of Pulse models for the built-ins
that have been put in Sil by the Erlang frontend:
- __erlang_make_nil, for creating an empty list like []
- __erlang_make_cons, for creating a nonempty list like [1|[]]
- __erlang_pattern_fail, which marks that no pattern matched
The models for the first two update the abstract state. The model for
the third generates a reportable error.
The diff also includes a test.
And also a few bugfixes:
- a type ErlangAny was used sometimes instead of ErlangAny*
- a load that was meant to be n=13 was instead n=*13;
changed to (*tmp=13; n=*tmp)
- the Makefile's guard for the rebar build-system test was inside the large
guard for java analyzers; of course, we don't need java to run rebar
Reviewed By: jvillard
Differential Revision: D29230161
fbshipit-source-id: c8fd6d88a
Summary: Added a new issue type for sending a message to nil when its return type is non-POD. To distinguish these issues from other nullptr dereference issues, we extend the `MustBeValid` attribute to contain the reason of why an address must be valid. For now a reason can only have `SelfOfNonPODReturnMethod` as it's value, but in the future we will use it for other nullability issue types, such as nil insertion into collections.
Reviewed By: jvillard
Differential Revision: D27762333
fbshipit-source-id: 689e5a431
Summary:
Before this diff, TOPL had 3 implementations:
1. a post-processing of biabduction summaries
2. a post-processing of pulse summaries
3. a deep embedding in pulse
1 and 2 additionally require instrumenting SIL to generate monitors for
the TOPL properties. 3 is faster than both 1 and 2, by a good lot, and
doesn't require instrumenting the SIL code. Thus, delete 1 and 2!
Also harmonise the CLI so that TOPL is activated by --topl, which
actives it as a checker, like other analyses.
Reviewed By: rgrig
Differential Revision: D27270178
fbshipit-source-id: e86cf972b
Summary: `STARVATION` is currently used as a catch-all for several blocking events. This diff splits out `IPC_ON_UI_THREAD`.
Reviewed By: skcho
Differential Revision: D26691868
fbshipit-source-id: 618423793
Summary:
This diff uses config-impact-issues.exp instead of issues.exp, like in
the cost checker.
Reviewed By: ezgicicek
Differential Revision: D26723761
fbshipit-source-id: 9c6779479
Summary:
Currently, we report on all functions that are not config checked. However, the aim of the analysis is to only report on these for specific functions. Moreover, this has performance implications in practice.
This diff instead reports on functions that occur on a json file that is passed by the command line option `config-data-file`.
Reviewed By: skcho
Differential Revision: D26666336
fbshipit-source-id: 290cd3ada
Summary:
Races in Nullsafe classes can undermine NPE safety despite the class passing the type checks.
This diff adds to the report text of THREAD_SAFETY_VIOLATION and GUARDEDBY_VIOLATION the following trailer:
> Data races in `Nullsafe` classes may still cause NPEs.
This only happens if the race is directly on a non-primitively-typed member field of the class.
It also uses distinct bug types (adds the suffix _NULLSAFE to the bug types above) for easier accounting.
Reviewed By: ezgicicek
Differential Revision: D26403274
fbshipit-source-id: 3cd6ca082
Summary:
`SettableFuture.set` invokes callbacks registered prior to the call, which may also try to acquire extra locks. If the called of `set` already holds a lock this creates lock dependencies which may lead to deadlocks.
Here we warn whenever `set` is called under a lock taken in a different source file. This avoids reporting when a class internally manages locks and calls `set`, reasoning that developers will be aware this is happening.
Reviewed By: jvillard
Differential Revision: D25562190
fbshipit-source-id: d1b5cb69c
Summary:
Dear Infer team,
To contribute to Infer community, I would like to integrate infer#'s language agnostic layer into Infer.
Please help to review, discuss and consider to merge this feature.
Thanks,
Xiaoyu
Pull Request resolved: https://github.com/facebook/infer/pull/1361
Reviewed By: skcho
Differential Revision: D25928458
Pulled By: jvillard
fbshipit-source-id: 7726150b8
Summary:
This diff adds uninitialized value check in pulse. For now, it supports only simple cases,
- declared variables with a type of integer, float, void, and pointer
- malloced pointer variables that points to integer, float, void, and pointer
TODOs: I will add more cases in the following diffs.
- declared/malloced array
- declared/malloced struct
- inter-procedural checking
Reviewed By: jvillard
Differential Revision: D25269073
fbshipit-source-id: 317df9a85
Summary:
This diff adds a new issue type for reporting modifications to immutable fields (when `report-immutable-modifications` is enabled).
The underlying analysis depends on impurity analysis which itself is based on post-processing of pulse's summaries.
Reviewed By: skcho
Differential Revision: D25216637
fbshipit-source-id: 42e843793
Summary:
This diff glues the previous work together.
The ClassLevelAnalysis finds list of provisional violation, builds the
graph based on them, and outputs this graph as a separate issue.
Reviewed By: artempyanykh
Differential Revision: D24682802
fbshipit-source-id: 8174da91a
Summary:
This diff adds a new experimental checker for detecting size of objects in autorelease pool in ObjC. The basic mechanism is almost the same with the previous cost calculation:
* Autorelease pool size is increased at explicit `autorelease` call
* Autorelease pool size is set as zero by the `autoreleasepool` block.
While it only supports the explicit calls as of now, we will extend the checker to handle more cases in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D23473145
fbshipit-source-id: 416488176
Summary:
This diff extends the cost_item json format to print the autoreleasepool_size field. Not yet, there
is no semantics for that code kind, so the results will always be zero with no traces.
Reviewed By: ezgicicek
Differential Revision: D23540665
fbshipit-source-id: 94442e376
Summary:
Report errors found by running Topl on top of Pulse, when using
--topl-pulse. Topl tests now run on top of Pulse.
Reviewed By: jvillard
Differential Revision: D23030771
fbshipit-source-id: 8770c2902
Summary:
We need to check if `folly::Optional` is not `folly::none` if we want to retrieve the value, otherwise a runtime exception is thrown:
```
folly::Optional<int> foo{folly::none};
return foo.value(); // bad
```
```
folly::Optional<int> foo{folly::none};
if (foo) {
return foo.value(); // ok
}
```
This diff adds a new issue type that reports if we try to access `folly::Optional` value when it is known to be `folly::none`.
Reviewed By: ezgicicek
Differential Revision: D22053352
fbshipit-source-id: 32cb00a99
Summary: This linters were not used much anymore, so we can delete them.
Reviewed By: ngorogiannis
Differential Revision: D22233895
fbshipit-source-id: f31180a05
Summary: There is now a compilation check for UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK so this check is less useful. Also the check REGISTERED_OBSERVER_BEING_DEALLOCATED is useful only in an old version of iOS.
Reviewed By: ngorogiannis
Differential Revision: D22231851
fbshipit-source-id: 72151fef5
Summary:
This diff adds a prototype of a new checker that collects config checkings between markers.
Basically, what the checker is doing is a taint analysis.
* Taint source: function calls of "marker start"
* Taint sink: function calls of config checking
* Taint remove: function calls of "marker end"
By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending.
I am separating the diff into three steps:
(1/3) Add basic abstract semantics
(2/3) Add trace information
(3/3) Add reporting with test examples
Reviewed By: jvillard
Differential Revision: D21998170
fbshipit-source-id: e7759f62f
Summary: Pulse has now a better version of this check, so let's delete it.
Reviewed By: ngorogiannis
Differential Revision: D22019247
fbshipit-source-id: 344678225
Summary:
This issue type was not giving good results and can be replaced by
Pulse's version.
Reviewed By: ngorogiannis
Differential Revision: D22019551
fbshipit-source-id: 5cf3db46d
Summary: The new memory leaks analysis is now ready to be enabled by default and turned on in production. This also replaces the biabduction one which is now disabled.
Reviewed By: jvillard
Differential Revision: D21998666
fbshipit-source-id: 9cd95e894
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:
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:
`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:
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
Radu Grigore
Sungkeun Cho
Daiva Naudziuniene
Jules Villard
Nikos Gorogiannis
Ezgi Çiçek
Xiaoyu Liu
Mitya Lyubarskiy
Dulma Churchill