aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* 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
* | | 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
| |/
* | 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
* | Main part of postpasssch proof now completedLéo Gourdin2020-11-247-3884/+108
* | Asmblockdeps is now finishedLéo Gourdin2020-11-241-226/+42
* | Start of the postpasschedproof, redefining verify schedule lemmasLéo Gourdin2020-11-234-172/+272
* | a step forward in bblock_simu_reduceSylvain Boulmé2020-11-231-40/+34
* | Trying to finish the bisimu reduce proof for builtin (last case admitted)Léo Gourdin2020-11-202-30/+77
* | draft of the exec_bblock Asmblockdeps proofLéo Gourdin2020-11-203-35/+137
* | Postpass scheduling OKLéo Gourdin2020-11-183-323/+77
* | fix the semantics ?Sylvain Boulmé2020-11-182-3/+11
* | Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-postpassLéo Gourdin2020-11-171-7/+56
|\ \
| * | extend the aarch64 scheduling verifier to check builtins.Sylvain Boulmé2020-11-171-7/+56
* | | Builtin mem spec in scheduler and some needed proof in Postpasssch.vLéo Gourdin2020-11-173-5/+6
|/ /
* | Remaining ctl insts except Pbuiltin (maps to error)Léo Gourdin2020-11-162-400/+538
* | Lemma for bisimu with potential builtins, alloc and constantLéo Gourdin2020-11-131-65/+132
* | Loads and stores opLéo Gourdin2020-11-132-31/+238
* | Arith inst OK for the verifierLéo Gourdin2020-11-122-67/+227
* | Verifier is now enabled with debug printsLéo Gourdin2020-11-111-7/+6
* | Finishing PArith cases in abb, and linking the pass to compileLéo Gourdin2020-11-111-387/+479
* | PArithCmpR0R in checkerLéo Gourdin2020-11-111-36/+130
* | PArithComparison special lemmas and adaptationsLéo Gourdin2020-11-101-17/+315
* | Simplifications using ltacs and XZR special caseLéo Gourdin2020-11-101-33/+150
* | First version of the oracle checker, does not compile yetLéo Gourdin2020-11-093-837/+590
generated by cgit (git 2.34.1) at 2024-06-12 17:54:21 +0000