Summary:
Instead of recording some facts as "known" (i.e., observed assignments),
record them as "pruned". This should be done any time the fact is not an
assignment, for instance when path-splitting on "is the argument =0?" as
in the model of `free()`.
Reviewed By: ezgicicek
Differential Revision: D26450362
fbshipit-source-id: 4fc980f90
Summary:
Using more than the "known" part of the arithmetic could accidentally
leak "pruned" information into certain facts.
I noticed this when adding more term equality reasoning to pulse in
another diff. At the moment this has little effect but is still more
correct conceptually.
Reviewed By: ezgicicek
Differential Revision: D26450333
fbshipit-source-id: eb31da344
Summary:
These were present for `std::optional` but not `folly::Optional` for
some reason.
Reviewed By: da319
Differential Revision: D26450400
fbshipit-source-id: 45051e828
Summary:
ClangWrapper.ml was skipping clang commands that didn't capture
by default. It was using the 'skip_analysis_in_path_skips_compilation'
flag to NOT skip commands. This is a confusing use of that flag.
Default should be to run clang (in case it does something useful),
and a new flag to disable this.
Reviewed By: ngorogiannis
Differential Revision: D26459100
fbshipit-source-id: 7f2e9a269
Summary: In Objective-C, `static const int var = ..` is not recognized as ICE (integral constant expression) unlike C++. To handle such loads better, this diff adds a check for `constant_global_array` as a workaround.
Reviewed By: skcho
Differential Revision: D26369461
fbshipit-source-id: e2dae11f1
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: As there are no dependencies between procedure and file analyses in RacerD, split them into separate modules.
Reviewed By: ezgicicek
Differential Revision: D26198874
fbshipit-source-id: 032aad9d8
Summary:
The `--pulse-model-return-nonnull` config option currently works for C++. Now we
will be using it also for Java. Changing type from string list to regexp to
make it more general.
Reviewed By: ezgicicek
Differential Revision: D26367888
fbshipit-source-id: 9a06b9b32
Summary:
Modeling Java instanceof operator in Pulse. This
implementation does not yet provide the proper semantics for instanceof.
For now, it will always return true. This is temporary and should reduce the false positive rate.
Reviewed By: da319
Differential Revision: D26317089
fbshipit-source-id: 494e3dec5
Summary: D25952894 (1bce54aaf3) changes translation of struct assignments. This diff adopts to this change for loads from global struct arrays.
Reviewed By: skcho
Differential Revision: D26398627
fbshipit-source-id: cc1fb47ab
Summary:
Before this diff:
```
// Summary of const global
// { global -> v }
n$0 =* global
// n$0 -> {global}
x *= n$0
// x -> {global}
```
However, this is incorrect because we expect `x` have `v` instead of the abstract location of `global`.
To fix the issue, this diff lookups the initializer summary when `global` is evaluated as RHS of load statement.
After this diff:
```
// Summary of const global
// { global -> v }
n$0 =* global
// n$0 -> v
x *= n$0
// x -> v
```
Reviewed By: ezgicicek
Differential Revision: D26369645
fbshipit-source-id: 98b1ed085
Summary:
Sometimes purity running failed because it couldn't find inferbo mem. Let's make it print a warning
message, instead of raising an exception.
Reviewed By: ezgicicek
Differential Revision: D26367275
fbshipit-source-id: d2350e855
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:
This diff resets the id generator before generating ObjC getter/setter, so parsed results are the
same without regard to the generation order. Note that the order may change when we change the type
of Procname.t since their hash values are used for the hash set of procnames.
Reviewed By: ngorogiannis
Differential Revision: D26277348
fbshipit-source-id: a66d77845
Summary:
We are getting lots of FPs due to modeling `Provider.get` as expensive. This is coming from Dependency Injection and Infer cannot statically determine the type of the provider and determine whether that provider is expensive (requires a global analysis and instrumentation).
Instead, we are downgrading this method to the default constant cost.
Reviewed By: skcho
Differential Revision: D26223978
fbshipit-source-id: 79f81c997
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: Added some basic examples for Objective-C we want to address next in pulse nullptr dereference analysis. In particular, we should not get a `nil` dereference error when we call a method on `nil`, except if the method returns a non-POD (Plain Old Data) type.
Reviewed By: ezgicicek
Differential Revision: D26053402
fbshipit-source-id: 66f4600c3
Summary:
**Existing heuristic**: If we have a call `foo(n)` that has no model and summary for `foo`, we underestimate its cost as constant[1].
However, if we have a model for `foo` (e.g.with modeled cost O(n)) but applying the model to arguments causes the cost to be Top (e.g if `n` has Top size), then we could have Top-poisoning where all the callers up the call chain will have Top costs [2].
To prevent these unintended Top-poisioning when adding models, this diff applies *the same heuristic* to modeled calls with Top cost and gives them constant cost. This way, when adding models, we wouldn't be introducing more Tops than if we were to have no models in the first place.
[1] This is problematic in itself and causes many FPs at diff time, but otherwise we would be getting Tops everywhere and would not be able to give any meaningful cost. E.g. for fblite, if we were to give unknown calls Top cost, #procedures with Top cost increases form 5% to 38% and #procedures with linear cost reduces by 99.75%.
[2] This was observed for `containsValue` for Instagram where %Tops increased by 88% :(
Reviewed By: skcho
Differential Revision: D26174644
fbshipit-source-id: 232354923
Summary:
In practice, it is not easy to mark all of NOT initialized elements of array, so let's ignore the
array value at the moment.
Reviewed By: jvillard
Differential Revision: D25372449
fbshipit-source-id: 02b2e217c
Summary:
Having different behaviours inter-procedurally and intra-procedurally
sounds like a bad design in retrospect. The model of free() should not
depend on whether we currently know the value is not null as that means
some specs are missing from the summary.
Reviewed By: skcho
Differential Revision: D26019712
fbshipit-source-id: 1ac4316a5
Summary:
Change most `t list access_result` to `t access_result list` so that the
Ok/Error is individual to each result in the list instead of having only
a toplevel Ok/Error affecting the whole list.
To make it not horrible to write this introduces new "monadic" operators
`let<*>` and `let<+>`. They are not entirely satisfactory but perhaps
it's just a notation issue as they are not quite bind/map operators
unlike what their notation might suggest. I'd say good enough for now.
The type change induced quite the churn but the new operators simplify
the code overall.
Reviewed By: skcho
Differential Revision: D26150505
fbshipit-source-id: 33764fae3
Summary:
Wrap the TOPL post-processing in the exit node debug wrapper too so that
we can see what it's doing if needed.
Reviewed By: skcho
Differential Revision: D26174365
fbshipit-source-id: dd63905ff
Summary:
When a union type has a member function in C++, it is parsed as `CppClass`. However, sometimes we may want
to distinguish normal cpp classes and union classes. This diff adds a field to the type name.
Reviewed By: jvillard
Differential Revision: D26125619
fbshipit-source-id: 44a6e8192
Summary:
When a single field struct is initialized with "type x{v}" form, the translated result is not straightforward. For example,
```
struct t {
int val_;
};
void foo(t x) {
t y{x};
}
```
calls the copy constructor with `x`. This is good.
```
void foo(int n) {
t y{n};
}
```
assigns the integer `n` to `y.val_`. This is good.
```
t get_v();
void foo() {
t y{get_v()};
}
```
assigns return value of `get_v` to `y.val_`, rather than calling the copy constructor. This is not
good, but doesn't matter for actual running; `&y.val_` is the same to `&y` and `t` value is the same
to `int` value.
Reviewed By: jvillard
Differential Revision: D26146578
fbshipit-source-id: 8a81bb1db
Summary:
The test compiled with warnings, not sure how to prevent this in the
future as `infer` will suppress all warnings anyway (I wanted to add
`-Werror` to the test Makefile but that was defeated by infer itself).
Reviewed By: ezgicicek
Differential Revision: D26019682
fbshipit-source-id: d7f8fc2d8
Summary:
providing models for the checkState and checkArgument
functions, both used in Java code.
Reviewed By: da319
Differential Revision: D26101726
fbshipit-source-id: 0cc73d252
Summary:
States would be considered equal when they describe the same heap shape
even though their path conditions were different. Not good.
Reviewed By: skcho
Differential Revision: D26022135
fbshipit-source-id: 510913cde
Summary:
This is all dead code but I had to do this to try something else and I
don't want to have to do that again :)
Reviewed By: skcho
Differential Revision: D26022111
fbshipit-source-id: 622ca10b9
Summary:
It is better for the derived comparison functions to start by comparing
the single offset `Q.t` instead of the map. The order of the pair
doesn't matter so the easiest way to achieve that is by putting the
offset first.
Reviewed By: skcho
Differential Revision: D26022080
fbshipit-source-id: 874ea5c66
Summary:
It's a potentially expensive operation given that it does graph
isomorphism twice on equal values so add a fast path for when they are
the same pointer. Also comparing "skipped calls" doesn't need to care
about traces.
Reviewed By: da319
Differential Revision: D26022022
fbshipit-source-id: 8178df37b
Summary: This diff fixes incorrect order of statements on `*p = !b;`.
Reviewed By: jvillard
Differential Revision: D26125069
fbshipit-source-id: 9dcefbd34
Summary:
Now that the buck java flavour is fully deployed, the genrule-based integrations for java can be removed. We also remove the combined (clang+java) integration as this will be reimplemented using flavours in the future.
Also, remove a bunch of deprecated arguments linked to these integrations.
Reviewed By: jvillard
Differential Revision: D26104384
fbshipit-source-id: 6b0059407
Summary: Creating model for the checkNotNull function from the Preconditions class in Pulse (Java). Whenever `checkNotNull(x)` is called, Pulse will assume that `x!= null`.
Reviewed By: ezgicicek
Differential Revision: D26075176
fbshipit-source-id: 40dcd395b
Summary:
This diff fixes incorrect order of statements on assignments.
In the translation of `LHS=RHS;`, if `RHS` is a complicated expression that introduced new nodes, eg a conditional expression, some load statements for `LHS` came after its usage. To avoid the issue, this diff forces it to introduce new nodes for `LHS`.
Reviewed By: jvillard
Differential Revision: D26099782
fbshipit-source-id: 27417cd99
Summary: This diff adds an additional parameter of struct return type in ObjC's methods. The additional parameter had been supported only in C/C++ functions/methods for 5 years (D2865091 (ec80d40bdd)). If there is no specific reason not to do that, let's do it and fix the incorrect frontend translations.
Reviewed By: jvillard
Differential Revision: D26049748
fbshipit-source-id: 414b3011f
Summary: In `ClosureSubstSpecializedMethod`, it duplicates a procedure with specialized closure parameters. Since it introduces a new procedure name, its local variables in the procedure body must be replaced to use the new procedure name. (Note that local variable type includes procedure name.) However, in the previous implementation, it missed the translations in some cases: compound expressions and metadata.
Reviewed By: ezgicicek
Differential Revision: D26075490
fbshipit-source-id: 2a5a30cd8
Adam Ernst
Jules Villard
Martin Trojer
Ezgi Çiçek
Nikos Gorogiannis
Gabriela Cunha Sampaio
Joshua Selbo
Loc Le
Sungkeun Cho
Xiaoyu Liu
Daiva Naudziuniene