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
Summary:
Record the db schema, infer version, and run dates into
infer-out/.infer_runstate.json. This allows us to check on startup whether the
results directory was generated using a compatible version of infer or not, and
give a better error message in the latter case than some SQLite error about
mismatching tables.
This will be used in a follow-up diff to record capture phases too, and avoid
relying on filesystem timestamps of the infer-out/capture/foo/ directories for
reactive analysis.
Had to change some tests Makefiles to make sure they do not attempt to re-use
stale infer-out directories, which would now fail the run.
The stale infer-out directory gets deleted if `--force-delete-results-dir` is
passed (but a warning still gets printed).
Reviewed By: mbouaziz
Differential Revision: D6760787
fbshipit-source-id: f36f7df
Summary:
This declutters `CommandLineOption` a little bit, and will be useful in a
follow-up diff where `InferCommand.t` will be used from an atd-generated file.
Reviewed By: mbouaziz
Differential Revision: D6772990
fbshipit-source-id: 3d32d00
Summary:
Was trying to decide where to add a new Java utility function and realized that things are a bit disorganized.
Some operations on `Typ.Name.t`'s live in `Typ.Procname`, and some live inside an inner `Java` module whereas some are outside of the module with a `java_` prefix.
Let's move toward putting all Java/C/Objc/C++-specific functions in dedicated modules.
This diff does some of the work for Java.
There are Java-specific functions that operate on `Typ.Procname.t`'s that will have to be converted to work on `Typ.Procname.Java.t`'s, but changing those clients will be more involved.
Will also move C/Objc/C++ functions in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D6737724
fbshipit-source-id: cdd6e68
Summary: Use the Hashtbl functions directly as `Cfg` knows that a cfg is a hashtbl.
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D6727732
fbshipit-source-id: 2cdda91
Summary:
Found the dead code with the script in the next commit, iteratively until no
warnings remained.
Methodology:
1. I kept pretty-printers for values, which can be useful to use from infer's REPL (or
when printf-debugging infer in general)
2. I kept functions that formed some consistent API (but not often, so YMMV), for instance if it looked like `Set.S`, or if it provides utility functions for stuff in development (mostly the procname dispatcher functions)
3. I tried not to lose comments associated with values no longer exported: if the value is commented in the .mli and not the .ml, I moved the comment
4. Some comments needed updating (not claiming I caught all of those)
5. Sometimes I rewrote the comments a bit when I noticed mis-attached comments
Reviewed By: mbouaziz
Differential Revision: D6723482
fbshipit-source-id: eabaafd
Summary:
Almost all the files are supposed to do this. When they don't, the build adds
it automatically anyway, but it's better to always include it to avoid
confusion (and help other automated tools).
Reviewed By: mbouaziz
Differential Revision: D6723285
fbshipit-source-id: 0fe8a16
Summary: This should make no difference as the `Ondemand` would already only run the analysis when the procedure description is found, and naturally skip the analysis otherwise.
Reviewed By: sblackshear, jvillard
Differential Revision: D6705813
fbshipit-source-id: 44bffee
Summary:
This is a more accurate type since an execution environment is always a single
file, and allows us to make one of the fields of `Exe_env.t` immutable.
Reviewed By: mbouaziz
Differential Revision: D6620477
fbshipit-source-id: 9553516
Summary:
This avoids relying on the directories in infer-out/captured/ being created,
and instead gets the list of captured source files from the DB. This gives a
better type to clusters: `SourceFile.t` instead of `DB.source_dir`, which makes
the code a bit nicer too.
Reviewed By: jeremydubreil
Differential Revision: D6620460
fbshipit-source-id: c0edbf6
Summary: This should avoid making copies of procedure descriptions which are mutable data-stuctures.
Reviewed By: sblackshear
Differential Revision: D6658527
fbshipit-source-id: 688a142
Summary: There was several implementations of the same function accross the codebase
Reviewed By: sblackshear
Differential Revision: D6658266
fbshipit-source-id: e12507b
Summary: Filtering the defined procedure at this level is not necessary. This check already happens when running the analysis in Ondemand. This could also cause flakiness if the "definedness" here does not agree with the check done in Ondemand. The fact that the analysis of a procedure is triggered from the top-level iteration or on-demand when analyzing another procedure is not deterministic.
Reviewed By: sblackshear
Differential Revision: D6575057
fbshipit-source-id: ff0bc2d
Summary:
Upgrade ocamlformat to 0.3, and (necessarily) base to v0.10.0.
- Fix accumulated mis-formatting
- Update opam.lock to unbreak clean build
- Update to base v0.10.0
- Update opam.lock for base
- Update offline opam repo
- Everyone should already have removed their ocamlformat pin
- ocamlformat 0.3 supports output to stdout natively
- bump version of ocamlformat
Reviewed By: jeremydubreil
Differential Revision: D6636741
fbshipit-source-id: 41a56a8
Summary: This is to allow the bi-abduction analysis and the nullable checker for Clang languages to run together without stepping on each other toes.
Reviewed By: sblackshear
Differential Revision: D6567934
fbshipit-source-id: a318c33
Summary:
Instead of storing the cfgs of source files inside their own individual files,
put them in results.db, in their own table. (that table may change in the
future to map source files to more than just their cfgs, eg their tenv as well)
Reviewed By: jberdine
Differential Revision: D6297201
fbshipit-source-id: 7fa891d
Summary:
This diff adds a layer of report deduplication logic in addition to
the existing scheme.
Suppose issue 1 with trace1a and trace1b, and issue 2 with trace2a and
trace2b. If trace1a ends at the same location as trace2a (resp.,
trace2b) and trace1b ends at the same location as trace2b (resp.,
trace2a), then consider issues 1 and 2 to be duplicates.
This chooses to report the issue with the smaller sum of trace
lengths, breaking ties using the issue hashes, and eventually the
entire issue. Therefore there is a potential for flakiness with
respect the the choice of which report to make within a
hash-equivalence class.
Reviewed By: sblackshear
Differential Revision: D6519607
fbshipit-source-id: 63210ab
Summary: As Dulma pointed out, adding or removing paramters in a method in Objective C is changing the name of the method. Such changes should not make pre-exisiting issues reported as introduced. This diff is to prevent this by only keeping in the bug hash the part of the name that is before the first colon.
Reviewed By: dulmarod
Differential Revision: D6491215
fbshipit-source-id: 3c00fae
Summary: For the Buck integration for Java, caching when a summary is not found avoids going through the whole classpath every time a summary for the same method is not found.
Reviewed By: mbouaziz, jvillard
Differential Revision: D6402833
fbshipit-source-id: 4feb422
Summary: This will avoid collisions when the inner classes are implementing the same methods. For example, the previous version of the bug hash could conflate the issues when several annonymous inner classes are implementing the same method, e.g. a annonymous subclass of `Runnable` implementing `run()`.
Reviewed By: sblackshear
Differential Revision: D6461594
fbshipit-source-id: 2bb8545
Summary:
Simpler bug hash that is more independent of the underlying analysis. This now computes the hash based on:
- the bug type.
- the base filename: i.e for my/source/File.java, just keep File.java. So the hash will not change when moving files around.
- the simple method name: i.e. without package information and list of parameters. So changing the list of parameters will not affect the bug hash.
- the error message were the line numbers have been removed. So moving code or reformatting will not affect the hash.
Reviewed By: jberdine
Differential Revision: D6445639
fbshipit-source-id: 82e3cbe
Summary:
Summaries can be big, and they can always be printed via `infer report` if we want to see them.
There's no reason to log them eagerly, even in debug mode.
Reviewed By: jeremydubreil
Differential Revision: D6451815
fbshipit-source-id: 643cd47
Summary: In every place this was used except one, `debug_mode` is also used as a gate.
Reviewed By: jeremydubreil
Differential Revision: D6450913
fbshipit-source-id: 6a5716d
Summary:
It seems that the abstraction instructions were not previously added the the CFG.
This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.
Reviewed By: sblackshear, jvillard
Differential Revision: D6383672
fbshipit-source-id: cedcb8a
Summary:
Deduping issues when generating a single report and then diffing the
reports can lead to introduced issues being considered duplicates of
existing issues.
Reviewed By: sblackshear
Differential Revision: D6414673
fbshipit-source-id: bba81fd
Summary: I accidentally deleted the support for `infer report file.specs` which was printing the summary to standard output.
Reviewed By: sblackshear
Differential Revision: D6416690
fbshipit-source-id: 62246f3
Summary:
The diff is very big but it's mostly removing code. It was inspired by the fact that we were getting Dead Store FPs because we were modeling some functions from CoreFoundation and CoreGraphics directly as alloc in the frontend, which caused the parameters of the function to be seen as dead. See the new test.
To deal with this, if we are going to skip the function, we model it as malloc instead. Given how many models we had for those "model as malloc" functions, I removed them to rely solely on the new mechanism.
The modeling of malloc and release was still based on the old retain count implementation, even though all we do here is a malloc/free kind of analysis. I also changed
that to be actually malloc/free which removed many Assert false in the tests. CFRelease is not exactly free though, and it's possible to use the variable afterwards. So used a custom free builtin that only cares about removing the Memory attribute and focuses on minimizing Memory Leaks FPs.
Otherwise we were translating CFBridgingRelease as a special cast, and this wasn't working. To simplify this as well, I removed all the code for the special cast, and just modeled CFBridgingRelease and CFAutorelease also as free_cf, to avoid Memory Leak false positives. I also treated the cast __bridge_transfer as a free_cf model. This means we stopped trying to report Memory Leaks on those objects.
The modeling of CoreGraph release functions was done in the frontend, but seemed simpler to also simplify that code and model all the relevant functions.
Reviewed By: sblackshear
Differential Revision: D6397150
fbshipit-source-id: b1dc636
Summary:
This is a good moment to close Sqlite's DB handles, and in general can be used to postpone some actions right before infer terminates.
Since exiting is done via uncaught exception handling, the `late_epilogue` callback will run at the very end, even after all the `at_exit` callbacks have been invoked. The only exception is made in case of signalling, in which case the `late_epilogue` is still invoked, but before any of the `at_exit` callbacks.
Reviewed By: jvillard
Differential Revision: D6404961
fbshipit-source-id: 8ff7a05
Summary: There is a lot of code to create LaTeX output of the Infer datastructures, but this does not seem to be used anymore.
Reviewed By: jvillard
Differential Revision: D6355686
fbshipit-source-id: 55de8e9
Summary:
This field was always empty.
depends on D6351097
Reviewed By: sblackshear, jvillard
Differential Revision: D6351243
fbshipit-source-id: 4a74bea
Summary: This option was for compatibility with the command line options of the previous, but is no longer used. This diff removes the option and the deprecated code.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6351097
fbshipit-source-id: 0e4cfc5
Summary:
This was already dead code that didn't know it was dead, doubly so:
1. Only active with `-a biabduction`, which is deprecated
2. Doesn't do anything since it somehow always iterates over an empty list of procedures (I don't really know why that is, but testing shows this is the case)
Reviewed By: jeremydubreil
Differential Revision: D6348430
fbshipit-source-id: 230d05d
Summary:
Naming a variable `_foo` makes the compiler not warn about them if they are
unused, but there are lots of instances of such variables in the code where
they are in fact used, defeating the warning and introducing confusion for
those used to this naming convention.
Basically `sed -i -e "s/ _\([a-zA-Z][a-zA-Z0-9_']*\)/ \1_/g" **/*.ml` followed
by manual fixing of compilation errors (lots of `compare__foo` ->
`compare_foo_`).
Reviewed By: mbouaziz
Differential Revision: D6358837
fbshipit-source-id: 7ffb4ac
Summary: This information is already available in the procedure name.
Reviewed By: jeremydubreil, jvillard
Differential Revision: D6119459
fbshipit-source-id: f07bfde
Summary:
`infer capture -a checkers ...` would accidentally trigger the analysis phase.
This crashes the Buck flavors integration when used with `--reactive` because
.start never gets created in the infer-out-* subfolders of buck-out.
Reviewed By: dulmarod
Differential Revision: D6336072
fbshipit-source-id: af0ab5e
Summary:
We need to use the procedure description of the callees for lazy dynamic dispatch and for the resolution of the lambda. We may also need this information in other analyses, e.g. for RacerD. This diff makes the procedure description of the callees as part of the summary.
The procedure description has been part of the summary for a while already without noticeable decrease in performance.
Reviewed By: mbouaziz
Differential Revision: D6322038
fbshipit-source-id: 84101cb
Summary:
Change ocamlformat installation procedure to use opam instead of
pinning.
Reformat all code with v0.2, which has a few improvements.
Reviewed By: jvillard
Differential Revision: D6292057
fbshipit-source-id: 759967f
Summary:
This diff adds a new way of executing blocks when they are passed as parameters to a method. So far we just skipped the block in this case.
Now we can execute it. Let's demonstrate with an example. Say we have
//foo has a block parameter that it executes in its body
foo (Block block) { block();}
// bar calls foo with a concrete block
bar() {
foo (^(){
self->x = 10;
});
};
Now, when we call the method foo with a concrete block, we create a copy of foo instantiated with the concrete block, which in itself is translated as a method with a made-up name.
The copy of foo will get a name that is foo extended with the name of the block parameter, the call to the block parameter will be replaced to a call to the concrete block, and the captured variables
of the concrete block (self in this case), will be added to the formals of the specialized method foo_block_name.
This is turned on at the moment for ObjC methods with ObjC blocks as parameters, and called with concrete blocks. Later on we can extend it to other types of methods, and to C++ lambdas, that are handled similarly to blocks.
Another extension is to check when the block has been called with nil instead of an actual block, and raise an error in that case.
After this diff, we can also model various methods and functions from the standard library that take blocks as parameters, and remove frontend hacks to deal with that.
Reviewed By: ddino
Differential Revision: D6260792
fbshipit-source-id: 0b6f22e
Summary:
This confuses the SIOF checker and causes false positives. This dummy deref is
generated for constructors of classes that are modeled as being pointer types
instead of the actual class in infer, typically for smart pointers. I do not
understand how this works.
The biabduction also analyses this code, so might now get confused itself.
Reviewed By: jberdine
Differential Revision: D6221817
fbshipit-source-id: 050c5a9
Summary: The Java bytecode does not contain information about the location of abstract of interface methods. Before this diff, the analysis trace was tuncated and the file where the abstract or interface method was not included in the trace, which makes it harder to understand the Infer report, especially when the method is on a generated file that is not checked in the repository.
Reviewed By: sblackshear
Differential Revision: D6223612
fbshipit-source-id: c80c6f2
Summary:
This diff takes the first step toward a more general filtering
system. This step is concerned only with filtering at the reporting
stage, filtering for the capture and analysis stages is left for
later.
This diff adds a new command line / config option
```
--filter-report +string
Specify a filter for issues to report. If multiple filters are
specified, they are applied in the order in which they are
specified. Each filter is applied to each issue detected, and only
issues which are accepted by all filters are reported. Each filter
is of the form:
`<issue_type_regex>:<filename_regex>:<reason_string>`. The first
two components are OCaml Str regular expressions, with an optional
`!` character prefix. If a regex has a `!` prefix, the polarity is
inverted, and the filter becomes a "blacklist" instead of a
"whitelist". Each filter is interpreted as an implication: an issue
matches if it does not match the `issue_type_regex` or if it does
match the `filename_regex`. The filenames that are tested by the
regex are relative to the `--project-root` directory. The
`<reason_string>` is a non-empty string used to explain why the
issue was filtered.
See also infer-report(1) and infer-run(1).
```
Reviewed By: jvillard
Differential Revision: D6182486
fbshipit-source-id: 9d3922b
Summary: This check is deprecated and will be replaced by a dedicated checker to detect unitialized values.
Reviewed By: mbouaziz
Differential Revision: D6133108
fbshipit-source-id: 1c0e9ac
Summary:
Install ocamlformat from github as part of `make devsetup`, and use it
for formatting OCaml (and jbuild) code.
Reviewed By: jvillard
Differential Revision: D6092464
fbshipit-source-id: 4ba0845
Summary:
Refactor `RegisterCheckers` to give a record type to checkers instead of a tuple type.
Print active checkers with their per-language information.
Improve the manual entries slightly.
Reviewed By: sblackshear
Differential Revision: D6051167
fbshipit-source-id: 90bcb61
Summary:
This will allow most of the checkers, except the bi-abduction, to skip the analysis on the specialized clone of the methods used to handle dynamic dispatch. Doing this, we can run the bi-abduction analysis using:
infer -a checkers --biabduction
without risk of conflicts on the resolution of dynamic dispatch.
Reviewed By: sblackshear
Differential Revision: D6052347
fbshipit-source-id: 0c75bf3
Summary:
1. Mark some Makefile targets as depending on `MAKEFILE_LIST` so they get rebuilt on Makefile changes
2. Do not show boolean options with no documentation in the man pages (like we do for other option types).
3. Default to Lazy dynamic dispatch for the checkers.
4. In the tests, use `--<checker>-only` instead of relying on `--no-default-checkers`
5. `--no-filtering` is redundant if `--debug-exceptions` is passed
Reviewed By: jeremydubreil
Differential Revision: D6030578
fbshipit-source-id: 3320f0a
Summary:
Another step toward running the biabduction analysis as a checker.
Depends on D6038210
Reviewed By: jvillard
Differential Revision: D6038682
fbshipit-source-id: fed45bf
Summary:
The previous version of the code was trying to lookup from disk the procedure description of the procedure to analyze, which was in fact already loaded in memory.
This diff fixes one of the issues preventing the bi-abduction to run as a checker when using the lazy dynamic dispatch algorithm.
Reviewed By: sblackshear
Differential Revision: D6038210
fbshipit-source-id: 10a98ee
Summary:
`pp_instr_list` was not tailrec causing a stack overflow on big code.
Also simplified a few things
Reviewed By: jvillard
Differential Revision: D5995451
fbshipit-source-id: 40a4911
Summary:
The biabduction backend can raise exceptions that will be caught when triggered
from within the biabduction backend itself (eg, `analyze_procedure` called from
Symexec as a result of an ondemand analysis, because Symexec will catch these),
but not caught when called as the result of an ondemand analysis emanating from
another analyzer (eg ThreadSafety).
Make the biabduction more self-contained by wrapping the analysis of a
procedure inside a `try/with` with similar properties as the one of Symexec.
Reviewed By: jeremydubreil
Differential Revision: D5986335
fbshipit-source-id: 36a5d32
Summary:
Running `infer report foo.specs` would overwrite report.json with an empty json.
Only recompute report.json when running `infer-analyze` or `infer-run`.
Reviewed By: mbouaziz
Differential Revision: D5963500
fbshipit-source-id: e579c6f
Summary:
Use a monotonic time source instead.
Also, sleep between retries in the Serialization code.
Reviewed By: jberdine
Differential Revision: D5941697
fbshipit-source-id: 05efbe1
Summary: Not sure if useful but seems sensible. It disappears at the top of the stack when we do merging in SQL.
Reviewed By: mbouaziz
Differential Revision: D5824131
fbshipit-source-id: fd64752
Summary:
Use an SQLite database to store proc attributes, instead of files on disk.
Wrap SQLite operations in two layers:
1. `SqliteUtils` provides helper functions to make sure DB operations succeed
2. `KeyValue` provides a functor to expose a simple and type-safe key/value store backed by the SQLite DB.
Reviewed By: jberdine
Differential Revision: D5640053
fbshipit-source-id: 31050e5
Summary:
This diff does two things:
# Infer no longer add the contrains that the return value of a skip function is never null. This was leading to false negatives and is not necessary as those return value are treated angelically
# Infer now support `Nonnull` on the return value of skip functions.
Reviewed By: jberdine, sblackshear
Differential Revision: D5840324
fbshipit-source-id: bbd8d82
Summary:
`reraise` was error-prone when one forgot to save the backtrace between where the exception is caught and where it is reraised.
If any exception was raised (even caught) in between, the printed backtrace would be the one of the last exception thrown and it would be very confusing.
This diff kills `reraise` and introduces `reraise_after exn ~f` and `reraise_if exn ~f` to be used right after catching the exception.
Also turned some of them to the common pattern `try_finally ~f ~finally`.
Reviewed By: jvillard
Differential Revision: D5911244
fbshipit-source-id: 9883d1e
Summary:
The only language types we have are Java/Clang/Python. The unit of analysis is a source file, and you can't write a source file that mixes two or more of these languages (to the best of my knowledge).
This diff simplifies using the assumption that all procedures in a file are written in the same language.
Reviewed By: jeremydubreil
Differential Revision: D5886942
fbshipit-source-id: 88c3759
Summary:
The only language types we have are Java/Clang/Python. The unit of analysis is a source file, and you can't write a source file that mixes two or more of these languages (to the best of my knowledge).
This diff simplifies using the assumption that all procedures in a file are written in the same language.
Reviewed By: jeremydubreil
Differential Revision: D5886942
fbshipit-source-id: 8555a16
Summary: Only Eradicate uses this, no need to create it for every checker.
Reviewed By: jeremydubreil
Differential Revision: D5886775
fbshipit-source-id: 7242437
Summary:
A Java cluster checker currently defines a "cluster" as all of the procedures in the same class.
But the cluster checker actually knows about all the procedures defined in the same source file.
In some checkers (such as thread-safety), we want to aggregate results across classes in the same file, not just methods in the same class.
This refactoring leaves the behavior the same for now, but will make it easier to do this in the near future.
Reviewed By: jeremydubreil
Differential Revision: D5885896
fbshipit-source-id: 0815fca
Summary:
Calling functions that raise exceptions (even if they get caught) may smudge
the backtraces we get from OCaml. We need to record the original backtrace
*before* calling such fuctions on the path between catching an exception and
reraising it.
Also change the heptuple returned by `Exceptions.recognize_exception` into a
record type, and make that function not raise when classifying exceptions.
Reviewed By: jberdine
Differential Revision: D5882934
fbshipit-source-id: 8e99fe8
Summary: The point of the tracing mode is to compute all the possible path leading to an error state. However, within a method, many of those paths are not feasibile in practice. This leads to many false alarms for the resource leak analysis.
Reviewed By: sblackshear
Differential Revision: D5888695
fbshipit-source-id: 2dbc57b
Summary:
Since D5381239, infer is careful not to delete directories that do not "look
like" results directories on startup, in case the user passed, eg, `-o /`.
In our repo, lots of results dir are created by build/test of infer, and when
the version of infer changes and the expected contents of results directories
change then it might start refusing to delete the results directories created
with another version of infer.
Add an option to force infer to delete the results directory no matter how
dodgy it looks, and use it in our repo by adding the option in every
.inferconfig.
Reviewed By: mbouaziz
Differential Revision: D5870984
fbshipit-source-id: 09412de
Summary:
This can be a long-running step and it's useful to know how long it took. We
already dump some statistics on stderr after merging is done, this just adds
one more line.
Reviewed By: mbouaziz
Differential Revision: D5833580
fbshipit-source-id: 70e19ab
Summary:
Simple instance of the problem: analyzing the following program times out.
```
#include <tuple>
void foo() {
std::tuple<std::tuple<int>> x;
}
```
Replacing `std::tuple<std::tuple<int>>` by `std::tuple<int>` makes the analysis
terminate.
In the AST, both tuple<tuple<int>> and tuple<int> have the same template
specialization type: "Pack" (which means we're supposed to go look into the
arguments of the template to get their values). This is not information enough
and that's the plugin fault.
On the backend side, this means that two types have the same Typ.Name.t, namely
"std::tuple<_>", so they collide in the tenv. The definition of
tuple<tuple<int>> is the one making it into the tenv. One of the fields of the
corresponding CxxRecord is of type "tuple<int>", which we see as the same
"tuple<_>", which causes the loop.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D5775840
fbshipit-source-id: 0528604
Summary:
Sort the complete set of warnings by everything except procname, then de-duplicate.
This scheme prevents reporting identical error messages on the same line/same file.
This is important for avoiding duplicate reports on multiple instantiations of the same template.
Reviewed By: jberdine
Differential Revision: D5819467
fbshipit-source-id: 984f47f
Summary: The resolution was previously only happening for constructors, but calls to private methods or to `super` are also neither static calls nor virtual calls. In this case, the resolution logic should be the same as for constructors.
Reviewed By: sblackshear
Differential Revision: D5830376
fbshipit-source-id: 9b56f80
Summary:
The reporting phases iterates over each procedure summary and print all the issues from each procedure.
That's nice because we don't have to build a big list of the issues in-memory, but it's not so nice if you want to ouput the reports in a certain order or de-duplicate them.
This diff builds the in-memory list and outputs the issues afterward. By itself, this isn't very useful. But in the near future it will allow us to:
- Group all of the issues from the same file (finally!!!)
- Get rid of duplicate issues on multiple instantiations of the same C++ template
- Probably other cool stuff too
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D5816646
fbshipit-source-id: 799bcd0
Summary:
"Running as clang" was its own infer subcommand. That's not terribly good
because it makes it hard to specify another subcommand, and in particular it
broke the `compile` subcommand in some integrations because "running as clang"
would always do capture. The cmake tests required to run with `--keep-going`
because of this.
Instead of having its own fake subcommand, simply add a new boolean in the
config for "infer runs as clang", as we do for javac already (used in the mvn
integration).
Also make logging of the environment better.
Reviewed By: jberdine
Differential Revision: D5813986
fbshipit-source-id: 72b96cd
Summary: I often find myself needing a generic `Pp.seq` where I can specify the separator.
Reviewed By: jeremydubreil
Differential Revision: D5803915
fbshipit-source-id: fb8d30d
Summary: Try to preserve the original backtrace. Introduce `reraise` in the global namespace.
Reviewed By: jberdine
Differential Revision: D5804121
fbshipit-source-id: 0947a47
Summary: With this diff, the analysis trace will jump to the definition of the skipped methods when the location is known. This is especially useful when the analysis is relying on the method annotations.
Reviewed By: sblackshear
Differential Revision: D5783428
fbshipit-source-id: 561b739
Summary: With Logging.exit you have more control of the code that invokes exit, for example when forking and running certain functions that may in turn invoke exit, and you want to handle the execution flow differently - like invoking certain callbacks before exiting, or not exiting at all.
Reviewed By: jvillard
Differential Revision: D5746914
fbshipit-source-id: 596fba1
Summary:
We supported globals as sources before, but we did so by allowing ClangTrace etc. to match against any access path in the footprint of the trace.
This is very powerful/flexible, but it's ultimately not a good idea because it leads to traces that are hard to read.
This is because a footprint source doesn't have any information about its provenance: we might know that the value came from a global, but we don't know where the read occurred.
The mechanism for handling procedure calls as sources already knows how to solve this problem.
This diff implements globals as sources as a special case of procedure call sources instead.
This will give us much nicer traces with full provenance of the read from the global.
Reviewed By: mbouaziz
Differential Revision: D5772299
fbshipit-source-id: 491ae81
Summary: It is not clear to me what the removed code was for in the first place. Basically, it was replacing the pure part of propositions in a semantically equivalent way, e.g. replacing `a = b /\ Attribute(a)` to `a = b /\ Attribute(b)`, and `a = b /\ Attribute(b)` to `a = b /\ Attribute(a)`.
Reviewed By: jberdine
Differential Revision: D5657366
fbshipit-source-id: 93cd9e0
Summary: We used to crash whenever we hit these. The simple translation implemented here is not particularly inspiring, but it is better than crashing.
Reviewed By: jvillard
Differential Revision: D5702095
fbshipit-source-id: 3795d43
Summary: This adds an option to only translate the body of a method when the file matches the give pattern. This is especially intended to be use for generated files.
Reviewed By: jvillard
Differential Revision: D5729120
fbshipit-source-id: 1e28469
Summary: With this, we can now get now get inter-procedural issues involving native methods.
Reviewed By: sblackshear
Differential Revision: D5730638
fbshipit-source-id: 3bdbdbd
Summary: Atoms of the form `identifier = footprint var` naturally occurs with the angelic analysis mode. So it is not clear to me why we should drop those.
Reviewed By: sblackshear
Differential Revision: D5654754
fbshipit-source-id: 9dd2eb5
Summary:
- failwith police: no more `failwith`. Instead, use `Logging.die`.
- Introduce the `SimpleLogging` module for dying from modules where `Logging`
cannot be used (usually because that would create a cyclic dependency).
- always log backtraces, and show backtraces on the console except for usage errors
- Also point out in the log file where the toplevel executions of infer happen
Reviewed By: jeremydubreil
Differential Revision: D5726362
fbshipit-source-id: d7a01fc
Summary: This makes the traces more readable when involving skipped functions.
Reviewed By: sblackshear
Differential Revision: D5731683
fbshipit-source-id: 49d363b
Summary:
This simplifies the jbuild files: no need to list these files explicitly
anymore, nor to exclude them explicitly from the main `InferModules` library
(due to their different compilation flags).
Isolate common parts into jbuild.common do `cat`-based code inclusion into
jbuild files to factorize code.
Reviewed By: jberdine
Differential Revision: D5678328
fbshipit-source-id: 6d7d925
Summary: In case of syntax errors in AL files, stdout will contain a JSON list with all files affected by the errors, including info like filename and line number.
Reviewed By: dulmarod, jvillard
Differential Revision: D5640272
fbshipit-source-id: 569b16d
Summary: This check is not possible in Java as it natirally happens in the totally legit case of the `try ... finally`.
Reviewed By: sblackshear
Differential Revision: D5568802
fbshipit-source-id: 24ca074
Summary:
Instead of a whitelist and blacklist and default issue types and default
blacklist and filtering, consider a simpler semantics where
1. checkers can be individually turned on or off on the command line
2. most checkers are on by default
3. `--no-filtering` turns all issue types on, but they can then be turned off again by further arguments
This provides a more flexible CLI and is similar to other options in the infer
CLI, where "global" behaviour is generally avoided.
Dynamically created checkers (eg, AL linters) cause some complications in the
implementation but I think the semantics is still clear.
Also change the name of the option to mention "issue types" instead of
"checks", since the latter can be confused with "checkers".
Reviewed By: jberdine
Differential Revision: D5583238
fbshipit-source-id: 21de476
Summary:
This gives additional information to users. For instance:
```
--biabduction
Activates: the separation logic based bi-abduction analysis using
the checkers framework (Conversely: --no-biabduction)
This option is relevant to infer-analyze(1).
```
Reviewed By: sblackshear
Differential Revision: D5583197
fbshipit-source-id: 2960b90
Summary:
The only path to the `MergeCaptured.slink` function is when we should merge, so
it doesn't make sense to check `Config.merge` again. In the case of `infer run
--flavors -- buck ...`, this would create regular symlinks instead of the much
faster multilinks.
Reviewed By: jberdine
Differential Revision: D5574020
fbshipit-source-id: df710ca
Summary:
This is a needed step in the direction of making prenalysis functional: it will return a view of the CFG rather than mutating the CFG.
ProcCfg already works by providing a view on the underyling CFG, but the bi-abduction can't leverage this because it uses the "raw" CFG.
This diff does a partial swap of the raw CFG for an exceptional ProcCfg. The goal is to make sure the bi-abduction never calls `Procdesc.get_instrs`; it should use the `ProcCfg` wrapper instead.
That way, preanalyses that add instructions (like the liveness prenalysis) will work.
There's still some calls to `Procdesc.get_succs` etc., but we can remove those in a future diff.
They're not on the critical path because the current preanalyses only add instructions, not nodes or edges.
Reviewed By: jeremydubreil
Differential Revision: D5556387
fbshipit-source-id: 4ffda00
Summary: Useful for identifying user-controlled array accesses that could lead to buffer overflows
Reviewed By: mbouaziz
Differential Revision: D5520985
fbshipit-source-id: 92984f6
Summary: This is unused, as far as I can tell. If we want to revive it, we can do it in AL or as a simple checker; it certainly doesn't require the full might of bi-abduction.
Reviewed By: jeremydubreil
Differential Revision: D5556325
fbshipit-source-id: e3895c2
Summary:
Replace `inferTraceBugs` with `infer-explore` with a similar CLI. Some options changed:
- --max-level -> --max-nesting, and "max" is the default value instead of a possible value
- --no-source -> --no-source-preview
Reviewed By: mbouaziz
Differential Revision: D5526651
fbshipit-source-id: 8383f37
Summary:
In some cases we normalize expressions to check some facts about them. In these
cases, trying to keep as much information as possible in the expression, such
as the fact it comes from a `sizeof()` expression, is not needed. Doing
destructive normalization allows us to replace `sizeof()` by its
statically-known value.
closes#706
Reviewed By: mbouaziz
Differential Revision: D5536685
fbshipit-source-id: cc3d731
Summary:
Do not use the deprecated (and slower) `#infer` flavor. Instead, `infer-run`
runs capture with the `#infer-capture-all` flavor, followed by merging targets,
followed by the analysis.
Move the call to `MergeCapture` around to make this change easier.
Reviewed By: mbouaziz
Differential Revision: D5547199
fbshipit-source-id: 53c9996
Summary: Those are not particularly relevant for the biabduction analysis. It would be easy to have a dedicated checker for this if we happen to need one day.
Reviewed By: sblackshear
Differential Revision: D5530834
fbshipit-source-id: 316e60f
Summary:
The Eradicate `Nullable` checker should now be run using:
infer -a checkers --eradicate ...
Reviewed By: mbouaziz
Differential Revision: D5529226
fbshipit-source-id: 0de2956
Summary:
This is unsound but will help the analysis to report less false alarms with the common pattern:
if (a.get() != null) {
a.get().foo();
}
Reviewed By: sblackshear
Differential Revision: D5528227
fbshipit-source-id: 750db4a
Summary:
Previously, only the bug type + file name (up to renaming) were taken into
account, which was too coarse. The key is file-independent and provides
additional signal.
Reviewed By: martinoluca
Differential Revision: D5536858
fbshipit-source-id: 70b732b
Summary: This was reusing the side effects of the `add_constraints_on_retval` for the final purpose of being angelic and just assigning a fresh value to the lhs of the load.
Reviewed By: sblackshear
Differential Revision: D5507037
fbshipit-source-id: ec1c89c
Summary: This seems more in line with the expectations of the JSON format.
Reviewed By: mbouaziz
Differential Revision: D5500939
fbshipit-source-id: 76dcc47
Summary: This used to be in a different module but now that `driver_mode` is in `Driver` it should really be called `Driver.mode`.
Reviewed By: mbouaziz
Differential Revision: D5499575
fbshipit-source-id: ab96473
Summary:
If you run `infer report --issues-txt ilovecats.txt ...` then bugs may mysteriously miss from `ilovecats.txt`, unless you flush. (See rules of thumb for `Format` module.)
Closes https://github.com/facebook/infer/pull/694
Reviewed By: mbouaziz
Differential Revision: D5442335
Pulled By: jvillard
fbshipit-source-id: 73272a0
Summary: Using a dedicated abstract domain, like Quandary does, is more suitable for taint analysis.
Reviewed By: sblackshear
Differential Revision: D5473794
fbshipit-source-id: c917417
Summary:
Both `stringWithUTF8String` and `stringWithString` implements copy semantics that copies the content of their parameter into a newly allocated buffer. We modeled this as pointer assignment in the past, which means that once we write
```
NSString* foo() {
char buf[...];
...
return [NSString stringWithUTF8String:buf];
}
```
We are going to get a spurious stack variable address escape report because local pointer `buf` is assigned to the newly created string and the string gets returned.
This diff tries to address the issue by heap-allocating a buffer and `memcpy` the contents in `stringWithUTF8String` and `stringWithString`. But this change will create another problem: the allocated buffer will be reported as leaked by the backend, while in reality those buffers won't actually be leaked as they are allocated in a region that will be periodically autoreleased. To suppress spurious memory leak FPs, I added another attribute `Awont_leak` that will suppress the leakage report on any expressions that get tagged with it.
Reviewed By: jeremydubreil
Differential Revision: D5403084
fbshipit-source-id: df6de7f
Summary:
First steps towards implementing diff analysis functionalities inside infer
itself. What works: run infer, checkout parent, re-run infer, checkout top
revision, compute the reportdiff (but no final surfacing on the console). Lots
of TODO still, inlined in the code.
Reviewed By: jberdine
Differential Revision: D5364226
fbshipit-source-id: 5b7f9a5
Summary:
Allowing the user to configure where to store the JSON report is asking for
trouble. In fact, some places in the code hardcoded "results.json" anyway.
Someone wanting to have results.json somewhere else can still copy report.json
once infer has run.
Reviewed By: jberdine
Differential Revision: D5415079
fbshipit-source-id: 9439cb6
Summary: Introduce `Logging.die` to try and exit with consistent error codes depending on what failed.
Reviewed By: mbouaziz
Differential Revision: D5406642
fbshipit-source-id: 25d98fc
Summary: This will allow us to gradually get rid of the exceptions thrown during the analysis while detecting the regressions earlier
Reviewed By: jberdine, jvillard
Differential Revision: D5385154
fbshipit-source-id: 605e3f5
Summary:
Conversion and reformat of infer source using ocamlformat
auto-formatting tool.
Current status:
- Because Reason does not handle docstrings, the output of the
conversion is not 'Warning 50'-clean, meaning that there are
docstrings with ambiguous placement. I'll need to manually fix
them just before landing.
Reviewed By: jvillard
Differential Revision: D5225546
fbshipit-source-id: 3bd2786
Summary: This will allow to replace type vars into concrete types in expressions.
Reviewed By: jvillard, mbouaziz
Differential Revision: D5209276
fbshipit-source-id: c1650f8
Summary: This is useful when we only want to examine the html for some but not all source files.
Reviewed By: jvillard
Differential Revision: D5334786
fbshipit-source-id: 774c23c
Summary: Rename historical option to its new form, since the old form was no longer accepted by infer.
Reviewed By: martinoluca
Differential Revision: D5329033
fbshipit-source-id: 4fa9402
Summary:
We keep track of both `beginPtr` and `endPtr` but the modelling was mostly
about `beginPtr` as some sort of approximation I guess. This shouldn't change
much but will be useful later when doing more iterator stuff.
Reviewed By: mbouaziz
Differential Revision: D5255772
fbshipit-source-id: 0f6e3e8
Summary:
This will be needed to re-use the functions now in Driver.ml in other contexts
without always adding to infer.ml. For instance, this is used in a later diff
to do a diff-analysis orchestrator that needs to run the capture and analysis
several times.
Reviewed By: jberdine
Differential Revision: D5319862
fbshipit-source-id: caf9551
Summary: Needed in a later diff to be able to compute the set of changed files *during* an infer execution.
Reviewed By: jberdine
Differential Revision: D5319667
fbshipit-source-id: 226ec91
Summary:
Thanks to the logging introduced in D5293334 (or because of, depending on your liking of spam), I noticed that there lots of errors being logged of the form
Couldn't read multilink file '/home/jul/infer/infer/tests/codetoanalyze/cpp/errors/infer-out/attributes/d0/multilink.txt': /home/jul/infer/infer/tests/codetoanalyze/cpp/errors/infer-out/attributes/d0/multilink.txt: No such file or directory
I don't think it makes sense to care about multilink files except when `--merge` is specified.
Also introduced a .mli and self-documented a function.
Reviewed By: akotulski
Differential Revision: D5310129
fbshipit-source-id: c3a6276
Summary:
Once the fixed/preexisting/introduced sets have been computed, they endure
further filtering which may decide that more of them are equal. These bugs just
get dropped on the floor. Put these into preexisting as well instead, at least
in the case of the "skip_duplicated_types_on_filenames" filter.
Reviewed By: martinoluca
Differential Revision: D5274248
fbshipit-source-id: 99b3f3d
Summary: This change introduces the a new argument that lets you restrict the results of a differential report to only certain files.
Reviewed By: mbouaziz
Differential Revision: D5236626
fbshipit-source-id: 52711e9
Summary:
Only one instance will win in the end so it's not useful to double register.
Log when that happens. Currently it happens in the Java tests on
`InferBuiltins` but I don't understand why so I left it alone.
Reviewed By: jberdine
Differential Revision: D5217928
fbshipit-source-id: dc7ccca
Summary:
This avoids race conditions when two processes or more try to lock a file for
writing. It could be that the process losing the race writes less than the
winner, then we get rubbish at the end of the file. Calling `ftruncate(2)` inside the critical section makes sure the
contents of the file are erased first. The harmful race was observed in
xcodebuild sometimes, as it can call infer on the same file several times in
parallel (!).
Reviewed By: jberdine
Differential Revision: D5209177
fbshipit-source-id: 744169c
Summary: I tested on Fresco and this reduced the number of calls to Prover.check_disequal by 30%.
Reviewed By: cristianoc
Differential Revision: D5237774
fbshipit-source-id: 377545e
Summary:
Now that we can run several inter-procedural analyses at the same time, we should no longer use the function `Reporting.log_error_deprecated` as it logs the errors in the specs table. This specs table is normally used for caching and will be deprecated in favor of having a cache summaries for the callees in the `Ondemand` module (to avoid deserialising a callee more than once within the same process).
This revision just renames the reporting functions.
Reviewed By: sblackshear
Differential Revision: D5205009
fbshipit-source-id: b066549
Summary:
This messes up with the Buck cache: if infer recaptures a file with only trivial changes that shouldn't affect the capture Buck will still believe it has to reanalyze everything that depends on that file if there's non-deterministic data in infer's output.
Re-use the `--buck` flag used by the Java Buck integration for mostly the same purposes. Add a few special cases for the flavours integration (eg: keep capture data).
Change perf stats registration to take `Config.buck_cache_mode` into account instead of relying on each call site to handle that peculiarity correctly. Also, there's no need to create the perf stats directories before calling the registration function since it will do that too.
Reviewed By: jeremydubreil
Differential Revision: D5192311
fbshipit-source-id: 334ea6e
Summary:
It is not used, so one fewer thing to track inside Python.
Note that Python does pass `--buck` to OCaml infer to make it aware that it is
running from within Buck, and the OCaml code uses that flag to trim infer-out
to only what's strictly necessary (and especially to remove non-deterministic
output that would mess with Buck's cache).
Reviewed By: jberdine
Differential Revision: D5200043
fbshipit-source-id: 1c84442
Summary:
Change the API of `Logging` wrt to writing to files and to the console (see
changes in logging.mli).
Write only to one log file: infer-out/log. Prefix each line with the kind of
warning and the PID of the process emitting it. Writing with `O_APPEND` is
atomic so the file should not get garbled by concurrent writes. To get the
output of a single process, find out which one interests you by looking at
infer-out/log, then `grep ^[<PID>] infer-out/log`.
Introduce 3 log levels for debug output and command-line options to set them
for various categories individually.
Change tons of `"\n"` to `"@\n"` so the `Format` module is aware of newlines
without us having to look through every character of every logged string for
`\n` characters.
Reviewed By: mbouaziz
Differential Revision: D5165317
fbshipit-source-id: 93c922f
Summary:
Introduce a new option `--no-report` (conversely `--report`) to stop reporting
after the analysis. This is useful to call sub-`infer-analyze` processes with
as they shouldn't compute "result.json" or report bugs to stderr. This bug
would only manifest itself when per-procedure parallelism disabled, which
explains why it was noticed only on Java.
Reviewed By: jberdine
Differential Revision: D5182110
fbshipit-source-id: a892470
Summary:
The logic is not that simple and this will be needed in a later diff to create
the log file as early as possible.
Reviewed By: jberdine
Differential Revision: D5173128
fbshipit-source-id: 830f105
Summary: This also allows us to better test that the new commands will keep working.
Reviewed By: jeremydubreil
Differential Revision: D5172891
fbshipit-source-id: 169bd6f
Summary:
Now `infer analyze` really has the same behaviour as `infer -- analyze`.
Previously it wouldn't create report.json or report.
Reviewed By: jeremydubreil
Differential Revision: D5172875
fbshipit-source-id: 8f9ddd1
Summary:
This will be needed higher up in the stack because the new `ProcessPool` module
will need to call into `Logging` to refresh the logging formatters to get the
right PID when writing to the log file.
+remove dead code `iter_parallel`
Reviewed By: jberdine
Differential Revision: D5165130
fbshipit-source-id: 95c949b
Summary: Allow type variables in `Typ.desc`. It will be used to store template type arguments.
Reviewed By: jberdine
Differential Revision: D5154757
fbshipit-source-id: 55b8e81
Summary: The previous error message recommended annotating the method in question with `GuardedBy`, which doesn't actually work.
Reviewed By: jeremydubreil
Differential Revision: D5149661
fbshipit-source-id: d935aec
Summary:
A recent diff tried to replace `L.out "error message"; assert false` with
`failwith "error message"` but infer relies on the type of raised exceptions to
sometimes keep going. A more careful change will be needed but in the meantime
restore the old behaviour.
Reviewed By: jberdine
Differential Revision: D5112969
fbshipit-source-id: 713fe20
Summary: There were some leftover uses of the `Tracing` analyzer option. While I was at it, I also rename the `Config` option name.
Reviewed By: jberdine
Differential Revision: D5113489
fbshipit-source-id: 68d5cc8
Summary:
Try and enforce the following rules:
- stderr is for updating the user about progress or errors
- Introduce Logging.progress that outputs to stderr, but honours --quiet
- Logging.stderr is as before
- Logging.out now prints to stderr (or to log files as before if set up) and
not stdout. If some information should go on stdout then the user should be
able to rely on it (ie, it's not just some progress message). For now only
the summary of the errors is printed on stdout by default.
- Logging.err* functions are gone. If the error is user-visible, it should be
Logging.stderr, or `failwith`. If not, go to the same log file as other
output, which personally I find much more convenient than having to dig through
2 log files every time I'm looking for some output.
Reviewed By: jberdine
Differential Revision: D5095720
fbshipit-source-id: 68999c9
Summary:
`infer analyze ...` (and `InferAnalyze` before it) was not actually running the
analysis in parallel, unlike `infer -- analyze`, which we want to deprecate.
Reviewed By: jberdine
Differential Revision: D5095676
fbshipit-source-id: ec28465
Summary:
After:
```
$ infer run -- clang -c examples/hello.c
Capturing in make/cc mode...
Found 1 source file to analyze in /home/jul/infer/infer-out
Starting analysis...
legend:
"F" analyzing a file
"." analyzing a procedure
F.
Found 1 issue
examples/hello.c:14: error: NULL_DEREFERENCE
pointer `s` last assigned on line 13 could be null and is dereferenced at line 14, column 3
12. void test() {
13. int* s = NULL;
14. > *s = 42;
15. }
Summary of the reports
NULL_DEREFERENCE: 1
```
Before, legend and analysis run were separated by 2 lines, one is now before
and the other is in the log files only:
```
Capturing in make/cc mode...
Starting analysis...
legend:
"F" analyzing a file
"." analyzing a procedure
Found 1 (out of 1) source files to be analyzed in /home/jul/infer/infer-out
per-procedure parallelism jobs:4
F.
Found 1 issue
examples/hello.c:14: error: NULL_DEREFERENCE
pointer `s` last assigned on line 13 could be null and is dereferenced at line 14, column 3
12. void test() {
13. int* s = NULL;
14. > *s = 42;
15. }
Summary of the reports
NULL_DEREFERENCE: 1
```
Reviewed By: mbouaziz
Differential Revision: D5069590
fbshipit-source-id: 8843422
Summary: The issues that are not reported by default are all experimental issues from the biabduction analysis. In that case, it is easier to use a blacklist of errors to filter out so that the issues found by the checkers based on the AI framework can be reported by default without having to add them to the whitelist.
Reviewed By: jvillard
Differential Revision: D5051327
fbshipit-source-id: 2a93b11
Summary:
An array has a static or dynamic length (number of elements), but it also has a
stride, determined by the type of the element: `sizeof(element_type)`. We don't
have a good `sizeof()` function available on SIL types, so record that stride
in the array type.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D4969697
fbshipit-source-id: 98e0670
Summary:
Introduce `infer-<command>` for each command, except for internal commands
(only `infer-clang` for now) which are not exported. Install these executables
(which are just symlinks to `infer`) on `make install`. The main executable
looks at the name it was invoked with to figure out if it should behave as a
particular command.
Get rid of `InferClang`, `InferAnalyze`, and `InferPrint`. As a bonus, we now
only need to build one executable: `infer`, which should be a few seconds
faster (less link time).
`InferAnalyze` is now `infer-analyze` and `InferPrint` is `infer-print`. To run
`InferClang`, use a symlink named `clang`, `clang++`, etc. to `infer`. There
are such symlinks available in "infer/lib/wrappers/" already.
I also noticed that the scripts in xcodebuild_wrappers/ don't seem useful
anymore, so use wrappers/ instead, as for `make`.
Reviewed By: mbouaziz
Differential Revision: D5036495
fbshipit-source-id: 4a90030
Summary:
Glorious, glorious man pages.
This changes a bunch of things that were hard to break up from the diff, so the
resulting diff is big.
Use `Cmdliner.Manpage` to format man pages (and also format a bit ourselves
since it is so stubborn).
As a bonus, introduce the following subcommands:
```
infer run ... # same as default mode with -- before
infer capture ... # -a capture
infer compile ... # -a compile
infer analyze ... # InferAnalyze
infer report ... # InferPrint
infer diff ... # this one is not new
infer clang ... # InferClang, not that you should use it
```
The man pages can still be improved a lot. Notable missing sections:
`ENVIRONMENT`, stuff about .inferconfig, some example usage, `DESCRIPTION`, ...
Reviewed By: jberdine
Differential Revision: D4921083
fbshipit-source-id: 9602230
Summary:
With this change, running the biabduction analysis with
infer -a infer -- ...
or with:
infer -a checkers --biabduction -- ...
take the same time and give the same list of results.
Reviewed By: sblackshear
Differential Revision: D5026676
fbshipit-source-id: ef23911
Varun Arora
Sungkeun Cho
Dulma Churchill
Jules Villard
Daiva Naudziuniene
Jeremy Dubreil
Sam Blackshear
Tony Hu
Josh Berdine
Martino Luca
Stephan Walters
anuolu
Mehdi Bouaziz
Dino Distefano
Jia Chen
Radu Grigore
Andrzej Kotulski
Don Stewart