diff --git a/domains/value_domain.ml b/domains/value_domain.ml index d6aaebe..8aa1fab 100644 --- a/domains/value_domain.ml +++ b/domains/value_domain.ml @@ -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) diff --git a/iterator/iterable.ml b/iterator/iterable.ml index 6352ec3..e81b88d 100644 --- a/iterator/iterable.ml +++ b/iterator/iterable.ml @@ -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 "@[[%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 "@[["; + 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 diff --git a/iterator/iterator.ml b/iterator/iterator.ml index ba3e431..42ee594 100644 --- a/iterator/iterator.ml +++ b/iterator/iterator.ml @@ -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 "@[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 diff --git a/rapport.md b/rapport.md new file mode 100644 index 0000000..de1685e --- /dev/null +++ b/rapport.md @@ -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).