aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/AsmToJSON.ml14
-rw-r--r--arm/AsmToJSON.mli8
-rw-r--r--backend/JsonAST.ml32
-rw-r--r--backend/JsonAST.mli2
-rw-r--r--driver/Driver.ml48
-rw-r--r--powerpc/AsmToJSON.ml14
-rw-r--r--powerpc/AsmToJSON.mli8
-rw-r--r--riscV/AsmToJSON.ml7
-rw-r--r--x86/AsmToJSON.ml8
-rw-r--r--x86/AsmToJSON.mli8
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
generated by cgit (git 2.34.1) at 2024-06-11 17:52:32 +0000