Summary:
Do no computation of stability abstract state if not explicitly requested via the command line flag.
Also, simplify the reporting.
Reviewed By: jeremydubreil
Differential Revision: D8614885
fbshipit-source-id: 25dd9de
Summary:
Specs do not get invalidated by reactive mode, so we need to delete them all.
Reactive just means that the capture remains valid and the analysis will only
use the freshly captured source files to start the analysis, but all the
dependencies will be re-analysed.
Reviewed By: da319
Differential Revision: D8735171
fbshipit-source-id: dc1eab3
Summary: Do not start with an invalid source file when we can avoid it. Follow up from D8418447.
Reviewed By: jeremydubreil
Differential Revision: D8732168
fbshipit-source-id: 28a183b
Summary:
The addresses of global variables do not need initialisation to exist and be valid as they are part of the code or data segment of the program. This means that taking the address of a global is not in itself a danger for SIOF. However, dereferencing such an address would be. In order to avoid false positives but avoid being too unsound, only ignore them when the address is taken only to set another global. The general case would require a more complicated abstract domain.
Fixes#866
Reviewed By: ngorogiannis
Differential Revision: D8055627
fbshipit-source-id: 92307b2
Summary:
The captured/ directory is not guaranteed to exist when the capture was run without debug mode, but the analysis assumes it will be. So, this crashes infer:
```
infer -- clang -c examples/hello.c
infer -g
```
There's no need for `DB.Results_dir.init` to create infer-out and infer-out/specs/ since this is now done in `ResultsDir`.
Reviewed By: jeremydubreil
Differential Revision: D8732739
fbshipit-source-id: aaac902
Summary: Otherwise the dead code checker sometimes crashes with a not-totally-related error.
Reviewed By: mbouaziz
Differential Revision: D8732546
fbshipit-source-id: 65caabd
Summary:
These just point to expressions that we know how to translate.
Fixes#950
Reviewed By: mbouaziz
Differential Revision: D8713784
fbshipit-source-id: 9eafa39
Summary: The frontend got better and now `assert` is correctly translated.
Reviewed By: dulmarod
Differential Revision: D8731877
fbshipit-source-id: ba11b0c
Summary: This was showing up during memory profiling with statistical-memprof. The surrounding code shows that we are trying not to allocate if nothing changes, but the `List.map` in the middle would defeat that.
Reviewed By: ngorogiannis
Differential Revision: D8661763
fbshipit-source-id: d44f7a7
Summary: This is make the callbacks are always set instead of silently returning `None`
Reviewed By: ngorogiannis
Differential Revision: D8651971
fbshipit-source-id: 7cd1c02
Summary: One step towards elminating the unsafe cache of procedure summaries in `Summary` and only rely on the one in `Ondemand`
Reviewed By: dulmarod, jvillard
Differential Revision: D8619782
fbshipit-source-id: 4096390
Summary:
This was spammy, especially for errors which we already know about and are
caught by the frontend (then the error message would be displayed about a
translation error without context about what the error was).
Reviewed By: dulmarod
Differential Revision: D8640145
fbshipit-source-id: 8b8b8a7
Summary:
The motivation is in a following diff: ensuring symbols do not cross procedure boundaries.
- This diff rewrites `Bound.subst` to be based on the substituted bound rather than folding on the symbol map.
- This way we are sure all symbols are substituted and no symbols from another procedure remains in the result.
- All cases from the previous version should still be here, I think I added a few constant approximations of minmax substituted with minmax (that would be return Top).
Side-effects (good):
- `mult_const` has also more constant approximations for minmax,
- substitution should be faster
Reviewed By: jvillard
Differential Revision: D8369993
fbshipit-source-id: 6ed8be8
Summary:
This changes the behaviour back to before the "fork once then pipe new tasks
for each source files" era: before that we would fork once per source file,
which had the effect of emptying the caches for every source file. Without this
the caches can grow unchecked.
This is probably suboptimal but should at least be the same behaviour as before.
Reviewed By: jeremydubreil
Differential Revision: D8615124
fbshipit-source-id: 69fc101
Summary:
- Do not add actuals of a call as unstable.
- Replace access trie with simple set of paths, which is easier to debug/argue correct.
- Fix bug where a prefix path was searched, as opposed to a *proper* prefix.
- Restrict interface to the minimum so that alternative implementations are easier.
Reviewed By: ilyasergey
Differential Revision: D8573792
fbshipit-source-id: 4c4e174
Summary: This prevents the task bar from scrolling the terminal in case the lines are not wide enough. Instead it will truncate the display to the terminal size. Also display only the most useful info when there is not much room.
Reviewed By: jeremydubreil
Differential Revision: D8590580
fbshipit-source-id: e12d5c9
Summary: `make deadcode` complains about circular dependencies but it works. Document mystery and remove dead code that was introduced while the tests were broken.
Reviewed By: da319
Differential Revision: D8590961
fbshipit-source-id: b52e290
Summary:
Previously we would block indefinitely waiting for that child to send us an
update. Now errors in the child are caught and the main process dies, taking
everyone down with it.
When a child dies, it sends a "Crash" message to the parent, unless it died
receiving a signal (like a segmentation fault, or an external signal). In that
case, the OCaml runtime won't get a chance to notice its death and send the
"Crash" message. Thus, always check if some child has died from under us as
well.
Reviewed By: mbouaziz
Differential Revision: D8577095
fbshipit-source-id: 519992b
Summary: C/C++ code can, in some cases, generate a large number of temporary (Sil) variables. Since we are already not reporting races on these, not recording them gives some perf back.
Reviewed By: mbouaziz, jvillard
Differential Revision: D8566999
fbshipit-source-id: 148ac46
Summary: Trying to convert a large int literal to an OCaml int raises an exception. The use case here actually needed a float anyway, so add an API for that.
Reviewed By: jeremydubreil
Differential Revision: D8550410
fbshipit-source-id: 382495b
Summary:
We inline the .ml and the .mli together using the .cmi rule (for reasons
explained in the Makefile of deadcode). This relies on the fact that rules will
start from the .cmx, which in turns depends on the .cmi as the last dependency
and so all the dependencies of the .cmx are satisfied by the time we hit the
.cmi. But that doesn't always work.
For some reason, making the .cmi depend on its .cmx works, even though it's
supposed to include a circular dependency (`make` should complain but doesn't).
Oh, well...
Reviewed By: jeremydubreil
Differential Revision: D8548032
fbshipit-source-id: 0dc9335
Summary:
Replace the previous outputting of "." and "F" with an actual progress bar and
a multiline display of what procedure each process is currently busy analysing.
Observe:
```lang=text
Found 19 source files to analyze in /home/jul/code/openssl-1.1.0d/infer-out
7/19 [######################......................................] 36%
⊢ [ 1.14s] crypto/mem.c: CRYPTO_malloc
⊢ [ 1.68s] crypto/o_time.c: julian_adj
⊢ [ 0.50s] crypto/mem.c: CRYPTO_zalloc
⊢ [ 1.80s] crypto/o_str.c: OPENSSL_strlcpy
```
This works by setting up a worker pool (as before) that waits to receive jobs
(not as before: we used to fork for each new job). Unix pipes are used for
communication.
The new worker pool can be used to experiment with other concurrency models,
such as reviving per-procedure-parallelism, or making sure each procedure is
analysed only once.
Perf tests indicate that this version is no slower than the previous one,
either on laptops or devserver: about 3% worse user time but ~40% better system time.
This new version forks <jobs> processes whereas the previous version would
fork `O(number of source files)` times.
`infer -j 1` shows a progress bar that doesn't update timing info (because it
would need a second process to do that).
Reviewed By: mbouaziz
Differential Revision: D8517507
fbshipit-source-id: c8ca104
Summary:
The execution environment is really just a cache. It happens to point to a
particular source file which is where the analysis was started from, but that
is not relevant, and in fact is confusing because it suggests that it is
somewhat tied to that file. In reality, exe_env caches information about any
procedure and source file encountered by the analysis.
This will make it easier to make further changes but I think it also brings a
bit more clarity to the code.
Reviewed By: jeremydubreil
Differential Revision: D8513735
fbshipit-source-id: f4b38ce
Nikos Gorogiannis
Jules Villard
Ezgi Çiçek
Martin Trojer
Dulma Churchill
Jeremy Dubreil
Mehdi Bouaziz
Daiva Naudziuniene
Martino Luca