aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2019-11-28 17:00:27 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2019-11-28 17:00:27 +0100
commita99406bbd9c01dc04e79b14681a254fe22c9d424 (patch)
treeb7901f046fbf73617ff4a0f810830cabcd876fdd /cfrontend
parent5dcd78a4382992e92955ec0614fc2f5c4f80c429 (diff)
downloadcompcert-a99406bbd9c01dc04e79b14681a254fe22c9d424.tar.gz
compcert-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 'cfrontend')
-rw-r--r--cfrontend/C2C.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index c1dfa9f4..9ae7bbd9 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -61,6 +61,11 @@ let atom_alignof a =
with Not_found ->
None
+let atom_is_aligned a sz =
+ match atom_alignof a with
+ | None -> false
+ | Some align -> align mod (Z.to_int sz) = 0
+
let atom_sections a =
try
(Hashtbl.find decl_atom a).a_sections