Summary: Parmap delivers a better scheduling, which works as a pipeline, as opposed to what existed before, which schedules processes in batches.
Reviewed By: jvillard
Differential Revision: D5678661
fbshipit-source-id: a632c71
Summary:
Suggesting to add `_Nullable` on the fields checked for, or assigned to, `nullptr` will allow the biabduction analysis to report null dereferences that are related to the lifetime of objects.
Depends on D5832147
Reviewed By: sblackshear
Differential Revision: D5836538
fbshipit-source-id: c1b8e48
Summary: The prune nodes where translated as `prune (expr = false)` and `prune ( expr != false)`. This case is a bit tricky to deconstruct in HIL. This diff translates the prune instructions as just `prune !expr` for the true branch and `prune expr` for the false branch.
Reviewed By: dulmarod
Differential Revision: D5832147
fbshipit-source-id: 2c3502d
Summary:
We need to make sure that destructors of virtual base classes are called only once. Similarly to what clang does, we have two destructors for a class: a destructor wrapper and an inner destructor.
Destructor wrapper is called from outside, i.e., when variables go out of scope or when destructors of fields are being called.
Destructor wrappers have calls to inner destructors of all virtual base classes in the inheritance as their bodies.
Inner destructors have destructor bodies and calls to destructor wrappers of fields and inner destructors of non-virtual base classes.
Reviewed By: dulmarod
Differential Revision: D5834555
fbshipit-source-id: 51db238
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
Summary:
When a lambda has an `auto` parameter, the inferred type of the parameter because part of the name.
Our heuristic for identifying lambda was checking if the lambda's name was exactly `operator()`, which won't catch this case.
Reviewed By: jvillard
Differential Revision: D5753323
fbshipit-source-id: 85ff75a
Summary:
Not translating these properly was causing false positives for the dead store analysis in cases like
```
int i = 0;
return [j = i]() { return j; }();
```
Reviewed By: da319
Differential Revision: D5731562
fbshipit-source-id: ae79ac8
Summary:
Keep track of generated files better and make sure we nuke them on `make clean`.
Also get rid of a few unused variables in infer/src/Makefile.
Reviewed By: sblackshear
Differential Revision: D5754553
fbshipit-source-id: b5fca41
Summary: We inject destructor calls of base classes inside destructor bodies after the destructor calls of fields.
Reviewed By: dulmarod
Differential Revision: D5745499
fbshipit-source-id: 90745ec
Summary: Refactoring destructor translation to take type pointer instead of qual type as a parameter, as we only have type pointers for base classes.
Reviewed By: dulmarod
Differential Revision: D5745490
fbshipit-source-id: 121f492
Summary: We used to crash whenever we hit these. The simple translation implemented here is not particularly inspiring, but it is better than crashing.
Reviewed By: jvillard
Differential Revision: D5702095
fbshipit-source-id: 3795d43
Summary: This appears to be interchangeable with `Config.debug`, so let's kill it.
Reviewed By: jvillard
Differential Revision: D5742685
fbshipit-source-id: d390b6b
Summary: This adds an option to only translate the body of a method when the file matches the give pattern. This is especially intended to be use for generated files.
Reviewed By: jvillard
Differential Revision: D5729120
fbshipit-source-id: 1e28469
Summary: With this, we can now get now get inter-procedural issues involving native methods.
Reviewed By: sblackshear
Differential Revision: D5730638
fbshipit-source-id: 3bdbdbd
Summary: Atoms of the form `identifier = footprint var` naturally occurs with the angelic analysis mode. So it is not clear to me why we should drop those.
Reviewed By: sblackshear
Differential Revision: D5654754
fbshipit-source-id: 9dd2eb5
Summary:
- failwith police: no more `failwith`. Instead, use `Logging.die`.
- Introduce the `SimpleLogging` module for dying from modules where `Logging`
cannot be used (usually because that would create a cyclic dependency).
- always log backtraces, and show backtraces on the console except for usage errors
- Also point out in the log file where the toplevel executions of infer happen
Reviewed By: jeremydubreil
Differential Revision: D5726362
fbshipit-source-id: d7a01fc
Summary: This makes the traces more readable when involving skipped functions.
Reviewed By: sblackshear
Differential Revision: D5731683
fbshipit-source-id: 49d363b
Summary: This new tests outlines that Infer does not detect inter-target issues involving native methods.
Reviewed By: sblackshear
Differential Revision: D5720873
fbshipit-source-id: cce8193
Summary: This should not affect the analysis results so there is no need to raise an exception here. We can always add this unsigned shift operator to SIL if we want the analysis to take them into account
Reviewed By: sblackshear
Differential Revision: D5703792
fbshipit-source-id: 739891f
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:
I'm working on parameterizing access trees with a config that will limit max depth + perhaps width if needed.
This is a stepping stone to enforcing max depth.
Reviewed By: jvillard
Differential Revision: D5693453
fbshipit-source-id: c15b0ee
Summary:
Rather than printing the footprint using its actual representation (an access trie with bool nodes), print it as a set of access paths.
This makes it easier to read sources in Quandary specs/debug Quandary.
Reviewed By: jeremydubreil
Differential Revision: D5682630
fbshipit-source-id: ac55b7f
Summary:
Add `is_empty` to `AbstractDomain.WithBottom` sig and use the empty checks for nicer printing of access trees: don't print empty nodes/traces.
This should make it easier to debug Quandary; it's pretty hard to stare at an access tree and see what's going on right now.
Reviewed By: jberdine
Differential Revision: D5682248
fbshipit-source-id: 56d2a9d
Summary:
This gets rid of the horrible hack of asking jbuilder to build
_build/{default,test}/.ppx/ppx_compare/ppx.exe prior to starting several
jbuilds in parallel. We now refrain from starting several jbuilds in parallel.
Also, I finally understood that order-only deps do nothing for phony targets,
and not much else for non-phony ones. I hate make even more.
Reviewed By: jberdine
Differential Revision: D5678699
fbshipit-source-id: 52179e8
Summary:
This simplifies the jbuild files: no need to list these files explicitly
anymore, nor to exclude them explicitly from the main `InferModules` library
(due to their different compilation flags).
Isolate common parts into jbuild.common do `cat`-based code inclusion into
jbuild files to factorize code.
Reviewed By: jberdine
Differential Revision: D5678328
fbshipit-source-id: 6d7d925
Summary: In case of syntax errors in AL files, stdout will contain a JSON list with all files affected by the errors, including info like filename and line number.
Reviewed By: dulmarod, jvillard
Differential Revision: D5640272
fbshipit-source-id: 569b16d
Martino Luca
Dulma Churchill
Jeremy Dubreil
Dino Distefano
Sam Blackshear
Daiva Naudziuniene
Jules Villard
Josh Berdine
Sungkeun Cho
Roy Li