From 96c8e33777663aa79e3dc7bbf3860ee250f602d4 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 24 Jul 2014 10:38:52 +0200 Subject: Experiment on dynamic partitionning (guarantee initial partition). --- abstract/abs_interp_dynpart.ml | 77 ++++++++++++-------------- doc/readme.pdf | Bin 263955 -> 263736 bytes doc/readme.tm | 119 ++++++++++++++++++++++------------------- 3 files changed, 98 insertions(+), 98 deletions(-) diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index 23df612..2ff950a 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -228,48 +228,41 @@ end = struct loc = Hashtbl.create 2; counter = ref 2; } in (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *) - let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in - let rstf = simplify_k [rstc] f in - let rstf = simplify_k (get_root_true rstf) rstf in - let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in - let nrstf = simplify_k [nrstc] f in - let nrstf = simplify_k (get_root_true nrstf) nrstf in - Hashtbl.add env.loc 0 - { - id = 0; - depth = 0; - def = apply_cl (top env) (conslist_of_f rstc); - is_init = true; - - f = rstf; - cl = conslist_of_f rstf; - - in_c = 0; - v = bottom env; - - out_t = []; - in_t = []; - verif_g = []; - violate_g = []; - }; - Hashtbl.add env.loc 1 - { - id = 1; - depth = 0; - def = apply_cl (top env) (conslist_of_f nrstc); - is_init = false; - - f = nrstf; - cl = conslist_of_f nrstf; - - in_c = 0; - v = bottom env; - - out_t = []; - in_t = []; - verif_g = []; - violate_g = []; - }; + let id = let i = ref 0 in fun () -> (incr i; !i) in + let add_loc is_init conds = + let cf = simplify_k conds f in + let cf = simplify_k (get_root_true cf) cf in + let id = id() in + Hashtbl.add env.loc id + { + id; + depth = 0; + def = apply_cl (top env) (conslist_of_f cf); + is_init; + + f = cf; + cl = conslist_of_f cf; + + in_c = 0; + v = bottom env; + + out_t = []; + in_t = []; + verif_g = []; + violate_g = []; + }; + in + + add_loc true [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)]; + + let rec div_g conds = function + | [] -> add_loc false conds + | (_, _, v)::r -> + add_loc false ((BEnumCons(E_NE, v, EItem bool_true))::conds); + div_g ((BEnumCons(E_EQ, v, EItem bool_true))::conds) r + in + div_g [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] env.guarantees; + env diff --git a/doc/readme.pdf b/doc/readme.pdf index aa680ca..89e5d4e 100644 Binary files a/doc/readme.pdf and b/doc/readme.pdf differ diff --git a/doc/readme.tm b/doc/readme.tm index f21a66c..c6cde6d 100644 --- a/doc/readme.tm +++ b/doc/readme.tm @@ -1705,10 +1705,6 @@ <\itemize> - Implémenter un domaine d'intervalles permettant de gérer les - rationnels en précision arbitraire, ou se brancher sur le module Box - d'Apron - Utiliser un opérateur de widening aproprié (cf Astrée) Implémenter la sémantique des nombres flottants machine (ce qui @@ -1794,29 +1790,29 @@ > > > - > - > - > - > - > - > - > - > + > + > + > + > + > + > + > + > > - > - > - > - > - > - > - > - > - > - > + > + > + > + > + > + > + > + > + > + > > - > - > - |\>|?>> + > + > + |\>|20>> > > > @@ -1950,77 +1946,88 @@ |.>>>>|> > - |math-font-series||6Partitionnement - dynamique> |.>>>>|> - + |5.3Partitionnement dynamique + |.>>>>|> + > + + |Découpage de base. + |.>>>>|> + > + + |Rafinement. + |.>>>>|> + > + + Observations. |.>>>>|> + - |math-font-series||7Implémentation> + |math-font-series||6Implémentation> |.>>>>|> - + - |7.1Parsing et affichage de + |6.1Parsing et affichage de programmes SCADE |.>>>>|> - > + > - |7.2Interprète SCADE + |6.2Interprète SCADE |.>>>>|> - > + > - |7.3Analyse statique par + |6.3Analyse statique par interprétation abstraite |.>>>>|> - > + > - |7.3.1Domaine à disjonctions + |6.3.1Domaine à disjonctions simples |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Options de l'analyse |.>>>>|> - > + > - |7.3.2Domaine à disjonction par + |6.3.2Domaine à disjonction par graphe de décision |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Options de l'analyse |.>>>>|> - > + > - |7.3.3Analyse par partitionnement + |6.3.3Analyse par partitionnement dynamique |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Paramètres de l'analyse |.>>>>|> - > + > - |math-font-series||8Prolongements + |math-font-series||7Prolongements envisageables> |.>>>>|> - + - |8.1Analyse des propriétés des + |7.1Analyse des propriétés des nombres flottants |.>>>>|> - > + > - |8.2Analyse de programmes \S + |7.2Analyse de programmes \S taille réelle \T |.>>>>|> - > + > - |math-font-series||9Références> + |math-font-series||Références> |.>>>>|> - + \ No newline at end of file -- cgit v1.2.3