diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Interp.ml | 23 | ||||
| -rw-r--r-- | driver/Interp_ext.ml | 121 |
2 files changed, 124 insertions, 20 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index 6f9336e..4777900 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -364,11 +364,7 @@ let do_printf ge m fmt args = end in scan 0 args; Buffer.contents b -(* Implementing external functions *) - -let re_stub = Str.regexp "\\$[ifl]*$" - -let chop_stub name = Str.replace_first re_stub "" name +(* Implementing external functions producing observable events *) let (>>=) opt f = match opt with None -> None | Some arg -> f arg @@ -376,17 +372,7 @@ let rec world ge m = Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) and world_io ge m id args = - match chop_stub(extern_atom id), args with - | "printf", EVptr_global(id, ofs) :: args' -> - flush stderr; - begin match extract_string ge m id ofs with - | Some fmt -> print_string (do_printf ge m fmt args') - | None -> print_string "<bad printf>\n" - end; - flush stdout; - Some(EVint Integers.Int.zero, world ge m) - | _, _ -> - None + None and world_vload ge m chunk id ofs = Genv.find_symbol ge id >>= fun b -> @@ -567,8 +553,7 @@ let rec explore_all p prog ge seen queue = executing events. Volatile variables are turned into non-volatile ones, so that reads and writes can be performed. - Readonly variables are kept, for string literals in particular. - Writable variables are turned into empty vars, so that + Other variables are turned into empty vars, so that reads and writes just fail. Functions are preserved, although they are not used. *) @@ -579,8 +564,6 @@ let world_program prog = let gv' = if gv.gvar_volatile then {gv with gvar_readonly = false; gvar_volatile = false} - else if gv.gvar_readonly then - gv else {gv with gvar_init = []} in (id, Gvar gv') diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml new file mode 100644 index 0000000..2fc12b8 --- /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 |