Summary: We have been referring to the arguments of a function call as "params". This has been bothering me. Let's fix it!
Reviewed By: ngorogiannis
Differential Revision: D27649158
fbshipit-source-id: 10e0b28cb
Summary:
To avoid too big abstract states due to instantiated templates in C++,
this diff loosens the compare functions of field names and ungated
callees.
Reviewed By: ezgicicek
Differential Revision: D27625775
fbshipit-source-id: e33e9d34c
Summary:
Nullsafe/biabduction tests were sensitive to Java version: they were recorded for Java 8 but if the machine that is used to run the tests had Java 11, tests would fail. This diff aims to resolve this issue by
- making our tests produce java8-compatible bytecode so that tests don't fail on Java 11 machines
- removing nullsafe tests that exercise obscure Java 8 behavior that cannot be alleviated with backward compatible bytecode on Java 11
- changing lambda argument printing to be Java 11 compatible
Reviewed By: martintrojer
Differential Revision: D27500731
fbshipit-source-id: 77fe302ea
Summary:
Reporting all ungated (un configed?) function calls causes many FPs. Instead, we rely on complexity analysis to determine whether a function is cheap/expensive: if the callee's complexity is not symbolic (e.g. constant), we consider it as cheap and don't keep track of it.
Note that we don't take the instantiated/modeled cost into account yet. So, if we have `foo(int n)` with complexity `O(n)`, and call it as `foo(3)`, we would still keep track of it. Similarly, if `foo` is a modeled function with constant time complexity, we would have no summary for it hence would keep track of it.
These will be improved later.
Reviewed By: skcho
Differential Revision: D27430485
fbshipit-source-id: d5f66320d
Summary:
This diff removes additional inferbo options `--bufferoverrun` from cost tests, since printing
inferbo issues is not that useful to understand cost results.
Reviewed By: ngorogiannis
Differential Revision: D27592496
fbshipit-source-id: 6ab3e6528
Summary:
Whenever an equality "t = v" (t an arbitrary term, v a variable) is
added (or "v = t"), remember the "t -> v" mapping after canonicalising t
and v. Use this to detect when two variables are equal to the same term:
`t = v` and `t = v'` now yields `v = v'` to be added to the equality
relation of variables. This increases the precision of the arithmetic
engine.
Interestingly, the impact on most code I've tried is:
1. mostly same perfs as before, if a bit slower (could be within noise)
2. slightly more (latent) bugs reported in absolute numbers
I would have expected it to be more expensive and yield fewer bugs (as
fewer false positives), but there could be second-order effects at play
here where we get more coverage. We definitely get more latent issues
due to dereferencing pointers after testing nullness, as can be seen in
the unit tests as well, which may alone explain (2).
There's some complexity when adding term equalities where the term
is linear, as we also need to add it to `linear_eqs` but `term_eqs` and
`linear_eqs` are interested in slightly different normal forms.
Reviewed By: skcho
Differential Revision: D27331336
fbshipit-source-id: 7314e127a
Summary:
It's better (=possibly more efficient) to take the opportunity to
normalize linear terms when we can instead of possibly having to apply
the same normalization over and over on individual terms until the next
round of proper normalization.
Reviewed By: skcho
Differential Revision: D27464885
fbshipit-source-id: 0dc01a089
Summary:
When we don't know the value being shifted it may help to translate
bit-shifting into multiplication by a constant as it might surface
linear terms, eg `x<<1` is `2*x`.
Reviewed By: skcho
Differential Revision: D27464847
fbshipit-source-id: 9b3b5f0d0
Summary:
The simplifications done by `simplify_shallow` are all taken care of by
`eval_const_shallow` as well, they just also happen to help when not
*all* of the term is a constant. However, they might be less
precise/efficient than in the constant case, in particular in the next
diff that translates `x << c` into `x * 2^c` when `c` is constant.
Reviewed By: skcho
Differential Revision: D27464805
fbshipit-source-id: 452bc6ab1
Summary:
On some pathological examples of crypto primitives like libsodium, later
diffs make pulse grind to a halt due to an explosion in the size of
literals. This is at least partly due to the fact the arithmetic doesn't
operate modulo 2^64.
Due to the fact the arithmetic is confused in any case when we reach
such large numbers, cap them, currently at 2^128. This removes pathological
cases for now, even now on libsodium Pulse is ~5 times faster than before!
Take this opportunity to put the modified Q/Z modules in the own files.
Reviewed By: jberdine
Differential Revision: D27463933
fbshipit-source-id: 342d941e2
Summary: Just some scaffolding to save a bit of churn from the next diff.
Reviewed By: skcho
Differential Revision: D27328348
fbshipit-source-id: 4f5bfcc65
Summary:
This was added in C++14. Was investigating how SIOF dealt with this but
it turns out it already does the right thing as the translation unit of
global variable templates shows up as the place they are instantiated
(not the one where they are declared), which works well for SIOF
checking.
Reviewed By: da319
Differential Revision: D27500998
fbshipit-source-id: b8b9b9c48
Summary:
This is better suited than the generic "cGeneral_utils", and saves
exporting one of them too.
Reviewed By: da319
Differential Revision: D27500933
fbshipit-source-id: f4224f63b
Summary: One source of non-deterministic diff result is when there are multiple overloaded methods the cardinals of unchecked callees of which are the same. This diff tries to select one of them in a more deterministic manner.
Reviewed By: ezgicicek, ngorogiannis
Differential Revision: D27430757
fbshipit-source-id: 38ba5d8dc
Summary: Error message was accidentally changed to a specific nullptr error message (D26887140 (cba144b779)) for any invalidation (use after delete, etc). This diff reverts back the error message for a general case and keeps the special case for nullptr dereference. Also fixed spacing for nullptr dereference error message.
Reviewed By: jvillard
Differential Revision: D27407628
fbshipit-source-id: 2649f3032
Summary:
The title
Also notice that there is a duplication of an error.
Reviewed By: skcho
Differential Revision: D27426933
fbshipit-source-id: dbd2f861a
Summary: Autogenerated methods sometimes lead to false positives. Also, clean up a little the models file.
Reviewed By: da319
Differential Revision: D27393933
fbshipit-source-id: f79b1a6eb
Summary: To support objc nil messaging for unknown function calls we prune `self` to be positive in the `normal` specification and add additional specification to handle nil case.
Reviewed By: skcho
Differential Revision: D27360757
fbshipit-source-id: 119999b30
Summary:
This addresses a test difference between java versions. Infer's java tests are recorded with Java8 where string concat with a constant string uses `toString`. However, if tests are run on a machine where Java 11 is used, string concat is done via `makeConcatWithConstants` which causes tests to fail.
As a workaround, we replace the test so that Java version dependent string concat is not used.
Reviewed By: ngorogiannis
Differential Revision: D27394621
fbshipit-source-id: dfe1af2ac
Summary:
Fixing `IsInstanceOf` term simplification for null case. Before, this
was only being done if value was known to be null at the moment of the
call to `instanceof`. Otherwise, the `IsInstanceOf` term would remain in
the formula unnecessarily.
Reviewed By: jvillard
Differential Revision: D27361025
fbshipit-source-id: 2d958a757
Summary:
Models for Java Map interface.
This consists of `Map.init()`, `Map.put(key, value)`, `Map.get(key)`,
`Map.containsKey(key)` and
`Map.isEmpty()`. With the exception of `Map.get(key)` and `Map.containsKey(key)`, these functions were modelled using the respective similar ones provided by the Java Collection interface.
Reviewed By: jvillard
Differential Revision: D27326716
fbshipit-source-id: e07f0c952
Summary:
This diff add semantics for collecting all object fields that may have config values. The collected information is used to instantiate conditional unchecked callees introduced in the previous diff.
How it works:
* The summary is extended to have `config_fields:Fields.t`. It has all fields that may have config values intra-procedurally.
* Before reporting to `config-impact-report.json`, it unions all `config_fields` from all specs.
* Using `all_config_fields`, it instantiates each summaries and writes results to `config-impact-report.json`.
Reviewed By: ezgicicek
Differential Revision: D27326306
fbshipit-source-id: 42f16ca45
Summary:
This diff extends domain and semantics to understand object fields that may have config values.
Now, `Summary.t` has one more field `unchecked_callees_conditional`, which is a map from a set of object fields to a set of callees. The meaning is that the callees are called depending of the fields, ie
* if one of field of the fields is known to be an actual config value, the callees are safely gated,
* otherwise, the callees are ungated.
For example,
```
void foo() {
if (mField1) {
if (mField2) {
callee1();
}
callee2();
}
}
```
`foo` will have `unchecked_callees_conditional` value of
```
{ {mField1,mField2} -> {callee1},
{mField1} -> {callee2} }
```
Later, if we know that `mField2` has a config value, we can say `callee1` is gated, or if we know that `mField1` has a config value, we can say `callee1` and `callee2` are gated.
The following diff will add an analysis that collects object fields that may have config values.
Reviewed By: ezgicicek
Differential Revision: D27325522
fbshipit-source-id: d4aff58cb
Summary:
Copied the documentation from a document created by rgrig
(thanks!!).
Reviewed By: rgrig
Differential Revision: D27325829
fbshipit-source-id: 118e1a2be
Summary:
The explicit marker for nondeterministic states was used to speed up the
shallow implementations of Topl, which ar enow removed.
Reviewed By: jvillard
Differential Revision: D27297019
fbshipit-source-id: 0fce93817
Summary:
refactoring Java Integer model so that it uses the new
API designed for manipulating fields in Java.
Reviewed By: jvillard
Differential Revision: D27231810
fbshipit-source-id: 0d9e3c951
Summary:
## Issue:
On `master`, it seems that there is a missing newline when Infer prints the `tenv` for a structure type:
```bash
avj@platypus /tmp/infer_bug$ cat test.c
typedef struct {
int a;
} st1;
typedef struct {
int b;
} st2;
avj@platypus /tmp/infer_bug$ infer --version
Infer version v1.0.0-55871dd28
Copyright 2009 - present Facebook. All Rights Reserved.
avj@platypus /tmp/infer_bug$ rm -rf infer-out && infer --debug run -P -- gcc -c test.c
Logs in /tmp/infer_bug/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /tmp/infer_bug/infer-out
No issues found
avj@platypus /tmp/infer_bug$ grep -A1 "dummy" infer-out/captured/*/*.tenv.debug
dummy: falsestruct st1
fields: {
--
dummy: falsestruct st2
fields: {
--
dummy: falsestruct objc_class
fields: {}
```
(notice that `dummy: false` and `struct objc_class` are on the same line, with no spacing)
## Resolution
Their PR adds an explicit newline at the end of pretty-printing a structured value, such that it is formatted correctly in the `tenv`:
```bash
avj@platypus /tmp/infer_bug$ infer --version
Infer version v1.1.0-bb5a33506
Copyright 2009 - present Facebook. All Rights Reserved.
avj@platypus /tmp/infer_bug$ rm -rf infer-out && infer --debug run -P -- gcc -c test.c
Logs in /tmp/infer_bug/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /tmp/infer_bug/infer-out
No issues found
avj@platypus /tmp/infer_bug$ grep -A1 "dummy" infer-out/captured/*/*.tenv.debug
dummy: false
struct st1
--
dummy: false
struct st2
--
dummy: false
struct objc_class
--
dummy: false
```
(*edit*: I forgot to build after committing; now with updated hash)
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
Pull Request resolved: https://github.com/facebook/infer/pull/1416
Reviewed By: skcho
Differential Revision: D27264518
Pulled By: jvillard
fbshipit-source-id: 3b86b4c22
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: This diff ignores java.lang.Math method calls since they are all cheap.
Reviewed By: ezgicicek
Differential Revision: D27267282
fbshipit-source-id: ad0a4ef4f
Summary:
There could still be divisions by zero, eg in the "mod" case: consider
"x mod (1/2)" (doesn't matter what x is). Then we'd check "1/2 =? 0" and
since it's false conclude that it's safe to take the modulo... oops!
To make things safer, harden `Z` to not throw anymore.
Also add a layer of defense in depth by wrapping the functions that do
Z/Q operations in another layer of exception catching because we really
don't want to crash the entire analysis due to that.
Reviewed By: martintrojer
Differential Revision: D27262569
fbshipit-source-id: e22187ca0
Summary:
Previously we would only simplify when the term is exactly IsInstanceOf,
and skip sub-terms. Most of the time this is the case but in the future
this could change.
Reviewed By: skcho
Differential Revision: D27156519
fbshipit-source-id: bd10574e0
Summary:
- some editing of the text
- the documentation of NULLPTR_DEREFERENCE was duplicated in
NULL_DEREFERENCE. Make the latter point to the former instead.
Reviewed By: skcho
Differential Revision: D27162785
fbshipit-source-id: 442d6efb9
Summary:
In Pulse, it usually havoc the actual parameters to unknown functions. However, it did not do that when the lengths of actuals and formals mismatch, which may happen when the frontend doesn't have enough information about procedures.
This diff havoc the actual parameters, also when there is mismatch between lengths of actuals and formals.
Reviewed By: ezgicicek
Differential Revision: D27163143
fbshipit-source-id: 1c5e0853a
Summary:
Two methods with identical method names but different number/type of args will have the same hash: e.g. `foo(int x)` and `foo(int x, int y)`. For Config Impact analysis, we assumed this type of hash collusion would never happen when we are comparing config-impact reports, but that assumption is wrong as demonstrated by the modified tests.
To deal with these, in cost analysis, we pick the highest degree among the potential collisions. We follow a similar idea here, picking the highest number of unchecked callees.
That has its own disadvantages:
E.g. giving an example from cost, if we had `foo(int x)` with O(1) before, and after the change, we have also added a linear `foo(int x, int y)`, I think we would introduce a complexity increase.
Still, it is better than picking only the first/last.
Reviewed By: skcho
Differential Revision: D27156722
fbshipit-source-id: c37388f1c
Summary:
10 seems better at no visible CPU cost. Not very scientific as this is
only one data point, but neither was choosing 5 in the first place.
Measurements on OpenSSL using Pulse.ISL:
```
$ time infer --pulse-only --scheduler callgraph -j 2 --pulse-report-latent-issues --pulse-isl
| fuel | user time (s) | under-normalisation | latent issues |
|------+---------------+---------------------+---------------|
| 5 | 163 | 3074 | 160 |
| 10 | 158 | 85 | 160 |
| 15 | 174 | 32 | 160 |
| 20 | 186 | 20 | 160 |
```
Reviewed By: skcho
Differential Revision: D27156497
fbshipit-source-id: 1114b8677
Summary:
This is a refactoring for a later change. This change alters behaviour
slightly to make it less chaotic: instead of normalization doing:
"""
do normalize(phi) until phi doesn't change anymore
normalize(phi):
do normalize_linear_part(phi) until this doesn't change phi anymore
do other normalizations
"""
we now do
"""
do normalize(phi) until phi doesn't change anymore
normalize(phi):
normalize_linear_part(phi)
do other normalizations if linear didn't change
"""
In particular we no longer spend potentially-quadratic amouns of fuel
during normalization.
Reviewed By: skcho
Differential Revision: D26450391
fbshipit-source-id: 9f63e1a04
Summary:
- add a pp_new_eq function to help people who want to printf-debug stuff
- fix one case where new_eqs were reset to `[]` instead of propagated
- do not add to `new_eqs` when nothing changes during normalisation.
This avoids duplicated new_eqs that arise from regenerating the linear
equality relation multiple times during normalisation.
Reviewed By: da319
Differential Revision: D27156042
fbshipit-source-id: 59b093ec8
Summary: To implement nil summaries for unknown calls I would like to reuse functionality from PulseObjectiveCSummary which already depends on PulseOperations causing circular dependencies.
Reviewed By: jvillard
Differential Revision: D27155092
fbshipit-source-id: 1c300ead0
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:
This first commit introduces test cases and the new summary type, in
particular how it is propagated during function calls. We don't yet
actually generate these summary types, this is for the next diff.
The goal is to catch this pattern:
```
foo(p) {
if(p) {}
*p = 42;
}
goo() { foo(NULL); }
```
We went foo(p) to be a latent error when p=0. Right now we detect a
contradiction p|->- * p=0 |- false. The next diff will fix it.
Reviewed By: skcho
Differential Revision: D26918552
fbshipit-source-id: 6614db17b
Summary: Mostly refactoring, get rid of some minor TODOs in the process.
Reviewed By: skcho
Differential Revision: D26916013
fbshipit-source-id: 53c34af05
Summary:
This is to avoid a circular dependency issue in the future when creating
summaries might cause new reports: PulseReport depends on
PulseExecuationDomain so the latter cannot emit reports. Move summary
creation functions to PulseSummary instead, which sits above both of
these modules.
Also limit the responsabilities of PulseLatentIssues to just latent
issues in preparation for another change.
Reviewed By: skcho
Differential Revision: D26915799
fbshipit-source-id: 3275cd514
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: "Please make sure this is an expected change." makes the reports longer. We already ask for feedback on whether it is expected or not at diff time.
Reviewed By: ngorogiannis
Differential Revision: D27009995
fbshipit-source-id: d1bc6e6b1
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:
This changes the results. I think it's because we cut short paths to
ISL errors sooner now, before they are duplicated and moved. I could not
really assess what was going on though so could be wrong.
On OpenSSL 1.0.2d:
Before: 106 issues
After: 90 issues
Reviewed By: ezgicicek
Differential Revision: D26822331
fbshipit-source-id: e861e7fc2
Summary:
This will enable further improvements: basically we want to be able to
abort the symbolic execution of a single disjunct whenever an error is
detected. Right now there is only one kind of error, which is now
explicitly called `ReportableError`.
The next diff refactors Pulse.ISL to add its own error type so that we
are able to get rid of the isl_status field (ISLOk/ISLError) inside
abductive states. ISLError states are really `Error _` states but
previously it would have been too much of an API change to expose that.
Now it's all going to be part of `AccessResult.t`.
A further change will add another error type for when a value is found
to be 0 after the fact by the arithmetic.
Reviewed By: ezgicicek
Differential Revision: D26821178
fbshipit-source-id: 2923db8e7
Summary:
It makes more sense to return a list of results than a result of lists:
the latter stops the execution on *all* the disjuncts that would have
been in the list as soon as *one* of them fails. This is the same issue
we solved for non-ISL pulse models earlier.
Reviewed By: skcho
Differential Revision: D26818409
fbshipit-source-id: 7cc1d8b39
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:
Only register biabduction-style timeouts the first time the function
exe_timeout is called. This avoid getting timeouts in other
long-running analyses. (Especially on windows, where the wall clock is
used.)
Pull Request resolved: https://github.com/facebook/infer/pull/1391
Reviewed By: skcho
Differential Revision: D26780445
Pulled By: jvillard
fbshipit-source-id: 19631b702
Summary:
gcc warnings are more strict starting from gcc10. Not having the const
qualifier triggers an error.
Pull Request resolved: https://github.com/facebook/infer/pull/1393
Reviewed By: skcho
Differential Revision: D26780417
Pulled By: jvillard
fbshipit-source-id: 4507c55eb
Summary:
It removed the result directory without check due to a bug. This diff fixes it to do the check and more careful removement of files.
* Before removing a result directory, it checks
* if the directory is empty: This is ok.
* if the directory is non-empty, but has `results.db`: This is ok, because the directory seems to be an infer's result directory.
* if the directory is non-empty and no `results.db`: This is not ok, so it does not remove the directory.
Reviewed By: jvillard
Differential Revision: D26635059
fbshipit-source-id: fa808265f
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:
Adapting existing model for `new` used in ObjC to Java.
This allows to compute dynamic type information and will facilitate
handling `instanceof`, for instance.
Changing attribute value type from Typ.Name.t to Typ.t to handle arrays.
Reviewed By: da319
Differential Revision: D26687839
fbshipit-source-id: 2cfcd0625
Summary:
Difficult to repro as most of the time other simplifactions catch this
before we actually get to dividing by zero. Nonetheless...
shamecube
Reviewed By: da319
Differential Revision: D26758187
fbshipit-source-id: b8718c515
Summary: Instead of accumulating all reports for a location in a list and then partitioning that list by issue type, just use a map from issue types to report lists.
Reviewed By: ezgicicek
Differential Revision: D26748929
fbshipit-source-id: 81c35cd4e
Summary: Now that all reports are deduplicated using the same criterion (trace length), use that to simplify deduplication functions.
Reviewed By: skcho
Differential Revision: D26726239
fbshipit-source-id: 77e3b319a
Summary:
A "severity" level was used for keeping the highest severity issue when deduplicating across many issues on the same location. This was used for only one of the issue types reported by the analysis.
It turned out this isn't very useful and it complicates significantly the reporting code.
This diff removes the type and uses trace depth to sort all the issue types in the same way all other issue types than `starvation` used.
Next diff will remove now unnecessary stuff.
Reviewed By: skcho
Differential Revision: D26725569
fbshipit-source-id: f9287dcd1
Summary:
The config impact checker prints ungated callees in a separate file config-impact-report.json,
because its results should be compared before actual reporting as the cost checker does.
Reviewed By: ezgicicek
Differential Revision: D26665097
fbshipit-source-id: 0c6e13403
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: This diff changes the compare function of `UncheckedCallee` not to distinguish direct/indirect call.
Reviewed By: ngorogiannis
Differential Revision: D26722968
fbshipit-source-id: f83f4de10
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:
In the following diff, we will add `JsonConfigImpactPrinter` that will share some common code base
with `JsonCostsPrinter`. This diff prepares the sharing.
Reviewed By: jvillard
Differential Revision: D26665070
fbshipit-source-id: 5032e0611
Summary:
In some corner cases where there are a lot of sequential statements, it raised stack overflow. To
avoid the issue, this diff changes the function as tail recursive by passing a callback function.
Reviewed By: ngorogiannis
Differential Revision: D26668338
fbshipit-source-id: 822d9a5f8
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:
As a first step to support the Java `instanceof`
operator, this change allows the path condition to be appended with
`IsInstanceOf(var, typ)`.
Reviewed By: jvillard
Differential Revision: D26664009
fbshipit-source-id: cd19dce83
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: If we record all callees with empty summary, we end up with FPs. This diff instead only records leaf calls. for non-leaf calls, we just load the summary.
Reviewed By: skcho
Differential Revision: D26606228
fbshipit-source-id: 77e76ee9e
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:
This diff makes the analysis inter-procedural.
* If a callee is called in a config check branch, it does nothing.
* if a callee is called outside config check branches,
* If callee's summary is empty, add the callee's name to the set of unchecked callees.
* If callee's summary is not empty, join the summary to the set of unchecked callees. (We intentionally don't add the callee's name here.)
Reviewed By: ezgicicek
Differential Revision: D26465235
fbshipit-source-id: ac3ad3543
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:
The impurity checker assumed that in pulse summary, all key addresses of PRE state should exist in
POST state. However, the assumption is not always true. For example,
```
void foo(int x) {
int y = x;
// HERE
}
```
At `HERE`, pulse's summary is
```
POST={
roots={ &x=v1 };
mem ={ v1 -> { * -> v4 } };
}
PRE={
roots={ &x=v1 };
mem ={ v1 -> { * -> v4 },
v4 -> { } };
}
```
The `v4` entry exists only at `PRE`. Although the `v4` entry is luckily removed in the summary by
the canonicalization in this example, basically there is no guarantee about the entry sets of PRE and POST.
Reviewed By: jvillard
Differential Revision: D26550338
fbshipit-source-id: 99a31cd43
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:
There should be no equalities relevant to the precondition to
canonicalize against in the first place: equalities come either from
assignments (hence strictly to the post condition) or from PRUNE
statements, and we don't use the latter to canonicalize states anyway.
Reviewed By: skcho
Differential Revision: D26488378
fbshipit-source-id: 7923f71ea
Summary:
This was a correctness issue as nothing guarantees that bindings are in
a specific order. The following commit violates that assumptions and
made the impurity tests fail without this change.
Reviewed By: ezgicicek
Differential Revision: D26488379
fbshipit-source-id: e9cc41147
Summary:
Pretty minor, it's more convenient to make it return the state and will
be used in a later diff when that function will actually sometimes
modify the state.
Reviewed By: skcho
Differential Revision: D26488376
fbshipit-source-id: a21eaf008
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
Ezgi Çiçek
Sungkeun Cho
Loc Le
Jules Villard
Artem Pianykh
Nikos Gorogiannis
Daiva Naudziuniene
Gabriela Cunha Sampaio
Radu Grigore
Andrew V. Jones
Mitya Lyubarskiy
Martin Trojer
Boris Yakobowski
Andrey Makeev
Daniel Schoepe
Adam Ernst
Joshua Selbo