diff options
-rw-r--r-- | arm/AsmToJSON.ml | 2 | ||||
-rw-r--r-- | arm/AsmToJSON.mli | 2 | ||||
-rw-r--r-- | driver/Driver.ml | 14 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 184 | ||||
-rw-r--r-- | powerpc/AsmToJSON.mli | 2 | ||||
-rw-r--r-- | riscV/AsmToJSON.ml | 2 | ||||
-rw-r--r-- | x86/AsmToJSON.ml | 2 | ||||
-rw-r--r-- | x86/AsmToJSON.mli | 2 |
8 files changed, 208 insertions, 2 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index 73706d3b..74c64180 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -16,3 +16,5 @@ let pp_program pp prog = Format.fprintf pp "null" + +let pp_mnemonics pp = () diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli index e4d9c39a..058a4e83 100644 --- a/arm/AsmToJSON.mli +++ b/arm/AsmToJSON.mli @@ -11,3 +11,5 @@ (* *********************************************************************) val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit + +val pp_mnemonics: Format.formatter -> unit diff --git a/driver/Driver.ml b/driver/Driver.ml index a09aa95d..6996f537 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -311,6 +311,14 @@ let enforce_buildnr nr = Please use matching builds of QSK and CompCert.\n" build nr; exit 2 end +let dump_mnemonics destfile = + let oc = open_out_bin destfile in + let pp = Format.formatter_of_out_channel oc in + AsmToJSON.pp_mnemonics pp; + Format.pp_print_flush pp (); + close_out oc; + exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_passing; option_fvararg_calls; option_funprototyped; @@ -338,10 +346,12 @@ let cmdline_actions = (* Getting version info *) Exact "-version", Unit print_version_and_exit; Exact "--version", Unit print_version_and_exit;] @ -(* Enforcing CompCert build numbers for QSKs *) +(* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Version.buildnr <> "" then [ Exact "-qsk-enforce-build", Integer enforce_buildnr; - Exact "--qsk-enforce-build", Integer enforce_buildnr; ] + Exact "--qsk-enforce-build", Integer enforce_buildnr; + Exact "-dump-mnemonics", String dump_mnemonics; + ] else []) @ (* Processing options *) [ Exact "-c", Set option_c; diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 2017d3e3..fb36b9d7 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -112,6 +112,184 @@ 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" + ; "Paddi" + ; "Paddic" + ; "Paddis" + ; "Paddis" + ; "Paddze" + ; "Pand_" + ; "Pandc" + ; "Pandi_" + ; "Pandi_" + ; "Pandis_" + ; "Pandis_" + ; "Pb" + ; "Pbctr" + ; "Pbctrl" + ; "Pbdnz" + ; "Pbf" + ; "Pbl" + ; "Pbs" + ; "Pblr" + ; "Pbt" + ; "Pbtbl" + ; "Pcmpb" + ; "Pcmpld" + ; "Pcmpldi" + ; "Pcmplw" + ; "Pcmplwi" + ; "Pcmpd" + ; "Pcmpdi" + ; "Pcmpw" + ; "Pcmpwi" + ; "Pcntlzd" + ; "Pcntlzw" + ; "Pcreqv" + ; "Pcror" + ; "Pcrxor" + ; "Pdcbf" + ; "Pdcbi" + ; "Pdcbt" + ; "Pdcbtst" + ; "Pdcbtls" + ; "Pdcbz" + ; "Pdivw" + ; "Pdivd" + ; "Pdivwu" + ; "Pdivdu" + ; "Peieio" + ; "Peqv" + ; "Pextsb" + ; "Pextsh" + ; "Pextsw" + ; "Pfabs" + ; "Pfadd" + ; "Pfadds" + ; "Pfcmpu" + ; "Pfcfid" + ; "Pfctidz" + ; "Pfctiw" + ; "Pfctiwz" + ; "Pfdiv" + ; "Pfdivs" + ; "Pfmr" + ; "Pfmul" + ; "Pfmuls" + ; "Pfneg" + ; "Pfrsp" + ; "Pfsub" + ; "Pfsubs" + ; "Pfmadd" + ; "Pfmsub" + ; "Pfnmadd" + ; "Pfnmsub" + ; "Pfsqrt" + ; "Pfrsqrte" + ; "Pfres" + ; "Pfsel" + ; "Pisel" + ; "Picbi" + ; "Picbtls" + ; "Pisync" + ; "Plwsync" + ; "Plbz" + ; "Plbzx" + ; "Pld" + ; "Pldx" + ; "Plfd" + ; "Plfdx" + ; "Plfs" + ; "Plfsx" + ; "Plha" + ; "Plhax" + ; "Plhbrx" + ; "Plhz" + ; "Plhzx" + ; "Pldi" + ; "Plfi" + ; "Plfis" + ; "Plwz" + ; "Plwzu" + ; "Plwzx" + ; "Plwarx" + ; "Plwbrx" + ; "Pmbar" + ; "Pmfcr" + ; "Pmflr" + ; "Pmr" + ; "Pmtctr" + ; "Pmtlr" + ; "Pmfspr" + ; "Pmtspr" + ; "Pmulhd" + ; "Pmulhdu" + ; "Pmulld" + ; "Pmulli" + ; "Pmullw" + ; "Pmulhw" + ; "Pmulhwu" + ; "Pnand" + ; "Pnor" + ; "Por" + ; "Porc" + ; "Pori" + ; "Pori" + ; "Poris" + ; "Poris" + ; "Prldicl" + ; "Prldinm" + ;"Prldimi" + ; "Prlwinm" + ;"Prlwimi" + ; "Psld" + ; "Pslw" + ; "Psrad" + ; "Psradi" + ; "Psraw" + ; "Psrawi" + ; "Psrd" + ; "Psrw" + ; "Pstb" + ; "Pstbx" + ; "Pstd" + ; "Pstdx" + ; "Pstdu" + ; "Pstfd" + ; "Pstfdu" + ; "Pstfdx" + ; "Pstfs" + ; "Pstfsx" + ; "Psth" + ; "Psthx" + ; "Psthbrx" + ; "Pstw" + ; "Pstwu" + ; "Pstwx" + ; "Pstwux" + ; "Pstwbrx" + ; "Pstwcx_" + ; "Psubfc" + ; "Psubfe" + ; "Psubfze" + ; "Psubfic" + ; "Psubfic" + ; "Psync" + ; "Ptrap" + ; "Pxor" + ; "Pxori" + ; "Pxori" + ; "Pxoris" + ; "Pxoris" + ; "Plabel" + ; "Pinlineasm" + ; "Pannot" + ] + let pp_instructions pp ic = let ic = List.filter (fun s -> match s with | Pbuiltin (ef,_,_) -> @@ -124,6 +302,7 @@ let pp_instructions pp ic = | Pcfi_rel_offset _ -> false | _ -> true) ic in let instruction pp n args = + assert (List.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; @@ -467,3 +646,8 @@ let pp_program pp prog = 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 + +let pp_mnemonics pp = + 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 diff --git a/powerpc/AsmToJSON.mli b/powerpc/AsmToJSON.mli index e4d9c39a..058a4e83 100644 --- a/powerpc/AsmToJSON.mli +++ b/powerpc/AsmToJSON.mli @@ -11,3 +11,5 @@ (* *********************************************************************) val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit + +val pp_mnemonics: Format.formatter -> unit diff --git a/riscV/AsmToJSON.ml b/riscV/AsmToJSON.ml index ea22bdab..1b2f7458 100644 --- a/riscV/AsmToJSON.ml +++ b/riscV/AsmToJSON.ml @@ -16,3 +16,5 @@ let pp_program pp prog = Format.fprintf pp "null" + +let pp_mnemonics pp = () diff --git a/x86/AsmToJSON.ml b/x86/AsmToJSON.ml index ca18999a..8488bfde 100644 --- a/x86/AsmToJSON.ml +++ b/x86/AsmToJSON.ml @@ -15,3 +15,5 @@ (* Dummy function *) let pp_program pp prog = Format.fprintf pp "null" + +let pp_mnemonics pp = () diff --git a/x86/AsmToJSON.mli b/x86/AsmToJSON.mli index e4d9c39a..058a4e83 100644 --- a/x86/AsmToJSON.mli +++ b/x86/AsmToJSON.mli @@ -11,3 +11,5 @@ (* *********************************************************************) val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit + +val pp_mnemonics: Format.formatter -> unit |