aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
...
* | | | 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
* | | 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
* | | Preparing the repo for debugging postpass and executing testsLéo Gourdin2020-11-062-31/+32
* | | set debug to false in oracleLéo Gourdin2020-11-051-1/+1
* | | A first (not well-tuned) working version of postpass scheduling for A64Léo Gourdin2020-11-052-1004/+1066
* | | Smart scheduler build problem and flatten solution OKLéo Gourdin2020-11-044-258/+374
* | | Dumb (identity) scheduling working and integratedLéo Gourdin2020-11-037-869/+2356
* | | Some adaptations on PostpassScheduling for aarch64, and defs in AsmblockLéo Gourdin2020-11-022-71/+47
* | | Author and stash single label Asmgenproof after mergeLéo Gourdin2020-11-022-0/+2246
* | | Merge branch 'aarch64_block_multiple_labels' into aarch64-postpassLéo Gourdin2020-11-022-28/+175
|\ \ \
| * | | Yarpgen C file to test multiple labels and corresponding codeLéo Gourdin2020-11-012-28/+175
* | | | Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-0213-81/+5515
|/ / /
* | | End of Asmblock translationLéo Gourdin2020-10-291-38/+36
* | | Bugfix in AsmgenLéo Gourdin2020-10-291-1/+1
* | | Found a bug in Asmgen about iregsp constructorLéo Gourdin2020-10-291-9/+9
* | | Some tests and load/store instrLéo Gourdin2020-10-291-26/+145
* | | If, op, and some tests with a scriptLéo Gourdin2020-10-281-6/+701
* | | Epilogue OK and loadimmLéo Gourdin2020-10-271-58/+96
* | | Merge remote-tracking branch 'origin/aarch64_asmblockgen' into aarch64_blockLéo Gourdin2020-10-271-47/+52
|\ \ \
| * | | another start for AsmblockgenSylvain Boulmé2020-10-271-131/+52
* | | | A more convenient way to handle basic instLéo Gourdin2020-10-271-99/+18
|/ / /
generated by cgit (git 2.34.1) at 2024-07-06 15:21:32 +0000