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:
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:
Having the `Node` module including in the `CFG` one is confusing.
Let's keep it separate.
Reviewed By: ngorogiannis
Differential Revision: D8185754
fbshipit-source-id: 62077e6
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: That name doesn't make sense anymore and could be confusing.
Reviewed By: mbouaziz
Differential Revision: D8235507
fbshipit-source-id: b6a6e71
Summary:
Forcing integration with `--force-integration` would only work for some
integrations that stayed in OCaml-land. This propagetes the forcing to
infer.py.
Also remove some unused options on the Python side, and add more debug
information.
Fixes#927
Reviewed By: mbouaziz
Differential Revision: D8235504
fbshipit-source-id: 1d98543
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: To simplify things, have a separate set of simple trace->event elements. Currently this is not used for reporting, in preparation for another diff.
Reviewed By: mbouaziz
Differential Revision: D8203721
fbshipit-source-id: ecc8bae
Summary:
For now: just moving this list behind an abstract type.
Next: changing the internal representation.
Reviewed By: ngorogiannis
Differential Revision: D8140926
fbshipit-source-id: 5b959b0
Summary:
`IList.map_changed` relies on `take_append`.
The existing code was a `take_rev_append` instead.
Fixed it.
Tests are still passing, we might want to look at callsites and consider a `map_changed_unordered`.
Reviewed By: jvillard
Differential Revision: D8201187
fbshipit-source-id: 151b95c
Summary: In preparation for allowing unbalanced locking, we need the lock state in the summary.
Reviewed By: mbouaziz
Differential Revision: D8201932
fbshipit-source-id: 05a1b38
Summary:
Preparing for the future change, we won't see instructions as lists but as an abstract type.
This change may be a very minor perf regression: does a few more (but bounded by a constant) instructions traversals only for the nodes involving a Printf-like function call, only for the PrintfArgs checker...
Reviewed By: jvillard
Differential Revision: D8094124
fbshipit-source-id: e2e2c5e
Summary:
We never really need the list of nodes/succs/preds, we only need to fold over them.
This will reduce garbage for computed lists like in the Exceptional CFG or the OneInstrPerNode CFG.
Reviewed By: ngorogiannis
Differential Revision: D8185665
fbshipit-source-id: d042beb
Summary: In preparation to change the underlying module structure so as to allow three-point traces (call-site, intermediate call-site and endpoint), rename modules to better reflect function plus use records vs pairs of pairs :P
Reviewed By: mbouaziz
Differential Revision: D8187369
fbshipit-source-id: ed3e4ac
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:
The main motivation is preparing for a future change.
This also reduces lifetime of potential garbage.
Reviewed By: jeremydubreil
Differential Revision: D8185648
fbshipit-source-id: 6d0a568
Summary:
Append can be costly, let's do it once only.
Depends on D8185619
Reviewed By: jeremydubreil
Differential Revision: D8185634
fbshipit-source-id: 67f84a9
Summary:
Rely on the underlying CFG preds:
- perf: no need to append lists
- correctness: the underlying CFG may be removing duplicates
Reviewed By: ngorogiannis
Differential Revision: D8185638
fbshipit-source-id: 3b6f70a
Summary:
- do not `List.rev` for `List.last`
- `List.rev_filter_map` rather than `filter |> map |> rev`
Reviewed By: da319
Differential Revision: D8185619
fbshipit-source-id: aeb41a4
Summary: The order of nodes means nothing, and should not matter, let's save the whales!
Reviewed By: ngorogiannis
Differential Revision: D8182137
fbshipit-source-id: bc14a2c
Mehdi Bouaziz
Nikos Gorogiannis
Jeremy Dubreil
Jules Villard
Dulma Churchill
Daiva Naudziuniene
Brandon Kieft
Martino Luca
Dino Distefano