Preparing for final commit
This commit is contained in:
Granahir2
parent
d26445d151
commit
d838756d0e
4 changed files with 95 additions and 12 deletions
|
|
@ -159,13 +159,13 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
|
|||
let rec revise_HC4 tree mapenv newval = match tree with
|
||||
| HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval))
|
||||
| HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in begin
|
||||
Format.printf "bwd_binary \"%a%s%a = %a\" -> %a, %a@ "
|
||||
(*Format.printf "bwd_binary \"%a%s%a = %a\" -> %a, %a@ "
|
||||
V.print (get_abst sub1)
|
||||
(Cfg_printer.string_of_int_binary_op bop)
|
||||
V.print (get_abst sub2)
|
||||
V.print (V.meet abst newval)
|
||||
V.print (refined1)
|
||||
V.print (refined2);
|
||||
V.print (refined2);*)
|
||||
meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) end
|
||||
| HC4_int_var (v, abst) -> E (VMap.add v (V.meet abst newval) mapenv)
|
||||
| HC4_int_const (z,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
|
||||
|
|
@ -181,13 +181,13 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
|
|||
| Bot -> Bot
|
||||
| E mapenv -> let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
|
||||
let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in (
|
||||
Format.printf "Refined comparison %a%s%a as %a%s%a@ "
|
||||
(*Format.printf "Refined comparison %a%s%a as %a%s%a@ "
|
||||
V.print (get_abst hc4_1)
|
||||
(Cfg_printer.string_of_compare_op cop)
|
||||
V.print (get_abst hc4_2)
|
||||
V.print newval1
|
||||
(Cfg_printer.string_of_compare_op cop)
|
||||
V.print newval2;
|
||||
V.print newval2;*)
|
||||
meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) )
|
||||
|
||||
let guard env boolexp = guard_noneg env (rm_negations boolexp)
|
||||
|
|
|
|||
|
|
@ -9,6 +9,8 @@ module type ITERABLE = sig
|
|||
|
||||
val do_compute : arc -> t (*source*) -> (arc -> unit) -> (func -> t -> t) -> t (*to accumulate*)
|
||||
val accumulate : arc -> t (*source*) -> t (*old dst*) -> t*bool (*dst*)
|
||||
|
||||
val print : Format.formatter -> t -> unit
|
||||
end
|
||||
|
||||
module SimpleIterable (D : DOMAIN) : ITERABLE = struct
|
||||
|
|
@ -17,15 +19,17 @@ module SimpleIterable (D : DOMAIN) : ITERABLE = struct
|
|||
let bottom = D.bottom
|
||||
let init x = D.init x
|
||||
|
||||
let print fmt abst = D.print fmt abst
|
||||
|
||||
let do_compute a src cb_fail cb_fun = match a.arc_inst with
|
||||
| CFG_skip _ -> src
|
||||
| CFG_assign (v, iexpr) -> D.assign src v iexpr
|
||||
| CFG_guard bexpr -> D.guard src bexpr
|
||||
| CFG_assert (bexpr, _) -> (let s = D.guard src (CFG_bool_unary (AST_NOT, bexpr)) in
|
||||
if D.is_bottom s then (
|
||||
Format.printf "State %a is disjoint with %a@ " D.print src Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr)));
|
||||
(*Format.printf "State %a is disjoint with %a@ " D.print src Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr)));*)
|
||||
src) else (
|
||||
Format.printf "Failure of assert on %a@ " D.print s;
|
||||
(*Format.printf "Failure of assert on %a@ " D.print s;*)
|
||||
cb_fail a;
|
||||
(D.guard src bexpr)))
|
||||
| CFG_call f -> cb_fun f src
|
||||
|
|
@ -34,13 +38,13 @@ module SimpleIterable (D : DOMAIN) : ITERABLE = struct
|
|||
let accumulate a dst_old dst_toacc =
|
||||
if D.subset dst_toacc dst_old then (dst_old, false) else (
|
||||
let accfun = if a.arc_dst.widen_target then D.widen else D.join in
|
||||
let str = if a.arc_dst.widen_target then "widen" else "join" in
|
||||
(*let str = if a.arc_dst.widen_target then "widen" else "join" in
|
||||
Format.printf "@[<h 0>[%i -> %i] Got node %i state %a %s %a " a.arc_src.node_id a.arc_dst.node_id a.arc_dst.node_id
|
||||
D.print dst_old
|
||||
str
|
||||
D.print dst_toacc;
|
||||
D.print dst_toacc;*)
|
||||
let r = accfun dst_old dst_toacc in
|
||||
Format.printf "= %a@]@ " D.print r; r,true)
|
||||
(*Format.printf "= %a@]@ " D.print r;*) r,true)
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -65,6 +69,13 @@ module DisjunctiveIterable (D : DOMAIN) : ITERABLE = struct
|
|||
let bottom = SCRMap.empty
|
||||
let init x = SCRMap.singleton [] (D.init x)
|
||||
|
||||
let print fmt abst =
|
||||
Format.fprintf fmt "@[<h 0>[";
|
||||
SCRMap.iter (fun k x -> Format.fprintf fmt "(";
|
||||
List.iter (fun (i, b) -> Format.fprintf fmt "%d:%b," i b) k;
|
||||
Format.fprintf fmt ") %a" D.print x) abst;
|
||||
Format.fprintf fmt "]@]"
|
||||
|
||||
let do_compute a src cb_fail cb_fun = match a.arc_inst with
|
||||
| CFG_skip _ -> src
|
||||
| CFG_assign (v, iexpr) -> SCRMap.map (fun d -> D.assign d v iexpr) src
|
||||
|
|
@ -74,7 +85,7 @@ module DisjunctiveIterable (D : DOMAIN) : ITERABLE = struct
|
|||
| false -> Some d) src None in
|
||||
(match b with
|
||||
| None -> src
|
||||
| Some d -> Format.printf "Failure of assert : cannot rule out state %a@ " D.print d;
|
||||
| Some _(*d*) -> (*Format.printf "Failure of assert : cannot rule out state %a@ " D.print d;*)
|
||||
cb_fail a; SCRMap.map (fun d -> D.guard d bexpr) src)
|
||||
| CFG_call f -> cb_fun f src
|
||||
|
||||
|
|
@ -85,7 +96,7 @@ module DisjunctiveIterable (D : DOMAIN) : ITERABLE = struct
|
|||
| (ci, _)::q -> (ci, a.arc_parity)::q
|
||||
|
||||
let accumulate a dst_old dst_toacc =
|
||||
Format.printf "[%i -> %i] accumulating...@ " a.arc_src.node_id a.arc_dst.node_id;
|
||||
(*Format.printf "[%i -> %i] accumulating...@ " a.arc_src.node_id a.arc_dst.node_id;*)
|
||||
let tounion = if a.arc_src.branch_node then
|
||||
let ml = SCRMap.to_list dst_toacc in
|
||||
let modlist = (List.map (fun (key,d) -> (tag_key a key, d)) ml) in
|
||||
|
|
@ -96,7 +107,7 @@ module DisjunctiveIterable (D : DOMAIN) : ITERABLE = struct
|
|||
let ns = SCRMap.merge (fun _ d d' -> match d,d' with
|
||||
| None, None -> None
|
||||
| Some d, None -> Some d (*just preserving old state*)
|
||||
| None, Some d -> (flag := true; Format.printf "Unreached branch took !@ "; Some d)
|
||||
| None, Some d -> (flag := true; (*Format.printf "Unreached branch took !@ ";*) Some d)
|
||||
| Some d, Some d' -> (if D.subset d' d then (Some d) else
|
||||
(flag := true; Some (acctor d d')))) dst_old tounion in
|
||||
ns, !flag
|
||||
|
|
|
|||
|
|
@ -46,6 +46,11 @@ module Iterator (I : ITERABLE) = struct
|
|||
iterate (NodeSet.choose !func_dirty)
|
||||
end in
|
||||
iterate f.func_entry;
|
||||
if f.func_name = "main" then
|
||||
Format.printf "@[<v 0>main() analysis result@ %a@]@ "
|
||||
(fun fmt l -> NodeMap.iter
|
||||
(fun n x -> Format.fprintf fmt "<%i> %a@ " n.node_id I.print x) l) !func_state;
|
||||
|
||||
node_abst f.func_exit;
|
||||
end
|
||||
in
|
||||
|
|
|
|||
67
rapport.md
Normal file
67
rapport.md
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
# Analyseur statique
|
||||
|
||||
Le projet reprend et complète la base de code fournie. Nous avons implémenté
|
||||
l'analyse disjonctive par chemin ainsi que le domaine de Karr.
|
||||
|
||||
Les tests de l'analyseur sont fournis avec les tests préexistants et selon leurs conventions. Ils sont intégrés
|
||||
à `scripts/test.sh`. Figurent des tests quand aux support des fonctions, des congruences, de l'analyse
|
||||
disjonctive.
|
||||
|
||||
## Considérations sur les domaines
|
||||
|
||||
### Des domaines nus
|
||||
Que ce soit dans les opérations en avant ou en arrière, le comportement de "Bot"
|
||||
(et dans une moindre mesure de "Top") dans un `VALUE_DOMAIN` ne dépend pas du domaine
|
||||
implémenté. Afin d'aiser l'implémentation des divers `VALUE_DOMAIN` (constantes,intervalles,
|
||||
congruences,signes) on a fait le choix d'implémenter un type de domaine `NAKED_VALUE_DOMAIN`,
|
||||
dont la sémantique est celle d'un `VALUE_DOMAIN` à ceci près que l'on interdit "Bot" et "Top"
|
||||
en entrée des fonctions (ce qui amène à changer un peu la signature, cf. domains/naked.ml).
|
||||
Un foncteur est alors défini, AddTopBot, qui complète un `NAKED_VALUE_DOMAIN` en `VALUE_DOMAIN`.
|
||||
|
||||
Un problème qui apparait est qu'un `NAKED_VALUE_DOMAIN` peut avoir besoin d'exprimer le concept de
|
||||
Top ou Bot, notamment dans les opérations à l'envers. Pour gérer cela, on utilise deux exceptions,
|
||||
`NeedTop` et `Absurd`.
|
||||
|
||||
### Une signature plus expressive
|
||||
|
||||
Afin de faciliter l'écriture du domaine de Karr, la signature de `DOMAIN` change le type de init en
|
||||
un `int -> t`; cela permet d'indiquer au domaine le nombre de variables prévu.
|
||||
|
||||
## L'itérateur
|
||||
|
||||
### Terminaison
|
||||
Dans notre projet, lors de l'exécution, certains noeuds du CFG sont annotés comme des `widen_target` :
|
||||
l'accumulation d'état abstrait se fait sur eux par des `widen` et non des `join`.
|
||||
La terminaison est alors assurée dès lors que chaque boucle apparaissant dans le CFG contient au moins une
|
||||
`widen_target`. Pour ce faire, on procède de deux manières :
|
||||
- lors de la conversion de l'AST en CFG, les noeuds "en tête" de boucle (ceux suivant immédiatement la décision
|
||||
de refaire un tour) sont annotés comme des `widen_target`;
|
||||
- cela ne suffisant pas pour les boucles "implicites" formées via des `goto`, une passe de recherche de cycle
|
||||
par BFS est ensuite effectuée sur chaque fonction; dès qu'elle trouve un cycle, elle note la tête du cycle comme
|
||||
`widen_target`.
|
||||
|
||||
Ce deuxième mécanisme n'apportant aucune garantie sur la pertinence de la cible choisie, un avertissement est
|
||||
émi lorsqu'il annote un noeud.
|
||||
|
||||
### Itérer dans des fonctions
|
||||
Nous avons fait le choix, lors de l'analyse d'une fonction, de remettre à zéro les états des noeuds
|
||||
internes à la fonction (excepté l'entrée). Cela permet à des appels différents à la même fonction de ne
|
||||
pas créer d'imprécision à cause de `join` fortuits. Une telle approche pourrait se généraliser aux
|
||||
fonctions récursives, mais il faudrait du support vis-à-vis du passage de paramètre, de valeur de retour
|
||||
et la terminaison semble plus subtile à garantir.
|
||||
|
||||
### Les iterables
|
||||
|
||||
Initialement, l'algorithme de _worklist_ a été implémenté directement à l'aide des domaines.
|
||||
Toutefois, adapter une telle structure à l'analyse disjonctive aurait nécessité de changer considérablement
|
||||
la signature des domaines pour l'annoter des informations de branchement.
|
||||
|
||||
Ces subtilités ont été encapsulées dans un type de domaine `ITERABLE` (iterator/iterable.ml), dont les
|
||||
instances sont en toute généralité des objets permettant d'effectuer l'algorithme de _worklist._
|
||||
Deux fonctions des domaines vers les itérables sont alors fournis,`SimpleIterable` fournissant une analyse
|
||||
naïve (disponible via l'option `-fno-disjunction`) dont les résultats sont plus lisibles et `DisjunctiveIterable`
|
||||
fournissant une analyse disjonctive.
|
||||
|
||||
Dans la sortie correspondant à une analyse disjonctive, chaque noeud est associé à une fonction partielle de listes de paires entier booléen
|
||||
vers des éléments du domaine. Une liste de paire (entier,booléen) correspond aux exécutions ayant rencontré exactement les conditionnelles indiquées
|
||||
par leur `node_id` et ayant pris la branche indiquée par le booléen (au dernier passage).
|
||||
Loading…
Reference in a new issue