Skip to content
Snippets Groups Projects
Commit 47f939b3 authored by Boris Yakobowski's avatar Boris Yakobowski Committed by Virgile Prevosto
Browse files

[Value] remove unfinished doc

parent 323d21fb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
doc/value/value-interval.org deleted 100644 → 0
+ 0
− 729
View file @ 323d21fb
Documentation de value
* Les treillis et grosses structures de donnees de value, et l'evaluation C, et leurs relations
#+latex_header: \usepackage{tikz} \usepackage{amsfonts} \usepackage[final]{pdfpages}
Ce document ne présente pas ce qu'est un treillis etc. ni une
introduction à la théorie de l'interprétation abstraite, supposés
connus; il s'agit plus d'un document haut-niveau expliquant les
structures de données et modules principaux du plugin Value.
# XXX: Je dis l'approximation d'une valeur ou "domaine des valeurs" pour
# l'ensemble des valeurs possibles (collecting semantics). J'utilise
# "ensemble" pour les ensembles non-approximes (e.g. dans la logique,
# pour une zone mémoire, etc).
#
# TODO: Une figure avec les relations entre tous les domaines (heritage
# quand on fait un include, "use",etc). Ou de manière semitextuelle
# (i.e. pour chaque noeud, dire module Toto = struct include Map_Functor(Mod1,Mod2) end; module CValue.Model = struct include LMap ... end)
# + juste rajouter les fleches pour dire "depend de" de manière générique.
# + regrouper
#
# + des fleches indiquant pour la relation si c'est "use", "extends", "contains" etc.
#
# : #+header: :imagemagick yes :iminoptions -density 600 :imoutoptions -geometry 400
#+header: :headers '("\\usepackage{tikz}")
#+begin_src latex :exports none :file teste.pdf
\hspace{-1cm}\scalebox{0.9}{
\begin{tikzpicture}[yscale=3, xscale=8]
\tikzstyle{module}=[draw, rectangle, rounded corners, fill=black!15, align=left, above right];
\tikzstyle{lattice}=[draw, rectangle, rounded corners, fill=yellow!25, align=left, above right];
% TODO: Faire differents groupes: Le groupe avec les CValues (utiles pour l'interpretation); le groupe avec
% les adresses (locations); le groupe avec les contenus (offsetmap et lmap); les treillis generiques auxilaires.
% Je vais mettre les groupes dans des scopes.
\begin{scope}[shift={(0,4.5)}]
\draw[fill=gray!60] (-0.05,-0.05) rectangle (2.6,1.1) node[below left,align=right] {\textbf{Evaluation}\\Evaluation du C et de la logique ACSL};
% DONE
\node[module] (op) at (2.25,0.3) {Eval\_op};
\node[module] (expr) at (1.5,0.35) {Eval\_expr};
\node[module] (funs) at (0,0.8) {Eval\_funs};
\node[module] (slevel) at (0,0) {Eval\_slevel};
% \node[module] (annot) at (0.3,0.3) {Eval\_annot};
\node[module] (annot) at (0.6,0.4) {Eval\_annot};
\node[module] (stmt) at (1.2,0) {Eval\_stmt};
%
\node[module] (terms) at (1.2,0.8) {Eval\_terms};
\tikzstyle{arrow}=[->,shorten >=1pt]
% DONE
\draw[arrow] (annot) -- (terms);
\draw[arrow] (expr) -- (op);
\draw[arrow] (funs) + (-0.18,0) -- (funs);
\draw[arrow] (funs) -- (slevel);
%\draw[arrow] (funs) -- (stmt); % Not an important dependency
% TODO: also, dependency from stmt to funs via a reference.
\draw[arrow] (funs) -- (annot);
\draw[arrow] (funs) -- (terms);
\draw[arrow] (slevel) -- (annot);
\draw[arrow] (slevel) -- (expr);
\draw[arrow] (slevel) -- (stmt);
\draw[arrow] (stmt) -- (expr);
\draw[arrow] (stmt) -- (op);
% \draw[arrow] (terms) -- (expr); % Not an important dependency
\draw[arrow] (terms) -- (op);
\end{scope}
\begin{scope}[shift={(0,1)}]
\draw[fill=gray!60] (-0.05,-0.05) rectangle (0.85,3.3) node[below left,align=right] {\textbf{CValue}\\Treillis utilisés pour l'évaluation du C};
\node[lattice] at (0,2.2) { module \textbf{CValue.Model} \\
\textit{Etat de la mémoire d'un programme C}\\
$\approx$ LMap(V\_OffsetMap)};
\node[lattice] at (0,1.5) { module \textbf{CValue.V\_Offsetmap} \\
\textit{Zone mémoire contig\"ue de valeurs C} \\
= Offsetmap.Make(V\_Or\_Uninitialized)};
\node[lattice] at (0,0.8) { module \textbf{CValue.V\_Or\_Uninitialized} \\
\textit{Valeur C eventuellement ``indeterminate''} \\
$\approx$ CValue.V $\times$ \\ \quad has\_uninitialized? $\times$ has\_escaping? };
\node[lattice] at (0,0.1) { module \textbf{CValue.V} \\ \textit{Valeur d'une lvalue C non indeterminate} \\ include Location\_Bytes};
\end{scope}
\begin{scope}[shift={(1.75,0.2)}]
\draw[fill=gray!60] (-0.05,-0.1) rectangle (0.85,4.1) node[below left,align=right] {\textbf{Locations}\\Représentation d'adresses mémoires\\Clés d'accès aux offsetmaps};
\node[lattice] at (0,2.8) { module \textbf{Zone} \\
\textit{Ensemble de locations de taille 1 bit} \\
$\approx$ Map of Base $\to$ Int\_Intervals | $\top$ };
\node[lattice] at (0,1.8) { type \textbf{location} = \\ \textit{Adresse + taille} \\
\textit{Clé d'accès au contenu de la mémoire} \\
\{ loc : Location\_Bits.t;\\ \ \ size: $\mathbb{N} \cup \top$ \}};
\node[lattice] at (0,1) { module \textbf{Location\_Bits} \\ \textit{Adresse en bits, ou valeur numérique} \\ = Location\_Bytes };
\node[lattice] at (0,0) {module \textbf{Location\_Bytes} \\
\textit{Adresse en octet, ou valeur numérique} \\
type t = Map\_Lattice.Make(...).t = \\
| Top of Base.SetLattice.t * Origin.t \\
| Map of Base $\to$ Ival };
\end{scope}
\begin{scope}[shift={(0,-1.7)}]
\draw[fill=gray!60] (-0.05,-0.05) rectangle (0.85,2.1) node[below left,align=right] {\textbf{LMap/Offsetmap}\\Contenu de la mémoire};
\node[lattice] at (0,0.7) { module \textbf{LMap}(OffsetMap)\\
\textit{Contenu de toute la mémoire}\\
= (Map Base $\to$ OffsetMap) $\cup \top \cup \bot $ \\
$\approx$ (Map location $\to$ V) $\cup \top \cup \bot $};
\node[lattice] at (0,0) { module \textbf{OffsetMap}(V) \\
\textit{Zone mémoire contig\"ue, bit-adressable} \\
$\approx$ Arbre d'intervalles de bits $\to$ V};
\end{scope}
\begin{scope}[shift={(1,-2.7)}]
\draw[fill=gray!60] (-0.05,-0.05) rectangle (1.6,2.6) node[below left,align=right] {\textbf{Base}\\Treillis et modules de base};
\node[lattice] at (0,1.4) { module \textbf{Ival} \\
\textit{Valeurs numériques} \\
type t = \\ | Set of $\mathbb{N}$ array \\
| Float(min,max) \\
| Top(min:$\mathbb{N} \cup -\infty$,max:$\mathbb{N} \cup +\infty$,\\\qquad \ \ \,rest:$\mathbb{N}$,modulo:$\mathbb{N}$) };
\end{scope}
\node[module] at (1.8,-1.5) { module \textbf{Base} \\ \textit{Adresse de base d'une zone mémoire} \\
type base $\approx$ \\
| Var(varinfo)\\
| Null\\
| String};
\node[lattice] at (1,-2) { Map\_Lattice; SetLattice; Int\_Intervals ... };
\end{tikzpicture}}
#+end_src
#+RESULTS:
#+BEGIN_LaTeX
[[file:teste.pdf]]
#+END_LaTeX
#+BEGIN_LaTeX
\includepdf[page=1]{teste.pdf}
#+END_LaTeX
** Les treillis de value
*** TODO Notion de treillis
Un treillis est
=is_included=, join/surapproximation du least-upper-bound, et transfer functions.
*** Les domaines numériques
**** TODO Ival
Domaine des valeurs numériques (Flottant ou Entier).
**** DONE =Int_Base=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-20 jeu. 17:05]
:END:
Un domaine simple où on a soit un entier connu de manière exact, soit
Top (un entier inconnu).
Ce domaine est utilisé pour modéliser des tailles de zones mémoire
(généralement connues statiquement). Top est rarement rencontré, car
il ne peut être obtenu qu'en le créant explicitement: il correspond
notamment aux tailles des structures inconnues, ou offset de
structures contenant des structures inconnue.
*** TODO Bases.ml
L'état mémoire du programme est constituée d'un ensemble de plages
d'adresses contigues (ou storages). Une =base= est un identifiant (un
nom)q pour une de ces plages d'adresse (de manière équivalente, une
=base= identifie l'adresse de base de cette plage d'adresse).
Les différentes bases correspondent donc aux manières dont de la
mémoire est allouée en C. En première approximation, on peut dire que:
- =Var= correspond au storage associé aux variables globales, locales,
et formelles
- =Initialized_Var= au storage alloué dynamiquement ou spécialement (les puits)
- =CLogic_Var= permet de donner un storage pour l'évaluation des variables logiques
- =String= donne un storage aux chaines de caractère
- =Null= correspond aux adresses absolues, e.g. (int *) 0x123. Notons
que =CValue.V= = =Location_Bytes= represente les valeurs comme des
couples (Base,offset), et que la base Null correspond également aux
valeurs non-pointeurs (e.g. les valeurs de type =int=).
Note: en réalité, la différence entre Var et Initialized_var est leur
utilisation dans les lmap. Pour diminuer la taille de l'état mémoire,
on ne stocke pas d'offsetmap pour les bases qui ont une "valeur par
défaut". La valeur par défaut des Var est un offsetmap rempli de la
valeur "uninitialized". Pour les Initialized_var, on peut changer
cette valeur par défaut.
# XXX: En explicant ca, on se rend compte que ce mecanisme est
# pas top... On pourrait fusionner Var et Initialized_var, et utiliser
# seulement le champs vlogic.
*** DONE Locations.ml
Les différentes locations representent les adresses et plages
d'adresses, avec ou sans information de taille. Elles ne representent
pas ce qui est contenu dans les adresses.
**** DONE =Locations.Locations_Bytes=
Est le domaine abstrait des "adresses ou valeur numérique",
i.e. represente l'approximation d'une adresse ou valeur numérique. Est
un type somme (hérité de =Map_Lattice=):
: type t =
: | Top of Base.SetLattice.t * Origin.t
: | Map of M.t
M.t est un Map des Bases vers Ival. Dit pour chaque Base, a quel
offset possible cela correspond. Par exemple, si on a la map
: { &a -> {8}; &b -> {4;8} }
Cela signifie qu'on a une adresse, contenue dans l'approximation
: { (void *) ((char *) &a + 8)
: U (void *) ((char *) &b + 4)
: U (void *) ((char *) &b + 8)
: }
La base NULL signifie une valeur numerique (pas une adresse). Ainsi
: { NULL -> [8-16] }
Signifie qu'on a une valeur numerique entiere entre 8 et 16.
Top représente un garbled mix: i.e. un mélange de pointeurs. Ils
garbled mix sont obtenus en faisant des opérations numériques sur des
adresses.
Notes:
- =Locations_Bytes= veut dire Location en Bytes, car l'unité
d'adressage est l'octet. Par opposition dans =Locations_Bits=,
l'unité d'adressage est le bit.
- Le type =Location_Bytes= est le meme que =CValue.V=: ainsi les
lvalues du C sont interpretees comme des =Locations_Bytes=.
- Le type =Location_Bytes= n'a pas de notion de taille. Ainsi, il est
possible d'avoir une lvalue qui s'evalue à 2^137 dans une adresse
qui correspond en fait à un char. La troncature est faite au niveau
supérieur: c'est décidé par Offsetmap, en appellant
=V.anisotropic_cast=.
**** DONE =Locations.Locations_Bits=
Représente le domaine des "adresses en bits, ou valeur numérique". Est
similaire à =Location_Bytes=, sauf que les adresses sont convertis en
bits, ce qui permet de traiter les bitfields. En interne, les
offsetmaps etc. sont adressés au niveau du bit.
Il y a deux modules (=Locations_Bytes= et =Locations_Bits=) pour
éviter toute confusion (notamment, les types sont différents). Il y a
des fonctions de conversion entre les deux.
**** DONE =Locations.location= = =Locations.Location.t=
Les locations représentent une approximation des adresses (en bits,
i.e. de type =Location_Bits=) avec une taille ( =Int_Base=, i.e. un
entier précis ou top).
Les locations sont utilisées comme clés pour accéder à la mémoire. La
mémoire est représentée par le module =CValue.Model = LMap=. Le
déreférencement en lecture se fait par l'appel à la fonction
=CValue.Model.find state loc=, où =state= représente toute la mémoire,
et =loc= est de type =Locations.location=. Le déréférencement en
écriture se fait avec =CValue.Model.add_binding state loc v=.
L'information de taille permet, par exemple, de retourner des valeurs
différentes que l'on lise un =char= ou un =long= à la même adresse.
Note: si une location est précise (i.e. le domaine comprend une seule
base avec un seul offset), les écritures peut faire un "strong
update", i.e. remplacer l'ancienne valeur par une nouvelle, car on est
sûr de l'endroit où on écrit. Sinon, on fait un "weak update", i.e. on
rajoute la nouvelle valeur à l'ensemble des valeurs possibles pour la
case. Par exemple, à la fin du code C suivant:
#+begin_src c
int a[3] = {0;0;0};
void main(void) {
int *p0 = &a[0];
int *p12;
if(rand()) { p12 = &a[1]; } else { p12 = &a[2];}
*p0 = 1; // p0 est précis, on fait un strong update
*p12 = 1; // p12 est imprécis, on fait un weak update
}
#+end_src
La mémoire contiendra:
: a[0] = 1
: a[1] = {0;1}
: a[2] = {0;1}
**** DONE =Locations.Zone=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-25 mar. 15:46]
:END:
Les zones représentent une sur-approximation d'un ensemble de
locations de taille un bit, le bit étant la plus petite unité de
stockage de l'information et donc indivisible. Les zones permettent la
représentation d'emplacements dans la mémoire, sans considérer la
taille des accès.
On peut ainsi voir les zones comme une approximation des locations, où
on a perdu l'information de taille. Notamment, si on prend les deux
locations suivantes:
: {&a->{0;1;2;3}} taille 1 et
: {&a->{0}} taille 4
La première location est un ensemble imprécis de locations de taille 1
tandis que l'autre est une location de taille 4 précise. Mais à ces
deux locations correspondra la même zone.
L'intérêt des zones est justement d'avoir oublié cette information de
taille, ce qui permet notamment de faire des /joins/ sur des ensembles
de locations de tailles différentes.
Au niveau de l'implémentation, les Zones sont des Maps des bases vers
une union d'intervalle d'entiers disjoints; la valeur =Top= représente
un garbled mix, comme pour les =Location_Bytes=, mais n'est
actuellement pas utilisée.
Note: Les zones sont également utilisées comme clés pour les
=OffsetMap_bitwise= et =LMap_Bitwise=. Comme leur nom l'indique, ces
dernières structures permettent de stocker des informations relatives
à chaque bit de la mémoire, sans information de taille d'accès.
*** DONE =Lmap= et =OffsetMap=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-28 ven. 15:43]
- State "DONE" from "TODO" [2013-06-27 jeu. 17:55]
:END:
Ces structures de données représentent le contenu de la mémoire. Une
=OffsetMap= représente le contenu d'une zone contig\"ue de mémoire; par
exemple à une définition de variable globale correspond une =OffsetMap=
représentant la mémoire allouée par cette définition. Les appels à
malloc créent également de nouvelles =OffsetMaps=.
Les =LMap= représentent le contenu de toute la mémoire; il s'agit
d'une =Map= associant à chaque =Base= une =OffsetMap=. Ainsi, pour
chaque variable globale C est créée une nouvelle base, à laquelle est
associée une unique =OffsetMap=. Les appels à =malloc= ou =alloca=, la
rentrée dans un nouveau scope avec des variables locales, les chaines
de caractères ..., créent également de nouvelles bases qui sont
ajoutées au contenu de la mémoire.
**** DONE =OffsetMap=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-27 jeu. 17:55]
:END:
Les =OffsetMap= sont une structure de donnée générique permettant
d'associer à un intervalle d'entiers une valeur de =V=, le module
passé en paramètre.
Dans leur utilisation par =CValue.V_OffsetMap=, le début de
l'intervalle correspond à l'offset (en bits) de la donnée par rapport
à l'adresse de base, et la fin à l'offset de la donnée plus sa taille.
Par exemple, si on considère la définition d'une variable globale C:
: struct { int x; int y; int z; } point;
avec les =int= de taille 32 bits. Dans ce programme, une =OffsetMap=
de taille 96 bits est associée à =point=; =point.x= correspond à
l'intervalle [0;31] de cette intervalle, =point.y= à [32;63], et
=point.z= à [64;95].
Le grand intérêt des =OffsetMap= est de pouvoir représenter la mémoire
malgré les accès non-typés; e.g. un appel à =bzero= dans une
structure, suivie d'une lecture du champs sera correctement
effectuée.
Son autre intérêt est algorithmique: l'opération =OffsetMap.find=
prend en argument une surapproximation des intervalles d'offsets
possibles (exprimé par un =Ival=), ce qui conduit à faire des =V.join=
sur toutes les valeurs qui peuvent être retournées à ces offsets. Les
=OffsetMap= permettent de réaliser cette opération plus efficacement.
Le paramètre =V= de l'OffsetMap est un treillis qui doit fournir des
fonctions de transferts supplémentaires, permettant de ne regarder
qu'une partie des bits d'une valeur, ou de "recoller" des valeurs
contig\"ues.
Le paramètre =V= de l'=OffsetMap= est un treillis avec
/isotropie/. Une valeur est dite isotrope si tous ses bits ont même
valeur, preservée par concaténation des bits. Par exemple,
=CValue.V.Top= (garbled mix) ou =Ival.zero= sont des valeurs
isotropes. Ces valeurs sont représentées de manière optimisée dans
l'offsetmap.
Note:
- L'OffsetMap tel qu'implémenté n'a pas une structure de treillis. En
particulier, certaines valeurs ont plusieurs représentations
(e.g. 0x22 peut être représenté comme "0x22" sur 8 bits ou comme
"0x2" sur 4 bits, répétés deux fois) et la structure n'essaye pas
de normaliser. De fait l'opération =join= ne calcule pas le _least_
upper bound de deux offsetmaps. Néanmoins, le =join= devrait être
commutatif, idempotent, associatif et surtout monotone, ce qui
permet aux itérations de Kleene de converger.
- Les offsetmaps effectuent les opérations de découpe et de recollage
des données du treillis donné en paramètre =V= de manière
paresseuse. Pour cela, l'implémentation maintient, pour chaque
écriture:
- l'offset de début et l'offset de fin. On définit la longueur
comme étant (=offset_fin= - =offset_debut= + 1).
- la taille (égal à la longueur lors de l'écriture initiale)
- le décalage, qui explicite quelle partie de la valeur initiale
reste.
Par exemple, si initialement, on stocke une valeur =v= entre les
offsets 16 et 31; la longueur de l'intervalle est de 16 bits, la
taille de =v= est également de 16 bits, et le décalage est de 0. Si
on écris par la suite une autre valeur =w= entre les offsets 16 et
23, alors l'offsetmap contiendra =w= entre 16 et 23; et entre =24
et 31=, il contiendra un =v= de taille =16= sur un intervalle de
longueur =8=, décalé de =8= (puisqu'on n'a pas pris les 8 bits de
poids fort).
#
# XXX: Isotropie.
#
#
# Maps d'ensembles d'adresses vers des cvalues? I.e. de locations vers des cvalues.
#
# Lmap: map de base vers offsetmap = CValue.Model. Etat complet du
# systeme. Les cles des lmap/cmodel sont des locations.
#
***** COMMENT offsetmap n'est pas un treillis, mais un quasi-treillis?
il y a plusieurs representations possibles pour une meme
valeur. Est-ce un problème?
e.g. si on fait un
: memset(0xFE,4,&int) -> représentation: 0xFE x 4
: *int = 0xFEFEFEFE -> représentation: 0xFEFEFEFE x 1
Si on prend les définitions du papier: abstract interpretation over
non-lattice abstract domain. Pour avoir un treillis, il suffit d'avoir
des opérations =join= et =is_included= correctes.
Le test d'inclusion $\sqsubseteq$ (=is_included=) est un ordre partiel:
1. reflexivité: OK
2. transitivité: OK
3. antysymettrie ($x \sqsubseteq y \land y \sqsubseteq x
\ \Rightarrow \ x = y$): OK si on renvoie faux pour au moins un des sens
de $\sqsubseteq$
L'autre opérateur est le join, qui doit être un least upper bound des
deux éléments. i.e.:
1. $x \sqsubseteq (x \sqcup y)$
2. $y \sqsubseteq (x \sqcup y)$
3. $\forall z, x \sqsubseteq z \ \land \ y \sqsubseteq z \quad\Rightarrow\quad (x \sqcup y) \sqsubseteq z$
Comme on a (0xFE x 4) $\sqcup$ (0xFEFEFEFE x 1) qui est égal à l'un
des deux, il faut qu'un des deux soit plus petit que l'autre.
Conclusion: il faut s'accorder sur lequel de (0xFE x 4) ou de
(0xFEFEFEFE x 1) est le plus petit, que $\sqcup$ renvoie le plus grand
des deux, que $\sqsubseteq$ renvoie vrai dans le bon sens et faux dans
l'autre sens, et les offsetmaps seront (sont déjà?) un vrai treillis.
# XXX: OK, nos opérations $\sqcup$ ne sont pas un least upper bound,
# mais juste un upper bound. Par contre, ils sont monotone, idempotents,
# commutatifs et associatifs.
#
# Knapster-Tarki marche si l'opérateur est monotone. $\sqcup$ Monotone veut dire que
#
# $\forall x,y:\quad x \sqsubseteq y \ \Rightarrow\ \forall z, x \sqcup z \sqsubseteq y \sqcup z$
#
# XXX: Treillis intéressant à étudier: Ival avec recollement.
#
# Des valeurs de ce treillis sont "{x congrus a 3 mod 17} sur 32 bits,
# répété deux fois" et "{x congrus a 3 mod 17} sur 64 bits, répété une
# fois". Le least upper bound de ce treillis est complexe à calculer, en
# particulier avec les ivals qui peuvent se transformer en énumération,
# mais si on y arrive on peut faire des offsetmaps une vraie structure
# de treillis.
#
**** DONE =Lmap=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-28 ven. 15:43]
:END:
Si LMap est implémenté comme étant une map des bases vers des
offsetmaps, il est plus destiné à être utilisé comme une map de
=location= vers =V=, le paramètre passé en argument de l'offsetmap
(d'où le nom LMap signifiant LocationMap).
Comme dans toute =Map=, les deux opérations les plus importantes sont
(en ignorant les paramètres optionels) =find: t -> location -> v= et
=add_binding: t -> location -> v -> t=, qui associent aux locations
utilisées comme clés des valeurs du treillis =V=. Une =Location=
représentant un triplet (base,offset,taille), on utilise la base pour
retrouver l'offsetmap correspondante, et l'offset et la taille pour
écrire à l'intérieur de l'offsetmap.
=Cvalue.Model= est une instantiation de =LMap= qui permet de
représenter toute la mémoire. Dans cette utilisation, =find=
correspond au déréférencement d'une adresse en lecture, et
=add_binding= au déréférencement d'une adresse en écriture.
Note: Le foncteur de =LMap=, =Lmap.Make_LOffset= prend en argument le
module d'offsetmap, un module =Default_offsetmap=, et le module =V=
également passé en argument à =OffsetMap.Make=. =Default_offsetmap=
permet de définir l'état initial de la lmap. On aurait pu éviter de
passer =V= en ayant incluant =V= dans la structure définie par
=OffsetMap.Make(V)=, mais le système de type de OCaml ne sait pas
toujours traquer les alias de types dans différents modules, aussi
est-il plus simple de repasser =V= en argument.
# XXX: C'est lié au fait que le système de module de OCaml est
# applicatif, et non génfératif, également.
*** CValue
**** TODO =CValue.V=
C'est =Location_Bytes=, avec des operations en plus (e.g. additions,
etc). En première approximation, il s'agit des valeurs qui peuvent
être contenues dans un mot mémoire ou un registre en C (pas exactement
vrai, car les CValue.V peuvent contenir des entiers de taille infinie;
voir la section sur les casts pour voir comment ce problème est réglé.)
Open question: est-ce que la signature (ou une partie) ne devrait pas
être commune avec les ival?
**** DONE =CValue.V_Or_Uninitialized=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-25 mar. 18:19]
:END:
L'idée de ce domaine est que si =CValue.V= correspond à un ensemble
des valeurs possibles d'un mot mémoire, =CValue.V_Or_Uninitialized=
correspond au même ensemble auxquels ont peut rajouter les valeurs
spéciales "Uninitialized" (la valeur n'a jamais été initialisée), ou
"Escaping" (dangling pointeur, i.e. pointe sur un bloc mémoire qui a
été libéré).
Ainsi, la valeur "toujours non-initializé" est représenté par
: C_uninit_noesc of V.bottom
Notes:
- Plutôt que d'utiliser un type produit =CValue.V= $\times$
has\_uninitialized? $\times$ has\_escaping?, les bits sont encodés
dans le tag du type somme, pour gagner une indirection.
- La représentation permet une réduction simple d'une valeur
possiblement indeterminate vers une valeur qui ne l'est pas
(=CValue.V=), ce qui est une opération très courante.
- Dans la norme C, "uninitialized or escaping" se dit "indeterminate";
certaines fonctions de l'API utilisent ce nom là.
**** TODO =CValue.V_Offsetmap=
Tout simplement l'instantiation des offsetmap sur
V_Or_Uninitialized. Peu utilisé directement, contrairement à LMap.
**** TODO =CValue.Model=
Instantiation des LMap avec V_OffsetMap et V.
La mémoire associe à chaque base, i.e. chaque zone de mémoire allouée
statiquement représentant une variable globale, une =Offsetmap=,
i.e. une zone mémoire contigue de taille fixe.
Dans cette instantiation, "find" correspond au déréférencement en
lecture, et add_binding au déréférnecement en écriture.
Une des fonctions les plus importantes est =CValue.Model.find=, qui
permet un déréférencement en lecture. Un déréférencement ne récupère
pas toute l'offsetmap associée à une base, mais seulement une partie;
cette fonction prend donc comme clé une =Locations.location=, i.e. une
adresse avec une taille, qu'elle utilise pour extraire la partie utile
en regardant d'abord quel est la base de la location, puis en
extrayant l'intervalle utile dans l'offsetmap associé à cette base.
De manière similaire, =CValue.Model.add_binding= permet un
déréferencement en écriture.
Représente l'ensemble de la mémoire. Est implémenté par le module
=LMap=.
** Domaines basiques
*** DONE =Map_Lattice=
:LOGBOOK:
- State "DONE" from "TODO" [2013-06-25 mar. 17:45]
:END:
Ce module définit le treillis des maps d'un ensemble de clés
(isomorphe à un sous-ensemble de $\mathbb{Z}$), et sans structure de
treillis) vers un treillis de valeurs. Les opérations sur le treillis
sont interprétée de manière naturelle; ainsi
\[ (m1 \sqcup_m m2)[k] = \left\{ \begin{array}{rclcl}
m1[k] \sqcup_v m2[k] & \mathrm{ si } & k \in K(m1) &\cap& K(m2) \\
m1[k] & \mathrm{ si } & k \in K(m1) &\backslash& K(m2) \\
m2[k] & \mathrm{ si } & k \in K(m2) &\backslash& K(m1)
\end{array} \right. \]
Notons qu'une map $m$ est isomorphe à l'ensemble partitionné de
couples (clés,valeurs):
\[ \bigcup_{k \in K(m)} (k, m[k]) \]
Ainsi le domaine des adresses est représenté par une Map des bases
vers des offsets, et doit être vu comme l'ensemble des "base+offset"
comme dans le couple ci-dessus.
Additionellement:
- Une des clés, =null= est différenciée.
- La Map peut être dégradée en =Top=. =Top= est représenté par un
ensemble de clés, et doit être interprété ainsi:
\[ \top_m(K) = \bigcup_{k \in \top_m(K)} (k, \top_v) \]
L'intérêt du constructeur =Top= est de pourvoir traquer l'origine
de la dégradation vers =Top=, avec l'argument de type =Origin.t=.
- On peut voir =Top= comme étant le "mélange" entre les différentes
clés (ceci peut être obtenu par exemple en effectuant un "xor" ou
un "add" entre deux adresses précises). Dans ce cas, $\bigcup_{k
\in \top_m(K)} (k, \top_v)$ n'est pas égal à $\top_m(K)$, mais est
obtenu par réduction de $\top_m(K)$.
- =Top(top_set)= n'est actuellement pas utilisé (il ne peut être
obtenu que par lecture de =CValue.Model.top=, qui ne devrait
jamais être créé).
** Treillis hors value
*** TODO =Lmap_bitwise= et =OffsetMap_bitwise=
Voir [[file:bucket-work.org::*offsetmap%20bitwise%20vs%20offsetmap][offsetmap bitwise vs offsetmap]]
Contrairement aux offsetmaps, les bitwises n'associent pas des données
aux intervalles, mais à chaque bit. C' est comme si toutes les données
étaient isotropes.
** TODO L'évaluation et la réduction
Eval slevel: l'endroit où est paramétré le dataflow de cil.
** DONE Note sur le fonctionnement des casts aux différents niveaux.
Dans les différents niveaux, on a les connaissances suivantes:
- Niveau evaluation (=eval_expr=): on connait les types C (on peut
faire des casts par rapport au type, et on en fait pour toutes les
valeurs récupérées). I.e. c'est là que le + est interprété comme un
"+ modulo taille".
- Niveau =LMap/Offsetmap=: on ne connait plus les types C, mais on
connait la taille des données (on peut faire des casts par rapport à
la taille).
- =CValue.V= et en dessous: on ne connait plus ni la taille, ni le
type C.
# (mais il y a la distinction Float/Int du domaine abstrait)
En théorie, on pourrait ne faire les casts qu'au niveau
=eval_expr/C=. On le fait dans les offsetmap non pas pour diminuer les
intervalles des valeurs stoquees, mais surtout pour la raison
suivante; si on fait un cast de "Null $\to [-128 - 127]$" ou de "Null
$\to [0-255]$" pour 8 bits, on peut le remplacer en un
=Top(None,None,0,1)=, qui permet aux offsetmaps contigus de se
recoller. C'est la raison pour laquelle dans les offsetmap, on fait
des casts au moment de leur écriture.
** TODO Explication sur le rangement des modules dans les differents repertoires
ai,value,=memory_state=...
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