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:
Allows:
- matching function arguments with or without capturing,
- capturing part of an argument, e.g. expression only,
- optional arguments, wrapped into an OCaml option if captured.
Reviewed By: jvillard
Differential Revision: D6544992
fbshipit-source-id: a64ba45
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: This factors out some duplicated code for {,de}serializing source files.
Reviewed By: mbouaziz
Differential Revision: D6324234
fbshipit-source-id: 1741657
Summary:
Instead of storing the cfgs of source files inside their own individual files,
put them in results.db, in their own table. (that table may change in the
future to map source files to more than just their cfgs, eg their tenv as well)
Reviewed By: jberdine
Differential Revision: D6297201
fbshipit-source-id: 7fa891d
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:
This diff adds a layer of report deduplication logic in addition to
the existing scheme.
Suppose issue 1 with trace1a and trace1b, and issue 2 with trace2a and
trace2b. If trace1a ends at the same location as trace2a (resp.,
trace2b) and trace1b ends at the same location as trace2b (resp.,
trace2a), then consider issues 1 and 2 to be duplicates.
This chooses to report the issue with the smaller sum of trace
lengths, breaking ties using the issue hashes, and eventually the
entire issue. Therefore there is a potential for flakiness with
respect the the choice of which report to make within a
hash-equivalence class.
Reviewed By: sblackshear
Differential Revision: D6519607
fbshipit-source-id: 63210ab
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: It is difficult to understand a lock consistency violation if error message includes an access path with a logical variable or a temporary variable as a base. As a temporary fix, we want to suppress all such warnings.
Reviewed By: sblackshear
Differential Revision: D6460559
fbshipit-source-id: 6f3fc18
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: For the Buck integration for Java, caching when a summary is not found avoids going through the whole classpath every time a summary for the same method is not found.
Reviewed By: mbouaziz, jvillard
Differential Revision: D6402833
fbshipit-source-id: 4feb422
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: I always get confused by `accessPath.ml` not being next to HIL when trying to open files
Reviewed By: sblackshear
Differential Revision: D6462980
fbshipit-source-id: 8ba9b71
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:
Summaries can be big, and they can always be printed via `infer report` if we want to see them.
There's no reason to log them eagerly, even in debug mode.
Reviewed By: jeremydubreil
Differential Revision: D6451815
fbshipit-source-id: 643cd47
Summary: In every place this was used except one, `debug_mode` is also used as a gate.
Reviewed By: jeremydubreil
Differential Revision: D6450913
fbshipit-source-id: 6a5716d
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:
On spinning disks the performance of commits are worse when `synchronous=NORMAL`.
Reading the documentation of SQLite, when `synchronous=OFF` there's a risk of DB corruption when the operating system crashes or the computer loses power before that data has been written to the disk surface; on the other hand, a crash in Infer should keep data in the DB in a sound state.
Buck reached the same conclusions too: 4680162279
Reviewed By: mbouaziz
Differential Revision: D6413384
fbshipit-source-id: 99e4650
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:
Deduping issues when generating a single report and then diffing the
reports can lead to introduced issues being considered duplicates of
existing issues.
Reviewed By: sblackshear
Differential Revision: D6414673
fbshipit-source-id: bba81fd
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:
justmovingthingsaround
Models need these functions, they have to be somewhere else.
The split might seem weird for now but will (hopefully) look more obvious in the following diff.
Reviewed By: skcho
Differential Revision: D6408322
fbshipit-source-id: c7e430f
Summary:
Extends `ProcnameDispatcher` to allow matching typenames only.
There isn't much new here, mainly moving stuff so that we only have to open one module to use the operators.
Reviewed By: skcho
Differential Revision: D6408245
fbshipit-source-id: afc6533
Summary: I accidentally deleted the support for `infer report file.specs` which was printing the summary to standard output.
Reviewed By: sblackshear
Differential Revision: D6416690
fbshipit-source-id: 62246f3
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:
This is a good moment to close Sqlite's DB handles, and in general can be used to postpone some actions right before infer terminates.
Since exiting is done via uncaught exception handling, the `late_epilogue` callback will run at the very end, even after all the `at_exit` callbacks have been invoked. The only exception is made in case of signalling, in which case the `late_epilogue` is still invoked, but before any of the `at_exit` callbacks.
Reviewed By: jvillard
Differential Revision: D6404961
fbshipit-source-id: 8ff7a05
Summary:
The model is the same as `com.google.common.base.Preconditions`.
We could imagine a more generic ways of dealing with `x.y.Z.checkNotNull()` but this would work for now.
Reviewed By: sblackshear
Differential Revision: D6341869
fbshipit-source-id: 5b6e507
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:
A modeled function is not only an evaluator but also a checker, at least in Inferbo where both things happen in two passes.
This diff just prepares for it without generating new alarms.
Reviewed By: jvillard
Differential Revision: D6373051
fbshipit-source-id: 264696f
Summary:
In C++ some modeled functions have definitions, which leads to traces
that contain an access from the modeling, but continue on into the
implementation of the modeled function. Such traces appear the same as
those that are truncated due to limitations of the buck integration in
the Java analysis. Since all Java models are for functions without
definitions in the code base, this diff limits the truncated trace
suppression to the Java analysis.
Reviewed By: sblackshear
Differential Revision: D6373793
fbshipit-source-id: 1f01509
Summary: There is a lot of code to create LaTeX output of the Infer datastructures, but this does not seem to be used anymore.
Reviewed By: jvillard
Differential Revision: D6355686
fbshipit-source-id: 55de8e9
Summary:
This field was always empty.
depends on D6351097
Reviewed By: sblackshear, jvillard
Differential Revision: D6351243
fbshipit-source-id: 4a74bea
Jeremy Dubreil
Martino Luca
Mehdi Bouaziz
Sam Blackshear
Dino Distefano
Jules Villard
Dulma Churchill
Daiva Naudziuniene
Josh Berdine
Peter O'Hearn
Peter Goldsborough