Summary:
- changes the `Ondemand` callbacks to take the execution environment instead of a `get_proc_desc` function.
- removes all the cases passing `get_proc_desc` as parameter to use `Ondemand.get_proc_desc` instead.
Reviewed By: jvillard
Differential Revision: D9200583
fbshipit-source-id: d16c218b5
Summary:
Exposing the in-memory cache seems dangerous. There were only 2 uses anyway:
eradicate and biabduction. I think the biabduction one is safe to remove. The
eradicate one I do not really understand as we return a different summary than
the one we cache... the tests pass though.
Reviewed By: jeremydubreil
Differential Revision: D9150167
fbshipit-source-id: cf30af232
Summary: I don't understand what this function is for. Let's remove it.
Reviewed By: mbouaziz
Differential Revision: D8320839
fbshipit-source-id: eeb14f7
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
Preparing for bigger changes...
- Rename `payload` field to `payloads`
- Move `payload` type to `Payloads.t`
- `SummaryPayload`s only have to implement a change on `Payloads.t` rather than `Summary.t`
Reviewed By: sblackshear
Differential Revision: D7987211
fbshipit-source-id: c9d7a74
Summary:
Attempt at a better naming scheme:
- `Specs.summary` are now `Summary.t`. The `Summary` module (replacing `Specs`) contains the summary of a procedure: the results of all the analyses, etc.
- `Summary.ml` is now `SummaryPayload.ml`. This concerns how each (AI) analysis extracts its payload from the master summary.
- Accordingly, checkers now define a `Payload` module where previously they defined a `Summary` module. The type is also cleaned up to use `t` instead of `payload`, etc.
- Cleaned up some names as a result, for instance `Specs.get_summary` -> `Summary.get`, etc.
Reviewed By: ngorogiannis
Differential Revision: D7935883
fbshipit-source-id: 1766545
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.
Reviewed By: jvillard
Differential Revision: D7663537
fbshipit-source-id: 3e90970
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:
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:
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:
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 field was always empty.
depends on D6351097
Reviewed By: sblackshear, jvillard
Differential Revision: D6351243
fbshipit-source-id: 4a74bea
Summary: This does not seem to be used anymore. If we happen to need this, we should update the payload, not the attributes.
Reviewed By: jberdine
Differential Revision: D6321824
fbshipit-source-id: 5c19359
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:
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: Only Eradicate uses this, no need to create it for every checker.
Reviewed By: jeremydubreil
Differential Revision: D5886775
fbshipit-source-id: 7242437
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:
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:
This is step further simplify the code to avoid cases where the summary of the procedure being analyzed can exist in two different versions:
# one version is the summary passed as parameter to every checker
# the other is a copy of the summary in the in-memory specs table
This diff implements:
# the analysis always run through the `Ondemand` module (was already the case before)
# the summary of the procedure being analyzed is created at the beginning of the on-demand analysis call
# all the checkers run in sequence, update their respective part of the payload and log errors to the error table
# the summary is store at the end of the on-demand analysis call
Reviewed By: sblackshear
Differential Revision: D4787414
fbshipit-source-id: 2d115c9
Summary:
One limitation of Eradicate is that certain nullability patterns are not expressible using simply the `Nullable` annotation.
One such pattern is using the knowledge that a function returns null when passed null, but returns an object otherwise.
The annotation `PropagatesNullable` is a variant of `Nullable` applied to parameters when their value propagates to the return value.
A method annotated
```
B m(PropagatesNullable A x) { return x == null ? x : B(x); }
```
indicates that `m` returns null if `x` is null, or an object of class `B` if the argument is not null.
Examples with multiple parameters are in the test cases.
This diff builds some infrastructure for annotation transformers: the example above represents the identity function on nullability annotations.
Reviewed By: jvillard
Differential Revision: D4705938
fbshipit-source-id: 9f6194e
Summary: Run all the checkers one after each other, which allows the Infer AI framework to run several checkers together, including the possibility for them to collaborate.
Reviewed By: sblackshear
Differential Revision: D4621838
fbshipit-source-id: e264d67
Summary:
Changes every checker to take a summary as parameter and return the updated summary to the next checker. Since several operations, like `Reporting.log_*` are modifying the summary in memory by loading them from the in-memory cache of summaries, we currently need to rely on `Specs.get_summary_unsafe` to return the updated version of the summary.
This diff allows to change the API of `Reporting` to take a summary as input and progressively remove all the calls `Specs.get_summary_unsafe` independently from adding the possibility to run several checkers at the same time. The final objective to have every checker just passing around the summary of the procedure being analyzed, and having the in-memory cache only use to store the summaries of the callees.
Reviewed By: sblackshear
Differential Revision: D4649252
fbshipit-source-id: 98f7ca7
Summary: This function was actually doing the same as `Idenv.create`.
Reviewed By: cristianoc
Differential Revision: D4654241
fbshipit-source-id: 87c098b
Summary:
This is part of the plan to have every checker take a summary as input, and return the updated sumamry as output. Doing so, we can run all the registered checkers in sequence for every method
This diff change the type of `Ondemand.analyze_ondemand` to return the analysis summary.
Reviewed By: sblackshear
Differential Revision: D4626918
fbshipit-source-id: f8ad928
Summary:
Remove the remaining uses of polymorphic equality `=`.
In case of basic types, this is replaced by String.equal or Int.equal.
In case of `= []`, this is replaced by `List.is_empty`.
In case of `= None`, this is replaced by `is_none`.
In case of a datatype definition such as `type a = A | B`,
a `compare_a` function is defined by adding `type a = A | B [@deriving compare]`
and a `equal_a` function is defined as `let equal_a = [%compare.equal : a]`.
In case of comparison with a polymorphic variant `= `Yes`, the equality
defined in `PVariant.(=)` is used. Typically, `open! Pvariant` is added
at the beginning of the file to cover all the uses.
Reviewed By: jberdine
Differential Revision: D4456129
fbshipit-source-id: f31c433
Summary:
Make the html output available to checkers when -g is used on the command-line.
A checker needs to call a function to start and finish the processing of each node,
and add prints during the processing.
This diff illustrates the case for Eradicate, by adding printing of the pre-state
and post-states.
Reviewed By: sblackshear
Differential Revision: D4421379
fbshipit-source-id: 67501ba
Summary:
Utils contains definitions intended to be in the global namespace for
all of the infer code-base, as well as pretty-printing functions, and
assorted utility functions mostly for dealing with files and processes.
This diff changes the module opened into the global namespace to
IStd (Std conflict with extlib), and moves the pretty-printing
definitions from Utils to Pp.
Reviewed By: jvillard
Differential Revision: D4232457
fbshipit-source-id: 1e070e0
Summary:
The global reference `DB.current_source` is used internally in the module DB, by all the front-ends, and directly and indirectly by the back-end, including saving and restoring the state in case of on-demand procedure calls. In particular, it is heavily used in printing functions.
This diff cleans up the flow of information about what the current file is, making it explicit, and removes the reference.
Reviewed By: jberdine
Differential Revision: D3901247
fbshipit-source-id: ef596bd
Summary:
This diff removes the redundancy in the representation of types where
struct types could be represented either directly using Tstruct or
indirectly using Tvar to refer to the type environment. A consequence
is that it is much harder to construct large type values.
Reviewed By: sblackshear, cristianoc
Differential Revision: D3839753
fbshipit-source-id: cf04ea5
Summary:
Move the Sil.attribute type and associated types and operations to a new
PredSymb module.
Reviewed By: cristianoc
Differential Revision: D3683834
fbshipit-source-id: d3606a8
Summary:public
Eliminate the use of the -open Utils command line option passed to the compiler in favor of `open! Utils` in each source file. While slightly convenient, this option causes more headaches than it is worth with other tools e.g. merlin.
Reviewed By: jvillard
Differential Revision: D3168193
fb-gh-sync-id: 4285ef6
fbshipit-source-id: 4285ef6
Jeremy Dubreil
Jules Villard
Mehdi Bouaziz
Josh Berdine
Sam Blackshear
Cristiano Calcagno
Andrzej Kotulski