Summary:
The deadcode checker is poorly written and as a result is more useful than
intended!
Reviewed By: mbouaziz
Differential Revision: D8088654
fbshipit-source-id: 19a94b8
Summary: Use AccessExpressions instead of AccessPath in uninit analysis. This will allow us to distinguish between pointers and their dereferences.
Reviewed By: jvillard
Differential Revision: D8042359
fbshipit-source-id: 604bcbc
Summary:
It improves the precision of widening operations of interval:
upper_bound_widen (min(n, s), s) = s
lower_bound_widen (max(n, s), s) = s
Reviewed By: mbouaziz
Differential Revision: D8038941
fbshipit-source-id: 61b10cb
Summary:
Labels inside switch statements were causing havoc (see test), and the translation of switch statements in general could be improved to handle more cases.
It turns out that `case` (and `default`) statements are more or less fancy labels into the code. In other words, if you erase all the `case XXX:` and `default:` strings in the `switch` statement you get the real structure of the program, and `switch` just jumps straight to the first `case` directives (and to the second if the first one is not satisfied, etc. until all `case`/`default` have been considered).
This suggests an alternative implementation: translate the body of the `switch` and simply record the list of switch cases inside that body, along with where they point to. Then post-process this list to construct the control flow of the `switch`, which points into the control-flow of the `body`. In order not to modify every function in `CTrans` to propagate the current list of cases, I created an ugly `ref` inside `SwitchCase` instead (but it cannot be directly accessed and it's guaranteed to be well-parenthesised wrt nested switches by the `SwitchCase` API so it's not too bad).
[unrelated] Also make translation failures output more information about what exactly in the source code is causing the crash, and the ancestors in the AST that lead to the crash site.
Reviewed By: martinoluca
Differential Revision: D8011046
fbshipit-source-id: 8455090
Summary: Moving this function since it's about a single procdesc. Slight rewrite too.
Reviewed By: da319
Differential Revision: D8030494
fbshipit-source-id: f7cc58e
Summary:
- Reorder modules in mli for readability.
- Match mli module order in the implementation.
- Move some functions that operate on domains from RacerD.ml to the domain file.
- Kill some module type invocation.
- Use standard module signatures.
Reviewed By: mbouaziz
Differential Revision: D8026386
fbshipit-source-id: ee2af22
Summary: Method overloading creates the potential for report duplication even though the reports are actually distinct. Make the report message unique by not using shortened method names.
Reviewed By: jeremydubreil
Differential Revision: D8005862
fbshipit-source-id: 53d8ea0
Summary: Follow C++ in having local variables owned plus silence reports on paths rooted on logical vars. We need both because when propagating ownership from right to left, the initial status of a temp var as owned is lost.
Reviewed By: sblackshear
Differential Revision: D7988575
fbshipit-source-id: 2e817d7
Summary: There was a bit of code and comments referring to potential soundness. Kill those.
Reviewed By: da319
Differential Revision: D8004256
fbshipit-source-id: c20b62a
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: Fixing the support for single core analysis in 8ce79a0613 was improving the performance of the genrule-based integration by more that 2X. Running Infer in single core more with the external compiler integration for Buck also improves the performance significantly.
Reviewed By: mbouaziz
Differential Revision: D7989255
fbshipit-source-id: 71fb842
Summary:
This diff:
- translates C++ `catch` blocks
- adds an exceptional control-flow edge from the end of a `try` block to the beginning of a `catch` block
This obviously doesn't reflect the way exceptions actually work, but I think it is better than what we have now. For one thing, we'll see/translate code inside `catch` blocks, which were opaque before. If Clang analyses don't want this behavior, they can simply use `ProcCfg.Normal` (which, up until this diff, behaved identically to `ProcCfg.Exceptional`.
In the future, we can extend `trans_state` to track blocks that might throw an exception, and have each of these blocks transition to `catch` instead.
Reviewed By: jvillard
Differential Revision: D7814521
fbshipit-source-id: 67b86a6
Summary:
- delete getter for `CContext.context.procdesc`
- change API of `CLocation`, in particular to take just a source file instead of a `CContext` since that's all they need (but maybe we'd rather type less?)
- thread `source_range` of source statement to where useful for logging (could do more in the future)
Reviewed By: da319
Differential Revision: D7950573
fbshipit-source-id: 2755f7d
Summary: Makes sense given that they share a lot of the same `Intent`-related sinks.
Reviewed By: mbouaziz
Differential Revision: D7877282
fbshipit-source-id: 38b2040
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
Mehdi Bouaziz
Jules Villard
Ezgi Çiçek
Dino Distefano
Sam Blackshear
Daiva Naudziuniene
Martino Luca
Dulma Churchill
Sungkeun Cho
Nikos Gorogiannis
Jeremy Dubreil
Jose Blanco
Oliver Castillo
Brandon Kieft
Tony Hu
Frédéric Bour
Josh Berdine