Summary:
It's useful to test that the bucket a given error is classified as doesn't
change over time without notice.
This records the bucket for *all* the tests, even though some never produce a
bucket. This is to be on the safe size instead of risking to forget adding the
bucket information when the test changes, or when copy/pasting from a test that
doesn't have buckets to one that does.
The implementation is pretty crude: it greps the beginning of the qualifier
string for a `[bucket]`.
Reviewed By: mbouaziz
Differential Revision: D8236393
fbshipit-source-id: b3b1eb9
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
There can be multiple reports per line, especially when calling in a method which has itself multiple reports.
When reporting at the callsite, report only the issue with the highest severity (picked manually per type of event).
Deadlocks are not de-duplicated, as they are relatively rare and the info in mupltiple reports may be important.
Reviewed By: mbouaziz
Differential Revision: D8160940
fbshipit-source-id: ea6a5c0
Summary:
Moving away from C++ include-based models means that we cannot reliably detect
anymore whether a file includes <iostream> or not. In order not to be too
spammy, let's always assume standard streams are initialized for now when the
include models are off.
Recent versions of libstdc++ make these models redundant so there is hope that in a
bright future the analysis of std streams initialisation will work correctly without infer
having to have its own models anyway.
Reviewed By: mbouaziz
Differential Revision: D8043467
fbshipit-source-id: d118043
Summary: Set arguments of pointer type as initialised for indirect function calls.
Reviewed By: mbouaziz
Differential Revision: D8097895
fbshipit-source-id: 830f568
Summary: Track and surface the reasons why a method is assessed to run on the UI thread.
Reviewed By: mbouaziz
Differential Revision: D8096099
fbshipit-source-id: 2403c6c
Summary:
The reported location was always the start of the enclosing procedure, which is wrong in many ways.
A nice side-effect is that some code can then be eliminated and Ondemand.analyze used, avoiding getting the procdescs in the process.
Reviewed By: jeremydubreil
Differential Revision: D8056306
fbshipit-source-id: 67c2c8d
Summary: Treat array accesses as initialised if they are passed by reference.
Reviewed By: jvillard
Differential Revision: D8071247
fbshipit-source-id: 5480e90
Summary: Use AccessExpressions instead of AccessPath in uninit analysis. This will allow us to distinguish between pointers and their dereferences.
Reviewed By: jvillard
Differential Revision: D8042359
fbshipit-source-id: 604bcbc
Summary:
It improves the precision of widening operations of interval:
upper_bound_widen (min(n, s), s) = s
lower_bound_widen (max(n, s), s) = s
Reviewed By: mbouaziz
Differential Revision: D8038941
fbshipit-source-id: 61b10cb
Summary:
Labels inside switch statements were causing havoc (see test), and the translation of switch statements in general could be improved to handle more cases.
It turns out that `case` (and `default`) statements are more or less fancy labels into the code. In other words, if you erase all the `case XXX:` and `default:` strings in the `switch` statement you get the real structure of the program, and `switch` just jumps straight to the first `case` directives (and to the second if the first one is not satisfied, etc. until all `case`/`default` have been considered).
This suggests an alternative implementation: translate the body of the `switch` and simply record the list of switch cases inside that body, along with where they point to. Then post-process this list to construct the control flow of the `switch`, which points into the control-flow of the `body`. In order not to modify every function in `CTrans` to propagate the current list of cases, I created an ugly `ref` inside `SwitchCase` instead (but it cannot be directly accessed and it's guaranteed to be well-parenthesised wrt nested switches by the `SwitchCase` API so it's not too bad).
[unrelated] Also make translation failures output more information about what exactly in the source code is causing the crash, and the ancestors in the AST that lead to the crash site.
Reviewed By: martinoluca
Differential Revision: D8011046
fbshipit-source-id: 8455090
Summary: Follow C++ in having local variables owned plus silence reports on paths rooted on logical vars. We need both because when propagating ownership from right to left, the initial status of a temp var as owned is lost.
Reviewed By: sblackshear
Differential Revision: D7988575
fbshipit-source-id: 2e817d7
Summary:
This diff:
- translates C++ `catch` blocks
- adds an exceptional control-flow edge from the end of a `try` block to the beginning of a `catch` block
This obviously doesn't reflect the way exceptions actually work, but I think it is better than what we have now. For one thing, we'll see/translate code inside `catch` blocks, which were opaque before. If Clang analyses don't want this behavior, they can simply use `ProcCfg.Normal` (which, up until this diff, behaved identically to `ProcCfg.Exceptional`.
In the future, we can extend `trans_state` to track blocks that might throw an exception, and have each of these blocks transition to `catch` instead.
Reviewed By: jvillard
Differential Revision: D7814521
fbshipit-source-id: 67b86a6
Summary:
Before we were computing the size of an abstract state (`range`) using the `NonNegativeBound` domain but it wasn't able to express product of symbolic values.
This diff introduces a domain for that.
The range of an interval is still computed in `NonNegativeBound` but then the product is done in `TopLiftedPolynomial` so all costs end up being of that type.
The //symbols// of a polynomial are `NonNegativeBound` (so the polynomial only represent non-negative values, perfect for a cost), which handles substitution correctly, i.e. it gives zero instead of negative values.
Reviewed By: ddino
Differential Revision: D7397229
fbshipit-source-id: 6868bb7
Summary:
The annotation UiThread can, and is, used on classes as opposed to just methods, so extend the modelling to account for this.
Also, consider the annotation hereditary.
Reviewed By: jeremydubreil
Differential Revision: D7910762
fbshipit-source-id: 0df2c81
Summary:
Previously, the type of `trans_result` contained a list of SIL expressions.
However, most of the time we expect to get exactly one, and getting a different
number is a soft(!) error, usually returning `-1`.
This splits `trans_result` into `control`, which contains the information
needed for temporary computation (hence when we don't necessarily know the
return value yet), and a new version of `trans_result` that includes `control`,
the previous `exps` list but replaced by a single `return` expression instead,
and a couple other values that made sense to move out of `control`. This allows
some flexibility in the frontend compared to enforcing exactly one return
expression always: if they are not known yet we stick to `control` instead (see
eg `compute_controls_to_parent`).
This creates more garbage temporary identifiers, however they do not show up in
the final cfg. Instead, we see that temporary IDs are now often not
consecutive...
The most painful complication is in the treatment of `DeclRefExpr`, which was
actually returning *two* expressions: the method name and the `this` object.
Now the method name is a separate (optional) field in `trans_result`.
Reviewed By: mbouaziz
Differential Revision: D7881088
fbshipit-source-id: 41ad3b5
Summary: With the genrule approach, the directory the generated script is run from is inside `buck-out`. So we need to specify the project root before calling the `buck` command.
Reviewed By: mbouaziz
Differential Revision: D7938130
fbshipit-source-id: c265476
Summary:
This is an attempt to make things more consistent, and maybe save some work
from the `Format` module in case flambda doesn't have our backs.
Reviewed By: jberdine
Differential Revision: D7775496
fbshipit-source-id: 59a6314
Summary: Without the class name, it is not always clear from the error message where the method expecing non-null parameters defined.
Reviewed By: mbouaziz
Differential Revision: D7919492
fbshipit-source-id: 044fb83
Summary: I needed it for debugging but, to my dismay, it was borked again. This time it was because `jbuilder` moved the object files to another directory since the last jbuilder update.
Reviewed By: mbouaziz
Differential Revision: D7926267
fbshipit-source-id: 42ad26a
Summary:
Make the starvation checker enabled by default.
Add a deadlock issue type, distinct to starvation, which will be kept for UI thread starvation.
Add checks so that checker will do nothing on non-Java code.
Reviewed By: mbouaziz, ddino
Differential Revision: D7908381
fbshipit-source-id: 889f373
Summary: Calling Future.get from UI thread, or under a lock the UI thread may try to take has been associated with ANRs.
Reviewed By: ddino
Differential Revision: D7859296
fbshipit-source-id: b87bd94
Summary: std::lock allows for locking multiple lockable objects, while avoiding deadlock. This will fix some FPs in C++.
Reviewed By: da319
Differential Revision: D7844198
fbshipit-source-id: 2b7140a
Summary: We were wrongly using the underapproximation of `min` rather than the overapproximation
Reviewed By: ddino
Differential Revision: D7844267
fbshipit-source-id: c9d9247
Summary:
This simplifies the frontends and backends in most cases. Before this diff,
returning `void` could be modelled either with a `None` return, or a dummy
return variable with type `Tvoid`. Now it's always the latter.
Reviewed By: sblackshear, dulmarod
Differential Revision: D7832938
fbshipit-source-id: 0a403d1
Summary:
The abstract interpreter tried to handle exceptional control-flow by propagating the *pre* of a block that threw an exception rather than the *post*.
This was a half-measure that isn't correct when an exception-throwing instruction isn't in the middle of a block.
The handling of exceptions wasn't actually used anywhere and was leading to further hacks in `ProcCfg`, so let's get rid of it.
Reviewed By: mbouaziz, jvillard
Differential Revision: D7843872
fbshipit-source-id: 2a4a815
Summary: Returning the list of sub-expressions is not right and can cause assertion failures elsewhere in the frontend.
Reviewed By: dulmarod
Differential Revision: D7813493
fbshipit-source-id: 33ac9c1
Summary:
We want instr-granular invariant maps so let's use the OneInstrPerNode CFG in the AI analyzers.
This requires specializing the TransferFunctions.
Keep using the normal CFG where we only need node-granular informations.
Depends on D7587241
Depends on D7608526
Reviewed By: sblackshear
Differential Revision: D7618320
fbshipit-source-id: 73918f0
Summary:
When looking at large CFGs, at least in `xdot`, it's often difficult to find
the procedure you're looking for. Sorting the proc names puts them in
alphabetical order, which makes searching one procedure easier.
Reviewed By: mbouaziz
Differential Revision: D7758521
fbshipit-source-id: 8e9997f
Summary: We already suppress race reports if the field is marked in this way; makes sense to do the same thing for these reports.
Reviewed By: ngorogiannis
Differential Revision: D7589275
fbshipit-source-id: 8f0aeab
Summary: Currently when we look for already abduced expression and find an assertion [exp|->strexp:typexp], we use typexp rather than strexp.
Reviewed By: sblackshear
Differential Revision: D7617193
fbshipit-source-id: c089720
Summary:
Run with `SHELL = bash -e -u -o pipefail` to catch many kinds of failures. We
were silently failing during `make install` because of some missing escaping,
and the failure was hidden because it was happening inside a bash `for` loop.
This fixes the escaping issue and makes sure such issues will result in an
error as of now.
Also removes dangerous `find -exec` instances: `find` will `exit 0` event if
some commands failed.
Fixes#887
Reviewed By: mbouaziz
Differential Revision: D7569054
fbshipit-source-id: 542fe50
Summary:
This information is already available in the trace, and can contain absolute
paths to system includes (or infer's own clang runtime), which confuses the
diff analysis.
Reviewed By: mbouaziz
Differential Revision: D7534609
fbshipit-source-id: 5bd8f8b
Summary:
This can be noticed when the format of the DB changes, and other fun things
like that. No longer require to `make clean` to be able to pass these tests.
Reviewed By: mbouaziz
Differential Revision: D7533559
fbshipit-source-id: 670cb60
Summary:
It renames `eval_locs` to `eval_arr` and we use it for getting array block values the given input expressions are pointing to. For example, when given a program variable `x` as an input, `eval_arr` returns array blocks that `x` is pointing to, on the other hand, `eval` returns an abstract location of `x`.
Depends on D7471891
Reviewed By: mbouaziz
Differential Revision: D7471915
fbshipit-source-id: b994944
Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).
Reviewed By: mbouaziz
Differential Revision: D7453510
fbshipit-source-id: db8738e
Summary:
Report nullable inconsistencies by relying on the bytecode, and not on the presence of analysis summary on disk.
This use the `--external-java-packages` to avoid reporting inconsistencies outside of the codebase.
Reviewed By: sblackshear
Differential Revision: D7481101
fbshipit-source-id: 281135d
Summary:
It's already turned of systematically for the Java integration, this just
generalises it. The Buck daemon seems to cause issues with infer from time to
time that are hard to debug.
Reviewed By: jeremydubreil
Differential Revision: D7400068
fbshipit-source-id: f05ee07
Summary:
If an aggregate `a` has a field `f` whose type has a constructor (e.g., `std::string`), we translate creating a local aggregate `A { "hi" }` as `string(&(a.f), "hi")`.
This diff makes sure that we recognize this as initializing `a`.
Reviewed By: jeremydubreil
Differential Revision: D7404624
fbshipit-source-id: 0ba90a7
Summary:
Show where the invalidation occurred in the trace.
Should make things easier to understand.
Reviewed By: jeremydubreil
Differential Revision: D7312182
fbshipit-source-id: 44ba9cc
Summary: This was causing false positives when returning the constant integer 0.
Reviewed By: sblackshear
Differential Revision: D7330143
fbshipit-source-id: 45d19dd
Summary: It adds an issue type, `BUFFER_OVERRUN_U5`, for alarms involving unknown values, i.e., when the trace set includes an unknown function call.
Reviewed By: mbouaziz
Differential Revision: D7178841
fbshipit-source-id: bfe857b
Summary:
At the moment, Java and Clang sources/sinks live in the same inferconfig entry.
If we try to parse a Java procedure that happens to be an invalid Clang qualified name (e.g., `MyClass.<init>`),
parsing will crash.
As a temporary fix, throw an exception and catch it instead.
In the future, we can avoid this by requiring that JSON source/sink specifications to indicate the language.
Reviewed By: mbouaziz
Differential Revision: D7291880
fbshipit-source-id: f8f4502
Summary:
Aggregate initialization (e.g., `S s{1, 2}`) doesn't invoke a contructor.
Our frontend translates aggregation initialization as assigning to each field in the struct.
To avoid the appearance of the struct being uninitialized, count any assignment to a field of an aggregate struct as initializing the struct.
Reviewed By: jeremydubreil
Differential Revision: D7189671
fbshipit-source-id: ace02fc
Summary:
Previously, `backend_stats` were getting logged correctly only when `infer analyze` was directly called, not `infer run`. Now, we report `backend_stats` directly, as part of the `iterate_callbacks` function in the task passed to the `ProcessPool`.
As a side benefit, `aggregated_stats` are also logged correctly now.
Reviewed By: dulmarod
Differential Revision: D7195525
fbshipit-source-id: fb2a400
Summary: It corrects a precision bug in the interval domain, with adding some test cases.
Reviewed By: mbouaziz
Differential Revision: D7230918
fbshipit-source-id: 3ec641a
Summary:
:
Previously, we did not have information about type of `exp` in `sizeof exp` from clang plugin which led to `Bad_footprint` errors. Infer did not understand `sizeof *p` in `struct Person* p = malloc(sizeof *p);` and used some default type.
This resulted in `Bad_footprint` error when trying to assign to a field `age` in `p->age=42;`.
This diff uses the version of clang plugin which exports the appropriate type information.
update-submodule: facebook-clang-plugins
Reviewed By: dulmarod
Differential Revision: D7179870
fbshipit-source-id: 4104f10
Summary:
Show some `SymAssign`s (corresponding to parameters) in the trace.
Depends on D7194448
Reviewed By: skcho
Differential Revision: D7194479
fbshipit-source-id: 0deff6c
Summary: It corrects a bug that `&(x.f[n])` was evaluated to `&(x.f[0])`.
Reviewed By: mbouaziz
Differential Revision: D7179620
fbshipit-source-id: 04cbaa7
Summary: It simply resizes the target structure instead of allocating new heap memories and copying values.
Reviewed By: mbouaziz
Differential Revision: D7179353
fbshipit-source-id: 9c20f64
Summary: If a `Closure` expression `e` captures variable `x`, consider `e` as borrowing from `x`. When the closure is invoked via `operator()`, check that the borrow is still valid.
Reviewed By: jeremydubreil
Differential Revision: D7071839
fbshipit-source-id: d923a6a
Summary: It avoids that locations of array fields are evaluated to the `unknown` location incorrectly by addressing the case in the `eval_lindex` function.
Reviewed By: mbouaziz
Differential Revision: D7152736
fbshipit-source-id: 2dc825e
Summary: It collects array accesses from all sub expressions in commands.
Reviewed By: mbouaziz
Differential Revision: D7165098
fbshipit-source-id: 584dc80
Summary: It does not only malloc a new heap memory, but also copy its contents.
Reviewed By: mbouaziz
Differential Revision: D7152194
fbshipit-source-id: 58cba5e
Summary: This is to make sure than the analysis produces the same results independently from the order in which the members of a call cycle are analyzed.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6881971
fbshipit-source-id: 23872e1
Summary: Add a new command-line option `--external-java-packages` which allows the user to specify a list of Java package prefixes for external packages. Then the analysis will not report non-actionable warnings on those packages (e.g., inconsistent `Nullable` annotations in external packages).
Reviewed By: jeremydubreil
Differential Revision: D7126960
fbshipit-source-id: c4f3c7c
Summary: When a property was defined in a protocol, we were not translating its attributes which leads to retain cycles false positives. This diff fixes it. It also refactors the code for translating fields a bit.
Reviewed By: mbouaziz
Differential Revision: D7136355
fbshipit-source-id: b5e7445
Summary:
Fairly simple approach here:
- If the RHS of an assignment is a frontend-generated temporary variable, assume it transfers ownership to the LHS variable
- If the RHS of an assignment is a program variable, assume that the LHS variable is borrowing from it.
- If we try to access a variable that has borrowed from a variable that is now invalid, complain.
Reviewed By: jeremydubreil
Differential Revision: D7069947
fbshipit-source-id: 99b8ee2
Summary:
At function calls, it copies a subset of heap memory that is newly
allocated by callees and is reachable from the return value.
Reviewed By: mbouaziz
Differential Revision: D7081425
fbshipit-source-id: 1ce777a
Summary:
This is to fix the conflicts between Eradicate and the Biabduction when reporting the same kind of errors: when Eradicate is on, the Eradicate warnings will have priority over the null deference reported by the biabduction.
If this approach proved to be successful in prod, I will refactor the reporting mechanism in the analysis itself to simply not report the null dereference in this case at all. For the codebases that aren't yet fully consistently using `Nullable`, this combined approach looks like a good way to deploy Infer toward full null safety.
Reviewed By: mbouaziz
Differential Revision: D7102119
fbshipit-source-id: 35d3add
Summary:
Before D7100561, the frontend translated capture-by-ref and capture-by-value in the same way.
Now we can tell the difference and report bugs in the capture-by-value case.
Reviewed By: jeremydubreil
Differential Revision: D7102214
fbshipit-source-id: e9d3ac7
Summary:
The `may_last_field` boolean value in the `decl_sym_val` function presents that the location *may* (not *must*) be a flexible array member.
By the modular analysis nature, it is impossible to determine whether a given argument is a flexible array member or not---because of lack of calling context. For example, there are two function calls of `foo` below: (2) passes a flexible array member as an argument and (1) passes a non-flexible array, however it is hard to notice when analyzing the `foo` function.
```
struct T {
int c[1];
};
struct S {
struct T a;
struct T b;
};
void foo(struct T x) { ... }
void goo () {
struct S* x = (struct S*)malloc(sizeof(struct S) + 10 * sizeof(int));
foo(&(x->a)); // (1)
foo(&(x->b)); // (2)
}
```
We assume that any given arguments may stem from the last field of struct, i.e., flexible array member. (This is why `decl_sym_val` is called with `may_last_field:true` at the first time.) With some tests, we noticed that the assumption does not harm the analysis precision, because whether regarding a parameter as a flexible array member or not is about using a symbolic array size instead of a constant array size written in the type during the analysis of callee. Therefore still it can raise correct alarms if the actual parameter is given in its caller.
Reviewed By: mbouaziz
Differential Revision: D7081295
fbshipit-source-id: a4d57a0
Summary:
Switch to the current stable branch for clang.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D7067890
fbshipit-source-id: aedff90
Summary:
You can capture a variable by reference in a lambda, assign to it, and then invoke the lambda.
This looks like a dead store from the perspective of the current analysis.
This diff mitigates the problem by computing an additional analysis that tracks variables captured by ref at each program point.
It refuses to report a dead store on a variable that has already been captured by reference.
Later, we might want to incorporate the results of this analysis directly into the liveness analysis instead of just using it to gate reporting.
Reviewed By: jeremydubreil
Differential Revision: D7090291
fbshipit-source-id: 25eeffa
Summary:
Ran into this issue on Debian Testing, in which assert.h is probably different
due to a more recent toolchain. Without this change I get the following CFG
for `assert(e)`:
```
start
|-> prune (e) -> join
|-> prune (!e) -> __infer_fail("ASSERTION_FAILURE") -> exit
```
Notice that the first branch does not get to the exit, so infer must think that
the assertion is *always* violated, and reports `error: ASSERTION_FAILURE`.
This is broken.
Reviewed By: dulmarod
Differential Revision: D7067822
fbshipit-source-id: a2bf5ac
Summary:
It supports flexible array member using the following heuristic:
- a memory for a class is allocated by `malloc(sizeof(C) + n * sizeof(T))` format
- the last field of the class is an array
- the static size of the last field is one, i.e., `T field_name[1]`
When allocating and initializing members of classes, it sets the size of flexible array to `n+1` if the above conditions are met.
Reviewed By: mbouaziz
Differential Revision: D7056291
fbshipit-source-id: 31c5868
Summary:
The semantics of "placement new" is defined simply as an assignment.
For example, `C* x = new (y) C();` is analyzed as if `C* x = y;`.
Reviewed By: mbouaziz
Differential Revision: D7054007
fbshipit-source-id: 1c6754f
Summary:
The struct fields in Cil have been sorted for long time, however the
checkers do not seem to depend on the sortedness.
Reviewed By: sblackshear
Differential Revision: D7027858
fbshipit-source-id: 9e7ab96
Summary:
This commit improves precision of symbol instantiations.
When a return value of a callee is `[s1 + s2, _]` and if we want to
instantiate `s1` to `c3 + max(c4, s5)`, the lower bound was
substituted to `-oo` because our domain cannot express `c3 + max(c4,
s5) + s2`.
However, we can have instantiations that are preciser than `-oo`:
(1) `c3 + c4 + s2`
(2) or `c3 + s5 + s2`
because they are smaller than the ideal instantiation, `c3 + max(c4,
s5) + s2` and it is on the lower bound position.
For now, the implementation instantiates to (1) between the two ones,
because constant values introduced by `assert` or `assume`(`if`)
command are often used as safety conditions, e.g., `assert(index >=
0);` can place before array accesses. (We can change the stratege
later if we find that it doesn't work on some other cases.)
Reviewed By: mbouaziz
Differential Revision: D7020063
fbshipit-source-id: 62fb390
Summary:
A simple intraprocedural analysis that tracks when a storage location is read or deleted.
For now, this works only with local variable storage locations; field and array accesses are ignored.
In order to test this, I added a new "use-after-lifetime" warning. It complains when a variable is read or deleted after it has already been deleted.
Reviewed By: jeremydubreil
Differential Revision: D6961314
fbshipit-source-id: 75e95a2
Summary: We do not inject a destructor call if the destructor declaration does not contain a body in AST. We miss all the cases where the destructor is declared in `.h` file and defined in `.cpp` file as other files include `.h` file and do not contain the body of the destructor when destructor calls are being injected based on AST information. After this diff we inject destructor calls even if we do not have body for the destructor in AST.
Reviewed By: sblackshear
Differential Revision: D6796567
fbshipit-source-id: 1c187ec
Summary:
It prunes abstract memories on `assert` commands.
Problem: Since the assert command is sometimes translated to two
sequential `if` statments, it was not able to prune the memory
precisely at `assert` commands in Inferbo---the pruned memory at the
first branch was joined before the second branch.
Solution: To avoid losing the pruning information at the first branch,
now, it records which locations are pruned at the first branch and
applies the same pruning at the next branch if they have
semantically the same condition.
Reviewed By: mbouaziz
Differential Revision: D6895919
fbshipit-source-id: 15ac1cb
Summary:
See comment--`Prop(resType = blah) myProp` will generate `.myProp`, `.myPropRes`, and `.myPropAttr`, and any of them can be used to set the prop.
Because our annotation parameter parsing is a bit primitive, handle this by simply checking the `Res` and `Attr` suffixes for every `Prop`.
This shouldn't lead to false negatives because these methods will only exist if the `resType` annotation is specified anyway.
Reviewed By: jeremydubreil
Differential Revision: D6955362
fbshipit-source-id: ec59b21
Summary: In Obj-C blocks, we explicitly insert reads of the captured vars. This does the same thing for C++. For example, `foo() { int x = 1; [x]() { return x; } }` would previously not contain a read of `x` in `foo`. Now, we'll create a temporary that reads from `x` and pass it to the closure value.
Reviewed By: dulmarod
Differential Revision: D6939997
fbshipit-source-id: f218afc
Summary:
1) Fixes some false negatives when a method annotated with `nullable` in the header is not annotated in the implementation and the attribute lookup returns the implementation. In that case, we should follow the information given in the header.
2) Fixes some false positives when annotations are in the other way around, i.e. annotated in the implementation but not in the headers. For now, there should be no report in this case, but the analysis should be extended to report the inconsistency between the header and the implementation
3) Fixes some cases of weird reports caused by name conflicts where the method in the include has the same name has another method annotated differently.
Reviewed By: jvillard
Differential Revision: D6935379
fbshipit-source-id: 3577eb0
Summary:
Added a check for recursive calls not to add abduced reference parameters constraints. Abduced reference parameters constraints were causing assertion failure when renaming variables in specs, in particular, when transforming variables into callee variables.
A similar check is already in place for abduced retvals constraints.
Reviewed By: jeremydubreil
Differential Revision: D6856919
fbshipit-source-id: acfe840
Summary:
This allows Eradicate to lookup the annotations from the classpath and without requiring the code in the classpath to have been previously analyzed. The benefit is that source files can be analyzed independently of each other as long as the classpath is known.
The main goal is to run be able to run Eradicate as a linter without losing warnings.
We may have to add some more models of the standard libraries as no `Nullable` on a parameter does not necessarily mean that the method does not accept `null`.
Reviewed By: sblackshear
Differential Revision: D6921720
fbshipit-source-id: f525269
Summary:
- Combine two fields from ProcAttributes.t into a single field `method_kind` with more information
- New field details whether the procedure is an `OBJC_INSTANCE`, `CPP_INSTANCE`, `OBJ_CLASS`, `CPP_CLASS`, `BLOCK`, or `C_FUNCTION`
- `is_objc_instance_method` and `is_cpp_instance_method` fields no longer necessary
- Changed `is_instance` field in CMethod_signature to `method_kind` field of type ProcAttributes.method_kind
Reviewed By: dulmarod
Differential Revision: D6884402
fbshipit-source-id: 4b916c3
Summary:
Record "capture phases" in the runstate and in the source files table of the
database. Use this instead of filesystem timestamps to decide which files need
re-analyzing in the reactive analysis.
Reviewed By: jeremydubreil
Differential Revision: D6760833
fbshipit-source-id: 7955621
Summary:
The boolean lock domain is simple and surprisingly effective.
But it's starting to cause false positives in the case where locks are nested.
Releasing the inner lock also releases the outer lock.
This diff introduces a new locks domain: a map of locks (access paths) to a bounded count representing an underapproximation of the number of times the lock has been acquired.
For now, we just use a single dummy access path to represent all locks (and thus a count actually would have been sufficiently expressive; we don't need the map yet).
But I'm planning to remove this limitation in a follow-up by refactoring the lock models to give us an access path.
Knowing the names of locks could be useful for error messages and suggesting fixes.
Reviewed By: jberdine
Differential Revision: D6182006
fbshipit-source-id: 6624971
Summary:
Previously, we could understand than an access was safe either because it was possibly owned or protected by a thread/lock, but not both. If an access was both protected by a lock and rooted in a paramer (i.e., possibly owned), we would forget the ownership part of the precondition and remember only the lock bit. This leads to false positives in cases where an access protected by a lock is owned, but another unowned access to the same memory is not protected by a lock (see the new `unownedLockedWriteOk` E2E test for an example).
This diff makes access safety conditions disjunctive so we can simultaneously track whether an access is owned and whether an access is protected by a thread/lock. This will fix false positives like the one explained in T24015160.
Reviewed By: jberdine
Differential Revision: D6671489
fbshipit-source-id: d17715f
Summary:
We already knew not to warn when non-resource `Closeable`'s like `ByteArrayOutputStream` weren't closed, but we still warned on their subtypes.
This diff fixes that problem by checking subclasses in the frontend.
This also removes the need for Java source code models of non-resource types, so I removed them.
Reviewed By: jeremydubreil
Differential Revision: D6843413
fbshipit-source-id: 60fe7fb
Summary: The heuristics to determine the end of a block/procedure was too brittle, the new one ignores non significant instructions.
Reviewed By: jvillard
Differential Revision: D6845380
fbshipit-source-id: feab557
Summary:
The infer results directories in buck-out/ are "cleaned up" to avoid polluting
the Buck cache with too much data or non-deterministic data. In particular, the
runstate is deleted, which confused subsequent infer processes trying to read
the pre-existing results directory.
Add a special case in infer to delete pre-existing results directories in
buck-out instead of trying to load their state.
Reviewed By: mbouaziz
Differential Revision: D6845128
fbshipit-source-id: 5c716aa
Summary:
This diff fixes the translation of `new` and `placement new` with one argument. If `placement new` has more than one argument it means that it is user-defined (this will be addressed in another diff).
update-submodule: facebook-clang-plugins
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6807751
fbshipit-source-id: 7cf0290
Summary: This should allow to report several occurences of the an issue appearing several times within the same method.
Reviewed By: jvillard
Differential Revision: D6783298
fbshipit-source-id: 5555906
Summary:
This lets us fix the limitation of reporting false positives when a `private` function calls `build()` on a parameter without passing all of the required props.
We will now report such issues in the caller only if it fails to pass the required props.
An unfortunate consequence of this change is that we lose track of where the actual call to `build` occurs--we now report on the declaration of the caller function rather than on the call site of `build`.
I'll work on addressing that in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D6764153
fbshipit-source-id: 3b173e5
Summary:
The captured variables of a closure are tuples (id, var, typ) with the implicit assumption
that &var -> id holds in the heap. This is true when the closure is created, but is not enforce otherwise.
This becomes a problem when the closure is stored in the heap, goes passed a bi-abduction, and then it's executed
(see new test). This was failing before this diff and now succeeds.
We add the verification of this constraint to the normalization of sigma.
At the moment I expect Precondition_not_met to be removed, but also later, we will be able to compute retain cycles
over the closures, as the correct captured variable info is kept through the execution.
Reviewed By: jvillard
Differential Revision: D6796525
fbshipit-source-id: a8a7655
Summary:
Not sure what an "iCFG" is but the dotty is only about CFGs anyway.
Diff obtained by mass-`sed`.
Reviewed By: sblackshear
Differential Revision: D6324280
fbshipit-source-id: b7603bb
Summary: At each call to `Component$Builder.build()`, checks that the required props for `Component` have been set via prior calls to the `Builder`. Does not yet handle `Prop(optional = true)`, but will address that in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D6735524
fbshipit-source-id: 0c812fd
Summary:
Record the db schema, infer version, and run dates into
infer-out/.infer_runstate.json. This allows us to check on startup whether the
results directory was generated using a compatible version of infer or not, and
give a better error message in the latter case than some SQLite error about
mismatching tables.
This will be used in a follow-up diff to record capture phases too, and avoid
relying on filesystem timestamps of the infer-out/capture/foo/ directories for
reactive analysis.
Had to change some tests Makefiles to make sure they do not attempt to re-use
stale infer-out directories, which would now fail the run.
The stale infer-out directory gets deleted if `--force-delete-results-dir` is
passed (but a warning still gets printed).
Reviewed By: mbouaziz
Differential Revision: D6760787
fbshipit-source-id: f36f7df
Summary:
Previously imports with relative filenames would not get resolved so the result
would depend on where infer had been run from. Usually this was the project
root. Now, resolve path names of imports relative to the file doing the
`#IMPORT`. This changes behaviour most of the time.
Reviewed By: dulmarod
Differential Revision: D6784740
fbshipit-source-id: 4ccb7bf
Summary:
This changes the syntax for AL imports from `#IMPORT <file>` to `#IMPORT
"file"`. As a side-effect, the `file` part is now lex'd more permissively too.
Reviewed By: dulmarod
Differential Revision: D6784669
fbshipit-source-id: cc1bb73
Summary:
In Java, static variables are distinguished by package/class:
the file where they are defined doesn't matter.
Fixes#831.
Closes https://github.com/facebook/infer/pull/833
Reviewed By: jeremydubreil
Differential Revision: D6661240
Pulled By: sblackshear
fbshipit-source-id: beeb2f9
Summary:
Some commands (mostly `infer report`) would attempt to run the initialisation
code of infer from the default results directory instead of the one used by the
test. This is mostly harmless because we do not actually use anything from the
directory (typically, we pass `--from-json-results foo.json` and only foo.json
matters). However, this can trip the initialisation code, eg on db schema
changes.
Reviewed By: mbouaziz
Differential Revision: D6711641
fbshipit-source-id: f04b4c7
Summary: Previously we had a single sanitizer kind for escaping, but this isn't quite right. A function that escapes a URL doesn't necessarily make a string safe to execute in SQL, for example.
Reviewed By: the-st0rm
Differential Revision: D6656376
fbshipit-source-id: 572944e
Summary: The checker should only propagate the nullablility on the lhs when of pointer type.
Reviewed By: sblackshear
Differential Revision: D6630294
fbshipit-source-id: 07fe3d6
Summary: This subdirectory was only containing tests related to nullable on Objective C.
Reviewed By: sblackshear
Differential Revision: D6657654
fbshipit-source-id: 11003f2
Summary:
Model for `folly::split` that handles the representation in the cpp model.
Depends on D6544992
Reviewed By: jvillard
Differential Revision: D6545006
fbshipit-source-id: 2b7a139
Summary:
Before this diff, the nullable checker would not be able to find annotations involving methods annotated in the protocols
update-submodule: facebook-clang-plugins
Reviewed By: sblackshear
Differential Revision: D6534893
fbshipit-source-id: 39bd3dd
Summary: This is to allow the bi-abduction analysis and the nullable checker for Clang languages to run together without stepping on each other toes.
Reviewed By: sblackshear
Differential Revision: D6567934
fbshipit-source-id: a318c33
Summary: There was a back and forth conversion between `string` and `IssueType.t` which was not necessary.
Reviewed By: sblackshear
Differential Revision: D6562747
fbshipit-source-id: 70b57a2
Summary: As Dulma pointed out, adding or removing paramters in a method in Objective C is changing the name of the method. Such changes should not make pre-exisiting issues reported as introduced. This diff is to prevent this by only keeping in the bug hash the part of the name that is before the first colon.
Reviewed By: dulmarod
Differential Revision: D6491215
fbshipit-source-id: 3c00fae
Summary:
Our model of unique_ptr and shared_ptr relied on the fact that we could C-style cast a pointer to the internal pointer type used in the smart pointer.
This is wrong when the smart pointer is used with a custom deleter that declares its own pointer type whose is not constructible from just a single pointer.
Reviewed By: dulmarod
Differential Revision: D6496203
fbshipit-source-id: 1305137
Summary: Local `CKComponentScope`'s are often created purely for their side effects, so it's fine for them to be unread.
Reviewed By: jeremydubreil
Differential Revision: D6475475
fbshipit-source-id: 17e869a
Summary: This would allow the checker to detect indirect nullable violations, i.e. violations that are involving intermediate method calls on potentially `nil` values.
Reviewed By: sblackshear
Differential Revision: D6464900
fbshipit-source-id: 3663729
Summary: NSDictionary initialization will crash when using `nil` as a key or as a value
Reviewed By: dulmarod
Differential Revision: D6466349
fbshipit-source-id: 57bb012
Summary: This will avoid collisions when the inner classes are implementing the same methods. For example, the previous version of the bug hash could conflate the issues when several annonymous inner classes are implementing the same method, e.g. a annonymous subclass of `Runnable` implementing `run()`.
Reviewed By: sblackshear
Differential Revision: D6461594
fbshipit-source-id: 2bb8545
Summary:
Simpler bug hash that is more independent of the underlying analysis. This now computes the hash based on:
- the bug type.
- the base filename: i.e for my/source/File.java, just keep File.java. So the hash will not change when moving files around.
- the simple method name: i.e. without package information and list of parameters. So changing the list of parameters will not affect the bug hash.
- the error message were the line numbers have been removed. So moving code or reformatting will not affect the hash.
Reviewed By: jberdine
Differential Revision: D6445639
fbshipit-source-id: 82e3cbe
Summary: To avoid false positives, we treat `operator[]` in cpp as container read. Moreover, if a container `c` is owned, we make all accesses `c[i]` to be also owned.
Reviewed By: sblackshear
Differential Revision: D6396574
fbshipit-source-id: 94aabff
Summary:
It seems that the abstraction instructions were not previously added the the CFG.
This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.
Reviewed By: sblackshear, jvillard
Differential Revision: D6383672
fbshipit-source-id: cedcb8a
Summary:
As da319 points out, we did not handle this case correctly before. There were a few reasons why:
(1) An assignment like `struct S s = mk_s()` gets translated as `tmp = mk_s(); S(&s, tmp)`, so we didn't see the write to `s`.
(2) We counted uses of variables in destructors and dummy `_ = *s` assignments as reads, which meant that any struct values were considered as live.
This diff fixes these limitations so we can report on dead stores of struct values.
Reviewed By: da319
Differential Revision: D6327564
fbshipit-source-id: 2ead4be
Summary:
The diff is very big but it's mostly removing code. It was inspired by the fact that we were getting Dead Store FPs because we were modeling some functions from CoreFoundation and CoreGraphics directly as alloc in the frontend, which caused the parameters of the function to be seen as dead. See the new test.
To deal with this, if we are going to skip the function, we model it as malloc instead. Given how many models we had for those "model as malloc" functions, I removed them to rely solely on the new mechanism.
The modeling of malloc and release was still based on the old retain count implementation, even though all we do here is a malloc/free kind of analysis. I also changed
that to be actually malloc/free which removed many Assert false in the tests. CFRelease is not exactly free though, and it's possible to use the variable afterwards. So used a custom free builtin that only cares about removing the Memory attribute and focuses on minimizing Memory Leaks FPs.
Otherwise we were translating CFBridgingRelease as a special cast, and this wasn't working. To simplify this as well, I removed all the code for the special cast, and just modeled CFBridgingRelease and CFAutorelease also as free_cf, to avoid Memory Leak false positives. I also treated the cast __bridge_transfer as a free_cf model. This means we stopped trying to report Memory Leaks on those objects.
The modeling of CoreGraph release functions was done in the frontend, but seemed simpler to also simplify that code and model all the relevant functions.
Reviewed By: sblackshear
Differential Revision: D6397150
fbshipit-source-id: b1dc636
Summary:
- Plug model checkers
- Add alloc size safety condition on alloc of negative, zero or big size
Reviewed By: sblackshear
Differential Revision: D6375144
fbshipit-source-id: bbea6f3
Summary: This option was for compatibility with the command line options of the previous, but is no longer used. This diff removes the option and the deprecated code.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6351097
fbshipit-source-id: 0e4cfc5
Summary: Adding a null key or a null value will cause a runtime exception.
Reviewed By: sblackshear
Differential Revision: D6378618
fbshipit-source-id: 8bd27c6
Summary:
This resolves#796 . Effectively it adds file specific suffix to name of all global initializers (so initializersof two global variable of the same name will have unique Typ.Procname). which is the same rule as currently used by constructing Procname for the static functions. However this change applies to initializers of all global variables and not just static (arguably it's a right thing. since GCC used to allow multiple global variables with the same name).
Consequences of this change that it becomes impossible to know name of generated initialization function of global ('extern') variables. However get_initializer_pname function is only referenced by the frontend (when creating initializer for the defined global variables) and by the SIOF checker.
Closes https://github.com/facebook/infer/pull/801
Reviewed By: jvillard
Differential Revision: D6335034
Pulled By: dulmarod
fbshipit-source-id: 1a92c08
Summary: Adding a nil object to an NSArray will crash. Adding this case to the checker.
Reviewed By: sblackshear
Differential Revision: D6346241
fbshipit-source-id: 3fe6f20
Summary: The clang compiler introduces a materialized temporary expression which should be treated similarly to the Infer internal temporary variables.
Reviewed By: sblackshear
Differential Revision: D6331237
fbshipit-source-id: 81d8196
Summary:
We would previously skip any function that had one of these.
A no-op translation is sufficient to fix this issue (see new E2E test).
Reviewed By: mbouaziz
Differential Revision: D6317323
fbshipit-source-id: 0855bd8
Summary: Just changing ClangTrace to actually look at the different sanitizer kinds.
Reviewed By: jeremydubreil
Differential Revision: D6325086
fbshipit-source-id: 5da236d
Summary: In a thread safety report we used the access path from the final sink. This diffs change the report to include the expanded access path from the initial sink.
Reviewed By: sblackshear
Differential Revision: D6297848
fbshipit-source-id: 2386063
Summary:
This diff adds a new way of executing blocks when they are passed as parameters to a method. So far we just skipped the block in this case.
Now we can execute it. Let's demonstrate with an example. Say we have
//foo has a block parameter that it executes in its body
foo (Block block) { block();}
// bar calls foo with a concrete block
bar() {
foo (^(){
self->x = 10;
});
};
Now, when we call the method foo with a concrete block, we create a copy of foo instantiated with the concrete block, which in itself is translated as a method with a made-up name.
The copy of foo will get a name that is foo extended with the name of the block parameter, the call to the block parameter will be replaced to a call to the concrete block, and the captured variables
of the concrete block (self in this case), will be added to the formals of the specialized method foo_block_name.
This is turned on at the moment for ObjC methods with ObjC blocks as parameters, and called with concrete blocks. Later on we can extend it to other types of methods, and to C++ lambdas, that are handled similarly to blocks.
Another extension is to check when the block has been called with nil instead of an actual block, and raise an error in that case.
After this diff, we can also model various methods and functions from the standard library that take blocks as parameters, and remove frontend hacks to deal with that.
Reviewed By: ddino
Differential Revision: D6260792
fbshipit-source-id: 0b6f22e
Summary: The checker should not report unitinialzed values on the throw branch.
Reviewed By: ddino
Differential Revision: D6267019
fbshipit-source-id: 05768f1
Summary: We were conflating reads/writes with container reads/writes that created false positives.
Reviewed By: sblackshear
Differential Revision: D6232768
fbshipit-source-id: 39159cb
Summary: This is a hack to removes most of the false positives of this checker in Objective C.
Reviewed By: sblackshear
Differential Revision: D6239914
fbshipit-source-id: 1cf05de
Summary:
This confuses the SIOF checker and causes false positives. This dummy deref is
generated for constructors of classes that are modeled as being pointer types
instead of the actual class in infer, typically for smart pointers. I do not
understand how this works.
The biabduction also analyses this code, so might now get confused itself.
Reviewed By: jberdine
Differential Revision: D6221817
fbshipit-source-id: 050c5a9
Summary:
The issue is with classes defining static data members:
```
$ cat foo.h
struct A {
static int foo;
};
$ cat foo.cpp
#include "foo.h"
int A::foo = 12;
int f() { return A::foo; // should see A::foo as defined in this translation unit
$ cat bar.cpp
#include "foo.h"
void g() { return A::foo; // should see A::foo defined externally
```
Previously, both foo.cpp and bar.cpp would see `A::foo` as defined within their
translation unit, because it comes from the header. This is wrong, and static
data members should be treated as extern unless they're defined in the same
file.
This doesn't change much except for frontend tests. SIOF FP fix in the next diff.
update-submodule: facebook-clang-plugins
Reviewed By: da319
Differential Revision: D6221744
fbshipit-source-id: bef88fd
Summary: This only works for Java at the moment but we can re-organise the code later to add the Objective C equivalent of these assertion methods.
Reviewed By: mbouaziz
Differential Revision: D6230588
fbshipit-source-id: 46ee98e
Summary: The checker should not report nullable violations on repeated calls
Reviewed By: sblackshear
Differential Revision: D6195471
fbshipit-source-id: 16ff76d
Summary: The Java bytecode does not contain information about the location of abstract of interface methods. Before this diff, the analysis trace was tuncated and the file where the abstract or interface method was not included in the trace, which makes it harder to understand the Infer report, especially when the method is on a generated file that is not checked in the repository.
Reviewed By: sblackshear
Differential Revision: D6223612
fbshipit-source-id: c80c6f2
Summary: More general version of the fix in D6138749. This diff moves RacerD's lock modeling into a separate module and uses the module in the HIL translation to check when a function has lock/unlock semantics.
Reviewed By: jberdine, da319
Differential Revision: D6191886
fbshipit-source-id: 6e1fdc3
Summary: Functions that do not belong to a class or a struct are translated to c-style functions even in the context of cpp. We need to add ownership to locals for c-style functions too.
Reviewed By: sblackshear
Differential Revision: D6196882
fbshipit-source-id: 715f129
Summary:
vector::data returns a pointer to the first value of the vector.
- The size of the (array) pointer should be the same with the vector.
- The pointer should point to the same abstract value with the vector.
Reviewed By: mbouaziz
Differential Revision: D6196592
fbshipit-source-id: cc17096
Summary: `std::unique_lock` constructor allows to create a unique lock without locking the mutex. `std::unique_lock::try_lock` returns true if mutex has been acquired successfully, and false otherwise. It could be that an exception is being thrown while trying to acquire mutex, which is not modeled.
Reviewed By: jberdine
Differential Revision: D6185568
fbshipit-source-id: 192bf10
Summary:
Code often uses std::unique_lock::owns_lock to test if a deferred lock
using the 2-arg std::unique_lock constructor actually acquired the
lock.
Reviewed By: sblackshear
Differential Revision: D6181631
fbshipit-source-id: 11e9df2
Summary:
Use a distinct issue type for the Java and C++ concurrency analyses,
as the properties they are checking are significantly different.
Reviewed By: sblackshear
Differential Revision: D6151682
fbshipit-source-id: 00e00eb
Summary:
In a summary, you never want to see a trace where non-footprint sources flow to a sink.
Such a trace is useless because nothing the caller does can make more data flow into that sink.
Reviewed By: jeremydubreil
Differential Revision: D5779983
fbshipit-source-id: d06778a
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
Mehdi Bouaziz
Jeremy Dubreil
Jules Villard
Daiva Naudziuniene
Nikos Gorogiannis
Brandon Kieft
Martino Luca
Dino Distefano
Sam Blackshear
Sungkeun Cho
Ezgi Çiçek
Dulma Churchill
Oliver Castillo
Varun Arora
Tony Hu
Jérémie Marguerie
Radu Grigore
Peter O'Hearn
Vivek Dhiman
Dominic Cooney
Josh Berdine
Anders Papitto