LARA

Bitwidth Analysis

Given a language with signed 64 bit integers, determine as small as possible set of bits needed to store values of variables.

  • e.g. if analysis derives that a subset of $\{0,1,2,\ldots,7\}$ is sufficient, then we can use byte type to store the value
    • instead of having multiple integer types, we can have analysis infer the right 'subtypes' (ranges)
  • the analysis becomes even more important if we generate hardware from C code: analysis would enable us to save circuits and power

Let B = {-32,-31,…,-1,0,1,…,31} be a set of bits.

Simple abstract domain (at each program point), map $g : V \to 2^B$, specifying for each variable $x$ a subset of useful bits.

Abstract strongest postcondition for statement:

x = y + z

Updates possible bitwidth of $x$ given bitwidths of $y$ and $z$

One simple rule: $g(x)=$

Is this the most precise rule possible?

References