Some performance improvements

The map_no_copy and instruction visiting functions in the visitor implementation
were not tail recursive. This commit adds tail recursive versions of those functions.
This improves both memory use and performance.

Author: Alasdair

src/lib/jib_visitor.ml

@@ -240,15 +240,45 @@ let rec visit_instr vis outer_instr =
   do_visit vis (vis#vinstr outer_instr) aux outer_instr
 
 and visit_instrs vis outer_instrs =
-  let aux vis no_change =
-    match no_change with
+  let rec commit rev shared n =
+    if n = 0 then (rev, shared) else (match shared with x :: t -> commit (x :: rev) t (n - 1) | [] -> (rev, shared))
+  in
+  let rec unwind result = function
+    | [] -> result
+    | (rev_prefix, f) :: posts -> unwind (List.rev_append rev_prefix (f result)) posts
+  in
+  let rec go rev shared pending posts instrs =
+    match vis#vinstrs instrs with
+    | SkipChildren -> unwind (List.rev_append rev shared) posts
+    | ChangeTo instrs' ->
+        let rev, _ = commit rev shared pending in
+        unwind (List.rev_append rev instrs') posts
+    | DoChildren -> children rev shared pending posts instrs
+    | DoChildrenPost f ->
+        let rev, _ = commit rev shared pending in
+        children [] instrs 0
+          (( rev,
+             fun r ->
+               f ();
+               r
+           )
+          :: posts
+          )
+          instrs
+    | ChangeDoChildrenPost (instrs', f) ->
+        let rev, _ = commit rev shared pending in
+        children [] instrs' 0 ((rev, f) :: posts) instrs'
+  and children rev shared pending posts = function
+    | [] -> unwind (List.rev_append rev shared) posts
     | instr :: instrs ->
         let instr' = visit_instr vis instr in
-        let instrs' = visit_instrs vis instrs in
-        if instr == instr' && instrs == instrs' then no_change else instr' :: instrs'
-    | [] -> []
+        if instr' != instr then (
+          let rev, _ = commit rev shared pending in
+          go (instr' :: rev) instrs 0 posts instrs
+        )
+        else go rev shared (pending + 1) posts instrs
   in
-  do_visit vis (vis#vinstrs outer_instrs) aux outer_instrs
+  go [] outer_instrs 0 [] outer_instrs
 
 and visit_ctype_def vis no_change =
   match no_change with

src/lib/type_check.ml

@@ -742,11 +742,10 @@ let unify l env goals typ1 typ2 =
       )
   else unify_typ l env goals typ1 typ2
 
-let subst_unifiers unifiers typ =
-  List.fold_left (fun typ (v, arg) -> typ_subst v arg typ) typ (KBindings.bindings unifiers)
+let subst_unifiers unifiers typ = KBindings.fold (fun v arg typ -> typ_subst v arg typ) unifiers typ
 
 let subst_unifiers_typ_arg unifiers typ_arg =
-  List.fold_left (fun typ_arg (v, arg) -> typ_arg_subst v arg typ_arg) typ_arg (KBindings.bindings unifiers)
+  KBindings.fold (fun v arg typ_arg -> typ_arg_subst v arg typ_arg) unifiers typ_arg
 
 let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) =
   match aux with

src/lib/visitor.ml

@@ -125,22 +125,26 @@ let do_visit (vis : 'v) (action : 'a visit_action) (children : 'v -> 'a -> 'a) (
 
 let change_do_children node' = ChangeDoChildrenPost (node', fun n -> n)
 
-(* map_no_copy is like map but avoid copying the list if the function does not
- * change the elements. *)
-let rec map_no_copy (f : 'a -> 'a) = function
-  | [] -> []
-  | i :: resti as li ->
-      let i' = f i in
-      let resti' = map_no_copy f resti in
-      if i' != i || resti' != resti then i' :: resti' else li
-
-let rec map_no_copy_list (f : 'a -> 'a list) = function
-  | [] -> []
-  | i :: resti as li -> (
-      let il' = f i in
-      let resti' = map_no_copy_list f resti in
-      match il' with [i'] when i' == i && resti' == resti -> li | _ -> il' @ resti'
-    )
+(* map_no_copy is like map but avoids copying the list if the function does not
+   change any element (compared with physical equality). It is tail recursive:
+   elements up to the last change are rebuilt while the unchanged suffix is
+   shared with the original list, so nothing is allocated when nothing changes.
+   f is applied left-to-right, once per element. *)
+let map_no_copy (f : 'a -> 'a) li =
+  let rec commit rev shared n =
+    if n = 0 then (rev, shared) else (match shared with x :: t -> commit (x :: rev) t (n - 1) | [] -> (rev, shared))
+  in
+  let rec go rev shared pending = function
+    | [] -> List.rev_append rev shared
+    | i :: resti ->
+        let i' = f i in
+        if i' != i then (
+          let rev, shared = commit rev shared pending in
+          go (i' :: rev) resti 0 resti
+        )
+        else go rev shared (pending + 1) resti
+  in
+  go [] li 0 li
 
 (* not part of original cil framework *)
 let map_no_copy_opt (f : 'a -> 'a) : 'a option -> 'a option = function