diff options
-rw-r--r-- | aarch64/Asmblockgen.v | 6 | ||||
-rwxr-xr-x | test/aarch64/gen_tests/asmb_aarch64_gen_test.sh | 8 |
2 files changed, 10 insertions, 4 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 diff --git a/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh b/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh index 660ff7aa..38235f14 100755 --- a/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh +++ b/test/aarch64/gen_tests/asmb_aarch64_gen_test.sh @@ -11,9 +11,9 @@ done DIRS=( ../c/*.c # Special simple tests - ../../c/*.c + #../../c/*.c ../../clightgen/*.c - ../../compression/*.c + #../../compression/*.c ../../cse2/*.c # Monniaux test directory @@ -36,7 +36,7 @@ DIRS=( ../../monniaux/lustrev4_lv6-en-2cgc_heater_control/*.c #../../monniaux/lustrev6-carlightV2/*.c # Warnings #../../monniaux/lustrev6-convertible-2cgc/*.c # Unsupported feature? - ../../monniaux/lustrev6-convertible-en-2cgc/*.c + #../../monniaux/lustrev6-convertible-en-2cgc/*.c #../../monniaux/lustrev6-convertible/*.c # Warnings ../../monniaux/madd/*.c #../../monniaux/math/*.c # Unsupported feature? @@ -59,7 +59,7 @@ DIRS=( ) #FILES=../c/*.c CCOMP_BBLOCKS="../../../ccomp -fno-postpass" -CCOMP_REF="../../../../CompCert_aarch64-ref/ccomp" +CCOMP_REF="../../../../CompCert_kvx/ccomp" COUNT=0 if [ $WOFF -eq 1 ] |