diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-09 15:09:08 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-09 15:09:08 +0100 |
| commit | 7429e1f28da407de3dc64de9394dc4eab9c783a8 (patch) | |
| tree | 0402177a460a248939ed982bab763fe6ba909401 /aarch64/Asmgen.v | |
| parent | 37de1399449067121a8bb9a51a7cc7a043ad17e2 (diff) | |
| parent | ec49c7b8bd4502c380b88c78baa674000db109fd (diff) | |
| download | compcert-kvx-7429e1f28da407de3dc64de9394dc4eab9c783a8.tar.gz compcert-kvx-7429e1f28da407de3dc64de9394dc4eab9c783a8.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index c7332329..0c72c7cc 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -20,6 +20,11 @@ Local Open Scope string_scope. Local Open Scope list_scope. Local Open Scope error_monad_scope. +(** Alignment check for symbols *) + +Parameter symbol_is_aligned : ident -> Z -> bool. +(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) + (** Extracting integer or float registers. *) Definition ireg_of (r: mreg) : res ireg := @@ -942,7 +947,7 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) (insn (ADimm X16 Int64.zero) :: k)) | Aglobal id ofs, nil => assertion (negb (Archi.pic_code tt)); - if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero + if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k) else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k)) | Ainstack ofs, nil => |