Summary:
The `--continue-analysis` option enables continuing analysis after more targets are captured by
`--continue`. For example,
```
$ infer capture -- buck build tgt1
$ infer analyze --merge
$ infer capture --continue -- bucck build tgt2
$ infer analyze --merge --continue-analyze
```
In the last analysis, it reuses the analysis results of `tgt1` from the previous analysis. If
`tgt1` and `tgt2` have a same dependency to a library, the analysis results of the library is also
reused.
Reviewed By: dulmarod
Differential Revision: D19996598
fbshipit-source-id: bb6874a6f
Summary: The main job the schedulers do is building their work queues. That's being performed before the workers are forked which means they get copied into all of them. These changes push the initialization of the schedulers just after the forking takes place.
Reviewed By: ngorogiannis
Differential Revision: D19769741
fbshipit-source-id: 0b20ddd5c
Summary:
The ProcLocker uses files as locks and relies on the guarantees of the `Unix.open_file` function when using `O_CREAT` and `O_EXCL` simultaneously.
- `setup`: creates a directory for the lock files inside `infe-out` and deletes its content if it already existed.
- `clean`: does nothing for now. Any file locks that may have been left unlocked are removed by the `setup` in the next run. This way the user can see what locks were taken if the program crashes.
- `lock_exn`: try to lock the `Procname` and if it can't releases all the locks that is currently holding.
- `unlock`: removes the corresponding file.
Reviewed By: ngorogiannis
Differential Revision: D19639402
fbshipit-source-id: e02f277ff
Summary:
`replace_make_shared` is finding a constructor by iterating all fields of type structs, which may be
expensive if there are lots of fields or `replace_make_shared` is called many times with the same parameters.
Reviewed By: ngorogiannis
Differential Revision: D19446260
fbshipit-source-id: c5c279ca5
Summary:
These changes introduce the RestartScheduler which for now is a copy of the FileScheduler:
- added it as a possible argument to the recently added `--scheduler` option.
- made the necessary changes in `InferAnalyze` to call it if it was chosen.
Reviewed By: ngorogiannis
Differential Revision: D19373505
fbshipit-source-id: 98f065057
Summary:
This also prints the CFGs *after* pre-analysis for individual procedures
in infer-out/captured/<filename>/<proc>.dot. One can also look up the
CFGs before pre-analysis in infer-out/captured/proc_cfgs_frontend.dot.
Context: I want to add a pre-analysis that needs to look at proc
attributes inter-procedurally. For this to make sense it has to happen
*after* all of capture, and before analysis.
Thus, this diff brings back the lazy running of the pre-analysis like in
D15803492, except that we still make sure to run the pre-analyses
systematically regardless of the checkers being run by running the
pre-analysis from ondemand.ml. Also we don't need to re-introduce the
"did_preanalysis" proc attribute for the same reason that the
pre-analysis is now run once and for all by ondemand.ml (instead of each
individual checker back in the days).
This has the benefit of running the pre-analysis only when needed, and
the drawback that several concurrent processes analysing the same proc
descs will duplicate work. Since pre-analyses are supposed to be very
fast I assume that neither is a big deal. If they become more expensive
then the benefit gets bigger and the drawback is just the same as with
regular analyses.
Reviewed By: skcho
Differential Revision: D18573920
fbshipit-source-id: de350eaef
Summary:
This allows us to move the CFG rendering to IR/.
The parts of that file concerning CFGs and those concerning Biabduction
specs were entirely disjoint, it turns out, so that was easy.
Reviewed By: jberdine
Differential Revision: D18573924
fbshipit-source-id: 0a5ab6478
Summary:
- Convert `task_generator` into a module of `ProcessPool` and collect inside the two combinators which were in semi-random places.
- Make `SyntacticCallGraph` export a `task_generator` as opposed to a call-graph builder.
- Separate `target` type and put it in its own module to avoid dependency cycles.
Reviewed By: skcho
Differential Revision: D18425718
fbshipit-source-id: 7957edac8
Summary: Not used feature and with no obvious roadmap anymore.
Reviewed By: jberdine, jvillard
Differential Revision: D17855860
fbshipit-source-id: fd75b9d62
Summary:
The code was already trying to do that but failing. Now it works.
This revealed a slight bug where the progress bar would always stop at
N-1/N 99% jobs. Fixed by moving the progress bar updates *after* the
operation that might decrease the number of jobs left.
Reviewed By: mityal
Differential Revision: D17423978
fbshipit-source-id: fc32db5f3
Summary:
Previously we would incorrectly report the time for the whole process
and this could include capture time too.
Reviewed By: mityal
Differential Revision: D17423977
fbshipit-source-id: b3ed754b3
Summary: This calls the method `delete_capture_and_analysis_data` introduced in D17184424 once the appropriate specs files for incremental analysis have been deleted. This fixes two bugs that I observed in incremental analysis that were arising because of stale state left in the results directory.
Reviewed By: ngorogiannis
Differential Revision: D17184424
fbshipit-source-id: d63f59db9
Summary:
Currently, the specs directory is cleaned after running capture. This means that the `changed-files` are interpreted in the context of the second set of source files. Therefore if a procedure is deleted from the second set of source files, its specs file will not be deleted.
This moves the cleaning of the specs directory to before capture, to avoid this problem.
Reviewed By: ngorogiannis
Differential Revision: D17093980
fbshipit-source-id: e1a8d8a54
Summary:
This adds logging of the number of nodes in the reverse analysis call graph, and the number of these nodes that are invalidated by incremental analysis.
This data will show the precision of incremental analysis.
Reviewed By: ngorogiannis
Differential Revision: D16939101
fbshipit-source-id: 1e465f1a6
Summary:
It doesn't make sense to use incremental analysis without specifying changed files. This is a possible source of future bugs.
This commit causes infer to die if incremental analysis is used without changed files.
---
Previously:
I think this code is currently a bit brittle because the CI shadow builds sometimes use `--incremental-analysis` because they are called with the same command as the diff analysis.
I am worried that in the future the shadow builds could be broken by this, although everything looks like it works right now. This diff would prevent breaking smoke builds in future because the shadow builds don't set changed-files (afaik).
However, possibly this is not the right place to fix the problem. It might be better to change the CI, I'm not sure.
Reviewed By: mityal
Differential Revision: D16829192
fbshipit-source-id: 5ee1ce9d0
Summary: Remove duplicate `s` when printing the time taken by the analysis
Reviewed By: ngorogiannis
Differential Revision: D16710277
fbshipit-source-id: 3ba7f6693
Summary:
Add logging for the number of procedures whose summaries are invalidated by incremental analysis
This will help verify that incremental analysis is working as expected in production
Reviewed By: ngorogiannis
Differential Revision: D16686911
fbshipit-source-id: 53c89c3bb
Summary:
Count the following:
- how many procedures were *actually* analyzed (i.e. some checkers ran
on them)
- how many times an analysis result was retrieved from the local cache
and how many times it was missed
Reviewed By: skcho
Differential Revision: D16561867
fbshipit-source-id: 8c43ce13c
Summary: The reverse analysis call-graph is logged if `--debug-level-analysis` > 0, so that its value can be inspected for tests
Reviewed By: jvillard
Differential Revision: D16440567
fbshipit-source-id: 1ec6af1f3
Summary: This implements incremental diff analysis by deleting only the summaries that need to be re-analyzed, keeping all summaries corresponding to procedures that have not been changed (or had a callee change).
Reviewed By: jvillard
Differential Revision: D16358474
fbshipit-source-id: 660a704a0
Summary:
Minor improvements to a bunch of stuff
- mostly, always log backend stats and time spent analysing, regardless of `-j 1`
- output stats more like they appear in the record
- split `InferAnalyze.main` to be more readable (hopefully)
Reviewed By: mityal
Differential Revision: D16440586
fbshipit-source-id: 6f91f53cd
Summary:
Modify the scheduler to collect results from children at the end of the
parallel execution. Use this to collect backend stats and log their
aggregated sum.
Reviewed By: ezgicicek
Differential Revision: D16358867
fbshipit-source-id: 775792ef7
Summary:
Summary.ml defines both a bunch of types and how to use them and a
mechanism to save and store summaries on disk while maintaining a
complex in-memory cache of what's on disk. Make the distinction clear.
Reviewed By: ngorogiannis
Differential Revision: D16358869
fbshipit-source-id: 9d4c6cb77
Summary:
Currently, `Callbacks.analyze_procedures` creates a function to call the method `Callbacks.iterate_procedure_callbacks`. This is supplied as an argument to functions in `ondemand.ml`, so that it can be invoked. This is done to avoid a cyclic dependancy.
This diff moves the functions that `ondemand.ml` needs to call into `ondemand.ml`, avoiding the need to supply them as arguments.
Reviewed By: ngorogiannis
Differential Revision: D16028836
fbshipit-source-id: 16ae27a3e
Summary:
This can take a minute or so during which the user would have no idea
what infer is doing.
Reviewed By: ngorogiannis
Differential Revision: D16005393
fbshipit-source-id: 586812527
Summary:
The synthetic methods from `topl.Property` are now nonempty: they
simulate a nondeterministic automaton.
Reviewed By: jvillard
Differential Revision: D15668471
fbshipit-source-id: 050408283
Summary: There can be A LOT of procedures -- currently we log two lines (started/done) for each one, when doing call graph scheduling. This leads to ridiculously long log files. Switch to only log these messages in the log file and only if we are verbose logging.
Reviewed By: jvillard
Differential Revision: D15413330
fbshipit-source-id: 6e26693e8
Summary:
API and stub implementation for real-time logging capabilities.
Low-level implementation requires interaction with FB-specific deployment of Scribe, hence it is stubbed out.
Reviewed By: jberdine
Differential Revision: D15259559
fbshipit-source-id: 712cb99e1
Summary:
A more dynamic scheduling scheme will potentially run into the situation where no new work packets can be scheduled, but more work will be possible to schedule in the future, perhaps when some dependent work packet finishes being analysed.
The current implementation prevents that, as it expects that if a worker goes idle, it stays idle.
The changes here address this in two parts:
- the `select` call is always given a finite timeout. If given an infinite timeout, we will not be able to poll the task generator for more work, where none were previously possible.
- when the `select` call times out without updates, check if there is an idle child, and if so if the task generator has more work right now.
See also ProcessPool.mli for comments.
Reviewed By: mbouaziz
Differential Revision: D15197749
fbshipit-source-id: babe5da8e
Summary:
Before moving to any kind of non-trivial scheduling, we need to change the Tasks interface.
In particular, it's too restrictive to expect that the tasks to be scheduled are provided as a list before starting execution. For example, dynamic scheduling does not fit the bill here. Also, the list expectation means all scheduling work has to be done up front.
The solution here is to move to a `Sequence`-like interface with one difference:
- The function returning the next task expects a task option argument. That argument is the task that was just finished (if any) by the worker expecting new work. This will be useful for things like task dependencies (for instance, a procedure has been analysed, and can be marked so).
Reviewed By: mbouaziz
Differential Revision: D15181613
fbshipit-source-id: 21f3ba825
Summary: Experimental feature: Use memcached for summaries as a look-aside cache during analysis.
Reviewed By: jvillard
Differential Revision: D12939311
fbshipit-source-id: 9f78994e2
Summary: If we get to that point, it means we already want to run the analysis so no need for this check.
Reviewed By: mbouaziz
Differential Revision: D9942702
fbshipit-source-id: e89e22c91
Summary:
Print the following for each source file to analyse in non-interactive mode:
```
path/to/source_file.c starting
[...]
path/to/source_file.c DONE in <time>
```
This should help diagnose when infer is stuck. It also logs this information to
the log file regardless of the form of the progress bar.
Also add a `--progress-bar-style` option to allow the user to force a
particular rendering: plain (as above), multiline (The Glorious One), or auto
(selection depends on whether infer is connected to a TTY on stdin *and*
stderr).
Reviewed By: mbouaziz
Differential Revision: D9120509
fbshipit-source-id: 4b43b7464
Summary:
When `--reanalyze` is passed, mark the summaries of procedures matching
`--procedures-filter` as needing to be analysed before running the analysis.
This allows one to, for instance, re-run the analysis in debug mode on only
some files or procedures. However, this won't work for the Java Buck
integration since the summaries are hidden away in buck-out.
Reviewed By: mbouaziz
Differential Revision: D8783668
fbshipit-source-id: 9032d83
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:
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
Sungkeun Cho
Fernando Gasperi Jabalera
Nikos Gorogiannis
Jules Villard
Josh Berdine
Phoebe Nichols
Mitya Lyubarskiy
Radu Grigore
Artem Pianykh
Nikos Gorogiannis