Summary:
We were using the "filename" as the key because it's (kinda) unique *and* human
readable, but with the `infer explore --procedures` interface we don't really
need the human readable part anymore, so we can just use the OCaml marshalling
of the pname as the key. The human-readable version (sans unique-fying hash) is
now another column in the table, used to match procedure names in
`--procedures-filter`.
Reviewed By: sblackshear
Differential Revision: D7639158
fbshipit-source-id: e714605
Summary:
Add a `--procedures` option to `infer explore` to print information about the
procedures captured by infer. More precisely, `infer explore --procedures` will
print each row of the "procedures" table in the results database. A new
`--procedures-filter` controls which procedures to print information about, and
there is one flag per column in the db too to print more or less options about
each procedure (in particular, we can now print attributes), with some defaults.
Reviewed By: sblackshear
Differential Revision: D7639062
fbshipit-source-id: 034a2b8
Summary:
Now that everything can run at the same time and we have preanalyses, it can be quite hard to read debug sessions.
Here come session names!
Depends on D7607336
Reviewed By: sblackshear
Differential Revision: D7607481
fbshipit-source-id: 676af86
Summary:
- Less `^`
- `pp_print_string` instead of `F.fprintf fmt "%s"`
- and stuff like that
Reviewed By: jvillard
Differential Revision: D7607336
fbshipit-source-id: 5d985ef
Summary: Only RacerD uses the Cluster callbacks but we used to compute a lot of things anyway.
Reviewed By: sblackshear
Differential Revision: D7516279
fbshipit-source-id: 22f2b86
Summary:
There's actually a nice separation between IR/, base/, istd/, and the rest of
infer, so they can be made into separate jbuilder libraries so that the
separation remains. This helps make sense of the infer codebase.
Also:
- move everything biabduction-related out of backend/ and into a new
biabduction/ directory. This clarifies the current situation where backend/
contains a mix of analysis-independent code (still there now), and
biabduction-specific code (moved to biabduction/).
- move everything from base/ that is not infer-specific into istd/, e.g. IList.ml
- kill unused `FbTraceCalls`
- A couple of files needed to move around to complete the separation of base/ and IR/
Reviewed By: mbouaziz
Differential Revision: D7381842
fbshipit-source-id: cd86dea
Summary: - No need to log the string of stats type when registering a perf Epilogue
Reviewed By: dulmarod
Differential Revision: D7398544
fbshipit-source-id: 681a956
Summary:
Limit the scope of what gets included into IStd.ml to only values that we want
to shadow. New values go into other files.
Also, build istd/ with `Core` open.
Reviewed By: mbouaziz
Differential Revision: D7382111
fbshipit-source-id: 969f0e8
Summary:
- Time only stats are now reported from the driver for
- TotalFrontend
- TotalBackend
Reviewed By: dulmarod
Differential Revision: D7382161
fbshipit-source-id: 6e34ca2
Summary:
- PerfStats can now directly compute the filename / relative path of the stats to be logged
- There is no longer a need to pass in the filename as a parameter, simplifying the API to just be a one-liner
Reviewed By: dulmarod
Differential Revision: D7381886
fbshipit-source-id: e6623c3
Summary: `stats_type` can just include a `SourceFile.t`, as the existence of a `source_file` parameter previously depended on the value of `stats_type` anyway
Reviewed By: dulmarod
Differential Revision: D7381605
fbshipit-source-id: 953ee27
Summary:
The goal is not to end up with a deep copy when nothing has changed, as this
puts lots of pressure on the memory.
Reviewed By: mbouaziz
Differential Revision: D7113976
fbshipit-source-id: 1b85ecd
Summary:
There's no real reason not to use `Core` lists in this module. Changed the
interface to be more `Core`-like. Changed the `*_changed` functions to use a
ref to track changes instead of passing the changed state around.
Reviewed By: mbouaziz
Differential Revision: D7123211
fbshipit-source-id: b27791a
Summary:
- InferPrint reports time stats only, logged in `reporting_stats/` as well as a `PerformanceStats` event with `stats_type: reporting`
- Perf reporting can now be registered at one point (with desired start real and cpu times) and triggered later
Reviewed By: dulmarod
Differential Revision: D7332435
fbshipit-source-id: 2e17c7f
Summary:
Perf reporting can now be registered at one point (with desired start real and cpu times) and triggered later
- This is accomplished by storing perf file names in a hashtable mapping to the reporting function
- New `stats_kind` parameter that is either Time, Memory, or TimeAndMemory, where Time requires a Unix.process_times and an Mtime_clock.counter to be passed in, but TimeAndMemory just uses the time from the start of the process.
Reviewed By: dulmarod
Differential Revision: D7337158
fbshipit-source-id: 94699cd
Summary:
Perf reporting can now be registered at one point (with desired start real and cpu times) and triggered later
- This is accomplished by storing perf file names in a hashtable mapping to the reporting function
- New `stats_kind` parameter that is either Time, Memory, or TimeAndMemory, where Time requires a Unix.process_times and an Mtime_clock.counter to be passed in, but TimeAndMemory just uses the time from the start of the process.
Reviewed By: dulmarod
Differential Revision: D7337158
fbshipit-source-id: 3890cc7
Summary:
- PerfStats can now report either time and/or memory stats, by default reporting both
- This is in preparation for adding just time or memory related logging in the future
Reviewed By: mbouaziz, dulmarod
Differential Revision: D7324556
fbshipit-source-id: e265b12
Summary: Add new clang_method_kind field to AnalysisIssue, logged similarly to the existing one in AnalysisStats
Reviewed By: dulmarod
Differential Revision: D7273660
fbshipit-source-id: d1ca79b
Summary:
- Rather than passing a directory name to PerfStats reporting api to write the stats to, and then determining the EventLogger `stats_type` from that dirname, there is now a `stats_type` type in PerfStats, and the directory name and EventLogger tag is automatically determined from that type after it is passed to the API
- This allows us to determine whether we're in capture mode or linters mode dynamically from PerfStats itself, and use the appropriate tag when creating an event
Reviewed By: dulmarod
Differential Revision: D7251580
fbshipit-source-id: 0dec071
Summary:
Previously, `backend_stats` were getting logged correctly only when `infer analyze` was directly called, not `infer run`. Now, we report `backend_stats` directly, as part of the `iterate_callbacks` function in the task passed to the `ProcessPool`.
As a side benefit, `aggregated_stats` are also logged correctly now.
Reviewed By: dulmarod
Differential Revision: D7195525
fbshipit-source-id: fb2a400
Summary:
- Noticed that there were two different type aliases for the same type, representing the return value of `__POS__`
- Combined them under `ocaml_pos` name which more closely matches the pervasive
- Moved to Logging module
Reviewed By: dulmarod
Differential Revision: D7194034
fbshipit-source-id: 22cb949
Summary:
- PerformanceStats rows will be logged to EventLogger regardless of whether Infer is in developer mode
- PerformanceStats files will still not be created unless Infer is in developer mode
Reviewed By: dulmarod
Differential Revision: D7169403
fbshipit-source-id: 85bd7de
Summary:
- New Event type in EventLogger: PerformanceStats
- Contains some of the information logged to disk by PerfStats, as well as a `stats_type` tag to indicate which type of process the stats are from
- PerfStats.register_report_at_exit now takes 3 string arguments and constructs the file path and determines stats_type based off of them
- Changed all clients of PerfStats to use new api
Reviewed By: dulmarod
Differential Revision: D7131904
fbshipit-source-id: 9226b5d
Summary: This is to make sure than the analysis produces the same results independently from the order in which the members of a call cycle are analyzed.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6881971
fbshipit-source-id: 23872e1
Summary:
`Sequence` API to walk over free variables in expressions, instead of computing lists with uniqueness constraints that make them have linear complexity for insertion.
Switch to a Set representation when we don't care about the order of elements,
otherwise to a `Hash_queue`:
https://ocaml.janestreet.com/ocaml-core/113.33/doc/core/Std/Hash_queue.mod/S.modt/
Often, we don't even need to compute the sequence of free variables, as we are
just testing membership/emptiness/...
Reviewed By: mbouaziz
Differential Revision: D7099294
fbshipit-source-id: e96f84b
Summary:
The goal is to allocate less and generally be more efficient than handling
lists with uniqueness constraints.
Reviewed By: mbouaziz, jberdine
Differential Revision: D7098904
fbshipit-source-id: 7111f07
Summary:
A list of free variables was computed and passed around, but never used. The
reason OCaml wasn't complaining is that the list is eventually passed to a
recursive function, which passes it to its recursive call, so it looks like
it's used there.
Reviewed By: mbouaziz
Differential Revision: D7098556
fbshipit-source-id: b22a591
Summary:
As far as I can tell nothing uses it and it is ignored by the matching engine:
the "parameters" arguments are collected from config options but never actually
used for matching.
Reviewed By: sblackshear
Differential Revision: D6976273
fbshipit-source-id: 6fed5ff
Summary:
- EventLogger no longer depends on ProcAttributes
- This allows for other backend classes which are used by ProcAttributes to log in the future without creating a cyclic dependency structure
Reviewed By: dulmarod
Differential Revision: D7082444
fbshipit-source-id: f32a6e2
Summary: - When a CallTrace result is CR_skip, then a reason for skipping the call will be included in the record
Reviewed By: dulmarod
Differential Revision: D7082572
fbshipit-source-id: 20ed191
Summary:
- During the symbolic execution stage of the backend, Infer will log detailed stats about procedure calls
- Logging is accomplished directly within symExec/Tabulation
- call_result type is moved to tabulation.ml
CallStats was a broken module that allocated a lot of useless memory. Now, Specs.CallStats and InferPrint.CallsCsv as well as the Calls report kind in InferPrint no longer exist.
Reviewed By: dulmarod
Differential Revision: D7016439
fbshipit-source-id: 40911ee
Summary:
- StatsLogs is now its own functional module in InferPrint
- No longer stores events to be logged in a list to be later logged, just immediately logs them
Reviewed By: dulmarod
Differential Revision: D7010559
fbshipit-source-id: 1837ca9
Summary: Just some minor renaming to be more consistent with other modules. I was about to use these modules and was too lazy to type `Ident.IdentSet`.
Reviewed By: da319, avarun42
Differential Revision: D6999808
fbshipit-source-id: c24edef
Summary:
- change a use of clang_method_kind to match directly on the type rather than a brittle check for equality
- make the clang_method_kind field in AnalysisStats an option
- if procedure lang is not clang, then clang_method_kind field gets skipped while logging
Reviewed By: dulmarod
Differential Revision: D7010060
fbshipit-source-id: 077094d
Summary: We do not inject a destructor call if the destructor declaration does not contain a body in AST. We miss all the cases where the destructor is declared in `.h` file and defined in `.cpp` file as other files include `.h` file and do not contain the body of the destructor when destructor calls are being injected based on AST information. After this diff we inject destructor calls even if we do not have body for the destructor in AST.
Reviewed By: sblackshear
Differential Revision: D6796567
fbshipit-source-id: 1c187ec
Summary: InferPrint should not generate StatsLogs format at all unless Config.log_events is set to true
Reviewed By: mbouaziz, dulmarod
Differential Revision: D6976352
fbshipit-source-id: d12005a
Summary:
Added a check for recursive calls not to add abduced reference parameters constraints. Abduced reference parameters constraints were causing assertion failure when renaming variables in specs, in particular, when transforming variables into callee variables.
A similar check is already in place for abduced retvals constraints.
Reviewed By: jeremydubreil
Differential Revision: D6856919
fbshipit-source-id: acfe840
Summary:
This allows Eradicate to lookup the annotations from the classpath and without requiring the code in the classpath to have been previously analyzed. The benefit is that source files can be analyzed independently of each other as long as the classpath is known.
The main goal is to run be able to run Eradicate as a linter without losing warnings.
We may have to add some more models of the standard libraries as no `Nullable` on a parameter does not necessarily mean that the method does not accept `null`.
Reviewed By: sblackshear
Differential Revision: D6921720
fbshipit-source-id: f525269
Summary: Some tags like `Bucket` are used, but a lot are just added to the list of tags and never read.
Reviewed By: mbouaziz
Differential Revision: D6886980
fbshipit-source-id: 4474d7f
Summary:
There's a lot of code for building up and moving around `Tags`.
When working on cleaning up some of the `Errlog` code, I noticed that `Tags` were included in the JSON and wondered why.
The answer is suprisingly just one thing: only the line tags get used, and even then they are only used to decide what frame to select as the start frame for the trace (i.e., the one that is highlighted first).
That seems like overkill; starting on trace on the actual line where the error occurs, starting at the beginning of the procedure where the error occurs, or starting at the first line of the trace all seem equally reasonable.
If we are happy with any of these alternatives, we can kill `Tags` altogether and potentially save a decent amount space in our JSON artifacts.
Reviewed By: mbouaziz
Differential Revision: D6876752
fbshipit-source-id: 1580127
Summary:
- Combine two fields from ProcAttributes.t into a single field `method_kind` with more information
- New field details whether the procedure is an `OBJC_INSTANCE`, `CPP_INSTANCE`, `OBJ_CLASS`, `CPP_CLASS`, `BLOCK`, or `C_FUNCTION`
- `is_objc_instance_method` and `is_cpp_instance_method` fields no longer necessary
- Changed `is_instance` field in CMethod_signature to `method_kind` field of type ProcAttributes.method_kind
Reviewed By: dulmarod
Differential Revision: D6884402
fbshipit-source-id: 4b916c3
Summary: If the procedure is defined, then the attributes should be the same on the specs files or on the attributes table.
Reviewed By: sblackshear
Differential Revision: D6910086
fbshipit-source-id: 709b290
Summary:
Record "capture phases" in the runstate and in the source files table of the
database. Use this instead of filesystem timestamps to decide which files need
re-analyzing in the reactive analysis.
Reviewed By: jeremydubreil
Differential Revision: D6760833
fbshipit-source-id: 7955621
Summary:
- During backend execution, infer will log detailed stats about procedure analysis
- Logging is integrated with EventLogger
- `events_to_log` field added to Stats.t record in InferPrint
- New format in InferPrint - Logs
- `format_list` type changed to have a Utils.Outfile option to support Logs format
Reviewed By: dulmarod
Differential Revision: D6834538
fbshipit-source-id: 8c847f5
Summary:
The infer results directories in buck-out/ are "cleaned up" to avoid polluting
the Buck cache with too much data or non-deterministic data. In particular, the
runstate is deleted, which confused subsequent infer processes trying to read
the pre-existing results directory.
Add a special case in infer to delete pre-existing results directories in
buck-out instead of trying to load their state.
Reviewed By: mbouaziz
Differential Revision: D6845128
fbshipit-source-id: 5c716aa
Summary:
Before this diff, the `Ondemand` module would not cache the results of the function `analyze_proc_desc`, which is used by the toplvel iteration.
This should not have any effect on the performances at this point as the summaries were already cached in the `Specs` module. Now, we can start remove the use of the cache in the `Specs` module to avoid the duplication. Caching at the level of `Ondemand` is better as we can safely cache the information that the outcome of the analysis is `None`, which avoids scanning the filesystem or the DB multiple times.
Reviewed By: mbouaziz, jvillard
Differential Revision: D6713546
fbshipit-source-id: 309701b
Summary: This should allow to report several occurences of the an issue appearing several times within the same method.
Reviewed By: jvillard
Differential Revision: D6783298
fbshipit-source-id: 5555906
Summary:
The captured variables of a closure are tuples (id, var, typ) with the implicit assumption
that &var -> id holds in the heap. This is true when the closure is created, but is not enforce otherwise.
This becomes a problem when the closure is stored in the heap, goes passed a bi-abduction, and then it's executed
(see new test). This was failing before this diff and now succeeds.
We add the verification of this constraint to the normalization of sigma.
At the moment I expect Precondition_not_met to be removed, but also later, we will be able to compute retain cycles
over the closures, as the correct captured variable info is kept through the execution.
Reviewed By: jvillard
Differential Revision: D6796525
fbshipit-source-id: a8a7655
Summary:
Not sure what an "iCFG" is but the dotty is only about CFGs anyway.
Diff obtained by mass-`sed`.
Reviewed By: sblackshear
Differential Revision: D6324280
fbshipit-source-id: b7603bb
Summary:
Also make it optional, since it's only used for debug messages. Name a couple
more of these for other similar functions.
Reviewed By: sblackshear
Differential Revision: D6797385
fbshipit-source-id: e6e9b2e
Summary:
I needed to do this for something, now I don't know if I want to do the thing
anymore but this seems generally useful to decrease a little bit the size of
Config.ml.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6796427
fbshipit-source-id: d9c009d
Summary:
Also, make it explicit when we load the global tenv instead of the per-file tenv.
This allows for some nice simplifications in some places, notably:
- `tenv_file` is gone from `Exe_env.file_data`
- `DB.global_tenv_fname` is no more
This will help moving the tenv from the capture/source_file/ directories on the
filesystem to the database, as keys for the relevant table are `SourceFile.t`.
Reviewed By: mbouaziz
Differential Revision: D6796594
fbshipit-source-id: 1ffd5b0
Summary:
They were constructed for each source file, and then joined into a global call
graph, only to get per-file lists of procedures. A tad wasteful.
Get this list from cfgs instead. Still record them in `exe_env` for now as
changing that code is a whole other beast.
One test falls victim of the flakiness of the analysis of recursive functions.
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D6324268
fbshipit-source-id: d5ff58f
Summary:
Last piece of significant logic relying on the call graph: the execution
environment. Mostly carve out the logic to detect duplicate symbols to not rely
on the call graph.
Also make the keys of the `file_map` be source files, because not having the
"cg filename" makes it harder otherwise.
Reviewed By: sblackshear
Differential Revision: D6621196
fbshipit-source-id: cab50ba
Summary:
In preparation for getting rid of call graphs, we need to find another way to
get the list of defined procedures (which is the only place where we use the
globally-computed call graph for now).
The natural way to get the list of procedures defined in a file is to load the
cfg for that file and look at the proc names that are the keys of the cfg. This
is way too expensive, as the CFG is big. Thus, we cache this list of proc names
as another column in the SQLite database of cfgs. This gives good performance
in benchmarks.
Reviewed By: jeremydubreil
Differential Revision: D6621142
fbshipit-source-id: ed265fe
Jules Villard
Mehdi Bouaziz
Jeremy Dubreil
Nikos Gorogiannis
Dulma Churchill
Varun Arora
Sam Blackshear
Dino Distefano
Josh Berdine
Sungkeun Cho
Daiva Naudziuniene
Tony Hu