diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 6ba3f1bcf65f51b98dda78a25d3ad3e679c272b8..e850fed67f257e34cc4dfd930ae80015a9eaa6d9 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -19,21 +19,25 @@ open BinNums
open Camlcoq
open Json
-let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic"; "Pblreg";
- "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pcmn"; "Pconstants"; "Pfcpy_iif";
- "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pflid_lbl"; "Pflis_lbl"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd";
- "Pfabss"; "Pfaddd"; "Pfadds"; "Pfcmpd"; "Pfcmps"; "Pfcmpzd"; "Pfcmpzs";
- "Pfcpyd"; "Pfcpy_fs"; "Pfcpy_if";"Pfcvtds"; "Pfcvtsd"; "Pfdivd"; "Pfdivs"; "Pfldd";
- "Pflid"; "Pflds"; "Pflid_imm"; "Pflis_imm"; "Pfmuld"; "Pfmuls"; "Pfnegd";
- "Pfnegs"; "Pfsitod"; "Pfsitos"; "Pfsqrt"; "Pfstd";
- "Pfsts"; "Pfsubd"; "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd";
- "Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr";
- "Ploadsymbol_lbl"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb";
- "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; "Pfmovite";
- "Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Ploadsymbol_imm"; "Pnop"; "Porr";
- "Ppush"; "Prev"; "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull";
- "Pstr"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv";
- "Pumull" ]
+module StringSet = Set.Make(String)
+
+let mnemonic_names = StringSet.of_list
+ [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic";
+ "Pblreg"; "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp";
+ "Pcmn"; "Pconstants"; "Pfcpy_iif"; "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf";
+ "Pflid_lbl"; "Pflis_lbl"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd"; "Pfabss";
+ "Pfaddd"; "Pfadds"; "Pfcmpd"; "Pfcmps"; "Pfcmpzd"; "Pfcmpzs"; "Pfcpyd";
+ "Pfcpy_fs"; "Pfcpy_if";"Pfcvtds"; "Pfcvtsd"; "Pfdivd"; "Pfdivs"; "Pfldd";
+ "Pflid"; "Pflds"; "Pflid_imm"; "Pflis_imm"; "Pfmuld"; "Pfmuls"; "Pfnegd";
+ "Pfnegs"; "Pfsitod"; "Pfsitos"; "Pfsqrt"; "Pfstd"; "Pfsts"; "Pfsubd";
+ "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd"; "Pftouizs"; "Pfuitod";
+ "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr"; "Ploadsymbol_lbl";
+ "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb"; "Pldrsh";
+ "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; "Pfmovite"; "Pmovt"; "Pmovw";
+ "Pmul"; "Pmvn"; "Ploadsymbol_imm"; "Pnop"; "Porr"; "Ppush"; "Prev";
+ "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull";
+ "Pstr"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs";
+ "Pudiv";"Pumull" ]
type instruction_arg =
| ALabel of positive
@@ -143,7 +147,7 @@ let pp_instructions pp ic =
| _ -> true) ic in
let instruction pp n args =
- assert (List.mem n mnemonic_names);
+ assert (StringSet.mem n mnemonic_names);
pp_jobject_start pp;
pp_jmember ~first:true pp "Instruction Name" pp_jstring n;
pp_jmember pp "Args" (pp_jarray pp_arg) args;
@@ -313,8 +317,8 @@ let print_if prog sourcename =
| Some f ->
let f = Filename.concat !sdump_folder f in
let oc = open_out_bin f in
- JsonAST.pp_ast (Format.formatter_of_out_channel oc) pp_instructions prog sourcename;
+ JsonAST.pp_ast oc pp_instructions prog sourcename;
close_out oc
let pp_mnemonics pp =
- JsonAST.pp_mnemonics pp mnemonic_names
+ JsonAST.pp_mnemonics pp (StringSet.elements mnemonic_names)
diff --git a/backend/Json.ml b/backend/Json.ml
index b8f66c085816c2bc15ecf105ef06081b1055abd3..bd4d6ff90381c77e4a1aeb77258b7cc5facb7764 100644
--- a/backend/Json.ml
+++ b/backend/Json.ml
@@ -10,7 +10,6 @@
(* *)
(* *********************************************************************)
-open Format
open Camlcoq
@@ -18,16 +17,21 @@ open Camlcoq
(* Print a string as json string *)
let pp_jstring oc s =
- fprintf oc "\"%s\"" s
+ output_string oc "\"";
+ output_string oc s;
+ output_string oc "\""
(* Print a bool as json bool *)
-let pp_jbool oc = fprintf oc "%B"
+let pp_jbool oc b = output_string oc (string_of_bool b)
(* Print an int as json int *)
-let pp_jint oc = fprintf oc "%d"
+let pp_jint oc i = output_string oc (string_of_int i)
(* Print an int32 as json int *)
-let pp_jint32 oc = fprintf oc "%ld"
+let pp_jint32 oc i = output_string oc (Int32.to_string i)
+
+(* Print an int64 as json int *)
+let pp_jint64 oc i = output_string oc (Int64.to_string i)
(* Print optional value *)
let pp_jopt pp_elem oc = function
@@ -36,15 +40,19 @@ let pp_jopt pp_elem oc = function
(* Print opening and closing curly braces for json dictionaries *)
let pp_jobject_start pp =
- fprintf pp "@[<v 1>{"
+ output_string pp "\n{"
let pp_jobject_end pp =
- fprintf pp "@;<0 -1>}@]"
+ output_string pp "}"
(* Print a member of a json dictionary *)
let pp_jmember ?(first=false) pp name pp_mem mem =
- let sep = if first then "" else "," in
- fprintf pp "%s@ \"%s\": %a" sep name pp_mem mem
+ if not first then output_string pp ",";
+ output_string pp " ";
+ pp_jstring pp name;
+ output_string pp " :";
+ pp_mem pp mem;
+ output_string pp "\n"
(* Print singleton object *)
let pp_jsingle_object pp name pp_mem mem =
@@ -54,29 +62,31 @@ let pp_jsingle_object pp name pp_mem mem =
(* Print a list as json array *)
let pp_jarray elem pp l =
- match l with
- | [] -> fprintf pp "[]";
+ let pp_sep () = output_string pp ", " in
+ output_string pp "[";
+ begin match l with
+ | [] -> ()
| hd::tail ->
- fprintf pp "@[<v 1>[";
- fprintf pp "%a" elem hd;
- List.iter (fun l -> fprintf pp ",@ %a" elem l) tail;
- fprintf pp "@;<0 -1>]@]"
+ elem pp hd;
+ List.iter (fun l -> pp_sep (); elem pp l) tail;
+ end;
+ output_string pp "]"
(* Helper functions for printing coq integer and floats *)
let pp_int pp i =
- fprintf pp "%ld" (camlint_of_coqint i)
+ pp_jint32 pp (camlint_of_coqint i)
let pp_int64 pp i =
- fprintf pp "%Ld" (camlint64_of_coqint i)
+ pp_jint64 pp (camlint64_of_coqint i)
let pp_float32 pp f =
- fprintf pp "%ld" (camlint_of_coqint (Floats.Float32.to_bits f))
+ pp_jint32 pp (camlint_of_coqint (Floats.Float32.to_bits f))
let pp_float64 pp f =
- fprintf pp "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f))
+ pp_jint64 pp (camlint64_of_coqint (Floats.Float.to_bits f))
let pp_z pp z =
- fprintf pp "%s" (Z.to_string z)
+ output_string pp (Z.to_string z)
(* Helper functions for printing assembler constructs *)
let pp_atom pp a =
@@ -106,4 +116,4 @@ let reset_id () =
let pp_id_const pp () =
let i = next_id () in
- pp_jsingle_object pp "Integer" (fun pp i -> fprintf pp "%d" i) i
+ pp_jsingle_object pp "Integer" pp_jint i
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index 4e57106f6b92522ada2793291cf9979f8da04c78..8905e2521a2be3c8e96127c52582a3cc76343a45 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -15,7 +15,6 @@ open Asm
open AST
open C2C
open Json
-open Format
open Sections
@@ -54,8 +53,8 @@ let pp_section pp sec =
| Section_ais_annotation -> () (* There should be no info in the debug sections *)
let pp_int_opt pp = function
- | None -> fprintf pp "0"
- | Some i -> fprintf pp "%d" i
+ | None -> output_string pp "0"
+ | Some i -> pp_jint pp i
let pp_fundef pp_inst pp (name,fn) =
let alignment = atom_alignof name
@@ -119,9 +118,8 @@ let pp_program pp pp_inst prog =
pp_jobject_end pp
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 new_line pp () = Format.pp_print_string pp "\n" in
+ Format.pp_print_list ~pp_sep:new_line Format.pp_print_string pp mnemonic_names
let jdump_magic_number = "CompCertJDUMPRelease: " ^ Version.version
@@ -153,4 +151,4 @@ let pp_ast pp pp_inst ast sourcename =
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 ()
+ flush pp
diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli
index 7afdce51fb6d08d65d27a6294c8f172f4e07f046..c32439e495760a62d0eb31e7a04612a8f098dba1 100644
--- a/backend/JsonAST.mli
+++ b/backend/JsonAST.mli
@@ -13,4 +13,4 @@
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
+val pp_ast : out_channel -> (out_channel -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 99c51e43344717ddbf5e7b84a8f16c57a93039a9..f4d4285a4ac07a635a0553ca8c9076275b2d0fb5 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -17,12 +17,10 @@ open AST
open BinNums
open Camlcoq
open Json
-open Format
open JsonAST
let pp_reg pp t n =
- let s = sprintf "%s%s" t n in
- pp_jsingle_object pp "Register" pp_jstring s
+ pp_jsingle_object pp "Register" pp_jstring (t ^ n)
let pp_ireg pp reg =
pp_reg pp "r" (TargetPrinter.int_reg_name reg)
@@ -31,8 +29,8 @@ let pp_freg pp reg =
pp_reg pp "f" (TargetPrinter.float_reg_name reg)
let preg_annot = function
- | IR r -> sprintf "r%s" (TargetPrinter.int_reg_name r)
- | FR r -> sprintf "f%s" (TargetPrinter.float_reg_name r)
+ | IR r -> "r" ^ (TargetPrinter.int_reg_name r)
+ | FR r -> "f" ^ (TargetPrinter.float_reg_name r)
| _ -> assert false
let pp_constant pp c =
@@ -86,28 +84,31 @@ let pp_arg pp = function
| Atom a -> pp_atom_constant pp a
| String s -> pp_jsingle_object pp "String" pp_jstring s
-let mnemonic_names =["Padd"; "Paddc"; "Padde"; "Paddi"; "Paddic"; "Paddis"; "Paddze"; "Pand_";
- "Pandc"; "Pandi_"; "Pandis_"; "Pannot"; "Pb"; "Pbctr"; "Pbctrl"; "Pbdnz";
- "Pbf"; "Pbl"; "Pblr"; "Pbs"; "Pbt"; "Pbtbl"; "Pcmpb"; "Pcmpd"; "Pcmpdi";
- "Pcmpld"; "Pcmpldi"; "Pcmplw"; "Pcmplwi"; "Pcmpw"; "Pcmpwi"; "Pcntlzd";
- "Pcntlzw"; "Pcreqv"; "Pcror"; "Pcrxor"; "Pdcbf"; "Pdcbi"; "Pdcbt";
- "Pdcbtls"; "Pdcbtst"; "Pdcbz"; "Pdivd"; "Pdivdu"; "Pdivw"; "Pdivwu";
- "Peieio"; "Peqv"; "Pextsb"; "Pextsh"; "Pextsw"; "Pfabs"; "Pfadd"; "Pfadds";
- "Pfcfid"; "Pfcmpu"; "Pfctidz"; "Pfctiw"; "Pfctiwz"; "Pfdiv"; "Pfdivs";
- "Pfmadd"; "Pfmr"; "Pfmsub"; "Pfmul"; "Pfmuls"; "Pfneg"; "Pfnmadd";
- "Pfnmsub"; "Pfres"; "Pfrsp"; "Pfrsqrte"; "Pfsel"; "Pfsqrt"; "Pfsub";
- "Pfsubs"; "Picbi"; "Picbtls"; "Pinlineasm"; "Pisel"; "Pisync"; "Plabel";
- "Plbz"; "Plbzx"; "Pld"; "Pldbrx"; "Pldi"; "Pldx"; "Plfd"; "Plfdx"; "Plfi"; "Plfis";
- "Plfs"; "Plfsx"; "Plha"; "Plhax"; "Plhbrx"; "Plhz"; "Plhzx"; "Plwarx";
- "Plwbrx"; "Plwsync"; "Plwz"; "Plwzu"; "Plwzx"; "Pmbar"; "Pmfcr"; "Pmflr";
- "Pmfspr"; "Pmr"; "Pmtctr"; "Pmtlr"; "Pmtspr"; "Pmulhd"; "Pmulhdu"; "Pmulhw";
- "Pmulhwu"; "Pmulld"; "Pmulli"; "Pmullw"; "Pnand"; "Pnor"; "Por"; "Porc";
- "Pori"; "Poris"; "Prldicl"; "Prldimi"; "Prldinm"; "Prlwimi"; "Prlwinm";
- "Psld"; "Pslw"; "Psrad"; "Psradi"; "Psraw"; "Psrawi"; "Psrd"; "Psrw";
- "Pstb"; "Pstbx"; "Pstd"; "Pstdbrx"; "Pstdu"; "Pstdx"; "Pstfd"; "Pstfdu"; "Pstfdx";
- "Pstfs"; "Pstfsx"; "Psth"; "Psthbrx"; "Psthx"; "Pstw"; "Pstwbrx"; "Pstwcx_";
- "Pstwu"; "Pstwux"; "Pstwx"; "Psubfc"; "Psubfe"; "Psubfic"; "Psubfze";
- "Psync"; "Ptrap"; "Pxor"; "Pxori"; "Pxoris"]
+module StringSet = Set.Make(String)
+
+let mnemonic_names = StringSet.of_list
+ ["Padd"; "Paddc"; "Padde"; "Paddi"; "Paddic"; "Paddis"; "Paddze"; "Pand_";
+ "Pandc"; "Pandi_"; "Pandis_"; "Pannot"; "Pb"; "Pbctr"; "Pbctrl"; "Pbdnz";
+ "Pbf"; "Pbl"; "Pblr"; "Pbs"; "Pbt"; "Pbtbl"; "Pcmpb"; "Pcmpd"; "Pcmpdi";
+ "Pcmpld"; "Pcmpldi"; "Pcmplw"; "Pcmplwi"; "Pcmpw"; "Pcmpwi"; "Pcntlzd";
+ "Pcntlzw"; "Pcreqv"; "Pcror"; "Pcrxor"; "Pdcbf"; "Pdcbi"; "Pdcbt";
+ "Pdcbtls"; "Pdcbtst"; "Pdcbz"; "Pdivd"; "Pdivdu"; "Pdivw"; "Pdivwu";
+ "Peieio"; "Peqv"; "Pextsb"; "Pextsh"; "Pextsw"; "Pfabs"; "Pfadd"; "Pfadds";
+ "Pfcfid"; "Pfcmpu"; "Pfctidz"; "Pfctiw"; "Pfctiwz"; "Pfdiv"; "Pfdivs";
+ "Pfmadd"; "Pfmr"; "Pfmsub"; "Pfmul"; "Pfmuls"; "Pfneg"; "Pfnmadd";
+ "Pfnmsub"; "Pfres"; "Pfrsp"; "Pfrsqrte"; "Pfsel"; "Pfsqrt"; "Pfsub";
+ "Pfsubs"; "Picbi"; "Picbtls"; "Pinlineasm"; "Pisel"; "Pisync"; "Plabel";
+ "Plbz"; "Plbzx"; "Pld"; "Pldbrx"; "Pldi"; "Pldx"; "Plfd"; "Plfdx"; "Plfi";
+ "Plfis"; "Plfs"; "Plfsx"; "Plha"; "Plhax"; "Plhbrx"; "Plhz"; "Plhzx";
+ "Plwarx"; "Plwbrx"; "Plwsync"; "Plwz"; "Plwzu"; "Plwzx"; "Pmbar"; "Pmfcr";
+ "Pmflr"; "Pmfspr"; "Pmr"; "Pmtctr"; "Pmtlr"; "Pmtspr"; "Pmulhd"; "Pmulhdu";
+ "Pmulhw"; "Pmulhwu"; "Pmulld"; "Pmulli"; "Pmullw"; "Pnand"; "Pnor"; "Por";
+ "Porc"; "Pori"; "Poris"; "Prldicl"; "Prldimi"; "Prldinm"; "Prlwimi";
+ "Prlwinm"; "Psld"; "Pslw"; "Psrad"; "Psradi"; "Psraw"; "Psrawi"; "Psrd";
+ "Psrw"; "Pstb"; "Pstbx"; "Pstd"; "Pstdbrx"; "Pstdu"; "Pstdx"; "Pstfd";
+ "Pstfdu"; "Pstfdx"; "Pstfs"; "Pstfsx"; "Psth"; "Psthbrx"; "Psthx"; "Pstw";
+ "Pstwbrx"; "Pstwcx_"; "Pstwu"; "Pstwux"; "Pstwx"; "Psubfc"; "Psubfe";
+ "Psubfic"; "Psubfze"; "Psync"; "Ptrap"; "Pxor"; "Pxori"; "Pxoris"]
let pp_instructions pp ic =
let ic = List.filter (fun s -> match s with
@@ -126,7 +127,7 @@ let pp_instructions pp ic =
| Pcfi_rel_offset _ -> false
| _ -> true) ic in
let instruction pp n args =
- assert (List.mem n mnemonic_names);
+ assert (StringSet.mem n mnemonic_names);
pp_jobject_start pp;
pp_jmember ~first:true pp "Instruction Name" pp_jstring n;
pp_jmember pp "Args" (pp_jarray pp_arg) args;
@@ -251,7 +252,7 @@ let pp_instructions pp ic =
| Plhbrx (ir1,ir2,ir3) -> instruction pp "Plhbrx" [Ireg ir1; Ireg ir2; Ireg ir3]
| Plhz (ir1,c,ir2) -> instruction pp "Plhz" [Ireg ir1; Constant c; Ireg ir2]
| Plhzx (ir1,ir2,ir3) -> instruction pp "Plhzx" [Ireg ir1; Ireg ir2; Ireg ir3]
- | Pldi (ir,c) -> instruction pp "Pldi" [Ireg ir; Long c] (* FIXME Cint is too small, we need Clong *)
+ | Pldi (ir,c) -> instruction pp "Pldi" [Ireg ir; Long c]
| Plmake _ (* Should not occur *)
| Pllo _ (* Should not occur *)
| Plhi _ -> assert false (* Should not occur *)
@@ -385,8 +386,8 @@ let print_if prog sourcename =
| Some f ->
let f = Filename.concat !sdump_folder f in
let oc = open_out_bin f in
- pp_ast (formatter_of_out_channel oc) pp_instructions prog sourcename;
+ pp_ast oc pp_instructions prog sourcename;
close_out oc
let pp_mnemonics pp =
- pp_mnemonics pp mnemonic_names
+ pp_mnemonics pp (StringSet.elements mnemonic_names)