diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-26 12:19:10 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-26 12:19:10 +0100 |
| commit | 3f691c8c892c897791d2e9cef104f209f587abee (patch) | |
| tree | 081fea77c70842633ef1de9c6ec06f714c7e38c0 /aarch64/Asmblockgen.v | |
| parent | 02a86fb0cd2dcb63b8346c48ca78056b30c7fef6 (diff) | |
| download | compcert-kvx-3f691c8c892c897791d2e9cef104f209f587abee.tar.gz compcert-kvx-3f691c8c892c897791d2e9cef104f209f587abee.zip | |
Fixing a generation bug on shrx in Asmblockgen
I forgot this one and the gen test script reminds me
Diffstat (limited to 'aarch64/Asmblockgen.v')
| -rw-r--r-- | aarch64/Asmblockgen.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 268cd7fc..b25a95da 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -400,6 +400,9 @@ Definition arith_extended Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := if Int.eq n Int.zero then Pmov rd r1 ::bi k + else if Int.eq n Int.one then + Padd W (SOlsr (Int.repr 31)) X16 r1 r1 ::bi + Porr W (SOasr n) rd XZR X16 ::bi k else Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi @@ -408,6 +411,9 @@ Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode := if Int.eq n Int.zero then Pmov rd r1 ::bi k + else if Int.eq n Int.one then + Padd X (SOlsr (Int.repr 63)) X16 r1 r1 ::bi + Porr X (SOasr n) rd XZR X16 ::bi k else Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi |