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
Dulma Churchill
Sungkeun Cho
Sam Blackshear
Jules Villard
Nikos Gorogiannis
Ezgi Çiçek
Daiva Naudziuniene
Mehdi Bouaziz
Jeremy Dubreil
Martino Luca
Jose Blanco
Oliver Castillo