Revised modeling of external functions and built-in functions: just axiomatize

them.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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