From 47f939b3dc8126ffb6eff4da455391643a9718cf Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Wed, 23 Nov 2016 14:17:06 +0100
Subject: [PATCH] [Value] remove unfinished doc
---
doc/value/value-interval.org | 729 -----------------------------------
1 file changed, 729 deletions(-)
delete mode 100644 doc/value/value-interval.org
diff --git a/doc/value/value-interval.org b/doc/value/value-interval.org
deleted file mode 100644
index f7be7612be4..00000000000
--- a/doc/value/value-interval.org
+++ /dev/null
@@ -1,729 +0,0 @@
-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=...
-
--
GitLab