diff options
Diffstat (limited to 'tex/thesis/litreview')
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 127 |
1 files changed, 76 insertions, 51 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex index d2c5d6f..4b9f3da 100644 --- a/tex/thesis/litreview/litreview.tex +++ b/tex/thesis/litreview/litreview.tex @@ -1,15 +1,44 @@ +\newcommand{\Env}{\mathsf{Env}} +\newcommand{\PP}{\mathsf{PP}} +\newcommand{\States}{\mathsf{States}} + \chapter{Literature Review} \label{chap:litreview} \section{Program Semantics} +In order to perform any static analysis of a program it is necessary +to have some notion of the \emph{semantics}, or meaning, of a +program. + +A program's semantics can be realised by considering the possible +values for each variable at each point in the program, which we will +refer to as the possible \emph{states} of the program, and the +transitions between these states performed by \emph{statements}. + +If we consider a finite set of control points, $N$, and a finite set +of variables $X$ then we can capture the state of a program at a +particular point + +As a formalisation of these notions we can consider these to be +defined as follows: +\begin{align*} + \Env: {} & X \to \Z \\ + \PP: {} & \{ \text{program points} \} \\ + \States: {} & \PP \times \Env +\end{align*} + + + + + Let $X$ be the set of program variables, $D$ be the union of all possible domains from which variables can come, and $PP$ be the set of all edges in the Control Flow Graph of the program. \begin{eqnarray} -Env: & X \to D \\ -Expr: & Env \to D \\ -States: & PP \times Env +Env: {} & X \to D \\ +Expr: {} & Env \to D \\ +States: {} & PP \times Env \end{eqnarray} $States$, then, contains every possible state for the program ($Env$) @@ -114,13 +143,12 @@ formalise one of a CFG. For our purposes we will consider a CFG to be a tuple $G = (N, E, S, st)$. A finite set of \emph{control-points} $N$, a finite set $E \subseteq N \times N$ of \emph{edges} between these control points (ie. if $(u,v) \in E$ then an edge exists in the -CFG from $u$ to $v$). A mapping $S: N \times N \to Stmt$ +CFG from $u$ to $v$). A mapping $s: N \times N \to Stmt$ taking each edge in the CFG to a \emph{statement}. $st \in N$ denotes the special \emph{start control-point}. -We can now begin our construction of our collecting semantics -$V^\#[v], \forall v \in N$. - +We can now begin our construction of our abstract semantics $V^\#[v], +\forall v \in N$. \begin{align} V^\# [st] &\ge \alpha(\Z^n) \label{eqn:start-node} \\ V^\# [v] &\ge \llb s_{(u,v)} \rrb ^\# (V^\# [u]) & \forall (u,v) \in @@ -159,7 +187,7 @@ the edges coming in to $v$. In this case there are two incoming edges to $v$: $(u,v)$ and $(w,v)$. The edge $(u,v)$ leads to the state $\llb s_{(u,v)} \rrb^\# -(V^\#[u])$y. It is clear that $V^\#[v]$ must be either the same size +(V^\#[u])$. It is clear that $V^\#[v]$ must be either the same size or `larger' than this value, as it must either equal this constraint or it must be a looser constraint. This gives us the inequality \eqref{eqn:confluence}: $V^\#[v] \ge \llb s_{(u,v)}^\# \rrb @@ -179,8 +207,9 @@ We have not yet considered the effect that $s_{(u,v)}, \forall (u,v) \in E$ has on the state in each edge. The effect of the statement in the abstract domain depends on the statement's effect in the concrete domain, but for all statements we define $\llb s \rrb^\# := \alpha -\circ \llb s \rrb \circ \gamma$. In essence this is just `lifting' the -statement's effects in the abstract domain with our abstraction and +\circ \llb s \rrb \circ \gamma$. In essence this is just changing the +environment in which the statement is acting, so the statement's +effects are moved into our abstract domain with our abstraction and concretization functions. \begin{example} @@ -219,13 +248,10 @@ concretization functions. \label{fig:partial-ordered-construction} \end{figure} - This corresponds to the CFG presented in Figure - \ref{fig:partial-ordered-construction}. - We will now attempt to derive a system of inequalities from this for the \emph{least upper bound} of $x$: \begin{align*} - ub: & ~\text{\bf Vars} \to \CZ \\ + ub: {} & ~\text{\bf Vars} \to \CZ \\ ub(x) &= \min\{v \in \CZ ~|~ x \le v\} \end{align*} @@ -269,8 +295,8 @@ concretization functions. \end{align*} So, the upper bounds for $x$ can be found at every program point in - our original program by finding the smallest values of $x_A, x_B, - x_C$ subject to these constraints: + our original program by finding the smallest values of $ub(x_A), + ub(x_B), ub(x_C)$ subject to these constraints: \begin{align*} ub(x_A) &\ge \infty \\ ub(x_B) &\ge 1 \\ @@ -300,7 +326,7 @@ operator ($\land$), which are defined by the following relationships: In the case that we are considering, with $x, y \in \CZ$, the meet and join operators correspond with $\max$ and $\min$, respectively. This allows us to simplify the system of inequalities in Example -\ref{example:partial-ordered-construction} to the following following: +\ref{example:partial-ordered-construction} to the following: \begin{align*} ub(x_A) &= \infty \\ ub(x_B) &= \max(1, \min(ub(x_B), 99) + 1) \\ @@ -308,8 +334,8 @@ allows us to simplify the system of inequalities in Example \end{align*} The two constraints on the upper bound of $x_B$ can be combined into -one constraint by taking the maximum of them. This is because $x > -\max(a, b) ~\implies~ x > a \text{ and } x > b$ +one constraint by taking the maximum of them. This is because $x \ge +\max(a, b) ~\implies~ x \ge a \text{ and } x \ge b$ @@ -340,7 +366,7 @@ one constraint by taking the maximum of them. This is because $x > \path[every node/.style={fill=none}] (A) edge node[right]{$x = 0$} (B) - (B) edge [loop right] node[right]{$x <= 9: x = x + 1$} (B) + (B) edge [loop right] node[right]{$x \le 9: x = x + 1$} (B) (B) edge node[right]{$x > 9$} (C); \end{tikzpicture} @@ -355,8 +381,8 @@ one constraint by taking the maximum of them. This is because $x > In order to capture the state of the variables at each program point we will consider the abstract state as the two-dimensional vector $(ub(x), -lb(x))$, that is the upper bound of $x$, $ub(x)$, and the - \emph{negated} lower bound of $x$, $-lb(x)$. The greatest fixpoint - of our system of equations over $\CZ^2$ will then give us our bounds + \emph{negated} lower bound of $x$, $-lb(x)$. The least fixpoint of + our system of equations over $\CZ^2$ will then give us our bounds for $ub(x)$ and $lb(x)$. To begin with, let us once again consider the node $A$. At the point @@ -366,7 +392,7 @@ one constraint by taking the maximum of them. This is because $x > inequality: \begin{align*} \left(\begin{array}{c} - ub(x)_A \\ -lb(x)_A + ub(x_A) \\ -lb(x_A) \end{array}\right) &\ge \left(\begin{array}{c} @@ -383,7 +409,7 @@ one constraint by taking the maximum of them. This is because $x > simply sets $x$ to $1$. This is captured in the following inequality: \begin{align*} \left(\begin{array}{c} - ub(x)_B \\ -lb(x)_B + ub(x_B) \\ -lb(x_B) \end{array}\right) &\ge \left(\begin{array}{c} @@ -400,15 +426,15 @@ one constraint by taking the maximum of them. This is because $x > \end{array}\right) \) captures the effect of the addition on each of the bounds (increasing each of the bounds by one). - The $x <= 9$ conditional, which is present on the edge, is captured - by the restriction on the growth of the upper bound. \(\min(ub(x)_B, + The $x \le 9$ conditional, which is present on the edge, is captured + by the restriction on the growth of the upper bound. \(\min(ub(x_B), 9)\) ensures the upper-bound's growth is limited by the value $9$. It should be noted that there is no bound placed on the lower-bound as the program only bounds $x$'s growth from above on this edge. \begin{align*} \left(\begin{array}{c} - ub(x)_B \\ -lb(x)_B + ub(x_B) \\ -lb(x_B) \end{array}\right) &\ge \left[\begin{array}{cc} @@ -416,8 +442,8 @@ one constraint by taking the maximum of them. This is because $x > 0 & 1 \end{array}\right] \left(\begin{array}{c} - \min(ub(x)_B, 99) \\ - -lb(x)_B + \min(ub(x_B), 99) \\ + -lb(x_B) \end{array}\right) + \left(\begin{array}{c} @@ -433,20 +459,20 @@ one constraint by taking the maximum of them. This is because $x > following inequality: \begin{align*} \left(\begin{array}{c} - ub(x)_C \\ - -lb(x)_C + ub(x_C) \\ + -lb(x_C) \end{array}\right) &\ge \left(\begin{array}{c} - ub(x)_B \\ - \min(-lb(x)_B, 99) + ub(x_B) \\ + \min(-lb(x_B), 99) \end{array}\right) \end{align*} This gives us the following inequalities for this program: \begin{align*} \left(\begin{array}{c} - ub(x)_A \\ -lb(x)_A + ub(x_A) \\ -lb(x_A) \end{array}\right) &\ge \left(\begin{array}{c} @@ -454,7 +480,7 @@ one constraint by taking the maximum of them. This is because $x > \end{array}\right) \\ \left(\begin{array}{c} - ub(x)_B \\ -lb(x)_B + ub(x_B) \\ -lb(x_B) \end{array}\right) &\ge \left(\begin{array}{c} @@ -462,7 +488,7 @@ one constraint by taking the maximum of them. This is because $x > \end{array}\right) \\ \left(\begin{array}{c} - ub(x)_B \\ -lb(x)_B + ub(x_B) \\ -lb(x_B) \end{array}\right) &\ge \left[\begin{array}{cc} @@ -470,8 +496,8 @@ one constraint by taking the maximum of them. This is because $x > 0 & 1 \end{array}\right] \left(\begin{array}{c} - \min(ub(x)_B, 99) \\ - -lb(x)_B + \min(ub(x_B), 99) \\ + -lb(x_B) \end{array}\right) + \left(\begin{array}{c} @@ -480,13 +506,13 @@ one constraint by taking the maximum of them. This is because $x > \end{array}\right) \\ \left(\begin{array}{c} - ub(x)_C \\ - -lb(x)_C + ub(x_C) \\ + -lb(x_C) \end{array}\right) &\ge \left(\begin{array}{c} - ub(x)_B \\ - \min(-lb(x)_B, 99) + ub(x_B) \\ + \min(-lb(x_B), 99) \end{array}\right) \end{align*} @@ -495,7 +521,7 @@ one constraint by taking the maximum of them. This is because $x > of equations: \begin{align*} \left(\begin{array}{c} - ub(x)_A \\ -lb(x)_A + ub(x_A) \\ -lb(x_A) \end{array}\right) &= \left(\begin{array}{c} @@ -503,7 +529,7 @@ one constraint by taking the maximum of them. This is because $x > \end{array}\right) \\ \left(\begin{array}{c} - ub(x)_B \\ -lb(x)_B + ub(x_B) \\ -lb(x_B) \end{array}\right) &= \max\left( @@ -515,8 +541,8 @@ one constraint by taking the maximum of them. This is because $x > 0 & 1 \end{array}\right] \left(\begin{array}{c} - \min(ub(x)_B, 99) \\ - -lb(x)_B + \min(ub(x_B), 99) \\ + -lb(x_B) \end{array}\right) + \left(\begin{array}{c} @@ -526,16 +552,15 @@ one constraint by taking the maximum of them. This is because $x > \right) \\ \left(\begin{array}{c} - ub(x)_C \\ - -lb(x)_C + ub(x_C) \\ + -lb(x_C) \end{array}\right) &= \left(\begin{array}{c} - ub(x)_B \\ - \min(-lb(x)_B, 99) + ub(x_B) \\ + \min(-lb(x_B), 99) \end{array}\right) \end{align*} - \end{example} |