
%We again assume for simplicity to have two variables, $V = \{ x,y \}$.

\newcommand{\anode}{}
\newcommand{\bnode}{}
\newcommand{\cnode}{}
\newcommand{\dnode}{}
\newcommand{\enode}{}
\newcommand{\fnode}{}
\newcommand{\gnode}{}
\newcommand{\red}[1]{{\small \textcolor{blue}{#1}}}

\newcommand{\cfgex}{
\begin{minipage}{3.5cm}
\hspace*{-1.6cm}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2cm,
                    thick]
  \tikzstyle{every state}=[fill=none,draw=black,text=black,minimum size=0pt]

  \node[state,label=right:\anode] (A) {$a$};
  \node[state,label=below right:\bnode] (B) [below right of=A]  {$b$};
  \node[state,label=right:\cnode] (C) [right of=B]  {$c$};
  \node[state,label=right:\dnode] (D) [below of=B]  {$d$};
  \node[state,label=right:\enode] (E) [below left of=D] {$e$};
  \node[state,label=right:\fnode] (F) [below right of=D] {$f$};
  \node[state,label=right:\gnode] (G) [below right of=E] {$g$};

  \path (A) edge node {$i=0$} (B) 
        (B) edge node {$[i \ge 10]$} (C)
        (B) edge node {$[i \le 9]$} (D)
        (D) edge node [swap] {$[i \ge 2]$} (E)
        (D) edge node {$[i \le 1]$} (F)
        (E) edge node [swap] {$i=i+3$} (G)
        (F) edge node {$i=i+2$} (G);

  \draw [->] (G) .. controls +(-5cm,-1cm) and +(-3cm,0cm) .. (B);

%  \node at (0,0) {some text};

\end{tikzpicture}
\end{minipage}
}

\begin{frame}
\frametitle{Basic idea of abstract interpretation}
Abstract interpretation is a way to infer properties of program computations.

Consider the assignment: $z = x + y$.
\vspace{20pt}\\
Interpreter:
\begin{equation*}
\begin{pmatrix}&x: 10&\\ &y: -2 &\\&z: 3 &\end{pmatrix}
\xrightarrow{z = x + y}
\begin{pmatrix}&x: 10 &\\&y: -2 &\\&z: 8&\end{pmatrix}
\end{equation*}
%\vspace{10pt}\\
Abstract interpreter:
\begin{equation*}
\begin{pmatrix}&x \in &[0, 10]\\ &y \in &[-5, 5] \\&z \in &[0, 10] \end{pmatrix}
\xrightarrow{z = x + y}
\begin{pmatrix}&x \in &[0, 10]\\&y \in &[-5, 5]\\&z \in &[-5, 15]\end{pmatrix}
\end{equation*}
Each abstract state represents a set of concrete states.

{\small\it Patrick Cousot, Radhia Cousot:
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977: 238-252}
\end{frame}

%\begin{frame}
%\frametitle{Program Meaning is a Fixpoint. We Approximate It.}
%
%\begin{center}
%\includegraphics[height=6cm]{ai-big-idea.png}
%\end{center}
%\centerline{$\gamma$ maps abstract states to concrete states}
%\end{frame}

\newcommand{\Fs}{F_{\#}}

%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Programs as control-flow graphs}
\hspace{5pt}
\begin{minipage}{3.5cm}
\lstset{commentstyle=\codestyle\color{gray}}
\lstinputlisting{cfg-program.scala}
\end{minipage}
\begin{minipage}{8cm}
One possible corresponding control-flow graph is: \pause
%\includegraphics[width=\textwidth]{cfg-inc.png}
\scalebox{0.8}{\cfgex}
\end{minipage}
\end{frame}

%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Sets of states at each program point}
 Suppose that
\begin{itemize}
\item program state is given by the value of the integer variable $i$
\item initially, it is possible that i has any value
\end{itemize}
Compute the set of states at each vertex in the CFG.

\hspace*{1cm}
\begin{minipage}{4cm}
\lstset{commentstyle=\codestyle\color{gray}}
\lstinputlisting{cfg-program.scala}
\end{minipage}
\scalebox{0.8}{\cfgex}
\end{frame}

\renewcommand{\anode}{\red{$\mathbb{Z}$}}
\renewcommand{\bnode}{\red{$\{0,2,5,8,11\}$}}
\renewcommand{\cnode}{\red{$\{11\}$}}
\renewcommand{\dnode}{\red{$\{0,2,5,8\}$}}
\renewcommand{\enode}{\red{$\{2,5,8\}$}}
\renewcommand{\fnode}{\red{$\{0\}$}}
\renewcommand{\gnode}{\red{$\{2,5,8,11\}$}}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Sets of states at each program point}
 Suppose that
\begin{itemize}
\item program state is given by the value of the integer variable $i$
\item initially, it is possible that i has any value
\end{itemize}
Compute the set of states at each vertex in the CFG.

\hspace*{1cm}
\begin{minipage}{4cm}
\lstset{commentstyle=\codestyle\color{gray}}
\lstinputlisting{cfg-program.scala}
\end{minipage}
%\hspace*{-1cm}
\scalebox{0.8}{\cfgex}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Sets of states at each program point}
{\bf Running the Program}

One way to describe the set of states for each program point: for each initial state, run the CFG with this state and 
insert the modified states at appropriate points.

\ \\

{\bf Reachable States as A Set of Recursive Equations}

If $c$ is the label on the edge of the graph, let $\rho(c)$ denotes the relation between initial and final state that describes the meaning of statement. For example,
\[
\begin{array}{l}
  \rho(i=0) = \{ (i,i') \mid i' = 0 \}  \\
  \rho(i=i+2) = \{ (i,i') \mid i' = i+2 \}  \\
  \rho(i=i+3) = \{ (i,i') \mid i' = i+3 \}  \\
  \rho([i<10]) = \{ (i,i') \mid i'=i \land i < 10 \} \\
\end{array}
\]
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Sets of states at each program point}

We will write $T(S,c)$ (transfer function) for the image of set $S$ under relation $\rho(c)$. For example,
\[
   T(\{ 10, 15, 20 \},i=i+2) = \{ 12, 17, 22 \}
\]
General definition can be given using the notion of strongest postcondition 
\[
   T(S,c) = sp(S,\rho(c))
\]

If [p] is a condition (assume(p), coming from 'if' or 'while') then
\[
   T(S, [p]) = \{ x \in S \mid p \}
\]

If an edge has no label, we denote it skip. So, $T(S,skip)=S$.

\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Reachable States as A Set of Recursive Equations}
Now we can describe the meaning of our program using recursive equations:
\begin{tabular}{ll}
\begin{minipage}{2.4in}
\[
\begin{array}{l}
S(a) = \{ \ldots, -2, -1, 0, 1, 2, \ldots \} \\
S(b) = T(S(a),i=0) \cup T(S(g),skip) \\
S(c) = T(S(b),[\lnot(i<10)]) \\
S(d) = T(S(b),[i<10]) \\
S(e) = T(S(d),[i>1]) \\
S(f) = T(S(d),[\lnot(i>1)]) \\
S(g) \begin{array}[t]{l}
       = T(S(e),i=i+3) \\
       \cup T(S(f),i=i+2) 
     \end{array}
\end{array}
\]
\end{minipage} &
%\begin{minipage}{2in}
%\includegraphics[width=2.5in]{cfg-inc.png}
%\end{minipage}
\scalebox{0.7}{\cfgex}
\end{tabular}

{\small
  Our solution is the unique \textbf{least} solution of these equations.
  Can be computed by iterating starting from empty sets as initial solution.

{\bf The problem:}
 These exact equations are as difficult to compute as running the program on all possible input states.
Instead, we consider \textbf{approximate} descriptions of these sets of states.
}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{A Large Analysis Domain: All Intervals of Integers}

For every $L,U \in \mathbb{Z}$ interval:
\[
   \{ x \mid L \le x \land x \le U \}
\]

This domain has infinitely many elements, but is already an approximation of
all possible sets of integers.

\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Smaller Domain: Finitely Many Intervals}
\small
We continue with the same example but instead of allowing to denote all possible sets, 
we will allow sets represented by expressions 
\[
    [L, U]
\]
which denote the set $\{ x \mid L \le x \land x \le U \}$. \\
{\bf Example: } $[0,127]$ denotes integers between $0$ and $127$. 

\begin{itemize}
\item $L$ is the lower bound and $U$ is the upper bound, with $L \le U$.
\item to ensure that we have only a few elements, we let
\[
    L, U \in \{ \mbox{MININT}, -128, 1, 0, 1, 127, \mbox{MAXINT} \}
\]
\item $[\mbox{MININT},\mbox{MAXINT}]$ denotes all possible integers, denote it $\top$
\item instead of writing $[1,0]$ and other empty sets, we will always write $\bot$
\end{itemize}
 

So, we only work with a finite number of sets $1 + {7 \choose 2} = 22$.

Denote the family of these sets by $D$ (domain).

\end{frame}

%%%%%%%%%%%%%%%%%%
\newcommand{\approxEqns}{
\[
\begin{array}{l}
S^\#(a) = \top \\
S^\#(b) \begin{array}[t]{l}
        = T^\#(S^\#(a),i=0) \\
        \sqcup\ T^\#(S^\#(g),skip)
        \end{array} \\
S^\#(c) = T^\#(S^\#(b),[\lnot(i<10)]) \\
S^\#(d) = T^\#(S^\#(b),[i<10]) \\
S^\#(e) = T^\#(S^\#(d),[i>1]) \\
S^\#(f) = T^\#(S^\#(d),[\lnot(i>1)]) \\
S^\#(g) \begin{array}[t]{l}
       = T^\#(S^\#(e),i=i+3) \\
       \sqcup\ T^\#(S^\#(f),i=i+2) 
\end{array}
\end{array}
\]
}

\begin{frame}
\frametitle{New Set of Recursive Equations}
We want to write the same set of equations as before, but because we have only a finite number of sets, we must approximate. We approximate sets with possibly larger sets.
\approxEqns
\begin{itemize}
\item 
$S_1 \sqcup S_2$ denotes the approximation of $S_1 \cup S_2$: it is the set that contains both $S_1$ and $S_2$, that belongs to $D$, and is otherwise as small as possible. Here $[a,b] \sqcup [c,d] = [min(a,c),max(b,d)]$
\item 
We use approximate functions $T^\#(S,c)$ that give a result in $D$.
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Updating Sets}
We solve the equations by starting in the initial state and repeatedly applying them.
\begin{itemize}
\item in the 'entry' point, we put $\top$, in all others we put $\bot$.
\end{itemize}

\renewcommand{\anode}{\red{$\top$}}
\renewcommand{\bnode}{\red{$\bot$}}
\renewcommand{\cnode}{\red{$\bot$}}
\renewcommand{\dnode}{\red{$\bot$}}
\renewcommand{\enode}{\red{$\bot$}}
\renewcommand{\fnode}{\red{$\bot$}}
\renewcommand{\gnode}{\red{$\bot$}}

\begin{minipage}{6.2cm}
{\small\approxEqns}
\end{minipage}
%\begin{minipage}{5.5cm}
%\ \\
%\ \\
%\includegraphics[width=1.1\textwidth]{cfg-inc-abst-init.png}
%\end{minipage}
\scalebox{0.8}{\cfgex}
\end{frame}

\renewcommand{\anode}{\red{$\top$}}
\renewcommand{\bnode}{\red{$[0,0]$}}
\renewcommand{\cnode}{\red{$\bot$}}
\renewcommand{\dnode}{\red{$[0,0]$}}
\renewcommand{\enode}{\red{$\bot$}}
\renewcommand{\fnode}{\red{$[0,0]$}}
\renewcommand{\gnode}{\red{$[2,2]$}}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Updating Sets}
Sets after a few iterations:

\begin{minipage}{6cm}
{\small\approxEqns}
\end{minipage}
%\begin{minipage}{6cm}
%\includegraphics[width=\textwidth]{cfg-inc-abst-oneiter.png}
%\end{minipage}
\scalebox{0.8}{\cfgex}
\end{frame}

\renewcommand{\anode}{\red{$\top$}}
\renewcommand{\bnode}{\red{$[0,2]$}}
\renewcommand{\cnode}{\red{$\bot$}}
\renewcommand{\dnode}{\red{$[0,2]$}}
\renewcommand{\enode}{\red{$[2,2]$}}
\renewcommand{\fnode}{\red{$[0,1]$}}
\renewcommand{\gnode}{\red{$[2,5]$}}

\begin{frame}
\frametitle{Updating Sets}
Sets after a few more iterations:

\begin{minipage}{6cm}
{\small\approxEqns}
\end{minipage}
%\begin{minipage}{6cm}
%\includegraphics[width=\textwidth]{cfg-inc-abst-oneiter.png}
%\end{minipage}
\scalebox{0.8}{\cfgex}
\end{frame}

\renewcommand{\anode}{\red{$\top$}}
\renewcommand{\bnode}{\red{$[0,12]$}}
\renewcommand{\cnode}{\red{$[10,12]$}}
\renewcommand{\dnode}{\red{$[0,9]$}}
\renewcommand{\enode}{\red{$[2,9]$}}
\renewcommand{\fnode}{\red{$[0,1]$}}
\renewcommand{\gnode}{\red{$[2,12]$}}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Fixpoint Found}
Final values of sets:

\begin{minipage}{5cm}
{\small\approxEqns}
\end{minipage}
%\begin{minipage}{6cm}
%\includegraphics[width=\textwidth]{cfg-inc-abst-final.png}
%\end{minipage}
\scalebox{0.8}{\cfgex}

If we map intervals to sets, this is also solution of the original constraints.
\end{frame}

\begin{frame}
\frametitle{Automatically Constructed Hoare Logic Proof}
Final values of sets:

\begin{minipage}{5cm}
\lstset{commentstyle=\codestyle\color{gray}}
\lstinputlisting{hoare-cfg-program.scala}
\end{minipage}
%\begin{minipage}{6cm}
%\includegraphics[width=\textwidth]{cfg-inc-abst-final.png}
%\end{minipage}
\scalebox{0.8}{\cfgex}

This method constructed a sufficiently annotated program and ensured that all 
Hoare triples that were constructed hold
\end{frame}


