From ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 3 Nov 2014 17:40:22 +0100
Subject: Add Genv.public_symbol operation. Restrict pointer event values to
 public global names. Update proofs accordingly.  PowerPC and ARM need
 updating.

---
 driver/Interp.ml | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'driver/Interp.ml')

diff --git a/driver/Interp.ml b/driver/Interp.ml
index 1291d70c..9bb9d237 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -380,13 +380,33 @@ let do_printf m fmt args =
 
 let (>>=) opt f = match opt with None -> None | Some arg -> f arg
 
+(* Like eventval_of_val, but accepts static globals as well *)
+
+let convert_external_arg ge v t =
+  match v, t with
+  | Vint i, AST.Tint -> Some (EVint i)
+  | Vfloat f, AST.Tfloat -> Some (EVfloat f)
+  | Vsingle f, AST.Tsingle -> Some (EVsingle f)
+  | Vlong n, AST.Tlong -> Some (EVlong n)
+  | Vptr(b, ofs), AST.Tint -> 
+      Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
+  | _, _ -> None
+
+let rec convert_external_args ge vl tl =
+  match vl, tl with
+  | [], [] -> Some []
+  | v1::vl, t1::tl ->
+      convert_external_arg ge v1 t1 >>= fun e1 ->
+      convert_external_args ge vl tl >>= fun el -> Some (e1 :: el)
+  | _, _ -> None
+
 let do_external_function id sg ge w args m =
   match extern_atom id, args with
   | "printf", Vptr(b, ofs) :: args' ->
       extract_string m b ofs >>= fun fmt ->
       print_string (do_printf m fmt args');
       flush stdout;
-      Cexec.list_eventval_of_val ge args sg.sig_args >>= fun eargs ->
+      convert_external_args ge args sg.sig_args >>= fun eargs ->
       Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m)
   | _ ->
       None
-- 
cgit