Summary:
We previously lumped ownership predicates in with all other predicates. That limited us to a flat ownership domain.
This diff separates out the ownership predicates so we can have a richer lattice of predicates with each access path.
This lets us be more precise; for example, we can now show that
```
needToOwnBothParams(Obj o1, Obj o2) {
Obj alias;
if (*) { alias = o1; } else { alias = o2; }
alias.f = ... // both o1 and o2 need to be owned for this to be safe
}
void ownBothParamsOk() {
needToOwnBothParams(new Obj(), new Obj()); // ok, would have complained before
}
```
is safe.
Reviewed By: jberdine
Differential Revision: D5589898
fbshipit-source-id: 9606a46
Summary:
Use jbuilder to build infer instead of ocamlbuild. This is mainly to get faster builds:
```
times in 10ms, ±differences measured in speedups, 4 cores
| | ocb total | jb | ±total | ocb user | jb | ±user | ocb cpu | jb | ±cpu | ocb sys | jb | ±sys |
|-----------------------------------+-----------+------+--------+----------+------+-------+---------+-----+------+---------+------+------|
| byte from scratch | 6428 | 2456 | 2.62 | 7743 | 6662 | 1.16 | 138 | 331 | 2.40 | 1184 | 1477 | 0.80 |
| native from scratch | 9841 | 4289 | 2.29 | 9530 | 8834 | 1.08 | 110 | 245 | 2.23 | 1373 | 1712 | 0.80 |
| byte after native | 29578 | 1602 | 18.46 | 4514 | 4640 | 0.97 | 170 | 325 | 1.91 | 543 | 576 | 0.94 |
| change infer.ml byte | 344 | 282 | 1.22 | 292 | 215 | 1.36 | 96 | 99 | 1.03 | 040 | 066 | 0.61 |
| change infer.ml native | 837 | 223 | 3.75 | 789 | 174 | 4.53 | 98 | 99 | 1.01 | 036 | 47 | 0.77 |
| change Config.ml byte | 451 | 339 | 1.33 | 382 | 336 | 1.14 | 97 | 122 | 1.26 | 056 | 80 | 0.70 |
| change Config.ml native | 4024 | 1760 | 2.29 | 4585 | 4225 | 1.09 | 127 | 276 | 2.17 | 559 | 644 | 0.87 |
| change cFrontend_config.ml byte | 348 | 643 | 0.54 | 297 | 330 | 0.90 | 96 | 67 | 0.70 | 038 | 102 | 0.37 |
| change cFrontend_config.ml native | 1480 | 584 | 2.53 | 1435 | 906 | 1.58 | 106 | 185 | 1.75 | 136 | 178 | 0.76 |
#+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2
50 cores
| | ocb total | jb | ±total | ocb user | jb | ±user | ocb cpu | jb | ±cpu | ocb sys | jb | ±sys |
|---------------------+-----------+------+--------+----------+------+-------+---------+----+------+---------+------+------|
| byte from scratch | 9114 | 2061 | 4.42 | 9334 | 5133 | 1.82 | | | 0/0 | 2566 | 1726 | 1.49 |
| native from scratch | 13481 | 3967 | 3.40 | 12291 | 7608 | 1.62 | | | 0/0 | 3003 | 2100 | 1.43 |
| byte after native | 3467 | 1476 | 2.35 | 5067 | 3912 | 1.30 | | | 0/0 | 971 | 801 | 1.21 |
#+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2
```
Menu:
1. Write a jbuild file, autogenerated from jbuild.in because we need to fill in
some information at build-time (really, at configure time, but TODO), such as
whether or not clang is enabled.
2. Nuke lots of stuff from infer/src/Makefile that is now in the jbuild file
3. The jbuild file lives in infer/src/ so it can see all the sources. If we put it somewhere else, eg, infer/, then `jbuilder` scans too many files (all irrelevant) and takes 2.5s to start instead of .8s. Adding irrelevant directories to jbuild-ignore does not help.
4. jbuilder does not support subdirectories, so resort to listing all the
source files in the generated jbuild (only source directories need to be
manually listed in jbuild.in though). Still, the generated .merlin is wrong
and makes merlin find source files in _build, so manually tune it to get
good merlin support. We also lose some of merlin for unit tests as it
cannot see their build artefacts anymore.
5. checkCopyright gets its own jbuild because it's standalone. Also, remove
some deprecation warnings in checkCopyright due to the new version of Core from
a while ago.
6. Drop less-used Makefile features (they had regressed anyway) such as
building individual modules. Also, building mod_dep.pdf now takes all the
source files available so they better build (before, it would only take the
source files from the config, eg with or without clang) (that's pretty minor).
7. The toplevel is now built as a custom toplevel because that was easier. It
should soon be even easier: https://github.com/janestreet/jbuilder/issues/210
8. Move BUILTINS.mli to BUILTINS.ml because jbuilder is not happy about
interface files without implementations.
In particular, I did not try to migrate too much of the Makefile logic to jbuilder,
more can be done in the future.
Reviewed By: jberdine
Differential Revision: D5573661
fbshipit-source-id: 4ca6d8f
Summary:
When a sink name is specified in `.inferconfig` or in OCaml, it might conflict with a function of the same name that has a different number of args.
We shouldn't try to create a sink in this case, and we definitely shouldn't crash.
Reviewed By: jeremydubreil
Differential Revision: D5561216
fbshipit-source-id: fa1859b
Summary: Those are not particularly relevant for the biabduction analysis. It would be easy to have a dedicated checker for this if we happen to need one day.
Reviewed By: sblackshear
Differential Revision: D5530834
fbshipit-source-id: 316e60f
Summary:
The Eradicate `Nullable` checker should now be run using:
infer -a checkers --eradicate ...
Reviewed By: mbouaziz
Differential Revision: D5529226
fbshipit-source-id: 0de2956
Summary:
This is unsound but will help the analysis to report less false alarms with the common pattern:
if (a.get() != null) {
a.get().foo();
}
Reviewed By: sblackshear
Differential Revision: D5528227
fbshipit-source-id: 750db4a
Summary: This was reusing the side effects of the `add_constraints_on_retval` for the final purpose of being angelic and just assigning a fresh value to the lhs of the load.
Reviewed By: sblackshear
Differential Revision: D5507037
fbshipit-source-id: ec1c89c
Summary:
Works the same way as read/write races on fields, except that are more relaxed (er, unsound) in deciding whether two containers may alias.
This is needed to avoid reporting a ton of FP's; full explanation in comments.
Reviewed By: da319
Differential Revision: D5493404
fbshipit-source-id: 0a5d8b1
Summary:
The way we represented container writes before was pretty hacky: just use a dummy field for the name of the method that performs the container write.
This diff introduces a new access kind for container writes that is much more structured.
This will make it easier to soundly handle aliasing between containers and support container reads in the near future.
Reviewed By: da319
Differential Revision: D5465747
fbshipit-source-id: e021ec2
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: We get the wrong answer on most of them for now, but that is expected
Reviewed By: ngorogiannis
Differential Revision: D5429242
fbshipit-source-id: 4899079
Summary:
This just makes the warnings silent for now. We may improve the analysis to check if the null check on the captured fields are consistent with the annotation on the corresponding parameters.
Eradicate also has the same issue. I added a test to outline this. The biabduction analysis will also probably fail on the same of annotation lookup. We may want implement the proper fix at the level of `Annotation.field_has_annot`.
Reviewed By: sblackshear
Differential Revision: D5419243
fbshipit-source-id: 6460de8
Summary: Adding to the Quandary tests, the list of tests that are already working for the bi-abduction based taint analysis.
Reviewed By: sblackshear
Differential Revision: D5395734
fbshipit-source-id: c4f2e79
Summary: We had a model for `Pools.SimplePool`, but were missing models for `Pools.Pool`. Since `SimplePool` and `SynchronizedPool` both extend `Pool`, modeling it should cover all of the cases.
Reviewed By: ngorogiannis
Differential Revision: D5236280
fbshipit-source-id: 9bbdb25
Summary:
:
No longer use deprecated reporting function for the suggest nullable checker
Depends on D5205009
Reviewed By: grievejia
Differential Revision: D5205843
fbshipit-source-id: f6dd059
Summary:
Read/write race errors should always show one trace for a read and one trace for a write.
We forget to pass the conflicting writes to the reporting function in one case, which prevented us from showing a well-formed trace.
Fixed it by making the `conflicts` parameter non-optional
Reviewed By: jberdine
Differential Revision: D5209332
fbshipit-source-id: 05da01a
Summary: We were almost always using `~report_reachable:true`, and in the cases where we weren't it is fine to do so. In general, a sink could read any state from its parameters, so it makes sense to complain if anything reachable from them is tainted.
Reviewed By: mbouaziz
Differential Revision: D5169067
fbshipit-source-id: ea7d659
Summary:
For now, we just support clearing the taint on a return value.
Ideally, we would associate a kind with the sanitizer and only clear taint that matches that kind.
However, it's fairly complicated to make that work properly with footprint sources.
I have some ideas about how to do it with passthroughs instead, but let's just do the simple thing for now.
Reviewed By: jeremydubreil
Differential Revision: D5141906
fbshipit-source-id: a5b8b5e
Summary: Using Conjunction for thread join has known false negatives. Finer grained recording of threading information fixes this.
Reviewed By: sblackshear
Differential Revision: D5111161
fbshipit-source-id: aab483c
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:
First step to be able to enable and disable the checkers to run in the following form:
> infer -a checkers --checker1 --checker2 --checker3 -- ...
and have a predefined list of checkers that are run by default with:
> infer -a checkers -- ...
Reviewed By: sblackshear
Differential Revision: D5007377
fbshipit-source-id: d7339ef
Summary:
Before we understood ownership, we needed this to avoid a mountain of Builder-related FP's.
Now that we have fairly sophisticated understanding of ownership, we can kill this hack.
Reviewed By: jaegs
Differential Revision: D4940238
fbshipit-source-id: 8d86e57
Summary: The purpose of the annotation reachability analysis is to report when a method annotated with `X` never calls, directly or indirectly, another method annotated with `Y`. However, there can be different call stacks following different execution paths from `X` to `Y`. Reporting more than one call stack ending with the same annotated procedure does not bring more signal to the end user. So the purpose of this diff is to avoid those duplicated reports and report at most one annotation reachability issue per end of call stack.
Reviewed By: sblackshear
Differential Revision: D4942765
fbshipit-source-id: 46325a7
Summary: Sawja assigns them on multiple control-flow paths, so they're not SSA.
Reviewed By: peterogithub
Differential Revision: D4896745
fbshipit-source-id: c805216
Summary:
There are false positives in the current analysis due to the
use of conjunction in the treatment of threaded. Changing conjunction to disjunction
removes these false positives. Some new false negatives arise, but all the old tests pass.
This is a stopgap towards a better solution being planned.
Reviewed By: sblackshear
Differential Revision: D4883280
fbshipit-source-id: c2a7e6e
Summary:
If we couldn't project the callee access path into the caller during summary application, we still added the corresponding trace to the caller state.
This was wasteful; it just bloats the caller with state it will never look at.
Fixed it by making `get_caller_ap_node` return `None` when the state won't be visible in the caller.
Reviewed By: jeremydubreil
Differential Revision: D4727937
fbshipit-source-id: 87665e9
Summary: This should make the reports much easier to understand. We can generalize to reporting a stack trace for all of the writes in the future if we wish.
Reviewed By: peterogithub
Differential Revision: D4845641
fbshipit-source-id: 589fdbc
Summary: If two public methods touch the same state and only one is marked `ThreadSafe`, it's reasonable to report unsafe accesses on both of them.
Reviewed By: peterogithub
Differential Revision: D4785038
fbshipit-source-id: 5a80da4
Summary:
*Unless* the unprotected write runs on the main thread and the read doesn't.
Otherwise, we'll already report on the unprotected write, and we don't want to duplicate.
Reviewed By: peterogithub
Differential Revision: D4798357
fbshipit-source-id: 5de06a0
Summary:
This is step further simplify the code to avoid cases where the summary of the procedure being analyzed can exist in two different versions:
# one version is the summary passed as parameter to every checker
# the other is a copy of the summary in the in-memory specs table
This diff implements:
# the analysis always run through the `Ondemand` module (was already the case before)
# the summary of the procedure being analyzed is created at the beginning of the on-demand analysis call
# all the checkers run in sequence, update their respective part of the payload and log errors to the error table
# the summary is store at the end of the on-demand analysis call
Reviewed By: sblackshear
Differential Revision: D4787414
fbshipit-source-id: 2d115c9
Summary:
Adds a new type and branching for a missing path of execution.
closes#575
Reviewed By: jvillard
Differential Revision: D4738681
fbshipit-source-id: f72344c
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:
No new functionality here; mostly `FN_` tests documenting our current limitations.
Will start chipping away at the false negatives in follow-up diffs.
Reviewed By: peterogithub
Differential Revision: D4780013
fbshipit-source-id: 7a0c821
Summary: Bringing the logic back to where it was before the big refactoring of the reporting logic.
Reviewed By: peterogithub
Differential Revision: D4774541
fbshipit-source-id: afeaaf8
Summary:
Move all of the reporting on top of the aggregation functionality.
This lets us delete lots of code
Reviewed By: peterogithub
Differential Revision: D4772223
fbshipit-source-id: 47cc51a
Summary:
This was the one type of races we were not yet reporting (besides ones that use the wrong synchronization :)).
Wrote new utility function to aggregate all accesses by the memory they access.
This makes it easy to say which accesses we should report and what their conflicts are.
Eventually, we can simplify the reporting of other kinds of unsafe accesses using this structure.
Reviewed By: peterogithub
Differential Revision: D4770542
fbshipit-source-id: 96d948e
Summary:
For collections whose type does not express that the collection is thread-safe (e.g., `Collections.syncrhonizedMap` and friends).
If you annotate a field holding one of these collections, we won't warn when you mutate the collection.
Reviewed By: jeremydubreil
Differential Revision: D4763565
fbshipit-source-id: 58b487a
Summary: It seems that we were not really using the `Bottom` part of the domain as a pair of (empty call map, empty tracking var map) was already acting as bottom.
Reviewed By: sblackshear
Differential Revision: D4759757
fbshipit-source-id: 53dedfe
Summary:
Most of our tests work by comparing the output of some command to a baseline
expected output. It's often needed to update that baseline.
Previously, that was crudely done by attempting to move every foo.exp.test file
to foo.exp. This does not work terribly well, in particular because
foo.exp.test might be stale.
Instead, add a `replace` target to every test that knows how to update the
baseline. This allows custom behaviours too, eg in the differential tests.
Most of the tests include base.make or differential.make, so add a replace target
there. A few tests are completely custom, add a replace target to them too.
Reviewed By: jeremydubreil
Differential Revision: D4754279
fbshipit-source-id: ec34273
Summary:
If I read off the main thread and write on the main we
could have a race. (Writes off main are already reported.)
Reviewed By: sblackshear
Differential Revision: D4746138
fbshipit-source-id: 8b6e9c5
Summary:
One limitation of Eradicate is that certain nullability patterns are not expressible using simply the `Nullable` annotation.
One such pattern is using the knowledge that a function returns null when passed null, but returns an object otherwise.
The annotation `PropagatesNullable` is a variant of `Nullable` applied to parameters when their value propagates to the return value.
A method annotated
```
B m(PropagatesNullable A x) { return x == null ? x : B(x); }
```
indicates that `m` returns null if `x` is null, or an object of class `B` if the argument is not null.
Examples with multiple parameters are in the test cases.
This diff builds some infrastructure for annotation transformers: the example above represents the identity function on nullability annotations.
Reviewed By: jvillard
Differential Revision: D4705938
fbshipit-source-id: 9f6194e
Summary:
Before, `trace_of_pname` only grabbed unprotected writes from the summary, so the traces ending in an unprotected read were truncated.
We now look at reads too when appropriate.
Reviewed By: peterogithub
Differential Revision: D4719740
fbshipit-source-id: 28f6e63
Sam Blackshear
Jules Villard
Jeremy Dubreil
azhdar
Kyriakos Nikolaos Gkorogiannis
Jia Chen
Peter O'Hearn
Paco Estevez Garcia
Martino Luca
Cristiano Calcagno