diff options
| -rw-r--r-- | arm/AsmToJSON.ml | 4 | ||||
| -rw-r--r-- | arm/AsmToJSON.mli | 2 | ||||
| -rw-r--r-- | driver/Driver.ml | 31 | ||||
| -rw-r--r-- | lib/Json.ml | 54 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 620 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.mli | 2 | ||||
| -rw-r--r-- | riscV/AsmToJSON.ml | 4 | ||||
| -rw-r--r-- | x86/AsmToJSON.ml | 4 | ||||
| -rw-r--r-- | x86/AsmToJSON.mli | 2 |
9 files changed, 370 insertions, 353 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index bb0c0c04..73706d3b 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -14,5 +14,5 @@ (* Dummy function *) -let p_program oc prog = - () +let pp_program pp prog = + Format.fprintf pp "null" diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli index 20bcba5e..e4d9c39a 100644 --- a/arm/AsmToJSON.mli +++ b/arm/AsmToJSON.mli @@ -10,4 +10,4 @@ (* *) (* *********************************************************************) -val p_program: out_channel -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit +val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit diff --git a/driver/Driver.ml b/driver/Driver.ml index 97082720..dfbac67f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -18,6 +18,7 @@ open Driveraux open Frontend open Assembler open Linker +open Json (* Optional sdump suffix *) let sdump_suffix = ref ".json" @@ -29,15 +30,29 @@ let jdump_magic_number = "CompCertJDUMP" ^ Version.version let dump_jasm asm sourcename destfile = let oc = open_out_bin destfile in - let print_args oc = - output_string oc Sys.executable_name; + 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 - fprintf oc " %s" (Responsefile.gnu_quote !argv.(i)) - done in - let dump_compile_info oc = - fprintf oc "{\n\"directory\":\"%s\",\n\"command\":\"%t\",\n\"file\":\"%s\"\n}" (Sys.getcwd ()) print_args sourcename in - fprintf oc "{\n\"Version\":\"%s\",\n\"System\":\"%s\"\n,\"Compile Info\" : %t,\n\"Compilation Unit\":\"%s\",\n\"Asm Ast\":%a}" - jdump_magic_number Configuration.system dump_compile_info sourcename AsmToJSON.p_program asm; + 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; + 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 diff --git a/lib/Json.ml b/lib/Json.ml index 22b50a9e..16819e8d 100644 --- a/lib/Json.ml +++ b/lib/Json.ml @@ -10,41 +10,51 @@ (* *) (* *********************************************************************) -open Printf +open Format (* Simple functions for JSON printing *) (* Print a string as json string *) -let p_jstring oc s = +let pp_jstring oc s = fprintf oc "\"%s\"" s -(* Print a list as json array *) -let p_jarray elem oc l = - match l with - | [] -> fprintf oc "[]" - | hd::tail -> - output_string oc "["; elem oc hd; - List.iter (fprintf oc ",%a" elem) tail; - output_string oc "]" - (* Print a bool as json bool *) -let p_jbool oc = fprintf oc "%B" +let pp_jbool oc = fprintf oc "%B" (* Print an int as json int *) -let p_jint oc = fprintf oc "%d" +let pp_jint oc = fprintf oc "%d" (* Print an int32 as json int *) -let p_jint32 oc = fprintf oc "%ld" +let pp_jint32 oc = fprintf oc "%ld" + +(* Print optional value *) +let pp_jopt pp_elem oc = function + | None -> output_string oc "null" + | Some i -> pp_elem oc i + +let pp_jobject_start pp = + fprintf pp "@[<v 1>{" + +let pp_jobject_end pp = + fprintf pp "@;<0 -1>}@]" (* Print a member *) -let p_jmember oc name p_mem mem = - fprintf oc "\n%a:%a" p_jstring name p_mem mem +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 (* Print singleton object *) -let p_jsingle_object oc name p_mem mem = - fprintf oc "{%a:%a}" p_jstring name p_mem mem +let pp_jsingle_object pp name pp_mem mem = + pp_jobject_start pp; + pp_jmember ~first:true pp name pp_mem mem; + pp_jobject_end pp -(* Print optional value *) -let p_jopt p_elem oc = function - | None -> output_string oc "null" - | Some i -> p_elem oc i +(* Print a list as json array *) +let pp_jarray elem pp l = + match l with + | [] -> fprintf pp "[]"; + | 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>]@]" diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index efb2d65d..3cfd42d3 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -18,61 +18,58 @@ open BinNums open C2C open Camlcoq open Json -open Printf +open Format open Sections -let p_reg oc t n = +let pp_reg pp t n = let s = sprintf "%s%s" t n in - p_jsingle_object oc "Register" p_jstring s + pp_jsingle_object pp "Register" pp_jstring s -let p_ireg oc reg = - p_reg oc "r" (TargetPrinter.int_reg_name reg) +let pp_ireg pp reg = + pp_reg pp "r" (TargetPrinter.int_reg_name reg) -let p_freg oc reg = - p_reg oc "f" (TargetPrinter.float_reg_name reg) +let pp_freg pp reg = + pp_reg pp "f" (TargetPrinter.float_reg_name reg) -let p_atom oc a = p_jstring oc (extern_atom a) +let pp_atom pp a = pp_jstring pp (extern_atom a) -let p_atom_constant oc a = p_jsingle_object oc "Atom" p_atom a +let pp_atom_constant pp a = pp_jsingle_object pp "Atom" pp_atom a -let p_int oc i = fprintf oc "%ld" (camlint_of_coqint i) -let p_int64 oc i = fprintf oc "%Ld" (camlint64_of_coqint i) -let p_float32 oc f = fprintf oc "%ld" (camlint_of_coqint (Floats.Float32.to_bits f)) -let p_float64 oc f = fprintf oc "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f)) -let p_z oc z = fprintf oc "%s" (Z.to_string z) +let pp_int pp i = fprintf pp "%ld" (camlint_of_coqint i) +let pp_int64 pp i = fprintf pp "%Ld" (camlint64_of_coqint i) +let pp_float32 pp f = fprintf pp "%ld" (camlint_of_coqint (Floats.Float32.to_bits f)) +let pp_float64 pp f = fprintf pp "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f)) +let pp_z pp z = fprintf pp "%s" (Z.to_string z) -let p_int_constant oc i = p_jsingle_object oc "Integer" p_int i -let p_float64_constant oc f = p_jsingle_object oc "Float" p_float64 f -let p_float32_constant oc f = p_jsingle_object oc "Float" p_float32 f +let pp_int_constant pp i = pp_jsingle_object pp "Integer" pp_int i +let pp_float64_constant pp f = pp_jsingle_object pp "Float" pp_float64 f +let pp_float32_constant pp f = pp_jsingle_object pp "Float" pp_float32 f -let p_sep oc = fprintf oc "," - -let p_constant oc c = - let p_symbol oc (i,c) = - output_string oc "{"; - p_jmember oc "Name" p_atom i; - p_sep oc; - p_jmember oc "Offset" p_int c; - output_string oc "}" in +let pp_constant pp c = + let pp_symbol pp (i,c) = + pp_jobject_start pp; + pp_jmember ~first:true pp "Name" pp_atom i; + pp_jmember pp "Offset" pp_int c; + pp_jobject_end pp in match c with - | Cint i -> p_int_constant oc i + | Cint i -> pp_int_constant pp i | Csymbol_low (i,c) -> - p_jsingle_object oc "Symbol_low" p_symbol (i,c) + pp_jsingle_object pp "Symbol_low" pp_symbol (i,c) | Csymbol_high (i,c) -> - p_jsingle_object oc "Symbol_high" p_symbol (i,c) + pp_jsingle_object pp "Symbol_high" pp_symbol (i,c) | Csymbol_sda (i,c) -> - p_jsingle_object oc "Symbol_sda" p_symbol (i,c) + pp_jsingle_object pp "Symbol_sda" pp_symbol (i,c) | Csymbol_rel_low (i,c) -> - p_jsingle_object oc "Symbol_rel_low" p_symbol (i,c) + pp_jsingle_object pp "Symbol_rel_low" pp_symbol (i,c) | Csymbol_rel_high (i,c) -> - p_jsingle_object oc "Symbol_rel_high" p_symbol (i,c) + pp_jsingle_object pp "Symbol_rel_high" pp_symbol (i,c) -let p_crbit oc c = - p_jsingle_object oc "CRbit" p_jint (TargetPrinter.num_crbit c) +let pp_crbit pp c = + pp_jsingle_object pp "CRbit" pp_jint (TargetPrinter.num_crbit c) -let p_label oc l = - p_jsingle_object oc "Label" p_jint32 (P.to_int32 l) +let pp_label pp l = + pp_jsingle_object pp "Label" pp_jint32 (P.to_int32 l) type instruction_arg = | Ireg of ireg @@ -96,259 +93,268 @@ let next_id () = let reset_id () = id := 0 -let p_arg oc = function - | Ireg ir -> p_ireg oc ir - | Freg fr -> p_freg oc fr - | Constant c -> p_constant oc c - | Long i -> p_jsingle_object oc "Integer" p_int64 i +let pp_arg pp = function + | Ireg ir -> pp_ireg pp ir + | Freg fr -> pp_freg pp fr + | Constant c -> pp_constant pp c + | Long i -> pp_jsingle_object pp "Integer" pp_int64 i | Id -> let i = next_id () in - p_jsingle_object oc "Integer" (fun oc i -> fprintf oc "%d" i) i - | Crbit cr -> p_crbit oc cr - | ALabel lbl -> p_label oc lbl - | Float32 f -> p_float32_constant oc f - | Float64 f -> p_float64_constant oc f - | Atom a -> p_atom_constant oc a + pp_jsingle_object pp "Integer" (fun pp i -> fprintf pp "%d" i) i + | Crbit cr -> pp_crbit pp cr + | ALabel lbl -> pp_label pp lbl + | Float32 f -> pp_float32_constant pp f + | Float64 f -> pp_float64_constant pp f + | Atom a -> pp_atom_constant pp a -let p_instruction oc ic = - let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_jarray p_arg) l - and inst_name oc s = p_jmember oc "Instruction Name" p_jstring s in - let first = ref true in - let sep oc = if !first then first := false else output_string oc ", " in - let instruction n args = fprintf oc "\n%t{%a,%a}" sep inst_name n p_args args in - let instruction = function +let pp_instructions pp ic = + let ic = List.filter (fun s -> match s with + | Pbuiltin (ef,_,_) -> + begin match ef with + | EF_inline_asm _ -> true + | _ -> false + end + | Pcfi_adjust _ (* Only debug relevant *) + | Pcfi_rel_offset _ -> false + | _ -> true) ic in + let instruction pp n args = + pp_jobject_start pp; + pp_jmember ~first:true pp "Instruction Name" pp_jstring n; + pp_jmember pp "Args" (pp_jarray pp_arg) args; + pp_jobject_end pp in + let instruction pp = function | Padd (ir1,ir2,ir3) - | Padd64 (ir1,ir2,ir3) -> instruction "Padd" [Ireg ir1; Ireg ir2; Ireg ir3] - | Paddc (ir1,ir2,ir3) -> instruction "Paddc" [Ireg ir1; Ireg ir2; Ireg ir3] - | Padde (ir1,ir2,ir3) -> instruction "Padde" [Ireg ir1; Ireg ir2; Ireg ir3] - | Paddi (ir1,ir2,c) -> instruction "Paddi" [Ireg ir1; Ireg ir2; Constant c] - | Paddi64 (ir1,ir2,n) -> instruction "Paddi" [Ireg ir1; Ireg ir2; Constant (Cint n)] (* FIXME, ugly, immediates are int64 but always fit into 16bits *) - | Paddic (ir1,ir2,c) -> instruction "Paddic" [Ireg ir1; Ireg ir2; Constant c] - | Paddis (ir1,ir2,c) -> instruction "Paddis" [Ireg ir1; Ireg ir2; Constant c] - | Paddis64 (ir1,ir2,n) -> instruction "Paddis" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Padd64 (ir1,ir2,ir3) -> instruction pp "Padd" [Ireg ir1; Ireg ir2; Ireg ir3] + | Paddc (ir1,ir2,ir3) -> instruction pp "Paddc" [Ireg ir1; Ireg ir2; Ireg ir3] + | Padde (ir1,ir2,ir3) -> instruction pp "Padde" [Ireg ir1; Ireg ir2; Ireg ir3] + | Paddi (ir1,ir2,c) -> instruction pp "Paddi" [Ireg ir1; Ireg ir2; Constant c] + | Paddi64 (ir1,ir2,n) -> instruction pp "Paddi" [Ireg ir1; Ireg ir2; Constant (Cint n)] (* FIXME, ugly, immediates are int64 but always fit into 16bits *) + | Paddic (ir1,ir2,c) -> instruction pp "Paddic" [Ireg ir1; Ireg ir2; Constant c] + | Paddis (ir1,ir2,c) -> instruction pp "Paddis" [Ireg ir1; Ireg ir2; Constant c] + | Paddis64 (ir1,ir2,n) -> instruction pp "Paddis" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Paddze (ir1,ir2) - | Paddze64 (ir1,ir2) -> instruction "Paddze" [Ireg ir1; Ireg ir2] - | Pallocframe _ -> assert false (* Should not occur *) + | Paddze64 (ir1,ir2) -> instruction pp "Paddze" [Ireg ir1; Ireg ir2] + | Pallocframe _ -> assert false (* Should not ppcur *) | Pand_ (ir1,ir2,ir3) - | Pand_64 (ir1,ir2,ir3) -> instruction "Pand_" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pandc (ir1,ir2,ir3) -> instruction "Pandc" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pandi_ (ir1,ir2,c) -> instruction "Pandi_" [Ireg ir1; Ireg ir2; Constant c] - | Pandi_64 (ir1,ir2,n) -> instruction "Pandi_" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Pandis_ (ir1,ir2,c) -> instruction "Pandis_" [Ireg ir1; Ireg ir2; Constant c] - | Pandis_64 (ir1,ir2,n) -> instruction "Pandis_" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Pb l -> instruction "Pb" [ALabel l] - | Pbctr s -> instruction "Pbctr" [] - | Pbctrl s -> instruction "Pbctrl" [] - | Pbdnz l -> instruction "Pbdnz" [ALabel l] - | Pbf (cr,l) -> instruction "Pbf" [Crbit cr; ALabel l] - | Pbl (i,s) -> instruction "Pbl" [Atom i] - | Pbs (i,s) -> instruction "Pbs" [Atom i] - | Pblr -> instruction "Pblr" [] - | Pbt (cr,l) -> instruction "Pbt" [Crbit cr; ALabel l] - | Pbtbl (i,lb) -> instruction "Pbtbl" ((Ireg i)::(List.map (fun a -> ALabel a) lb)) - | Pcmpb (ir1,ir2,ir3) -> instruction "Pcmpb" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pcmpld (ir1,ir2) -> instruction "Pcmpld" [Ireg ir1; Ireg ir2] - | Pcmpldi (ir,n) -> instruction "Pcmpldi" [Ireg ir; Constant (Cint n)] - | Pcmplw (ir1,ir2) -> instruction "Pcmplw" [Ireg ir1; Ireg ir2] - | Pcmplwi (ir,c) -> instruction "Pcmplwi" [Ireg ir; Constant c] - | Pcmpd (ir1,ir2) -> instruction "Pcmpd" [Ireg ir1; Ireg ir2] - | Pcmpdi (ir,n) -> instruction "Pcmpdi" [Ireg ir; Constant (Cint n)] - | Pcmpw (ir1,ir2) -> instruction "Pcmpw" [Ireg ir1; Ireg ir2] - | Pcmpwi (ir,c) -> instruction "Pcmpwi" [Ireg ir; Constant c] - | Pcntlzd (ir1,ir2) -> instruction "Pcntlzd" [Ireg ir1; Ireg ir2] - | Pcntlzw (ir1,ir2) -> instruction "Pcntlzw" [Ireg ir1; Ireg ir2] - | Pcreqv (cr1,cr2,cr3) -> instruction "Pcreqv" [Crbit cr1; Crbit cr2; Crbit cr3] - | Pcror (cr1,cr2,cr3) -> instruction "Pcror" [Crbit cr1; Crbit cr2; Crbit cr3] - | Pcrxor (cr1,cr2,cr3) -> instruction "Pcrxor" [Crbit cr1; Crbit cr2; Crbit cr3] - | Pdcbf (ir1,ir2) -> instruction "Pdcbf" [Ireg ir1; Ireg ir2] - | Pdcbi (ir1,ir2) -> instruction "Pdcbi" [Ireg ir1; Ireg ir2] - | Pdcbt (n,ir1,ir2) -> instruction "Pdcbt" [Constant (Cint n); Ireg ir1; Ireg ir2] - | Pdcbtst (n,ir1,ir2) -> instruction "Pdcbtst" [Constant (Cint n); Ireg ir1; Ireg ir2] - | Pdcbtls (n,ir1,ir2) -> instruction "Pdcbtls" [Constant (Cint n); Ireg ir1; Ireg ir2] - | Pdcbz (ir1,ir2) -> instruction "Pdcbz" [Ireg ir1; Ireg ir2] - | Pdivw (ir1,ir2,ir3) -> instruction "Pdivw" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pdivd (ir1,ir2,ir3) -> instruction "Pdivd" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pdivwu (ir1,ir2,ir3) -> instruction "Pdivwu" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pdivdu (ir1,ir2,ir3) -> instruction "Pdivdu" [Ireg ir1; Ireg ir2; Ireg ir3] - | Peieio -> instruction "Peieio" [] - | Peqv (ir1,ir2,ir3) -> instruction "Peqv" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pextsb (ir1,ir2) -> instruction "Pextsb" [Ireg ir1; Ireg ir2] - | Pextsh (ir1,ir2) -> instruction "Pextsh" [Ireg ir1; Ireg ir2] - | Pextsw (ir1,ir2) -> instruction "Pextsw" [Ireg ir1; Ireg ir2] - | Pextzw (ir1,ir2) -> assert false (* Should not occur *) - | Pfreeframe (c,i) -> assert false (* Should not occur *) + | Pand_64 (ir1,ir2,ir3) -> instruction pp "Pand_" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pandc (ir1,ir2,ir3) -> instruction pp "Pandc" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pandi_ (ir1,ir2,c) -> instruction pp "Pandi_" [Ireg ir1; Ireg ir2; Constant c] + | Pandi_64 (ir1,ir2,n) -> instruction pp "Pandi_" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Pandis_ (ir1,ir2,c) -> instruction pp "Pandis_" [Ireg ir1; Ireg ir2; Constant c] + | Pandis_64 (ir1,ir2,n) -> instruction pp "Pandis_" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Pb l -> instruction pp "Pb" [ALabel l] + | Pbctr s -> instruction pp "Pbctr" [] + | Pbctrl s -> instruction pp "Pbctrl" [] + | Pbdnz l -> instruction pp "Pbdnz" [ALabel l] + | Pbf (cr,l) -> instruction pp "Pbf" [Crbit cr; ALabel l] + | Pbl (i,s) -> instruction pp "Pbl" [Atom i] + | Pbs (i,s) -> instruction pp "Pbs" [Atom i] + | Pblr -> instruction pp "Pblr" [] + | Pbt (cr,l) -> instruction pp "Pbt" [Crbit cr; ALabel l] + | Pbtbl (i,lb) -> instruction pp "Pbtbl" ((Ireg i)::(List.map (fun a -> ALabel a) lb)) + | Pcmpb (ir1,ir2,ir3) -> instruction pp "Pcmpb" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pcmpld (ir1,ir2) -> instruction pp "Pcmpld" [Ireg ir1; Ireg ir2] + | Pcmpldi (ir,n) -> instruction pp "Pcmpldi" [Ireg ir; Constant (Cint n)] + | Pcmplw (ir1,ir2) -> instruction pp "Pcmplw" [Ireg ir1; Ireg ir2] + | Pcmplwi (ir,c) -> instruction pp "Pcmplwi" [Ireg ir; Constant c] + | Pcmpd (ir1,ir2) -> instruction pp "Pcmpd" [Ireg ir1; Ireg ir2] + | Pcmpdi (ir,n) -> instruction pp "Pcmpdi" [Ireg ir; Constant (Cint n)] + | Pcmpw (ir1,ir2) -> instruction pp "Pcmpw" [Ireg ir1; Ireg ir2] + | Pcmpwi (ir,c) -> instruction pp "Pcmpwi" [Ireg ir; Constant c] + | Pcntlzd (ir1,ir2) -> instruction pp "Pcntlzd" [Ireg ir1; Ireg ir2] + | Pcntlzw (ir1,ir2) -> instruction pp "Pcntlzw" [Ireg ir1; Ireg ir2] + | Pcreqv (cr1,cr2,cr3) -> instruction pp "Pcreqv" [Crbit cr1; Crbit cr2; Crbit cr3] + | Pcror (cr1,cr2,cr3) -> instruction pp "Pcror" [Crbit cr1; Crbit cr2; Crbit cr3] + | Pcrxor (cr1,cr2,cr3) -> instruction pp "Pcrxor" [Crbit cr1; Crbit cr2; Crbit cr3] + | Pdcbf (ir1,ir2) -> instruction pp "Pdcbf" [Ireg ir1; Ireg ir2] + | Pdcbi (ir1,ir2) -> instruction pp "Pdcbi" [Ireg ir1; Ireg ir2] + | Pdcbt (n,ir1,ir2) -> instruction pp "Pdcbt" [Constant (Cint n); Ireg ir1; Ireg ir2] + | Pdcbtst (n,ir1,ir2) -> instruction pp "Pdcbtst" [Constant (Cint n); Ireg ir1; Ireg ir2] + | Pdcbtls (n,ir1,ir2) -> instruction pp "Pdcbtls" [Constant (Cint n); Ireg ir1; Ireg ir2] + | Pdcbz (ir1,ir2) -> instruction pp "Pdcbz" [Ireg ir1; Ireg ir2] + | Pdivw (ir1,ir2,ir3) -> instruction pp "Pdivw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pdivd (ir1,ir2,ir3) -> instruction pp "Pdivd" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pdivwu (ir1,ir2,ir3) -> instruction pp "Pdivwu" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pdivdu (ir1,ir2,ir3) -> instruction pp "Pdivdu" [Ireg ir1; Ireg ir2; Ireg ir3] + | Peieio -> instruction pp "Peieio" [] + | Peqv (ir1,ir2,ir3) -> instruction pp "Peqv" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pextsb (ir1,ir2) -> instruction pp "Pextsb" [Ireg ir1; Ireg ir2] + | Pextsh (ir1,ir2) -> instruction pp "Pextsh" [Ireg ir1; Ireg ir2] + | Pextsw (ir1,ir2) -> instruction pp "Pextsw" [Ireg ir1; Ireg ir2] + | Pextzw (ir1,ir2) -> assert false (* Should not ppcur *) + | Pfreeframe (c,i) -> assert false (* Should not ppcur *) | Pfabs (fr1,fr2) - | Pfabss (fr1,fr2) -> instruction "Pfabs" [Freg fr1; Freg fr2] - | Pfadd (fr1,fr2,fr3) -> instruction "Pfadd" [Freg fr1; Freg fr2; Freg fr3] - | Pfadds (fr1,fr2,fr3) -> instruction "Pfadds" [Freg fr1; Freg fr2; Freg fr3] - | Pfcmpu (fr1,fr2) -> instruction "Pfcmpu" [Freg fr1; Freg fr2] + | Pfabss (fr1,fr2) -> instruction pp "Pfabs" [Freg fr1; Freg fr2] + | Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3] + | Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3] + | Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2] | Pfcfi (ir,fr) - | Pfcfl (ir,fr) -> assert false (* Should not occur *) - | Pfcfid (fr1,fr2) -> instruction "Pfcfid" [Freg fr1; Freg fr2] - | Pfcfiu _ (* Should not occur *) - | Pfcti _ (* Should not occur *) - | Pfctiu _ (* Should not occur *) - | Pfctid _ -> assert false (* Should not occur *) - | Pfctidz (fr1,fr2) -> instruction "Pfctidz" [Freg fr1; Freg fr2] - | Pfctiw (fr1,fr2) -> instruction "Pfctiw" [Freg fr1; Freg fr2] - | Pfctiwz (fr1,fr2) -> instruction "Pfctiwz" [Freg fr1; Freg fr2] - | Pfdiv (fr1,fr2,fr3) -> instruction "Pfdiv" [Freg fr1; Freg fr2; Freg fr3] - | Pfdivs (fr1,fr2,fr3) -> instruction "Pfdivs" [Freg fr1; Freg fr2; Freg fr3] - | Pfmake (fr,ir1,ir2) -> assert false (* Should not occur *) - | Pfmr (fr1,fr2) -> instruction "Pfmr" [Freg fr1; Freg fr2] - | Pfmul (fr1,fr2,fr3) -> instruction "Pfmul" [Freg fr1; Freg fr2; Freg fr3] - | Pfmuls(fr1,fr2,fr3) -> instruction "Pfmuls" [Freg fr1; Freg fr2; Freg fr3] + | Pfcfl (ir,fr) -> assert false (* Should not ppcur *) + | Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2] + | Pfcfiu _ (* Should not ppcur *) + | Pfcti _ (* Should not ppcur *) + | Pfctiu _ (* Should not ppcur *) + | Pfctid _ -> assert false (* Should not ppcur *) + | Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2] + | Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2] + | Pfctiwz (fr1,fr2) -> instruction pp "Pfctiwz" [Freg fr1; Freg fr2] + | Pfdiv (fr1,fr2,fr3) -> instruction pp "Pfdiv" [Freg fr1; Freg fr2; Freg fr3] + | Pfdivs (fr1,fr2,fr3) -> instruction pp "Pfdivs" [Freg fr1; Freg fr2; Freg fr3] + | Pfmake (fr,ir1,ir2) -> assert false (* Should not ppcur *) + | Pfmr (fr1,fr2) -> instruction pp "Pfmr" [Freg fr1; Freg fr2] + | Pfmul (fr1,fr2,fr3) -> instruction pp "Pfmul" [Freg fr1; Freg fr2; Freg fr3] + | Pfmuls(fr1,fr2,fr3) -> instruction pp "Pfmuls" [Freg fr1; Freg fr2; Freg fr3] | Pfneg (fr1,fr2) - | Pfnegs (fr1,fr2) -> instruction "Pfneg" [Freg fr1; Freg fr2] - | Pfrsp (fr1,fr2) -> instruction "Pfrsp" [Freg fr1; Freg fr2] - | Pfxdp (fr1,fr2) -> assert false (* Should not occur *) - | Pfsub (fr1,fr2,fr3) -> instruction "Pfsub" [Freg fr1; Freg fr2; Freg fr3] - | Pfsubs (fr1,fr2,fr3) -> instruction "Pfsubs" [Freg fr1; Freg fr2; Freg fr3] - | Pfmadd (fr1,fr2,fr3,fr4) -> instruction "Pfmadd" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] - | Pfmsub (fr1,fr2,fr3,fr4) -> instruction "Pfmsub" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] - | Pfnmadd (fr1,fr2,fr3,fr4) -> instruction "Pfnmadd" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] - | Pfnmsub (fr1,fr2,fr3,fr4) -> instruction "Pfnmsub" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] - | Pfsqrt (fr1,fr2) -> instruction "Pfsqrt" [Freg fr1; Freg fr2] - | Pfrsqrte (fr1,fr2) -> instruction "Pfrsqrte" [Freg fr1; Freg fr2] - | Pfres (fr1,fr2) -> instruction "Pfres" [Freg fr1; Freg fr2] - | Pfsel (fr1,fr2,fr3,fr4) -> instruction "Pfsel" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] - | Pisel (ir1,ir2,ir3,cr) -> instruction "Pisel" [Ireg ir1; Ireg ir2; Ireg ir3; Crbit cr] - | Picbi (ir1,ir2) -> instruction "Picbi" [Ireg ir1; Ireg ir2] - | Picbtls (n,ir1,ir2) -> instruction "Picbtls" [Constant (Cint n);Ireg ir1; Ireg ir2] - | Pisync -> instruction "Pisync" [] - | Plwsync -> instruction "Plwsync" [] - | Plbz (ir1,c,ir2) -> instruction "Plbz" [Ireg ir1; Constant c; Ireg ir2] - | Plbzx (ir1,ir2,ir3) -> instruction "Plbzx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pfnegs (fr1,fr2) -> instruction pp "Pfneg" [Freg fr1; Freg fr2] + | Pfrsp (fr1,fr2) -> instruction pp "Pfrsp" [Freg fr1; Freg fr2] + | Pfxdp (fr1,fr2) -> assert false (* Should not ppcur *) + | Pfsub (fr1,fr2,fr3) -> instruction pp "Pfsub" [Freg fr1; Freg fr2; Freg fr3] + | Pfsubs (fr1,fr2,fr3) -> instruction pp "Pfsubs" [Freg fr1; Freg fr2; Freg fr3] + | Pfmadd (fr1,fr2,fr3,fr4) -> instruction pp "Pfmadd" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] + | Pfmsub (fr1,fr2,fr3,fr4) -> instruction pp "Pfmsub" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] + | Pfnmadd (fr1,fr2,fr3,fr4) -> instruction pp "Pfnmadd" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] + | Pfnmsub (fr1,fr2,fr3,fr4) -> instruction pp "Pfnmsub" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] + | Pfsqrt (fr1,fr2) -> instruction pp "Pfsqrt" [Freg fr1; Freg fr2] + | Pfrsqrte (fr1,fr2) -> instruction pp "Pfrsqrte" [Freg fr1; Freg fr2] + | Pfres (fr1,fr2) -> instruction pp "Pfres" [Freg fr1; Freg fr2] + | Pfsel (fr1,fr2,fr3,fr4) -> instruction pp "Pfsel" [Freg fr1; Freg fr2; Freg fr3; Freg fr4] + | Pisel (ir1,ir2,ir3,cr) -> instruction pp "Pisel" [Ireg ir1; Ireg ir2; Ireg ir3; Crbit cr] + | Picbi (ir1,ir2) -> instruction pp "Picbi" [Ireg ir1; Ireg ir2] + | Picbtls (n,ir1,ir2) -> instruction pp "Picbtls" [Constant (Cint n);Ireg ir1; Ireg ir2] + | Pisync -> instruction pp "Pisync" [] + | Plwsync -> instruction pp "Plwsync" [] + | Plbz (ir1,c,ir2) -> instruction pp "Plbz" [Ireg ir1; Constant c; Ireg ir2] + | Plbzx (ir1,ir2,ir3) -> instruction pp "Plbzx" [Ireg ir1; Ireg ir2; Ireg ir3] | Pld (ir1,c,ir2) - | Pld_a (ir1,c,ir2) -> instruction "Pld" [Ireg ir1; Constant c; Ireg ir2] + | Pld_a (ir1,c,ir2) -> instruction pp "Pld" [Ireg ir1; Constant c; Ireg ir2] | Pldx (ir1,ir2,ir3) - | Pldx_a (ir1,ir2,ir3) -> instruction "Pldx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pldx_a (ir1,ir2,ir3) -> instruction pp "Pldx" [Ireg ir1; Ireg ir2; Ireg ir3] | Plfd (fr,c,ir) - | Plfd_a (fr,c,ir) -> instruction "Plfd" [Freg fr; Constant c; Ireg ir] + | Plfd_a (fr,c,ir) -> instruction pp "Plfd" [Freg fr; Constant c; Ireg ir] | Plfdx (fr,ir1,ir2) - | Plfdx_a (fr,ir1,ir2) -> instruction "Plfdx" [Freg fr; Ireg ir1; Ireg ir2] - | Plfs (fr,c,ir) -> instruction "Plfs" [Freg fr; Constant c; Ireg ir] - | Plfsx (fr,ir1,ir2) -> instruction "Plfsx" [Freg fr; Ireg ir1; Ireg ir2] - | Plha (ir1,c,ir2) -> instruction "Plha" [Ireg ir1; Constant c; Ireg ir2] - | Plhax (ir1,ir2,ir3) -> instruction "Plhax" [Ireg ir1; Ireg ir2; Ireg ir3] - | Plhbrx (ir1,ir2,ir3) -> instruction "Plhbrx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Plhz (ir1,c,ir2) -> instruction "Plhz" [Ireg ir1; Constant c; Ireg ir2] - | Plhzx (ir1,ir2,ir3) -> instruction "Plhzx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pldi (ir,c) -> instruction "Pldi" [Ireg ir; Long c] (* FIXME Cint is too small, we need Clong *) - | Plmake _ (* Should not occur *) - | Pllo _ (* Should not occur *) - | Plhi _ -> assert false (* Should not occur *) - | Plfi (fr,fc) -> instruction "Plfi" [Freg fr; Float64 fc] - | Plfis (fr,fc) -> instruction "Plfis" [Freg fr; Float32 fc] + | Plfdx_a (fr,ir1,ir2) -> instruction pp "Plfdx" [Freg fr; Ireg ir1; Ireg ir2] + | Plfs (fr,c,ir) -> instruction pp "Plfs" [Freg fr; Constant c; Ireg ir] + | Plfsx (fr,ir1,ir2) -> instruction pp "Plfsx" [Freg fr; Ireg ir1; Ireg ir2] + | Plha (ir1,c,ir2) -> instruction pp "Plha" [Ireg ir1; Constant c; Ireg ir2] + | Plhax (ir1,ir2,ir3) -> instruction pp "Plhax" [Ireg ir1; Ireg ir2; Ireg ir3] + | 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 *) + | Plmake _ (* Should not ppcur *) + | Pllo _ (* Should not ppcur *) + | Plhi _ -> assert false (* Should not ppcur *) + | Plfi (fr,fc) -> instruction pp "Plfi" [Freg fr; Float64 fc] + | Plfis (fr,fc) -> instruction pp "Plfis" [Freg fr; Float32 fc] | Plwz (ir1,c,ir2) - | Plwz_a (ir1,c,ir2) -> instruction "Plwz" [Ireg ir1;Constant c; Ireg ir2] - | Plwzu (ir1,c,ir2) -> instruction "Plwzu" [Ireg ir1; Constant c; Ireg ir2] + | Plwz_a (ir1,c,ir2) -> instruction pp "Plwz" [Ireg ir1;Constant c; Ireg ir2] + | Plwzu (ir1,c,ir2) -> instruction pp "Plwzu" [Ireg ir1; Constant c; Ireg ir2] | Plwzx (ir1,ir2,ir3) - | Plwzx_a (ir1,ir2,ir3) -> instruction "Plwzx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Plwarx (ir1,ir2,ir3) -> instruction "Plwarx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Plwbrx (ir1,ir2,ir3) -> instruction "Plwbrx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pmbar c -> instruction "Pmbar" [Constant (Cint c)] - | Pmfcr ir -> instruction "Pmfcr" [Ireg ir] - | Pmfcrbit (ir,crb) -> assert false (* Should not occur *) - | Pmflr ir -> instruction "Pmflr" [Ireg ir] - | Pmr (ir1,ir2) -> instruction "Pmr" [Ireg ir1; Ireg ir2] - | Pmtctr ir -> instruction "Pmtctr" [Ireg ir] - | Pmtlr ir -> instruction "Pmtlr" [Ireg ir] - | Pmfspr(ir, n) -> instruction "Pmfspr" [Ireg ir; Constant (Cint n)] - | Pmtspr(n, ir) -> instruction "Pmtspr" [Constant (Cint n); Ireg ir] - | Pmulhd (ir1,ir2,ir3) -> instruction "Pmulhd" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pmulhdu (ir1,ir2,ir3) -> instruction "Pmulhdu" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pmulld (ir1,ir2,ir3) -> instruction "Pmulld" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pmulli (ir1,ir2,c) -> instruction "Pmulli" [Ireg ir1; Ireg ir2; Constant c] - | Pmullw (ir1,ir2,ir3) -> instruction "Pmullw" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pmulhw (ir1,ir2,ir3) -> instruction "Pmulhw" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pmulhwu (ir1,ir2,ir3) -> instruction "Pmulhwu" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pnand (ir1,ir2,ir3) -> instruction "Pnand" [Ireg ir1; Ireg ir2; Ireg ir3] + | Plwzx_a (ir1,ir2,ir3) -> instruction pp "Plwzx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Plwarx (ir1,ir2,ir3) -> instruction pp "Plwarx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Plwbrx (ir1,ir2,ir3) -> instruction pp "Plwbrx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmbar c -> instruction pp "Pmbar" [Constant (Cint c)] + | Pmfcr ir -> instruction pp "Pmfcr" [Ireg ir] + | Pmfcrbit (ir,crb) -> assert false (* Should not ppcur *) + | Pmflr ir -> instruction pp "Pmflr" [Ireg ir] + | Pmr (ir1,ir2) -> instruction pp "Pmr" [Ireg ir1; Ireg ir2] + | Pmtctr ir -> instruction pp "Pmtctr" [Ireg ir] + | Pmtlr ir -> instruction pp "Pmtlr" [Ireg ir] + | Pmfspr(ir, n) -> instruction pp "Pmfspr" [Ireg ir; Constant (Cint n)] + | Pmtspr(n, ir) -> instruction pp "Pmtspr" [Constant (Cint n); Ireg ir] + | Pmulhd (ir1,ir2,ir3) -> instruction pp "Pmulhd" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulhdu (ir1,ir2,ir3) -> instruction pp "Pmulhdu" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulld (ir1,ir2,ir3) -> instruction pp "Pmulld" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulli (ir1,ir2,c) -> instruction pp "Pmulli" [Ireg ir1; Ireg ir2; Constant c] + | Pmullw (ir1,ir2,ir3) -> instruction pp "Pmullw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulhw (ir1,ir2,ir3) -> instruction pp "Pmulhw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulhwu (ir1,ir2,ir3) -> instruction pp "Pmulhwu" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pnand (ir1,ir2,ir3) -> instruction pp "Pnand" [Ireg ir1; Ireg ir2; Ireg ir3] | Pnor (ir1,ir2,ir3) - | Pnor64 (ir1,ir2,ir3) -> instruction "Pnor" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pnor64 (ir1,ir2,ir3) -> instruction pp "Pnor" [Ireg ir1; Ireg ir2; Ireg ir3] | Por (ir1,ir2,ir3) - | Por64 (ir1,ir2,ir3) -> instruction "Por" [Ireg ir1; Ireg ir2; Ireg ir3] - | Porc (ir1,ir2,ir3) -> instruction "Porc" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pori (ir1,ir2,c) -> instruction "Pori" [Ireg ir1; Ireg ir2; Constant c] - | Pori64 (ir1,ir2,n) -> instruction "Pori" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Poris (ir1,ir2,c) -> instruction "Poris" [Ireg ir1; Ireg ir2; Constant c] - | Poris64 (ir1,ir2,n) -> instruction "Poris" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Prldicl (ir1,ir2,ic1,ic2) -> instruction "Prldicl" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] - | Prldinm (ir1,ir2,ic1,ic2) -> instruction "Prldinm" [Ireg ir1; Ireg ir2; Long ic1; Long ic2] - | Prldimi (ir1,ir2,ic1,ic2) ->instruction "Prldimi" [Ireg ir1; Ireg ir2; Long ic1; Long ic2] - | Prlwinm (ir1,ir2,ic1,ic2) -> instruction "Prlwinm" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] - | Prlwimi (ir1,ir2,ic1,ic2) ->instruction "Prlwimi" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] - | Psld (ir1,ir2,ir3) -> instruction "Psld" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pslw (ir1,ir2,ir3) -> instruction "Pslw" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psrad (ir1,ir2,ir3) -> instruction "Psrad" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psradi (ir1,ir2,ic) -> instruction "Psradi" [Ireg ir1; Ireg ir2; Constant (Cint ic)] - | Psraw (ir1,ir2,ir3) -> instruction "Psraw" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psrawi (ir1,ir2,ic) -> instruction "Psrawi" [Ireg ir1; Ireg ir2; Constant (Cint ic)] - | Psrd (ir1,ir2,ir3) -> instruction "Psrd" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psrw (ir1,ir2,ir3) -> instruction "Psrw" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pstb (ir1,c,ir2) -> instruction "Pstb" [Ireg ir1; Constant c; Ireg ir2] - | Pstbx (ir1,ir2,ir3) -> instruction "Pstbx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Por64 (ir1,ir2,ir3) -> instruction pp "Por" [Ireg ir1; Ireg ir2; Ireg ir3] + | Porc (ir1,ir2,ir3) -> instruction pp "Porc" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pori (ir1,ir2,c) -> instruction pp "Pori" [Ireg ir1; Ireg ir2; Constant c] + | Pori64 (ir1,ir2,n) -> instruction pp "Pori" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Poris (ir1,ir2,c) -> instruction pp "Poris" [Ireg ir1; Ireg ir2; Constant c] + | Poris64 (ir1,ir2,n) -> instruction pp "Poris" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Prldicl (ir1,ir2,ic1,ic2) -> instruction pp "Prldicl" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Prldinm (ir1,ir2,ic1,ic2) -> instruction pp "Prldinm" [Ireg ir1; Ireg ir2; Long ic1; Long ic2] + | Prldimi (ir1,ir2,ic1,ic2) ->instruction pp "Prldimi" [Ireg ir1; Ireg ir2; Long ic1; Long ic2] + | Prlwinm (ir1,ir2,ic1,ic2) -> instruction pp "Prlwinm" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Prlwimi (ir1,ir2,ic1,ic2) ->instruction pp "Prlwimi" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Psld (ir1,ir2,ir3) -> instruction pp "Psld" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pslw (ir1,ir2,ir3) -> instruction pp "Pslw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psrad (ir1,ir2,ir3) -> instruction pp "Psrad" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psradi (ir1,ir2,ic) -> instruction pp "Psradi" [Ireg ir1; Ireg ir2; Constant (Cint ic)] + | Psraw (ir1,ir2,ir3) -> instruction pp "Psraw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psrawi (ir1,ir2,ic) -> instruction pp "Psrawi" [Ireg ir1; Ireg ir2; Constant (Cint ic)] + | Psrd (ir1,ir2,ir3) -> instruction pp "Psrd" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psrw (ir1,ir2,ir3) -> instruction pp "Psrw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstb (ir1,c,ir2) -> instruction pp "Pstb" [Ireg ir1; Constant c; Ireg ir2] + | Pstbx (ir1,ir2,ir3) -> instruction pp "Pstbx" [Ireg ir1; Ireg ir2; Ireg ir3] | Pstd (ir1,c,ir2) - | Pstd_a (ir1,c,ir2) -> instruction "Pstd" [Ireg ir1; Constant c; Ireg ir2] + | Pstd_a (ir1,c,ir2) -> instruction pp "Pstd" [Ireg ir1; Constant c; Ireg ir2] | Pstdx (ir1,ir2,ir3) - | Pstdx_a (ir1,ir2,ir3) -> instruction "Pstdx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pstdu (ir1,c,ir2) -> instruction "Pstdu" [Ireg ir1; Constant c; Ireg ir2] + | Pstdx_a (ir1,ir2,ir3) -> instruction pp "Pstdx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstdu (ir1,c,ir2) -> instruction pp "Pstdu" [Ireg ir1; Constant c; Ireg ir2] | Pstfd (fr,c,ir) - | Pstfd_a (fr,c,ir) -> instruction "Pstfd" [Freg fr; Constant c; Ireg ir] - | Pstfdu (fr,c,ir) -> instruction "Pstfdu" [Freg fr; Constant c; Ireg ir] + | Pstfd_a (fr,c,ir) -> instruction pp "Pstfd" [Freg fr; Constant c; Ireg ir] + | Pstfdu (fr,c,ir) -> instruction pp "Pstfdu" [Freg fr; Constant c; Ireg ir] | Pstfdx (fr,ir1,ir2) - | Pstfdx_a (fr,ir1,ir2) -> instruction "Pstfdx" [Freg fr; Ireg ir1; Ireg ir2] - | Pstfs (fr,c,ir) -> instruction "Pstfs" [Freg fr; Constant c; Ireg ir] - | Pstfsx (fr,ir1,ir2) -> instruction "Pstfsx" [Freg fr; Ireg ir1; Ireg ir2] - | Psth (ir1,c,ir2) -> instruction "Psth" [Ireg ir1; Constant c; Ireg ir2] - | Psthx (ir1,ir2,ir3) -> instruction "Psthx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psthbrx (ir1,ir2,ir3) -> instruction "Psthbrx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstfdx_a (fr,ir1,ir2) -> instruction pp "Pstfdx" [Freg fr; Ireg ir1; Ireg ir2] + | Pstfs (fr,c,ir) -> instruction pp "Pstfs" [Freg fr; Constant c; Ireg ir] + | Pstfsx (fr,ir1,ir2) -> instruction pp "Pstfsx" [Freg fr; Ireg ir1; Ireg ir2] + | Psth (ir1,c,ir2) -> instruction pp "Psth" [Ireg ir1; Constant c; Ireg ir2] + | Psthx (ir1,ir2,ir3) -> instruction pp "Psthx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psthbrx (ir1,ir2,ir3) -> instruction pp "Psthbrx" [Ireg ir1; Ireg ir2; Ireg ir3] | Pstw (ir1,c,ir2) - | Pstw_a (ir1,c,ir2) -> instruction "Pstw" [Ireg ir1; Constant c; Ireg ir2] - | Pstwu (ir1,c,ir2) -> instruction "Pstwu" [Ireg ir1; Constant c; Ireg ir2] + | Pstw_a (ir1,c,ir2) -> instruction pp "Pstw" [Ireg ir1; Constant c; Ireg ir2] + | Pstwu (ir1,c,ir2) -> instruction pp "Pstwu" [Ireg ir1; Constant c; Ireg ir2] | Pstwx (ir1,ir2,ir3) - | Pstwx_a (ir1,ir2,ir3) -> instruction "Pstwx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pstwux (ir1,ir2,ir3) -> instruction "Pstwux" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pstwbrx (ir1,ir2,ir3) -> instruction "Pstwbrx" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pstwcx_ (ir1,ir2,ir3) -> instruction "Pstwcx_" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstwx_a (ir1,ir2,ir3) -> instruction pp "Pstwx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstwux (ir1,ir2,ir3) -> instruction pp "Pstwux" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstwbrx (ir1,ir2,ir3) -> instruction pp "Pstwbrx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstwcx_ (ir1,ir2,ir3) -> instruction pp "Pstwcx_" [Ireg ir1; Ireg ir2; Ireg ir3] | Psubfc (ir1,ir2,ir3) - | Psubfc64 (ir1,ir2,ir3) -> instruction "Psubfc" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psubfe (ir1,ir2,ir3) -> instruction "Psubfe" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psubfze (ir1,ir2) -> instruction "Psubfze" [Ireg ir1; Ireg ir2] - | Psubfic (ir1,ir2,c) -> instruction "Psubfic" [Ireg ir1; Ireg ir2; Constant c] - | Psubfic64 (ir1,ir2,n) -> instruction "Psubfic" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Psync -> instruction "Psync" [] - | Ptrap -> instruction "Ptrap" [] + | Psubfc64 (ir1,ir2,ir3) -> instruction pp "Psubfc" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psubfe (ir1,ir2,ir3) -> instruction pp "Psubfe" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psubfze (ir1,ir2) -> instruction pp "Psubfze" [Ireg ir1; Ireg ir2] + | Psubfic (ir1,ir2,c) -> instruction pp "Psubfic" [Ireg ir1; Ireg ir2; Constant c] + | Psubfic64 (ir1,ir2,n) -> instruction pp "Psubfic" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Psync -> instruction pp "Psync" [] + | Ptrap -> instruction pp "Ptrap" [] | Pxor (ir1,ir2,ir3) - | Pxor64 (ir1,ir2,ir3) -> instruction "Pxor" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pxori (ir1,ir2,c) -> instruction "Pxori" [Ireg ir1; Ireg ir2; Constant c] - | Pxori64 (ir1,ir2,n) -> instruction "Pxori" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Pxoris (ir1,ir2,c) -> instruction "Pxoris" [Ireg ir1; Ireg ir2; Constant c] - | Pxoris64 (ir1,ir2,n) -> instruction "Pxoris" [Ireg ir1; Ireg ir2; Constant (Cint n)] - | Plabel l -> instruction "Plabel" [ALabel l] + | Pxor64 (ir1,ir2,ir3) -> instruction pp "Pxor" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pxori (ir1,ir2,c) -> instruction pp "Pxori" [Ireg ir1; Ireg ir2; Constant c] + | Pxori64 (ir1,ir2,n) -> instruction pp "Pxori" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Pxoris (ir1,ir2,c) -> instruction pp "Pxoris" [Ireg ir1; Ireg ir2; Constant c] + | Pxoris64 (ir1,ir2,n) -> instruction pp "Pxoris" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Plabel l -> instruction pp "Plabel" [ALabel l] | Pbuiltin (ef,_,_) -> begin match ef with | EF_inline_asm _ -> - instruction "Pinlineasm" [Id]; + instruction pp "Pinlineasm" [Id]; Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" - | _ -> () + | _ -> assert false end | Pcfi_adjust _ (* Only debug relevant *) - | Pcfi_rel_offset _ -> () in (* Only debug relevant *) - List.iter instruction ic + | Pcfi_rel_offset _ -> assert false in (* Only debug relevant *) + pp_jarray instruction pp ic -let p_storage oc static = - p_jstring oc (if static then "Static" else "Extern") +let pp_storage pp static = + pp_jstring pp (if static then "Static" else "Extern") -let p_section oc = function - | Section_text -> fprintf oc "{\"Section Name\":\"Text\"}" - | Section_data init -> fprintf oc "{\"Section Name\":\"Data\",\"Init\":%B}" init - | Section_small_data init -> fprintf oc "{\"Section Name\":\"Small Data\",\"Init\":%B}" init - | Section_const init -> fprintf oc "{\"Section Name\":\"Const\",\"Init\":%B}" init - | Section_small_const init -> fprintf oc "{\"Section Name\":\"Small Const\",\"Init\":%B}" init - | Section_string -> fprintf oc "{\"Section Name\":\"String\"}" - | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" - | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" - | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":\"%s\",\"Writable\":%B,\"Executable\":%B}" s w e +let pp_section pp = function + | Section_text -> fprintf pp "{\"Section Name\":\"Text\"}" + | Section_data init -> fprintf pp "{\"Section Name\":\"Data\",\"Init\":%B}" init + | Section_small_data init -> fprintf pp "{\"Section Name\":\"Small Data\",\"Init\":%B}" init + | Section_const init -> fprintf pp "{\"Section Name\":\"Const\",\"Init\":%B}" init + | Section_small_const init -> fprintf pp "{\"Section Name\":\"Small Const\",\"Init\":%B}" init + | Section_string -> fprintf pp "{\"Section Name\":\"String\"}" + | Section_literal -> fprintf pp "{\"Section Name\":\"Literal\"}" + | Section_jumptable -> fprintf pp "{\"Section Name\":\"Jumptable\"}" + | Section_user (s,w,e) -> fprintf pp "{\"Section Name\":\"%s\",\"Writable\":%B,\"Executable\":%B}" s w e | Section_debug_info _ | Section_debug_abbrev | Section_debug_line _ @@ -356,73 +362,58 @@ let p_section oc = function | Section_debug_ranges | Section_debug_str -> () (* There should be no info in the debug sections *) -let p_int_opt oc = function - | None -> fprintf oc "0" - | Some i -> fprintf oc "%d" i +let pp_int_opt pp = function + | None -> fprintf pp "0" + | Some i -> fprintf pp "%d" i -let p_fundef oc (name,f) = +let pp_fundef pp (name,f) = let alignment = atom_alignof name and inline = atom_is_inline name and static = atom_is_static name and c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in - output_string oc "{"; - p_jmember oc "Fun Name" p_atom name; - p_sep oc; - p_jmember oc "Fun Storage Class" p_storage static; - p_sep oc; - p_jmember oc "Fun Alignment" p_int_opt alignment; - p_sep oc; - p_jmember oc "Fun Section Code" p_section c_section; - p_sep oc; - p_jmember oc "Fun Section Literals" p_section l_section; - p_sep oc; - p_jmember oc "Fun Section Jumptable" p_section j_section; - p_sep oc; - p_jmember oc "Fun Inline" p_jbool inline; - p_sep oc; - p_jmember oc "Fun Code" (fun oc a -> fprintf oc "[%a]" p_instruction a) f.fn_code; - output_string oc "}\n" - + pp_jobject_start pp; + pp_jmember ~first:true pp "Fun Name" pp_atom name; + pp_jmember pp "Fun Storage Class" pp_storage static; + pp_jmember pp "Fun Alignment" pp_int_opt alignment; + pp_jmember pp "Fun Section Code" pp_section c_section; + pp_jmember pp "Fun Section Literals" pp_section l_section; + pp_jmember pp "Fun Section Jumptable" pp_section j_section; + pp_jmember pp "Fun Inline" pp_jbool inline; + pp_jmember pp "Fun Code" pp_instructions f.fn_code; + pp_jobject_end pp -let p_init_data oc = function - | Init_int8 ic -> p_jsingle_object oc "Init_int8" p_int ic - | Init_int16 ic -> p_jsingle_object oc "Init_int16" p_int ic - | Init_int32 ic -> p_jsingle_object oc "Init_int32" p_int ic - | Init_int64 lc -> p_jsingle_object oc "Init_int64" p_int64 lc - | Init_float32 f -> p_jsingle_object oc "Init_float32" p_float32 f - | Init_float64 f -> p_jsingle_object oc "Init_float64" p_float64 f - | Init_space z -> p_jsingle_object oc "Init_space" p_z z +let pp_init_data pp = function + | Init_int8 ic -> pp_jsingle_object pp "Init_int8" pp_int ic + | Init_int16 ic -> pp_jsingle_object pp "Init_int16" pp_int ic + | Init_int32 ic -> pp_jsingle_object pp "Init_int32" pp_int ic + | Init_int64 lc -> pp_jsingle_object pp "Init_int64" pp_int64 lc + | Init_float32 f -> pp_jsingle_object pp "Init_float32" pp_float32 f + | Init_float64 f -> pp_jsingle_object pp "Init_float64" pp_float64 f + | Init_space z -> pp_jsingle_object pp "Init_space" pp_z z | Init_addrof (p,i) -> - let p_addr_of oc (p,i) = - output_string oc "{"; - p_jmember oc "Addr" p_atom p; - p_sep oc; - p_jmember oc "Offset" p_int i; - output_string oc "}" in - p_jsingle_object oc "Init_addrof" p_addr_of (p,i) + let pp_addr_of pp (p,i) = + pp_jobject_start pp; + pp_jmember ~first:true pp "Addr" pp_atom p; + pp_jmember pp "Offset" pp_int i; + pp_jobject_end pp in + pp_jsingle_object pp "Init_addrof" pp_addr_of (p,i) -let p_vardef oc (name,v) = +let pp_vardef pp (name,v) = let alignment = atom_alignof name and static = atom_is_static name and section = match (atom_sections name) with [s] -> s | _ -> assert false in(* Should only have one section *) - output_string oc "{"; - p_jmember oc "Var Name" p_atom name; - p_sep oc; - p_jmember oc "Var Readonly" p_jbool v.gvar_readonly; - p_sep oc; - p_jmember oc "Var Volatile" p_jbool v.gvar_volatile; - p_sep oc; - p_jmember oc "Var Storage Class" p_storage static; - p_sep oc; - p_jmember oc "Var Alignment" p_int_opt alignment; - p_sep oc; - p_jmember oc "Var Section" p_section section; - p_sep oc; - p_jmember oc "Var Init" (p_jarray p_init_data) v.gvar_init; - output_string oc "}\n" + pp_jobject_start pp; + pp_jmember ~first:true pp "Var Name" pp_atom name; + pp_jmember pp "Var Readonly" pp_jbool v.gvar_readonly; + pp_jmember pp "Var Volatile" pp_jbool v.gvar_volatile; + pp_jmember pp "Var Storage Class" pp_storage static; + pp_jmember pp "Var Alignment" pp_int_opt alignment; + pp_jmember pp "Var Section" pp_section section; + pp_jmember pp "Var Init" (pp_jarray pp_init_data) v.gvar_init; + pp_jobject_end pp -let p_program oc prog = +let pp_program pp prog = reset_id (); let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> match def with @@ -433,6 +424,7 @@ let p_program oc prog = vars,funs | Gvar v -> (ident,v)::vars,funs | _ -> vars,funs) ([],[]) prog.prog_defs in - fprintf oc "{\"Global Variables\":%a,\n\"Functions\":%a}" - (p_jarray p_vardef) prog_vars - (p_jarray p_fundef) prog_funs + pp_jobject_start pp; + pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars; + pp_jmember pp "Functions" (pp_jarray pp_fundef) prog_funs; + pp_jobject_end pp diff --git a/powerpc/AsmToJSON.mli b/powerpc/AsmToJSON.mli index 20bcba5e..e4d9c39a 100644 --- a/powerpc/AsmToJSON.mli +++ b/powerpc/AsmToJSON.mli @@ -10,4 +10,4 @@ (* *) (* *********************************************************************) -val p_program: out_channel -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit +val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit diff --git a/riscV/AsmToJSON.ml b/riscV/AsmToJSON.ml index 3580b618..ea22bdab 100644 --- a/riscV/AsmToJSON.ml +++ b/riscV/AsmToJSON.ml @@ -14,5 +14,5 @@ (* Dummy function *) -let p_program oc prog = - () +let pp_program pp prog = + Format.fprintf pp "null" diff --git a/x86/AsmToJSON.ml b/x86/AsmToJSON.ml index 3214491f..ca18999a 100644 --- a/x86/AsmToJSON.ml +++ b/x86/AsmToJSON.ml @@ -13,5 +13,5 @@ (* Simple functions to serialize ia32 Asm to JSON *) (* Dummy function *) -let p_program oc prog = - () +let pp_program pp prog = + Format.fprintf pp "null" diff --git a/x86/AsmToJSON.mli b/x86/AsmToJSON.mli index 20bcba5e..e4d9c39a 100644 --- a/x86/AsmToJSON.mli +++ b/x86/AsmToJSON.mli @@ -10,4 +10,4 @@ (* *) (* *********************************************************************) -val p_program: out_channel -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit +val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit |