aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
* make Aarch64 muladd depend on the optionDavid Monniaux2020-05-062-4/+10
|
* Adding copyrightsCyril SIX2020-05-043-0/+38
|
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-202-3/+10
|\
| * test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
| |
| * adapting new stuff for ARM and AArch64David Monniaux2020-04-011-3/+8
| |
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-123-1/+43
|\ \
| * | fix for aarch64David Monniaux2020-04-111-1/+1
| | |
| * | fix writing profiling info for Aarch64David Monniaux2020-04-101-1/+7
| | |
| * | use proper local labelsDavid Monniaux2020-04-101-1/+1
| | |
| * | profiling still crashes on Aarch64David Monniaux2020-04-101-1/+0
| | |
| * | various fixes for aarch64 profilingDavid Monniaux2020-04-103-1/+38
| |/
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-087-340/+751
|\|
| * disable leaf function removal of return address restoration due to memcpy ↵David Monniaux2020-03-273-7/+13
| | | | | | | | overwriting the return address register
| * Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-273-5/+38
| |\
| | * better epilogue proofDavid Monniaux2020-03-251-8/+18
| | |
| | * removed RA restorationDavid Monniaux2020-03-253-4/+27
| | |
| * | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-262-225/+532
| |\|
| | * RA is preservedDavid Monniaux2020-03-252-18/+36
| | |
| | * proof forwardDavid Monniaux2020-03-251-1/+4
| | |
| | * proof forwardDavid Monniaux2020-03-251-5/+15
| | |
| | * proof forwardDavid Monniaux2020-03-251-6/+24
| | |
| | * Asmgenproof1David Monniaux2020-03-241-1/+3
| | |
| | * transl_addressing_correctDavid Monniaux2020-03-241-4/+9
| | |
| | * transl_op_correctDavid Monniaux2020-03-241-10/+14
| | |
| | * transl_condDavid Monniaux2020-03-241-143/+332
| | |
| | * progress in proofs about RADavid Monniaux2020-03-242-36/+92
| | |
| | * exec_straight_stepsDavid Monniaux2020-03-241-5/+7
| | | | | | | | | | | | | | | exec_straight_steps_goto exec_straight_opt_steps_goto
| * | fix for aarch64 DuplicateOpcodeHeuristic.mlDavid Monniaux2020-03-171-3/+27
| | |
| * | fix for aarch64David Monniaux2020-03-031-11/+9
| | |
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-032-0/+150
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | aarch64David Monniaux2020-03-032-0/+150
| | |/
| * | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-039-35/+193
| |\ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-107/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions.
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-252-10/+22
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-242-10/+22
| |\| | | | |/ | |/| | | | mppa-work-upstream-merge
| | * AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
| | | | | | | | | | | | | | | | | | | | | According to AAPCS64 (the AArch64 ABI specification), the top bits of the register containing the function result have unspecified value, so we need to sign- or zero-extend the function result before using it, as in the x86 port.
| | * Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized.
| | * Refine the type of function results in AST.signatureXavier Leroy2020-02-212-10/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* | | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-1/+3
|/ /
* | stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-071-0/+3
| |
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-153-24/+54
|\ \
| * | 2-instruction signed division by two on Aarch64David Monniaux2020-01-153-24/+54
| |/
| * Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-033-1/+8
| | | | | | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
| * Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-213-8/+1
| | | | | | | | | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-12-161-1/+1
|\|
| * The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-12-094-5/+26
|\| | | | | | | mppa-work-upstream-merge
| * Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-283-2/+8
| | | | | | | | | | | | | | | | | | 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.
| * Added dwarf register numbers for aarch64Bernhard Schommer2019-11-281-3/+18
| |
* | trapping opsDavid Monniaux2019-09-241-0/+30
| |
generated by cgit (git 2.34.1) at 2024-07-07 01:44:40 +0000