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 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 , specifying for each variable a subset of useful bits.

Abstract strongest postcondition for statement:

x = y + z

Updates possible bitwidth of given bitwidths of and

One simple rule:

Is this the most precise rule possible? No, consider adding only even numbers.

• Bitwidth Analysis with Application to Silicon Compilation