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, always log failures.
This also shows that the dead code detection does not detect dead exceptions :/
Reviewed By: jeremydubreil
Differential Revision: D6796843
fbshipit-source-id: 3d0ff5c
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:
The custom exception does not appear to serve any purpose. Also refactor the
complaining code to avoid duplication.
Reviewed By: mbouaziz
Differential Revision: D6784945
fbshipit-source-id: a2d969b
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: At each call to `Component$Builder.build()`, checks that the required props for `Component` have been set via prior calls to the `Builder`. Does not yet handle `Prop(optional = true)`, but will address that in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D6735524
fbshipit-source-id: 0c812fd
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:
Previously imports with relative filenames would not get resolved so the result
would depend on where infer had been run from. Usually this was the project
root. Now, resolve path names of imports relative to the file doing the
`#IMPORT`. This changes behaviour most of the time.
Reviewed By: dulmarod
Differential Revision: D6784740
fbshipit-source-id: 4ccb7bf
Summary:
This changes the syntax for AL imports from `#IMPORT <file>` to `#IMPORT
"file"`. As a side-effect, the `file` part is now lex'd more permissively too.
Reviewed By: dulmarod
Differential Revision: D6784669
fbshipit-source-id: cc1bb73
Summary:
- During program translation, infer logs details about SelfClassException exceptions that are caught
- Logging is integrated with EventLogger library, uses existing FrontendException event type
- ast_node field in FrontEndException record used to store SelfClassException class_name field
- SelfClassException exception type extended to add support for storing exception details
- All instances where SelfClassException exception is raised modified to pass these details
Reviewed By: mbouaziz
Differential Revision: D6760513
fbshipit-source-id: a8efa9d
Summary:
- During program translation, infer logs details about IncorrectAssumption exceptions that are caught
- Logging is integrated with EventLogger library, uses existing FrontendException event type
- IncorrectAssumption exception type extended to add support for storing exception details
- All instances where IncorrectAssumption exception is raised modified to pass these details
Reviewed By: mbouaziz
Differential Revision: D6759287
fbshipit-source-id: 64f520e
Summary:
This avoids rebuilding the man pages at every build. Also add a `byte_infer`
target to build infer in bytecode + the models, and an `opt` target, as I found
myself missing those.
Reviewed By: mbouaziz
Differential Revision: D6761008
fbshipit-source-id: ffedd4b
Summary:
Reading a different .inferconfig makes little sense and is in contradiction
with the fact that we try hard to make all the infer processes agree on the set
of options.
Reviewed By: sblackshear
Differential Revision: D6761146
fbshipit-source-id: 67a0c54
Summary:
- During program translation, infer logs details about Unimplemented exceptions that are caught
- Exception type, source location, exception triggering location, and the ast_item it occurred in
- Logging is integrated with EventLogger library
- New type of event in EventLogger
- Unimplemented exception type extended to add support for storing these extra details
- All instances where unimplemented exception is raised modified to pass these details
Reviewed By: dulmarod
Differential Revision: D6748734
fbshipit-source-id: 725c7f3
Summary:
and add mli. We already had the logic for iterating over call chains, but it was overfitted to the should-update analysis.
Will use the generalized version in a follow-up.
Reviewed By: jvillard
Differential Revision: D6740692
fbshipit-source-id: 8c0d89f
Summary:
Getting double-logged messages when logs have not yet been setup is confusing,
so just don't log these messages to a log file.
Reviewed By: mbouaziz
Differential Revision: D6739173
fbshipit-source-id: 14db6b0
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:
`&::.*-->` allows to match any path end.
Used for models of `std::array` to force unmodelled functions (and types) to have a Skip summary
Depends on D6408415
Reviewed By: jvillard
Differential Revision: D6611203
fbshipit-source-id: 6663b2c
Summary:
In buck queries, the `regex` in `kind(regex, ...)` is open, it can match superstrings, like `prebuilt_cxx_library` when we want `cxx_library` instead.
This adds `^` and `$` to our existing kind filtering.
Also optimizes the query in `buck_target_determinator.py`.
Reviewed By: dulmarod
Differential Revision: D6722665
fbshipit-source-id: 22d839f
Summary:
Facebook Open Source provides a Code of Conduct statement for all projects to follow, to promote a welcoming and safe open source community.
Exposing the COC via a separate markdown file is a standard being promoted by Github via the Community Profile in order to meet their Open Source Guide's recommended community standards.
Adding this file will improve the [Infer community profile](https://github.com/facebook/infer/community) checklist and increase the visibility of our COC.
Reviewed By: jvillard
Differential Revision: D6724173
fbshipit-source-id: 88e6f37
Summary:
Horrible but somewhat-documented hack to get inter-file dead code analysis for
the OCaml code.
Reviewed By: mbouaziz
Differential Revision: D6724234
fbshipit-source-id: 3a5b9cd
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:
- After completing program translation, infer logs # of attempted procedure translations and # of completed procedure translations via EventLogger
- New possible type of event in EventLogger
Reviewed By: dulmarod
Differential Revision: D6711662
fbshipit-source-id: 5e31332
Summary:
- After completing program translation, infer logs # of attempted procedure translations and # of completed procedure translations
- New global state in cFrontend_config.ml to represent # of attempted procedure translations and # of failed procedure translations
- Will be integrated with logging framework
Reviewed By: dulmarod
Differential Revision: D6703248
fbshipit-source-id: 10c916a
Summary:
In Java, static variables are distinguished by package/class:
the file where they are defined doesn't matter.
Fixes#831.
Closes https://github.com/facebook/infer/pull/833
Reviewed By: jeremydubreil
Differential Revision: D6661240
Pulled By: sblackshear
fbshipit-source-id: beeb2f9
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
Dulma Churchill
Jules Villard
Sam Blackshear
Varun Arora
Martino Luca
Tony Hu
Jeremy Dubreil
Mehdi Bouaziz
Radu Grigore