Merge PR #11411: Checker validation now performed over reified data

Reviewed-by: SkySkimmer

6 files changed, 178 insertions, 116 deletions

diff --git a/checker/check.ml b/checker/check.ml
index ffb2928d55..4ac5c56732 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -294,14 +294,22 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe
 (* Dependency graph *)
 let depgraph = ref LibraryMap.empty
 
-let marshal_in_segment f ch =
-  try
-    let stop = input_binary_int ch in
-    let v = Analyze.instantiate (Analyze.parse_channel ch) in
-    let digest = Digest.input ch in
+let marshal_in_segment ~validate ~value f ch =
+  if validate then
+    let v, stop, digest =
+      try
+        let stop = input_binary_int ch in
+        let v = Analyze.parse_channel ch in
+        let digest = Digest.input ch in
+        v, stop, digest
+      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
     Obj.obj v, stop, digest
-  with _ ->
-    user_err (str "Corrupted file " ++ quote (str f))
+  else
+    System.marshal_in_segment f ch
 
 let skip_in_segment f ch =
   try
@@ -312,30 +320,26 @@ let skip_in_segment f ch =
   with _ ->
     user_err (str "Corrupted file " ++ quote (str f))
 
-let marshal_or_skip ~intern_mode f ch =
-  if intern_mode <> Dep then
-    let v, pos, digest = marshal_in_segment f ch in
+let marshal_or_skip ~validate ~value f ch =
+  if validate then
+    let v, pos, digest = marshal_in_segment ~validate ~value f ch in
     Some v, pos, digest
   else
     let pos, digest = skip_in_segment f ch in
     None, pos, digest
 
 let intern_from_file ~intern_mode (dir, f) =
-  let validate a b c = if intern_mode <> Dep then Validate.validate a b c in
+  let validate = intern_mode <> Dep in
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
-      let marshal_in_segment f ch = if intern_mode <> Dep
-        then marshal_in_segment f ch
-        else System.marshal_in_segment f ch
-      in
       let ch = System.with_magic_number_check raw_intern_library f in
-      let (sd:summary_disk), _, digest = marshal_in_segment f ch in
-      let (md:library_disk), _, digest = marshal_in_segment f ch in
-      let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in
-      let (tasks:'a option), _, _ = marshal_in_segment f ch in
+      let (sd:summary_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_libsum f ch in
+      let (md:library_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_lib f ch in
+      let (opaque_csts:seg_univ option), _, udg = marshal_in_segment ~validate ~value:Values.v_univopaques f ch in
+      let (tasks:'a option), _, _ = marshal_in_segment ~validate ~value:Values.(Opt Any) f ch in
       let (table:seg_proofs option), pos, checksum =
-        marshal_or_skip ~intern_mode f ch in
+        marshal_or_skip ~validate ~value:Values.v_opaquetable f ch in
       (* Verification of the final checksum *)
       let () = close_in ch in
       let ch = open_in_bin f in
@@ -354,12 +358,7 @@ let intern_from_file ~intern_mode (dir, f) =
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
-      validate !Flags.debug Values.v_univopaques opaque_csts;
       end;
-      (* Verification of the unmarshalled values *)
-      validate !Flags.debug Values.v_libsum sd;
-      validate !Flags.debug Values.v_lib md;
-      validate !Flags.debug Values.(Opt v_opaquetable) table;
       Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
         if opaque_csts <> None then Safe_typing.Dvivo (digest,udg)
diff --git a/checker/validate.ml b/checker/validate.ml
index 070a112bb6..6ffc43394b 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,115 @@ 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_int64 mem o = 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
+  | Int64 -> val_int64 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 +172,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_int64 mem ctx o =
+  if not (is_int64 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 +208,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
diff --git a/checker/values.ml b/checker/values.ml
index df6a9136c8..fff166f27b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -34,7 +34,7 @@ type value =
   | Dyn
 
   | Proxy of value ref
-  | Uint63
+  | Int64
   | Float64
 
 let fix (f : value -> value) : value =
@@ -129,6 +129,9 @@ let v_cast = v_enum "cast_kind" 4
 let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
 let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 
+let v_uint63 =
+  if Sys.word_size == 64 then Int else Int64
+
 let rec v_constr =
   Sum ("constr",0,[|
     [|Int|]; (* Rel *)
@@ -148,7 +151,7 @@ let rec v_constr =
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
     [|v_proj;v_constr|]; (* Proj *)
-    [|Uint63|]; (* Int *)
+    [|v_uint63|]; (* Int *)
     [|Float64|] (* Int *)
   |])
 
diff --git a/checker/values.mli b/checker/values.mli
index ec3b91d5dd..15d307ee29 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -38,7 +38,7 @@ type value =
   | Proxy of value ref
   (** Same as the inner value, used to define recursive types *)
 
-  | Uint63
+  | Int64
   | Float64
 
 (** NB: List and Opt have their own constructors to make it easy to
diff --git a/checker/votour.ml b/checker/votour.ml
index 9adcc874ac..452809f7bb 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -157,7 +157,7 @@ let rec get_name ?(extra=false) = function
   |Annot (s,v) -> s^"/"^get_name ~extra v
   |Dyn -> "<dynamic>"
   | Proxy v -> get_name ~extra !v
-  | Uint63 -> "Uint63"
+  | Int64 -> "Int64"
   | Float64 -> "Float64"
 
 (** For tuples, its quite handy to display the inner 1st string (if any).
@@ -263,7 +263,7 @@ let rec get_children v o pos = match v with
     end
   |Fail s -> raise Forbidden
   | Proxy v -> get_children !v o pos
-  | Uint63 -> raise Exit
+  | Int64 -> raise Exit
   | Float64 -> raise Exit
 
 let get_children v o pos =