From 4af1682d04244bab9f793e00eb24090153a36a0f Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jul 2011 12:51:16 +0000 Subject: 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 --- driver/Clflags.ml | 1 + driver/Compiler.v | 9 +- driver/Driver.ml | 152 ++++++++++++-------- driver/Interp.ml | 408 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 510 insertions(+), 60 deletions(-) create mode 100644 driver/Interp.ml (limited to 'driver') 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] -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 .s - -c Compile to object file only (no linking), result in .o -Preprocessing options: - -I Add to search path for #include files - -D= Define preprocessor symbol - -U Undefine preprocessor symbol -Language support options (use -fno- to turn off -f) : - -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 Set maximal size for allocation in small data area - -fsmall-const Set maximal size for allocation in small constant area -Tracing options: - -dparse Save C file after parsing and elaboration in .parse.c - -dc Save generated Compcert C in .compcert.c - -dclight Save generated Clight in .light.c - -dcminor Save generated Cminor in .cm - -drtl Save unoptimized generated RTL in .rtl - -dtailcall Save RTL after tail call optimization in .tailcall.rtl - -dcastopt Save RTL after cast optimization in .castopt.rtl - -dconstprop Save RTL after constant propagation in .constprop.rtl - -dcse Save RTL after CSE optimization in .cse.rtl - -dalloc Save LTL after register allocation in .alloc.ltl - -dmach Save generated Mach code in .mach - -dasm Save generated assembly in .s -Linking options: - -l Link library - -L Add to search path for libraries - -o Generate executable in (default: a.out) -General options: - -stdlib 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] +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 .s + -c Compile to object file only (no linking), result in .o +Preprocessing options: + -I Add to search path for #include files + -D= Define preprocessor symbol + -U Undefine preprocessor symbol +Language support options (use -fno- to turn off -f) : + -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- to turn off -f) : + -fmadd (PowerPC) Use fused multiply-add and multiply-sub instructions [off] + -fsse (IA32) Use SSE2 instructions for some integer operations [on] + -fsmall-data Set maximal size for allocation in small data area + -fsmall-const Set maximal size for allocation in small constant area +Tracing options: + -dparse Save C file after parsing and elaboration in .parse.c + -dc Save generated Compcert C in .compcert.c + -dclight Save generated Clight in .light.c + -dcminor Save generated Cminor in .cm + -drtl Save unoptimized generated RTL in .rtl + -dtailcall Save RTL after tail call optimization in .tailcall.rtl + -dcastopt Save RTL after cast optimization in .castopt.rtl + -dconstprop Save RTL after constant propagation in .constprop.rtl + -dcse Save RTL after CSE optimization in .cse.rtl + -dalloc Save LTL after register allocation in .alloc.ltl + -dmach Save generated Mach code in .mach + -dasm Save generated assembly in .s +Linking options: + -l Link library + -L Add to search path for libraries + -o Generate executable in (default: a.out) +General options: + -stdlib 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 + | [] -> "" + | 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 "" + | Vundef -> fprintf p "" + +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@ @[%a@]" + (name_of_function prog f) + PrintCsyntax.print_stmt s + | ExprState(f, r, k, e, m) -> + fprintf p "in function %s, expression@ @[%a@]" + (name_of_function prog f) + PrintCsyntax.print_expr r + | Callstate(fd, args, k, m) -> + fprintf p "calling@ @[%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 ""; + 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 -> ""); + 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 ""; + 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 "@[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 "\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 "@[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 "@[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 -- cgit v1.2.3