1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
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
|
