diff options
| -rw-r--r-- | tex/lit-review/main.tex | 40 | ||||
| -rw-r--r-- | tex/lit-review/references.bib | 1 |
2 files changed, 36 insertions, 5 deletions
diff --git a/tex/lit-review/main.tex b/tex/lit-review/main.tex index 58dc8bb..8f5c5ce 100644 --- a/tex/lit-review/main.tex +++ b/tex/lit-review/main.tex @@ -46,7 +46,7 @@ $(+)$, negative $(-)$, zero $(0)$, unknown $(\pm)$ or undefined $(?)$. Using thi abstraction we can still define some semantics which reflect the program itself (as an example: $(+) \times (-) = (-)$, or the product of a positive number with a negative number is a negative number). Each abstract domain must also contain -a "top" $(\top)$ and a "bottom" $(\bottom)$ element. The existence of these two +a "top" $(\top)$ and a "bottom" $(\bot)$ element. The existence of these two elements turn our abstract domain into a complete lattice, which ensures some helpful properties of our abstract domain. @@ -81,12 +81,44 @@ sum of variables ($\pm a \pm b \leq c$). All of these above domains are actually shown to be instances of the polyhedra abstract domain in \cite{DBLP:conf/vmcai/SankaranarayananSM05}. The polyhedra domain expresses bounds on $a_1 x_1 + a_2 x_2 ... + a_n x_n + c \ge 0$, where -$a_i$ are fixed in advance (a predefined polyhedral shape). +$a_i$ are fixed in advance (a predefined polyhedral shape). This allows for +ranges to be expressed as $1 \times x_1 + c \ge 0$ provides a single bound for a +single variable (two such bounds is, of course, a range). Similarly for zones +one can define a polyhedra $1 \times x_1 + (-1) \times x_2 + c \ge 0$ which is +equivalent. The octagon domain is $(\pm 1) \times x_1 + (\pm 1) \times x_2 + c +\ge 0$. \section{Fixpoints} -Other test citation: \cite{DBLP:tr/trier/MI96-11} -\section{Strategy Improvement} +When performing static analysis there is a great need to perform some sort of +fixpoint solving to determine the possible resultant values for some operations. +When looping, for instance, it is necessary to "iterate" (in some sense) to find +what values each variable may take during a loop iteration. + +The most basic method for doing so is simply to perform a complete iteration in +the abstract domain, but doing so has no guarantee of termination and would not +be expected to be performant. In \cite{CousotCousot77-1} an approach of +"widening" and "narrowing" is introduced. + +This widening/narrowing method performs some fixed number of iteration steps. +If, after this fixed number, the iteration has not stabilised then it assumes +that it will not stabilise and will instead continue infinitely, so any affected +variables are "widened" to infinity. A "narrowing" step is then carried out +wherein variables are brought back into the finite domain by some terminating +condition on the loop. + +This approach is quite general, and so is applicable to many instances of real +programs, but is a crude approximation of the reality of the program. In +specific instances it is possible to perform a better approximation. In +particular the case of monotonic, expansive operators is considered in \cite{}. % something from thomas here +With this approach code points are converted into fixpoint equations with +$minimum$ and $maximum$ expressions. These fixpoint equations can then be solved +in order to give information about the program's abstract semantics. These +equations are solved using the technique of strategy iteration \cite{} % something about strategy iteration here +combined with a fast fixpoint-iteration algorithm (such as the one presented in +\cite{DBLP:tr/trier/MI96-11}). + +%Other test citation: \cite{DBLP:tr/trier/MI96-11} \section{Conclusion} diff --git a/tex/lit-review/references.bib b/tex/lit-review/references.bib index d3a257b..d6db721 100644 --- a/tex/lit-review/references.bib +++ b/tex/lit-review/references.bib @@ -53,7 +53,6 @@ year = {2005}, pages = {25-41}, ee = {http://dx.doi.org/10.1007/978-3-540-30579-8_2}, - crossref = {DBLP:conf/vmcai/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{Dor:2001:CCS:647170.718291, |