diff options
Diffstat (limited to 'checker/analyze.ml')
-rw-r--r-- | checker/analyze.ml | 86 |
1 files changed, 82 insertions, 4 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml index df75d5b93..7047d8a14 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -55,6 +55,55 @@ let magic_number = "\132\149\166\190" (** Memory reification *) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end = +struct + + let max_length = Sys.max_array_length + + type 'a t = 'a array array * 'a array + (** Invariants: + - All subarrays of the left array have length [max_length]. + - The right array has length < [max_length]. + *) + + let empty = [||], [||] + + let length (vl, vr) = + (max_length * Array.length vl) + Array.length vr + + let make n x = + let k = n / max_length in + let r = n mod max_length in + let vl = Array.init k (fun _ -> Array.make max_length x) in + let vr = Array.make r x in + (vl, vr) + + let get (vl, vr) n = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) + else if k == len then vr.(r) + else invalid_arg "index out of bounds" + + let set (vl, vr) n x = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) <- x + else if k == len then vr.(r) <- x + else invalid_arg "index out of bounds" + +end + type repr = | RInt of int | RBlock of (int * int) (* tag × len *) @@ -82,7 +131,7 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) end module Make(M : Input) = @@ -261,7 +310,7 @@ let parse_object chan = let parse chan = let (magic, len, _, _, size) = parse_header chan in let () = assert (magic = magic_number) in - let memory = Array.make size (Struct ((-1), [||])) in + let memory = LargeArray.make size (Struct ((-1), [||])) in let current_object = ref 0 in let fill_obj = function | RPointer n -> @@ -272,7 +321,7 @@ let parse chan = data, None | RString s -> let data = Ptr !current_object in - let () = memory.(!current_object) <- String s in + let () = LargeArray.set memory !current_object (String s) in let () = incr current_object in data, None | RBlock (tag, 0) -> @@ -282,7 +331,7 @@ let parse chan = | RBlock (tag, len) -> let data = Ptr !current_object in let nblock = Array.make len (Atm (-1)) in - let () = memory.(!current_object) <- Struct (tag, nblock) in + let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in let () = incr current_object in data, Some nblock | RCode addr -> @@ -343,3 +392,32 @@ module PString = Make(IString) let parse_channel = PChannel.parse let parse_string s = PString.parse (s, ref 0) + +let instantiate (p, mem) = + let len = LargeArray.length mem in + let ans = LargeArray.make len (Obj.repr 0) in + (** First pass: initialize the subobjects *) + for i = 0 to len - 1 do + let obj = match LargeArray.get mem i with + | Struct (tag, blk) -> Obj.new_block tag (Array.length blk) + | String str -> Obj.repr str + in + LargeArray.set ans i obj + done; + let get_data = function + | Int n -> Obj.repr n + | Ptr p -> LargeArray.get ans p + | Atm tag -> Obj.new_block tag 0 + | Fun _ -> assert false (** We shouldn't serialize closures *) + in + (** Second pass: set the pointers *) + for i = 0 to len - 1 do + match LargeArray.get mem i with + | Struct (_, blk) -> + let obj = LargeArray.get ans i in + for k = 0 to Array.length blk - 1 do + Obj.set_field obj k (get_data blk.(k)) + done + | String _ -> () + done; + get_data p |