diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-18 10:01:21 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-18 10:01:21 +0000 |
commit | 726c815f2070e9ae40bdf6df1d4e63b4a60b6e09 (patch) | |
tree | 037a214ed6eb1b519ce5fd9fe2617749b77ce9f5 /driver/Interp_ext.ml | |
parent | 0be44be49c5be412a9d23e37c7b4554a9049ecbe (diff) | |
download | compcert-726c815f2070e9ae40bdf6df1d4e63b4a60b6e09.tar.gz compcert-726c815f2070e9ae40bdf6df1d4e63b4a60b6e09.zip |
Revised semantics of external functions, continued:
- Also axiomatize the semantics of inline asm
- In Cexec, revised parameterization over do_external_function
- In Interp.ml, matching changes + suppression of Interp_ext.ml
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2370 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Interp_ext.ml')
-rw-r--r-- | driver/Interp_ext.ml | 121 |
1 files changed, 0 insertions, 121 deletions
diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml deleted file mode 100644 index 2fc12b87..00000000 --- a/driver/Interp_ext.ml +++ /dev/null @@ -1,121 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 |