| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
| |
There was an issue with the register PC in the eval_BA constructor for builtin : we were not able to prove that the concerned reg was different from PC.
This commit modify the definitions in Asmgen and Asmblock to support this, by replacing the parameter with a dreg instead of a preg.
|
|
|
|
|
|
| |
Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be
a misnomer since not all iregs are data regs)
TODO: Adjust names of PArithP, PArithPP and the like
|
|
|
|
|
|
|
| |
The previous version of unfold_bblock was copied from kvx/Asm.v. kvx's
version is slightly different in that for the (here removed) special
case it does not put a semicolon to separate bundles. Since aarch64 does
not have kvx's bundles the two versions should be equivalent.
|
| |
|
|
|
|
|
| |
Previously Asmblock.label_pos and Asm.label_pos could point to different
memory location for the same label.
|
|
|
|
|
|
| |
instructions otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions"
-- From the original aarch64/Asmgen.v
|
|
|
|
|
|
|
| |
In Asmblock, Pcsel is used for both integer and floating-point
conditional selection.
A previous commit (c764ff84) had incorrectly reverted the merging of
Pfsel into Pcsel.
|
| |
|
|
|
|
|
|
|
|
| |
Largely semi-automatically generated with vim regexes and macros. Right
now the only interesting case is Pmovk: here we ckeck that on the
Asmblock level the source and target register are the same. Then, we
can safely translate to Asm's Pmovk which takes a single register
(mutating it in-place).
|
| |
|
| |
|
|
|
|
| |
overwriting the return address register
|
|\ |
|
| | |
|
|\ \ |
|
| |/ |
|
|\|
| |
| |
| | |
mppa-work-upstream-merge
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/
|
|
| |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
|
|
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|