From 6742003891028d566edf23dc7092c34f6d40255f Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 24 Jul 2014 10:18:30 +0200 Subject: Plug into Apron Box domain for intervals. --- Makefile | 2 +- abstract/apron_domain.ml | 184 ++++++++++++++++++++++--------------- doc/readme.pdf | Bin 236320 -> 263955 bytes doc/readme.tm | 224 +++++++++++++++++++++++++++++++-------------- main.ml | 16 ++-- tests/source/updown.scade | 2 +- tests/source/updown2.scade | 2 +- 7 files changed, 280 insertions(+), 150 deletions(-) diff --git a/Makefile b/Makefile index 1faacde..07daf1d 100644 --- a/Makefile +++ b/Makefile @@ -34,7 +34,7 @@ all: $(BIN) $(BIN): $(SRC) ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp -I +str' \ - -lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa octMPQ.cmxa' \ + -lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa octMPQ.cmxa boxMPQ.cmxa' \ main.native \ -classic-display mv main.native $(BIN) diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 58cd544..e1b3007 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -11,18 +11,16 @@ open Apron Mostly direct translation between the two. *) -(* Polyhedra *) - -module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct +module Common = struct - (* manager *) - type man = Polka.loose Polka.t - let manager = Polka.manager_alloc_loose () - - type itv = Interval.t - - (* abstract elements *) - type t = man Abstract1.t + let v_env vars = + let intv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> not n) vars) in + let realv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> n) vars) in + (Environment.make (Array.of_list intv) (Array.of_list realv)) (* direct translation of numerical expressions into Apron tree expressions *) let rec texpr_of_nexpr = function @@ -67,16 +65,107 @@ module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct | CONS_GE -> Tcons1.SUPEQ in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op +end + +(* Apron Boxes (intervals) *) + +module ND_Box : NUMERICAL_ENVIRONMENT_DOMAIN = struct + + open Common + + (* manager *) + type man = Box.t + let manager = Box.manager_alloc () + + type itv = Interval.t + + (* abstract elements *) + type t = man Abstract1.t + (* implementation *) - let v_env vars = - let intv = List.map - (fun (s, _) -> Var.of_string s) - (List.filter (fun (_, n) -> not n) vars) in - let realv = List.map - (fun (s, _) -> Var.of_string s) - (List.filter (fun (_, n) -> n) vars) in - (Environment.make (Array.of_list intv) (Array.of_list realv)) + let top vars = + Abstract1.top manager (v_env vars) + let bottom vars = Abstract1.bottom manager (v_env vars) + let is_bot = Abstract1.is_bottom manager + let is_top = Abstract1.is_top manager + + let forgetvar x id = + let v = [| Var.of_string id |] in + Abstract1.forget_array manager x v false + + let vars x = + let (ivt, fvt) = Environment.vars (Abstract1.env x) in + let ivl = List.map Var.to_string (Array.to_list ivt) in + let fvl = List.map Var.to_string (Array.to_list fvt) in + (List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl) + + let vbottom x = + Abstract1.bottom manager (Abstract1.env x) + + let project x id = + Abstract1.bound_variable manager x (Var.of_string id) + + (* Apply some formula to the environment *) + let apply_cl x cons = + let env = Abstract1.env x in + let tca = Array.of_list (List.map (tcons_of_cons env) cons) in + let ar = Tcons1.array_make env (Array.length tca) in + Array.iteri (Tcons1.array_set ar) tca; + Abstract1.meet_tcons_array manager x ar + + let apply_cons x cons = apply_cl x [cons] + + + let assign x eqs = + let env = Abstract1.env x in + let vars = Array.of_list + (List.map (fun (id, _) -> Var.of_string id) eqs) in + let vals = Array.of_list + (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in + Abstract1.assign_texpr_array manager x vars vals None + + + (* Ensemblistic operations *) + let join = Abstract1.join manager + let meet = Abstract1.meet manager + let widen = Abstract1.widening manager + + let subset = Abstract1.is_leq manager + let eq = Abstract1.is_eq manager + + (* Pretty-printing *) + let print fmt x = + Abstract1.minimize manager x; + Format.fprintf fmt "%a@?" Abstract1.print x + + let print_vars fmt x idl = + let prevars = vars x in + let rm_vars_l = List.filter (fun (id, _) -> not (List.mem id idl)) prevars in + let rm_vars = Array.of_list + (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in + let xx = Abstract1.forget_array manager x rm_vars false in + print fmt xx + + let print_itv = Interval.print + +end + +(* Polyhedra *) + +module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct + open Common + + (* manager *) + type man = Polka.loose Polka.t + let manager = Polka.manager_alloc_loose () + + type itv = Interval.t + + (* abstract elements *) + type t = man Abstract1.t + + (* implementation *) let top vars = Abstract1.top manager (v_env vars) let bottom vars = Abstract1.bottom manager (v_env vars) @@ -129,7 +218,7 @@ module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* Pretty-printing *) let print fmt x = - if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x; + Abstract1.minimize manager x; Format.fprintf fmt "%a@?" Abstract1.print x let print_vars fmt x idl = @@ -149,6 +238,8 @@ end module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct + open Common + (* manager *) type man = Oct.t let manager = Oct.manager_alloc() @@ -158,59 +249,7 @@ module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* abstract elements *) type t = man Abstract1.t - (* direct translation of numerical expressions into Apron tree expressions *) - let rec texpr_of_nexpr = function - | NIdent id -> Texpr1.Var (Var.of_string id) - | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i)) - | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r)) - | NUnary(AST_UPLUS, e, is_real) -> - Texpr1.Unop( - Texpr1.Cast, - texpr_of_nexpr e, - (if is_real then Texpr1.Real else Texpr1.Int), - Texpr1.Rnd) - | NUnary(AST_UMINUS, e, is_real) -> - (* APRON bug ? Unary negate seems to not work correctly... *) - Texpr1.Binop( - Texpr1.Sub, - Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")), - (texpr_of_nexpr e), - (if is_real then Texpr1.Real else Texpr1.Int), - Texpr1.Rnd) - | NBinary(op, e1, e2, is_real) -> - let f = match op with - | AST_PLUS -> Texpr1.Add - | AST_MINUS -> Texpr1.Sub - | AST_MUL -> Texpr1.Mul - | AST_DIV -> Texpr1.Div - | AST_MOD -> Texpr1.Mod - in - Texpr1.Binop( - f, - (texpr_of_nexpr e1), - (texpr_of_nexpr e2), - (if is_real then Texpr1.Real else Texpr1.Int), - Texpr1.Rnd) - - (* direct translation of constraints into Apron constraints *) - let tcons_of_cons env (eq, op) = - let op = match op with - | CONS_EQ -> Tcons1.EQ - | CONS_NE -> Tcons1.DISEQ - | CONS_GT -> Tcons1.SUP - | CONS_GE -> Tcons1.SUPEQ - in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op - (* implementation *) - let v_env vars = - let intv = List.map - (fun (s, _) -> Var.of_string s) - (List.filter (fun (_, n) -> not n) vars) in - let realv = List.map - (fun (s, _) -> Var.of_string s) - (List.filter (fun (_, n) -> n) vars) in - (Environment.make (Array.of_list intv) (Array.of_list realv)) - let top vars = Abstract1.top manager (v_env vars) let bottom vars = Abstract1.bottom manager (v_env vars) @@ -263,7 +302,6 @@ module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* Pretty-printing *) let print fmt x = - if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x; Format.fprintf fmt "%a@?" Abstract1.print x let print_vars fmt x idl = diff --git a/doc/readme.pdf b/doc/readme.pdf index 4a97029..aa680ca 100644 Binary files a/doc/readme.pdf and b/doc/readme.pdf differ diff --git a/doc/readme.tm b/doc/readme.tm index 8622a9a..f21a66c 100644 --- a/doc/readme.tm +++ b/doc/readme.tm @@ -823,20 +823,22 @@ peut être caractérisée par sa fonction de concrétisation : <\eqnarray*> - >>||\\|)>>>>> + >||\\|)>>>>> \ On peut aussi généralement s'appuyer sur l'existence d'une fonction d'abstraction : <\eqnarray*> - >>|||)>\\>>>> + >|||)>\\>>>> Cette fonction fait correspondre à une partie de > sa - meilleure approximation dans le domaine abstrait (par exemple dans le cas - des polyèdres, l'abstraction d'un ensemble fini de points est leur - enveloppe convexe, mais un cercle n'a pas de meilleure abstraction). + meilleure approximation dans le domaine abstrait, lorsque celle-ci existe + (par exemple dans le cas des polyèdres, l'abstraction d'un ensemble fini de + points est leur enveloppe convexe, mais un cercle n'a pas de meilleure + abstraction). En pratique la fonction d'abstraction n'est pas très + utilisée. Dans tous les cas, on s'attend à ce que x\\,x\\|)>> @@ -1441,11 +1443,65 @@ Dans ce cas, on s'arrête si =s>. - + - Une autre approche à base de partitionnement dynamique a été tentée, mais - elle n'a pas donné de très bons résultats par manque d'une heuristique sur - les partitionnements à effectuer. Détails à venir. + Une autre approche à base de partitionnement dynamique a été tentée (cf + ), mais elle + n'a pas donné de très bons résultats par manque d'une heuristique sur les + partitionnements à effectuer. + + L'idée de base consiste à se donner une liste de conditions + ,d,\,d> qui définissent + parties de > (en principe disjointes, mais les + approximations mènent parfois à des recoupenents). On étudie les parties + (ou ) =|d|\>|)>> + comme un système de transitions pour lequel on calcule un point fixe par + itérations chaotiques. + + Les conditions > sont données par une heuristique qui + découpe à chaque rafinement un des lieux > en + plusieurs sous-lieux. + + Le découpage de base est généralement : init + ; non init et propriété vérifiée ; non init et propriété non vérifiée. + + On note \S> + si dans notre sur-approximation on peut être à un cycle dans + > et dans le suivant dans >. + + On recherche un lieu > et une condition + apparaissant dans le programme (ou la négation d'une telle condition) tel + qu'il existe un état > ayant les propriétés + suivantes : + + <\eqnarray*> + >|>|>>|>|>||c|\>S>>>> + + + On peut aussi le faire dans l'autre sens : + + <\eqnarray*> + >|>|>>||c|\>S>|>|>>>> + + + Si une telle condition est détectée, alors on peut diviser le lieu + > en deux parties, + |c|\>S> et + |\c|\>S>, + c'est-à-dire qu'on pose comme nouvelles définitions + ,\,d,c\d,\c\d,d,\,d>. + On refait ensuite un point fixe. Notre analyse est en principe plus fine, + donc on espère trouver des lieux inacessibles. + + En pratique ça ne marche pas très bien car les + rafinements ne sont pas effectués dans le bon ordre. Dans le papier + sus-cité, une double analyse en avant et en arrière était utilisée pour + trouver l'intersection des valeurs accessibles depuis l'état initial et + co-accessibles jusqu'à un état qui provoque une erreur (ie dont la + définition est : la propriété est violée), mais nous n'avons pas tenté + d'implémenter une telle analyse, qui serait sans doute bien plus précise. + Remarquons que l'implémentation de pour LUSTRE est + disponnible sur sa page web (c'est l'outil NBac). @@ -1463,13 +1519,20 @@ logique ; quelques simplifications sur les formules logiques (, ). - domaine numérique non-relationnel basé sur les intervalles ; - domaine relationnel basé sur la bibliothèque externe Apron - (, , - , ...) + trois domaines numériques basés sur Apron : intervalles, polyèdres + et octogones () + + vestige d'une implémentation \S maison \T d'un domaine + non-relationnel à base d'intervalles (, + , + , ) - deux domaines abstraits et analyseur statique correspondant - (, ) + deux domaines abstraits à disjonctions et procédures d'analyse + statique correspondantes (, + ) + + procédure d'analyse par partitionnement dynamique + () En nous basant sur les options de la ligne de commande, nous allons @@ -1518,8 +1581,10 @@ en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la partie numérique - : de même mais utilise le domaine abstrait - relationnel basé sur Apron (polyèdres) pour la partie numérique + : de même mais utilise le domaine abstrait + relationnel basé sur les polyèdres d'Apron pour la partie numérique + + : de même mais utilise les octogones @@ -1534,10 +1599,17 @@ : affiche encore plus de détails n\> : définit un délai pour les - opérations de widening (par défaut 5) + opérations de widening (par défaut 5). Ce délai est utilisé à deux + endroits différents de l'analyse : pour le point fixe local de chaque + itération chaotique, et pour le point fixe global des itérations. vars\> : variables à utiliser comme - variables de disjonction (par défaut : aucune) + variables de disjonction (par défaut : aucune). Donner comme argument + permet d'utiliser toutes les variables énumérées pour les + disjonctions. Donner comme argument > permet + d'utilsier toutes les variables énumérées qui sont utilisées dans une + mémoire. On peut aussi utiliser la syntaxe pour + rajouter des variables aux variables mémoire. scopes\> : donne un certain nombre de scopes pour lesquels ne pas introduire de variable @@ -1568,8 +1640,10 @@ utilisant le domaine à base d'EDD et en utilisant les intervalles comme domaine de valeurs numériques - : de même mais utilise le domaine abstrait - relationnel basé sur Apron (polyèdres) pour la partie numérique + : de même mais utilise le domaine abstrait + relationnel basé sur les polyèdres d'Apron pour la partie numérique + + : de même mais utilise les octogones @@ -1590,10 +1664,7 @@ - Une troisième forme d'analyse, basée sur un partitionnement dynamique de - > a été tentée. Celle-ci n'a pas donné de très bons - résultats, mais nous indiquons néanmoins son existence ici. - L'implémentation existe dans . + Cette analyse est implémentée dans . @@ -1606,7 +1677,7 @@ utilise des graphes de décision pour représenter les conditions sur les énumérées et les intervalles pour la partie numérique - + : utilise les polyèdres d'Apron @@ -1670,7 +1741,7 @@ ...) que l'on exécuterait comme pré-processing sur le programme. - + <\itemize> , > > > - > - > - > - > - > - > - > - > + > + > + > + > + > + > + > + > > - > - > - > - > - > - > - > - > - > - > + > + > + > + > + > + > + > + > + > + > > + > + > + |\>|?>> > > > @@ -1876,61 +1950,77 @@ |.>>>>|> > - |math-font-series||6Implémentation> - |.>>>>|> + |math-font-series||6Partitionnement + dynamique> |.>>>>|> - |6.1Parsing et affichage de + |math-font-series||7Implémentation> + |.>>>>|> + + + |7.1Parsing et affichage de programmes SCADE |.>>>>|> - > + > - |6.2Interprète SCADE + |7.2Interprète SCADE |.>>>>|> - > + > - |6.3Analyse statique par + |7.3Analyse statique par interprétation abstraite |.>>>>|> - > + > - |6.3.1Domaine à disjonctions + |7.3.1Domaine à disjonctions simples |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Options de l'analyse |.>>>>|> - > + > - |6.3.2Domaine à disjonction par + |7.3.2Domaine à disjonction par graphe de décision |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Options de l'analyse |.>>>>|> - > + > - |6.3.3Analyse par partitionnement + |7.3.3Analyse par partitionnement dynamique |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Paramètres de l'analyse |.>>>>|> - > + > + + |math-font-series||8Prolongements + envisageables> |.>>>>|> + + + |8.1Analyse des propriétés des + nombres flottants |.>>>>|> + > + + |8.2Analyse de programmes \S + taille réelle \T |.>>>>|> + > - |math-font-series||Bibliographie> + |math-font-series||9Références> |.>>>>|> - + \ No newline at end of file diff --git a/main.ml b/main.ml index 08ec36a..c283328 100644 --- a/main.ml +++ b/main.ml @@ -13,24 +13,26 @@ open Abs_interp_dynpart module Interpret = Interpret.I -module ItvND = Nonrelational.ND(Intervals_domain.VD) +module ItvND = Apron_domain.ND_Box (* Nonrelational.ND(Intervals_domain.VD) *) +module PolyND = Apron_domain.ND_Poly +module OctND = Apron_domain.ND_Oct module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND) -module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Poly) -module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Oct) +module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND) +module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) -module AI_Poly_EDD = Abs_interp_edd.I(Apron_domain.ND_Poly) -module AI_Oct_EDD = Abs_interp_edd.I(Apron_domain.ND_Oct) +module AI_Poly_EDD = Abs_interp_edd.I(PolyND) +module AI_Oct_EDD = Abs_interp_edd.I(OctND) module AI_S_Itv_DP = Abs_interp_dynpart.I (Enum_domain.MultiValuation)(ItvND) module AI_S_Rel_DP = Abs_interp_dynpart.I - (Enum_domain.MultiValuation)(Apron_domain.ND_Poly) + (Enum_domain.MultiValuation)(PolyND) module AI_EDD_Itv_DP = Abs_interp_dynpart.I (Enum_domain_edd.EDD)(ItvND) module AI_EDD_Rel_DP = Abs_interp_dynpart.I - (Enum_domain_edd.EDD)(Apron_domain.ND_Poly) + (Enum_domain_edd.EDD)(PolyND) (* command line options *) let times = ref false diff --git a/tests/source/updown.scade b/tests/source/updown.scade index c736dd8..4bfa5e3 100644 --- a/tests/source/updown.scade +++ b/tests/source/updown.scade @@ -1,4 +1,4 @@ -const bound: int = 7; +const bound: int = 10; node updown() returns(probe x: int) var last_x: int; diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade index 72d5bed..29069e5 100644 --- a/tests/source/updown2.scade +++ b/tests/source/updown2.scade @@ -1,4 +1,4 @@ -const bound: int = 7; +const bound: int = 10; node updown2() returns(probe x, probe y, probe z: int) var last_x, last_y: int; -- cgit v1.2.3