diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-16 14:48:50 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-16 14:48:50 +0100 |
| commit | 341d1123c475e3fb73032e2f6c6a337c4e2c59c1 (patch) | |
| tree | 710a667568170aee285e357cca1eddb4319a2414 /aarch64/Asmblockgen.v | |
| parent | 21f6353cfbed8192c63bc44551ab3c1b5bf7d85a (diff) | |
| download | compcert-kvx-341d1123c475e3fb73032e2f6c6a337c4e2c59c1.tar.gz compcert-kvx-341d1123c475e3fb73032e2f6c6a337c4e2c59c1.zip | |
intermediatet commit before builtins
Diffstat (limited to 'aarch64/Asmblockgen.v')
| -rw-r--r-- | aarch64/Asmblockgen.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 96e7db4b..e260bd69 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -389,9 +389,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 +(* 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 + 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 @@ -400,9 +400,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 +(* 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 + 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 @@ -1141,8 +1141,11 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c) | MBop op args res => transl_op op args res k - | MBload _ chunk addr args dst => - transl_load chunk addr args dst k + | MBload t chunk addr args dst => + match t with + | TRAP => transl_load chunk addr args dst k + | NOTRAP => Error(msg "Asmgenblock.transl_instr_basic: NOTRAP load not supported in aarch64.") + end | MBstore chunk addr args src => transl_store chunk addr args src k end. |