This is an old revision of the document!
Bitwidth Analysis
Given a language with signed 64 bit integers, determine as small as possible set of bits needed to store values of variables.
- if the bit is small we can use e.g. 'byte' to store it
- it becomes even more important if we generate hardware from C code (saving wires)
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: