summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-06-01 10:06:35 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-06-01 10:06:35 +0200
commit652d04c5476fdfb9cc7a2d93de3df4d76a6882ce (patch)
tree128e3af9f8c23d9edf8ceb949565ead5840fd46a
parent1038c28dab7775278c67e941a5e29d6e128eb09d (diff)
downloadSemVerif-Projet-652d04c5476fdfb9cc7a2d93de3df4d76a6882ce.tar.gz
SemVerif-Projet-652d04c5476fdfb9cc7a2d93de3df4d76a6882ce.zip
Implémentation des intervalles ; début rédaction du rapport.
-rw-r--r--abstract/interpret.ml1
-rw-r--r--abstract/intervals_domain.ml41
-rw-r--r--abstract/nonrelational.ml2
-rw-r--r--rapport.tm338
4 files changed, 378 insertions, 4 deletions
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index cb32e22..f6a6cb4 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -73,7 +73,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
(binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
env
-
| _ -> env
end
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index b63f8a9..d95a938 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -33,6 +33,21 @@ module Intervals : VALUE_DOMAIN = struct
| Int(x), Int(y) -> Int(Z.mul x y)
| MInf, PInf | PInf, MInf -> MInf
| MInf, MInf | PInf, PInf -> PInf
+ let bound_div a b =
+ match a, b with
+ | _, PInf | _, MInf -> Int Z.zero
+ | PInf, Int i ->
+ if i < Z.zero then MInf
+ else PInf
+ | MInf, Int i ->
+ if i < Z.zero then PInf
+ else MInf
+ | Int i, Int j ->
+ if j = Z.zero then
+ if i < Z.zero then MInf
+ else PInf
+ else Int (Z.div i j)
+
let bound_min a b = match a, b with
| MInf, _ | _, MInf -> MInf
@@ -50,6 +65,8 @@ module Intervals : VALUE_DOMAIN = struct
| PInf -> MInf
| MInf -> PInf
| Int i -> Int (Z.neg i)
+
+ let bound_abs a = bound_max a (bound_neg a)
(* implementation *)
let top = Itv(MInf, PInf)
@@ -101,8 +118,28 @@ module Intervals : VALUE_DOMAIN = struct
(bound_max (bound_mul b c) (bound_mul b d))))
- let div a b = top (* TODO *)
- let rem a b = top (* TODO *)
+ let div a b = match a, b with
+ | Bot, _ -> Bot
+ | Itv(a, b), q ->
+ let p1 = match meet q (Itv(Int (Z.of_int 1), PInf)) with
+ | Bot -> Bot
+ | Itv(c, d) ->
+ Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d))
+ in
+ let p2 = match meet q (Itv(MInf, Int (Z.of_int (-1)))) with
+ | Bot -> Bot
+ | Itv(c, d) ->
+ Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d))
+ in
+ join p1 p2
+
+ let rem a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) ->
+ Itv(
+ Int Z.zero,
+ bound_max (bound_abs c) (bound_abs d)
+ )
let leq a b = match a, b with
| Bot, _ | _, Bot -> Bot, Bot
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index aa34d14..188c8bc 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -110,7 +110,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
| Env m, Env n ->
VarMap.for_all2o
(fun _ _ -> true)
- (fun _ _ -> true)
+ (fun _ v -> v = V.top)
(fun _ a b -> V.subset a b)
m n
diff --git a/rapport.tm b/rapport.tm
new file mode 100644
index 0000000..cb9a68b
--- /dev/null
+++ b/rapport.tm
@@ -0,0 +1,338 @@
+<TeXmacs|1.0.7.21>
+
+<style|<tuple|article|french>>
+
+<\body>
+ <doc-data|<doc-title|Rapport de projet : interprtation
+ abstraite>|<doc-author|<author-data|<author-name|Alex AUVOLAT>>>>
+
+ <section|Introduction>
+
+ <subsection|Analyse statique abstraite>
+
+ L'analyse statique abstraite d'un programme consiste excuter ce
+ programme non pas sur une entre particulire mais sur un domaine abstrait
+ qui reprsente toute un ensemble de donnes possibles. Cette faon de
+ tester permet de dcouvrir des proprits qui sont vraies quelle que soit
+ l'entre sur laquelle le programme est excut, et ce en une seule passe
+ d'analyse statique (dont on est sre qu'elle termine - contrairement au
+ programme lui-mme).
+
+ L'analyse abstraite consiste faire se propager le domaine abstrait tous
+ les points du programme. En plaant des assertions des endroits
+ judicieux, on peut s'assurer que certaines conditions sont toujours
+ vrifies.
+
+ Le domaine abstrait ne peut pas reprsenter avec la prcision ncessaire
+ (infinie) exactement tous les tats du programme, c'est pourquoi nous
+ sommes obligs d'en considrer une sur-approximation. Le but du jeu tant
+ d'avoir la sur-approximation avec le moins de marge par rapport aux
+ ensembles d'tats concrets reprsents, afin de pouvoir prouver un maximum
+ de proprits.
+
+ <subsection|Notre tche>
+
+ Dans le cadre du cours \S smantique et application la vrification de
+ programmes \T, nous avons eu travailler sur un interprteur abstrait pour
+ un fragment du langage C. Le travail minimum demand comportait les aspects
+ suivants :
+
+ <\itemize>
+ <item>Dfinition d'un interprteur sur un domaine abstrait prenant en
+ compte les dclarations de variables locales, les affectations, ainsi que
+ les constructions <verbatim|if>, <verbatim|while>, <verbatim|assert>,
+ <verbatim|print>, <verbatim|halt> ;
+
+ <item>Prise en charge du non-dterminisme (fonction <verbatim|rand>) ;
+
+ <item>Interprtation possible dans plusieurs domaines abstraits : deux
+ domaines non-relationnels (treillis des constantes et treillis des
+ intervalles) et un domaine relationnel (domaine des polyhdres).
+ </itemize>
+
+ Notre code s'appuie sur de nombreux lments extrieurs :
+
+ <\itemize>
+ <item>La bibliothque <name|zarith>, pour la manipulation d'entiers en
+ prcision arbitraire ;
+
+ <item>La bibliothque <name|apron>, pour la manipulation du domaine des
+ polyhdres ;
+
+ <item>Un lexer et un parser pour notre fragment de C fourni par
+ l'enseignant.
+ </itemize>
+
+ <section|Dcoupage des modules>
+
+ Pour raliser ce projet, nous avons tent de factoriser notre code au
+ maximum. Grce une interface de modules et de foncteurs astucieuse, nous
+ avons crit un code dont la partie \S interprtation abstraite \T fait
+ moins de 1000 lignes. Nous prsentons maintenant des extraits de cette
+ interface, largement inspire de celle propose par l'enseignant dans les
+ transparents de son cours \S Abstract Interpretation II \T.
+
+ Dans tout le code, les entiers sont reprsents par le type <verbatim|Z.t>
+ de la bibliothque <name|zarith>, qui permet de manipuler des entiers en
+ prcision arbitraire.
+
+ <subsection|La signature de module <verbatim|ENVIRONMENT_DOMAIN>>
+
+ Cette signature de module dfinit les fonctions que doivent implmenter
+ tout module pouvant tre utilis comme domaine abstrait (relationnel ou non
+ relationnel). Il est utilis pour paramtrer le module
+ <verbatim|Interpret.Make>, qui contient le cur de l'interprteur abstrait.
+
+ <verbatim|>
+
+ <\itemize>
+ <item><verbatim|type t>
+
+ Le type abstrait reprsentant un environnement abstrait de notre
+ interprteur.
+
+ <item><verbatim|val init, bottom : t>
+
+ Reprsentations respectives de <math|\<top\>> et <math|\<bot\>>. Remarque
+ : l'environnement reprsentant <math|\<top\>> est diffrent en fonction
+ des variables que cet environnement contient. <verbatim|init> est
+ l'environnement <math|\<top\>> ne contenant aucune variable. Il y a une
+ fonction de test <verbatim|is_bot> mais pas de test <verbatim|is_top> car
+ celui-ci n'est pas ncessaire.
+
+ <item><verbatim|val addvar, rmvar : t -\<gtr\> id -\<gtr\> t>
+
+ Ajoute une variable un environnement (elle est initialise sans aucune
+ contrainte, c'est--dire <math|\<top\>> dans le cas des environnements
+ non-relationnels) ; supprime une variable d'un environnement.
+
+ <item><verbatim|val assign : t -\<gtr\> id -\<gtr\> expr ext -\<gtr\> t>
+
+ Ralise l'affectation d'une expression une variable :
+ <math|S<around*|\<llbracket\>|x\<leftarrow\>e|\<rrbracket\>>>.
+
+ <item><verbatim|val compare_leq, compare_eq : t -\<gtr\> expr ext
+ -\<gtr\> expr ext -\<gtr\> t>
+
+ Restreint le domaine abstrait une portion vrifiant une quation :
+ <math|S<around*|\<llbracket\>|e<rsub|1>\<leqslant\>e<rsub|2>?|\<rrbracket\>>>
+ et <math|S<around*|\<llbracket\>|e<rsub|1>=e<rsub|2>?|\<rrbracket\>>>.
+
+ <item><verbatim|val join, meet, widen : t -\<gtr\> t -\<gtr\> t>
+
+ Implmentation de l'union abstraite <math|\<sqcup\>>, de l'intersection
+ abstraite <math|\<sqcap\>> et de l'opration de widening
+ <math|\<nabla\>>.
+
+ <item><verbatim|val subset: t -\<gtr\> t -\<gtr\> bool>
+
+ Implmentation de la condition d'inclusion <math|\<sqsubseteq\>>. Une
+ seule implication : <verbatim|subset a b>
+ <math|\<Rightarrow\>a\<sqsubseteq\>b>.
+ </itemize>
+
+ \
+
+ <subsection|La signature de module <verbatim|VALUE_DOMAIN>>
+
+ Cette signature de module dfinit les fonctions requises pour tout module
+ dcrivant un domaine de valeurs pour une abstraction non relationnelle.
+ Cette signature est le paramtre du module <verbatim|NonRelationnal> qui
+ contient le code gnrique pour un <verbatim|ENVIRONMENT_DOMAIN> non
+ relationnel.
+
+ <\itemize>
+ <item><verbatim|type t>
+
+ Le type abstrait d'une valeur abstraite
+
+ <item><verbatim|val top, bottom : t>
+
+ Les reprsentations de <math|\<top\>> et <math|\<bot\>>. Il n'y a pas de
+ fonctions de tests <verbatim|is_bot> et <verbatim|is_top>, les
+ reprsentations sont uniques.
+
+ <item><verbatim|val const : Z.t -\<gtr\> t>
+
+ Obtenir la reprsentation d'une constante.
+
+ <item><verbatim|val rand : Z.t -\<gtr\> Z.t -\<gtr\> t>
+
+ Obtenir la reprsentation d'un intervalle.
+
+ <item><verbatim|val subset : t -\<gtr\> t -\<gtr\> bool>
+
+ Implmentation de la relation d'inclusion <math|\<sqsubset\>> sur les
+ valeurs.
+
+ <item><verbatim|val join, meet, widen : t -\<gtr\> t -\<gtr\> t>
+
+ Implmentation de l'union <math|\<sqcup\>>, de l'intersection
+ <math|\<sqcap\>> et du widening <math|\<nabla\>>.
+
+ <item><verbatim|val neg : t -\<gtr\> t>
+
+ Ngation unaire abstraite
+
+ <item><verbatim|val add, sub, mul, div, rem : t -\<gtr\> t -\<gtr\> t>
+
+ Oprateurs binaires abstraits
+
+ <item><verbatim|val leq : t -\<gtr\> t -\<gtr\> t * t>
+
+ Restreint deux valeurs <math|a\<nocomma\>> et <math|b> aux meilleurs
+ sur-approximations que l'on peut avoir en restreignant le domaine avec
+ une condition de la forme <math|a\<leqslant\>b>.
+ </itemize>
+
+ <subsection|Le module <verbatim|Constants>>
+
+ Ce module implmente un <verbatim|VALUE_DOMAIN> correspondant au treillis
+ des constantes. Le code est extrmement simple et implmente directement la
+ smantique vue en cours.
+
+ <subsection|Le module <verbatim|Intervals>>
+
+ Ce module implmente un <verbatim|VALUE_DOMAIN> correspondant au treillis
+ des intervales. Le code est extrmement simple et implmente directement la
+ smantique vue en cours.
+
+ <subsection|Le module <verbatim|NonRelationnal>>
+
+ Ce module implmente toutes les fonctions communes aux domaines
+ non-relationnels (constantes, intervalles). Il est paramtr par un
+ <verbatim|VALUE_DOMAIN> <verbatim|V>.
+
+ <\itemize>
+ <item>Le type <verbatim|t> reprsentant un environnement abstrait est
+ soit un map des identifieurs vers les lments de <verbatim|V>, soit
+ <math|\<bot\>>. Ds qu'une valeur vaur <math|\<bot\>>, on s'interdit de
+ la mettre dans le map et on transforme tout l'environnement abstrait en
+ <math|\<bot\>>. La fonction <verbatim|strict> permet de s'en assurer.
+
+ <item>Les expressions sont values selont des modalits trs simples :
+ on rcupre les valeurs abstraites correspondant aux constantes et aux
+ variables et on applique les oprateurs de <verbatim|V> qui
+ correspondent, ce qui donne une nouvelle valeur. L'valuation d'une
+ expression de cette manire est utilie pour l'affectation ainsi que dans
+ les operations <verbatim|compare_leq> et <verbatim|compare_eq>.
+
+ <item>Pour un oprateur <math|\<ltimes\>\<in\><around*|{|\<leqslant\>,=|}>>,
+ les filtrages du type <math|S<around*|\<llbracket\>|e<rsub|1>\<ltimes\>e<rsub|2>?|\<rrbracket\>>>
+ sont implments comme suit (fonction <verbatim|compare>) :
+
+ <\itemize>
+ <item><math|S<around*|\<llbracket\>|x\<ltimes\>y?|\<rrbracket\>>> : on
+ applique l'oprateur (<verbatim|leq> pour <math|\<leqslant\>> ou
+ <verbatim|meet> pour <math|=>) de <verbatim|V> sur les deux valeurs, ce
+ qui donne deux nouvelles valeurs pour <math|x> et <math|y> (ou deux
+ fois <math|\<bot\>> si la conditin ne peut pas tre remplie). On
+ utilise ces deux valeurs pour mettre jour l'environnement.
+
+ <item><math|S<around*|\<llbracket\>|x\<ltimes\>e?|\<rrbracket\>>> et
+ <math|S<around*|\<llbracket\>|e\<ltimes\>x?|\<rrbracket\>>> : on value
+ l'expression <math|e> et on applique l'oprateur de <verbatim|V> sur
+ cette valeur et la valeur de <math|x>, ce qui restreint ventuellement
+ la valeur de <math|x>, ou peut donner <math|\<bot\>>.
+
+ <item><math|S<around*|\<llbracket\>|e<rsub|1>\<ltimes\>e<rsub|2>?|\<rrbracket\>>>
+ : on value les expressions <math|e<rsub|1>> et <math|e<rsub|2>> et on
+ applique l'oprateur de <verbatim|V>. Aucune valeur n'est restreinte
+ dans l'environnement mais on peut dtecter une condition impossible,
+ auquel cas l'environnement est pass <math|\<bot\>>.
+ </itemize>
+
+ <item>Les oprateurs <math|\<sqcup\>>, <math|\<sqcap\>> et
+ <math|\<nabla\>> sur les environnements appliquent l'oprateur
+ correspondant sur les valeurs point-par-point pour chaque variable. Pour
+ que ces oprateurs n'chouent pas, il faut que les mmes variables soient
+ dclares dans les deux environnements.
+
+ <item>L'oprateur <math|\<sqsubset\>> sur les environnements fonctionne
+ aussi point-par-point mais n'choue pas dans le cas de deux
+ environnements ne dclarant pas les mmes variables.
+ </itemize>
+
+ <subsection|Le module <verbatim|RelationnalDomain>>
+
+ Ce module implmente le domaine abstrait des polyhdres (domaine
+ relationnel) en faisant appel la bibliothque Apron. En pratique, ce
+ module fait une simple traduction entre les appels et structures de notre
+ programme et ceux de la bibliothque Apron.
+
+ <subsection|Le module <verbatim|Interpret.Make>>
+
+ TODO
+</body>
+
+<\initial>
+ <\collection>
+ <associate|page-medium|paper>
+ <associate|page-screen-margin|false>
+ </collection>
+</initial>
+
+<\references>
+ <\collection>
+ <associate|auto-1|<tuple|1|1>>
+ <associate|auto-10|<tuple|2.6|?>>
+ <associate|auto-11|<tuple|2.7|?>>
+ <associate|auto-2|<tuple|1.1|1>>
+ <associate|auto-3|<tuple|1.2|1>>
+ <associate|auto-4|<tuple|2|2>>
+ <associate|auto-5|<tuple|2.1|2>>
+ <associate|auto-6|<tuple|2.2|2>>
+ <associate|auto-7|<tuple|2.3|2>>
+ <associate|auto-8|<tuple|2.4|2>>
+ <associate|auto-9|<tuple|2.5|2>>
+ </collection>
+</references>
+
+<\auxiliary>
+ <\collection>
+ <\associate|toc>
+ <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-1><vspace|0.5fn>
+
+ <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|2<space|2spc>Dcoupage
+ des modules> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-2><vspace|0.5fn>
+
+ <with|par-left|<quote|1tab>|2.1<space|2spc>La signature de module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|ENVIRONMENT_DOMAIN>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-3>>
+
+ <with|par-left|<quote|1tab>|2.2<space|2spc>La signature de module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|VALUE_DOMAIN>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-4>>
+
+ <with|par-left|<quote|1tab>|2.3<space|2spc>Le module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|Constants>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-5>>
+
+ <with|par-left|<quote|1tab>|2.4<space|2spc>Le module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|Intervals>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-6>>
+
+ <with|par-left|<quote|1tab>|2.5<space|2spc>Le module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|NonRelationnal>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-7>>
+
+ <with|par-left|<quote|1tab>|2.6<space|2spc>Le module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|RelationnalDomain>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-8>>
+
+ <with|par-left|<quote|1tab>|2.7<space|2spc>Le module
+ <with|font-family|<quote|tt>|language|<quote|verbatim>|Interpret.Make>
+ <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+ <no-break><pageref|auto-9>>
+ </associate>
+ </collection>
+</auxiliary> \ No newline at end of file