From 726c815f2070e9ae40bdf6df1d4e63b4a60b6e09 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Nov 2013 10:01:21 +0000 Subject: 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 --- driver/Interp.ml | 58 ++++++++++++++---------- driver/Interp_ext.ml | 121 --------------------------------------------------- 2 files changed, 36 insertions(+), 143 deletions(-) delete mode 100644 driver/Interp_ext.ml (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index 4777900..5fcca0b 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -12,14 +12,11 @@ (* Interpreting CompCert C sources *) -type caml_float = float - open Format open Camlcoq open Datatypes open AST open Integers -open Floats open Values open Memory open Globalenvs @@ -281,12 +278,12 @@ let rec purge_seen nextblock seen = (* Extract a string from a global pointer *) -let extract_string ge m id ofs = +let extract_string m blk ofs = let b = Buffer.create 80 in let rec extract blk ofs = - match Memory.Mem.load Mint8unsigned m blk ofs with + match Mem.load Mint8unsigned m blk ofs with | Some(Vint n) -> - let c = Char.chr (Int32.to_int (camlint_of_coqint n)) in + let c = Char.chr (Z.to_int n) in if c = '\000' then begin Some(Buffer.contents b) end else begin @@ -295,9 +292,7 @@ let extract_string ge m id ofs = end | _ -> None in - match Genv.find_symbol ge id with - | None -> None - | Some blk -> extract blk ofs + extract blk ofs (* Emulation of printf *) @@ -306,14 +301,14 @@ let extract_string ge m id ofs = let re_conversion = Str.regexp "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\|ll\\)?\\([aAcdeEfgGinopsuxX%]\\)" -external format_float: string -> caml_float -> string +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 ge m fmt args = +let do_printf m fmt args = let b = Buffer.create 80 in let len = String.length fmt in @@ -339,24 +334,24 @@ let do_printf ge m fmt args = | [], _ -> Buffer.add_string b ""; scan pos' [] - | EVint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> + | Vint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> Buffer.add_string b (format_int32 pat (camlint_of_coqint i)); scan pos' args' - | EVfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> + | Vfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f)); scan pos' args' - | EVlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> + | 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' - | EVptr_global(id, ofs) :: args', 's' -> + | Vptr(blk, ofs) :: args', 's' -> Buffer.add_string b - (match extract_string ge m id ofs with + (match extract_string m blk ofs with | Some s -> s | None -> ""); scan pos' args' - | EVptr_global(id, ofs) :: args', 'p' -> - Printf.bprintf b "<&%s%+ld>" (extern_atom id) (camlint_of_coqint ofs); + | 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 ""; @@ -364,10 +359,29 @@ let do_printf ge m fmt args = end in scan 0 args; Buffer.contents b -(* Implementing external functions producing observable events *) +(* Implementation of external functions *) + +let re_stub = Str.regexp "\\$[ifl]*$" + +let chop_stub name = Str.replace_first re_stub "" name let (>>=) opt f = match opt with None -> None | Some arg -> f arg +let do_external_function id sg ge w args m = + match chop_stub(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 -> + Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) + | _ -> + None + +let do_inline_assembly txt ge w args m = None + +(* Implementing external functions producing observable events *) + let rec world ge m = Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) @@ -388,7 +402,7 @@ and world_vstore ge m chunk id ofs ev = let do_event p ge time w ev = if !trace >= 1 then - fprintf p "@[Time %d: observable event: %a@]@." + fprintf p "@[Time %d: observable event:@ @[%a@]@]@." time print_event ev; (* Return new world after external action *) match ev with @@ -429,7 +443,7 @@ let diagnose_stuck_expr p ge w f a kont e m = | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs | _, _ -> false in if found then true else begin - let l = Cexec.step_expr ge e w k a m in + let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin PrintCsyntax.print_pointer_hook := print_pointer ge e; fprintf p "@[Stuck subexpression:@ %a@]@." @@ -464,7 +478,7 @@ let do_step p prog ge time (s, w) = | First | Random -> exit (Int32.to_int (camlint_of_coqint r)) end | None -> - let l = Cexec.do_step ge w s in + let l = Cexec.do_step ge do_external_function do_inline_assembly w s in if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin pp_set_max_boxes p 1000; fprintf p "@[Stuck state: %a@]@." print_state (prog, ge, s); diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml deleted file mode 100644 index 2fc12b8..0000000 --- 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 ""; - 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 -> ""); - 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 ""; - 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 "\n" - end; - flush stdout; - Some Vundef - | _ -> - None -- cgit v1.2.3