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: D8395399
fbshipit-source-id: b4bb48c
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: Removing an internal error in SIL to HIL translation which I had added before to log how often the particular case was happening. It happens quite often, and I have a task to investigate the issue. Removing it as it spams the analysis output a lot.
Reviewed By: dulmarod
Differential Revision: D8316822
fbshipit-source-id: 4047cbe
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: I don't understand what this function is for. Let's remove it.
Reviewed By: mbouaziz
Differential Revision: D8320839
fbshipit-source-id: eeb14f7
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:
See the results online!
http://fbinfer.com/docs/man-pages.htmlhttp://fbinfer.com/docs/internal-API.html
These html pages are written by hand, but their target is auto-generated.
I cheated a bit by generating the docs for the current version of infer and not
0.15.0 but they are hopefully very similar.
Depends on D8314572
Reviewed By: jeremydubreil
Differential Revision: D8318132
fbshipit-source-id: ffca43c
Summary:
`make doc` will use `jbuilder` (which in turn uses `odoc`) to generate the
documentation for infer's modules. This is useful to browse the APIs of infer
and gives a more discoverable place to host more general documentation about
infer's internals.
Besides the actual plumbing necessary to generate the docs, this diff also
- Moves the various infer/src/*/README.md to index.mld files that make it to the generated docs
- Fixes some doc comments that would anger `ocamldoc`
Closes#435
Reviewed By: mbouaziz
Differential Revision: D8314572
fbshipit-source-id: 4a5c70e
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:
Now the result won't depend on the visit order of instructions
Depends on D8235834
Reviewed By: jeremydubreil
Differential Revision: D8235907
fbshipit-source-id: a6eb469
Summary: The clang distribution uses symlinks in some places, which avoids copying rather large binaries. `make install` was replacing these with actual copies. Try not to be so wasteful anymore.
Reviewed By: mbouaziz
Differential Revision: D8260777
fbshipit-source-id: eccabab
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
Mehdi Bouaziz
Nikos Gorogiannis
Dulma Churchill
Martino Luca
Daiva Naudziuniene
Dino Distefano
Ezgi Çiçek
Jeremy Dubreil
Jules Villard