aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | | 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.
* | | | | | Allowing non-consec store, and cleaningLéo Gourdin2020-12-111-8/+41
| | | | | |
* | | | | | Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-109-539/+551
| |_|_|/ / |/| | | |
* | | | | Peephole finished for nowLéo Gourdin2020-12-101-86/+211
| | | | |
* | | | | Non conseq storesLéo Gourdin2020-12-091-39/+87
| | | | |
* | | | | Non conseq loads in peepholeLéo Gourdin2020-12-091-82/+192
| | | | |
* | | | | Ocaml peephole oracle and array datastruct instead of listsLéo Gourdin2020-12-083-181/+246
| | | | |
* | | | | Some cleanup in todosLéo Gourdin2020-12-074-624/+13
| | | | |
* | | | | Simplifications in Peephole and size proof.Léo Gourdin2020-12-072-116/+48
| | | | |
* | | | | Simplification by merging fixpointsLéo Gourdin2020-12-071-21/+96
| | | | |
* | | | | peephole optLéo Gourdin2020-12-071-4/+3
| | | | |
* | | | | Asmgen proof completely proved with ldp/stpLéo Gourdin2020-12-066-133/+198
| | | | |
* | | | | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-0413-205/+640
| | | | |
* | | | | Adding semantics for PldpLéo Gourdin2020-12-0210-123/+215
| | | | | | | | | | | | | | | This commit prepare the backend for a peephole optimization in Asmblock.
* | | | | add option in scheduler to record bb sizeLéo Gourdin2020-11-301-0/+5
| | | | |
* | | | | Merge remote-tracking branch 'origin/aarch64-prepass+postpass' into ↵Léo Gourdin2020-11-3010-1545/+1056
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | aarch64-finetuningtest
| * \ \ \ \ Merge remote-tracking branch 'origin/aarch64-postpass' into ↵David Monniaux2020-11-281-58/+92
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | aarch64-prepass+postpass
| * \ \ \ \ \ Merge branch 'kvx-test-prepass' of ↵David Monniaux2020-11-2710-1545/+1056
| |\ \ \ \ \ \ | | | |_|_|/ / | | |/| | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass
| | * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-4/+76
| | |\ \ \ \ \
| | * | | | | | 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
| | | |_|/ / / | | |/| | | |
* | | | | | | Changing weights system at asmblock level instead of asmLéo Gourdin2020-11-302-537/+154
| | | | | | |
* | | | | | | Some optimizations againLéo Gourdin2020-11-281-27/+30
| |_|_|/ / / |/| | | | |
* | | | | | Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-postpassLéo Gourdin2020-11-283-4/+90
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/kvx-work' into aarch64-postpassDavid Monniaux2020-11-273-4/+90
| |\ \ \ \ \ | | | |_|_|/ | | |/| | |
| | * | | | pointer_eq copiedDavid Monniaux2020-11-251-0/+14
| | | |/ / | | |/| |
| | * | | fix wrong version of file on AArch64David Monniaux2020-11-231-1/+4
| | | | |
| | * | | fix bug #223 on AArch64David Monniaux2020-11-231-3/+72
| | |/ /
generated by cgit (git 2.34.1) at 2024-07-06 15:29:43 +0000