aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml49
-rw-r--r--checker/validate.ml228
-rw-r--r--checker/validate.mli4
-rw-r--r--checker/values.ml7
-rw-r--r--checker/values.mli2
-rw-r--r--checker/votour.ml4
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:34:47 +0000