diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:23 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:23 +0000 |
commit | 589c0c07eb3f9554f6d0949c07f475be53b1bb2b (patch) | |
tree | 678f2eb6b62d89696875e177e6232359586fcf64 /lib | |
parent | 6bcf420febbce8092db54eb23ed17fa3963c0c99 (diff) |
votour: a small tool for guided tours of .vo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r-- | lib/cObj.ml | 130 | ||||
-rw-r--r-- | lib/cObj.mli | 25 |
2 files changed, 136 insertions, 19 deletions
diff --git a/lib/cObj.ml b/lib/cObj.ml index ed14563df..7f3ee1855 100644 --- a/lib/cObj.ml +++ b/lib/cObj.ml @@ -47,7 +47,7 @@ module H = Hashtbl.Make( struct type t = Obj.t let equal = (==) - let hash o = Hashtbl.hash (Obj.magic o : int) + let hash = Hashtbl.hash end) let node_table = (H.create 257 : unit H.t) @@ -66,25 +66,23 @@ let size_of_double = Obj.size (Obj.repr 1.0) let count = ref 0 let rec traverse t = - if not (in_table t) then begin - if Obj.is_block t then begin - add_in_table t; - let n = Obj.size t in - let tag = Obj.tag t in - if tag < Obj.no_scan_tag then begin + if not (in_table t) && Obj.is_block t then begin + add_in_table t; + let n = Obj.size t in + let tag = Obj.tag t in + if tag < Obj.no_scan_tag then + begin count := !count + 1 + n; - for i = 0 to n - 1 do - let f = Obj.field t i in traverse f - done - end else if tag = Obj.string_tag then - count := !count + 1 + n - else if tag = Obj.double_tag then - count := !count + size_of_double - else if tag = Obj.double_array_tag then - count := !count + 1 + size_of_double * n - else - incr count - end + for i = 0 to n - 1 do traverse (Obj.field t i) done + end + else if tag = Obj.string_tag then + count := !count + 1 + n + else if tag = Obj.double_tag then + count := !count + size_of_double + else if tag = Obj.double_array_tag then + count := !count + 1 + size_of_double * n + else + incr count end (*s Sizes of objects in words and in bytes. The size in bytes is computed @@ -100,6 +98,100 @@ let size_b o = (size o) * (Sys.word_size / 8) let size_kb o = (size o) / (8192 / Sys.word_size) +(** {6 Physical sizes with sharing} *) + +(** This time, all the size of objects are computed with respect + to a larger object containing them all, and we only count + the new blocks not already seen earlier in the left-to-right + visit of the englobing object. + + The very same object could have a zero size or not, depending + of the occurrence we're considering in the englobing object. + For speaking of occurrences, we use an [int list] for a path + of field indexes from the outmost block to the one we're looking. + In the list, the leftmost integer is the field index in the deepest + block. +*) + +(** We now store in the hashtable the size (with sharing), and + also the position of the first occurrence of the object *) + +let node_sizes = (H.create 257 : (int*int list) H.t) +let get_size o = H.find node_sizes o +let add_size o n pos = H.replace node_sizes o (n,pos) +let reset_sizes () = H.clear node_sizes +let global_object = ref (Obj.repr 0) + +(** [sum n f] is [f 0 + f 1 + ... + f (n-1)], evaluated from left to right *) + +let sum n f = + let rec loop k acc = if k >= n then acc else loop (k+1) (acc + f k) + in loop 0 0 + +(** Recursive visit of the main object, filling the hashtable *) + +let rec compute_size o pos = + if not (Obj.is_block o) then 0 + else + try + let _ = get_size o in 0 (* already seen *) + with Not_found -> + let n = Obj.size o in + add_size o (-1) pos (* temp size, for cyclic values *); + let tag = Obj.tag o in + let size = + if tag < Obj.no_scan_tag then + 1 + n + sum n (fun i -> compute_size (Obj.field o i) (i::pos)) + else if tag = Obj.string_tag then + 1 + n + else if tag = Obj.double_tag then + size_of_double + else if tag = Obj.double_array_tag then + size_of_double * n + else + 1 + in + add_size o size pos; + size + +(** Provides the global object in which we'll search shared sizes *) + +let register_shared_size t = + let o = Obj.repr t in + reset_sizes (); + global_object := o; + ignore (compute_size o []) + +(** Shared size of an object with respect to the global object given + by the last [register_shared_size] *) + +let shared_size pos o = + if not (Obj.is_block o) then 0 + else + let size,pos' = + try get_size o + with Not_found -> failwith "shared_size: unregistered structure ?" + in + match pos with + | Some p when p <> pos' -> 0 + | _ -> size + +let shared_size_of_obj t = shared_size None (Obj.repr t) + +(** Shared size of the object at some positiion in the global object given + by the last [register_shared_size] *) + +let shared_size_of_pos pos = + let rec obj_of_pos o = function + | [] -> o + | n::pos' -> + let o' = obj_of_pos o pos' in + assert (Obj.is_block o' && n < Obj.size o'); + Obj.field o' n + in + shared_size (Some pos) (obj_of_pos !global_object pos) + + (*s Total size of the allocated ocaml heap. *) let heap_size () = diff --git a/lib/cObj.mli b/lib/cObj.mli index 3264ca61f..16933a4aa 100644 --- a/lib/cObj.mli +++ b/lib/cObj.mli @@ -19,6 +19,31 @@ val size_b : 'a -> int val size_kb : 'a -> int (** Same as [size] in kilobytes. *) +(** {6 Physical size of an ocaml value with sharing.} *) + +(** This time, all the size of objects are computed with respect + to a larger object containing them all, and we only count + the new blocks not already seen earlier in the left-to-right + visit of the englobing object. *) + +(** Provides the global object in which we'll search shared sizes *) + +val register_shared_size : 'a -> unit + +(** Shared size (in word) of an object with respect to the global object + given by the last [register_shared_size]. *) + +val shared_size_of_obj : 'a -> int + +(** Same, with an object indicated by its occurrence in the global + object. The very same object could have a zero size or not, depending + of the occurrence we're considering in the englobing object. + For speaking of occurrences, we use an [int list] for a path + of field indexes (leftmost = deepest block, rightmost = top block of the + global object). *) + +val shared_size_of_pos : int list -> int + (** {6 Logical size of an OCaml value.} *) val obj_stats : 'a -> int * int * int |