Summary:
- Add nary expressions implemented using a form of multisets which
support any integer multiplicity
- Reimplement polynomials using new nary expressions
- Move the decomposition of exps into "base plus offset" form into
Exp, to enforce simplification invariants
- Revise expression simplification to cooperate with congruence
closure (mainly: simplification should not invent new
subexpressions)
- Reimplement congruence closure plus integer offsets to
+ cope with new representation of polynomials using nary expression forms
+ be diligent about maintaining which expressions are in the relation
+ add lots of invariant checking for the correlations between the
componnents of the congruence closure data structures
Reviewed By: jvillard
Differential Revision: D14075512
fbshipit-source-id: 2dbaf3d11
Summary:
Even pretty-printed congruence relations are verbose, and most
operations do not change much of the relation. So on return, print
only the symmetric difference between input and output relations.
Reviewed By: mbouaziz
Differential Revision: D14075513
fbshipit-source-id: b1f0ae6d0
Summary:
This is significant for operations involving the NULL pointer, which
is an integer of pointer type.
Reviewed By: mbouaziz
Differential Revision: D14075516
fbshipit-source-id: b727cb4c8
Summary:
Trace.parse is exposed across a module boundary, so handle its own
exceptions and return an `error`.
Reviewed By: mbouaziz
Differential Revision: D14081602
fbshipit-source-id: 4087c5d5b
Summary:
This allows exposing `Trace.parse`, which can be used to call
`Trace.init` in test code.
Reviewed By: mbouaziz
Differential Revision: D14075522
fbshipit-source-id: 4715c643f
Summary:
This makes it convenient to call
`Trace.init ~margin:70 ~config:all ()`
in test modules.
Reviewed By: mbouaziz
Differential Revision: D14075515
fbshipit-source-id: 3d3940eb1
Summary:
This diff adds a constant to the set of widening thresholds if the
constant is compared to an abstract value in condition expressions.
Each abstract value has its own set of thresholds.
Reviewed By: mbouaziz
Differential Revision: D14147150
fbshipit-source-id: ca0db34d4
Summary: We don't want to use Cost analysis results when `Config.hoisting_report_only_expensive` is false
Reviewed By: ezgicicek
Differential Revision: D14124555
fbshipit-source-id: e809bb80a
Summary:
In this diff, it avoids a precision-losing pruning, which was needed
to keep effects of assume commands.
```
unsigned int c = a + b; // (1)
if (c > 0) { // (2)
char result[c];
result[c - 1] = 0; // (4)
}
```
For example, in the example, `c` is assigned by `[a+b,a+b]` at (1),
then it tried to prune the lower bound of `c` to 1 at (2) while losing
precision, in order to say `c - 1` at (4) is safe in terms of integer
underflow. Instead, it could not say that `c - 1` is smaller than `c`
in the buffer access, because the former is analyzed to `[0,a+b-1]` and
the latter `[1,a+b]` at (4).
Now, the situation has changed. By adopting conditional proof
obligation (D13749914), the FP of integer overflow can be suppressed
without the precision-losing pruning.
Reviewed By: mbouaziz
Differential Revision: D14122770
fbshipit-source-id: 634744e99
Summary: Since Inferbo's current min/max domain can keep only a single symbol, e.g. min(constant, symbol) , it loses precision when trying to prune a value including multiple symbols.
Reviewed By: ezgicicek
Differential Revision: D14099399
fbshipit-source-id: 71d677b75
Summary: Record where each symbol in a polynomial is coming from: either a loop, function call or a modeled call.
Reviewed By: mbouaziz
Differential Revision: D14047420
fbshipit-source-id: 56d0bd926
Summary: It keeps alias of simple plus/minus arithmetic in order to pruning the value of "++i" expression.
Reviewed By: mbouaziz
Differential Revision: D14080230
fbshipit-source-id: d3af32a32
Summary: Provide hooks into the autoconf configure script to define where libgmp and libmpfr may be found. Use these and opam to copy the more exotic library objects into the installation of infer on a new `make install-with-libs` target so that the binaries can be distributed usefully, i.e., without users having to install gmp, mpfr, and more importantly apron and elina (which need ocaml + opam + ..., which would defeat the point of having binaries).
Reviewed By: skcho
Differential Revision: D14065317
fbshipit-source-id: 9a2ac7200
Summary:
- Decouple analysis/reporting a little bit
- Avoids carrying the summary while computing stuff
Depends on D14028249
Reviewed By: ngorogiannis
Differential Revision: D14028673
fbshipit-source-id: 18e7298f8
Summary: In SIL, Java's array member is a pointer to an array, while C++'s is the array itself. This diff differentiate them in evaluating abstract locations.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D14021451
fbshipit-source-id: 00f14fe3b
Summary:
`AnalyzerNodesBasicCost` is just mapping instructions to abstract costs, it doesn't need to use AI.
Also it was keeping a map (node -> cost) for each node, this is completely removed.
Depends on D14028171
Reviewed By: ddino
Differential Revision: D14028249
fbshipit-source-id: 63f39261a
Summary:
- There is no need to use AI to compute a dot product: let's just fold over all nodes, but still do it in order (using the WTO) to report at the right place
- The previous version was computing a dot product on nodes for each node, which was quadratic, the new version is linear
- Report only once, the first time the threshold is reached (if in a loop, report at the loop head)
Reviewed By: ddino
Differential Revision: D14028171
fbshipit-source-id: b4a840c6e
Summary:
The former Makefile does not work when $(LN) is cp, because
it tries to copy a binary that has not been installed yet
Pull Request resolved: https://github.com/facebook/infer/pull/1060
Differential Revision: D14044696
Pulled By: jvillard
fbshipit-source-id: f89d9db81
Summary:
Add an option to specify some classes that we really want to warn about
with the liveness checker, even when they appear used because of the
implicit destructor call inserted by the compiler.
Reviewed By: mbouaziz
Differential Revision: D13991129
fbshipit-source-id: 7fafdba84
Summary:
Get rid of false positive as in the test by modelling `Double`. Longer term we
should probably prevent biabduction from blocking the angelic analysis on
`Nullable` fields but that seems harder.
Reviewed By: jeremydubreil
Differential Revision: D14005228
fbshipit-source-id: 59ef2ed66
Josh Berdine
Mehdi Bouaziz
Sungkeun Cho
Jeremy Dubreil
Ezgi Çiçek
Jules Villard
Nikos Gorogiannis
Boris Valkov
Boris Yakobowski
Dino Distefano
Martin Trojer