package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file validate.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (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 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 *)

type error_frame =
| CtxAnnot of string
| CtxType of string
| CtxField of int
| CtxTag of int

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 * 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 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 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 mem ctx o
     with Failure _ -> fail mem ctx o "expected a string")
  | Any -> ()
  | 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 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 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 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,
   or a constructed variant. each element of vv is an array of
   value representations of the constructor arguments.
   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 mem ctx o =
  let ctx = ctx/CtxType name in
  if is_block mem o then
    (val_block mem ctx o;
    let n = Array.length vv 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) 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 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 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_int64 mem ctx o =
  if not (is_int64 mem o) then
    fail mem ctx o "not a 63-bit unsigned integer"

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
| CtxAnnot t -> t
| CtxField i -> Printf.sprintf "fld=%i" i
| CtxTag i -> Printf.sprintf "tag=%i" i

let validate v (o, mem) =
  try val_gen v mem mt_ec o
  with ValidObjError(msg,ctx,obj) ->
    let rctx = List.rev_map print_frame ctx in
    print_endline ("Context: "^String.concat"/"rctx);
    pr_obj mem obj;
    failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")")
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct