aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
* fix new register erasing scheme for AArch64David Monniaux2020-12-083-553/+241
|
* Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-082-8/+11
|\
| * AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | | | | | | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
* | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-175/+1231
|\ \ | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-4/+76
| |\ \
| | * | fix wrong version of file on AArch64David Monniaux2020-11-231-1/+4
| | | |
| | * | fix bug #223 on AArch64David Monniaux2020-11-231-3/+72
| | | |
| * | | disable debug printing in schedulerDavid Monniaux2020-11-041-3/+5
| | | |
| * | | new OpWeights for aarch64David Monniaux2020-10-221-318/+342
| | | |
| * | | allow changing target cpuDavid Monniaux2020-10-222-21/+40
| | | |
| * | | prefix all calls to OpWeights as preparation to using a structureDavid Monniaux2020-10-221-14/+14
| | | |
| * | | op_valid_pointer_eq for aarch64David Monniaux2020-10-191-0/+14
| | | |
| * | | so that all architectures compileDavid Monniaux2020-10-021-0/+473
| | | |
| * | | non trapping opDavid Monniaux2020-09-304-88/+73
| | | |
| * | | non trappingDavid Monniaux2020-09-301-2/+0
| | | |
| * | | AArch64 division no longer "traps"David Monniaux2020-09-306-81/+221
| | | |
| * | | floating-point division uses the divisorDavid Monniaux2020-09-291-4/+5
| | | |
| * | | attempt at separating the divisionsDavid Monniaux2020-09-291-0/+5
| | | |
| * | | try to model resourcesDavid Monniaux2020-09-291-5/+164
| | | |
| * | | attempt at latencies for Cortex A53David Monniaux2020-09-291-2/+147
| | | |
| * | | first opweights, bogus weightsDavid Monniaux2020-09-161-0/+19
| |/ /
* | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-33/+34
|\ \ \ | |/ / |/| / | |/
| * Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| | | | | | | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035
| * Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib.
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| * Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-8/+0
| | | | | | | | These functions are now available on all targets.
| * AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| | | | | | | | Using the "rbit" instruction (reverse bits).
| * No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | | | | | | | __builtin_fabs has already been expanded in backend/Selection.v .
| * Move shared code in new file.Bernhard Schommer2020-06-281-17/+0
| | | | | | | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
| * Remove the `can_reserve_register` function.Bernhard Schommer2020-06-281-2/+0
| | | | | | | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
| * Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
| * Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
| | | | | | | | | | | | The corresponding files in all other ports are dual-licensed (GPL + non-commercial), there is no reason it should be different for aarch64.
* | 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
| | | |
generated by cgit (git 2.34.1) at 2024-07-04 02:27:38 +0000