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:
Changing model for Java `Collection` interface. Every collection has now two internal fields, initially set to `null`. We also keep an extra field to compute emptiness. This model was implemented based on the [preexisting model for HashMap](https://github.com/facebook/infer/blob/master/infer/models/java/src/java/util/HashMap.java).
Existing models (`add`, `remove`, `set` and `is_empty`) have been updated accordingly and new models are provided: `init` and `clear`.
This model is not yet compatible with the `Map` interface but this change will happen very soon.
Reviewed By: ezgicicek
Differential Revision: D27126815
fbshipit-source-id: 79a5fe306
Summary:
See updated tests and code comments: this changes many arithmetic
operations to detect when a contradiction "p|->- * p=0" is about to be
detected, and generate a latent issue instead. It's hacky but it does
what we want. Many APIs change because of this so there's some code
churn but the overall end result is not much worse thanks to monadic
operators.
Reviewed By: skcho
Differential Revision: D26918553
fbshipit-source-id: da2abc652
Summary: Although `Set.contains` could be logarithmic in the worst case, on average, the contains() runs in O(1) time. We rather take the average here, following the most common case.
Reviewed By: ngorogiannis
Differential Revision: D27078794
fbshipit-source-id: 24e3476e8
Summary:
`Initializer` annotation is an advanced feature that should be used
sparingly. Let's remove it from the error message and hence discourage
overuse
Reviewed By: ngorogiannis
Differential Revision: D27047431
fbshipit-source-id: 8eb7ba7ab
Summary: The translation of captured by reference variables has been fixed for ObjC blocks (D26945575 (778c629401)), so we do not need to ignore them in uninit analysis anymore.
Reviewed By: skcho
Differential Revision: D27063663
fbshipit-source-id: 447084d37
Summary:
This diff handles live variables in catch blocks. To do that, this diff adds another metadata,
`CatchEntry`.
Domain change: The domain is changed to
```
(normal:variables) x (exn:try_id->variables)
```
`exn` is a map from try-catch-id to a set of live variables that are live at the corresponding entry
of catch blocks.
Semantics change: It is a backward analysis.
* on `CatchEntry`: It updates `exn` with `try_id` and current `normal`.
* on `Call`: As of now, we assume all function calls can raise an exception. Therefore, it copies
all live variables in `exn` to `normal`.
* on `TryEntry`: It removes corresponding `try_id` from `exn`.
Reviewed By: jvillard
Differential Revision: D26952755
fbshipit-source-id: 1da854a89
Summary: This diff adds TryEntry and TryExit statements to the entry and exit of C++ `try` block, in order to handle exceptional control flow better in analyses.
Reviewed By: da319, jvillard
Differential Revision: D26946188
fbshipit-source-id: 33f4ae9e7
Summary:
Update Infer to LLVM (clang) 11.1.0.
Infer/clang now uses the LLVM 'monorepo' release, simplifying the download script.
Some changes done to how/when ASTExporter mangles names, this to avoid the
plugin hitting asserts in the clang code when mangling names.
Reviewed By: jvillard
Differential Revision: D27006986
fbshipit-source-id: 4d4b6ba05
Summary:
We use `procedure_name` which is coming from `Procname.get_method` in explanation of cost issues. For blocks, procedure name includes a prefix `objc_block` and a suffix with `_x` where x is the block counter. However, displaying this name to the user is not pretty. Especially when we have nested blocks, procedure name looks like `objc_blockobjc_blockdirectUIMessageFromContentAndMetadata_10_23`.
This diff drops the block index suffix and replaces `objc_block` with a prettier version `^`(signifying block).
so instead, in the cost report, we will have `^^blockdirectUIMessageFromContentAndMetadata`.
Reviewed By: skcho
Differential Revision: D26945333
fbshipit-source-id: 9d135423c
Summary: Variables captured by reference do not have correct type in objc blocks. They are missing one reference. This diff sets the correct type of captured reference variables inside procdesc, similarly as we already have for cpp lambdas. The translation of block's body will then take into account the type of captured variable from procdesc.
Reviewed By: ezgicicek
Differential Revision: D26945575
fbshipit-source-id: 06a9d9cc6
Summary: This diff adds a test replicating the issue fixed in D26975222 (7110c1ca3f) in [commit 7110c1c](7110c1ca3f)
Reviewed By: ngorogiannis
Differential Revision: D26978562
fbshipit-source-id: 41e41df8c
Summary: We shouldn't report a complexity increase here because `existing_block_here` is a removed function (that doesn't exist in current version)!
Reviewed By: skcho
Differential Revision: D26947439
fbshipit-source-id: 6620804be
Summary: Adding option to suppress errors involving unknown code. If `--pulse-report-ignore-unknown-java-methods-patterns` is provided, reports containing skipped functions not matching at least one of the given regexps are suppressed.
Reviewed By: jvillard
Differential Revision: D26820575
fbshipit-source-id: b6e1df7b2
Summary:
Adapting error messages in Pulse so that they become more intuitive for
developers.
Reviewed By: jvillard
Differential Revision: D26887140
fbshipit-source-id: 896970ba2
Summary:
RacerD needs to analyse the class initialiser in order to establish field properties in its post, such as that certain static fields are synchronized containers.
There was a bug where class initializers were not analysed at all, from the time where there was no analysis of field properties in the post.
We still don't want to report on the class initialiser since it cannot possibly race with itself (JVM guarantees that) and it cannot race with any of the other methods in its class (because it must finish before any other method can be called).
Reviewed By: da319
Differential Revision: D26887151
fbshipit-source-id: 570aff370
Summary: The `NonBlocking` annotation should zero out all domain elements that represent blocking calls. The current implementation only really removes such elements when they are generated by the current method under analysis, leaving such elements from callees unaffected. This diff fixes that.
Reviewed By: jvillard
Differential Revision: D26874704
fbshipit-source-id: 2d4859b30
Summary: In ObjC, when a method is called on nil, there is no NPE, the method is actually not called and the return value is 0/false/nil. There is an exception in the case where the return type is non-POD. In that case it's UB and we want to report an error.
Reviewed By: jvillard
Differential Revision: D26815687
fbshipit-source-id: 8126414ab
Summary: We were missing a part of the trace if it was going through a nil summary as the invalidation was set in the nil summary. Instead of creating a fresh value for return in the nil summary {self=0}{return=0}, we return self {self=0}{return=self}. This way we keep all the information about invalidation in the trace.
Reviewed By: jvillard
Differential Revision: D26871098
fbshipit-source-id: 6eb175e68
Summary:
Providing model for the android function TextUtils.isEmpty(). For now,
this always returns false assuming that the given value is not null.
Reviewed By: jvillard
Differential Revision: D26779619
fbshipit-source-id: 3d8e26813
Summary: Adding support for the Java instanceof operator in Pulse.
Reviewed By: jvillard
Differential Revision: D26275046
fbshipit-source-id: 8ba608cca
Summary:
This diff runs `infer reportdiff` on config impact results, ie previous and current
`config-impact-report.json`s. Ungated and added/removed callees are reported at `introduced.json`.
Reviewed By: ezgicicek
Differential Revision: D26723054
fbshipit-source-id: efabd0d5f
Summary: Adding temporary model for Collections/Map isEmpty() as an attempt to reduce false positives before we provide a full model for Collections.
Reviewed By: ezgicicek
Differential Revision: D26724085
fbshipit-source-id: d3418c173
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:
The javax.crypto.Mac classes behaves like a container
and can lead to race conditions when used in a concurrent context.
This adds Mac operations as container writes/reads in RacerD's models.
Pull Request resolved: https://github.com/facebook/infer/pull/1395
Test Plan: CI
Reviewed By: skcho
Differential Revision: D26722737
Pulled By: ngorogiannis
fbshipit-source-id: 74f03e9a5
Summary: When a method is called in ObjC on nil, there is no NPE, the method is actually not called and the return value is 0/false/nil. (There is an exception in the case where the return type is non-POD. In that case it's UB. This will be addressed later). To implement this behaviour we add additional summary to ObjC instance methods {self = 0} {return = 0}. We also want to make sure that inferred summary will not be used in we call a method on nil, hence, we add a path condition {self > 0} to get a contradiction when needed.
Reviewed By: jvillard
Differential Revision: D26664187
fbshipit-source-id: cdac2a5bb
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:
See added tests. Passing a variable by reference to a function `foo` can
cause the variable to be added to the global state so any stores after
that might be live as long as there is another function call after the
store (since the global state shouldn't outlive the scope of the
function). Currently we don't check that the latter is true; to report
these we would need to extend the abstract domain to remember which
stores have been made without a subsequent call.
Also change Blacklisted -> Dangerous everywhere since the corresponding
option is called "liveness_dangerous_classes".
Reviewed By: skcho
Differential Revision: D26606151
fbshipit-source-id: e869e5df1
Summary:
Providing model for Java `instanceof` operator that
avoids to return true when given object is null. This is a temporary
solution that will reduce FPs while we do not provide the correct
semantics for `instanceof`.
Reviewed By: jvillard
Differential Revision: D26608043
fbshipit-source-id: 87c82b906
Summary: This diff finds a declared variable name or declared field names from trace, then constructs an error message including access paths.
Reviewed By: jvillard
Differential Revision: D26544275
fbshipit-source-id: 135c90a1b
Summary:
`add_edge_on_src` is to prepare a stack location for a local variable. Before this diff, it was
called several times for each fields.
Reviewed By: jvillard
Differential Revision: D26543715
fbshipit-source-id: 49ebf2b65
Summary:
This resolves a few instances of false negatives; typically:
```
if (x == y) {
// HERE
*x = 10;
*y = 44;
// THERE
}
```
We used to get
```
HERE: &x->v * &y ->v' * v == v'
THERE: &x->v * &y ->v' * v == v' * v |-> 10 * v' |-> 44
```
The state at THERE was thus inconsistent and detected as such (v` and
`v'` are allocated separately in the heap hence cannot be equal).
Now we normalize the state more eagerly and so we get:
```
HERE: &x->v * &y->v
THERE: &x->v * &y->v * v |-> 44
```
Reviewed By: skcho
Differential Revision: D26488377
fbshipit-source-id: 568e685f0
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:
These were present for `std::optional` but not `folly::Optional` for
some reason.
Reviewed By: da319
Differential Revision: D26450400
fbshipit-source-id: 45051e828
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:
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
Jules Villard
Gabriela Cunha Sampaio
Ezgi Çiçek
Mitya Lyubarskiy
Daiva Naudziuniene
Sungkeun Cho
Martin Trojer
Nikos Gorogiannis
Daniel Schoepe
Adam Ernst