Nouveau profiler compatible avec ocaml >= 3.01

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1871 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 66 insertions, 0 deletions

diff --git a/lib/profile.ml b/lib/profile.ml
index ac5b0e5207..f28c55ad8f 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -661,3 +661,49 @@ let profile7 e f a b c d g h i =
     last_alloc := get_alloc ();
     raise exn
 
+(* Some utilities to compute the logical and physical sizes and depth
+   of ML objects *)
+
+open Obj
+
+let rec obj_stats d (s, b, m as u) t =
+  if is_int t || (tag t >= no_scan_tag) then (s, b, max d m)
+  else
+    let n = Obj.size t in
+    block_stats (d + 1) (s + n , b + 1, m) (n - 1) t
+
+and block_stats d u i t =
+  if i < 0 then u else block_stats d (obj_stats d u (field t i)) (i-1) t
+
+let obj_stats a = obj_stats 0 (0,0,0) (Obj.repr a)
+
+let tbl = Hashtbl.create 13
+
+let rec obj_shared_size s t =
+  if is_int t || (tag t >= no_scan_tag) then s
+  else 
+    if Hashtbl.mem tbl t then s
+    else 
+      let n = Obj.size t in
+      Hashtbl.add tbl t t;
+      block_shared_size (s + n + 1) (n - 1) t
+
+and block_shared_size s i t =
+  if i < 0 then s
+  else block_shared_size (obj_shared_size s (field t i)) (i-1) t
+
+let obj_shared_size a =
+  Hashtbl.clear tbl;
+  obj_shared_size 0 (Obj.repr a)
+
+let print_logical_stats a =
+  let (s, b, d) = obj_stats a in
+  Printf.printf "Expanded size: %10d  Depth: %6d\n" (s + b) d
+
+let print_stats a =
+  let (s, b, d) = obj_stats a in
+  let o = obj_shared_size a in
+  Printf.printf "Size: %10d (%10d)  Depth: %6d\n" o (s + b) d
+(*
+let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }
+*)
diff --git a/lib/profile.mli b/lib/profile.mli
index 8d4105cf6a..13c75cc8c0 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -106,3 +106,23 @@ val profile7 :
   ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) 
     -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
 
+
+(* Some utilities to compute the logical and physical sizes and depth
+   of ML objects *)
+
+(* Print logical size (in words) and depth of its argument *)
+(* This function does not disturb the heap *)
+val print_logical_stats : 'a -> unit
+
+(* Print physical size, logical size (in words) and depth of its argument *)
+(* This function allocates itself a lot (the same order of magnitude
+   as the physical size of its argument) *)
+val print_stats : 'a -> unit
+
+(* Return physical size, logical size (in words) and depth of its argument *)
+(* This function allocates itself a lot *)
+val obj_stats : 'a -> int * int * int
+
+(* Return physical size of its argument *)
+(* This function allocates itself a lot *)
+val obj_shared_size : 'a -> int