aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* intermediatet commit before builtinsLéo Gourdin2020-12-165-98/+3291
* Generals lemmas for asmblockgenproofLéo Gourdin2020-12-144-13/+896
* Removing the PseudoAsm IRLéo Gourdin2020-12-136-44/+301
* 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
* add option in scheduler to record bb sizeLéo Gourdin2020-11-301-0/+5
* Merge remote-tracking branch 'origin/aarch64-prepass+postpass' into aarch64-f...Léo Gourdin2020-11-3010-1545/+1056
|\
| * Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-prepass+p...David Monniaux2020-11-281-58/+92
| |\
| * \ Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-2710-1545/+1056
| |\ \
| | * \ 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
| | |/
* | / Optimizing Asmblockdeps proofLéo Gourdin2020-11-281-58/+92
|/ /
* | Merge branch 'aarch64_Pfmovimm_tuning' into aarch64-postpassLéo Gourdin2020-11-265-259/+143
|\ \
| * | Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-265-288/+148
| * | Fine tuning for PfmovimmLéo Gourdin2020-11-264-27/+51
* | | finish Asmgenproof.transf_program_correctSylvain Boulmé2020-11-261-5/+15
* | | Fixing a generation bug on shrx in AsmblockgenLéo Gourdin2020-11-261-0/+6
|/ /
* | This commit fix the issue #226Léo Gourdin2020-11-261-50/+57
* | Removing OrigAsmgen by moving the necessary functions in Asmgen.v Léo Gourdin2020-11-253-285/+80
* | Preservation proof with post pass scheduling in Asmgenproof almost doneLéo Gourdin2020-11-252-14/+14
* | Restoring asmgenproof on multiple labels issueLéo Gourdin2020-11-242-176/+29