Summary:
Before we were computing the size of an abstract state (`range`) using the `NonNegativeBound` domain but it wasn't able to express product of symbolic values.
This diff introduces a domain for that.
The range of an interval is still computed in `NonNegativeBound` but then the product is done in `TopLiftedPolynomial` so all costs end up being of that type.
The //symbols// of a polynomial are `NonNegativeBound` (so the polynomial only represent non-negative values, perfect for a cost), which handles substitution correctly, i.e. it gives zero instead of negative values.
Reviewed By: ddino
Differential Revision: D7397229
fbshipit-source-id: 6868bb7
Summary:
The annotation UiThread can, and is, used on classes as opposed to just methods, so extend the modelling to account for this.
Also, consider the annotation hereditary.
Reviewed By: jeremydubreil
Differential Revision: D7910762
fbshipit-source-id: 0df2c81
Summary:
Java arrays have an internal length that can be retrieved with the internal `__get_array_length`.
Here is a model for it.
Reviewed By: jvillard
Differential Revision: D7931572
fbshipit-source-id: fd4c179
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:
Move the biabduction-specific payloads (the "`'a spec`" stuff) from specs.ml
into a new `BiabductinoSummary` module, similar to other checkers.
Reviewed By: ngorogiannis
Differential Revision: D7935815
fbshipit-source-id: bdff3b9
Summary:
Previously, the type of `trans_result` contained a list of SIL expressions.
However, most of the time we expect to get exactly one, and getting a different
number is a soft(!) error, usually returning `-1`.
This splits `trans_result` into `control`, which contains the information
needed for temporary computation (hence when we don't necessarily know the
return value yet), and a new version of `trans_result` that includes `control`,
the previous `exps` list but replaced by a single `return` expression instead,
and a couple other values that made sense to move out of `control`. This allows
some flexibility in the frontend compared to enforcing exactly one return
expression always: if they are not known yet we stick to `control` instead (see
eg `compute_controls_to_parent`).
This creates more garbage temporary identifiers, however they do not show up in
the final cfg. Instead, we see that temporary IDs are now often not
consecutive...
The most painful complication is in the treatment of `DeclRefExpr`, which was
actually returning *two* expressions: the method name and the `this` object.
Now the method name is a separate (optional) field in `trans_result`.
Reviewed By: mbouaziz
Differential Revision: D7881088
fbshipit-source-id: 41ad3b5
Summary: When passing `--genrule-mode` option, Infer will remove the logs and the other kind of data that are not compatible with the Buck distributed cache.
Reviewed By: mbouaziz
Differential Revision: D7943346
fbshipit-source-id: 4e7ca4d
Summary: With the genrule approach, the directory the generated script is run from is inside `buck-out`. So we need to specify the project root before calling the `buck` command.
Reviewed By: mbouaziz
Differential Revision: D7938130
fbshipit-source-id: c265476
Summary: It seems that we don't need to rely on `make` anymore as the internal process manager is working fine on Buck Java projects.
Reviewed By: jvillard
Differential Revision: D7903639
fbshipit-source-id: 9b32f05
Summary:
This is an attempt to make things more consistent, and maybe save some work
from the `Format` module in case flambda doesn't have our backs.
Reviewed By: jberdine
Differential Revision: D7775496
fbshipit-source-id: 59a6314
Summary: Make errors stand out with colours. Also improve error messages around save states.
Reviewed By: mbouaziz
Differential Revision: D7928794
fbshipit-source-id: c81cfe2
Summary: Without the class name, it is not always clear from the error message where the method expecing non-null parameters defined.
Reviewed By: mbouaziz
Differential Revision: D7919492
fbshipit-source-id: 044fb83
Summary: I needed it for debugging but, to my dismay, it was borked again. This time it was because `jbuilder` moved the object files to another directory since the last jbuilder update.
Reviewed By: mbouaziz
Differential Revision: D7926267
fbshipit-source-id: 42ad26a
Summary:
Make the starvation checker enabled by default.
Add a deadlock issue type, distinct to starvation, which will be kept for UI thread starvation.
Add checks so that checker will do nothing on non-Java code.
Reviewed By: mbouaziz, ddino
Differential Revision: D7908381
fbshipit-source-id: 889f373
Summary: Historically, this option was only used to parallelize the biabduction analysis, which is now run using the checkers framework.
Reviewed By: jvillard
Differential Revision: D7895118
fbshipit-source-id: 2a54bca
Summary: Calling Future.get from UI thread, or under a lock the UI thread may try to take has been associated with ANRs.
Reviewed By: ddino
Differential Revision: D7859296
fbshipit-source-id: b87bd94
Summary:
One source of non-determinism is racing on procedure summaries when reporting. In particular, the summary of a method may be computed and stored by one thread, but another may be trying to report on it (eg, in cluster checkers).
One solution (at least until everything is in sqlite) is to have separate files just for the reports, a la linters. This diff improves the interface of LintIssues and generalises it ahead of using it in other analysers.
Reviewed By: jeremydubreil
Differential Revision: D7859973
fbshipit-source-id: 8672d3b
Summary: Folly has a macro SYNCHRONIZED(..) {...} which boils down to the creation/destruction of a LockedPtr object, doing the locking/unlocking. Add support for that.
Reviewed By: sblackshear
Differential Revision: D7844847
fbshipit-source-id: c7a146d
Summary: std::lock allows for locking multiple lockable objects, while avoiding deadlock. This will fix some FPs in C++.
Reviewed By: da319
Differential Revision: D7844198
fbshipit-source-id: 2b7140a
Summary:
We had a semantics for ownership of prefix paths in mind (see comment), but it was enforced partially in the domain and partially in the transfer functions.
Moving all of the logic into the domain makes things much cleaner/shorter.
Reviewed By: ngorogiannis
Differential Revision: D7845981
fbshipit-source-id: 4a2da95
Summary:
The Cost analysis uses `Bound` for non-negative values only, let's make it a separate module (and abstract type).
This also separates the abstract domain part of `Bound` which we wanted anyway.
Depends on D7844267
Depends on D7843351
Depends on D7782184
Reviewed By: ddino
Differential Revision: D7844572
fbshipit-source-id: 0e6b620
Summary: We were wrongly using the underapproximation of `min` rather than the overapproximation
Reviewed By: ddino
Differential Revision: D7844267
fbshipit-source-id: c9d9247
Summary:
This simplifies the frontends and backends in most cases. Before this diff,
returning `void` could be modelled either with a `None` return, or a dummy
return variable with type `Tvoid`. Now it's always the latter.
Reviewed By: sblackshear, dulmarod
Differential Revision: D7832938
fbshipit-source-id: 0a403d1
Summary:
The abstract interpreter tried to handle exceptional control-flow by propagating the *pre* of a block that threw an exception rather than the *post*.
This was a half-measure that isn't correct when an exception-throwing instruction isn't in the middle of a block.
The handling of exceptions wasn't actually used anywhere and was leading to further hacks in `ProcCfg`, so let's get rid of it.
Reviewed By: mbouaziz, jvillard
Differential Revision: D7843872
fbshipit-source-id: 2a4a815
Summary: Returning the list of sub-expressions is not right and can cause assertion failures elsewhere in the frontend.
Reviewed By: dulmarod
Differential Revision: D7813493
fbshipit-source-id: 33ac9c1
Summary: It's useful for client analyses to be able to see which methods a type defines.
Reviewed By: jvillard
Differential Revision: D7813582
fbshipit-source-id: 675c041
Summary:
Needed to prevent a circular dependency between `CProcname` and `CType_decl`.
An upcoming diff will introduce a function for getting all the methods from a struct that requires both modules.
Reviewed By: dulmarod
Differential Revision: D7813367
fbshipit-source-id: b049d36
Summary: Extracting function from `get_struct_fields` and making it work for everything in the AST.
Reviewed By: jvillard
Differential Revision: D7813040
fbshipit-source-id: 082f087
Summary:
This required a translation unit context, but really all it needs is a bool specifying whether the procname is a cpp name.
Makes it easier to call this function from a place where I'll need it in the near future.
Reviewed By: jvillard
Differential Revision: D7812835
fbshipit-source-id: 7900893
Summary:
Add warning 60 (unused module) to the list of fatal warnings. Whitelisting
modules at toplevel is tricky (see inline comments) but doable.
Reviewed By: mbouaziz
Differential Revision: D7790073
fbshipit-source-id: 6f591c4
Summary:
Previously, the command parsing code filtered out any elements that were `False`y in the Python sense (starting with D5507925).
This meant that a command like `javac -classpath '' -Xmaxerrs 1000 MyFile.java` would be parsed as `javac -classpath -Xmaxerrs 1000 MyFile.java`, which will fail with "unrecognized option 1000".
This diff removes the filtering and fixes that issue.
Reviewed By: jeremydubreil
Differential Revision: D7797560
fbshipit-source-id: 63df06b
Summary:
Now that we have the abstract state at the instruction level, we don't need to reexecute instructions during the checking phase and can just query the invariant map.
Depends on D7608526
Reviewed By: skcho
Differential Revision: D7775889
fbshipit-source-id: be17e2d
Summary: Easy simplification now that we have a set of access snapshots.
Reviewed By: ngorogiannis
Differential Revision: D7754720
fbshipit-source-id: 91d0bd7
Summary:
Add a `--source-files` option to `infer explore` to print information about the source files captured by infer.
More precisely, `infer explore --source-files` will print each row of the "source_files" table in the results database.
Option `--source-files-filter` can be used to filter output to file names matching an SQLite "LIKE" pattern.
Flags `--source-files-cfgs`, `--source-files-type-environment`, `--source-files-procedure-names` and `--source-files-freshly-captured` control which columns to print.
The printers for some existing types have been tweaked to improve the output.
Reviewed By: jvillard
Differential Revision: D7735535
fbshipit-source-id: 572389a
Summary:
Now that the cost analysis doesn't hackily compute the instruction index, we can make this an abstract type to ensure `List.nth_exn` in `OneInstrPerNode` will not fail.
Depends on D7618320
Reviewed By: sblackshear
Differential Revision: D7628908
fbshipit-source-id: 89e8618
Summary:
We want instr-granular invariant maps so let's use the OneInstrPerNode CFG in the AI analyzers.
This requires specializing the TransferFunctions.
Keep using the normal CFG where we only need node-granular informations.
Depends on D7587241
Depends on D7608526
Reviewed By: sblackshear
Differential Revision: D7618320
fbshipit-source-id: 73918f0
Summary:
Now that we have a proper InstrNode, we can kill `instr_ids`!
Of course:
Depends on D7608526
Reviewed By: sblackshear
Differential Revision: D7618124
fbshipit-source-id: b3609cd
Summary:
When looking at large CFGs, at least in `xdot`, it's often difficult to find
the procedure you're looking for. Sorting the proc names puts them in
alphabetical order, which makes searching one procedure easier.
Reviewed By: mbouaziz
Differential Revision: D7758521
fbshipit-source-id: 8e9997f
Summary:
[This is a stepping stone before moving the specs data to sqlite.]
Previously, things worked like this (ignore ObjC):
1. capture & analyse C models
2. capture & analyse C++ models
3. copy C *.specs files to lib/specs/
4. copy C++ *.specs files to lib/specs/
Now it works like this:
1. capture C models
2. capture C++ models
3. analyse both together
4. install *.specs files to lib/specs
Reviewed By: sblackshear
Differential Revision: D7639322
fbshipit-source-id: 58d7c53
Summary:
It works now. Jumping to definition or calling merlin-document on files from
opam libraries doesn't seem to work when several libraries used by infer define
the same module (e.g. string.ml exists in ocaml lib, core_kernel, and base).
Reviewed By: let-def
Differential Revision: D7708218
fbshipit-source-id: 8e74b9b
Summary: Random edits made while reading ZipLib.ml. They're really not interesting, sorry...
Reviewed By: sblackshear
Differential Revision: D7686159
fbshipit-source-id: 19ef1ce
Summary:
Given a difference between two files, return the relevant lines in the new file; a line is relevant when a change took place in it, or nearby. To generate a valid input for this parser, use unix-diff command with the following formatter arguments:
```
diff --unchanged-line-format="U" --old-line-format="O" --new-line-format="N" File1 File2
```
Reviewed By: ezgicicek
Differential Revision: D7385267
fbshipit-source-id: 0cc3143
Summary:
This is to make sure we do not influence the analysis of the models by accident
when a .inferconfig exists in some directory higher up (eg, `$HOME`, infer/,
...).
Reviewed By: sblackshear
Differential Revision: D7686136
fbshipit-source-id: 9a250ff
Summary: It makes sense to run the same prelude and epilogue for `infer analyze` as for `infer run`.
Reviewed By: da319
Differential Revision: D7639363
fbshipit-source-id: 26170c1
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: We already suppress race reports if the field is marked in this way; makes sense to do the same thing for these reports.
Reviewed By: ngorogiannis
Differential Revision: D7589275
fbshipit-source-id: 8f0aeab
Summary:
We were using the "filename" as the key because it's (kinda) unique *and* human
readable, but with the `infer explore --procedures` interface we don't really
need the human readable part anymore, so we can just use the OCaml marshalling
of the pname as the key. The human-readable version (sans unique-fying hash) is
now another column in the table, used to match procedure names in
`--procedures-filter`.
Reviewed By: sblackshear
Differential Revision: D7639158
fbshipit-source-id: e714605
Summary:
Add a `--procedures` option to `infer explore` to print information about the
procedures captured by infer. More precisely, `infer explore --procedures` will
print each row of the "procedures" table in the results database. A new
`--procedures-filter` controls which procedures to print information about, and
there is one flag per column in the db too to print more or less options about
each procedure (in particular, we can now print attributes), with some defaults.
Reviewed By: sblackshear
Differential Revision: D7639062
fbshipit-source-id: 034a2b8
Summary: Currently when we look for already abduced expression and find an assertion [exp|->strexp:typexp], we use typexp rather than strexp.
Reviewed By: sblackshear
Differential Revision: D7617193
fbshipit-source-id: c089720
Summary:
Now that everything can run at the same time and we have preanalyses, it can be quite hard to read debug sessions.
Here come session names!
Depends on D7607336
Reviewed By: sblackshear
Differential Revision: D7607481
fbshipit-source-id: 676af86
Summary:
- Less `^`
- `pp_print_string` instead of `F.fprintf fmt "%s"`
- and stuff like that
Reviewed By: jvillard
Differential Revision: D7607336
fbshipit-source-id: 5d985ef
Summary:
Use an adhoc type for `StructuralConstraints` instead of hacky `Exp`s.
Also use a cleaner `Node.IdMap` instead of `Int.Map`.
Depends on D7586645
Reviewed By: ddino
Differential Revision: D7587241
fbshipit-source-id: f9d65bb
Summary:
So we can share stuff between analyses using the same CFG and node representation.
Depends on D7586302
Depends on D7586348
Depends on D7568701
Reviewed By: sblackshear
Differential Revision: D7586645
fbshipit-source-id: ed64b2c
Summary:
Run with `SHELL = bash -e -u -o pipefail` to catch many kinds of failures. We
were silently failing during `make install` because of some missing escaping,
and the failure was hidden because it was happening inside a bash `for` loop.
This fixes the escaping issue and makes sure such issues will result in an
error as of now.
Also removes dangerous `find -exec` instances: `find` will `exit 0` event if
some commands failed.
Fixes#887
Reviewed By: mbouaziz
Differential Revision: D7569054
fbshipit-source-id: 542fe50
Summary:
Let's see in later diffs if that's that useful
Instead of rebuilding these modules, let's share them
Reviewed By: sblackshear
Differential Revision: D7586302
fbshipit-source-id: de69b39
Summary:
Try to skip running even `clang -###` when we know there's nothing to capture
in the clang command. Do that by recording in the `ClangCommand.t` whether the
command is pre- or post-running `clang -###`, and apply slightly different
filters in each case. In particular, the filter has to let in more commands
than necessary pre-`clang -###` because the flags are not normalised at that
point.
Also regard `-x cuda` commands as unsupported.
Reviewed By: mbouaziz
Differential Revision: D7584934
fbshipit-source-id: c27bb63
Summary: This will facilitate accessing Inferbo abstract state at the instruction level from the Cost analysis
Reviewed By: ddino
Differential Revision: D7568701
fbshipit-source-id: 84ac648
Summary:
Got rid of `Itv.equal` which was ambiguous and use an abstract boolean type for abstract comparison results
Depends on D7568573
Reviewed By: jvillard
Differential Revision: D7568583
fbshipit-source-id: 0e897e9
Summary:
Convenience function for `prune_eq` with zero (needed for stacked diffs).
Renamed `prune_zero` to `prune_ne_zero` to avoid ambiguity.
Reviewed By: jvillard
Differential Revision: D7568556
fbshipit-source-id: b95ab6d
Summary: Only RacerD uses the Cluster callbacks but we used to compute a lot of things anyway.
Reviewed By: sblackshear
Differential Revision: D7516279
fbshipit-source-id: 22f2b86
Summary:
This information is already available in the trace, and can contain absolute
paths to system includes (or infer's own clang runtime), which confuses the
diff analysis.
Reviewed By: mbouaziz
Differential Revision: D7534609
fbshipit-source-id: 5bd8f8b
Summary:
This can be noticed when the format of the DB changes, and other fun things
like that. No longer require to `make clean` to be able to pass these tests.
Reviewed By: mbouaziz
Differential Revision: D7533559
fbshipit-source-id: 670cb60
Summary:
It renames `eval_locs` to `eval_arr` and we use it for getting array block values the given input expressions are pointing to. For example, when given a program variable `x` as an input, `eval_arr` returns array blocks that `x` is pointing to, on the other hand, `eval` returns an abstract location of `x`.
Depends on D7471891
Reviewed By: mbouaziz
Differential Revision: D7471915
fbshipit-source-id: b994944
Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).
Reviewed By: mbouaziz
Differential Revision: D7453510
fbshipit-source-id: db8738e
Summary:
It feels risky to me to swallow the `Sys_error` here since this could hide deeper issues with the deserialization of summaries.
This is only used with the Buck Integration for Java when extracting the summaries from the jar files.
Reviewed By: sblackshear
Differential Revision: D7490123
fbshipit-source-id: 68cd556
Summary:
This is unused, but the logic for keeping its value up to date was still alive
and kicking.
I don't know that making use of this flag would be easy: we could just use it
in `Ondemand.should_analyze`, but it would be unsound because a procedure might
need to be re-analysed becauese its dependencies have changed. Since there's
not code to deal with that currently I think it's best to remove it and
re-introduce it when we have some idea how to use it.
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D7444179
fbshipit-source-id: 99a1ec5
Summary:
Report nullable inconsistencies by relying on the bytecode, and not on the presence of analysis summary on disk.
This use the `--external-java-packages` to avoid reporting inconsistencies outside of the codebase.
Reviewed By: sblackshear
Differential Revision: D7481101
fbshipit-source-id: 281135d
Summary:
Utility function that's basically `Logging.progress` but with a more obvious
name for debugging.
The `[@deprecated ...]` ensures no uses gets landed, and the `[@warning "-32"]` ensures that it's not a compile error that there are no uses of this function.
Inspired by #716.
Reviewed By: mbouaziz
Differential Revision: D7443224
fbshipit-source-id: e94798f
Summary:
Without it `make` will not rebuild infer when "infer/src/infer.ml" changes
(since D7381842 moved it out of backend/).
Reviewed By: mbouaziz
Differential Revision: D7443275
fbshipit-source-id: 33ea10b
Summary:
Partial revert of a21644685f / D7381857 due to an
issue introduced in 1.0+beta19 that prevents jbuilder from generating the
correct .merlin (https://github.com/ocaml/dune/issues/657).
Reviewed By: mbouaziz
Differential Revision: D7414970
fbshipit-source-id: 10561e9
Summary:
It's already turned of systematically for the Java integration, this just
generalises it. The Buck daemon seems to cause issues with infer from time to
time that are hard to debug.
Reviewed By: jeremydubreil
Differential Revision: D7400068
fbshipit-source-id: f05ee07
Summary:
Looks like the remaining issues were solved. In particular, build the toplevel
with the same ppx as infer so that the ppx information makes it to .merlin.
Reviewed By: mbouaziz
Differential Revision: D7381857
fbshipit-source-id: 5847d56
Summary:
There's actually a nice separation between IR/, base/, istd/, and the rest of
infer, so they can be made into separate jbuilder libraries so that the
separation remains. This helps make sense of the infer codebase.
Also:
- move everything biabduction-related out of backend/ and into a new
biabduction/ directory. This clarifies the current situation where backend/
contains a mix of analysis-independent code (still there now), and
biabduction-specific code (moved to biabduction/).
- move everything from base/ that is not infer-specific into istd/, e.g. IList.ml
- kill unused `FbTraceCalls`
- A couple of files needed to move around to complete the separation of base/ and IR/
Reviewed By: mbouaziz
Differential Revision: D7381842
fbshipit-source-id: cd86dea
Summary:
If an aggregate `a` has a field `f` whose type has a constructor (e.g., `std::string`), we translate creating a local aggregate `A { "hi" }` as `string(&(a.f), "hi")`.
This diff makes sure that we recognize this as initializing `a`.
Reviewed By: jeremydubreil
Differential Revision: D7404624
fbshipit-source-id: 0ba90a7
Summary:
New command line option job-id meant to contain the Sandcastle job id
itslog
- New command line option job-id meant to contain the ID of the job that Infer is running in
- If the id is passed to infer, then log it with every row in EventLogger
Reviewed By: dulmarod
Differential Revision: D7398537
fbshipit-source-id: c5186e9
Summary: - No need to log the string of stats type when registering a perf Epilogue
Reviewed By: dulmarod
Differential Revision: D7398544
fbshipit-source-id: 681a956
Summary:
Limit the scope of what gets included into IStd.ml to only values that we want
to shadow. New values go into other files.
Also, build istd/ with `Core` open.
Reviewed By: mbouaziz
Differential Revision: D7382111
fbshipit-source-id: 969f0e8
Mehdi Bouaziz
Dulma Churchill
Nikos Gorogiannis
Martino Luca
Jose Blanco
Oliver Castillo
Jules Villard
Jeremy Dubreil
Brandon Kieft
Daiva Naudziuniene
Ezgi Çiçek
Sam Blackshear
Dino Distefano
Tony Hu
Frédéric Bour
Josh Berdine
Sungkeun Cho
Varun Arora