diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-11-28 17:00:27 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-11-28 17:00:27 +0100 |
| commit | a99406bbd9c01dc04e79b14681a254fe22c9d424 (patch) | |
| tree | b7901f046fbf73617ff4a0f810830cabcd876fdd /aarch64 | |
| parent | 5dcd78a4382992e92955ec0614fc2f5c4f80c429 (diff) | |
| download | compcert-kvx-a99406bbd9c01dc04e79b14681a254fe22c9d424.tar.gz compcert-kvx-a99406bbd9c01dc04e79b14681a254fe22c9d424.zip | |
Fix for AArch64 alignment problem (#206)
In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time.
This PR extends the check for a representable offset for the addressing of global
variables to also check whether the variable is correctly aligned. Only if both conditions are
met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic
loadsymbol sequence.
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgen.v | 7 | ||||
| -rw-r--r-- | aarch64/Asmgenproof1.v | 2 | ||||
| -rw-r--r-- | aarch64/extractionMachdep.v | 1 |
3 files changed, 8 insertions, 2 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 1c0e41a1..875f3fd1 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 => diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 663ee50b..6d44bcc8 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -1592,7 +1592,7 @@ Proof. simpl; rewrite Int64.add_zero; auto. intros. apply C; eauto with asmgen. - (* Aglobal *) - destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero); inv TR. + destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. + econstructor; econstructor; split. apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto. split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v index a447d12f..e82056e2 100644 --- a/aarch64/extractionMachdep.v +++ b/aarch64/extractionMachdep.v @@ -21,3 +21,4 @@ Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) (* Asm *) Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false". +Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned". |