blob: 8c5cf982adc6aea0cfb7b21b7656c0ae8c41af7b (
about) (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
\documentclass{article}
\usepackage[a4paper]{geometry}
\usepackage{hyperref}
\usepackage{amsmath}
\title{INFO5993 \\ Research outline}
\author{Carlo Zancanaro}
\begin{document}
\maketitle
\section{Introduction}
As my research contribution I intend to implement an algorithm presented in
\cite{gawlitza} for solving systems of fixpoint-equations for their least
solutions. I will then utilise this algorithm for the implementation of a static
analysis pass, interpreting program semantics over zones, within the LLVM
compiler framework. Finally I will be evaluating this new technique to determine
whether it is of practical use in real-world static analysis.
\section{Technologies}
My implementation will be provided in the {\tt C++} programming language, as it
is the language in which LLVM has been written. It will primarily be designed to
analyse programs written in the {\tt C} language.
At the conclusion of my thesis I will have an implementation of the above
algorithm implemented as an LLVM optimisation/analysis pass. This will plug in
to the LLVM/Clang static-analysis framework in order to leverage the significant
work that has been done on the LLVM project. This will also mean that I do not
have to write a complete parser for the {\tt C} programming language (which
would no doubt be a long and error-prone operation).
\section{Evaluation}
To evaluate the algorithm I will be investigating two factors: execution time
and analysis range.
\subsection{Execution time}
Given the increased precision of results provided by the above algorithm I will
be interested in determining the runtime performance of the algorithm. Static
analysis is traditionally a slow process and so any speed-gains which can be
made will be especially beneficial to real world applications. This will also
mean that my optimisations must be especially aggressive to ensure that there is
no missed opportunity for speed gains to be made.
\subsection{Analysis range}
In the above algorithm there is a trade-off made wherein we sacrifice the
generality of the algorithm to provide more precise results. An important factor
in the utility of this algorithm will be whether it is applicable to the
majority of real-world code. The restrictions in the paper seem to be general
enough to encompass a large amount of existing code, but it remains to be shown
empirically whether this is the case.
\section{Conclusion}
My thesis will consist of implementing and evaluating a new approach to
fixpoint-iteration in order to perform abstract interpretation over zones for
the verification of program invariants. This implementation will be done within
the LLVM-compiler framework. The evaluation will particularly consider factors
of execution time and analysis range of the algorithm.
\bibliographystyle{abbrv}
\bibliography{references.bib}
\end{document}
|
