diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:20:11 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:20:11 +0200 |
commit | 71cec9c9126ee4385ce12fd29dec557995d5a903 (patch) | |
tree | 26e86fc9b15680721baea86d5294ee9faaf2508c /arm | |
parent | 1801685f8352b7a120d87d5b529d290728129529 (diff) | |
parent | e1725209b2b4401adc63ce5238fa5db7c134609c (diff) | |
download | compcert-kvx-71cec9c9126ee4385ce12fd29dec557995d5a903.tar.gz compcert-kvx-71cec9c9126ee4385ce12fd29dec557995d5a903.zip |
Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'arm')
-rw-r--r-- | arm/AsmToJSON.ml | 40 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 4 |
2 files changed, 24 insertions, 20 deletions
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) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 75d32ea3..56534c04 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -757,7 +757,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). @@ -770,7 +770,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. |