Some bug fixes for the solver.

Still doesn't work in clang, though.

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}