Added animation of the CompCert C semantics (ccomp -interp)

test/regression: int main() so that interpretation works
Revised once more implementation of __builtin_memcpy (to check for PPC & ARM)


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

4 files changed, 510 insertions, 60 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 2a96c38..87de59f 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -22,6 +22,7 @@ let option_fbitfields = ref false
 let option_fvararg_calls = ref true
 let option_fpacked_structs = ref false
 let option_fmadd = ref false
+let option_fsse = ref true
 let option_dparse = ref false
 let option_dcmedium = ref false
 let option_dclight = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
index a51cd8f..37a187e 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -24,6 +24,7 @@ Require Import Smallstep.
 Require Csyntax.
 Require Csem.
 Require Cstrategy.
+Require Cexec.
 Require Clight.
 Require Csharpminor.
 Require Cminor.
@@ -82,8 +83,8 @@ Require Reloadtyping.
 Require Stackingproof.
 Require Stackingtyping.
 Require Asmgenproof.
+
 (** Pretty-printers (defined in Caml). *)
-Parameter print_Csyntax: Csyntax.program -> unit.
 Parameter print_Clight: Clight.program -> unit.
 Parameter print_Cminor: Cminor.program -> unit.
 Parameter print_RTL: RTL.fundef -> unit.
@@ -180,13 +181,13 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program :=
 
 Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
   OK p 
-   @@ print print_Csyntax
   @@@ SimplExpr.transl_program
   @@@ transf_clight_program.
 
-(** Force [Initializers] to be extracted as well. *)
+(** Force [Initializers] and [Cexec] to be extracted as well. *)
 
 Definition transl_init := Initializers.transl_init.
+Definition cexec_do_step := Cexec.do_step.
 
 (** The following lemmas help reason over compositions of passes. *)
 
@@ -403,7 +404,7 @@ Theorem transf_cstrategy_program_correct:
 Proof.
   intros.
   assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)).
-  revert H; unfold transf_c_program; simpl. rewrite print_identity.
+  revert H; unfold transf_c_program; simpl.
   caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
   intros EQ1.
   eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 6aa63e0..d5a659d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -62,9 +62,9 @@ let preprocess ifile ofile =
     exit 2
   end
 
-(* From preprocessed C to asm *)
+(* From preprocessed C to Csyntax *)
 
-let compile_c_file sourcename ifile ofile =
+let parse_c_file sourcename ifile =
   Sections.initialize();
   (* Simplification options *)
   let simplifs =
@@ -94,11 +94,22 @@ let compile_c_file sourcename ifile ofile =
     | None -> exit 2
     | Some p -> p in
   flush stderr;
-  (* Prepare to dump Csyntax, Clight, RTL, etc, if requested *)
+  (* Save CompCert C AST if requested *)
+  if !option_dcmedium then begin
+    let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in
+    let oc = open_out ofile in
+    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
+    close_out oc
+  end;
+  csyntax
+
+(* From CompCert C AST to asm *)
+
+let compile_c_ast sourcename csyntax ofile =
+  (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (Filename.chop_suffix sourcename ".c" ^ ext)
                    else None in
-  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
   set_dest PrintClight.destination option_dclight ".light.c";
   set_dest PrintCminor.destination option_dcminor ".cm";
   set_dest PrintRTL.destination_rtl option_drtl ".rtl";
@@ -120,6 +131,11 @@ let compile_c_file sourcename ifile ofile =
   PrintAsm.print_program oc asm;
   close_out oc
 
+(* From C source to asm *)
+
+let compile_c_file sourcename ifile ofile =
+  compile_c_ast sourcename (parse_c_file sourcename ifile) ofile
+
 (* From Cminor to asm *)
 
 let compile_cminor_file ifile ofile =
@@ -178,6 +194,8 @@ let linker exe_name files =
 
 (* Processing of a .c file *)
 
+let option_interp = ref false
+
 let process_c_file sourcename =
   let prefixname = Filename.chop_suffix sourcename ".c" in
   if !option_E then begin
@@ -185,7 +203,10 @@ let process_c_file sourcename =
   end else begin
     let preproname = Filename.temp_file "compcert" ".i" in
     preprocess sourcename preproname;
-    if !option_S then begin
+    if !option_interp then begin
+      let csyntax = parse_c_file sourcename preproname in
+      Interp.execute csyntax
+    end else if !option_S then begin
       compile_c_file sourcename preproname (prefixname ^ ".s")
     end else begin
       let asmname =
@@ -235,57 +256,13 @@ let process_S_file sourcename =
   end;
   prefixname ^ ".o"
 
-(* Command-line parsing *)
+(* Interpretation of a .c file *)
 
-let usage_string =
-"ccomp [options] <source files>
-Recognized source files:
-  .c             C source file
-  .cm            Cminor source file
-  .s             Assembly file
-  .S             Assembly file, to be run through the preprocessor
-  .o             Object file
-  .a             Library file
-Processing options:
-  -E             Preprocess only, send result to standard output
-  -S             Compile to assembler only, save result in <file>.s
-  -c             Compile to object file only (no linking), result in <file>.o
-Preprocessing options:
-  -I<dir>        Add <dir> to search path for #include files
-  -D<symb>=<val> Define preprocessor symbol
-  -U<symb>       Undefine preprocessor symbol
-Language support options (use -fno-<opt> to turn off -f<opt>) :
-  -fbitfields    Emulate bit fields in structs [off]
-  -flonglong     Partial emulation of 'long long' types [on]
-  -fstruct-passing  Emulate passing structs and unions by value [off]
-  -fstruct-assign   Emulate assignment between structs or unions [off]
-  -fvararg-calls Emulate calls to variable-argument functions [on]
-  -fpacked-structs  Emulate packed structs [off]
-Code generation options:
-  -fmadd         Use fused multiply-add and multiply-sub instructions [off]
-  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
-  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
-Tracing options:
-  -dparse        Save C file after parsing and elaboration in <file>.parse.c
-  -dc            Save generated Compcert C in <file>.compcert.c
-  -dclight       Save generated Clight in <file>.light.c
-  -dcminor       Save generated Cminor in <file>.cm
-  -drtl          Save unoptimized generated RTL in <file>.rtl
-  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
-  -dcastopt      Save RTL after cast optimization in <file>.castopt.rtl
-  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
-  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
-  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
-  -dmach         Save generated Mach code in <file>.mach
-  -dasm          Save generated assembly in <file>.s
-Linking options:
-  -l<lib>        Link library <lib>
-  -L<dir>        Add <dir> to search path for libraries
-  -o <file>      Generate executable in <file> (default: a.out)
-General options:
-  -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
-  -v             Print external commands before invoking them
-"
+let execute_c_file sourcename =
+  let preproname = Filename.temp_file "compcert" ".i" in
+  preprocess sourcename preproname
+
+(* Command-line parsing *)
 
 type action =
   | Set of bool ref
@@ -340,6 +317,63 @@ let parse_cmdline spec usage =
     end
   in parse 1
 
+let usage_string =
+"ccomp [options] <source files>
+Recognized source files:
+  .c             C source file
+  .cm            Cminor source file
+  .s             Assembly file
+  .S             Assembly file, to be run through the preprocessor
+  .o             Object file
+  .a             Library file
+Processing options:
+  -E             Preprocess only, send result to standard output
+  -S             Compile to assembler only, save result in <file>.s
+  -c             Compile to object file only (no linking), result in <file>.o
+Preprocessing options:
+  -I<dir>        Add <dir> to search path for #include files
+  -D<symb>=<val> Define preprocessor symbol
+  -U<symb>       Undefine preprocessor symbol
+Language support options (use -fno-<opt> to turn off -f<opt>) :
+  -fbitfields    Emulate bit fields in structs [off]
+  -flonglong     Partial emulation of 'long long' types [on]
+  -fstruct-passing  Emulate passing structs and unions by value [off]
+  -fstruct-assign   Emulate assignment between structs or unions [off]
+  -fvararg-calls Emulate calls to variable-argument functions [on]
+  -fpacked-structs  Emulate packed structs [off]
+Code generation options: (use -fno-<opt> to turn off -f<opt>) :
+  -fmadd         (PowerPC) Use fused multiply-add and multiply-sub instructions [off]
+  -fsse          (IA32) Use SSE2 instructions for some integer operations [on]
+  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
+  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
+Tracing options:
+  -dparse        Save C file after parsing and elaboration in <file>.parse.c
+  -dc            Save generated Compcert C in <file>.compcert.c
+  -dclight       Save generated Clight in <file>.light.c
+  -dcminor       Save generated Cminor in <file>.cm
+  -drtl          Save unoptimized generated RTL in <file>.rtl
+  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
+  -dcastopt      Save RTL after cast optimization in <file>.castopt.rtl
+  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
+  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
+  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
+  -dmach         Save generated Mach code in <file>.mach
+  -dasm          Save generated assembly in <file>.s
+Linking options:
+  -l<lib>        Link library <lib>
+  -L<dir>        Add <dir> to search path for libraries
+  -o <file>      Generate executable in <file> (default: a.out)
+General options:
+  -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
+  -v             Print external commands before invoking them
+Interpreter mode:
+  -interp        Execute given .c files using the reference interpreter
+  -quiet         Suppress diagnostic messages for the interpreter
+  -trace         Have the interpreter produce a detailed trace of reductions
+  -random        Randomize execution order
+  -all           Simulate all possible execution orders
+"
+
 let cmdline_actions =
   let f_opt name ref =
     ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
@@ -367,6 +401,11 @@ let cmdline_actions =
   "-S$", Set option_S;
   "-c$", Set option_c;
   "-v$", Set option_v;
+  "-interp$", Set option_interp;
+  "-quiet$", Self (fun _ -> Interp.trace := 0);
+  "-trace$", Self (fun _ -> Interp.trace := 2);
+  "-random$", Self (fun _ -> Interp.mode := Interp.Random);
+  "-all$", Self (fun _ -> Interp.mode := Interp.All);
   ".*\\.c$", Self (fun s ->
       let objfile = process_c_file s in
       linker_options := objfile :: !linker_options);
@@ -391,6 +430,7 @@ let cmdline_actions =
   @ f_opt "vararg-calls" option_fvararg_calls
   @ f_opt "madd" option_fmadd
   @ f_opt "packed-structs" option_fpacked_structs
+  @ f_opt "sse" option_fsse
 
 let _ =
   Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };
@@ -405,7 +445,7 @@ let _ =
   CPragmas.initialize();
   parse_cmdline cmdline_actions usage_string;
   if !linker_options <> [] 
-  && not (!option_c || !option_S || !option_E)
+  && not (!option_c || !option_S || !option_E || !option_interp)
   then begin
     linker !exe_name !linker_options
   end
diff --git a/driver/Interp.ml b/driver/Interp.ml
new file mode 100644
index 0000000..84037ae
--- /dev/null
+++ b/driver/Interp.ml
@@ -0,0 +1,408 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Interpreting CompCert C sources *)
+
+open Format
+open Camlcoq
+open Datatypes
+open BinPos
+open BinInt
+open AST
+open Values
+open Memory
+open Globalenvs
+open Events
+open Csyntax
+open Csem
+open Clflags
+
+(* Configuration *)
+
+let trace = ref 1   (* 0 if quiet, 1 if normally verbose, 2 if full trace *)
+
+type mode = First | Random | All
+
+let mode = ref First
+
+(* Printing events *)
+
+let print_eventval p = function
+  | EVint n -> fprintf p "%ld" (camlint_of_coqint n)
+  | EVfloat f -> fprintf p "%F" f
+  | EVptr_global(id, ofs) -> 
+      fprintf p "&%s%+ld" (extern_atom id) (camlint_of_coqint ofs)
+
+let print_eventval_list p = function
+  | [] -> ()
+  | v1 :: vl ->
+      print_eventval p v1;
+      List.iter (fun v -> fprintf p ",@ %a" print_eventval v) vl
+
+let print_event p = function
+  | Event_syscall(id, args, res) ->
+      fprintf p "extcall %s(%a) -> %a"
+                (extern_atom id)
+                print_eventval_list args
+                print_eventval res
+  | Event_vload(chunk, id, ofs, res) ->
+      fprintf p "volatile load %s[&%s%+ld] -> %a"
+                (PrintCminor.name_of_chunk chunk)
+                (extern_atom id) (camlint_of_coqint ofs)
+                print_eventval res
+  | Event_vstore(chunk, id, ofs, arg) ->
+      fprintf p "volatile store %s[&%s%+ld] <- %a"
+                (PrintCminor.name_of_chunk chunk)
+                (extern_atom id) (camlint_of_coqint ofs)
+                print_eventval arg
+  | Event_annot(text, args) ->
+      fprintf p "annotation \"%s\" %a"
+                (extern_atom text)
+                print_eventval_list args
+
+(* Printing states *)
+
+let name_of_fundef prog fd =
+  let rec find_name = function
+  | [] -> "<unknown function>"
+  | Coq_pair(id, fd') :: rem ->
+      if fd = fd' then extern_atom id else find_name rem
+  in find_name prog.prog_funct
+
+let name_of_function prog fn =
+  name_of_fundef prog (Internal fn)
+
+let print_val p = function
+  | Vint n -> fprintf p "%ld" (camlint_of_coqint n)
+  | Vfloat f -> fprintf p "%F" f
+  | Vptr(b, ofs) -> fprintf p "<ptr>"
+  | Vundef -> fprintf p "<undef>"
+
+let print_val_list p = function
+  | [] -> ()
+  | v1 :: vl ->
+      print_val p v1;
+      List.iter (fun v -> fprintf p ",@ %a" print_val v) vl
+
+let print_state prog p = function
+  | State(f, s, k, e, m) ->
+      fprintf p "in function %s, statement@ @[<hv 0>%a@]"
+              (name_of_function prog f)
+              PrintCsyntax.print_stmt s 
+  | ExprState(f, r, k, e, m) ->
+      fprintf p "in function %s, expression@ @[<hv 0>%a@]"
+              (name_of_function prog f)
+              PrintCsyntax.print_expr r
+  | Callstate(fd, args, k, m) ->
+      fprintf p "calling@ @[<hov 2>%s(%a)@]"
+              (name_of_fundef prog fd)
+              print_val_list args
+  | Returnstate(res, k, m) ->
+      fprintf p "returning@ %a"
+              print_val res
+
+let mem_of_state = function
+  | State(f, s, k, e, m) -> m
+  | ExprState(f, r, k, e, m) -> m
+  | Callstate(fd, args, k, m) -> m
+  | Returnstate(res, k, m) -> m
+
+(* Comparing memory states *)
+
+let rec compare_Z_range lo hi f =
+  if coq_Zcompare lo hi = Lt then begin
+    let c = f lo in if c <> 0 then c else compare_Z_range (coq_Zsucc lo) hi f
+  end else 0
+
+let compare_mem m1 m2 =
+  if m1 == m2 then 0 else
+  let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else
+  compare_Z_range Z0 m1.Mem.nextblock (fun b ->
+    let (Coq_pair(lo, hi) as bnds) = m1.Mem.bounds b in
+    let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else
+    let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in
+    if contents1 == contents2 then 0 else
+    let c = compare_Z_range lo hi (fun ofs ->
+               compare (contents1 ofs) (contents2 ofs)) in if c <> 0 then c else
+    let access1 = m1.Mem.mem_access b and access2 = m2.Mem.mem_access b in
+    if access1 == access2 then 0 else
+    compare_Z_range lo hi (fun ofs -> compare (access1 ofs) (access2 ofs)))
+
+(* Comparing continuations *)
+
+let some_expr = Evar(Coq_xH, Tvoid)
+
+let rank_cont = function
+  | Kstop -> 0
+  | Kdo _ -> 1
+  | Kseq _ -> 2
+  | Kifthenelse _ -> 3
+  | Kwhile1 _ -> 4
+  | Kwhile2 _ -> 5
+  | Kdowhile1 _ -> 6
+  | Kdowhile2 _ -> 7
+  | Kfor2 _ -> 8
+  | Kfor3 _ -> 9
+  | Kfor4 _ -> 10
+  | Kswitch1 _ -> 11
+  | Kswitch2 _ -> 12
+  | Kreturn _ -> 13
+  | Kcall _ -> 14
+
+let rec compare_cont k1 k2 =
+  if k1 == k2 then 0 else
+  match k1, k2 with
+  | Kstop, Kstop -> 0
+  | Kdo k1, Kdo k2 -> compare_cont k1 k2
+  | Kseq(s1, k1), Kseq(s2, k2) ->  
+      let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2
+  | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) ->
+      let c = compare (s1,s1') (s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kwhile1(e1, s1, k1), Kwhile1(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kwhile2(e1, s1, k1), Kwhile2(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kdowhile1(e1, s1, k1), Kdowhile1(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kdowhile2(e1, s1, k1), Kdowhile2(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kfor2(e1, s1, s1', k1), Kfor2(e2, s2, s2', k2) ->
+      let c = compare (e1,s1,s1') (e2,s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kfor3(e1, s1, s1', k1), Kfor3(e2, s2, s2', k2) ->
+      let c = compare (e1,s1,s1') (e2,s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kfor4(e1, s1, s1', k1), Kfor4(e2, s2, s2', k2) ->
+      let c = compare (e1,s1,s1') (e2,s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kswitch1(sl1, k1), Kswitch1(sl2, k2) ->
+      let c = compare sl1 sl2 in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kreturn k1, Kreturn k2 ->
+      compare_cont k1 k2
+  | Kcall(f1, e1, c1, ty1, k1), Kcall(f2, e2, c2, ty2, k2) ->
+      let c = compare (f1, e1, c1 some_expr, ty1) (f2, e2, c2 some_expr, ty2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | _, _ ->
+      compare (rank_cont k1) (rank_cont k2)
+
+(* Comparing states *)
+
+let rank_state = function
+  | State _ -> 0
+  | ExprState _ -> 1
+  | Callstate _ -> 2
+  | Returnstate _ -> 3
+
+let compare_state s1 s2 =
+  if s1 == s2 then 0 else
+  match s1, s2 with
+  | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) ->
+      let c = compare (f1,s1,e1) (f2,s2,e2) in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | ExprState(f1,r1,k1,e1,m1), ExprState(f2,r2,k2,e2,m2) ->
+      let c = compare (f1,r1,e1) (f2,r2,e2) in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | Callstate(fd1,args1,k1,m1), Callstate(fd2,args2,k2,m2) ->
+      let c = compare (fd1,args1) (fd2,args2) in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | Returnstate(res1,k1,m1), Returnstate(res2,k2,m2) ->
+      let c = compare res1 res2 in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | _, _ ->
+      compare (rank_state s1) (rank_state s2)
+
+module StateSet =
+  Set.Make(struct type t = state let compare = compare_state end)
+
+(* Extract a string from a global pointer *)
+
+let extract_string ge m id ofs =
+  let b = Buffer.create 80 in
+  let rec extract blk ofs =
+    match Memory.Mem.load Mint8unsigned m blk ofs with
+    | Some(Vint n) ->
+        let c = Char.chr (Int32.to_int (camlint_of_coqint n)) in
+        if c = '\000' then begin
+          Some(Buffer.contents b)
+        end else begin
+          Buffer.add_char b c; 
+          extract blk (coq_Zsucc ofs)
+        end
+    | _ ->
+        None in
+  match Genv.find_symbol ge id with
+  | None -> None
+  | Some blk -> extract blk ofs
+
+(* Emulation of printf *)
+
+(* All ISO C 99 formats except size modifiers [ll] (long long) and [L]
+   (long double) *)
+
+let re_conversion = Str.regexp
+  "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\)?\\([aAcdeEfgGinopsuxX%]\\)"
+
+external format_float: string -> float -> string
+  = "caml_format_float"
+external format_int32: string -> int32 -> string
+  = "caml_int32_format"
+
+let do_printf ge 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' []
+        | EVint 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') ->
+            Buffer.add_string b (format_float pat f);
+            scan pos' args'
+        | EVptr_global(id, ofs) :: args', 's' ->
+            Buffer.add_string b
+              (match extract_string ge m id ofs with
+               | Some s -> s
+               | None -> "<bad string>");
+            scan pos' args'
+        | EVptr_global(id, ofs) :: args', 'p' ->
+            Printf.bprintf b "<&%s%+ld>" (extern_atom id) (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
+
+(* Implementing external functions *)
+
+let re_stub = Str.regexp "\\$[if]*$"
+
+let chop_stub name = Str.replace_first re_stub "" name
+
+let rec world = Determinism.World(world_io, world_vload, world_vstore)
+
+and world_io id args =
+  match chop_stub(extern_atom id), args with
+  | "printf", EVptr_global(id, ofs) :: args' ->
+      Some(Coq_pair(EVint Integers.Int.zero, world))
+  | _, _ ->
+      None
+
+and world_vload chunk id ofs =
+  let res = match chunk with
+    | Mint8signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x100l) 0x80l))
+    | Mint8unsigned -> EVint(coqint_of_camlint(Random.int32 0x100l))
+    | Mint16signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x10000l) 0x8000l))
+    | Mint16unsigned -> EVint(coqint_of_camlint(Random.int32 0x10000l))
+    | Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl))
+    | Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0))
+    | Mfloat64 -> EVfloat(Random.float 1.0)
+  in Some(Coq_pair(res, world))
+
+and world_vstore chunk id ofs arg =
+  Some world
+
+let do_event p ge time s ev =
+  if !trace >= 1 then
+    fprintf p "@[<hov 2>Time %d: observable event: %a@]@."
+              time print_event ev;
+  match ev with
+  | Event_syscall(name, EVptr_global(id, ofs) :: args', res) 
+    when chop_stub (extern_atom name) = "printf" ->
+      flush stderr;
+      let m = mem_of_state s in
+      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
+  | _ -> ()
+
+let do_events p ge time s t =
+  List.iter (do_event p ge time s) t
+
+(* Exploration *)
+
+let do_step p prog ge time s =
+  if !trace >= 2 then
+    fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+  match Cexec.at_final_state s with
+  | Some r ->
+      if !trace >= 1 then begin
+        fprintf p "Time %d: program terminated (exit code = %ld)@."
+                  time (camlint_of_coqint r);
+        []
+      end else begin
+        exit (Int32.to_int (camlint_of_coqint r))
+      end
+  | None ->
+      match Cexec.do_step ge world s with
+      | [] ->
+          if !trace = 1 then
+            fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+          fprintf p "ERROR: Undefined behavior@.";
+          fprintf p "@].";
+          exit 126
+      | l ->
+          List.iter (fun (Coq_pair(t, s')) -> do_events p ge time s t) l;
+          List.map snd l
+
+let rec explore p prog ge time ss =
+  let succs =
+    StateSet.fold (fun s l -> do_step p prog ge time s @ l) ss [] in
+  if succs <> [] then begin
+    let ss' =
+      match !mode with
+      | First -> StateSet.singleton (List.hd succs)
+      | Random -> StateSet.singleton (List.nth succs (Random.int (List.length succs)))
+      | All -> List.fold_right StateSet.add succs StateSet.empty in
+    explore p prog ge (time + 1) ss'
+  end
+
+let execute prog =
+  let p = err_formatter in
+  pp_set_max_boxes p 10;
+  begin match Cexec.do_initial_state prog with
+  | None -> fprintf p "ERROR: Initial state undefined@."
+  | Some(Coq_pair(ge, s)) -> explore p prog ge 0 (StateSet.singleton s)
+  end