From b9048e5347c207b832d2bf2af022322025e59c08 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 19:43:24 +0100 Subject: Fixing representation of dynamics in votour (again). --- checker/values.ml | 12 ++++++------ checker/votour.ml | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'checker') diff --git a/checker/values.ml b/checker/values.ml index c986415070..2b375651b1 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -332,19 +332,19 @@ let v_univopaques = (** Registering dynamic values *) -module StringOrd = +module IntOrd = struct - type t = string + type t = int let compare (x : t) (y : t) = compare x y end -module StringMap = Map.Make(StringOrd) +module IntMap = Map.Make(IntOrd) -let dyn_table : value StringMap.t ref = ref StringMap.empty +let dyn_table : value IntMap.t ref = ref IntMap.empty let register_dyn name t = - dyn_table := StringMap.add name t !dyn_table + dyn_table := IntMap.add name t !dyn_table let find_dyn name = - try StringMap.find name !dyn_table + try IntMap.find name !dyn_table with Not_found -> Any diff --git a/checker/votour.ml b/checker/votour.ml index d016b45632..f8d8f392ac 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -12,7 +12,7 @@ open Values (** Name of a value *) -type dyn = { dyn_tag : string; dyn_obj : Obj.t; } +type dyn = { dyn_tag : int; dyn_obj : Obj.t; } let to_dyn obj = (Obj.magic obj : dyn) -- cgit v1.2.3 From 2e8e5cc85bfb7f2339fc38babd2dec0026ff5aa4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 19:58:18 +0100 Subject: Functorized interface over object representation in votour. This gives more safety in object manipulation, as we delimit the uses of Obj functions, and allows for an alternative implementation of the representation of OCaml structures. --- checker/votour.ml | 152 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 108 insertions(+), 44 deletions(-) (limited to 'checker') diff --git a/checker/votour.ml b/checker/votour.ml index f8d8f392ac..2db92853ab 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,11 +10,44 @@ open Values (** {6 Interactive visit of a vo} *) -(** Name of a value *) - -type dyn = { dyn_tag : int; dyn_obj : Obj.t; } +type 'a repr = +| INT of int +| STRING of string +| BLOCK of int * 'a array +| OTHER + +module type S = +sig + type obj + val input : in_channel -> obj + val repr : obj -> obj repr + val size : int list -> int +end + +module Repr : S = +struct + type obj = Obj.t + + let input chan = + let obj = input_value chan in + let () = CObj.register_shared_size obj in + obj + + let repr obj = + if Obj.is_block obj then + let tag = Obj.tag obj in + if tag = Obj.string_tag then STRING (Obj.magic obj) + else if tag < Obj.no_scan_tag then + let data = Obj.dup obj in + let () = Obj.set_tag data 0 in + BLOCK (tag, Obj.magic data) + else OTHER + else INT (Obj.magic obj) + + let size p = CObj.shared_size_of_pos p +end -let to_dyn obj = (Obj.magic obj : dyn) +(** Name of a value *) let rec get_name ?(extra=false) = function |Any -> "?" @@ -32,69 +65,101 @@ let rec get_name ?(extra=false) = function (** 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 = +let get_string_in_tuple o = try - for i = 0 to Array.length v - 1 do - if v.(i) = String then - failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]"); + for i = 0 to Array.length o - 1 do + match Repr.repr o.(i) with + | STRING s -> + failwith (Printf.sprintf " [..%s..]" s) + | _ -> () 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 rec get_details v o = match v, Repr.repr o with + | (String | Any), STRING s -> + Printf.sprintf " [%s]" (String.escaped s) + |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o + |(Sum _|Any), BLOCK (tag, _) -> + Printf.sprintf " [tag=%i]" tag + |(Sum _|Any), INT i -> + Printf.sprintf " [imm=%i]" i + |Int, INT i -> Printf.sprintf " [imm=%i]" i + |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)" + " (size "^ string_of_int (Repr.size 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 access_children vs os pos = + if Array.length os = Array.length vs then + Array.mapi (fun i v -> v, os.(i), i::pos) vs + else raise Exit + +let access_list v o pos = + let rec loop o pos = match Repr.repr o with + | INT 0 -> [] + | BLOCK (0, [|hd; tl|]) -> + (v, hd, 0 :: pos) :: loop tl (1 :: pos) + | _ -> raise Exit + in + Array.of_list (loop o pos) + +let access_block o = match Repr.repr o with +| BLOCK (tag, os) -> (tag, os) +| _ -> raise Exit +let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit + +(** raises Exit if the object has not the expected structure *) 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)) + |Tuple (_, v) -> + let (_, os) = access_block o in + access_children v os pos + |Sum (_, _, vv) -> + begin match Repr.repr o with + | BLOCK (tag, os) -> access_children vv.(tag) os pos + | INT _ -> [||] + | _ -> raise Exit + end + |Array v -> + let (_, os) = access_block o in + access_children (Array.make (Array.length os) v) os pos + |List v -> access_list v o pos |Opt v -> - if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||] + begin match Repr.repr o with + | INT 0 -> [||] + | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|] + | _ -> raise Exit + end |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 [||] + |Any -> raise Exit |Dyn -> - let t = to_dyn o in - let tpe = find_dyn t.dyn_tag in - [|(Int, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|] + begin match Repr.repr o with + | BLOCK (0, [|id; o|]) -> + let n = access_int id in + let tpe = find_dyn n in + [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] + | _ -> raise Exit + end |Fail s -> failwith "forbidden" +let get_children v o pos = + try get_children v o pos + with Exit -> match Repr.repr o with + | BLOCK (_, os) -> Array.mapi (fun i o -> Any, o, i :: pos) os + | _ -> [||] + type info = { nam : string; typ : value; - obj : Obj.t; + obj : Repr.obj; pos : int list } @@ -176,8 +241,7 @@ let visit_vo f = let l = read_line () in let seg = int_of_string l in seek_in ch segments.(seg).pos; - let o = (input_value ch : Obj.t) in - let () = CObj.register_shared_size o in + let o = Repr.input ch in let () = init () in visit segments.(seg).typ o [] done -- cgit v1.2.3 From 578d73a8b8eb6623bfa688c1e3ed9d1442bd435f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 Mar 2015 09:24:00 +0100 Subject: Exporting memory representation of STM tasks for votour. --- checker/values.ml | 27 +++++++++++++++++++++++++++ checker/votour.ml | 2 +- 2 files changed, 28 insertions(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/values.ml b/checker/values.ml index 2b375651b1..cf93466b00 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -321,6 +321,33 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) +(** STM objects *) + +let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|]) +let v_states = v_pair Any v_frozen +let v_state = Tuple ("state", [|v_states; Any; v_bool|]) + +let v_vcs = + let data = Opt Any in + let vcs = + Tuple ("vcs", + [|Any; Any; + Tuple ("dag", + [|Any; Any; v_map Any (Tuple ("state_info", + [|Any; Any; Opt v_state; v_pair data Any|])) + |]) + |]) + in + let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in + vcs + +let v_uuid = Any +let v_request id doc = + Tuple ("request", [|Any; Any; doc; Any; id; String|]) +let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool) +let v_counters = Any +let v_stm_seg = v_pair v_tasks v_counters + (** Toplevel structures in a vo (see Cic.mli) *) let v_lib = diff --git a/checker/votour.ml b/checker/votour.ml index 2db92853ab..7c954d6f98 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -219,7 +219,7 @@ let visit_vo f = {name="library"; pos=0; typ=Values.v_lib}; {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; {name="discharging info"; pos=0; typ=Opt Any}; - {name="STM tasks"; pos=0; typ=Opt Any}; + {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg}; {name="opaque proofs"; pos=0; typ=Values.v_opaques}; |] in while true do -- cgit v1.2.3