Merge branch 'fix/eva/tail-recursive-wto' into 'master'

[Eva] Tail-recursive implementation of the WTO computation.

See merge request frama-c/frama-c!3561

src/libraries/utils/wto.ml

@@ -153,8 +153,12 @@ module Make(N:sig
         this loop with the lowest level. This vertex is also the deepest in the
         stack and the neareast vertex from the root that is below [vertex] in
         the spanning tree built by the DFS);
-      - [partition] is returned completed. *)
-  let rec visit ~pref state vertex partition =
+      - [partition] is returned completed.
+
+      A tail-recursive implementation of this function is now used to avoid
+      stack overflow errors on very large functions. This function is kept
+      for documentation purposes, as it is simpler and more readable. *)
+  let rec _visit ~pref state vertex partition =
     match DFN.find state.dfn vertex with
     (* The vertex is already in the partition *)
     | Invisible -> NoLoop, partition (* skip it *)
@@ -171,7 +175,7 @@ module Make(N:sig
       (* Visit all its successors *)
       let succs = state.succs vertex in
       let (loop,partition) = List.fold_left (fun (loop,partition) succ ->
-          let (loop',partition) = visit ~pref state succ partition in
+          let (loop',partition) = _visit ~pref state succ partition in
           let loop = min_loop loop loop' in
           (loop,partition)
         ) (NoLoop,partition) succs
@@ -211,7 +215,7 @@ module Make(N:sig
         (* Restart the component analysis *)
         let component = List.fold_left
             (fun component succ ->
-               let (loop,component) = visit ~pref state succ component in
+               let (loop,component) = _visit ~pref state succ component in
                (* Since we reset the component we should have no loop *)
                assert (loop = NoLoop);
                component
@@ -224,12 +228,123 @@ module Make(N:sig
            be added during the second visit of the SCC. *)
         (loop,partition)
 
+
+  (* Types for the tail-recursive function of [visit]. *)
+
+  (* Whether to apply [min_loop] at the end of the visit of a vertex. *)
+  type kind = Default | MinLoop
+
+  (* [visit] contains two recursive calls; its tail-recursive version is split
+     into several steps accordingly. For the visit of a vertex, this type
+     indicates the step that must be done. *)
+  type step =
+    | Start of kind
+    (* Starts the visit of a vertex. If [kind] = [MinLoop], then apply
+       [min_loop] between the previous and the resulting loop. *)
+    | Continue
+    (* Resumes the visit of a vertex after the first recursive call. *)
+    | End of N.t partition
+    (* Ends the visit of a vertex after the second recursive call. *)
+    | Min_loop of loop
+    (* Apply [Min_loop] between [loop] (from the previous result) and the
+       current loop. *)
+
+  (* The list of steps that must be done, with their related vertex. It starts
+     with [init, Start Default] and grows for each original recursive call. *)
+  type continuation = (N.t * step) list
+
+  (** Tail-recursive version of the [visit] function above. *)
+  let tail_recursive_visit ~pref state vertex partition =
+    (* Visit according to the next step to be done. *)
+    let rec visit (cont: continuation) (loop, partition) =
+      match cont with
+      | [] -> loop, partition
+      | (vertex, step) :: cont ->
+        match step with
+        | Start kind ->
+          let cont =
+            if kind = MinLoop then (vertex, Min_loop loop) :: cont else cont
+          in
+          visit_first cont vertex partition
+        | Continue ->
+          visit_second cont vertex loop partition
+        | End partition' ->
+          assert (loop = NoLoop);
+          let r = NoLoop, Component (vertex, partition) :: partition' in
+          visit cont r
+        | Min_loop loop' ->
+          let r = min_loop loop' loop, partition in
+          visit cont r
+
+    (* Visits all successors of [vertex], then continue with [next] and the
+       [continuation]. The status of [vertex] is first set to [status]. *)
+    and visit_succs continuation next (vertex, status) kind acc =
+      let succs = state.succs vertex in
+      DFN.replace state.dfn vertex status;
+      let list = List.map (fun v -> v, Start kind) succs in
+      visit (list @ (vertex, next) :: continuation) (NoLoop, acc)
+
+    and visit_first continuation vertex partition =
+      match DFN.find state.dfn vertex with
+      (* The vertex is already in the partition *)
+      | Invisible ->
+        visit continuation (NoLoop, partition) (* skip it *)
+      (* The vertex have been visited but is not yet in the partition *)
+      | Parent i ->
+        visit continuation (Loop (vertex,i), partition) (* we are in a loop *)
+      (* The vertex have not been visited yet *)
+      | exception Not_found ->
+        (* Put the current vertex into the stack *)
+        Stack.push vertex state.stack;
+        (* Number it and mark it as visited *)
+        let n = state.num + 1 in
+        state.num <- n;
+        (* Visit all its successors. *)
+        visit_succs continuation Continue (vertex, Parent n) MinLoop partition
+
+    and visit_second continuation vertex loop partition =
+      match loop with
+      (* We are not in a loop. Add the vertex to the partition *)
+      | NoLoop ->
+        let _ = Stack.pop state.stack in
+        DFN.replace state.dfn vertex Invisible;
+        visit continuation (NoLoop,Node(vertex)::partition)
+      (* We are in a loop and the current vertex is the head of this loop *)
+      | Loop(head,_) when N.equal head vertex ->
+        (* Unmark all vertices in the loop, and, if pref is given, try to
+           return a better head *)
+        let rec reset_SCC best_head =
+          (** pop until vertex *)
+          let element = Stack.pop state.stack in
+          DFN.remove state.dfn element;
+          if not (N.equal element vertex) then begin
+            (** the strict is important because we are conservative *)
+            let best_head =
+              if pref best_head element < 0 then element else best_head
+            in
+            reset_SCC best_head
+          end
+          else
+            best_head
+        in
+        let best_head = reset_SCC vertex in
+        let vertex = if N.equal best_head vertex then vertex else best_head in
+        (* Makes [vertex] invisible and visits all its successors. *)
+        visit_succs continuation (End partition) (vertex, Invisible) Default []
+      | _ ->
+        (* [vertex] is part of a strongly connected component but is not the
+           head. Do not update partition; the vertex will
+           be added during the second visit of the SCC. *)
+        visit continuation (loop, partition)
+    in
+    visit [vertex, Start Default] (NoLoop, partition)
+
   type pref = N.t -> N.t -> int
 
   let partition ~pref ~init ~succs =
     let state = {dfn = DFN.create 17; num = 0; succs;
                  stack = Stack.create () } in
-    let loop,component = visit ~pref state init [] in
+    let loop,component = tail_recursive_visit ~pref state init [] in
     assert (loop = NoLoop);
     component