From 7d5db993033ce049776fa290ae1ebc6051dea0f3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sat, 17 Aug 2019 10:10:42 +0200 Subject: Fix compile for architectures other than AArch64 (#192) Some changes were not correctly propagated to all architectures. --- arm/SelectOpproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm') diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 5d54d94f..70f8f191 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -754,7 +754,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. + rewrite Val.zero_ext_and. apply eval_andimm. omega. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -767,7 +767,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. + rewrite Val.zero_ext_and. apply eval_andimm. omega. Qed. Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. -- cgit From a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 12 Sep 2019 17:03:14 +0200 Subject: Reworked json export. The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions --- arm/AsmToJSON.ml | 40 ++++++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 18 deletions(-) (limited to 'arm') diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index 6ba3f1bc..e850fed6 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) -- cgit