checker/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

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* 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()

(**************************************************************************)
(* 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 * Obj.t
let fail ctx o s = raise (ValidObjError(s,ctx,o))

type func = error_context -> Obj.t -> unit

(* 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 ()
  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"
  | String ->
    (try val_tag Obj.string_tag ctx o
     with Failure _ -> fail 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

(* 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 =
  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
  else
    fail ctx o
      ("tuple size: found "^string_of_int (Obj.size 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 ctx o =
  let ctx = ctx/CtxType name in
  if Obj.is_block o then
    (val_block ctx o;
    let n = Array.length vv in
    let i = Obj.tag 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 n<0 || n>=cc then
      fail ctx o ("bad constant constructor "^string_of_int n))
  else fail 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)
  done

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 debug v x =
  let o = Obj.repr x in
  try val_gen v mt_ec o
  with ValidObjError(msg,ctx,obj) ->
    if debug then begin
      let ctx = List.rev_map print_frame ctx in
      print_endline ("Validation failed: "^msg);
      print_endline ("Context: "^String.concat"/"ctx);
      pr_obj obj
    end;
    failwith "vo structure validation failed"