Improved precision in polyhedral analysis with wrapping

- We improve on a method to make the polyhedral domain sound for bounded integers.
- Our method keeps all polyhedra finite, reducing the risk of imprecision.
- Experiments show that significant improvements can be achieved.

Abstract interpretation using convex polyhedra is a common and powerful program analysis technique to discover linear relationships among variables in a program. A value analysis based on a polyhedral abstract domain can be very precise, thus reducing the number of false alarms when used to verify the absence of bugs in the code. However, the classical way of performing polyhedral analysis does not model the fact that values typically are stored as fixed-size binary strings and usually have wrap-around semantics in the case of overflows. In resource-constrained embedded systems, where 8 or 16 bit processors are used, wrapping behaviour may even be used intentionally to save instructions and execution time. Thus, to analyse such systems accurately and correctly, the wrapping has to be modelled.Simon and King [1] devised a technique to handle wrapping in polyhedral analysis in a sound way. However, their approach can sometimes yield large overapproximations. We show how the analysis can be made significantly more precise by simple means, thus making the approach more practically useful for program verification. An experimental evaluation shows that there indeed can be significant improvements in precision.