diff options
-rw-r--r-- | arm/AsmToJSON.ml | 14 | ||||
-rw-r--r-- | arm/AsmToJSON.mli | 8 | ||||
-rw-r--r-- | backend/JsonAST.ml | 32 | ||||
-rw-r--r-- | backend/JsonAST.mli | 2 | ||||
-rw-r--r-- | driver/Driver.ml | 48 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 14 | ||||
-rw-r--r-- | powerpc/AsmToJSON.mli | 8 | ||||
-rw-r--r-- | riscV/AsmToJSON.ml | 7 | ||||
-rw-r--r-- | x86/AsmToJSON.ml | 8 | ||||
-rw-r--r-- | x86/AsmToJSON.mli | 8 |
10 files changed, 87 insertions, 62 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index 85ef0603..c11162d6 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -302,9 +302,17 @@ let pp_instructions pp ic = in pp_jarray instruction pp ic -let pp_program pp prog = - reset_id (); - JsonAST.pp_program pp pp_instructions prog +let destination : string option ref = ref None +let sdump_folder : string ref = ref "" + +let print_if prog sourcename = + match !destination with + | None -> () + | Some f -> + let f = Filename.concat !sdump_folder f in + let oc = open_out f in + JsonAST.pp_ast (Format.formatter_of_out_channel oc) pp_instructions prog sourcename; + close_out oc let pp_mnemonics pp = JsonAST.pp_mnemonics pp mnemonic_names diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli index 058a4e83..52c055c4 100644 --- a/arm/AsmToJSON.mli +++ b/arm/AsmToJSON.mli @@ -10,6 +10,10 @@ (* *) (* *********************************************************************) -val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit - val pp_mnemonics: Format.formatter -> unit + +val print_if: (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit + +val destination: string option ref + +val sdump_folder : string ref diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml index 73cac31e..3469bdc6 100644 --- a/backend/JsonAST.ml +++ b/backend/JsonAST.ml @@ -122,3 +122,35 @@ let pp_mnemonics pp mnemonic_names = let mnemonic_names = List.sort (String.compare) mnemonic_names in let new_line pp () = pp_print_string pp "\n" in pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names + +let jdump_magic_number = "CompCertJDUMP" ^ Version.version + +let pp_ast pp pp_inst ast sourcename = + let get_args () = + let buf = Buffer.create 100 in + Buffer.add_string buf Sys.executable_name; + for i = 1 to (Array.length !Commandline.argv - 1) do + Buffer.add_string buf " "; + Buffer.add_string buf (Responsefile.gnu_quote !Commandline.argv.(i)); + done; + Buffer.contents buf in + let dump_compile_info pp () = + pp_jobject_start pp; + pp_jmember ~first:true pp "directory" pp_jstring (Sys.getcwd ()); + pp_jmember pp "command" pp_jstring (get_args ()); + pp_jmember pp "file" pp_jstring sourcename; + pp_jobject_end pp in + pp_jobject_start pp; + pp_jmember ~first:true pp "Version" pp_jstring jdump_magic_number; + let json_arch = + match Configuration.arch, !Clflags.option_mthumb with + | "arm", false -> "arm-arm" + | "arm", true -> "arm-thumb" + | a, _ -> a in + pp_jmember pp "Architecture" pp_jstring json_arch; + pp_jmember pp "System" pp_jstring Configuration.system; + pp_jmember pp "Compile Info" dump_compile_info (); + pp_jmember pp "Compilation Unit" pp_jstring sourcename; + pp_jmember pp "Asm Ast" (fun pp prog -> pp_program pp pp_inst prog) ast; + pp_jobject_end pp; + Format.pp_print_flush pp () diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli index c6fd80c9..7afdce51 100644 --- a/backend/JsonAST.mli +++ b/backend/JsonAST.mli @@ -12,5 +12,5 @@ -val pp_program : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit val pp_mnemonics : Format.formatter -> string list -> unit +val pp_ast : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit diff --git a/driver/Driver.ml b/driver/Driver.ml index 9726f107..27a8edcc 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -18,52 +18,13 @@ open Driveraux open Frontend open Assembler open Linker -open Json (* Optional sdump suffix *) let sdump_suffix = ref ".json" -let sdump_folder = ref "" - -(* Dump Asm code in asm format for the validator *) - -let jdump_magic_number = "CompCertJDUMP" ^ Version.version let nolink () = !option_c || !option_S || !option_E || !option_interp -let dump_jasm asm sourcename destfile = - let oc = open_out_bin destfile in - let pp = Format.formatter_of_out_channel oc in - let get_args () = - let buf = Buffer.create 100 in - Buffer.add_string buf Sys.executable_name; - for i = 1 to (Array.length !argv - 1) do - Buffer.add_string buf " "; - Buffer.add_string buf (Responsefile.gnu_quote !argv.(i)); - done; - Buffer.contents buf in - let dump_compile_info pp () = - pp_jobject_start pp; - pp_jmember ~first:true pp "directory" pp_jstring (Sys.getcwd ()); - pp_jmember pp "command" pp_jstring (get_args ()); - pp_jmember pp "file" pp_jstring sourcename; - pp_jobject_end pp in - pp_jobject_start pp; - pp_jmember ~first:true pp "Version" pp_jstring jdump_magic_number; - let json_arch = - match Configuration.arch, !Clflags.option_mthumb with - | "arm", false -> "arm-arm" - | "arm", true -> "arm-thumb" - | a, _ -> a in - pp_jmember pp "Architecture" pp_jstring json_arch; - pp_jmember pp "System" pp_jstring Configuration.system; - pp_jmember pp "Compile Info" dump_compile_info (); - pp_jmember pp "Compilation Unit" pp_jstring sourcename; - pp_jmember pp "Asm Ast" AsmToJSON.pp_program asm; - pp_jobject_end pp; - Format.pp_print_flush pp (); - close_out oc - let object_filename sourcename suff = if nolink () then output_filename ~final: !option_c sourcename suff ".o" @@ -85,6 +46,7 @@ let compile_c_file sourcename ifile ofile = set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest PrintLTL.destination option_dltl ".ltl"; set_dest PrintMach.destination option_dmach ".mach"; + set_dest AsmToJSON.destination option_sdump !sdump_suffix; (* Parse the ast *) let csyntax = parse_c_file sourcename ifile in (* Convert to Asm *) @@ -98,11 +60,7 @@ let compile_c_file sourcename ifile ofile = eprintf "%s: %a" sourcename print_error msg; exit 2 in (* Dump Asm in binary and JSON format *) - if !option_sdump then begin - let sf = output_filename sourcename ".c" !sdump_suffix in - let csf = Filename.concat !sdump_folder sf in - dump_jasm asm sourcename csf - end; + AsmToJSON.print_if asm sourcename; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm; @@ -421,7 +379,7 @@ let cmdline_actions = option_dasm := true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); - Exact "-sdump-folder", String (fun s -> sdump_folder := s); + Exact "-sdump-folder", String (fun s -> AsmToJSON.sdump_folder := s); (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 696f7ca5..5baed5dc 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -370,9 +370,17 @@ let pp_instructions pp ic = | Pcfi_rel_offset _ -> assert false in (* Only debug relevant *) pp_jarray instruction pp ic -let pp_program pp prog = - reset_id (); - pp_program pp pp_instructions prog +let destination : string option ref = ref None +let sdump_folder : string ref = ref "" + +let print_if prog sourcename = + match !destination with + | None -> () + | Some f -> + let f = Filename.concat !sdump_folder f in + let oc = open_out f in + pp_ast (formatter_of_out_channel oc) pp_instructions prog sourcename; + close_out oc let pp_mnemonics pp = pp_mnemonics pp mnemonic_names diff --git a/powerpc/AsmToJSON.mli b/powerpc/AsmToJSON.mli index 058a4e83..52c055c4 100644 --- a/powerpc/AsmToJSON.mli +++ b/powerpc/AsmToJSON.mli @@ -10,6 +10,10 @@ (* *) (* *********************************************************************) -val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit - val pp_mnemonics: Format.formatter -> unit + +val print_if: (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit + +val destination: string option ref + +val sdump_folder : string ref diff --git a/riscV/AsmToJSON.ml b/riscV/AsmToJSON.ml index 1b2f7458..8a6a97a7 100644 --- a/riscV/AsmToJSON.ml +++ b/riscV/AsmToJSON.ml @@ -13,8 +13,11 @@ (* Simple functions to serialize RISC-V Asm to JSON *) (* Dummy function *) +let destination: string option ref = ref None -let pp_program pp prog = - Format.fprintf pp "null" +let sdump_folder = ref "" + +let print_if prog sourcename = + () let pp_mnemonics pp = () diff --git a/x86/AsmToJSON.ml b/x86/AsmToJSON.ml index 8488bfde..59cc7d40 100644 --- a/x86/AsmToJSON.ml +++ b/x86/AsmToJSON.ml @@ -13,7 +13,11 @@ (* Simple functions to serialize ia32 Asm to JSON *) (* Dummy function *) -let pp_program pp prog = - Format.fprintf pp "null" +let destination: string option ref = ref None + +let sdump_folder = ref "" + +let print_if prog sourcename = + () let pp_mnemonics pp = () diff --git a/x86/AsmToJSON.mli b/x86/AsmToJSON.mli index 058a4e83..52c055c4 100644 --- a/x86/AsmToJSON.mli +++ b/x86/AsmToJSON.mli @@ -10,6 +10,10 @@ (* *) (* *********************************************************************) -val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit - val pp_mnemonics: Format.formatter -> unit + +val print_if: (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit + +val destination: string option ref + +val sdump_folder : string ref |