# 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 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: