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: 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: 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:
- 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: This diff unset powloc and arrayblk values of p when assume(p==Null).
Reviewed By: mbouaziz, jvillard
Differential Revision: D13415366
fbshipit-source-id: a491a957f
Summary:
For abstract values representing one concrete value, create only one symbol instead of two.
Still create two symbols (lb, ub) for abstract values representing multiple concrete values (like array cells).
As a consequence, comparisons of symbolic values are more precise (we can even prove equality). I expect to remove a bunch of FPs.
Another consequence is the disappearance of `.lb` and `.ub` in many reports.
Reviewed By: skcho
Differential Revision: D13072084
fbshipit-source-id: 9bc0b9881
Summary:
It materializes symbolic values of function parameters on-demand. The on-demand materialization is triggered when finding a value from an abstract memory and joining/widening abstract memories.
Depends on D13294630
Main idea:
* Symbolic values are on-demand-ly generated by a symbol path and its type
* In order to avoid infinite generation of symbolic values, symbol paths are canonicalized by structure types and field names (which means they are abstracted to the same value). For example, in a linked list, a symbolic value `x->next->next` is canonicalized to `x->next` when the structures (`*x` and `*x->next`) have the same structure type and the same field name (`next`).
Changes from the previous code:
* `Symbol.t` does not include `id` and `pname` for distinguishing symbols. Now, all symbols are compared by `path:SymbolPath.partial` and `bound_end`.
* `SymbolTable` is no longer used, which was used for generating symbolic values with new `id`s.
Reviewed By: mbouaziz
Differential Revision: D13294635
fbshipit-source-id: fa422f084
Summary:
At function calls, it copies callee's values that are reachable from parameters.
Depends on D13231291
Reviewed By: mbouaziz
Differential Revision: D13231711
fbshipit-source-id: 1e8aed1c4
Summary:
For more deduplications of issues, this diff loosens the condition of
similar bounds. The previous condition of similar bounds was too
strict, so [0,0] and [0,+oo] were not similar.
Depends on D10851762
Reviewed By: mbouaziz
Differential Revision: D10866127
fbshipit-source-id: 4ba912a88
Summary:
This diff preserves values of offset and index separately, rather than
one value of their addition, because premature addition results in
imprecise FPs by the limited expressiveness of the domain.
Reviewed By: mbouaziz
Differential Revision: D10851393
fbshipit-source-id: 1685ead36
Summary:
It avoids checking integer overflow when it definitely cannot happen.
For example, it does not check integer overflow of addition when one
of parameters is a negative number, or underflow of subtraction when
its first parameter is a positive number.
Reviewed By: mbouaziz
Differential Revision: D10446161
fbshipit-source-id: b8c86e1b2
Summary: This diff changes pp of binary operation condition in order to avoid a `make test` failure. For the same `uint64_t` type, it is translated to `unsigned long long` in 64bit mac, but `unsigned long` in 64bit linux, which made a `make test` failure.
Reviewed By: mbouaziz
Differential Revision: D10459466
fbshipit-source-id: 449ab548e
Ezgi Çiçek
Dino Distefano
Mehdi Bouaziz
Sungkeun Cho