diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2021-03-23 20:07:22 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-24 17:58:33 +0200 |
commit | 69e175746c27f340f544c329204d6ad030c3c347 (patch) | |
tree | 043304e5c7638dd52614df3f4035f6505feed992 /test/raytracer/simplify.h | |
parent | d36130f936a07773d925e83d595f27f8779cb3f3 (diff) | |
download | compcert-69e175746c27f340f544c329204d6ad030c3c347.tar.gz compcert-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 'test/raytracer/simplify.h')
0 files changed, 0 insertions, 0 deletions