SafeUnmarshal: more problems

SafeUnmarshal: more problems

[Hendrik Tews]

Hi,

in the context of olmar I am using the SafeUnmarshal module to
check if some ocaml value created in C/C++ is consistent with its
supposed type. I came across the following two problems:

1. tyrepr's cannot be build in the program:

  Assume I have a value v which is supposed to have type "blah list"
  and suppose that SafeUnmarshal.check v [^ blah list ^] fails.

  I would now like to diagnose whether the problem is in the list
  structure or in one of the blah's inside the list. I would like
  to write code like this

    let check_list (value : 'a list) (list_elem_type : 'a tyrepr) =
      if SafeUnmarshal.check value (Ty.apply list_elem_type [^ list ^])
      then 
	printf "everything fine\n"
      else if SafeUnmarshal.check value [^ 'a list ^]
      then begin
	printf "list structure ok, problem inside\n";
	(* check all the elements of the list *)
	end 
      else
	printf "list structure broken";

  In this code (Ty.apply list_elem_type [^ list ^]) should give
  somthing like [^ list_elem_type list ^]. However, there is
  nothing to build values of type tyrepr and 
  [^ list_elem_type list ^] does not work because list_elem_type
  is a variable and not an ocaml type expression.

  I would even like to abstract away the list in the code above,
  because I need the same for options, references and hash
  tables.

  What is missing, is function Ty.description -> tyrepr.


2. Checking polymorphic types

  Point 1 makes it clear that it makes sense to check against
  poymorphic types, even against invalid polymorphic types. With
  the latter I mean that I want

     SafeUnmarshal.check (ref 2) [^ 'a ref ^]

  to return true, because the reference cell is ok, EVEN THOUGH I
  want 

     SafeUnmarshal.from_string (Marshal.to_string (ref 2) []) [^ 'a ref ^]

  to fail, because (ref 2) cannot safely given the type 'a ref.
  In the current source SafeUnmarshal.from_string calls check, so
  it is impossible to satisfay both requirements.

  At the moment 

     SafeUnmarshal.check (ref 2) [^ 'a ref ^]

  fails, because there Check.check_int maps Tabstract to false
  (similar to SafeUnmarshal.check 2 [^ 'a ^]). However, one can
  also find the following code inside Check.check_block (which is
  actually excuted before check_int fails:

    | Trecord ntys when tag = 0 -> 
	Array.length ntys = size && 
	ObjHelpers.for_all2 
	  (fun obj (_,mut,ty) ->
	     let ty = cut_head_quantification ty in
	     if mut && not (is_monomorphic ty) then false
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
	     else check_obj obj ty) 
	  obj ntys

  read mut as mutable (which apprears to be true for mutable
  fields) then the marked line seems to be a check that mutable
  fields must have monomorphic type. The trouble is only that
  is_monomorphic returns true on [^ 'a ref ^].

  Is this last point a bug or a feature?

  Assuming it is a bug, how can I check for a mutable data
  structure, such as a hash table, that the top level structure
  is ok?


Finally I would like to stress that the problems mentioned here
(as well as the onces mentioned in August and other bugs (try
SafeUnmarshal.check [| 2 |] [^ int array ^] )) come all from the
use of catch all cases that deliver a value, like

  and is_monomorphic_desc context desc =
    match desc with
	  ....
    | ty -> true


  and check_int i ty =
    match Ty.repr ty with
	....
    | _ -> false


I would like to suggest again to use only 

    | _ -> assert false

because the careful analysis necessary to justify the catch all
cases has apparently not been done (and will not be redone on
every change of the source). 

Using assert false would also safe the users a lot of time,
because they would immediately see that they hit an unsupported
feature. 


Bye,

Hendrik