Differences
This shows you the differences between two versions of the page.
|
sav08:bitwidth_analysis [2008/05/20 18:58] vkuncak |
sav08:bitwidth_analysis [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== 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 | ||
| - | * 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)=$ | ||
| - | ++++| | ||
| - | \[\begin{array}{l} | ||
| - | let\ L = \min(g(y)) + \min(g(z))-1 \\ | ||
| - | let\ U = \max(g(y)) + \max(g(z))+1 \\ | ||
| - | if\ (L < 32) \lor (U > 31)\ then\ B \\ | ||
| - | else\ [L,U] | ||
| - | \end{array} | ||
| - | \] | ||
| - | ++++ | ||
| - | |||
| - | Is this the most precise rule possible? ++|No, consider adding only even numbers.++ | ||
| - | |||
| - | ===== References ===== | ||
| - | |||
| - | * [[http://citeseer.ist.psu.edu/stephenson00bitwidth.html|Bitwidth Analysis with Application to Silicon Compilation]] | ||