diff options
Diffstat (limited to 'driver/Interp_ext.ml')
-rw-r--r-- | driver/Interp_ext.ml | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml new file mode 100644 index 00000000..2fc12b87 --- /dev/null +++ b/driver/Interp_ext.ml @@ -0,0 +1,121 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Implementing external functions for the reference interpreter. + The only such function currently implemented is "printf". *) + +open Format +open Camlcoq +open AST +open Values +open Memory + +(* Extract a string from a global pointer *) + +let extract_string m blk ofs = + let b = Buffer.create 80 in + let rec extract blk ofs = + match Mem.load Mint8unsigned m blk ofs with + | Some(Vint n) -> + let c = Char.chr (Z.to_int n) in + if c = '\000' then begin + Some(Buffer.contents b) + end else begin + Buffer.add_char b c; + extract blk (Z.succ ofs) + end + | _ -> + None in + extract blk ofs + +(* Emulation of printf *) + +(* All ISO C 99 formats except size modifier [L] (long double) *) + +let re_conversion = Str.regexp + "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\|ll\\)?\\([aAcdeEfgGinopsuxX%]\\)" + +external format_float: string -> float -> string + = "caml_format_float" +external format_int32: string -> int32 -> string + = "caml_int32_format" +external format_int64: string -> int64 -> string + = "caml_int64_format" + +let do_printf m fmt args = + + let b = Buffer.create 80 in + let len = String.length fmt in + + let opt_search_forward pos = + try Some(Str.search_forward re_conversion fmt pos) + with Not_found -> None in + + let rec scan pos args = + if pos < len then begin + match opt_search_forward pos with + | None -> + Buffer.add_substring b fmt pos (len - pos) + | Some pos1 -> + Buffer.add_substring b fmt pos (pos1 - pos); + let pat = Str.matched_string fmt + and conv = Str.matched_group 3 fmt + and pos' = Str.match_end() in + match args, conv.[0] with + | _, '%' -> + Buffer.add_char b '%'; + scan pos' args + | [], _ -> + Buffer.add_string b "<missing argument>"; + scan pos' [] + | Vint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> + Buffer.add_string b (format_int32 pat (camlint_of_coqint i)); + scan pos' args' + | Vfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> + Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f)); + scan pos' args' + | Vlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> + let pat = Str.replace_first (Str.regexp "ll") "" pat in + Buffer.add_string b (format_int64 pat (camlint64_of_coqint i)); + scan pos' args' + | Vptr(blk, ofs) :: args', 's' -> + Buffer.add_string b + (match extract_string m blk ofs with + | Some s -> s + | None -> "<bad string>"); + scan pos' args' + | Vptr(blk, ofs) :: args', 'p' -> + Printf.bprintf b "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs); + scan pos' args' + | _ :: args', _ -> + Buffer.add_string b "<formatting error>"; + scan pos' args' + end + in scan 0 args; Buffer.contents b + +(* Implementation of external functions *) + +let re_stub = Str.regexp "\\$[ifl]*$" + +let chop_stub name = Str.replace_first re_stub "" name + +let do_external_function id sg args m = + match chop_stub(extern_atom id), args with + | "printf", Vptr(b, ofs) :: args' -> + begin match extract_string m b ofs with + | Some fmt -> print_string (do_printf m fmt args') + | None -> print_string "<bad printf>\n" + end; + flush stdout; + Some Vundef + | _ -> + None |