diff options
| author | vgross | 2010-03-23 16:26:17 +0000 |
|---|---|---|
| committer | vgross | 2010-03-23 16:26:17 +0000 |
| commit | 4139b04506f80f5f7acddbe9df7027f4b5d0dc8a (patch) | |
| tree | abf34783bd7946c12656a17d0d49ed8280a19589 /lib | |
| parent | 96cbb1ef0a7bcc23e8fe29fe4b6e226acc5b16e5 (diff) | |
infrastructure for safe marshal-based IPC
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12879 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/safe_marshal.ml | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/lib/safe_marshal.ml b/lib/safe_marshal.ml new file mode 100644 index 0000000000..88101b5d2f --- /dev/null +++ b/lib/safe_marshal.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i) +let bohcnv = Array.init 256 (fun i -> i - + (if 0x30 <= i then 0x30 else 0) - + (if 0x41 <= i then 0x7 else 0) - + (if 0x61 <= i then 0x20 else 0)) + +let hex_of_bin ch = hobcnv.(int_of_char ch) +let bin_of_hex s = bohcnv.(char_of_int s[0]) * 16 + bohcnv.(char_of_int s[1]) + +let send cout expr = + let mshl_expr = Marshal.to_string expr [] in + let payload = Buffer.create (String.length mshl_expr * 2) in + String.iter (fun c -> Buffer.add_string payload (hex_of_bin c)) mshl_expr; + Buffer.add_char payload '\n'; + output_string cout (Buffer.contents payload); + flush cout + + +let receive cin = + let payload = input_line cin in + let mshl_expr_len = String.length payload / 2 in + let mshl_expr = Buffer.create mshl_expr_len in + let buf = String.create 2 in + for i = 0 to mshl_expr_len - 1 do + String.blit payload (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex buf) + done; + Marshal.from_string (Buffer.contents mshl_expr) 0 + |
