Skip to content
Snippets Groups Projects
Commit a1ace968 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[doc] restore PDG and Slicing french documentation

parent 1d061de1
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2574 additions and 0 deletions
doc/pdg/.gitignore 0 → 100644
+ 6
− 0
View file @ a1ace968
biblio.bib
frama-c-book.cls
frama-c-cover.pdf
frama-c-left.pdf
frama-c-right.pdf
main.pdf
doc/pdg/Makefile 0 → 100644
+ 70
− 0
View file @ a1ace968
.PHONY: all clean
all: main.pdf
GENERATED=biblio.bib
GENERATED+=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
include ../MakeLaTeXModern
DWNLDDIR=../manuals
DOCNAME=pdg-documentation-fr.pdf
TEST_DIR=../../tests/pdg/
BIB_FILE = ../slicing/bib-slicing.bib
main.bbl : $(BIB_FILE)
@echo "=== Fichier .bib plus récent -> effacement du .bbl"
rm -f $(SRC).bbl
main.pdf: $(FRAMAC_MODERN) $(BIB_FILE) \
main.tex pdg.tex macros_pdg.tex \
intro.tex conclusion.tex \
data.tex ctrl.tex calls.tex utilisation.tex mark.tex impact.tex \
../images/cealistlogo.jpg \
exple-call.c call-f.pdf call-g.pdf \
ctrl-dpds.pdf ex-goto.pdf goto.pdf pdg-call.pdf
###############################################################################
GENERATED+=call-f.fig call-g.fig
%.fig : %.dot
dot -Tfig $< > $@
GENERATED+=call-f.pdf call-g.pdf
%.pdf : %.fig
fig2dev -L pdf $< $@
GENERATED+=call-f.dot call-g.dot
call-%.dot : $(TEST_DIR)/call.%.dot
cp $< $@
call-%.dot :
@echo
@echo "ERROR : $@ not found : you should run PDG tests to have it"
@echo " Run : cd ../.. ; make pdg_tests ; cd - "
@echo
exit 1
GENERATED+=exple-call.c
exple-%.c : $(TEST_DIR)/%.c
sed "1,/BDOC/d" $< > $@
###############################################################################
%.pdf: %.tex
pdflatex $*
bibtex $*
pdflatex $*
pdflatex $*
install: main.pdf
@echo "copying main.pdf in $(DWNLDDIR)/$(DOCNAME)"
@rm -f "$(DWNLDDIR)/$(DOCNAME)"
@cp main.pdf "$(DWNLDDIR)/$(DOCNAME)"
clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
*.haux *.hbbl *.htoc \
*.cb *.cb2 *.cm? *.bbl *.blg *.idx *.ind *.ilg \
$(GENERATED)
###############################################################################
doc/pdg/calls.tex 0 → 100644
+ 209
− 0
View file @ a1ace968
\chapter{Dépendances interprocédurales}\label{sec-intro-call}
On a vu qu'un PDG est associé à une fonction.
La question se pose donc de savoir
comment calculer des dépendances interprocédurales, c'est-à-dire comment mettre
en relation les appels de fonctions et les dépendances des fonctions appelées.
Nous allons tout d'abord voir qu'un appel de fonction
est représenté par plusieurs éléments dans le PDG (\S\ref{sec-call}).
Puis, nous allons voir que pour mettre en relation des appels et les fonctions
appelées, ils faut ajouter d'autres éléments à chaque fonction
(\S\ref{sec-fct-inout}).
\section{Appels de fonction}\label{sec-call}
L'instruction contenant l'appel est représentée par plusieurs
éléments dans le graphe de dépendances
afin de pouvoir plus précisément mettre en relation les appels aux
fonctions appelées.
Les éléments créés sont les suivants~:
\begin{itemize}
\item un élément pour chaque paramètre de la fonction appelée;
les dépendances sont crées par une simulation
de l'affectation des arguments d'appel dans les paramètres formels,
\item un élément représentant le contrôle du point d'entrée de la fonction
appelée (un peu comme si l'appel était dans un bloc et que ce noeud
représentait ce bloc),
\item un élément pour chaque sortie, dépendant des entrées correspondantes.
\end{itemize}
Pour ne pas avoir à calculer les flots de données de toutes les fonctions de
l'application, il a été décidé d'utiliser les dépendances ({\it from})
calculées indépendamment par \ppc.
La liste des entrées et des sorties, ainsi que les dépendances entre les unes et
les autres sont extraites des spécifications des fonctions appelées, et non de
leur PDG\footnote{c'est peut-être un problème
si on fait de la coupure de branche, car les dépendances peuvent être réduites
par une telle spécialisation.}.
Ceci est vrai également pour les
fonctions dont le code est absent de l'application étudiée
car cela permet d'être cohérent avec les autres analyses.
Cela permettra en particulier, d'utiliser d'éventuelles propriétés
fournies par la suite par l'utilisateur.
\begin{exemple}
\begin{tabular}{m{0.35\textwidth} m{0.6\textwidth}}
\begin{verbatim}
struct {int a;
int b; } G;
/*@ assigns \result {a},
G.a {G, a} */
int g (int a);
int f (int x, int y) {
G.b = x;
x = g (x+y);
return x + G.b;
}
\end{verbatim}
&
Ici, pour représenter l'appel à \verbtt{g} dans \verbtt{f} dans le PDG,
on va avoir~:
\begin{itemize}
\item un élément représentant le point d'entrée dans \verbtt{g},
\item un élément $e_1$ pour représenter \verbtt{a = x+y},
c'est-à-dire l'affectation de l'argument de l'appel
dans le paramètre formel de \verbtt{g},
\item un élément $e_2$ pour calculer la valeur de retour de \verbtt{g},
qui dépend de la valeur de $e_1$
(utilisation de la spécification de $g$),
\item et enfin, un élément $e_3$ qui représente la seconde sortie de \verbtt{g}~:
\verbtt{G.a} qui dépend du paramètre \verbtt{a} et donc de $e_1$
et de des éléments $\{ e_G \}$
correspondant à
la valeur de $G$ avant l'appel
(selon la spécification de $g$).
\end{itemize}
\end{tabular}
\end{exemple}
On note que, contrairement à ce qui était fait dans la version précédente,
on ne crée par d'élément pour l'entrée implicite $G$ de $g$ dans $f$.
Cela permet d'améliorer la précision des dépendances lorsque
l'ajout d'un tel noeud conduisait au regroupement de plusieurs données.
Ainsi, dans l'exemple précédent, on ne crée pas d'élément pour
représenter la valeur de $G$ avant l'appel, même si l'élément $e_3$ en dépend,
et on conserve donc l'information que $G.b$ ne dépend que de l'affectation
précédent l'appel.
\section{Entrées/sorties d'une fonction}\label{sec-fct-inout}
Pour relier un appel de fonction au PDG de la fonction appelée,
il faut ajouter des éléments représentant ses entrées/sorties,
c'est-à-dire~:
\begin{itemize}
\item un élément correspondant au point de contrôle d'entrée
dans la fonction,
\item deux éléments pour chaque paramètre (cf. \S\ref{sec-decl-param}),
\item un élément pour les entrées implicites (cf. \S\ref{sec-impl-in}),
\item un élément pour la sortie de la fonction si celle-ci retourne
quelque chose.
\end{itemize}
On note que, contrairement à ce qui était fait dans la version précédente,
on ne crée par d'élément pour les sorties implicites de la fonction.
Cela permet d'améliorer la précision des dépendances lorsque
l'ajout d'un tel noeud conduisait au regroupement de plusieurs données.
C'est par exemple le cas lorsqu'une fonction calcule $G.a$,
puis $G.a.x$ car un élément de sortie regrouperait les deux alors que
si par la suite on s'intéresse juste à $G.a.x$ à la sortie de la fonction,
le fait de ne pas avoir créé cet élément permet de retrouver l'information plus
précise.
\subsection{Entrées implicites}\label{sec-impl-in}
Au cours du calcul du PDG, on mémorise l'utilisation des données
qui ne sont pas préalablement définies.
Cela permet par la suite que créer des éléments pour ces entrées dites
implicites. On ne crée pas d'élément pour les variables locales non
initialisées, mais un message d'avertissement est émis.
Il est possible que ce soit une fausse alerte dans le cas où l'initialisation
est faite dans une branche dont la condition est forcement vrai à chaque
exécution où l'on passe par la suite par l'utilisation.
Diverses stratégies de regroupement de ces entrées peuvent être utilisées.
A ce jour, l'outil construit tous les éléments lui permettant d'avoir une
meilleure précision. C'est-à-dire que deux éléments peuvent représenter les
données qui ont une intersection.
\subsection{Déclaration des paramètres formels}\label{sec-decl-param}
En plus de l'élément représentant la valeur des paramètres,
on crée un second élément qui représente sa déclaration,
le premier dépendant du second.
Cette représentation peut permettre d'avoir une meilleure précision
dans le cas où certains calcul ne dépendent pas de la valeur du
paramètre, mais uniquement de sa déclaration.
\begin{exemple}
\begin{tabular}{m{5cm} m{\linewidth - 6cm}}
\begin{verbatim}
int g (int a) {
G = 2 * a;
a = calcul_a ();
return a;
}
int f (void) {
int x = calcul_x ();
return g (x);
}
\end{verbatim}
&
On voit que la valeur de retour de \verbtt{g} ne nécessite pas la valeur initiale
de \verbtt{a}, mais seulement sa déclaration. La valeur de retour de \verbtt{f}
ne dépend donc pas de l'appel à \verbtt{calcul\_x}.
\end{tabular}
\end{exemple}
Ce point n'est pas encore implémenté dans la version actuelle,
car dans des cas plus complexe, il est délicat de savoir ce qu'il faut
garder dans la fonction appelante. Le plus simple serait sans doute
de transformer le paramètre formel en une variable locale,
mais le filtrage permet à l'heure actuelle de garder ou d'effacer des
éléments existants, mais pas d'effectuer des transformations de code...
\section{Fonctions à nombre d'arguments variable}
Pour l'instant, on ne calcule pas le PDG des fonctions à nombre
d'arguments variable, c'est-à-dire que pour le reste de l'application,
tout se passe comme si on n'avait pas le code source de ces fonctions.\\
En revanche, les appels à de telles fonctions sont gérées de manière semblable à
ce qui est fait pour les autres appels, c'est-à-dire~:
\begin{itemize}
\item création d'un noeud d'entrée pour chaque argument d'appel,
(il y en a donc éventuellement plus que que paramètres formels dans le
déclaration de la fonction appelée)
\item utilisation des informations {\it from} pour créer les éventuelles
entrées implicites, les sorties, et les liens de dépendance.
\end{itemize}
\section{Exemple}
\begin{exemple}
\lstinputlisting[language=c]{exple-call.c}
\end{exemple}
Graphe de la fonction \verbtt{f}: \\
\includegraphics[width=0.6\textwidth]{call-f}
\\
\clearpage
Graphe de la fonction \verbtt{g}: \\
\includegraphics[width=1\textwidth]{call-g}
\\
Les graphes sont ceux qui sont effectivement produits par l'outil.
doc/pdg/conclusion.tex 0 → 100644
+ 22
− 0
View file @ a1ace968
\chapter{Conclusion}
La version actuelle de ce greffon semble fonctionner.
Elle est utilisée par les greffons {\sc Security}, {\sc Sparecode} et
{\sc Slicing}. Ces résultats peuvent également être visualisés
graphiquement en utilisant la fonction d'exportation
au format {\tt .dot}.\\
D'autres information relatives au développement peuvent être trouvées dans la documentation du code dont un point d'entrée
est~:
\centerline{\tt doc/code/pdg/index.html}
\section{Limitations}
Les fonctions ayant un nombre d'arguments variable
ne sont pas traitées (mais les appels à de telles fonctions sont gérés).
Par ailleurs, les calculs se basant sur l'analyse de valeur,
et sur le calcul des dépendances fonctionnelles (\from)
il hérite des limitations de ces modules.
doc/pdg/ctrl-dpds.fig 0 → 100644
+ 106
− 0
View file @ a1ace968
#FIG 3.2
Portrait
Center
Metric
A4
100.00
Single
-2
1200 2
0 32 #ffffff
6 4410 2610 5355 3195
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
4417 2645 5314 2645 5314 3165 4417 3165 4417 2645
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
4417 2645 5314 2645 5314 3165 4417 3165 4417 2645
4 1 0 0 0 16 17 0.0000 6 180 810 4866 2976 START\001
-6
6 5715 6210 6120 6795
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
5728 6236 6082 6236 6082 6755 5728 6755 5728 6236
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
5728 6236 6082 6236 6082 6755 5728 6755 5728 6236
4 1 0 0 0 16 17 0.0000 6 180 165 5905 6566 B\001
-6
6 7470 4860 7965 5445
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
7488 4889 7960 4889 7960 5409 7488 5409 7488 4889
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
7488 4889 7960 4889 7960 5409 7488 5409 7488 4889
4 1 0 0 0 16 17 0.0000 6 180 300 7724 5220 S2\001
-6
6 5715 4860 6120 5445
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
5740 4889 6094 4889 6094 5409 5740 5409 5740 4889
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
5740 4889 6094 4889 6094 5409 5740 5409 5740 4889
4 1 0 0 0 16 17 0.0000 6 180 150 5917 5220 Z\001
-6
6 4725 5715 5220 6255
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
4748 5716 5220 5716 5220 6236 4748 6236 4748 5716
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
4748 5716 5220 5716 5220 6236 4748 6236 4748 5716
4 1 0 0 0 16 17 0.0000 6 180 285 4984 6047 Z1\001
-6
6 6435 5715 6975 6255
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
6472 5716 6968 5716 6968 6236 6472 6236 6472 5716
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
6472 5716 6968 5716 6968 6236 6472 6236 6472 5716
4 1 0 0 0 16 17 0.0000 6 180 285 6720 6047 Z2\001
-6
6 4455 7155 5220 7740
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
4464 7181 5196 7181 5196 7700 4464 7700 4464 7181
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
4464 7181 5196 7181 5196 7700 4464 7700 4464 7181
4 1 0 0 0 16 17 0.0000 6 180 675 4830 7511 STOP\001
-6
6 6480 3375 6885 3960
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
6519 3401 6874 3401 6874 3921 6519 3921 6519 3401
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
6519 3401 6874 3401 6874 3921 6519 3921 6519 3401
4 1 0 0 0 16 17 0.0000 6 180 165 6696 3732 A\001
-6
6 4725 4185 5220 4725
2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5
4745 4204 5194 4204 5194 4724 4745 4724 4745 4204
2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5
4745 4204 5194 4204 5194 4724 4745 4724 4745 4204
4 1 0 0 0 16 17 0.0000 6 180 300 4970 4535 S1\001
-6
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
5310 2925 6345 2925 6705 3420
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
4500 3150 4275 5445 4680 7200
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
6525 3600 5175 3600 4950 4185
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
6885 3600 7245 3600 7650 4905
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
5175 4455 5625 4455 5895 4905
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
5760 5175 5310 5175 4950 5715
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
6075 5175 6480 5175 6750 5715
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
4950 6210 4995 6390 5715 6615
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
6750 6210 6705 6390 6075 6615
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
7650 5400 7650 6300 5175 7425
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
2 1 1.00 60.00 120.00
5850 6750 5850 6975 5175 7290
doc/pdg/ctrl.tex 0 → 100644
+ 747
− 0
View file @ a1ace968
This diff is collapsed.
doc/pdg/data.tex 0 → 100644
+ 138
− 0
View file @ a1ace968
\chapter{Dépendances liées aux données}
Le calcul de dépendances de données et d'adresse consiste principalement
à retrouver les éléments de flot correspondant aux données utilisées dans les
expressions.
Mais comme les données peuvent être incluses les unes dans les
autres, il ne suffit pas de retrouver les éléments de flot qui calculent
exactement ces données, mais aussi ceux qui ont une intersection possible.
Par exemple, dans la séquence~:\\
\centerline{\verbtt{d = d0; x = d.a;}}
il faut être capable de voir que \verbtt{x} dépend de \verbtt{d0}.
Autre exemple~: dans la séquence~:\\
\centerline{\verbtt{d0.a = a; d0.b = b; d = d0;}}
il faut voir que \verbtt{d} dépend éventuellement de la valeur initiale de \verbtt{d0}
(si \verbtt{d0} contient d'autres champs que \verbtt{.a} et \verbtt{.b}), mais aussi
de \verbtt{a}, et de \verbtt{b}.\\
\section{Recherche arrière}
Le premier calcul mis en {\oe}uvre procédait par recherche en arrière
des éléments de la table ayant une intersection avec les données présentes en
partie droite de l'instruction. Mais cette recherche était compliquée en cas de
dépendances partielles comme dans le second exemple ci-dessus. Cette solution a
donc été abandonnée.
\section{Propagation avant d'un état}\label{sec-propagation-etat}
La méthode finalement choisie pour calculer ces dépendances
consiste à propager en avant, par une analyse du type flot de données,
un \indexdef{état des données}
qui contient pour chaque donnée, une liste de liens vers les éléments
du graphe qui ont permis de déterminer sa valeur en ce point.
Cet état doit avoir les propriétés suivantes~:
\begin{itemize}
\item on veut pouvoir associer un nouveau noeud à une donnée
en précisant s'il faut faire l'union avec l'ensemble précédemment stocké.
Par exemple~;
\begin{itemize}
\item pour l'instruction \verbtt{x = 3;} on construit un nouvel élément
dans le PDG, et on mémorise dans l'état que \verbtt{x} est maintenant associé
à cet élément. L'ancienne association est perdue.
\item pour l'instruction \verbtt{*p = 3;} si \verbtt{p} peut pointer sur \verbtt{x},
il faut mémoriser que \verbtt{x} peut être défini par l'élément du PDG
correspondant, mais comme ce n'est pas sûr, il faut faire l'union avec
ce qui était précédemment stocké pour \verbtt{x}.
\end{itemize}
\item lorsque l'on demande l'ensemble associé à une donnée,
le résultat doit contenir au moins ce qu'on a stocké
(il peut contenir plus d'élément en cas de perte de précision),
\item la consultation ne doit pas modifier l'état,
\item il faut savoir faire l'union de deux états.
\end{itemize}
La structure de donnée du module \verbtt{Lmap} de \ppc correspond à ces critères,
et peut donc être utilisée pour ce calcul.\\
\section{Propagation arrière d'un état}
Une autre solution aurait pu être de propager en arrière
un état contenant les utilisations
de variables, et mettre à jour le graphe en rencontrant la définition.
Le coût de ce calcul semble être le même que le précèdent,
mais la propagation avant nous permet d'avoir, à chaque point de programme,
un état donnant la correspondance entre une donnée et les éléments du graphe,
même si cette donnée n'est pas utilisée à ce point.
Cette information nous permet par la suite de définir des critères
de \slicing moins restrictifs.
\section{Traitement de l'affectation}
Le principe de l'algorithme du traitement d'une affectation
\verbtt{lval = exp;} est donc le suivant~:
\begin{itemize}
\item recherche des données $\{d_v\}$
utilisées dans \verbtt{exp} à l'aide des résultats de l'analyse d'alias préalable,
\item calcul de {\it dpdv},
c'est-à-dire l'union des ensembles associées à ces données $d_v$ dans l'état,
\item recherche des données $\{d_a\}$
utilisées pour calculer l'adresse de {\it lval},
\item calcul de {\it dpda}
c'est-à-dire l'union des ensembles associées à ces données $d_a$ dans l'état,
\item recherche de l'élément $e$
correspondant à cette instruction dans le graphe,
et création de cet élément s'il n'existe pas,
\item ajout des dépendances {\it dpdv} et {\it dpda} à $e$,
\item recherche des données $\{d_x\}$
potentiellement modifiées par cette affectation,
\item calcul du nouvel état (après l'instruction)
en ajoutant dans l'ancien état un lien entre les $\{d_x\}$ et $e$.
\end{itemize}
\section{Déclarations}
Les déclarations de variable doivent être traitées séparément
des valeurs, car on peut parfois dépendre de l'adresse d'une variable
sans dépendre de ce qu'elle contient.
C'est par exemple le cas lorsque la variable apparaît à gauche
d'une affectation (\verbtt{x = 3;})
ou encore quand on n'utilise que son adresse (\verbtt{p = \&x;}).
On garde donc une table qui permet de retrouver les éléments
du graphe de dépendances qui correspondent aux déclarations.
\section{Calcul de conditions}
Les noeuds du graphe de dépendances représentant
les calculs de condition des \verbtt{if} ou \verbtt{switch}
ont des dépendances de donnée sur les données utilisées.
\section{Dépendances de donnée dans les boucles}
Pour les boucles {\it explicites}, il suffirait d'effectuer deux tours
de la boucle pour obtenir toutes les dépendances de donnée car le premier
capture les dépendances avec les données provenant d'avant la boucle,
ou interne à un tour, et le second capture les dépendances entre un tour et le
suivant.
Mais comme les boucles peuvent être introduites par la présence de sauts
quelconques,
le plus simple est dans un premier temps d'itérer jusqu'à obtenir un point fixe
sur l'état des données. Il faut noter que les noeuds ne sont créés que lors de la
première itération, les suivantes n'ajoutant que de nouvelles dépendances entre
ces noeuds. Le nombre de noeuds étant fini (de l'ordre de grandeur du nombre
d'instruction de la fonction), l'atteignabilité du point fixe est
garantie.
\section{Appels de fonction}
Le traitement des appels de fonction est présenté
dans le chapitre \ref{sec-intro-call}
doc/pdg/ex-goto.fig 0 → 100644
+ 113
− 0
View file @ a1ace968
#FIG 3.2
Landscape
Center
Metric
A4
100.00
Single
-2
1200 2
6 3195 2160 8010 5130
6 3195 2385 4950 4950
6 3195 2385 3780 2790
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 2565 270 180 3465 2565 3735 2745
4 1 0 50 -1 0 12 0.0000 4 150 390 3465 2610 entry\001
-6
6 3195 3105 3780 3510
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 3285 270 180 3465 3285 3735 3465
4 1 0 50 -1 0 12 0.0000 4 135 90 3465 3330 2\001
-6
6 3195 3825 3780 4230
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 4005 270 180 3465 4005 3735 4185
4 1 0 50 -1 0 12 0.0000 4 135 90 3465 4050 5\001
-6
6 4365 3105 4950 3510
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 4635 3285 270 180 4635 3285 4905 3465
4 1 0 50 -1 0 12 0.0000 4 135 90 4635 3330 3\001
-6
6 4365 3825 4950 4230
6 4590 3915 4680 4050
4 1 0 50 -1 0 12 0.0000 4 135 90 4635 4050 4\001
-6
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 4635 4005 270 180 4635 4005 4905 4185
-6
6 3195 4545 3780 4950
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 4725 270 180 3465 4725 3735 4905
4 1 0 50 -1 0 12 0.0000 4 135 90 3465 4770 6\001
-6
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
3465 2745 3465 3105
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
3465 3465 3465 3825
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
3465 4185 3465 4545
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
4635 3465 4635 3825
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
3735 3285 4365 3285
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
4545 4185 3735 4725
-6
6 5715 2385 7470 4950
6 5715 2385 6300 2790
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 2565 270 180 5985 2565 6255 2745
4 1 0 50 -1 0 12 0.0000 4 150 390 5985 2610 entry\001
-6
6 5715 3105 6300 3510
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 3285 270 180 5985 3285 6255 3465
4 1 0 50 -1 0 12 0.0000 4 135 90 5985 3330 2\001
-6
6 5715 3825 6300 4230
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 4005 270 180 5985 4005 6255 4185
4 1 0 50 -1 0 12 0.0000 4 135 90 5985 4050 5\001
-6
6 6885 3105 7470 3510
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 7155 3285 270 180 7155 3285 7425 3465
4 1 0 50 -1 0 12 0.0000 4 135 90 7155 3330 3\001
-6
6 5715 4545 6300 4950
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 4725 270 180 5985 4725 6255 4905
4 1 0 50 -1 0 12 0.0000 4 135 90 5985 4770 6\001
-6
6 6885 3825 7470 4230
6 7110 3915 7200 4050
4 1 0 50 -1 0 12 0.0000 4 135 90 7155 4050 4\001
-6
1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 7155 4005 270 180 7155 4005 7425 4185
-6
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
5985 2745 5985 3105
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
5985 3465 5985 3825
2 1 1 2 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
0 0 1.00 60.00 120.00
5985 4185 5985 4545
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
6255 3285 6885 3285
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
6255 3285 7155 3825
-6
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
2 1 1.00 60.00 120.00
7515 4860 7965 4860
2 1 1 2 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
0 0 1.00 60.00 120.00
7515 5085 7965 5085
2 1 1 2 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
0 0 1.00 60.00 120.00
6975 3375 6255 4725
4 1 0 50 -1 2 12 0.0000 4 135 375 4365 2295 CFG\001
4 1 0 50 -1 2 12 0.0000 4 135 390 6885 2295 PDG\001
4 1 0 50 -1 2 10 0.0000 4 150 675 7065 4860 CDG edge\001
4 1 0 50 -1 2 10 0.0000 4 150 690 7065 5085 DDG edge\001
-6
doc/pdg/goto.fig 0 → 100644
+ 35
− 0
View file @ a1ace968
#FIG 3.2
Portrait
Center
Metric
A4
100.000000
Single
-2
1200 2
0 32 #ffffff
6 0 0 0 0
1 1 0 1 32 32 0 0 20 0.000000 1 0.0 5722 1299 767 472 0 0 0 0
1 1 0 1 0 -1 0 0 -1 0.000000 1 0.0 5722 1299 767 472 0 0 0 0
4 1 0 0 0 16 22.762205 0.0 6 0.0 0.0 5722 1393 G\001
-6
6 0 0 0 0
1 1 0 1 32 32 0 0 20 0.000000 1 0.0 5090 3622 767 472 0 0 0 0
1 1 0 1 0 -1 0 0 -1 0.000000 1 0.0 5090 3622 767 472 0 0 0 0
4 1 0 0 0 16 22.762205 0.0 6 0.0 0.0 5090 3716 S\001
-6
6 0 0 0 0
2 1 0 1 0 0 0 0 -1 0.000000 0 0 0 1 0 4
0 0 3.149606 236.220472 236.220472
6490 1299 6962 1299 6962 5756 6490 5756
-6
6 0 0 0 0
1 1 0 1 32 32 0 0 20 0.000000 1 0.0 5722 5756 767 472 0 0 0 0
1 1 0 1 0 -1 0 0 -1 0.000000 1 0.0 5722 5756 767 472 0 0 0 0
4 1 0 0 0 16 22.762205 0.0 6 0.0 0.0 5722 5851 L\001
-6
6 0 0 0 0
2 1 1 1 0 0 0 0 -1 12.598425 0 0 0 1 0 4
0 0 3.149606 236.220472 377.952756
5722 1771 5722 2460 5090 2460 5090 3149
-6
doc/pdg/impact.tex 0 → 100644
+ 205
− 0
View file @ a1ace968
\chapter{Aide à l'analyse d'impact}\label{sec-impact}
Le document \cite{baudinImpact} spécifie un outil d'aide à l'analyse d'impact
après avoir analysé les besoins dans ce domaine.
L'exploitation du graphe de dépendances est présenté comme étant
un composant important de cet outil.
Nous reprenons ici les éléments de spécification
décrits dans le paragraphe 5.3 de ce document,
auxquels nous ajoutons quelques nouveaux critères.\\
\section{Définition d'ensembles}\label{sec-ensembles}\label{sec-defR}
\newcommand{\remitem}[1]{\begin{itemize}\item #1 \end{itemize}}
\newcommand{\warnitem}[1]{\begin{itemize}\item[$\blacktriangle$] #1
\end{itemize}}
\newcommand{\question}[1]{\begin{itemize}\item[{\bf ?}] #1 \end{itemize}}
\newcommand{\smilitem}[1]{\begin{itemize}\item[$\smiley$] #1 \end{itemize}}
\newcommand{\frownitem}[1]{\begin{itemize}\item[$\frownie$] #1 \end{itemize}}
Il s'agit de définir des sous-ensembles d'instructions
répondant à différents critères.
Donnons tout d'abord quelques notations :
\begin{itemize}
\item S : un ensemble d'instructions,
\item L : un point de programme,
\item V : une zone mémoire (le V se réfère à {\bf V}ariable,
mais il peut s'agir d'une donnée quelconque comme un champ de structure ou
un élément de tableau),
\end{itemize}
Les ensembles sont tous relatifs à un point de programme $L$,
et peuvent se classer en deux catégories~:
\begin{itemize}
\item ceux qui contiennent des instructions situées {\bf avant} $L$~:
ils portent un indice 0,
\item et ceux qui contiennent des instructions situées {\bf après} $L$~:
ils portent un indice 1.\\
\end{itemize}
\begin{description}
\item[$R_0(S,L)$] : sous-ensemble d'instructions de S depuis lesquelles
L est accessible.
\warnitem{mais L ne postdomine pas forcement toutes les instructions de cet ensemble.}
\item[$R_{1}(S,L)$] : sous-ensemble d'instructions de S
qui sont (éventuellement) accessibles depuis L.
\item[$R_{L0}(S,L)$] : accessibilité à un point du code.
\remitem{il s'agit du sous-ensemble des instructions de $R_0(S,L)$
qui conditionnent le passage en L,
c'est-à-dire les instructions de branchement
et les dépendances de ces conditions de branchement.
}
%\item[$R_{L1}(S,L)$] : ?
\item[$R_{V0}(S,L,V)$] : contenu d'une zone mémoire en un point du code.
\remitem{il s'agit du critère traditionnel de \slicing,
c'est-à-dire que cet ensemble contient les instructions de $S$ qui
ont une influence sur la valeur de $V$ en $L$.
}
\item[$R_{V1}(S,L,V)$] : utilisation d'une zone mémoire.
\remitem{il s'agit du sous-ensemble des instructions de $R_{1}(S,L)$
influencées par la valeur qu'à la zone mémoire $V$ a en $L$.}
\item[$R_{DV0}(S,L,V)$] : définition de la valeur d'une variable à un point de
programme.
\remitem{il s'agit de l'ensemble des instructions qui {\bf définissent}
tout ou partie de la valeur de $V$ en $L$. Ces instructions
sont donc nécessairement des affectations ou des appels de fonction.
On note que~: $R_{DV0}(S,L,V) \subseteq R_{V0}(S,L,V)$
}
\warnitem{
Il serait probablement utile d'avoir un élément spécial
qui indique qu'il existe
un ou plusieurs chemin menant à $L$ pour le(s)quel(s)
$V$ n'est pas entièrement défini.
}
\item[$R_{DV1}(S,L,V)$] : modification de la valeur d'une variable.
\remitem{il s'agit de trouver les instructions $I_i$ accessibles depuis L
qui modifient la valeur de $V$,
et telles qu'il existe un chemin entre $L$ et $I_i$
le long duquel $V$ n'est pas modifiée.
Cela signifie que ces instructions sont les premières à modifier la valeur
de $V$ sur les chemins partant de $L$.}
\remitem{Il n'est pas sûr que cet ensemble soit très utile.
L'ensemble $R_{P1}(S,L,V)$ ci-dessous en sans doute plus intéressant.
}
\item[$R_{P0}(S,L,V)$] :
portée arrière de la valeur d'une variable à un point de programme.
\remitem{il s'agit d'un sous-ensemble de $R_{L0}(S,L)$
contenant les instructions $I_i$ pour lesquelles la valeur de $V$
n'a été modifiée sur aucun chemin entre le point qui précède $I_i$ et $L$.
C'est-à-dire que la valeur de $V$ en $L$ est la même qu'avant chacune de ces
instructions, et qu'elle n'est pas modifiée entre les deux.
}
\item[$R_{P1}(S,L,V)$] :
portée de la valeur d'une variable à un point de programme~.
\remitem{il s'agit d'un sous-ensemble de $R_{1}(S,L)$
contenant les instructions $I_i$ pour lesquelles la valeur de $V$
n'a été modifiée sur aucun chemin entre $L$ et le point de programme
qui précède $I_i$.
}
\item[$R_{PV0}(S,L,V)$] : utilisation arrière d'une zone mémoire dans sa portée.
\remitem{il s'agit du sous-ensemble des instructions $R_{P0}(S,L,V)$
qui sont influencées, directement ou non, par $V$.
}
\item[$R_{PV1}(S,L,V)$] : utilisation d'une zone mémoire dans sa portée.
\remitem{il s'agit du sous-ensemble
des instructions influencées, directement ou non,
par la valeur de $V$ en $L$
qui sont dans la portée de cette valeur.
On a donc : $R_{PV1}(S,L,V) = R_{V1}(S,L,V) \cap R_{P1}(S,L,V)$
}
\end{description}
\begin{exemple1}
On montre ici différents ensembles relatifs au point $L$
et à la variable $v$~:
\end{exemple1}
\begin{center}
\begin{scriptsize}
\begin{tabular}{|l||c|c|c|c|c|c||c|c|c|c|c| }
\hline
S & $R_{0}$ & $R_{L0}$ & $R_{V0}$ & $R_{DV0}$ & $R_{P0}$ & $R_{VP0}$
& $R_{1}$ & $R_{V1}$ & $R_{DV1}$ & $R_{P1}$ & $R_{VP1}$ \\
\hline
\verb!! & & & & & & & & & & & \\
\verb!v = a; ! & X & X & X & X & & & & & & & \\
\verb!x = b; ! & X & & X & & & & & & & & \\
\verb!z = c; ! & X & & & & & & & & & & \\
\verb!if (c1>v) { ! & X & X & X & & & & & & & & \\
\verb! z++; ! & & & & & & & & & & & \\
\verb! } ! & & & & & & & & & & & \\
\verb!else { ! & & & & & & & & & & & \\
\verb! if (c2) ! & X & X & X & & & & & & & & \\
\verb! v += x; ! & X & X & X & X & & & & & & & \\
\verb! if (c3) { ! & X & X & X & & X & & & & & & \\
\verb! z += v; ! & X & X & & & X & X & & & & & \\
\hline
{\tt\bf L:}
\verb! y = v; ! & & & & & & & X & X & & X & X \\
\verb! z++; ! & & & & & & & X & & & X & \\
\verb! v++; ! & & & & & & & X & X & & X & X \\
\verb! } ! & & & & & & & & & & & \\
\verb! z += 2*y; ! & & & & & & & X & X & & & \\
\verb! } ! & & & & & & & & & & & \\
\verb!z += x; ! & & & & & & & X & X & & & \\
\verb!v = 0; ! & & & & & & & & & X & & \\
\verb!! & & & & & & & & & & & \\
\hline
\end{tabular}\end{scriptsize}\end{center}
\begin{exemple2}
\end{exemple2}
La construction des ensembles ci-dessus exploite le CFG (le flot de contrôle)
et le PDG (les dépendances).\\
La construction des ensembles ci-dessous exploite en plus la sémantique du
programme car elle utilise une contrainte $C(...v_i...)$ portant
sur les valeurs des données en $L$~:
\begin{description}
\item[$R_{C0}(S,L,C(...v_i...))$] :
accessibilité contrainte à un point.
\remitem{il s'agit de déterminer l'ensemble des instructions
qui, si elles sont présentes, rendent fausse la contrainte $C$ au point $L$.
En fait, il s'agit de déplacer $C$ pour essayer de couper des branches.
La condition de branchement sera alors éventuellement
remplacée par un \verbtt{assert}.
}
\smilitem{Dans la séquence \verbtt{int x = 0; x=x-1; L:} pour laquelle
on a une contrainte $x \ge 0$, il ne s'agit pas de supprimer l'instruction
\verbtt{x=x-1;} mais bien de dire que cette branche est impossible...}
\item[$R_{C1}(S,L,C(...v_i...))$] : accessibilité contrainte depuis un point.
\remitem{il s'agit de déterminer le sous-ensemble des instructions de
$R_{1}(S,L)$ qui ne peuvent pas être atteintes si l'état en L est tel que
$C$ est satisfaite.\\
On notera que certaines instructions n'appartenant ni à $R_{L0}$, ni à $R_{1}$
peuvent également ne pas être atteintes du fait de la contrainte.\\
}
\end{description}
\section{Exploitation du graphe pour le calcul d'ensembles}
La plupart des ensembles définis en \ref{sec-ensembles}
peuvent être calculés simplement en exploitant le flot de contrôle
et les fonction du graphe de dépendances présentées en \$\ref{sec-find}.
doc/pdg/intro.tex 0 → 100644
+ 246
− 0
View file @ a1ace968
\chapter{Introduction}
\section{Objectif}
L'objectif initial a été de réaliser un module de \slicing
dans le cadre d'un outil généraliste d'analyse de programme (voir
\cite{ppcSlicing}).
Or, la plupart des réductions à effectuer se basent sur l'analyse des
dépendances entre les données du programme.
En effet, si l'utilisateur demande la sélection
d'une instruction \verb!return x;!, il va falloir retrouver ce qui permet de
calculer cette valeur de \verbtt{x} dans les instructions qui précèdent.\\
Il s'agit donc de calculer le \indexdef{graphe de dépendances} d'une fonction
(appelé \indexdef{PDG}~: {\it Program Dependence Graph} dans la littérature)
c'est-à-dire de représenter finement les liens de
dépendances entre les différentes instructions qui la composent.
Le résultat ce calcul est un graphe dans lequel les sommets
représentent les instructions,
éventuellement décomposées en plusieurs noeuds représentant
le calcul d'informations élémentaires.\\
Dans le cadre de l'outil de \slicing,
l'intérêt de ce calcul préalable est de pouvoir
travailler en plusieurs passes lors de l'application des
requêtes de réduction sans avoir à
refaire ce calcul qui peut être lourd (alias, dépendances partielles, etc). En
effet, même si l'on souhaite à terme calculer des réductions qui utilisent
davantage la sémantique du programme, les réductions à l'aide des dépendances
peuvent simplifier le problème.\\
Par la suite, il a été jugé intéressant de considérer ce calcul
comme un module à part entière car il peut avoir d'autres
utilités comme étudier la
propagation du flot d'information pour des analyses de sécurité, par exemple.
\section{Spécifications du PDG}\label{sec-flot}
Le PDG que l'on souhaite calculer comporte plusieurs types de dépendances~:
\subsection{Dépendances sur la valeur des données}
Les \indextxtdef{dépendances sur la valeur}{dépendance!valeur}
d'une donnée sont les plus intuitives.
\begin{exemple}
\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}}
\begin{clisting}
x = a + b;
\end{clisting}
&
Ici, \verbtt{x} dépend de
\verbtt{a} et \verbtt{b} car la valeur de \verbtt{x} après cette instruction dépend
des valeurs de \verbtt{a} et \verbtt{b} avant.
\end{tabular}
\end{exemple}
La question se pose néanmoins de définir la granularité à laquelle
on s'intéresse aux données.
L'utilisation d'autres analyses et structures de données de \ppc
conduit à choisir la même précision
(pour plus de détail, voir par exemple l'analyse de valeurs de \ppc).
\subsection{Dépendances de calcul d'adresse}
Pour les affectations, la valeur qui est écrite en mémoire dépend de la partie
droite, mais le choix de l'adresse à laquelle on l'écrit peut également dépendre
de variables qui apparaissent dans la partie gauche.
\begin{exemple}
\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}}
\begin{clisting}
*p = x;
\end{clisting}
&
Ici, la valeur de la donnée modifiée dépend de \verbtt{x},
mais le choix de la case dans laquelle on la range dépend de \verbtt{p}.
En effet, si $p$ pointe sur $a$ ou $b$, c'est soit \verbtt{a} soit \verbtt{b} qui
va être modifié.
\end{tabular}
\end{exemple}
On parle alors de \indextxtdef{dépendances sur l'adresse}{dépendance!adresse}.
\subsection{Dépendances de contrôle}
Lorsqu'une donnée peut-être modifiée par plusieurs chemins d'exécution,
elle dépend des conditions qui permettent de choisir le chemin.
\begin{exemple}
\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}}
\begin{clisting}
if (c)
x = a;
L :
\end{clisting}
&
La valeur de \verbtt{x} en \verbtt{L} dépend de \verbtt{a}, mais aussi de \verbtt{c}.\\
\end{tabular}
\end{exemple}
Il s'agit d'une \indextxtdef{dépendance de contrôle}{dépendance!contrôle}.
\subsection{Dépendances sur les déclarations}
Lorsque des variables sont utilisées dans une instruction, celle-ci dépend de
leurs déclarations, car si on veut la compiler, il faut que les variables
existent.
Les déclarations des variables lues (partie droite d'une affectation) sont
considérées comme participant au calcul de la valeur.
Les déclarations des
variables utilisées pour déterminer la case affectée (partie gauche d'une
affectation) sont considérées comme des dépendances sur l'adresse.
\begin{exemple}
\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}}
\begin{clisting}
/* 1 */ int x;
/* 2 */ int y;
...
/* i */ x = 3;
/* j */ y = 4;
...
/* n */ x = y;
\end{clisting}
&
L'instruction (n) a une dépendance d'adresse sur la déclaration de x (1),
et des dépendances de donnée sur l'affectation de y (j)
et sa déclaration (2). Dans ce cas, on aurait pu se passer de de cette dernière
dépendance car (j) dépend déjà de (2), mais ce n'est pas forcement le cas
en présence d'alias.
\end{tabular}
\end{exemple}
\subsection{Résumé}
On voit donc qu'on distingue trois types de dépendances~:
\begin{itemize}
\item les calculs de valeurs,
\item les calculs d'adresses,
\item le contrôle.
\end{itemize}
\section{État de l'art}\label{sec-lart}
Voyons tout d'abord ce que dit la littérature sur ce sujet
afin de voir les solutions qui peuvent répondre à notre besoin,
et les points à modifier.
\subsection{Origine}
Les graphes de dépendances ont principalement été étudiés dans le cadre du
\slicing{}, mais ils sont aussi utilisés dans les travaux sur la compilation.
\subsection{Graphes de dépendances}
\cite{Ottenstein84}, puis \cite{Ferrante87}
introduisent la notion de PDG ({\it Program Dependence Graph}).
Un tel graphe est utilisé pour représenter les différentes dépendances
entre les instructions d'un programme.
Ils l'exploitent pour calculer les instructions
qui influencent la valeur des variables en un point.\\
Cette représentation, initialement intraprocédurale, a été étendue
à l'analyse interprocédurale dans \cite{horwitz88interprocedural} où elle
porte le nom de SDG ({\it System Dependance Graph}).
Elle est maintenant, à quelques variantes près,
quasiment universellement utilisée.
\subsection{Exploitation du graphe}
Lorsque l'on utilise le graphe de dépendance pour faire du \slicing,
le calcul se résume à un problème d'accessibilité à un noeud car comme le dit
Susan Horwitz~:
\begin{definition}{slicing selon \cite{horwitz88interprocedural}}
A slice of a program with respect to program point p and variable x
consists of a set of statements of the program that might affect
the value of x at p.
\end{definition}
c'est-à-dire qu'il faut garder toutes les instructions correspondant à des
noeuds du graphe pour lesquels il existe un chemin vers le noeud représentant le
calcul de {\tt x} en {\tt p}.
Mais le problème est que ce noeud n'existe que si {\tt x} est défini
par l'instruction située en {\tt p}.
Nous verrons que cette limitation peut être levée si l'on garde
(ou recalcule) les structures de données utilisées
lors de la construction du graphe.\\
Le traitement des appels de fonction est souvent compliqué par le fait qu'il
est également ramené à un problème d'accessibilité dans un graphe qui,
cette fois, représente toute l'application. Or, dans un tel graphe,
si on ne prend pas de précautions supplémentaires,
on parcourt des chemins impossibles qui entrent dans une fonction
par un appel, et sortent par un autre site d'appel.
Ces chemins existent en effet dans le graphe,
mais pas dans la réalité.
Comme nous nous proposons de traiter ce problème de manière modulaire,
nous devrions échapper à une partie de ce problème.
Mais nous verrons par la suite que l'utilisation d'une analyse d'alias globale
produit néanmoins quelques effets de bord indésirables.
\subsection{Programmes non structurés}
Les premiers algorithmes utilisés fonctionnent
correctement sur des programmes structurés,
mais produisent des résultats erronés en présence de \verbtt{goto}.
Le problème vient du fait que ces instructions ne modifient pas de données~:
il n'y a donc pas de dépendance de donnée~; et il n'y a pas
de dépendance de contrôle non plus car dans le CFG,
une seule branche sort du noeud pour aller vers le point de branchement.
Plusieurs personnes (\cite{Choi94}, \cite{agrawal94slicing},
\cite{harman98new}, \cite{kumar02better} entre autres)
se sont donc intéressées
aux sauts (\verbtt{goto}) qui brisaient la structure du programme.
Ce point, qui nous intéresse tout particulièrement, est présenté en détail
en \S\ref{sec-cdg}.
\subsection{Pointeurs et données structurées}
De nombreux articles s'intéressent aux traitements des données structurées,
et plus encore des pointeurs. Dans le cadre de cette étude,
nous n'avons pas exploré ces recherches étant donné que
nous nous appuyons déjà sur une analyse d'alias précise.
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\section{Plan}
Les trois chapitres suivants
exposent comment est calculé notre graphe de dépendances.
Puis, nous verrons au chapitre \ref{sec-find} comment
exploiter les informations calculées et au chapitre
\ref{sec-mark} comment associer des informations aux éléments
et les propager dans le graphe.
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
doc/pdg/macros_pdg.tex 0 → 100644
+ 130
− 0
View file @ a1ace968
%==============================================================================
\usepackage{tabularx}
\usepackage{wasysym}
\usepackage{stmaryrd}
%------------------------------------------------------------------------------
\newcommand{\setenvclass}[2]{}
\usepackage{listings}
% TODO :
\lstdefinestyle{clststyle}{}
\lstnewenvironment{clisting}
{
\setenvclass{lstlisting}{clisting}
\lstset{language=C, style=clststyle}}
{}
%-----------------------------------------------
% Commandes pour mettre des ref dans l'index :
\newcommand{\idb}[1]{\textbf{#1}}
\newcommand{\indextxt}[1]{\index{#1}{\bf #1}}
\newcommand{\indexdef}[1]{\index{#1|idb}{{\bf #1}}}
\newcommand{\indextxtdef}[2]{\index{#2|idb}{{\bf #1}}}
%-----------------------------------------------
% quelques "mots" spéciaux
\newcommand{\slicing}{{\it slicing}\xspace}
\newcommand{\slicingb}{{\it slicing\ }}
% permet de corriger les cas où \slicing est suivi d'une {
% car il semble que xspace gère mal ce cas.
\newcommand{\caml}{{\sc Ocaml}\xspace}
\newcommand{\caveat}{{\sc Caveat}\xspace}
\newcommand{\cil}{{\sc CIL}\xspace}
\newcommand{\ppc}{{\sc Frama-C}\xspace}
\newcommand{\from}{{\sc From}\xspace}
\newcommand{\mylet}{\text{\it let }}
\newcommand{\myin}{\text{\it in }}
%------------------------------------------------------------------------------
\newcommand{\verbtt}[1]{{\small{\tt{#1}}}}
%------------------------------------------------------------------------------
% Légende des figures :
\usepackage[hang,small]{caption}
\renewcommand{\captionfont}{\it}
\renewcommand{\captionlabelfont}{\it \bf \small}
%\renewcommand{\captionlabeldelim}{ : }
%-----------------------------------------------
% prend le nom du fichier
% et éventuellement un facteur d'échelle (1 par défaut)
\newcommand{\uneimage}[2][1]{
\includegraphics[width=(#1)\textwidth]{#2}
}
%--------------------------------
\newcommand{\labcenterepsfig}[3]{
\begin{center}
\begin{figure}[hbt]
\centering{
\leavevmode
\uneimage{#1}
}
\caption{\label{#3} #2}
\end{figure}
\end{center}
}
%------------------------------------------------------------------------------
\newenvironment{debutenv}[1]
{
\vspace{5mm}
\begin{footnotesize}
\setenvclass{minipage}{myminipage}
\noindent\begin{minipage}[t]{\textwidth}
\fbox{\bf #1} \hrule
\vspace{3mm}
}
{
\end{minipage}
\end{footnotesize}
}
\newenvironment{finenv}
{
\begin{footnotesize}
\setenvclass{minipage}{myminipage}
\noindent\begin{minipage}[t]{\textwidth}
}
{
\hrule
\
\end{minipage}
\end{footnotesize}
\vspace{5mm}
}
\newenvironment{monenv}[1]
{\begin{debutenv}{#1}}
{\end{debutenv}
\par
\begin{finenv}
\end{finenv}}
\newcounter{numexemple}
\newcommand{\titreexemple}{%
\stepcounter{numexemple}{Exemple \arabic{numexemple}}}
\newenvironment{exemple}
{\begin{monenv}{\titreexemple}}
{\end{monenv}}
\newenvironment{exemple1}
{\begin{debutenv}{\titreexemple}}
{\end{debutenv}}
\newenvironment{exemple2}
{\begin{finenv}}
{\end{finenv}}
\newenvironment{astuce}
{\begin{monenv}{Astuce}}
{\end{monenv}}
\newenvironment{definition}[1]
{\begin{monenv}{Definition (#1)}}
{\end{monenv}}
\newenvironment{algo}[1]
{\begin{monenv}{Algorithme (#1)}}
{\end{monenv}}
\newcounter{numrque}
\newenvironment{remarque}[1]
{\refstepcounter{numrque}{\bf Remarque \arabic{numrque}} :\label{#1}}
{}
%==============================================================================
doc/pdg/main.tex 0 → 100644
+ 27
− 0
View file @ a1ace968
\documentclass[a4paper,11pt,twoside,openright,web,lang=french]{frama-c-book}
\input{macros_pdg.tex}
%==============================================================================
\begin{document}
\coverpage{PDG --- Documentation technique}
\begin{titlepage}
\begin{flushleft}
\includegraphics[height=14mm]{../images/cealistlogo.jpg}
\end{flushleft}
\vfill
\title{Documentation du greffon PDG}{Calcul de dépendances dans un programme C}
\author{Anne Pacalet et Patrick Baudin}
\begin{tabular}{l}
CEA LIST, Laboratoire de Sûreté et Sécurité des Logiciels, Saclay, F-91191 \\
\end{tabular}
\vfill
\begin{flushleft}
\textcopyright 2007-2020 CEA LIST
\end{flushleft}
\end{titlepage}
\input{pdg.tex}
\end{document}
doc/pdg/mark.tex 0 → 100644
+ 159
− 0
View file @ a1ace968
\chapter{Marquage générique}\label{sec-mark}
\section{Objectif}
On souhaite pouvoir associer une information à certains éléments d'un PDG,
propager cette information dans les dépendances de ces éléments,
et calculer ce qu'il faut propager dans les autres PDG de l'application
pour avoir un traitement interprocédural cohérent. \\
Par exemple, l'information peut être un simple booléen qui indique si l'élément
correspondant est visible ou non. Pour qu'un élément soit visible, il faut que
toutes ses dépendances le soit aussi.
On voit dans cet exemple qu'on s'intéresse dans un premier temps à une
propagation arrière.\\
Comme un PDG est associé à une fonction, la propagation s'arrête aux entrées
de la fonction. Par ailleurs, les appels de fonction sont traités localement,
sans descendre dans la fonction appelée.
Pour gérer la propagation interprocédurale, les fonctions élémentaires de
marquage doivent fournir l'information à propager aussi bien dans les fonctions
appelées que dans les appelants.
\section{Marquage générique}
Le marquage pouvant être utilisé pour différents besoins,
les marques peuvent être définies par l'utilisateur.
Il lui suffit de définir comment en faire l'union.
On utilise deux types d'union~:
\begin{itemize}
\item l'une permet de faire une simple union de deux marques,
\item l'autre permet d'ajouter une marque à un élément de programme~:
elle calcule donc une nouvelle marque à partir de l'ancienne,
et de la marque à ajouter et fournit aussi la marque à propager dans les
dépendances.
\end{itemize}
\section{Propagation arrière}
\subsection{Marquage intraprocédural}
La propagation arrière s'effectue très simplement en suivant les dépendances,
en ajoutant la marque propagée à la marque existante,
et en s'arrêtant quand la marque à propager rendue par la fonction de marquage
est $m_{\bot}$.\\
En cours de propagation, lorsque l'on traite un élément correspondant à la
sortie d'un appel de fonction, ou à une entrée de la fonction courante,
la marque à propager ainsi que l'identifiant de l'élément sont stockés.
A l'issu du marquage, on a donc~:
\begin{itemize}
\item un ensemble de couple (entrée de la fonction, marque à propager),
\item une liste des appels de fonction, avec pour chacun un ensemble de
couples (sortie de l'appel, marque à propager).
\end{itemize}
C'est cette information qui permettra de faire la propagation interprocédurale.
\subsection{Propagation interprocédurale}
\subsubsection{Méthode automatique}
Le module de marquage permet de faire automatiquement
la propagation interprocédurale si on le souhaite.
Il est utilisé de cette façon dans la détection de code mort par exemple.\\
L'utilisateur peut, s'il le souhaite,
donner des fonctions de transformation des marques~:
\begin{itemize}
\item une qui est utilisée pour transformer les marques des entrées d'une
fonction avant la propagation dans les appelants,
\item une autre qui est utilisée pour transformer les marques des sorties
d'un appel de fonction avant propagation dans la fonction appelée.
\end{itemize}
Dans les cas les plus simples, ces fonctions ne font rien, et rendent
simplement la marque qui leur est passée.
\subsubsection{Méthode manuelle}
Dans certains cas, il est souhaitable de gérer cette propagation à la main.
C'est par exemple le cas dans le \slicing{} où une fonction source est associée
à plusieurs marquages différents.\\
Des fonctions aident néanmoins à retrouver les éléments à marquer dans les
autres fonctions à partir du résultat fourni par le marquage intraprocédural.
Ces fonctions traduisent les informations~:
\begin{itemize}
\item (entrée de la fonction, marque à propager) en un ensemble d'éléments à
marquer dans une~- ou toutes les~- fonction(s) appelante(s),
\item (appel, \{(sortie de l'appel, marque à propager)\})
en un ensemble d'éléments à marquer dans la fonction appelée.
\end{itemize}
Les éléments rendu sont les nouveaux points de départ de marquages
intraprocéduraux.
L'utilisateur peut, comme lors de la propagation automatique,
donner des fonctions de transformation des marques aux traductions.
\subsubsection{Données non définies}
Lorsque les points de départ marquage initial sont des éléments du PDG,
toutes les propagations s'effectueront a priori sur des éléments existant.
Mais ce n'est pas forcement le cas lorsqu'il s'agit de marquer les données
qui n'interviennent pas dans les calculs. Par exemple~:
\begin{exemple}
\begin{verbatim}
int X1, X2;
void f (int x) { /*@ assert X1 >= 0; */ return x + 1; }
void f2 (void) { X2 = f (2); }
void main (void) { X1 = 0; X2 = 0; f2 (); }
\end{verbatim}
Ici, si on s'intéresse à l'assertion de \verbtt{f}, il faut sélectionner
\verbtt{X1} à l'entrée de \verbtt{f}, propager cette information à travers
\verbtt{f2} pour enfin marquer l'affectation à \verbtt{X1} dans le \verbtt{main}
alors que cette donnée n'apparaît pas dans les PDG de \verbtt{f} et \verbtt{f2}.
\end{exemple}
On voit donc que dans les informations fournies et calculées
pour gérer l'interprocédural, il peut y avoir des éléments ne correspondant
pas à des noeuds de PDG.
\subsubsection{Terminaison}
La terminaison du processus dépend de la définition des marques.
C'est donc à l'utilisateur de s'assurer que celle-ci permet la stabilisation du
marquage.
\section{Propagation avant}
La propagation avant n'est pas effectuée automatiquement à l'heure actuelle.
La propagation intraprocédurale ne pose pas de problèmes particuliers,
car elle est très semblable au calcul en arrière~: il suffit simplement de
parcourir les liens de dépendance dans l'autre sens.\\
La partie interprocédurale semble un peu plus délicate,
car il n'y a aucun point de repère dans le PDG
pour identifier les endroits à partir desquels il faut propager
(hormis le noeud correspondant au \verbtt{return}
pour la propagation vers les appelants et les arguments explicites pour
la propagation dans les appels de fonction).
Des fonctions supplémentaires sont donc fournies pour~:
\begin{itemize}
\item trouver les noeuds d'entrées d'une fonction qui doivent être
sélectionnés à partir des noeuds sélectionnés dans l'appelant,
\item trouver les noeuds de sortie d'un appel de fonction
qui doivent être
sélectionnés à partir des noeuds sélectionnés dans la fonction appelée.
\end{itemize}
En cas d'utilisation intensive de ces fonctionnalités,
il serait sans doute intéressant de mémoriser les liens entre les
différents PDG (cela est également vrai pour la propagation interprocédurale
arrière...).\\
doc/pdg/pdg-call.fig 0 → 100644
+ 151
− 0
View file @ a1ace968
#FIG 3.2
Landscape
Center
Metric
A4
100.00
Single
-2
1200 2
6 7830 3330 8820 3780
2 3 0 1 0 7 50 -1 -1 4.000 0 0 0 0 0 7
8190 3702 8301 3534 8211 3354 8010 3342 7899 3510 7989 3690
8190 3702
2 3 0 1 0 7 50 -1 -1 4.000 0 0 0 0 0 7
8640 3690 8751 3522 8661 3342 8460 3330 8349 3498 8439 3678
8640 3690
4 1 0 50 -1 0 12 0.0000 4 135 150 8100 3600 f0\001
4 1 0 50 -1 0 12 0.0000 4 135 150 8550 3600 f1\001
-6
6 7650 2880 8010 3150
2 2 0 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 5
7650 2880 8010 2880 8010 3150 7650 3150 7650 2880
4 1 0 50 -1 0 12 0.0000 4 90 90 7830 3060 a\001
-6
6 8550 2880 8910 3150
2 2 0 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 5
8550 2880 8910 2880 8910 3150 8550 3150 8550 2880
4 1 0 50 -1 0 12 0.0000 4 135 90 8730 3060 b\001
-6
6 8190 1440 8730 1980
1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 8460 1710 180 180 8460 1890 8460 1530
4 1 0 50 -1 0 12 0.0000 4 135 135 8460 1800 G\001
-6
6 8550 2340 9090 2790
1 2 0 1 0 7 50 -1 -1 4.000 1 0.0000 8820 2565 180 135 8640 2430 9000 2700
4 1 0 50 -1 0 12 0.0000 4 90 90 8820 2610 z\001
-6
6 7380 2340 8010 2790
1 2 0 1 0 7 50 -1 -1 4.000 1 0.0000 7695 2565 225 135 7470 2430 7920 2700
4 1 0 50 -1 0 12 0.0000 4 135 330 7740 2610 x+y \001
-6
6 7290 1800 7650 2250
1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 7470 2025 135 135 7470 2160 7470 1890
4 1 0 50 -1 0 12 0.0000 4 90 90 7470 2070 x\001
-6
6 7740 1800 8100 2250
1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 7920 2025 135 135 7920 2160 7920 1890
4 1 0 50 -1 0 12 0.0000 4 135 90 7920 2070 y\001
-6
6 7650 3780 8010 4230
1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 7830 4005 135 135 7830 4140 7830 3870
4 1 0 50 -1 0 12 0.0000 4 90 90 7830 4050 z\001
-6
6 4770 1620 6390 3870
6 4860 1800 5220 2790
2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5
4860 1800 5220 1800 5220 2070 4860 2070 4860 1800
2 3 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5
4860 2430 5220 2430 5040 2790 4860 2430 4860 2430
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
5040 2070 5040 2430
4 1 0 50 -1 0 12 0.0000 4 90 90 5040 1980 a\001
4 1 0 50 -1 0 12 0.0000 4 90 90 5040 2610 a\001
-6
6 5400 1800 5760 2790
2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5
5400 1800 5760 1800 5760 2070 5400 2070 5400 1800
2 3 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5
5400 2430 5760 2430 5580 2790 5400 2430 5400 2430
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
5580 2070 5580 2430
4 1 0 50 -1 0 12 0.0000 4 135 90 5580 2610 b\001
4 1 0 50 -1 0 12 0.0000 4 135 90 5580 1980 b\001
-6
6 5940 2430 6300 2790
2 3 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5
5940 2430 6300 2430 6120 2790 5940 2430 5940 2430
4 1 0 50 -1 0 12 0.0000 4 135 135 6120 2610 G\001
-6
2 4 0 1 0 7 50 -1 -1 0.000 0 0 7 0 0 5
6390 3870 6390 1620 4770 1620 4770 3870 6390 3870
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
6030 1620 6390 1980
2 3 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 7
5490 3780 5601 3612 5511 3432 5310 3420 5199 3588 5289 3768
5490 3780
2 3 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 7
6051 3780 6162 3612 6072 3432 5871 3420 5760 3588 5850 3768
6051 3780
3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3
6120 2790 6210 3240 6030 3420
0.000 1.000 0.000
3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3
5580 2790 5400 3060 5940 3420
0.000 1.000 0.000
3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3
6120 2790 5940 3060 5490 3420
0.000 1.000 0.000
3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3
5040 2790 4950 3150 5310 3420
0.000 1.000 0.000
4 0 0 50 -1 0 12 0.0000 4 135 60 6210 1800 f\001
4 1 0 50 -1 0 12 0.0000 4 135 90 5400 3690 0\001
4 1 0 50 -1 0 12 0.0000 4 135 90 5940 3690 1\001
-6
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7830 3150 8010 3330
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8730 3150 8640 3330
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8820 2700 8730 2880
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7740 2700 7830 2880
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8370 1890 8190 3330
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8460 1890 8460 3330
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7560 2160 7650 2430
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7830 2160 7740 2430
2 4 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 5
9180 3780 9180 2340 7290 2340 7290 3780 9180 3780
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8100 3690 7920 3870
2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8550 3690 8730 4050
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
9270 1800 8820 1350
2 4 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 5
9270 4500 9270 1350 7200 1350 7200 4500 9270 4500
4 1 0 50 -1 0 12 0.0000 4 135 90 9090 1530 g\001
4 1 0 50 -1 14 12 0.0000 4 180 1365 8370 1170 z = f(x+y,z);\001
4 1 0 50 -1 0 12 0.0000 4 135 1245 4050 2610 Valeurs initiales\001
4 1 0 50 -1 0 12 0.0000 4 135 975 4050 1980 D\351clarations\001
4 1 0 50 -1 0 12 0.0000 4 135 540 4050 3690 Sorties\001
4 1 0 50 -1 14 12 0.0000 4 165 1890 5580 1350 T1 f (T2 a, T3 b);\001
4 1 0 50 -1 3 12 0.0000 4 150 1845 5580 4140 \\res From a , G.a, G.b;\001
4 1 0 50 -1 3 12 0.0000 4 150 1050 5580 4410 G From b, G;\001
doc/pdg/pdg.tex 0 → 100644
+ 78
− 0
View file @ a1ace968
%===============================================================================
% Versions
\section*{Versions}
\begin{small}
Seules les versions Vx.0 sont des documents achevés~;
les autres sont à considérer comme des brouillons.
\begin{enumerate}
\item[V3.0 -] 2 novembre 2020~:
\begin{itemize}
\item Document sous licence Creative Commons
``Attribution-ShareAlike 4.0 International''
\url{https://creativecommons.org/licenses/by/4.0/}.
\end{itemize}
\item[V2.0 -] 3 décembre 2008~:
\begin{itemize}
\item réorganisation,
\item mise à jour,
\item partie sur l'utilisation.
\end{itemize}
\item[V1.4 - ] 30 mai 2008~:
\begin{itemize}
\item ajout d'une partie sur le marquage.
\end{itemize}
\item[V1.3 - ] 22 novembre 2007~:
\begin{itemize}
\item mise à jour de la partie sur l'interprocédural.
\end{itemize}
\item[V1.2 - ] 07 novembre 2007~:
\begin{itemize}
\item mise à jour de la partie sur les dépendances de contrôle.
\end{itemize}
\item[V1.1 - ] 20 septembre 2007~:
\begin{itemize}
\item réorganisation complète,
\item développement de la partie sur les dépendances de contrôle,
\item discussion au sujet des boucles infinies.
\end{itemize}
\item[V1.0 - ] 26 juin 2007~:
\begin{itemize}
\item relecture et petites corrections.
\end{itemize}
\item[V0.2 - ] 24 mai 2007~:
\begin{itemize}
\item révision générale,
\end{itemize}
\item[V0.1 - ] 23 mars 2007~:
\begin{itemize}
\item création du module de calcul de PDG,
\item extraction de la documentation du PDG du rapport sur le {\it
slicing}.
\end{itemize}
\end{enumerate}
\end{small}
%===============================================================================
\cleardoublepage
\tableofcontents
%===============================================================================
\cleardoublepage\input{intro.tex}
\cleardoublepage\input{data.tex}
\cleardoublepage\input{ctrl.tex}
\cleardoublepage\input{calls.tex}
\cleardoublepage\input{utilisation.tex}
\cleardoublepage\input{mark.tex}
\cleardoublepage\input{conclusion.tex}
%===============================================================================
\appendix
%--------------------------------------
\cleardoublepage \input{impact.tex}
%-------------------------------------------------------------------------------
\cleardoublepage
\bibliographystyle{abbrvnat}
\bibliography{../slicing/bib-slicing}
%--------------------------------------
\cleardoublepage
\printindex
%===============================================================================
doc/pdg/utilisation.tex 0 → 100644
+ 49
− 0
View file @ a1ace968
\chapter{Retrouver l'information}\label{sec-find}
Jusqu'à présent, on a vu comment calculer le graphe de dépendances.
Dans ce chapitre, nous présentons les fonctions fournies pour
trouver des éléments du PDG suivant un certain nombre de critères.
L'annexe \ref{sec-impact} rappelle certains objectifs initiaux
d'une utilisation de ces fonctions pour effectuer une analyse d'impact.\\
Par ailleurs, outre la manipulation d'ensemble d'éléments du PDG,
un système de gestion et de propagation de marques est également proposé.
Il est présenté au chapitre \ref{sec-mark}.
\section{A partir de leur clé}
Au cours du calcul, chaque élément du PDG est associé à une clé
qui correspond à l'élément de programme qu'il représente (cf. {\tt
pdgIndex.mli}).
On peut par la suite retrouver un élément à partir de cette clé
comme par exemple l'élément correspondant à une instruction simple,
à un paramètre d'entrée, à une déclaration locale, etc.
\section{A partir d'une zone mémoire}
Grâce à l'état qui est propagé lors de la construction
des dépendances de données (cf. \S\ref{sec-propagation-etat})
on peut retrouver les éléments qui participent au calcul
d'une zone mémoire à un point de programme.
Cette fonction doit également vérifier si les éléments trouvés
définissent complètement la donnée recherchée ou non,
et si ce n'est pas le cas, indiquer la zone susceptible de ne pas être
complètement définie au point considéré.
\section{A partir de propriétés}
D'autres fonctionnalités de \ppc permettent d'interpréter une propriété
du programme et d'en extraire les zones mémoire nécessaires à son évaluation.
Comme on sait par ailleurs trouver les éléments qui correspondent
a une zone mémoire en un point de programme (voir ci-dessus),
on peut ainsi trouver par exemple les éléments dont dépendent une assertion
ou tout autre propriété.
\section{En exploitant les dépendances}
Après avoir retrouver des éléments dans le graphe, on veut en général exploiter
leurs dépendances. On peut facilement retrouver les dépendances avant ou
arrière,
avec ou sans filtrage sur leur type (donnée, contrôle,...),
récursivement ou non.
doc/slicing/.gitignore 0 → 100644
+ 11
− 0
View file @ a1ace968
biblio.bib
frama-c-book.cls
frama-c-cover.pdf
frama-c-left.pdf
frama-c-right.pdf
main.pdf
call.pdf
choose_call.pdf
exple2.pdf
propagation.pdf
propagation.pdf
doc/slicing/Makefile 0 → 100644
+ 50
− 0
View file @ a1ace968
.PHONY: all clean
all: main.pdf
GENERATED=biblio.bib
GENERATED+=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
include ../MakeLaTeXModern
DWNLDDIR=../manuals
DOCNAME=slicing-documentation-fr.pdf
BIB_FILE = bib-slicing.bib
main.bbl : $(BIB_FILE)
@echo "=== Fichier .bib plus récent -> effacement du .bbl"
rm -f $(SRC).bbl
main.pdf: $(FRAMAC_MODERN) $(BIB_FILE) \
main.tex macros_slicing.tex slicing.tex \
intro.tex conclusion.tex \
fonction.tex interproc.tex interproc2.tex man.tex \
algo.tex interexples.tex intercmds.tex projets.tex \
algoH.mli algo.ml \
call.pdf choose_call.pdf exple2.pdf propagation.pdf propagation.pdf
###############################################################################
GENERATED+=call.pdf choose_call.pdf exple2.pdf propagation.pdf propagation.pdf
%.pdf : %.fig
fig2dev -L pdf $< $@
###############################################################################
%.pdf: %.tex
pdflatex $*
bibtex $*
pdflatex $*
pdflatex $*
install: main.pdf
@echo "copying main.pdf in $(DWNLDDIR)/$(DOCNAME)"
@rm -f "$(DWNLDDIR)/$(DOCNAME)"
@cp main.pdf "$(DWNLDDIR)/$(DOCNAME)"
clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
*.haux *.hbbl *.htoc \
*.cb *.cb2 *.cm? *.bbl *.blg *.idx *.ind *.ilg \
$(GENERATED)
###############################################################################
doc/slicing/algo.ml 0 → 100644
+ 22
− 0
View file @ a1ace968
(* On nomme H le module des hypothèses. *)
module H = AlgoH ;;
(* produit une nouvelle fonction spécialisée en partant de [ff]
en marquant l'élément [e] et toutes ses dépendances avec la marque [m]. *)
let rec mark_rec_pdg_elem pdg stmt_elems m e ff =
let new_ff = add_elem_mark pdg stmt_elems m e ff in
let dpds = H.get_dpds e pdg in
List.fold_right (mark_rec_pdg_elem pdg stmt_elems m) dpds new_ff
(* ;; *)
and
(* [add_elem_mark] ajoute la marque [m] à l'instruction correspondant à
l'élément [e] et marque les autres éléments éventuels comme superflus. *)
add_elem_mark pdg stmt_elems m e ff =
let stmt = H.get_stmt e stmt_elems in
let old_m = H.get_stmt_mark stmt ff in
let new_m = H.combine_mark old_m m in
let new_ff = H.replace_stmt_mark ff stmt new_m in
let elems = H.get_elems stmt stmt_elems in
let (_, other_elems) = List.partition (fun elem -> elem = e) elems in
let mark_spare_elem e ff = mark_rec_pdg_elem pdg stmt_elems H.spare_mark e ff in
List.fold_right mark_spare_elem other_elems new_ff
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment