Computes the time complexity of functions and methods. Can be used to detect changes in runtime complexity with
- C/C++/ObjC: Yes
- Java: Yes
- C#/.Net: Yes
Cost analysis statically estimates an upper bound on the worst-case execution cost of a program (WCET). This page gives an overview of how the analysis works for Java code. The analyser also has limited support for C/C++ and Objective-C.
To run the analysis, you can use run
infer --cost (which will run cost analysis along with other
analyses that are run by default) or
infer --cost-only (which will only run cost analysis).
For example, the command
infer --cost-only -- javac File.java will run
cost analysis on File.java.
Most ideas behind this analysis is based on Stefan Bydge's PhD thesis Static WCET Analysis based on Abstract Interpretation and Counting of Elements.
The analysis computes two things for each node in the CFG:
- the cost of its instructions, i.e. how much one execution of this node costs,
- how many times it can be executed.
The total cost of the node is the scalar product of these two vectors. Then, these are passed to a constraint solver that computes the execution cost of the procedure based on the incoming/outgoing edges.
At a high level, the analysis has three steps:
- Choose control variables that allude to "how many times a loop may iterate".
- Get abstract ranges of the control variables from InferBO (a numerical analysis that infers symbolic intervals)
- Construct complexity polynomials for loops and functions by via a constraint solving algorithm.
Infer’s cost analysis statically estimates the execution cost of a program without running the code. For instance, assume that we had the following program:
For this program, Infer statically infers a polynomial (e.g.
8|list|+16) for the execution cost of this program by giving each instruction in Infer's intermediate language a symbolic cost (where
|.| refers to the length of a list). Here---overlooking the actual constants---the analysis infers that this program’s asymptotic complexity is
O(|list|), that is loop is linear in the size of its input list. Then, at diff time, if a developer modifies this code to,
foo has a linear cost in its parameter, then Infer automatically detects that the complexity of loop has increased from
O(|list|^2) and then reports an
Unlike other Infer analyses (which report found issues/bugs when running infer once), cost analysis only reports an issue for differential analysis (i.e. when comparing the analysis results on the original and the modified files). Instead, infer writes the execution cost of the program into
infer-out/costs-report.json file. For each procedure,
costs-report.json includes the actual polynomial (for the exection cost) along with the degree of the polynomial, the procedure name, line number etc.
Differential cost analysis in action:
- first run infer's cost analysis on
previous-costs-report.json(Note that the file should be copied outside the result directory because the directory will be removed in the second infer run.)
File.javaas shown above
- re-run infer on
infer reportdiff --costs-current current-costs-report.json --costs-previous previous-costs-report.json.
infer-out/differential/introduced.jsonto see the newly found complexity increase issue(s).
There are a number of known limitations to the design of the static cost analysis:
InferBo's intervals are limited to affine expressions, not full-blown polynomials. Hence, we can automatically infer bounds involving square roots.
We do not handle recursion.
If the execution cost of a program depends on an unknown call (e.g. an unmodeled library calls), we can't compute a static upper bound and return T (unknown cost).
The following issue types are reported by this checker: