Checker validation acts on object representations rather than objects.

3 files changed, 149 insertions, 87 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 0f427e457a..4ac5c56732 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -305,8 +305,8 @@ let marshal_in_segment ~validate ~value f ch =
       with _ ->
         user_err (str "Corrupted file " ++ quote (str f))
     in
+    let () = Validate.validate ~debug:!Flags.debug value v in
     let v = Analyze.instantiate v in
-    let () = Validate.validate !Flags.debug value v in
     Obj.obj v, stop, digest
   else
     System.marshal_in_segment f ch
diff --git a/checker/validate.ml b/checker/validate.ml
index 070a112bb6..c3e7d18e56 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -8,32 +8,39 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Analyze
+
 (* This module defines validation functions to ensure an imported
    value (using input_value) has the correct structure. *)
 
-let rec pr_obj_rec o =
-  if Obj.is_int o then
-    Format.print_int(Obj.magic o)
-  else if Obj.is_block o then
-    let t = Obj.tag o in
-    if t > Obj.no_scan_tag then
-      if t = Obj.string_tag then
-        Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
-      else
-        Format.print_string "?"
-    else
-      (let n = Obj.size o in
-      Format.print_string ("#"^string_of_int t^"(");
-      Format.open_hvbox 0;
-      for i = 0 to n-1 do
-        pr_obj_rec (Obj.field o i);
-        if i<>n-1 then (Format.print_string ","; Format.print_cut())
-      done;
-      Format.close_box();
-      Format.print_string ")")
-  else Format.print_string "?"
-
-let pr_obj o = pr_obj_rec o; Format.print_newline()
+let rec pr_obj_rec mem o = match o with
+| Int i ->
+    Format.print_int i
+| Ptr p ->
+  let v = LargeArray.get mem p in
+  begin match v with
+  | Struct (tag, data) ->
+    let n = Array.length data in
+    Format.print_string ("#"^string_of_int tag^"(");
+    Format.open_hvbox 0;
+    for i = 0 to n-1 do
+      pr_obj_rec mem (Array.get data i);
+      if i<>n-1 then (Format.print_string ","; Format.print_cut())
+    done;
+    Format.close_box();
+    Format.print_string ")"
+  | String s ->
+    Format.print_string ("\""^String.escaped s^"\"")
+  | Int64 _
+  | Float64 _ ->
+    Format.print_string "?"
+  end
+| Atm tag ->
+  Format.print_string ("#"^string_of_int tag^"()");
+| Fun addr ->
+  Format.printf "fun@%x" addr
+
+let pr_obj mem o = pr_obj_rec mem o; Format.print_newline()
 
 (**************************************************************************)
 (* Obj low-level validators *)
@@ -48,63 +55,117 @@ type error_context = error_frame list
 let mt_ec : error_context = []
 let (/) (ctx:error_context) s : error_context = s::ctx
 
-exception ValidObjError of string * error_context * Obj.t
-let fail ctx o s = raise (ValidObjError(s,ctx,o))
+exception ValidObjError of string * error_context * data
+let fail _mem ctx o s = raise (ValidObjError(s,ctx,o))
+
+let is_block mem o = match o with
+| Ptr _ | Atm _ -> true
+| Fun _ | Int _ -> false
+
+let is_int _mem o = match o with
+| Int _ -> true
+| Fun _ | Ptr _ | Atm _ -> false
+
+let is_uint63 mem o =
+  if Sys.word_size == 64 then is_int mem o
+  else match o with
+  | Int _ | Fun _ | Atm _ -> false
+  | Ptr p ->
+    match LargeArray.get mem p with
+    | Int64 _ -> true
+    | Float64 _ | Struct _ | String _ -> false
+
+let is_float64 mem o = match o with
+| Int _ | Fun _ | Atm _ -> false
+| Ptr p ->
+  match LargeArray.get mem p with
+  | Float64 _ -> true
+  | Int64 _ | Struct _ | String _ -> false
+
+let get_int _mem = function
+| Int i -> i
+| Fun _ | Ptr _ | Atm _ -> assert false
+
+let tag mem o = match o with
+| Atm tag -> tag
+| Fun _ -> Obj.out_of_heap_tag
+| Int _ -> Obj.int_tag
+| Ptr p ->
+  match LargeArray.get mem p with
+  | Struct (tag, _) -> tag
+  | String _ -> Obj.string_tag
+  | Float64 _ -> Obj.double_tag
+  | Int64 _ -> Obj.custom_tag
+
+let size mem o = match o with
+| Atm _ -> 0
+| Fun _ | Int _ -> assert false
+| Ptr p ->
+  match LargeArray.get mem p with
+  | Struct (tag, blk) -> Array.length blk
+  | String _ | Float64 _ | Int64 _ -> assert false
+
+let field mem o i = match o with
+| Atm _ | Fun _ | Int _ -> assert false
+| Ptr p ->
+  match LargeArray.get mem p with
+  | Struct (tag, blk) -> Array.get blk i
+  | String _ | Float64 _ | Int64 _ -> assert false
 
 (* Check that object o is a block with tag t *)
-let val_tag t ctx o =
-  if Obj.is_block o && Obj.tag o = t then ()
-  else fail ctx o ("expected tag "^string_of_int t)
-
-let val_block ctx o =
-  if Obj.is_block o then
-    (if Obj.tag o > Obj.no_scan_tag then
-      fail ctx o "block: found no scan tag")
-  else fail ctx o "expected block obj"
-
-let val_dyn ctx o =
-  let fail () = fail ctx o "expected a Dyn.t" in
-  if not (Obj.is_block o) then fail ()
-  else if not (Obj.size o = 2) then fail ()
-  else if not (Obj.tag (Obj.field o 0) = Obj.int_tag) then fail ()
+let val_tag t mem ctx o =
+  if is_block mem o && tag mem o = t then ()
+  else fail mem ctx o ("expected tag "^string_of_int t)
+
+let val_block mem ctx o =
+  if is_block mem o then
+    (if tag mem o > Obj.no_scan_tag then
+      fail mem ctx o "block: found no scan tag")
+  else fail mem ctx o "expected block obj"
+
+let val_dyn mem ctx o =
+  let fail () = fail mem ctx o "expected a Dyn.t" in
+  if not (is_block mem o) then fail ()
+  else if not (size mem o = 2) then fail ()
+  else if not (tag mem (field mem o 0) = Obj.int_tag) then fail ()
   else ()
 
 open Values
 
-let rec val_gen v ctx o = match v with
-  | Tuple (name,vs) -> val_tuple ~name vs ctx o
-  | Sum (name,cc,vv) -> val_sum name cc vv ctx o
-  | Array v -> val_array v ctx o
-  | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] ctx o
-  | Opt v -> val_sum "option" 1 [|[|v|]|] ctx o
-  | Int -> if not (Obj.is_int o) then fail ctx o "expected an int"
+let rec val_gen v mem ctx o = match v with
+  | Tuple (name,vs) -> val_tuple ~name vs mem ctx o
+  | Sum (name,cc,vv) -> val_sum name cc vv mem ctx o
+  | Array v -> val_array v mem ctx o
+  | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] mem ctx o
+  | Opt v -> val_sum "option" 1 [|[|v|]|] mem ctx o
+  | Int -> if not (is_int mem o) then fail mem ctx o "expected an int"
   | String ->
-    (try val_tag Obj.string_tag ctx o
-     with Failure _ -> fail ctx o "expected a string")
+    (try val_tag Obj.string_tag mem ctx o
+     with Failure _ -> fail mem ctx o "expected a string")
   | Any -> ()
-  | Fail s -> fail ctx o ("unexpected object " ^ s)
-  | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
-  | Dyn -> val_dyn ctx o
-  | Proxy { contents = v } -> val_gen v ctx o
-  | Uint63 -> val_uint63 ctx o
-  | Float64 -> val_float64 ctx o
+  | Fail s -> fail mem ctx o ("unexpected object " ^ s)
+  | Annot (s,v) -> val_gen v mem (ctx/CtxAnnot s) o
+  | Dyn -> val_dyn mem ctx o
+  | Proxy { contents = v } -> val_gen v mem ctx o
+  | Uint63 -> val_uint63 mem ctx o
+  | Float64 -> val_float64 mem ctx o
 
 (* Check that an object is a tuple (or a record). vs is an array of
    value representation for each field. Its size corresponds to the
    expected size of the object. *)
-and val_tuple ?name vs ctx o =
+and val_tuple ?name vs mem ctx o =
   let ctx = match name with
     | Some n -> ctx/CtxType n
     | _ -> ctx
   in
   let n = Array.length vs in
   let val_fld i v =
-    val_gen v (ctx/(CtxField i)) (Obj.field o i) in
-  val_block ctx o;
-  if Obj.size o = n then Array.iteri val_fld vs
+    val_gen v mem (ctx/(CtxField i)) (field mem o i) in
+  val_block mem ctx o;
+  if size mem o = n then Array.iteri val_fld vs
   else
-    fail ctx o
-      ("tuple size: found "^string_of_int (Obj.size o)^
+    fail mem ctx o
+      ("tuple size: found "^string_of_int (size mem o)^
           ", expected "^string_of_int n)
 
 (* Check that the object is either a constant constructor of tag < cc,
@@ -113,35 +174,35 @@ and val_tuple ?name vs ctx o =
    The size of vv corresponds to the number of non-constant
    constructors, and the size of vv.(i) is the expected arity of the
    i-th non-constant constructor. *)
-and val_sum name cc vv ctx o =
+and val_sum name cc vv mem ctx o =
   let ctx = ctx/CtxType name in
-  if Obj.is_block o then
-    (val_block ctx o;
+  if is_block mem o then
+    (val_block mem ctx o;
     let n = Array.length vv in
-    let i = Obj.tag o in
+    let i = tag mem o in
     let ctx' = if n=1 then ctx else ctx/CtxTag i in
-    if i < n then val_tuple vv.(i) ctx' o
-    else fail ctx' o ("sum: unexpected tag"))
-  else if Obj.is_int o then
-    let (n:int) = Obj.magic o in
+    if i < n then val_tuple vv.(i) mem ctx' o
+    else fail mem ctx' o ("sum: unexpected tag"))
+  else if is_int mem o then
+    let (n:int) = get_int mem o in
     (if n<0 || n>=cc then
-      fail ctx o ("bad constant constructor "^string_of_int n))
-  else fail ctx o "not a sum"
+      fail mem ctx o ("bad constant constructor "^string_of_int n))
+  else fail mem ctx o "not a sum"
 
 (* Check the o is an array of values satisfying f. *)
-and val_array v ctx o =
-  val_block (ctx/CtxType "array") o;
-  for i = 0 to Obj.size o - 1 do
-    val_gen v ctx (Obj.field o i)
+and val_array v mem ctx o =
+  val_block mem (ctx/CtxType "array") o;
+  for i = 0 to size mem o - 1 do
+    val_gen v mem ctx (field mem o i)
   done
 
-and val_uint63 ctx o =
-  if not (Uint63.is_uint63 o) then
-    fail ctx o "not a 63-bit unsigned integer"
+and val_uint63 mem ctx o =
+  if not (is_uint63 mem o) then
+    fail mem ctx o "not a 63-bit unsigned integer"
 
-and val_float64 ctx o =
-  if not (Float64.is_float64 o) then
-    fail ctx o "not a 64-bit float"
+and val_float64 mem ctx o =
+  if not (is_float64 mem o) then
+    fail mem ctx o "not a 64-bit float"
 
 let print_frame = function
 | CtxType t -> t
@@ -149,12 +210,11 @@ let print_frame = function
 | CtxField i -> Printf.sprintf "fld=%i" i
 | CtxTag i -> Printf.sprintf "tag=%i" i
 
-let validate debug v x =
-  let o = Obj.repr x in
-  try val_gen v mt_ec o
+let validate ~debug v (o, mem) =
+  try val_gen v mem mt_ec o
   with ValidObjError(msg,ctx,obj) ->
     (if debug then
       let ctx = List.rev_map print_frame ctx in
       print_endline ("Context: "^String.concat"/"ctx);
-      pr_obj obj);
+      pr_obj mem obj);
     failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")")
diff --git a/checker/validate.mli b/checker/validate.mli
index fbcea3121b..584ea6ed95 100644
--- a/checker/validate.mli
+++ b/checker/validate.mli
@@ -8,4 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val validate : bool -> Values.value -> 'a -> unit
+open Analyze
+
+val validate : debug:bool -> Values.value -> data * obj LargeArray.t -> unit