Summary:
We lost InferClang++ a long time ago... It was installed properly on `make
install` but not during normal compilation!
Reviewed By: akotulski
Differential Revision: D4905947
fbshipit-source-id: 56375c2
Summary:
The error was complaining about a missing `etree` package but that's actually
part of the `lxml` package and that wasn't clear from the output.
See for instance https://github.com/facebook/infer/issues/635
Reviewed By: martinoluca
Differential Revision: D4905953
fbshipit-source-id: 28b26af
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:
These were showing up as allocation huge amounts of memory on some analysis
profiles from OpenSSL using Spacetime. Doesn't hurt to make them allocate less.
Reviewed By: jeremydubreil
Differential Revision: D4884520
fbshipit-source-id: e79b815
Summary:
Running `infer --help` with spacetime showed that `Str` was a hog. And indeed perf is 74% better now:
```
before:
bash -c 'for i in $(seq 100); do infer --help > /dev/null 2>/dev/null; done' 28.02s user 0.62s system 98% cpu 29.205 total
after:
bash -c 'for i in $(seq 100); do infer --help > /dev/null 2>/dev/null; done' 6.34s user 0.64s system 92% cpu 7.557 total
```
Running on many files one after the other is now 64% faster too:
```
$ cd infer/tests/codetoanalyze/c/errors
$ # before
$ rm -fr infer-out && time bash -c 'for src in */*.c; do infer -a capture --continue -- clang -c $src; done'
bash -c 7.77s user 0.66s system 97% cpu 8.647 total
$ # after
$ rm -fr infer-out && time bash -c 'for src in */*.c; do infer -a capture --continue -- clang -c $src; done'
bash -c 2.35s user 0.56s system 93% cpu 3.119 total
$ time infer -a capture -- clang -c */*.c
infer -a capture -- clang -c */*.c 0.54s user 0.20s system 99% cpu 0.737 total
```
Reviewed By: mbouaziz
Differential Revision: D4875803
fbshipit-source-id: cfcfa69
Summary:
OCaml 4.04.0 new warnings raised a few valid points!
Fixing warning 57 in two ways:
- best way: introduce an auxiliary function to avoid code duplication
- not-so-best way: introduce code duplication. I did that when the branches body are small. Typically the number of bound variables in the pattern is high, so an auxiliary function would need to take many arguments and the whole thing will not be readable (we'd still duplicate the arguments we pass to the function for instance).
Reviewed By: jberdine
Differential Revision: D4851006
fbshipit-source-id: fbf1867
Summary:
Limit the use of `SourceFile.invalid` (renamed from `SourceFile.empty`) as much
as possible. In particular, do not generate bogus procnames for external global
variables: their translation unit was set to the invalid source file, now we
distinguish between extern/non-extern global variables more explicitly.
`SourceFile.invalid` is still used in too many places to actually remove it, often as a dummy initial value that never gets used, but sometimes as an actual value... Worse, we cannot fail on all operations on `SourceFile.Invalid` yet: the `SourceFile.to_string` method is used in too many places where it could get `SourceFile.Invalid` as argument. It's easy to see where it's used by making it raise in the code, then running the tests. This results in spaghetti backtraces that are hard to trace back to a root cause.
Reviewed By: akotulski, jeremydubreil
Differential Revision: D4860019
fbshipit-source-id: 45be040
Summary:
Try to read .inferconfig in the current directory, then in .., then in ../..,
etc. This can be overriden with the `INFERCONFIG` environment variable.
This removes the need for two-phase parsing, so clean up that code too.
Paths in .inferconfig are interpreted relative to where .inferconfig is located.
This does not apply to other path-sensitive things like regexpes... this is not
a show stopper because regexpes can account for the fact that infer may be
called from different project roots.
Make sure we fail when .inferconfig exists but cannot be read.
Reviewed By: jberdine
Differential Revision: D4843142
fbshipit-source-id: 340a63f
Summary: The flakiness is exercised by upgrading the OCaml compiler to 4.04.0.
Reviewed By: jberdine
Differential Revision: D4859904
fbshipit-source-id: 0dd7ff6
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 is required to upgrade OCaml as our ancient Reason is not available on 4.04.0.
Reviewed By: yunxing
Differential Revision: D4851582
fbshipit-source-id: 994a9a8
Summary:
It's distracting to see the debug HTML for the preanalysis when you're trying to debug something else.
Also, it breaks the nice bi-abduction debug feature of marking the visited nodes as green.
Reviewed By: akotulski
Differential Revision: D4858578
fbshipit-source-id: 8e77976
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: Prereq for reporting a call stack for both the read and write in a read/write race.
Reviewed By: peterogithub
Differential Revision: D4845603
fbshipit-source-id: ebfeb9b
Summary:
We shouldn't encourage contributors to run only a subset of the tests with
`make test`, but it's more helpful to complain clearly should they try to do
so.
Now `make test` will ensure that both the clang and the Java analyzers are
enabled, otherwise it will refuse to run and suggest to run `make config_tests`
instead.
It can still be useful to be able to run only the Java or Clang tests. The diff
also fixes the cases where that previously failed.
Fixes#634
Reviewed By: jberdine
Differential Revision: D4826515
fbshipit-source-id: 4b76029
Summary:
This debugger stops the execution of CTL during the evaluation of formulas, then shows useful info about the current state:
- Which formula is being evaluated
- In which part of the AST is such formula being evaluated
- Line number of the source file
- Whether a CTL-Transition will take place or not
- Node-ID that can be related to the dotty file containing the evaluation graph (the one in infer-out/lint_dotty/)
The AST is shown with coloured nodes, where each colour has the following meaning:
- [Default terminal colour], Bold: The node is being evaluated
- Green, Bold: The formula returned true on the current node
- Red, Bold: The formula returned false on the current node
Reviewed By: ddino
Differential Revision: D4834451
fbshipit-source-id: c9aa970
Summary:
Make it possible to write one model which will be used by all template instantiations.
There is one big missing piece: infer never tries to do template instantiation by itself. With current code, it's possible to use generic models
as long as header contains `__infer_generic_model` annotation (see the test as an example).
This is not viable to modify all headers with this annotation hence infer will try to do template instantiation for generic models in later diffs.
Reviewed By: jberdine
Differential Revision: D4826365
fbshipit-source-id: 2233e42
Summary:
Initial version of naming, required for generic models. It's simply non mangled name stripped from any template arguments.
This makes it impossible to have two generic models with
1. different template arguments
2. different overloads (function with same name, but different types of arguments)
Reviewed By: jberdine
Differential Revision: D4826358
fbshipit-source-id: 42ac763
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: `__attribute__((annotate("")))` is better way of passing information to the frontend
Reviewed By: jberdine
Differential Revision: D4818805
fbshipit-source-id: 6e8add2
Summary:
- Do not print OCaml backtrace unless in developer mode.
- Print javac output when it fails.
- Refactor Javac.ml so that rerunning the command doesn't duplicate code.
The output of the clang and Javac integration is good, the output for mvn is
ok, the output for Buck is still fairly "meh".
Reviewed By: jberdine
Differential Revision: D4818722
fbshipit-source-id: 1973b93
Summary: This will avoid the redefine this Map and Set module as pretty printable when used to create abstract domains.
Reviewed By: sblackshear
Differential Revision: D4811849
fbshipit-source-id: e2f6763
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:
Currently --per-procedure-parallelism defaults to a chunk size of 1
procedure, which has a high overhead. Add a command line option to
control it, and raise the default value.
Reviewed By: jvillard
Differential Revision: D4794692
fbshipit-source-id: 7715a40
Summary:
Otherwise, we can get an exception when calling `Fieldname.java_get_field`.
Thanks to ngorogiannis for reporting.
Reviewed By: jeremydubreil
Differential Revision: D4805197
fbshipit-source-id: 3141bb1
Summary: This representation is more natural and results in less `List.rev` calls.
Reviewed By: jberdine
Differential Revision: D4762629
fbshipit-source-id: 481cbe4
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:
This checker was always running by default but was apparently never reporting.
This checkers can always be run using:
infer -a checkers --checkers-repeated-calls -- ...
Reviewed By: sblackshear
Differential Revision: D4782472
fbshipit-source-id: 5ec77f4
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:
Add support for Makefiles to the copyright linter. Makefiles are a bit
different than shell because they should start with the copyright notice
straight away (whereas shell starts with the #! stuff).
Reviewed By: mbouaziz
Differential Revision: D4786620
fbshipit-source-id: 504dc23
Summary:
Nuking the specs then building the models was not a great idea: the models do
not look at specs but only at some dummy marker files, eg
infer/lib/specs/c_models, so they don't necessarily realize that they need to
be rebuilt when the specs have been nuked!
One easy workaround would be to also delete the marker files, but then we would
*always* rebuild the models when building infer. Not good.
The solution here is to nuke the specs and marker files only when the clang
dependencies change, then rebuild all the models.
Reviewed By: jberdine, jeremydubreil
Differential Revision: D4781424
fbshipit-source-id: 2d2606e
Summary:
We shouldn't install byte-executables unless the user types `make byte`.
Othewise everything gets very slow and the cause is not obvious.
Reviewed By: jeremydubreil
Differential Revision: D4779135
fbshipit-source-id: 757bfa2
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: We only need one "global" view of all the summaries in a file.
Reviewed By: peterogithub
Differential Revision: D4773646
fbshipit-source-id: 29e5316
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:
We can simplify the code now that the procedure callback are always executed through Ondemand. The procedure callback is still registered for Ondemand analysis by the time we run the cluster callbacks. This allows to run allows to run `Summary.read_summary`, which may run the analysis on-demand, while collecting the summaries for reporting errors.
This allows further simplifications of the Ondemand API.
Reviewed By: sblackshear
Differential Revision: D4764251
fbshipit-source-id: d0bdda4
Summary: This was annoying as "jump to next error" was otherwise always jumping to this warning about shadowing `|>`
Reviewed By: sblackshear
Differential Revision: D4767571
fbshipit-source-id: 932145c
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: Writing the summaries to disk now happens automatically during the on-demand analysis calls. So, individual checkers do not need to worry anymore about when should the analysis summaries be written to disk for the interprocedural analysis to do the right thing.
Reviewed By: sblackshear
Differential Revision: D4764337
fbshipit-source-id: 63870db
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:
Don't pass names as strings in clang frontend. Instead use QualifiedCppName which preserves
each identifier of qualified name.
Done by
1. change return type of `Cast_utils.get_qualified_name` to return `QualifiedCppName.t`
2. change types in `Typ.Name.t` and `Typ.Procname.t` to use qualified names where applicable
3. Keep changing the code until it compiles
Reviewed By: jberdine
Differential Revision: D4754242
fbshipit-source-id: 9d723cb
Summary: This call is redundant and is already done in `AbstractInterpreter`
Reviewed By: sblackshear
Differential Revision: D4754251
fbshipit-source-id: af2d11e
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:
This issue was spotted in the wild. There may be more of those, unfortunately it's hard to predict
More general problem is that types in infer frontend diverge from clang's types for DerivedToBase cast.
Then, infer uses types from clang anyway and that confuses backend. Getting it always right is very hard
Reviewed By: jvillard
Differential Revision: D4754081
fbshipit-source-id: 5fb7069
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:
Improve type of `Fieldname.t` in `Clang` variant - make it store qualified classname and method name.
Based on those changes, fix matching in `Errdesc` to use `QualifiedCppName.Match` instead of string comparisons
Reviewed By: jberdine
Differential Revision: D4746735
fbshipit-source-id: 6f52413
Summary:
Split Fieldname.t into `Java` and `Clang`. Each of them have different naming conventions and this way it's easier to differentiate between them.
Make `Java` variant store string instead of mangled since mangled part was always empty
Changes to `Clang` variant are coming in the next diff
Reviewed By: jeremydubreil
Differential Revision: D4746708
fbshipit-source-id: c5858a8
Summary:
Reorganize by using a top-level iteration over the access map and using a helper function for updating the caller accesses.
The new code is shorter and much more readable.
Reviewed By: peterogithub
Differential Revision: D4740657
fbshipit-source-id: 8e18cd5
Summary: Add `QualifiedCppName.t` and some functions to manipulate it. More places will start using this type (such as `Procnames` or `Typ.Name`) in later diff
Reviewed By: jberdine
Differential Revision: D4738991
fbshipit-source-id: 8f20dd6
Summary:
All tests were redirecting `stderr` into duplicates.txt which made it much harder to see other error messages in stderr (such as uncaught exceptions).
To mitigate it, write duplicates to separate file and don't redirect `stderr` to another file.
Reviewed By: jvillard
Differential Revision: D4728938
fbshipit-source-id: 8ad2fc8
Summary: There was a lot of indirection going on in `Typ.Name` type definition. Inline all those indirections into single variant type
Reviewed By: jberdine
Differential Revision: D4737644
fbshipit-source-id: c5e181b
Summary: Now that all the checkers are now run in a way that will prevent conflicts between them, we can make this change that was breaking the analysis.
Reviewed By: jvillard
Differential Revision: D4621953
fbshipit-source-id: f17c729
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
Summary: That tuple has 3 elements already, there may be 4th element coming.
Reviewed By: mbouaziz
Differential Revision: D4721342
fbshipit-source-id: cba44ef
Summary:
This removes the dependency of libffi, and gives better guarantees at
compile-time. A bit overkill to retrieve the width of the terminal but what do
you know...
Reviewed By: jberdine
Differential Revision: D4700003
fbshipit-source-id: 036989b
Summary:
Two issues in the previous code:
1. We'd just tack on `#compilation-database` so if there already are `#flavors`
in a Buck target then we get a malformed `#flavors#compilation-database`
instead of `#flavors,compilation-database`. There's already code to deal
with that for other flavors (`#infer-capture-all`), so extend and reuse that.
2. The code didn't work if there are spaces in target names (sigh). Harden the
code a bit so that it works. Unfortunately Buck doesn't escape spaces at all
in its `buck targets --show-output` output, so the parsing still relies on
there being no spaces in flavors to work correctly. Sample output:
```
$ buck targets --show-full-output //clang_compilation_database:Hel\ lo#compilation-database
Not using buckd because watchman isn't installed.
[+] PROCESSING BUCK FILES...0.1s [100%] 🐳 New buck daemon
//clang_compilation_database:Hel lo#compilation-database /home/jul/infer/infer/tests/build_systems/codetoanalyze/buck-out/gen/clang_compilation_database/__Hel lo#compilation-database.json
```
Also, some code in codetoanalyze/clang-compilation-database/ didn't compile, so
fix that.
Reviewed By: dulmarod
Differential Revision: D4714338
fbshipit-source-id: b8ae324
Summary:
These are mentioned on fbinfer.com so IMHO should be displayed when running infer -h
Closes https://github.com/facebook/infer/pull/617
Differential Revision: D4697682
Pulled By: jvillard
fbshipit-source-id: 3d7dd7b
Summary:
It is definitely useful to collect information about how long the analysis of every procedure takes. It allows to detect and focus on outliers when trying to improve performance. However, this kind of information could be collected using a standard logging mechanism and does not need to be stored within the analysis artifacts.
I intend to add some form of similar logging in the context of #16348004 once we can get every analysis procedure analyzed through the `Ondemand` module. In this case, it would be easy to have a single place to log how does the analysis of a procedure take.
Reviewed By: jberdine
Differential Revision: D4636755
fbshipit-source-id: 01f3bca
Summary: Now, running `infer -a checkers -- ...` will also run the ThreadSafety checker
Reviewed By: sblackshear
Differential Revision: D4691330
fbshipit-source-id: 04fc781
Summary: Fail early when there is no registered callbacks to run the analysis of a procedure on-demand
Reviewed By: sblackshear
Differential Revision: D4573726
fbshipit-source-id: a8ee74b
Summary: Run all the checkers one after each other, which allows the Infer AI framework to run several checkers together, including the possibility for them to collaborate.
Reviewed By: sblackshear
Differential Revision: D4621838
fbshipit-source-id: e264d67
Summary:
This option is not needed anymore as it was introduced to counter an uncovered
perf issue with creating human readable reports. The perf issue has been
addressed.
Instead of this option, one can use `infer --report-hook /bin/true ...` to
disable reporting. However, right now the Buck integration doesn't honor it so
this would need to be fixed to be a true equivalent of `--disable-bug-list`.
Reviewed By: jberdine
Differential Revision: D4712877
fbshipit-source-id: a09304f
Summary: This is dead code, and depends on libffi which we could get rid of otherwise.
Reviewed By: jberdine
Differential Revision: D4705645
fbshipit-source-id: efd28ef
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
Sam Blackshear
Jules Villard
Peter O'Hearn
Josh Berdine
Mehdi Bouaziz
Dulma Churchill
Dino Distefano
Andrzej Kotulski
Martino Luca
htxs
Jeremy Dubreil
Paco Estevez Garcia
Cristiano Calcagno
Kihong Heo
Matthew Haughton