Désérialisation typée pour Objective Caml

Cette page est en cours de construction :
TODO : fichier LISEZMOI;

Exemple

# let v = (1.2, 1);;
v : ( float * int ) = (1.2 , 1)
# let str = Marshal.to_string v [] ;;
str : string = "..."
# SafeUnmarshal.from_string [^ ( float * int ) ^] str 0 ;;
- : ( float * int ) = (1.2, 1)
# SafeUnmarshal.from_string [^ ( int * float ) ^] str 0 ;;
Exception: SafeUnmarshal.Fail

Pour un exemple plus complet, c'est par ici.

Pour les pressés :
./make_source_tree.sh ocaml-ty && cd ocaml-ty && ./configure && make world && make -C otherlibs/safe_unmarshaling top

Principe

Cette désérialisation sûre est obtenue sans modification du runtime d'ocaml, et notamment sans modifier le format actuel de sérialisation. La fonction de désérialisation est typée en passant explicitement un argument supplémentaire représentant le type attendu pour la valeur à lire. La vérification dynamique de compatibilité entre la valeur et le type est effectuée par un parcours exhaustif où les cycles et le partage introduisent du polymorphisme.

Pour cela il a fallu d'abord ajouter :

au langage :
- une construction syntaxique pour représenter des types statiques comme des valeurs manipulables durant l'exécution :
  
  expr ::= ...
  
  ∣ [^ typexpr ^]
- un type prédéfini 'a tyrepr tel que la valeur [^ τ ^] soit du type τ tyrepr ;
à la bibliothèque de base :
- un module Ty pour déconstruire et explorer les valeurs de type 'a tyrepr.

L'algorithme de vérification de type est ensuite réalisé par une bibliothèque nommée SafeUnmarshal. Pour plus de précisions sur le fonctionnement de cet algorithme voir les références.

Comment tester ?

Attention, ce code est de qualité alpha ... et n'a été prouvé correct que sur le papier, pour tout les nouveaux bugs, écrivez à : gregoire.henry AT pps.jussieu.fr

Le code est disponible sous la forme de deux patches (1) puis (2) pour la branche 3.09 du compilateur Objective Caml. Il est nécessaire de bootstraper le compilateur avant et après l'application du second patch : make core && make bootstrap -- ou bien, de copier ces versions déjà bootstrapées d'ocamlc et d'ocamllex dans le répertoire ocaml/boot/ (avant ou après l'application des patches ... mais avant de compiler !).

Pour obtenir directement une version patchée et directement compilable du compilateur de l'INRIA, il est aussi possible au choix :

d'utiliser ce petit script : make_source_tree.sh dest_dir, qui récupère la version CVS d'ocaml à partir de laquelle les patches ont été générés, puis patche le tout et place les versions bootstrappées aux bons endroits !
de télécharger cette volumineuse -- mais complète -- archive tgz et suivre les instructions de son fichier LISEZMOI.

Exemples complets

Chargement.

$ ocaml safeUnmarshal.cma
Objective Caml version 3.09.2+ty1

# open SafeUnmarshal;;
# from_string;;
- : 'a tyrepr -> string -> int -> 'a

Fonction de test.

# let test ty obj =
  try
    let _ = from_string ty (Marshal.to_string obj []) 0 in true
  with Fail -> false;;
- : 'a tyrepr -> 'b -> bool = <fun>
# test [^ int ^] 3;;
- : bool = true
# test [^ int ^] 3.4;;
- : bool = false
# test [^ int ^] false;;
- : bool = true

Type somme.

# type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree;;
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
# let t = Node (Node (Leaf, 3, Leaf), 5, Leaf);;
val t : int tree = Node (Node (Leaf, 3, Leaf), 5, Leaf)
# test [^ int tree ^] t;;
- : bool = true
# test [^ bool tree ^] t;;
- : bool = false

Type enregistrement.

# type point = { x: int; y: int };;
type point = { x : int; y : int; }
# type point3D = { a: int; b: int; c:int };;
type point3D = { a : int; b : int; c : int; }
# let p = { x=4; y=0 };;
val p : point = {x = 4; y = 0}
# test [^ point ^] p;;
- : bool = true
# test [^ point3D ^] p;;
- : bool = false

Type abstraits.

# module M : sig type t val v : t end = struct
    type t = (int * float) list
    let v = [(1,1.2);(4,3.)]
  end;;
module M : sig type t val v : t end
# test [^ M.t ^] M.v;;
- : bool = true
# test [^ M.t ^] p;;
- : bool = false

Partage et cycles

# type ('node, 'leaf) btree =
| Node of ('node, 'leaf) btree * 'node * ('node, 'leaf) btree
| Leaf of 'leaf ;;
type ('a, 'b) btree = Leaf of 'b | Node of ('a, 'b) btree * 'a * ('a, 'b) btree
# let l = Leaf 3;;
val l : ('a, int) btree = Leaf 3
# let t = Node (l, 5.2, l), Node (l, 'a', l);;
val t : (float, int) btree * (char, int) btree =
(Node (Leaf 3, 5.2, Leaf 3), Node (Leaf 3, 'a', Leaf 3))
# test [^ (float, int) btree * (char, int) btree ^] t;;
- : bool = true
# let rec t2 = Node ( t2, "E", t2 );;
val t2 : (string, 'a) btree = ...
# test [^ (string, 'a) btree ^] t2;;
- : bool = true
# test [^ (string, int) btree * (string, float) btree ^] (t2, t2);;
- : bool = true

Références

# let r = ref [];;
val r : '_a list ref = {contents = []}
# test [^ float list ref ^] r;;
- : bool = true
# test [^ int list ref ^] r;;
- : bool = true
# test [^ int list ref * float list ref ^] (r,r);;
- : bool = false

Conversion étrange

# copy [^ int ^] true;;
- : int = 1
# copy [^ bool ^] 0;;
- : bool = false
# copy [^ bool ^] 2;;
Exception: SafeUnmarshal.Fail

# copy [^ point ^] (1,2);;
- : point = {x = 1; y = 2}
# copy [^ point3D ^] (1,2);;
Exception: SafeUnmarshal.Fail

# copy [^ M.t ^] [];;
- : M.t = <abstr>
# copy [^ M.t ^] [(1,2.3)];;
- : M.t = <abstr>
# copy [^ M.t ^] [1;2;3];;
Exception: SafeUnmarshal.Fail

# copy [^ string tree ^] t2;;
- : string tree = ...
# copy [^ string tree ^] l;;
Exception: SafeUnmarshal.Fail.

Caractéristiques et limitations

On sait vérifier tous les types primitifs (sauf format4, lazy_t, exn et ->) ainsi que tous les types construits.

On sait vérifier les types abstraits lorsqu'ils sont implémentés en ocaml, mais pas lorsqu'ils correspondent à des blocks "Custom".

Lorsque l'on compile un projet qui contient un fichier d'interface sans implémentation, il faut ou bien créer une implémentation (lien symbolique sur le .mli) ou alors utiliser l'option -noty pour compiler les .ml dépendant de cet interface.

Le support des variants polymorphes est encore partiel.

Les informations de variance ne sont pas prises en compte.

L'algorithme de vérification ne sait pas vérifier les fermetures, par conséquent il n'est pas possible de désérialiser une fonction ou un objet.

Le filtrage de motifs n'est pas possible sur les valeurs de type 'a tyrepr.

Clairement, la syntaxe des valeurs de type 'a tyrepr pourrait être étendue avec un mécanisme d'anti-quotation. Dans une future version...

Références

Ce code est issue du stage de deuxième année de Master que j'ai effectué en 2005 sous la direction de Michel Mauny et d'Emmanuel Chailloux. Mon rapport de stage est disponible avec ceux de mes voisins de classe sur le site web du MPRI, mais depuis cette période de stress une version article sans doute plus lisible a été publiée aux JFLA'2006, voici aussi les transparents de l'exposé.

expr	::=	...
	∣	[^ typexpr ^]