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:
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
Jules Villard
Josh Berdine
Sam Blackshear
Dulma Churchill
Dino Distefano
Andrzej Kotulski
Martino Luca
Jeremy Dubreil