Skip to content

Ptanal polishing #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: ptanal-fixes
Choose a base branch
from
Open

Ptanal polishing #13

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0654f7e
Fix incomplete documentation with respect to Ptranal.
cspiel Jul 5, 2014
0833977
Document the new option `--ptr_use_olf' of cilly.
cspiel Jul 5, 2014
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 19 additions & 14 deletions doc/cil.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1935,15 +1935,14 @@ \subsection{Dominators}
\subsection{Points-to Analysis}

The module \t{ptranal.ml} contains two interprocedural points-to
analyses for CIL: \t{Olf} and \t{Golf}. \t{Olf} is the default.
(Switching from \t{olf.ml} to \t{golf.ml} requires a change in
\t{Ptranal} and a recompiling \t{cilly}.)
analyses for CIL: \t{Olf} and \t{Golf}. \t{Golf} is the default.
Switch to \t{Olf} with {\bf -{}-ptr\_use\_olf}.

The analyses have the following characteristics:
\begin{itemize}
\item Not based on C types (inferred pointer relationships are sound
despite most kinds of C casts)
\item One level of subtyping
\item One level of subtyping
\item One level of context sensitivity (Golf only)
\item Monomorphic type structures
\item Field insensitive (fields of structs are conflated)
Expand All @@ -1953,12 +1952,18 @@ \subsection{Points-to Analysis}

The analysis itself is factored into two components: \t{Ptranal},
which walks over the CIL file and generates constraints, and \t{Olf}
or \t{Golf}, which solve the constraints. The analysis is invoked
with the function \t{Ptranal.analyze\_file: Cil.file ->
unit}. This function builds the points-to graph for the CIL file
and stores it internally. There is currently no facility for clearing
internal state, so \t{Ptranal.analyze\_file} should only be called
once.
or \t{Golf}, which solve the constraints.

The analysis is invoked with the function \t{Ptranal.analyze\_file:
Cil.file -> unit}. This function builds the points-to graph for the
CIL file and stores it internally. (There is currently no facility
for clearing internal state, so \t{Ptranal.analyze\_file} should only
be called once.) After building the points-to graph the result
database must be built with a call to \t{Ptranal.compute\_results: bool ref -> unit}.
This will essentially serialize the points-to graph. If invoked with \t{true}, the
function will print out the points-to set of each variable in the
file, which is useful for debugging.


%%% Interface for querying the points-to graph...
The constructed points-to graph supports several kinds of queries,
Expand Down Expand Up @@ -1986,6 +1991,10 @@ \subsection{Points-to Analysis}
of several flags:

\begin{itemize}
\item \t{Ptranal.olf\_backend: bool ref}.
If \t{true}, module \t{Olf} performs the analysis. The default is
\t{false} and module \t{Golf} is used. Associated commandline option:
{\bf -{}-ptr\_use\_olf}.
\item \t{Ptranal.no\_sub: bool ref}.
If \t{true}, subtyping is disabled. Associated commandline option:
{\bf -{}-ptr\_unify}.
Expand Down Expand Up @@ -2040,10 +2049,6 @@ \subsection{Points-to Analysis}
\t{true}, this output is sufficient to reconstruct the points-to
graph. One nice feature is that there is a pretty printer for
recursive types, so the print routine does not loop.
\item \t{Ptranal.compute\_results: bool ref}.
If \t{true}, the analysis will print out the points-to set of each
variable in the program. This will essentially serialize the
points-to graph.
\end{itemize}

\subsection{StackGuard}
Expand Down