aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmexpand.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2021-03-23 20:07:22 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-04-24 17:58:33 +0200
commit69e175746c27f340f544c329204d6ad030c3c347 (patch)
tree043304e5c7638dd52614df3f4035f6505feed992 /powerpc/Asmexpand.ml
parentd36130f936a07773d925e83d595f27f8779cb3f3 (diff)
downloadcompcert-kvx-69e175746c27f340f544c329204d6ad030c3c347.tar.gz
compcert-kvx-69e175746c27f340f544c329204d6ad030c3c347.zip
Tentative first fix for offsets of ld/std.
The offsets immediates used in the ld and std instructions must be a multiple of the word size. This commit changes the two functions which are used when generating load/stores in Asmgen, accessind and transl_memory_access. For accessind one only needs an additional check that the offset is a multiple of the word size for the case that the high part of the offset is zero, since otherwise the immediate is loaded into a register anyway. The transl_memory_access function needs some slightly more complex adoption. For all variants that do not construct the address in a register before hand we must check that the offsets are multiples of the word size and additionally if a symbol is used that the alignment of the symbol is also a multiple of the word size. Therefore a new parameter is introduced that allows checking the alignment. In order to reduce the code duplication for the proofs these two functions get an additional parameter in order to indicate wether the offset needs to be a multiple of the word size or not. Bug 30983
Diffstat (limited to 'powerpc/Asmexpand.ml')
0 files changed, 0 insertions, 0 deletions