Summary: Just for fun, and because killing InferPrint.ml is just so satisfying.
Reviewed By: ngorogiannis
Differential Revision: D20362643
fbshipit-source-id: 039cfec61
Summary:
Now that this module only prints report.json and costs_report.json, we
can dis-entangle the whole callback spaghetti.
Reviewed By: ngorogiannis
Differential Revision: D20362640
fbshipit-source-id: 56ffa4e08
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:
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:
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:
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: Not needed any more as infer's concurrency isn't controlled via make.
Reviewed By: jvillard
Differential Revision: D19905712
fbshipit-source-id: f97ef4421
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:
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:
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:
This generates a lot of code (the datatype is not trivial) and
transitively requires other datatypes to have compare functions, just so
we can then ask whether the mode is "Analyze".
Reviewed By: ngorogiannis
Differential Revision: D19164589
fbshipit-source-id: be6a12b41
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:
I observed a bug in incremental analysis for thread safety analysis, where a thread safety violation was not being reported because the folder `racerd` was not being cleaned. This meant that the violation was determined to be a preexisting issue when it was actually an introduced issue.
This method can be used to fix this problem by cleaning the `racerd` folder. It also cleans the `captured` folder, I've done this following the original version of the method (see D16602417).
I'm not sure if the `captured` folder is used; it wasn't used in the tests I did. Thoughts about this?
Reviewed By: ngorogiannis
Differential Revision: D17261504
fbshipit-source-id: 8fea23e98
Summary:
An exception thrown during capture/analysis may leave the daemon
running. Kill it even when one is thrown.
Reviewed By: martintrojer
Differential Revision: D17181090
fbshipit-source-id: a7b002f23
Summary:
Implementation of write-serializer for Sqlite. Points of note:
- A Unix socket is used for communication. This avoids buffer-size limitations, as the objects we send for writing may exceed said limits.
- No daemon is used if running under buck or in genrule mode, as this usually means a single-threaded job capturing into the DB.
- When the daemon is running, read-only access is *not* enforced for other processes. This makes starting and stopping the daemon during Infer execution easier and more robust. In WAL mode this should not have any effect on performance.
- This version is not economical with connections, it uses one per query, todo.
Reviewed By: jvillard
Differential Revision: D17077183
fbshipit-source-id: fa9877d6c
Summary:
Write contention is becoming a problem in parallel capture (eg when make runs with high parallelism) or when analysis writes CFGs to the DB in parallel (eg when analysing blocks in ObC). This is believed to lead to BUSY errors in Sqlite.
This is step 1 of a process where all writes are cordoned-off in one module, and fixing the interface for that module.
Reviewed By: skcho
Differential Revision: D16985034
fbshipit-source-id: 3d7ce381b
Summary:
It's not being worked on and is not in a state where it works.
It would probably better to write this as a script of some kind or else
resurrect this subcommand in a form where it behaves more like a script,
ie fork/execs infer analyses instead of having them be function calls
(but then it might as well *be* a script as it would likely be more
flexible).
In any case...
youarealreadydead
Reviewed By: ezgicicek
Differential Revision: D16602417
fbshipit-source-id: d0d129539
Summary:
Move genrule capture integration logic from shell to OCaml.
Also, stop relying on side-effects of buck compilation for constructing the infer-deps.txt file used for merging. Now this is obtained by passing `--show-output` to buck, which spits out the `buck-out` output paths to the targets we asked to build.
Reviewed By: ezgicicek
Differential Revision: D15715608
fbshipit-source-id: 8fa896ba6
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: Use the value of other options instead since we're trying to get rid of it. This should be equivalent.
Reviewed By: jeremydubreil
Differential Revision: D9943274
fbshipit-source-id: 055e1bdd2
Summary:
This adds an option `--trace-events` that generates a Chrome trace event[1] to
quickly visualise the performance of infer.
Reviewed By: mbouaziz
Differential Revision: D9831599
fbshipit-source-id: 96a33c627
Martin Trojer
Jules Villard
Nikos Gorogiannis
Josh Berdine
Dulma Churchill
Phoebe Nichols
Artem Pianykh
Mitya Lyubarskiy
Nikos Gorogiannis
Vincent Siles