Summary: Trying to convert a large int literal to an OCaml int raises an exception. The use case here actually needed a float anyway, so add an API for that.
Reviewed By: jeremydubreil
Differential Revision: D8550410
fbshipit-source-id: 382495b
Summary: Record that it is not supported: https://github.com/facebook/infer/issues/8
Reviewed By: mbouaziz, dulmarod
Differential Revision: D8442762
fbshipit-source-id: fa271cb
Summary:
I realized that control variable analysis was broken when we had multiple back-edges for the same loop. This is often the case when we have a switch statement combined with continue in a loop (see `test_switch` in `switch_continue.c`) or when we have disjunctive guards in do-while loops.
This diff fixes that by
- defining a loop by its loophead (the target of its backedges) rather than its back-edges. Then it converts back-edge list to a map from loop_head to sources of the loop's back-edges.
- collecting multiple guard nodes that come from potentially multiple exit nodes per loop head
In addition, it also removes the wrong assumption that an exit node belongs to a single loop head.
Reviewed By: mbouaziz
Differential Revision: D8398061
fbshipit-source-id: abaf288
Summary:
We need to report on non-private methods (the opposite even leads to FPs sometimes on deadlocks). To do this, the domain needs to change so that the interpretation of an order pair `a,b` is no longer "lock `a` is taken in the *current method* and held until lock `b` is taken". Instead the meaning is now "lock `a` is taken in some method *of the same class with the current method* and is held until `b` is taken".
These changes are quite drastic because the previous implementation optimised extensively around the previous use case.
Reviewed By: mbouaziz
Differential Revision: D8395351
fbshipit-source-id: a2bd22b
Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.
```
Potential deadlock.
Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```
Reviewed By: mbouaziz
Differential Revision: D8394978
fbshipit-source-id: 671ccb0
Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.
```
Potential deadlock.
Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```
Reviewed By: mbouaziz
Differential Revision: D8379328
fbshipit-source-id: bc33983
Summary: Deadlocks can be very noisy, so dedup reports on same line by showing only the one with the shortest trace and a count of the suppressed ones.
Reviewed By: mbouaziz
Differential Revision: D8351148
fbshipit-source-id: 8913db2
Summary: We were missing reads of `a` if it was used in void cast, i.e. `(void) a;` This caused dead store false positives: we were not using `exp` that was the result of translating `a`. This diff creates a call to built-in skip function with `exp` as its argument, which causes the analyses to see reads of `exp`.
Reviewed By: mbouaziz
Differential Revision: D8332092
fbshipit-source-id: f3b0e10
Summary: Introduce an annotation that forces the summary of a method to be free of blocking events, without suppressing other reports.
Reviewed By: jeremydubreil
Differential Revision: D8276787
fbshipit-source-id: be9eed8
Summary: The case of nullable properties was already working but there was no test for it.
Reviewed By: dulmarod
Differential Revision: D8266468
fbshipit-source-id: c074d69
Summary: Create mechanism for suppressing starvation reports. To do that, refactor and expose a Checkers function.
Reviewed By: mbouaziz
Differential Revision: D8259583
fbshipit-source-id: f5b5a63
Summary: There is a number of dangling pointer dereference false positives coming from our treatment of union in c/cpp. For now, do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8279802
fbshipit-source-id: a339b0e
Summary: We get a lot of false positives for union types as union fields are treated as separate memory locations at the moment. For now we do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8277363
fbshipit-source-id: efe5b4a
Summary:
Use the component of the abstract state `events` to report. This set contains reachability facts about blocking calls and lock acquisitions.
The other component, `order`, contained pairs of a reachable event `e'` from an event option with the semantics that if the option is `None` then we have an element that now goes into `events`, and if the option is `Some e` then the element represents a lock acquired and a trace *from* `e` to `e'`
Now, `order` can be simplified to proper pairs of events, without the option.
Reviewed By: jvillard
Differential Revision: D8227665
fbshipit-source-id: e6f4dac
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
Martin Trojer
Jeremy Dubreil
Nikos Gorogiannis
Ezgi Çiçek
Jules Villard
Mehdi Bouaziz
Dulma Churchill
Daiva Naudziuniene
Brandon Kieft
Martino Luca
Dino Distefano
Sam Blackshear
Sungkeun Cho