Summary:
Due to limitations in our Buck integration, the thread-safety analysis cannot create a trace that bottoms out in a Buck target that is not a direct dependency of the current target.
These truncated traces are confusing and tough to act on.
Until we can address these limitations, let's avoid reporting on truncated traces.
Reviewed By: jeremydubreil
Differential Revision: D5969840
fbshipit-source-id: 877b9de
Summary:
:
Make both buck capture and compilation database handle buck command line arguments and invoke buck query the same way.
Plus allow:
- target patterns `//some/dir:` and `//some/dir/...`. However since `//some/dir:#flavor` and `//some/dir/...#flavor` are not supported, they need to be expanded before adding the infer flavor.
- target aliases (defined in `.buckconfig`)
- shortcuts `//some/dir` rewritten to `//some/dir:dir`
- relative path `some/dir:name` rewritten to `//some/dir:name`
Reviewed By: jvillard
Differential Revision: D5321087
fbshipit-source-id: 48876d4
Summary:
If you write
```
boolean readUnderLockOk() {
synchronized (mLock) {
return mField;
}
}
```
it will be turned into
```
lock()
irvar0 = mField
unlock()
return irvar0
```
in the bytecode. Since HIL eliminates reads/writes to temporaries, it will make the above code appear to perform a read of `mField` outside of the lock.
This diff fixes the problem by forcing HIL to perform all pending reads/writes before you exit a critical section.
Reviewed By: jberdine
Differential Revision: D6138749
fbshipit-source-id: e8ad9a0
Summary: In HIL, allow deref'ing a magic address like `0xdeadbeef` for debugging purposes. Previously, we would crash on code like this.
Reviewed By: mbouaziz
Differential Revision: D6143802
fbshipit-source-id: 4151924
Summary: This check is deprecated and will be replaced by a dedicated checker to detect unitialized values.
Reviewed By: mbouaziz
Differential Revision: D6133108
fbshipit-source-id: 1c0e9ac
Summary: Previously, this would incorrectly classify types like `map<std::string, int>` as a buffer
Reviewed By: mbouaziz
Differential Revision: D6125530
fbshipit-source-id: c8564de
Summary:
This is in the spec for clang compilation databases.
Also improves error messages when we fail to parse the compilation database.
closes#771
Reviewed By: dulmarod
Differential Revision: D6123832
fbshipit-source-id: 070f70f
Summary: In preparation for making `-a checkers` the default (when no analyzer is specified), let's test `-a checkers` by default.
Reviewed By: mbouaziz
Differential Revision: D6051177
fbshipit-source-id: d8ef611
Summary:
Refactor `RegisterCheckers` to give a record type to checkers instead of a tuple type.
Print active checkers with their per-language information.
Improve the manual entries slightly.
Reviewed By: sblackshear
Differential Revision: D6051167
fbshipit-source-id: 90bcb61
Summary:
Whenever we see a use of a lock, infer that the current method can run in a multithreaded context. But only report when there's a write under a lock that can be read or written without synchronization elsewhere.
For now, we only infer this based on the direct usage of a lock; we don't assume a caller runs in a multithreaded context just because its (transitive) callee can.
We can work on that trickier case later, and we can work on smarter inference that takes reads under sync into account. But for now, warning on unprotected writes of reads that occur under sync appears to be too noisy.
Reviewed By: jberdine
Differential Revision: D5918801
fbshipit-source-id: 2450cf2
Summary: This commit adds unsigned symbol for preciser analysis results with less number of uses of min/max operators.
Reviewed By: mbouaziz
Differential Revision: D6040437
fbshipit-source-id: 999ca4c
Summary:
This was a crutch from the days before ownership analysis.
We shouldn't need it anymore, and it was actually causing FP's because we were skipping analysis of `ImmutableList.builder()` and not understanding that the return value is owned.
Reviewed By: jeremydubreil
Differential Revision: D6035631
fbshipit-source-id: afa0ade
Summary:
This generates `--resource-leak-only` automatically, and make the other
checkers' `-only` option work as expected with respect to `--resource-leak` too
(eg, `--resource-leak --biabduction-only` disables resource leak).
Reviewed By: jeremydubreil
Differential Revision: D6051134
fbshipit-source-id: 2d4a2ba
Summary:
1. Mark some Makefile targets as depending on `MAKEFILE_LIST` so they get rebuilt on Makefile changes
2. Do not show boolean options with no documentation in the man pages (like we do for other option types).
3. Default to Lazy dynamic dispatch for the checkers.
4. In the tests, use `--<checker>-only` instead of relying on `--no-default-checkers`
5. `--no-filtering` is redundant if `--debug-exceptions` is passed
Reviewed By: jeremydubreil
Differential Revision: D6030578
fbshipit-source-id: 3320f0a
Summary: We will then be able to merge the tests for the other checkers without affecting these lab tests
Reviewed By: jvillard
Differential Revision: D6039433
fbshipit-source-id: e575ce9
Summary:
Another step toward running the biabduction analysis as a checker.
Depends on D6038210
Reviewed By: jvillard
Differential Revision: D6038682
fbshipit-source-id: fed45bf
Summary: Stack-allocated variables cannot be raced on in cpp as every thread has its own stack. At the beginning of the analysis we add ownership to the local variables.
Reviewed By: jberdine
Differential Revision: D6020506
fbshipit-source-id: 0a90a97
Summary: Now that we report write-write races involving more than one write, we need to improve the traces accordingly.
Reviewed By: jberdine
Differential Revision: D6026845
fbshipit-source-id: b1366dd
Summary:
Next step to issue deduplication: do not keep safety conditions that are subsumed by others.
Only do it if they do not have infinite bound: replacing `0 < size` by `1 < size` is ok, but replacing it by `+oo < size` is not because it looks much more like a lack of precision.
Reviewed By: skcho
Differential Revision: D5978455
fbshipit-source-id: acc2384
Summary:
A specific type of alias is added for the vector::empty() result and it is used at pruning.
Now, there are two types of aliases:
- "simple" alias: x=y
- "empty" alias: x=v.empty() and y=v.size
So, if x!=0, y is pruned by (y=0). Otherwise, i.e., x==0, y is pruned by (y>=1).
Reviewed By: mbouaziz
Differential Revision: D6004968
fbshipit-source-id: bb8d50d
Summary:
Attempting to translate these will not go well as the declaration still depends
on some template arguments. Added a test that was previously crashing the
frontend.
Also extend the catching of "Unimplemented" and other errors to `translate_one_decl` as it was useful to debug this issue. In particular, reraise all exceptions and log some additional context when doing so.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D5976357
fbshipit-source-id: fca8e38
Summary:
Previously, annotating something ThreadSafe meant "check that it is safe to run all of this procedure's methods in parallel with each other" (including self-parallelization).
This makes sense, but it means that if the user writes no annotations, we do no checking.
I'm moving toward a model of inferring when an access might happen on a thread that can run concurrently with other threads, then automatically checking that it is thread-safe w.r.t to all other accesses to the same memory (on or off the current thread thread).
This will let us report even when there are no `ThreadSafe` annotations.
Any method that is known to run on a new thread (e.g., `Runnable.run`) will be modeled as running on a thread that can run in parallel with other threads, and so will any method that is `synchronized` or acquires a lock.
In this setup, adding `ThreadSafe` to a method just means: "assume that the current method can run in parallel with any thread, including another thread that includes a different invocation of the same method (a self race) unless you see evidence to the contrary" (e.g., calling `assertMainThread` or annotating with `UiThread`).
The key step in this diff is changing the threads domain to abstract *what threads the current thread may run in parallel with* rather than *what the current thread* is. This makes things much simpler.
Reviewed By: jberdine
Differential Revision: D5895242
fbshipit-source-id: 2e23d1e
Summary:
Indicate if read or write is protected, and do not print only the
field but also the object involved in the race.
Reviewed By: sblackshear
Differential Revision: D5974250
fbshipit-source-id: 351a576
Summary:
Move Inferbo safety conditions to their own file.
Split the old `Condition.t` to a condition together with a trace.
This will ease having: different kind of condition and several traces for the same condition (see following diff)
Reviewed By: jvillard
Differential Revision: D5942030
fbshipit-source-id: d74a612
Summary:
Inject a marker using a global variable in <iostream>, and whitelist it so that
the frontend translates it.
Use the marker in the SIOF checker to tell whether a file includes <iostream>.
If so, start the analysis of its methods assuming that the standard streams are
initialised.
Reviewed By: sblackshear
Differential Revision: D5941343
fbshipit-source-id: 3388d55
Summary:
The previous domain for SIOF was duplicating some work with the generic Trace
domain, and basically was a bit confused and confusing. A sink was a set of
global accesses, and a state contains a set of sinks. Then the checker has to
needlessly jump through hoops to normalize this set of sets of accesses into a
set of accesses.
The new domain has one sink = one access, as suggested by sblackshear. This simplifies
a few things, and makes the dedup logic much easier: just grab the first report
of the list of reports for a function.
We only report on the fake procedures generated to initialise a global, and the
filtering means that we keep only one report per global.
Reviewed By: sblackshear
Differential Revision: D5932138
fbshipit-source-id: acb7285
Summary:
This adds more structure to the SQL schema backing attributes. With that, we
can transfer the logic for updating attributes in SQLite, instead of doing
optimistic concurrency in the client.
Reviewed By: jberdine
Differential Revision: D5891038
fbshipit-source-id: 6577ba2
Summary: The case of closures was not considered for the convertion of SIL instructions into HIL instructions
Reviewed By: sblackshear
Differential Revision: D5929675
fbshipit-source-id: bb6920a
Summary: The tests are slower when running in debug mode, and it creates a lot of html outputs
Reviewed By: sblackshear
Differential Revision: D5916511
fbshipit-source-id: 07c90b7
Summary:
This diff does two things:
# Infer no longer add the contrains that the return value of a skip function is never null. This was leading to false negatives and is not necessary as those return value are treated angelically
# Infer now support `Nonnull` on the return value of skip functions.
Reviewed By: jberdine, sblackshear
Differential Revision: D5840324
fbshipit-source-id: bbd8d82
Summary: Example of combination between annotating fields with nullable and the biabduction analysis in Objective C
Reviewed By: dulmarod
Differential Revision: D5906016
fbshipit-source-id: b95c6e0
Summary:
The interval bound of the abstract domain is extended.
`[min|max](int, symbol)` => `int [+|-] [min|max](int, symbol)`
As a result, `vector::empty` can be modelled to return a more precise value: `1 - min(1, size)`.
Reviewed By: mbouaziz
Differential Revision: D5899404
fbshipit-source-id: c8c3f49
Summary:
We take it into account to not report bugs inside the available block. This requires a plugin change.
update-submodule: facebook-clang-plugins
Reviewed By: jvillard
Differential Revision: D5891511
fbshipit-source-id: 21a02ad
Summary:
With this change and the previous facebook-clang-plugins change, infer no
longer exhausts the biniou buffer when reading the serialized C++ AST.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D5891081
fbshipit-source-id: cf48eac
Summary: Infer can then detect the resource leak when resources are stored into a container
Reviewed By: sblackshear
Differential Revision: D5887702
fbshipit-source-id: 6106cfb
Summary: The point of the tracing mode is to compute all the possible path leading to an error state. However, within a method, many of those paths are not feasibile in practice. This leads to many false alarms for the resource leak analysis.
Reviewed By: sblackshear
Differential Revision: D5888695
fbshipit-source-id: 2dbc57b
Summary: Model the `remove(...)` and the `clear()` method of `HashMap`.
Reviewed By: sblackshear
Differential Revision: D5887674
fbshipit-source-id: c3f40ee
Summary: Handling the utility functions for asserting that we're on background thread.
Reviewed By: jberdine
Differential Revision: D5863435
fbshipit-source-id: 3ad95b5
Summary:
Previously, we just tracked a boolean representing whether we were possibly on the main thread (true) or definitely not on the main thread (false).
In order to start supporting `Thread.start`, `Runnable.run`, etc., we'll need something more expressive.
This diff introduces a lattice:
```
Any
/ \
Main Background
\ /
Unknown
```
as the new threads domain. The initial value is `Unknown`, and we introduce `Main` in situations where we would have introduced `true` before.
This (mostly) preserves behavior: the main difference is that before code like
```
if (*) {
assertMainThread()
} else {
x.f = ...
}
```
would have recorded that the access to `x.f` was on the main thread, whereas now we'll say that it's on an unknown thread.
Reviewed By: peterogithub
Differential Revision: D5860256
fbshipit-source-id: efee330
Summary:
It's useful to be able to disable de-duplication on the command line with `--no-filtering`.
Gate de-duplication with `Config.filtering` and move the de-duplication tests to a new directory under the build systems tests.
Reviewed By: jeremydubreil
Differential Revision: D5865329
fbshipit-source-id: 5094f5b
Summary:
Since D5381239, infer is careful not to delete directories that do not "look
like" results directories on startup, in case the user passed, eg, `-o /`.
In our repo, lots of results dir are created by build/test of infer, and when
the version of infer changes and the expected contents of results directories
change then it might start refusing to delete the results directories created
with another version of infer.
Add an option to force infer to delete the results directory no matter how
dodgy it looks, and use it in our repo by adding the option in every
.inferconfig.
Reviewed By: mbouaziz
Differential Revision: D5870984
fbshipit-source-id: 09412de
Summary: Will then be easier to understand if some changes in the test results is legit or not.
Reviewed By: sblackshear
Differential Revision: D5863961
fbshipit-source-id: 7eb3f33
Summary:
Suggesting to add `_Nullable` on the fields checked for, or assigned to, `nullptr` will allow the biabduction analysis to report null dereferences that are related to the lifetime of objects.
Depends on D5832147
Reviewed By: sblackshear
Differential Revision: D5836538
fbshipit-source-id: c1b8e48
Summary: The prune nodes where translated as `prune (expr = false)` and `prune ( expr != false)`. This case is a bit tricky to deconstruct in HIL. This diff translates the prune instructions as just `prune !expr` for the true branch and `prune expr` for the false branch.
Reviewed By: dulmarod
Differential Revision: D5832147
fbshipit-source-id: 2c3502d
Summary:
We need to make sure that destructors of virtual base classes are called only once. Similarly to what clang does, we have two destructors for a class: a destructor wrapper and an inner destructor.
Destructor wrapper is called from outside, i.e., when variables go out of scope or when destructors of fields are being called.
Destructor wrappers have calls to inner destructors of all virtual base classes in the inheritance as their bodies.
Inner destructors have destructor bodies and calls to destructor wrappers of fields and inner destructors of non-virtual base classes.
Reviewed By: dulmarod
Differential Revision: D5834555
fbshipit-source-id: 51db238
Summary:
The "placement new" operator `new (e) T` constructs a `T` in the pre-allocated memory address `e`.
We weren't translating the `e` part, which was leading to false positives in the dead store analysis.
Reviewed By: dulmarod
Differential Revision: D5814191
fbshipit-source-id: 05c6fa9
Summary:
Simple instance of the problem: analyzing the following program times out.
```
#include <tuple>
void foo() {
std::tuple<std::tuple<int>> x;
}
```
Replacing `std::tuple<std::tuple<int>>` by `std::tuple<int>` makes the analysis
terminate.
In the AST, both tuple<tuple<int>> and tuple<int> have the same template
specialization type: "Pack" (which means we're supposed to go look into the
arguments of the template to get their values). This is not information enough
and that's the plugin fault.
On the backend side, this means that two types have the same Typ.Name.t, namely
"std::tuple<_>", so they collide in the tenv. The definition of
tuple<tuple<int>> is the one making it into the tenv. One of the fields of the
corresponding CxxRecord is of type "tuple<int>", which we see as the same
"tuple<_>", which causes the loop.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D5775840
fbshipit-source-id: 0528604
Summary:
Sort the complete set of warnings by everything except procname, then de-duplicate.
This scheme prevents reporting identical error messages on the same line/same file.
This is important for avoiding duplicate reports on multiple instantiations of the same template.
Reviewed By: jberdine
Differential Revision: D5819467
fbshipit-source-id: 984f47f
Summary: The resolution was previously only happening for constructors, but calls to private methods or to `super` are also neither static calls nor virtual calls. In this case, the resolution logic should be the same as for constructors.
Reviewed By: sblackshear
Differential Revision: D5830376
fbshipit-source-id: 9b56f80
Dulma Churchill
Jules Villard
Dino Distefano
Sam Blackshear
Mehdi Bouaziz
Jeremy Dubreil
Anders Papitto
Josh Berdine
Sungkeun Cho
Daiva Naudziuniene
Kyriakos Nikolaos Gkorogiannis