diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 60 | ||||
| -rw-r--r-- | driver/Interp.ml | 6 |
2 files changed, 43 insertions, 23 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 6d8cf9ac..eccd233c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -86,29 +86,35 @@ let compile_cminor_file ifile ofile = Sections.initialize(); let ic = open_in ifile in let lb = Lexing.from_channel ic in - try - match Compiler.transf_cminor_program - (CMtypecheck.type_program - (CMparser.prog CMlexer.token lb)) with + (* Parse cminor *) + let cm = + try CMtypecheck.type_program (CMparser.prog CMlexer.token lb) + with Parsing.Parse_error -> + eprintf "File %s, character %d: Syntax error\n" + ifile (Lexing.lexeme_start lb); + exit 2 + | CMlexer.Error msg -> + eprintf "File %s, character %d: %s\n" + ifile (Lexing.lexeme_start lb) msg; + exit 2 + | CMtypecheck.Error msg -> + eprintf "File %s, type-checking error:\n%s" + ifile msg; + exit 2 in + (* Convert to Asm *) + let asm = + match Compiler.apply_partial + (Compiler.transf_cminor_program cm) + Asmexpand.expand_program with + | Errors.OK asm -> + asm | Errors.Error msg -> eprintf "%s: %a" ifile print_error msg; - exit 2 - | Errors.OK p -> - let oc = open_out ofile in - PrintAsm.print_program oc p; - close_out oc - with Parsing.Parse_error -> - eprintf "File %s, character %d: Syntax error\n" - ifile (Lexing.lexeme_start lb); - exit 2 - | CMlexer.Error msg -> - eprintf "File %s, character %d: %s\n" - ifile (Lexing.lexeme_start lb) msg; - exit 2 - | CMtypecheck.Error msg -> - eprintf "File %s, type-checking error:\n%s" - ifile msg; - exit 2 + exit 2 in + (* Print Asm in text form *) + let oc = open_out ofile in + PrintAsm.print_program oc asm; + close_out oc (* Processing of a .c file *) @@ -327,6 +333,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -dltl Save LTL after register allocation in <file>.ltl\n\ \ -dmach Save generated Mach code in <file>.mach\n\ \ -dasm Save generated assembly in <file>.s\n\ +\ -dall Save all generated intermidate files in <file>.<ext>\n\ \ -sdump Save info for post-linking validation in <file>.json\n\ \ -doptions Save the compiler configurations in <file>.opt.json\n\ General options:\n\ @@ -435,6 +442,17 @@ let cmdline_actions = Exact "-dalloctrace", Set option_dalloctrace; Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; + Exact "-dall", Self (fun _ -> + option_dprepro := true; + option_dparse := true; + option_dcmedium := true; + option_dclight := true; + option_dcminor := true; + option_drtl := true; + option_dalloctrace := true; + option_dmach := true; + option_dasm := true; + dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); Exact "-doptions", Set dump_options; diff --git a/driver/Interp.ml b/driver/Interp.ml index 5c2158ae..f42bed32 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -387,10 +387,12 @@ let do_external_function id sg ge w args m = match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> - print_string (do_printf m fmt args'); + let fmt' = do_printf m fmt args' in + let len = coqint_of_camlint (Int32.of_int (String.length fmt')) in + print_string fmt'; flush stdout; convert_external_args ge args sg.sig_args >>= fun eargs -> - Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) + Some(((w, [Event_syscall(id, eargs, EVint len)]), Vint len), m) | _ -> None |