Francesco Logozzo and Matthieu Martel
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 guarantees 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.
In Semantics, Abstract Interpretation, and Reasoning about Programs
Publisher Electronic Proceedings in Theoretical Computer Science
Francesco Logozzo and Tom Ball. Modular and Verified Automatic Program Repair, ACM SIGPLAN, 23 October 2012.
Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.