Summary:
Correct the models of ArrayList initialization. Basically, there are two ways to initialize:
- by setting an initial capacity, which creates an empty list
- by passing another collection as an argument
Before, we had only modeled the second case which was resulting in wrong memory model for the first case. This diff fixes that.
Reviewed By: skcho
Differential Revision: D16711055
fbshipit-source-id: e82faf191
Summary: Models of Java's Collection mistakenly assumed that there was an argument for empty set whereas `Collections.emptySet()` doesn't have any actuals. This diff fixes that an also removes the type argument from the corresponding model definition.
Reviewed By: skcho
Differential Revision: D16582314
fbshipit-source-id: d4304dc60
Summary:
The `represents_multiple_values` flag was adopted to decide whether updating abstract value strongly or weakly. However, the flag was included in the `Val` domain, which is strange, because it is a property of abstract locations, rather than abstract values. This makes the behavior of memory update function depend on the abstract value to update, making its code complicated.
This diff detach the `represents_multiple_values` flag from the `Value` domain, thus the memory update does not depend on the abstract value. Since this is a refactoring, I believe the diff should not make many semantic changes.
Reviewed By: ezgicicek
Differential Revision: D16441734
fbshipit-source-id: 4c10779d7
Summary:
- Add allocation costs to `costs-report.json` and enable diffing over allocation costs.
- Also, let's be more consistent and modular in naming our cost issues.
- introduce a generic issue type `X_TIME_COMPLEXITY_INCREASE` where `X` can be one of the cost kinds. If the function is on the cold start, issue can have the `COLD_START` suffix. Similarly for infinite/zero/expensive calls.
- Change `PERFORMANCE_VARIATION` -> `EXECUTION_TIME_COMPLEXITY_INCREASE`
- Add new issue type for `ALLOCATION_COMPLEXITY_INCREASE_COLD_START` which will be enabled by default
- Refactor cost issues to be more modular and succinct. This also makes addition of a new cost kind very easy by adding the kind into the `enabled_cost_kinds` list in `CostKind.ml`
Reviewed By: mbouaziz
Differential Revision: D15822681
fbshipit-source-id: cf89ece59
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
Ezgi Çiçek
Sungkeun Cho
Josh Berdine
Dino Distefano
Mehdi Bouaziz