- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:bitwidth_analysis [2008/05/20 18:58] vkuncak |
sav08:bitwidth_analysis [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 3: | Line 3: | ||

Given a language with signed 64 bit integers, determine as small as possible set of bits needed to store values of variables. | 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 | * 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 | * the analysis becomes even more important if we generate hardware from C code: analysis would enable us to save circuits and power | ||

Line 16: | Line 17: | ||

One simple rule: $g(x)=$ | One simple rule: $g(x)=$ | ||

++++| | ++++| | ||

- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |

let\ L = \min(g(y)) + \min(g(z))-1 \\ | let\ L = \min(g(y)) + \min(g(z))-1 \\ | ||

let\ U = \max(g(y)) + \max(g(z))+1 \\ | let\ U = \max(g(y)) + \max(g(z))+1 \\ | ||

Line 22: | Line 23: | ||

else\ [L,U] | else\ [L,U] | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

++++ | ++++ | ||