Commit afa55b8b authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Initial commit

parents
include ../common.mk
all: slides-automates-interpretes.pdf
slides-automates-interpretes.pdf:
# Fdb version 3
["pdflatex"] 1522421015 "slides-automates-interpretes.tex" "latexmk/slides-automates-interpretes.pdf" "slides-automates-interpretes" 1522421015
"/etc/texmf/web2c/texmf.cnf" 1514599600 475 c0e671620eb5563b2130f56340a5fde8 ""
"/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1503024366 32036 8f10cb8f6ef259fb5791f09c065d3d13 ""
"/usr/share/texmf/web2c/texmf.cnf" 1503024366 32036 8f10cb8f6ef259fb5791f09c065d3d13 ""
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1514604876 746790 783f1306a03726491aef5babf67e730d ""
"latexmk/slides-automates-interpretes.aux" 1522421015 8 a94a2480d3289e625eea47cd1b285758 ""
"slides-automates-interpretes.tex" 1522420935 1632 c1ef7cabf46c3a82e77453ec9e6c7ad8 ""
(generated)
"latexmk/slides-automates-interpretes.log"
"latexmk/slides-automates-interpretes.pdf"
PWD /export/home/vperrelle/work/presentations/2018-lsl-automates-interpetes
INPUT /etc/texmf/web2c/texmf.cnf
INPUT /usr/share/texmf/web2c/texmf.cnf
INPUT /usr/share/texlive/texmf-dist/web2c/texmf.cnf
INPUT /var/lib/texmf/web2c/pdftex/pdflatex.fmt
INPUT slides-automates-interpretes.tex
OUTPUT latexmk/slides-automates-interpretes.log
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/Debian) (preloaded format=pdflatex 2017.12.30) 30 MAR 2018 16:43
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**slides-automates-interpretes.tex
(./slides-automates-interpretes.tex
LaTeX2e <2017-04-15>
Babel <3.12> and hyphenation patterns for 5 language(s) loaded.
! LaTeX Error: Missing \begin{document}.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.1 -
--
?
! Emergency stop.
...
l.1 -
--
You're in trouble here. Try typing <return> to proceed.
If that doesn't work, type X <return> to quit.
Here is how much of TeX's memory you used:
7 strings out of 494902
367 string characters out of 6179581
46338 words of memory out of 5000000
3422 multiletter control sequences out of 15000+600000
3640 words of font info for 14 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191
5i,0n,4p,38b,14s stack positions out of 5000i,500n,10000p,200000b,80000s
! ==> Fatal error occurred, no output PDF file produced!
---
title: "Interpreted Automata and how they are used in Frama-C"
author: Valentin Perrelle
date: April 9, 2018
header-includes:
- \usepackage{tikz}
- \usepackage{macros}
- \usetikzlibrary{chains,interpretedautomata,backgrounds,calc}
...
Interpreted Automata
====================
Context
-------
- Static analysis of C code with \FramaC / \Eva
- Control Flow partially abstracted by Cil
- All loops are transformed into `while (true)` loops
- Returns are only allowed as the last statement
- The `Cfg` module can translate `break`, `continue` and `switch` to
`if` and `goto`
- The analysis still have to deal with "undefined sequences"
- ... and new constructs from C++ like `try` - `catch`
- Generic dataflow analysis are possible (modules `Dataflow2`, `Dataflows`)
- It completely abstract the control-flow for the analyser, but forces the
logic and the order of iteration
Why use intermediate representations ?
--------------------------------------
- Avoir une représentation intermédiaire du flot de contrôle
- Décharge du besoin de se préoccuper de l'analyse du flot de contrôle
- Ouverte aux transformations
- (Indépendante du langage source)
- Sans notion d'ordre d'itération
- Les analyses peuvent fixer l'ordre d'itération librement
Automates Interprétés : Exemple {.fragile}
-------------------------------
\noindent
\begin{minipage}{.3\textwidth}
\begin{lstlisting}[language=C]
int i = 0, j = 0;
while (i < 10) {
if (i % 2) {
j++;
}
i++;
}
\end{lstlisting}
\end{minipage}
\begin{minipage}{.3\textwidth}
\begin{tikzpicture}[chainautomata]
\node[cp] (c1) {$c_1$};
\node[cp] (c2) {$c_2$};
\node[cp] (c3) {$c_3$};
\node[cp] (c4) {$c_4$};
\node[cp] (c5) {$c_5$};
\node[cp] (c7) {$c_7$};
\node[cp,right=16mm of c4] (c8) {$c_8$};
\node[cp,right=of c5] (c6) {$c_6$};
\draw
(c1) edge node[right] {\tt i = 0} (c2)
(c2) edge node[right] {\tt j = 0} (c3)
(c3) edge node[right] {\tt i < 10} (c4)
edge node[above right] {\tt i >= 10} (c8)
(c4) edge node[left] {\tt i \% 2} (c5)
edge node[right] {\tt !(i \% 2)} (c6)
(c5) edge node[left] {\tt j++} (c7)
(c6) edge node[right] {\tt j += 2} (c7)
(c7) edge [bend left=90] node[left] {\tt i++} (c3)
;
\end{tikzpicture}
\end{minipage}
Définition
----------
- Graphe de flot de contrôle
Flot de contrôle + annotation sur les arcs
- Représentation intermédiaire
- Motivation : Simplifier le traitement des statements
Semantics {.fragile}
---------
\newcommand{\abs}[1]{#1^\#}
### Operational Semantics
\noindent
\begin{minipage}{.23\textwidth}
\centering
\begin{tikzpicture}[chainautomata]
\node [cp] (c1) {$c_1$};
\node [cp] (c2) {$c_2$};
\draw
(c1) edge node[right] {$f$} (c2)
;
\end{tikzpicture}
\end{minipage}
\begin{minipage}{.75\textwidth}
\begin{tabular}{lll}
$f$ is a {\bf guard} : & $c1,\sigma \longrightarrow c2,\sigma$ & if $f(\sigma)$ \\
$f$ is a {\bf command} : & $c1,\sigma \longrightarrow c2,f(\sigma)$ &
\end{tabular}
\end{minipage}
### Collecting Semantics
\noindent
\begin{minipage}{.23\textwidth}
\centering
\begin{tikzpicture}[chainautomata]
\node [cp] (c1) {$c_1$};
\node [right=2mm of c1] (c2) {$\dots$};
\node [cp,right=2mm of c2] (cn) {$c_n$};
\node [cp,below=5mm of c2] (d) {$d$};
\draw
(c1) edge node[left] {$F_1$} (d)
(c2) edge (d)
(cn) edge node[right] {$F_n$} (d)
;
\end{tikzpicture}
\end{minipage}
\begin{minipage}{.75\textwidth}
\[
Y = \bigcup_{c_i \rightarrow d} F_i\tikzlabel{tf}(X_i)
\]
\end{minipage}
\uncover<2>{\tikzcomment{tf}{{\it Transfer functions}, in theory could be \\ any monotonic function}}
### Abstract Semantics
\noindent
\begin{minipage}{.23\textwidth}
\centering
\begin{tikzpicture}[chainautomata]
\node [cp] (c1) {$c_1$};
\node [right=2mm of c1] (c2) {$\dots$};
\node [cp,right=2mm of c2] (cn) {$c_n$};
\node [cp,below=5mm of c2] (d) {$d$};
\draw
(c1) edge node[left] {$\abs{F}_1$} (d)
(c2) edge (d)
(cn) edge node[right] {$\abs{F}_n$} (d)
;
\end{tikzpicture}
\end{minipage}
\begin{minipage}{.75\textwidth}
\[
\abs{Y} = \bigsqcup_{c_i \rightarrow d} \abs{F}_i(\abs{X}_i)
\]
\end{minipage}
Expressivity {.fragile}
------------
### Incompleteness
\centering
\begin{tikzpicture}[chainautomata]
\node[cp] (c1) {$c_1$};
\node[cp] (c2) {$c_2$};
\node[cp] (c3) {$c_3$};
\draw
(c1) edge node[right] {\tt i = [0..10]} (c2)
(c2) edge node[right] {\tt i < 5} (c3)
;
\end{tikzpicture}
### Nondeterminism
\centering
\begin{tikzpicture}[chainautomata]
\node[cp] (c1) {$c_1$};
\node[cp] (c2) {$c_2$};
\node[cp,below left=5mm and 3mm of c2] (c3) {$c_3$};
\node[cp,below right=5mm and 3mm of c2] (c4) {$c_4$};
\draw
(c1) edge node[right] {\tt i = [0..10]} (c2)
(c2) edge node[left] {\tt i < 7} (c3)
edge node[right] {\tt i > 3} (c4)
;
\end{tikzpicture}
Weak Topological Order {.fragile}
----------------------
\noindent
\begin{minipage}{.4\textwidth}
\begin{onlyenv}<1-2>
\begin{lstlisting}[language=C]
int A[10][10];
int i = 0;
while (i < 10) {
int j = 0;
while (j < 10) {
A[i][j] = 0;
j++;
}
i++;
}
\end{lstlisting}
\end{onlyenv}
\begin{onlyenv}<3->
\begin{lstlisting}[language=C]
int A[10][10];
int i = 0;
l1: if (i < 10) {
int j = 0;
l2 : if (j < 10) {
A[i][j] = 0;
j++;
goto l2;
}
i++;
goto l1;
}
\end{lstlisting}
\end{onlyenv}
\end{minipage}
\begin{minipage}{.5\textwidth}
\only<1>{\tikzstyle{head} = [cp]}
\only<2->{\tikzstyle{head} = [wp]}
\begin{tikzpicture}[chainautomata]
\node[cp] (c1) {$c_1$};
\node[head] (c2) {$c_2$};
\node[cp] (c3) {$c_3$};
\node[head] (c4) {$c_4$};
\node[cp] (c5) {$c_5$};
\node[cp] (c6) {$c_6$};
\node[cp] (c7) {$c_7$};
\node[cp,right=20mm of c3] (c8) {$c_8$};
\draw
(c1) edge node[right] {\tt i = 0} (c2)
(c2) edge node[right] {\tt i < 10} (c3)
edge node[above right] {\tt i >= 10} (c8)
(c3) edge node[right] {\tt j = 0} (c4)
(c4) edge node[right] {\tt j < 10} (c5)
(c5) edge node[right] {\tt A[i][j] = 0} (c6)
(c6) edge [bend left=45] node[left] {\tt j++} (c4)
(c7) edge [bend left=70] node[left] {\tt i++} (c3)
;
\draw (c4) .. controls +(2.0, 0) and +(2.0,0.0) .. node[right] {\tt j >= 10} (c7);
\begin{scope}[on background layer]
\uncover<2->{
\draw[component,fill=white!80!green] ($(c7.south west)-(1.5,0.2)$) rectangle ($(c2.north east)+(1.5,0.1)$);
\draw[component] ($(c6.south west)-(0.4,0.2)$) rectangle ($(c4.north east)+(0.4,0.1)$);
}
\end{scope}
\end{tikzpicture}
\uncover<2->{
$(c_1~(c_2~c_3~(c_4~c_5~c_6)~c_7)~c_8)$
}
\end{minipage}
Pourquoi le Wto ?
-----------------
- Calcul
- Intérêt
- reconstruit les boucles originales mais détecte également les boucles non originales
- marche aussi sur les boucles non naturelles
- définit des points de widening
Wto avec priorités
------------------
Avantages (invariants de boucles), inconvénients (boucles non naturelles)
Les automates interprétés dans Frama-C
======================================
Frama-C Architecture Changes
----------------------------
\begin{center}
\tikzstyle{brique} = [
rounded corners=2mm,
draw, semithick,
blur shadow={shadow blur steps=5},
minimum height=10mm,
minimum width=18mm,
align=center,
font=\small,
node distance=5mm
]
\tikzstyle{original} = [brique,fill=white!80!green]
\tikzstyle{changed} = [brique,fill=white!80!yellow]
\begin{tikzpicture}[>=stealth]
\node (CAbs) [original] {CAbs};
\node (Cil) [original,right=of CAbs] {Cil};
\node (Cfg) [original,right=of Cil] {Cfg};
\node (Dtf) [original,right=of Cfg] {Dataflow};
\node (M1) [above right=of Dtf] {\dots};
\draw[->] (CAbs.east) to (Cil.west);
\draw[->] (Cil.east) to (Cfg.west);
\draw[->] (Cfg.east) to (Dtf.west);
\draw[->] (Dtf.east) to (M1.west);
\uncover<1>{
\node (PD) [original,right=of Dtf] {Eva};
\node (WP) [original,below right=6mm and 6mm of Cfg] {WP};
\draw[->] (Dtf.east) to (PD.west);
\draw[->] (Cfg.east) to (WP.west);
}
\uncover<2>{
\draw[dashed] (Cfg.south west) -- ($(Cfg.south west)-(0,0.6)$);
\draw[dashed] (Cfg.south east) -- ($(Cfg.south east)-(0,0.6)$);
\draw[dashed] (Dtf.south west) -- ($(Dtf.south west)-(0,0.6)$);
\draw[dashed] (Dtf.south east) -- ($(Dtf.south east)-(0,0.6)$);
\node (M2) [right=of Dtf] {\dots};
\node (IA) [changed,below right=6mm and 5mm of Cil, minimum width=28mm] {Interpreted \\ Automata};
\node (PD') [changed,right=of IA] {Eva};
\node (WP') [changed,below right=6mm and 5mm of IA] {WP};
\draw[->] (Dtf.east) to (M2.west);
\draw[->] (Cil.east) to (IA.west);
\draw[->] (IA.east) to (PD'.west);
\draw[->] (IA.east) to (WP'.west);
}
\end{tikzpicture}
\end{center}
Intérêt des automates interprétés
---------------------------------
Simplification du moteur d'itération
- Leave / Enter, If-then-else, Instanciation du foncteur Dataflow
Ajout de passes de compilation intermédiaires
Réutilisation de la structure pour exporter les informations
Ocaml Definition
----------------
Choix architecturaux
--------------------
- Une seule fonction de transfert par arc
- Beaucoup de noeuds intermédiaires
Calcul de point fixe sur un automate interprété
-----------------------------------------------
Séquences descendantes
----------------------
- Intérêt
- Chemins de sortie
Bonus : slevel vs déroulage de boucles
======================================
\section{Interpreted Automata}\label{interpreted-automata}
\begin{frame}[fragile]{Context}
\begin{itemize}
\tightlist
\item
Analyse statique de code C avec FramaC / Eva
\item
Flot de contrôle déjà partiellement abstrait par Cil
\begin{itemize}
\tightlist
\item
Toutes les boucles sont transformées en boucles
\lstinline!while (true)!
\end{itemize}
\item
Algorithmes flot de données génériques (\lstinline!Dataflow2!,
\lstinline!Dataflows!)
\begin{itemize}
\tightlist
\item
Abstrait le flot de contrôle mais fixe l'ordre d'itération
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}{Automates Interprétés : Motivation}
\begin{itemize}
\tightlist
\item
Avoir une représentation intermédiaire du flot de contrôle
\begin{itemize}
\tightlist
\item
Décharge du besoin de se préoccuper de l'analyse du flot de contrôle
\item
Ouverte aux transformations
\item
(Indépendante du langage source)
\end{itemize}
\item
Sans notion d'ordre d'itération
\begin{itemize}
\tightlist
\item
Les analyses peuvent fixer l'ordre d'itération librement
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]{Automates Interprétés : Exemple}
\noindent
\begin{minipage}{.3\textwidth}
\begin{lstlisting}[language=C]
int i = 0, j = 0;
while (i < 10) {
if (i % 2) {
j++;
}
i++;
}
\end{lstlisting}
\end{minipage}\begin{minipage}{.3\textwidth}
\begin{tikzpicture}[chainautomata]
\node[cp] (c1) {$c_1$};
\node[cp] (c2) {$c_2$};
\node[cp] (c3) {$c_3$};
\node[cp] (c4) {$c_4$};
\node[cp] (c5) {$c_5$};
\node[cp] (c7) {$c_7$};
\node[cp,right=16mm of c4] (c8) {$c_8$};
\node[cp,right=of c5] (c6) {$c_6$};
\draw
(c1) edge [->] node[right] {\tt i = 0} (c2)
(c2) edge [->] node[right] {\tt j = 0} (c3)
(c3) edge [->] node[right] {\tt i < 10} (c4)
edge [->] node[above right] {\tt i >= 10} (c8)
(c4) edge [->] node[left] {\tt i \% 2} (c5)
edge [->] node[right] {\tt !(i \% 2)} (c6)
(c5) edge [->] node[left] {\tt j++} (c7)
(c6) edge [->] node[right] {\tt j += 2} (c7)
(c7) edge [->,bend left=90] node[left] {\tt i++} (c3)
;
\end{tikzpicture}
\end{minipage}
\end{frame}
\begin{frame}{Définition}
\begin{itemize}
\tightlist
\item
Graphe de flot de contrôle Flot de contrôle + annotation sur les arcs
\item
Représentation intermédiaire
\item
Motivation : Simplifier le traitement des statements
\end{itemize}
\end{frame}
\begin{frame}[fragile]{Semantics}
\newcommand{\abs}[1]{#1^\#}
\begin{block}{Operational Semantics}
\noindent
\begin{minipage}{.23\textwidth}
\centering
\begin{tikzpicture}[chainautomata]
\node [cp] (c1) {$c_1$};
\node [cp] (c2) {$c_2$};
\draw
(c1) edge [->] node[right] {$f$} (c2)
;
\end{tikzpicture}
\end{minipage}\begin{minipage}{.75\textwidth}
\begin{tabular}{lll}
$f$ is a {\bf guard} : & $c1,\sigma \longrightarrow c2,\sigma$ & if $f(\sigma)$ \\
$f$ is a {\bf command} : & $c1,\sigma \longrightarrow c2,f(\sigma)$ &
\end{tabular}
\end{minipage}
\end{block}
\begin{block}{~Collecting Semantics}
\noindent
\begin{minipage}{.23\textwidth}
\centering
\begin{tikzpicture}[chainautomata]
\node [cp] (c1) {$c_1$};
\node [right=2mm of c1] (c2) {$\dots$};
\node [cp,right=2mm of c2] (cn) {$c_n$};
\node [cp,below=5mm of c2] (d) {$d$};
\draw
(c1) edge [->] node[left] {$F_1$} (d)
(c2) edge [->] (d)
(cn) edge [->] node[right] {$F_n$} (d)
;
\end{tikzpicture}
\end{minipage}\begin{minipage}{.75\textwidth}
\[
Y = \bigcup_{c_i \rightarrow d} F_i\tikzlabel{tf}(X_i)
\]
\end{minipage}