aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorvgross2010-03-23 16:26:17 +0000
committervgross2010-03-23 16:26:17 +0000
commit4139b04506f80f5f7acddbe9df7027f4b5d0dc8a (patch)
treeabf34783bd7946c12656a17d0d49ed8280a19589 /lib
parent96cbb1ef0a7bcc23e8fe29fe4b6e226acc5b16e5 (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.ml39
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
+