Summary:
The models are only for biabduction so try to make that clearer in the
code and documentation.
Reviewed By: skcho
Differential Revision: D16603147
fbshipit-source-id: 4a2be53de
Summary:
Get rid of false positive as in the test by modelling `Double`. Longer term we
should probably prevent biabduction from blocking the angelic analysis on
`Nullable` fields but that seems harder.
Reviewed By: jeremydubreil
Differential Revision: D14005228
fbshipit-source-id: 59ef2ed66
Summary:
Goal of the stack: deprecate the `--analyzer` option in favour of turning
individual features on and off. This option is a mess: some of the options are
now subcommands (compile, capture), others are aliases (infer and checkers),
and they can all be replicated using some straightforward combination of other
options.
This diff: stop using `--analyzer` in tests. It's mostly `checkers` everywhere,
which is already the default. `linters` becomes `--no-capture --linters-only`.
`infer` is supposed to be `checkers` already. `crashcontext` is
`--crashcontext-only`.
Reviewed By: mbouaziz
Differential Revision: D9942689
fbshipit-source-id: 048281761
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:
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 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:
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:
Another step toward running the biabduction analysis as a checker.
Depends on D6038210
Reviewed By: jvillard
Differential Revision: D6038682
fbshipit-source-id: fed45bf
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: Model the `remove(...)` and the `clear()` method of `HashMap`.
Reviewed By: sblackshear
Differential Revision: D5887674
fbshipit-source-id: c3f40ee
Summary: This is to prevent test failures to happen whenchanging the code a little.
Reviewed By: sblackshear
Differential Revision: D5815349
fbshipit-source-id: 8516102
Summary:
This approach was requiring the `InferArray` class to always be part of the classpath, and the only benefit was to preserve the length of the arrays, when known, on calls to `clone()` method. However, adding it to the models would create circular dependencies between the models, the builtins and the tests.
The code is now simpler and we can more aggressively fail when classes that are supposed to be found from the classpath are not found.
Reviewed By: sblackshear
Differential Revision: D5703173
fbshipit-source-id: 3e6cea5
Summary:
Saw these two types of errors before (but they're hard to reproduce locally) when building the models:
- `ERROR: Zip.Error("/mnt/btrfs/trunk-git-infer-739-1503054473/infer/bin/../lib/java/models.jar", "", "end of central directory not found, not a ZIP file")`. I think this means infer reads a partially-written models jar. We shouldn't try to load this in models mode.
- `install` would complain that the destination already exists. I think this can only happen if there's a race and the file gets created between when install first checks and when it tries to write to it.
This made me realise that the some of the models are computed in C and C++ mode
and we pick one computed spec arbitrarily. That sounds a bit dodgy but at least
now we do so in a non-racy way.
Reviewed By: jeremydubreil
Differential Revision: D5658389
fbshipit-source-id: 8077279
Summary: Using a dedicated abstract domain, like Quandary does, is more suitable for taint analysis.
Reviewed By: sblackshear
Differential Revision: D5473794
fbshipit-source-id: c917417
Summary: This fixes a couple of false positives as objects of BufferedReader don't need to be closed if the wrapped reader resource gets closed correctly.
Reviewed By: sblackshear
Differential Revision: D5106596
fbshipit-source-id: 725fb80
Summary: Useful to have Eradicate and Biabduction agree on how to inform that the analysis that some objects are not null.
Reviewed By: sblackshear
Differential Revision: D5075127
fbshipit-source-id: 9e56981
Summary:
It can be useful when debugging infer or the Makefiles themselves to see what
`make` is doing. Instead of editing Makefiles to remove `@` now you can `make
VERBOSE=1`.
This is just `git ls-files | grep -e Makefile -e '.*\.make' | xargs sed -e 's/^\t@/\t$(QUIET)/' -i`, and adding the definition of `QUIET` to Makefile.config.
Reviewed By: jeremydubreil
Differential Revision: D4779115
fbshipit-source-id: e6e4642
Summary:
This makes sure that one can run `./build-infer.sh` then `make`. Otherwise it's
not always clear what one should do to recompile infer, eg when `make` will
work and when `./build-infer.sh` should be used instead, in particular when the
user doesn't have opam configured for her terminal.
Reviewed By: jberdine
Differential Revision: D4698159
fbshipit-source-id: 5df8059
Summary:
This is helpful to make sure tests are up to date wrt the models.
Also made the Java deps depend on the models.jar instead of the model sources
as that's what the tests will be using. In particular, updating the sources of
the models will not update the results of a test unless someone rebuilds
models.jar, so rerunning the tests when the models haven't been rebuilt is
useless.
Reviewed By: akotulski
Differential Revision: D4635129
fbshipit-source-id: 75b4ab6
Summary:
The Java models for resources are way to complex. The main issue I am facing with these models is that small changes in the analysis can affect the generation of the models in some weird ways. For instance, I get different specs for some of the models between my devserver and my devvm, which seems to be mostly related with the backend treatment of `instanceof`.
The objective here is to simplify the models as much as possible in order to:
1) make debugging regressions easier
2) get simpler specs and less modeled methods shipped in `models.jar`
Reviewed By: sblackshear
Differential Revision: D4536115
fbshipit-source-id: 577183a
Summary: The diff remove the no-op model for `Cursor.close()` by the frontend-based `Closeable` as resources mechanism where every call of the form `object.close()` removes the file attribute on `object` when `object` is of type `Closeable`.
Reviewed By: sblackshear
Differential Revision: D4519386
fbshipit-source-id: 83633d4
Summary: Those should be treated angelically during the analysis with the same end results
Reviewed By: sblackshear
Differential Revision: D4518930
fbshipit-source-id: ee5bae8
Summary: Not clear why we need to disable this case and in which case is Infer creating too many disjunctions.
Reviewed By: sblackshear
Differential Revision: D4509394
fbshipit-source-id: fbc106d
Summary:
Turns this was needed only because we want infer-out to be models/infer.
Passing `--buck` together with passing `-d models` to `javac` was achieving the
same thing in a more roundabout way.
Reviewed By: jeremydubreil
Differential Revision: D4423185
fbshipit-source-id: 7cafe3b
Summary: Need to upgrade in order to specify some taint properties on a more recent `WebView` API.
Reviewed By: cristianoc
Differential Revision: D4382590
fbshipit-source-id: 0925742
Summary: Use the lazy dynamic dispatch by default in prod for the Java analysis
Reviewed By: sblackshear
Differential Revision: D4356872
fbshipit-source-id: 491e92e
Summary: Using multicore introduces some flakiness when building the models. This leads to summries for the models that are not always the same after rebuidling from scratch.
Reviewed By: jberdine
Differential Revision: D4306468
fbshipit-source-id: 96933d6
Summary:
The way interfaces are dealt with led to a false positive,
where tryLock() works OK for a Lock but not for a ReentrantLock.
The solution is just to provide the model.
While I am at it I am adding some more standard tests for Lock and ReentrantLock, which were not present.
Reviewed By: sblackshear
Differential Revision: D4204551
fbshipit-source-id: 9b6de28
Summary:
`install` will not do anything if the file didn't change, which should give
`make` more opportunities to not do work.
Reviewed By: jeremydubreil
Differential Revision: D4161918
fbshipit-source-id: 9b9061a
Jules Villard
Josh Berdine
Mehdi Bouaziz
Jeremy Dubreil
Sam Blackshear
Peter O'Hearn