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:
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: 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:
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: 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:
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:
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: 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:
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:
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: Destroying local variables that are out of scope after `continue`.
Reviewed By: jberdine
Differential Revision: D5804120
fbshipit-source-id: 638cff5
Summary: Destroying local variables that are out of scope after `break`.
Reviewed By: jberdine
Differential Revision: D5764647
fbshipit-source-id: a7e06ae
Summary: The successor node of `continue` was not correct inside the `do while`.
Reviewed By: sblackshear
Differential Revision: D5769578
fbshipit-source-id: d7b0843
Summary:
We supported globals as sources before, but we did so by allowing ClangTrace etc. to match against any access path in the footprint of the trace.
This is very powerful/flexible, but it's ultimately not a good idea because it leads to traces that are hard to read.
This is because a footprint source doesn't have any information about its provenance: we might know that the value came from a global, but we don't know where the read occurred.
The mechanism for handling procedure calls as sources already knows how to solve this problem.
This diff implements globals as sources as a special case of procedure call sources instead.
This will give us much nicer traces with full provenance of the read from the global.
Reviewed By: mbouaziz
Differential Revision: D5772299
fbshipit-source-id: 491ae81
Summary:
When a lambda has an `auto` parameter, the inferred type of the parameter because part of the name.
Our heuristic for identifying lambda was checking if the lambda's name was exactly `operator()`, which won't catch this case.
Reviewed By: jvillard
Differential Revision: D5753323
fbshipit-source-id: 85ff75a
Summary:
Not translating these properly was causing false positives for the dead store analysis in cases like
```
int i = 0;
return [j = i]() { return j; }();
```
Reviewed By: da319
Differential Revision: D5731562
fbshipit-source-id: ae79ac8
Summary: We inject destructor calls of base classes inside destructor bodies after the destructor calls of fields.
Reviewed By: dulmarod
Differential Revision: D5745499
fbshipit-source-id: 90745ec
Summary: We used to crash whenever we hit these. The simple translation implemented here is not particularly inspiring, but it is better than crashing.
Reviewed By: jvillard
Differential Revision: D5702095
fbshipit-source-id: 3795d43
Summary: This makes the traces more readable when involving skipped functions.
Reviewed By: sblackshear
Differential Revision: D5731683
fbshipit-source-id: 49d363b
Summary:
In looking at summaries that Quandary took a long time to compute, one thing I notice frequently is redundancy in the footprint sources (e.g., I might see `Footprint(x), Footprint(x.f), Footprint(x*)`).
`sudo perf top` indicates that joining big sets of sources is a major performance bottleneck, and a large number of footprint sources is surely a big part of this (since we expect the number of non-footprint sources to be small).
This diff addresses the redundancy issue by using a more complex representation for a set of sources. The "known" sources are still in a set, but the footprint sources are now represented as a set of access paths (via an access trie).
The access path trie is a minimal representation of a set of access paths, so it would represent the example above as a simple `x*`.
This should make join/widen/<= faster and improve performance
Reviewed By: jberdine
Differential Revision: D5663980
fbshipit-source-id: 9fb66f8
Summary:
The previous widening operator added stars to the *end* of paths that existed in `next` but not `prev`. This is not enough to ensure termination in the case where the trie is growing both deeper and wider at the same time.
The newly added test demonstrates this issue. In the code, there's an ever-growing path of the form `tmp.prev.next.prev.next...` that wasn't summarized by the previous widening operator. The new widening is much more aggressive: it replaces *any* node present in `next` but not `prev` with a `*` (rather than trying to tack a star onto the end). This fixes the issue.
This issue was causing divergence on tricky doubly-linked list code in prod.
Reviewed By: jeremydubreil
Differential Revision: D5665719
fbshipit-source-id: 1310a92
Summary:
This makes it easier to test a single checker.
Also refactor the code to make it harder to mess up the list of default/all checkers.
Reviewed By: sblackshear
Differential Revision: D5583209
fbshipit-source-id: 7c919b2
Summary:
Previous version was hard to understand because it was doing many things within same code. New version has different code for Arrays, Structs and others.
There is some copy-paste, but it's easier to follow code (open to suggestions though)
Reviewed By: dulmarod
Differential Revision: D5547999
fbshipit-source-id: 77ecb24
Summary: It wasn't using code from `std::vector::empty` which recently was improved. Instead of inlining `std::vector::empty`, call it to know whether vector is empty or not.
Reviewed By: jvillard
Differential Revision: D5573379
fbshipit-source-id: e024a42
Summary: Useful for identifying user-controlled array accesses that could lead to buffer overflows
Reviewed By: mbouaziz
Differential Revision: D5520985
fbshipit-source-id: 92984f6
Summary:
With current model, there are issues with cxx range loop. It looks like
it comes from std::vector::size model.
example of such FP:
```
int t = vec.size();
for(auto& elem : vec) {
auto x = elem
}
```
Reviewed By: jvillard
Differential Revision: D5545914
fbshipit-source-id: fbe55b3
Summary: Those are not particularly relevant for the biabduction analysis. It would be easy to have a dedicated checker for this if we happen to need one day.
Reviewed By: sblackshear
Differential Revision: D5530834
fbshipit-source-id: 316e60f
Summary:
Bumps facebook-clang-plugins to a version that outputs sizeof() info in bytes and not bits.
update-submodule: facebook-clang-plugins
Reviewed By: akotulski
Differential Revision: D5526747
fbshipit-source-id: 6019542
Summary: The `--failures-allowed` was doing for the Clang frontend what `--keep-doing` was doing for the backend. This revision merges the two options to simplify the Infer CLI and our tests.
Reviewed By: jvillard
Differential Revision: D5474347
fbshipit-source-id: 09bcea4
Summary:
update-submodule: facebook-clang-plugins
Moving to a newer version of clang, see ffb5dd0114
Reviewed By: jvillard
Differential Revision: D5452529
fbshipit-source-id: 28bc215
Summary:
Pretty basic: warn when we see an assignment instruction `x = ...` and `x` is not live in the post of the instruction.
Only enabled for Clang at the moment because linters already warn on this for Java. But we can enable it later if we want to (should be fully generic).
Reviewed By: jeremydubreil
Differential Revision: D5450439
fbshipit-source-id: 693514c
Summary:
This commit avoids precision loss on pruning.
// x -> [s$1, s$2]
if(x) { ... }
// x -> ?
before: x -> [min(0, s$1), max(0, s$2)]
because two x values, [0, 0] (true case) and [s$1, s$2] (false case), were joined after the if branch.
after: x -> [s$1, s$2]
Reviewed By: mbouaziz
Differential Revision: D5431009
fbshipit-source-id: 14a9efe
Summary:
Problem: The analyzer did not know that the value of `v.size()` is an alias of `v.infer_size`, so `v.infer_size` is not pruned by the if condition. As a result it raises a false alarm.
void safe_access(std::vector<int> v) {
if (v.size() >= 10) {
v[9] = 1; // error: BUFFER_OVERRUN Offset: [9, 9] Size: [5, 5]
}
}
void call_safe_access_Good() {
std::vector<int> v(5, 0);
safe_access(v);
}
Solution: Adding alias for return value to the abstract domain.
Now Inferbo can prune `v.infer_size` because it knows that the value of `v.size()` is an alias of `v.infer_size`. There is already an alias domain in Inferbo, so we added a specific room for the retrun value.
Reviewed By: jvillard, mbouaziz
Differential Revision: D5396988
fbshipit-source-id: 4a4702c
Summary:
:
because otherwise people would believe they can use the internal representation of these std lib but it fails for our models.
Reviewed By: jvillard
Differential Revision: D5368671
fbshipit-source-id: 4e53d5a
Summary:
:
Get rid of model location in reports.
The goal is to avoid changing `issues.exp` whenever a model is updated.
Reviewed By: jvillard
Differential Revision: D5356608
fbshipit-source-id: 88ecaba
Summary:
Indexing into a string literal expression would generate a fresh
variable on every application of a transformer. This violated
finiteness of the domain, and caused divergence.
Reviewed By: da319
Differential Revision: D5342951
fbshipit-source-id: e95e84e
Jeremy Dubreil
Sam Blackshear
Josh Berdine
Jules Villard
Dulma Churchill
Dino Distefano
Sungkeun Cho
Daiva Naudziuniene
Mehdi Bouaziz
Kyriakos Nikolaos Gkorogiannis
Jia Chen
Andrzej Kotulski
Martino Luca
Kihong Heo