Summary:
The "placement new" operator `new (e) T` constructs a `T` in the pre-allocated memory address `e`.
We weren't translating the `e` part, which was leading to false positives in the dead store analysis.
Reviewed By: dulmarod
Differential Revision: D5814191
fbshipit-source-id: 05c6fa9
Summary:
With flambda (`-O3`), compilation time is ~5x slower, but the backend is ~25% faster!
To mitigate the atrocious compilation times, introduce a new `opt` build mode in the jbuilder files.
- build in "opt" mode by default from the toplevel (so that install scripts and external users get the fastest infer by default), in "default" mode by default from infer/src (since the latter is only called directly by infer devs, for faster builds)
- `make byte` is as fast as before in any mode
- `make test` will build "opt" by default, which is very slow. Solution for testing (or building the models) locally: `make BUILD_MODE=default test`.
- You can even change the default locally with `export BUILD_MODE=default`.
The benchmarks are to be taken with a sizable pinch of salt because I ran them only once and other stuff could be running in the background. That said, the perf win is consistent across all projects, with 15-20% win in wallclock time and around 25% win in total CPU time, ~9% win in sys time, and ~25% fewer minor allocations, and ~5-10% fewer overall allocations. This is only for the backend; the capture is by and large unaffected (either the same or a tad faster within noise range).
Here are the results running on OpenSSL 1.0.2d on osx (12 cores, 32G RAM)
=== base
infer binary: 26193088 bytes
compile time: 40s
capture:
```lang=text
real 1m7.513s
user 3m11.437s
sys 0m55.236s
```
analysis:
```lang=text
real 5m41.580s
user 61m37.855s
sys 1m12.870s
```
Memory profile:
```lang=json
{
...
"minor_gb": 0.1534719169139862,
"promoted_gb": 0.0038930922746658325,
"major_gb": 0.4546157643198967,
"allocated_gb": 0.6041945889592171,
"minor_collections": 78,
"major_collections": 23,
"compactions": 7,
"top_heap_gb": 0.07388687133789062,
"stack_kb": 0.3984375,
"minor_heap_kb": 8192.0,
...
}
```
=== flambda with stock options (no `-Oclassic`, just the same flags as base)
Exactly the same as base.
=== flambda `-O3`
infer binary: 56870376 bytes (2.17x bigger)
compile time: 191s (4.78x slower)
capture is the same as base:
```lang=text
real 1m9.203s
user 3m12.242s
sys 0m58.905s
```
analysis is ~20% wallclock time faster, ~25% CPU time faster:
```lang=text
real 4m32.656s
user 46m43.987s
sys 1m2.424s
```
memory usage is a bit lower too:
```lang=json
{
...
"minor_gb": 0.11583046615123749, // 75% of previous
"promoted_gb": 0.00363825261592865, // 93% of previous
"major_gb": 0.45415670424699783, // about same
"allocated_gb": 0.5663489177823067, // 94% of previous
"minor_collections": 73,
"major_collections": 22,
"compactions": 7,
"top_heap_gb": 0.07165145874023438,
"stack_kb": 0.3359375,
"minor_heap_kb": 8192.0,
...
}
```
=== flambda `-O2`
Not nearly as exciting as `-O3`, but the compilation cost is still quite high:
infer: 37826856 bytes
compilation of infer: 100s
Capture and analysis timings are mostly the same as base.
Reviewed By: jberdine
Differential Revision: D4867979
fbshipit-source-id: 99230b7
Summary:
This can be a long-running step and it's useful to know how long it took. We
already dump some statistics on stderr after merging is done, this just adds
one more line.
Reviewed By: mbouaziz
Differential Revision: D5833580
fbshipit-source-id: 70e19ab
Summary:
Simple instance of the problem: analyzing the following program times out.
```
#include <tuple>
void foo() {
std::tuple<std::tuple<int>> x;
}
```
Replacing `std::tuple<std::tuple<int>>` by `std::tuple<int>` makes the analysis
terminate.
In the AST, both tuple<tuple<int>> and tuple<int> have the same template
specialization type: "Pack" (which means we're supposed to go look into the
arguments of the template to get their values). This is not information enough
and that's the plugin fault.
On the backend side, this means that two types have the same Typ.Name.t, namely
"std::tuple<_>", so they collide in the tenv. The definition of
tuple<tuple<int>> is the one making it into the tenv. One of the fields of the
corresponding CxxRecord is of type "tuple<int>", which we see as the same
"tuple<_>", which causes the loop.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D5775840
fbshipit-source-id: 0528604
Summary:
Sort the complete set of warnings by everything except procname, then de-duplicate.
This scheme prevents reporting identical error messages on the same line/same file.
This is important for avoiding duplicate reports on multiple instantiations of the same template.
Reviewed By: jberdine
Differential Revision: D5819467
fbshipit-source-id: 984f47f
Summary: The resolution was previously only happening for constructors, but calls to private methods or to `super` are also neither static calls nor virtual calls. In this case, the resolution logic should be the same as for constructors.
Reviewed By: sblackshear
Differential Revision: D5830376
fbshipit-source-id: 9b56f80
Summary:
The reporting phases iterates over each procedure summary and print all the issues from each procedure.
That's nice because we don't have to build a big list of the issues in-memory, but it's not so nice if you want to ouput the reports in a certain order or de-duplicate them.
This diff builds the in-memory list and outputs the issues afterward. By itself, this isn't very useful. But in the near future it will allow us to:
- Group all of the issues from the same file (finally!!!)
- Get rid of duplicate issues on multiple instantiations of the same C++ template
- Probably other cool stuff too
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D5816646
fbshipit-source-id: 799bcd0
Summary:
The clang frontend uses `assert false` for unimplemented features that should
abort method translations, as well as for genuine internal errors.
Distinguishing between the two, we can fail hard on the latter and not the
former.
1. This introduces a new exception `Unimplemented` that is used instead of `assert false` where appropriate.
2. Changed some other cases into `die ...` (when there's an error message to display)
3. Wherever a path in the code that we assumed to be unreachable was observed reachable, we now raise `IncorrectAssumption`. These should be fixed, but the fixes are not obvious.
Reviewed By: sblackshear
Differential Revision: D5784384
fbshipit-source-id: 61b55af
Summary:
In the most recent version of clang plugin, lambda captures were moved from `LambdaExpr` to `CXXRecordDecl`. Updating infer to reflect this change.
update-submodule: facebook-clang-plugins
Reviewed By: jvillard
Differential Revision: D5823034
fbshipit-source-id: dd5fc45
Summary: This will run infer with `--no-keep-going` by default in our tests.
Reviewed By: sblackshear
Differential Revision: D5814237
fbshipit-source-id: c1e1a4e
Summary:
"Running as clang" was its own infer subcommand. That's not terribly good
because it makes it hard to specify another subcommand, and in particular it
broke the `compile` subcommand in some integrations because "running as clang"
would always do capture. The cmake tests required to run with `--keep-going`
because of this.
Instead of having its own fake subcommand, simply add a new boolean in the
config for "infer runs as clang", as we do for javac already (used in the mvn
integration).
Also make logging of the environment better.
Reviewed By: jberdine
Differential Revision: D5813986
fbshipit-source-id: 72b96cd
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: Destroying local variables that are out of scope after `continue`.
Reviewed By: jberdine
Differential Revision: D5804120
fbshipit-source-id: 638cff5
Summary: I often find myself needing a generic `Pp.seq` where I can specify the separator.
Reviewed By: jeremydubreil
Differential Revision: D5803915
fbshipit-source-id: fb8d30d
Summary: That match branch is Java-only but could be reached with a C++ method, causing a crash.
Reviewed By: jberdine, mbouaziz
Differential Revision: D5814041
fbshipit-source-id: 6b1b501
Summary: It's useful to be able to configure both max depth and max width
Reviewed By: jeremydubreil
Differential Revision: D5801567
fbshipit-source-id: 0138cd7
Summary:
Races on the internal implementation of data structures defined in
system headers are currently not detected, since the memory accesses
are in procedures that are not analyzed.
This diff adds models for a few std::map operations that indicate if
they read or write the underlying representation.
Reviewed By: da319
Differential Revision: D5804293
fbshipit-source-id: 55ff28c
Summary: Try to preserve the original backtrace. Introduce `reraise` in the global namespace.
Reviewed By: jberdine
Differential Revision: D5804121
fbshipit-source-id: 0947a47
Summary:
This makes it much easier to read infer logs coming from these subprocesses
that use a sub-results dir.
Reviewed By: jberdine
Differential Revision: D5777783
fbshipit-source-id: f074536
Summary: Destroying local variables that are out of scope after `break`.
Reviewed By: jberdine
Differential Revision: D5764647
fbshipit-source-id: a7e06ae
Summary: The successor node of `continue` was not correct inside the `do while`.
Reviewed By: sblackshear
Differential Revision: D5769578
fbshipit-source-id: d7b0843
Summary:
Read the documentation and it doesn't seem like these functions are guaranteed to choose the same value in different runs.
I hypothesize that these may be the source of flakiness in the thread-safety tests/smoke tests.
Reviewed By: jvillard
Differential Revision: D5794384
fbshipit-source-id: 02b7a96
Summary: With this diff, the analysis trace will jump to the definition of the skipped methods when the location is known. This is especially useful when the analysis is relying on the method annotations.
Reviewed By: sblackshear
Differential Revision: D5783428
fbshipit-source-id: 561b739
Summary: The code was previously inconsistent as passing the option was using an empty list of instructions to translate the code but still using the original JBIR representation to connect the nodes.
Reviewed By: sblackshear
Differential Revision: D5795903
fbshipit-source-id: 88c0e64
Summary:
The behaviour of infer was observed to be different in 4.04.2 vs (4.05.0 or
4.04.2+flambda). Investigating further, the behaviour is also different in byte
vs native versions of infer under 4.04.2. Looking at the Changelog of 4.05.0
(thanks mbouaziz), there are fixes for inconsistent behaviours between byte
and native relative to evaluation order.
Lots of debugging later, this 1 line patch is born. Also use `List.concat_map`
instead of re-implementing it.
Reviewed By: jberdine
Differential Revision: D5793809
fbshipit-source-id: 374fb4c
Summary: With Logging.exit you have more control of the code that invokes exit, for example when forking and running certain functions that may in turn invoke exit, and you want to handle the execution flow differently - like invoking certain callbacks before exiting, or not exiting at all.
Reviewed By: jvillard
Differential Revision: D5746914
fbshipit-source-id: 596fba1
Summary: This will prevent trivial errors like misspelling node names, e.g. when those are typed as part of the operators `IN-NODE <node-name>` or `HOLDS-IN-NODE <node-name>`
Reviewed By: dulmarod
Differential Revision: D5680411
fbshipit-source-id: e241c1c
Summary: This should be equivalent as far as bug finding is concerned, but will allow the analysis traces to jump into the skipped methods.
Reviewed By: sblackshear
Differential Revision: D5778245
fbshipit-source-id: 3fd061f
Summary:
We supported globals as sources before, but we did so by allowing ClangTrace etc. to match against any access path in the footprint of the trace.
This is very powerful/flexible, but it's ultimately not a good idea because it leads to traces that are hard to read.
This is because a footprint source doesn't have any information about its provenance: we might know that the value came from a global, but we don't know where the read occurred.
The mechanism for handling procedure calls as sources already knows how to solve this problem.
This diff implements globals as sources as a special case of procedure call sources instead.
This will give us much nicer traces with full provenance of the read from the global.
Reviewed By: mbouaziz
Differential Revision: D5772299
fbshipit-source-id: 491ae81
Summary: This is almost equivalent to the previous one except in the case where new and old are both undefined: before, we would just pick "old", but now we pick the biggest according to their source files. I think the previous behaviour was a bug because it was more non-deterministic.
Reviewed By: jberdine
Differential Revision: D5649481
fbshipit-source-id: aeb527d
Summary: It is not clear to me what the removed code was for in the first place. Basically, it was replacing the pure part of propositions in a semantically equivalent way, e.g. replacing `a = b /\ Attribute(a)` to `a = b /\ Attribute(b)`, and `a = b /\ Attribute(b)` to `a = b /\ Attribute(a)`.
Reviewed By: jberdine
Differential Revision: D5657366
fbshipit-source-id: 93cd9e0
Summary: The list of fields of a Java object in SIL is the list of fields declared in the class plus all the fields declared in the the super classes. It turns out that we were missing the fields declared in the implemented interfaces.
Reviewed By: sblackshear
Differential Revision: D5720386
fbshipit-source-id: d65c9de
Summary:
Calling `Exn.backtrace` doesn't give us the current backtrace, only the one of
the latest exception raised. Change the logic of toplevel exception catching to
print the right backtrace.
Also, do not use `Format` to print from `Config` as `Logging` may have messed
with it already.
Finally, throw in some colours!
Reviewed By: jberdine
Differential Revision: D5764825
fbshipit-source-id: cd51688
Summary: Add procedure where error is triggered (if available) + bad data to messages.
Reviewed By: jvillard
Differential Revision: D5756398
fbshipit-source-id: a16f7cf
Sam Blackshear
Jules Villard
Jeremy Dubreil
Dulma Churchill
Daiva Naudziuniene
Dino Distefano
Josh Berdine
Sungkeun Cho
Martino Luca