Source file `chaoticIteration.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
(**************************************************************************)
(*                                                                        *)
(*  Ocamlgraph: a generic graph library for OCaml                         *)
(*  Copyright (C) 2004-2010                                               *)
(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* Copyright © 2015 Thibault Suzanne <thi.suzanne (@) gmail.com>
 * École Normale Supérieure, Département d'Informatique
 * Paris Sciences et Lettres
*)

(* Original algorithm by François Bourdoncle. See :
 * "Efficient chaotic iteration strategies with widenings",
 * Formal Methods in Programming and their Applications,
 * Springer Berlin Heidelberg, 1993.
*)

let ( |> ) x f = f x

type 'a widening_set =
  | FromWto
  | Predicate of ('a -> bool)

module type G = sig
  type t

  module V : Sig.COMPARABLE

  module E : sig
    type t
    val src : t -> V.t
  end

  val fold_pred_e : (E.t -> 'a -> 'a) -> t -> V.t -> 'a -> 'a
end

module type Data = sig
  type t

  type edge

  val join : t -> t -> t
  val equal : t -> t -> bool

  val analyze : edge -> t -> t

  val widening : t -> t -> t
end

module Make
    (G : G)
    (D : Data with type edge = G.E.t)
=
struct
  module M = Map.Make (G.V)

  let recurse g wto init widening_set widening_delay =

    (* The following two functions are predicates used to know whether
       to compute a widening when analysing a vertex which is not
       (resp. is) the head of a WTO component. They will be called
       only if the specified number of steps before widening has been
       done. *)
    let do_nonhead_widen v = match widening_set with
      | FromWto -> false
      | Predicate f -> f v
    in

    let do_head_widen v = match widening_set with
      | FromWto -> true
      | Predicate f -> f v
    in

    let find vertex data =
      try M.find vertex data
      with Not_found -> init vertex
    in

    let analyze_vertex widening_steps do_widen v data =
      (* Computes the result of the analysis for one vertex *)
      let result = G.fold_pred_e
          (fun edge acc ->
             let src = G.E.src edge in
             let data_src = find src data in
             let data_dst = D.analyze edge data_src in
             D.join data_dst acc)
          g v (init v) in
      if widening_steps <= 0 && do_widen v
      then D.widening (find v data) result
      else result
    in

    let rec analyze_elements widening_steps comp data =
      (* Computes the result of one iteration of the analysis of the
         elements of a component. *)
      WeakTopological.fold_left (analyze_element widening_steps) data comp

    and stabilize can_stop widening_steps head comps data =
      (* Iterates the analysis of a component until
         stabilisation. [can_stop] is [false] if no iteration has been
         made so far, since at least one is needed before ending with
         stabilisation. *)
      let old_data_head =
        find head data in
      let new_data_head =
        analyze_vertex widening_steps do_head_widen head data in
      if can_stop && D.equal old_data_head new_data_head
      then data
      else
        data
        |> M.add head new_data_head
        |> analyze_elements widening_steps comps
        |> stabilize true (widening_steps - 1) head comps

    and analyze_element widening_steps data = function
      (* Computes the result of the analysis of one element *)
      | WeakTopological.Vertex v ->
        M.add v (analyze_vertex widening_steps do_nonhead_widen v data) data
      | WeakTopological.Component (head, comps) ->
        stabilize false widening_delay head comps data
    in

    analyze_elements widening_delay wto M.empty
end