Summary:
At this point in the stack, here's what's left in InferPrint.ml:
1. how to output report.json and costs_report.json
2. how to print summaries from the command line (`infer report`)
3. how to print --issues-tests stuff (`infer report --issues-tests`)
Keep only 1. in there. 2. goes to SpecsFiles.ml directly from infer.ml,
and 3. goes to its own module (also the fields to output in
--issues-tests get a non-poly variant).
1. does some extra stuff sometimes, eg in test-determinator mode. Keep
this for now.
Reviewed By: ngorogiannis
Differential Revision: D20362642
fbshipit-source-id: 0d9f0e8e2
Summary:
Make <infer-out>/report.json the default value for this option, as this
is what is used 99% of the time. Clean up test options using this.
Reviewed By: ngorogiannis
Differential Revision: D20362644
fbshipit-source-id: a1bb18757
Summary:
InferPrint hasn't been in charge of writing bugs.txt since forever.
This will be re-implemented as a post-processing of report.json instead
(like it is now, but in OCaml instead of python).
Reviewed By: ngorogiannis
Differential Revision: D20362641
fbshipit-source-id: 83d8cb53d
Summary:
I don't think anyone uses this. Meta-goal: cleaning up InferPrint.ml.
Measuring stats about summaries is good in principle, but we should do
it somewhere else instead of in the InferPrint callback hell. For
instance when we record each summary. Meanwhile, delete this.
Reviewed By: ngorogiannis
Differential Revision: D20362639
fbshipit-source-id: c73d431a5
Summary:
Warning: This might be a bit brutal.
PerfStats and EventLogger are pretty much subsumed by `ScubaLogging`.
It seems no one has been looking at the data they generate recently.
Let's delete them! If we need to re-implement some parts later on, let's
do that using `ScubaLogging`, which is better (eg, still produces data
when infer crashes).
Things we lose:
- errors in the clang frontend due to missing decl translation, etc.
- errors in biabduction due to timeouts, functions not found, etc.
We could also re-implement these using BackendStats and ScubaLogging
instead of brutally deleting everything.
Reviewed By: ngorogiannis
Differential Revision: D20343087
fbshipit-source-id: 90a3121ca
Summary:
The goals are to have all the checker definitions and documentation in one
place (except how to actually run them, since that's not quite the same
concept; for example inferbo is one checker but several analyses depend on its
symbolic execution), and later on to be able to link issues reported by infer
back to the checker that generated them.
This makes apparent that the documentation of our checkers is lacking,
not touching that in this diff.
Not sure if "analysis" would be a better name than "checker" at this
point? For instance "Linters" is one of the checkers, which historically
at least we have not considered to be the case.
Reviewed By: mityal
Differential Revision: D20252386
fbshipit-source-id: fc611bfb7
Summary:
Problem: `infer report <specs file name>` is called manually sometimes to see analysis results in CLI. However, giving the specs file name is sometimes annoying, because the specs file name may be quite long and include special characters sometimes.
This diff introduces `--procedures-summary` to lookup the summaries interactively in `infer explore`.
example1: There are 8 procedures that include "max" in their names, then I selected one of them by entering a number.
```
$ infer explore --procedures --procedures-filter '.*max.*' --procedures-summary
0: minmax_div_const2_Bad_FN
1: minmax_div_const_Good
2: use_int64_max_Bad
3: use_uint64_max_Good
4: use_int64_max_Good
5: minmax_div_const_Bad
6: minmax_div_const2_Good
7: use_uint64_max_Bad
Select one number (type 'a' for selecting all, 'q' for quit): 2
void use_int64_max_Bad()
Analyzed
ERRORS: BUFFER_OVERRUN_L1
WARNINGS:
FAILURE:NONE SYMOPS:0
BufferOverrunAnalysis: StackLocs: { } MemPure: { } Alias: { ret= }
BufferOverrunChecker: Safety conditions:
{ }
```
example2: If there is only one specs file that satisfies the given filter, it reports the summary of that procedure without an interaction.
```
$ infer explore --procedures --procedures-filter '.*add_in_loop_ok.*' --procedures-summary
Selected proc name: void ArrayListTest.add_in_loop_ok()
void void ArrayListTest.add_in_loop_ok()(ArrayListTest* this)
Analyzed
ERRORS:
WARNINGS:
FAILURE:NONE SYMOPS:0
BufferOverrunAnalysis: StackLocs: { } MemPure: { } Alias:
{ i=size(__new-390022197-0-1.elements), ret= }
LatestPrune: latest { i -> (5, { }, { }) by ((5, { }, { }) >= (5, { }, { })),
__new-390022197-0-1.elements -> (⊥, { }, { __new-390022197-1-1 -> length : 5 }) by ((5, { }, { }) >= (5, { }, { })) }
BufferOverrunChecker: Safety conditions:
{ }
```
Reviewed By: jvillard
Differential Revision: D20284052
fbshipit-source-id: 2131339f1
Summary: Experiments suggest that infer does not take advantage of hardware threads and using more CPUs than the number of physical cores actually hurts performance. On Linux, `ProcessPool` now by default uses only the same number of workers as physical CPUs and pins them evenly.
Reviewed By: ngorogiannis
Differential Revision: D20193171
fbshipit-source-id: f8b9f55bf
Summary: Add the possibility of passing Scuba tagsets through the command line arguments.
Reviewed By: ngorogiannis
Differential Revision: D20262807
fbshipit-source-id: 9134cce8f
Summary:
It's a lot of code to maintain for something that no one ever uses
anymore.
Reviewed By: ngorogiannis
Differential Revision: D20282794
fbshipit-source-id: 28422c415
Summary:
These were not used (and were actually activated byt the same config
param). They both are in experimental stage that never reached maturity.
Since the team does not have immediate plans to work on ObjC nullability
checker; and since "eradicate" (now known as nullsafe) is the main
solution for Java, removing it is sensible.
Reviewed By: jvillard
Differential Revision: D20279866
fbshipit-source-id: 79e64992b
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:
More newer = more better.
This flips the Not_found -> Not_found_s switch, and forbids a bunch more
polymorphic comparisons (mostly turned into `int` comparisons for
convenience). Earlier diffs prepare for this so this diff is only about
breaking changes in the API, of which there are only a few.
Reviewed By: jberdine
Differential Revision: D19861583
fbshipit-source-id: fe54ce8f0
Summary:
The big one:
- stop using polymorphic `<>`, `<`, `>`, ..
- add `<>` to `PolyVariantEqual` escape hatch now that `<>` is as taboo as `=`
- Interestingly, there were a lot of uses of `Z.(x < y)`, which although
they seem to use `Z.lt` actually used polymorphic comparison. The actual
comparison infix operators of `Z` are cleverly hidden in `Z.Compare`
instead, which makes them impractical to use...
Reviewed By: jberdine
Differential Revision: D19861584
fbshipit-source-id: 5dce08ad9
Summary:
This diff adds a taint domain in Inferbo. The taint value will be used to find vulnerable array
accesses in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D19391028
fbshipit-source-id: 566b4c0fe
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:
Now we can either disable it, or enable it only.
For integrations that disable it, this will allow to enable it for
NullsafeStrict classes without enabled it fully
Reviewed By: artempyanykh
Differential Revision: D19409131
fbshipit-source-id: a2b1fe650
Summary:
That was used only by the now-defunct Java Buck integration without
genrules.
Reviewed By: ngorogiannis
Differential Revision: D19176545
fbshipit-source-id: 8253b614a
Summary:
You should use `--buck-java` instead, which uses the new "genrule
master" integration.
This diff makes it impossible to select the previous integration.
Upcoming diffs will clean up the resulting dead code.
This also make infer fail hard when no buck mode is specified in a buck
capture command, eg `infer -- buck build //foo:foo`. The reason is that
we need to choose between 3 incompatible integrations and making any of
them the default will confuse at least one person in the future.
Reviewed By: ngorogiannis
Differential Revision: D19176391
fbshipit-source-id: 707d18b50
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: Add command line option that directs racerd to treat all return values from unknown code (including abstract methods) as owned objects. This is essentially treating return values with full angelicism
Reviewed By: artempyanykh
Differential Revision: D19368375
fbshipit-source-id: 6a10153fa
Summary:
This changes how we select amongst our (currently) 4 Buck integrations
for Java and clang, as well as how the user's choice is reflected by the
Config module.
The old command line interface is still supported but is now deprecated.
The changes in how to select each integration are:
- clang via "flavors", activated with `--flavors`, now with `--buck-clang`
- clang via "compilation DB", activated with `--buck-compilation-database`, unchanged
- Java via "genrule", activated with `--genrule-master-mode`, now with `--buck-java`
- Java "without genrules", used to be activated by *not specifying any other Buck mode*, unchanged
Instead of various `Config` flags corresponding to the previous CLI that
are allowed in any combination of `flavors`,
`buck_compilation_database`, `genrule_master_mode`, `Config` now exposes
a single `buck_mode` datatype. This allows, eg, `flavors` to override
`buck_compilation_database` if needed. It will also make it easier to
get rid of the old "Java without genrules" integration in a later diff
(see inline comments).
Reviewed By: ngorogiannis
Differential Revision: D19175686
fbshipit-source-id: 29b3831be
Summary:
The re-execution phase uses only the preconditions found by the footprint phase. Thus, Infer should
not spend time optimizing POSTconditions. These are used only to find custom errors.
Reviewed By: jvillard
Differential Revision: D19035495
fbshipit-source-id: d52b82733
Summary:
Inferbo does not use the external relational domains, apron and elina. At some point, the parts of
inferbo using them were broken and they do not seem to be fixed easily in the near future. Let's
remove them and keep the code base cleaner.
Reviewed By: jvillard
Differential Revision: D19022905
fbshipit-source-id: e0eafe79f
Summary: The new domain is much better than the old one. Let's kill the old one (along with old litho tests) and simplify things.
Reviewed By: skcho
Differential Revision: D18959627
fbshipit-source-id: df77ae20e
Summary: It is not used anywhere and there are no plans to revive it. Kill it!
Reviewed By: skcho
Differential Revision: D18934719
fbshipit-source-id: b9b069b96
Summary: This diff checks litho condition on the new abstract value. This is triggered with `--new-litho-domain`, but it is intra-procedural as of now.
Reviewed By: ezgicicek
Differential Revision: D18783203
fbshipit-source-id: 98570104e
Summary:
This diff enables parsing and auto-formatting documentation
comments (aka docstrings).
I have looked at this entire diff and manually made some changes to
improve the formatting. In some cases it looked like it would take too
much time, or benefit from someone more familiar with the code doing
it, and I instead disabled auto-formatting docstrings in those files.
Also, there are some source files where the docstrings are invalid,
and some where the structure detected by the parser appears not to
match what was intended. Auto-formatting has been disabled for these
files.
Reviewed By: ezgicicek
Differential Revision: D18755888
fbshipit-source-id: 68d72465d
Summary:
We were wrongly not supressing third-party calls in
case third party repo is provided: there was a bug in the function is_modelled_externally.
because of this we accidentally stopped supressing third party and
started to advertise it in non-strict mode.
we do plan doing that, but little bit further ahead :)
So let's add a param guiding this.
Reviewed By: artempyanykh
Differential Revision: D18658271
fbshipit-source-id: 703f2675b
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:
First step towards a global analysis. A new command line flag activates the step in `Driver`.
The whole-program analysis is a simple, quadratic (inefficient-as-yet), iteration over all domain elements. However, it is restricted to those elements that are explicitly scheduled to run.
Reviewed By: skcho
Differential Revision: D17787441
fbshipit-source-id: 9fecd766c
Summary:
Ability to accept relative path is convenient for testing and local
debugging.
Ability to accept absolute paths is needed for buck integration - buck
knows absolute path (to properly invalidate cache when the content of
the folder is changed) and passes it to infer.
Reviewed By: artempyanykh
Differential Revision: D18370407
fbshipit-source-id: be7f12ae1
Summary:
In this diff, we just load the info from the storage. Next diff will be
actually using this information to infer nullability.
`ThirdPartyAnnotationGlobalRepo.get_repo` will be used in the next diff,
hence #skipdeadcode
Reviewed By: artempyanykh
Differential Revision: D18347647
fbshipit-source-id: 82a9223c6
Summary:
Describe what the --report-*-* options actually do instead of their
outdated documentation from the time where this was
`--checkers-blacklist-regex`, `--infer-blacklist-regex` and the like.
Reviewed By: dulmarod, mityal
Differential Revision: D17906015
fbshipit-source-id: 204349e9e
Jules Villard
Sungkeun Cho
Martin Trojer
Fernando Gasperi Jabalera
Mitya Lyubarskiy
Nikos Gorogiannis
Radu Grigore
Ezgi Çiçek
Josh Berdine
Dulma Churchill