Program analysis and machine arithmetic

G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey

Across programming languages, the most widely used integers are of fixed 
width.  And in low-level languages such as LLVM IR, the only integer types
available are fixed-width.  Arithmetic operations on these types do not 
have the usual integer semantics; they obey laws of modular arithmetic.
Program analyses and transformations that pretend their results are
integers go wrong. Yet much of the published research on program analysis
assumes integers in the classical sense.

Over the last three years we have investigated the problem of adjusting
classical analyses to take the fixed-width nature of integers into 
account while maintaining analysis speed and precision. This is often
a challenge. For example, program analyses that reason about array bounds
often utilise fast algorithms that solve systems of so-called difference
constraints. However, the problem of solving these constraints in
modular arithmetic turns out to be NP-complete.

In this talk we discuss the challenges of doing machine-arithmetic-aware
program analysis.  As a concrete example, we outline, as far as time 
permits, an interval analysis suitable for LLVM IR and similar languages.