Summary: This diff introduces an inequality for the size alias targets, in order to get preciser array lengths after loops. The alias domain in inferbo was able to express strict equality between alias source and its targets, e.g. x=size(array). Now, for the size alias target, it can express less than or equal relations, e.g. x>=size(array).
Reviewed By: ezgicicek
Differential Revision: D17606222
fbshipit-source-id: 2557d3bd0
Summary:
This diff extends the `Simple` alias domain to address Java's
temporary variables better. It now has an additional field to denote
an alias temporary variable.
Reviewed By: jvillard
Differential Revision: D17421907
fbshipit-source-id: 8b8b47461
Summary:
This diff addresses collection adds in loop. For example,
```
ArrayList<...> a = new ArrayList<>();
for (int i = 0; i < size; i++) {
a.add(...);
}
// we want to know the size of `a` here!
```
This is a common pattern on initializing a collection in Java.
How we did: Instead of adopting general (but complicated) solutions such as relational domain, we
extended the current alias domain of inferbo, to be able to handle this specific case:
* An array `a` should have size 0, at the entry of the loop.
* The iterating variable `i` should start with 0.
* `add` should be called once inside the loop.
Reviewed By: jvillard
Differential Revision: D17319350
fbshipit-source-id: 99b6acae1
Summary: This diff adds models of Java String. In order to keep the precision of cost checker, I fixed cost models for String in this diff too.
Reviewed By: ngorogiannis
Differential Revision: D17203309
fbshipit-source-id: 8cc2814fc
Summary:
It prunes the size of collections when the size function is called in the condition expression. The diff extended the alias domain to understand temporary variables of SIL from Java.
Depends on D16761461
Reviewed By: ezgicicek
Differential Revision: D16761611
fbshipit-source-id: 849c5c71c
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: This diff substitutes symbolic values for unknown functions in proof obligations to top. The goal of the diff is to avoid generating too many number of proof obligations that cannot be concretized.
Reviewed By: ezgicicek
Differential Revision: D14537542
fbshipit-source-id: 7f8f3bb4b
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: 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
Sungkeun Cho
Ezgi Çiçek
Josh Berdine
Mehdi Bouaziz