Automatic Repair of Overflowing Expressions with Abstract Interpretation
This addresses the issue of integer overflow in software for developers, but it is incremental as it builds on existing abstract interpretation techniques.
The paper tackles the problem of automatically synthesizing integer arithmetic expressions that are provably non-overflowing, using abstract interpretation to infer numerical properties and then checking or repairing expressions, with results including a complete polynomial algorithm for linear expressions with intervals.
We consider the problem of synthesizing provably non-overflowing integer arithmetic expressions or Boolean relations among integer arithmetic expressions. First we use a numerical abstract domain to infer numerical properties among program variables. Then we check if those properties guarantee that a given expression does not overflow. If this is not the case, we synthesize an equivalent, yet not-overflowing expression, or we report that such an expression does not exists. The synthesis of a non-overflowing expression depends on three, orthogonal factors: the input expression (e.g., is it linear, polynomial,... ?), the output expression (e.g., are case splits allowed?), and the underlying numerical abstract domain - the more precise the abstract domain is, the more correct expressions can be synthesized. We consider three common cases: (i) linear expressions with integer coefficients and intervals; (ii) Boolean expressions of linear expressions; and (iii) linear expressions with templates. In the first case we prove there exists a complete and polynomial algorithm to solve the problem. In the second case, we have an incomplete yet polynomial algorithm, whereas in the third we have a complete yet worst-case exponential algorithm.