\documentclass[11pt]{article}
\usepackage{palatino}
\usepackage{latexsym}
\usepackage{verbatim}
\usepackage{alltt}
\usepackage{url}
\usepackage{amsmath,proof,amsthm,amssymb,enumerate}

% FIXME be more precise about parens in question 2

\newcommand{\question}[2]
  {\bigskip \noindent
   {\bf Question #1} (#2 points).}

\newcommand{\extracreditquestion}[1]
  {\bigskip \noindent
   {\bf Question #1} (EXTRA CREDIT).}

\newcommand{\definition}[2]
  {\bigskip
   \begin{tabular}{p{1.5in}p{4.0in}}
        \textbf{#1} & #2 \\
        \end{tabular}
  }

\def\prop{\textsf{\,\,prop}}
\def\thm{\textsf{\,\,thm}}
\def\implies{\Rightarrow}

\title{Assignment 5 (Written/Programming):\\
Dataflow Analysis}
\author{17-654/17-754: Analysis of Software Artifacts \\
        Jonathan Aldrich ({\tt jonathan.aldrich@cs.cmu.edu})}
\date{Due: Thursday, March 2, 2006 (5:00 pm) \\[1em]
100 points total
}

\begin{document}
\begin{sloppypar}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}

\newcommand{\pfalse}{\mbox{false}}
\newcommand{\ptrue}{\mbox{true}}
\newcommand{\pand}{\mbox{and}}
\newcommand{\por}{\mbox{or}}
\newcommand{\pskip}{\mbox{skip}}
\newcommand{\pif}{\mbox{if}}
\newcommand{\pthen}{\mbox{then}}
\newcommand{\pelse}{\mbox{else}}
\newcommand{\pdo}{\mbox{do}}
\newcommand{\pwhile}{\mbox{while}}




\maketitle

Turn in a file named $<$username$>$-17654-A5.\{zip\}, where username
is your Andrew id.  The zip file should contain the file answers.xxx
(the answers to text questions in txt, pdf, or Word (doc) format),
each of the .java files you wrote, and output.xxx (either analysis
output in .txt format or a screenshot in some common graphics format).
At the top of answers.txt, state your name,
Andrew id, and how long you spent on the assignment.


\vspace{1ex}\noindent\textbf{Assignment Objectives:}
\begin{itemize}
\item Precisely define an analysis using lattices, abstraction functions, and flow functions.
\item Implement a dataflow analysis in a code framework built based on the concepts of flow functions and lattices.
\item Demonstrate understanding of local soundness by providing a counterexample to local soundness for a buggy analysis specification.
\end{itemize}


\clearpage

\section{Valid Pointer Analysis Specification (30 points)}

Your first task is to precisely define a valid pointer analysis for
\textsc{While}.  A valid pointer is a pointer which it is safe to
dereference (i.e. it is not null and does not point to garbage).
Assume that \textsc{While} has been extended with
the following syntactic construct:

\[
\begin{array}{lll}
a & ::= & ... \\
 & | & \&x \\
\end{array}
\]

The $\&x$ expression takes the address of some variable $x$, resulting
in a valid pointer.  For the present, we will assume \textsc{While}
has a C-like pointer model, where regular integer variables can hold
pointer values.  We represent null with the constant 0.  We also
assume that integer constants--including zero--are not valid pointers.

\question{1.1}{15}

\begin{quote}
Design a lattice for a single variable.  Your lattice should be able
to represent both definitely valid and definitely not valid states, as well as
possibly valid. Define the lattice by
giving (a) the set of lattice elements and (b) the ordering relation
between them, (c) the top element and (d) the bottom element.
%5, 5, 3, 2
\end{quote}

\question{1.2}{5}
\begin{quote}
What is the initial analysis information before the first statement of
each function?  Justify your choice (more than one answer may be
correct, so long as it is justified).
%2 points for the analysis info, 3 for the justification
\end{quote}

\question{1.3}{10}
\begin{quote}
Define the flow functions for your analysis, using the notation given
in class.  Naturally, you will need to include flow functions for the
new expression form $\&x$, as well as for integer constants such as 0
(which are invalid pointers).
\end{quote}

\clearpage

\section{Valid Pointer Analysis Implementation (50 points)}

Next, you will implement your valid pointer analysis for the Java
programming language using Crystal.  In Java, integer variables are
separate from pointer variables, so your implementation need not keep
track of whether integer variables and expressions are valid or not
(you may if you wish; if so, these are all invalid).  However, pointer
variables are either valid or null (with null taking the place of 0 in
\textsc{While}).  Thus, your analysis should track the nullness of
local variables, but should assume that values in fields and method
parameters could be either null or non-null.

You should implement your analysis by defining a new subclass of
LatticeElement which describes a valid pointer lattice for a single
variable, and using this with the TupleLattice class to build a tuple
lattice for vlaid pointer analysis.  You should subclass
FlowAnalysisDefinition to define your flow functions as well as the
initial and bottom analysis info.

Finally, you should subclass AbstractCrystalMethodAnalysis to write a
client analysis that will report invalid pointer dereferences.  Your
analysis should produce a warning in the errors window or the console
for each of the errors marked with comments in the test file
TestNull.java.

To make the assignment more feasible to grade, all the classes you write
must be put in the package edu.cmu.cs.crystal2.asst5.  The client
analysis class (the one that inherits from
AbstractCrystalMethodAnalysis and needs to be registered in
CrystalPlugin) must be named NullPointerAnalysis.java.


\question{2.1}{10}
\begin{quote}
Turn in a screenshot of the problems window, or the text produced by
your analysis if you wrote to the errors window. When capturing the
screenshot, resize the window if necessary to show all the errors.
\end{quote}

\question{2.2}{40}
\begin{quote}
Turn in your analysis code.  Your code should follow the basic design
described above.  Remember to use package edu.cmu.cs.crystal2.asst5
and client class name NullPointerAnalysis.java.

\textbf{Important note:} Your code must be robust.  For example, it
should not throw unexpected exceptions when analyzing valid Java code
(these exceptions will show up on the Crystal console).  We will be
running your code on a large codebase to check its robustness, and we
recommend you do so as well.  One simple approach is to run your analysis
on the Crystal codebase.
\end{quote}

%\clearpage

\section{Local Soundness (20 points)}

Consider the following hypothetical flow function for constant
propagation:

\[
f_{\mbox{\tiny{CP}}}(\sigma,[[...]_n + [...]_m]_k) = [t_k {\mapsto} (\sigma(t_n) -_{\top} \sigma(t_m))] \sigma
\]

Here the operator $-_{\top}$ is like $\textit{op}_{\top}$ defined in
lecture: the same as $-$ for integers, but yeilding $\top$ if either of
its operands is $\top$.

This flow function is ``obviously'' incorrect.  However, to prove that
it is incorrect, you must show that it violates the criterion of local
soundness defined in class.  That is, you must find an environment
 $\eta$ and a statement $S$ such that $(\eta,S) \mapsto (\eta',S')$
and $\alpha_{\textit{CP}}(\eta') \not\sqsubseteq f_{\textit{CP}}^*(\sigma, S)$
with $\sigma = \alpha_{\textit{CP}}(\eta)$.

\question{3.1}{5}
\begin{quote}
Find a pair $(\eta, S)$ that illustrates the local unsoundness.
What are $\eta$ and $S$?
\end{quote}

\question{3.4}{2}
\begin{quote}
What is $\sigma=\alpha_{\textit{CP}}(\eta)$?
\end{quote}

\question{3.3}{3}
\begin{quote}
Assume $(\eta, S) \mapsto (\eta',\textit{skip})$.  What is $\eta'$?
\end{quote}

\question{3.5}{2}
\begin{quote}
What is $\alpha_{\textit{CP}}(\eta')$?
\end{quote}

\question{3.6}{4}
\begin{quote}
What is $\sigma'=f_{\textit{CP}}^*(\sigma, S)$?
\end{quote}

\question{3.7}{4}
\begin{quote}
Show that $\alpha_{\textit{CP}}(\eta') \not\sqsubseteq \sigma'$
\end{quote}




\end{sloppypar}
\end{document}
