diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-12-15 00:01:30 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2017-12-15 00:01:30 +0100 |
| commit | 73ab7968d862c4d4d883fb3d3215353eba905b0f (patch) | |
| tree | ed09a92dc480a54eb26987e66d3dfb83fbe03de7 /arm/AsmToJSON.ml | |
| parent | cdf6681b3450baa1489c6a62e1903a450c0e2c3f (diff) | |
| download | compcert-kvx-73ab7968d862c4d4d883fb3d3215353eba905b0f.tar.gz compcert-kvx-73ab7968d862c4d4d883fb3d3215353eba905b0f.zip | |
Introduce 'cmn' instruction and optimize compare-with-immediate when negated immediates can be encoded.
Diffstat (limited to 'arm/AsmToJSON.ml')
| -rw-r--r-- | arm/AsmToJSON.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index e105ea20..85ef0603 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -20,7 +20,7 @@ open Camlcoq open Json let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic"; "Pblreg"; - "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pconstants";"Pfcpy_iif"; + "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"; @@ -207,6 +207,7 @@ let pp_instructions pp ic = | Pbtbl(r, tbl) -> instruction pp "Pbtbl" ((Ireg r)::(List.map (fun a -> ALabel a) tbl)) | Pclz(r1, r2) -> instruction pp "Pclz" [Ireg r1; Ireg r2] | Pcmp(r1,so) -> instruction pp "Pcmp" [Ireg r1; Shift so] + | Pcmn(r1,so) -> instruction pp "Pcmn" [Ireg r1; Shift so] | Pdmb -> instruction pp "Pdmb" [] | Pdsb -> instruction pp "Pdsb" [] | Peor(r1, r2, so) -> instruction pp "Peor" [Ireg r1; Ireg r2; Shift so] |