Summary: We do not use an arbitrary threshold to test cost results anymore but instead rely on `cost-issues` which do not have any trace attached. This diff adds traces to `costs-report.json` so that we can test cost issues with traces.
Reviewed By: skcho
Differential Revision: D21858846
fbshipit-source-id: e73321a92
Summary:
Now that we have a way to write cost issues, let's not rely on some arbitrary threshold (and also get rid of `EXPENSIVE_EXECUTION_TIME` issues in tests).
One consequence of this is that we will loose the cost traces in tests since `costs-report.json` doesn't have any traces. Next diff fixes that.
Reviewed By: skcho
Differential Revision: D21837574
fbshipit-source-id: 86b4d028d
Summary:
The model returns an array the length of which is the same to that of enum entries.
It takes the length of enum entries from the summary of `Enum.values` because it is not written in `tenv`. In order to do that, the model semantics should be able to request the summary of the function with `get_summary`, so I extended `model_env` to include the functionality.
Reviewed By: ezgicicek
Differential Revision: D21843319
fbshipit-source-id: d6f10eb91
Summary:
The model returns an array the length of which is the number of known
fields in `tenv`.
Reviewed By: ezgicicek
Differential Revision: D21840375
fbshipit-source-id: 891517c6e
Summary:
In order to test cost analysis results, currently we rely on having an arbitrary cost threshold (200) and report issues that exceed this cost. For instance, a cost of 201 is considered expensive and reported as `EXPENSIVE_EXECUTION_TIME` issue in cost tests.
This means, if we change the cost analysis in a slight way that results in some constant cost increase under 200, we wouldn't able to detect it. I find this unsatisfactory and somewhat hacky.
This diff adds the ability to write the result of `costs-report.json` into a separate `cost-issues.exp` and then compare the actual costs (not only than relying on this arbitrary threshold reporting mechanism).
Reviewed By: skcho
Differential Revision: D21816312
fbshipit-source-id: 93b531928
Summary: Similarly to Enum.name, we model Class.getCanonicalName as returning an arbitrary non-empty string.
Reviewed By: ngorogiannis
Differential Revision: D21207120
fbshipit-source-id: 1e2dbd1fd
Summary:
We model Enum.name as returing a constant name, rather than getting real field names. We did this
because we couldn't think of any big gains, in terms of analysis precision/performance, from getting
the real names.
Reviewed By: ezgicicek
Differential Revision: D21201730
fbshipit-source-id: a2dc01a44
Summary: This diff revises the models of Collection.set and get to handle its elements.
Reviewed By: ezgicicek
Differential Revision: D21201242
fbshipit-source-id: 9c248453d
Summary: This diff suppresses cost issues on lambda and auto-generated procedures, since they were too noisy.
Reviewed By: ezgicicek
Differential Revision: D21153619
fbshipit-source-id: 65ad6dcc3
Summary:
This diff distinguishes array declaration and size-setting in trace. For example, when there is an
assume statement on an array size, the array size can be pruned to another value. In which case, we
want to see "Set array size" in the trace, instead of "Array declaration".
Reviewed By: jvillard
Differential Revision: D20914930
fbshipit-source-id: 0253fb69e
Summary:
Currenlty the cost issue is printed at the first node of a function, which is usually the first
statment of the function. This may give a wrong impression that the cost of the statement is
changed.
This diff re-locate where to print issues with heuristics. Going backward from the first node
lines, it looks up a line satisfying,
1. A line should start with <fname> or should include " <fname>".
2. The <fname> found in 1 should be followed by a space, '<', '(', or end of line.
Reviewed By: jvillard
Differential Revision: D20766876
fbshipit-source-id: b4fee3180
Summary:
To find a method in non-abstract sub-classes, this diff applies the
same heuristics of inferbo.
* If the class is an interface: Find its unique sub-class and apply the heuristics recursively.
* If the class is an abstract class: Find/use its own summary if possible. If not found, find
one (arbitrary but deterministic) summary from its sub-classes.
* Otherwise: Find its own summary.
Reviewed By: ezgicicek
Differential Revision: D20647101
fbshipit-source-id: 2f8f3ff81
Summary:
`make test` failed in some test directories, because we were getting warnings
```
Foo.java uses unchecked or unsafe operations.
```
This diff fixes or suppresses these warnings.
Reviewed By: skcho
Differential Revision: D20557572
fbshipit-source-id: 63ecd3dfa
Summary: The `FN_loop2` was not actually FN because infer analyzes its complexity as degree 1 correctly.
Reviewed By: dulmarod
Differential Revision: D20468367
fbshipit-source-id: 9e4c19415
Summary: The `iterate_over_mycollection_quad_FN` was not actually FN because infer analyzes its complexity as degree 2 correctly. So, this diff removed `_FN` from there.
Reviewed By: ezgicicek
Differential Revision: D20467398
fbshipit-source-id: b10340612
Summary:
`JavaSplitName` is used to represent Java types (in `Procname` in particular). The type itself is a pair of string (an optional package qualifier) and a "type name" (the quotes are there because it may contain array qualifiers).
For example `java.lang.Object[][]` should be represented as
```
{package=Some "java.lang"; typename="Object[][]"}
```
The constructor `make` was misused to construct instead types such as
```
{package=None; typename="java.lang.Object[][]"}`
```
This is evident when we print the return type of a `Procname` non-verbosely (the default), but we still see the package qualifier.
Obviously this is not just a pretty-printing bug, the values were themselves wrong.
The fix is to use the `of_string` constructor which will parse the package and separate it correctly. Another bug (in response to this one) had to be fixed in `Procname.is_vararg` to maintain behaviour in Nullsafe and Quandary.
Reviewed By: mityal
Differential Revision: D20394146
fbshipit-source-id: 4633902eb
Summary: Type is not enough to say a function call of `Provider.get` is expensive or not.
Reviewed By: jvillard
Differential Revision: D20366206
fbshipit-source-id: 83d3e8741
Summary:
This diff uses a type parameter of `Provider.get` to decide whether assigning expensive cost to the
function call or not. For example, if the type is small one like `Provider<Integer>`, it be
evaluated to have a unit cost, otherwise a linear cost.
To get the return type of `Provider.get`, I added a simple analyzer that collects "casted" types
backwards. In Sil, while the function call statement loses the return type, e.g,
```
n$5=_fun_Object Provider.get()(n$3:javax.inject.Provider*);
```
the `n$5`'s value is usually casted to a specific type at some point later.
```
*&$irvar0:java.lang.Object*=n$5
n$8=*&$irvar0:java.lang.Object*
n$9=_fun___cast(n$8:java.lang.Object*,sizeof(t=java.lang.Integer;sub_t=( sub )(cast)):void)
```
So, the analyzer starts from the cast statements backward, collecting the types to cast for each
variables.
Reviewed By: ezgicicek
Differential Revision: D20345268
fbshipit-source-id: 704b42ec1
Summary:
This diff renames `ZERO_XXX` issues to more appropriately named and descriptive
`XXX_UNREACHABLE_AT_EXIT` and replaces bottom with
unreachable in cost kinds and issues.
Reviewed By: skcho
Differential Revision: D20140301
fbshipit-source-id: eb6076b30
Summary:
The issue type `ZERO_EXECUTION_TIME` actually corresponds to bottom state but has been mistakenly used to mean
- unreachable nodes (program never reaching exit state)
- having zero cost (e.g. for allocations).
Note that, for execution costs, the latter doesn't make sense since we always incur a unit cost for the start node. Hence, a function with empty body will have unit cost. For allocations or IO however, we only incur costs for specific primitives, so a function with no allocations/IO could have a zero cost. However, there is no point reporting functions with zero cost as a specific issue type. Instead, what we want to track is the former, i.e. functions whose cost becomes 0 due to program never reaching exit state.
This diff aims to split these cases into two by only reporting on the latter and adds traces to bottom/unreachable cost by creating a special category in polynomials.
Next diff will rename `ZERO_XXX` to `XXX_UNREACHABLE_AT_EXIT`.
Reviewed By: skcho
Differential Revision: D20005774
fbshipit-source-id: 46b9abd5a
Summary:
> We don't report when the cost is Top as it corresponds to subsequent 'don't know's. Instead, we
> report Top cost only at the top level per function
The previous code just ignored top costed nodes, so it was able to report a non-top cost that was
from another node. For example,
```
void foo() {
linear-cost();
top-cost();
}
```
It reported inconsistent reports: `EXPENSIVE_EXECUTION_TIME` with a linear cost and
`INFINITE_EXECUTION_TIME` at the same time.
This diff fixes it not to report `EXPENSIVE_EXECUTION_TIME` when there is a node with the top cost.
Reviewed By: ezgicicek
Differential Revision: D20139408
fbshipit-source-id: 9fedd4aec
Summary:
In the previous report, it reported the first cost of node that exceeds a threshold. However, this
may hide a bigger cost of node that appears later. This diff changes this to report the biggest
cost of node among the costs exceeding the threshold.
Reviewed By: ezgicicek
Differential Revision: D20116162
fbshipit-source-id: 06199fb46
Summary: The semantics of the `values` function of Java enum class was missing, when it is called outside the class initializer. This diff gets the size of the enum elements from the summary of class initializer function, `<clinit>`.
Reviewed By: ezgicicek
Differential Revision: D20094880
fbshipit-source-id: 7362bba1c
Summary: We don't use allocation costs in prod at the moment. There is no plan to do so in the near future. Let's not report them anymore and also save some space in `costs-report.json`.
Reviewed By: skcho
Differential Revision: D19766828
fbshipit-source-id: 06dffa61d
Summary: This diff returns non-symbolic value (top) for unknown external function calls because the symbolic values sometimes make it hard to understand costs.
Reviewed By: ezgicicek
Differential Revision: D18685715
fbshipit-source-id: 1b39c718b
Summary:
`String` and `StringBuilder` both implement `CharSequence`. Let's generalize the model for `String` to `CharSequence` wherever possible and add missing models for
- `StringBuilder.append`
- `StringBuilder.toString`
Reviewed By: skcho
Differential Revision: D19558009
fbshipit-source-id: 0dfdb21af
Summary:
Java's String models were broken for
- initializing a String object with a locally defined constant string (which is an `Object*` in SIL).
- initializing a String object with a `char`/`byte` array
This diff fixes them and also adds models for `new String ()`.
Reviewed By: skcho
Differential Revision: D19662180
fbshipit-source-id: 23968d0aa
Summary: `String.split(regexp)` returns an array that is split by the given regexp. If the regexp doesn't match, the original string is returned. Hence, the resulting array's length must be in `[1, max(1, n_u -1)]` where`n_u` is the upper bound of the string's length.
Reviewed By: dulmarod
Differential Revision: D19578318
fbshipit-source-id: 675af7376
Summary: This diff use actuall call path in the cost results instead of `class name + method name`.
Reviewed By: ngorogiannis
Differential Revision: D19194969
fbshipit-source-id: b72018586
Summary:
This diff updates the relation between iterator (offset) and integer value not only at
assignments (`x += 1`), but also at function calls (`foo()`) that increase integer values by one in
their side effects.
Reviewed By: ezgicicek
Differential Revision: D19163214
fbshipit-source-id: 47e52f939
Summary: This diff extends the domain to express the relation between iterator's offset and integer value.
Reviewed By: ezgicicek
Differential Revision: D19143670
fbshipit-source-id: 6223bc934
Summary:
Old versions of sawja/javalib got the line numbers slightly wrong. The workaround was to do a regexp search in the source file for the right line.
My understanding is that this is no longer necessary. This diff removes it.
Reviewed By: jvillard
Differential Revision: D19033415
fbshipit-source-id: 2da19d66d
Summary: This diff extends the bound domain to express multiplication of bounds in some simple cases.
Reviewed By: ezgicicek
Differential Revision: D18745246
fbshipit-source-id: 4f2dcb42c
Summary:
This diff fixes the model of substring.
Problem: The cost model of the substring function was to return `size of string - start index` as a
cost. However, sometimes this was a negative number, because of state abstractions on paths, array
elements, call contexts, etc, which caused an exception inadvertently.
This diff changes the model to return just `size of string`, when it cannot say `size of string` is
bigger than `start index`.
Reviewed By: ezgicicek
Differential Revision: D18707954
fbshipit-source-id: 63f27e461
Summary:
This diff avoids unqualified variables by `ItvUpdatedBy` are qualified later. For example,
```
z = x & y;
z = z + 1;
```
While `z` should not be selected as a control variable, it wasn't, because it was qualified by the addition. This pattern introduces FPs in many cases.
Reviewed By: ngorogiannis
Differential Revision: D18505894
fbshipit-source-id: 13aec3008
Summary:
This diff excludes integer variables from control variables when their values are calculated by
binary operators.
Reviewed By: ezgicicek
Differential Revision: D18505826
fbshipit-source-id: 710533d4c
Summary:
There was a precision loss during the substitution of array block. For example:
Callee's abstract memory includes an array block as follows, where `a` is a parameter.
```
a.elements -> { a.elements[*] with a.elements.size }
```
Callers' abstract memory includes a pointer that may point to multiple array blocks.
```
c -> { x, y }
x.elements -> { x.elements[*] with x.elements.size }
y.elements -> { y.elements[*] with y.elements.size }
```
When the callee is called with the parameter `c`, the callees memory is substituted to:
```
x.elements -> { x.elements[*] with top , y.elements[*] with top }
y.elements -> { x.elements[*] with top , y.elements[*] with top }
```
because `a.elements[*]` was substituted to `{ x.elements[*] , y.elements[*] }`
and `a.elements.size` was substituted to `top ( = x.elements.size join y.elements.size )`.
This diff tries to keep the precision in the specific case, not to join the sizes of array blocks.
So now the same callee's abstract memory is substituted to:
```
x.elements -> { x.elements[*] with x.elements.size }
y.elements -> { y.elements[*] with y.elements.size }
```
Reviewed By: ngorogiannis
Differential Revision: D18480585
fbshipit-source-id: b70e63c22
Summary:
It returns non-top value when one of the parameters of band is positive, i.e., `x & 255` returns
`[0, 255]` instead of top.
Reviewed By: ezgicicek
Differential Revision: D18448614
fbshipit-source-id: aaa298a66
Ezgi Çiçek
Sungkeun Cho
Nikos Gorogiannis