Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss
G Gange, JA Navas, P Schachte, H Sondergaard, PJ Stuckey
ACM Transactions on Programming Languages and Systems | Association for Computing Machinery | Published : 2015
The most commonly used integer types have fixed bit-width, making it possible for computations to wrap around, and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.
Related Projects (1)
Awarded by Australian Research Council, under ARC
This work is supported by the Australian Research Council, under ARC grant DP110102579.