diff options
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | checker/votour.ml | 150 | ||||
| -rw-r--r-- | lib/cObj.ml | 130 | ||||
| -rw-r--r-- | lib/cObj.mli | 25 |
4 files changed, 292 insertions, 19 deletions
diff --git a/Makefile.build b/Makefile.build index d8b9df0d4..0601abef2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -541,6 +541,12 @@ $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BEST $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,unix) +# votour: a small vo explorer (based on the checker) + +bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, -I checker,) + # Special rule for the compatibility-with-camlp5 extension for camlp4 ifeq ($(CAMLP4),camlp4) diff --git a/checker/votour.ml b/checker/votour.ml new file mode 100644 index 000000000..19c188310 --- /dev/null +++ b/checker/votour.ml @@ -0,0 +1,150 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Values + +(** {6 Interactive visit of a vo} *) + +(** Name of a value *) + +let rec get_name ?(extra=false) = function + |Any -> "?" + |Tuple (name,_) -> name + |Sum (name,_,_) -> name + |Array v -> "array"^(if extra then "/"^get_name ~extra v else "") + |List v -> "list"^(if extra then "/"^get_name ~extra v else "") + |Opt v -> "option"^(if extra then "/"^get_name ~extra v else "") + |Int -> "int" + |String -> "string" + |Annot (s,v) -> s^"/"^get_name ~extra v + +(** For tuples, its quite handy to display the inner 1st string (if any). + Cf. [structure_body] for instance *) + +let get_string_in_tuple v o = + try + for i = 0 to Array.length v - 1 do + if v.(i) = String then + failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]"); + done; + "" + with Failure s -> s + +(** Some details : tags, integer value for non-block, etc etc *) + +let rec get_details v o = match v with + |String | Any when (Obj.is_block o && Obj.tag o = Obj.string_tag) -> + " [" ^ String.escaped (Obj.magic o : string) ^"]" + |Tuple (_,v) -> get_string_in_tuple v o + |(Sum _|Any) when Obj.is_block o -> + " [tag=" ^ string_of_int (Obj.tag o) ^"]" + |(Sum _|Any) -> + " [imm=" ^ string_of_int (Obj.magic o : int) ^"]" + |Int -> " [" ^ string_of_int (Obj.magic o : int) ^"]" + |Annot (s,v) -> get_details v o + |_ -> "" + +let node_info (v,o,p) = + get_name ~extra:true v ^ get_details v o ^ + " (size "^ string_of_int (CObj.shared_size_of_pos p)^"w)" + +(** Children of a block : type, object, position. + For lists, we collect all elements of the list at once *) + +let access_children vs o pos = + Array.mapi (fun i v -> v, Obj.field o i, i::pos) vs + +let rec get_children v o pos = match v with + |Tuple (_,v) -> access_children v o pos + |Sum (_,_,vv) -> + if Obj.is_block o then access_children vv.(Obj.tag o) o pos + else [||] + |Array v -> access_children (Array.make (Obj.size o) v) o pos + |List v -> + let rec loop pos = function + | [] -> [] + | o :: ol -> (v,o,0::pos) :: loop (1::pos) ol + in + Array.of_list (loop pos (Obj.magic o : Obj.t list)) + |Opt v -> + if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||] + |String | Int -> [||] + |Annot (s,v) -> get_children v o pos + |Any -> + if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then + Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos)) + else [||] + +type info = { + nam : string; + typ : value; + obj : Obj.t; + pos : int list +} + +let stk = ref ([] : info list) + +let init () = stk := [] + +let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk + +let pop () = match !stk with + | i::s -> stk := s; i + | _ -> failwith "empty stack" + +let rec visit v o pos = + Printf.printf "\nDepth %d Pos %s Context %s\n" + (List.length !stk) + (String.concat "." (List.rev_map string_of_int pos)) + (String.concat "/" (List.rev_map (fun i -> i.nam) !stk)); + Printf.printf "-------------\n"; + let children = get_children v o pos in + let nchild = Array.length children in + Printf.printf "Here: %s, %d child%s\n" + (node_info (v,o,pos)) nchild (if nchild = 0 then "" else "ren:"); + Array.iteri + (fun i vop -> Printf.printf " %d: %s\n" i (node_info vop)) + children; + Printf.printf "-------------\n"; + Printf.printf ("# %!"); + let l = read_line () in + try + if l = "u" then let info = pop () in visit info.typ info.obj info.pos + else + let v',o',pos' = children.(int_of_string l) in + push (get_name v) v o pos; + visit v' o' pos' + with Failure _ | Invalid_argument _ -> visit v o pos + +(** Loading the vo *) + +let opaque = ref false + +let visit_vo f = + Printf.printf "Welcome to votour !\n"; + Printf.printf "Enjoy your guided tour of a Coq .vo\n"; + Printf.printf "Object sizes are in words\n"; + Printf.printf "At prompt, <n> enters the <n>-th child and u goes up\n%!"; + let ch = open_in_bin f in + let _magic = input_binary_int ch in + let lib = (input_value ch : Obj.t) in (* actually Cic.library_disk *) + let _ = (input_value ch : Digest.t) in + let tbl = (input_value ch : Obj.t) in (* actually Cic.opaque_table *) + let () = close_in ch in + let o = if !opaque then tbl else lib in + let ty = if !opaque then Values.v_opaques else Values.v_lib in + let () = CObj.register_shared_size o in + let () = init () in + visit ty o [] + +let main = + if not !Sys.interactive then + Arg.parse ["-opaques",Arg.Set opaque,"visit the table of opaque terms"] + visit_vo + ("votour: guided tour of a Coq .vo file\n"^ + "Usage: votour [opts] foo.vo") 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 |